From 6d5fd5d980f52062f48eb90bca93e807b65debd4 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Mon, 6 May 2019 12:14:27 -0700
Subject: [PATCH] getting rid of from_index_dummy

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/util/lp/nla_defs.h  |  2 +-
 src/util/lp/var_eqs.cpp |  4 ++--
 src/util/lp/var_eqs.h   | 10 ++++++----
 3 files changed, 9 insertions(+), 7 deletions(-)

diff --git a/src/util/lp/nla_defs.h b/src/util/lp/nla_defs.h
index 37c0085ed..aafe6de11 100644
--- a/src/util/lp/nla_defs.h
+++ b/src/util/lp/nla_defs.h
@@ -35,8 +35,8 @@ class signed_var {
 public:
     // constructor, sign = true means minus
     signed_var(lpvar v, bool sign): m_sv((v << 1) + (sign ? 1 : 0)) {}
+    explicit signed_var(unsigned sv) : m_sv(sv) {}
     // constructor
-    signed_var(unsigned sv, from_index_dummy): m_sv(sv) {}
     bool sign() const { return 0 != (m_sv & 0x1); }
     lpvar var() const { return m_sv >> 1; }
     unsigned index() const { return m_sv; }        
diff --git a/src/util/lp/var_eqs.cpp b/src/util/lp/var_eqs.cpp
index daec49ff3..31da7d92b 100644
--- a/src/util/lp/var_eqs.cpp
+++ b/src/util/lp/var_eqs.cpp
@@ -62,7 +62,7 @@ signed_var var_eqs::find(signed_var v) const {
         return v;
     }
     unsigned idx = m_uf.find(v.index());
-    return signed_var(idx, from_index_dummy());
+    return signed_var(idx);
 }
 
 void var_eqs::explain_dfs(signed_var v1, signed_var v2, lp::explanation& e) const {
@@ -174,7 +174,7 @@ std::ostream& var_eqs::display(std::ostream& out) const {
     unsigned idx = 0;
     for (auto const& edges : m_eqs) {
         if (!edges.empty()) {
-            auto v = signed_var(idx, from_index_dummy());
+            auto v = signed_var(idx);
             out << v << " root: " << find(v) << " : ";
             for (auto const& jv : edges) {
                 out << jv.m_var << " ";
diff --git a/src/util/lp/var_eqs.h b/src/util/lp/var_eqs.h
index 7f0ef16e4..71fb05688 100644
--- a/src/util/lp/var_eqs.h
+++ b/src/util/lp/var_eqs.h
@@ -161,7 +161,7 @@ public:
     public:
         iterator(var_eqs& ve, unsigned idx, bool t) : m_ve(ve), m_idx(idx), m_touched(t) {}
         signed_var operator*() const {
-            return signed_var(m_idx, from_index()); // 0 is needed to call the right constructor
+            return signed_var(m_idx);
         }
         iterator& operator++() { m_idx = m_ve.m_uf.next(m_idx); m_touched = true; return *this; }
         bool operator==(iterator const& other) const { return m_idx == other.m_idx && m_touched == other.m_touched; }
@@ -191,18 +191,20 @@ public:
 
     void unmerge_eh(unsigned i, unsigned j) { 
         if (m_merge_handler) {
-            m_merge_handler->unmerge_eh(signed_var(i, from_index_dummy()), signed_var(j, from_index_dummy())); 
+            m_merge_handler->unmerge_eh(signed_var(i), signed_var(j)); 
         }
     }
     void merge_eh(unsigned r2, unsigned r1, unsigned v2, unsigned v1) {
         if (m_merge_handler) {
-            m_merge_handler->merge_eh(signed_var(r2, from_index_dummy()), signed_var(r1, from_index_dummy()), signed_var(v2, from_index_dummy()), signed_var(v1, from_index_dummy())); 
+            m_merge_handler->merge_eh(signed_var(r2), signed_var(r1),
+                                      signed_var(v2), signed_var(v1)); 
         }
     }
 
     void after_merge_eh(unsigned r2, unsigned r1, unsigned v2, unsigned v1) {
         if (m_merge_handler) {
-            m_merge_handler->after_merge_eh(signed_var(r2, from_index_dummy()), signed_var(r1, from_index_dummy()), signed_var(v2, from_index_dummy()), signed_var(v1, from_index_dummy())); 
+            m_merge_handler->after_merge_eh(signed_var(r2), signed_var(r1),
+                                            signed_var(v2), signed_var(v1)); 
         }
     }