mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-22 13:53:39 +00:00
Code Activity

Normalize to 0 < 0 instead of 1 <= 0

Browse source
This commit is contained in:
Jakob Rath 2022-11-07 15:32:34 +01:00
parent e7c77a22ab
commit eaf38abf17
1 changed files with 4 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/math/polysat/ule_constraint.cpp
View file

@ -84,7 +84,7 @@ namespace {
if (lhs.val() <= rhs.val()) if (lhs.val() <= rhs.val())
lhs = 0, rhs = 0; lhs = 0, rhs = 0;
else else
lhs = 1, rhs = 0; lhs = 0, rhs = 0, is_positive = !is_positive;
return; return;
} }
// k <= p --> p - k <= - k - 1 // k <= p --> p - k <= - k - 1
@ -100,9 +100,10 @@ namespace {
rhs = 0; rhs = 0;
is_positive = !is_positive; is_positive = !is_positive;
} }
// 2p + 1 <= 0 --> 1 <= 0 // 2p + 1 <= 0 --> 0 < 0
if (rhs.is_zero() && lhs.is_never_zero()) { if (rhs.is_zero() && lhs.is_never_zero()) {
lhs = 1; lhs = 0;
is_positive = !is_positive;
return; return;
} }
// a*p + q <= 0 --> p + a^-1*q <= 0 for a odd // a*p + q <= 0 --> p + a^-1*q <= 0 for a odd