debug emons

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

src/smt/smt_context_pp.cpp

@@ -493,6 +493,7 @@ namespace smt {
         TRACE("lemma", tout << strm.str() << "\n";);
         display_lemma_as_smt_problem(out, num_antecedents, antecedents, num_eq_antecedents, eq_antecedents, consequent, logic);
         out.close();
+        if (m_lemma_id==6998) exit(0);
         return m_lemma_id;
     }
 

src/util/lp/emonomials.cpp

@@ -26,7 +26,7 @@
 namespace nla {
 
 
-    void emonomials::inc_visited() const {
+void emonomials::inc_visited() const {
     ++m_visited;
     if (m_visited == 0) {
         for (auto& svt : m_monomials) {
@@ -34,15 +34,16 @@ namespace nla {
         }
         ++m_visited;
     }
-    }
+}
 
-    void emonomials::push() { 
+void emonomials::push() { 
     m_lim.push_back(m_monomials.size());
     m_region.push_scope();
     m_ve.push();
-    }
+    SASSERT(monomials_are_canonized());
+}
 
-    void emonomials::pop(unsigned n) {
+void emonomials::pop(unsigned n) {
     m_ve.pop(n);
     unsigned old_sz = m_lim[m_lim.size() - n];
     for (unsigned i = m_monomials.size(); i-- > old_sz; ) {
@@ -61,9 +62,10 @@ namespace nla {
     m_monomials.shrink(old_sz);
     m_region.pop_scope(n);
     m_lim.shrink(m_lim.size() - n);
-    }
+    SASSERT(monomials_are_canonized());
+}
 
-    void emonomials::remove_cell(head_tail& v, unsigned mIndex) {
+void emonomials::remove_cell(head_tail& v, unsigned mIndex) {
     cell*& cur_head = v.m_head;
     cell*& cur_tail = v.m_tail;
     cell* old_head = cur_head->m_next;
@@ -75,18 +77,18 @@ namespace nla {
         cur_head = old_head;
         cur_tail->m_next = old_head;
     }
-    }
+}
 
-    void emonomials::insert_cell(head_tail& v, unsigned mIndex) {
+void emonomials::insert_cell(head_tail& v, unsigned mIndex) {
     cell*& cur_head = v.m_head;
     cell*& cur_tail = v.m_tail;
     cell* new_head = new (m_region) cell(mIndex, cur_head);
     cur_head = new_head;
     if (!cur_tail) cur_tail = new_head;
     cur_tail->m_next = new_head;
-    }
+}
 
-    void emonomials::merge_cells(head_tail& root, head_tail& other) {
+void emonomials::merge_cells(head_tail& root, head_tail& other) {
     if (&root == &other) return;
     cell*& root_head = root.m_head;
     cell*& root_tail = root.m_tail;
@@ -105,9 +107,9 @@ namespace nla {
     else {
         // other_head = other_tail = nullptr
     }
-    }
+}
 
-    void emonomials::unmerge_cells(head_tail& root, head_tail& other) {
+void emonomials::unmerge_cells(head_tail& root, head_tail& other) {
     if (&root == &other) return;
     cell*& root_head = root.m_head;
     cell*& root_tail = root.m_tail;
@@ -125,15 +127,15 @@ namespace nla {
         root_tail->m_next = root_head;
         other_tail->m_next = other_head;
     }
-    }
+}
 
-    emonomials::cell* emonomials::head(lpvar v) const {
+emonomials::cell* emonomials::head(lpvar v) const {
     v = m_ve.find(v).var();
     m_use_lists.reserve(v + 1);
     return m_use_lists[v].m_head;
-    }
+}
 
-    monomial const* emonomials::find_canonical(svector<lpvar> const& vars) const {
+monomial const* emonomials::find_canonical(svector<lpvar> const& vars) const {
     SASSERT(m_ve.is_root(vars));
     m_find_key = vars;
     std::sort(m_find_key.begin(), m_find_key.end());
@@ -143,10 +145,10 @@ namespace nla {
         result = &m_monomials[m_var2index[w]];
     }
     return result;
-    }
+}
 
 
-    void emonomials::remove_cg(lpvar v) {
+void emonomials::remove_cg(lpvar v) {
     cell* c = m_use_lists[v].m_head;
     if (c == nullptr) {
         return;
@@ -163,9 +165,9 @@ namespace nla {
         }
     }
     while (c != first);
-    }
+}
 
-    void emonomials::remove_cg(unsigned idx, monomial& m) {
+void emonomials::remove_cg(unsigned idx, monomial& m) {
     monomial& sv = m_monomials[idx];
     unsigned next = sv.next();
     unsigned prev = sv.prev();
@@ -185,16 +187,16 @@ namespace nla {
         sv.next() = idx;
         sv.prev() = idx;
     }
-    }
+}
 
-    /**
+/**
    \brief insert canonized monomials using v into a congruence table.
    Prior to insertion, the monomials are canonized according to the current
    variable equivalences. The canonized monomials (monomial) are considered
    in the same equivalence class if they have the same set of representative
    variables. Their signs may differ.       
-    */
+*/
-    void emonomials::insert_cg(lpvar v) {
+void emonomials::insert_cg(lpvar v) {
     cell* c = m_use_lists[v].m_head;
     if (c == nullptr) {
         return;
@@ -212,9 +214,9 @@ namespace nla {
         }
     }
     while (c != first);
-    }
+}
 
-    void emonomials::insert_cg(unsigned idx, monomial & m) {
+void emonomials::insert_cg(unsigned idx, monomial & m) {
     do_canonize(m);
     lpvar v = m.var(), w;
     if (m_cg_table.find(v, w)) {
@@ -231,24 +233,24 @@ namespace nla {
         SASSERT(m_monomials[idx].next() == idx);
         SASSERT(m_monomials[idx].prev() == idx);
     }        
-    }
+}
 
-    void emonomials::set_visited(monomial& m) const {
+void emonomials::set_visited(monomial& m) const {
     m_monomials[m_var2index[m.var()]].visited() = m_visited;
-    }
+}
 
-    bool emonomials::is_visited(monomial const& m) const {
+bool emonomials::is_visited(monomial const& m) const {
     return m_visited == m_monomials[m_var2index[m.var()]].visited();
-    }
+}
 
-    /**
+/**
    \brief insert a new monomial.
 
    Assume that the variables are canonical, that is, not equal in current
    context to another variable. The monomial is inserted into a congruence
    class of equal up-to var_eqs monomials.
-     */
+*/
-    void emonomials::add(lpvar v, unsigned sz, lpvar const* vs) {
+void emonomials::add(lpvar v, unsigned sz, lpvar const* vs) {
     unsigned idx = m_monomials.size();
     m_monomials.push_back(monomial(v, sz, vs, idx));
     lpvar last_var = UINT_MAX;
@@ -264,17 +266,33 @@ namespace nla {
     SASSERT(m_ve.is_root(v));
     m_var2index.setx(v, idx, UINT_MAX);
     insert_cg(idx, m_monomials[idx]);
-    }
+}
 
-    void emonomials::do_canonize(monomial & m) const {
+void emonomials::do_canonize(monomial & m) const {
     m.reset_rfields();
     for (lpvar v : m.vars()) {
         m.push_rvar(m_ve.find(v));
     }
     m.sort_rvars();
-    }
+}
 
-    bool emonomials::canonize_divides(monomial& m, monomial & n) const {
+bool emonomials::is_canonized(const monomial & m) const {
+    monomial mm(m);
+    do_canonize(mm);
+    return mm.rvars() == m.rvars();
+}
+
+bool emonomials:: monomials_are_canonized() const {
+    for (auto & m: m_monomials) {
+        if (! is_canonized(m)) {
+            return false;
+        }
+    }
+    return true;
+}
+
+
+bool emonomials::canonize_divides(monomial& m, monomial & n) const {
     if (m.size() > n.size()) return false;
     unsigned ms = m.size(), ns = n.size();
     unsigned i = 0, j = 0;
@@ -295,20 +313,20 @@ namespace nla {
             ++j;
         }
     }
-    }
+}
 
 // yes, assume that monomials are non-empty.
-    emonomials::pf_iterator::pf_iterator(emonomials const& m, monomial & mon, bool at_end):
+emonomials::pf_iterator::pf_iterator(emonomials const& m, monomial & mon, bool at_end):
     m_em(m), m_mon(&mon), m_it(iterator(m, m.head(mon.vars()[0]), at_end)), m_end(iterator(m, m.head(mon.vars()[0]), true)) {
     fast_forward();
-    }
+}
 
-    emonomials::pf_iterator::pf_iterator(emonomials const& m, lpvar v, bool at_end):
+emonomials::pf_iterator::pf_iterator(emonomials const& m, lpvar v, bool at_end):
     m_em(m), m_mon(nullptr), m_it(iterator(m, m.head(v), at_end)), m_end(iterator(m, m.head(v), true)) {
     fast_forward();
-    }
+}
 
-    void emonomials::pf_iterator::fast_forward() {
+void emonomials::pf_iterator::fast_forward() {
     for (; m_it != m_end; ++m_it) {
         if (m_mon && m_mon->var() != (*m_it).var() && m_em.canonize_divides(*m_mon, *m_it) && !m_em.is_visited(*m_it)) {
             m_em.set_visited(*m_it);
@@ -319,32 +337,32 @@ namespace nla {
             break;
         }
     }
-    }
+}
 
-    void emonomials::merge_eh(signed_var r2, signed_var r1, signed_var v2, signed_var v1) {
+void emonomials::merge_eh(signed_var r2, signed_var r1, signed_var v2, signed_var v1) {
     // no-op
-    }
+}
 
-    void emonomials::after_merge_eh(signed_var r2, signed_var r1, signed_var v2, signed_var v1) {
+void emonomials::after_merge_eh(signed_var r2, signed_var r1, signed_var v2, signed_var v1) {
     if (!r2.sign() && m_ve.find(~r2) != m_ve.find(r1)) {
         m_use_lists.reserve(std::max(r2.var(), r1.var()) + 1);
         rehash_cg(r1.var()); 
         merge_cells(m_use_lists[r2.var()], m_use_lists[r1.var()]);
     }   
-    }
+}
 
-    void emonomials::unmerge_eh(signed_var r2, signed_var r1) {
+void emonomials::unmerge_eh(signed_var r2, signed_var r1) {
     if (!r2.sign() && m_ve.find(~r2) != m_ve.find(r1)) {
         unmerge_cells(m_use_lists[r2.var()], m_use_lists[r1.var()]);            
         rehash_cg(r1.var());
     }        
-    }
+}
 
 std::ostream& emonomials::display(const core& cr, std::ostream& out) const {
     out << "monomials\n";
     unsigned idx = 0;
     for (auto const& m : m_monomials) {
-           out << (idx++) << ": " << pp_mon(cr, m) << "\n";
+        out << (idx++) << ": " << pp_rmon(cr, m) << "\n";
     }
     out << "use lists\n";
     idx = 0;
@@ -362,6 +380,6 @@ std::ostream& emonomials::display(const core& cr, std::ostream& out) const {
         ++idx;
     }
     return out;
-   }
+}
 
 }

src/util/lp/emonomials.h

@@ -100,7 +100,6 @@ class emonomials : public var_eqs_merge_handler {
     void rehash_cg(lpvar v) { remove_cg(v); insert_cg(v); }
 
     void do_canonize(monomial& m) const; 
-
     cell* head(lpvar v) const;
     void set_visited(monomial& m) const;
     bool is_visited(monomial const& m) const;
@@ -141,6 +140,8 @@ public:
     */
     monomial const& operator[](lpvar v) const { return m_monomials[m_var2index[v]]; }
     monomial & operator[](lpvar v) { return m_monomials[m_var2index[v]]; }
+    bool is_canonized(const monomial&) const;    
+    bool monomials_are_canonized() const;
     
     /**
        \brief obtain the representative canonized monomial 
@@ -204,7 +205,9 @@ public:
     public:
         pf_iterator(emonomials const& m, monomial& mon, bool at_end);
         pf_iterator(emonomials const& m, lpvar v, bool at_end);
-        monomial & operator*() { return *m_it; }
+        monomial & operator*() {
+            return *m_it;
+        }
         pf_iterator& operator++() { ++m_it; fast_forward(); return *this; }
         pf_iterator operator++(int) { pf_iterator tmp = *this; ++*this; return tmp; }
         bool operator==(pf_iterator const& other) const { return m_it == other.m_it; }

src/util/lp/monomial.h

@@ -63,7 +63,7 @@ public:
     svector<lpvar> const& rvars() const { return m_rvars; }
     bool sign() const { return m_rsign; }
     rational rsign() const { return rational(m_rsign ? -1 : 1); }
-    void reset_rfields() { m_rsign = false; m_rvars.reset(); }
+    void reset_rfields() { m_rsign = false; m_rvars.reset(); SASSERT(m_rvars.size() == 0); }
     void push_rvar(signed_var sv) { m_rsign ^= sv.sign(); m_rvars.push_back(sv.var()); }
     void sort_rvars() {
         std::sort(m_rvars.begin(), m_rvars.end());

src/util/lp/nla_basics_lemmas.cpp

@@ -121,11 +121,13 @@ bool basics::basic_sign_lemma_on_mon(lpvar v, std::unordered_set<unsigned> & exp
     if (!try_insert(v, explored)) {
         return false;
     }
-
     const monomial& m_v = c().m_emons[v];
-    TRACE("nla_solver_details", tout << "mon = " << pp_mon(c(), m_v););
+    TRACE("nla_solver", tout << "m_v = " << pp_rmon(c(), m_v););
+    SASSERT(c().m_emons.is_canonized(m_v));
 
     for (auto const& m : c().m_emons.enum_sign_equiv_monomials(v)) {
+        TRACE("nla_solver_details", tout << "m = " << pp_rmon(c(), m););
+        SASSERT(m.rvars() == m_v.rvars());
         if (m_v.var() != m.var() && basic_sign_lemma_on_two_monomials(m_v, m) && done()) 
             return true;
     }
@@ -154,12 +156,14 @@ bool basics::basic_sign_lemma(bool derived) {
 void basics::generate_sign_lemma(const monomial& m, const monomial& n, const rational& sign) {
     add_empty_lemma();
     TRACE("nla_solver",
-          tout << "m = "; c().print_monomial_with_vars(m, tout);
+          tout << "m = " << pp_rmon(_(), m);
-          tout << "n = "; c().print_monomial_with_vars(n, tout);
+          tout << "n = " << pp_rmon(_(), n);
           );
     c().mk_ineq(m.var(), -sign, n.var(), llc::EQ);
     explain(m);
+    TRACE("nla_solver", tout << "m exp = "; _().print_explanation(_().current_expl(), tout););
     explain(n);        
+    TRACE("nla_solver", tout << "n exp = "; _().print_explanation(_().current_expl(), tout););
     TRACE("nla_solver", c().print_lemma(tout););
 }
 // try to find a variable j such that val(j) = 0

src/util/lp/nla_core.cpp

@@ -112,7 +112,9 @@ void core::push() {
      
 void core::pop(unsigned n) {
     TRACE("nla_solver", tout << "n = " << n << "\n";);
+    TRACE("nla_solver", tout << "before pop mons = " << pp_emons(*this, m_emons) << "\n";);   
     m_emons.pop(n); 
+    TRACE("nla_solver", tout << "after pop mons = " << pp_emons(*this, m_emons) << "\n";);   
 }
 
 rational core::product_value(const unsigned_vector & m) const {
@@ -718,7 +720,8 @@ std::ostream & core::print_var(lpvar j, std::ostream & out) const {
         out << " = " << val(j);;
     }
         
-    m_lar_solver.print_column_info(j, out) <<";";
+    m_lar_solver.print_column_info(j, out);
+    out << "root=" << m_evars.find(j) << "\n";
     return out;
 }
 

src/util/lp/var_eqs.cpp

@@ -120,6 +120,8 @@ void var_eqs::explain_dfs(signed_var v1, signed_var v2, lp::explanation& e) cons
 }
 
 void var_eqs::explain_bfs(signed_var v1, signed_var v2, lp::explanation& e) const {
+    static int ddd=0;
+    TRACE("nla_solver", tout << ++ddd << "\n";);
     SASSERT(find(v1) == find(v2));
     if (v1 == v2) {
         return;