mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-05 17:14:07 +00:00
Code Activity

#5722 - internalize unary xnor

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-12-22 13:32:53 -08:00
parent 4d8bf2a874
commit 71b868d7f6
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -166,6 +166,7 @@ namespace bv {
#define internalize_pun(F) pun = [&](unsigned sz, expr* const* xs, unsigned p, expr_ref_vector& bits) { m_bb.F(sz, xs, p, bits);}; internalize_par_unary(a, pun);
#define internalize_nfl(F) ebin = [&](unsigned sz, expr* const* xs, expr* const* ys, expr_ref& out) { m_bb.F(sz, xs, ys, out);}; internalize_novfl(a, ebin);
#define internalize_int(B, U) ibin = [&](expr* x, expr* y) { return B(x, y); }; iun = [&](expr* x) { return U(x); }; internalize_interp(a, ibin, iun);
#define if_unary(F) if (a->get_num_args() == 1) { internalize_un(F); break; }
switch (a->get_decl_kind()) {
case OP_BV_NUM: internalize_num(a); break;
@ -190,7 +191,7 @@ namespace bv {
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_BXNOR: internalize_bin(mk_xnor); 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;
case OP_ZERO_EXT: internalize_pun(mk_zero_extend); break;