mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 17:45:32 +00:00
Code Activity

avoid fallback to circuit

Browse source
This commit is contained in:
Jakob Rath 2023-02-20 12:09:11 +01:00
parent 7f41761616
commit af683ea5f9
2 changed files with 13 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/sat/smt/bv_internalize.cpp
View file

@ -199,8 +199,8 @@ namespace bv {
case OP_BAND: internalize_ac(mk_and); break;
case OP_BOR: internalize_ac(mk_or); break;
case OP_BXOR: internalize_ac(mk_xor); break;
case OP_BNAND: internalize_bin(mk_nand); break;
case OP_BNOR: internalize_bin(mk_nor); break;
case OP_BNAND: if_unary(mk_not); internalize_bin(mk_nand); break;
case OP_BNOR: if_unary(mk_not); internalize_bin(mk_nor); break;
case OP_BXNOR: if_unary(mk_not); internalize_bin(mk_xnor); break;
case OP_BCOMP: internalize_bin(mk_comp); break;
case OP_SIGN_EXT: internalize_pun(mk_sign_extend); break;

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

@ -32,6 +32,8 @@ namespace bv {
void solver::internalize_polysat(app* a) {
#define if_unary(F) if (a->get_num_args() == 1) { polysat_unary(a, [&](pdd const& p) { return F(p); }); break; }
switch (to_app(a)->get_decl_kind()) {
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;
@ -41,9 +43,9 @@ namespace bv {
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_BXNOR: polysat_binary(a, [&](pdd const& p, pdd const& q) { return m_polysat.bxnor(p, q); }); break;
case OP_BNAND: if_unary(m_polysat.bnot); polysat_binary(a, [&](pdd const& p, pdd const& q) { return m_polysat.bnand(p, q); }); break;
case OP_BNOR: if_unary(m_polysat.bnot); polysat_binary(a, [&](pdd const& p, pdd const& q) { return m_polysat.bnor(p, q); }); break;
case OP_BXNOR: if_unary(m_polysat.bnot); polysat_binary(a, [&](pdd const& p, pdd const& q) { return m_polysat.bxnor(p, q); }); break;
case OP_BNOT: polysat_unary(a, [&](pdd const& p) { return m_polysat.bnot(p); }); break;
case OP_BNEG: polysat_unary(a, [&](pdd const& p) { return -p; }); break;
@ -94,9 +96,15 @@ namespace bv {
return;
default:
std::cout << "fall back to circuit " << mk_pp(a, m) << "\n";
NOT_IMPLEMENTED_YET();
return;
#if 0
// TODO: this path leads to segfault / floating point exception
internalize_circuit(a);
break;
#endif
}
#undef if_unary
}
void solver::polysat_binaryc(app* e, std::function<polysat::signed_constraint(polysat::pdd, polysat::pdd)> const& fn) {