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

For r = p & q: "p = 0 => r = 0" is subsumed by "r <= p"

Browse source
This commit is contained in:
Jakob Rath 2022-11-30 11:35:36 +01:00
parent e6eea83b67
commit 4026ac9427
1 changed files with 6 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/math/polysat/op_constraint.cpp
View file

@ -311,15 +311,15 @@ namespace polysat {
}
/**
* Produce lemmas:
* p & q <= p
* p & q <= q
* p = q => p & q = r
* p = 0 => r = 0
* q = 0 => r = 0
* Produce lemmas for constraint: r == p & q
* r <= p
* r <= q
* p = q => r = p
* p[i] && q[i] = r[i]
*
* Possible other:
* r = 0 && q = 2^k-1 => p >= 2^k
* r = 0 && p = 2^k-1 => q >= 2^k
* p = max_value => q = r
* q = max_value => p = r
*/
@ -335,10 +335,6 @@ namespace polysat {
s.add_clause(~andc, s.ule(r(), q()), true);
else if (pv.is_val() && qv.is_val() && rv.is_val() && pv == qv && rv != pv)
s.add_clause(~andc, ~s.eq(p(), q()), s.eq(r(), p()), true);
else if (pv.is_zero() && rv.is_val() && !rv.is_zero())
s.add_clause(~andc, ~s.eq(p()), s.eq(r()), true);
else if (qv.is_zero() && rv.is_val() && !rv.is_zero())
s.add_clause(~andc, ~s.eq(q()), s.eq(r()), true);
else if (pv.is_val() && qv.is_val() && rv.is_val()) {
unsigned K = p().manager().power_of_2();
for (unsigned i = 0; i < K; ++i) {