mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-18 11:58:31 +00:00
Code Activity

fix incremental pre-processing to work with assumptions/cores and consequences

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-02-01 19:47:58 -08:00
parent 7767144051
commit 6c7dd4a863
1 changed files with 24 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

28
src/solver/simplifier_solver.cpp
View file

@ -95,10 +95,21 @@ class simplifier_solver : public solver {
expr_ref_vector m_assumptions; expr_ref_vector m_assumptions;
model_converter_ref m_mc; model_converter_ref m_mc;
bool m_inconsistent = false; bool m_inconsistent = false;
expr_safe_replace m_core_replace;
void replace(expr_ref_vector& r) {
expr_ref tmp(m);
for (unsigned i = 0; i < r.size(); ++i) {
m_core_replace(r.get(i), tmp);
r[i] = tmp;
}
}
void flush(expr_ref_vector& assumptions) { void flush(expr_ref_vector& assumptions) {
unsigned qhead = m_preprocess_state.qhead(); unsigned qhead = m_preprocess_state.qhead();
if (qhead < m_fmls.size()) { expr_ref_vector orig_assumptions(assumptions);
m_core_replace.reset();
if (qhead < m_fmls.size() || !assumptions.empty()) {
for (expr* a : assumptions) for (expr* a : assumptions)
m_preprocess_state.freeze(a); m_preprocess_state.freeze(a);
TRACE("solver", tout << "qhead " << qhead << "\n"); TRACE("solver", tout << "qhead " << qhead << "\n");
@ -107,6 +118,8 @@ class simplifier_solver : public solver {
if (!m.inc()) if (!m.inc())
return; return;
m_preprocess_state.advance_qhead(); m_preprocess_state.advance_qhead();
for (unsigned i = 0; i < assumptions.size(); ++i)
m_core_replace.insert(assumptions.get(i), orig_assumptions.get(i));
} }
m_mc = m_preprocess_state.model_trail().get_model_converter(); m_mc = m_preprocess_state.model_trail().get_model_converter();
m_cached_mc = nullptr; m_cached_mc = nullptr;
@ -148,6 +161,7 @@ public:
m_preprocess_state(*this), m_preprocess_state(*this),
m_preprocess(m, s->get_params(), m_preprocess_state), m_preprocess(m, s->get_params(), m_preprocess_state),
m_assumptions(m), m_assumptions(m),
m_core_replace(m),
m_proof(m) m_proof(m)
{ {
if (fac) if (fac)
@ -189,7 +203,7 @@ public:
lbool check_sat_core(unsigned num_assumptions, expr* const* assumptions) override { lbool check_sat_core(unsigned num_assumptions, expr* const* assumptions) override {
expr_ref_vector _assumptions(m, num_assumptions, assumptions); expr_ref_vector _assumptions(m, num_assumptions, assumptions);
flush(_assumptions); flush(_assumptions);
return s->check_sat_core(num_assumptions, assumptions); return s->check_sat_core(num_assumptions, _assumptions.data());
} }
void collect_statistics(statistics& st) const override { void collect_statistics(statistics& st) const override {
@ -258,7 +272,7 @@ public:
std::string reason_unknown() const override { return s->reason_unknown(); } std::string reason_unknown() const override { return s->reason_unknown(); }
void set_reason_unknown(char const* msg) override { s->set_reason_unknown(msg); } void set_reason_unknown(char const* msg) override { s->set_reason_unknown(msg); }
void get_labels(svector<symbol>& r) override { s->get_labels(r); } void get_labels(svector<symbol>& r) override { s->get_labels(r); }
void get_unsat_core(expr_ref_vector& r) { s->get_unsat_core(r); } void get_unsat_core(expr_ref_vector& r) { s->get_unsat_core(r); replace(r); }
ast_manager& get_manager() const override { return s->get_manager(); } ast_manager& get_manager() const override { return s->get_manager(); }
void reset_params(params_ref const& p) override { s->reset_params(p); } void reset_params(params_ref const& p) override { s->reset_params(p); }
params_ref const& get_params() const override { return s->get_params(); } params_ref const& get_params() const override { return s->get_params(); }
@ -276,7 +290,13 @@ public:
lbool check_sat_cc(expr_ref_vector const& cube, vector<expr_ref_vector> const& clauses) override { return check_sat_cc(cube, clauses); } lbool check_sat_cc(expr_ref_vector const& cube, vector<expr_ref_vector> const& clauses) override { return check_sat_cc(cube, clauses); }
void set_progress_callback(progress_callback* callback) override { s->set_progress_callback(callback); } void set_progress_callback(progress_callback* callback) override { s->set_progress_callback(callback); }
lbool get_consequences(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) override { lbool get_consequences(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) override {
return s->get_consequences(asms, vars, consequences); expr_ref_vector es(m);
es.append(asms);
es.append(vars);
flush(es);
lbool r = s->get_consequences(asms, vars, consequences);
replace(consequences);
return r;
} }
lbool find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes) override { return s->find_mutexes(vars, mutexes); } lbool find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes) override { return s->find_mutexes(vars, mutexes); }
lbool preferred_sat(expr_ref_vector const& asms, vector<expr_ref_vector>& cores) override { return s->preferred_sat(asms, cores); } lbool preferred_sat(expr_ref_vector const& asms, vector<expr_ref_vector>& cores) override { return s->preferred_sat(asms, cores); }