From 426e4cc75cb3792634352f5d850431fc499e222f Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 3 Apr 2020 16:37:59 -0700
Subject: [PATCH] fix #3557
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/ackermannization/lackr.h | 2 +-
src/api/api_opt.cpp | 4 ++--
src/api/api_solver.cpp | 2 +-
src/ast/ast.h | 3 ++-
src/ast/normal_forms/nnf.cpp | 2 +-
.../bit_blaster/bit_blaster_tpl_def.h | 2 +-
src/ast/rewriter/rewriter_def.h | 4 ++--
src/cmd_context/cmd_context.cpp | 4 ++--
src/math/grobner/grobner.cpp | 12 +++++-----
src/math/subpaving/tactic/expr2subpaving.cpp | 2 +-
src/muz/base/dl_context.h | 2 +-
src/muz/base/hnf.cpp | 2 +-
src/muz/bmc/dl_bmc_engine.cpp | 10 ++++-----
src/muz/spacer/spacer_context.cpp | 7 ++----
src/muz/tab/tab_context.cpp | 10 ++++-----
src/muz/transforms/dl_mk_karr_invariants.cpp | 2 +-
src/opt/maxlex.cpp | 2 +-
src/opt/maxres.cpp | 6 ++---
src/opt/opt_context.cpp | 2 +-
src/opt/opt_pareto.cpp | 4 ++--
src/opt/optsmt.cpp | 22 +++++++++----------
src/opt/pb_sls.cpp | 2 +-
src/opt/sortmax.cpp | 2 +-
src/opt/wmax.cpp | 6 ++---
src/qe/qe.cpp | 2 +-
src/qe/qe_arith.cpp | 4 ++--
src/qe/qe_lite.cpp | 12 ++++------
src/qe/qe_mbp.cpp | 4 ++--
src/qe/qe_tactic.cpp | 3 +--
src/qe/qsat.cpp | 12 +++++-----
src/sat/tactic/goal2sat.cpp | 4 ++--
src/smt/asserted_formulas.cpp | 4 ++--
src/smt/asserted_formulas.h | 2 +-
src/smt/smt_consequences.cpp | 2 +-
src/smt/smt_context_inv.cpp | 2 +-
src/smt/tactic/ctx_solver_simplify_tactic.cpp | 6 ++---
src/smt/tactic/unit_subsumption_tactic.cpp | 4 +---
src/smt/theory_arith_inv.h | 2 +-
src/smt/theory_bv.cpp | 7 +++++-
src/smt/theory_lra.cpp | 18 +++++++--------
src/solver/combined_solver.cpp | 4 ++--
src/solver/parallel_tactic.cpp | 6 ++---
src/solver/solver.cpp | 4 ++--
src/solver/solver2tactic.cpp | 2 +-
src/tactic/aig/aig.cpp | 2 +-
src/tactic/arith/arith_bounds_tactic.cpp | 4 +---
src/tactic/arith/degree_shift_tactic.cpp | 2 +-
src/tactic/arith/diff_neq_tactic.cpp | 2 +-
src/tactic/arith/fm_tactic.cpp | 5 +++--
src/tactic/arith/lia2card_tactic.cpp | 2 +-
src/tactic/bv/bv_size_reduction_tactic.cpp | 2 +-
src/tactic/bv/bvarray2uf_tactic.cpp | 2 +-
src/tactic/core/cofactor_elim_term_ite.cpp | 3 +--
src/tactic/core/ctx_simplify_tactic.cpp | 3 +--
src/tactic/core/occf_tactic.cpp | 3 +--
src/tactic/core/reduce_args_tactic.cpp | 3 +--
src/tactic/core/reduce_invertible_tactic.cpp | 3 +--
src/tactic/core/solve_eqs_tactic.cpp | 3 +--
src/tactic/core/tseitin_cnf_tactic.cpp | 3 +--
.../fd_solver/bounded_int2bv_solver.cpp | 2 +-
src/tactic/fd_solver/smtfd_solver.cpp | 4 +---
src/tactic/sls/sls_engine.cpp | 3 +--
src/tactic/tactic.cpp | 4 ++++
src/tactic/tactic.h | 3 +++
src/tactic/ufbv/quasi_macros_tactic.cpp | 3 +--
65 files changed, 135 insertions(+), 146 deletions(-)
diff --git a/src/ackermannization/lackr.h b/src/ackermannization/lackr.h
index aad1fdfcd..e559b5c77 100644
--- a/src/ackermannization/lackr.h
+++ b/src/ackermannization/lackr.h
@@ -71,7 +71,7 @@ class lackr {
// timeout mechanism
//
void checkpoint() {
- if (m.canceled()) {
+ if (!m.inc()) {
throw tactic_exception(TACTIC_CANCELED_MSG);
}
}
diff --git a/src/api/api_opt.cpp b/src/api/api_opt.cpp
index 1eed57b8c..e509bc528 100644
--- a/src/api/api_opt.cpp
+++ b/src/api/api_opt.cpp
@@ -162,11 +162,11 @@ extern "C" {
r = to_optimize_ptr(o)->optimize(asms);
}
catch (z3_exception& ex) {
- if (!mk_c(c)->m().canceled()) {
+ if (mk_c(c)->m().inc()) {
mk_c(c)->handle_exception(ex);
}
r = l_undef;
- if (ex.msg() == std::string("canceled") && mk_c(c)->m().canceled()) {
+ if (ex.msg() == std::string("canceled") && !mk_c(c)->m().inc()) {
to_optimize_ptr(o)->set_reason_unknown(ex.msg());
}
else {
diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp
index a512d7a46..90929416e 100644
--- a/src/api/api_solver.cpp
+++ b/src/api/api_solver.cpp
@@ -583,7 +583,7 @@ extern "C" {
catch (z3_exception & ex) {
to_solver_ref(s)->set_reason_unknown(eh);
to_solver(s)->set_eh(nullptr);
- if (!mk_c(c)->m().canceled()) {
+ if (mk_c(c)->m().inc()) {
mk_c(c)->handle_exception(ex);
}
return Z3_L_UNDEF;
diff --git a/src/ast/ast.h b/src/ast/ast.h
index 389c31948..d81abc559 100644
--- a/src/ast/ast.h
+++ b/src/ast/ast.h
@@ -1621,7 +1621,8 @@ public:
}
reslimit& limit() { return m_limit; }
- bool canceled() { return !limit().inc(); }
+ // bool canceled() { return !limit().inc(); }
+ bool inc() { return limit().inc(); }
void register_plugin(symbol const & s, decl_plugin * plugin);
diff --git a/src/ast/normal_forms/nnf.cpp b/src/ast/normal_forms/nnf.cpp
index fce1cf89f..9610c1ade 100644
--- a/src/ast/normal_forms/nnf.cpp
+++ b/src/ast/normal_forms/nnf.cpp
@@ -382,7 +382,7 @@ struct nnf::imp {
void checkpoint() {
if (memory::get_allocation_size() > m_max_memory)
throw nnf_exception(Z3_MAX_MEMORY_MSG);
- if (m.canceled())
+ if (!m.inc())
throw nnf_exception(m.limit().get_cancel_msg());
}
diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h
index 6dd1ca403..a21563c14 100644
--- a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h
+++ b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h
@@ -27,7 +27,7 @@ template<typename Cfg>
void bit_blaster_tpl<Cfg>::checkpoint() {
if (memory::get_allocation_size() > m_max_memory)
throw rewriter_exception(Z3_MAX_MEMORY_MSG);
- if (m().canceled())
+ if (!m().inc())
throw rewriter_exception(m().limit().get_cancel_msg());
}
diff --git a/src/ast/rewriter/rewriter_def.h b/src/ast/rewriter/rewriter_def.h
index f32b07a9c..963a8ad94 100644
--- a/src/ast/rewriter/rewriter_def.h
+++ b/src/ast/rewriter/rewriter_def.h
@@ -699,7 +699,7 @@ template<typename Config>
template<bool ProofGen>
void rewriter_tpl<Config>::main_loop(expr * t, expr_ref & result, proof_ref & result_pr) {
result_pr = nullptr;
- if (m().canceled()) {
+ if (!m().inc()) {
if (m_cancel_check) {
reset();
throw rewriter_exception(m().limit().get_cancel_msg());
@@ -738,7 +738,7 @@ template<bool ProofGen>
void rewriter_tpl<Config>::resume_core(expr_ref & result, proof_ref & result_pr) {
SASSERT(!frame_stack().empty());
while (!frame_stack().empty()) {
- if (m().canceled()) {
+ if (!m().inc()) {
if (m_cancel_check) {
reset();
throw rewriter_exception(m().limit().get_cancel_msg());
diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index fb798fd26..0198f6a9a 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -1579,7 +1579,7 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
scoped_rlimit _rlimit(m().limit(), rlimit);
try {
r = m_solver->check_sat(num_assumptions, assumptions);
- if (r == l_undef && m().canceled()) {
+ if (r == l_undef && !m().inc()) {
m_solver->set_reason_unknown(eh);
}
}
@@ -1587,7 +1587,7 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
throw ex;
}
catch (z3_exception & ex) {
- if (m().canceled()) {
+ if (!m().inc()) {
m_solver->set_reason_unknown(eh);
}
else {
diff --git a/src/math/grobner/grobner.cpp b/src/math/grobner/grobner.cpp
index 329c08f92..5e547f806 100644
--- a/src/math/grobner/grobner.cpp
+++ b/src/math/grobner/grobner.cpp
@@ -656,7 +656,7 @@ grobner::equation * grobner::simplify(equation const * source, equation * target
simplify(target);
}
}
- while (simplified && !m_manager.canceled());
+ while (simplified && m_manager.inc());
TRACE("grobner", tout << "result: "; display_equation(tout, *target););
return result ? target : nullptr;
}
@@ -680,7 +680,7 @@ grobner::equation * grobner::simplify_using_processed(equation * eq) {
simplified = true;
eq = new_eq;
}
- if (m_manager.canceled()) {
+ if (!m_manager.inc()) {
return nullptr;
}
}
@@ -736,7 +736,7 @@ bool grobner::simplify_processed(equation * eq) {
ptr_buffer<equation> to_delete;
equation_set::iterator it = m_processed.begin();
equation_set::iterator end = m_processed.end();
- for (; it != end && !m_manager.canceled(); ++it) {
+ for (; it != end && m_manager.inc(); ++it) {
equation * curr = *it;
m_changed_leading_term = false;
// if the leading term is simplified, then the equation has to be moved to m_to_process
@@ -770,7 +770,7 @@ bool grobner::simplify_processed(equation * eq) {
m_processed.erase(eq);
for (equation* eq : to_delete)
del_equation(eq);
- return !m_manager.canceled();
+ return m_manager.inc();
}
/**
@@ -908,7 +908,7 @@ bool grobner::compute_basis_step() {
m_equations_to_unfreeze.push_back(eq);
eq = new_eq;
}
- if (m_manager.canceled()) return false;
+ if (!m_manager.inc()) return false;
if (!simplify_processed(eq)) return false;
superpose(eq);
m_processed.insert(eq);
@@ -919,7 +919,7 @@ bool grobner::compute_basis_step() {
bool grobner::compute_basis(unsigned threshold) {
compute_basis_init();
- while (m_num_new_equations < threshold && !m_manager.canceled()) {
+ while (m_num_new_equations < threshold && m_manager.inc()) {
if (compute_basis_step()) return true;
}
return false;
diff --git a/src/math/subpaving/tactic/expr2subpaving.cpp b/src/math/subpaving/tactic/expr2subpaving.cpp
index aff0abd48..09ebe40e3 100644
--- a/src/math/subpaving/tactic/expr2subpaving.cpp
+++ b/src/math/subpaving/tactic/expr2subpaving.cpp
@@ -93,7 +93,7 @@ struct expr2subpaving::imp {
}
void checkpoint() {
- if (m().canceled())
+ if (!m().inc())
throw default_exception(Z3_CANCELED_MSG);
}
diff --git a/src/muz/base/dl_context.h b/src/muz/base/dl_context.h
index 2ae0e53ef..adb98592d 100644
--- a/src/muz/base/dl_context.h
+++ b/src/muz/base/dl_context.h
@@ -497,7 +497,7 @@ namespace datalog {
// -----------------------------------
bool canceled() {
- return m.canceled() && (m_last_status = CANCELED, true);
+ return !m.inc() && (m_last_status = CANCELED, true);
}
void cleanup();
diff --git a/src/muz/base/hnf.cpp b/src/muz/base/hnf.cpp
index d2ba9b999..dab81e878 100644
--- a/src/muz/base/hnf.cpp
+++ b/src/muz/base/hnf.cpp
@@ -172,7 +172,7 @@ public:
}
bool checkpoint() {
- return !m.canceled();
+ return m.inc();
}
void set_name(symbol const& n) {
diff --git a/src/muz/bmc/dl_bmc_engine.cpp b/src/muz/bmc/dl_bmc_engine.cpp
index 28de7950b..332817cec 100644
--- a/src/muz/bmc/dl_bmc_engine.cpp
+++ b/src/muz/bmc/dl_bmc_engine.cpp
@@ -26,6 +26,7 @@ Revision History:
#include "ast/scoped_proof.h"
#include "smt/smt_solver.h"
#include "tactic/fd_solver/fd_solver.h"
+#include "tactic/tactic.h"
#include "muz/base/dl_context.h"
#include "muz/base/dl_rule_transformer.h"
#include "muz/bmc/dl_bmc_engine.h"
@@ -35,6 +36,7 @@ Revision History:
#include "muz/transforms/dl_mk_rule_inliner.h"
#include "muz/base/fp_params.hpp"
+
namespace datalog {
// ---------------------------------------------------------------------------
@@ -485,7 +487,7 @@ namespace datalog {
}
proof_ref get_proof(model_ref& md, func_decl* pred, app* prop, unsigned level) {
- if (m.canceled()) {
+ if (!m.inc()) {
return proof_ref(nullptr, m);
}
TRACE("bmc", tout << "Predicate: " << pred->get_name() << "\n";);
@@ -1173,7 +1175,7 @@ namespace datalog {
private:
void get_model(unsigned level) {
- if (m.canceled()) {
+ if (!m.inc()) {
return;
}
rule_manager& rm = b.m_ctx.get_rule_manager();
@@ -1520,9 +1522,7 @@ namespace datalog {
}
void bmc::checkpoint() {
- if (m.canceled()) {
- throw default_exception(Z3_CANCELED_MSG);
- }
+ tactic::checkpoint(m);
}
void bmc::display_certificate(std::ostream& out) const {
diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp
index c77ae86f0..3fd44c69c 100644
--- a/src/muz/spacer/spacer_context.cpp
+++ b/src/muz/spacer/spacer_context.cpp
@@ -2759,11 +2759,8 @@ lbool context::solve(unsigned from_lvl)
}
-void context::checkpoint()
-{
- if (m.canceled ()) {
- throw default_exception("spacer canceled");
- }
+void context::checkpoint() {
+ tactic::checkpoint(m);
}
unsigned context::get_cex_depth()
diff --git a/src/muz/tab/tab_context.cpp b/src/muz/tab/tab_context.cpp
index e580f84e1..c1d26b378 100644
--- a/src/muz/tab/tab_context.cpp
+++ b/src/muz/tab/tab_context.cpp
@@ -581,7 +581,7 @@ namespace tb {
// extract pre_cond => post_cond validation obligation from match.
bool find_match(unsigned& subsumer) {
- for (unsigned i = 0; !m.canceled() && i < m_index.size(); ++i) {
+ for (unsigned i = 0; m.inc() && i < m_index.size(); ++i) {
if (match_rule(i)) {
subsumer = m_index[i]->get_seqno();
return true;
@@ -618,7 +618,7 @@ namespace tb {
app* q = g.get_predicate(predicate_index);
- for (unsigned i = 0; !m.canceled() && i < m_preds.size(); ++i) {
+ for (unsigned i = 0; m.inc() && i < m_preds.size(); ++i) {
app* p = m_preds[i].get();
m_subst.push_scope();
unsigned limit = m_sideconds.size();
@@ -647,7 +647,7 @@ namespace tb {
expr_ref_vector fmls(m_sideconds);
m_subst.reset_cache();
- for (unsigned i = 0; !m.canceled() && i < fmls.size(); ++i) {
+ for (unsigned i = 0; m.inc() && i < fmls.size(); ++i) {
m_subst.apply(2, deltas, expr_offset(fmls[i].get(), 0), q);
fmls[i] = q;
}
@@ -664,7 +664,7 @@ namespace tb {
}
}
m_rw.mk_and(fmls.size(), fmls.c_ptr(), postcond);
- if (m.canceled()) {
+ if (!m.inc()) {
return false;
}
if (m.is_false(postcond)) {
@@ -1493,7 +1493,7 @@ namespace datalog {
m_status = l_undef;
while (true) {
IF_VERBOSE(2, verbose_stream() << m_instruction << "\n";);
- if (m.canceled()) {
+ if (!m.inc()) {
cleanup();
return l_undef;
}
diff --git a/src/muz/transforms/dl_mk_karr_invariants.cpp b/src/muz/transforms/dl_mk_karr_invariants.cpp
index fd14538c5..ac5dbab02 100644
--- a/src/muz/transforms/dl_mk_karr_invariants.cpp
+++ b/src/muz/transforms/dl_mk_karr_invariants.cpp
@@ -214,7 +214,7 @@ namespace datalog {
get_invariants(*src_loop);
- if (m.canceled()) {
+ if (!m.inc()) {
return nullptr;
}
diff --git a/src/opt/maxlex.cpp b/src/opt/maxlex.cpp
index 0e4c9a9a0..8360f4e8b 100644
--- a/src/opt/maxlex.cpp
+++ b/src/opt/maxlex.cpp
@@ -159,7 +159,7 @@ namespace opt {
switch (is_sat) {
case l_true:
update_assignment();
- SASSERT(soft.value == l_true || m.canceled());
+ SASSERT(soft.value == l_true || m.limit().get_cancel_flag());
break;
case l_false:
soft.set_value(l_false);
diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp
index 7ff1d8491..15d7ee825 100644
--- a/src/opt/maxres.cpp
+++ b/src/opt/maxres.cpp
@@ -207,7 +207,7 @@ public:
s().display(tout << m_asms << "\n") << "\n";
display(tout););
is_sat = check_sat_hill_climb(m_asms);
- if (m.canceled()) {
+ if (!m.inc()) {
return l_undef;
}
switch (is_sat) {
@@ -247,7 +247,7 @@ public:
if (is_sat != l_true) return is_sat;
while (m_lower < m_upper) {
is_sat = check_sat_hill_climb(m_asms);
- if (m.canceled()) {
+ if (!m.inc()) {
return l_undef;
}
switch (is_sat) {
@@ -862,7 +862,7 @@ public:
tout << "other solver\n";
s().display(tout);
);
- VERIFY(is_sat == l_false || m.canceled());
+ VERIFY(is_sat == l_false || !m.inc());
}
void verify_assumptions() {
diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index 21642323d..c513048fa 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -615,7 +615,7 @@ namespace opt {
std::string context::reason_unknown() const {
- if (m.canceled()) {
+ if (!m.inc()) {
return Z3_CANCELED_MSG;
}
if (m_solver.get()) {
diff --git a/src/opt/opt_pareto.cpp b/src/opt/opt_pareto.cpp
index 0b2ab077a..0b98dfd7f 100644
--- a/src/opt/opt_pareto.cpp
+++ b/src/opt/opt_pareto.cpp
@@ -36,7 +36,7 @@ namespace opt {
m_solver->get_model(m_model);
solver::scoped_push _s(*m_solver.get());
while (is_sat == l_true) {
- if (m.canceled()) {
+ if (!m.inc()) {
return l_undef;
}
@@ -96,7 +96,7 @@ namespace opt {
lbool oia_pareto::operator()() {
solver::scoped_push _s(*m_solver.get());
lbool is_sat = m_solver->check_sat(0, nullptr);
- if (m.canceled()) {
+ if (!m.inc()) {
is_sat = l_undef;
}
if (is_sat == l_true) {
diff --git a/src/opt/optsmt.cpp b/src/opt/optsmt.cpp
index 3e2892f69..8dff3f924 100644
--- a/src/opt/optsmt.cpp
+++ b/src/opt/optsmt.cpp
@@ -71,7 +71,7 @@ namespace opt {
expr* vars[1];
solver::scoped_push _push(*m_s);
- while (is_sat == l_true && !m.canceled()) {
+ while (is_sat == l_true && m.inc()) {
tmp = m.mk_fresh_const("b", m.mk_bool_sort());
vars[0] = tmp;
@@ -83,7 +83,7 @@ namespace opt {
}
}
- if (m.canceled() || is_sat == l_undef) {
+ if (!m.inc() || is_sat == l_undef) {
return l_undef;
}
@@ -110,7 +110,7 @@ namespace opt {
unsigned num_scopes = 0;
unsigned delta_index = 0; // index of objective to speed up.
- while (!m.canceled()) {
+ while (m.inc()) {
SASSERT(delta_per_step.is_int());
SASSERT(delta_per_step.is_pos());
is_sat = m_s->check_sat(0, nullptr);
@@ -176,7 +176,7 @@ namespace opt {
}
}
- if (m.canceled() || is_sat == l_undef) {
+ if (!m.inc() || is_sat == l_undef) {
return l_undef;
}
@@ -208,7 +208,7 @@ namespace opt {
rational delta_per_step(1);
unsigned num_scopes = 0;
- while (!m.canceled()) {
+ while (m.inc()) {
SASSERT(delta_per_step.is_int());
SASSERT(delta_per_step.is_pos());
is_sat = m_s->check_sat(0, nullptr);
@@ -265,7 +265,7 @@ namespace opt {
return l_false;
}
- if (m.canceled() || is_sat == l_undef) {
+ if (!m.inc() || is_sat == l_undef) {
return l_undef;
}
@@ -315,7 +315,7 @@ namespace opt {
lbool is_sat = l_true;
solver::scoped_push _push(*m_s);
- while (!m.canceled()) {
+ while (m.inc()) {
m_s->assert_expr(fml);
TRACE("opt", tout << fml << "\n";);
is_sat = m_s->check_sat(1,vars);
@@ -349,7 +349,7 @@ namespace opt {
bound = mk_or(m_lower_fmls);
m_s->assert_expr(bound);
- if (m.canceled()) {
+ if (!m.inc()) {
return l_undef;
}
return geometric_opt();
@@ -418,7 +418,7 @@ namespace opt {
vector<inf_eps> mid;
- for (unsigned i = 0; i < m_lower.size() && !m.canceled(); ++i) {
+ for (unsigned i = 0; i < m_lower.size() && m.inc(); ++i) {
if (m_lower[i] < m_upper[i]) {
mid.push_back((m_upper[i]+m_lower[i])/rational(2));
bound = m_s->mk_ge(i, mid[i]);
@@ -430,7 +430,7 @@ namespace opt {
}
}
bool progress = false;
- for (unsigned i = 0; i < m_lower.size() && !m.canceled(); ++i) {
+ for (unsigned i = 0; i < m_lower.size() && m.inc(); ++i) {
if (m_lower[i] <= mid[i] && mid[i] <= m_upper[i] && m_lower[i] < m_upper[i]) {
th.enable_record_conflict(bounds[i].get());
lbool is_sat = m_s->check_sat(1, bounds.c_ptr() + i);
@@ -460,7 +460,7 @@ namespace opt {
progress = true;
}
}
- if (m.canceled()) {
+ if (!m.inc()) {
return l_undef;
}
if (!progress) {
diff --git a/src/opt/pb_sls.cpp b/src/opt/pb_sls.cpp
index 17c3f9128..615be9ac9 100644
--- a/src/opt/pb_sls.cpp
+++ b/src/opt/pb_sls.cpp
@@ -194,7 +194,7 @@ namespace smt {
while (m_max_flips > 0) {
--m_max_flips;
literal lit = flip();
- if (m.canceled()) {
+ if (!m.inc()) {
return l_undef;
}
IF_VERBOSE(3, verbose_stream()
diff --git a/src/opt/sortmax.cpp b/src/opt/sortmax.cpp
index 1a19032e2..83ef72a83 100644
--- a/src/opt/sortmax.cpp
+++ b/src/opt/sortmax.cpp
@@ -90,7 +90,7 @@ namespace opt {
s().assert_expr(out[first]);
is_sat = s().check_sat(0, nullptr);
TRACE("opt", tout << is_sat << "\n"; s().display(tout); tout << "\n";);
- if (m.canceled()) {
+ if (!m.inc()) {
is_sat = l_undef;
}
if (is_sat == l_true) {
diff --git a/src/opt/wmax.cpp b/src/opt/wmax.cpp
index 9fb683179..c4e36f857 100644
--- a/src/opt/wmax.cpp
+++ b/src/opt/wmax.cpp
@@ -77,9 +77,9 @@ namespace opt {
TRACE("opt",
s().display(tout)<< "\n";
tout << "lower: " << m_lower << " upper: " << m_upper << "\n";);
- while (!m.canceled() && m_lower < m_upper) {
+ while (m.inc() && m_lower < m_upper) {
is_sat = s().check_sat(0, nullptr);
- if (m.canceled()) {
+ if (!m.inc()) {
is_sat = l_undef;
}
if (is_sat == l_undef) {
@@ -106,7 +106,7 @@ namespace opt {
update_assignment();
- if (!m.canceled() && is_sat == l_undef && m_lower == m_upper) {
+ if (m.inc() && is_sat == l_undef && m_lower == m_upper) {
is_sat = l_true;
}
if (is_sat == l_false) {
diff --git a/src/qe/qe.cpp b/src/qe/qe.cpp
index 8cee2919e..9d1c2f7e7 100644
--- a/src/qe/qe.cpp
+++ b/src/qe/qe.cpp
@@ -2049,7 +2049,7 @@ namespace qe {
}
void checkpoint() {
- if (m.canceled())
+ if (!m.inc())
throw tactic_exception(m.limit().get_cancel_msg());
}
diff --git a/src/qe/qe_arith.cpp b/src/qe/qe_arith.cpp
index 41f8d290b..70a0e6a99 100644
--- a/src/qe/qe_arith.cpp
+++ b/src/qe/qe_arith.cpp
@@ -65,9 +65,9 @@ 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.canceled() || m.is_true(val)););
+ SASSERT(m.limit().get_cancel_flag() || m.is_true(val)););
- if (!m.limit().inc())
+ if (!m.inc())
return false;
TRACE("opt", tout << mk_pp(lit, m) << " " << a.is_lt(lit) << " " << a.is_gt(lit) << "\n";);
diff --git a/src/qe/qe_lite.cpp b/src/qe/qe_lite.cpp
index 50f7985a0..97deb47a6 100644
--- a/src/qe/qe_lite.cpp
+++ b/src/qe/qe_lite.cpp
@@ -682,8 +682,7 @@ namespace qel {
}
void checkpoint() {
- if (m.canceled())
- throw tactic_exception(m.limit().get_cancel_msg());
+ tactic::checkpoint(m);
}
public:
@@ -870,8 +869,7 @@ namespace qel {
}
void checkpoint() {
- if (m.canceled())
- throw tactic_exception(m.limit().get_cancel_msg());
+ tactic::checkpoint(m);
}
public:
@@ -2144,8 +2142,7 @@ namespace fm {
}
void checkpoint() {
- if (m.canceled())
- throw tactic_exception(m.limit().get_cancel_msg());
+ tactic::checkpoint(m);
}
public:
@@ -2411,8 +2408,7 @@ class qe_lite_tactic : public tactic {
qe_lite m_qe;
void checkpoint() {
- if (m.canceled())
- throw tactic_exception(m.limit().get_cancel_msg());
+ tactic::checkpoint(m);
}
#if 0
diff --git a/src/qe/qe_mbp.cpp b/src/qe/qe_mbp.cpp
index 2e8970b61..d7850d1ef 100644
--- a/src/qe/qe_mbp.cpp
+++ b/src/qe/qe_mbp.cpp
@@ -207,10 +207,10 @@ class mbp::impl {
continue;
}
m_visited.mark(e);
- if (m.is_bool(e) && !m.is_true(e) && !m.is_false(e) && !m.canceled()) {
+ if (m.is_bool(e) && !m.is_true(e) && !m.is_false(e) && m.inc()) {
expr_ref val = eval(e);
TRACE("qe", tout << "found: " << mk_pp(e, m) << "\n";);
- if (m.canceled())
+ if (!m.inc())
continue;
SASSERT(m.is_true(val) || m.is_false(val));
if (!m_bool_visited.is_marked(e)) {
diff --git a/src/qe/qe_tactic.cpp b/src/qe/qe_tactic.cpp
index 3bc5d65f4..0aa3824e7 100644
--- a/src/qe/qe_tactic.cpp
+++ b/src/qe/qe_tactic.cpp
@@ -43,8 +43,7 @@ class qe_tactic : public tactic {
}
void checkpoint() {
- if (m.canceled())
- throw tactic_exception(m.limit().get_cancel_msg());
+ tactic::checkpoint(m);
}
void operator()(goal_ref const & g,
diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp
index 4dcc41582..aa1cc2eb3 100644
--- a/src/qe/qsat.cpp
+++ b/src/qe/qsat.cpp
@@ -856,9 +856,7 @@ namespace qe {
}
void check_cancel() {
- if (m.canceled()) {
- throw tactic_exception(m.limit().get_cancel_msg());
- }
+ tactic::checkpoint(m);
}
void display(std::ostream& out) const {
@@ -1125,7 +1123,7 @@ namespace qe {
expr_ref_vector fmls(m);
fmls.append(core.size(), core.c_ptr());
s.get_assertions(fmls);
- return check_fmls(fmls) || m.canceled();
+ return check_fmls(fmls) || !m.inc();
#endif
}
@@ -1138,7 +1136,7 @@ namespace qe {
lbool is_sat = solver.check();
CTRACE("qe", is_sat != l_false,
tout << fmls << "\nare not unsat\n";);
- return (is_sat == l_false) || m.canceled();
+ return (is_sat == l_false) || !m.inc();
}
bool validate_model(expr_ref_vector const& asms) {
@@ -1157,7 +1155,7 @@ namespace qe {
bool validate_model(model& mdl, unsigned sz, expr* const* fmls) {
expr_ref val(m);
for (unsigned i = 0; i < sz; ++i) {
- if (!m_model->is_true(fmls[i]) && !m.canceled()) {
+ if (!m_model->is_true(fmls[i]) && m.inc()) {
TRACE("qe", tout << "Formula does not evaluate to true in model: " << mk_pp(fmls[i], m) << "\n";);
return false;
}
@@ -1189,7 +1187,7 @@ namespace qe {
TRACE("qe", tout << "Projection is false in model\n";);
return false;
}
- if (m.canceled()) {
+ if (!m.inc()) {
return true;
}
for (unsigned i = 0; i < m_avars.size(); ++i) {
diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp
index c4bc4c64d..b461d128b 100644
--- a/src/sat/tactic/goal2sat.cpp
+++ b/src/sat/tactic/goal2sat.cpp
@@ -779,7 +779,7 @@ struct goal2sat::imp {
}
while (!m_frame_stack.empty()) {
loop:
- if (m.canceled())
+ if (!m.inc())
throw tactic_exception(m.limit().get_cancel_msg());
if (memory::get_allocation_size() > m_max_memory)
throw tactic_exception(TACTIC_MAX_MEMORY_MSG);
@@ -1098,7 +1098,7 @@ struct sat2goal::imp {
}
void checkpoint() {
- if (m.canceled())
+ if (!m.inc())
throw tactic_exception(m.limit().get_cancel_msg());
if (memory::get_allocation_size() > m_max_memory)
throw tactic_exception(TACTIC_MAX_MEMORY_MSG);
diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp
index c76c61ed9..7d0baf1e1 100644
--- a/src/smt/asserted_formulas.cpp
+++ b/src/smt/asserted_formulas.cpp
@@ -180,13 +180,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.canceled());
+ SASSERT(inconsistent() || m_qhead == m_formulas.size() || m.limit().get_cancel_flag());
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.canceled());
+ SASSERT(inconsistent() || s.m_formulas_lim == m_qhead || m.limit().get_cancel_flag());
s.m_inconsistent_old = m_inconsistent;
m_defined_names.push();
m_elim_term_ite.push();
diff --git a/src/smt/asserted_formulas.h b/src/smt/asserted_formulas.h
index b6f09af89..1c08734ba 100644
--- a/src/smt/asserted_formulas.h
+++ b/src/smt/asserted_formulas.h
@@ -212,7 +212,7 @@ class asserted_formulas {
bool invoke(simplify_fmls& s);
void swap_asserted_formulas(vector<justified_expr>& new_fmls);
void push_assertion(expr * e, proof * pr, vector<justified_expr>& result);
- bool canceled() { return m.canceled(); }
+ bool canceled() { return !m.inc(); }
bool check_well_sorted() const;
unsigned get_total_size() const;
diff --git a/src/smt/smt_consequences.cpp b/src/smt/smt_consequences.cpp
index b71561c5a..885c438d2 100644
--- a/src/smt/smt_consequences.cpp
+++ b/src/smt/smt_consequences.cpp
@@ -522,7 +522,7 @@ namespace smt {
unsigned num_restarts = 0;
while (true) {
- if (m.canceled()) {
+ if (!m.inc()) {
is_sat = l_undef;
break;
}
diff --git a/src/smt/smt_context_inv.cpp b/src/smt/smt_context_inv.cpp
index 94b30bf83..1caf0fbb3 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().canceled()) {
+ if (inconsistent() || get_manager().limit().get_cancel_flag()) {
return true;
}
for (bool_var v = 0; v < num; v++) {
diff --git a/src/smt/tactic/ctx_solver_simplify_tactic.cpp b/src/smt/tactic/ctx_solver_simplify_tactic.cpp
index 597ecf4e4..f0df5b949 100644
--- a/src/smt/tactic/ctx_solver_simplify_tactic.cpp
+++ b/src/smt/tactic/ctx_solver_simplify_tactic.cpp
@@ -96,7 +96,7 @@ protected:
m_solver.push();
reduce(fml);
m_solver.pop(1);
- if (m.canceled())
+ if (!m.inc())
return;
SASSERT(m_solver.get_scope_level() == 0);
TRACE("ctx_solver_simplify_tactic",
@@ -172,7 +172,7 @@ protected:
names.push_back(n);
m_solver.push();
- while (!todo.empty() && !m.canceled()) {
+ while (!todo.empty() && m.inc()) {
expr_ref res(m);
args.reset();
expr* e = todo.back().m_expr;
@@ -244,7 +244,7 @@ protected:
names.pop_back();
m_solver.pop(1);
}
- if (!m.canceled()) {
+ if (m.inc()) {
VERIFY(cache.find(fml, path_r));
result = path_r.m_expr;
}
diff --git a/src/smt/tactic/unit_subsumption_tactic.cpp b/src/smt/tactic/unit_subsumption_tactic.cpp
index 4cbe425c4..44086aa7e 100644
--- a/src/smt/tactic/unit_subsumption_tactic.cpp
+++ b/src/smt/tactic/unit_subsumption_tactic.cpp
@@ -57,9 +57,7 @@ struct unit_subsumption_tactic : public tactic {
}
void checkpoint() {
- if (m.canceled()) {
- throw tactic_exception(m.limit().get_cancel_msg());
- }
+ tactic::checkpoint(m);
}
void reduce_core(goal_ref const& g, goal_ref_buffer& result) {
diff --git a/src/smt/theory_arith_inv.h b/src/smt/theory_arith_inv.h
index 12dd0bb38..a46cc3e02 100644
--- a/src/smt/theory_arith_inv.h
+++ b/src/smt/theory_arith_inv.h
@@ -215,7 +215,7 @@ namespace smt {
template<typename Ext>
bool theory_arith<Ext>::valid_assignment() const {
- if (get_manager().canceled())
+ if (get_manager().limit().get_cancel_flag())
return true;
if (valid_row_assignment() &&
satisfy_bounds() &&
diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp
index 4baae8b2a..9b3b7bc57 100644
--- a/src/smt/theory_bv.cpp
+++ b/src/smt/theory_bv.cpp
@@ -1862,7 +1862,10 @@ namespace smt {
literal l = lits[i];
if (l.var() == true_bool_var) {
unsigned is_true = (l == true_literal);
- SASSERT(!bits[!is_true][i]); // no complementary bits
+ if (bits[!is_true][i]) {
+ // expect a conflict later on.
+ return true;
+ }
if (!bits[is_true][i]) {
bits[is_true][i] = true;
num_bits++;
@@ -1888,6 +1891,8 @@ namespace smt {
}
bool theory_bv::check_invariant() {
+ if (get_manager().limit().get_cancel_flag())
+ return true;
if (get_context().inconsistent())
return true;
unsigned num = get_num_vars();
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index e9ff9badb..ebb6e8c48 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -164,7 +164,7 @@ class theory_lra::imp {
imp& m_imp;
public:
resource_limit(imp& i): m_imp(i) { }
- bool get_cancel_flag() override { return m_imp.m.canceled(); }
+ bool get_cancel_flag() override { return !m_imp.m.inc(); }
};
@@ -1563,7 +1563,7 @@ public:
void init_variable_values() {
reset_variable_values();
- if (!m.canceled() && m_solver.get() && th.get_num_vars() > 0) {
+ if (m.inc() && m_solver.get() && th.get_num_vars() > 0) {
TRACE("arith", display(tout << "update variable values\n"););
lp().get_model(m_variable_values);
}
@@ -1721,7 +1721,7 @@ public:
return FC_CONTINUE;
case l_undef:
TRACE("arith", tout << "check feasiable is undef\n";);
- return m.canceled() ? FC_CONTINUE : FC_GIVEUP;
+ return m.inc() ? FC_CONTINUE : FC_GIVEUP;
default:
UNREACHABLE();
break;
@@ -2019,7 +2019,7 @@ public:
lbool check_lia() {
TRACE("arith",);
- if (m.canceled()) {
+ if (!m.inc()) {
TRACE("arith", tout << "canceled\n";);
return l_undef;
}
@@ -2177,7 +2177,7 @@ public:
lbool check_nra() {
m_use_nra_model = false;
- if (m.canceled()) {
+ if (!m.inc()) {
TRACE("arith", tout << "canceled\n";);
return l_undef;
}
@@ -2259,7 +2259,7 @@ public:
}
lbool lbl = make_feasible();
- if (m.canceled())
+ if (!m.inc())
return;
switch(lbl) {
@@ -2297,7 +2297,7 @@ public:
lp().propagate_bounds_for_touched_rows(bp);
- if (m.canceled()) {
+ if (!m.inc()) {
return;
}
@@ -2305,7 +2305,7 @@ public:
get_infeasibility_explanation_and_set_conflict();
}
else {
- for (unsigned i = 0; !m.canceled() && !ctx().inconsistent() && i < bp.m_ibounds.size(); ++i) {
+ for (unsigned i = 0; m.inc() && !ctx().inconsistent() && i < bp.m_ibounds.size(); ++i) {
propagate_lp_solver_bound(bp.m_ibounds[i]);
}
}
@@ -3398,7 +3398,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.canceled()));
+ SASSERT("integer variables should have integer values: " && (!a.is_int(o) || r.is_int() || m.limit().get_cancel_flag()));
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/solver/combined_solver.cpp b/src/solver/combined_solver.cpp
index 4339e45aa..267a22de0 100644
--- a/src/solver/combined_solver.cpp
+++ b/src/solver/combined_solver.cpp
@@ -191,7 +191,7 @@ public:
return m_solver2->get_consequences(asms, vars, consequences);
}
catch (z3_exception& ex) {
- if (get_manager().canceled()) {
+ if (!get_manager().inc()) {
throw;
}
else {
@@ -217,7 +217,7 @@ public:
if (m_inc_timeout == UINT_MAX) {
IF_VERBOSE(PS_VB_LVL, verbose_stream() << "(combined-solver \"using solver 2 (without a timeout)\")\n";);
lbool r = m_solver2->check_sat_core(num_assumptions, assumptions);
- if (r != l_undef || !use_solver1_when_undef() || get_manager().canceled()) {
+ if (r != l_undef || !use_solver1_when_undef() || !get_manager().inc()) {
return r;
}
}
diff --git a/src/solver/parallel_tactic.cpp b/src/solver/parallel_tactic.cpp
index 71a99ea79..b9bc77ad6 100644
--- a/src/solver/parallel_tactic.cpp
+++ b/src/solver/parallel_tactic.cpp
@@ -321,7 +321,7 @@ class parallel_tactic : public tactic {
}
bool canceled() {
- return m_giveup || m().canceled();
+ return m_giveup ||! m().inc();
}
std::ostream& display(std::ostream& out) {
@@ -634,7 +634,7 @@ private:
cube_and_conquer(*st);
collect_statistics(*st);
m_queue.task_done(st);
- if (st->m().canceled()) m_queue.shutdown();
+ if (!st->m().inc()) m_queue.shutdown();
IF_VERBOSE(1, display(verbose_stream()););
dealloc(st);
}
@@ -748,7 +748,7 @@ public:
g->assert_expr(m.mk_false(), pr, lcore);
break;
case l_undef:
- if (m.canceled()) {
+ if (!m.inc()) {
throw tactic_exception(Z3_CANCELED_MSG);
}
break;
diff --git a/src/solver/solver.cpp b/src/solver/solver.cpp
index d7d1a07ea..0c69da779 100644
--- a/src/solver/solver.cpp
+++ b/src/solver/solver.cpp
@@ -89,7 +89,7 @@ lbool solver::get_consequences(expr_ref_vector const& asms, expr_ref_vector cons
return get_consequences_core(asms, vars, consequences);
}
catch (z3_exception& ex) {
- if (asms.get_manager().canceled()) {
+ if (!asms.get_manager().inc()) {
set_reason_unknown(Z3_CANCELED_MSG);
return l_undef;
}
@@ -335,7 +335,7 @@ lbool solver::check_sat(unsigned num_assumptions, expr * const * assumptions) {
}
throw;
}
- if (r == l_undef && get_manager().canceled()) {
+ if (r == l_undef && !get_manager().inc()) {
dump_state(num_assumptions, assumptions);
}
return r;
diff --git a/src/solver/solver2tactic.cpp b/src/solver/solver2tactic.cpp
index 5d35b879c..ffc93a21a 100644
--- a/src/solver/solver2tactic.cpp
+++ b/src/solver/solver2tactic.cpp
@@ -153,7 +153,7 @@ public:
break;
}
case l_undef:
- if (m.canceled()) {
+ if (!m.inc()) {
throw tactic_exception(Z3_CANCELED_MSG);
}
model_converter_ref mc;
diff --git a/src/tactic/aig/aig.cpp b/src/tactic/aig/aig.cpp
index b3b69f640..c17093f78 100644
--- a/src/tactic/aig/aig.cpp
+++ b/src/tactic/aig/aig.cpp
@@ -126,7 +126,7 @@ struct aig_manager::imp {
void checkpoint() {
if (memory::get_allocation_size() > m_max_memory)
throw aig_exception(TACTIC_MAX_MEMORY_MSG);
- if (m().canceled())
+ if (!m().inc())
throw aig_exception(m().limit().get_cancel_msg());
}
diff --git a/src/tactic/arith/arith_bounds_tactic.cpp b/src/tactic/arith/arith_bounds_tactic.cpp
index e4af53f23..a8fcc4e00 100644
--- a/src/tactic/arith/arith_bounds_tactic.cpp
+++ b/src/tactic/arith/arith_bounds_tactic.cpp
@@ -33,9 +33,7 @@ struct arith_bounds_tactic : public tactic {
}
void checkpoint() {
- if (m.canceled()) {
- throw tactic_exception(m.limit().get_cancel_msg());
- }
+ tactic::checkpoint(m);
}
diff --git a/src/tactic/arith/degree_shift_tactic.cpp b/src/tactic/arith/degree_shift_tactic.cpp
index f90b94f27..d3c5bb74c 100644
--- a/src/tactic/arith/degree_shift_tactic.cpp
+++ b/src/tactic/arith/degree_shift_tactic.cpp
@@ -97,7 +97,7 @@ class degree_shift_tactic : public tactic {
void checkpoint() {
- if (m.canceled())
+ if (!m.inc())
throw tactic_exception(m.limit().get_cancel_msg());
}
diff --git a/src/tactic/arith/diff_neq_tactic.cpp b/src/tactic/arith/diff_neq_tactic.cpp
index e91d22b6a..b838a7127 100644
--- a/src/tactic/arith/diff_neq_tactic.cpp
+++ b/src/tactic/arith/diff_neq_tactic.cpp
@@ -288,7 +288,7 @@ class diff_neq_tactic : public tactic {
init_forbidden();
unsigned nvars = num_vars();
while (m_stack.size() < nvars) {
- if (m.canceled())
+ if (!m.inc())
throw tactic_exception(m.limit().get_cancel_msg());
TRACE("diff_neq_tactic", display_model(tout););
var x = m_stack.size();
diff --git a/src/tactic/arith/fm_tactic.cpp b/src/tactic/arith/fm_tactic.cpp
index 20cde5e21..0c6945054 100644
--- a/src/tactic/arith/fm_tactic.cpp
+++ b/src/tactic/arith/fm_tactic.cpp
@@ -198,7 +198,8 @@ class fm_tactic : public tactic {
clauses::iterator it = m_clauses[i].begin();
clauses::iterator end = m_clauses[i].end();
for (; it != end; ++it) {
- if (m.canceled()) throw tactic_exception(m.limit().get_cancel_msg());
+ if (!m.inc())
+ throw tactic_exception(m.limit().get_cancel_msg());
switch (process(x, *it, u, *md, val)) {
case NONE:
TRACE("fm_mc", tout << "no bound for:\n" << mk_ismt2_pp(*it, m) << "\n";);
@@ -1542,7 +1543,7 @@ class fm_tactic : public tactic {
}
void checkpoint() {
- if (m.canceled())
+ if (!m.inc())
throw tactic_exception(m.limit().get_cancel_msg());
if (memory::get_allocation_size() > m_max_memory)
throw tactic_exception(TACTIC_MAX_MEMORY_MSG);
diff --git a/src/tactic/arith/lia2card_tactic.cpp b/src/tactic/arith/lia2card_tactic.cpp
index 0c5661cf0..52e2b0e3a 100644
--- a/src/tactic/arith/lia2card_tactic.cpp
+++ b/src/tactic/arith/lia2card_tactic.cpp
@@ -164,7 +164,7 @@ public:
}
void checkpoint() {
- if (m.canceled()) {
+ if (!m.inc()) {
throw tactic_exception(m.limit().get_cancel_msg());
}
}
diff --git a/src/tactic/bv/bv_size_reduction_tactic.cpp b/src/tactic/bv/bv_size_reduction_tactic.cpp
index 52f9f450e..eaa63ac70 100644
--- a/src/tactic/bv/bv_size_reduction_tactic.cpp
+++ b/src/tactic/bv/bv_size_reduction_tactic.cpp
@@ -171,7 +171,7 @@ public:
}
void checkpoint() {
- if (m.canceled())
+ if (!m.inc())
throw tactic_exception(m.limit().get_cancel_msg());
}
diff --git a/src/tactic/bv/bvarray2uf_tactic.cpp b/src/tactic/bv/bvarray2uf_tactic.cpp
index b9fa9622a..0cc19a806 100644
--- a/src/tactic/bv/bvarray2uf_tactic.cpp
+++ b/src/tactic/bv/bvarray2uf_tactic.cpp
@@ -48,7 +48,7 @@ class bvarray2uf_tactic : public tactic {
void checkpoint() {
- if (m_manager.canceled())
+ if (!m_manager.inc())
throw tactic_exception(m_manager.limit().get_cancel_msg());
}
diff --git a/src/tactic/core/cofactor_elim_term_ite.cpp b/src/tactic/core/cofactor_elim_term_ite.cpp
index 3a4f3ce0c..2d9aafbda 100644
--- a/src/tactic/core/cofactor_elim_term_ite.cpp
+++ b/src/tactic/core/cofactor_elim_term_ite.cpp
@@ -33,8 +33,7 @@ struct cofactor_elim_term_ite::imp {
void checkpoint() {
if (memory::get_allocation_size() > m_max_memory)
throw tactic_exception(TACTIC_MAX_MEMORY_MSG);
- if (m.canceled())
- throw tactic_exception(m.limit().get_cancel_msg());
+ tactic::checkpoint(m);
}
// Collect atoms that contain term if-then-else
diff --git a/src/tactic/core/ctx_simplify_tactic.cpp b/src/tactic/core/ctx_simplify_tactic.cpp
index eb4092cd4..ff955e5af 100644
--- a/src/tactic/core/ctx_simplify_tactic.cpp
+++ b/src/tactic/core/ctx_simplify_tactic.cpp
@@ -203,8 +203,7 @@ struct ctx_simplify_tactic::imp {
void checkpoint() {
if (memory::get_allocation_size() > m_max_memory)
throw tactic_exception(TACTIC_MAX_MEMORY_MSG);
- if (m.canceled())
- throw tactic_exception(m.limit().get_cancel_msg());
+ tactic::checkpoint(m);
}
bool shared(expr * t) const {
diff --git a/src/tactic/core/occf_tactic.cpp b/src/tactic/core/occf_tactic.cpp
index 9b90d27ef..2deef831f 100644
--- a/src/tactic/core/occf_tactic.cpp
+++ b/src/tactic/core/occf_tactic.cpp
@@ -35,8 +35,7 @@ class occf_tactic : public tactic {
}
void checkpoint() {
- if (m.canceled())
- throw tactic_exception(TACTIC_CANCELED_MSG);
+ tactic::checkpoint(m);
}
bool is_literal(expr * t) const {
diff --git a/src/tactic/core/reduce_args_tactic.cpp b/src/tactic/core/reduce_args_tactic.cpp
index 390790c73..d3fa82ceb 100644
--- a/src/tactic/core/reduce_args_tactic.cpp
+++ b/src/tactic/core/reduce_args_tactic.cpp
@@ -112,8 +112,7 @@ struct reduce_args_tactic::imp {
}
void checkpoint() {
- if (m_manager.canceled())
- throw tactic_exception(m_manager.limit().get_cancel_msg());
+ tactic::checkpoint(m_manager);
}
struct find_non_candidates_proc {
diff --git a/src/tactic/core/reduce_invertible_tactic.cpp b/src/tactic/core/reduce_invertible_tactic.cpp
index 8d967098e..cb2888e2f 100644
--- a/src/tactic/core/reduce_invertible_tactic.cpp
+++ b/src/tactic/core/reduce_invertible_tactic.cpp
@@ -101,8 +101,7 @@ public:
private:
void checkpoint() {
- if (m.canceled())
- throw tactic_exception(m.limit().get_cancel_msg());
+ tactic::checkpoint(m);
}
bool is_bv_neg(expr * e) {
diff --git a/src/tactic/core/solve_eqs_tactic.cpp b/src/tactic/core/solve_eqs_tactic.cpp
index 112fb97fb..b6aed81ce 100644
--- a/src/tactic/core/solve_eqs_tactic.cpp
+++ b/src/tactic/core/solve_eqs_tactic.cpp
@@ -86,8 +86,7 @@ class solve_eqs_tactic : public tactic {
}
void checkpoint() {
- if (m().canceled())
- throw tactic_exception(m().limit().get_cancel_msg());
+ tactic::checkpoint(m());
}
// Check if the number of occurrences of t is below the specified threshold :solve-eqs-max-occs
diff --git a/src/tactic/core/tseitin_cnf_tactic.cpp b/src/tactic/core/tseitin_cnf_tactic.cpp
index cc038aea3..add9868eb 100644
--- a/src/tactic/core/tseitin_cnf_tactic.cpp
+++ b/src/tactic/core/tseitin_cnf_tactic.cpp
@@ -786,8 +786,7 @@ class tseitin_cnf_tactic : public tactic {
void checkpoint() {
- if (m.canceled())
- throw tactic_exception(TACTIC_CANCELED_MSG);
+ tactic::checkpoint(m);
if (memory::get_allocation_size() > m_max_memory)
throw tactic_exception(TACTIC_MAX_MEMORY_MSG);
}
diff --git a/src/tactic/fd_solver/bounded_int2bv_solver.cpp b/src/tactic/fd_solver/bounded_int2bv_solver.cpp
index 6d97c958c..ca40607d4 100644
--- a/src/tactic/fd_solver/bounded_int2bv_solver.cpp
+++ b/src/tactic/fd_solver/bounded_int2bv_solver.cpp
@@ -329,7 +329,7 @@ private:
for (expr* a : m_assertions) {
sub(a, fml1);
m_rewriter(fml1, fml2, proof);
- if (m.canceled()) {
+ if (!m.inc()) {
m_rewriter.reset();
return;
}
diff --git a/src/tactic/fd_solver/smtfd_solver.cpp b/src/tactic/fd_solver/smtfd_solver.cpp
index 6237f0202..8ba9dc44d 100644
--- a/src/tactic/fd_solver/smtfd_solver.cpp
+++ b/src/tactic/fd_solver/smtfd_solver.cpp
@@ -1815,9 +1815,7 @@ namespace smtfd {
}
void checkpoint() {
- if (m.canceled()) {
- throw tactic_exception(m.limit().get_cancel_msg());
- }
+ tactic::checkpoint(m);
}
expr* rep(expr* e) { return m_abs.rep(e); }
diff --git a/src/tactic/sls/sls_engine.cpp b/src/tactic/sls/sls_engine.cpp
index bf3cede69..58676edfb 100644
--- a/src/tactic/sls/sls_engine.cpp
+++ b/src/tactic/sls/sls_engine.cpp
@@ -93,8 +93,7 @@ void sls_engine::collect_statistics(statistics& st) const {
}
void sls_engine::checkpoint() {
- if (m_manager.canceled())
- throw tactic_exception(m_manager.limit().get_cancel_msg());
+ tactic::checkpoint(m_manager);
}
bool sls_engine::full_eval(model & mdl) {
diff --git a/src/tactic/tactic.cpp b/src/tactic/tactic.cpp
index b5c5025fa..66631357e 100644
--- a/src/tactic/tactic.cpp
+++ b/src/tactic/tactic.cpp
@@ -246,3 +246,7 @@ void fail_if_has_quantifiers(char const* tactic_name, goal_ref const& g) {
}
}
+void tactic::checkpoint(ast_manager& m) {
+ if (!m.inc())
+ throw tactic_exception(m.limit().get_cancel_msg());
+}
diff --git a/src/tactic/tactic.h b/src/tactic/tactic.h
index 41fe1d040..3458567c0 100644
--- a/src/tactic/tactic.h
+++ b/src/tactic/tactic.h
@@ -74,6 +74,9 @@ public:
// translate tactic to the given manager
virtual tactic * translate(ast_manager & m) = 0;
+
+ static void checkpoint(ast_manager& m);
+
protected:
friend class nary_tactical;
friend class binary_tactical;
diff --git a/src/tactic/ufbv/quasi_macros_tactic.cpp b/src/tactic/ufbv/quasi_macros_tactic.cpp
index 850c03e20..33c2927bb 100644
--- a/src/tactic/ufbv/quasi_macros_tactic.cpp
+++ b/src/tactic/ufbv/quasi_macros_tactic.cpp
@@ -57,8 +57,7 @@ class quasi_macros_tactic : public tactic {
}
do {
- if (m().canceled())
- throw tactic_exception(m().limit().get_cancel_msg());
+ tactic::checkpoint(m());
}
while (qm(forms, proofs, deps));