From 2d144cd7748d94dd95ef8fd1e72f310f98e4e3d3 Mon Sep 17 00:00:00 2001
From: Lev <levnach@hotmail.com>
Date: Wed, 21 Nov 2018 12:17:29 -0800
Subject: [PATCH] simplify m_monomials_by_abs_vals

Signed-off-by: Lev <levnach@hotmail.com>
---
 src/util/lp/nla_solver.cpp     | 39 +++++++++++++++++++++++++++-------
 src/util/lp/vars_equivalence.h | 17 ++++++---------
 2 files changed, 38 insertions(+), 18 deletions(-)

diff --git a/src/util/lp/nla_solver.cpp b/src/util/lp/nla_solver.cpp
index eb4f301c9..2a55438f2 100644
--- a/src/util/lp/nla_solver.cpp
+++ b/src/util/lp/nla_solver.cpp
@@ -344,16 +344,36 @@ struct solver::imp {
         mk_ineq(m_monomials[i].var(), -sign, m_monomials[k].var(), lp::lconstraint_kind::EQ);        
         TRACE("nla_solver", print_lemma(tout););
     }
+
+
+    static int rat_sign(const rational& r) {
+        return r.is_pos()? 1 : ( r.is_neg()? -1 : 0);
+    }
+
+    int vars_sign(const svector<lpvar>& v) {
+        int sign = 1;
+        for (lpvar j : v) {
+            sign *= rat_sign(vvr(j));
+            if (sign == 0) 
+                return 0;
+        }
+        return sign;
+    }
     
-    bool basic_sign_lemma_on_a_bucket_of_abs_vals(const vector<rational>& abs_vals, const vector<index_with_sign>& list){   
-        rational sign = list[0].m_sign;
-        rational val =  vvr(m_monomials[list[0].m_i].var());
+    
+    bool basic_sign_lemma_on_a_bucket_of_abs_vals(const vector<rational>& abs_vals, const unsigned_vector& list){
+        rational val =  vvr(m_monomials[list[0]].var());
+        int sign = vars_sign(m_monomials[list[0]].vars());
+        if (sign == 0) {
+            return false;
+        }
         
         for (unsigned i = 1; i < list.size(); i++) {
-            rational other_sign = list[i].m_sign;
-            rational other_val =  vvr(m_monomials[list[i].m_i].var());
-            if (val * sign != other_val * other_sign) {
-                generate_sign_lemma(abs_vals, list[0].m_i, list[i].m_i, sign * other_sign);
+            rational rsign = rational(vars_sign(m_monomials[list[i]].vars()) * sign);
+            SASSERT(!rsign.is_zero());
+            rational other_val =  vvr(m_monomials[list[i]].var());
+            if (val * rsign != other_val) {
+                generate_sign_lemma(abs_vals, list[0], list[i], rsign);
                 return true;
             }
         }
@@ -920,6 +940,7 @@ struct solver::imp {
                                                       unsigned i_bd_equiv,
                                                       unsigned i_bd,
                                                       unsigned d, unsigned i_ac, const factorization& ac, unsigned k) {
+        return false;
     }
         
 
@@ -931,6 +952,8 @@ struct solver::imp {
     bool order_lemma_on_factor_equiv_and_other_mon_eq(unsigned i_bd_equiv,
                                                      unsigned i_bd,
                                                      unsigned d, unsigned i_ac, const factorization& ac, unsigned k) {
+        return false;
+        /*
         TRACE("nla_solver", tout << "i_bd_equiv = "; print_monomial_with_vars(i_bd_equiv, tout); );
         rational abs_d = abs(vvr(d));
         for (unsigned k = 0; k < m_monomials[i_bd_equiv].size(); k++) {
@@ -947,7 +970,7 @@ struct solver::imp {
                     return true;
             }
         }
-        return false;
+        return false;*/
     }    
 
     
diff --git a/src/util/lp/vars_equivalence.h b/src/util/lp/vars_equivalence.h
index 54f8e825d..73bdfd2c5 100644
--- a/src/util/lp/vars_equivalence.h
+++ b/src/util/lp/vars_equivalence.h
@@ -82,9 +82,8 @@ struct vars_equivalence {
     vector<equiv>                                m_equivs;         // all equivalences extracted from constraints
     std::unordered_map<rational,unsigned_vector> m_vars_by_abs_values;
     std::unordered_map<vector<rational>,
-                       vector<index_with_sign>,
-                       hash_vector>
-                                                 m_monomials_by_abs_vals;
+                       unsigned_vector,
+                       hash_vector>              m_monomials_by_abs_vals;
 
     std::function<rational(lpvar)> m_vvr;
 
@@ -93,7 +92,7 @@ struct vars_equivalence {
     vars_equivalence(std::function<rational(lpvar)> vvr) : m_vvr(vvr) {}
     
     const std::unordered_map<vector<rational>,
-                       vector<index_with_sign>,
+                             unsigned_vector,
                              hash_vector>& monomials_by_abs_values() const {
         return m_monomials_by_abs_vals;
     }
@@ -223,7 +222,7 @@ struct vars_equivalence {
     void deregister_monomial_from_abs_vals(const monomial & m, unsigned i){
         int sign;
         auto key = get_sorted_abs_vals_from_mon(m, sign);
-        SASSERT(m_monomials_by_abs_vals.find(key)->second.back() == index_with_sign(i, rational(sign)));
+        SASSERT(m_monomials_by_abs_vals.find(key)->second.back() == i);
         m_monomials_by_abs_vals.find(key)->second.pop_back();
     }
 
@@ -244,17 +243,15 @@ struct vars_equivalence {
     void register_monomial_in_abs_vals(unsigned i, const monomial & m ) {
         int sign;
         vector<rational> abs_vals = get_sorted_abs_vals_from_mon(m, sign);
-        index_with_sign ms(i, rational(sign));
         auto it = m_monomials_by_abs_vals.find(abs_vals);
-        
         if (it == m_monomials_by_abs_vals.end()) {
-            vector<index_with_sign> v;
-            v.push_back(ms);
+            unsigned_vector v;
+            v.push_back(i);
             // v is a vector containing a single index_with_sign
             m_monomials_by_abs_vals.emplace(abs_vals, v);
         } 
         else {
-            it->second.push_back(ms);
+            it->second.push_back(i);
         }
         
     }