From 3f9229a6989a405264f8ce4b623a8fefe3843e4f Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Fri, 29 Mar 2019 12:39:05 -0700
Subject: [PATCH] stop keying monomials by abs values

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/util/lp/nla_solver.cpp     | 49 ----------------------------------
 src/util/lp/vars_equivalence.h | 42 -----------------------------
 2 files changed, 91 deletions(-)

diff --git a/src/util/lp/nla_solver.cpp b/src/util/lp/nla_solver.cpp
index 45033d390..285b728d1 100644
--- a/src/util/lp/nla_solver.cpp
+++ b/src/util/lp/nla_solver.cpp
@@ -859,41 +859,6 @@ struct solver::imp {
         return true;
     }
 
-    void init_abs_val_table() {
-        // register those vars that a factors in a monomial
-        for (auto & p : m_monomials_containing_var) {
-            m_vars_equivalence.register_var_with_abs_val(p.first, vvr(p.first));
-        }
-        // register monomial vars too
-        for (auto & p : m_var_to_its_monomial) {
-            m_vars_equivalence.register_var_with_abs_val(p.first, vvr(p.first));
-        }
-    }
-
-    // replaces each var with its abs root and sorts the return vector
-    template <typename T>
-    unsigned_vector get_abs_key(const T& m) const {
-        unsigned_vector r;
-        for (unsigned j : m) {
-            r.push_back(m_vars_equivalence.get_abs_root_for_var(abs(vvr(j))));
-        }
-        std::sort(r.begin(), r.end());
-        return r;
-    }
-
-    // For each monomial m = m_monomials[i], where i is in m_to_refine,
-    // try adding the pair (get_abs_key(m), i) to map
-    std::unordered_map<unsigned_vector, unsigned, hash_svector> create_relevant_abs_keys() {
-        std::unordered_map<unsigned_vector, unsigned, hash_svector> r;
-        for (unsigned i : m_to_refine) {
-            unsigned_vector key = get_abs_key(m_monomials[i]);
-            if (contains(r, key))
-                continue;
-            r[key] = i;
-        }
-        return r;
-    }
-
     void basic_sign_lemma_model_based_one_mon(const monomial& m, int product_sign) {
         if (product_sign == 0) {
             TRACE("nla_solver_bl", tout << "zero product sign\n";);
@@ -909,9 +874,6 @@ struct solver::imp {
     }
     
     bool basic_sign_lemma_model_based() {
-        init_abs_val_table();        
-        std::unordered_map<unsigned_vector, unsigned, hash_svector> key_mons =
-            create_relevant_abs_keys();
         unsigned i = random() % m_to_refine.size();
         unsigned ii = i;
         do {
@@ -2239,17 +2201,6 @@ struct solver::imp {
         }
     }
     
-    vector<factor> factors_with_the_same_abs_val(const factor& c) const {
-        vector<factor> r;
-        std::unordered_set<lpvar> found_vars;
-        std::unordered_set<unsigned> found_rm;
-        TRACE("nla_solver", tout << "c = "; print_factor_with_vars(c, tout););
-        for (lpvar i :  m_vars_equivalence.get_vars_with_the_same_abs_val(vvr(c))) {
-            maybe_add_a_factor(i, c, found_vars, found_rm, r);
-        }
-        return r;
-    }
-    
     bool order_lemma_on_ac_explore(const rooted_mon& rm, const factorization& ac, unsigned k) {
         const factor c = ac[k];
         TRACE("nla_solver", tout << "c = "; print_factor_with_vars(c, tout); );
diff --git a/src/util/lp/vars_equivalence.h b/src/util/lp/vars_equivalence.h
index bbb19860d..6173a115b 100644
--- a/src/util/lp/vars_equivalence.h
+++ b/src/util/lp/vars_equivalence.h
@@ -64,7 +64,6 @@ struct vars_equivalence {
     // If m_tree[v] == -1 then the variable is a root.
     // if m_tree[v] is not equal to -1 then m_equivs[m_tree[v]] = (k, v) or (v, k), where k is the parent of v
     vector<equiv>                                 m_equivs;         // all equivalences extracted from constraints
-    std::unordered_map<rational, unsigned_vector> m_vars_by_abs_values;
     std::function<rational(lpvar)>                m_vvr;
     
 
@@ -74,16 +73,8 @@ struct vars_equivalence {
     void clear() {
         m_equivs.clear();
         m_tree.clear();
-        m_vars_by_abs_values.clear(); 
     }
 
-    const svector<lpvar>& get_vars_with_the_same_abs_val(const rational& v) const {
-        auto it = m_vars_by_abs_values.find(abs(v));
-        SASSERT (it != m_vars_by_abs_values.end());
-        TRACE("nla_solver", tout << "size of same_abs_vals = " << it->second.size(); );
-        return it->second; 
-    } 
-
     // j itself is also included
     svector<lpvar> eq_vars(lpvar j) const {
         svector<lpvar> r = path_to_root(j);
@@ -256,38 +247,5 @@ struct vars_equivalence {
             explain(j, exp);
     }
 
-    lpvar get_abs_root_for_var(const rational & v) const {
-        SASSERT(!v.is_neg());
-        lpvar j = *(m_vars_by_abs_values.find(v)->second.begin());
-        SASSERT(abs(m_vvr(j)) == v);
-        return j;
-    }
-
-    void register_var_with_abs_val(unsigned j, const rational& val) {
-        TRACE("nla_vars_eq", tout << "j = " << j;);
-        rational v = abs(val);
-        auto it = m_vars_by_abs_values.find(v);
-        if (it == m_vars_by_abs_values.end()) {
-            unsigned_vector uv;
-            uv.push_back(j);
-            m_vars_by_abs_values[v] = uv;
-        } else {
-            it->second.push_back(j);
-        }
-    }
-
-    vector<rational> get_sorted_abs_vals_from_mon(const monomial& m, int & sign) {
-        sign = 1;
-        vector<rational> abs_vals;
-        for (lpvar j : m) {
-            const rational v = m_vvr(j);
-            abs_vals.push_back(abs(v));
-            if (v.is_neg()) {
-                sign = -sign;
-            }
-        }
-        std::sort(abs_vals.begin(), abs_vals.end());
-        return abs_vals;
-    }
 }; // end of vars_equivalence
 }