From 9769322690b8bb4fc56e0e6f027d8105c8e48bf2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 11 Dec 2015 16:21:24 -0800 Subject: [PATCH] reworking cancellation Signed-off-by: Nikolaj Bjorner --- src/api/api_context.cpp | 10 ++-- src/api/api_context.h | 4 +- src/api/api_polynomial.cpp | 10 +--- src/api/api_polynomial.h | 3 +- src/api/api_rcf.cpp | 2 +- src/ast/arith_decl_plugin.cpp | 4 -- src/ast/arith_decl_plugin.h | 4 -- src/ast/ast.cpp | 6 -- src/ast/ast.h | 4 -- src/ast/normal_forms/name_exprs.cpp | 3 - src/ast/normal_forms/name_exprs.h | 3 - src/ast/rewriter/arith_rewriter.cpp | 3 - src/ast/rewriter/arith_rewriter.h | 2 - .../bit_blaster/bit_blaster_rewriter.cpp | 4 -- .../bit_blaster/bit_blaster_rewriter.h | 1 - .../rewriter/bit_blaster/bit_blaster_tpl.h | 5 -- .../bit_blaster/bit_blaster_tpl_def.h | 2 +- src/ast/rewriter/der.cpp | 6 -- src/ast/rewriter/der.h | 3 - src/ast/rewriter/expr_replacer.cpp | 7 --- src/ast/rewriter/expr_replacer.h | 3 - src/ast/rewriter/rewriter.h | 5 -- src/ast/rewriter/rewriter_def.h | 3 - src/ast/rewriter/th_rewriter.cpp | 10 ---- src/ast/rewriter/th_rewriter.h | 3 - src/cmd_context/cmd_context.cpp | 13 ++--- src/cmd_context/eval_cmd.cpp | 2 +- .../extra_cmds/polynomial_cmds.cpp | 6 +- src/cmd_context/tactic_cmds.cpp | 4 +- src/duality/duality_wrapper.h | 3 +- src/math/interval/interval.h | 7 +-- src/math/interval/interval_def.h | 5 +- src/math/polynomial/algebraic_numbers.cpp | 18 +----- src/math/polynomial/algebraic_numbers.h | 4 -- src/math/polynomial/polynomial.cpp | 32 ++++------- src/math/polynomial/polynomial.h | 9 +-- src/math/polynomial/rpolynomial.cpp | 2 - src/math/polynomial/rpolynomial.h | 2 - src/math/polynomial/upolynomial.cpp | 10 +--- src/math/polynomial/upolynomial.h | 10 ++-- .../polynomial/upolynomial_factorization.cpp | 12 ++-- src/math/realclosure/realclosure.cpp | 19 ++----- src/math/realclosure/realclosure.h | 6 +- src/math/simplex/simplex.h | 1 - src/math/subpaving/subpaving_t.h | 7 +-- src/math/subpaving/subpaving_t_def.h | 3 +- src/math/subpaving/tactic/expr2subpaving.cpp | 10 +--- src/math/subpaving/tactic/expr2subpaving.h | 7 +-- .../subpaving/tactic/subpaving_tactic.cpp | 6 -- src/model/model_evaluator.cpp | 6 -- src/model/model_evaluator.h | 3 - src/muz/fp/horn_tactic.cpp | 9 +-- src/nlsat/nlsat_solver.cpp | 20 ++----- src/nlsat/nlsat_solver.h | 1 - src/nlsat/tactic/goal2nlsat.cpp | 11 ---- src/nlsat/tactic/goal2nlsat.h | 2 - src/nlsat/tactic/nlsat_tactic.cpp | 10 ---- src/opt/mus.cpp | 12 +--- src/opt/mus.h | 2 - src/opt/opt_cmds.cpp | 2 +- src/opt/opt_solver.cpp | 6 +- src/opt/opt_solver.h | 2 +- src/sat/sat_mus.cpp | 2 +- src/sat/sat_sls.cpp | 6 +- src/sat/sat_sls.h | 2 - src/sat/sat_solver.cpp | 8 +-- src/sat/sat_solver.h | 6 +- src/sat/sat_solver/inc_sat_solver.cpp | 7 +-- src/sat/tactic/goal2sat.cpp | 26 +-------- src/sat/tactic/goal2sat.h | 2 - src/sat/tactic/sat_tactic.cpp | 12 ---- src/smt/asserted_formulas.cpp | 6 +- src/smt/asserted_formulas.h | 3 +- src/smt/expr_context_simplifier.h | 1 - src/smt/smt_context.cpp | 11 ---- src/smt/smt_context.h | 4 +- src/smt/smt_kernel.cpp | 12 ---- src/smt/smt_kernel.h | 13 +---- src/smt/smt_solver.cpp | 5 +- src/smt/tactic/ctx_solver_simplify_tactic.cpp | 13 +---- src/smt/tactic/smt_tactic.cpp | 4 -- src/smt/tactic/unit_subsumption_tactic.cpp | 13 +---- src/solver/check_sat_result.h | 3 + src/solver/combined_solver.cpp | 21 +++---- src/solver/solver.h | 6 +- src/solver/tactic2solver.cpp | 12 +--- src/solver/tactic2solver.h | 1 + src/tactic/aig/aig.cpp | 10 +--- src/tactic/aig/aig.h | 1 - src/tactic/aig/aig_tactic.cpp | 8 --- src/tactic/arith/add_bounds_tactic.cpp | 9 --- src/tactic/arith/arith_bounds_tactic.cpp | 14 +---- src/tactic/arith/card2bv_tactic.cpp | 4 -- src/tactic/arith/degree_shift_tactic.cpp | 14 +---- src/tactic/arith/diff_neq_tactic.cpp | 15 +---- src/tactic/arith/elim01_tactic.cpp | 5 +- src/tactic/arith/eq2bv_tactic.cpp | 3 - src/tactic/arith/factor_tactic.cpp | 11 +--- src/tactic/arith/fix_dl_var_tactic.cpp | 11 +--- src/tactic/arith/fm_tactic.cpp | 18 +----- src/tactic/arith/lia2card_tactic.cpp | 6 +- src/tactic/arith/lia2pb_tactic.cpp | 8 --- src/tactic/arith/normalize_bounds_tactic.cpp | 9 --- src/tactic/arith/pb2bv_tactic.cpp | 10 +--- src/tactic/arith/probe_arith.cpp | 2 +- src/tactic/arith/propagate_ineqs_tactic.cpp | 9 --- src/tactic/arith/purify_arith_tactic.cpp | 2 - src/tactic/arith/recover_01_tactic.cpp | 9 --- src/tactic/bv/bit_blaster_tactic.cpp | 8 --- src/tactic/bv/bv1_blaster_tactic.cpp | 8 --- src/tactic/bv/bv_size_reduction_tactic.cpp | 15 +---- src/tactic/bv/bvarray2uf_tactic.cpp | 12 +--- src/tactic/bv/elim_small_bv_tactic.cpp | 8 --- src/tactic/bv/max_bv_sharing_tactic.cpp | 11 +--- src/tactic/core/blast_term_ite_tactic.cpp | 8 --- src/tactic/core/cofactor_elim_term_ite.cpp | 11 +--- src/tactic/core/cofactor_elim_term_ite.h | 3 - src/tactic/core/cofactor_term_ite_tactic.cpp | 1 - src/tactic/core/ctx_simplify_tactic.cpp | 11 +--- src/tactic/core/ctx_simplify_tactic.h | 2 - src/tactic/core/der_tactic.cpp | 10 +--- src/tactic/core/distribute_forall_tactic.cpp | 5 -- src/tactic/core/elim_term_ite_tactic.cpp | 7 --- src/tactic/core/elim_uncnstr_tactic.cpp | 9 --- src/tactic/core/occf_tactic.cpp | 13 +---- src/tactic/core/pb_preprocess_tactic.cpp | 3 - src/tactic/core/propagate_values_tactic.cpp | 8 --- src/tactic/core/reduce_args_tactic.cpp | 13 +---- src/tactic/core/simplify_tactic.cpp | 7 --- src/tactic/core/simplify_tactic.h | 2 - src/tactic/core/solve_eqs_tactic.cpp | 18 ++---- src/tactic/core/tseitin_cnf_tactic.cpp | 14 +---- src/tactic/extension_model_converter.cpp | 8 --- src/tactic/extension_model_converter.h | 2 - src/tactic/fpa/fpa2bv_tactic.cpp | 9 --- src/tactic/nlsat_smt/nl_purify_tactic.cpp | 15 +---- src/tactic/sls/sls_engine.cpp | 3 +- src/tactic/sls/sls_engine.h | 4 -- src/tactic/sls/sls_tactic.cpp | 4 -- src/tactic/tactic.cpp | 12 ---- src/tactic/tactic.h | 5 -- src/tactic/tactical.cpp | 55 ++----------------- src/tactic/ufbv/macro_finder_tactic.cpp | 10 +--- src/tactic/ufbv/quasi_macros_tactic.cpp | 12 +--- src/tactic/ufbv/ufbv_rewriter_tactic.cpp | 13 +---- 145 files changed, 172 insertions(+), 958 deletions(-) diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index d5901e97f..9d0abe3a7 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -75,7 +75,8 @@ namespace api { m_dtutil(m()), m_last_result(m()), m_ast_trail(m()), - m_replay_stack() { + m_replay_stack(), + m_pmanager(m_limit) { m_error_code = Z3_OK; m_print_mode = Z3_PRINT_SMTLIB_FULL; @@ -122,9 +123,8 @@ namespace api { { if (m_interruptable) (*m_interruptable)(); - m().set_cancel(true); - if (m_rcf_manager.get() != 0) - m_rcf_manager->set_cancel(true); + m_limit.cancel(); + m().limit().cancel(); } } @@ -323,7 +323,7 @@ namespace api { // ----------------------- realclosure::manager & context::rcfm() { if (m_rcf_manager.get() == 0) { - m_rcf_manager = alloc(realclosure::manager, m_rcf_qm); + m_rcf_manager = alloc(realclosure::manager, m_limit, m_rcf_qm); } return *(m_rcf_manager.get()); } diff --git a/src/api/api_context.h b/src/api/api_context.h index 2e7d89e7b..40b59d1b2 100644 --- a/src/api/api_context.h +++ b/src/api/api_context.h @@ -187,10 +187,12 @@ namespace api { // // ----------------------- private: + reslimit m_limit; pmanager m_pmanager; public: polynomial::manager & pm() { return m_pmanager.pm(); } - + reslimit & poly_limit() { return m_limit; } + // ------------------------ // // RCF manager diff --git a/src/api/api_polynomial.cpp b/src/api/api_polynomial.cpp index 93635507b..cecb63a7c 100644 --- a/src/api/api_polynomial.cpp +++ b/src/api/api_polynomial.cpp @@ -29,17 +29,13 @@ Notes: namespace api { - pmanager::pmanager(): - m_pm(m_nm) { + pmanager::pmanager(reslimit& lim): + m_pm(lim, m_nm) { } pmanager::~pmanager() { } - void pmanager::set_cancel(bool f) { - m_pm.set_cancel(f); - } - }; extern "C" { @@ -66,7 +62,7 @@ extern "C" { polynomial_ref r(pm); expr_ref _r(mk_c(c)->m()); { - cancel_eh eh(mk_c(c)->m().limit()); + cancel_eh eh(mk_c(c)->poly_limit()); api::context::set_interruptable si(*(mk_c(c)), eh); scoped_timer timer(mk_c(c)->params().m_timeout, &eh); pm.psc_chain(_p, _q, v_x, rs); diff --git a/src/api/api_polynomial.h b/src/api/api_polynomial.h index a5a0bd7c3..b93372ca9 100644 --- a/src/api/api_polynomial.h +++ b/src/api/api_polynomial.h @@ -28,10 +28,9 @@ namespace api { polynomial::manager m_pm; // TODO: add support for caching expressions -> polynomial and back public: - pmanager(); + pmanager(reslimit& limx); virtual ~pmanager(); polynomial::manager & pm() { return m_pm; } - void set_cancel(bool f); }; }; diff --git a/src/api/api_rcf.cpp b/src/api/api_rcf.cpp index 42558ba9e..a4770c56c 100644 --- a/src/api/api_rcf.cpp +++ b/src/api/api_rcf.cpp @@ -30,7 +30,7 @@ static rcmanager & rcfm(Z3_context c) { } static void reset_rcf_cancel(Z3_context c) { - rcfm(c).reset_cancel(); + // no-op } static Z3_rcf_num from_rcnumeral(rcnumeral a) { diff --git a/src/ast/arith_decl_plugin.cpp b/src/ast/arith_decl_plugin.cpp index 174082f8c..22751aa46 100644 --- a/src/ast/arith_decl_plugin.cpp +++ b/src/ast/arith_decl_plugin.cpp @@ -110,10 +110,6 @@ parameter arith_decl_plugin::translate(parameter const & p, decl_plugin & target return parameter(_target.aw().mk_id(aw().idx2anum(p.get_ext_id())), true); } -void arith_decl_plugin::set_cancel(bool f) { - if (m_aw) - m_aw->m_amanager.set_cancel(f); -} void arith_decl_plugin::set_manager(ast_manager * m, family_id id) { decl_plugin::set_manager(m, id); diff --git a/src/ast/arith_decl_plugin.h b/src/ast/arith_decl_plugin.h index 252bd8ed6..8df4234fa 100644 --- a/src/ast/arith_decl_plugin.h +++ b/src/ast/arith_decl_plugin.h @@ -211,7 +211,6 @@ public: virtual expr * get_some_value(sort * s); - virtual void set_cancel(bool f); }; /** @@ -398,9 +397,6 @@ public: return m_manager.mk_eq(lhs, rhs); } - void set_cancel(bool f) { - plugin().set_cancel(f); - } }; #endif /* ARITH_DECL_PLUGIN_H_ */ diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 111f1df78..2ee6c7556 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -1433,12 +1433,6 @@ ast_manager::~ast_manager() { } } -void ast_manager::set_cancel(bool f) { - for (unsigned i = 0; i < m_plugins.size(); i++) { - m_plugins[i]->set_cancel(f); - } -} - void ast_manager::compact_memory() { m_alloc.consolidate(); unsigned capacity = m_ast_table.capacity(); diff --git a/src/ast/ast.h b/src/ast/ast.h index 1348bf2f9..0c058fce8 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -932,7 +932,6 @@ public: virtual ~decl_plugin() {} virtual void finalize() {} - virtual void set_cancel(bool f) {} virtual decl_plugin * mk_fresh() = 0; @@ -1472,9 +1471,6 @@ public: ~ast_manager(); // propagate cancellation signal to decl_plugins - void set_cancel(bool f); - void cancel() { set_cancel(true); } - void reset_cancel() { set_cancel(false); } bool has_trace_stream() const { return m_trace_stream != 0; } std::ostream & trace_stream() { SASSERT(has_trace_stream()); return *m_trace_stream; } diff --git a/src/ast/normal_forms/name_exprs.cpp b/src/ast/normal_forms/name_exprs.cpp index eea7a924f..5a2e1659d 100644 --- a/src/ast/normal_forms/name_exprs.cpp +++ b/src/ast/normal_forms/name_exprs.cpp @@ -87,9 +87,6 @@ public: TRACE("name_exprs", tout << mk_ismt2_pp(n, m_rw.m()) << "\n---->\n" << mk_ismt2_pp(r, m_rw.m()) << "\n";); } - virtual void set_cancel(bool f) { - m_rw.set_cancel(f); - } virtual void reset() { m_rw.reset(); diff --git a/src/ast/normal_forms/name_exprs.h b/src/ast/normal_forms/name_exprs.h index 9d351375a..9403f3d12 100644 --- a/src/ast/normal_forms/name_exprs.h +++ b/src/ast/normal_forms/name_exprs.h @@ -37,9 +37,6 @@ public: proof_ref & p // [OUT] proof for (iff n p) ) = 0; - virtual void set_cancel(bool f) = 0; - void cancel() { set_cancel(true); } - void reset_cancel() { set_cancel(false); } virtual void reset() = 0; }; diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp index 81a610c50..e48a4fd2a 100644 --- a/src/ast/rewriter/arith_rewriter.cpp +++ b/src/ast/rewriter/arith_rewriter.cpp @@ -1032,9 +1032,6 @@ br_status arith_rewriter::mk_abs_core(expr * arg, expr_ref & result) { return BR_REWRITE2; } -void arith_rewriter::set_cancel(bool f) { - m_util.set_cancel(f); -} // Return true if t is of the form c*Pi where c is a numeral. // Store c into k diff --git a/src/ast/rewriter/arith_rewriter.h b/src/ast/rewriter/arith_rewriter.h index 6c8501ccb..68a60e1f0 100644 --- a/src/ast/rewriter/arith_rewriter.h +++ b/src/ast/rewriter/arith_rewriter.h @@ -167,8 +167,6 @@ public: } br_status mk_is_int(expr * arg, expr_ref & result); - void set_cancel(bool f); - br_status mk_sin_core(expr * arg, expr_ref & result); br_status mk_cos_core(expr * arg, expr_ref & result); br_status mk_tan_core(expr * arg, expr_ref & result); diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp index 0d78a8dc4..bf9e7f394 100644 --- a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp +++ b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp @@ -649,10 +649,6 @@ void bit_blaster_rewriter::updt_params(params_ref const& p) { m_imp->m_cfg.updt_params(p); } -void bit_blaster_rewriter::set_cancel(bool f) { - m_imp->set_cancel(f); - m_imp->m_blaster.set_cancel(f); -} void bit_blaster_rewriter::push() { m_imp->push(); diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.h b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.h index 3b4715657..b23daab3a 100644 --- a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.h +++ b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.h @@ -30,7 +30,6 @@ public: bit_blaster_rewriter(ast_manager & m, params_ref const & p); ~bit_blaster_rewriter(); void updt_params(params_ref const & p); - void set_cancel(bool f); ast_manager & m() const; unsigned get_num_steps() const; void cleanup(); diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_tpl.h b/src/ast/rewriter/bit_blaster/bit_blaster_tpl.h index b66cb7026..ea8209c61 100644 --- a/src/ast/rewriter/bit_blaster/bit_blaster_tpl.h +++ b/src/ast/rewriter/bit_blaster/bit_blaster_tpl.h @@ -36,7 +36,6 @@ protected: void mk_ext_rotate_left_right(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref_vector & out_bits); unsigned long long m_max_memory; - volatile bool m_cancel; bool m_use_wtm; /* Wallace Tree Multiplier */ bool m_use_bcm; /* Booth Multiplier for constants */ void checkpoint(); @@ -45,7 +44,6 @@ public: bit_blaster_tpl(Cfg const & cfg = Cfg(), unsigned long long max_memory = UINT64_MAX, bool use_wtm = false, bool use_bcm=false): Cfg(cfg), m_max_memory(max_memory), - m_cancel(false), m_use_wtm(use_wtm), m_use_bcm(use_bcm) { } @@ -54,9 +52,6 @@ public: m_max_memory = max_memory; } - void set_cancel(bool f) { m_cancel = f; } - void cancel() { set_cancel(true); } - void reset_cancel() { set_cancel(false); } // Cfg required API ast_manager & m() const { return Cfg::m(); } 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 9284ff420..74721d981 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 void bit_blaster_tpl::checkpoint() { if (memory::get_allocation_size() > m_max_memory) throw rewriter_exception(Z3_MAX_MEMORY_MSG); - if (m_cancel) + if (m().canceled()) throw rewriter_exception(Z3_CANCELED_MSG); cooperate("bit-blaster"); } diff --git a/src/ast/rewriter/der.cpp b/src/ast/rewriter/der.cpp index 4a4f438a7..83ed94ece 100644 --- a/src/ast/rewriter/der.cpp +++ b/src/ast/rewriter/der.cpp @@ -444,12 +444,6 @@ void der_rewriter::operator()(expr * t, expr_ref & result, proof_ref & result_pr m_imp->operator()(t, result, result_pr); } -void der_rewriter::set_cancel(bool f) { - #pragma omp critical (der_rewriter) - { - m_imp->set_cancel(f); - } -} void der_rewriter::cleanup() { ast_manager & m = m_imp->m(); diff --git a/src/ast/rewriter/der.h b/src/ast/rewriter/der.h index 07ff581dd..9de028be8 100644 --- a/src/ast/rewriter/der.h +++ b/src/ast/rewriter/der.h @@ -174,9 +174,6 @@ public: void operator()(expr * t, expr_ref & result, proof_ref & result_pr); - void cancel() { set_cancel(true); } - void reset_cancel() { set_cancel(false); } - void set_cancel(bool f); void cleanup(); void reset(); }; diff --git a/src/ast/rewriter/expr_replacer.cpp b/src/ast/rewriter/expr_replacer.cpp index 4265fc1ad..3552c7d49 100644 --- a/src/ast/rewriter/expr_replacer.cpp +++ b/src/ast/rewriter/expr_replacer.cpp @@ -107,9 +107,6 @@ public: } } - virtual void set_cancel(bool f) { - m_replacer.set_cancel(f); - } virtual unsigned get_num_steps() const { return m_replacer.get_num_steps(); @@ -146,10 +143,6 @@ public: m_r.reset_used_dependencies(); } - virtual void set_cancel(bool f) { - m_r.set_cancel(f); - } - virtual unsigned get_num_steps() const { return m_r.get_num_steps(); } diff --git a/src/ast/rewriter/expr_replacer.h b/src/ast/rewriter/expr_replacer.h index a770abe55..2e445eadc 100644 --- a/src/ast/rewriter/expr_replacer.h +++ b/src/ast/rewriter/expr_replacer.h @@ -39,9 +39,6 @@ public: virtual void operator()(expr * t, expr_ref & result); virtual void operator()(expr_ref & t) { expr_ref s(t, m()); (*this)(s, t); } - void cancel() { set_cancel(true); } - void reset_cancel() { set_cancel(false); } - virtual void set_cancel(bool f) = 0; virtual unsigned get_num_steps() const { return 0; } virtual void reset() = 0; diff --git a/src/ast/rewriter/rewriter.h b/src/ast/rewriter/rewriter.h index 812b07f96..934d186aa 100644 --- a/src/ast/rewriter/rewriter.h +++ b/src/ast/rewriter/rewriter.h @@ -212,7 +212,6 @@ protected: }; Config & m_cfg; unsigned m_num_steps; - volatile bool m_cancel; ptr_vector m_bindings; var_shifter m_shifter; expr_ref m_r; @@ -333,10 +332,6 @@ public: Config & cfg() { return m_cfg; } Config const & cfg() const { return m_cfg; } - void set_cancel(bool f) { m_cancel = f; } - void cancel() { set_cancel(true); } - void reset_cancel() { set_cancel(false); } - ~rewriter_tpl(); void reset(); diff --git a/src/ast/rewriter/rewriter_def.h b/src/ast/rewriter/rewriter_def.h index 77da6785f..44b5d192e 100644 --- a/src/ast/rewriter/rewriter_def.h +++ b/src/ast/rewriter/rewriter_def.h @@ -495,7 +495,6 @@ rewriter_tpl::rewriter_tpl(ast_manager & m, bool proof_gen, Config & cfg rewriter_core(m, proof_gen), m_cfg(cfg), m_num_steps(0), - m_cancel(false), m_shifter(m), m_r(m), m_pr(m), @@ -576,8 +575,6 @@ template void rewriter_tpl::resume_core(expr_ref & result, proof_ref & result_pr) { SASSERT(!frame_stack().empty()); while (!frame_stack().empty()) { - if (m_cancel) - throw rewriter_exception(Z3_CANCELED_MSG); if (!m().canceled()) { if (m().limit().cancel_flag_set()) { throw rewriter_exception(Z3_CANCELED_MSG); diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp index aa1b35b89..e2aca747b 100644 --- a/src/ast/rewriter/th_rewriter.cpp +++ b/src/ast/rewriter/th_rewriter.cpp @@ -685,9 +685,6 @@ struct th_rewriter_cfg : public default_rewriter_cfg { return false; } - void set_cancel(bool f) { - m_a_rw.set_cancel(f); - } }; template class rewriter_tpl; @@ -734,13 +731,6 @@ unsigned th_rewriter::get_num_steps() const { return m_imp->get_num_steps(); } -void th_rewriter::set_cancel(bool f) { - #pragma omp critical (th_rewriter) - { - m_imp->set_cancel(f); - m_imp->cfg().set_cancel(f); - } -} void th_rewriter::cleanup() { ast_manager & m = m_imp->m(); diff --git a/src/ast/rewriter/th_rewriter.h b/src/ast/rewriter/th_rewriter.h index 627ce0694..222625077 100644 --- a/src/ast/rewriter/th_rewriter.h +++ b/src/ast/rewriter/th_rewriter.h @@ -45,9 +45,6 @@ public: void operator()(expr * t, expr_ref & result, proof_ref & result_pr); void operator()(expr * n, unsigned num_bindings, expr * const * bindings, expr_ref & result); - void cancel() { set_cancel(true); } - void reset_cancel() { set_cancel(false); } - void set_cancel(bool f); void cleanup(); void reset(); diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 3eb710180..74cec1191 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -352,16 +352,15 @@ cmd_context::~cmd_context() { } void cmd_context::set_cancel(bool f) { - if (m_solver) { + if (has_manager()) { + m().set_cancel(f); if (f) { - m_solver->cancel(); + m().limit().cancel(); } else { - m_solver->reset_cancel(); + m().limit().reset_cancel(); } } - if (has_manager()) - m().set_cancel(f); } opt_wrapper* cmd_context::get_opt() { @@ -1453,7 +1452,7 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions else if (m_solver) { m_check_sat_result = m_solver.get(); // solver itself stores the result. m_solver->set_progress_callback(this); - cancel_eh eh(*m_solver); + cancel_eh eh(m().limit()); scoped_ctrl_c ctrlc(eh); scoped_timer timer(timeout, &eh); scoped_rlimit _rlimit(m().limit(), rlimit); @@ -1612,7 +1611,7 @@ void cmd_context::validate_model() { model_evaluator evaluator(*(md.get()), p); contains_array_op_proc contains_array(m()); { - cancel_eh eh(evaluator); + cancel_eh eh(m().limit()); expr_ref r(m()); scoped_ctrl_c ctrlc(eh); ptr_vector::const_iterator it = begin_assertions(); diff --git a/src/cmd_context/eval_cmd.cpp b/src/cmd_context/eval_cmd.cpp index 7ebe2f54f..318f7efaa 100644 --- a/src/cmd_context/eval_cmd.cpp +++ b/src/cmd_context/eval_cmd.cpp @@ -64,7 +64,7 @@ public: expr_ref r(ctx.m()); unsigned timeout = m_params.get_uint("timeout", UINT_MAX); model_evaluator ev(*(md.get()), m_params); - cancel_eh eh(ev); + cancel_eh eh(ctx.m().limit()); { scoped_ctrl_c ctrlc(eh); scoped_timer timer(timeout, &eh); diff --git a/src/cmd_context/extra_cmds/polynomial_cmds.cpp b/src/cmd_context/extra_cmds/polynomial_cmds.cpp index b045c236f..afd4713bd 100644 --- a/src/cmd_context/extra_cmds/polynomial_cmds.cpp +++ b/src/cmd_context/extra_cmds/polynomial_cmds.cpp @@ -33,7 +33,7 @@ Notes: static void to_poly(cmd_context & ctx, expr * t) { polynomial::numeral_manager nm; - polynomial::manager pm(nm); + polynomial::manager pm(ctx.m().limit(), nm); default_expr2polynomial expr2poly(ctx.m(), pm); polynomial::polynomial_ref p(pm); polynomial::scoped_numeral d(nm); @@ -52,7 +52,7 @@ static void to_poly(cmd_context & ctx, expr * t) { static void factor(cmd_context & ctx, expr * t, polynomial::factor_params const & ps) { polynomial::numeral_manager nm; - polynomial::manager pm(nm); + polynomial::manager pm(ctx.m().limit(), nm); default_expr2polynomial expr2poly(ctx.m(), pm); polynomial::polynomial_ref p(pm); polynomial::scoped_numeral d(nm); @@ -95,7 +95,7 @@ class poly_isolate_roots_cmd : public cmd { context(ast_manager & m): m_util(m), - m_pm(m_qm), + m_pm(m.limit(), m_qm), m_am(m_lim, m_qm), m_p(m_pm), m_expr2poly(m, m_pm), diff --git a/src/cmd_context/tactic_cmds.cpp b/src/cmd_context/tactic_cmds.cpp index de5abb874..54dd5510a 100644 --- a/src/cmd_context/tactic_cmds.cpp +++ b/src/cmd_context/tactic_cmds.cpp @@ -199,7 +199,7 @@ public: ctx.set_check_sat_result(result.get()); { tactic & t = *tref; - cancel_eh eh(t); + cancel_eh eh(m.limit()); { scoped_ctrl_c ctrlc(eh); scoped_timer timer(timeout, &eh); @@ -310,7 +310,7 @@ public: std::string reason_unknown; bool failed = false; - cancel_eh eh(t); + cancel_eh eh(m.limit()); { scoped_ctrl_c ctrlc(eh); scoped_timer timer(timeout, &eh); diff --git a/src/duality/duality_wrapper.h b/src/duality/duality_wrapper.h index b5027d7d2..e5e55efed 100644 --- a/src/duality/duality_wrapper.h +++ b/src/duality/duality_wrapper.h @@ -936,8 +936,7 @@ namespace Duality { void cancel(){ scoped_proof_mode spm(m(),m_mode); canceled = true; - if(m_solver) - m_solver->cancel(); + m().limit().cancel(); } unsigned get_scope_level(){ scoped_proof_mode spm(m(),m_mode); return m_solver->get_scope_level();} diff --git a/src/math/interval/interval.h b/src/math/interval/interval.h index 805cb3fda..4c0204604 100644 --- a/src/math/interval/interval.h +++ b/src/math/interval/interval.h @@ -21,6 +21,7 @@ Revision History: #include"mpq.h" #include"ext_numeral.h" +#include"rlimit.h" /** \brief Default configuration for interval manager. @@ -110,6 +111,7 @@ public: typedef typename numeral_manager::numeral numeral; typedef typename C::interval interval; private: + reslimit& m_limit; C m_c; numeral m_result_lower; numeral m_result_upper; @@ -127,7 +129,6 @@ private: interval m_3_pi_div_2; interval m_2_pi; - volatile bool m_cancel; void round_to_minus_inf() { m_c.round_to_minus_inf(); } void round_to_plus_inf() { m_c.round_to_plus_inf(); } @@ -161,11 +162,9 @@ private: void checkpoint(); public: - interval_manager(C const & c); + interval_manager(reslimit& lim, C const & c); ~interval_manager(); - void set_cancel(bool f) { m_cancel = f; } - numeral_manager & m() const { return m_c.m(); } void del(interval & a); diff --git a/src/math/interval/interval_def.h b/src/math/interval/interval_def.h index e529ceceb..aba4c3975 100644 --- a/src/math/interval/interval_def.h +++ b/src/math/interval/interval_def.h @@ -30,11 +30,10 @@ Revision History: // #define TRACE_NTH_ROOT template -interval_manager::interval_manager(C const & c):m_c(c) { +interval_manager::interval_manager(reslimit& lim, C const & c): m_limit(lim), m_c(c) { m().set(m_minus_one, -1); m().set(m_one, 1); m_pi_n = 0; - m_cancel = false; } template @@ -63,7 +62,7 @@ void interval_manager::del(interval & a) { template void interval_manager::checkpoint() { - if (m_cancel) + if (m_limit.canceled()) throw default_exception("canceled"); cooperate("interval"); } diff --git a/src/math/polynomial/algebraic_numbers.cpp b/src/math/polynomial/algebraic_numbers.cpp index fd92c52b5..5d6779d21 100644 --- a/src/math/polynomial/algebraic_numbers.cpp +++ b/src/math/polynomial/algebraic_numbers.cpp @@ -83,7 +83,6 @@ namespace algebraic_numbers { scoped_upoly m_add_tmp; polynomial::var m_x; polynomial::var m_y; - volatile bool m_cancel; // configuration int m_min_magnitude; @@ -104,8 +103,8 @@ namespace algebraic_numbers { m_qmanager(m), m_bqmanager(m), m_bqimanager(m_bqmanager), - m_pmanager(m, &a), - m_upmanager(m), + m_pmanager(lim, m, &a), + m_upmanager(lim, m), m_is_rational_tmp(m), m_isolate_tmp1(upm()), m_isolate_tmp2(upm()), @@ -118,7 +117,6 @@ namespace algebraic_numbers { m_add_tmp(upm()) { updt_params(p); reset_statistics(); - m_cancel = false; m_x = pm().mk_var(); m_y = pm().mk_var(); } @@ -126,14 +124,8 @@ namespace algebraic_numbers { ~imp() { } - void set_cancel(bool f) { - m_cancel = f; - pm().set_cancel(f); - upm().set_cancel(f); - } - void checkpoint() { - if (m_cancel) + if (!m_limit.inc()) throw algebraic_exception("canceled"); cooperate("algebraic"); } @@ -2785,10 +2777,6 @@ namespace algebraic_numbers { void manager::updt_params(params_ref const & p) { } - void manager::set_cancel(bool f) { - m_imp->set_cancel(f); - } - unsynch_mpq_manager & manager::qm() const { return m_imp->qm(); } diff --git a/src/math/polynomial/algebraic_numbers.h b/src/math/polynomial/algebraic_numbers.h index 13e20233c..e86be7752 100644 --- a/src/math/polynomial/algebraic_numbers.h +++ b/src/math/polynomial/algebraic_numbers.h @@ -64,10 +64,6 @@ namespace algebraic_numbers { static void get_param_descrs(param_descrs & r); static void collect_param_descrs(param_descrs & r) { get_param_descrs(r); } - void set_cancel(bool f); - void cancel() { set_cancel(true); } - void reset_cancel() { set_cancel(false); } - void updt_params(params_ref const & p); unsynch_mpq_manager & qm() const; diff --git a/src/math/polynomial/polynomial.cpp b/src/math/polynomial/polynomial.cpp index 5599156d5..4a12249e1 100644 --- a/src/math/polynomial/polynomial.cpp +++ b/src/math/polynomial/polynomial.cpp @@ -1829,6 +1829,7 @@ namespace polynomial { typedef _scoped_numeral scoped_numeral; typedef _scoped_numeral_vector scoped_numeral_vector; + reslimit& m_limit; manager & m_wrapper; numeral_manager m_manager; up_manager m_upm; @@ -1847,7 +1848,6 @@ namespace polynomial { unsigned_vector m_degree2pos; bool m_use_sparse_gcd; bool m_use_prs_gcd; - volatile bool m_cancel; // Debugging method: check if the coefficients of p are in the numeral_manager. bool consistent_coeffs(polynomial const * p) { @@ -2323,13 +2323,13 @@ namespace polynomial { inc_ref(m_unit_poly); m_use_sparse_gcd = true; m_use_prs_gcd = false; - m_cancel = false; } - imp(manager & w, unsynch_mpz_manager & m, monomial_manager * mm): + imp(reslimit& lim, manager & w, unsynch_mpz_manager & m, monomial_manager * mm): + m_limit(lim), m_wrapper(w), m_manager(m), - m_upm(m) { + m_upm(lim, m) { if (mm == 0) mm = alloc(monomial_manager); m_monomial_manager = mm; @@ -2337,10 +2337,11 @@ namespace polynomial { init(); } - imp(manager & w, unsynch_mpz_manager & m, small_object_allocator * a): + imp(reslimit& lim, manager & w, unsynch_mpz_manager & m, small_object_allocator * a): + m_limit(lim), m_wrapper(w), m_manager(m), - m_upm(m) { + m_upm(lim, m) { m_monomial_manager = alloc(monomial_manager, a); m_monomial_manager->inc_ref(); init(); @@ -2371,13 +2372,8 @@ namespace polynomial { m_monomial_manager->dec_ref(); } - void set_cancel(bool f) { - m_cancel = f; - m_upm.set_cancel(f); - } - void checkpoint() { - if (m_cancel) { + if (!m_limit.inc()) { throw polynomial_exception("canceled"); } cooperate("polynomial"); @@ -6883,12 +6879,12 @@ namespace polynomial { } }; - manager::manager(numeral_manager & m, monomial_manager * mm) { - m_imp = alloc(imp, *this, m, mm); + manager::manager(reslimit& lim, numeral_manager & m, monomial_manager * mm) { + m_imp = alloc(imp, lim, *this, m, mm); } - manager::manager(numeral_manager & m, small_object_allocator * a) { - m_imp = alloc(imp, *this, m, a); + manager::manager(reslimit& lim, numeral_manager & m, small_object_allocator * a) { + m_imp = alloc(imp, lim, *this, m, a); } manager::~manager() { @@ -6927,10 +6923,6 @@ namespace polynomial { return m_imp->mm().allocator(); } - void manager::set_cancel(bool f) { - m_imp->set_cancel(f); - } - void manager::add_del_eh(del_eh * eh) { m_imp->add_del_eh(eh); } diff --git a/src/math/polynomial/polynomial.h b/src/math/polynomial/polynomial.h index 3a4442e63..cb1880495 100644 --- a/src/math/polynomial/polynomial.h +++ b/src/math/polynomial/polynomial.h @@ -28,6 +28,7 @@ Notes: #include"scoped_numeral_vector.h" #include"params.h" #include"mpbqi.h" +#include"rlimit.h" class small_object_allocator; @@ -190,8 +191,8 @@ namespace polynomial { private: imp * m_imp; public: - manager(numeral_manager & m, monomial_manager * mm = 0); - manager(numeral_manager & m, small_object_allocator * a); + manager(reslimit& lim, numeral_manager & m, monomial_manager * mm = 0); + manager(reslimit& lim, numeral_manager & m, small_object_allocator * a); ~manager(); numeral_manager & m() const; @@ -218,10 +219,6 @@ namespace polynomial { void set_zp(numeral const & p); void set_zp(uint64 p); - void set_cancel(bool f); - void cancel() { set_cancel(true); } - void reset_cancel() { set_cancel(false); } - /** \brief Abstract event handler. */ diff --git a/src/math/polynomial/rpolynomial.cpp b/src/math/polynomial/rpolynomial.cpp index 2ae90bf69..03cfac8c8 100644 --- a/src/math/polynomial/rpolynomial.cpp +++ b/src/math/polynomial/rpolynomial.cpp @@ -58,7 +58,6 @@ namespace rpolynomial { numeral_manager & m_manager; small_object_allocator * m_allocator; bool m_own_allocator; - volatile bool m_cancel; imp(manager & w, numeral_manager & m, small_object_allocator * a): m_wrapper(w), @@ -67,7 +66,6 @@ namespace rpolynomial { m_own_allocator(a == 0) { if (a == 0) m_allocator = alloc(small_object_allocator, "rpolynomial"); - m_cancel = false; } ~imp() { diff --git a/src/math/polynomial/rpolynomial.h b/src/math/polynomial/rpolynomial.h index de2140c5e..b84dcca95 100644 --- a/src/math/polynomial/rpolynomial.h +++ b/src/math/polynomial/rpolynomial.h @@ -57,8 +57,6 @@ namespace rpolynomial { numeral_manager & m() const; small_object_allocator & allocator() const; - void set_cancel(bool f); - /** \brief Create a new variable. */ diff --git a/src/math/polynomial/upolynomial.cpp b/src/math/polynomial/upolynomial.cpp index e2bf322d6..3068df33c 100644 --- a/src/math/polynomial/upolynomial.cpp +++ b/src/math/polynomial/upolynomial.cpp @@ -134,9 +134,9 @@ namespace upolynomial { std::swap(m_total_degree, other.m_total_degree); } - core_manager::core_manager(unsynch_mpz_manager & m): + core_manager::core_manager(reslimit& lim, unsynch_mpz_manager & m): + m_limit(lim), m_manager(m) { - m_cancel = false; } core_manager::~core_manager() { @@ -153,12 +153,8 @@ namespace upolynomial { reset(m_pw_tmp); } - void core_manager::set_cancel(bool f) { - m_cancel = f; - } - void core_manager::checkpoint() { - if (m_cancel) + if (!m_limit.inc()) throw upolynomial_exception("canceled"); cooperate("upolynomial"); } diff --git a/src/math/polynomial/upolynomial.h b/src/math/polynomial/upolynomial.h index 32214c5db..789759dc6 100644 --- a/src/math/polynomial/upolynomial.h +++ b/src/math/polynomial/upolynomial.h @@ -29,6 +29,7 @@ Notes: #include"polynomial.h" #include"z3_exception.h" #include"mpbq.h" +#include"rlimit.h" #define FACTOR_VERBOSE_LVL 1000 namespace upolynomial { @@ -101,6 +102,7 @@ namespace upolynomial { }; protected: + reslimit& m_limit; numeral_manager m_manager; numeral_vector m_basic_tmp; numeral_vector m_div_tmp1; @@ -114,7 +116,6 @@ namespace upolynomial { numeral_vector m_sqf_tmp1; numeral_vector m_sqf_tmp2; numeral_vector m_pw_tmp; - volatile bool m_cancel; static bool is_alias(numeral const * p, numeral_vector & buffer) { return buffer.c_ptr() != 0 && buffer.c_ptr() == p; } void neg_core(unsigned sz1, numeral const * p1, numeral_vector & buffer); @@ -128,12 +129,12 @@ namespace upolynomial { void CRA_combine_images(numeral_vector const & q, numeral const & p, numeral_vector & C, numeral & bound); public: - core_manager(z_numeral_manager & m); + core_manager(reslimit& lim, z_numeral_manager & m); ~core_manager(); z_numeral_manager & zm() const { return m_manager.m(); } numeral_manager & m() const { return const_cast(this)->m_manager; } - + reslimit& lim() const { return m_limit; } /** \brief Return true if Z_p[X] */ @@ -156,7 +157,6 @@ namespace upolynomial { void checkpoint(); - void set_cancel(bool f); /** \brief set p size to 0. That is, p is the zero polynomial after this operation. @@ -576,7 +576,7 @@ namespace upolynomial { bool factor_core(unsigned sz, numeral const * p, factors & r, factor_params const & params); public: - manager(z_numeral_manager & m):core_manager(m) {} + manager(reslimit& lim, z_numeral_manager & m):core_manager(lim, m) {} ~manager(); void reset(numeral_vector & p) { core_manager::reset(p); } diff --git a/src/math/polynomial/upolynomial_factorization.cpp b/src/math/polynomial/upolynomial_factorization.cpp index 0b2977a22..b36658bba 100644 --- a/src/math/polynomial/upolynomial_factorization.cpp +++ b/src/math/polynomial/upolynomial_factorization.cpp @@ -518,7 +518,7 @@ bool check_hansel_lift(z_manager & upm, numeral_vector const & C, scoped_mpz br(nm); nm.mul(b, r, br); - zp_manager br_upm(upm.zm()); + zp_manager br_upm(upm.lim(), upm.zm()); br_upm.set_zp(br); if (A_lifted.size() != A.size()) return false; @@ -543,7 +543,7 @@ bool check_hansel_lift(z_manager & upm, numeral_vector const & C, return false; } - zp_manager b_upm(nm); + zp_manager b_upm(upm.lim(), nm); b_upm.set_zp(b); // test2: A_lifted = A (mod b) @@ -596,7 +596,7 @@ void hensel_lift(z_manager & upm, numeral const & a, numeral const & b, numeral tout << "C = "; upm.display(tout, C); tout << ")" << endl; ); - zp_manager r_upm(nm); + zp_manager r_upm(upm.lim(), nm); r_upm.set_zp(r); SASSERT(upm.degree(C) == upm.degree(A) + upm.degree(B)); @@ -717,7 +717,7 @@ void hensel_lift_quadratic(z_manager& upm, numeral_vector const & C, ); // we create a new Z_p manager, since we'll be changing the input one - zp_manager zp_upm(nm); + zp_manager zp_upm(upm.lim(), nm); zp_upm.set_zp(zpe_upm.m().p()); // get the U, V, such that A*U + B*V = 1 (mod p) @@ -1055,7 +1055,7 @@ bool factor_square_free(z_manager & upm, numeral_vector const & f, factors & fs, // the variables we'll be using and updating in Z_p scoped_numeral p(nm); nm.set(p, 2); - zp_manager zp_upm(nm.m()); + zp_manager zp_upm(upm.lim(), nm.m()); zp_upm.set_zp(p); zp_factors zp_fs(zp_upm); scoped_numeral zp_fs_p(nm); nm.set(zp_fs_p, 2); @@ -1163,7 +1163,7 @@ bool factor_square_free(z_manager & upm, numeral_vector const & f, factors & fs, ); // we got a prime factoring, so we do the lifting now - zp_manager zpe_upm(nm.m()); + zp_manager zpe_upm(upm.lim(), nm.m()); zpe_upm.set_zp(zp_fs_p); zp_numeral_manager & zpe_nm = zpe_upm.m(); diff --git a/src/math/realclosure/realclosure.cpp b/src/math/realclosure/realclosure.cpp index 1ca8823a1..13a9ab030 100644 --- a/src/math/realclosure/realclosure.cpp +++ b/src/math/realclosure/realclosure.cpp @@ -369,6 +369,7 @@ namespace realclosure { typedef sbuffer int_buffer; typedef sbuffer unsigned_buffer; + reslimit& m_limit; small_object_allocator * m_allocator; bool m_own_allocator; unsynch_mpq_manager & m_qm; @@ -400,7 +401,6 @@ namespace realclosure { bool m_in_aux_values; // True if we are computing SquareFree polynomials or Sturm sequences. That is, the values being computed will be discarded. - volatile bool m_cancel; struct scoped_polynomial_seq { typedef ref_buffer value_seq; @@ -494,7 +494,8 @@ namespace realclosure { #define INC_DEPTH() ((void) 0) #endif - imp(unsynch_mpq_manager & qm, params_ref const & p, small_object_allocator * a): + imp(reslimit& lim, unsynch_mpq_manager & qm, params_ref const & p, small_object_allocator * a): + m_limit(lim), m_allocator(a == 0 ? alloc(small_object_allocator, "realclosure") : a), m_own_allocator(a == 0), m_qm(qm), @@ -514,7 +515,6 @@ namespace realclosure { m_in_aux_values = false; - m_cancel = false; updt_params(p); } @@ -547,7 +547,7 @@ namespace realclosure { small_object_allocator & allocator() { return *m_allocator; } void checkpoint() { - if (m_cancel) + if (!m_limit.inc()) throw exception("canceled"); cooperate("rcf"); } @@ -730,9 +730,6 @@ namespace realclosure { return m_extensions[extension::ALGEBRAIC].size(); } - void set_cancel(bool f) { - m_cancel = f; - } void updt_params(params_ref const & _p) { rcf_params p(_p); @@ -6033,8 +6030,8 @@ namespace realclosure { ~save_interval_ctx() { m->restore_saved_intervals(); } }; - manager::manager(unsynch_mpq_manager & m, params_ref const & p, small_object_allocator * a) { - m_imp = alloc(imp, m, p, a); + manager::manager(reslimit& lim, unsynch_mpq_manager & m, params_ref const & p, small_object_allocator * a) { + m_imp = alloc(imp, lim, m, p, a); } manager::~manager() { @@ -6045,10 +6042,6 @@ namespace realclosure { rcf_params::collect_param_descrs(r); } - void manager::set_cancel(bool f) { - m_imp->set_cancel(f); - } - void manager::updt_params(params_ref const & p) { m_imp->updt_params(p); } diff --git a/src/math/realclosure/realclosure.h b/src/math/realclosure/realclosure.h index 4fef4dc25..10d35f58d 100644 --- a/src/math/realclosure/realclosure.h +++ b/src/math/realclosure/realclosure.h @@ -28,6 +28,7 @@ Notes: #include"scoped_numeral_vector.h" #include"interval.h" #include"z3_exception.h" +#include"rlimit.h" namespace realclosure { class num; @@ -47,7 +48,7 @@ namespace realclosure { friend class save_interval_ctx; imp * m_imp; public: - manager(unsynch_mpq_manager & m, params_ref const & p = params_ref(), small_object_allocator * a = 0); + manager(reslimit& lim, unsynch_mpq_manager & m, params_ref const & p = params_ref(), small_object_allocator * a = 0); ~manager(); typedef num numeral; typedef svector numeral_vector; @@ -57,9 +58,6 @@ namespace realclosure { static void get_param_descrs(param_descrs & r); static void collect_param_descrs(param_descrs & r) { get_param_descrs(r); } - void set_cancel(bool f); - void cancel() { set_cancel(true); } - void reset_cancel() { set_cancel(false); } void updt_params(params_ref const & p); diff --git a/src/math/simplex/simplex.h b/src/math/simplex/simplex.h index 06fcd54ec..277179507 100644 --- a/src/math/simplex/simplex.h +++ b/src/math/simplex/simplex.h @@ -97,7 +97,6 @@ namespace simplex { mutable eps_manager em; mutable matrix M; unsigned m_max_iterations; - volatile bool m_cancel; var_heap m_to_patch; vector m_vars; svector m_row2base; diff --git a/src/math/subpaving/subpaving_t.h b/src/math/subpaving/subpaving_t.h index a24199451..f138899cc 100644 --- a/src/math/subpaving/subpaving_t.h +++ b/src/math/subpaving/subpaving_t.h @@ -31,6 +31,7 @@ Revision History: #include"statistics.h" #include"lbool.h" #include"id_gen.h" +#include"rlimit.h" #ifdef _MSC_VER #pragma warning(disable : 4200) #pragma warning(disable : 4355) @@ -526,8 +527,6 @@ private: numeral m_tmp1, m_tmp2, m_tmp3; interval m_i_tmp1, m_i_tmp2, m_i_tmp3; - // Cancel flag - volatile bool m_cancel; friend class node; @@ -759,7 +758,7 @@ private: bool check_invariant() const; public: - context_t(C const & c, params_ref const & p, small_object_allocator * a); + context_t(reslimit& lim, C const & c, params_ref const & p, small_object_allocator * a); ~context_t(); /** @@ -835,8 +834,6 @@ public: void set_display_proc(display_var_proc * p) { m_display_proc = p; } - void set_cancel(bool f) { m_cancel = f; im().set_cancel(f); } - void updt_params(params_ref const & p); static void collect_param_descrs(param_descrs & d); diff --git a/src/math/subpaving/subpaving_t_def.h b/src/math/subpaving/subpaving_t_def.h index c215ddf98..f94692532 100644 --- a/src/math/subpaving/subpaving_t_def.h +++ b/src/math/subpaving/subpaving_t_def.h @@ -431,7 +431,6 @@ context_t::context_t(C const & c, params_ref const & p, small_object_allocato m_node_selector = alloc(breadth_first_node_selector, this); m_var_selector = alloc(round_robing_var_selector, this); m_node_splitter = alloc(midpoint_node_splitter, this); - m_cancel = false; m_num_nodes = 0; updt_params(p); reset_statistics(); @@ -459,7 +458,7 @@ context_t::~context_t() { template void context_t::checkpoint() { - if (m_cancel) + if (m_limit.canceled()) throw default_exception("canceled"); if (memory::get_allocation_size() > m_max_memory) throw default_exception(Z3_MAX_MEMORY_MSG); diff --git a/src/math/subpaving/tactic/expr2subpaving.cpp b/src/math/subpaving/tactic/expr2subpaving.cpp index ba8dac208..9968c2f62 100644 --- a/src/math/subpaving/tactic/expr2subpaving.cpp +++ b/src/math/subpaving/tactic/expr2subpaving.cpp @@ -51,7 +51,6 @@ struct expr2subpaving::imp { obj_map m_lit_cache; - volatile bool m_cancel; imp(ast_manager & m, subpaving::context & s, expr2var * e2v): m_manager(m), @@ -71,7 +70,6 @@ struct expr2subpaving::imp { m_expr2var_owner = false; } - m_cancel = false; } ~imp() { @@ -95,7 +93,7 @@ struct expr2subpaving::imp { } void checkpoint() { - if (m_cancel) + if (m().canceled()) throw default_exception("canceled"); cooperate("expr2subpaving"); } @@ -357,9 +355,6 @@ struct expr2subpaving::imp { return m_expr2var->is_var(t); } - void set_cancel(bool f) { - m_cancel = f; - } subpaving::var internalize_term(expr * t, mpz & n, mpz & d) { return process(t, 0, n, d); @@ -386,9 +381,6 @@ bool expr2subpaving::is_var(expr * t) const { return m_imp->is_var(t); } -void expr2subpaving::set_cancel(bool f) { - m_imp->set_cancel(f); -} subpaving::var expr2subpaving::internalize_term(expr * t, mpz & n, mpz & d) { return m_imp->internalize_term(t, n, d); diff --git a/src/math/subpaving/tactic/expr2subpaving.h b/src/math/subpaving/tactic/expr2subpaving.h index 7373ecf1e..8e6e69332 100644 --- a/src/math/subpaving/tactic/expr2subpaving.h +++ b/src/math/subpaving/tactic/expr2subpaving.h @@ -40,12 +40,7 @@ public: \brief Return true if t was encoded as a variable by the translator. */ bool is_var(expr * t) const; - - /** - \brief Cancel/Interrupt execution. - */ - void set_cancel(bool f); - + /** \brief Internalize a Z3 arithmetical expression into the subpaving data-structure. diff --git a/src/math/subpaving/tactic/subpaving_tactic.cpp b/src/math/subpaving/tactic/subpaving_tactic.cpp index d03bacebb..35935ff22 100644 --- a/src/math/subpaving/tactic/subpaving_tactic.cpp +++ b/src/math/subpaving/tactic/subpaving_tactic.cpp @@ -124,7 +124,6 @@ class subpaving_tactic : public tactic { } void set_cancel(bool f) { - m_e2s->set_cancel(f); m_ctx->set_cancel(f); } @@ -279,11 +278,6 @@ public: } } -protected: - virtual void set_cancel(bool f) { - if (m_imp) - m_imp->set_cancel(f); - } }; diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp index 8ee2fb9cc..2baedacdd 100644 --- a/src/model/model_evaluator.cpp +++ b/src/model/model_evaluator.cpp @@ -256,12 +256,6 @@ unsigned model_evaluator::get_num_steps() const { return m_imp->get_num_steps(); } -void model_evaluator::set_cancel(bool f) { - #pragma omp critical (model_evaluator) - { - m_imp->set_cancel(f); - } -} void model_evaluator::cleanup(params_ref const & p) { model & md = m_imp->cfg().m_model; diff --git a/src/model/model_evaluator.h b/src/model/model_evaluator.h index 0884c1850..e0d76ec01 100644 --- a/src/model/model_evaluator.h +++ b/src/model/model_evaluator.h @@ -41,9 +41,6 @@ public: void operator()(expr * t, expr_ref & r); - void set_cancel(bool f); - void cancel() { set_cancel(true); } - void reset_cancel() { set_cancel(false); } void cleanup(params_ref const & p = params_ref()); void reset(params_ref const & p = params_ref()); diff --git a/src/muz/fp/horn_tactic.cpp b/src/muz/fp/horn_tactic.cpp index a77c97f3f..c1a74f5c7 100644 --- a/src/muz/fp/horn_tactic.cpp +++ b/src/muz/fp/horn_tactic.cpp @@ -63,9 +63,6 @@ class horn_tactic : public tactic { m_ctx.collect_statistics(st); } - void set_cancel(bool f) { - } - void normalize(expr_ref& f) { bool is_positive = true; expr* e = 0; @@ -420,11 +417,7 @@ public: } } -protected: - virtual void set_cancel(bool f) { - if (m_imp) - m_imp->set_cancel(f); - } + }; tactic * mk_horn_tactic(ast_manager & m, params_ref const & p) { diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index 1a90bb886..52a204191 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -141,7 +141,6 @@ namespace nlsat { svector m_trail; anum m_zero; - bool m_cancel; // configuration unsigned long long m_max_memory; @@ -164,7 +163,7 @@ namespace nlsat { m_solver(s), m_rlimit(rlim), m_allocator("nlsat"), - m_pm(m_qm, &m_allocator), + m_pm(rlim, m_qm, &m_allocator), m_cache(m_pm), m_am(rlim, m_qm, p, &m_allocator), m_asm(*this, m_allocator), @@ -180,7 +179,6 @@ namespace nlsat { m_lemma_assumptions(m_asm) { updt_params(p); reset_statistics(); - m_cancel = false; mk_true_bvar(); } @@ -218,15 +216,11 @@ namespace nlsat { m_am.updt_params(p.p); } - void set_cancel(bool f) { - m_pm.set_cancel(f); - m_am.set_cancel(f); - m_cancel = f; - } - void checkpoint() { - if (m_cancel) throw solver_exception(Z3_CANCELED_MSG); - if (!m_rlimit.inc()) throw solver_exception(Z3_MAX_RESOURCE_MSG); + if (!m_rlimit.inc()) { + if (m_rlimit.cancel_flag_set()) throw solver_exception(Z3_CANCELED_MSG); + throw solver_exception(Z3_MAX_RESOURCE_MSG); + } if (memory::get_allocation_size() > m_max_memory) throw solver_exception(Z3_MAX_MEMORY_MSG); } @@ -2571,10 +2565,6 @@ namespace nlsat { return m_imp->check(); } - void solver::set_cancel(bool f) { - m_imp->set_cancel(f); - } - void solver::collect_param_descrs(param_descrs & d) { algebraic_numbers::manager::collect_param_descrs(d); nlsat_params::collect_param_descrs(d); diff --git a/src/nlsat/nlsat_solver.h b/src/nlsat/nlsat_solver.h index d99f4371a..2875bbc8c 100644 --- a/src/nlsat/nlsat_solver.h +++ b/src/nlsat/nlsat_solver.h @@ -154,7 +154,6 @@ namespace nlsat { void updt_params(params_ref const & p); static void collect_param_descrs(param_descrs & d); - void set_cancel(bool f); void collect_statistics(statistics & st); void reset_statistics(); void display_status(std::ostream & out) const; diff --git a/src/nlsat/tactic/goal2nlsat.cpp b/src/nlsat/tactic/goal2nlsat.cpp index 1af98c7e8..031dc5ff5 100644 --- a/src/nlsat/tactic/goal2nlsat.cpp +++ b/src/nlsat/tactic/goal2nlsat.cpp @@ -61,7 +61,6 @@ struct goal2nlsat::imp { unsigned long long m_max_memory; bool m_factor; - volatile bool m_cancel; imp(ast_manager & _m, params_ref const & p, nlsat::solver & s, expr2var & a2b, expr2var & t2x): m(_m), @@ -73,7 +72,6 @@ struct goal2nlsat::imp { m_t2x(t2x), m_expr2poly(m_solver, m, m_solver.pm(), &m_t2x) { updt_params(p); - m_cancel = false; } void updt_params(params_ref const & p) { @@ -82,11 +80,6 @@ struct goal2nlsat::imp { m_fparams.updt_params(p); } - void set_cancel(bool f) { - m_cancel = f; - m_pm.set_cancel(f); - } - nlsat::atom::kind flip(nlsat::atom::kind k) { switch (k) { case nlsat::atom::EQ: return k; @@ -303,7 +296,3 @@ void goal2nlsat::operator()(goal const & g, params_ref const & p, nlsat::solver local_imp(g); } -void goal2nlsat::set_cancel(bool f) { - if (m_imp) - m_imp->set_cancel(f); -} diff --git a/src/nlsat/tactic/goal2nlsat.h b/src/nlsat/tactic/goal2nlsat.h index 0d65b72d5..ae9bbdb74 100644 --- a/src/nlsat/tactic/goal2nlsat.h +++ b/src/nlsat/tactic/goal2nlsat.h @@ -51,7 +51,6 @@ public: */ void operator()(goal const & g, params_ref const & p, nlsat::solver & s, expr2var & a2b, expr2var & t2x); - void set_cancel(bool f); }; class nlsat2goal { @@ -69,7 +68,6 @@ public: void operator()(nlsat::solver const & s, expr2var const & a2b, expr2var const & t2x, params_ref const & p, goal & g, model_converter_ref & mc); - void set_cancel(bool f); }; #endif diff --git a/src/nlsat/tactic/nlsat_tactic.cpp b/src/nlsat/tactic/nlsat_tactic.cpp index 348e68da1..8ab6ed83f 100644 --- a/src/nlsat/tactic/nlsat_tactic.cpp +++ b/src/nlsat/tactic/nlsat_tactic.cpp @@ -57,11 +57,6 @@ class nlsat_tactic : public tactic { m_params = p; m_solver.updt_params(p); } - - void set_cancel(bool f) { - m_solver.set_cancel(f); - m_g2nl.set_cancel(f); - } bool contains_unsupported(expr_ref_vector & b2a, expr_ref_vector & x2t) { for (unsigned x = 0; x < x2t.size(); x++) { @@ -240,11 +235,6 @@ public: virtual void cleanup() {} - virtual void set_cancel(bool f) { - if (m_imp) - m_imp->set_cancel(f); - } - virtual void collect_statistics(statistics & st) const { st.copy(m_stats); } diff --git a/src/opt/mus.cpp b/src/opt/mus.cpp index 27361a4f9..aa8446256 100644 --- a/src/opt/mus.cpp +++ b/src/opt/mus.cpp @@ -33,25 +33,20 @@ struct mus::imp { ast_manager& m; expr_ref_vector m_cls2expr; obj_map m_expr2cls; - volatile bool m_cancel; model_ref m_model; expr_ref_vector m_soft; vector m_weights; rational m_weight; imp(solver& s, ast_manager& m): - m_s(s), m(m), m_cls2expr(m), m_cancel(false), m_soft(m) + m_s(s), m(m), m_cls2expr(m), m_soft(m) {} void reset() { m_cls2expr.reset(); m_expr2cls.reset(); } - - void set_cancel(bool f) { - m_cancel = f; - } - + unsigned add_soft(expr* cls) { SASSERT(is_uninterp_const(cls) || @@ -216,9 +211,6 @@ lbool mus::get_mus(unsigned_vector& mus) { return m_imp->get_mus(mus); } -void mus::set_cancel(bool f) { - m_imp->set_cancel(f); -} void mus::reset() { m_imp->reset(); diff --git a/src/opt/mus.h b/src/opt/mus.h index b58a303e8..8ca7ab91d 100644 --- a/src/opt/mus.h +++ b/src/opt/mus.h @@ -39,8 +39,6 @@ namespace opt { void reset(); - void set_cancel(bool f); - /** Instrument MUS extraction to also provide the minimal penalty model, if any is found. diff --git a/src/opt/opt_cmds.cpp b/src/opt/opt_cmds.cpp index 7041265de..0a62caf3c 100644 --- a/src/opt/opt_cmds.cpp +++ b/src/opt/opt_cmds.cpp @@ -195,7 +195,7 @@ public: opt.add_hard_constraint(*it); } lbool r = l_undef; - cancel_eh eh(opt); + cancel_eh eh(m.limit()); { scoped_ctrl_c ctrlc(eh); scoped_timer timer(timeout, &eh); diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp index 195567a29..78b52a9ea 100644 --- a/src/opt/opt_solver.cpp +++ b/src/opt/opt_solver.cpp @@ -297,11 +297,7 @@ namespace opt { m_context.get_relevant_labels(0, tmp); r.append(tmp.size(), tmp.c_ptr()); } - - void opt_solver::set_cancel(bool f) { - m_context.set_cancel(f); - } - + void opt_solver::set_progress_callback(progress_callback * callback) { m_callback = callback; m_context.set_progress_callback(callback); diff --git a/src/opt/opt_solver.h b/src/opt/opt_solver.h index a12c7ffb0..7337b86ed 100644 --- a/src/opt/opt_solver.h +++ b/src/opt/opt_solver.h @@ -100,11 +100,11 @@ namespace opt { virtual proof * get_proof(); virtual std::string reason_unknown() const; virtual void get_labels(svector & r); - virtual void set_cancel(bool f); virtual void set_progress_callback(progress_callback * callback); virtual unsigned get_num_assertions() const; virtual expr * get_assertion(unsigned idx) const; virtual void display(std::ostream & out) const; + virtual ast_manager& get_manager() { return m; } void set_logic(symbol const& logic); smt::theory_var add_objective(app* term); diff --git a/src/sat/sat_mus.cpp b/src/sat/sat_mus.cpp index 9791db118..b5abc7544 100644 --- a/src/sat/sat_mus.cpp +++ b/src/sat/sat_mus.cpp @@ -84,7 +84,7 @@ namespace sat { tout << "core: " << core << "\n"; tout << "mus: " << mus << "\n";); - if (s.m_cancel) { + if (s.canceled()) { set_core(); return l_undef; } diff --git a/src/sat/sat_sls.cpp b/src/sat/sat_sls.cpp index 24f952ea9..76e222f02 100644 --- a/src/sat/sat_sls.cpp +++ b/src/sat/sat_sls.cpp @@ -50,7 +50,7 @@ namespace sat { return m_elems[rnd(num_elems())]; } - sls::sls(solver& s): s(s), m_cancel(false) { + sls::sls(solver& s): s(s) { m_prob_choose_min_var = 43; m_clause_generation = 0; } @@ -64,7 +64,7 @@ namespace sat { lbool sls::operator()(unsigned sz, literal const* tabu, bool reuse_model) { init(sz, tabu, reuse_model); unsigned i; - for (i = 0; !m_false.empty() && !m_cancel && i < m_max_tries; ++i) { + for (i = 0; !m_false.empty() && !s.canceled() && i < m_max_tries; ++i) { flip(); } IF_VERBOSE(2, verbose_stream() << "tries " << i << "\n";); @@ -378,7 +378,7 @@ namespace sat { } DEBUG_CODE(check_invariant();); unsigned i = 0; - for (; !m_cancel && m_best_value > 0 && i < m_max_tries; ++i) { + for (; !s.canceled() && m_best_value > 0 && i < m_max_tries; ++i) { wflip(); if (m_false.empty()) { double val = evaluate_model(m_model); diff --git a/src/sat/sat_sls.h b/src/sat/sat_sls.h index 7ea472083..f1bf55543 100644 --- a/src/sat/sat_sls.h +++ b/src/sat/sat_sls.h @@ -54,12 +54,10 @@ namespace sat { clause_allocator m_alloc; // clause allocator clause_vector m_bin_clauses; // binary clauses svector m_tabu; // variables that cannot be swapped - volatile bool m_cancel; public: sls(solver& s); virtual ~sls(); lbool operator()(unsigned sz, literal const* tabu, bool reuse_model); - void set_cancel(bool f) { m_cancel = f; } void set_max_tries(unsigned mx) { m_max_tries = mx; } virtual void display(std::ostream& out) const; protected: diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 008ba8a18..f636c726b 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -32,7 +32,6 @@ Revision History: namespace sat { solver::solver(params_ref const & p, reslimit& l, extension * ext): - m_cancel(false), m_rlimit(l), m_config(p), m_ext(ext), @@ -2714,11 +2713,6 @@ namespace sat { scc::collect_param_descrs(d); } - void solver::set_cancel(bool f) { - m_cancel = f; - m_wsls.set_cancel(f); - } - void solver::collect_statistics(statistics & st) const { m_stats.collect_statistics(st); m_cleaner.collect_statistics(st); @@ -2784,7 +2778,7 @@ namespace sat { // // ----------------------- bool solver::check_invariant() const { - if (m_cancel) return true; + if (!m_rlimit.inc()) return true; integrity_checker checker(*this); SASSERT(checker()); return true; diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index 23033d940..95988f3ca 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -71,7 +71,6 @@ namespace sat { public: struct abort_solver {}; protected: - volatile bool m_cancel; reslimit& m_rlimit; config m_config; stats m_stats; @@ -158,7 +157,6 @@ namespace sat { void updt_params(params_ref const & p); static void collect_param_descrs(param_descrs & d); - void set_cancel(bool f); void collect_statistics(statistics & st) const; void reset_statistics(); void display_status(std::ostream & out) const; @@ -239,13 +237,13 @@ namespace sat { lbool status(clause const & c) const; clause_offset get_offset(clause const & c) const { return m_cls_allocator.get_offset(&c); } void checkpoint() { - if (m_cancel) throw solver_exception(Z3_CANCELED_MSG); - if (!m_rlimit.inc()) { m_cancel = true; throw solver_exception(Z3_CANCELED_MSG); } + if (!m_rlimit.inc()) { throw solver_exception(Z3_CANCELED_MSG); } ++m_num_checkpoints; if (m_num_checkpoints < 10) return; m_num_checkpoints = 0; if (memory::get_allocation_size() > m_config.m_max_memory) throw solver_exception(Z3_MAX_MEMORY_MSG); } + bool canceled() { return !m_rlimit.inc(); } typedef std::pair bin_clause; protected: watch_list & get_wlist(literal l) { return m_watches[l.index()]; } diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 3f2700053..4f002f20b 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -85,7 +85,6 @@ public: simp2_p.set_bool("flat", true); // required by som simp2_p.set_bool("hoist_mul", false); // required by som simp2_p.set_bool("elim_and", true); - m_preprocess = and_then(mk_card2bv_tactic(m, m_params), using_params(mk_simplify_tactic(m), simp2_p), @@ -169,11 +168,6 @@ public: } return r; } - virtual void set_cancel(bool f) { - m_goal2sat.set_cancel(f); - m_solver.set_cancel(f); - if (f) m_preprocess->cancel(); else m_preprocess->reset_cancel(); - } virtual void push() { internalize_formulas(); m_solver.user_push(); @@ -215,6 +209,7 @@ public: assert_expr(t); } } + virtual ast_manager& get_manager() { return m; } virtual void assert_expr(expr * t) { TRACE("sat", tout << mk_pp(t, m) << "\n";); m_fmls.push_back(t); diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index 9f066e33b..4e649862a 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -58,7 +58,6 @@ struct goal2sat::imp { sat::bool_var m_true; bool m_ite_extra; unsigned long long m_max_memory; - volatile bool m_cancel; expr_ref_vector m_trail; bool m_default_external; @@ -70,7 +69,6 @@ struct goal2sat::imp { m_trail(m), m_default_external(default_external) { updt_params(p); - m_cancel = false; m_true = sat::null_bool_var; } @@ -334,7 +332,7 @@ struct goal2sat::imp { while (!m_frame_stack.empty()) { loop: cooperate("goal2sat"); - if (m_cancel) + if (m.canceled()) throw tactic_exception(TACTIC_CANCELED_MSG); if (memory::get_allocation_size() > m_max_memory) throw tactic_exception(TACTIC_MAX_MEMORY_MSG); @@ -442,7 +440,6 @@ struct goal2sat::imp { process(fs[i]); } - void set_cancel(bool f) { m_cancel = f; } }; struct unsupported_bool_proc { @@ -507,14 +504,6 @@ void goal2sat::operator()(goal const & g, params_ref const & p, sat::solver & t, proc(g); } -void goal2sat::set_cancel(bool f) { - #pragma omp critical (goal2sat) - { - if (m_imp) - m_imp->set_cancel(f); - } -} - struct sat2goal::imp { @@ -631,9 +620,8 @@ struct sat2goal::imp { expr_ref_vector m_lit2expr; unsigned long long m_max_memory; bool m_learned; - volatile bool m_cancel; - imp(ast_manager & _m, params_ref const & p):m(_m), m_lit2expr(m), m_cancel(false) { + imp(ast_manager & _m, params_ref const & p):m(_m), m_lit2expr(m) { updt_params(p); } @@ -643,7 +631,7 @@ struct sat2goal::imp { } void checkpoint() { - if (m_cancel) + if (m.canceled()) throw tactic_exception(TACTIC_CANCELED_MSG); if (memory::get_allocation_size() > m_max_memory) throw tactic_exception(TACTIC_MAX_MEMORY_MSG); @@ -731,7 +719,6 @@ struct sat2goal::imp { assert_clauses(s.begin_learned(), s.end_learned(), r); } - void set_cancel(bool f) { m_cancel = f; } }; sat2goal::sat2goal():m_imp(0) { @@ -765,10 +752,3 @@ void sat2goal::operator()(sat::solver const & t, atom2bool_var const & m, params proc(t, m, g, mc); } -void sat2goal::set_cancel(bool f) { - #pragma omp critical (sat2goal) - { - if (m_imp) - m_imp->set_cancel(f); - } -} diff --git a/src/sat/tactic/goal2sat.h b/src/sat/tactic/goal2sat.h index e1f78d916..c6776f2f7 100644 --- a/src/sat/tactic/goal2sat.h +++ b/src/sat/tactic/goal2sat.h @@ -59,7 +59,6 @@ public: */ void operator()(goal const & g, params_ref const & p, sat::solver & t, atom2bool_var & m, dep2asm_map& dep2asm, bool default_external = false); - void set_cancel(bool f); }; @@ -83,7 +82,6 @@ public: */ void operator()(sat::solver const & t, atom2bool_var const & m, params_ref const & p, goal & s, model_converter_ref & mc); - void set_cancel(bool f); }; #endif diff --git a/src/sat/tactic/sat_tactic.cpp b/src/sat/tactic/sat_tactic.cpp index f04100ca2..d6ec1dff0 100644 --- a/src/sat/tactic/sat_tactic.cpp +++ b/src/sat/tactic/sat_tactic.cpp @@ -123,11 +123,6 @@ class sat_tactic : public tactic { result.push_back(g.get()); } - void set_cancel(bool f) { - m_goal2sat.set_cancel(f); - m_sat2goal.set_cancel(f); - m_solver.set_cancel(f); - } void dep2assumptions(obj_map& dep2asm, sat::literal_vector& assumptions) { @@ -223,13 +218,6 @@ public: } protected: - virtual void set_cancel(bool f) { - #pragma omp critical (sat_tactic) - { - if (m_imp) - m_imp->set_cancel(f); - } - } }; diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp index b66e15cb2..6543bddad 100644 --- a/src/smt/asserted_formulas.cpp +++ b/src/smt/asserted_formulas.cpp @@ -54,8 +54,7 @@ asserted_formulas::asserted_formulas(ast_manager & m, smt_params & p): m_macro_manager(m, m_simplifier), m_bit2int(m), m_bv_sharing(m), - m_inconsistent(false), - m_cancel_flag(false) { + m_inconsistent(false){ m_bsimp = 0; m_bvsimp = 0; @@ -223,9 +222,6 @@ void asserted_formulas::reset() { m_inconsistent = false; } -void asserted_formulas::set_cancel_flag(bool f) { - m_cancel_flag = f; -} #ifdef Z3DEBUG bool asserted_formulas::check_well_sorted() const { diff --git a/src/smt/asserted_formulas.h b/src/smt/asserted_formulas.h index 33781abf6..8478311dc 100644 --- a/src/smt/asserted_formulas.h +++ b/src/smt/asserted_formulas.h @@ -62,7 +62,6 @@ class asserted_formulas { bool m_inconsistent_old; }; svector m_scopes; - volatile bool m_cancel_flag; void setup_simplifier_plugins(simplifier & s, basic_simplifier_plugin * & bsimp, arith_simplifier_plugin * & asimp, bv_simplifier_plugin * & bvsimp); void reduce_asserted_formulas(); @@ -97,7 +96,7 @@ class asserted_formulas { unsigned get_total_size() const; bool has_bv() const; void max_bv_sharing(); - bool canceled() { return m_cancel_flag; } + bool canceled() { return m_manager.canceled(); } public: asserted_formulas(ast_manager & m, smt_params & p); diff --git a/src/smt/expr_context_simplifier.h b/src/smt/expr_context_simplifier.h index 07183ad12..7745bffff 100644 --- a/src/smt/expr_context_simplifier.h +++ b/src/smt/expr_context_simplifier.h @@ -77,7 +77,6 @@ public: void collect_statistics(statistics & st) const { m_solver.collect_statistics(st); } void reset_statistics() { m_solver.reset_statistics(); } - void set_cancel(bool f) { m_solver.set_cancel(f); } }; #endif /* EXPR_CONTEXT_SIMPLIFIER_H_ */ diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 18a00d7ff..26ca2e68a 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -45,7 +45,6 @@ namespace smt { m_fparams(p), m_params(_p), m_setup(*this, p), - m_cancel_flag(false), m_asserted_formulas(m, p), m_qmanager(alloc(quantifier_manager, *this, p, _p)), m_model_generator(alloc(model_generator, m)), @@ -3069,11 +3068,6 @@ namespace smt { if (m_manager.has_trace_stream()) m_manager.trace_stream() << "[begin-check] " << m_scope_lvl << "\n"; - if (reset_cancel) { - m_cancel_flag = false; - m_asserted_formulas.set_cancel_flag(false); - } - if (memory::above_high_watermark()) { m_last_search_failure = MEMOUT; return false; @@ -4154,11 +4148,6 @@ namespace smt { return m_last_search_failure; } - void context::set_cancel_flag(bool f) { - m_cancel_flag = f; - m_asserted_formulas.set_cancel_flag(f); - } - }; #ifdef Z3DEBUG diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 08d68c723..fd1049626 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -79,7 +79,6 @@ namespace smt { smt_params & m_fparams; params_ref m_params; setup m_setup; - volatile bool m_cancel_flag; timer m_timer; asserted_formulas m_asserted_formulas; scoped_ptr m_qmanager; @@ -233,9 +232,8 @@ namespace smt { return m_params; } - virtual void set_cancel_flag(bool f = true); - bool get_cancel_flag() { return m_cancel_flag || !m_manager.limit().inc(); } + bool get_cancel_flag() { return !m_manager.limit().inc(); } region & get_region() { return m_region; diff --git a/src/smt/smt_kernel.cpp b/src/smt/smt_kernel.cpp index de0f91d97..f390b2f33 100644 --- a/src/smt/smt_kernel.cpp +++ b/src/smt/smt_kernel.cpp @@ -169,10 +169,6 @@ namespace smt { void display_istatistics(std::ostream & out) const { m_kernel.display_istatistics(out); } - - void set_cancel(bool f) { - m_kernel.set_cancel_flag(f); - } bool canceled() { return m_kernel.get_cancel_flag(); @@ -328,14 +324,6 @@ namespace smt { m_imp->display_istatistics(out); } - void kernel::set_cancel(bool f) { - #pragma omp critical (smt_kernel) - { - if (m_imp) - m_imp->set_cancel(f); - } - } - bool kernel::canceled() const { return m_imp->canceled(); } diff --git a/src/smt/smt_kernel.h b/src/smt/smt_kernel.h index a7a467964..ce429151b 100644 --- a/src/smt/smt_kernel.h +++ b/src/smt/smt_kernel.h @@ -204,18 +204,7 @@ namespace smt { \brief Display statistics in low level format. */ void display_istatistics(std::ostream & out) const; - - /** - \brief Interrupt the kernel. - */ - void set_cancel(bool f = true); - void cancel() { set_cancel(true); } - - /** - \brief Reset interruption. - */ - void reset_cancel() { set_cancel(false); } - + /** \brief Return true if the kernel was interrupted. */ diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index 5104291e8..3d84483e5 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -101,9 +101,8 @@ namespace smt { r.append(tmp.size(), tmp.c_ptr()); } - virtual void set_cancel(bool f) { - m_context.set_cancel(f); - } + virtual ast_manager& get_manager() { return m_context.m(); } + virtual void set_progress_callback(progress_callback * callback) { m_callback = callback; diff --git a/src/smt/tactic/ctx_solver_simplify_tactic.cpp b/src/smt/tactic/ctx_solver_simplify_tactic.cpp index 622d67a34..d59ef5254 100644 --- a/src/smt/tactic/ctx_solver_simplify_tactic.cpp +++ b/src/smt/tactic/ctx_solver_simplify_tactic.cpp @@ -35,12 +35,10 @@ class ctx_solver_simplify_tactic : public tactic { func_decl_ref m_fn; obj_map m_fns; unsigned m_num_steps; - volatile bool m_cancel; public: ctx_solver_simplify_tactic(ast_manager & m, params_ref const & p = params_ref()): m(m), m_params(p), m_solver(m, m_front_p), - m_arith(m), m_mk_app(m), m_fn(m), m_num_steps(0), - m_cancel(false) { + m_arith(m), m_mk_app(m), m_fn(m), m_num_steps(0) { sort* i_sort = m_arith.mk_int(); m_fn = m.mk_func_decl(symbol(0xbeef101), i_sort, m.mk_bool_sort()); } @@ -86,15 +84,10 @@ public: virtual void cleanup() { reset_statistics(); m_solver.reset(); - m_cancel = false; } protected: - virtual void set_cancel(bool f) { - m_solver.set_cancel(f); - m_cancel = false; - } void reduce(goal& g) { SASSERT(g.is_well_sorted()); @@ -177,7 +170,7 @@ protected: names.push_back(n); m_solver.push(); - while (!todo.empty() && !m_cancel) { + while (!todo.empty() && !m.canceled()) { expr_ref res(m); args.reset(); expr* e = todo.back().m_expr; @@ -249,7 +242,7 @@ protected: names.pop_back(); m_solver.pop(1); } - if (!m_cancel) { + if (!m.canceled()) { VERIFY(cache.find(fml, path_r)); result = path_r.m_expr; } diff --git a/src/smt/tactic/smt_tactic.cpp b/src/smt/tactic/smt_tactic.cpp index a42f00274..4ae31d778 100644 --- a/src/smt/tactic/smt_tactic.cpp +++ b/src/smt/tactic/smt_tactic.cpp @@ -132,10 +132,6 @@ public: smt_params_helper::collect_param_descrs(r); } - virtual void set_cancel(bool f) { - if (m_ctx) - m_ctx->set_cancel(f); - } virtual void collect_statistics(statistics & st) const { if (m_ctx) diff --git a/src/smt/tactic/unit_subsumption_tactic.cpp b/src/smt/tactic/unit_subsumption_tactic.cpp index afc81723a..ab7b40a26 100644 --- a/src/smt/tactic/unit_subsumption_tactic.cpp +++ b/src/smt/tactic/unit_subsumption_tactic.cpp @@ -22,7 +22,6 @@ struct unit_subsumption_tactic : public tactic { ast_manager& m; params_ref m_params; smt_params m_fparams; - volatile bool m_cancel; smt::context m_context; expr_ref_vector m_clauses; unsigned m_clause_count; @@ -34,19 +33,11 @@ struct unit_subsumption_tactic : public tactic { params_ref const& p): m(m), m_params(p), - m_cancel(false), m_context(m, m_fparams, p), m_clauses(m) { } - - void set_cancel(bool f) { - m_cancel = f; - m_context.set_cancel_flag(f); - } - virtual void cleanup() { - set_cancel(false); - } + void cleanup() {} virtual void operator()(/* in */ goal_ref const & in, /* out */ goal_ref_buffer & result, @@ -66,7 +57,7 @@ struct unit_subsumption_tactic : public tactic { } void checkpoint() { - if (m_cancel) { + if (m.canceled()) { throw tactic_exception(TACTIC_CANCELED_MSG); } } diff --git a/src/solver/check_sat_result.h b/src/solver/check_sat_result.h index 5d63d1a7c..73a24fc7b 100644 --- a/src/solver/check_sat_result.h +++ b/src/solver/check_sat_result.h @@ -52,6 +52,7 @@ public: virtual proof * get_proof() = 0; virtual std::string reason_unknown() const = 0; virtual void get_labels(svector & r) = 0; + virtual ast_manager& get_manager() = 0; }; /** @@ -63,9 +64,11 @@ struct simple_check_sat_result : public check_sat_result { expr_ref_vector m_core; proof_ref m_proof; std::string m_unknown; + simple_check_sat_result(ast_manager & m); virtual ~simple_check_sat_result(); + virtual ast_manager& get_manager() { return m_proof.get_manager(); } virtual void collect_statistics(statistics & st) const; virtual void get_unsat_core(ptr_vector & r); virtual void get_model(model_ref & m); diff --git a/src/solver/combined_solver.cpp b/src/solver/combined_solver.cpp index 85f84e26e..91e1b8bf5 100644 --- a/src/solver/combined_solver.cpp +++ b/src/solver/combined_solver.cpp @@ -84,7 +84,7 @@ private: volatile bool m_canceled; aux_timeout_eh(solver * s):m_solver(s), m_canceled(false) {} virtual void operator()() { - m_solver->cancel(); + m_solver->get_manager().cancel(); m_canceled = true; } }; @@ -96,6 +96,8 @@ private: m_inc_unknown_behavior = static_cast(p.solver2_unknown()); } + virtual ast_manager& get_manager() { return m_solver1->get_manager(); } + bool has_quantifiers() const { unsigned sz = get_num_assertions(); for (unsigned i = 0; i < sz; i++) { @@ -220,25 +222,18 @@ public: m_use_solver1_results = false; 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";); + IF_VERBOSE(PS_VB_LVL, verbose_stream() << "(combined-solver \"solver 2 failed, trying solver1\")\n";); + } IF_VERBOSE(PS_VB_LVL, verbose_stream() << "(combined-solver \"using solver 1\")\n";); m_use_solver1_results = true; return m_solver1->check_sat(0, 0); } - - virtual void set_cancel(bool f) { - if (f) { - m_solver1->cancel(); - m_solver2->cancel(); - } - else { - m_solver1->reset_cancel(); - m_solver2->reset_cancel(); - } - } virtual void set_progress_callback(progress_callback * callback) { m_solver1->set_progress_callback(callback); diff --git a/src/solver/solver.h b/src/solver/solver.h index 8b5e98433..a53ea07ee 100644 --- a/src/solver/solver.h +++ b/src/solver/solver.h @@ -108,11 +108,11 @@ public: /** \brief Interrupt this solver. */ - void cancel() { set_cancel(true); } + //void cancel() { set_cancel(true); } /** \brief Reset the interruption. */ - void reset_cancel() { set_cancel(false); } + //void reset_cancel() { set_cancel(false); } /** \brief Set a progress callback procedure that is invoked by this solver during check_sat. @@ -158,7 +158,7 @@ public: }; protected: - virtual void set_cancel(bool f) = 0; + //virtual void set_cancel(bool f) = 0; }; #endif diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp index 02b9bd347..f66132f00 100644 --- a/src/solver/tactic2solver.cpp +++ b/src/solver/tactic2solver.cpp @@ -59,7 +59,6 @@ public: virtual void pop_core(unsigned n); virtual lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions); - virtual void set_cancel(bool f); virtual void collect_statistics(statistics & st) const; virtual void get_unsat_core(ptr_vector & r); @@ -74,8 +73,11 @@ public: virtual expr * get_assertion(unsigned idx) const; virtual void display(std::ostream & out) const; + virtual ast_manager& get_manager(); }; +ast_manager& tactic2solver::get_manager() { return m_assertions.get_manager(); } + tactic2solver::tactic2solver(ast_manager & m, tactic * t, params_ref const & p, bool produce_proofs, bool produce_models, bool produce_unsat_cores, symbol const & logic): solver_na2as(m), m_assertions(m) { @@ -177,14 +179,6 @@ lbool tactic2solver::check_sat_core(unsigned num_assumptions, expr * const * ass return m_result->status(); } -void tactic2solver::set_cancel(bool f) { - if (m_tactic.get()) { - if (f) - m_tactic->cancel(); - else - m_tactic->reset_cancel(); - } -} solver* tactic2solver::translate(ast_manager& m, params_ref const& p) { tactic* t = m_tactic->translate(m); diff --git a/src/solver/tactic2solver.h b/src/solver/tactic2solver.h index 22038bcc5..9158a00b7 100644 --- a/src/solver/tactic2solver.h +++ b/src/solver/tactic2solver.h @@ -37,6 +37,7 @@ solver * mk_tactic2solver(ast_manager & m, bool produce_unsat_cores = false, symbol const & logic = symbol::null); + solver_factory * mk_tactic2solver_factory(tactic * t); solver_factory * mk_tactic_factory2solver_factory(tactic_factory * f); diff --git a/src/tactic/aig/aig.cpp b/src/tactic/aig/aig.cpp index e3101ad67..3f5e7bdfe 100644 --- a/src/tactic/aig/aig.cpp +++ b/src/tactic/aig/aig.cpp @@ -119,7 +119,6 @@ struct aig_manager::imp { aig_lit m_false; bool m_default_gate_encoding; unsigned long long m_max_memory; - volatile bool m_cancel; void dec_ref_core(aig * n) { SASSERT(n->m_ref_count > 0); @@ -131,7 +130,7 @@ struct aig_manager::imp { void checkpoint() { if (memory::get_allocation_size() > m_max_memory) throw aig_exception(TACTIC_MAX_MEMORY_MSG); - if (m_cancel) + if (m().canceled()) throw aig_exception(TACTIC_CANCELED_MSG); cooperate("aig"); } @@ -1309,8 +1308,7 @@ public: m_num_aigs(0), m_var2exprs(m), m_allocator("aig"), - m_true(mk_var(m.mk_true())), - m_cancel(false) { + m_true(mk_var(m.mk_true())) { SASSERT(is_true(m_true)); m_false = m_true; m_false.invert(); @@ -1328,7 +1326,6 @@ public: ast_manager & m() const { return m_var2exprs.get_manager(); } - void set_cancel(bool f) { m_cancel = f; } void inc_ref(aig * n) { n->m_ref_count++; } void inc_ref(aig_lit const & r) { inc_ref(r.ptr()); } @@ -1754,8 +1751,5 @@ unsigned aig_manager::get_num_aigs() const { return m_imp->get_num_aigs(); } -void aig_manager::set_cancel(bool f) { - m_imp->set_cancel(f); -} diff --git a/src/tactic/aig/aig.h b/src/tactic/aig/aig.h index 69babe677..fbbde7de6 100644 --- a/src/tactic/aig/aig.h +++ b/src/tactic/aig/aig.h @@ -73,7 +73,6 @@ public: void display(std::ostream & out, aig_ref const & r) const; void display_smt2(std::ostream & out, aig_ref const & r) const; unsigned get_num_aigs() const; - void set_cancel(bool f); }; #endif diff --git a/src/tactic/aig/aig_tactic.cpp b/src/tactic/aig/aig_tactic.cpp index f1f1c7330..76495d7e4 100644 --- a/src/tactic/aig/aig_tactic.cpp +++ b/src/tactic/aig/aig_tactic.cpp @@ -111,14 +111,6 @@ public: virtual void cleanup() {} -protected: - virtual void set_cancel(bool f) { - #pragma omp critical (aig_tactic) - { - if (m_aig_manager) - m_aig_manager->set_cancel(f); - } - } }; tactic * mk_aig_tactic(params_ref const & p) { diff --git a/src/tactic/arith/add_bounds_tactic.cpp b/src/tactic/arith/add_bounds_tactic.cpp index 9bf967be3..dba8c0bde 100644 --- a/src/tactic/arith/add_bounds_tactic.cpp +++ b/src/tactic/arith/add_bounds_tactic.cpp @@ -62,7 +62,6 @@ class add_bounds_tactic : public tactic { ast_manager & m; rational m_lower; rational m_upper; - volatile bool m_cancel; imp(ast_manager & _m, params_ref const & p): m(_m) { @@ -74,9 +73,6 @@ class add_bounds_tactic : public tactic { m_upper = p.get_rat("add_bound_upper", rational(2)); } - void set_cancel(bool f) { - m_cancel = f; - } struct add_bound_proc { arith_util m_util; @@ -180,11 +176,6 @@ public: dealloc(d); } -protected: - virtual void set_cancel(bool f) { - if (m_imp) - m_imp->set_cancel(f); - } }; tactic * mk_add_bounds_tactic(ast_manager & m, params_ref const & p) { diff --git a/src/tactic/arith/arith_bounds_tactic.cpp b/src/tactic/arith/arith_bounds_tactic.cpp index 83b5c6daf..1111d7f1f 100644 --- a/src/tactic/arith/arith_bounds_tactic.cpp +++ b/src/tactic/arith/arith_bounds_tactic.cpp @@ -13,24 +13,15 @@ struct arith_bounds_tactic : public tactic { ast_manager& m; arith_util a; - volatile bool m_cancel; arith_bounds_tactic(ast_manager& m): m(m), - a(m), - m_cancel(false) + a(m) { } ast_manager& get_manager() { return m; } - void set_cancel(bool f) { - m_cancel = f; - } - - virtual void cleanup() { - m_cancel = false; - } virtual void operator()(/* in */ goal_ref const & in, /* out */ goal_ref_buffer & result, @@ -45,7 +36,7 @@ struct arith_bounds_tactic : public tactic { } void checkpoint() { - if (m_cancel) { + if (m.canceled()) { throw tactic_exception(TACTIC_CANCELED_MSG); } } @@ -155,6 +146,7 @@ struct arith_bounds_tactic : public tactic { TRACE("arith_subsumption", s->display(tout); ); } + virtual void cleanup() {} }; diff --git a/src/tactic/arith/card2bv_tactic.cpp b/src/tactic/arith/card2bv_tactic.cpp index 3ef1d786d..7d7097958 100644 --- a/src/tactic/arith/card2bv_tactic.cpp +++ b/src/tactic/arith/card2bv_tactic.cpp @@ -462,10 +462,6 @@ public: virtual void collect_param_descrs(param_descrs & r) { } - void set_cancel(bool f) { - m_rw1.set_cancel(f); - m_rw2.set_cancel(f); - } virtual void operator()(goal_ref const & g, goal_ref_buffer & result, diff --git a/src/tactic/arith/degree_shift_tactic.cpp b/src/tactic/arith/degree_shift_tactic.cpp index e8fb72be4..55b88ba51 100644 --- a/src/tactic/arith/degree_shift_tactic.cpp +++ b/src/tactic/arith/degree_shift_tactic.cpp @@ -40,7 +40,6 @@ class degree_shift_tactic : public tactic { rational m_one; bool m_produce_models; bool m_produce_proofs; - volatile bool m_cancel; expr * mk_power(expr * t, rational const & k) { if (k.is_one()) @@ -96,15 +95,11 @@ class degree_shift_tactic : public tactic { m_pinned(_m), m_one(1), m_rw(0) { - m_cancel = false; } - void set_cancel(bool f) { - m_cancel = f; - } void checkpoint() { - if (m_cancel) + if (m.canceled()) throw tactic_exception(TACTIC_CANCELED_MSG); cooperate("degree_shift"); } @@ -326,12 +321,7 @@ public: } dealloc(d); } - -protected: - virtual void set_cancel(bool f) { - if (m_imp) - m_imp->set_cancel(f); - } + }; tactic * mk_degree_shift_tactic(ast_manager & m, params_ref const & p) { diff --git a/src/tactic/arith/diff_neq_tactic.cpp b/src/tactic/arith/diff_neq_tactic.cpp index 1a33bf4f2..7f03c05b2 100644 --- a/src/tactic/arith/diff_neq_tactic.cpp +++ b/src/tactic/arith/diff_neq_tactic.cpp @@ -45,7 +45,6 @@ class diff_neq_tactic : public tactic { vector m_var_diseqs; typedef svector decision_stack; decision_stack m_stack; - volatile bool m_cancel; bool m_produce_models; rational m_max_k; @@ -58,7 +57,6 @@ class diff_neq_tactic : public tactic { u(m), m_var2expr(m) { updt_params(p); - m_cancel = false; } void updt_params(params_ref const & p) { @@ -67,11 +65,7 @@ class diff_neq_tactic : public tactic { if (m_max_k >= rational(INT_MAX/2)) m_max_k = rational(INT_MAX/2); } - - void set_cancel(bool f) { - m_cancel = f; - } - + void throw_not_supported() { throw tactic_exception("goal is not diff neq"); } @@ -294,7 +288,7 @@ class diff_neq_tactic : public tactic { init_forbidden(); unsigned nvars = num_vars(); while (m_stack.size() < nvars) { - if (m_cancel) + if (m.canceled()) throw tactic_exception(TACTIC_CANCELED_MSG); TRACE("diff_neq_tactic", display_model(tout);); var x = m_stack.size(); @@ -407,11 +401,6 @@ public: dealloc(d); } -protected: - virtual void set_cancel(bool f) { - if (m_imp) - m_imp->set_cancel(f); - } }; tactic * mk_diff_neq_tactic(ast_manager & m, params_ref const & p) { diff --git a/src/tactic/arith/elim01_tactic.cpp b/src/tactic/arith/elim01_tactic.cpp index dda3d8fc9..1aef52d78 100644 --- a/src/tactic/arith/elim01_tactic.cpp +++ b/src/tactic/arith/elim01_tactic.cpp @@ -136,10 +136,7 @@ public: virtual ~elim01_tactic() { } - - void set_cancel(bool f) { - } - + virtual void updt_params(params_ref const & p) { m_max_hi = rational(p.get_uint("max_coefficient", m_max_hi_default)); m_params = p; diff --git a/src/tactic/arith/eq2bv_tactic.cpp b/src/tactic/arith/eq2bv_tactic.cpp index 7cba66a5a..7957edbc4 100644 --- a/src/tactic/arith/eq2bv_tactic.cpp +++ b/src/tactic/arith/eq2bv_tactic.cpp @@ -139,9 +139,6 @@ public: virtual ~eq2bv_tactic() { } - void set_cancel(bool f) { - m_rw.set_cancel(f); - } void updt_params(params_ref const & p) { } diff --git a/src/tactic/arith/factor_tactic.cpp b/src/tactic/arith/factor_tactic.cpp index dc17a4f87..f00ff81c9 100644 --- a/src/tactic/arith/factor_tactic.cpp +++ b/src/tactic/arith/factor_tactic.cpp @@ -34,7 +34,7 @@ class factor_tactic : public tactic { rw_cfg(ast_manager & _m, params_ref const & p): m(_m), m_util(_m), - m_pm(m_qm), + m_pm(m.limit(), m_qm), m_expr2poly(m, m_pm) { updt_params(p); } @@ -251,10 +251,6 @@ class factor_tactic : public tactic { m_rw(m, p) { } - void set_cancel(bool f) { - m_rw.set_cancel(f); - m_rw.cfg().m_pm.set_cancel(f); - } void updt_params(params_ref const & p) { m_rw.cfg().updt_params(p); @@ -341,10 +337,7 @@ public: dealloc(d); } - virtual void set_cancel(bool f) { - if (m_imp) - m_imp->set_cancel(f); - } + }; tactic * mk_factor_tactic(ast_manager & m, params_ref const & p) { diff --git a/src/tactic/arith/fix_dl_var_tactic.cpp b/src/tactic/arith/fix_dl_var_tactic.cpp index 6d9f98f39..d9a3150fc 100644 --- a/src/tactic/arith/fix_dl_var_tactic.cpp +++ b/src/tactic/arith/fix_dl_var_tactic.cpp @@ -247,11 +247,7 @@ class fix_dl_var_tactic : public tactic { void updt_params(params_ref const & p) { m_rw.updt_params(p); } - - void set_cancel(bool f) { - m_rw.set_cancel(f); - } - + void operator()(goal_ref const & g, goal_ref_buffer & result, model_converter_ref & mc, @@ -345,11 +341,6 @@ public: } dealloc(d); } - - virtual void set_cancel(bool f) { - if (m_imp) - m_imp->set_cancel(f); - } }; tactic * mk_fix_dl_var_tactic(ast_manager & m, params_ref const & p) { diff --git a/src/tactic/arith/fm_tactic.cpp b/src/tactic/arith/fm_tactic.cpp index 8d7a0eab0..722b3db30 100644 --- a/src/tactic/arith/fm_tactic.cpp +++ b/src/tactic/arith/fm_tactic.cpp @@ -44,7 +44,6 @@ class fm_tactic : public tactic { ast_manager & m; ptr_vector m_xs; vector m_clauses; - volatile bool m_cancel; enum r_kind { NONE, @@ -182,7 +181,6 @@ class fm_tactic : public tactic { virtual void operator()(model_ref & md, unsigned goal_idx) { TRACE("fm_mc", model_v2_pp(tout, *md); display(tout);); - m_cancel = false; model_evaluator ev(*(md.get())); ev.set_model_completion(true); arith_util u(m); @@ -199,7 +197,7 @@ 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_cancel) throw tactic_exception(TACTIC_CANCELED_MSG); + if (m.canceled()) throw tactic_exception(TACTIC_CANCELED_MSG); switch (process(x, *it, u, ev, val)) { case NONE: TRACE("fm_mc", tout << "no bound for:\n" << mk_ismt2_pp(*it, m) << "\n";); @@ -244,9 +242,6 @@ class fm_tactic : public tactic { TRACE("fm_mc", model_v2_pp(tout, *md);); } - virtual void cancel() { - m_cancel = true; - } virtual void display(std::ostream & out) { out << "(fm-model-converter"; @@ -394,7 +389,6 @@ class fm_tactic : public tactic { obj_hashtable m_forbidden_set; // variables that cannot be eliminated because occur in non OCC ineq part goal_ref m_new_goal; ref m_mc; - volatile bool m_cancel; id_gen m_id_gen; bool m_produce_models; bool m_fm_real_only; @@ -784,7 +778,6 @@ class fm_tactic : public tactic { m_var2expr(m), m_inconsistent_core(m) { updt_params(p); - m_cancel = false; } ~imp() { @@ -801,9 +794,6 @@ class fm_tactic : public tactic { m_fm_occ = p.get_bool("fm_occ", false); } - void set_cancel(bool f) { - m_cancel = f; - } struct forbidden_proc { imp & m_owner; @@ -1552,7 +1542,7 @@ class fm_tactic : public tactic { void checkpoint() { cooperate("fm"); - if (m_cancel) + if (m.canceled()) throw tactic_exception(TACTIC_CANCELED_MSG); if (memory::get_allocation_size() > m_max_memory) throw tactic_exception(TACTIC_MAX_MEMORY_MSG); @@ -1676,10 +1666,6 @@ public: r.insert("fm_extra", CPK_UINT, "(default: 0) max. increase on the number of inequalities for each FM variable elimination step."); } - virtual void set_cancel(bool f) { - if (m_imp) - m_imp->set_cancel(f); - } virtual void cleanup() { imp * d = alloc(imp, m_imp->m, m_params); diff --git a/src/tactic/arith/lia2card_tactic.cpp b/src/tactic/arith/lia2card_tactic.cpp index b46b7a9b6..7dda928d3 100644 --- a/src/tactic/arith/lia2card_tactic.cpp +++ b/src/tactic/arith/lia2card_tactic.cpp @@ -152,11 +152,7 @@ public: dealloc(m_todo); dealloc(m_01s); } - - void set_cancel(bool f) { - m_rw.set_cancel(f); - } - + void updt_params(params_ref const & p) { m_params = p; m_compile_equality = p.get_bool("compile_equality", false); diff --git a/src/tactic/arith/lia2pb_tactic.cpp b/src/tactic/arith/lia2pb_tactic.cpp index 8d200c80d..3a745fae3 100644 --- a/src/tactic/arith/lia2pb_tactic.cpp +++ b/src/tactic/arith/lia2pb_tactic.cpp @@ -60,9 +60,6 @@ class lia2pb_tactic : public tactic { updt_params_core(p); } - void set_cancel(bool f) { - m_rw.set_cancel(f); - } bool is_target_core(expr * n, rational & u) { if (!is_uninterp_const(n)) @@ -356,11 +353,6 @@ public: dealloc(d); } -protected: - virtual void set_cancel(bool f) { - if (m_imp) - m_imp->set_cancel(f); - } }; tactic * mk_lia2pb_tactic(ast_manager & m, params_ref const & p) { diff --git a/src/tactic/arith/normalize_bounds_tactic.cpp b/src/tactic/arith/normalize_bounds_tactic.cpp index 323903f6c..729d9986e 100644 --- a/src/tactic/arith/normalize_bounds_tactic.cpp +++ b/src/tactic/arith/normalize_bounds_tactic.cpp @@ -52,9 +52,6 @@ class normalize_bounds_tactic : public tactic { updt_params_core(p); } - void set_cancel(bool f) { - m_rw.set_cancel(f); - } bool is_target(expr * var, rational & val) { bool strict; @@ -198,12 +195,6 @@ public: } dealloc(d); } - -protected: - virtual void set_cancel(bool f) { - if (m_imp) - m_imp->set_cancel(f); - } }; tactic * mk_normalize_bounds_tactic(ast_manager & m, params_ref const & p) { diff --git a/src/tactic/arith/pb2bv_tactic.cpp b/src/tactic/arith/pb2bv_tactic.cpp index 1ef0efc47..ebb82fbc1 100644 --- a/src/tactic/arith/pb2bv_tactic.cpp +++ b/src/tactic/arith/pb2bv_tactic.cpp @@ -884,10 +884,6 @@ private: r.erase("elim_and"); } - void set_cancel(bool f) { - m_rw.set_cancel(f); - } - virtual void operator()(goal_ref const & g, goal_ref_buffer & result, model_converter_ref & mc, @@ -1015,11 +1011,7 @@ public: dealloc(d); } -protected: - virtual void set_cancel(bool f) { - if (m_imp) - m_imp->set_cancel(f); - } + }; tactic * mk_pb2bv_tactic(ast_manager & m, params_ref const & p) { diff --git a/src/tactic/arith/probe_arith.cpp b/src/tactic/arith/probe_arith.cpp index 9c02b5f0f..5d5590263 100644 --- a/src/tactic/arith/probe_arith.cpp +++ b/src/tactic/arith/probe_arith.cpp @@ -33,7 +33,7 @@ class arith_degree_probe : public probe { unsigned long long m_acc_degree; unsigned m_counter; - proc(ast_manager & _m):m(_m), m_pm(m_qm), m_expr2poly(m, m_pm), m_util(m) { + proc(ast_manager & _m):m(_m), m_pm(m.limit(), m_qm), m_expr2poly(m, m_pm), m_util(m) { m_max_degree = 0; m_acc_degree = 0; m_counter = 0; diff --git a/src/tactic/arith/propagate_ineqs_tactic.cpp b/src/tactic/arith/propagate_ineqs_tactic.cpp index 977f15167..cec110fd1 100644 --- a/src/tactic/arith/propagate_ineqs_tactic.cpp +++ b/src/tactic/arith/propagate_ineqs_tactic.cpp @@ -55,8 +55,6 @@ public: virtual void operator()(goal_ref const & g, goal_ref_buffer & result, model_converter_ref & mc, proof_converter_ref & pc, expr_dependency_ref & core); virtual void cleanup(); -protected: - virtual void set_cancel(bool f); }; tactic * mk_propagate_ineqs_tactic(ast_manager & m, params_ref const & p) { @@ -512,9 +510,6 @@ struct propagate_ineqs_tactic::imp { TRACE("propagate_ineqs_tactic", r->display(tout);); } - void set_cancel(bool f) { - // TODO - } }; propagate_ineqs_tactic::propagate_ineqs_tactic(ast_manager & m, params_ref const & p): @@ -546,10 +541,6 @@ void propagate_ineqs_tactic::operator()(goal_ref const & g, SASSERT(r->is_well_sorted()); } -void propagate_ineqs_tactic::set_cancel(bool f) { - if (m_imp) - m_imp->set_cancel(f); -} void propagate_ineqs_tactic::cleanup() { imp * d = alloc(imp, m_imp->m, m_params); diff --git a/src/tactic/arith/purify_arith_tactic.cpp b/src/tactic/arith/purify_arith_tactic.cpp index ac383c39a..47f7a5576 100644 --- a/src/tactic/arith/purify_arith_tactic.cpp +++ b/src/tactic/arith/purify_arith_tactic.cpp @@ -748,8 +748,6 @@ public: virtual void cleanup() { } - virtual void set_cancel(bool f) { - } }; tactic * mk_purify_arith_tactic(ast_manager & m, params_ref const & p) { diff --git a/src/tactic/arith/recover_01_tactic.cpp b/src/tactic/arith/recover_01_tactic.cpp index 3d222cf56..4e7f8f342 100644 --- a/src/tactic/arith/recover_01_tactic.cpp +++ b/src/tactic/arith/recover_01_tactic.cpp @@ -66,9 +66,6 @@ class recover_01_tactic : public tactic { updt_params_core(p); } - void set_cancel(bool f) { - m_rw.set_cancel(f); - } bool save_clause(expr * c) { if (!m.is_or(c)) @@ -432,12 +429,6 @@ public: } dealloc(d); } - -protected: - virtual void set_cancel(bool f) { - if (m_imp) - m_imp->set_cancel(f); - } }; tactic * mk_recover_01_tactic(ast_manager & m, params_ref const & p) { diff --git a/src/tactic/bv/bit_blaster_tactic.cpp b/src/tactic/bv/bit_blaster_tactic.cpp index 924843af0..391057877 100644 --- a/src/tactic/bv/bit_blaster_tactic.cpp +++ b/src/tactic/bv/bit_blaster_tactic.cpp @@ -49,9 +49,6 @@ class bit_blaster_tactic : public tactic { ast_manager & m() const { return m_rewriter->m(); } - void set_cancel(bool f) { - m_rewriter->set_cancel(f); - } void operator()(goal_ref const & g, goal_ref_buffer & result, @@ -163,11 +160,6 @@ public: return m_imp->get_num_steps(); } -protected: - virtual void set_cancel(bool f) { - if (m_imp) - m_imp->set_cancel(f); - } }; diff --git a/src/tactic/bv/bv1_blaster_tactic.cpp b/src/tactic/bv/bv1_blaster_tactic.cpp index f6a6017de..55709b01e 100644 --- a/src/tactic/bv/bv1_blaster_tactic.cpp +++ b/src/tactic/bv/bv1_blaster_tactic.cpp @@ -377,9 +377,6 @@ class bv1_blaster_tactic : public tactic { ast_manager & m() const { return m_rw.m(); } - void set_cancel(bool f) { - m_rw.set_cancel(f); - } void operator()(goal_ref const & g, goal_ref_buffer & result, @@ -478,11 +475,6 @@ public: return m_imp->get_num_steps(); } -protected: - virtual void set_cancel(bool f) { - if (m_imp) - m_imp->set_cancel(f); - } }; tactic * mk_bv1_blaster_tactic(ast_manager & m, params_ref const & p) { diff --git a/src/tactic/bv/bv_size_reduction_tactic.cpp b/src/tactic/bv/bv_size_reduction_tactic.cpp index 707a9284b..0bc41ad11 100644 --- a/src/tactic/bv/bv_size_reduction_tactic.cpp +++ b/src/tactic/bv/bv_size_reduction_tactic.cpp @@ -43,7 +43,6 @@ public: virtual void operator()(goal_ref const & g, goal_ref_buffer & result, model_converter_ref & mc, proof_converter_ref & pc, expr_dependency_ref & core); virtual void cleanup(); - virtual void set_cancel(bool f); }; tactic * mk_bv_size_reduction_tactic(ast_manager & m, params_ref const & p) { @@ -64,13 +63,11 @@ struct bv_size_reduction_tactic::imp { ref m_fmc; scoped_ptr m_replacer; bool m_produce_models; - volatile bool m_cancel; imp(ast_manager & _m): m(_m), m_util(m), - m_replacer(mk_default_expr_replacer(m)), - m_cancel(false) { + m_replacer(mk_default_expr_replacer(m)) { } void update_signed_lower(app * v, numeral const & k) { @@ -178,7 +175,7 @@ struct bv_size_reduction_tactic::imp { } void checkpoint() { - if (m_cancel) + if (m.canceled()) throw tactic_exception(TACTIC_CANCELED_MSG); } @@ -375,10 +372,6 @@ struct bv_size_reduction_tactic::imp { TRACE("after_bv_size_reduction", g.display(tout); if (m_mc) m_mc->display(tout);); } - void set_cancel(bool f) { - m_replacer->set_cancel(f); - m_cancel = f; - } }; bv_size_reduction_tactic::bv_size_reduction_tactic(ast_manager & m) { @@ -404,10 +397,6 @@ void bv_size_reduction_tactic::operator()(goal_ref const & g, SASSERT(g->is_well_sorted()); } -void bv_size_reduction_tactic::set_cancel(bool f) { - if (m_imp) - m_imp->set_cancel(f); -} void bv_size_reduction_tactic::cleanup() { imp * d = alloc(imp, m_imp->m); diff --git a/src/tactic/bv/bvarray2uf_tactic.cpp b/src/tactic/bv/bvarray2uf_tactic.cpp index 940cfa37d..d5c381ad7 100644 --- a/src/tactic/bv/bvarray2uf_tactic.cpp +++ b/src/tactic/bv/bvarray2uf_tactic.cpp @@ -34,7 +34,6 @@ class bvarray2uf_tactic : public tactic { bool m_produce_models; bool m_produce_proofs; bool m_produce_cores; - volatile bool m_cancel; bvarray2uf_rewriter m_rw; ast_manager & m() { return m_manager; } @@ -44,17 +43,13 @@ class bvarray2uf_tactic : public tactic { m_produce_models(false), m_produce_proofs(false), m_produce_cores(false), - m_cancel(false), m_rw(m, p) { updt_params(p); } - void set_cancel(bool f) { - m_cancel = f; - } void checkpoint() { - if (m_cancel) + if (m_manager.canceled()) throw tactic_exception(TACTIC_CANCELED_MSG); } @@ -155,11 +150,6 @@ public: dealloc(d); } - virtual void set_cancel(bool f) { - if (m_imp) - m_imp->set_cancel(f); - } - }; diff --git a/src/tactic/bv/elim_small_bv_tactic.cpp b/src/tactic/bv/elim_small_bv_tactic.cpp index a5f329101..f93102645 100644 --- a/src/tactic/bv/elim_small_bv_tactic.cpp +++ b/src/tactic/bv/elim_small_bv_tactic.cpp @@ -229,10 +229,6 @@ class elim_small_bv_tactic : public tactic { m_rw(m, p) { } - void set_cancel(bool f) { - m_rw.set_cancel(f); - } - void updt_params(params_ref const & p) { m_rw.cfg().updt_params(p); } @@ -318,10 +314,6 @@ public: dealloc(d); } - virtual void set_cancel(bool f) { - if (m_imp) - m_imp->set_cancel(f); - } }; tactic * mk_elim_small_bv_tactic(ast_manager & m, params_ref const & p) { diff --git a/src/tactic/bv/max_bv_sharing_tactic.cpp b/src/tactic/bv/max_bv_sharing_tactic.cpp index 56b18dd8d..5e25b719d 100644 --- a/src/tactic/bv/max_bv_sharing_tactic.cpp +++ b/src/tactic/bv/max_bv_sharing_tactic.cpp @@ -235,11 +235,7 @@ class max_bv_sharing_tactic : public tactic { } ast_manager & m() const { return m_rw.m(); } - - void set_cancel(bool f) { - m_rw.set_cancel(f); - } - + void operator()(goal_ref const & g, goal_ref_buffer & result, model_converter_ref & mc, @@ -318,11 +314,6 @@ public: } dealloc(d); } - - virtual void set_cancel(bool f) { - if (m_imp) - m_imp->set_cancel(f); - } }; tactic * mk_max_bv_sharing_tactic(ast_manager & m, params_ref const & p) { diff --git a/src/tactic/core/blast_term_ite_tactic.cpp b/src/tactic/core/blast_term_ite_tactic.cpp index fbc66c418..4251a10bd 100644 --- a/src/tactic/core/blast_term_ite_tactic.cpp +++ b/src/tactic/core/blast_term_ite_tactic.cpp @@ -109,9 +109,6 @@ class blast_term_ite_tactic : public tactic { m_rw(m, p) { } - void set_cancel(bool f) { - m_rw.set_cancel(f); - } void updt_params(params_ref const & p) { m_rw.cfg().updt_params(p); @@ -198,11 +195,6 @@ public: } } - virtual void set_cancel(bool f) { - if (m_imp) - m_imp->set_cancel(f); - } - static void blast_term_ite(expr_ref& fml) { ast_manager& m = fml.get_manager(); scoped_no_proof _sp(m); diff --git a/src/tactic/core/cofactor_elim_term_ite.cpp b/src/tactic/core/cofactor_elim_term_ite.cpp index aca6d9084..305b59ab4 100644 --- a/src/tactic/core/cofactor_elim_term_ite.cpp +++ b/src/tactic/core/cofactor_elim_term_ite.cpp @@ -30,13 +30,12 @@ struct cofactor_elim_term_ite::imp { params_ref m_params; unsigned long long m_max_memory; bool m_cofactor_equalities; - volatile bool m_cancel; void checkpoint() { cooperate("cofactor ite"); if (memory::get_allocation_size() > m_max_memory) throw tactic_exception(TACTIC_MAX_MEMORY_MSG); - if (m_cancel) + if (m.canceled()) throw tactic_exception(TACTIC_CANCELED_MSG); } @@ -315,9 +314,6 @@ struct cofactor_elim_term_ite::imp { r.insert("cofactor_equalities", CPK_BOOL, "(default: true) use equalities to rewrite bodies of ite-expressions. This is potentially expensive."); } - void set_cancel(bool f) { - m_cancel = f; - } struct cofactor_rw_cfg : public default_rewriter_cfg { ast_manager & m; @@ -659,7 +655,6 @@ struct cofactor_elim_term_ite::imp { m(_m), m_params(p), m_cofactor_equalities(true) { - m_cancel = false; updt_params(p); } @@ -698,10 +693,6 @@ void cofactor_elim_term_ite::operator()(expr * t, expr_ref & r) { m_imp->operator()(t, r); } -void cofactor_elim_term_ite::set_cancel(bool f) { - if (m_imp) - m_imp->set_cancel(f); -} void cofactor_elim_term_ite::cleanup() { ast_manager & m = m_imp->m; diff --git a/src/tactic/core/cofactor_elim_term_ite.h b/src/tactic/core/cofactor_elim_term_ite.h index 9579729d3..98142837c 100644 --- a/src/tactic/core/cofactor_elim_term_ite.h +++ b/src/tactic/core/cofactor_elim_term_ite.h @@ -35,10 +35,7 @@ public: void operator()(expr * t, expr_ref & r); - void cancel() { set_cancel(true); } - void reset_cancel() { set_cancel(false); } void cleanup(); - void set_cancel(bool f); }; diff --git a/src/tactic/core/cofactor_term_ite_tactic.cpp b/src/tactic/core/cofactor_term_ite_tactic.cpp index bc719a85e..24b381476 100644 --- a/src/tactic/core/cofactor_term_ite_tactic.cpp +++ b/src/tactic/core/cofactor_term_ite_tactic.cpp @@ -73,7 +73,6 @@ public: virtual void cleanup() { return m_elim_ite.cleanup(); } - virtual void set_cancel(bool f) { m_elim_ite.set_cancel(f); } }; tactic * mk_cofactor_term_ite_tactic(ast_manager & m, params_ref const & p) { diff --git a/src/tactic/core/ctx_simplify_tactic.cpp b/src/tactic/core/ctx_simplify_tactic.cpp index bb38d28ce..27354a7e0 100644 --- a/src/tactic/core/ctx_simplify_tactic.cpp +++ b/src/tactic/core/ctx_simplify_tactic.cpp @@ -57,21 +57,16 @@ struct ctx_simplify_tactic::imp { unsigned m_max_depth; unsigned m_max_steps; bool m_bail_on_blowup; - volatile bool m_cancel; imp(ast_manager & _m, params_ref const & p): m(_m), m_allocator("context-simplifier"), m_occs(true, true), m_mk_app(m, p) { - m_cancel = false; m_scope_lvl = 0; updt_params(p); } - void set_cancel(bool f) { - m_cancel = f; - } ~imp() { pop(m_scope_lvl); @@ -100,7 +95,7 @@ struct ctx_simplify_tactic::imp { cooperate("ctx_simplify_tactic"); if (memory::get_allocation_size() > m_max_memory) throw tactic_exception(TACTIC_MAX_MEMORY_MSG); - if (m_cancel) + if (m.canceled()) throw tactic_exception(TACTIC_CANCELED_MSG); } @@ -541,10 +536,6 @@ void ctx_simplify_tactic::operator()(goal_ref const & in, result.push_back(in.get()); } -void ctx_simplify_tactic::set_cancel(bool f) { - if (m_imp) - m_imp->set_cancel(f); -} void ctx_simplify_tactic::cleanup() { ast_manager & m = m_imp->m; diff --git a/src/tactic/core/ctx_simplify_tactic.h b/src/tactic/core/ctx_simplify_tactic.h index 3cf2544aa..dfc512d66 100644 --- a/src/tactic/core/ctx_simplify_tactic.h +++ b/src/tactic/core/ctx_simplify_tactic.h @@ -45,8 +45,6 @@ public: expr_dependency_ref & core); virtual void cleanup(); -protected: - virtual void set_cancel(bool f); }; inline tactic * mk_ctx_simplify_tactic(ast_manager & m, params_ref const & p = params_ref()) { diff --git a/src/tactic/core/der_tactic.cpp b/src/tactic/core/der_tactic.cpp index 2277c3fa8..b136adef7 100644 --- a/src/tactic/core/der_tactic.cpp +++ b/src/tactic/core/der_tactic.cpp @@ -28,11 +28,7 @@ class der_tactic : public tactic { } ast_manager & m() const { return m_manager; } - - void set_cancel(bool f) { - m_r.set_cancel(f); - } - + void reset() { m_r.reset(); } @@ -98,10 +94,6 @@ public: dealloc(d); } - virtual void set_cancel(bool f) { - if (m_imp) - m_imp->set_cancel(f); - } }; tactic * mk_der_tactic(ast_manager & m) { diff --git a/src/tactic/core/distribute_forall_tactic.cpp b/src/tactic/core/distribute_forall_tactic.cpp index 53a1ce4ae..074dfdb54 100644 --- a/src/tactic/core/distribute_forall_tactic.cpp +++ b/src/tactic/core/distribute_forall_tactic.cpp @@ -140,11 +140,6 @@ public: } } - virtual void set_cancel(bool f) { - if (m_rw) - m_rw->set_cancel(f); - } - virtual void cleanup() {} }; diff --git a/src/tactic/core/elim_term_ite_tactic.cpp b/src/tactic/core/elim_term_ite_tactic.cpp index e49884004..1e7f91c1c 100644 --- a/src/tactic/core/elim_term_ite_tactic.cpp +++ b/src/tactic/core/elim_term_ite_tactic.cpp @@ -94,9 +94,6 @@ class elim_term_ite_tactic : public tactic { m_rw(m, p) { } - void set_cancel(bool f) { - m_rw.set_cancel(f); - } void updt_params(params_ref const & p) { m_rw.cfg().updt_params(p); @@ -182,10 +179,6 @@ public: dealloc(d); } - virtual void set_cancel(bool f) { - if (m_imp) - m_imp->set_cancel(f); - } }; tactic * mk_elim_term_ite_tactic(ast_manager & m, params_ref const & p) { diff --git a/src/tactic/core/elim_uncnstr_tactic.cpp b/src/tactic/core/elim_uncnstr_tactic.cpp index 6d7bcb2f2..6ccbe2a56 100644 --- a/src/tactic/core/elim_uncnstr_tactic.cpp +++ b/src/tactic/core/elim_uncnstr_tactic.cpp @@ -993,10 +993,6 @@ class elim_uncnstr_tactic : public tactic { } } - void set_cancel(bool f) { - if (m_rw) - m_rw->set_cancel(f); - } }; imp * m_imp; @@ -1058,11 +1054,6 @@ public: m_imp->m_num_elim_apps = 0; } -protected: - virtual void set_cancel(bool f) { - if (m_imp) - m_imp->set_cancel(f); - } }; tactic * mk_elim_uncnstr_tactic(ast_manager & m, params_ref const & p) { diff --git a/src/tactic/core/occf_tactic.cpp b/src/tactic/core/occf_tactic.cpp index 9b974ae19..0914bfdef 100644 --- a/src/tactic/core/occf_tactic.cpp +++ b/src/tactic/core/occf_tactic.cpp @@ -29,20 +29,14 @@ Revision History: class occf_tactic : public tactic { struct imp { ast_manager & m; - volatile bool m_cancel; filter_model_converter * m_mc; imp(ast_manager & _m): m(_m) { - m_cancel = false; - } - - void set_cancel(bool f) { - m_cancel = f; } void checkpoint() { - if (m_cancel) + if (m.canceled()) throw tactic_exception(TACTIC_CANCELED_MSG); cooperate("occf"); } @@ -233,11 +227,6 @@ public: dealloc(d); } -protected: - virtual void set_cancel(bool f) { - if (m_imp) - m_imp->set_cancel(f); - } }; tactic * mk_occf_tactic(ast_manager & m, params_ref const & p) { diff --git a/src/tactic/core/pb_preprocess_tactic.cpp b/src/tactic/core/pb_preprocess_tactic.cpp index 51e92ef11..b4f335db5 100644 --- a/src/tactic/core/pb_preprocess_tactic.cpp +++ b/src/tactic/core/pb_preprocess_tactic.cpp @@ -264,9 +264,6 @@ public: return m_progress; } - virtual void set_cancel(bool f) { - } - virtual void updt_params(params_ref const & p) { } diff --git a/src/tactic/core/propagate_values_tactic.cpp b/src/tactic/core/propagate_values_tactic.cpp index 39df3b174..30f63942a 100644 --- a/src/tactic/core/propagate_values_tactic.cpp +++ b/src/tactic/core/propagate_values_tactic.cpp @@ -54,9 +54,6 @@ class propagate_values_tactic : public tactic { ast_manager & m() const { return m_manager; } - void set_cancel(bool f) { - m_r.set_cancel(f); - } bool is_shared(expr * t) { return m_occs.is_shared(t); @@ -267,11 +264,6 @@ public: dealloc(d); } -protected: - virtual void set_cancel(bool f) { - if (m_imp) - m_imp->set_cancel(f); - } }; tactic * mk_propagate_values_tactic(ast_manager & m, params_ref const & p) { diff --git a/src/tactic/core/reduce_args_tactic.cpp b/src/tactic/core/reduce_args_tactic.cpp index 99375e6e8..3990b9a1f 100644 --- a/src/tactic/core/reduce_args_tactic.cpp +++ b/src/tactic/core/reduce_args_tactic.cpp @@ -75,7 +75,6 @@ public: virtual void operator()(goal_ref const & g, goal_ref_buffer & result, model_converter_ref & mc, proof_converter_ref & pc, expr_dependency_ref & core); virtual void cleanup(); - virtual void set_cancel(bool f); }; tactic * mk_reduce_args_tactic(ast_manager & m, params_ref const & p) { @@ -85,21 +84,16 @@ tactic * mk_reduce_args_tactic(ast_manager & m, params_ref const & p) { struct reduce_args_tactic::imp { ast_manager & m_manager; bool m_produce_models; - volatile bool m_cancel; ast_manager & m() const { return m_manager; } imp(ast_manager & m): m_manager(m) { - m_cancel = false; } - void set_cancel(bool f) { - m_cancel = f; - } void checkpoint() { - if (m_cancel) + if (m_manager.canceled()) throw tactic_exception(TACTIC_CANCELED_MSG); cooperate("reduce-args"); } @@ -535,11 +529,6 @@ void reduce_args_tactic::operator()(goal_ref const & g, SASSERT(g->is_well_sorted()); } -void reduce_args_tactic::set_cancel(bool f) { - if (m_imp) - m_imp->set_cancel(f); -} - void reduce_args_tactic::cleanup() { ast_manager & m = m_imp->m(); imp * d = alloc(imp, m); diff --git a/src/tactic/core/simplify_tactic.cpp b/src/tactic/core/simplify_tactic.cpp index fea5ac86e..8f4b9fb9e 100644 --- a/src/tactic/core/simplify_tactic.cpp +++ b/src/tactic/core/simplify_tactic.cpp @@ -36,9 +36,6 @@ struct simplify_tactic::imp { ast_manager & m() const { return m_manager; } - void set_cancel(bool f) { - m_r.set_cancel(f); - } void reset() { m_r.reset(); @@ -111,10 +108,6 @@ void simplify_tactic::operator()(goal_ref const & in, } } -void simplify_tactic::set_cancel(bool f) { - if (m_imp) - m_imp->set_cancel(f); -} void simplify_tactic::cleanup() { ast_manager & m = m_imp->m(); diff --git a/src/tactic/core/simplify_tactic.h b/src/tactic/core/simplify_tactic.h index d9a8be752..ec72404dd 100644 --- a/src/tactic/core/simplify_tactic.h +++ b/src/tactic/core/simplify_tactic.h @@ -45,8 +45,6 @@ public: unsigned get_num_steps() const; virtual tactic * translate(ast_manager & m) { return alloc(simplify_tactic, m, m_params); } -protected: - virtual void set_cancel(bool f); }; diff --git a/src/tactic/core/solve_eqs_tactic.cpp b/src/tactic/core/solve_eqs_tactic.cpp index 3b0a57d20..bf1364314 100644 --- a/src/tactic/core/solve_eqs_tactic.cpp +++ b/src/tactic/core/solve_eqs_tactic.cpp @@ -48,7 +48,6 @@ class solve_eqs_tactic : public tactic { bool m_produce_proofs; bool m_produce_unsat_cores; bool m_produce_models; - volatile bool m_cancel; imp(ast_manager & m, params_ref const & p, expr_replacer * r, bool owner): m_manager(m), @@ -56,8 +55,8 @@ class solve_eqs_tactic : public tactic { m_r_owner(r == 0 || owner), m_a_util(m), m_num_steps(0), - m_num_eliminated_vars(0), - m_cancel(false) { + m_num_eliminated_vars(0) + { updt_params(p); if (m_r == 0) m_r = mk_default_expr_replacer(m); @@ -75,14 +74,9 @@ class solve_eqs_tactic : public tactic { m_theory_solver = p.get_bool("theory_solver", true); m_max_occs = p.get_uint("solve_eqs_max_occs", UINT_MAX); } - - void set_cancel(bool f) { - m_cancel = f; - m_r->set_cancel(f); - } - + void checkpoint() { - if (m_cancel) + if (m().canceled()) throw tactic_exception(TACTIC_CANCELED_MSG); cooperate("solve-eqs"); } @@ -772,10 +766,6 @@ public: m_imp->m_num_eliminated_vars = 0; } - virtual void set_cancel(bool f) { - if (m_imp) - m_imp->set_cancel(f); - } }; tactic * mk_solve_eqs_tactic(ast_manager & m, params_ref const & p, expr_replacer * r) { diff --git a/src/tactic/core/tseitin_cnf_tactic.cpp b/src/tactic/core/tseitin_cnf_tactic.cpp index c5be7ab1f..ffdb36ac3 100644 --- a/src/tactic/core/tseitin_cnf_tactic.cpp +++ b/src/tactic/core/tseitin_cnf_tactic.cpp @@ -105,7 +105,6 @@ class tseitin_cnf_tactic : public tactic { unsigned long long m_max_memory; unsigned m_num_aux_vars; - volatile bool m_cancel; imp(ast_manager & _m, params_ref const & p): m(_m), @@ -115,8 +114,7 @@ class tseitin_cnf_tactic : public tactic { m_clauses(_m), m_deps(_m), m_rw(_m), - m_num_aux_vars(0), - m_cancel(false) { + m_num_aux_vars(0) { updt_params(p); m_rw.set_flat(false); } @@ -756,13 +754,10 @@ class tseitin_cnf_tactic : public tactic { if (r == CONT) goto loop; \ if (r == DONE) { m_frame_stack.pop_back(); continue; } - void set_cancel(bool f) { - m_cancel = f; - } void checkpoint() { cooperate("tseitin cnf"); - if (m_cancel) + if (m.canceled()) throw tactic_exception(TACTIC_CANCELED_MSG); if (memory::get_allocation_size() > m_max_memory) throw tactic_exception(TACTIC_MAX_MEMORY_MSG); @@ -908,11 +903,6 @@ public: dealloc(d); } - virtual void set_cancel(bool f) { - if (m_imp) - m_imp->set_cancel(f); - } - virtual void collect_statistics(statistics & st) const { st.update("cnf encoding aux vars", m_imp->m_num_aux_vars); } diff --git a/src/tactic/extension_model_converter.cpp b/src/tactic/extension_model_converter.cpp index e006068da..0f40578a2 100644 --- a/src/tactic/extension_model_converter.cpp +++ b/src/tactic/extension_model_converter.cpp @@ -91,14 +91,6 @@ void extension_model_converter::operator()(model_ref & md, unsigned goal_idx) { TRACE("extension_mc", model_v2_pp(tout, *md); display_decls_info(tout, md);); } -void extension_model_converter::cancel() { - #pragma omp critical (extension_model_converter) - { - if (m_eval) - m_eval->cancel(); - } -} - void extension_model_converter::display(std::ostream & out) { ast_manager & m = m_vars.get_manager(); out << "(extension-model-converter"; diff --git a/src/tactic/extension_model_converter.h b/src/tactic/extension_model_converter.h index da1f8ea56..ba113c7ab 100644 --- a/src/tactic/extension_model_converter.h +++ b/src/tactic/extension_model_converter.h @@ -40,8 +40,6 @@ public: virtual void operator()(model_ref & md, unsigned goal_idx); - virtual void cancel(); - virtual void display(std::ostream & out); // register a variable that was eliminated diff --git a/src/tactic/fpa/fpa2bv_tactic.cpp b/src/tactic/fpa/fpa2bv_tactic.cpp index eb2aeaa0c..e067a6ade 100644 --- a/src/tactic/fpa/fpa2bv_tactic.cpp +++ b/src/tactic/fpa/fpa2bv_tactic.cpp @@ -46,10 +46,6 @@ class fpa2bv_tactic : public tactic { m_rw.cfg().updt_params(p); } - void set_cancel(bool f) { - m_rw.set_cancel(f); - } - virtual void operator()(goal_ref const & g, goal_ref_buffer & result, model_converter_ref & mc, @@ -166,11 +162,6 @@ public: dealloc(d); } -protected: - virtual void set_cancel(bool f) { - if (m_imp) - m_imp->set_cancel(f); - } }; tactic * mk_fpa2bv_tactic(ast_manager & m, params_ref const & p) { diff --git a/src/tactic/nlsat_smt/nl_purify_tactic.cpp b/src/tactic/nlsat_smt/nl_purify_tactic.cpp index 34458dd57..575aa4422 100644 --- a/src/tactic/nlsat_smt/nl_purify_tactic.cpp +++ b/src/tactic/nlsat_smt/nl_purify_tactic.cpp @@ -73,7 +73,6 @@ class nl_purify_tactic : public tactic { params_ref m_params; bool m_produce_proofs; ref m_fmc; - bool m_cancel; tactic_ref m_nl_tac; // nlsat tactic goal_ref m_nl_g; // nlsat goal ref m_solver; // SMT solver @@ -289,7 +288,7 @@ private: arith_util & u() { return m_util; } void check_point() { - if (m_cancel) { + if (m.canceled()) { throw tactic_exception("canceled"); } } @@ -701,7 +700,6 @@ public: m_util(m), m_params(p), m_fmc(0), - m_cancel(false), m_nl_tac(mk_nlsat_tactic(m, p)), m_nl_g(0), m_solver(mk_smt_solver(m, p, symbol::null)), @@ -721,17 +719,6 @@ public: return alloc(nl_purify_tactic, m, m_params); } - virtual void set_cancel(bool f) { - m_nl_tac->set_cancel(f); - if (f) { - m_solver->cancel(); - } - else { - m_solver->reset_cancel(); - } - m_cancel = f; - } - virtual void collect_statistics(statistics & st) const { m_nl_tac->collect_statistics(st); m_solver->collect_statistics(st); diff --git a/src/tactic/sls/sls_engine.cpp b/src/tactic/sls/sls_engine.cpp index a1c122dc2..d0798e375 100644 --- a/src/tactic/sls/sls_engine.cpp +++ b/src/tactic/sls/sls_engine.cpp @@ -37,7 +37,6 @@ sls_engine::sls_engine(ast_manager & m, params_ref const & p) : m_zero(m_mpz_manager.mk_z(0)), m_one(m_mpz_manager.mk_z(1)), m_two(m_mpz_manager.mk_z(2)), - m_cancel(false), m_bv_util(m), m_tracker(m, m_bv_util, m_mpz_manager, m_powers), m_evaluator(m, m_bv_util, m_tracker, m_mpz_manager, m_powers) @@ -95,7 +94,7 @@ void sls_engine::collect_statistics(statistics& st) const { } void sls_engine::checkpoint() { - if (m_cancel) + if (m_manager.canceled()) throw tactic_exception(TACTIC_CANCELED_MSG); cooperate("sls"); } diff --git a/src/tactic/sls/sls_engine.h b/src/tactic/sls/sls_engine.h index a771eaefc..ccd4f5b5a 100644 --- a/src/tactic/sls/sls_engine.h +++ b/src/tactic/sls/sls_engine.h @@ -64,7 +64,6 @@ protected: powers m_powers; mpz m_zero, m_one, m_two; bool m_produce_models; - volatile bool m_cancel; bv_util m_bv_util; sls_tracker m_tracker; sls_evaluator m_evaluator; @@ -93,9 +92,6 @@ public: ast_manager & m() const { return m_manager; } - void set_cancel(bool f) { m_cancel = f; } - void cancel() { set_cancel(true); } - void reset_cancel() { set_cancel(false); } void updt_params(params_ref const & _p); diff --git a/src/tactic/sls/sls_tactic.cpp b/src/tactic/sls/sls_tactic.cpp index 4df74f20a..38101c2fe 100644 --- a/src/tactic/sls/sls_tactic.cpp +++ b/src/tactic/sls/sls_tactic.cpp @@ -95,10 +95,6 @@ public: m_engine->reset_statistics(); } - virtual void set_cancel(bool f) { - if (m_engine) - m_engine->set_cancel(f); - } }; tactic * mk_sls_tactic(ast_manager & m, params_ref const & p) { diff --git a/src/tactic/tactic.cpp b/src/tactic/tactic.cpp index 0cfc9e3b2..92e916d80 100644 --- a/src/tactic/tactic.cpp +++ b/src/tactic/tactic.cpp @@ -22,19 +22,7 @@ Notes: #include"stopwatch.h" #include"model_v2_pp.h" -void tactic::cancel() { - #pragma omp critical (tactic_cancel) - { - set_cancel(true); - } -} -void tactic::reset_cancel() { - #pragma omp critical (tactic_cancel) - { - set_cancel(false); - } -} struct tactic_report::imp { char const * m_id; diff --git a/src/tactic/tactic.h b/src/tactic/tactic.h index 9ccb98042..a9e50ff10 100644 --- a/src/tactic/tactic.h +++ b/src/tactic/tactic.h @@ -44,9 +44,6 @@ public: virtual void updt_params(params_ref const & p) {} virtual void collect_param_descrs(param_descrs & r) {} - - void cancel(); - void reset_cancel(); /** \brief Apply tactic to goal \c in. @@ -101,8 +98,6 @@ protected: friend class unary_tactical; friend class nl_purify_tactic; - virtual void set_cancel(bool f) {} - }; typedef ref tactic_ref; diff --git a/src/tactic/tactical.cpp b/src/tactic/tactical.cpp index d92ef4c36..69a1d650e 100644 --- a/src/tactic/tactical.cpp +++ b/src/tactic/tactical.cpp @@ -27,18 +27,12 @@ class binary_tactical : public tactic { protected: tactic * m_t1; tactic * m_t2; - volatile bool m_cancel; - void checkpoint() { - if (m_cancel) - throw tactic_exception(TACTIC_CANCELED_MSG); - } public: binary_tactical(tactic * t1, tactic * t2): m_t1(t1), - m_t2(t2), - m_cancel(false) { + m_t2(t2) { SASSERT(m_t1); SASSERT(m_t2); m_t1->inc_ref(); @@ -99,11 +93,6 @@ public: protected: - virtual void set_cancel(bool f) { - m_cancel = f; - m_t1->set_cancel(f); - m_t2->set_cancel(f); - } template tactic * translate_core(ast_manager & m) { @@ -147,7 +136,6 @@ public: SASSERT(!is_decided(r1) || (!pc1 && !core1)); // the pc and core of decided goals is 0 unsigned r1_size = r1.size(); SASSERT(r1_size > 0); - checkpoint(); if (r1_size == 1) { if (r1[0]->is_decided()) { result.push_back(r1[0]); @@ -168,7 +156,6 @@ public: sbuffer sz_buffer; goal_ref_buffer r2; for (unsigned i = 0; i < r1_size; i++) { - checkpoint(); goal_ref g = r1[i]; r2.reset(); model_converter_ref mc2; @@ -293,15 +280,9 @@ tactic * and_then(unsigned num, tactic * const * ts) { class nary_tactical : public tactic { protected: ptr_vector m_ts; - volatile bool m_cancel; - void checkpoint() { - if (m_cancel) - throw tactic_exception(TACTIC_CANCELED_MSG); - } public: - nary_tactical(unsigned num, tactic * const * ts): - m_cancel(false) { + nary_tactical(unsigned num, tactic * const * ts) { for (unsigned i = 0; i < num; i++) { SASSERT(ts[i]); m_ts.push_back(ts[i]); @@ -383,15 +364,6 @@ public: protected: - virtual void set_cancel(bool f) { - m_cancel = f; - ptr_vector::iterator it = m_ts.begin(); - ptr_vector::iterator end = m_ts.end(); - for (; it != end; ++it) - if (*it) - (*it)->set_cancel(f); - } - template tactic * translate_core(ast_manager & m) { ptr_buffer new_ts; @@ -422,7 +394,6 @@ public: unsigned sz = m_ts.size(); unsigned i; for (i = 0; i < sz; i++) { - checkpoint(); tactic * t = m_ts[i]; result.reset(); mc = 0; @@ -568,7 +539,6 @@ public: if (first) { for (unsigned j = 0; j < sz; j++) { if (static_cast(i) != j) { - ts.get(j)->cancel(); managers[j]->limit().cancel(); } } @@ -673,7 +643,6 @@ public: SASSERT(!is_decided(r1) || (!pc1 && !core1)); // the pc and core of decided goals is 0 unsigned r1_size = r1.size(); SASSERT(r1_size > 0); - checkpoint(); if (r1_size == 1) { // Only one subgoal created... no need for parallelism if (r1[0]->is_decided()) { @@ -771,7 +740,6 @@ public: if (curr_failed) { for (unsigned j = 0; j < r1_size; j++) { if (static_cast(i) != j) { - ts2.get(j)->cancel(); managers[j]->limit().cancel(); } } @@ -793,7 +761,6 @@ public: if (first) { for (unsigned j = 0; j < r1_size; j++) { if (static_cast(i) != j) { - ts2.get(j)->cancel(); managers[j]->limit().cancel(); } } @@ -929,18 +896,11 @@ tactic * par_and_then(unsigned num, tactic * const * ts) { class unary_tactical : public tactic { protected: tactic * m_t; - volatile bool m_cancel; - void checkpoint() { - if (m_cancel) - throw tactic_exception(TACTIC_CANCELED_MSG); - - } public: unary_tactical(tactic * t): - m_t(t), - m_cancel(false) { + m_t(t) { SASSERT(t); t->inc_ref(); } @@ -971,11 +931,6 @@ public: virtual void set_logic(symbol const& l) { m_t->set_logic(l); } virtual void set_progress_callback(progress_callback * callback) { m_t->set_progress_callback(callback); } protected: - virtual void set_cancel(bool f) { - m_cancel = f; - if (m_t) - m_t->set_cancel(f); - } template tactic * translate_core(ast_manager & m) { @@ -1029,7 +984,6 @@ class repeat_tactical : public unary_tactical { } unsigned r1_size = r1.size(); SASSERT(r1_size > 0); - checkpoint(); if (r1_size == 1) { if (r1[0]->is_decided()) { result.push_back(r1[0]); @@ -1050,7 +1004,6 @@ class repeat_tactical : public unary_tactical { sbuffer sz_buffer; goal_ref_buffer r2; for (unsigned i = 0; i < r1_size; i++) { - checkpoint(); goal_ref g = r1[i]; r2.reset(); model_converter_ref mc2; @@ -1199,7 +1152,7 @@ public: model_converter_ref & mc, proof_converter_ref & pc, expr_dependency_ref & core) { - cancel_eh eh(*m_t); + cancel_eh eh(in->m().limit()); { // Warning: scoped_timer is not thread safe in Linux. scoped_timer timer(m_timeout, &eh); diff --git a/src/tactic/ufbv/macro_finder_tactic.cpp b/src/tactic/ufbv/macro_finder_tactic.cpp index 2f0262fc8..c14521bf4 100644 --- a/src/tactic/ufbv/macro_finder_tactic.cpp +++ b/src/tactic/ufbv/macro_finder_tactic.cpp @@ -30,21 +30,16 @@ class macro_finder_tactic : public tactic { struct imp { ast_manager & m_manager; - bool m_cancel; bool m_elim_and; imp(ast_manager & m, params_ref const & p) : m_manager(m), - m_cancel(false), m_elim_and(false) { updt_params(p); } ast_manager & m() const { return m_manager; } - void set_cancel(bool f) { - m_cancel = f; - } void operator()(goal_ref const & g, goal_ref_buffer & result, @@ -152,10 +147,7 @@ public: dealloc(d); } - virtual void set_cancel(bool f) { - if (m_imp) - m_imp->set_cancel(f); - } + }; tactic * mk_macro_finder_tactic(ast_manager & m, params_ref const & p) { diff --git a/src/tactic/ufbv/quasi_macros_tactic.cpp b/src/tactic/ufbv/quasi_macros_tactic.cpp index cea8f2cfc..1647a97e2 100644 --- a/src/tactic/ufbv/quasi_macros_tactic.cpp +++ b/src/tactic/ufbv/quasi_macros_tactic.cpp @@ -31,17 +31,13 @@ class quasi_macros_tactic : public tactic { struct imp { ast_manager & m_manager; - bool m_cancel; - imp(ast_manager & m, params_ref const & p) : m_manager(m),m_cancel(false) { + imp(ast_manager & m, params_ref const & p) : m_manager(m) { updt_params(p); } ast_manager & m() const { return m_manager; } - void set_cancel(bool f) { - m_cancel = f; - } void operator()(goal_ref const & g, goal_ref_buffer & result, @@ -80,7 +76,7 @@ class quasi_macros_tactic : public tactic { } while (more) { // CMW: use repeat(...) ? - if (m_cancel) + if (m().canceled()) throw tactic_exception(TACTIC_CANCELED_MSG); new_forms.reset(); @@ -159,10 +155,6 @@ public: dealloc(d); } - virtual void set_cancel(bool f) { - if (m_imp) - m_imp->set_cancel(f); - } }; tactic * mk_quasi_macros_tactic(ast_manager & m, params_ref const & p) { diff --git a/src/tactic/ufbv/ufbv_rewriter_tactic.cpp b/src/tactic/ufbv/ufbv_rewriter_tactic.cpp index efecb38ba..ffe704354 100644 --- a/src/tactic/ufbv/ufbv_rewriter_tactic.cpp +++ b/src/tactic/ufbv/ufbv_rewriter_tactic.cpp @@ -26,18 +26,13 @@ class ufbv_rewriter_tactic : public tactic { struct imp { ast_manager & m_manager; - bool m_cancel; - imp(ast_manager & m, params_ref const & p) : m_manager(m),m_cancel(false) { + imp(ast_manager & m, params_ref const & p) : m_manager(m) { updt_params(p); } ast_manager & m() const { return m_manager; } - - void set_cancel(bool f) { - m_cancel = f; - } - + void operator()(goal_ref const & g, goal_ref_buffer & result, model_converter_ref & mc, @@ -127,10 +122,6 @@ public: dealloc(d); } - virtual void set_cancel(bool f) { - if (m_imp) - m_imp->set_cancel(f); - } }; tactic * mk_ufbv_rewriter_tactic(ast_manager & m, params_ref const & p) {