bug fixes and cleanup in projection functions

spacer would drop variables of sorts not handled by main loop.
- projection with witness needs to disable qel style preprocessing to ensure witnesses are returned.
- add euf plugin to handle uninterpreted sorts (and then uninterpreted functions)

src/qe/mbp/CMakeLists.txt

@@ -6,6 +6,7 @@ z3_add_component(mbp
     mbp_basic_tg.cpp
     mbp_datatypes.cpp
     mbp_dt_tg.cpp
+    mbp_euf.cpp	
     mbp_qel.cpp
     mbp_qel_util.cpp
     mbp_plugin.cpp

src/qe/mbp/mbp_basic_tg.h

@@ -27,7 +27,7 @@ class mbp_basic_tg : public mbp_tg_plugin {
     struct impl;
     impl *m_impl;
 
-  public:
+public:
     mbp_basic_tg(ast_manager &man, mbp::term_graph &tg, model &mdl,
                  obj_hashtable<app> &vars_set, expr_sparse_mark &seen);
     // iterate through all terms in m_tg and apply all basic MBP rules once

src/qe/mbp/mbp_euf.cpp

@@ -0,0 +1,85 @@
+/*++
+Copyright (c) 2025 Microsoft Corporation
+
+--*/
+
+
+#include "ast/ast_util.h"
+#include "ast/for_each_expr.h"
+#include "qe/mbp/mbp_euf.h"
+#include "qe/mbp/mbp_term_graph.h"
+
+namespace mbp {
+    euf_project_plugin::euf_project_plugin(ast_manager& m): project_plugin(m) {
+        
+    }
+
+    euf_project_plugin::~euf_project_plugin() {
+
+    }
+    
+    bool euf_project_plugin::project1(model& model, app* var, app_ref_vector& vars, expr_ref_vector& lits) {
+        return false;
+    }
+    
+    family_id euf_project_plugin::get_family_id() {
+        return basic_family_id;        
+    }
+    
+    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;
+        flatten_and(lits);
+        expr_mark var_set;
+        auto is_pure = [&](expr_mark& var_set, expr* v) {
+            return all_of(subterms::all(expr_ref(v, m)), [&](expr* w) { return !var_set.is_marked(w); });
+        };
+        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
+
+        // 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;
+
+        term_graph tg(m);
+        tg.add_lits(lits);
+        for (auto v : vars) 
+            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.
+        // 
+
+        
+        return has_def;
+    }
+
+}

src/qe/mbp/mbp_euf.h

@@ -0,0 +1,30 @@
+
+/*++
+Copyright (c) 2025 Microsoft Corporation
+
+--*/
+
+
+#pragma once
+
+#include "model/model.h"
+#include "qe/mbp/mbp_plugin.h"
+
+namespace mbp {
+
+    class euf_project_plugin : public project_plugin {
+    public:
+        euf_project_plugin(ast_manager& m);
+        ~euf_project_plugin() override;
+        
+        bool project1(model& model, app* var, app_ref_vector& vars, expr_ref_vector& lits) override;
+        bool solve(model& model, app_ref_vector& vars, expr_ref_vector& lits) override { return false; }
+        family_id get_family_id() override;
+        bool operator()(model& model, app_ref_vector& vars, expr_ref_vector& lits) override;
+        bool project(model& model, app_ref_vector& vars, expr_ref_vector& lits, vector<def>& defs) override;
+        void saturate(model& model, func_decl_ref_vector const& shared, expr_ref_vector& lits) override { UNREACHABLE(); }
+
+    };
+
+};
+

src/qe/mbp/mbp_plugin.cpp

@@ -205,7 +205,7 @@ namespace mbp {
             else
                 extract_bools(eval, fmls, i, fml, true);
         }
-        TRACE("qe", tout << fmls << "\n";);
+        TRACE("qe", tout << "fmls: " << fmls << "\n";);
     }
 
     void project_plugin::extract_bools(model_evaluator& eval, expr_ref_vector& fmls, unsigned idx, expr* fml, bool is_true) {

src/qe/mbp/mbp_plugin.h

@@ -21,6 +21,7 @@ Revision History:
 #pragma once
 
 #include "ast/ast.h"
+#include "ast/ast_pp.h"
 #include "util/params.h"
 #include "model/model.h"
 #include "math/simplex/model_based_opt.h"
@@ -32,11 +33,12 @@ namespace mbp {
 
     struct def {
         expr_ref var, term;
-        def(const expr_ref& v, expr_ref& t): var(v), term(t) {}
     };
 
     class project_plugin {
+    protected:
         ast_manager&     m;
+    private:
         expr_mark        m_visited;
         ptr_vector<expr> m_to_visit;
         expr_mark        m_bool_visited;
@@ -110,3 +112,6 @@ namespace mbp {
     };
 }
 
+inline std::ostream& operator<<(std::ostream& out, mbp::def const& d) {
+    return out << d.var << " -> " << d.term << "\n";
+}

src/qe/mbp/mbp_term_graph.cpp

@@ -1018,8 +1018,7 @@ void term_graph::to_lits(expr_ref_vector &lits, bool all_equalities,
 void term_graph::to_lits_qe_lite(expr_ref_vector &lits,
                                  std::function<bool(expr *)> *non_core) {
     DEBUG_CODE(for (auto t : m_terms) SASSERT(t->get_repr()););
-    DEBUG_CODE(for (auto t
-                    : m_terms)
+    DEBUG_CODE(for (auto t : m_terms)
                    SASSERT(!t->is_cgr() || t->get_repr()->is_cgr()););
     is_non_core not_in_core(non_core);
     check_pred contains_nc(not_in_core, m, false);

src/qe/mbp/mbp_term_graph.h

@@ -32,10 +32,10 @@ Notes:
 #include "util/plugin_manager.h"
 
 namespace mbp {
-namespace is_ground_ns {
-struct proc;
-struct found;
-} // namespace is_ground_ns
+    namespace is_ground_ns {
+        struct proc;
+        struct found;
+    } // namespace is_ground_ns
 class term;
 
 class term_graph {
@@ -246,16 +246,16 @@ private:
     bool makes_cycle(term *t);
 };
 
-namespace is_ground_ns {
-struct found {};
-struct proc {
-    term_graph::is_variable_proc &m_is_var;
-    proc(term_graph::is_variable_proc &is_var) : m_is_var(is_var) {}
-    void operator()(var *n) const {}
-    void operator()(app const *n) const {
-        if (m_is_var.contains(n->get_decl())) throw found();
-    }
-    void operator()(quantifier *n) const {}
-};
-} // namespace is_ground_ns
+    namespace is_ground_ns {
+        struct found {};
+        struct proc {
+            term_graph::is_variable_proc &m_is_var;
+            proc(term_graph::is_variable_proc &is_var) : m_is_var(is_var) {}
+            void operator()(var *n) const {}
+            void operator()(app const *n) const {
+                if (m_is_var.contains(n->get_decl())) throw found();
+            }
+            void operator()(quantifier *n) const {}
+        };
+    } // namespace is_ground_ns
 } // namespace mbp

src/qe/mbp/mbp_tg_plugins.h

@@ -23,12 +23,12 @@ Revision History:
 #include "util/obj_hashtable.h"
 
 class mbp_tg_plugin {
-    public:
-        // iterate through all terms in m_tg and apply all theory MBP rules once
-        // returns true if any rules were applied
-        virtual bool apply() { return false; };
-        virtual ~mbp_tg_plugin() = default;
-        virtual void use_model() { };
-        virtual void get_new_vars(app_ref_vector*&) { };
-        virtual family_id get_family_id() const { return null_family_id; };
+public:
+    // iterate through all terms in m_tg and apply all theory MBP rules once
+    // returns true if any rules were applied
+    virtual bool apply() { return false; };
+    virtual ~mbp_tg_plugin() = default;
+    virtual void use_model() { };
+    virtual void get_new_vars(app_ref_vector*&) { };
+    virtual family_id get_family_id() const { return null_family_id; };
 };

src/qe/qe_mbp.cpp

@@ -37,6 +37,7 @@ Revision History:
 #include "qe/lite/qel.h"
 #include "qe/mbp/mbp_arith.h"
 #include "qe/mbp/mbp_arrays.h"
+#include "qe/mbp/mbp_euf.h"
 #include "qe/mbp/mbp_qel.h"
 #include "qe/mbp/mbp_datatypes.h"
 
@@ -352,6 +353,7 @@ public:
         add_plugin(alloc(mbp::arith_project_plugin, m));
         add_plugin(alloc(mbp::datatype_project_plugin, m));
         add_plugin(alloc(mbp::array_project_plugin, m));
+        add_plugin(alloc(mbp::euf_project_plugin, m));
         updt_params(p);
     }
 
@@ -392,18 +394,18 @@ public:
             flatten_and(fml, fmls);
         }
         else {
-        extract_literals(model, vars, fmls);
-        bool change = true;
-        while (change && !vars.empty()) {
-            change = solve(model, vars, fmls);
-            for (auto* p : m_plugins) {
-                if (p && p->solve(model, vars, fmls)) {
-                    change = true;
+            extract_literals(model, vars, fmls);
+            bool change = true;
+            while (change && !vars.empty()) {
+                change = solve(model, vars, fmls);
+                for (auto* p : m_plugins) {
+                    if (p && p->solve(model, vars, fmls)) {
+                        change = true;
+                    }
                 }
             }
         }
     }
-    }
 
     bool validate_model(model& model, expr_ref_vector const& fmls) {
         for (expr* f : fmls) {
@@ -419,24 +421,27 @@ public:
         return any_of(subterms::all(e), [&](expr* c) { return seq.is_char(c) || seq.is_seq(c); });
     }
     void operator()(bool force_elim, app_ref_vector& vars, model& model, expr_ref_vector& fmls, vector<mbp::def>* defs = nullptr) {
-            //don't use mbp_qel on some theories where model evaluation is
-            //incomplete This is not a limitation of qel. Fix this either by
-            //making mbp choices less dependent on the model evaluation methods
-            //or fix theory rewriters to make terms evaluation complete
-            if (m_use_qel && !has_unsupported_th(fmls) && !defs) {
-                bool dsub = m_dont_sub;
-                m_dont_sub = !force_elim;
-                expr_ref fml(m);
-                fml = mk_and(fmls);
-                spacer_qel(vars, model, fml);
-                fmls.reset();
-                flatten_and(fml, fmls);
-                m_dont_sub = dsub;
-            }
-            else {
-                mbp(force_elim, vars, model, fmls, defs);
-            }
+        //don't use mbp_qel on some theories where model evaluation is
+        //incomplete This is not a limitation of qel. Fix this either by
+        //making mbp choices less dependent on the model evaluation methods
+        //or fix theory rewriters to make terms evaluation complete
+        if (m_use_qel && !has_unsupported_th(fmls) && !defs) {
+            bool dsub = m_dont_sub;
+            m_dont_sub = !force_elim;
+            expr_ref fml(m);
+            fml = mk_and(fmls);
+            spacer_qel(vars, model, fml);
+            fmls.reset();
+            flatten_and(fml, fmls);
+            m_dont_sub = dsub;
+            TRACE("qe", tout << "spacer-qel " << vars << " " << fml << "\n");
         }
+        else {
+            mbp(force_elim, vars, model, fmls, defs);
+            TRACE("qe", tout << "mbp " << vars << " " << fmls << "\n";
+                  if (defs) { tout << "defs: "; for (auto const& d : *defs) tout << d << "\n"; tout << "\n";});
+        }
+    }
 
     void mbp(bool force_elim, app_ref_vector& vars, model& model, expr_ref_vector& fmls, vector<mbp::def>* defs) {
         SASSERT(validate_model(model, fmls));
@@ -444,9 +449,12 @@ public:
         app_ref var(m);
         expr_ref_vector unused_fmls(m);
         bool progress = true;
-        preprocess_solve(model, vars, fmls);
+        TRACE("qe", tout << "eliminate vars: " << vars << "fmls: " << fmls << "\n");
+        if (!defs)
+            preprocess_solve(model, vars, fmls);
         filter_variables(model, vars, fmls, unused_fmls);
         project_bools(model, vars, fmls);
+        TRACE("qe", tout << "eliminate vars: " << vars << "\nfmls: " << fmls << "\nunused: " << unused_fmls <<"\n");
         while (progress && !vars.empty() && !fmls.empty() && m.limit().inc()) {
             app_ref_vector new_vars(m);
             progress = false;
@@ -455,10 +463,12 @@ public:
                     unsigned sz = defs->size();
                     p->project(model, vars, fmls, *defs);
                     progress |= sz < defs->size();
+                    TRACE("qe", tout << "after project " << m.get_family_name(p->get_family_id()) << ": " << vars << "\n");
                 }
                 else if (p)
                     (*p)(model, vars, fmls);
             }
+            TRACE("qe", tout << "projecting " << vars << "\n");
             while (!vars.empty() && !fmls.empty() && !defs && m.limit().inc()) {
                 var = vars.back();
                 vars.pop_back();
@@ -491,16 +501,17 @@ public:
             if (!m.limit().inc())
                 return;
             vars.append(new_vars);
-            if (progress) {
+            if (progress && !defs) 
                 preprocess_solve(model, vars, fmls);
-            }
+            TRACE("qe", tout << "looping " << vars << "\n");
+            
         }
         if (fmls.empty()) {
             vars.reset();
         }
         fmls.append(unused_fmls);
         SASSERT(validate_model(model, fmls));
-        TRACE("qe", tout << vars << " " << fmls << "\n";);
+        TRACE("qe", tout << "vars: " << vars << "\nfmls: " << fmls << "\n";);
     }
 
     void do_qe_lite(app_ref_vector& vars, expr_ref& fml) {
@@ -529,16 +540,16 @@ public:
         fml = mk_and(fmls);
     }
 
-  void qel_project(app_ref_vector &vars, model &mdl, expr_ref &fml, bool reduce_all_selects) {
-      flatten_and(fml);
-      mbp::mbp_qel mbptg(m, m_params);
-      mbptg(vars, fml, mdl);
-      if (reduce_all_selects) rewrite_read_over_write(fml, mdl, fml);
-      m_rw(fml);
-      TRACE("qe", tout << "After mbp_tg:\n"
-            << fml << " models " << mdl.is_true(fml) << "\n"
-            << "Vars: " << vars << "\n";);
-  }
+    void qel_project(app_ref_vector &vars, model &mdl, expr_ref &fml, bool reduce_all_selects) {
+        flatten_and(fml);
+        mbp::mbp_qel mbptg(m, m_params);
+        mbptg(vars, fml, mdl);
+        if (reduce_all_selects) rewrite_read_over_write(fml, mdl, fml);
+        m_rw(fml);
+        TRACE("qe", tout << "After mbp_tg:\n"
+              << fml << " models " << mdl.is_true(fml) << "\n"
+              << "Vars: " << vars << "\n";);
+    }
 
     void spacer_qel(app_ref_vector& vars, model& mdl, expr_ref& fml) {
         TRACE("qe", tout << "Before projection:\n" << fml << "\n" << "Vars: " << vars << "\n";);
@@ -600,12 +611,11 @@ public:
     }
 
     void spacer(app_ref_vector& vars, model& mdl, expr_ref& fml) {
-        if (m_use_qel) {
+        TRACE("qe", tout << "spacer " << m_use_qel << " " << fml << " " << vars << "\n");
+        if (m_use_qel) 
             spacer_qel(vars, mdl, fml);
-        }
-        else {
+        else 
             spacer_qe_lite(vars, mdl, fml);
-        }
     }
 
     void spacer_qe_lite(app_ref_vector& vars, model& mdl, expr_ref& fml) {