From 98dca454ae80ce40e4343824ae0cb89c7cbd3066 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Wed, 3 Apr 2019 16:02:36 -0700
Subject: [PATCH] debug var_eqs

---
 src/util/lp/var_eqs.cpp | 16 ++++++++++++++++
 src/util/lp/var_eqs.h   | 10 ++++++++++
 2 files changed, 26 insertions(+)

diff --git a/src/util/lp/var_eqs.cpp b/src/util/lp/var_eqs.cpp
index 273e47b3b..60167d523 100644
--- a/src/util/lp/var_eqs.cpp
+++ b/src/util/lp/var_eqs.cpp
@@ -91,6 +91,7 @@ namespace nla {
                     f.m_index = i + 1;
                     m_todo.push_back(dfs_frame(jv.m_var, 0));
                     m_dfs_trail.push_back(jv.m_j);
+                    m_marked_trail.push_back(jv.m_var.index());
                     m_marked[jv.m_var.index()] = true;
                 }
             }
@@ -111,4 +112,19 @@ namespace nla {
         m_marked_trail.reset();
     }
 
+
+    std::ostream& var_eqs::display(std::ostream& out) const {
+        m_uf.display(out);
+        unsigned idx = 0;
+        for (auto const& edges : m_eqs) {
+            out << signed_var(idx, from_index()) << ": ";
+            for (auto const& jv : edges) {
+                out << jv.m_var << " ";
+            }
+            out << "\n";
+            ++idx;
+        }
+        return out;
+    }
+
 }
diff --git a/src/util/lp/var_eqs.h b/src/util/lp/var_eqs.h
index 32cc45cd0..d1882914d 100644
--- a/src/util/lp/var_eqs.h
+++ b/src/util/lp/var_eqs.h
@@ -50,8 +50,16 @@ public:
         return m_sv != other.m_sv;
     }
     rational rsign() const { return sign() ? rational::minus_one() : rational::one(); }
+
+    std::ostream& display(std::ostream& out) const {
+        return out << (sign()?"-":"") << var();
+    }
 };
 
+    inline std::ostream& operator<<(std::ostream& out, signed_var const& sv) {
+        return sv.display(out);
+    }
+
 class eq_justification {
     lpci m_cs[4];
 public:
@@ -177,5 +185,7 @@ public:
     eq_class equiv_class(signed_var v) { return eq_class(*this, v); }
 
     eq_class equiv_class(lpvar v) { return equiv_class(signed_var(v, false)); }
+
+    std::ostream& display(std::ostream& out) const;
 }; 
 }