better model replay for loose entries

src/ast/simplifiers/elim_unconstrained.cpp

@@ -80,7 +80,7 @@ void elim_unconstrained::eliminate() {
             continue;
         }
         expr* e = get_parent(v);
-        TRACE("elim_unconstrained", for (expr* p : n.m_parents) verbose_stream() << "parent " << mk_bounded_pp(p, m) << " @ " << get_node(p).m_refcount << "\n";);
+        TRACE("elim_unconstrained", for (expr* p : n.m_parents) tout << "parent " << mk_bounded_pp(p, m) << " @ " << get_node(p).m_refcount << "\n";);
         if (!e || !is_app(e) || !is_ground(e)) {
             n.m_refcount = 0;
             continue;

src/ast/simplifiers/model_reconstruction_trail.cpp

@@ -61,7 +61,7 @@ void model_reconstruction_trail::replay(unsigned qhead, expr_ref_vector& assumpt
         return;
 
     for (auto& t : m_trail) {
-        TRACE("simplifier", tout << " active " << t->m_active << " hide " << t->is_hide() << " intersects " << t->intersects(free_vars) << "\n");
+        TRACE("simplifier", tout << " active " << t->m_active << " hide " << t->is_hide() << " intersects " << t->intersects(free_vars) << " loose " << t->is_loose() << "\n");
         if (!t->m_active)
             continue;
 
@@ -74,9 +74,22 @@ void model_reconstruction_trail::replay(unsigned qhead, expr_ref_vector& assumpt
 
         // 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()) {
+
+        if (t->is_loose() && !t->is_def() && t->is_subst()) {
+            for (auto const& [k, v] : t->m_subst->sub())
+                st.add(dependent_expr(m, m.mk_eq(k, v), nullptr, nullptr));
+            t->m_active = false;
+            continue;
+        }
+
+        bool all_const = true;
+        for (auto const& [d, def, dep] : t->m_defs) 
+            all_const &= d->get_arity() == 0;
+
+        if (t->is_loose() && (!t->is_def() || !all_const || t->is_subst())) {
             for (auto r : t->m_removed) {
                 add_vars(r, free_vars);
+                TRACE("simplifier", tout << "replay removed " << r << "\n");
                 st.add(r);
             }
             m_trail_stack.push(value_trail(t->m_active));
@@ -116,6 +129,12 @@ void model_reconstruction_trail::replay(unsigned qhead, expr_ref_vector& assumpt
                     assumptions[i] = g;
                 // ignore dep.
             }
+            if (t->is_loose()) {
+                SASSERT(all_const);
+                SASSERT(!t->is_subst());
+                for (auto const& [d, def, dep] : t->m_defs) 
+                    st.add(dependent_expr(m, m.mk_eq(m.mk_const(d), def), nullptr, nullptr));
+            }
             continue;
         }
 
@@ -156,6 +175,8 @@ void model_reconstruction_trail::replay(unsigned qhead, expr_ref_vector& assumpt
             // ignore dep.
         }        
     }
+
+    TRACE("simplifier", st.display(tout));
 }
 
 /**

src/ast/simplifiers/model_reconstruction_trail.h

@@ -101,7 +101,6 @@ class model_reconstruction_trail {
     */
     void add_model_var(func_decl* f) {
         if (!m_model_vars.is_marked(f)) {
-            verbose_stream() << "add model var " << f->get_name() << "\n";
             m_model_vars_trail.push_back(f);
             m_model_vars.mark(f, true);
             m_trail_stack.push(undo_model_var(*this));