fix loop in equiv_monomials (#91)

* fix loop in equiv_monomials

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fixes

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/util/lp/emonomials.cpp

@@ -228,15 +228,16 @@ namespace nla {
     }
 
     void emonomials::insert_cg(unsigned idx, monomial const& m) {
-        canonize(m);
+        do_canonize(m);
         lpvar v = m.var(), w;
         if (m_cg_table.find(v, w)) {
             SASSERT(w != v);
             unsigned idxr = m_var2index[w];
-            // Insert idx to the right of idxr
+            unsigned idxl = m_canonized[idxr].m_next;
-            m_canonized[idx].m_prev  = idxr;
+            m_canonized[idx].m_next  = idxr;
-            m_canonized[idx].m_next  = m_canonized[idxr].m_next;
+            m_canonized[idx].m_prev  = idxl;
-            m_canonized[idxr].m_next = idx;
+            m_canonized[idxr].m_prev = idx;
+            m_canonized[idxl].m_next = idx;
         }
         else {
             m_cg_table.insert(v);

src/util/lp/emonomials.h

@@ -305,27 +305,37 @@ namespace nla {
         */
         class sign_equiv_monomials_it {
             emonomials const& m;
-            unsigned m_index;
+            unsigned          m_index;
-            bool     m_touched;
+            bool              m_touched;
         public:
-            sign_equiv_monomials_it(emonomials const& m, unsigned idx, bool at_end): m(m), m_index(idx), m_touched(at_end) {}
+            sign_equiv_monomials_it(emonomials const& m, unsigned idx, bool at_end): 
+                m(m), m_index(idx), m_touched(at_end) {}
+
             monomial const& operator*() { return m.m_monomials[m_index]; }
+
             sign_equiv_monomials_it& operator++() { 
                 m_touched = true; 
                 m_index = m.m_canonized[m_index].m_next; 
                 return *this; 
             }
-            sign_equiv_monomials_it operator++(int) { sign_equiv_monomials_it tmp = *this; ++*this; return tmp; }
+
+            sign_equiv_monomials_it operator++(int) { 
+                sign_equiv_monomials_it tmp = *this; 
+                ++*this; 
+                return tmp; 
+            }
+
             bool operator==(sign_equiv_monomials_it const& other) const { 
                 return m_index == other.m_index && m_touched == other.m_touched; 
             }
+
             bool operator!=(sign_equiv_monomials_it const& other) const { 
                 return m_index != other.m_index || m_touched != other.m_touched; 
             }
         };
 
         class sign_equiv_monomials {
-            emonomials& em;
+            emonomials&     em;
             monomial const& m;
             unsigned index() const { return em.m_var2index[m.var()]; }
         public:

src/util/lp/nla_basics_lemmas.cpp

@@ -245,13 +245,14 @@ bool basics::basic_lemma(bool derived) {
         return true;
     if (derived)
         return false;
-    c().init_rm_to_refine();
     const auto& rm_ref = c().m_to_refine;
     TRACE("nla_solver", tout << "rm_ref = "; print_vector(rm_ref, tout););
     unsigned start = c().random();
-    for (unsigned j = rm_ref.size(); j-- > 0; ) {
+    unsigned sz = rm_ref.size();
-        const signed_vars& r = c().m_emons.canonical[(j + start) % rm_ref.size()];
+    for (unsigned j = 0; j < sz; ++j) {
-        SASSERT (!c().check_monomial(c().m_emons[r.var()]));
+        lpvar v = rm_ref[(j + start) % rm_ref.size()];
+        const signed_vars& r = c().m_emons.canonical[v];
+        SASSERT (!c().check_monomial(c().m_emons[v]));
         basic_lemma_for_mon(r, derived);
     } 
         

src/util/lp/nla_core.h

@@ -276,7 +276,6 @@ public:
 
     template <typename T>
     bool mon_has_zero(const T& product) const;
-    void init_rm_to_refine() { NOT_IMPLEMENTED_YET(); }
     lp::lp_settings& settings();
     unsigned random();
     void map_monomial_vars_to_monomial_indices(unsigned i);

src/util/lp/nla_order_lemmas.cpp

@@ -138,7 +138,6 @@ void order::negate_var_factor_relation(const rational& a_sign, lpvar a, const ra
 
 void order::order_lemma() {
     TRACE("nla_solver", );
-    c().init_rm_to_refine();
     const auto& rm_ref = c().m_to_refine;
     unsigned start = random();
     unsigned sz = rm_ref.size();