From c9bd8d59aca75218307801326b2c8ab6d68fc7c4 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 8 Sep 2024 19:26:51 -0700
Subject: [PATCH] Refactor handling of term registration and enhance distinct
 handling in sls_euf_plugin

---
 src/ast/sls/sls_context.cpp    |  3 +--
 src/ast/sls/sls_euf_plugin.cpp | 29 +++++++++++++++++++++++++++++
 2 files changed, 30 insertions(+), 2 deletions(-)

diff --git a/src/ast/sls/sls_context.cpp b/src/ast/sls/sls_context.cpp
index 610841087..6eb396fa5 100644
--- a/src/ast/sls/sls_context.cpp
+++ b/src/ast/sls/sls_context.cpp
@@ -446,6 +446,7 @@ namespace sls {
         auto visit = [&](expr* e) {
             m_allterms.setx(e->get_id(), e);
             ensure_plugin(e);
+            register_term(e);
         };
         if (is_visited(e))
             return;
@@ -468,7 +469,6 @@ namespace sls {
                     }
                     if (m.is_bool(e))
                         mk_literal(e);
-                    register_term(e);
                     visit(e);
                 }
                 else {
@@ -479,7 +479,6 @@ namespace sls {
             else {
                 expr_ref _e(e, m);
                 m_todo.pop_back();
-                register_term(e);
                 visit(e);
             }
         }
diff --git a/src/ast/sls/sls_euf_plugin.cpp b/src/ast/sls/sls_euf_plugin.cpp
index 2d36611ab..20a2c1a6a 100644
--- a/src/ast/sls/sls_euf_plugin.cpp
+++ b/src/ast/sls/sls_euf_plugin.cpp
@@ -227,8 +227,37 @@ namespace sls {
                 }
                 else
                     m_values.insert(t);
+           }
+        }
+
+        for (auto lit : ctx.root_literals()) {
+            if (!ctx.is_true(lit))
+                lit.neg();
+            auto e = ctx.atom(lit.var());
+            if (lit.sign() && e && m.is_distinct(e)) {
+                auto n = to_app(e)->get_num_args();
+                expr_ref_vector eqs(m);
+                for (unsigned i = 0; i < n; ++i) {
+                    auto arg = to_app(e)->get_arg(i);
+                    auto a = ctx.get_value(arg);
+                    for (unsigned j = i + 1; j < n; ++j) {
+                        auto argb = to_app(e)->get_arg(j);
+                        auto b = ctx.get_value(argb);
+                        if (a == b)
+                            goto done_distinct;
+                        eqs.push_back(m.mk_eq(arg, argb));
+                    }
+                }
+                // distinct(a, b, c) or a = b or a = c or b = c
+                eqs.push_back(e);
+                ctx.add_constraint(m.mk_or(eqs));
+                new_constraint = true;
+            done_distinct:
+                ;
             }
         }
+
+        
         return new_constraint;
     }