diff --git a/src/ast/bv_decl_plugin.h b/src/ast/bv_decl_plugin.h index 9126b97b7..4eeac49ee 100644 --- a/src/ast/bv_decl_plugin.h +++ b/src/ast/bv_decl_plugin.h @@ -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); diff --git a/src/sat/smt/polysat/core.h b/src/sat/smt/polysat/core.h index b303ff8b8..b70e70d9b 100644 --- a/src/sat/smt/polysat/core.h +++ b/src/sat/smt/polysat/core.h @@ -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(); } diff --git a/src/sat/smt/polysat_internalize.cpp b/src/sat/smt/polysat_internalize.cpp index 709ae5da3..0afcf06d4 100644 --- a/src/sat/smt/polysat_internalize.cpp +++ b/src/sat/smt/polysat_internalize.cpp @@ -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 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 const& fn) { SASSERT(e->get_num_args() == 1); auto p = expr2pdd(e->get_arg(0)); diff --git a/src/sat/smt/polysat_solver.h b/src/sat/smt/polysat_solver.h index 3b5eb27ba..f3435f364 100644 --- a/src/sat/smt/polysat_solver.h +++ b/src/sat/smt/polysat_solver.h @@ -98,6 +98,7 @@ namespace polysat { void add_def(sat::literal def, sat::literal l); void internalize_unary(app* e, std::function const& fn); void internalize_binary(app* e, std::function const& fn); + void internalize_binary(app* e, std::function const& fn); void internalize_binaryc(app* e, std::function const& fn); void internalize_par_unary(app* e, std::function const& fn); void internalize_novfl(app* n, std::function& 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 void internalize_le(app* n); void internalize_zero_extend(app* n);