From 032a4efdb60e9a82367b07eecb54a5f2d4f4a877 Mon Sep 17 00:00:00 2001
From: Lev <levnach@hotmail.com>
Date: Fri, 10 Aug 2018 14:51:21 +0800
Subject: [PATCH] work on switcher

Signed-off-by: Lev <levnach@hotmail.com>
---
 src/smt/theory_lra.cpp | 35 +++++++++++++++++++++++++++++++++--
 1 file changed, 33 insertions(+), 2 deletions(-)

diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index de3bff1b5..148624b5a 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -264,6 +264,37 @@ class theory_lra::imp {
     bool                     m_use_nra_model;
     scoped_ptr<scoped_anum>  m_a1, m_a2;
 
+    struct switcher {
+        theory_lra::imp& m_th_imp;
+        scoped_ptr<nra::solver>*  m_nra;
+        scoped_ptr<niil::solver>* m_niil;
+        bool m_use_niil;
+        switcher(theory_lra::imp& i): m_th_imp(i), m_nra(nullptr), m_niil(nullptr) {
+        }
+        void push() {
+            if (m_use_niil) {
+                if (m_niil != nullptr)
+                    (*m_niil)->push();
+            }
+            else {
+                if (m_nra != nullptr)
+                    (*m_nra)->push();
+            }
+        }
+
+        void add_monomial(lp::var_index v, unsigned sz, lp::var_index const* vs) {
+            if (m_use_niil) {
+                m_th_imp.ensure_niil();
+                (*m_niil)->add_monomial(v, sz, vs);
+            }
+            else {
+                m_th_imp.ensure_nra();
+                (*m_nra)->add_monomial(v, sz, vs);
+            }
+        }
+ 
+    };
+
     // integer arithmetic
     scoped_ptr<lp::int_solver> m_lia;
 
@@ -328,7 +359,7 @@ class theory_lra::imp {
 
         m_solver->settings().m_int_run_gcd_test = ctx().get_fparams().m_arith_gcd_test;
         m_solver->settings().set_random_seed(ctx().get_fparams().m_random_seed);
-        m_use_niil = lp.niil();
+        m_switcher.m_use_niil = m_use_niil = lp.niil();
         m_lia = alloc(lp::int_solver, m_solver.get());
         get_one(true);
         get_zero(true);
@@ -1005,7 +1036,7 @@ public:
         s.m_underspecified_lim = m_underspecified.size();
         s.m_var_trail_lim = m_var_trail.size();
         m_solver->push();
-        if (m_nra) m_nra->push();
+        m_switcher.push();
     }
 
     void pop_scope_eh(unsigned num_scopes) {