mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 21:38:44 +00:00
Code Activity

fix build

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-01-31 14:53:04 -08:00
parent 88bf3c6e51
commit ebc2cd572b
2 changed files with 19 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

26
src/ast/simplifiers/model_reconstruction_trail.h
View file

@ -96,6 +96,9 @@ class model_reconstruction_trail {
} }
}; };
/**
* register that f occurs in the model reconstruction trail.
*/
void add_model_var(func_decl* f) { void add_model_var(func_decl* f) {
if (!m_model_vars.is_marked(f)) { if (!m_model_vars.is_marked(f)) {
m_model_vars_trail.push_back(f); m_model_vars_trail.push_back(f);
@ -104,6 +107,11 @@ class model_reconstruction_trail {
} }
} }
/**
* walk the free functions of 'e' and add them to 'free_vars'.
* record if there is an intersection with the model_vars that are
* registered when updates are added to the trail.
*/
void add_vars(expr* e, ast_mark& free_vars) { void add_vars(expr* e, ast_mark& free_vars) {
for (expr* t : subterms::all(expr_ref(e, m))) for (expr* t : subterms::all(expr_ref(e, m)))
if (is_app(t) && is_uninterp(t)) { if (is_app(t) && is_uninterp(t)) {
@ -129,10 +137,15 @@ class model_reconstruction_trail {
return any_of(added, [&](dependent_expr const& d) { return intersects(free_vars, d); }); return any_of(added, [&](dependent_expr const& d) { return intersects(free_vars, d); });
} }
/**
* Append new updates to model converter.
*/
void append(generic_model_converter& mc);
public: public:
model_reconstruction_trail(ast_manager& m, trail_stack& tr): model_reconstruction_trail(ast_manager& m, trail_stack& tr):
m(m), m_trail_stack(tr) {} m(m), m_trail_stack(tr), m_model_vars_trail(m) {}
/** /**
* add a new substitution to the trail * add a new substitution to the trail
@ -177,17 +190,12 @@ public:
*/ */
void replay(unsigned qhead, expr_ref_vector& assumptions, dependent_expr_state& fmls); void replay(unsigned qhead, expr_ref_vector& assumptions, dependent_expr_state& fmls);
/** /**
* retrieve the current model converter corresponding to chaining substitutions from the trail. * retrieve the current model converter corresponding to chaining substitutions from the trail.
*/ */
model_converter_ref get_model_converter(); model_converter_ref get_model_converter();
/**
* Append new updates to model converter, update m_trail_index in the process.
*/
void append(generic_model_converter& mc);
std::ostream& display(std::ostream& out) const; std::ostream& display(std::ostream& out) const;
}; };

6
src/solver/simplifier_solver.cpp
View file

@ -62,7 +62,6 @@ class simplifier_solver : public solver {
if (s.m.is_false(f)) if (s.m.is_false(f))
s.set_inconsistent(); s.set_inconsistent();
} }
void append(generic_model_converter& mc) { model_trail().append(mc); }
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); }
void flatten_suffix() override { void flatten_suffix() override {
expr_mark seen; expr_mark seen;
@ -94,7 +93,7 @@ class simplifier_solver : public solver {
dep_expr_state m_preprocess_state; dep_expr_state m_preprocess_state;
seq_simplifier m_preprocess; seq_simplifier m_preprocess;
expr_ref_vector m_assumptions; expr_ref_vector m_assumptions;
generic_model_converter_ref m_mc; model_converter_ref m_mc;
bool m_inconsistent = false; bool m_inconsistent = false;
void flush(expr_ref_vector& assumptions) { void flush(expr_ref_vector& assumptions) {
@ -109,9 +108,8 @@ class simplifier_solver : public solver {
return; return;
m_preprocess_state.advance_qhead(); m_preprocess_state.advance_qhead();
} }
m_mc = alloc(generic_model_converter, m, "simplifier-model-converter"); m_mc = m_preprocess_state.model_trail().get_model_converter();
m_cached_mc = nullptr; m_cached_mc = nullptr;
m_preprocess_state.append(*m_mc);
for (; qhead < m_fmls.size(); ++qhead) for (; qhead < m_fmls.size(); ++qhead)
add_with_dependency(m_fmls[qhead]); add_with_dependency(m_fmls[qhead]);
} }