set up model reconstruction trail

src/ast/expr_substitution.h

@@ -44,8 +44,10 @@ public:
     bool empty() const { return m_subst.empty(); }
     unsigned size() const { return m_subst.size(); }
     void insert(expr * s, expr * def, proof * def_pr = nullptr, expr_dependency * def_dep = nullptr);
+    void insert(expr* s, expr* def, expr_dependency* def_dep) { insert(s, def, nullptr, def_dep); }
     void erase(expr * s);
-    expr* find(expr* s) { proof* pr; expr* def; VERIFY(find(s, def, pr)); SASSERT(def); return def; }
+    expr* find(expr* s) { return m_subst[s]; }
+    expr_dependency* dep(expr* s) { return (*m_subst_dep)[s]; }
     bool find(expr * s, expr * & def, proof * & def_pr);
     bool find(expr * s, expr * & def, proof * & def_pr, expr_dependency * & def_dep);
     bool contains(expr * s);

src/ast/rewriter/expr_replacer.cpp

@@ -25,6 +25,11 @@ void expr_replacer::operator()(expr * t, expr_ref & result, proof_ref & result_p
     operator()(t, result, result_pr, result_dep);
 }
 
+void expr_replacer::operator()(expr* t, expr_ref& result, expr_dependency_ref& result_dep) {
+    proof_ref result_pr(m());
+    operator()(t, result, result_pr, result_dep);
+}
+
 void expr_replacer::operator()(expr * t, expr_ref & result) {
     proof_ref pr(m());
     operator()(t, result, pr);

src/ast/rewriter/expr_replacer.h

@@ -34,9 +34,10 @@ public:
     virtual void set_substitution(expr_substitution * s) = 0;
 
     virtual void operator()(expr * t, expr_ref & result, proof_ref & result_pr, expr_dependency_ref & deps) = 0;
-    virtual void operator()(expr * t, expr_ref & result, proof_ref & result_pr);
+    void operator()(expr* t, expr_ref& result, expr_dependency_ref& deps);
-    virtual void operator()(expr * t, expr_ref & result);
+    void operator()(expr * t, expr_ref & result, proof_ref & result_pr);
-    virtual void operator()(expr_ref & t) { expr_ref s(t, m()); (*this)(s, t); }
+    void operator()(expr * t, expr_ref & result);
+    void operator()(expr_ref & t) { expr_ref s(t, m()); (*this)(s, t); }
 
     virtual unsigned get_num_steps() const { return 0; }
     virtual void reset() = 0;

src/ast/simplifiers/dependent_expr.h

@@ -69,6 +69,10 @@ public:
         m_dep = nullptr;
     }
 
+    ast_manager& get_manager() const { return m; }
+
+    expr* fml() const { return m_fml; }
+    
     std::tuple<expr*, expr_dependency*> operator()() const { 
         return { m_fml, m_dep }; 
     }

src/ast/simplifiers/model_reconstruction_trail.cpp

