mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-09 20:50:50 +00:00
Code Activity

alternative bor

Browse source
This commit is contained in:
Jakob Rath 2023-03-29 15:57:15 +02:00
parent 0704f90e9f
commit 5e16a17f90
1 changed files with 6 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -523,9 +523,15 @@ namespace polysat {
} }
pdd constraint_manager::bor(pdd const& p, pdd const& q) { pdd constraint_manager::bor(pdd const& p, pdd const& q) {
#if 1
// From "Hacker's Delight", section 2-2. Addition Combined with Logical Operations; // 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 // found via Int-Blasting paper; see https://doi.org/10.1007/978-3-030-94583-1_24
return (p + q) - band(p, q); return (p + q) - band(p, q);
#else
// Alternatively, de Morgan:
// (advantage: only one occurrence of p, q)
return bnot(band(bnot(p), bnot(q)));
#endif
} }
pdd constraint_manager::bxor(pdd const& p, pdd const& q) { pdd constraint_manager::bxor(pdd const& p, pdd const& q) {