From db54cab8b26d445f23204af9da4a642d4f412f1b Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 23 May 2017 16:26:46 -0700
Subject: [PATCH] initial skeletons for nra solver

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/util/lp/nra_solver.cpp | 38 +++++++++++++++++++++++++++++++++++++-
 1 file changed, 37 insertions(+), 1 deletion(-)

diff --git a/src/util/lp/nra_solver.cpp b/src/util/lp/nra_solver.cpp
index cb47b36e5..08b17030c 100644
--- a/src/util/lp/nra_solver.cpp
+++ b/src/util/lp/nra_solver.cpp
@@ -10,11 +10,35 @@ namespace lp {
 
     struct nra_solver::imp {
         lean::lar_solver& s;
-        imp(lean::lar_solver& s): s(s) {}
+
+        svector<lean::var_index>         m_vars;
+        vector<svector<lean::var_index>> m_monomials;
+        unsigned_vector                  m_lim;
+
+        imp(lean::lar_solver& s): s(s) {
+            m_lim.push_back(0);
+        }
 
         lean::final_check_status check_feasible() {
             return lean::final_check_status::GIVEUP;
         }
+
+        void add(lean::var_index v, unsigned sz, lean::var_index const* vs) {
+            m_vars.push_back(v);
+            m_monomials.push_back(svector<lean::var_index>(sz, vs));
+        }
+
+        void push() {
+            m_lim.push_back(m_vars.size());
+        }
+
+        void pop(unsigned n) {
+            SASSERT(n < m_lim.size());
+            m_lim.shrink(m_lim.size() - n);       
+            m_vars.shrink(m_lim.back());
+            m_monomials.shrink(m_lim.back());
+        }
+
     };
 
     nra_solver::nra_solver(lean::lar_solver& s) {
@@ -25,7 +49,19 @@ namespace lp {
         dealloc(m_imp);
     }
 
+    void nra_solver::add_monomial(lean::var_index v, unsigned sz, lean::var_index const* vs) {
+        m_imp->add(v, sz, vs);
+    }
+
     lean::final_check_status nra_solver::check_feasible() {
         return m_imp->check_feasible();
     }
+
+    void nra_solver::push() {
+        m_imp->push();
+    }
+
+    void nra_solver::pop(unsigned n) {
+        m_imp->pop(n);
+    }
 }