From 0900ea8f7219e32ff4b8ac5c1379a32f09611e9e Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 8 Dec 2022 07:32:52 -0800
Subject: [PATCH] updated display

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/sat/smt/xor_gaussian.cpp | 22 +++++++++++++---------
 src/sat/smt/xor_gaussian.h   |  6 ++----
 2 files changed, 15 insertions(+), 13 deletions(-)

diff --git a/src/sat/smt/xor_gaussian.cpp b/src/sat/smt/xor_gaussian.cpp
index 158a55d02..ed4f91d7c 100644
--- a/src/sat/smt/xor_gaussian.cpp
+++ b/src/sat/smt/xor_gaussian.cpp
@@ -359,28 +359,32 @@ bool EGaussian::full_init(bool& created) {
 }
 
 std::ostream& PackedMatrix::display_dense(std::ostream& out) const {
-    for (unsigned rowIdx = 0; rowIdx < num_rows(); rowIdx++) {
-        const PackedRow& row = (*this)[rowIdx];
-        for(int i = 0; i < row.get_size() * 64; i++) 
+    unsigned rowIdx = 0;
+    for (auto const& row : *this) {
+        for (int i = 0; i < row.get_size() * 64; i++) 
             out << (int)row[i];
         out << " -- rhs: " << row.rhs() << " -- row: " << rowIdx << "\n";
+        ++rowIdx;
     }
     return out;
 }
 
-std::ostream& PackedMatrix::display_sparse(std::ostream& out) const {
-    for (auto const& row : *this) {
+std::ostream& EGaussian::display(std::ostream& out) const {
+    for (auto const& row : m_mat) {
         bool first = true;
         for (int i = 0; i < row.get_size() * 64; ++i) {
             if (row[i]) {
+                if (first)
+                    out << "(x";
+                int v = m_column_to_var[i];
                 if (first && !row.rhs())
-                    out << -i-1 << " ";
-                else
-                    out << i+1 << " ";
+                    v = -v;
+                out << " " << v;
                 first = false;
             }
         }
-        out << "\n";
+        if (!first)
+            out << ")";
     }
     return out;
 }
diff --git a/src/sat/smt/xor_gaussian.h b/src/sat/smt/xor_gaussian.h
index bacb5bc54..570c0c0a6 100644
--- a/src/sat/smt/xor_gaussian.h
+++ b/src/sat/smt/xor_gaussian.h
@@ -547,9 +547,7 @@ namespace xr {
         }
 
         std::ostream& display_dense(std::ostream& out) const;
-        
-        std::ostream& display_sparse(std::ostream& out) const;
-        
+                
     private:
     
         int64_t* mp = nullptr;
@@ -614,7 +612,7 @@ namespace xr {
             out << std::endl;
         }
 
-        std::ostream& display(std::ostream& out) const { return m_mat.display_sparse(out); }
+        std::ostream& display(std::ostream& out) const;
     
     private:
         xr::solver& m_solver;   // original sat solver