From 4312611bd66dd7cdc1bdd2a14ef639d3a407bcc2 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Fri, 23 Sep 2022 15:58:44 +0200
Subject: [PATCH] nicer lit_pp

---
 src/math/polysat/log_helper.h | 69 +++++++++++++++++++++++++++--------
 src/math/polysat/solver.cpp   | 21 ++++++++---
 2 files changed, 69 insertions(+), 21 deletions(-)

diff --git a/src/math/polysat/log_helper.h b/src/math/polysat/log_helper.h
index 1eb9470da..359243618 100644
--- a/src/math/polysat/log_helper.h
+++ b/src/math/polysat/log_helper.h
@@ -46,23 +46,62 @@ show_deref_t<T> show_deref(Ptr const& ptr) {
     return show_deref_t<T>{ptr.get()};
 }
 
+
+template <typename T>
+struct repeat {
+    unsigned count;
+    T const& obj;
+    repeat(unsigned count, T const& obj): count(count), obj(obj) {}
+};
+
+template <typename T>
+std::ostream& operator<<(std::ostream& out, repeat<T> const& r) {
+    for (unsigned i = r.count; i-- > 0; ) {
+        out << r.obj;
+    }
+    return out;
+}
+
+enum class pad_direction {
+    left,
+    right,
+};
+
+template <typename T>
+struct pad {
+    pad_direction dir;
+    unsigned width;
+    T const& obj;
+    pad(pad_direction dir, unsigned width, T const& obj): dir(dir), width(width), obj(obj) {}
+};
+
+template <typename T>
+std::ostream& operator<<(std::ostream& out, pad<T> const& p) {
+    std::stringstream tmp;
+    tmp << p.obj;
+    std::string s = tmp.str();
+    unsigned n = (s.length() < p.width) ? (p.width - s.length()) : 0;
+    switch (p.dir) {
+    case pad_direction::left:
+        out << repeat(n, ' ') << s;
+        break;
+    case pad_direction::right:
+        out << s << repeat(n, ' ');
+        break;
+    }
+    return out;
+}
+
 /// Fill with spaces to the right:
 /// out << rpad(8, "hello")
 /// writes "hello   ".
 template <typename T>
-struct rpad {
-    unsigned width;
-    T const& obj;
-    rpad(unsigned width, T const& obj): width(width), obj(obj) {}
-};
-
-template <typename T>
-std::ostream& operator<<(std::ostream& out, rpad<T> const& pad) {
-    std::stringstream tmp;
-    tmp << pad.obj;
-    auto s = tmp.str();
-    out << s;
-    if (s.length() < pad.width)
-        out << std::string(pad.width - s.length(), ' ');
-    return out;
+pad<T> rpad(unsigned width, T const& obj) {
+    return pad<T>(pad_direction::right, width, obj);
+}
+
+/// Fill with spaces to the left.
+template <typename T>
+pad<T> lpad(unsigned width, T const& obj) {
+    return pad<T>(pad_direction::left, width, obj);
 }
diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index e04f65993..5e82f50c0 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -994,12 +994,21 @@ namespace polysat {
 
     std::ostream& lit_pp::display(std::ostream& out) const {
         auto c = s.lit2cnstr(lit);
-        out << lit << ": " << c << "  [";
-        out << " bvalue=" << s.m_bvars.value(lit);
-        if (s.m_bvars.is_assigned(lit))
-            out << " @" << s.m_bvars.level(lit);
-        out << " pwatched=" << c->is_pwatched();
-        out << "  ]";
+        out << lpad(4, lit) << ": " << rpad(30, c) << "  [";
+        out << " " << s.m_bvars.value(lit);
+        if (s.m_bvars.is_assigned(lit)) {
+            out << ' ';
+            if (s.m_bvars.is_assumption(lit))
+                out << "assert";
+            else if (s.m_bvars.is_bool_propagation(lit))
+                out << "bprop";
+            else if (s.m_bvars.is_value_propagation(lit))
+                out << "eval";
+            out << '@' << s.m_bvars.level(lit);
+        }
+        if (c->is_pwatched())
+            out << " pwatched";
+        out << " ]";
         return out;
     }