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

xnor

Browse source
This commit is contained in:
Jakob Rath 2023-02-20 11:56:23 +01:00
parent 4501a372b1
commit 7f41761616
4 changed files with 9 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/math/polysat/constraint_manager.cpp
View file

@ -502,6 +502,10 @@ namespace polysat {
pdd constraint_manager::bnor(pdd const& p, pdd const& q) {
return bnot(bor(p, q));
}
pdd constraint_manager::bxnor(pdd const& p, pdd const& q) {
return bnot(bxor(p, q));
}
pdd constraint_manager::pseudo_inv(pdd const& p) {
auto& m = p.manager();

1
src/math/polysat/constraint_manager.h
View file

@ -130,6 +130,7 @@ namespace polysat {
pdd bxor(pdd const& p, pdd const& q);
pdd bnand(pdd const& p, pdd const& q);
pdd bnor(pdd const& p, pdd const& q);
pdd bxnor(pdd const& p, pdd const& q);
pdd pseudo_inv(pdd const& p);
constraint* const* begin() const { return m_constraints.data(); }

3
src/math/polysat/solver.h
View file

@ -403,6 +403,9 @@ namespace polysat {
/** Create expression for bit-wise xor of p, q. */
pdd bxor(pdd const& p, pdd const& q) { return m_constraints.bxor(p, q); }
/** Create expression for bit-wise xnor of p, q. */
pdd bxnor(pdd const& p, pdd const& q) { return m_constraints.bxnor(p, q); }
/** Create expression for bit-wise nand of p, q. */
pdd bnand(pdd const& p, pdd const& q) { return m_constraints.bnand(p, q); }

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

@ -43,6 +43,7 @@ namespace bv {
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_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;