mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 00:26:38 +00:00
Code Activity

more internalize cases

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-12-10 23:49:23 -08:00
parent 286932684a
commit f89de2b455
4 changed files with 58 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/ast/bv_decl_plugin.h
View file

@ -411,6 +411,12 @@ public:
MATCH_BINARY(is_bv_sdiv);
MATCH_BINARY(is_bv_udiv);
MATCH_BINARY(is_bv_smod);
MATCH_BINARY(is_bv_and);
MATCH_BINARY(is_bv_or);
MATCH_BINARY(is_bv_xor);
MATCH_BINARY(is_bv_nand);
MATCH_BINARY(is_bv_nor);
MATCH_BINARY(is_bv_uremi);
MATCH_BINARY(is_bv_sremi);

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

@ -119,12 +119,9 @@ namespace polysat {
pdd ashr(pdd a, pdd b) { NOT_IMPLEMENTED_YET(); throw default_exception("ashr nyi"); }
pdd shl(pdd a, pdd b) { NOT_IMPLEMENTED_YET(); throw default_exception("shlh nyi"); }
pdd band(pdd a, pdd b) { NOT_IMPLEMENTED_YET(); throw default_exception("band nyi"); }
pdd bxor(pdd a, pdd b) { NOT_IMPLEMENTED_YET(); throw default_exception("bxor nyi"); }
pdd bor(pdd a, pdd b) { NOT_IMPLEMENTED_YET(); throw default_exception("bir ==nyi"); }
pdd bnand(pdd a, pdd b) { NOT_IMPLEMENTED_YET(); throw default_exception("bnand nyi"); }
pdd bxnor(pdd a, pdd b) { NOT_IMPLEMENTED_YET(); throw default_exception("bxnor nyi"); }
pdd bnor(pdd a, pdd b) { NOT_IMPLEMENTED_YET(); throw default_exception("bnotr nyi"); }
pdd bnot(pdd a) { NOT_IMPLEMENTED_YET(); throw default_exception("bnot nyi"); }
pdd bnot(pdd a) { return -a - 1; }
pvar add_var(unsigned sz);
pdd var(pvar p) { return m_vars[p]; }
unsigned size(pvar v) const { return m_vars[v].power_of_2(); }

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

@ -87,11 +87,11 @@ namespace polysat {
case OP_BLSHR: internalize_binary(a, [&](pdd const& p, pdd const& q) { return m_core.lshr(p, q); }); break;
case OP_BSHL: internalize_binary(a, [&](pdd const& p, pdd const& q) { return m_core.shl(p, q); }); break;
case OP_BAND: internalize_binary(a, [&](pdd const& p, pdd const& q) { return m_core.band(p, q); }); break;
case OP_BOR: internalize_binary(a, [&](pdd const& p, pdd const& q) { return m_core.bor(p, q); }); break;
case OP_BXOR: internalize_binary(a, [&](pdd const& p, pdd const& q) { return m_core.bxor(p, q); }); break;
case OP_BNAND: if_unary(m_core.bnot); internalize_binary(a, [&](pdd const& p, pdd const& q) { return m_core.bnand(p, q); }); break;
case OP_BNOR: if_unary(m_core.bnot); internalize_binary(a, [&](pdd const& p, pdd const& q) { return m_core.bnor(p, q); }); break;
case OP_BXNOR: if_unary(m_core.bnot); internalize_binary(a, [&](pdd const& p, pdd const& q) { return m_core.bxnor(p, q); }); break;
case OP_BOR: internalize_bor(a); break;
case OP_BXOR: internalize_bxor(a); break;
case OP_BNAND: if_unary(m_core.bnot); internalize_bnand(a); break;
case OP_BNOR: if_unary(m_core.bnot); internalize_bnor(a); break;
case OP_BXNOR: if_unary(m_core.bnot); internalize_bxnor(a); break;
case OP_BNOT: internalize_unary(a, [&](pdd const& p) { return m_core.bnot(p); }); break;
case OP_BNEG: internalize_unary(a, [&](pdd const& p) { return -p; }); break;
case OP_MKBV: internalize_mkbv(a); break;
@ -202,6 +202,34 @@ namespace polysat {
internalize(rm);
}
// 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
// (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)); });
}
// 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
// (p + q) - 2*band(p, q);
void solver::internalize_bxor(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_add(bv.mk_bv_and(x, y), bv.mk_bv_and(x, y)));
});
}
void solver::internalize_bnor(app* n) {
internalize_binary(n, [&](expr* const& x, expr* const& y) { return bv.mk_bv_not(bv.mk_bv_or(x, y)); });
}
void solver::internalize_bnand(app* n) {
internalize_binary(n, [&](expr* const& x, expr* const& y) { return bv.mk_bv_not(bv.mk_bv_and(x, y)); });
}
void solver::internalize_bxnor(app* n) {
internalize_binary(n, [&](expr* const& x, expr* const& y) { return bv.mk_bv_not(bv.mk_bv_xor(x, y)); });
}
void solver::internalize_urem_i(app* rem) {
expr* x, *y;
euf::enode* n = expr2enode(rem);
@ -317,7 +345,7 @@ namespace polysat {
void solver::internalize_div_rem(app* e, bool is_div) {
bv_rewriter_params p(s().params());
if (p.hi_div0()) {
if (bv.is_bv_udivi(e))
if (is_div)
internalize_udiv_i(e);
else
internalize_urem_i(e);
@ -385,6 +413,15 @@ namespace polysat {
internalize_set(e, p);
}
void solver::internalize_binary(app* e, std::function<expr* (expr*, expr*)> const& fn) {
SASSERT(e->get_num_args() >= 1);
expr* r = e->get_arg(0);
for (unsigned i = 1; i < e->get_num_args(); ++i)
r = fn(r, e->get_arg(i));
ctx.internalize(r);
internalize_set(e, var2pdd(expr2enode(r)->get_th_var(get_id())));
}
void solver::internalize_unary(app* e, std::function<pdd(pdd)> const& fn) {
SASSERT(e->get_num_args() == 1);
auto p = expr2pdd(e->get_arg(0));

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

@ -98,6 +98,7 @@ namespace polysat {
void add_def(sat::literal def, sat::literal l);
void internalize_unary(app* e, std::function<pdd(pdd)> const& fn);
void internalize_binary(app* e, std::function<pdd(pdd, pdd)> const& fn);
void internalize_binary(app* e, std::function<expr*(expr*, expr*)> const& fn);
void internalize_binaryc(app* e, std::function<signed_constraint(pdd, pdd)> const& fn);
void internalize_par_unary(app* e, std::function<pdd(pdd,unsigned)> const& fn);
void internalize_novfl(app* n, std::function<void(unsigned, expr* const*, expr* const*, expr_ref&)>& fn);
@ -113,6 +114,11 @@ namespace polysat {
void internalize_extract(app* n);
void internalize_repeat(app* n);
void internalize_bit2bool(app* n);
void internalize_bor(app* n);
void internalize_bxor(app* n);
void internalize_bnor(app* n);
void internalize_bnand(app* n);
void internalize_bxnor(app* n);
template<bool Signed, bool Reverse, bool Negated>
void internalize_le(app* n);
void internalize_zero_extend(app* n);