mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

Browse source 
simplify assumptions and only replay assumptions after constraints are simplified. This allows simplifying assumptions with the current set of constraints independently of whether there is another check-sat.
This commit is contained in:
Nikolaj Bjorner 2023-10-05 17:23:03 +09:00
parent 4133a1cc5a
commit b0df74c1c1
2 changed files with 20 additions and 6 deletions

6
src/smt/theory_lra.cpp
View file

@ -2113,7 +2113,10 @@ public:
m_model_is_initialized = false;
flush_bound_axioms();
// disabled in master:
// propagate_nla();
// propagate_nla();
if (ctx().inconsistent())
return true;
if (!can_propagate_core())
return false;
m_new_def = false;
@ -3547,7 +3550,6 @@ public:
if (r == l_true) {
nctx.display_asserted_formulas(std::cout);
std::cout.flush();
std::cout.flush();
}
return l_true != r;
}

20
src/solver/simplifier_solver.cpp
View file

@ -24,6 +24,7 @@ Author:
#include "ast/rewriter/expr_safe_replace.h"
#include "ast/simplifiers/dependent_expr_state.h"
#include "ast/simplifiers/then_simplifier.h"
#include "ast/rewriter/th_rewriter.h"
#include "solver/solver.h"
#include "solver/simplifier_solver.h"
#include "solver/solver_preprocess.h"
@ -62,7 +63,16 @@ class simplifier_solver : public solver {
if (s.m.is_false(f))
s.set_inconsistent();
}
void replay(unsigned qhead, expr_ref_vector& assumptions) { m_reconstruction_trail.replay(qhead, assumptions, *this); }
void replay(unsigned qhead, expr_ref_vector& assumptions) {
m_reconstruction_trail.replay(qhead, assumptions, *this);
th_rewriter rw(s.m);
expr_ref tmp(s.m);
for (unsigned i = 0; i < assumptions.size(); ++i) {
tmp = assumptions.get(i);
rw(tmp);
assumptions[i] = tmp;
}
}
void flatten_suffix() override {
expr_mark seen;
unsigned j = qhead();
@ -109,15 +119,16 @@ class simplifier_solver : public solver {
unsigned qhead = m_preprocess_state.qhead();
expr_ref_vector orig_assumptions(assumptions);
m_core_replace.reset();
if (qhead < m_fmls.size() || !assumptions.empty()) {
m_preprocess_state.replay(qhead, assumptions);
m_preprocess_state.freeze(assumptions);
if (qhead < m_fmls.size()) {
m_preprocess.reduce();
if (!m.inc())
return;
TRACE("solver", tout << "qhead " << qhead << "\n";
m_preprocess_state.display(tout));
m_preprocess_state.advance_qhead();
}
if (!assumptions.empty()) {
m_preprocess_state.replay(m_preprocess_state.qhead(), assumptions);
for (unsigned i = 0; i < assumptions.size(); ++i)
m_core_replace.insert(assumptions.get(i), orig_assumptions.get(i));
}
@ -203,6 +214,7 @@ public:
lbool check_sat_core(unsigned num_assumptions, expr* const* assumptions) override {
expr_ref_vector _assumptions(m, num_assumptions, assumptions);
flush(_assumptions);
TRACE("simplifier", tout << _assumptions);
return s->check_sat_core(num_assumptions, _assumptions.data());
}