work on switcher

Signed-off-by: Lev <levnach@hotmail.com>

src/smt/theory_lra.cpp

@@ -271,6 +271,31 @@ class theory_lra::imp {
         bool m_use_niil;
         switcher(theory_lra::imp& i): m_th_imp(i), m_nra(nullptr), m_niil(nullptr) {
         }
+
+        lbool check(lp::explanation_t& ex) {
+            if (m_use_niil) {
+                if (m_niil != nullptr)
+                    return (*m_niil)->check(ex);
+            }
+            else {
+                if (m_nra != nullptr)
+                    return (*m_nra)->check(ex);
+            }
+            return l_undef;
+        }
+        
+        bool need_check() {
+            if (m_use_niil) {
+                if (m_niil != nullptr)
+                    return (*m_niil)->need_check();
+            }
+            else {
+                if (m_nra != nullptr)
+                    return (*m_nra)->need_check();
+            }
+            return false;
+        }
+        
         void push() {
             if (m_use_niil) {
                 if (m_niil != nullptr)
@@ -1591,6 +1616,7 @@ public:
 
     bool is_eq(theory_var v1, theory_var v2) {
         if (m_use_nra_model) {
+            lp_assert(!m_use_niil);
             return m_nra->am().eq(nl_value(v1, *m_a1), nl_value(v2, *m_a2));
         }
         else {
@@ -2028,9 +2054,9 @@ public:
             return l_undef;
         }
         if (!m_nra) return l_true;
-        if (!m_nra->need_check()) return l_true;
+        if (!m_switcher.need_check()) return l_true;
         m_a1 = nullptr; m_a2 = nullptr;
-        lbool r = m_nra->check(m_explanation);
+        lbool r = m_switcher.check(m_explanation);
         m_a1 = alloc(scoped_anum, m_nra->am());
         m_a2 = alloc(scoped_anum, m_nra->am());
         switch (r) {

src/util/lp/niil_solver.cpp

@@ -21,6 +21,9 @@ Revision History:
 #include "util/map.h"
 namespace niil {
 struct solver::imp {
+
+    vector<mon_eq>         m_monomials;
+    unsigned_vector        m_monomials_lim;
     imp(lp::lar_solver& s, reslimit& lim, params_ref const& p)
     // :
         // s(s), 
@@ -28,15 +31,39 @@ struct solver::imp {
         // m_params(p)
     {
     }
+
+    void add(lp::var_index v, unsigned sz, lp::var_index const* vs) {
+        m_monomials.push_back(mon_eq(v, sz, vs));
+    }
+
+    void push() {
+        m_monomials_lim.push_back(m_monomials.size());
+    }
+    void pop(unsigned n) {
+        if (n == 0) return;
+        m_monomials.shrink(m_monomials_lim[m_monomials_lim.size() - n]);
+        m_monomials_lim.shrink(m_monomials_lim.size() - n);       
+    }
 };
 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) {
+bool solver::need_check() { return true; }
+
+lbool solver::check(lp::explanation_t& ex) {
+    lp_assert(false);
+    return l_undef;
+}
+
+
+void solver::push(){
+    m_imp->push();
+}
+void solver::pop(unsigned n) {
+    m_imp->pop(n);
 }
 
-void solver::push(){ }
 
 solver::solver(lp::lar_solver& s, reslimit& lim, params_ref const& p) {
     m_imp = alloc(imp, s, lim, p);

src/util/lp/niil_solver.h

@@ -36,5 +36,7 @@ public:
     imp* get_imp();
     void push();
     void pop(unsigned scopes);
+    bool need_check();
+    lbool check(lp::explanation_t& ex);
 };
 }