remove m_mons_to_rehash, fix a bug in emonomials::after_merge_eh(), generate order and tangent lemmas on any monomial

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

src/util/lp/emonomials.cpp

@@ -64,12 +64,7 @@ void emonomials::pop(unsigned n) {
     m_region.pop_scope(n);
     m_lim.shrink(m_lim.size() - n);
     SASSERT(monomials_are_canonized());
-    m_mons_to_rehash.clear();
     m_u_f_stack.pop_scope(n);
-    for (unsigned j : m_mons_to_rehash) {
-        remove_cg_mon(m_monomials[j]);
-        insert_cg_mon(m_monomials[j]);
-    }
 }
 
 void emonomials::remove_cell(head_tail& v, unsigned mIndex) {
@@ -384,8 +379,8 @@ void emonomials::after_merge_eh(signed_var r2, signed_var r1, signed_var v2, sig
     if (m_ve.find(~r1) == m_ve.find(~r2)) { // the other sign has also been merged
         m_use_lists.reserve(std::max(r2.var(), r1.var()) + 1);
         TRACE("nla_solver", tout << "rehasing " << r1.var() << "\n";);
-        rehash_cg(r1.var()); 
         merge_cells(m_use_lists[r2.var()], m_use_lists[r1.var()]);
+        rehash_cg(r1.var()); 
     }   
 }
 

src/util/lp/emonomials.h

@@ -82,7 +82,6 @@ class emonomials {
     
     union_find<emonomials>          m_u_f;
     trail_stack<emonomials>         m_u_f_stack;
-    std::unordered_set<unsigned>       m_mons_to_rehash;
     mutable svector<lpvar>          m_find_key; // the key used when looking for a monomial with the specific variables
     var_eqs<emonomials>&            m_ve;
     mutable vector<monomial>        m_monomials;     // set of monomials
@@ -133,8 +132,6 @@ public:
 
     void unmerge_eh(unsigned i, unsigned j) {
         TRACE("nla_solver", tout << "unmerged " << i << " and " << j << "\n";);
-        m_mons_to_rehash.insert(i);
-        m_mons_to_rehash.insert(j);
     }
     
     void merge_eh(unsigned r2, unsigned r1, unsigned v2, unsigned v1) {}

src/util/lp/nla_core.cpp

@@ -1599,13 +1599,12 @@ bool core::find_bfc_to_refine_on_monomial(const monomial& m, factorization & bf)
     return false;
 }
 
-// finds a canonical monomial with its binary factorization
+// finds a monomial to refine with its binary factorization
 bool core::find_bfc_to_refine(const monomial* & m, factorization & bf){
     m = nullptr;
     unsigned r = random(), sz = m_to_refine.size();
     for (unsigned k = 0; k < sz; k++) {
         lpvar i = m_to_refine[(k + r) % sz];
-        if (!is_canonical_monomial(i)) continue;
         m = &m_emons[i];
         SASSERT (!check_monomial(*m));
         if (m->size() == 2) {

src/util/lp/nla_order_lemmas.cpp

@@ -38,8 +38,7 @@ void order::order_lemma() {
     unsigned sz = to_ref.size();
     for (unsigned i = 0; i < sz && !done(); ++i) {
         lpvar j = to_ref[(i + r) % sz];
-        if (c().is_canonical_monomial(j))
-            order_lemma_on_canonical_monomial(c().emons()[j]);
+        order_lemma_on_monomial(c().emons()[j]);
     }
 }
 
@@ -47,7 +46,7 @@ void order::order_lemma() {
 // a > b && c > 0 => ac > bc
 // Consider here some binary factorizations of m=ac and
 // try create order lemmas with either factor playing the role of c.
-void order::order_lemma_on_canonical_monomial(const monomial& m) {
+void order::order_lemma_on_monomial(const monomial& m) {
     TRACE("nla_solver_details",
           tout << "m = " << pp_mon(c(), m););
 

src/util/lp/nla_order_lemmas.h

@@ -67,7 +67,7 @@ private:
     void order_lemma_on_binomial_ac_bd(const monomial& ac, bool k, const monomial& bd, const factor& b, lpvar d);
     void order_lemma_on_binomial_sign(const monomial& ac, lpvar x, lpvar y, int sign);
     void order_lemma_on_binomial(const monomial& ac);
-    void order_lemma_on_canonical_monomial(const monomial& rm);
+    void order_lemma_on_monomial(const monomial& rm);
     // |c_sign| = 1, and c*c_sign > 0
     // ac > bc => ac/|c| > bc/|c| => a*c_sign > b*c_sign
     void generate_ol(const monomial& ac,