From 8ecd8a2a521d01e3fff9c9789fd3904628b94115 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 23 May 2017 18:07:58 -0700
Subject: [PATCH] Dev (#50)

* initial skeletons for nra solver

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

* initial skeletons for nra solver

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 contrib/cmake/src/util/lp/CMakeLists.txt |  3 +-
 src/util/lp/nra_solver.cpp               | 67 ++++++++++++++++++++++++
 src/util/lp/nra_solver.h                 | 47 +++++++++++++++++
 3 files changed, 116 insertions(+), 1 deletion(-)
 create mode 100644 src/util/lp/nra_solver.cpp
 create mode 100644 src/util/lp/nra_solver.h

diff --git a/contrib/cmake/src/util/lp/CMakeLists.txt b/contrib/cmake/src/util/lp/CMakeLists.txt
index ec9a2e137..75051d68c 100644
--- a/contrib/cmake/src/util/lp/CMakeLists.txt
+++ b/contrib/cmake/src/util/lp/CMakeLists.txt
@@ -19,8 +19,9 @@ z3_add_component(lp
     lp_solver_instances.cpp
     lu_instances.cpp
     matrix_instances.cpp
+    nra_solver.cpp
     permutation_matrix_instances.cpp
-	quick_xplain.cpp
+    quick_xplain.cpp
     row_eta_matrix_instances.cpp
     scaler_instances.cpp
     sparse_matrix_instances.cpp
diff --git a/src/util/lp/nra_solver.cpp b/src/util/lp/nra_solver.cpp
new file mode 100644
index 000000000..08b17030c
--- /dev/null
+++ b/src/util/lp/nra_solver.cpp
@@ -0,0 +1,67 @@
+/*
+  Copyright (c) 2017 Microsoft Corporation
+  Author: Lev Nachmanson
+*/
+
+#pragma once
+#include "util/lp/nra_solver.h"
+
+namespace lp {
+
+    struct nra_solver::imp {
+        lean::lar_solver& 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) {
+        m_imp = alloc(imp, s);
+    }
+
+    nra_solver::~nra_solver() {
+        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);
+    }
+}
diff --git a/src/util/lp/nra_solver.h b/src/util/lp/nra_solver.h
new file mode 100644
index 000000000..bae76b0d1
--- /dev/null
+++ b/src/util/lp/nra_solver.h
@@ -0,0 +1,47 @@
+/*
+  Copyright (c) 2017 Microsoft Corporation
+  Author: Lev Nachmanson
+*/
+
+#pragma once
+#include "util/vector.h"
+#include "util/lp/lp_settings.h"
+#include "util/lp/lar_solver.h"
+
+namespace lean {
+    class lar_solver;
+}
+
+namespace lp {
+
+    class nra_solver {
+        struct imp;
+        imp* m_imp;
+
+    public:
+
+        nra_solver(lean::lar_solver& s);
+        
+        ~nra_solver();
+
+        /*
+          \brief Add a definition v = vs[0]*vs[1]*...*vs[sz-1]
+          The variable v is equal to the product of variables vs.
+        */
+        void add_monomial(lean::var_index v, unsigned sz, lean::var_index const* vs);
+
+        /*
+          \brief Check feasiblity of linear constraints augmented by polynomial definitions
+          that are added.
+         */
+        lean::final_check_status check_feasible();
+
+        /*
+          \brief push and pop scope. 
+          Monomial definitions are retraced when popping scope.
+        */
+        void push();
+        
+        void pop(unsigned n);
+    };
+}