3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-06-03 21:10:07 -07:00
parent cbf089e10d
commit 9ca5b3f304
14 changed files with 20 additions and 21 deletions

View file

@ -362,7 +362,7 @@ namespace dd {
}
bool solver::canceled() {
return m_limit.get_cancel_flag();
return m_limit.is_canceled();
}
bool solver::done() {

View file

@ -78,7 +78,7 @@ struct solver::imp {
r = m_nlsat->check();
}
catch (z3_exception&) {
if (m_limit.get_cancel_flag()) {
if (m_limit.is_canceled()) {
r = l_undef;
}
else {

View file

@ -1759,7 +1759,7 @@ namespace nlsat {
if (assigned_value(antecedent) == l_undef) {
checkpoint();
// antecedent must be false in the current arith interpretation
SASSERT(value(antecedent) == l_false || m_rlimit.get_cancel_flag());
SASSERT(value(antecedent) == l_false || m_rlimit.is_canceled());
if (!is_marked(b)) {
SASSERT(is_arith_atom(b) && max_var(b) < m_xk); // must be in a previous stage
TRACE("nlsat_resolve", tout << "literal is unassigned, but it is false in arithmetic interpretation, adding it to lemma\n";);
@ -1837,10 +1837,10 @@ namespace nlsat {
for (unsigned i = 0; i < sz; i++) {
literal l = m_lazy_clause[i];
if (l.var() != b) {
SASSERT(value(l) == l_false || m_rlimit.get_cancel_flag());
SASSERT(value(l) == l_false || m_rlimit.is_canceled());
}
else {
SASSERT(value(l) == l_true || m_rlimit.get_cancel_flag());
SASSERT(value(l) == l_true || m_rlimit.is_canceled());
SASSERT(!l.sign() || m_bvalues[b] == l_false);
SASSERT(l.sign() || m_bvalues[b] == l_true);
}

View file

@ -161,7 +161,7 @@ namespace opt {
case l_true:
if (!update_assignment())
return l_undef;
SASSERT(soft.value == l_true || m.limit().get_cancel_flag());
SASSERT(soft.value == l_true || m.limit().is_canceled());
break;
case l_false:
soft.set_value(l_false);

View file

@ -65,7 +65,7 @@ namespace qe {
DEBUG_CODE(expr_ref val(m);
eval(lit, val);
CTRACE("qe", !m.is_true(val), tout << mk_pp(lit, m) << " := " << val << "\n";);
SASSERT(m.limit().get_cancel_flag() || !m.is_false(val)););
SASSERT(m.limit().is_canceled() || !m.is_false(val)););
if (!m.inc())
return false;

View file

@ -182,13 +182,13 @@ void asserted_formulas::get_assertions(ptr_vector<expr> & result) const {
void asserted_formulas::push_scope() {
reduce();
commit();
SASSERT(inconsistent() || m_qhead == m_formulas.size() || m.limit().get_cancel_flag());
SASSERT(inconsistent() || m_qhead == m_formulas.size() || m.limit().is_canceled());
TRACE("asserted_formulas_scopes", tout << "before push: " << m_scopes.size() << "\n";);
m_scoped_substitution.push();
m_scopes.push_back(scope());
scope & s = m_scopes.back();
s.m_formulas_lim = m_formulas.size();
SASSERT(inconsistent() || s.m_formulas_lim == m_qhead || m.limit().get_cancel_flag());
SASSERT(inconsistent() || s.m_formulas_lim == m_qhead || m.limit().is_canceled());
s.m_inconsistent_old = m_inconsistent;
m_defined_names.push();
m_elim_term_ite.push();

View file

@ -554,7 +554,7 @@ namespace smt {
catch (...) {
// Restore trail size since procedure was interrupted in the middle.
// If the add_eq_trail remains on the trail stack, then Z3 may crash when the destructor is invoked.
TRACE("add_eq", tout << "add_eq interrupted. This is unsafe " << m.limit().get_cancel_flag() << "\n";);
TRACE("add_eq", tout << "add_eq interrupted. This is unsafe " << m.limit().is_canceled() << "\n";);
m_trail_stack.shrink(old_trail_size);
throw;
}

View file

@ -264,7 +264,7 @@ namespace smt {
bool context::check_th_diseq_propagation() const {
TRACE("check_th_diseq_propagation", tout << "m_propagated_th_diseqs.size() " << m_propagated_th_diseqs.size() << "\n";);
int num = get_num_bool_vars();
if (inconsistent() || get_manager().limit().get_cancel_flag()) {
if (inconsistent() || get_manager().limit().is_canceled()) {
return true;
}
for (bool_var v = 0; v < num; v++) {

View file

@ -191,7 +191,7 @@ namespace smt {
template<typename Ext>
bool theory_arith<Ext>::satisfy_bounds() const {
if (get_manager().limit().get_cancel_flag())
if (get_manager().limit().is_canceled())
return true;
int num = get_num_vars();
for (theory_var v = 0; v < num; v++) {
@ -217,7 +217,7 @@ namespace smt {
template<typename Ext>
bool theory_arith<Ext>::valid_assignment() const {
if (get_manager().limit().get_cancel_flag())
if (get_manager().limit().is_canceled())
return true;
if (valid_row_assignment() &&
satisfy_bounds() &&

View file

@ -1811,7 +1811,7 @@ namespace smt {
}
bool theory_bv::check_invariant() {
if (m.limit().get_cancel_flag())
if (m.limit().is_canceled())
return true;
if (ctx.inconsistent())
return true;

View file

@ -3441,7 +3441,7 @@ public:
else {
rational r = get_value(v);
TRACE("arith", tout << mk_pp(o, m) << " v" << v << " := " << r << "\n";);
SASSERT("integer variables should have integer values: " && (!a.is_int(o) || r.is_int() || m.limit().get_cancel_flag()));
SASSERT("integer variables should have integer values: " && (!a.is_int(o) || r.is_int() || m.limit().is_canceled()));
if (a.is_int(o) && !r.is_int()) r = floor(r);
return alloc(expr_wrapper_proc, m_factory->mk_value(r, m.get_sort(o)));
}

View file

@ -2301,7 +2301,7 @@ void theory_seq::validate_fmls(enode_pair_vector const& eqs, literal_vector cons
k.assert_expr(f);
}
lbool r = k.check();
if (r != l_false && !m.limit().get_cancel_flag()) {
if (r != l_false && !m.limit().is_canceled()) {
model_ref mdl;
k.get_model(mdl);
IF_VERBOSE(0,

View file

@ -44,14 +44,12 @@ uint64_t reslimit::count() const {
bool reslimit::inc() {
++m_count;
bool r = (m_cancel == 0 && (m_limit == 0 || m_count <= m_limit)) || m_suspend;
return r;
return not_canceled();
}
bool reslimit::inc(unsigned offset) {
m_count += offset;
bool r = (m_cancel == 0 && (m_limit == 0 || m_count <= m_limit)) || m_suspend;
return r;
return not_canceled();
}
void reslimit::push(unsigned delta_limit) {

View file

@ -50,7 +50,8 @@ public:
uint64_t count() const;
bool suspended() const { return m_suspend; }
bool get_cancel_flag() const { return m_cancel > 0 && !m_suspend; }
inline bool not_canceled() const { return (m_cancel == 0 && (m_limit == 0 || m_count <= m_limit)) || m_suspend; }
inline bool is_canceled() const { return !not_canceled(); }
char const* get_cancel_msg() const;
void cancel();
void reset_cancel();