mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 00:26:38 +00:00
Code Activity

remove old code/notes

Browse source
This commit is contained in:
Jakob Rath 2023-03-29 16:14:01 +02:00
parent 5e16a17f90
commit f9147a7dc0
1 changed files with 5 additions and 26 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -64,7 +64,9 @@ The following forms are equivalent:
Useful lemmas:
- p <= q ==> p == 0 || -q <= -p
p <= q && q+1 != 0 ==> p+1 <= q+1
p <= q && p != 0 ==> -q <= -p
--*/
@ -104,19 +106,6 @@ namespace {
return;
}
#if 0
// simple version that we had for a long time, subsumed by rule in #else
// p + 1 <= p --> p + 1 <= 0
// p <= p - 1 --> p <= 0
//
// p + k <= p --> p + k <= k - 1
// p <= p - k --> p <= k - 1
if ((lhs - rhs).is_val()) {
pdd k = lhs - rhs;
rhs = k - 1;
}
#else
// Try to reduce the number of variables on one side using one of these rules:
//
// p <= q --> p <= p - q - 1
@ -144,11 +133,11 @@ namespace {
// verbose_stream() << "OUT: " << ule_pp(to_lbool(is_positive), lhs, rhs) << "\n";
}
}
#endif
#if 0
// TODO: maybe enable this later to make some constraints more "readable"
// TODO: maybe enable this later to make some constraints more readable
// p - k <= -k - 1 --> k <= p
// ALTERNATIVE: p > k-1 to keep the polynomial on the lhs? allows us to have boolean conflicts between x <= k and x > k ? (otherwise it is x <= k and k+1 <= x.)
if (rhs.is_val() && !rhs.is_zero() && lhs.offset() == (rhs + 1).val()) {
// verbose_stream() << "IN: " << ule_pp(to_lbool(is_positive), lhs, rhs) << "\n";
std::abort();
@ -172,16 +161,6 @@ namespace {
is_positive = !is_positive;
}
#if 0
// TODO: enabling this rule leads to unsoundness in 1041-minimized (but the rule itself is correct)
// k <= p --> p - k <= - k - 1
if (lhs.is_val()) {
pdd k = lhs;
lhs = rhs - k;
rhs = - k - 1;
}
#endif
// p > -2 --> p + 1 <= 0
// p <= -2 --> p + 1 > 0
if (rhs.is_val() && !rhs.is_zero() && (rhs + 2).is_zero()) {