mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

bugbash bit-wise operations

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-01-10 16:05:55 -08:00
parent 33f17215f7
commit 33c37cfdf0
4 changed files with 71 additions and 71 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/sat/smt/polysat/constraints.h
View file

@ -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); }

103
src/sat/smt/polysat/op_constraint.cpp
View file

@ -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<signed_constraint>(sc))
propagate(c, ~*std::get_if<signed_constraint>(&sc));
if (std::holds_alternative<signed_constraint>(sc) &&
!propagate(c, ~*std::get_if<signed_constraint>(&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) {

8
src/sat/smt/polysat/op_constraint.h
View file

@ -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;

29
src/sat/smt/polysat/viable.cpp
View file

@ -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;
}