diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index ac581f385..ce7d34d4c 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -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()); diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h index 81cb0fb65..bc6fb4582 100644 --- a/src/math/polysat/solver.h +++ b/src/math/polysat/solver.h @@ -294,15 +294,40 @@ namespace polysat { std::tuple 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. */ diff --git a/src/sat/smt/bv_polysat.cpp b/src/sat/smt/bv_polysat.cpp index d30b7f9ad..341335a7a 100644 --- a/src/sat/smt/bv_polysat.cpp +++ b/src/sat/smt/bv_polysat.cpp @@ -32,20 +32,19 @@ namespace bv { void solver::internalize_polysat(app* a) { - std::function bin; - std::function 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(a); break; case OP_SGT: polysat_le(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& fn) { + void solver::polysat_binaryc(app* e, std::function 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& fn) { + void solver::polysat_binary(app* e, std::function 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 const& fn) { + SASSERT(e->get_num_args() == 1); + auto p = expr2pdd(e->get_arg(0)); + polysat_set(e, fn(p)); + } + template 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 } diff --git a/src/sat/smt/bv_solver.h b/src/sat/smt/bv_solver.h index 8241415f9..b9b4088a7 100644 --- a/src/sat/smt/bv_solver.h +++ b/src/sat/smt/bv_solver.h @@ -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& fn); + void polysat_unary(app* e, std::function const& fn); + void polysat_binary(app* e, std::function 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 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& fn); + void polysat_binaryc(app* e, std::function 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);