From 33c37cfdf035c397d6bd08d72db1744efcc94429 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 10 Jan 2024 16:05:55 -0800 Subject: [PATCH] bugbash bit-wise operations Signed-off-by: Nikolaj Bjorner --- src/sat/smt/polysat/constraints.h | 2 +- src/sat/smt/polysat/op_constraint.cpp | 103 ++++++++++++-------------- src/sat/smt/polysat/op_constraint.h | 8 +- src/sat/smt/polysat/viable.cpp | 29 +++++--- 4 files changed, 71 insertions(+), 71 deletions(-) diff --git a/src/sat/smt/polysat/constraints.h b/src/sat/smt/polysat/constraints.h index eb8766350..168deb29f 100644 --- a/src/sat/smt/polysat/constraints.h +++ b/src/sat/smt/polysat/constraints.h @@ -161,7 +161,7 @@ namespace polysat { signed_constraint sgt(unsigned p, pdd const& q) { return slt(q, p); } signed_constraint sge(pdd const& p, pdd const& q) { return ~slt(q, p); } - signed_constraint sge(pdd const& p, int q) { return ~slt(q, p); } + signed_constraint sge(pdd const& p, int q) { return sge(p, p.manager().mk_val(q)); } signed_constraint umul_ovfl(pdd const& p, rational const& q) { return umul_ovfl(p, p.manager().mk_val(q)); } signed_constraint umul_ovfl(rational const& p, pdd const& q) { return umul_ovfl(q.manager().mk_val(p), q); } diff --git a/src/sat/smt/polysat/op_constraint.cpp b/src/sat/smt/polysat/op_constraint.cpp index 280e5c38a..a611e0607 100644 --- a/src/sat/smt/polysat/op_constraint.cpp +++ b/src/sat/smt/polysat/op_constraint.cpp @@ -99,10 +99,17 @@ namespace polysat { auto M = m.max_value(); auto N = M + 1; if (p.val() >= N / 2) { - if (q.val() >= m.power_of_2()) - return to_lbool(r.val() == M); + if (q.val() >= m.power_of_2()) { + if (p.is_zero()) + return to_lbool(r.val() == 0); + else + return to_lbool(r.val() == M); + } unsigned k = q.val().get_unsigned(); - return to_lbool(r.val() == p.val() - rational::power_of_two(k)); + // p >>a q = p / 2^k - 2^{N-k} + auto pdiv2k = machine_div2k(p.val(), k); + auto pNk = rational::power_of_two(m.power_of_2() - k); + return to_lbool(r.val() == pdiv2k + N - pNk); } else return eval_lshr(p, q, r); @@ -244,6 +251,7 @@ namespace polysat { c.add_axiom("q >= N -> p >>l q = 0", { ~C.uge(q, N), C.eq(r) }, false); c.add_axiom("q = 0 -> p >>l q = p", { ~C.eq(q), C.eq(r, p) }, false); c.add_axiom("p = 0 -> p >>l q = p", { ~C.eq(p), C.eq(r, p) }, false); + c.add_axiom("p >>l q <= p", { C.ule(r, p) }, false); break; case code::shl_op: c.add_axiom("q >= N -> p << q = 0", { ~C.uge(q, N), C.eq(r) }, false); @@ -288,15 +296,21 @@ namespace polysat { } - void op_constraint::propagate(core& c, signed_constraint const& sc) { + bool op_constraint::propagate(core& c, signed_constraint const& sc) { + if (c.weak_eval(sc) != l_true) + return false; c.propagate(sc, c.explain_weak_eval(sc)); + return true; } - void op_constraint::add_conflict(core& c, char const* ax, constraint_or_dependency_list const& cs) { + bool op_constraint::add_conflict(core& c, char const* ax, constraint_or_dependency_list const& cs) { for (auto sc : cs) - if (std::holds_alternative(sc)) - propagate(c, ~*std::get_if(&sc)); + if (std::holds_alternative(sc) && + !propagate(c, ~*std::get_if(&sc))) + return false; + c.add_axiom(ax, cs, true); + return true; } /** * Enforce basic axioms for r == p >> q: @@ -314,7 +328,7 @@ namespace polysat { * when q is a constant, several axioms can be enforced at activation time. * */ - void op_constraint::propagate_lshr(core& c) { + bool op_constraint::propagate_lshr(core& c) { auto& m = p.manager(); auto const pv = c.subst(p); auto const qv = c.subst(q); @@ -323,45 +337,23 @@ namespace polysat { auto& C = c.cs(); - if (pv.is_val() && rv.is_val() && rv.val() > pv.val()) - return add_conflict(c, "lshr 1", { C.ule(r, p) }); + if (!pv.is_val() || !qv.is_val() || !rv.is_val()) + return false; - else if (qv.is_val() && qv.val() >= N && rv.is_val() && !rv.is_zero()) - // TODO: instead of rv.is_val() && !rv.is_zero(), we should use !is_forced_zero(r) which checks whether eval(r) = 0 or bvalue(r=0) = true; see saturation.cpp - c.add_axiom("q >= N -> r = 0", { ~C.ule(N, q), C.eq(r) }, true); - else if (qv.is_zero() && pv.is_val() && rv.is_val() && pv != rv) - c.add_axiom("q = 0 -> p = r", { ~C.eq(q), C.eq(p, r) }, true); - else if (qv.is_val() && !qv.is_zero() && pv.is_val() && rv.is_val() && !pv.is_zero() && rv.val() >= pv.val()) - c.add_axiom("q != 0 & p > 0 -> r < p", { C.eq(q), C.ule(p, 0), C.ult(r, p) }, true); - else if (qv.is_val() && !qv.is_zero() && qv.val() < N && rv.is_val() && rv.val() > rational::power_of_two(N - qv.val().get_unsigned()) - 1) - c.add_axiom("q >= k -> r <= 2^{N-k} - 1", { ~C.ule(qv.val(), q), C.ule(r, rational::power_of_two(N - qv.val().get_unsigned()) - 1) }, true); - else if (pv.is_val() && rv.is_val() && qv.is_val() && !qv.is_zero()) { - unsigned k = qv.val().get_unsigned(); - for (unsigned i = 0; i < N - k; ++i) { - if (rv.val().get_bit(i) && !pv.val().get_bit(i + k)) - c.add_axiom("q = k -> r[i] = p[i+k] for 0 <= i < N - k", { ~C.eq(q, k), ~C.bit(r, i), C.bit(p, i + k) }, true); + SASSERT(!qv.is_zero()); + SASSERT(qv.val() < N); - if (!rv.val().get_bit(i) && pv.val().get_bit(i + k)) - c.add_axiom("q = k -> r[i] = p[i+k] for 0 <= i < N - k", { ~C.eq(q, k), C.bit(r, i), ~C.bit(p, i + k) }, true); - } - } - else { - // forward propagation - SASSERT(!(pv.is_val() && qv.is_val() && rv.is_val())); - // LOG(p << " = " << pv << " and " << q << " = " << qv << " yields [>>] " << r << " = " << (qv.val().is_unsigned() ? machine_div2k(pv.val(), qv.val().get_unsigned()) : rational::zero())); - if (qv.is_val() && !rv.is_val()) { - rational const& q_val = qv.val(); - if (q_val >= N) - // q >= N ==> r = 0 - c.add_axiom("q >= N ==> r = 0", { ~C.ule(N, q), C.eq(r) }, true); - else if (pv.is_val()) { - SASSERT(q_val.is_unsigned()); - // - rational const r_val = machine_div2k(pv.val(), q_val.get_unsigned()); - c.add_axiom("p = p_val & q = q_val ==> r = p_val / 2^q_val", { ~C.eq(p, pv), ~C.eq(q, qv), C.eq(r, r_val) }, true); - } - } - } + auto k = qv.val().get_unsigned(); + + // q = k & 0 < k < N => 2^k r <= p <= 2^k*x + 2^k - 1 + + auto twoK = rational::power_of_two(k); + auto twoNK = rational::power_of_two(N - k); + 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; } void op_constraint::propagate_ashr(core& c) { @@ -397,10 +389,12 @@ namespace polysat { rational twoN = rational::power_of_two(N); rational twoK = rational::power_of_two(k); rational twoNk = rational::power_of_two(N - k); - auto eqK = C.eq(q, k); - c.add_axiom("q = k -> r*2^k + p < 2^k", { ~eqK, C.ult(p - r * twoK, twoK) }, true); - c.add_axiom("q = k & p >= 0 -> r < 2^{N-k}", { ~eqK, ~C.ule(0, p), C.ult(r, twoNk) }, true); - c.add_axiom("q = k & p < 0 -> r >= 2^N - 2^{N-k}", { ~eqK, ~C.slt(p, 0), C.uge(r, twoN - twoNk) }, true); + + bool c1 = add_conflict(c, "q = k & 0 < k < N -> 2^k r <= p", { ~C.eq(q, k), C.ule(r * twoK, p) }); + bool c2 = add_conflict(c, "q = k & 0 < k < N -> p <= 2^k*x + 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}", { ~C.eq(q, k), ~C.slt(p, 0), C.uge(r, twoN - twoNk) }); + bool c4 = add_conflict(c, "p >= 0 & q = k -> r < 2^{N-k}", { ~C.eq(q, k), C.slt(p, 0), C.ult(r, twoNk)}); + VERIFY(c1 || c2 || c3 || c4); } } @@ -432,10 +426,6 @@ namespace polysat { auto twoK = rational::power_of_two(k); -#if 0 - if (rv.is_val() && rv.val() < twoK && !rv.is_zero()) - return add_conflict(c, "q >= k -> r = 0 or r >= 2^k", { ~C.uge(q, k), C.eq(r), C.uge(r, twoK) }); -#endif add_conflict(c, "p << k = 2^k*p", { ~C.eq(q, k), C.eq(r, p * twoK) }); } @@ -487,7 +477,7 @@ namespace polysat { } } - void op_constraint::propagate_or(core& c) { + bool op_constraint::propagate_or(core& c) { auto& m = p.manager(); auto pv = c.subst(p); auto qv = c.subst(q); @@ -495,7 +485,7 @@ namespace polysat { auto& C = c.cs(); if (!pv.is_val() || !qv.is_val() || !rv.is_val()) - return; + 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)}); @@ -518,8 +508,9 @@ namespace polysat { add_conflict(c, "(p|q)[i] => p[i] or q[i]", { C.bit(p, i), C.bit(q, i), ~C.bit(r, i) }); else UNREACHABLE(); - return; + return true; } + return false; } bool op_constraint::propagate_mask(core& c, pdd const& p, pdd const& q, pdd const& r, rational const& pv, rational const& qv, rational const& rv) { diff --git a/src/sat/smt/polysat/op_constraint.h b/src/sat/smt/polysat/op_constraint.h index e8a1361f3..22ce56274 100644 --- a/src/sat/smt/polysat/op_constraint.h +++ b/src/sat/smt/polysat/op_constraint.h @@ -60,16 +60,16 @@ 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); - void propagate_lshr(core& c); + bool propagate_lshr(core& c); void propagate_ashr(core& c); void propagate_shl(core& c); void propagate_and(core& c); - void propagate_or(core& c); + bool propagate_or(core& c); void 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); - void propagate(core& c, signed_constraint const& sc); - void add_conflict(core& c, char const* ax, constraint_or_dependency_list const& cs); + bool propagate(core& c, signed_constraint const& sc); + bool add_conflict(core& c, char const* ax, constraint_or_dependency_list const& cs); std::ostream& display(std::ostream& out, char const* eq) const; diff --git a/src/sat/smt/polysat/viable.cpp b/src/sat/smt/polysat/viable.cpp index 56549cfd8..1a480de76 100644 --- a/src/sat/smt/polysat/viable.cpp +++ b/src/sat/smt/polysat/viable.cpp @@ -619,10 +619,16 @@ namespace polysat { // t in ] (value - 1) * 2^{bw - ebw} ; value * 2^{bw - ebw} ] // t in [ (value - 1) * 2^{bw - ebw} - 1 ; value * 2^{bw - ebw} + 1 [ +#if 0 + verbose_stream() << e.value << " " << t << "\n"; + if (t.is_val()) verbose_stream() << "tval " << t.val() << "\n"; + verbose_stream() << "[" << vlo << " " << vhi << "[\n"; + verbose_stream() << "bw " << ebw << " " << bw << " " << e.e->interval << " bw " << abw << " " << aw << " " << after.e->coeff << " " << after.e->interval << "\n"; if (!t.is_val()) IF_VERBOSE(0, verbose_stream() << "symbolic t : " << t << "\n"); +#endif auto sc = cs.ult(t - vlo, vhi - vlo); - SASSERT(!sc.is_always_false()); + VERIFY(!sc.is_always_false()); if (!sc.is_always_true()) deps.push_back(c.propagate(sc, c.explain_weak_eval(sc))); t.reset(lo.manager()); @@ -706,34 +712,35 @@ namespace polysat { // k = 3, lo = 1, hi = 2, new_lo = 1 div 2^3 + 1 = 1, new_hi = 2 div 2^3 + 1 = 1 // lo > hi + TRACE("bv", display_one(tout << "try to reduce entry: ", v, ne) << "\n"); pdd const& pdd_lo = ne->interval.lo(); pdd const& pdd_hi = ne->interval.hi(); rational const& lo = ne->interval.lo_val(); rational const& hi = ne->interval.hi_val(); + rational twoK = rational::power_of_two(k); - rational new_lo = machine_div2k(lo, k); + rational new_lo = machine_div2k(mod2k(lo + twoK - 1, w), k); pdd lo_eq = pdd_lo * rational::power_of_two(w - k); if (mod2k(lo, k).is_zero()) { if (!lo_eq.is_zero()) ne->side_cond.push_back(cs.eq(lo_eq)); } else { - new_lo = machine_div2k(new_lo, k); - new_lo += 1; - if (!lo_eq.is_val() || lo_eq.is_zero()) + SASSERT(!lo_eq.is_val() || !lo_eq.is_zero()); + if (!lo_eq.is_val()) ne->side_cond.push_back(~cs.eq(lo_eq)); } - rational new_hi = machine_div2k(hi, k); + + rational new_hi = machine_div2k(mod2k(hi + twoK - 1, w), k); pdd hi_eq = pdd_hi * rational::power_of_two(w - k); if (mod2k(hi, k).is_zero()) { if (!hi_eq.is_zero()) ne->side_cond.push_back(cs.eq(hi_eq)); } else { - new_hi = machine_div2k(new_hi, k); - new_hi += 1; - if (!hi_eq.is_val() || hi_eq.is_zero()) + SASSERT(!hi_eq.is_val() || !hi_eq.is_zero()); + if (!hi_eq.is_val()) ne->side_cond.push_back(~cs.eq(hi_eq)); } @@ -748,6 +755,8 @@ namespace polysat { ne->coeff = 1; ne->interval = eval_interval::proper(pdd_lo, new_lo, pdd_hi, new_hi); ne->bit_width -= k; + + TRACE("bv", display_one(tout << "reduced: ", v, ne) << "\n"); intersect(v, ne); } if (ne->interval.is_full()) { @@ -1013,7 +1022,7 @@ namespace polysat { 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"; + display_one(out << "v" << m_var << "[" << e.e->bit_width << "] : = " << e.value << " ", m_var, e.e) << "\n"; return out; }