forbidden intervals for strict inequalities

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

src/math/polysat/explain.cpp

@@ -176,7 +176,6 @@ namespace polysat {
             core.reset();
             LOG_H3("Polynomial superposition " << eq << " " << c << " reduced to " << c2);
             if (c2.bvalue(s) == l_false) {
-                UNREACHABLE();
                 // TODO this loops or crashes depending on whether we
                 // return true or false.
                 core.insert(eq);

src/math/polysat/forbidden_intervals.cpp

@@ -52,12 +52,24 @@ namespace polysat {
         // We keep the e1, e2 around in case we need side conditions such as e1=b1, e2=b2.
         auto [ok1, a1, e1, b1] = linear_decompose(v, c->to_ule().lhs(), fi.side_cond);
         auto [ok2, a2, e2, b2] = linear_decompose(v, c->to_ule().rhs(), fi.side_cond);
-        if (!ok1 || !ok2 || (a1.is_zero() && a2.is_zero()))
+
+        _backtrack.released = true;
+                
+        // v > q
+        if (ok1 && !ok2 && match_non_zero(c, a1, b1, e1, fi))
+            return true;
+
+        // p > v
+        if (!ok1 && ok2 && match_non_max(c, a2, b2, e2, fi))
+            return true;
+            
+        if (!ok1 || !ok2 || (a1.is_zero() && a2.is_zero())) {
+            _backtrack.released = false;
             return false;
+        }
         SASSERT(b1.is_val());
         SASSERT(b2.is_val());
    
-        _backtrack.released = true;
 
         if (match_linear1(c, a1, b1, e1, a2, b2, e2, fi))
             return true;
@@ -250,6 +262,55 @@ namespace polysat {
         return false;
     }
 
+    /** 
+     * v > q
+     * forbidden interval for v is [0,1[
+     * 
+     * Generalizations todo:
+     *
+     * v - k > q
+     * forbidden interval for v is [k,k+1[
+     * 
+     * a*v - k > q, a odd
+     * forbidden interval for v is [a^-1*k, a^-1*k + 1[
+     */
+    bool forbidden_intervals::match_non_zero(
+        signed_constraint const& c,
+        rational const & a1, pdd const& b1, pdd const& e1,
+        fi_record& fi) {
+        if (a1.is_odd() && b1.is_zero() && !c.is_positive()) {
+            auto& m = e1.manager();
+            rational lo_val(0);
+            auto lo = m.zero();
+            rational hi_val(1);
+            auto hi = m.one();
+            fi.coeff = 1;
+            fi.interval = eval_interval::proper(lo, lo_val, hi, hi_val);
+            if (b1 != e1)
+                fi.side_cond.push_back(s.eq(b1, e1));
+            return true;
+        }
+        return false;
+    }
+
+    /**
+     * p > v
+     * forbidden interval for v is [-1,0[
+     * p > v + k
+     * forbidden interval for v is [-k-1,-k[
+     */
+    bool forbidden_intervals::match_non_max(
+        signed_constraint const& c,
+        rational const & a2, pdd const& b2, pdd const& e2,
+        fi_record& fi) {
+        if (a2.is_one() && b2.is_zero() && !c.is_positive()) {
+            // todo
+            
+        }
+        return false;
+    }
+
+
     void forbidden_intervals::add_non_unit_side_conds(fi_record& fi, pdd const& b1, pdd const& e1, pdd const& b2, pdd const& e2) {
         if (fi.coeff == 1)
             return;

src/math/polysat/forbidden_intervals.h

@@ -52,6 +52,14 @@ namespace polysat {
 
         void add_non_unit_side_conds(fi_record& fi, pdd const& b1, pdd const& e1, pdd const& b2, pdd const& e2);
 
+        bool match_non_zero(signed_constraint const& c,
+            rational const & a1, pdd const& b1, pdd const& e1,
+            fi_record& fi);
+
+        bool match_non_max(signed_constraint const& c,
+            rational const & a2, pdd const& b2, pdd const& e2,
+            fi_record& fi);
+
     public:
         forbidden_intervals(solver& s) :s(s) {}
         bool get_interval(signed_constraint const& c, pvar v, fi_record& fi);

src/math/polysat/solver.cpp

@@ -831,7 +831,7 @@ namespace polysat {
 
     // Add lemma to storage
     void solver::add_clause(clause& clause) {
-        LOG("Lemma: " << clause);
+        LOG((clause.is_redundant() ? "Lemma: ": "Aux: ") << clause);
         for (sat::literal lit : clause) {
             LOG("   Literal " << lit << " is: " << lit2cnstr(lit));
             // SASSERT(m_bvars.value(lit) != l_true);

src/math/polysat/ule_constraint.cpp

@@ -125,7 +125,9 @@ namespace polysat {
         auto p = lhs().subst_val(s.assignment());
         auto q = rhs().subst_val(s.assignment());
 
-        LOG_H3("Narrowing " << *this);
+        signed_constraint sc(this, is_positive);
+
+        LOG_H3("Narrowing " << sc);
         LOG("Assignment: " << assignments_pp(s));
         LOG("Substituted LHS: " << lhs() << " := " << p);
         LOG("Substituted RHS: " << rhs() << " := " << q);
@@ -141,26 +143,32 @@ namespace polysat {
         }
 
         pvar v = null_var;
+        bool first = true;
         if (p.is_unilinear())
             v = p.var();
         else if (q.is_unilinear())
-            v = q.var();
+            v = q.var(), first = false;
         else
             return;
 
-        signed_constraint sc(this, is_positive);
-        if (!s.m_viable.intersect(v, sc))
-            return;
-        rational val;
-        switch (s.m_viable.find_viable(v, val)) {
-        case dd::find_t::singleton:
-            s.propagate(v, val, sc); // TBD why is sc used as justification? It should be all of viable
-            break;
-        case dd::find_t::empty:
-            s.set_conflict(v);
-            break;
-        default:
-            break;
+    try_viable:
+        if (s.m_viable.intersect(v, sc)) {
+            rational val;
+            switch (s.m_viable.find_viable(v, val)) {
+            case dd::find_t::singleton:
+                s.propagate(v, val, sc); // TBD why is sc used as justification? It should be all of viable            
+                break;
+            case dd::find_t::empty:
+                s.set_conflict(v);
+                return;
+            default:
+                break;
+            }
+        }
+        if (first && q.is_unilinear() && q.var() != v) {
+            v = q.var();
+            first = false;
+            goto try_viable;
         }
     }