From ff0de59a704d9ed6abd817462999aa06a45850b4 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 15 Mar 2021 16:23:35 -0700
Subject: [PATCH] more streamlined diagnostics to prepare for #5106

---
 src/math/lp/lar_solver.cpp        | 9 +++++++++
 src/math/lp/lar_solver.h          | 2 ++
 src/sat/smt/arith_diagnostics.cpp | 8 +-------
 src/smt/theory_lra.cpp            | 8 +-------
 4 files changed, 13 insertions(+), 14 deletions(-)

diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp
index 6a799b1ff..61c0b3e5d 100644
--- a/src/math/lp/lar_solver.cpp
+++ b/src/math/lp/lar_solver.cpp
@@ -1252,6 +1252,15 @@ namespace lp {
 
     // ********** print region start
 
+    std::ostream& lar_solver::display(std::ostream& out) const {
+        out << constraints();
+        print_terms(out);
+        pp(out).print();
+        for (unsigned j = 0; j < number_of_vars(); j++) 
+            print_column_info(j, out);
+        return out;
+    }
+
     std::ostream& lar_solver::print_terms(std::ostream& out) const {
         for (auto it : m_terms) {
             print_term(*it, out) << "\n";
diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h
index 420a41d16..452614caa 100644
--- a/src/math/lp/lar_solver.h
+++ b/src/math/lp/lar_solver.h
@@ -525,6 +525,8 @@ public:
     std::ostream& print_constraint_indices_only(const lar_base_constraint * c, std::ostream & out) const;
     std::ostream& print_implied_bound(const implied_bound& be, std::ostream & out) const;
     std::ostream& print_values(std::ostream& out) const;
+    std::ostream& display(std::ostream& out) const;
+
     bool init_model() const;
     mpq get_value(column_index const& j) const;
     mpq get_tv_value(tv const& t) const;
diff --git a/src/sat/smt/arith_diagnostics.cpp b/src/sat/smt/arith_diagnostics.cpp
index 735de4d75..770aeff98 100644
--- a/src/sat/smt/arith_diagnostics.cpp
+++ b/src/sat/smt/arith_diagnostics.cpp
@@ -23,13 +23,7 @@ namespace arith {
 
     
     std::ostream& solver::display(std::ostream& out) const { 
-            out << lp().constraints();
-            lp().print_terms(out);
-            // the tableau
-            lp().pp(out).print();
-            for (unsigned j = 0; j < lp().number_of_vars(); j++) {
-                lp().print_column_info(j, out);
-            }
+        lp().display(out);
         
         if (m_nla) {
             m_nla->display(out);
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index d050fcb77..87ca94e92 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -3659,13 +3659,7 @@ public:
 
     void display(std::ostream & out) {
         if (m_solver) {
-            out << lp().constraints();
-            lp().print_terms(out);
-            // the tableau
-            lp().pp(out).print();
-            for (unsigned j = 0; j < lp().number_of_vars(); j++) {
-                lp().print_column_info(j, out);
-            }
+            m_solver->display(out);
         }
         if (m_nla) {
             m_nla->display(out);