From 253facff465bc3fad06fccf00febbba1aa1ae39e Mon Sep 17 00:00:00 2001
From: Lev <levnach@hotmail.com>
Date: Fri, 10 Aug 2018 15:17:13 +0800
Subject: [PATCH] work on switcher

Signed-off-by: Lev <levnach@hotmail.com>
---
 src/smt/theory_lra.cpp      | 39 ++++++++++++++++++++++++++-----------
 src/util/lp/niil_solver.cpp |  6 ++++++
 src/util/lp/niil_solver.h   |  3 +++
 3 files changed, 37 insertions(+), 11 deletions(-)

diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 148624b5a..5a44ff6b1 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -282,6 +282,18 @@ class theory_lra::imp {
             }
         }
 
+        void pop(unsigned scopes) {
+            if (m_use_niil) {
+                if (m_niil != nullptr)
+                    (*m_niil)->pop(scopes);
+            }
+            else {
+                if (m_nra != nullptr)
+                    (*m_nra)->pop(scopes);
+            }
+        }
+
+        
         void add_monomial(lp::var_index v, unsigned sz, lp::var_index const* vs) {
             if (m_use_niil) {
                 m_th_imp.ensure_niil();
@@ -398,10 +410,21 @@ class theory_lra::imp {
         return add_const(1, is_int ? m_one_var : m_rone_var, is_int);
     }
 
-    lp::var_index get_zero(bool is_int) {
-        return add_const(0, is_int ? m_zero_var : m_rzero_var, is_int);
+    lp::var_index get_zero() {
+        add_const(0, m_zero_var);
+        return m_zero_var;
+    }
+    void ensure_niil() {
+        if (!m_niil) {
+            std::cout << "ensure_niil\n";
+            m_niil = alloc(niil::solver, *m_solver.get(), m.limit(), ctx().get_params());
+            m_switcher.m_niil = &m_niil;
+            for (auto const& _s : m_scopes) {
+                (void)_s;
+                m_niil->push();
+            }
+        }
     }
-
 
     void found_not_handled(expr* n) {
         m_not_handled = n;
@@ -598,13 +621,7 @@ class theory_lra::imp {
         }
         TRACE("arith", tout << "v" << v << "(" << get_var_index(v) << ") := " << mk_pp(t, m) << " " << _has_var << "\n";);
         if (!_has_var) {
-            if (m_use_niil) {
-                ensure_niil();
-                m_niil->add_monomial(get_var_index(v), vars.size(), vars.c_ptr());
-            } else {
-                ensure_nra();
-                m_nra->add_monomial(get_var_index(v), vars.size(), vars.c_ptr());
-            }
+            m_switcher.add_monomial(get_var_index(v), vars.size(), vars.c_ptr());
         }
     }
 
@@ -1068,7 +1085,7 @@ public:
         // VERIFY(l_false != make_feasible());
         m_new_bounds.reset();
         m_to_check.reset();
-        if (m_nra) m_nra->pop(num_scopes);
+        m_switcher.pop(num_scopes);
         TRACE("arith", tout << "num scopes: " << num_scopes << " new scope level: " << m_scopes.size() << "\n";);
     }
 
diff --git a/src/util/lp/niil_solver.cpp b/src/util/lp/niil_solver.cpp
index 526de29b7..14038d698 100644
--- a/src/util/lp/niil_solver.cpp
+++ b/src/util/lp/niil_solver.cpp
@@ -32,6 +32,12 @@ struct solver::imp {
 void solver::add_monomial(lp::var_index v, unsigned sz, lp::var_index const* vs) {
     std::cout << "called add_monomial\n";
 }
+
+void solver::pop(unsigned) {
+}
+
+void solver::push(){ }
+
 solver::solver(lp::lar_solver& s, reslimit& lim, params_ref const& p) {
     m_imp = alloc(imp, s, lim, p);
 }
diff --git a/src/util/lp/niil_solver.h b/src/util/lp/niil_solver.h
index 653e52feb..d2e73721e 100644
--- a/src/util/lp/niil_solver.h
+++ b/src/util/lp/niil_solver.h
@@ -33,5 +33,8 @@ public:
     void add_monomial(lp::var_index v, unsigned sz, lp::var_index const* vs);
     solver(lp::lar_solver& s, reslimit& lim, params_ref const& p);
 
+    imp* get_imp();
+    void push();
+    void pop(unsigned scopes);
 };
 }