From a2df3cb828faeb04fdc6cccff3130c9140ce6d53 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 11 Jan 2024 11:45:05 -0800 Subject: [PATCH] have propagate return whether it did something --- src/sat/smt/polysat/constraints.h | 4 +- src/sat/smt/polysat/op_constraint.cpp | 58 ++++++++++---------- src/sat/smt/polysat/op_constraint.h | 10 ++-- src/sat/smt/polysat/saturation.cpp | 2 +- src/sat/smt/polysat/ule_constraint.h | 2 +- src/sat/smt/polysat/umul_ovfl_constraint.cpp | 9 +-- src/sat/smt/polysat/umul_ovfl_constraint.h | 2 +- 7 files changed, 45 insertions(+), 42 deletions(-) diff --git a/src/sat/smt/polysat/constraints.h b/src/sat/smt/polysat/constraints.h index 168deb29f..871b027c2 100644 --- a/src/sat/smt/polysat/constraints.h +++ b/src/sat/smt/polysat/constraints.h @@ -49,7 +49,7 @@ namespace polysat { virtual lbool weak_eval(assignment const& a) const = 0; 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 propagate(core& c, lbool value, dependency const& d) = 0; virtual bool is_linear() const { return false; } }; @@ -75,7 +75,7 @@ namespace polysat { unsigned num_watch() const { return m_constraint->num_watch(); } void set_num_watch(unsigned n) { m_constraint->set_num_watch(n); } void activate(core& c, dependency const& d) { m_constraint->activate(c, m_sign, d); } - void propagate(core& c, lbool value, dependency const& d) { m_constraint->propagate(c, value, d); } + bool propagate(core& c, lbool value, dependency const& d) { return 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_linear() const { return m_constraint->is_linear(); } diff --git a/src/sat/smt/polysat/op_constraint.cpp b/src/sat/smt/polysat/op_constraint.cpp index 9e997538a..271d7f46e 100644 --- a/src/sat/smt/polysat/op_constraint.cpp +++ b/src/sat/smt/polysat/op_constraint.cpp @@ -264,36 +264,31 @@ namespace polysat { } } - void op_constraint::propagate(core& c, lbool value, dependency const& dep) { + bool op_constraint::propagate(core& c, lbool value, dependency const& dep) { SASSERT(value == l_true); switch (m_op) { case code::lshr_op: - propagate_lshr(c); - break; + return propagate_lshr(c); case code::ashr_op: - propagate_ashr(c); - break; + return propagate_ashr(c); case code::shl_op: - propagate_shl(c); - break; + return propagate_shl(c); case code::and_op: - propagate_and(c); - break; + return propagate_and(c); case code::or_op: - propagate_or(c); - break; + return propagate_or(c); case code::inv_op: - propagate_inv(c); - break; + return propagate_inv(c); default: verbose_stream() << "not implemented yet: " << *this << "\n"; NOT_IMPLEMENTED_YET(); break; } + return false; } - void op_constraint::propagate_inv(core& s) { - + bool op_constraint::propagate_inv(core& s) { + return false; } bool op_constraint::propagate(core& c, signed_constraint const& sc) { @@ -352,11 +347,10 @@ namespace polysat { bool c1 = add_conflict(c, "q = k & 0 < k < N -> 2^k (p >>l q) <= p", { ~C.eq(q, k), C.ule(r * twoK, p)}); bool c2 = add_conflict(c, "q = k & 0 < k < N -> p <= 2^k*(p >>l q) + 2^k - 1", { ~C.eq(q, k), C.ule(p, r * twoK + twoK - 1) }); bool c3 = add_conflict(c, "q = k & 0 < k < N -> (p >>l q) < 2^{N-k}", { ~C.eq(q, k), C.ult(r, twoNK) }); - VERIFY(c1 || c2 || c3); - return true; + return c1 || c2 || c3; } - void op_constraint::propagate_ashr(core& c) { + bool op_constraint::propagate_ashr(core& c) { // // Suppose q = k, p >= 0: // p = ab, where b has length k, a has length N - k @@ -400,8 +394,9 @@ namespace polysat { bool c2 = add_conflict(c, "q = k & 0 < k < N -> p <= 2^k*r + 2^k - 1", { ~C.eq(q, k), C.ule(p, r * twoK + twoK - 1) }); bool c3 = add_conflict(c, "p < 0 & q = k -> r >= 2^N - 2^{N-k-1}", { ~C.eq(q, k), ~C.slt(p, 0), C.uge(r, twoN - twoNk1) }); bool c4 = add_conflict(c, "p >= 0 & q = k -> r < 2^{N-k-1}", { ~C.eq(q, k), C.slt(p, 0), C.ult(r, twoNk1)}); - VERIFY(c1 || c2 || c3 || c4); + return c1 || c2 || c3 || c4; } + return false; } @@ -414,7 +409,7 @@ namespace polysat { * q >= k -> r = 0 \/ r >= 2^k * q >= k -> r[i] = 0 for i < k */ - void op_constraint::propagate_shl(core& c) { + bool op_constraint::propagate_shl(core& c) { auto& m = p.manager(); auto const pv = c.subst(p); auto const qv = c.subst(q); @@ -423,16 +418,16 @@ namespace polysat { auto& C = c.cs(); if (!qv.is_val()) - return; + return false; if (qv.is_zero() || qv.val() >= N) - return; + return false; auto k = qv.val().get_unsigned(); auto twoK = rational::power_of_two(k); - add_conflict(c, "p << k = 2^k*p", { ~C.eq(q, k), C.eq(r, p * twoK) }); + return add_conflict(c, "p << k = 2^k*p", { ~C.eq(q, k), C.eq(r, p * twoK) }); } /** @@ -448,7 +443,7 @@ namespace polysat { * p = 2^k - 1 && r = 0 && q != 0 => q >= 2^k * q = 2^k - 1 && r = 0 && p != 0 => p >= 2^k */ - void op_constraint::propagate_and(core& c) { + bool op_constraint::propagate_and(core& c) { auto& m = p.manager(); auto pv = c.subst(p); auto qv = c.subst(q); @@ -456,13 +451,16 @@ namespace polysat { auto& C = c.cs(); if (!pv.is_val() || !qv.is_val() || !rv.is_val()) - return; + return false; + + if (eval_and(pv, qv, rv) == l_true) + return false; if (propagate_mask(c, p, q, r, pv.val(), qv.val(), rv.val())) - return; + return true; if (propagate_mask(c, q, p, r, qv.val(), pv.val(), rv.val())) - return; + return true; unsigned const N = m.power_of_2(); for (unsigned i = 0; i < N; ++i) { @@ -479,8 +477,9 @@ namespace polysat { add_conflict(c, "p&q[i] = p[i]&q[i]", { C.bit(q, i), ~C.bit(r, i) }); else UNREACHABLE(); - return; + return true; } + return false; } bool op_constraint::propagate_or(core& c) { @@ -493,6 +492,9 @@ namespace polysat { if (!pv.is_val() || !qv.is_val() || !rv.is_val()) return false; + if (eval_or(pv, qv, rv) == l_true) + return false; + if (pv.is_max() && pv != rv) return add_conflict(c, "p = -1 => p & q = p", { ~C.eq(p, m.max_value()), C.eq(p, r)}); diff --git a/src/sat/smt/polysat/op_constraint.h b/src/sat/smt/polysat/op_constraint.h index 95a659e17..dcaf280b2 100644 --- a/src/sat/smt/polysat/op_constraint.h +++ b/src/sat/smt/polysat/op_constraint.h @@ -61,11 +61,11 @@ namespace polysat { static lbool eval_or(pdd const& p, pdd const& q, pdd const& r); bool propagate_lshr(core& c); - void propagate_ashr(core& c); - void propagate_shl(core& c); - void propagate_and(core& c); + bool propagate_ashr(core& c); + bool propagate_shl(core& c); + bool propagate_and(core& c); bool propagate_or(core& c); - void propagate_inv(core& c); + bool propagate_inv(core& c); bool propagate_mask(core& c, pdd const& p, pdd const& q, pdd const& r, rational const& pv, rational const& qv, rational const& rv); bool propagate(core& c, signed_constraint const& sc); @@ -84,7 +84,7 @@ namespace polysat { bool is_always_true() const { return false; } bool is_always_false() const { return false; } void activate(core& c, bool sign, dependency const& dep) override; - void propagate(core& c, lbool value, dependency const& dep) override; + bool propagate(core& c, lbool value, dependency const& dep) override; }; } diff --git a/src/sat/smt/polysat/saturation.cpp b/src/sat/smt/polysat/saturation.cpp index 883968833..7bf9dd526 100644 --- a/src/sat/smt/polysat/saturation.cpp +++ b/src/sat/smt/polysat/saturation.cpp @@ -243,7 +243,7 @@ namespace polysat { void saturation::try_op(pvar v, signed_constraint& sc, dependency const& d) { SASSERT(sc.is_op()); - sc.propagate(c, l_true, d); + VERIFY(sc.propagate(c, l_true, d)); } // possible algebraic rule: diff --git a/src/sat/smt/polysat/ule_constraint.h b/src/sat/smt/polysat/ule_constraint.h index fe0035545..5a90d294a 100644 --- a/src/sat/smt/polysat/ule_constraint.h +++ b/src/sat/smt/polysat/ule_constraint.h @@ -42,7 +42,7 @@ namespace polysat { 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) {} + bool propagate(core& c, lbool value, dependency const& dep) { return false; } bool is_eq() const { return m_rhs.is_zero(); } unsigned power_of_2() const { return m_lhs.power_of_2(); } diff --git a/src/sat/smt/polysat/umul_ovfl_constraint.cpp b/src/sat/smt/polysat/umul_ovfl_constraint.cpp index 5d0852834..98d86528c 100644 --- a/src/sat/smt/polysat/umul_ovfl_constraint.cpp +++ b/src/sat/smt/polysat/umul_ovfl_constraint.cpp @@ -80,16 +80,17 @@ namespace polysat { } - void umul_ovfl_constraint::propagate(core& c, lbool value, dependency const& dep) { + bool umul_ovfl_constraint::propagate(core& c, lbool value, dependency const& dep) { if (value == l_undef) - return; + return false; auto& C = c.cs(); auto p1 = c.subst(p()); auto q1 = c.subst(q()); if (narrow_bound(c, value == l_true, p(), q(), p1, q1, dep)) - return; + return true; if (narrow_bound(c, value == l_true, q(), p(), q1, p1, dep)) - return; + return true; + return false; } /** diff --git a/src/sat/smt/polysat/umul_ovfl_constraint.h b/src/sat/smt/polysat/umul_ovfl_constraint.h index 6afeb7562..4a5dd080e 100644 --- a/src/sat/smt/polysat/umul_ovfl_constraint.h +++ b/src/sat/smt/polysat/umul_ovfl_constraint.h @@ -38,7 +38,7 @@ namespace polysat { 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 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(); } };