From a51239c641b5fdcef66c5c477e7721946dae3188 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 7 May 2025 15:57:47 -0700
Subject: [PATCH] update namespace, hoist exported functions outside of
 embedded namespace

---
 src/ast/euf/euf_mam.cpp  | 53 ++++++++++++++++++++--------------------
 src/ast/euf/euf_mam.h    |  5 ----
 src/sat/smt/q_ematch.cpp |  8 +++---
 src/sat/smt/q_ematch.h   |  2 +-
 4 files changed, 32 insertions(+), 36 deletions(-)

diff --git a/src/ast/euf/euf_mam.cpp b/src/ast/euf/euf_mam.cpp
index 7fb90cdc5..c4cb2d28c 100644
--- a/src/ast/euf/euf_mam.cpp
+++ b/src/ast/euf/euf_mam.cpp
@@ -60,7 +60,7 @@ Revision History:
 
 #define IS_CGR_SUPPORT true
 
-namespace q {
+namespace euf {
     // ------------------------------------
     //
     // Trail
@@ -3885,31 +3885,32 @@ namespace q {
         }
     };
 
-    void mam::ground_subterms(expr* e, ptr_vector<app>& ground) {
-        ground.reset();
-        expr_fast_mark1 mark;
-        ptr_buffer<app> todo;
-        if (is_app(e))
-            todo.push_back(to_app(e));
-        while (!todo.empty()) {
-            app * n = todo.back();
-            todo.pop_back();
-            if (mark.is_marked(n))
-                continue;
-            mark.mark(n);
-            if (n->is_ground()) 
-                ground.push_back(n);
-            else {
-                for (expr* arg : *n) 
-                    if (is_app(arg))
-                        todo.push_back(to_app(arg));
-            }
-        }
-    }
-
-    mam* mam::mk(euf::mam_solver& ctx, euf::on_binding_callback& em) {
-        return alloc(mam_impl, ctx, em, true);
-    }
 
 }
 
+
+void euf::mam::ground_subterms(expr* e, ptr_vector<app>& ground) {
+    ground.reset();
+    expr_fast_mark1 mark;
+    ptr_buffer<app> todo;
+    if (is_app(e))
+        todo.push_back(to_app(e));
+    while (!todo.empty()) {
+        app* n = todo.back();
+        todo.pop_back();
+        if (mark.is_marked(n))
+            continue;
+        mark.mark(n);
+        if (n->is_ground())
+            ground.push_back(n);
+        else {
+            for (expr* arg : *n)
+                if (is_app(arg))
+                    todo.push_back(to_app(arg));
+        }
+    }
+}
+
+euf::mam* euf::mam::mk(euf::mam_solver& ctx, euf::on_binding_callback& em) {
+    return alloc(mam_impl, ctx, em, true);
+}
\ No newline at end of file
diff --git a/src/ast/euf/euf_mam.h b/src/ast/euf/euf_mam.h
index 72d2f8f0e..c391f6c09 100644
--- a/src/ast/euf/euf_mam.h
+++ b/src/ast/euf/euf_mam.h
@@ -39,16 +39,11 @@ namespace euf {
         virtual ~on_binding_callback() = default;
         virtual void on_binding(quantifier* q, app* pat, euf::enode* const* binding, unsigned max_generation, unsigned min_gen, unsigned max_gen) = 0;
     };
-};
-
-namespace q {
 
     typedef euf::enode enode;
     typedef euf::egraph egraph;
     typedef euf::enode_vector enode_vector;
 
-    class ematch;
-
     /**
        \brief Matching Abstract Machine (MAM)
     */
diff --git a/src/sat/smt/q_ematch.cpp b/src/sat/smt/q_ematch.cpp
index e1a5ed175..f2988c9c2 100644
--- a/src/sat/smt/q_ematch.cpp
+++ b/src/sat/smt/q_ematch.cpp
@@ -76,7 +76,7 @@ namespace q {
             if (!ctx.relevancy_enabled())
                 ctx.get_egraph().set_on_make(_on_make);
         }
-        m_mam = mam::mk(ctx, *this);
+        m_mam = euf::mam::mk(ctx, *this);
     }
 
     void ematch::relevant_eh(euf::enode* n) {
@@ -85,7 +85,7 @@ namespace q {
     }
 
     void ematch::ensure_ground_enodes(expr* e) {
-        mam::ground_subterms(e, m_ground);
+        euf::mam::ground_subterms(e, m_ground);
         for (expr* g : m_ground) 
             m_qs.e_internalize(g);
     }
@@ -557,7 +557,7 @@ namespace q {
      * Attach ground subterms of patterns so they appear shared.
      */
     void ematch::attach_ground_pattern_terms(expr* pat) {
-        mam::ground_subterms(pat, m_ground);
+        euf::mam::ground_subterms(pat, m_ground);
         for (expr* g : m_ground) { 
             euf::enode* n = ctx.get_egraph().find(g);
             if (!n->is_attached_to(m_qs.get_id())) 
@@ -602,7 +602,7 @@ namespace q {
             if (!unary && j >= num_eager_multi_patterns) {
                 TRACE("q", tout << "delaying (too many multipatterns):\n" << mk_ismt2_pp(mp, m) << "\n";);
                 if (!m_lazy_mam)
-                    m_lazy_mam = mam::mk(ctx, *this);
+                    m_lazy_mam = euf::mam::mk(ctx, *this);
                 m_lazy_mam->add_pattern(q, mp);
             }
             else 
diff --git a/src/sat/smt/q_ematch.h b/src/sat/smt/q_ematch.h
index 5edefff05..40ad12200 100644
--- a/src/sat/smt/q_ematch.h
+++ b/src/sat/smt/q_ematch.h
@@ -75,7 +75,7 @@ namespace q {
         queue                         m_inst_queue;
         svector<prop>                 m_prop_queue;
         pattern_inference_rw          m_infer_patterns;
-        scoped_ptr<q::mam>            m_mam, m_lazy_mam;
+        scoped_ptr<euf::mam>          m_mam, m_lazy_mam;
         ptr_vector<clause>            m_clauses;
         obj_map<quantifier, unsigned> m_q2clauses;
         vector<unsigned_vector>       m_watch;     // expr_id -> clause-index*