From b4902f374ba6022d6b778eaed72e8059f1d119aa Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Fri, 18 Aug 2023 16:21:59 +0200
Subject: [PATCH] slicing equivalent vars + explain

---
 src/math/polysat/slicing.cpp | 34 ++++++++++++++++++++++++++++++++++
 src/math/polysat/slicing.h   | 10 ++++++++++
 2 files changed, 44 insertions(+)

diff --git a/src/math/polysat/slicing.cpp b/src/math/polysat/slicing.cpp
index be7771b91..377a80c21 100644
--- a/src/math/polysat/slicing.cpp
+++ b/src/math/polysat/slicing.cpp
@@ -625,6 +625,30 @@ namespace polysat {
         explain_equal(var2slice(x), var2slice(y), out_deps);
     }
 
+    void slicing::explain_equal(pvar x, pvar y, std::function<void(sat::literal)> const& on_lit) {
+        SASSERT(m_marked_lits.empty());
+        SASSERT(m_tmp_deps.empty());
+        explain_equal(x, y, m_tmp_deps);
+        for (void* dp : m_tmp_deps) {
+            dep_t const d = dep_t::decode(dp);
+            if (d.is_null())
+                continue;
+            if (d.is_lit()) {
+                sat::literal lit = d.lit();
+                if (m_marked_lits.contains(lit))
+                    continue;
+                m_marked_lits.insert(lit);
+                on_lit(d.lit());
+            }
+            else {
+                // equivalence between to variables cannot be due to value assignment
+                UNREACHABLE();
+            }
+        }
+        m_marked_lits.reset();
+        m_tmp_deps.reset();
+    }
+
     void slicing::explain(ptr_vector<void>& out_deps) {
         SASSERT(is_conflict());
         m_egraph.begin_explain();
@@ -1530,6 +1554,16 @@ namespace polysat {
         explain_value(n, on_lit, on_var);
     }
 
+    pvar_vector slicing::equivalent_vars(pvar v) const {
+        pvar_vector xs;
+        for (enode* n : euf::enode_class(var2slice(v))) {
+            pvar const x = slice2var(n);
+            if (x != null_var)
+                xs.push_back(x);
+        }
+        return xs;
+    }
+
     std::ostream& slicing::display(std::ostream& out) const {
         enode_vector base;
         for (pvar v = 0; v < m_var2slice.size(); ++v) {
diff --git a/src/math/polysat/slicing.h b/src/math/polysat/slicing.h
index fcb5d9e02..5c21d73d6 100644
--- a/src/math/polysat/slicing.h
+++ b/src/math/polysat/slicing.h
@@ -375,6 +375,16 @@ namespace polysat {
         void collect_fixed(pvar v, justified_fixed_bits_vector& out);
         void explain_fixed(enode* just, std::function<void(sat::literal)> const& on_lit, std::function<void(pvar)> const& on_var);
 
+        /**
+         * Collect variables that are equivalent to v (including v itself)
+         *
+         * NOTE: this might miss some variables that are equal due to equivalent base slices. With 'polysat.slicing.congruence=true' and after propagate(), it should return all equal variables.
+         */
+        pvar_vector equivalent_vars(pvar v) const;
+
+        /** Explain why variables x and y are equivalent */
+        void explain_equal(pvar x, pvar y, std::function<void(sat::literal)> const& on_lit);
+
         std::ostream& display(std::ostream& out) const;
         std::ostream& display_tree(std::ostream& out) const;
     };