From 0755b2b5f71b3743f516f260e3d48c67a16ce2af Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 16 Oct 2024 19:01:20 -0700
Subject: [PATCH] axiomatize dt

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/sls/sls_bv_eval.cpp         | 5 +++--
 src/ast/sls/sls_datatype_plugin.cpp | 8 +++++---
 2 files changed, 8 insertions(+), 5 deletions(-)

diff --git a/src/ast/sls/sls_bv_eval.cpp b/src/ast/sls/sls_bv_eval.cpp
index e2447e0f2..e6f8f8ab5 100644
--- a/src/ast/sls/sls_bv_eval.cpp
+++ b/src/ast/sls/sls_bv_eval.cpp
@@ -735,6 +735,7 @@ namespace sls {
                     a.set_mul(out, out, c.bits());
                 };
                 fold_oper(m_mul_tmp, e, i, f);
+                m_mul_tmp.set_bw(a.bw);
                 return try_repair_mul(assign_value(e), wval(e, i), m_mul_tmp);
             }
         case OP_BNOT:
@@ -907,7 +908,7 @@ namespace sls {
             auto& v = wval(e);
             v.get_variant(m_tmp, m_rand);
             auto d = lookahead(e, m_tmp);
-            verbose_stream() << mk_bounded_pp(e, m) << " " << d << "\n";
+            //verbose_stream() << mk_bounded_pp(e, m) << " " << d << "\n";
         }
         return false;
     }
@@ -1105,7 +1106,7 @@ namespace sls {
     * 8*e = a*(2b), then a = 4e*b^-1
     */
     bool bv_eval::try_repair_mul(bvect const& e, bvval& a, bvect const& b) {
-        //verbose_stream() << e << " := " << a << " * " << b << "\n";
+        // verbose_stream() << e << " := " << a << " * " << b << "\n";
         unsigned parity_e = a.parity(e);
         unsigned parity_b = a.parity(b);
 
diff --git a/src/ast/sls/sls_datatype_plugin.cpp b/src/ast/sls/sls_datatype_plugin.cpp
index babe33169..7d59225df 100644
--- a/src/ast/sls/sls_datatype_plugin.cpp
+++ b/src/ast/sls/sls_datatype_plugin.cpp
@@ -17,12 +17,14 @@ Notes:
 
 Eager reduction to EUF:
    is-c(c(t))                for each c(t) in T
-   f_i(c(t_i)) = t_i         for each c(..t_i..) in T
+   acc_i(c(t_i)) = t_i       for each c(..t_i..) in T
    is-c(t) => t = c(...acc_j(t)..) for each acc_j(t) in T
 
    sum_i is-c_i(t) = 1
    is-c(t) <=> c = t         for each 0-ary constructor c
 
+   is-c(t) <=> t = c(acc_1(t)..acc_n(t))
+
    s = acc(...(acc(t)) => s != t   if t is recursive
 
    or_i t = t_i              if t is a finite sort with terms t_i
@@ -238,7 +240,7 @@ namespace sls {
                     expr_ref_vector args(m);
                     for (auto a : acc)
                         args.push_back(m.mk_app(a, t));
-                    m_axioms.push_back(m.mk_implies(m.mk_app(r, t), m.mk_eq(t, m.mk_app(c, args))));
+                    m_axioms.push_back(m.mk_iff(m.mk_app(r, t), m.mk_eq(t, m.mk_app(c, args))));
                 }
 
                 //
@@ -456,7 +458,7 @@ namespace sls {
                     idx = todo.size() - 1;
                     if (con)
                         for (auto child : euf::enode_args(con))
-                            if (color.get(child->get_root_id(), white) == white && dt.is_datatype(child->get_expr()))
+                            if (color.get(child->get_root_id(), black) != black && dt.is_datatype(child->get_expr()))
                                 todo.push_back({ depth + 1, child, idx });
                     break;
                 }