From 51ce17bcd46f0f6bde9046bc5bf11a0c3c266bf5 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Sat, 8 Jul 2023 20:34:46 +0200
Subject: [PATCH] start using z3's egraph for slicing

---
 src/math/polysat/slicing.cpp | 22 ++++++++++++++++++++++
 src/math/polysat/slicing.h   | 11 ++++++++++-
 2 files changed, 32 insertions(+), 1 deletion(-)

diff --git a/src/math/polysat/slicing.cpp b/src/math/polysat/slicing.cpp
index 4dac35d23..533856cf8 100644
--- a/src/math/polysat/slicing.cpp
+++ b/src/math/polysat/slicing.cpp
@@ -46,6 +46,28 @@ Recycle the z3 egraph?
 
 namespace polysat {
 
+    slicing::slicing(solver& s):
+        m_solver(s),
+        m_egraph(m_ast)
+    {
+        m_slice_sort = m_ast.mk_uninterpreted_sort(symbol("slice"));
+    }
+
+    func_decl* slicing::get_concat_decl(unsigned arity) {
+        SASSERT(arity >= 2);
+        func_decl* decl = m_concat_decls.get(arity, nullptr);
+        if (!decl) {
+            ptr_vector<sort> domain;
+            for (unsigned i = arity; i-- > 0; )
+                domain.push_back(m_slice_sort);
+            SASSERT_EQ(arity, domain.size());
+            // TODO: mk_fresh_func_decl("concat", ...) if overload doesn't work
+            func_decl* decl = m_ast.mk_func_decl(symbol("slice-concat"), arity, domain.data(), m_slice_sort);
+            m_concat_decls.setx(arity, decl, nullptr);
+        }
+        return decl;
+    }
+
     void slicing::push_scope() {
         m_scopes.push_back(m_trail.size());
     }
diff --git a/src/math/polysat/slicing.h b/src/math/polysat/slicing.h
index 9f104fc73..ed8d6a633 100644
--- a/src/math/polysat/slicing.h
+++ b/src/math/polysat/slicing.h
@@ -24,6 +24,7 @@ Notation:
 
 --*/
 #pragma once
+#include "ast/euf/euf_egraph.h"
 #include "math/polysat/types.h"
 #include "math/polysat/constraint.h"
 #include <optional>
@@ -38,6 +39,14 @@ namespace polysat {
 
         solver&     m_solver;
 
+        ast_manager m_ast;
+        euf::egraph m_egraph;
+
+        sort*                   m_slice_sort;
+        ptr_vector<func_decl>   m_concat_decls;
+
+        func_decl* get_concat_decl(unsigned arity);
+
         using dep_t = sat::literal;
         using dep_vector = sat::literal_vector;
         static constexpr sat::literal null_dep = sat::null_literal;
@@ -214,7 +223,7 @@ namespace polysat {
         bool invariant() const;
 
     public:
-        slicing(solver& s): m_solver(s) {}
+        slicing(solver& s);
 
         void push_scope();
         void pop_scope(unsigned num_scopes = 1);