From f61bf0843bda8e9e7022756e611090c79da2a9df Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Wed, 12 Jul 2023 15:46:40 +0200
Subject: [PATCH] display

---
 src/math/polysat/slicing.cpp | 49 ++++++++++++++++++++++--------------
 src/math/polysat/slicing.h   |  4 ++-
 src/test/slicing.cpp         |  8 +++---
 3 files changed, 38 insertions(+), 23 deletions(-)

diff --git a/src/math/polysat/slicing.cpp b/src/math/polysat/slicing.cpp
index 533856cf8..b7e870156 100644
--- a/src/math/polysat/slicing.cpp
+++ b/src/math/polysat/slicing.cpp
@@ -703,35 +703,46 @@ namespace polysat {
             base.reset();
             slice const vs = var2slice(v);
             find_base(vs, base);
-            // unsigned hi = width(var2slice(v)) - 1;
-            for (slice s : base) {
-                // unsigned w = width(s);
-                // unsigned lo = hi - w + 1;
-                // out << " s" << s << "_[" << hi << ":" << lo << "]";
-                // hi -= w;
+            for (slice s : base)
                 display(out << " ", s);
-            }
-            if (has_value(vs)) {
-                out << "        -- (val:" << get_value(vs) << ")";
-            }
+            // if (has_value(vs)) {
+            //     out << "        -- (val:" << get_value(vs) << ")";
+            // }
             out << "\n";
         }
-        for (pvar v = 0; v < m_var2slice.size(); ++v) {
-            out << "v" << v << ":";
-            slice const s = m_var2slice[v];
-        }
         return out;
     }
 
-    std::ostream& slicing::display_tree(std::ostream& out, char const* name, slice s) const {
-        // TODO
+    std::ostream& slicing::display_tree(std::ostream& out) const {
+        for (pvar v = 0; v < m_var2slice.size(); ++v) {
+            out << "v" << v << ":\n";
+            slice const s = var2slice(v);
+            display_tree(out, s, 4, width(s) - 1, 0);
+        }
+        return out;
+    }
+
+    std::ostream& slicing::display_tree(std::ostream& out, slice s, unsigned indent, unsigned hi, unsigned lo) const {
+        out << std::string(indent, ' ') << "[" << hi << ":" << lo << "]";
+        out << " id=" << s;
+        out << " w=" << width(s);
+        if (find(s) != s)
+            out << " root=" << find(s);
+        // if (has_value(s))
+        //     out << " value=" << get_value(s);
+        out << "\n";
+        if (has_sub(s)) {
+            unsigned cut = m_slice_cut[s];
+            display_tree(out, sub_hi(s), indent + 4, hi, cut + 1 + lo);
+            display_tree(out, sub_lo(s), indent + 4, cut + lo, lo);
+        }
+        return out;
     }
 
     std::ostream& slicing::display(std::ostream& out, slice s) const {
         out << "{id:" << s << ",w:" << width(s);
-        if (has_value(s)) {
-            out << ",val:" << get_value(s);
-        }
+        // if (has_value(s))
+        //     out << ",val:" << get_value(s);
         out << "}";
         return out;
     }
diff --git a/src/math/polysat/slicing.h b/src/math/polysat/slicing.h
index ed8d6a633..e86313d47 100644
--- a/src/math/polysat/slicing.h
+++ b/src/math/polysat/slicing.h
@@ -250,8 +250,10 @@ namespace polysat {
         void propagate(signed_constraint c);
 
         std::ostream& display(std::ostream& out) const;
-        std::ostream& display_tree(std::ostream& out, char const* name, slice s) const;
         std::ostream& display(std::ostream& out, slice s) const;
+
+        std::ostream& display_tree(std::ostream& out) const;
+        std::ostream& display_tree(std::ostream& out, slice s, unsigned indent, unsigned hi, unsigned lo) const;
     };
 
     inline std::ostream& operator<<(std::ostream& out, slicing const& s) { return s.display(out); }
diff --git a/src/test/slicing.cpp b/src/test/slicing.cpp
index 2a9535226..632122494 100644
--- a/src/test/slicing.cpp
+++ b/src/test/slicing.cpp
@@ -49,6 +49,8 @@ namespace polysat {
             sl.find_base(sl.var2slice(y), y_base);
             VERIFY(sl.merge(x_base, y_base, sat::literal(3)));
             std::cout << sl << "\n";
+
+            sl.display_tree(std::cout);
         }
 
         // x[7:3] = a
@@ -185,9 +187,9 @@ namespace polysat {
 void tst_slicing() {
     using namespace polysat;
     test_slicing::test1();
-    test_slicing::test2();
-    test_slicing::test3();
-    test_slicing::test4();
+    // test_slicing::test2();
+    // test_slicing::test3();
+    // test_slicing::test4();
     // test_slicing::test5();
     std::cout << "ok\n";
 }