add equivalence explanations

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

src/util/lp/explanation.h

@@ -35,9 +35,11 @@ public:
         m_explanation.push_back(std::make_pair(one_of_type<mpq>(), j));
     }
 
-    template <typename A> void add(const A& a) { for (constraint_index j : a) push_justification(j); }
+    template <typename A>
-    bool empty() const {
+    void add(const A& a) { for (auto j : a) push_justification(j); }
-        return m_explanation.empty();
+
-    }
+    void add(unsigned j) { push_justification(j); }
+    
+    bool empty() const {  return m_explanation.empty();  }
 };
 }

src/util/lp/nla_solver.cpp

@@ -155,20 +155,22 @@ struct solver::imp {
         return sign * m_lar_solver.get_column_value(j) != m_lar_solver.get_column_value(k);
     }
 
-    void explain(const rooted_mon& rm) {
-        expl_set e;
-        add_explanation_of_reducing_to_rooted_monomial_and_set_expl(rm, e);
-    }
     
-    void add_explanation_of_reducing_to_rooted_monomial(const monomial& m, expl_set & exp) const {
+    void explain(const monomial& m) const {
-        m_vars_equivalence.add_explanation_of_reducing_to_rooted_monomial(m, exp);
+        m_vars_equivalence.explain(m, *m_expl);
     }
 
-    void add_explanation_of_reducing_to_rooted_monomial(lpvar j, expl_set & exp) const {
+    void explain(const rooted_mon& rm) const {
-        auto it = m_var_to_its_monomial.find(j);
+        auto & m = m_monomials[rm.orig_index()];
-        if (it == m_var_to_its_monomial.end())
+        explain(m);
-            return; // j is not a var of a monomial
+    }
-        add_explanation_of_reducing_to_rooted_monomial(it->second, exp);
+
+    void explain(const factor& f) const {
+        if (f.type() == factor_type::VAR) {
+            m_vars_equivalence.explain(f.index(), *m_expl);
+        } else {
+            m_vars_equivalence.explain(m_monomials[m_rm_table.vec()[f.index()].orig_index()], *m_expl);
+        }
     }
 
     template <typename T>
@@ -304,14 +306,11 @@ struct solver::imp {
         mk_ineq(j, cmp, rational::zero());
     }
     
-    // the monomials should be equal by modulo sign but this is not so the model
+    // the monomials should be equal by modulo sign but this is not so in the model
     void fill_explanation_and_lemma_sign(const monomial& a, const monomial & b, rational const& sign) {
-        expl_set expl;
         SASSERT(sign == 1 || sign == -1);
-        add_explanation_of_reducing_to_rooted_monomial(a, expl);
+        explain(a);
-        add_explanation_of_reducing_to_rooted_monomial(b, expl);
+        explain(b);
-        m_expl->clear();
-        m_expl->add(expl);
         TRACE("nla_solver",
               tout << "used constraints: ";
               for (auto &p : *m_expl)
@@ -556,17 +555,6 @@ struct solver::imp {
         return true;
     }
 
-    void add_explanation_of_reducing_to_rooted_monomial_and_set_expl(const rooted_mon& rm, expl_set& ex) {
-        add_explanation_of_reducing_to_rooted_monomial(m_monomials[rm.orig_index()], ex);
-        set_expl(ex);
-    }
-    
-    void set_expl(const expl_set & e) {
-        m_expl->clear();
-        for (lpci ci : e)
-            m_expl->push_justification(ci);
-    }
-
     void trace_print_monomial_and_factorization(const rooted_mon& rm, const factorization& f, std::ostream& out) const {
         out << "rooted vars: ";
         print_product(rm.m_vars, out);
@@ -926,6 +914,12 @@ struct solver::imp {
         negate_factor_equality(c, d);
         negate_factor_relation(rational(c_sign), a, rational(d_sign), b);
         mk_ineq(flip_sign(ac), var(ac), -flip_sign(bd), var(bd), ab_cmp);
+        explain(ac);
+        explain(a);
+        explain(c);
+        explain(bd);
+        explain(b);
+        explain(d);
     }
 
     bool get_cd_signs_for_ol(const rational& c, const rational& d, int& c_sign, int & d_sign) const {

src/util/lp/vars_equivalence.h

@@ -17,10 +17,11 @@
 
 
   --*/
+
 namespace nla {
 
 typedef lp::constraint_index     lpci;
-typedef std::unordered_set<lpci> expl_set;
+typedef lp::explanation          expl_set;
 typedef lp::var_index            lpvar;
 struct hash_svector {
     size_t operator()(const unsigned_vector & v) const {
@@ -197,7 +198,13 @@ struct vars_equivalence {
         }
     }
 
-    void add_equiv_exp(unsigned j, expl_set& exp) const {
+    template <typename T>
+    void explain(const T& collection, expl_set & exp) const {
+        for (lpvar j : collection) {
+            explain(j, exp);
+        }
+    } 
+    void explain(lpvar j, expl_set& exp) const {
         while (true) {
             auto it = m_tree.find(j);
             if (it == m_tree.end())
@@ -205,16 +212,16 @@ struct vars_equivalence {
             if (it->second == static_cast<unsigned>(-1))
                 return;
             const equiv & e = m_equivs[it->second];
-            exp.insert(e.m_c0);
+            exp.add(e.m_c0);
-            exp.insert(e.m_c1);
+            exp.add(e.m_c1);
             j = get_parent_node(j, e);
         }
     }
     
     template <typename T>
     void add_explanation_of_reducing_to_rooted_monomial(const T & m, expl_set & exp) const {
-        for (auto j : m)
+        for (lpvar j : m)
-            add_equiv_exp(j, exp);
+            explain(j, exp);
     }
 
     void register_var(unsigned j, const rational& val) {