From 8495be11f97862a61a184789ed55e73bb43f1246 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 31 Jan 2023 13:34:52 -0800 Subject: [PATCH] add shortcut filter to avoid traversing model reconstruction trail if there are no intersections with model --- .../model_reconstruction_trail.cpp | 16 ++++++--- .../simplifiers/model_reconstruction_trail.h | 35 ++++++++++++++++--- src/cmd_context/simplifier_cmds.cpp | 2 +- 3 files changed, 43 insertions(+), 10 deletions(-) diff --git a/src/ast/simplifiers/model_reconstruction_trail.cpp b/src/ast/simplifiers/model_reconstruction_trail.cpp index 22b600ded..65635c8e4 100644 --- a/src/ast/simplifiers/model_reconstruction_trail.cpp +++ b/src/ast/simplifiers/model_reconstruction_trail.cpp @@ -22,20 +22,26 @@ Author: // accumulate a set of dependent exprs, updating m_trail to exclude loose // substitutions that use variables from the dependent expressions. -// TODO: add filters to skip sections of the trail that do not touch the current free variables. void model_reconstruction_trail::replay(unsigned qhead, expr_ref_vector& assumptions, dependent_expr_state& st) { - TRACE("simplifier", - for (unsigned i = qhead; i < st.qtail(); ++i) - tout << mk_bounded_pp(st[i].fml(), m) << "\n"; - ); + ast_mark free_vars; + m_intersects_with_model = false; scoped_ptr rp = mk_default_expr_replacer(m, false); for (unsigned i = qhead; i < st.qtail(); ++i) add_vars(st[i], free_vars); for (expr* a : assumptions) add_vars(a, free_vars); + TRACE("simplifier", + tout << "intersects " << m_intersects_with_model << "\n"; + for (unsigned i = qhead; i < st.qtail(); ++i) + tout << mk_bounded_pp(st[i].fml(), m) << "\n"; + ); + + if (!m_intersects_with_model) + return; + for (auto& t : m_trail) { TRACE("simplifier", tout << " active " << t->m_active << " hide " << t->is_hide() << " intersects " << t->intersects(free_vars) << "\n"); if (!t->m_active) diff --git a/src/ast/simplifiers/model_reconstruction_trail.h b/src/ast/simplifiers/model_reconstruction_trail.h index 89a112c24..d9b51cb22 100644 --- a/src/ast/simplifiers/model_reconstruction_trail.h +++ b/src/ast/simplifiers/model_reconstruction_trail.h @@ -40,7 +40,6 @@ class model_reconstruction_trail { vector m_removed; func_decl_ref m_decl; vector> m_defs; - bool m_active = true; entry(ast_manager& m, expr_substitution* s, vector const& rem) : @@ -84,12 +83,35 @@ class model_reconstruction_trail { ast_manager& m; trail_stack& m_trail_stack; scoped_ptr_vector m_trail; + func_decl_ref_vector m_model_vars_trail; + ast_mark m_model_vars; + bool m_intersects_with_model = false; + + struct undo_model_var : public trail { + model_reconstruction_trail& s; + undo_model_var(model_reconstruction_trail& s) : s(s) {} + virtual void undo() { + s.m_model_vars.mark(s.m_model_vars_trail.back(), false); + s.m_model_vars_trail.pop_back(); + } + }; + + void add_model_var(func_decl* f) { + if (!m_model_vars.is_marked(f)) { + m_model_vars_trail.push_back(f); + m_model_vars.mark(f, true); + m_trail_stack.push(undo_model_var(*this)); + } + } 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)) { - TRACE("simplifier", tout << "add var " << to_app(t)->get_decl()->get_name() << "\n"); - free_vars.mark(to_app(t)->get_decl(), true); + func_decl* f = to_app(t)->get_decl(); + TRACE("simplifier", tout << "add var " << f->get_name() << "\n"); + free_vars.mark(f, true); + if (m_model_vars.is_marked(f)) + m_intersects_with_model = true; } } @@ -117,7 +139,9 @@ public: */ void push(expr_substitution* s, vector const& removed) { m_trail.push_back(alloc(entry, m, s, removed)); - m_trail_stack.push(push_back_vector(m_trail)); + m_trail_stack.push(push_back_vector(m_trail)); + for (auto& [k, v] : s->sub()) + add_model_var(to_app(k)->get_decl()); } /** @@ -134,6 +158,7 @@ public: void push(func_decl* f, expr* def, expr_dependency* dep, vector const& removed) { m_trail.push_back(alloc(entry, m, f, def, dep, removed)); m_trail_stack.push(push_back_vector(m_trail)); + add_model_var(f); } /** @@ -142,6 +167,8 @@ public: void push(vector> const& defs, vector const& removed) { m_trail.push_back(alloc(entry, m, defs, removed)); m_trail_stack.push(push_back_vector(m_trail)); + for (auto const& [f, def, dep] : defs) + add_model_var(f); } /** diff --git a/src/cmd_context/simplifier_cmds.cpp b/src/cmd_context/simplifier_cmds.cpp index 0ea88e095..0050dc548 100644 --- a/src/cmd_context/simplifier_cmds.cpp +++ b/src/cmd_context/simplifier_cmds.cpp @@ -123,7 +123,7 @@ ATOMIC_CMD(help_simplifier_cmd, "help-simplifier", "display the simplifier combi class set_simplifier_cmd : public parametric_cmd { protected: - sexpr * m_simplifier; + sexpr * m_simplifier = nullptr; public: set_simplifier_cmd(): parametric_cmd("set-simplifier") {}