mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-14 18:06:15 +00:00
Code Activity

add built-in support for bvor: the rewriter converts bitwise and to bit-wise or so using bvor as a basis makes better sense

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-01-10 10:16:31 -08:00
parent e2c5d7d358
commit e7c9c5f7a2
10 changed files with 279 additions and 137 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/sat/smt/polysat/constraints.cpp
View file

@ -63,6 +63,12 @@ namespace polysat {
return signed_constraint(ckind_t::op_t, cnstr);
}
signed_constraint constraints::bor(pdd const& a, pdd const& b, pdd const& r) {
auto* cnstr = alloc(op_constraint, op_constraint::code::or_op, a, b, r);
c.trail().push(new_obj_trail(cnstr));
return signed_constraint(ckind_t::op_t, cnstr);
}
// parity p >= k if low order k bits of p are 0
signed_constraint constraints::parity_at_least(pdd const& p, unsigned k) {
if (k == 0)
@ -82,6 +88,12 @@ namespace polysat {
return eq(p * rational::power_of_two(N - k));
}
// 2^{N-i-1}* p >= 2^{N-1}
signed_constraint constraints::bit(pdd const& p, unsigned i) {
unsigned N = p.manager().power_of_2();
return uge(p * rational::power_of_two(N - i - 1), rational::power_of_two(N - 1));
}
bool signed_constraint::is_eq(pvar& v, rational& val) {
if (m_sign)
return false;

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

@ -22,6 +22,8 @@ namespace polysat {
class core;
class ule_constraint;
class umul_ovfl_constraint;
class op_constraint;
class assignment;
using pdd = dd::pdd;
@ -84,8 +86,10 @@ namespace polysat {
bool is_ule() const { return m_op == ule_t; }
bool is_umul_ovfl() const { return m_op == umul_ovfl_t; }
bool is_smul_fl() const { return m_op == smul_fl_t; }
bool is_op() const { return m_op == op_t; }
ule_constraint const& to_ule() const { SASSERT(is_ule()); return *reinterpret_cast<ule_constraint*>(m_constraint); }
umul_ovfl_constraint const& to_umul_ovfl() const { SASSERT(is_umul_ovfl()); return *reinterpret_cast<umul_ovfl_constraint*>(m_constraint); }
op_constraint const& to_op() const { SASSERT(is_op()); return *reinterpret_cast<op_constraint*>(m_constraint); }
bool is_eq(pvar& v, rational& val);
std::ostream& display(std::ostream& out) const;
};
@ -108,7 +112,7 @@ namespace polysat {
signed_constraint umul_ovfl(pdd const& p, pdd const& q);
signed_constraint smul_ovfl(pdd const& p, pdd const& q) { throw default_exception("smul ovfl nyi"); }
signed_constraint smul_udfl(pdd const& p, pdd const& q) { throw default_exception("smult-udfl nyi"); }
signed_constraint bit(pdd const& p, unsigned i) { throw default_exception("bit nyi"); }
signed_constraint bit(pdd const& p, unsigned i);
signed_constraint diseq(pdd const& p) { return ~eq(p); }
signed_constraint diseq(pdd const& p, pdd const& q) { return diseq(p - q); }
@ -172,6 +176,7 @@ namespace polysat {
signed_constraint ashr(pdd const& a, pdd const& b, pdd const& r);
signed_constraint shl(pdd const& a, pdd const& b, pdd const& r);
signed_constraint band(pdd const& a, pdd const& b, pdd const& r);
signed_constraint bor(pdd const& a, pdd const& b, pdd const& r);
//signed_constraint even(pdd const& p) { return parity_at_least(p, 1); }
//signed_constraint odd(pdd const& p) { return ~even(p); }

4
src/sat/smt/polysat/core.cpp
View file

@ -206,6 +206,7 @@ namespace polysat {
case l_false:
return sat::check_result::CR_CONTINUE;
case l_undef:
verbose_stream() << "giveup assign\n";
return sat::check_result::CR_GIVEUP;
// or:
// r = l_undef;
@ -220,6 +221,7 @@ namespace polysat {
TRACE("bv", tout << "saturate\n");
return sat::check_result::CR_CONTINUE;
case l_undef:
verbose_stream() << "giveup saturate\n";
r = l_undef;
break;
}
@ -231,6 +233,7 @@ namespace polysat {
TRACE("bv", tout << "refine\n");
return sat::check_result::CR_CONTINUE;
case l_undef:
verbose_stream() << "giveup refine\n";
r = l_undef;
break;
}
@ -242,6 +245,7 @@ namespace polysat {
TRACE("bv", tout << "blast\n");
return sat::check_result::CR_CONTINUE;
case l_undef:
verbose_stream() << "giveup blast\n";
r = l_undef;
break;
}

1
src/sat/smt/polysat/core.h
View file

@ -129,6 +129,7 @@ namespace polysat {
void ashr(pdd const& a, pdd const& b, pdd const& r) { add_opdef(m_constraints.ashr(a, b, r)); }
void shl(pdd const& a, pdd const& b, pdd const& r) { add_opdef(m_constraints.shl(a, b, r)); }
void band(pdd const& a, pdd const& b, pdd const& r) { add_opdef(m_constraints.band(a, b, r)); }
void bor(pdd const& a, pdd const& b, pdd const& r) { add_opdef(m_constraints.bor(a, b, r)); }
pdd bnot(pdd p) { return -p - 1; }
pvar mul(unsigned n, pdd const* args) { return m_monomials.mk(n, args); }

2
src/sat/smt/polysat/monomials.cpp
View file

@ -86,10 +86,10 @@ namespace polysat {
// bit blast a monomial definition
lbool monomials::bit_blast() {
// disable for now
return l_undef;
init_to_refine();
if (m_to_refine.empty())
return l_true;
return l_undef;
shuffle(m_to_refine.size(), m_to_refine.data(), c.rand());
if (any_of(m_to_refine, [&](auto i) { return bit_blast(m_monomials[i]); }))
return l_false;

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

@ -61,6 +61,8 @@ namespace polysat {
return eval_shl(p, q, r);
case code::and_op:
return eval_and(p, q, r);
case code::or_op:
return eval_or(p, q, r);
case code::inv_op:
return eval_inv(p, r);
case code::ashr_op:
@ -144,6 +146,19 @@ namespace polysat {
return l_undef;
}
/** Evaluate constraint: r == p | q */
lbool op_constraint::eval_or(pdd const& p, pdd const& q, pdd const& r) {
if (p.is_zero() && q == r)
return l_true;
if (q.is_zero() && p == r)
return l_true;
if (p.is_val() && q.is_val() && r.is_val())
return r.val() == bitwise_or(p.val(), q.val()) ? l_true : l_false;
return l_undef;
}
/** Evaluate constraint: r == inv p */
lbool op_constraint::eval_inv(pdd const& p, pdd const& r) {
if (!p.is_val() || !r.is_val())
@ -173,6 +188,8 @@ namespace polysat {
return out << "<<";
case op_constraint::code::and_op:
return out << "&";
case op_constraint::code::or_op:
return out << "|";
case op_constraint::code::inv_op:
return out << "inv";
default:
@ -202,6 +219,13 @@ namespace polysat {
case code::and_op:
activate_and(c, dep);
break;
case code::or_op:
c.add_axiom("p | q >= p", { C.ule(p, r) }, false);
c.add_axiom("p | q >= q", { C.ule(q, r) }, false);
c.add_axiom("p = q -> p | q = p", { ~C.eq(p, q), C.eq(r, p) }, false);
c.add_axiom("p | 0 = p", { ~C.eq(q), C.eq(r, p) }, false);
c.add_axiom("0 | q = q", { ~C.eq(p), C.eq(r, q) }, false);
break;
case code::ashr_op:
c.add_axiom("q >= N & p < 0 -> p <<a q = -1", { ~C.uge(q, N), ~C.slt(p, 0), C.eq(r, m.max_value()) }, false);
c.add_axiom("q >= N & p >= 0 -> p <<a q = 0", { ~C.uge(q, N), ~C.sge(p, 0), C.eq(r) }, false);
@ -226,19 +250,22 @@ namespace polysat {
SASSERT(value == l_true);
switch (m_op) {
case code::lshr_op:
propagate_lshr(c, dep);
propagate_lshr(c);
break;
case code::ashr_op:
propagate_ashr(c, dep);
propagate_ashr(c);
break;
case code::shl_op:
propagate_shl(c, dep);
propagate_shl(c);
break;
case code::and_op:
propagate_and(c, dep);
propagate_and(c);
break;
case code::or_op:
propagate_or(c);
break;
case code::inv_op:
propagate_inv(c, dep);
propagate_inv(c);
break;
default:
verbose_stream() << "not implemented yet: " << *this << "\n";
@ -247,10 +274,20 @@ namespace polysat {
}
}
void op_constraint::propagate_inv(core& s, dependency const& dep) {
void op_constraint::propagate_inv(core& s) {
}
void op_constraint::propagate(core& c, signed_constraint const& sc) {
c.propagate(sc, c.explain_weak_eval(sc));
}
void 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));
c.add_axiom(ax, cs, true);
}
/**
* Enforce basic axioms for r == p >> q:
*
@ -270,10 +307,10 @@ namespace polysat {
*
* TODO: use also
* s.m_viable.min_viable();
* s.m_viable.max_viable()
* s.m_viable.max_viable(
* when r, q are variables.
*/
void op_constraint::propagate_lshr(core& c, dependency const& d) {
void op_constraint::propagate_lshr(core& c) {
auto& m = p.manager();
auto const pv = c.subst(p);
auto const qv = c.subst(q);
@ -283,7 +320,7 @@ namespace polysat {
auto& C = c.cs();
if (pv.is_val() && rv.is_val() && rv.val() > pv.val())
c.add_axiom("lshr 1", { C.ule(r, p) }, false);
return add_conflict(c, "lshr 1", { C.ule(r, p) });
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
@ -352,7 +389,7 @@ namespace polysat {
}
}
void op_constraint::propagate_ashr(core& c, dependency const& dep) {
void op_constraint::propagate_ashr(core& c) {
//
// Suppose q = k, p >= 0:
// p = ab, where b has length k, a has length N - k
@ -402,7 +439,7 @@ namespace polysat {
* q = k -> r[i+k] = p[i] for 0 <= i < N - k
* q = 0 -> r = p
*/
void op_constraint::propagate_shl(core& c, dependency const& d) {
void op_constraint::propagate_shl(core& c) {
auto& m = p.manager();
auto const pv = c.subst(p);
auto const qv = c.subst(q);
@ -460,44 +497,35 @@ 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, dependency const& d) {
void op_constraint::propagate_and(core& c) {
auto& m = p.manager();
auto pv = c.subst(p);
auto qv = c.subst(q);
auto rv = c.subst(r);
auto& C = c.cs();
if (pv.is_val() && rv.is_val() && rv.val() > pv.val())
c.add_axiom("p & q <= p", { C.ule(r, p) }, true);
else if (qv.is_val() && rv.is_val() && rv.val() > qv.val())
c.add_axiom("p & q <= q", { C.ule(r, q) }, true);
else if (pv.is_val() && qv.is_val() && rv.is_val() && pv == qv && rv != pv)
c.add_axiom("p = q => p & q = p", { ~C.eq(p, q), C.eq(r, p) }, true);
// p = a && q = b ==> r = a & b
else if (pv.is_val() && qv.is_val() && !rv.is_val())
// Just assign by this very weak justification. It will be strengthened in saturation in case of a conflict
c.add_axiom("p = a & q = b => r = a&b", { ~C.eq(p, pv), ~C.eq(q, qv), C.eq(r, bitwise_and(pv.val(), qv.val())) }, true);
else if (pv.is_val() && qv.is_val() && rv.is_val()) {
if (pv.is_max() && qv != rv)
c.add_axiom("p = -1 => p & q = q", { ~C.eq(p, m.max_value()), C.eq(q, r) }, true);
else if (qv.is_max() && pv != rv)
c.add_axiom("q = -1 => p & q = p", { ~C.eq(q, m.max_value()), C.eq(p, r) }, true);
else {
unsigned const N = m.power_of_2();
unsigned pow;
if ((pv.val() + 1).is_power_of_two(pow)) {
if (rv.is_zero() && !qv.is_zero() && qv.val() <= pv.val())
c.add_axiom("p = 2^k - 1 && p & q = 0 && q != 0 => q >= 2^k", { ~C.eq(p, pv), ~C.eq(r), C.eq(q), C.ule(pv + 1, q) }, true);
else if (rv != qv)
c.add_axiom("p = 2^k - 1 ==> (p&q)*2^{N - k} = q*2^{N - k}", { ~C.eq(p, pv), C.eq(r * rational::power_of_two(N - pow), q * rational::power_of_two(N - pow)) }, true);
}
if ((qv.val() + 1).is_power_of_two(pow)) {
if (rv.is_zero() && !pv.is_zero() && pv.val() <= qv.val())
c.add_axiom("q = 2^k - 1 && p & q = 0 && p != 0 ==> p >= 2^k", { ~C.eq(q, qv), ~C.eq(r), C.eq(p), C.ule(qv + 1, p) }, true);
else if (rv != pv)
c.add_axiom("q = 2^k - 1 ==> (p&q)*2^{N - k} = p*2^{N - k}", { ~C.eq(q, qv), C.eq(r * rational::power_of_two(N - pow), p * rational::power_of_two(N - pow)) }, true);
}
if (!pv.is_val() || !qv.is_val() || !rv.is_val())
return;
if (pv.is_max() && qv != rv)
return add_conflict(c, "p = -1 => p & q = q", { ~C.eq(p, m.max_value()), C.eq(q, r) });
if (qv.is_max() && pv != rv)
return add_conflict(c, "q = -1 => p & q = p", { ~C.eq(q, m.max_value()), C.eq(p, r) });
if (pv.is_zero() && !rv.is_zero())
return add_conflict(c, "p = 0 => p & q = 0", { ~C.eq(p), C.eq(r) });
if (qv.is_zero() && !rv.is_zero())
return add_conflict(c, "q = 0 => p & q = 0", { ~C.eq(q), C.eq(r) });
if (propagate_mask(c, p, q, r, pv.val(), qv.val(), rv.val()))
return;
if (propagate_mask(c, q, p, r, qv.val(), pv.val(), rv.val()))
return;
unsigned const N = m.power_of_2();
for (unsigned i = 0; i < N; ++i) {
bool pb = pv.val().get_bit(i);
bool qb = qv.val().get_bit(i);
@ -505,17 +533,73 @@ namespace polysat {
if (rb == (pb && qb))
continue;
if (pb && qb && !rb)
c.add_axiom("p&q[i] = p[i]&q[i]", { ~C.bit(p, i), ~C.bit(q, i), C.bit(r, i) }, true);
add_conflict(c, "p&q[i] = p[i]&q[i]", { ~C.bit(p, i), ~C.bit(q, i), C.bit(r, i) });
else if (!pb && rb)
c.add_axiom("p&q[i] = p[i]&q[i]", { C.bit(p, i), ~C.bit(r, i) }, true);
add_conflict(c, "p&q[i] = p[i]&q[i]", { C.bit(p, i), ~C.bit(r, i) });
else if (!qb && rb)
c.add_axiom("p&q[i] = p[i]&q[i]", { C.bit(q, i), ~C.bit(r, i) }, true);
add_conflict(c, "p&q[i] = p[i]&q[i]", { C.bit(q, i), ~C.bit(r, i) });
else
UNREACHABLE();
return;
}
}
void op_constraint::propagate_or(core& c) {
auto& m = p.manager();
auto pv = c.subst(p);
auto qv = c.subst(q);
auto rv = c.subst(r);
auto& C = c.cs();
verbose_stream() << "propagate or " << p << " | " << q << " = " << r << "\n";
if (!pv.is_val() || !qv.is_val() || !rv.is_val())
return;
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)});
if (qv.is_max() && qv != rv)
return add_conflict(c, "q = -1 => p & q = q", { ~C.eq(q, m.max_value()), C.eq(q, r) });
unsigned const N = m.power_of_2();
for (unsigned i = 0; i < N; ++i) {
bool pb = pv.val().get_bit(i);
bool qb = qv.val().get_bit(i);
bool rb = rv.val().get_bit(i);
if (rb == (pb || qb))
continue;
if (pb && !qb && rb)
add_conflict(c, "p[i] => (p|q)[i]", { ~C.bit(p, i), C.bit(r, i) });
else if (!pb && qb && rb)
add_conflict(c, "q[i] => (p|q)[i]", { ~C.bit(q, i), C.bit(r, i) });
else if (!pb && !qb && rb)
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;
}
}
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) {
auto& m = p.manager();
auto& C = c.cs();
unsigned const N = m.power_of_2();
unsigned pow;
if (!(pv + 1).is_power_of_two(pow))
return false;
if (rv.is_zero() && !qv.is_zero() && qv <= pv) {
add_conflict(c, "p = 2^k - 1 && p & q = 0 && q != 0 => q >= 2^k", { ~C.eq(p, pv), ~C.eq(r), C.eq(q), C.ule(pv + 1, q) });
return true;
}
if (rv != qv) {
add_conflict(c, "p = 2^k - 1 ==> (p&q)*2^{N - k} = q*2^{N - k}", { ~C.eq(p, pv), C.eq(r * rational::power_of_two(N - pow), q * rational::power_of_two(N - pow)) });
return true;
}
return false;
}
}
}

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

@ -35,6 +35,8 @@ namespace polysat {
shl_op,
/// r is the bit-wise 'and' of p and q.
and_op,
/// r is the bit-wise 'or' of p and q.
or_op,
/// r is the smallest multiplicative pseudo-inverse of p;
/// by definition we set r == 0 when p == 0.
/// Note that in general, there are 2^parity(p) many pseudo-inverses of p.
@ -56,12 +58,18 @@ namespace polysat {
static lbool eval_shl(pdd const& p, pdd const& q, pdd const& r);
static lbool eval_and(pdd const& p, pdd const& q, pdd const& r);
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& s, dependency const& dep);
void propagate_ashr(core& s, dependency const& dep);
void propagate_shl(core& s, dependency const& dep);
void propagate_and(core& s, dependency const& dep);
void propagate_inv(core& s, dependency const& dep);
void propagate_lshr(core& c);
void propagate_ashr(core& c);
void propagate_shl(core& c);
void propagate_and(core& c);
void 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);

14
src/sat/smt/polysat/saturation.cpp
View file

@ -51,6 +51,8 @@ namespace polysat {
resolve(v, inequality::from_ule(c, id));
else if (sc.is_umul_ovfl())
try_umul_ovfl(v, umul_ovfl(id, sc));
else if (sc.is_op())
try_op(v, sc, c.get_dependency(id));
return c.inconsistent();
}
@ -238,4 +240,16 @@ namespace polysat {
add_clause("ax + b = 0 & cx + d = 0 ==> cb - da = 0", { i.dep(), j.dep(), C.eq(r) }, true);
}
void saturation::try_op(pvar v, signed_constraint& sc, dependency const& d) {
verbose_stream() << "try op " << sc << "\n";
SASSERT(sc.is_op());
sc.propagate(c, l_true, d);
}
// possible algebraic rule:
// From "Hacker's Delight", section 2-2. Addition Combined with Logical Operations;
// found via Int-Blasting paper; see https://doi.org/10.1007/978-3-030-94583-1_24
// bor(p,q) = (p + q) - band(p, q);
}

1
src/sat/smt/polysat/saturation.h
View file

@ -65,6 +65,7 @@ namespace polysat {
void try_ugt_y(pvar v, inequality const& i);
void try_ugt_z(pvar z, inequality const& i);
void try_umul_ovfl(pvar v, umul_ovfl const& sc);
void try_op(pvar v, signed_constraint& sc, dependency const& d);
signed_constraint ineq(bool is_strict, pdd const& x, pdd const& y);

15
src/sat/smt/polysat_internalize.cpp
View file

@ -215,8 +215,21 @@ namespace polysat {
// found via Int-Blasting paper; see https://doi.org/10.1007/978-3-030-94583-1_24
// (p + q) - band(p, q);
void solver::internalize_bor(app* n) {
internalize_binary(n, [&](expr* const& x, expr* const& y) { return bv.mk_bv_sub(bv.mk_bv_add(x, y), bv.mk_bv_and(x, y)); });
if (n->get_num_args() == 2) {
expr* x, * y;
VERIFY(bv.is_bv_or(n, x, y));
m_core.bor(expr2pdd(x), expr2pdd(y), expr2pdd(n));
}
else {
expr_ref z(n->get_arg(0), m);
for (unsigned i = 1; i < n->get_num_args(); ++i) {
z = bv.mk_bv_or(z, n->get_arg(i));
ctx.internalize(z);
}
internalize_set(n, expr2pdd(z));
}
}
// From "Hacker's Delight", section 2-2. Addition Combined with Logical Operations;
// found via Int-Blasting paper; see https://doi.org/10.1007/978-3-030-94583-1_24