mirror of
https://github.com/Z3Prover/z3
synced 2025-04-14 12:58:44 +00:00
Made quantifier-related parts of smt::model_finder and smt::model_checker interruptable.
Fixes #178
This commit is contained in:
Christoph M. Wintersteiger
parent
0e886cfe5e
commit
b9e273800c
|
|
@ -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);
|
||||
}
|
||||
|
||||
};
|
||||
|
|
|
|||
|
|
@ -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() {
|
||||
|
|
|
|||
|
|
@ -51,6 +51,7 @@ namespace smt {
|
|||
unsigned m_iteration_idx;
|
||||
proto_model * m_curr_model;
|
||||
obj_map<expr, expr *> 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; }
|
||||
};
|
||||
};
|
||||
|
||||
|
|
|
|||
|
|
@ -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<instantiation_set> * 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<qinfo>::iterator it = m_qinfo_vect.begin();
|
||||
ptr_vector<qinfo>::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);
|
||||
}
|
||||
|
||||
};
|
||||
|
|
|
|||
|
|
@ -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<simple_macro_solver> m_sm_solver;
|
||||
scoped_ptr<hint_solver> m_hint_solver;
|
||||
scoped_ptr<non_auf_macro_solver> m_nm_solver;
|
||||
bool m_cancel;
|
||||
|
||||
struct scope {
|
||||
unsigned m_quantifiers_lim;
|
||||
|
|
@ -102,6 +105,12 @@ namespace smt {
|
|||
void process_auf(ptr_vector<quantifier> 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);
|
||||
};
|
||||
};
|
||||
|
||||
|
|
|
|||
|
|
@ -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) {
|
||||
|
|
|
|||
Loading…
Reference in a new issue