From a703cf81b185383122c2718051ba8cfa58bf4e33 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 15 Feb 2025 19:34:52 -0800
Subject: [PATCH] replace model_ref by model* in tg_project,

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/qe/mbp/mbp_arith.cpp      |  2 +-
 src/qe/mbp/mbp_euf.cpp        | 71 +++++++++++++++++++++++++----------
 src/qe/mbp/mbp_euf.h          |  1 +
 src/qe/mbp/mbp_term_graph.cpp |  4 +-
 4 files changed, 55 insertions(+), 23 deletions(-)

diff --git a/src/qe/mbp/mbp_arith.cpp b/src/qe/mbp/mbp_arith.cpp
index 5c1654a09..49ecb6e68 100644
--- a/src/qe/mbp/mbp_arith.cpp
+++ b/src/qe/mbp/mbp_arith.cpp
@@ -471,7 +471,7 @@ namespace mbp {
                     t = a.mk_idiv(t, a.mk_numeral(d.m_div, is_int));
                 else if (!d.m_div.is_one() && !is_int)
                     t = a.mk_div(t, a.mk_numeral(d.m_div, is_int));
-                result.push_back(def(expr_ref(x, m), t));
+                result.push_back({ expr_ref(x, m), t });
             }
         }
 
diff --git a/src/qe/mbp/mbp_euf.cpp b/src/qe/mbp/mbp_euf.cpp
index 632d7a7df..7fd8c6a51 100644
--- a/src/qe/mbp/mbp_euf.cpp
+++ b/src/qe/mbp/mbp_euf.cpp
@@ -29,10 +29,8 @@ namespace mbp {
     bool euf_project_plugin::operator()(model& model, app_ref_vector& vars, expr_ref_vector& lits) {
         return false;
     }
-    
-    bool euf_project_plugin::project(model& model, app_ref_vector& vars, expr_ref_vector& lits, vector<def>& defs) {
-        if (vars.empty())
-            return false;
+
+    void euf_project_plugin::solve_eqs(model& model, app_ref_vector& vars, expr_ref_vector& lits, vector<def>& defs) {
         flatten_and(lits);
         expr_mark var_set;
         auto is_pure = [&](expr_mark& var_set, expr* v) {
@@ -40,29 +38,37 @@ namespace mbp {
         };
         for (auto v : vars)
             var_set.mark(v, true);
-        unsigned has_def = false;
-#if 1
         // solve trivial equations
         for (auto e : lits) {
             expr* x = nullptr, *y = nullptr;
             if (m.is_eq(e, x, y) && var_set.is_marked(x) && is_pure(var_set, y)) {
                 vars.erase(to_app(x));
                 defs.push_back({ expr_ref(x, m), expr_ref(y, m) });
-                has_def = true;
             }
             else if (m.is_eq(e, y, x) && var_set.is_marked(x) && is_pure(var_set, y)) {
                 vars.erase(to_app(x));
                 defs.push_back({ expr_ref(x, m), expr_ref(y, m) });
-                has_def = true;
             }
         }
-        if (has_def)
-            return true;
-#endif
+    }
+    
+    bool euf_project_plugin::project(model& model, app_ref_vector& vars, expr_ref_vector& lits, vector<def>& defs) {
+        if (vars.empty())
+            return false;
+        unsigned sz = defs.size();
+        while (true) {
+            unsigned sz1 = defs.size();
+            solve_eqs(model, vars, lits, defs);
+            if (sz1 == defs.size())
+                break;
+        }
 
+        if (sz < defs.size())
+            return true;
+        
         // check if there is a variable of uninterp sort
         if (all_of(vars, [&](expr* v) { return !m.is_uninterp(v->get_sort()); }))
-            return has_def;
+            return false;
 
         term_graph tg(m);
         tg.add_lits(lits);
@@ -70,16 +76,41 @@ namespace mbp {
             if (m.is_uninterp(v->get_sort()))
                 tg.add_var(v);
 
-        //
-        // now what:
-        /// walk all subterms of lits.
-        // push in partitions by value.
-        // add equations from model
-        // compute repr from tg.
-        // 
+        expr_ref_vector terms(m);
+        for (expr* f : subterms::all(lits))
+            if (!m.is_bool(f))
+                terms.push_back(f);
+
+
+        // try to project on representatives:
+        tg.add_model_based_terms(model, terms);
+        unsigned j = 0;        
+        for (unsigned i = 0; i < vars.size(); ++i) {
+            app* v = vars.get(i);
+            if (m.is_uninterp(v->get_sort())) {
+                expr* r = tg.rep_of(v);
+                if (r) 
+                    defs.push_back({ expr_ref(v, m), expr_ref(r, m) });
+                else
+                    vars[j++] = v;
+            }
+            else
+                vars[j++] = v;
+        }
+        vars.shrink(j);
+
+        if (sz < defs.size())
+            return true;
+        
+
+        // walk equivalence classes.
+        // try to unify with pure classes.
+
+
+        // try to build a fresh term using available signature
 
         
-        return has_def;
+        return false;
     }
 
 }
diff --git a/src/qe/mbp/mbp_euf.h b/src/qe/mbp/mbp_euf.h
index f74e27f7d..055b6167b 100644
--- a/src/qe/mbp/mbp_euf.h
+++ b/src/qe/mbp/mbp_euf.h
@@ -13,6 +13,7 @@ Copyright (c) 2025 Microsoft Corporation
 namespace mbp {
 
     class euf_project_plugin : public project_plugin {
+        void solve_eqs(model& model, app_ref_vector& vars, expr_ref_vector& lits, vector<def>& defs);
     public:
         euf_project_plugin(ast_manager& m);
         ~euf_project_plugin() override;
diff --git a/src/qe/mbp/mbp_term_graph.cpp b/src/qe/mbp/mbp_term_graph.cpp
index e9a729d53..973d2c5cd 100644
--- a/src/qe/mbp/mbp_term_graph.cpp
+++ b/src/qe/mbp/mbp_term_graph.cpp
@@ -1086,7 +1086,7 @@ class term_graph::projector {
     u_map<expr *> m_root2rep;
     th_rewriter m_rewriter;
 
-    model_ref m_model;
+    model* m_model = nullptr;
     expr_ref_vector m_pinned; // tracks expr in the maps
 
     expr *mk_pure(term const &t) {
@@ -1454,7 +1454,7 @@ class term_graph::projector {
         m_term2app.reset();
         m_root2rep.reset();
         m_pinned.reset();
-        m_model.reset();
+        m_model = nullptr;
     }
 
     expr_ref_vector project() {