From 9ca5b3f30439bf88f5e7ac3867e0d07111123bc2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 3 Jun 2020 21:10:07 -0700 Subject: [PATCH] fix #4449 Signed-off-by: Nikolaj Bjorner --- src/math/grobner/pdd_solver.cpp | 2 +- src/math/lp/nra_solver.cpp | 2 +- src/nlsat/nlsat_solver.cpp | 6 +++--- src/opt/maxlex.cpp | 2 +- src/qe/qe_arith.cpp | 2 +- src/smt/asserted_formulas.cpp | 4 ++-- src/smt/smt_context.cpp | 2 +- src/smt/smt_context_inv.cpp | 2 +- src/smt/theory_arith_inv.h | 4 ++-- src/smt/theory_bv.cpp | 2 +- src/smt/theory_lra.cpp | 2 +- src/smt/theory_seq.cpp | 2 +- src/util/rlimit.cpp | 6 ++---- src/util/rlimit.h | 3 ++- 14 files changed, 20 insertions(+), 21 deletions(-) diff --git a/src/math/grobner/pdd_solver.cpp b/src/math/grobner/pdd_solver.cpp index 337ce6b7c..78978ce4c 100644 --- a/src/math/grobner/pdd_solver.cpp +++ b/src/math/grobner/pdd_solver.cpp @@ -362,7 +362,7 @@ namespace dd { } bool solver::canceled() { - return m_limit.get_cancel_flag(); + return m_limit.is_canceled(); } bool solver::done() { diff --git a/src/math/lp/nra_solver.cpp b/src/math/lp/nra_solver.cpp index 97c8a0b3f..f741a04f7 100644 --- a/src/math/lp/nra_solver.cpp +++ b/src/math/lp/nra_solver.cpp @@ -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 { diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index 65c2a8795..d36d7b96b 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -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); } diff --git a/src/opt/maxlex.cpp b/src/opt/maxlex.cpp index 4acd875ca..9b73df8ca 100644 --- a/src/opt/maxlex.cpp +++ b/src/opt/maxlex.cpp @@ -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); diff --git a/src/qe/qe_arith.cpp b/src/qe/qe_arith.cpp index 1fa65a1b4..ec3a7d09f 100644 --- a/src/qe/qe_arith.cpp +++ b/src/qe/qe_arith.cpp @@ -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; diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp index 576a85a87..8da9c8fad 100644 --- a/src/smt/asserted_formulas.cpp +++ b/src/smt/asserted_formulas.cpp @@ -182,13 +182,13 @@ void asserted_formulas::get_assertions(ptr_vector & 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(); diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 6c120c833..46e6c05cd 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -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; } diff --git a/src/smt/smt_context_inv.cpp b/src/smt/smt_context_inv.cpp index 92a08df14..0fc8d5fff 100644 --- a/src/smt/smt_context_inv.cpp +++ b/src/smt/smt_context_inv.cpp @@ -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++) { diff --git a/src/smt/theory_arith_inv.h b/src/smt/theory_arith_inv.h index e569d221a..9517f558f 100644 --- a/src/smt/theory_arith_inv.h +++ b/src/smt/theory_arith_inv.h @@ -191,7 +191,7 @@ namespace smt { template bool theory_arith::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 bool theory_arith::valid_assignment() const { - if (get_manager().limit().get_cancel_flag()) + if (get_manager().limit().is_canceled()) return true; if (valid_row_assignment() && satisfy_bounds() && diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp index 853961912..e6c8b25e7 100644 --- a/src/smt/theory_bv.cpp +++ b/src/smt/theory_bv.cpp @@ -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; diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 5a966a324..a545d7215 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -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))); } diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 09e3c139c..dac2f3070 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -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, diff --git a/src/util/rlimit.cpp b/src/util/rlimit.cpp index a38f0ebf2..c88505f83 100644 --- a/src/util/rlimit.cpp +++ b/src/util/rlimit.cpp @@ -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) { diff --git a/src/util/rlimit.h b/src/util/rlimit.h index 6502c0426..cd3599f6f 100644 --- a/src/util/rlimit.h +++ b/src/util/rlimit.h @@ -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();