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

Fix parity lemma

Browse source
This commit is contained in:
Jakob Rath 2023-03-13 07:55:42 +01:00
parent 69fbfc3616
commit 3b7b7a6867
1 changed files with 6 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -563,8 +563,14 @@ namespace polysat {
if (prodv < rational::power_of_two(middle)) if (prodv < rational::power_of_two(middle))
return s.mk_clause("r = inv p & parity(p) >= k ==> p*r >= 2^k", return s.mk_clause("r = inv p & parity(p) >= k ==> p*r >= 2^k",
{~invc, ~s.parity_at_least(p(), middle), s.uge(prod, rational::power_of_two(middle))}, false); {~invc, ~s.parity_at_least(p(), middle), s.uge(prod, rational::power_of_two(middle))}, false);
// parity(p) >= k ==> r <= 2^(N - k) - 1 (because r is the smallest pseudo-inverse)
rational const max_rv = rational::power_of_two(m.power_of_2() - middle) - 1;
if (rv.val() > max_rv)
return s.mk_clause("r = inv p & parity(p) >= k ==> r <= 2^(N - k) - 1",
{~invc, ~s.parity_at_least(p(), middle), s.ule(r(), max_rv)}, false);
} }
else { // parity less than middle else { // parity less than middle
SASSERT(parity_pv < middle);
upper = middle; upper = middle;
LOG("Its in [" << lower << "; " << upper << ")"); LOG("Its in [" << lower << "; " << upper << ")");
// parity(p) < k ==> p * r <= 2^k - 1 // parity(p) < k ==> p * r <= 2^k - 1
@ -572,11 +578,6 @@ namespace polysat {
return s.mk_clause("r = inv p & parity(p) < k ==> p*r <= 2^k - 1", return s.mk_clause("r = inv p & parity(p) < k ==> p*r <= 2^k - 1",
{~invc, s.parity_at_least(p(), middle), s.ule(prod, rational::power_of_two(middle) - 1)}, false); {~invc, s.parity_at_least(p(), middle), s.ule(prod, rational::power_of_two(middle) - 1)}, false);
} }
// parity(p) < k ==> r <= 2^(N - k) - 1 (because r is the smallest pseudo-inverse)
rational const max_rv = rational::power_of_two(m.power_of_2() - middle) - 1;
if (rv.val() > max_rv)
return s.mk_clause("r = inv p & parity(p) < k ==> r <= 2^(N-k) - 1",
{~invc, s.parity_at_least(p(), middle), s.ule(r(), max_rv)}, false);
} }
// Why did it evaluate to false in this case? // Why did it evaluate to false in this case?
UNREACHABLE(); UNREACHABLE();