From 88ea90fbb95b67532dedeccfe75de358e7efb813 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 17 Aug 2018 18:52:52 -0700
Subject: [PATCH] handle output from niil_solver (#77)

* handle output from niil_solver

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

* add proper equality handling

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/theory_lra.cpp | 67 +++++++++++++++++++++++++++++++++++++++++-
 1 file changed, 66 insertions(+), 1 deletion(-)

diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index f9ced9981..c056358a8 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -1678,6 +1678,22 @@ public:
         return FC_GIVEUP;
     }
 
+    // create a eq atom representing "term = 0"
+    app_ref mk_eq(lp::lar_term const& term) {
+        rational offset(0);
+        u_map<rational> coeffs;
+        term2coeffs(term, coeffs, rational::one(), offset);
+        offset.neg();
+        bool isint = offset.is_int();
+        for (auto const& kv : coeffs) isint &= is_int(kv.m_key) && kv.m_value.is_int();
+        app_ref atom(m);
+        app_ref t = coeffs2app(coeffs, rational::zero(), isint);
+        atom = m.mk_eq(t, a.mk_numeral(offset, isint));
+        ctx().internalize(atom, true);
+        ctx().mark_as_relevant(atom.get());
+        return atom;
+    }
+
     // create a bound atom representing term >= k is lower_bound is true, and term <= k if it is false
     app_ref mk_bound(lp::lar_term const& term, rational const& k, bool lower_bound) {
         bool is_int = k.is_int();
@@ -2059,6 +2075,47 @@ public:
     niil::lemma m_lemma;
  
     lbool check_aftermath_niil(lbool r) {
+        TRACE("arith", tout << "niil: " << r << "\n";);
+        switch (r) {
+        case l_false: {            
+            literal_vector core;
+            for (auto const& ineq : m_lemma) {
+                bool is_lower = true, pos = true, is_eq = false;
+                
+                switch (ineq.m_cmp) {
+                case lp::LE: is_lower = false; pos = true;  break;
+                case lp::LT: is_lower = true;  pos = false; break;
+                case lp::GE: is_lower = true;  pos = true;  break;
+                case lp::GT: is_lower = true;  pos = false; break;
+                case lp::EQ: is_eq = true; pos = true; break;
+                case lp::NE: is_eq = true; pos = false; break;
+                default: UNREACHABLE();
+                }
+                app_ref atom(m);
+                if (is_eq) {
+                    atom = mk_eq(ineq.m_term);
+                }
+                else {
+                    // create term >= 0 (or term <= 0)
+                    atom = mk_bound(ineq.m_term, rational::zero(), is_lower);
+                }
+                literal lit(ctx().get_bool_var(atom), pos);
+                core.push_back(~lit);
+            }
+            std::cout << "the following conjunction should be unsat:\n";
+            ctx().display_literals_verbose(std::cout << "core ", core) << "\n";
+            display_evidence(std::cout, m_explanation); std::cout << "\n";
+            set_conflict(core);
+            break;
+        }
+        case l_true:
+            if (assume_eqs()) {
+                return l_false;
+            }
+            break;
+        case l_undef:
+            break;
+        }
         return r;
     }
 	
@@ -3116,9 +3173,17 @@ public:
     }
 
     void set_conflict1() {
+        literal_vector core;
+        set_conflict(core);
+    }
+
+    void set_conflict(literal_vector const& core) {
         m_eqs.reset();
         m_core.reset();
         m_params.reset();
+        for (literal lit : core) {
+            m_core.push_back(lit);
+        }
         // m_solver->shrink_explanation_to_minimum(m_explanation); // todo, enable when perf is fixed
         /*
           static unsigned cn = 0;
@@ -3135,7 +3200,7 @@ public:
                 set_evidence(ev.second);
             }
         }
-        //        SASSERT(validate_conflict());
+        // SASSERT(validate_conflict());
         dump_conflict();
         ctx().set_conflict(
             ctx().mk_justification(