From 92376e67f283445073af27214976b45721784579 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 16 Oct 2024 13:07:04 -0700
Subject: [PATCH] better model replay for loose entries

---
 src/ast/simplifiers/elim_unconstrained.cpp    |  2 +-
 .../model_reconstruction_trail.cpp            | 25 +++++++++++++++++--
 .../simplifiers/model_reconstruction_trail.h  |  1 -
 3 files changed, 24 insertions(+), 4 deletions(-)

diff --git a/src/ast/simplifiers/elim_unconstrained.cpp b/src/ast/simplifiers/elim_unconstrained.cpp
index 44b1ee091..34579b710 100644
--- a/src/ast/simplifiers/elim_unconstrained.cpp
+++ b/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;
diff --git a/src/ast/simplifiers/model_reconstruction_trail.cpp b/src/ast/simplifiers/model_reconstruction_trail.cpp
index 1f3c74ea2..500e67f78 100644
--- a/src/ast/simplifiers/model_reconstruction_trail.cpp
+++ b/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));
 }
 
 /**
diff --git a/src/ast/simplifiers/model_reconstruction_trail.h b/src/ast/simplifiers/model_reconstruction_trail.h
index 4c064124a..02271c6b4 100644
--- a/src/ast/simplifiers/model_reconstruction_trail.h
+++ b/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));