add isolated hide/add model converter functions

src/ast/simplifiers/model_reconstruction_trail.cpp

@@ -30,8 +30,9 @@ void model_reconstruction_trail::replay(dependent_expr const& d, vector<dependen
         if (!t->m_active)
             continue;
 
-        if (t->m_hide)
+        if (t->is_hide())
             continue;
+
         
         // updates that have no intersections with current variables are skipped
         if (!t->intersects(free_vars)) 
@@ -48,6 +49,9 @@ void model_reconstruction_trail::replay(dependent_expr const& d, vector<dependen
             continue;
         }
         
+        if (t->is_def())
+            NOT_IMPLEMENTED_YET();
+
         rp->set_substitution(t->m_subst.get());
         // rigid entries:
         // apply substitution to added in case of rigid model convertions
@@ -63,48 +67,23 @@ void model_reconstruction_trail::replay(dependent_expr const& d, vector<dependen
  * retrieve the current model converter corresponding to chaining substitutions from the trail.
  */
 model_converter_ref model_reconstruction_trail::get_model_converter() {
-
-    //
-    // walk the trail from the back
-    // add substitutions from the back to the generic model converter
-    // after they have been normalized using a global replace that replaces 
-    // substituted variables by their terms.
-    //
-
     
     scoped_ptr<expr_replacer> rp = mk_default_expr_replacer(m, false);
     expr_substitution subst(m, true, false);
     rp->set_substitution(&subst);
     generic_model_converter_ref mc = alloc(generic_model_converter, m, "dependent-expr-model");
-    bool first = true;
+    for (unsigned i = 0; i < m_trail.size(); ++i) {
-    for (unsigned i = m_trail.size(); i-- > 0; ) {
         auto* t = m_trail[i];
         if (!t->m_active)
             continue;
-
+        else if (t->is_hide()) 
-        if (t->m_hide) {
+            mc->hide(t->m_decl);
-            mc->hide(t->m_hide);
+        else if (t->is_def()) 
-            continue;
+            mc->add(t->m_decl, t->m_def);
-        }
+        else {
-
+            for (auto const& [v, def] : t->m_subst->sub())
-        if (first) {
-            first = false;
-            for (auto const& [v, def] : t->m_subst->sub()) {
-                expr_dependency* dep = t->m_subst->dep(v);
-                subst.insert(v, def, dep);
                 mc->add(v, def);
-            }
+        }        
-            continue;
-        }
-
-        for (auto const& [v, def] : t->m_subst->sub()) {
-            auto [new_def, new_dep] = rp->replace_with_dep(def);
-            expr_dependency* dep = t->m_subst->dep(v);
-            new_dep = m.mk_join(dep, new_dep);
-            subst.insert(v, new_def, new_dep);
-            mc->add(v, new_def);
-        }
-
     }
     return model_converter_ref(mc.get());
 

src/ast/simplifiers/model_reconstruction_trail.h

@@ -35,22 +35,35 @@ class model_reconstruction_trail {
     struct entry {
         scoped_ptr<expr_substitution> m_subst;
         vector<dependent_expr>        m_removed;
-        func_decl*                    m_hide = nullptr;
+        func_decl_ref                 m_decl;
+        expr_ref                      m_def;
         bool                          m_active = true;
 
-        entry(expr_substitution* s, vector<dependent_expr> const& rem) :
-            m_subst(s), m_removed(rem) {}
 
-        entry(func_decl* h) : m_hide(h) {}
+        entry(ast_manager& m, expr_substitution* s, vector<dependent_expr> const& rem) :
+            m_subst(s), m_removed(rem), m_decl(m), m_def(m) {}
+
+        entry(ast_manager& m, func_decl* h) : m_decl(h, m), m_def(m) {}
+
+        entry(ast_manager& m, func_decl* f, expr* def, vector<dependent_expr> const& rem) :
+            m_decl(f, m), m_def(def, m), m_removed(rem) {}
 
         bool is_loose() const { return !m_removed.empty(); }
 
         bool intersects(ast_mark const& free_vars) const {
+            if (is_hide())
+                return false;
+            if (is_def())
+                return free_vars.is_marked(m_decl);
             for (auto const& [k, v] : m_subst->sub())
                 if (free_vars.is_marked(k))
                     return true;
             return false;
         }
+
+        bool is_hide() const { return m_decl && !m_def; }
+        bool is_def() const { return m_decl && m_def; }
+        bool is_subst() const { return !m_decl; }
     };
 
     ast_manager&             m;
@@ -81,7 +94,7 @@ public:
     * add a new substitution to the trail
     */
     void push(expr_substitution* s, vector<dependent_expr> const& removed) {
-        m_trail.push_back(alloc(entry, s, removed));
+        m_trail.push_back(alloc(entry, m, s, removed));
         m_trail_stack.push(push_back_vector(m_trail));       
     }
 
@@ -89,7 +102,15 @@ public:
     * add declaration to hide
     */
     void push(func_decl* f) {
-        m_trail.push_back(alloc(entry, f));
+        m_trail.push_back(alloc(entry, m, f));
+        m_trail_stack.push(push_back_vector(m_trail));
+    }
+
+    /**
+     * add definition
+     */
+    void push(func_decl* f, expr* def, vector<dependent_expr> const& removed) {
+        m_trail.push_back(alloc(entry, m, f, def, removed));
         m_trail_stack.push(push_back_vector(m_trail));
     }