mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-13 09:26:15 +00:00
Code Activity

experiment

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-12-03 06:32:34 -08:00
parent 68d9b44d67
commit ff22b433cc
1 changed files with 13 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -87,12 +87,25 @@ namespace {
lhs = 0, rhs = 0, is_positive = !is_positive; lhs = 0, rhs = 0, is_positive = !is_positive;
return; return;
} }
#if 0
// !(k <= p) -> p <= k - 1
if (!is_positive && lhs.is_val() && lhs.val() > 0) {
pdd k = lhs;
lhs = rhs;
rhs = k - 1;
is_positive = true;
}
#endif
// k <= p --> p - k <= - k - 1 // k <= p --> p - k <= - k - 1
if (lhs.is_val()) { if (lhs.is_val()) {
pdd k = lhs; pdd k = lhs;
lhs = rhs - k; lhs = rhs - k;
rhs = - k - 1; rhs = - k - 1;
} }
// NSB: why this?
// p > -2 --> p + 1 <= 0 // p > -2 --> p + 1 <= 0
// p <= -2 --> p + 1 > 0 // p <= -2 --> p + 1 > 0
if (rhs.is_val() && (rhs + 2).is_zero()) { if (rhs.is_val() && (rhs + 2).is_zero()) {