mirror of
https://github.com/Z3Prover/z3
synced 2025-04-28 11:25:51 +00:00
Merge branch 'master' of https://github.com/Z3Prover/z3
This commit is contained in:
Christoph M. Wintersteiger
commit
8fef9e57c5
7 changed files with 24 additions and 65 deletions
|
|
@ -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);
|
||||
}
|
||||
|
||||
};
|
||||
|
|
|
|||
|
|
@ -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) {
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -51,7 +51,6 @@ 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();
|
||||
|
|
@ -98,8 +97,6 @@ namespace smt {
|
|||
|
||||
void reset();
|
||||
|
||||
void set_cancel(bool f) { m_cancel = f; }
|
||||
|
||||
void operator()(expr* e);
|
||||
|
||||
};
|
||||
|
|
|
|||
|
|
@ -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<instantiation_set> * 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<cond_macro>::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<quantifier, quantifier_info *>::iterator it = m_q2info.begin();
|
||||
obj_map<quantifier, quantifier_info *>::iterator end = m_q2info.end();
|
||||
for (; it != end; ++it)
|
||||
(*it).m_value->set_cancel(f);
|
||||
}
|
||||
|
||||
};
|
||||
|
|
|
|||
|
|
@ -85,7 +85,6 @@ 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;
|
||||
|
|
@ -104,12 +103,8 @@ namespace smt {
|
|||
void process_non_auf_macros(ptr_vector<quantifier> & qs, ptr_vector<quantifier> & residue, proto_model * m);
|
||||
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();
|
||||
|
||||
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);
|
||||
};
|
||||
};
|
||||
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
};
|
||||
};
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue