From 1235621610c4bf82618b751b8253774c87069b06 Mon Sep 17 00:00:00 2001
From: Lev <levnach@hotmail.com>
Date: Tue, 29 Jan 2019 14:45:50 -0800
Subject: [PATCH] search for the sign lemma on the equivalence class of
 monomials

Signed-off-by: Lev <levnach@hotmail.com>
---
 src/util/lp/equiv_monomials.h | 114 ----------------------------------
 src/util/lp/nla_solver.cpp    |  11 ++--
 2 files changed, 5 insertions(+), 120 deletions(-)
 delete mode 100644 src/util/lp/equiv_monomials.h

diff --git a/src/util/lp/equiv_monomials.h b/src/util/lp/equiv_monomials.h
deleted file mode 100644
index 24eb280d0..000000000
--- a/src/util/lp/equiv_monomials.h
+++ /dev/null
@@ -1,114 +0,0 @@
-/*++
-  Copyright (c) 2017 Microsoft Corporation
-
-  Module Name:
-
-  <name>
-
-  Abstract:
-
-  <abstract>
-
-  Author:
-  Nikolaj Bjorner (nbjorner)
-  Lev Nachmanson (levnach)
-
-  Revision History:
-
-
-  --*/
-namespace nla {
-struct const_iterator_equiv_mon {
-    // fields
-    const vector<unsigned_vector>&                      m_eq_vars;
-    vector<unsigned_vector::const_iterator>             m_its;
-    bool                                                m_done;
-    std::function<unsigned (const unsigned_vector&)>    m_find_monomial;
-    // constructor for begin()
-    const_iterator_equiv_mon(const vector<unsigned_vector>& abs_vals,
-                             std::function<unsigned (const unsigned_vector&)> find_monomial)
-        : m_eq_vars(abs_vals),
-          m_done(false),
-          m_find_monomial(find_monomial) {
-        for (auto& vars: abs_vals){
-            m_its.push_back(vars.begin());
-        }
-    }
-    // constructor for end()
-    const_iterator_equiv_mon(const vector<unsigned_vector>& does_not_matter) : m_eq_vars(does_not_matter), m_done(true) {}
-        
-    //typedefs
-    typedef const_iterator_equiv_mon self_type;
-    typedef unsigned value_type;
-    typedef unsigned reference;
-    typedef int difference_type;
-    typedef std::forward_iterator_tag iterator_category;
-
-    void advance() {
-        if (m_done)
-            return;
-        unsigned k = 0;
-        for (; k < m_its.size(); k++) {
-            auto & it = m_its[k];
-            it++;
-            const auto & evars = m_eq_vars[k];
-            if (it == evars.end()) {
-                it = evars.begin();
-            } else {
-                break;
-            }
-        }
-            
-        if (k == m_its.size()) {
-            m_done = true;
-        }
-    }
-
-    unsigned_vector get_key() const {
-        unsigned_vector r;
-        for(const auto& it : m_its){
-            r.push_back(*it);
-        }
-        std::sort(r.begin(), r.end());
-        return r;
-    }
-        
-    self_type operator++() {self_type i = *this; operator++(1); return i;}
-    self_type operator++(int) { advance(); return *this; }
-
-    bool operator==(const self_type &other) const { return m_done == other.m_done;}
-    bool operator!=(const self_type &other) const { return ! (*this == other); }
-    reference operator*() const {
-        return m_find_monomial(get_key());
-    }
-};
-
-struct equiv_monomials {
-    const monomial &                                    m_mon;
-    std::function<unsigned_vector (lpvar)>              m_eq_vars;
-    std::function<unsigned (const unsigned_vector&)>    m_find_monomial;
-    vector<unsigned_vector>                             m_vars_eqs;
-    equiv_monomials(const monomial & m,
-                    std::function<unsigned_vector (lpvar)> eq_vars,
-                    std::function<unsigned (const unsigned_vector&)> find_monomial) :
-        m_mon(m),
-        m_eq_vars(eq_vars),
-        m_find_monomial(find_monomial),
-        m_vars_eqs(vars_eqs())
-    {}
-
-    vector<unsigned_vector> vars_eqs() const {
-        vector<unsigned_vector> r;
-        for(lpvar j : m_mon.vars()) {
-            r.push_back(m_eq_vars(j));
-        }
-        return r;
-    } 
-    const_iterator_equiv_mon begin() const {
-        return const_iterator_equiv_mon(m_vars_eqs, m_find_monomial);
-    }
-    const_iterator_equiv_mon end() const {
-        return const_iterator_equiv_mon(m_vars_eqs);
-    }
-};
-} // end of namespace nla
diff --git a/src/util/lp/nla_solver.cpp b/src/util/lp/nla_solver.cpp
index ce2a2c91f..99cecbc1c 100644
--- a/src/util/lp/nla_solver.cpp
+++ b/src/util/lp/nla_solver.cpp
@@ -24,7 +24,6 @@
 #include "util/lp/vars_equivalence.h"
 #include "util/lp/factorization.h"
 #include "util/lp/rooted_mons.h"
-#include "util/lp/equiv_monomials.h"
 namespace nla {
 
 typedef lp::lconstraint_kind llc;
@@ -639,12 +638,12 @@ struct solver::imp {
     bool basic_sign_lemma_on_mon(unsigned i){
         const monomial& m = m_monomials[i];
         TRACE("nla_solver", tout << "i = " << i << ", mon = "; print_monomial_with_vars(m, tout););
-        auto mons_to_explore = equiv_monomials(m,
-                                               [this](lpvar j) {return eq_vars(j);},
-                                               [this](const unsigned_vector& key) {return find_monomial(key);});
+        const index_with_sign&  rm_i_s = m_rm_table.get_rooted_mon(i);
+        const auto& mons_to_explore = m_rm_table.vec()[rm_i_s.index()].m_mons;
         
-        for (unsigned n : mons_to_explore) {
-            if (n == static_cast<unsigned>(-1) || n == i) continue;
+        for (index_with_sign i_s : mons_to_explore) {
+            unsigned n = i_s.index();
+            if (n == i) continue;
             if (basic_sign_lemma_on_two_monomials(m, m_monomials[n]))
                 return true;
         }