conflict

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

src/math/polysat/ule_constraint.cpp

@@ -129,6 +129,31 @@ namespace polysat {
             return;
         }
 
+#if 0
+        // setup with viable2:
+        // we no longer need cjust
+        pvar v = null_var;
+        if (p.is_unilinear())
+            v = p.var();
+        else if (q.is_unilinear())
+            v = q.var();
+        if (v != null_var) {
+            signed_constraint sc(this, is_positive);
+            s.m_viable2.intersect(v, sc);
+            rational val;
+            switch (s.m_viable2.find_viable(v, val)) {
+            case dd::find_t::singleton:
+                s.propagate(v, val, sc);
+                break;
+            case dd::find_t::empty:
+                s.set_conflict(v);
+                break;
+            default:
+                break;
+            }                
+        }
+#else
+
         // p <= 0, e.g., p == 0
         if (q.is_zero() && p.is_unilinear()) {
             // a*x + b == 0
@@ -184,6 +209,7 @@ namespace polysat {
         }
 
         // TODO: other cheap constraints possible?
+#endif
     }
 
     bool ule_constraint::is_always_false(bool is_positive, pdd const& lhs, pdd const& rhs) const {

src/math/polysat/viable2.cpp

@@ -246,6 +246,42 @@ namespace polysat {
             return dd::find_t::multiple;
     }
 
+    void viable2::get_core(pvar v, conflict& core) {
+        core.reset();
+        auto* e = m_viable[v];
+        entry* first = e;
+        SASSERT(e);
+        SASSERT(!has_viable(v));
+        do {
+            // Build constraint: upper bound of each interval is not contained in the next interval,
+            // using the equivalence:  t \in [l;h[  <=>  t-l < h-l
+            entry* n = e->next();
+            if (!e->interval.is_full()) {
+                auto const& hi = e->interval.hi();
+                auto const& next_lo = n->interval.lo();
+                auto const& next_hi = n->interval.hi();
+                auto lhs = hi - next_lo;
+                auto rhs = next_hi - next_lo;
+                signed_constraint c = s.m_constraints.ult(lhs, rhs);
+                core.insert(c);
+            }
+            for (auto sc : e->side_cond)
+                core.insert(sc);
+            core.insert(e->src);
+            e = n;
+        }             
+        while (e != first);
+
+        core.set_bailout();
+        for (auto c : core) {
+            if (c.bvalue(s) == l_false) {
+                core.reset();
+                core.set(~c);
+                break;
+            }
+        }
+    }
+
     void viable2::log(pvar v) {
         auto* e = m_viable[v];
         if (!e)

src/math/polysat/viable2.h

@@ -21,11 +21,9 @@ Author:
 #include "util/dlist.h"
 #include "util/small_object_allocator.h"
 #include "math/polysat/types.h"
+#include "math/polysat/conflict.h"
 #include "math/polysat/constraint.h"
 
-
-
-
 namespace polysat {
 
     class solver;
@@ -95,6 +93,12 @@ namespace polysat {
          */
         dd::find_t find_viable(pvar v, rational & val);
 
+        /**
+        * Retrieve the unsat core for v.
+        * \pre there are no viable values for v
+        */
+        void get_core(pvar v, conflict& core);
+
         /** Log all viable values for the given variable.
          * (Inefficient, but useful for debugging small instances.)
          */