diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 0be27bc08..18a00d7ff 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -4157,7 +4157,6 @@ namespace smt { void context::set_cancel_flag(bool f) { m_cancel_flag = f; m_asserted_formulas.set_cancel_flag(f); - m_qmanager->set_cancel(f); } }; diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp index c88be746f..09b8fe4b6 100644 --- a/src/smt/smt_model_checker.cpp +++ b/src/smt/smt_model_checker.cpp @@ -40,7 +40,6 @@ namespace smt { m_max_cexs(1), m_iteration_idx(0), m_curr_model(0), - m_cancel(false), m_new_instances_bindings(m) { } diff --git a/src/smt/smt_model_checker.h b/src/smt/smt_model_checker.h index f7fcd8198..2b8f1aa4d 100644 --- a/src/smt/smt_model_checker.h +++ b/src/smt/smt_model_checker.h @@ -51,7 +51,6 @@ namespace smt { unsigned m_iteration_idx; proto_model * m_curr_model; obj_map m_value2expr; - bool m_cancel; friend class instantiation_set; void init_aux_context(); @@ -98,8 +97,6 @@ namespace smt { void reset(); - void set_cancel(bool f) { m_cancel = f; } - void operator()(expr* e); }; diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp index 08cf34e72..1f51e8bf2 100644 --- a/src/smt/smt_model_finder.cpp +++ b/src/smt/smt_model_finder.cpp @@ -1734,6 +1734,7 @@ namespace smt { (when it is marked as relevant in the end of the search). */ class quantifier_info { + model_finder& m_mf; quantifier_ref m_flat_q; // flat version of the quantifier bool m_is_auf; bool m_has_x_eq_y; @@ -1744,14 +1745,11 @@ namespace smt { // when the quantifier is satisfied by a macro/hint, it may not be processed by the AUF solver. // in this case, the quantifier_info stores the instantiation sets. ptr_vector * m_uvar_inst_sets; - volatile bool m_cancel; friend class quantifier_analyzer; void checkpoint() { - cooperate("quantifier_info"); - if (m_cancel) - throw tactic_exception(TACTIC_CANCELED_MSG); + m_mf.checkpoint("quantifer_info"); } void insert_qinfo(qinfo * qi) { @@ -1776,13 +1774,13 @@ namespace smt { public: typedef ptr_vector::const_iterator macro_iterator; - quantifier_info(ast_manager & m, quantifier * q): + quantifier_info(model_finder& mf, ast_manager & m, quantifier * q): + m_mf(mf), m_flat_q(m), m_is_auf(true), m_has_x_eq_y(false), m_the_one(0), - m_uvar_inst_sets(0), - m_cancel(false) { + m_uvar_inst_sets(0) { if (has_quantifiers(q->get_expr())) { static bool displayed_flat_msg = false; if (!displayed_flat_msg) { @@ -1936,8 +1934,6 @@ namespace smt { m_uvar_inst_sets = 0; } } - - void set_cancel(bool f) { m_cancel = f; } }; /** @@ -1945,12 +1941,12 @@ namespace smt { fill the structure quantifier_info. */ class quantifier_analyzer { + model_finder& m_mf; ast_manager & m_manager; macro_util m_mutil; array_util m_array_util; arith_util m_arith_util; bv_util m_bv_util; - bool m_cancel; quantifier_info * m_info; @@ -2363,9 +2359,7 @@ namespace smt { } void checkpoint() { - cooperate("quantifier_analyzer"); - if (m_cancel) - throw tactic_exception(TACTIC_CANCELED_MSG); + m_mf.checkpoint("quantifier_analyzer"); } void process_formulas_on_stack() { @@ -2455,13 +2449,13 @@ namespace smt { public: - quantifier_analyzer(ast_manager & m, simplifier & s): + quantifier_analyzer(model_finder& mf, ast_manager & m, simplifier & s): + m_mf(mf), m_manager(m), m_mutil(m, s), m_array_util(m), m_arith_util(m), m_bv_util(m), - m_cancel(false), m_info(0) { } @@ -2492,11 +2486,6 @@ namespace smt { m_info = 0; } - void set_cancel(bool f) { - m_cancel = f; - if (m_info) m_info->set_cancel(f); - } - }; /** @@ -3309,13 +3298,12 @@ namespace smt { model_finder::model_finder(ast_manager & m, simplifier & s): m_manager(m), m_context(0), - m_analyzer(alloc(quantifier_analyzer, m, s)), + m_analyzer(alloc(quantifier_analyzer, *this, m, s)), m_auf_solver(alloc(auf_solver, m, s)), m_dependencies(m), m_sm_solver(alloc(simple_macro_solver, m, m_q2info)), m_hint_solver(alloc(hint_solver, m, m_q2info)), m_nm_solver(alloc(non_auf_macro_solver, m, m_q2info, m_dependencies)), - m_cancel(false), m_new_constraints(m) { } @@ -3323,6 +3311,16 @@ namespace smt { reset(); } + void model_finder::checkpoint() { + checkpoint("model_finder"); + } + + void model_finder::checkpoint(char const* msg) { + cooperate(msg); + if (m_context && m_context->get_cancel_flag()) + throw tactic_exception(TACTIC_CANCELED_MSG); + } + mf::quantifier_info * model_finder::get_quantifier_info(quantifier * q) const { quantifier_info * info = 0; m_q2info.find(q, info); @@ -3339,7 +3337,7 @@ namespace smt { void model_finder::register_quantifier(quantifier * q) { TRACE("model_finder", tout << "registering:\n" << mk_pp(q, m_manager) << "\n";); - quantifier_info * new_info = alloc(quantifier_info, m_manager, q); + quantifier_info * new_info = alloc(quantifier_info, *this, m_manager, q); m_q2info.insert(q, new_info); m_quantifiers.push_back(q); m_analyzer->operator()(new_info); @@ -3591,14 +3589,4 @@ namespace smt { m_new_constraints.reset(); } } - - void model_finder::set_cancel(bool f) { - m_cancel = f; - m_analyzer->set_cancel(f); - obj_map::iterator it = m_q2info.begin(); - obj_map::iterator end = m_q2info.end(); - for (; it != end; ++it) - (*it).m_value->set_cancel(f); - } - }; diff --git a/src/smt/smt_model_finder.h b/src/smt/smt_model_finder.h index 9fd0e2645..0694b008b 100644 --- a/src/smt/smt_model_finder.h +++ b/src/smt/smt_model_finder.h @@ -85,7 +85,6 @@ namespace smt { scoped_ptr m_sm_solver; scoped_ptr m_hint_solver; scoped_ptr m_nm_solver; - bool m_cancel; struct scope { unsigned m_quantifiers_lim; @@ -104,12 +103,8 @@ namespace smt { void process_non_auf_macros(ptr_vector & qs, ptr_vector & residue, proto_model * m); void process_auf(ptr_vector const & qs, proto_model * m); instantiation_set const * get_uvar_inst_set(quantifier * q, unsigned i) const; + void checkpoint(); - void checkpoint() { - cooperate("model_finder"); - if (m_cancel) - throw tactic_exception(TACTIC_CANCELED_MSG); - } public: model_finder(ast_manager & m, simplifier & s); @@ -129,7 +124,7 @@ namespace smt { void restart_eh(); - void set_cancel(bool f); + void checkpoint(char const* component); }; }; diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp index f3e4959f8..69bf0b72f 100644 --- a/src/smt/smt_quantifier.cpp +++ b/src/smt/smt_quantifier.cpp @@ -236,10 +236,6 @@ namespace smt { return m_plugin->check_model(m, root2value); } - void set_cancel(bool f) { - m_plugin->set_cancel(f); - } - }; quantifier_manager::quantifier_manager(context & ctx, smt_params & fp, params_ref const & p) { @@ -366,14 +362,7 @@ namespace smt { plugin->set_manager(*this); } } - - void quantifier_manager::set_cancel(bool f) { - #pragma omp critical (quantifier_manager) - { - m_imp->set_cancel(f); - } - } - + void quantifier_manager::display(std::ostream & out) const { } @@ -591,12 +580,6 @@ namespace smt { return quantifier_manager::UNKNOWN; } - virtual void set_cancel(bool f) { - // TODO: interrupt MAM and MBQI - m_model_finder->set_cancel(f); - m_model_checker->set_cancel(f); - } - virtual final_check_status final_check_eh(bool full) { if (!full) { if (m_fparams->m_qi_lazy_instantiation) diff --git a/src/smt/smt_quantifier.h b/src/smt/smt_quantifier.h index a8becae36..e814afcb1 100644 --- a/src/smt/smt_quantifier.h +++ b/src/smt/smt_quantifier.h @@ -83,7 +83,6 @@ namespace smt { void pop(unsigned num_scopes); void reset(); - void set_cancel(bool f); void display(std::ostream & out) const; void display_stats(std::ostream & out, quantifier * q) const; @@ -166,7 +165,6 @@ namespace smt { virtual void push() = 0; virtual void pop(unsigned num_scopes) = 0; - virtual void set_cancel(bool f) = 0; }; };