diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 6d39019c6..e63fc148d 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -4016,6 +4016,7 @@ 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 163003c01..4a1d9c6e6 100644 --- a/src/smt/smt_model_checker.cpp +++ b/src/smt/smt_model_checker.cpp @@ -40,7 +40,8 @@ namespace smt { m_max_cexs(1), m_iteration_idx(0), m_curr_model(0), - m_new_instances_bindings(m) { + m_new_instances_bindings(m), + m_cancel(false) { } model_checker::~model_checker() { diff --git a/src/smt/smt_model_checker.h b/src/smt/smt_model_checker.h index 053621f1a..93488ff65 100644 --- a/src/smt/smt_model_checker.h +++ b/src/smt/smt_model_checker.h @@ -51,6 +51,7 @@ 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(); @@ -92,6 +93,8 @@ namespace smt { void restart_eh(); void reset(); + + void set_cancel(bool f) { m_cancel = f; } }; }; diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp index 568e9fca9..393bd6db2 100644 --- a/src/smt/smt_model_finder.cpp +++ b/src/smt/smt_model_finder.cpp @@ -34,6 +34,8 @@ Revision History: #include"well_sorted.h" #include"model_pp.h" #include"ast_smt2_pp.h" +#include"cooperate.h" +#include"tactic_exception.h" namespace smt { @@ -1714,14 +1716,22 @@ 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; + bool m_cancel; friend class quantifier_analyzer; + void checkpoint() { + cooperate("quantifier_info"); + if (m_cancel) + throw tactic_exception(TACTIC_CANCELED_MSG); + } + void insert_qinfo(qinfo * qi) { // I'm assuming the number of qinfo's per quantifier is small. So, the linear search is not a big deal. ptr_vector::iterator it = m_qinfo_vect.begin(); ptr_vector::iterator end = m_qinfo_vect.end(); for (; it != end; ++it) { + checkpoint(); if (qi->is_equal(*it)) { dealloc(qi); return; @@ -1743,7 +1753,8 @@ namespace smt { m_is_auf(true), m_has_x_eq_y(false), m_the_one(0), - m_uvar_inst_sets(0) { + m_uvar_inst_sets(0), + m_cancel(false) { if (has_quantifiers(q->get_expr())) { static bool displayed_flat_msg = false; if (!displayed_flat_msg) { @@ -1896,6 +1907,7 @@ namespace smt { } } + void set_cancel(bool f) { m_cancel = f; } }; /** @@ -1908,6 +1920,7 @@ namespace smt { array_util m_array_util; arith_util m_arith_util; bv_util m_bv_util; + bool m_cancel; quantifier_info * m_info; @@ -2318,9 +2331,16 @@ namespace smt { visit_formula(n->get_arg(1), POS); visit_formula(n->get_arg(1), NEG); } + + void checkpoint() { + cooperate("quantifier_analyzer"); + if (m_cancel) + throw tactic_exception(TACTIC_CANCELED_MSG); + } void process_formulas_on_stack() { while (!m_ftodo.empty()) { + checkpoint(); entry & e = m_ftodo.back(); expr * curr = e.first; polarity pol = e.second; @@ -2411,7 +2431,8 @@ namespace smt { m_array_util(m), m_arith_util(m), m_bv_util(m), - m_info(0) { + m_info(0), + m_cancel(false) { } @@ -2441,6 +2462,11 @@ namespace smt { m_info = 0; } + void set_cancel(bool f) { + m_cancel = f; + m_info->set_cancel(f); + } + }; /** @@ -3259,7 +3285,8 @@ namespace smt { 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_new_constraints(m) { + m_new_constraints(m), + m_cancel(false) { } model_finder::~model_finder() { @@ -3535,4 +3562,9 @@ namespace smt { } } + void model_finder::set_cancel(bool f) { + m_cancel = f; + m_analyzer->set_cancel(f); + } + }; diff --git a/src/smt/smt_model_finder.h b/src/smt/smt_model_finder.h index a509ab1a5..9fd0e2645 100644 --- a/src/smt/smt_model_finder.h +++ b/src/smt/smt_model_finder.h @@ -50,6 +50,8 @@ Revision History: #include"func_decl_dependencies.h" #include"simplifier.h" #include"proto_model.h" +#include"cooperate.h" +#include"tactic_exception.h" namespace smt { class context; @@ -83,6 +85,7 @@ 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; @@ -102,6 +105,12 @@ namespace smt { void process_auf(ptr_vector const & qs, proto_model * m); instantiation_set const * get_uvar_inst_set(quantifier * q, unsigned i) const; + void checkpoint() { + cooperate("model_finder"); + if (m_cancel) + throw tactic_exception(TACTIC_CANCELED_MSG); + } + public: model_finder(ast_manager & m, simplifier & s); ~model_finder(); @@ -119,6 +128,8 @@ namespace smt { bool restrict_sks_to_inst_set(context * aux_ctx, quantifier * q, expr_ref_vector const & sks); void restart_eh(); + + void set_cancel(bool f); }; }; diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp index f824cb3f1..f3e4959f8 100644 --- a/src/smt/smt_quantifier.cpp +++ b/src/smt/smt_quantifier.cpp @@ -593,6 +593,8 @@ namespace smt { 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) {