mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
separate rewriter used by smt context from asserted formulas to avoid term substitution, exposed by #2370
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
e5dffeace4
commit
db87f2aab0
|
@ -244,7 +244,7 @@ public:
|
|||
expr * get_formula(unsigned idx) const { return m_formulas[idx].get_fml(); }
|
||||
proof * get_formula_proof(unsigned idx) const { return m_formulas[idx].get_proof(); }
|
||||
|
||||
th_rewriter & get_rewriter() { return m_rewriter; }
|
||||
params_ref const& get_params() const { return m_params; }
|
||||
void get_assertions(ptr_vector<expr> & result) const;
|
||||
bool empty() const { return m_formulas.empty(); }
|
||||
void display(std::ostream & out) const;
|
||||
|
|
|
@ -47,6 +47,7 @@ namespace smt {
|
|||
m_params(_p),
|
||||
m_setup(*this, p),
|
||||
m_asserted_formulas(m, p, _p),
|
||||
m_rewriter(m),
|
||||
m_qmanager(alloc(quantifier_manager, *this, p, _p)),
|
||||
m_model_generator(alloc(model_generator, m)),
|
||||
m_relevancy_propagator(mk_relevancy_propagator(*this)),
|
||||
|
@ -94,6 +95,7 @@ namespace smt {
|
|||
SASSERT(m_search_lvl == 0);
|
||||
|
||||
m_case_split_queue = mk_case_split_queue(*this, p);
|
||||
m_rewriter.updt_params(m_asserted_formulas.get_params());
|
||||
|
||||
init();
|
||||
|
||||
|
|
|
@ -85,6 +85,7 @@ namespace smt {
|
|||
setup m_setup;
|
||||
timer m_timer;
|
||||
asserted_formulas m_asserted_formulas;
|
||||
th_rewriter m_rewriter;
|
||||
scoped_ptr<quantifier_manager> m_qmanager;
|
||||
scoped_ptr<model_generator> m_model_generator;
|
||||
scoped_ptr<relevancy_propagator> m_relevancy_propagator;
|
||||
|
@ -261,7 +262,7 @@ namespace smt {
|
|||
}
|
||||
|
||||
th_rewriter & get_rewriter() {
|
||||
return m_asserted_formulas.get_rewriter();
|
||||
return m_rewriter;
|
||||
}
|
||||
|
||||
smt_params & get_fparams() {
|
||||
|
|
|
@ -426,6 +426,7 @@ namespace smt {
|
|||
bool negated;
|
||||
|
||||
s(ante, s_ante);
|
||||
|
||||
if (ctx.get_cancel_flag()) return;
|
||||
negated = m.is_not(s_ante, s_ante_n);
|
||||
if (negated) s_ante = s_ante_n;
|
||||
|
|
Loading…
Reference in a new issue