add shortcut filter to avoid traversing model reconstruction trail if there are no intersections with model

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<expr_replacer> 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)

src/ast/simplifiers/model_reconstruction_trail.h

@@ -40,7 +40,6 @@ class model_reconstruction_trail {
         vector<dependent_expr>        m_removed;
         func_decl_ref                 m_decl;
         vector<std::tuple<func_decl_ref, expr_ref, expr_dependency_ref>> m_defs;
-
         bool                          m_active = true;
 
         entry(ast_manager& m, expr_substitution* s, vector<dependent_expr> const& rem) :
@@ -84,12 +83,35 @@ class model_reconstruction_trail {
     ast_manager&             m;
     trail_stack&             m_trail_stack;
     scoped_ptr_vector<entry> 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");
+                func_decl* f = to_app(t)->get_decl();
-                free_vars.mark(to_app(t)->get_decl(), true);
+                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<dependent_expr> 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<dependent_expr> 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<std::tuple<func_decl_ref, expr_ref, expr_dependency_ref>> const& defs, vector<dependent_expr> 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);
     }
 
     /**

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") {}