@@ -21,24 +21,86 @@ void model_reconstruction_trail::replay(dependent_expr const& d, vector<dependen
     // accumulate a set of dependent exprs, updating m_trail to exclude loose 
     // substitutions that use variables from the dependent expressions.
     ast_mark free_vars;
-    auto [f, dep] = d();
-    for (expr* t : subterms::all(expr_ref(f, m))) 
-        free_vars.mark(t, true);
     
-    NOT_IMPLEMENTED_YET();
+    add_vars(d, free_vars);
+
+    added.push_back(d);
+
+    for (auto& t : m_trail) {
+        if (!t->m_active)
+            continue;
+
+        // updates that have no intersections with current variables are skipped
+        if (!t->intersects(free_vars)) 
+            continue;        
+
+        // loose entries that intersect with free vars are deleted from the trail
+        // and their removed formulas are added to the resulting constraints.
+        if (t->is_loose()) {
+            added.append(t->m_removed); 
+            for (auto r : t->m_removed) 
+                add_vars(r, free_vars);            
+            m_trail_stack.push(value_trail(t->m_active));
+            t->m_active = false;      
+            continue;
+        }
+        
+        // rigid entries:
+        // apply substitution to added in case of rigid model convertions
+        for (auto& d : added) {
+            auto [f, dep1] = d();
+            expr_ref g(m);
+            expr_dependency_ref dep2(m);
+            (*t->m_replace)(f, g, dep2);
+            d = dependent_expr(m, g, m.mk_join(dep1, dep2));
+        }    
+    }
 }
 
 /**
  * retrieve the current model converter corresponding to chaining substitutions from the trail.
  */
 model_converter_ref model_reconstruction_trail::get_model_converter() {
-    model_converter_ref mc = alloc(generic_model_converter, m, "dependent-expr-model");
+
+    //
     // 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.
-    NOT_IMPLEMENTED_YET();
+    //
-    return mc;
+
+    scoped_ptr<expr_replacer> rp = mk_default_expr_replacer(m, true);
+    scoped_ptr<expr_substitution> subst = alloc(expr_substitution, m, true, false);
+    rp->set_substitution(subst.get());
+    generic_model_converter_ref mc = alloc(generic_model_converter, m, "dependent-expr-model");
+    bool first = true;
+    for (unsigned i = m_trail.size(); i-- > 0; ) {
+        auto* t = m_trail[i];
+        if (!t->m_active)
+            continue;
+
+        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;
+        }
+        expr_dependency_ref new_dep(m);
+        expr_ref new_def(m);
+
+        for (auto const& [v, def] : t->m_subst->sub()) {
+            rp->operator()(def, new_def, new_dep);
+            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

@@ -24,33 +24,62 @@ Author:
 #pragma once
 
 #include "util/scoped_ptr_vector.h"
+#include "util/trail.h"
+#include "ast/for_each_expr.h"
 #include "ast/rewriter/expr_replacer.h"
 #include "ast/simplifiers/dependent_expr.h"
 #include "ast/converters/model_converter.h"
 
 class model_reconstruction_trail {
 
-    ast_manager& m;
+    struct entry {
-
-    struct model_reconstruction_trail_entry {
         scoped_ptr<expr_replacer>     m_replace;
+        scoped_ptr<expr_substitution> m_subst;
         vector<dependent_expr>        m_removed;
-        model_reconstruction_trail_entry(expr_replacer* r, vector<dependent_expr> const& rem) :
+        bool                          m_active = true;
-            m_replace(r), m_removed(rem) {}
+
+        entry(expr_replacer* r, expr_substitution* s, vector<dependent_expr> const& rem) :
+            m_replace(r), m_subst(s), m_removed(rem) {}
+
+        bool is_loose() const { return !m_removed.empty(); }
+
+        bool intersects(ast_mark const& free_vars) const {
+            return std::any_of(m_subst->sub().begin(), m_subst->sub().end(), [&](auto const& kv) { return free_vars.is_marked(kv.m_key); });
+        }
+
+
     };
 
-    scoped_ptr_vector<model_reconstruction_trail_entry> m_trail;
+    ast_manager&             m;
-    unsigned_vector m_limit;
+    trail_stack&             m_trail_stack;
+    scoped_ptr_vector<entry> m_trail;
+
+    void add_vars(dependent_expr const& d, ast_mark& free_vars) {
+        for (expr* t : subterms::all(expr_ref(d.fml(), d.get_manager())))
+            free_vars.mark(t, true);
+    }
+
+    bool intersects(ast_mark const& free_vars, dependent_expr const& d) {
+        expr_ref term(d.fml(), d.get_manager());
+        auto iter = subterms::all(term);
+        return std::any_of(iter.begin(), iter.end(), [&](expr* t) { return free_vars.is_marked(t); });
+    }
+
+    bool intersects(ast_mark const& free_vars, vector<dependent_expr> const& added) {
+        return std::any_of(added.begin(), added.end(), [&](dependent_expr const& d) { return intersects(free_vars, d); });
+    }
 
 public:
 
-    model_reconstruction_trail(ast_manager& m) : m(m) {}
+    model_reconstruction_trail(ast_manager& m, trail_stack& tr): 
+        m(m), m_trail_stack(tr) {}
 
     /**
     * add a new substitution to the stack
     */
     void push(expr_replacer* r, vector<dependent_expr> const& removed) {
-        m_trail.push_back(alloc(model_reconstruction_trail_entry, r, removed));
+        m_trail.push_back(alloc(entry, r, nullptr, removed));
+        m_trail_stack.push(push_back_vector(m_trail));
     }
 
     /**
@@ -63,18 +92,5 @@ public:
     * retrieve the current model converter corresponding to chaining substitutions from the trail.
     */
     model_converter_ref get_model_converter();
-
-    /**
-    * push a context. Portions of the trail added within a context are removed after a context pop.
-    */
-    void push() {
-        m_limit.push_back(m_trail.size());
-    }
-
-    void pop(unsigned n) {
-        unsigned old_sz = m_limit[m_limit.size() - n];
-        m_trail.resize(old_sz);
-        m_limit.shrink(m_limit.size() - n);
-    }
 };
 

src/ast/simplifiers/solve_eqs.cpp

@@ -60,7 +60,7 @@ namespace euf {
         m_id2level.reset();
         m_id2level.resize(m_id2var.size(), UINT_MAX);
         m_subst_ids.reset();
-        m_subst = alloc(expr_substitution, m, false, false);
+        m_subst = alloc(expr_substitution, m, true, false);
 
         auto is_explored = [&](unsigned id) {
             return m_id2level[id] != UINT_MAX;
@@ -120,16 +120,15 @@ namespace euf {
 
         expr_dependency_ref new_dep(m);
         expr_ref new_def(m);
-        proof_ref new_pr(m);
 
         for (unsigned id : m_subst_ids) {
             if (!m.inc())
                 break;
             auto const& [v, def, dep] = m_next[id][0];
-            rp->operator()(def, new_def, new_pr, new_dep);
+            rp->operator()(def, new_def, new_dep);
             m_stats.m_num_steps += rp->get_num_steps() + 1;
             new_dep = m.mk_join(dep, new_dep);
-            m_subst->insert(v, new_def, new_pr, new_dep);
+            m_subst->insert(v, new_def, nullptr, new_dep);
             // we updated the substitution, but we don't need to reset rp
             // because all cached values there do not depend on v.
         }
@@ -149,11 +148,10 @@ namespace euf {
         scoped_ptr<expr_replacer> rp = mk_default_expr_replacer(m, true);
         rp->set_substitution(m_subst.get());
         expr_ref new_f(m);
-        proof_ref new_pr(m);
         expr_dependency_ref new_dep(m);
         for (unsigned i = m_qhead; i < m_fmls.size() && !m_fmls.inconsistent(); ++i) {
             auto [f, d] = m_fmls[i]();
-            rp->operator()(f, new_f, new_pr, new_dep);
+            rp->operator()(f, new_f, new_dep);
             if (new_f == f)
                 continue;
             new_dep = m.mk_join(d, new_dep);

src/muz/spacer/spacer_iuc_solver.cpp

@@ -244,12 +244,10 @@ namespace spacer {
     }
     
     void iuc_solver::elim_proxies (expr_ref_vector &v) {
-        expr_ref f = mk_and (v);
         scoped_ptr<expr_replacer> rep = mk_expr_simp_replacer (m);
         rep->set_substitution (&m_elim_proxies_sub);
-        (*rep)(f);
+        (*rep)(v);
-        v.reset();
+        flatten_and(v);
-        flatten_and(f, v);
     }
     
     void iuc_solver::get_iuc(expr_ref_vector &core) {