work on niil

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

src/smt/theory_lra.cpp

@@ -272,20 +272,6 @@ class theory_lra::imp {
         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) {
-                    std::cout << "check niil\n";
-                    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)
@@ -2070,10 +2056,12 @@ public:
         return r;
     }
 
+    niil::lemma m_lemma;
+ 
     lbool check_aftermath_niil(lbool r) {
         return r;
     }
-    
+	
     lbool check_nra() {
         m_use_nra_model = false;
         if (m.canceled()) {
@@ -2083,7 +2071,8 @@ public:
         if (!m_nra && !m_niil) return l_true;
         if (!m_switcher.need_check()) return l_true;
         m_a1 = nullptr; m_a2 = nullptr;
-        lbool r = m_switcher.check(m_explanation);
+        
+        lbool r = m_nra? m_nra->check(m_explanation): m_niil->check(m_lemma);
         return m_nra? check_aftermath_nra(r) : check_aftermath_niil(r);
     }
 

src/util/lp/niil_solver.cpp

@@ -59,7 +59,7 @@ struct solver::imp {
         return r == model_val;
     }
     
-    lbool check(lp::explanation_t& ex) {
+    lbool check(lemma& ) {
         lp_assert(m_lar_solver.get_status() == lp::lp_status::OPTIMAL);
         svector<unsigned> to_refine;
         for (unsigned i = 0; i < m_monomials.size(); i++) {
@@ -80,8 +80,8 @@ void solver::add_monomial(lp::var_index v, unsigned sz, lp::var_index const* vs)
 
 bool solver::need_check() { return true; }
 
-lbool solver::check(lp::explanation_t& ex) {
-    return m_imp->check(ex);
+lbool solver::check(lemma& l) {
+    return m_imp->check(l);
 }
 
 

src/util/lp/niil_solver.h

@@ -25,6 +25,13 @@ Revision History:
 #include "nlsat/nlsat_solver.h"
 #include "util/lp/lar_solver.h"
 namespace niil {
+struct ineq {
+    lp::lconstraint_kind m_cmp;
+    lp::lar_term         m_term;
+};
+
+typedef vector<ineq> lemma;
+
 // nonlinear integer incremental linear solver
 class solver {
 public:
@@ -37,6 +44,6 @@ public:
     void push();
     void pop(unsigned scopes);
     bool need_check();
-    lbool check(lp::explanation_t& ex);
+    lbool check(lemma&);
 };
 }

src/util/lp/ul_pair.h

@@ -27,9 +27,7 @@ Revision History:
 
 namespace lp {
 
-enum lconstraint_kind {
-    LE = -2, LT = -1 , GE = 2, GT = 1, EQ = 0
-};
+enum lconstraint_kind { LE = -2, LT = -1 , GE = 2, GT = 1, EQ = 0, NE = 3 };
 
 
 inline bool kind_is_strict(lconstraint_kind kind) { return kind == LT || kind == GT;}