Add propagate/narrow for ule_constraint (#5214)

* Add helper to check whether pdd is univariate and linear

* Reorganize propagate/narrow of eq_constraint

* Implement propagate/narrow for ule constraints

* Also push trail instruction in push_viable

src/math/dd/dd_pdd.h

@@ -386,6 +386,8 @@ namespace dd {
         bool is_one() const { return m.is_one(root); }
         bool is_zero() const { return m.is_zero(root); }
         bool is_linear() const { return m.is_linear(root); }
+        /** Polynomial is of the form: a * x + b */
+        bool is_unilinear() const { return !is_val() && lo().is_val() && hi().is_val(); }
         bool is_unary() const { return !is_val() && lo().is_zero() && hi().is_val(); } 
         bool is_binary() const { return m.is_binary(root); }
         bool is_monomial() const { return m.is_monomial(root); }

src/math/polysat/eq_constraint.cpp

@@ -36,39 +36,9 @@ namespace polysat {
                 return true;
             }
         }        
-
-        LOG("Assignments: " << s.m_search);
-        auto q = p().subst_val(s.m_search);
-        LOG("Substituted: " << p() << " := " << q);
-        TRACE("polysat", tout << p() << " := " << q << "\n";);
-        if (q.is_zero()) 
-            return false;
-        if (q.is_never_zero()) {
-            LOG("Conflict (never zero under current assignment)");
-            s.set_conflict(*this);
-            return false;
-        }
-
         // at most one variable remains unassigned.
-        auto other_var = vars()[1 - idx];
-        SASSERT(!q.is_val() && q.var() == other_var);
-
-        // Detect and apply unit propagation.
-        if (try_narrow_with(q, s)) {
-            rational val;
-            switch (s.find_viable(other_var, val)) {
-            case dd::find_t::empty:
-                s.set_conflict(*this);
-                return false;
-            case dd::find_t::singleton:
-                s.propagate(other_var, val, *this);
-                return false;
-            case dd::find_t::multiple:
-                /* do nothing */
-                break;
-            }
-        }
 
+        narrow(s);
         return false;
     }
 
@@ -89,31 +59,37 @@ namespace polysat {
         return nullptr;
     }
 
