From 0d3e88fd311975a141359f28246791cfd99439f0 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Thu, 28 Mar 2024 16:38:41 +0100
Subject: [PATCH] display_explain

---
 src/sat/smt/polysat/viable.cpp | 8 ++++++--
 src/sat/smt/polysat/viable.h   | 1 +
 2 files changed, 7 insertions(+), 2 deletions(-)

diff --git a/src/sat/smt/polysat/viable.cpp b/src/sat/smt/polysat/viable.cpp
index dedaa53be..23d34706e 100644
--- a/src/sat/smt/polysat/viable.cpp
+++ b/src/sat/smt/polysat/viable.cpp
@@ -1208,11 +1208,15 @@ namespace polysat {
         out << "explain_kind " << m_explain_kind << "\n";
         display_state(out);
         for (auto const& e : m_explain)
-            display_one(out << "v" << m_var << "[" << e.e->bit_width << "] := " << e.value << " ", e.e) << "\n";
+            display_explain(out, e) << "\n";
         return out;
     }
 
-      /*
+    std::ostream& viable::display_explain(std::ostream& out, explanation const& e) const {
+        return display_one(out << "v" << e.e->var << "[" << e.e->bit_width << "] := " << e.value << " ", e.e);
+    }
+
+    /*
      * Lower bounds are strictly ascending.
      * Intervals don't contain each-other (since lower bounds are ascending, it suffices to check containment in one direction).
      */
diff --git a/src/sat/smt/polysat/viable.h b/src/sat/smt/polysat/viable.h
index 18ea430b3..451bd35ba 100644
--- a/src/sat/smt/polysat/viable.h
+++ b/src/sat/smt/polysat/viable.h
@@ -153,6 +153,7 @@ namespace polysat {
         void init_overlaps(pvar v);
         std::ostream& display_state(std::ostream& out) const;
         std::ostream& display_explain(std::ostream& out) const;
+        std::ostream& display_explain(std::ostream& out, explanation const& e) const;
 
     public:
         viable(core& c);