From 80cc45c5c14e978fd121c7049861162d986955fe Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 8 Jul 2020 13:32:41 -0700
Subject: [PATCH] display justifications compactly for tracing #4575

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/ast.h              |  6 ++++++
 src/smt/smt_context.h      |  2 ++
 src/smt/smt_context_pp.cpp | 31 ++++++++++++++++++++++++++++++-
 3 files changed, 38 insertions(+), 1 deletion(-)

diff --git a/src/ast/ast.h b/src/ast/ast.h
index 6fdbb2902..22f627fb1 100644
--- a/src/ast/ast.h
+++ b/src/ast/ast.h
@@ -1572,6 +1572,12 @@ public:
 
     bool has_trace_stream() const { return m_trace_stream != nullptr; }
     std::ostream & trace_stream() { SASSERT(has_trace_stream()); return *m_trace_stream; }
+    struct suspend_trace {
+        ast_manager& m;
+        std::fstream* m_tr;
+        suspend_trace(ast_manager& m): m(m), m_tr(m.m_trace_stream) { m.m_trace_stream = nullptr; }
+        ~suspend_trace() { m.m_trace_stream = m_tr; }
+    };
 
     void enable_int_real_coercions(bool f) { m_int_real_coercions = f; }
     bool int_real_coercions() const { return m_int_real_coercions; }
diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index efa40e3f6..dac44365f 100644
--- a/src/smt/smt_context.h
+++ b/src/smt/smt_context.h
@@ -1406,6 +1406,8 @@ namespace smt {
 
         std::ostream& display(std::ostream& out, b_justification j) const;
 
+        std::ostream& display_compact_j(std::ostream& out, b_justification j) const;
+
         // -----------------------------------
         //
         // Debugging support
diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp
index 9f318620e..92d9c09a2 100644
--- a/src/smt/smt_context_pp.cpp
+++ b/src/smt/smt_context_pp.cpp
@@ -618,15 +618,44 @@ namespace smt {
         return out << "\n";
     }
 
+    std::ostream& context::display_compact_j(std::ostream& out, b_justification j) const {
+        switch (j.get_kind()) {
+        case b_justification::AXIOM:
+            out << "axiom";
+            break;
+        case b_justification::BIN_CLAUSE: 
+            out << "bin " << j.get_literal();
+            break;
+        case b_justification::CLAUSE: {
+            clause * cls = j.get_clause();
+            out << "clause ";
+            if (cls) out << literal_vector(cls->get_num_literals(), cls->begin());
+            break;
+        }
+        case b_justification::JUSTIFICATION: {
+            literal_vector lits;
+            const_cast<conflict_resolution&>(*m_conflict_resolution).justification2literals(j.get_justification(), lits);
+            out << "justification " << j.get_justification()->get_from_theory() << ": ";
+            out << lits;
+            break;
+        }
+        default:
+            UNREACHABLE();
+            break;
+        }
+        return out << "\n";
+    }
+
     void context::trace_assign(literal l, b_justification j, bool decision) const {
         SASSERT(m.has_trace_stream());
         std::ostream & out = m.trace_stream();
+        ast_manager::suspend_trace _st(m);
         out << "[assign] ";
         display_literal(out, l);
         if (decision)
             out << " decision";
         out << " ";
-        display(out, j);
+        display_compact_j(out, j);
     }
 
     std::ostream& operator<<(std::ostream& out, enode_pp const& p) {