mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
fix issues #581: nested timeouts canceled each-other
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
a020b13f10
commit
e29adbf304
|
@ -272,8 +272,6 @@ public:
|
|||
cmd_context(bool main_ctx = true, ast_manager * m = 0, symbol const & l = symbol::null);
|
||||
~cmd_context();
|
||||
void set_cancel(bool f);
|
||||
void cancel() { set_cancel(true); }
|
||||
void reset_cancel() { set_cancel(false); }
|
||||
context_params & params() { return m_params; }
|
||||
solver_factory &get_solver_factory() { return *m_solver_factory; }
|
||||
solver_factory &get_interpolating_solver_factory() { return *m_interpolating_solver_factory; }
|
||||
|
|
|
@ -20,14 +20,6 @@ Revision History:
|
|||
|
||||
#include "model_based_opt.h"
|
||||
|
||||
std::ostream& operator<<(std::ostream& out, opt::bound_type bt) {
|
||||
switch (bt) {
|
||||
case opt::unbounded: return out << "unbounded";
|
||||
case opt::strict: return out << "strict";
|
||||
case opt::non_strict: return out << "non-strict";
|
||||
}
|
||||
return out;
|
||||
}
|
||||
|
||||
std::ostream& operator<<(std::ostream& out, opt::ineq_type ie) {
|
||||
switch (ie) {
|
||||
|
@ -128,8 +120,10 @@ namespace opt {
|
|||
return inf_eps::infinity();
|
||||
}
|
||||
}
|
||||
|
||||
//
|
||||
// update the evaluation of variables to satisfy the bound.
|
||||
//
|
||||
|
||||
update_values(bound_vars, bound_trail);
|
||||
|
||||
|
@ -164,10 +158,10 @@ namespace opt {
|
|||
SASSERT(!x_coeff.is_zero());
|
||||
val /= -x_coeff;
|
||||
// Adjust epsilon to be s
|
||||
if (eps.is_zero() || (!val.is_zero() && eps > abs(val))) {
|
||||
if (!val.is_zero() && (eps.is_zero() || eps > abs(val))) {
|
||||
eps = abs(val)/rational(2);
|
||||
}
|
||||
if (eps.is_zero() || (!r.m_value.is_zero() && eps > abs(r.m_value))) {
|
||||
if (!r.m_value.is_zero() && (eps.is_zero() || eps > abs(r.m_value))) {
|
||||
eps = abs(r.m_value)/rational(2);
|
||||
}
|
||||
//
|
||||
|
@ -186,10 +180,6 @@ namespace opt {
|
|||
// <=> x > t/a
|
||||
// <=> x := t/a + epsilon
|
||||
//
|
||||
|
||||
if (x_coeff.is_pos() && r.m_type == t_lt) {
|
||||
val -= eps;
|
||||
}
|
||||
else if (x_coeff.is_neg() && r.m_type == t_lt) {
|
||||
val += eps;
|
||||
}
|
||||
|
@ -265,48 +255,36 @@ namespace opt {
|
|||
}
|
||||
}
|
||||
|
||||
// v0 - v1 <= 0
|
||||
// v0 - v2 <= 0
|
||||
// v2 >= v1
|
||||
// -> v1 - v2 <= 0
|
||||
//
|
||||
// t1 + a1*x <= 0
|
||||
// t2 + a2*x <= 0
|
||||
// (t2 + a2*x) <= (t1 + a1*x)*a2/a1
|
||||
// => t2*a1/a2 - t1 <= 0
|
||||
// => t2 - t1*a2/a1 <= 0
|
||||
// Let
|
||||
// row1: t1 + a1*x <= 0
|
||||
// row2: t2 + a2*x <= 0
|
||||
//
|
||||
// assume a1, a2 have the same signs:
|
||||
// (t2 + a2*x) <= (t1 + a1*x)*a2/a1
|
||||
// <=> t2*a1/a2 - t1 <= 0
|
||||
// <=> t2 - t1*a2/a1 <= 0
|
||||
//
|
||||
// assume a1 > 0, -a2 < 0:
|
||||
// t1 + a1*x <= 0, t2 - a2*x <= 0
|
||||
// t2/a2 <= -t1/a1
|
||||
// t2 + t1*a2/a1 <= 0
|
||||
// assume -a1 < 0, a2 > 0:
|
||||
// t1 - a1*x <= 0, t2 + a2*x <= 0
|
||||
// t1/a1 <= -t2/a2
|
||||
// t2 + t1*a2/a1 <= 0
|
||||
//
|
||||
// the resolvent is the same in all cases (simpler proof should exist)
|
||||
//
|
||||
|
||||
bool model_based_opt::resolve(unsigned row_id1, rational const& a1, unsigned row_id2, unsigned x) {
|
||||
void model_based_opt::resolve(unsigned row_src, rational const& a1, unsigned row_dst, unsigned x) {
|
||||
|
||||
SASSERT(a1 == get_coefficient(row_id1, x));
|
||||
SASSERT(a1 == get_coefficient(row_src, x));
|
||||
SASSERT(!a1.is_zero());
|
||||
|
||||
//
|
||||
// row1 is of the form a1*x + t1 <~ 0
|
||||
// row2 is of the form a2*x + t2 <~ 0
|
||||
// assume that a1, a2 have the same sign.
|
||||
// if a1 is positive, then val(t1*a2/a1) <= val(t2*a1/a2)
|
||||
// replace row2 with the new inequality of the form:
|
||||
// t1 - a1*t2/a2 <~~ 0
|
||||
// where <~~ is strict if either <~1 or <~2 is strict.
|
||||
// if a1 is negative, then ....
|
||||
//
|
||||
|
||||
row& row2 = m_rows[row_id2];
|
||||
if (!row2.m_alive) {
|
||||
return false;
|
||||
}
|
||||
rational a2 = get_coefficient(row_id2, x);
|
||||
if (a2.is_zero()) {
|
||||
return false;
|
||||
}
|
||||
if (a1.is_pos() == a2.is_pos() || row2.m_type == t_eq) {
|
||||
mul_add(row_id2, -a2/a1, row_id1);
|
||||
return true;
|
||||
}
|
||||
else {
|
||||
row2.m_alive = false;
|
||||
return false;
|
||||
if (m_rows[row_dst].m_alive) {
|
||||
rational a2 = get_coefficient(row_dst, x);
|
||||
mul_add(row_dst, -a2/a1, row_src);
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -314,6 +292,9 @@ namespace opt {
|
|||
// set row1 <- row1 + c*row2
|
||||
//
|
||||
void model_based_opt::mul_add(unsigned row_id1, rational const& c, unsigned row_id2) {
|
||||
if (c.is_zero()) {
|
||||
return;
|
||||
}
|
||||
m_new_vars.reset();
|
||||
row& r1 = m_rows[row_id1];
|
||||
row const& r2 = m_rows[row_id2];
|
||||
|
@ -364,6 +345,9 @@ namespace opt {
|
|||
if (r2.m_type == t_lt) {
|
||||
r1.m_type = t_lt;
|
||||
}
|
||||
else if (r2.m_type == t_le && r1.m_type == t_eq) {
|
||||
r1.m_type = t_le;
|
||||
}
|
||||
SASSERT(invariant(row_id1, r1));
|
||||
}
|
||||
|
||||
|
|
|
@ -33,11 +33,6 @@ namespace opt {
|
|||
t_le
|
||||
};
|
||||
|
||||
enum bound_type {
|
||||
unbounded,
|
||||
strict,
|
||||
non_strict
|
||||
};
|
||||
|
||||
typedef inf_eps_rational<inf_rational> inf_eps;
|
||||
|
||||
|
@ -78,7 +73,7 @@ namespace opt {
|
|||
|
||||
rational get_coefficient(unsigned row_id, unsigned var_id);
|
||||
|
||||
bool resolve(unsigned row_id1, rational const& a1, unsigned row_id2, unsigned x);
|
||||
void resolve(unsigned row_src, rational const& a1, unsigned row_dst, unsigned x);
|
||||
|
||||
void mul_add(unsigned row_id1, rational const& c, unsigned row_id2);
|
||||
|
||||
|
@ -118,7 +113,6 @@ namespace opt {
|
|||
|
||||
}
|
||||
|
||||
std::ostream& operator<<(std::ostream& out, opt::bound_type bt);
|
||||
std::ostream& operator<<(std::ostream& out, opt::ineq_type ie);
|
||||
|
||||
|
||||
|
|
|
@ -238,6 +238,11 @@ namespace opt {
|
|||
import_scoped_state();
|
||||
normalize();
|
||||
internalize();
|
||||
#if 0
|
||||
if (is_qsat_opt()) {
|
||||
return run_qsat_opt();
|
||||
}
|
||||
#endif
|
||||
update_solver();
|
||||
solver& s = get_solver();
|
||||
s.assert_expr(m_hard_constraints);
|
||||
|
@ -1465,7 +1470,7 @@ namespace opt {
|
|||
term = m_arith.mk_uminus(term);
|
||||
}
|
||||
inf_eps value;
|
||||
lbool result = qe::maximize(m_hard_constraints, term, value, m_params);
|
||||
lbool result = qe::maximize(m_hard_constraints, term, value, m_model, m_params);
|
||||
if (result != l_undef && obj.m_type == O_MINIMIZE) {
|
||||
value.neg();
|
||||
}
|
||||
|
|
|
@ -403,7 +403,7 @@ namespace smt2 {
|
|||
void check_float(char const * msg) { if (!curr_is_float()) throw parser_exception(msg); }
|
||||
|
||||
void error(unsigned line, unsigned pos, char const * msg) {
|
||||
m_ctx.reset_cancel();
|
||||
m_ctx.set_cancel(false);
|
||||
if (use_vs_format()) {
|
||||
m_ctx.diagnostic_stream() << "Z3(" << line << ", " << pos << "): ERROR: " << msg;
|
||||
if (msg[strlen(msg)-1] != '\n')
|
||||
|
|
|
@ -968,32 +968,34 @@ namespace qe {
|
|||
|
||||
|
||||
opt::inf_eps maximize(expr_ref_vector const& fmls, model& mdl, app* t, expr_ref& bound) {
|
||||
SASSERT(a.is_real(t));
|
||||
opt::model_based_opt mbo;
|
||||
opt::inf_eps value;
|
||||
obj_map<expr, rational> ts;
|
||||
obj_map<expr, unsigned> tids;
|
||||
|
||||
// extract objective function.
|
||||
vars coeffs;
|
||||
rational c(0), mul(1);
|
||||
linearize(mdl, mul, t, c, ts);
|
||||
extract_coefficients(ts, tids, coeffs);
|
||||
mbo.set_objective(coeffs, c);
|
||||
|
||||
// extract linear constraints
|
||||
for (unsigned i = 0; i < fmls.size(); ++i) {
|
||||
linearize(mdl, mbo, fmls[i], tids);
|
||||
}
|
||||
|
||||
|
||||
// find optimal value
|
||||
value = mbo.maximize();
|
||||
|
||||
|
||||
|
||||
expr_ref val(a.mk_numeral(value.get_rational(), false), m);
|
||||
if (!value.is_finite()) {
|
||||
bound = m.mk_false();
|
||||
return value;
|
||||
}
|
||||
|
||||
// update model
|
||||
// update model to use new values that satisfy optimality
|
||||
ptr_vector<expr> vars;
|
||||
obj_map<expr, unsigned>::iterator it = tids.begin(), end = tids.end();
|
||||
for (; it != end; ++it) {
|
||||
|
@ -1009,6 +1011,7 @@ namespace qe {
|
|||
}
|
||||
}
|
||||
|
||||
// update the predicate 'bound' which forces larger values.
|
||||
if (value.get_infinitesimal().is_neg()) {
|
||||
bound = a.mk_le(val, t);
|
||||
}
|
||||
|
|
|
@ -1285,7 +1285,7 @@ namespace qe {
|
|||
opt::inf_eps m_value;
|
||||
bool m_was_sat;
|
||||
|
||||
lbool maximize(expr_ref_vector const& fmls, app* t, opt::inf_eps& value) {
|
||||
lbool maximize(expr_ref_vector const& fmls, app* t, model_ref& mdl, opt::inf_eps& value) {
|
||||
expr_ref_vector defs(m);
|
||||
expr_ref fml = negate_core(fmls);
|
||||
hoist(fml);
|
||||
|
@ -1299,6 +1299,7 @@ namespace qe {
|
|||
m_ex.assert_expr(fml);
|
||||
m_fa.assert_expr(m.mk_not(fml));
|
||||
lbool is_sat = check_sat();
|
||||
mdl = m_model.get();
|
||||
switch (is_sat) {
|
||||
case l_false:
|
||||
if (!m_was_sat) {
|
||||
|
@ -1329,10 +1330,10 @@ namespace qe {
|
|||
|
||||
};
|
||||
|
||||
lbool maximize(expr_ref_vector const& fmls, app* t, opt::inf_eps& value, params_ref const& p) {
|
||||
lbool maximize(expr_ref_vector const& fmls, app* t, opt::inf_eps& value, model_ref& mdl, params_ref const& p) {
|
||||
ast_manager& m = fmls.get_manager();
|
||||
qsat qs(m, p, qsat_maximize);
|
||||
return qs.maximize(fmls, t, value);
|
||||
return qs.maximize(fmls, t, mdl, value);
|
||||
}
|
||||
};
|
||||
|
||||
|
|
|
@ -114,7 +114,7 @@ namespace qe {
|
|||
void collect_statistics(statistics& st) const;
|
||||
};
|
||||
|
||||
lbool maximize(expr_ref_vector const& fmls, app* t, opt::inf_eps& value, params_ref const& p);
|
||||
lbool maximize(expr_ref_vector const& fmls, app* t, opt::inf_eps& value, model_ref& mdl, params_ref const& p);
|
||||
|
||||
}
|
||||
|
||||
|
|
|
@ -83,9 +83,14 @@ private:
|
|||
solver * m_solver;
|
||||
volatile bool m_canceled;
|
||||
aux_timeout_eh(solver * s):m_solver(s), m_canceled(false) {}
|
||||
~aux_timeout_eh() {
|
||||
if (m_canceled) {
|
||||
m_solver->get_manager().limit().dec_cancel();
|
||||
}
|
||||
}
|
||||
virtual void operator()() {
|
||||
m_solver->get_manager().limit().cancel();
|
||||
m_canceled = true;
|
||||
m_solver->get_manager().limit().inc_cancel();
|
||||
}
|
||||
};
|
||||
|
||||
|
@ -225,9 +230,6 @@ public:
|
|||
if ((r != l_undef || !use_solver1_when_undef()) && !eh.m_canceled) {
|
||||
return r;
|
||||
}
|
||||
if (eh.m_canceled) {
|
||||
m_solver1->get_manager().limit().reset_cancel();
|
||||
}
|
||||
}
|
||||
IF_VERBOSE(PS_VB_LVL, verbose_stream() << "(combined-solver \"solver 2 failed, trying solver1\")\n";);
|
||||
}
|
||||
|
|
|
@ -26,12 +26,14 @@ Revision History:
|
|||
*/
|
||||
template<typename T>
|
||||
class cancel_eh : public event_handler {
|
||||
bool m_canceled;
|
||||
T & m_obj;
|
||||
public:
|
||||
cancel_eh(T & o):m_obj(o) {}
|
||||
~cancel_eh() { m_obj.reset_cancel(); }
|
||||
cancel_eh(T & o): m_canceled(false), m_obj(o) {}
|
||||
~cancel_eh() { if (m_canceled) m_obj.dec_cancel(); }
|
||||
virtual void operator()() {
|
||||
m_obj.cancel();
|
||||
m_canceled = true;
|
||||
m_obj.inc_cancel();
|
||||
}
|
||||
};
|
||||
|
||||
|
|
|
@ -31,7 +31,7 @@ uint64 reslimit::count() const {
|
|||
|
||||
bool reslimit::inc() {
|
||||
++m_count;
|
||||
return !m_cancel && (m_limit == 0 || m_count <= m_limit);
|
||||
return m_cancel == 0 && (m_limit == 0 || m_count <= m_limit);
|
||||
}
|
||||
|
||||
bool reslimit::inc(unsigned offset) {
|
||||
|
@ -46,7 +46,7 @@ void reslimit::push(unsigned delta_limit) {
|
|||
}
|
||||
m_limits.push_back(m_limit);
|
||||
m_limit = m_limit==0?new_limit:std::min(new_limit, m_limit);
|
||||
m_cancel = false;
|
||||
m_cancel = 0;
|
||||
}
|
||||
|
||||
void reslimit::pop() {
|
||||
|
@ -55,11 +55,11 @@ void reslimit::pop() {
|
|||
}
|
||||
m_limit = m_limits.back();
|
||||
m_limits.pop_back();
|
||||
m_cancel = false;
|
||||
m_cancel = 0;
|
||||
}
|
||||
|
||||
char const* reslimit::get_cancel_msg() const {
|
||||
if (m_cancel) {
|
||||
if (m_cancel > 0) {
|
||||
return Z3_CANCELED_MSG;
|
||||
}
|
||||
else {
|
||||
|
@ -84,7 +84,7 @@ void reslimit::pop_child() {
|
|||
void reslimit::cancel() {
|
||||
#pragma omp critical (reslimit_cancel)
|
||||
{
|
||||
set_cancel(true);
|
||||
set_cancel(m_cancel+1);
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -92,11 +92,28 @@ void reslimit::cancel() {
|
|||
void reslimit::reset_cancel() {
|
||||
#pragma omp critical (reslimit_cancel)
|
||||
{
|
||||
set_cancel(false);
|
||||
set_cancel(0);
|
||||
}
|
||||
}
|
||||
|
||||
void reslimit::set_cancel(bool f) {
|
||||
void reslimit::inc_cancel() {
|
||||
#pragma omp critical (reslimit_cancel)
|
||||
{
|
||||
set_cancel(m_cancel+1);
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
void reslimit::dec_cancel() {
|
||||
#pragma omp critical (reslimit_cancel)
|
||||
{
|
||||
if (m_cancel > 0) {
|
||||
set_cancel(m_cancel-1);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void reslimit::set_cancel(unsigned f) {
|
||||
m_cancel = f;
|
||||
for (unsigned i = 0; i < m_children.size(); ++i) {
|
||||
m_children[i]->set_cancel(f);
|
||||
|
|
|
@ -22,13 +22,13 @@ Revision History:
|
|||
#include "vector.h"
|
||||
|
||||
class reslimit {
|
||||
volatile bool m_cancel;
|
||||
volatile unsigned m_cancel;
|
||||
uint64 m_count;
|
||||
uint64 m_limit;
|
||||
svector<uint64> m_limits;
|
||||
ptr_vector<reslimit> m_children;
|
||||
|
||||
void set_cancel(bool f);
|
||||
void set_cancel(unsigned f);
|
||||
|
||||
public:
|
||||
reslimit();
|
||||
|
@ -42,10 +42,13 @@ public:
|
|||
uint64 count() const;
|
||||
|
||||
|
||||
bool get_cancel_flag() const { return m_cancel; }
|
||||
bool get_cancel_flag() const { return m_cancel > 0; }
|
||||
char const* get_cancel_msg() const;
|
||||
void cancel();
|
||||
void reset_cancel();
|
||||
|
||||
void inc_cancel();
|
||||
void dec_cancel();
|
||||
};
|
||||
|
||||
class scoped_rlimit {
|
||||
|
|
Loading…
Reference in a new issue