From c1e0c79a69a574ede2231c919abbceb638d30db3 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Thu, 1 Nov 2018 11:36:04 -0700
Subject: [PATCH] integrating Nikolaj's changes

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/smt/theory_lra.cpp   | 44 +++++++++++++++++++++++++++++++++-------
 src/util/lp/monomial.h   |  5 ++++-
 src/util/lp/nla_solver.h |  4 +++-
 3 files changed, 44 insertions(+), 9 deletions(-)

diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 7980d6261..32acc3fd5 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -1568,7 +1568,8 @@ public:
             }
             enode* n2 = get_enode(other);
             if (n1->get_root() != n2->get_root()) {
-                TRACE("arith", tout << enode_eq_pp(enode_pair(n1, n2), ctx());
+                TRACE("arith", tout << mk_pp(n1->get_owner(), m) << " = " << mk_pp(n2->get_owner(), m) << "\n";
+                      tout << mk_pp(n1->get_owner(), m) << " = " << mk_pp(n2->get_owner(), m) << "\n";
                       tout << "v" << v << " = " << "v" << other << "\n";);
                 m_assume_eq_candidates.push_back(std::make_pair(v, other));
                 result = true;
@@ -2073,6 +2074,32 @@ public:
 
     nla::lemma m_lemma;
  
+    lp::lar_term mk_term(nla::polynomial const& poly) {
+        lp::lar_term term;
+        for (auto const& mon : poly) {
+            SASSERT(!mon.empty());
+            if (mon.size() == 1) {
+                term.add_coeff_var(mon.get_coeff(), mon[0]);
+            }
+            else {
+                // create the expression corresponding to the product.
+                // internalize it.
+                // extract the theory var representing the product.
+                // convert the theory var back to lp::var_index
+                expr_ref_vector mul(m);
+                for (lp::var_index v : mon) {
+                    theory_var w = m_var_index2theory_var[v];
+                    mul.push_back(get_enode(w)->get_owner());
+                }
+                app_ref t(a.mk_mul(mul.size(), mul.c_ptr()), m);
+                VERIFY(internalize_term(t));
+                theory_var w = ctx().get_enode(t)->get_th_var(get_id());
+                term.add_coeff_var(mon.get_coeff(), m_theory_var2var_index[w]);
+            }
+        }
+        return term;
+    }
+
     lbool check_aftermath_nla(lbool r) {
         switch (r) {
         case l_false: {            
@@ -2091,6 +2118,8 @@ public:
                 }
                 TRACE("arith", tout << "is_lower: " << is_lower << " pos " << pos << "\n";);
                 app_ref atom(m);
+                // TBD utility: lp::lar_term term = mk_term(ineq.m_poly);
+                // then term is used instead of ineq.m_term
                 if (is_eq) {
                     atom = mk_eq(ineq.m_term, ineq.m_rs);
                 }
@@ -3081,15 +3110,15 @@ public:
                                 get_id(), ctx().get_region(), m_core.size(), m_core.c_ptr(), m_eqs.size(), m_eqs.c_ptr(), x, y, 0, nullptr));
 
                     TRACE("arith",
-                          for (literal c : m_core) {
-                              ctx().display_detailed_literal(tout, c);
+                          for (unsigned i = 0; i <  m_core.size(); ++i) {
+                              ctx().display_detailed_literal(tout, m_core[i]);
                               tout << "\n";
                           } 
-                          for (enode_pair const& p : m_eqs) {
-                              tout << enode_eq_pp(p, ctx());
+                          for (unsigned i = 0; i < m_eqs.size(); ++i) {
+                              tout << mk_pp(m_eqs[i].first->get_owner(), m) << " = " << mk_pp(m_eqs[i].second->get_owner(), m) << "\n";
                           } 
                           tout << " ==> ";
-                          tout << enode_pp(x, ctx()) << " = " << enode_pp(y, ctx()) << "\n";
+                          tout << mk_pp(x->get_owner(), m) << " = " << mk_pp(y->get_owner(), m) << "\n";
                           );
 
                     // parameters are TBD.
@@ -3675,7 +3704,8 @@ public:
                 break;
             }
             case equality_source: 
-                out << enode_eq_pp(m_equalities[idx], ctx());
+                out << mk_pp(m_equalities[idx].first->get_owner(), m) << " = " 
+                    << mk_pp(m_equalities[idx].second->get_owner(), m) << "\n"; 
                 break;
             case definition_source: {
                 theory_var v = m_definitions[idx];
diff --git a/src/util/lp/monomial.h b/src/util/lp/monomial.h
index 1d40eb561..ab9bab14f 100644
--- a/src/util/lp/monomial.h
+++ b/src/util/lp/monomial.h
@@ -16,6 +16,7 @@ namespace nla {
         // fields
         lp::var_index          m_v;
         svector<lp::var_index> m_vs;
+        rational               m_coeff;
     public:
         // constructors
         monomial(lp::var_index v, unsigned sz, lp::var_index const* vs):
@@ -30,6 +31,8 @@ namespace nla {
         svector<lp::var_index>::const_iterator begin() const { return m_vs.begin(); }
         svector<lp::var_index>::const_iterator end() const { return m_vs.end(); }
         const svector<lp::var_index> vars() const { return m_vs; }
+        bool empty() const { return m_vs.empty(); }
+        const rational& get_coeff() const { return m_coeff; } 
     };
 
     typedef std::unordered_map<lp::var_index, rational> variable_map_type;
@@ -56,7 +59,7 @@ namespace nla {
             monomial(v, vs),
             m_coeff(coeff) {}
 
-       rational const& coeff() const { return m_coeff; }
+        rational const& coeff() const { return m_coeff; }
     };
 
 }
diff --git a/src/util/lp/nla_solver.h b/src/util/lp/nla_solver.h
index 8e04458e1..588cbca3f 100644
--- a/src/util/lp/nla_solver.h
+++ b/src/util/lp/nla_solver.h
@@ -24,6 +24,8 @@ Revision History:
 #include "util/params.h"
 #include "nlsat/nlsat_solver.h"
 #include "util/lp/lar_solver.h"
+#include "util/lp/monomial.h"
+
 namespace nla {
 struct ineq {
     lp::lconstraint_kind m_cmp;
@@ -36,7 +38,7 @@ struct ineq {
 };
 
 typedef vector<ineq> lemma;
-
+typedef vector<monomial> polynomial;
 // nonlinear integer incremental linear solver
 class solver {
     struct imp;