From 3441f565b231f3ad0a9db958add658771f95f41d Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Fri, 25 Jan 2019 14:48:08 -0800
Subject: [PATCH] before changes is basic_sign_lemma

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/util/debug.h               |  8 ++++----
 src/util/lp/nla_solver.cpp     |  5 ++++-
 src/util/lp/rooted_mons.h      | 12 ++++++++++++
 src/util/lp/vars_equivalence.h | 14 ++------------
 4 files changed, 22 insertions(+), 17 deletions(-)

diff --git a/src/util/debug.h b/src/util/debug.h
index 48f4e548e..613328013 100644
--- a/src/util/debug.h
+++ b/src/util/debug.h
@@ -38,11 +38,11 @@ bool assertions_enabled();
 #include "util/error_codes.h"
 #include "util/warning.h"
 
-//#ifdef Z3DEBUG
-//#define DEBUG_CODE(CODE) { CODE } ((void) 0)
-//#else
+#ifdef Z3DEBUG
+#define DEBUG_CODE(CODE) { CODE } ((void) 0)
+#else
 #define DEBUG_CODE(CODE) ((void) 0)
-//#endif
+#endif
 
 #ifdef __APPLE__
 #include <TargetConditionals.h>
diff --git a/src/util/lp/nla_solver.cpp b/src/util/lp/nla_solver.cpp
index 2039958f9..8e78e0c3e 100644
--- a/src/util/lp/nla_solver.cpp
+++ b/src/util/lp/nla_solver.cpp
@@ -684,6 +684,7 @@ struct solver::imp {
     bool basic_sign_lemma_on_mon(unsigned i){
         TRACE("nla_solver", tout << "i = " << i << ", mon = "; print_monomial_with_vars(m_monomials[i], tout););
         const monomial& m = m_monomials[i];
+        
         for (unsigned n : equiv_monomials(m, [this](lpvar j) {return &abs_eq_vars(j);},
                                           [this](const unsigned_vector& key) {return find_monomial(key);})
              ) {
@@ -716,6 +717,7 @@ struct solver::imp {
      -ab = a(-b)
     */
     bool basic_sign_lemma() {
+        TRACE("nla_solver", tout << "m_to_refine.size = " << m_to_refine.size(););
         for (unsigned i : m_to_refine){
             if (basic_sign_lemma_on_mon(i))
                 return true;
@@ -1177,13 +1179,13 @@ struct solver::imp {
     
     // x is equivalent to y if x = +- y
     void init_vars_equivalence() {
-        TRACE("nla_solver",);
         SASSERT(m_vars_equivalence.empty());
         collect_equivs();
         m_vars_equivalence.create_tree();
         for (lpvar j = 0; j < m_lar_solver.number_of_vars(); j++) {
             m_vars_equivalence.register_var(j, vvr(j));
         }
+        TRACE("nla_solver", tout << "number of equivs = " << m_vars_equivalence.size(););
         
         SASSERT((m_lar_solver.settings().random_next() % 100) || tables_are_ok());
     }
@@ -1564,6 +1566,7 @@ struct solver::imp {
     }
     
     bool order_lemma() {
+        TRACE("nla_solver", );
         for (const auto& rm : m_rm_table.vec()) {
             if (check_monomial(m_monomials[rm.orig_index()]))
                 continue;
diff --git a/src/util/lp/rooted_mons.h b/src/util/lp/rooted_mons.h
index 40a6aa99a..892c1a941 100644
--- a/src/util/lp/rooted_mons.h
+++ b/src/util/lp/rooted_mons.h
@@ -21,6 +21,18 @@
 #pragma once
 #include "util/lp/lp_utils.h"
 namespace nla {
+struct index_with_sign {
+    unsigned m_i; // the index
+    rational m_sign; // the sign: -1 or 1
+    index_with_sign(unsigned i, rational sign) : m_i(i), m_sign(sign) {}
+    index_with_sign() {}
+    bool operator==(const index_with_sign& b) {
+        return m_i == b.m_i && m_sign == b.m_sign;
+    }
+    unsigned var() const { return m_i; }
+    const rational& sign() const { return m_sign; }
+};
+    
 struct rooted_mon {
     svector<lpvar>   m_vars;
     index_with_sign  m_orig;
diff --git a/src/util/lp/vars_equivalence.h b/src/util/lp/vars_equivalence.h
index f7dee5a5a..250debf1e 100644
--- a/src/util/lp/vars_equivalence.h
+++ b/src/util/lp/vars_equivalence.h
@@ -29,17 +29,6 @@ struct hash_svector {
     }
 };
 
-struct index_with_sign {
-    unsigned m_i; // the index
-    rational m_sign; // the sign: -1 or 1
-    index_with_sign(unsigned i, rational sign) : m_i(i), m_sign(sign) {}
-    index_with_sign() {}
-    bool operator==(const index_with_sign& b) {
-        return m_i == b.m_i && m_sign == b.m_sign;
-    }
-    unsigned var() const { return m_i; }
-    const rational& sign() const { return m_sign; }
-};
 
 
 struct vars_equivalence {
@@ -68,7 +57,7 @@ struct vars_equivalence {
     // m_tree is a spanning tree of the graph of equivs represented by m_equivs
     std::unordered_map<unsigned, unsigned>        m_tree;  
     // 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), that k is the parent of v
+    // 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;
@@ -86,6 +75,7 @@ struct vars_equivalence {
     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; 
     }