-    bool eq_constraint::try_narrow_with(pdd const& q, solver& s) {
+    void eq_constraint::narrow(solver& s) {
-        if (q.is_linear() && q.free_vars().size() == 1) {
+        LOG("Assignment: " << s.m_search);
+        auto q = p().subst_val(s.m_search);
+        LOG("Substituted: " << p() << " := " << q);
+        if (q.is_zero())
+            return;
+        if (q.is_never_zero()) {
+            LOG("Conflict (never zero under current assignment)");
+            s.set_conflict(*this);
+            return;
+        }
+
+        if (q.is_unilinear()) {
             // a*x + b == 0
             pvar v = q.var();
             rational a = q.hi().val();
             rational b = q.lo().val();
             bddv const& x = s.var2bits(v).var();
             bdd xs = (a * x + b == rational(0));
-            s.intersect_viable(v, xs);
             s.push_cjust(v, this);
-            return true;
+            s.intersect_viable(v, xs);
-        }
-        // TODO: what other constraints can be extracted cheaply?
-        return false;
-    }
 
-    void eq_constraint::narrow(solver& s) {
+            rational val;
-        // NSB code review:
+            if (s.find_viable(v, val) == dd::find_t::singleton) {
-        // This should also use the current assignment so be similar to propagate.
+                s.propagate(v, val, *this);
-        // The idea is that narrow is invoked when the constraint is first added
+            }
-        // and also when the constraint is used in a conflict.
+
-        // When it is used in a conflict, there could be a partial assignment in s.m_search
+            return;
-        // that fixes variables in p().
+        }
-        // 
+
-        (void)try_narrow_with(p(), s);
+        // TODO: what other constraints can be extracted cheaply?
     }
 
     bool eq_constraint::is_always_false() {

src/math/polysat/eq_constraint.h

@@ -32,7 +32,6 @@ namespace polysat {
         bool is_always_false() override;
         bool is_currently_false(solver& s) override;
         void narrow(solver& s) override;
-        bool try_narrow_with(pdd const& q, solver& s);
     };
 
 }

src/math/polysat/solver.h

@@ -91,6 +91,7 @@ namespace polysat {
 
 
         void push_viable(pvar v) {
+            m_trail.push_back(trail_instr_t::viable_i);
             m_viable_trail.push_back(std::make_pair(v, m_viable[v]));
         }
 

src/math/polysat/ule_constraint.cpp

@@ -14,6 +14,7 @@ Author:
 
 #include "math/polysat/constraint.h"
 #include "math/polysat/solver.h"
+#include "math/polysat/log.h"
 
 namespace polysat {
 
@@ -22,6 +23,21 @@ namespace polysat {
     }
 
     bool ule_constraint::propagate(solver& s, pvar v) {
+        LOG_H3("Propagate " << s.m_vars[v] << " in " << *this);
+        SASSERT(!vars().empty());
+        unsigned idx = 0;
+        if (vars()[idx] != v)
+            idx = 1;
+        SASSERT(v == vars()[idx]);
+        // find other watch variable.
+        for (unsigned i = vars().size(); i-- > 2; ) {
+            if (!s.is_assigned(vars()[i])) {
+                std::swap(vars()[idx], vars()[i]);
+                return true;
+            }
+        }
+
+        narrow(s);
         return false;
     }
 
@@ -30,14 +46,77 @@ namespace polysat {
     }
 
     void ule_constraint::narrow(solver& s) {
+        LOG("Assignment: " << s.m_search);
+        auto p = lhs().subst_val(s.m_search);
+        LOG("Substituted LHS: " << lhs() << " := " << p);
+        auto q = rhs().subst_val(s.m_search);
+        LOG("Substituted RHS: " << rhs() << " := " << q);
+
+        if (is_always_false(p, q)) {
+            s.set_conflict(*this);
+            return;
+        }
+        if (p.is_val() && q.is_val()) {
+            SASSERT(p.val() <= q.val());
+            return;
+        }
+
+        pvar v = null_var;
+        rational a, b, c, d;
+        if (p.is_unilinear() && q.is_unilinear() && p.var() == q.var()) {
+            // a*x + b <=u c*x + d
+            v = p.var();
+            a = p.hi().val();
+            b = p.lo().val();
+            c = q.hi().val();
+            d = q.lo().val();
+        }
+        else if (p.is_unilinear() && q.is_val()) {
+            // a*x + b <=u d
+            v = p.var();
+            a = p.hi().val();
+            b = p.lo().val();
+            c = rational::zero();
+            d = q.val();
+        }
+        else if (p.is_val() && q.is_unilinear()) {
+            // b <=u c*x + d
+            v = q.var();
+            a = rational::zero();
+            b = p.val();
+            c = q.hi().val();
+            d = q.lo().val();
+        }
+        if (v != null_var) {
+            bddv const& x = s.var2bits(v).var();
+            bdd xs = (a * x + b <= c * x + d);
+            s.push_cjust(v, this);
+            s.intersect_viable(v, xs);
+
+            rational val;
+            if (s.find_viable(v, val) == dd::find_t::singleton) {
+                s.propagate(v, val, *this);
+            }
+
+            return;
+        }
+
+        // TODO: other cheap constraints possible?
+    }
+
+    bool ule_constraint::is_always_false(pdd const& lhs, pdd const& rhs) {
+        // TODO: other conditions (e.g. when forbidden interval would be full)
+        return lhs.is_val() && rhs.is_val() && !(lhs.val() <= rhs.val());
     }
 
     bool ule_constraint::is_always_false() {
-        return false;
+        return is_always_false(lhs(), rhs());
     }
 
     bool ule_constraint::is_currently_false(solver& s) {
-        return false;
+        auto p = lhs().subst_val(s.m_search);
+        auto q = rhs().subst_val(s.m_search);
+        return is_always_false(p, q);
     }
 
 }

src/math/polysat/ule_constraint.h

@@ -29,9 +29,12 @@ namespace polysat {
                     m_vars.push_back(v);
         }
         ~ule_constraint() override {}
+        pdd const& lhs() const { return m_lhs; }
+        pdd const& rhs() const { return m_rhs; }
         std::ostream& display(std::ostream& out) const override;
         bool propagate(solver& s, pvar v) override;
         constraint* resolve(solver& s, pvar v) override;
+        static bool is_always_false(pdd const& lhs, pdd const& rhs);
         bool is_always_false() override;
         bool is_currently_false(solver& s) override;
         void narrow(solver& s) override;