From 996012adb144e2cbafbb80c31e3d9e12a446dd9f Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Thu, 17 Aug 2023 17:32:08 +0200
Subject: [PATCH] logging fix

---
 src/math/polysat/inference_logger.cpp | 8 ++++++--
 src/math/polysat/inference_logger.h   | 1 +
 src/math/polysat/search_state.cpp     | 4 ++--
 3 files changed, 9 insertions(+), 4 deletions(-)

diff --git a/src/math/polysat/inference_logger.cpp b/src/math/polysat/inference_logger.cpp
index e1be4d6f1..ba2f3efd7 100644
--- a/src/math/polysat/inference_logger.cpp
+++ b/src/math/polysat/inference_logger.cpp
@@ -23,8 +23,13 @@ Notes:
 
 namespace polysat {
 
+    dummy_inference_logger::dummy_inference_logger() {
+        // LOG("created dummy_inference_logger");
+    }
+
     file_inference_logger::file_inference_logger(solver& s)
         : s(s) {
+        // LOG("created file_inference_logger");
     }
 
     std::ostream& file_inference_logger::out() {
@@ -102,7 +107,6 @@ namespace polysat {
     }
 
     void file_inference_logger::end_conflict() {
-        // search_state const& search, viable const& v
         out() << "\n" << hline() << "\n\n";
         out() << "Search state (part):\n";
         for (auto const& item : s.m_search)
@@ -110,7 +114,7 @@ namespace polysat {
                 out_indent() << search_item_pp(s.m_search, item, true) << "\n";
         out() << hline() << "\nViable (part):\n";
         for (pvar v : m_used_vars)
-            out_indent() << "v" << std::setw(3) << std::left << v << ": " << viable::var_pp(s.m_viable, v) << "\n";
+            out_indent() << "v" << rpad(3, v) << ": " << viable::var_pp(s.m_viable, v) << "\n";
         out() << "End CONFLICT #" << m_num_conflicts << "\n";
         out().flush();
         LOG("End CONFLICT #" << m_num_conflicts);
diff --git a/src/math/polysat/inference_logger.h b/src/math/polysat/inference_logger.h
index 6d97661c8..7e22e4080 100644
--- a/src/math/polysat/inference_logger.h
+++ b/src/math/polysat/inference_logger.h
@@ -77,6 +77,7 @@ namespace polysat {
 
     class dummy_inference_logger : public inference_logger {
     public:
+        dummy_inference_logger();
         virtual void begin_conflict(displayable const& header) override {}
         virtual void log(inference const& inf) override {}
         virtual void log_var(pvar v) override {}
diff --git a/src/math/polysat/search_state.cpp b/src/math/polysat/search_state.cpp
index 018e4777d..3a6a2711a 100644
--- a/src/math/polysat/search_state.cpp
+++ b/src/math/polysat/search_state.cpp
@@ -24,8 +24,8 @@ namespace polysat {
             pvar const var = item.var();
             rational const& val = s.m_value[var];
             auto const& j = s.m_justification[var];
-            out << "v" << std::setw(3) << std::left << var << " := ";
-            out << std::setw(30) << std::left << num_pp(s, var, val);
+            out << "v" << rpad(3, var) << " := ";
+            out << rpad(30, num_pp(s, var, val));
             out << " @" << j.level();
             switch (j.kind()) {
             case justification_k::decision: