From 6e72182194939019aa318b501ed90fd6589fd043 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 1 Feb 2024 09:57:28 -0800 Subject: [PATCH] remove unused propagation in umul_overflow code. Rename propagate to saturate to reflect where it gets used Signed-off-by: Nikolaj Bjorner --- src/sat/smt/polysat/constraints.h | 4 +- src/sat/smt/polysat/core.cpp | 15 ---- src/sat/smt/polysat/core.h | 1 - src/sat/smt/polysat/op_constraint.cpp | 26 +++---- src/sat/smt/polysat/op_constraint.h | 14 ++-- src/sat/smt/polysat/saturation.cpp | 2 +- src/sat/smt/polysat/ule_constraint.h | 2 +- src/sat/smt/polysat/umul_ovfl_constraint.cpp | 78 -------------------- src/sat/smt/polysat/umul_ovfl_constraint.h | 4 +- 9 files changed, 25 insertions(+), 121 deletions(-) diff --git a/src/sat/smt/polysat/constraints.h b/src/sat/smt/polysat/constraints.h index d089c9105..8dbf150a5 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 bool propagate(core& c, lbool value, dependency const& d) = 0; + virtual bool saturate(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); } - bool propagate(core& c, lbool value, dependency const& d) { return m_constraint->propagate(c, value, d); } + bool saturate(core& c, lbool value, dependency const& d) { return m_constraint->saturate(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/core.cpp b/src/sat/smt/polysat/core.cpp index 5adf7001e..5bc8ea2e4 100644 --- a/src/sat/smt/polysat/core.cpp +++ b/src/sat/smt/polysat/core.cpp @@ -487,21 +487,6 @@ namespace polysat { return d; } - void core::propagate(constraint_id id, signed_constraint& sc, lbool value, dependency const& d) { - 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_weak_eval(sc), "constraint-propagate"); - else if (value != eval_value) { - m_unsat_core = explain_weak_eval(sc); - m_unsat_core.push_back(m_constraint_index[id.id].d); - verbose_stream() << "infeasible propagation " << m_unsat_core << "\n"; - s.set_conflict(m_unsat_core, "polysat-constraint-core"); - decay_activity(); - } - } - void core::get_bitvector_suffixes(pvar v, offset_slices& out) { s.get_bitvector_suffixes(v, out); } diff --git a/src/sat/smt/polysat/core.h b/src/sat/smt/polysat/core.h index 4996fe33f..04cd264f9 100644 --- a/src/sat/smt/polysat/core.h +++ b/src/sat/smt/polysat/core.h @@ -98,7 +98,6 @@ namespace polysat { void propagate_eval(constraint_id idx); 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_weak_eval(unsigned_vector const& vars); void add_watch(unsigned idx, unsigned var); diff --git a/src/sat/smt/polysat/op_constraint.cpp b/src/sat/smt/polysat/op_constraint.cpp index 271d7f46e..3e88c799a 100644 --- a/src/sat/smt/polysat/op_constraint.cpp +++ b/src/sat/smt/polysat/op_constraint.cpp @@ -264,21 +264,21 @@ namespace polysat { } } - bool op_constraint::propagate(core& c, lbool value, dependency const& dep) { + bool op_constraint::saturate(core& c, lbool value, dependency const& dep) { SASSERT(value == l_true); switch (m_op) { case code::lshr_op: - return propagate_lshr(c); + return saturate_lshr(c); case code::ashr_op: - return propagate_ashr(c); + return saturate_ashr(c); case code::shl_op: - return propagate_shl(c); + return saturate_shl(c); case code::and_op: - return propagate_and(c); + return saturate_and(c); case code::or_op: - return propagate_or(c); + return saturate_or(c); case code::inv_op: - return propagate_inv(c); + return saturate_inv(c); default: verbose_stream() << "not implemented yet: " << *this << "\n"; NOT_IMPLEMENTED_YET(); @@ -287,7 +287,7 @@ namespace polysat { return false; } - bool op_constraint::propagate_inv(core& s) { + bool op_constraint::saturate_inv(core& s) { return false; } @@ -323,7 +323,7 @@ namespace polysat { * when q is a constant, several axioms can be enforced at activation time. * */ - bool op_constraint::propagate_lshr(core& c) { + bool op_constraint::saturate_lshr(core& c) { auto& m = p.manager(); auto const pv = c.subst(p); auto const qv = c.subst(q); @@ -350,7 +350,7 @@ namespace polysat { return c1 || c2 || c3; } - bool op_constraint::propagate_ashr(core& c) { + bool op_constraint::saturate_ashr(core& c) { // // Suppose q = k, p >= 0: // p = ab, where b has length k, a has length N - k @@ -409,7 +409,7 @@ namespace polysat { * q >= k -> r = 0 \/ r >= 2^k * q >= k -> r[i] = 0 for i < k */ - bool op_constraint::propagate_shl(core& c) { + bool op_constraint::saturate_shl(core& c) { auto& m = p.manager(); auto const pv = c.subst(p); auto const qv = c.subst(q); @@ -443,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 */ - bool op_constraint::propagate_and(core& c) { + bool op_constraint::saturate_and(core& c) { auto& m = p.manager(); auto pv = c.subst(p); auto qv = c.subst(q); @@ -482,7 +482,7 @@ namespace polysat { return false; } - bool op_constraint::propagate_or(core& c) { + bool op_constraint::saturate_or(core& c) { auto& m = p.manager(); auto pv = c.subst(p); auto qv = c.subst(q); diff --git a/src/sat/smt/polysat/op_constraint.h b/src/sat/smt/polysat/op_constraint.h index dcaf280b2..6edfb026d 100644 --- a/src/sat/smt/polysat/op_constraint.h +++ b/src/sat/smt/polysat/op_constraint.h @@ -60,12 +60,12 @@ namespace polysat { static lbool eval_inv(pdd const& p, pdd const& r); static lbool eval_or(pdd const& p, pdd const& q, pdd const& r); - bool propagate_lshr(core& c); - bool propagate_ashr(core& c); - bool propagate_shl(core& c); - bool propagate_and(core& c); - bool propagate_or(core& c); - bool propagate_inv(core& c); + bool saturate_lshr(core& c); + bool saturate_ashr(core& c); + bool saturate_shl(core& c); + bool saturate_and(core& c); + bool saturate_or(core& c); + bool saturate_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; - bool propagate(core& c, lbool value, dependency const& dep) override; + bool saturate(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 8f26ca732..f37675b67 100644 --- a/src/sat/smt/polysat/saturation.cpp +++ b/src/sat/smt/polysat/saturation.cpp @@ -342,7 +342,7 @@ namespace polysat { void saturation::try_op(pvar v, signed_constraint& sc, dependency const& d) { SASSERT(sc.is_op()); - VERIFY(sc.propagate(c, l_true, d)); + VERIFY(sc.saturate(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 47c9b893c..f2a942802 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) override; - bool propagate(core& c, lbool value, dependency const& dep) override { return false; } + bool saturate(core& c, lbool value, dependency const& dep) override { 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 98d86528c..65d7573b0 100644 --- a/src/sat/smt/polysat/umul_ovfl_constraint.cpp +++ b/src/sat/smt/polysat/umul_ovfl_constraint.cpp @@ -80,83 +80,5 @@ namespace polysat { } - bool umul_ovfl_constraint::propagate(core& c, lbool value, dependency const& dep) { - if (value == l_undef) - 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 true; - if (narrow_bound(c, value == l_true, q(), p(), q1, p1, dep)) - return true; - return false; - } - - /** - * if p constant, q, propagate inequality - */ - bool umul_ovfl_constraint::narrow_bound(core& c, bool is_positive, pdd const& p0, pdd const& q0, pdd const& p, pdd const& q, dependency const& d) { - LOG("p: " << p0 << " := " << p); - LOG("q: " << q0 << " := " << q); - - if (!p.is_val()) - return false; - SASSERT(!p.is_zero() && !p.is_one()); // evaluation should catch this case - - rational const& M = p.manager().two_to_N(); - auto& C = c.cs(); - - // q_bound - // = min q . Ovfl(p_val, q) - // = min q . p_val * q >= M - // = min q . q >= M / p_val - // = ceil(M / p_val) - rational const q_bound = ceil(M / p.val()); - SASSERT(2 <= q_bound && q_bound <= M / 2); - SASSERT(p.val() * q_bound >= M); - SASSERT(p.val() * (q_bound - 1) < M); - // LOG("q_bound: " << q.manager().mk_val(q_bound)); - - // We need the following properties for the bounds: - // - // p_bound * (q_bound - 1) < M - // p_bound * q_bound >= M - // - // With these properties we get: - // - // p <= p_bound & q < q_bound ==> ~Ovfl(p, q) - // p >= p_bound & q >= q_bound ==> Ovfl(p, q) - // - // Written as lemmas: - // - // Ovfl(p, q) & p <= p_bound ==> q >= q_bound - // ~Ovfl(p, q) & p >= p_bound ==> q < q_bound - // - if (is_positive) { - // Find largest bound for p such that q_bound is still correct. - // p_bound = max p . (q_bound - 1)*p < M - // = max p . p < M / (q_bound - 1) - // = ceil(M / (q_bound - 1)) - 1 - rational const p_bound = ceil(M / (q_bound - 1)) - 1; - SASSERT(p.val() <= p_bound); - SASSERT(p_bound * q_bound >= M); - SASSERT(p_bound * (q_bound - 1) < M); - // LOG("p_bound: " << p.manager().mk_val(p_bound)); - c.add_axiom("~Ovfl(p, q) & p <= p_bound -> q < q_bound", { d, ~C.ule(p0, p_bound), C.ule(q_bound, q0) }, true); - } - else { - // Find lowest bound for p such that q_bound is still correct. - // p_bound = min p . Ovfl(p, q_bound) = ceil(M / q_bound) - rational const p_bound = ceil(M / q_bound); - SASSERT(p_bound <= p.val()); - SASSERT(p_bound * q_bound >= M); - SASSERT(p_bound * (q_bound - 1) < M); - // LOG("p_bound: " << p.manager().mk_val(p_bound)); - c.add_axiom("~Ovfl(p, q) & p >= p_bound -> q < q_bound", { d, ~C.ule(p_bound, p0), C.ult(q0, q_bound) }, true); - } - return true; - } - } diff --git a/src/sat/smt/polysat/umul_ovfl_constraint.h b/src/sat/smt/polysat/umul_ovfl_constraint.h index 4a5dd080e..6938a14d9 100644 --- a/src/sat/smt/polysat/umul_ovfl_constraint.h +++ b/src/sat/smt/polysat/umul_ovfl_constraint.h @@ -25,8 +25,6 @@ namespace polysat { static bool is_always_false(bool is_positive, pdd const& p, pdd const& q) { return is_always_true(!is_positive, p, q); } static lbool eval(pdd const& p, pdd const& q); - bool narrow_bound(core& c, bool is_positive, pdd const& p0, pdd const& q0, pdd const& p, pdd const& q, dependency const& d); - public: umul_ovfl_constraint(pdd const& p, pdd const& q); ~umul_ovfl_constraint() override {} @@ -38,7 +36,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; - bool propagate(core& c, lbool value, dependency const& dep) override; + bool saturate(core& c, lbool value, dependency const& dep) override { return false; } bool is_linear() const override { return p().is_linear_or_value() && q().is_linear_or_value(); } };