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

Add basic support for not, or, xor, nand, nor via rewriting

Browse source
This commit is contained in:
Jakob Rath 2022-09-30 12:59:23 +02:00
parent 9b907d709f
commit 5e54cd3e44
4 changed files with 81 additions and 36 deletions
Download patch file Download diff file Expand all files Collapse all files

26
src/math/polysat/solver.cpp
View file

@ -166,6 +166,10 @@ namespace polysat {
return r;
}
pdd solver::bnot(pdd const& p) {
return -p - 1;
}
pdd solver::band(pdd const& p, pdd const& q) {
auto& m = p.manager();
unsigned sz = m.power_of_2();
@ -174,6 +178,28 @@ namespace polysat {
return r;
}
pdd solver::bor(pdd const& p, pdd const& q) {
// 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
// TODO: switch to op_constraint once supported
return (p + q) - band(p, q);
}
pdd solver::bxor(pdd const& p, pdd const& q) {
// 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
// TODO: switch to op_constraint once supported
return bor(p, q) - band(p, q);
// return (p + q) - 2*band(p, q);
}
pdd solver::bnand(pdd const& p, pdd const& q) {
return bnot(band(p, q));
}
pdd solver::bnor(pdd const& p, pdd const& q) {
return bnot(bor(p, q));
}
void solver::assign_eh(signed_constraint c, dependency dep) {
backjump(base_level());

31
src/math/polysat/solver.h
View file

@ -294,15 +294,40 @@ namespace polysat {
std::tuple<pdd, pdd> quot_rem(pdd const& a, pdd const& b);
/**
* Create expression for the logical right shift of p by q.
*/
* Create expression for the logical right shift of p by q.
*/
pdd lshr(pdd const& p, pdd const& q);
/**
* Create expression for bit-wise and of p by q.
* Create expression for the bit-wise negation of p.
*/
pdd bnot(pdd const& p);
/**
* Create expression for bit-wise and of p, q.
*/
pdd band(pdd const& p, pdd const& q);
/**
* Create expression for bit-wise or of p, q.
*/
pdd bor(pdd const& p, pdd const& q);
/**
* Create expression for bit-wise xor of p, q.
*/
pdd bxor(pdd const& p, pdd const& q);
/**
* Create expression for bit-wise nand of p, q.
*/
pdd bnand(pdd const& p, pdd const& q);
/**
* Create expression for bit-wise nor of p, q.
*/
pdd bnor(pdd const& p, pdd const& q);
/**
* Create polynomial constant.
*/

54
src/sat/smt/bv_polysat.cpp
View file

@ -32,20 +32,19 @@ namespace bv {
void solver::internalize_polysat(app* a) {
std::function<polysat::pdd(polysat::pdd, polysat::pdd)> bin;
std::function<polysat::signed_constraint(polysat::pdd, polysat::pdd)> binc;
#define mk_binary(a, fn) bin = fn; polysat_binary(a, bin);
#define mk_binaryc(a, fn) binc = fn; polysat_binaryc(a, binc);
switch (to_app(a)->get_decl_kind()) {
case OP_BMUL: mk_binary(a, [&](pdd const& p, pdd const& q) { return p * q; }); break;
case OP_BADD: mk_binary(a, [&](pdd const& p, pdd const& q) { return p + q; }); break;
case OP_BSUB: mk_binary(a, [&](pdd const& p, pdd const& q) { return p - q; }); break;
case OP_BLSHR: mk_binary(a, [&](pdd const& p, pdd const& q) { return m_polysat.lshr(p, q); }); break;
case OP_BAND: mk_binary(a, [&](pdd const& p, pdd const& q) { return m_polysat.band(p, q); }); break;
case OP_BMUL: polysat_binary(a, [&](pdd const& p, pdd const& q) { return p * q; }); break;
case OP_BADD: polysat_binary(a, [&](pdd const& p, pdd const& q) { return p + q; }); break;
case OP_BSUB: polysat_binary(a, [&](pdd const& p, pdd const& q) { return p - q; }); break;
case OP_BLSHR: polysat_binary(a, [&](pdd const& p, pdd const& q) { return m_polysat.lshr(p, q); }); break;
case OP_BAND: polysat_binary(a, [&](pdd const& p, pdd const& q) { return m_polysat.band(p, q); }); break;
case OP_BOR: polysat_binary(a, [&](pdd const& p, pdd const& q) { return m_polysat.bor(p, q); }); break;
case OP_BXOR: polysat_binary(a, [&](pdd const& p, pdd const& q) { return m_polysat.bxor(p, q); }); break;
case OP_BNAND: polysat_binary(a, [&](pdd const& p, pdd const& q) { return m_polysat.bnand(p, q); }); break;
case OP_BNOR: polysat_binary(a, [&](pdd const& p, pdd const& q) { return m_polysat.bnor(p, q); }); break;
case OP_BNOT: polysat_unary(a, [&](pdd const& p) { return m_polysat.bnot(p); }); break;
case OP_BNEG: polysat_neg(a); break;
case OP_BNEG: polysat_unary(a, [&](pdd const& p) { return -p; }); break;
case OP_MKBV: polysat_mkbv(a); break;
case OP_BV_NUM: polysat_num(a); break;
@ -58,9 +57,9 @@ namespace bv {
case OP_UGT: polysat_le<false, false, true>(a); break;
case OP_SGT: polysat_le<true, false, true>(a); break;
case OP_BUMUL_NO_OVFL: mk_binaryc(a, [&](pdd const& p, pdd const& q) { return m_polysat.umul_ovfl(p, q); }); break;
case OP_BSMUL_NO_OVFL: mk_binaryc(a, [&](pdd const& p, pdd const& q) { return m_polysat.smul_ovfl(p, q); }); break;
case OP_BSMUL_NO_UDFL: mk_binaryc(a, [&](pdd const& p, pdd const& q) { return m_polysat.smul_udfl(p, q); }); break;
case OP_BUMUL_NO_OVFL: polysat_binaryc(a, [&](pdd const& p, pdd const& q) { return m_polysat.umul_ovfl(p, q); }); break;
case OP_BSMUL_NO_OVFL: polysat_binaryc(a, [&](pdd const& p, pdd const& q) { return m_polysat.smul_ovfl(p, q); }); break;
case OP_BSMUL_NO_UDFL: polysat_binaryc(a, [&](pdd const& p, pdd const& q) { return m_polysat.smul_udfl(p, q); }); break;
case OP_BUDIV_I: polysat_div_rem_i(a, true); break;
case OP_BUREM_I: polysat_div_rem_i(a, false); break;
@ -84,11 +83,6 @@ namespace bv {
case OP_BSMOD_I:
case OP_BSHL:
case OP_BASHR:
case OP_BOR:
case OP_BXOR:
case OP_BNAND:
case OP_BNOR:
case OP_BNOT:
case OP_BCOMP:
case OP_SIGN_EXT:
case OP_ZERO_EXT:
@ -104,7 +98,7 @@ namespace bv {
}
}
void solver::polysat_binaryc(app* e, std::function<polysat::signed_constraint(polysat::pdd, polysat::pdd)>& fn) {
void solver::polysat_binaryc(app* e, std::function<polysat::signed_constraint(polysat::pdd, polysat::pdd)> const& fn) {
auto p = expr2pdd(e->get_arg(0));
auto q = expr2pdd(e->get_arg(1));
auto sc = ~fn(p, q);
@ -139,12 +133,6 @@ namespace bv {
ctx.add_aux(eqZ, eqI);
}
void solver::polysat_neg(app* e) {
SASSERT(e->get_num_args() == 1);
auto p = expr2pdd(e->get_arg(0));
polysat_set(e, -p);
}
void solver::polysat_num(app* a) {
numeral val;
unsigned sz = 0;
@ -167,7 +155,7 @@ namespace bv {
}
}
void solver::polysat_binary(app* e, std::function<polysat::pdd(polysat::pdd, polysat::pdd)>& fn) {
void solver::polysat_binary(app* e, std::function<polysat::pdd(polysat::pdd, polysat::pdd)> const& fn) {
SASSERT(e->get_num_args() >= 1);
auto p = expr2pdd(e->get_arg(0));
for (unsigned i = 1; i < e->get_num_args(); ++i)
@ -175,6 +163,12 @@ namespace bv {
polysat_set(e, p);
}
void solver::polysat_unary(app* e, std::function<polysat::pdd(polysat::pdd)> const& fn) {
SASSERT(e->get_num_args() == 1);
auto p = expr2pdd(e->get_arg(0));
polysat_set(e, fn(p));
}
template<bool Signed, bool Rev, bool Negated>
void solver::polysat_le(app* e) {
auto p = expr2pdd(e->get_arg(0));
@ -309,8 +303,8 @@ namespace bv {
ctx.push(set_bitvector_trail(m_var2pdd_valid, v));
m_var2pdd[v] = p;
#ifndef NDEBUG
expr* e = var2enode(v)->get_expr();
std::cerr << "polysat_set: " << mk_ismt2_pp(e, m) << " -> " << p << std::endl;
expr* e = var2enode(v)->get_expr();
std::cerr << "polysat_set: " << mk_ismt2_pp(e, m) << " -> " << p << std::endl;
#endif
}

6
src/sat/smt/bv_solver.h
View file

@ -286,17 +286,17 @@ namespace bv {
void internalize_polysat(app* a);
void polysat_push();
void polysat_pop(unsigned n);
void polysat_binary(app* e, std::function<polysat::pdd(polysat::pdd, polysat::pdd)>& fn);
void polysat_unary(app* e, std::function<polysat::pdd(polysat::pdd)> const& fn);
void polysat_binary(app* e, std::function<polysat::pdd(polysat::pdd, polysat::pdd)> const& fn);
polysat::pdd expr2pdd(expr* e);
void polysat_set(euf::theory_var v, polysat::pdd const& p);
polysat::pdd var2pdd(euf::theory_var v);
void polysat_set(expr* e, polysat::pdd const& p);
template<bool Signed, bool Reverse, bool Negated>
void polysat_le(app* n);
void polysat_neg(app* a);
void polysat_num(app* a);
void polysat_mkbv(app* a);
void polysat_binaryc(app* e, std::function<polysat::signed_constraint(polysat::pdd, polysat::pdd)>& fn);
void polysat_binaryc(app* e, std::function<polysat::signed_constraint(polysat::pdd, polysat::pdd)> const& fn);
void polysat_div_rem_i(app* e, bool is_div);
void polysat_div_rem(app* e, bool is_div);
void polysat_bit2bool(atom* a, expr* e, unsigned idx);