overflow example works

- introduce weak/strong eval to temper unit propagation to use only weak evaluation.
- harness the amount of interval propagation provided on overflow constraints
- weak evaluation on overflow constraints is now trivialized
- viable insertion also does conflict detection

src/sat/smt/polysat/constraints.cpp

@@ -103,13 +103,13 @@ namespace polysat {
         return true;
     }
 
-    lbool signed_constraint::eval(assignment& a) const {
+    lbool signed_constraint::weak_eval(assignment& a) const {
-        lbool r = m_constraint->eval(a);
+        lbool r = m_constraint->weak_eval(a);
         return m_sign ? ~r : r;
     }
 
-    lbool signed_constraint::eval_unfold(assignment& a) const {
+    lbool signed_constraint::strong_eval(assignment& a) const {
-        lbool r = m_constraint->eval_unfold(a);
+        lbool r = m_constraint->strong_eval(a);
         return m_sign ? ~r : r;
     }
 
@@ -118,12 +118,4 @@ namespace polysat {
         return out << *m_constraint;        
     }
 
-    bool signed_constraint::is_currently_true(core& c) const { 
-        return eval(c.get_assignment()) == l_true; 
-    }
-
-    bool signed_constraint::is_currently_false(core& c) const { 
-        return eval(c.get_assignment()) == l_false; 
-    }
-
 }

src/sat/smt/polysat/constraints.h

@@ -44,8 +44,8 @@ namespace polysat {
         virtual std::ostream& display(std::ostream& out, lbool status) const = 0;
         virtual std::ostream& display(std::ostream& out) const = 0;
         virtual lbool eval() const = 0;
-        virtual lbool eval(assignment const& a) const = 0;
+        virtual lbool weak_eval(assignment const& a) const = 0;
-        virtual lbool eval_unfold(assignment const& a) const { return eval(a); }
+        virtual lbool strong_eval(assignment const& a) const = 0;
         virtual void activate(core& c, bool sign, dependency const& d) = 0;
         virtual void propagate(core& c, lbool value, dependency const& d) = 0;
         virtual bool is_linear() const { return false; }
@@ -76,11 +76,9 @@ namespace polysat {
         void propagate(core& c, lbool value, dependency const& d) { m_constraint->propagate(c, value, d); }
         bool is_always_true() const { return eval() == l_true; }
         bool is_always_false() const { return eval() == l_false; }
-        bool is_currently_true(core& c) const;
-        bool is_currently_false(core& c) const;
         bool is_linear() const { return m_constraint->is_linear(); }
-        lbool eval(assignment& a) const;
+        lbool weak_eval(assignment& a) const;
-        lbool eval_unfold(assignment& a) const;
+        lbool strong_eval(assignment& a) const;
         lbool eval() const { return m_sign ? ~m_constraint->eval() : m_constraint->eval();}
         ckind_t op() const { return m_op; }
         bool is_ule() const { return m_op == ule_t; }

src/sat/smt/polysat/core.cpp

@@ -257,7 +257,7 @@ namespace polysat {
 
 #if 0        
         // If no saturation propagation was possible, explain the conflict using the variable assignment.
-        m_unsat_core = explain_eval_unfold(get_constraint(conflict_idx));
+        m_unsat_core = explain_strong_eval(get_constraint(conflict_idx));
         m_unsat_core.push_back(get_dependency(conflict_idx));
         s.set_conflict(m_unsat_core, "polysat-bail-out-conflict");
         decay_activity();
@@ -333,10 +333,10 @@ namespace polysat {
                 return;
             v = w;
         }
-        if (v != null_var && !m_viable.add_unitary(v, idx))
+        if (v != null_var && !m_viable.add_unitary(v, idx, m_values[v]))
             viable_conflict(v);
-        else if (v == null_var && sc.is_currently_false(*this)) {
+        else if (v == null_var && weak_eval(sc) == l_false) {
-            auto ex = explain_eval(sc);
+            auto ex = explain_weak_eval(sc);
             ex.push_back(dep);
             s.set_conflict(ex, "infeasible propagation");
         }
@@ -389,7 +389,7 @@ namespace polysat {
             if (!is_assigned(v0) || is_assigned(v1))
                 continue;
             // detect unitary, add to viable, detect conflict?
-            if (value != l_undef && !m_viable.add_unitary(v1, { idx }))
+            if (value != l_undef && !m_viable.add_unitary(v1, { idx }, m_values[v]))
                 viable_conflict(v1);
         }
         SASSERT(m_watch[v].size() == sz && "size of watch list was not changed");
@@ -402,14 +402,14 @@ namespace polysat {
     */
     void core::propagate_eval(constraint_id idx) {
         auto [sc, d, value] = m_constraint_index[idx.id];
-        switch (eval(sc)) {
+        switch (weak_eval(sc)) {
         case l_false:
             if (value != l_false)
-                s.propagate(d, true, explain_eval(sc), "eval-propagate");
+                s.propagate(d, true, explain_weak_eval(sc), "eval-propagate");
             break;
         case l_true:
             if (value != l_true)
-                s.propagate(d, false, explain_eval(sc), "eval-propagate");
+                s.propagate(d, false, explain_weak_eval(sc), "eval-propagate");
             break;
         default:
             break;
@@ -424,13 +424,13 @@ namespace polysat {
     }
 
     void core::propagate(constraint_id id, signed_constraint& sc, lbool value, dependency const& d) {
-        lbool eval_value = eval(sc);
+        lbool eval_value = weak_eval(sc);
         if (eval_value == l_undef)
             sc.propagate(*this, value, d);
         else if (value == l_undef)
-            s.propagate(d, eval_value != l_true, explain_eval(sc), "constraint-propagate");
+            s.propagate(d, eval_value != l_true, explain_weak_eval(sc), "constraint-propagate");
         else if (value != eval_value) {
-            m_unsat_core = explain_eval(sc);
+            m_unsat_core = explain_weak_eval(sc);
             m_unsat_core.push_back(m_constraint_index[id.id].d);
             s.set_conflict(m_unsat_core, "polysat-constraint-core");
             decay_activity();
@@ -493,7 +493,7 @@ namespace polysat {
         s.trail().push(unassign(*this, index.id));
     }
 
-    dependency_vector core::explain_eval(unsigned_vector const& vars) {
+    dependency_vector core::explain_weak_eval(unsigned_vector const& vars) {
         dependency_vector deps;
         for (auto v : vars) {
             if (is_assigned(v)) {
@@ -504,20 +504,20 @@ namespace polysat {
         return deps;
     }
 
-    dependency_vector core::explain_eval(signed_constraint const& sc) {
+    dependency_vector core::explain_weak_eval(signed_constraint const& sc) {
-        return explain_eval(sc.vars());
+        return explain_weak_eval(sc.vars());
     }
 
-    dependency_vector core::explain_eval_unfold(signed_constraint const& sc) {
+    dependency_vector core::explain_strong_eval(signed_constraint const& sc) {
-        return explain_eval(sc.unfold_vars());
+        return explain_weak_eval(sc.unfold_vars());
     }
 
-    lbool core::eval(signed_constraint const& sc) { 
+    lbool core::weak_eval(signed_constraint const& sc) { 
-        return sc.eval(m_assignment);
+        return sc.weak_eval(m_assignment);
     }
 
-    lbool core::eval_unfold(signed_constraint const& sc) {
+    lbool core::strong_eval(signed_constraint const& sc) {
-        return sc.eval_unfold(m_assignment);
+        return sc.strong_eval(m_assignment);
     }
 
     pdd core::subst(pdd const& p) { 
@@ -579,12 +579,12 @@ namespace polysat {
         return sc;
     }
 
-    lbool core::eval(constraint_id id) {
+    lbool core::weak_eval(constraint_id id) {
-        return get_constraint(id).eval(m_assignment);
+        return get_constraint(id).weak_eval(m_assignment);
     }
 
-    lbool core::eval_unfold(constraint_id id) {
+    lbool core::strong_eval(constraint_id id) {
-        return get_constraint(id).eval_unfold(m_assignment);
+        return get_constraint(id).strong_eval(m_assignment);
     }
 
     void core::inc_activity(pvar v) {

src/sat/smt/polysat/core.h

@@ -86,7 +86,7 @@ namespace polysat {
         void propagate_assignment(pvar v, rational const& value, dependency dep);
         void propagate_activation(constraint_id idx, signed_constraint& sc, dependency dep);
         void propagate(constraint_id id, signed_constraint& sc, lbool value, dependency const& d);
-        dependency_vector explain_eval(unsigned_vector const& vars);
+        dependency_vector explain_weak_eval(unsigned_vector const& vars);
 
         void add_watch(unsigned idx, unsigned var);
 
@@ -169,13 +169,13 @@ namespace polysat {
         constraint_id_vector const& assigned_constraints() const { return m_prop_queue; }
         dependency get_dependency(constraint_id idx) const;
         // dependency_vector get_dependencies(constraint_id_vector const& ids) const;
-        lbool eval(constraint_id id);
+        lbool weak_eval(constraint_id id);
-        lbool eval_unfold(constraint_id id);
+        lbool strong_eval(constraint_id id);
         dependency propagate(signed_constraint const& sc, dependency_vector const& deps) { return s.propagate(sc, deps, nullptr); }
-        lbool eval(signed_constraint const& sc);
+        lbool weak_eval(signed_constraint const& sc);
-        lbool eval_unfold(signed_constraint const& sc);
+        lbool strong_eval(signed_constraint const& sc);
-        dependency_vector explain_eval(signed_constraint const& sc);
+        dependency_vector explain_weak_eval(signed_constraint const& sc);
-        dependency_vector explain_eval_unfold(signed_constraint const& sc);
+        dependency_vector explain_strong_eval(signed_constraint const& sc);
         svector<pvar> find_conflict_variables(constraint_id idx);
         bool inconsistent() const;
 

src/sat/smt/polysat/forbidden_intervals.cpp

@@ -102,13 +102,31 @@ namespace polysat {
                 fi.side_cond.push_back(s.cs().ule(e2, 1));
             }
             else {
+                // A := div(2^N - 1, b2.val())
+                //   := hi_val - 1
+                // max B such that A*B < 2^N
+                //     := ceil(2^N / A) - 1
+                //     := div(2^N + A - 1, A) - 1
+                //     := div(bound + A, A) - 1
                 // [0, div(bound, b2.val()) + 1[
+                rational A = div(bound, b2.val());
+                rational B = div(bound + A, A) - 1;
+
+                if (A >= 4 && B >= 4) {
+                    _backtrack.released = false;
+                    return false;
+                }
                 rational lo_val(0);
-                rational hi_val(div(bound, b2.val()) + 1);
+                rational hi_val = A + 1;
                 pdd lo = m.mk_val(lo_val);
                 pdd hi = m.mk_val(hi_val);
+                
+                SASSERT(b2.val() <= B);
+                SASSERT(A * B <= bound);
+                SASSERT((A + 1) * B > bound);
+                SASSERT(A * (B + 1) > bound);
                 fi.interval = eval_interval::proper(lo, lo_val, hi, hi_val);
-                fi.side_cond.push_back(s.cs().ule(e2, b2.val()));
+                fi.side_cond.push_back(s.cs().ule(e2, B));                
             }
 
         }
@@ -119,8 +137,23 @@ namespace polysat {
             }
             else {
                 // [div(bound, b2.val()) + 1, 0[
-                rational lo_val(div(bound, b2.val()) + 1);
+                // A := div(2^N - 1, b2.val())
+                // min B . A*B >= 2^N
+                //       := ceil(2^N / A)
+                //       := div(2^N + A - 1, A)
+                rational A = div(bound, b2.val()) + 1;
+                rational B = div(bound + A, A);
+                if (A >= 4 && B >= 4) {
+                    _backtrack.released = false;
+                    return false;
+                }
+                rational lo_val = A;
                 rational hi_val(0);
+                SASSERT(A * B > bound);
+                SASSERT(A * (B - 1) <= bound);
+                SASSERT((A - 1) * B <= bound);
+                SASSERT(b2.val() >= B);
+
                 pdd lo = m.mk_val(lo_val);
                 pdd hi = m.mk_val(hi_val);
                 fi.interval = eval_interval::proper(lo, lo_val, hi, hi_val);

src/sat/smt/polysat/op_constraint.cpp

@@ -45,7 +45,11 @@ namespace polysat {
         return eval(p, q, r);
     }
 
-    lbool op_constraint::eval(assignment const& a) const {
+    lbool op_constraint::weak_eval(assignment const& a) const {
+        return eval();
+    }
+
+    lbool op_constraint::strong_eval(assignment const& a) const {
         return eval(a.apply_to(p), a.apply_to(q), a.apply_to(r));
     }
 

src/sat/smt/polysat/op_constraint.h

@@ -75,7 +75,8 @@ namespace polysat {
         std::ostream& display(std::ostream& out, lbool status) const override;
         std::ostream& display(std::ostream& out) const override;
         lbool eval() const override;
-        lbool eval(assignment const& a) const override;
+        lbool weak_eval(assignment const& a) const override;
+        lbool strong_eval(assignment const& a) const override;
         bool is_always_true() const { return false; }
         bool is_always_false() const { return false; }
         void activate(core& c, bool sign, dependency const& dep) override;

src/sat/smt/polysat/saturation.cpp

@@ -25,7 +25,7 @@ namespace polysat {
         bool has_conflict = false;
         for (auto idx : c.assigned_constraints()) {
             auto sc = c.get_constraint(idx);
-            lbool eval_value = c.eval_unfold(sc);
+            lbool eval_value = c.strong_eval(sc);
             if (eval_value == l_true)
                 continue;
 
@@ -77,9 +77,9 @@ namespace polysat {
             }
             else if (std::holds_alternative<signed_constraint>(e)) {
                 auto sc = *std::get_if<signed_constraint>(&e);
-                if (c.eval(sc) != l_false)
+                if (c.strong_eval(sc) != l_false)
                     return;
-                auto d = c.propagate(~sc, c.explain_eval(sc));
+                auto d = c.propagate(~sc, c.explain_strong_eval(sc));
                 lemma.push_back(d);
             }
             else

src/sat/smt/polysat/ule_constraint.cpp

@@ -131,13 +131,10 @@ namespace polysat {
             unsigned const rhs_vars = rhs.free_vars().size();
             unsigned const diff_vars = (lhs - rhs).free_vars().size();
             if (diff_vars < lhs_vars || diff_vars < rhs_vars) {
-                LOG("reduce number of varables");
-                // verbose_stream() << "IN:  " << ule_pp(to_lbool(is_positive), lhs, rhs) << "\n";
                 if (lhs_vars <= rhs_vars)
                     rhs = lhs - rhs - 1;
                 else
                     lhs = rhs - lhs;
-                // verbose_stream() << "OUT: " << ule_pp(to_lbool(is_positive), lhs, rhs) << "\n";
             }
         }
 
@@ -231,7 +228,7 @@ namespace polysat {
             lhs *= x;
             SASSERT(lhs.leading_coefficient().is_power_of_two());
         }
-        // verbose_stream() << "simplified " << lhs << " <= " << rhs << "\n";
+        TRACE("bv", tout << "simplified " << lhs << " <= " << rhs << "\n");
     } // simplify_impl
 }
 
@@ -346,11 +343,11 @@ namespace polysat {
         return eval(lhs(), rhs());
     }
 
-    lbool ule_constraint::eval(assignment const& a) const {
+    lbool ule_constraint::weak_eval(assignment const& a) const {
         return eval(a.apply_to(lhs()), a.apply_to(rhs()));
     }
 
-    lbool ule_constraint::eval_unfold(assignment const& a) const {
+    lbool ule_constraint::strong_eval(assignment const& a) const {
         return eval(a.apply_to(unfold_lhs()), a.apply_to(unfold_rhs()));
     }
 

src/sat/smt/polysat/ule_constraint.h

@@ -38,8 +38,8 @@ namespace polysat {
         std::ostream& display(std::ostream& out, lbool status) const override;
         std::ostream& display(std::ostream& out) const override;
         lbool eval() const override;
-        lbool eval(assignment const& a) const override;
+        lbool weak_eval(assignment const& a) const override;
-        lbool eval_unfold(assignment const& a) const override;
+        lbool strong_eval(assignment const& a) const override;
         bool is_linear() const override { return lhs().is_linear_or_value() && rhs().is_linear_or_value(); }
         void activate(core& c, bool sign, dependency const& dep);
         void propagate(core& c, lbool value, dependency const& dep) {}

src/sat/smt/polysat/umul_ovfl_constraint.cpp

@@ -68,7 +68,11 @@ namespace polysat {
         return eval(p(), q());
     }
 
-    lbool umul_ovfl_constraint::eval(assignment const& a) const {
+    lbool umul_ovfl_constraint::weak_eval(assignment const& a) const {
+        return eval();
+    }
+
+    lbool umul_ovfl_constraint::strong_eval(assignment const& a) const {
         return eval(a.apply_to(p()), a.apply_to(q()));
     }
 

src/sat/smt/polysat/umul_ovfl_constraint.h

@@ -35,7 +35,8 @@ namespace polysat {
         std::ostream& display(std::ostream& out, lbool status) const override;
         std::ostream& display(std::ostream& out) const override;
         lbool eval() const override;
-        lbool eval(assignment const& a) const override;
+        lbool weak_eval(assignment const& a) const override;
+        lbool strong_eval(assignment const& a) const override;
         void activate(core& c, bool sign, dependency const& dep) override;
         void propagate(core& c, lbool value, dependency const& dep) override;
         bool is_linear() const override { return p().is_linear_or_value() && q().is_linear_or_value(); }

src/sat/smt/polysat/viable.cpp

@@ -488,13 +488,15 @@ namespace polysat {
         auto after = last;
         unsigned bw = c.size(last.e->var);
 
+        TRACE("bv", display_explain(tout));
+
         result.append(m_fixed_bits.explain());
 
         if (last.e->interval.is_full()) {
             if (m_var != last.e->var)
                 result.push_back(offset_claim(m_var, { last.e->var, 0 }));
             for (auto const& sc : last.e->side_cond)
-                result.push_back(c.propagate(sc, c.explain_eval(sc)));
+                result.push_back(c.propagate(sc, c.explain_weak_eval(sc)));
             result.push_back(c.get_dependency(last.e->constraint_index));
             SASSERT(m_explain.size() == 1);
         }
@@ -510,7 +512,7 @@ namespace polysat {
             if (m_var != e.e->var)
                 result.push_back(offset_claim(m_var, { e.e->var, 0 }));
             for (auto const& sc : e.e->side_cond)
-                result.push_back(c.propagate(sc, c.explain_eval(sc)));
+                result.push_back(c.propagate(sc, c.explain_weak_eval(sc)));
             result.push_back(c.get_dependency(index));
             if (e.e == last.e)
                 break;
@@ -575,7 +577,7 @@ namespace polysat {
             auto sc = cs.ult(t - vlo, vhi - vlo);
             SASSERT(!sc.is_always_false());
             if (!sc.is_always_true())
-                deps.push_back(c.propagate(sc, c.explain_eval(sc)));
+                deps.push_back(c.propagate(sc, c.explain_weak_eval(sc)));
             t.reset(lo.manager());
             t = c.value(mod(e.value, rational::power_of_two(aw)), aw);
         }
@@ -586,19 +588,19 @@ namespace polysat {
         auto sc = cs.ult(t - lo, hi - lo);
         SASSERT(!sc.is_always_false());
         if (!sc.is_always_true())
-            deps.push_back(c.propagate(sc, c.explain_eval(sc)));
+            deps.push_back(c.propagate(sc, c.explain_weak_eval(sc)));
     }
 
     /*
     * Register constraint at index 'idx' as unitary in v.
     */
-    bool viable::add_unitary(pvar v, constraint_id idx) {
+    bool viable::add_unitary(pvar v, constraint_id idx, rational& var_value) {
 
         if (c.is_assigned(v))
             return true;
-        auto [sc, d, value] = c.m_constraint_index[idx.id];
+        auto [sc, d, truth_value] = c.m_constraint_index[idx.id];
-        SASSERT(value != l_undef);
+        SASSERT(truth_value != l_undef);
-        if (value == l_false)
+        if (truth_value == l_false)
             sc = ~sc;
 
         if (!sc.is_linear()) 
@@ -708,6 +710,12 @@ namespace polysat {
             m_var = v;
             return false;
         }
+        switch (find_viable(v, var_value)) {
+        case find_t::empty:
+            return false;
+        default:
+            break;
+        }
         return true;
     }
 
@@ -961,6 +969,13 @@ namespace polysat {
         return out;
     }
 
+    std::ostream& viable::display_explain(std::ostream& out) const {
+        display_state(out);
+        for (auto const& e : m_explain)
+            display_one(out << e.value << " ", m_var, e.e) << "\n";
+        return out;
+    }
+
       /*
      * Lower bounds are strictly ascending.
      * Intervals don't contain each-other (since lower bounds are ascending, it suffices to check containment in one direction).

src/sat/smt/polysat/viable.h

@@ -141,6 +141,7 @@ namespace polysat {
         offset_slices   m_overlaps;
         void init_overlaps(pvar v);
         std::ostream& display_state(std::ostream& out) const;
+        std::ostream& display_explain(std::ostream& out) const;
 
     public:
         viable(core& c);
@@ -160,7 +161,7 @@ namespace polysat {
         /*
         * Register constraint at index 'idx' as unitary in v.
         */
-        bool add_unitary(pvar v, constraint_id);
+        bool add_unitary(pvar v, constraint_id, rational& value);
 
         /*
         * Ensure data-structures tracking variable v.