From 3f3ac924abceead01c1638c22dc8faef3137f29e Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 6 Feb 2024 09:48:09 -0800
Subject: [PATCH] add debugging output

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/sat/smt/polysat/viable.cpp | 16 +++++++++++++++-
 src/sat/smt/polysat/viable.h   |  3 +++
 src/sat/smt/polysat_egraph.cpp |  5 +++++
 3 files changed, 23 insertions(+), 1 deletion(-)

diff --git a/src/sat/smt/polysat/viable.cpp b/src/sat/smt/polysat/viable.cpp
index dc8f0e02e..758968c99 100644
--- a/src/sat/smt/polysat/viable.cpp
+++ b/src/sat/smt/polysat/viable.cpp
@@ -546,6 +546,18 @@ namespace polysat {
         return false;
     }
 
+
+    std::ostream& operator<<(std::ostream& out, viable::explain_t e) {
+        switch(e) {
+        case viable::explain_t::conflict: return out << "conflict";
+        case viable::explain_t::propagation: return out << "propagation";
+        case viable::explain_t::assignment: return out << "assignment";
+        case viable::explain_t::none: return out << "none";
+        default: UNREACHABLE();
+        }
+        return out;
+    }
+
     /*
     * Explain why the current variable is not viable or
     * or why it can only have a single value.
@@ -555,6 +567,8 @@ namespace polysat {
         auto last = m_explain.back();
         auto after = last;
 
+        verbose_stream() << m_explain_kind << "\n";
+
         if (c.inconsistent())
             verbose_stream() << "inconsistent explain\n";
         TRACE("bv", display_explain(tout));
@@ -631,7 +645,7 @@ namespace polysat {
         return result;
     }
 
-    dependency viable::propagate_from_containing_slice(entry* e, rational const& value, dependency_vector const& e_deps) {
+    dependency viable::propagate_from_containing_slice(entry* e, rational const& value, dependency_vector const& e_deps) {        
         for (auto const& slice : m_overlaps)
             if (auto d = propagate_from_containing_slice(e, value, e_deps, slice); !d.is_null())
                 return d;
diff --git a/src/sat/smt/polysat/viable.h b/src/sat/smt/polysat/viable.h
index 2fc77eee6..cf95b0a9d 100644
--- a/src/sat/smt/polysat/viable.h
+++ b/src/sat/smt/polysat/viable.h
@@ -145,6 +145,9 @@ namespace polysat {
             assignment,
             none
         };
+
+        friend std::ostream& operator<<(std::ostream& out, explain_t e);
+
         pvar            m_var = null_var;
         explain_t       m_explain_kind = explain_t::none;
         unsigned        m_num_bits = 0;
diff --git a/src/sat/smt/polysat_egraph.cpp b/src/sat/smt/polysat_egraph.cpp
index b0d97d56c..5c14aa752 100644
--- a/src/sat/smt/polysat_egraph.cpp
+++ b/src/sat/smt/polysat_egraph.cpp
@@ -124,6 +124,11 @@ namespace polysat {
         euf::theory_var v = m_pddvar2var[pv];
         expr_ref val(bv.mk_numeral(slice.value, slice.length), m);
         euf::enode* b = ctx.get_egraph().find(val);
+        if (!b) {
+            verbose_stream() << v << " " << val << "\n";
+            ctx.get_egraph().display(verbose_stream());
+        }
+
         SASSERT(b);
         m_bv_plugin->explain_slice(var2enode(v), slice.offset, b, consume_eq);
     }