From 5fdf300557d72d1c2df6fa724d93fb327dfd7df3 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 14 Oct 2024 17:55:52 -0700
Subject: [PATCH] adding dt plugin

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/sls/CMakeLists.txt          |  1 +
 src/ast/sls/sls_datatype_plugin.cpp | 54 ++++++++++++++++++++++++++
 src/ast/sls/sls_datatype_plugin.h   | 59 +++++++++++++++++++++++++++++
 3 files changed, 114 insertions(+)
 create mode 100644 src/ast/sls/sls_datatype_plugin.cpp
 create mode 100644 src/ast/sls/sls_datatype_plugin.h

diff --git a/src/ast/sls/CMakeLists.txt b/src/ast/sls/CMakeLists.txt
index 519497e9f..8961b535b 100644
--- a/src/ast/sls/CMakeLists.txt
+++ b/src/ast/sls/CMakeLists.txt
@@ -13,6 +13,7 @@ z3_add_component(ast_sls
     sls_bv_terms.cpp
     sls_bv_valuation.cpp
     sls_context.cpp
+    sls_datatype_plugin.cpp
     sls_euf_plugin.cpp
     sls_smt_solver.cpp
   COMPONENT_DEPENDENCIES
diff --git a/src/ast/sls/sls_datatype_plugin.cpp b/src/ast/sls/sls_datatype_plugin.cpp
new file mode 100644
index 000000000..01c718996
--- /dev/null
+++ b/src/ast/sls/sls_datatype_plugin.cpp
@@ -0,0 +1,54 @@
+/*++
+Copyright (c) 2024 Microsoft Corporation
+
+Module Name:
+
+    sls_datatype_plugin.cpp
+
+Abstract:
+
+    Algebraic Datatypes for SLS
+    
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2024-10-14
+    
+--*/
+#pragma once
+
+#include "ast/sls/sls_datatype_plugin.h"
+
+namespace sls {
+    
+    datatype_plugin::datatype_plugin(context& c):
+        plugin(c),
+        m_dt(m) {
+        m_fid = m_dt.get_family_id();
+    }
+    
+    datatype_plugin::~datatype_plugin() {}
+
+    void datatype_plugin::add_axioms() {
+        for (auto t : ctx.subterms()) {
+            auto s = t->get_sort();
+            if (!m_dt.is_datatype(s))
+                continue;
+        }
+    }
+
+    expr_ref datatype_plugin::get_value(expr* e) { return expr_ref(m); }
+    void datatype_plugin::initialize() {}
+    void datatype_plugin::start_propagation() {}
+    void datatype_plugin::propagate_literal(sat::literal lit) {}
+    bool datatype_plugin::propagate() { return false; }       
+    bool datatype_plugin::is_sat() { return true; }
+    void datatype_plugin::register_term(expr* e) {}
+    std::ostream& datatype_plugin::display(std::ostream& out) const {
+        return out;
+    }
+    void datatype_plugin::mk_model(model& mdl) {}
+        
+    void datatype_plugin::collect_statistics(statistics& st) const {}
+    void datatype_plugin::reset_statistics() {}
+    
+}
diff --git a/src/ast/sls/sls_datatype_plugin.h b/src/ast/sls/sls_datatype_plugin.h
new file mode 100644
index 000000000..d7359a1c8
--- /dev/null
+++ b/src/ast/sls/sls_datatype_plugin.h
@@ -0,0 +1,59 @@
+/*++
+Copyright (c) 2024 Microsoft Corporation
+
+Module Name:
+
+    sls_datatype_plugin.h
+
+Abstract:
+
+    Algebraic Datatypes for SLS
+    
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2024-10-14
+    
+--*/
+#pragma once
+
+#include "ast/sls/sls_context.h"
+#include "ast/datatype_decl_plugin.h"
+
+namespace sls {
+    
+    class datatype_plugin : public plugin {
+        struct stats {
+            unsigned m_num_axioms = 0;
+            void reset() { memset(this, 0, sizeof(*this)); }
+        };
+        obj_map<sort, ptr_vector<expr>> m_dts;
+
+        datatype_util m_dt;
+        stats m_stats;
+
+        void add_axioms();
+
+    public:
+        datatype_plugin(context& c);
+        ~datatype_plugin() override;
+        family_id fid() { return m_fid; }
+        expr_ref get_value(expr* e) override;
+        void initialize() override;
+        void start_propagation() override;
+        void propagate_literal(sat::literal lit) override;
+        bool propagate() override;       
+        bool is_sat() override;
+        void register_term(expr* e) override;
+        std::ostream& display(std::ostream& out) const override;
+        void mk_model(model& mdl) override;
+        bool set_value(expr* e, expr* v) override { return false; }
+
+        void repair_up(app* e) override {}
+        bool repair_down(app* e) override { return false; }
+        void repair_literal(sat::literal lit) override {}
+
+        void collect_statistics(statistics& st) const override;
+        void reset_statistics() override;
+    };
+    
+}