cleanup and adding an assert in emons

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

src/util/lp/emonomials.h

@@ -30,7 +30,6 @@ namespace nla {
 class core;
 
 class emonomials : public var_eqs_merge_handler {
-    mutable svector<lpvar> m_find_key;
     /**
        \brief singly-lined cyclic list of monomial indices where variable occurs.
        Each variable points to the head and tail of the cyclic list.
@@ -75,6 +74,7 @@ class emonomials : public var_eqs_merge_handler {
         }
     };
 
+    mutable svector<lpvar>            m_find_key; // the key used when looking for a monomial with the specific variables
     var_eqs&                        m_ve;
     mutable vector<monomial>        m_monomials;     // set of monomials
     mutable unsigned_vector         m_var2index;     // var_mIndex -> mIndex
@@ -266,16 +266,16 @@ public:
     };
 
     class sign_equiv_monomials {
-        emonomials&     em;
+        const emonomials&     em;
         monomial const& m;
         unsigned index() const { return em.m_var2index[m.var()]; }
     public:
-        sign_equiv_monomials(emonomials & em, monomial const& m): em(em), m(m) {}
+        sign_equiv_monomials(const emonomials & em, monomial const& m): em(em), m(m) {}
         sign_equiv_monomials_it begin() { return sign_equiv_monomials_it(em, index(), false); }
         sign_equiv_monomials_it end() { return sign_equiv_monomials_it(em, index(), true); }
     };
 
-    sign_equiv_monomials enum_sign_equiv_monomials(monomial const& m) { return sign_equiv_monomials(*this, m); }
+    sign_equiv_monomials enum_sign_equiv_monomials(monomial const& m) const { return sign_equiv_monomials(*this, m); }
     sign_equiv_monomials enum_sign_equiv_monomials(lpvar v) { return enum_sign_equiv_monomials((*this)[v]); }
     /**
        \brief display state of emonomials

src/util/lp/nla_basics_lemmas.h

@@ -19,7 +19,6 @@
   --*/
 #pragma once
 #include "util/lp/monomial.h"    
-#include "util/lp/rooted_mons.h"    
 #include "util/lp/factorization.h"    
 #include "util/lp/nla_common.h"    
 

src/util/lp/nla_core.cpp

@@ -1866,6 +1866,7 @@ lbool core:: inner_check(bool derived) {
         }
         if (derived) continue;
         TRACE("nla_solver", tout << "passed derived and basic lemmas\n";);
+        SASSERT(elists_are_consistent());
         if (search_level == 1) {
             m_order.order_lemma();
         } else { // search_level == 2
@@ -1875,8 +1876,58 @@ lbool core:: inner_check(bool derived) {
     }
     return m_lemma_vec->empty()? l_undef : l_false;
 }
+
+struct hash_svector {
+    size_t operator()(const unsigned_vector & v) const {
+        return svector_hash<unsigned_hash>()(v);
+    }
+};
+
+bool core::elist_is_consistent(const std::unordered_set<lpvar> & list) const {
+    bool first = true;
+    bool p;
+    for (lpvar j : list) {
+        if (first) {
+            p = check_monomial(m_emons[j]);
+            first = false;
+        } else 
+            if (check_monomial(m_emons[j]) != p)
+                return false;
+    }
+    return true;
+}
+
+bool core::elists_are_consistent() const {
     
-lbool core:: check(vector<lemma>& l_vec) {
+    std::unordered_map<unsigned_vector, std::unordered_set<lpvar>, hash_svector> lists;
+    for (auto const & m : m_emons) {
+        auto it = lists.find(m.rvars());
+        if (it == lists.end()) {
+            std::unordered_set<lpvar> v;
+            v.insert(m.var());
+            lists[m.rvars()] = v;            
+        } else {
+            it->second.insert(m.var());
+        }
+    }
+    for (auto const & m : m_emons) {
+        if (!is_canonical_monomial(m.var()))
+            continue;
+        std::unordered_set<lpvar> c;
+        for (const monomial& e : m_emons.enum_sign_equiv_monomials(m))
+            c.insert(e.var());
+        auto it = lists.find(m.rvars());
+        SASSERT(it->second == c);
+    }
+
+    for (const auto & p : lists) {
+        if (! elist_is_consistent(p.second))
+            return false;
+    }
+    return true;
+}
+
+lbool core::check(vector<lemma>& l_vec) {
     settings().st().m_nla_calls++;
     TRACE("nla_solver", tout << "calls = " << settings().st().m_nla_calls << "\n";);
     m_lemma_vec =  &l_vec;

src/util/lp/nla_core.h

@@ -241,7 +241,8 @@ public:
         
     bool find_canonical_monomial_of_vars(const svector<lpvar>& vars, lpvar & i) const;
     bool is_canonical_monomial(lpvar) const;
-
+    bool elists_are_consistent() const;
+    bool elist_is_consistent(const std::unordered_set<lpvar>&) const;
     bool var_has_positive_lower_bound(lpvar j) const;
 
     bool var_has_negative_upper_bound(lpvar j) const;

src/util/lp/nla_order_lemmas.h

@@ -18,7 +18,6 @@
 
   --*/
 #pragma once
-#include "util/lp/rooted_mons.h"
 #include "util/lp/factorization.h"
 #include "util/lp/nla_common.h"
 

src/util/lp/nla_tangent_lemmas.h

@@ -19,7 +19,6 @@
   --*/
 #pragma once
 #include "util/rational.h"
-#include "util/lp/rooted_mons.h"
 #include "util/lp/factorization.h"
 #include "util/lp/nla_common.h"
 

src/util/lp/var_eqs.h

@@ -154,6 +154,7 @@ public:
         return explain(find(s), s, e); 
     }
 
+    // iterates over the class of signed_var(m_idx)
     class iterator {
         var_eqs& m_ve;        // context.
         unsigned m_idx;       // index into a signed variable, same as union-find index