fixes (#96)

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

src/smt/theory_lra.cpp

@@ -1642,6 +1642,7 @@ public:
                 return FC_CONTINUE;
             }
 
+            TRACE("arith", display(tout););
             switch (check_lia()) {
             case l_true:
                 break;
@@ -3574,7 +3575,7 @@ public:
         for (const auto & ti : term) {
             theory_var w;
             if (lp().is_term(ti.var())) {
-                //w = m_term_index2theory_var.get(lp().adjust_term_index(ti.var()), null_theory_var);
+                //w = m_term_index2theory_var.get(lp().adjust_term_index(ti.m_key), null_theory_var);
                 //if (w == null_theory_var) // if extracting expressions directly from nested term
                 lp::lar_term const& term1 = lp().get_term(ti.var());
                 rational coeff2 = coeff * ti.coeff();

src/util/lp/lar_term.h

@@ -41,13 +41,8 @@ public:
         }
     }
 
-    void add_var(unsigned j) {
-        rational c(1);
-        add_coeff_var(c, j);
-    }
-
     bool is_empty() const {
-        return m_coeffs.empty();
+        return m_coeffs.empty(); // && is_zero(m_v);
     }
     
     unsigned size() const { return static_cast<unsigned>(m_coeffs.size()); }
@@ -57,7 +52,12 @@ public:
         return m_coeffs;
     }
     
-    bool operator==(const lar_term & a) const {  return m_coeffs == a.m_coeffs; }
+    lar_term(const vector<std::pair<mpq, unsigned>>& coeffs) {
+        for (const auto & p : coeffs) {
+            add_monomial(p.first, p.second);
+        }
+    }
+    bool operator==(const lar_term & a) const {  return false; } // take care not to create identical terms
     bool operator!=(const lar_term & a) const {  return ! (*this == a);}
     // some terms get used in add constraint
     // it is the same as the offset in the m_constraints
@@ -76,7 +76,7 @@ public:
         if (it == nullptr) return;
         const mpq & b = it->get_data().m_value;
         for (unsigned it_j :li.m_index) {
-            add_coeff_var(- b * li.m_data[it_j], it_j);
+            add_monomial(- b * li.m_data[it_j], it_j);
         }
         m_coeffs.erase(j);
     }

src/util/lp/nla_core.cpp

@@ -47,8 +47,8 @@ bool core::compare_holds(const rational& ls, llc cmp, const rational& rs) const
 
 rational core::value(const lp::lar_term& r) const {
     rational ret(0);
-    for (const auto & t : r.coeffs()) {
-        ret += t.second * val(t.first);
+    for (const auto & t : r) {
+        ret += t.coeff() * val(t.var());
     }
     return ret;
 }

src/util/lp/nla_solver.cpp

@@ -45,6 +45,11 @@ void solver::push(){
 void solver::pop(unsigned n) {
     m_core->pop(n);
 }
+
+    std::ostream& solver::display(std::ostream& out) {
+        return m_core->print_monomials(out);
+    }
+
         
 solver::solver(lp::lar_solver& s, reslimit& lim, params_ref const& p) {
     m_core = alloc(core, s, lim, p);

src/util/lp/nla_solver.h

@@ -41,5 +41,6 @@ public:
     void pop(unsigned scopes);
     bool need_check();
     lbool check(vector<lemma>&);
+    std::ostream& display(std::ostream& out);
 };
 }

src/util/map.h

@@ -180,6 +180,16 @@ public:
     void swap(table2map & other) {
         m_table.swap(other.m_table);
     }
+
+    bool operator==(table2map const& other) const {
+        if (size() != other.size()) return false;
+        for (auto const& kv : *this) {
+            auto* e = other.find_core(kv.m_key);
+            if (!e) return false;
+            if (e->get_data().m_value != kv.m_value) return false;
+        }
+        return true;
+    }
     
 #ifdef Z3DEBUG