From 7a809fe4f0f566e7615f0a0f9605cc7b56b8d85b Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 24 May 2017 14:56:59 -0700
Subject: [PATCH] adding nra solver

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/theory_lra.cpp     | 25 +++++++++++++++++++++++++
 src/util/lp/lar_solver.cpp |  5 +++++
 src/util/lp/lar_solver.h   |  2 ++
 3 files changed, 32 insertions(+)

diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index addf37153..cd663f354 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -415,6 +415,31 @@ namespace smt {
             }
         }
 
+        void internalize_mul(app* t) {
+            SASSERT(a.is_mul(t));
+            mk_enode(t);
+            theory_var v = mk_var(t);
+            svector<lean::var_index> vars;
+            ptr_vector<expr> todo;
+            todo.push_back(t);
+            while (!todo.empty()) {
+                expr* n = todo.back();
+                todo.pop_back();
+                expr* n1, *n2;
+                if (a.is_mul(n, n1, n2)) {
+                    todo.push_back(n1);
+                    todo.push_back(n2);
+                }
+                else {
+                    if (!ctx().e_internalized(n)) {
+                        ctx().internalize(n, false);
+                    }
+                    vars.push_back(get_var_index(mk_var(n)));
+                }
+            }
+            // m_solver->add_monomial(get_var_index(v), vars);
+        }
+
         enode * mk_enode(app * n) {
             if (ctx().e_internalized(n)) {
                 return get_enode(n);
diff --git a/src/util/lp/lar_solver.cpp b/src/util/lp/lar_solver.cpp
index 97e1c102f..b3da4e8ba 100644
--- a/src/util/lp/lar_solver.cpp
+++ b/src/util/lp/lar_solver.cpp
@@ -1092,6 +1092,11 @@ final_check_status lar_solver::check_nra(nra_model_t& model, explanation_t& expl
     return m_nra->check(model, explanation);
 }
 
+void lar_solver::add_monomial(var_index v, svector<var_index> const& vars) {
+    m_nra->add_monomial(v, vars.size(), vars.c_ptr());
+}
+
+
 void lar_solver::get_infeasibility_explanation_for_inf_sign(
                                                             vector<std::pair<mpq, constraint_index>> & explanation,
                                                             const vector<std::pair<mpq, unsigned>> & inf_row,
diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h
index 9a80335ac..6937455ae 100644
--- a/src/util/lp/lar_solver.h
+++ b/src/util/lp/lar_solver.h
@@ -205,6 +205,8 @@ public:
     lp_status find_feasible_solution();
    
     final_check_status check_nra(nra_model_t& model, explanation_t& explanation);    
+
+    void add_monomial(var_index v, svector<var_index> const& vars);
     
     lp_status solve();