From 4203d954c6cb096f82d910b75902bedc4c66867e Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 17 Jun 2025 17:07:39 -0700
Subject: [PATCH] ematching skeleton

---
 src/ast/euf/euf_ematch.cpp | 26 ++++++++++++++++++++++++++
 src/ast/euf/euf_ematch.h   | 37 +++++++++++++++++++++++++++++++++++++
 2 files changed, 63 insertions(+)
 create mode 100644 src/ast/euf/euf_ematch.cpp
 create mode 100644 src/ast/euf/euf_ematch.h

diff --git a/src/ast/euf/euf_ematch.cpp b/src/ast/euf/euf_ematch.cpp
new file mode 100644
index 000000000..5b3917014
--- /dev/null
+++ b/src/ast/euf/euf_ematch.cpp
@@ -0,0 +1,26 @@
+/*++
+Copyright (c) 2023 Microsoft Corporation
+
+Module Name:
+
+    euf_match.cpp
+
+Abstract:
+
+    basic E-matching algorithm with SO support.
+    
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2025-6-16
+
+--*/
+
+#include "ast/euf/euf_ematch.h"
+
+namespace euf {
+
+
+    void ematch::operator()(expr* pat, enode* t, enode** binding) {
+    }
+
+}
diff --git a/src/ast/euf/euf_ematch.h b/src/ast/euf/euf_ematch.h
new file mode 100644
index 000000000..7f04512fb
--- /dev/null
+++ b/src/ast/euf/euf_ematch.h
@@ -0,0 +1,37 @@
+/*++
+Copyright (c) 2023 Microsoft Corporation
+
+Module Name:
+
+    euf_ematch.h
+
+Abstract:
+
+    basic E-matching algorithm with SO support.
+    
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2025-6-16
+
+--*/
+
+#pragma once
+
+#include "ast/euf/euf_egraph.h"
+
+namespace euf {
+
+    class ematch {
+    protected:
+        egraph& g;
+        std::ostream& display(std::ostream& out) const { return out; }
+        std::function<void(void)> m_on_match;
+    public:
+        ematch(egraph& g):
+            g(g)
+        {}
+
+        void operator()(expr* pat, enode* t, enode** binding) {}        
+            
+    };
+}