From ebc2cd572b1952635842ada67d239b52d739df06 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 31 Jan 2023 14:53:04 -0800 Subject: [PATCH] fix build Signed-off-by: Nikolaj Bjorner --- .../simplifiers/model_reconstruction_trail.h | 26 ++++++++++++------- src/solver/simplifier_solver.cpp | 6 ++--- 2 files changed, 19 insertions(+), 13 deletions(-) diff --git a/src/ast/simplifiers/model_reconstruction_trail.h b/src/ast/simplifiers/model_reconstruction_trail.h index d9b51cb22..79a38401a 100644 --- a/src/ast/simplifiers/model_reconstruction_trail.h +++ b/src/ast/simplifiers/model_reconstruction_trail.h @@ -96,6 +96,9 @@ class model_reconstruction_trail { } }; + /** + * register that f occurs in the model reconstruction trail. + */ void add_model_var(func_decl* f) { if (!m_model_vars.is_marked(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) { for (expr* t : subterms::all(expr_ref(e, m))) 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); }); } + /** + * Append new updates to model converter. + */ + void append(generic_model_converter& mc); + public: 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 @@ -177,17 +190,12 @@ public: */ 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(); - - /** - * 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; }; diff --git a/src/solver/simplifier_solver.cpp b/src/solver/simplifier_solver.cpp index 6cdb4cd59..219b2c46b 100644 --- a/src/solver/simplifier_solver.cpp +++ b/src/solver/simplifier_solver.cpp @@ -62,7 +62,6 @@ class simplifier_solver : public solver { if (s.m.is_false(f)) 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 flatten_suffix() override { expr_mark seen; @@ -94,7 +93,7 @@ class simplifier_solver : public solver { dep_expr_state m_preprocess_state; seq_simplifier m_preprocess; expr_ref_vector m_assumptions; - generic_model_converter_ref m_mc; + model_converter_ref m_mc; bool m_inconsistent = false; void flush(expr_ref_vector& assumptions) { @@ -109,9 +108,8 @@ class simplifier_solver : public solver { return; 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_preprocess_state.append(*m_mc); for (; qhead < m_fmls.size(); ++qhead) add_with_dependency(m_fmls[qhead]); }