mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-04 18:30:24 +00:00
Code Activity

disable old bounds prop as it is unsound

Browse source
This commit is contained in:
Jakob Rath 2023-03-11 11:22:24 +01:00
parent 592b206097
commit 3096ddaf33
1 changed files with 14 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/math/polysat/saturation.cpp
View file

@ -1608,8 +1608,21 @@ namespace polysat {
verbose_stream() << "& " << s.ule(c, c_val) << "\n"; verbose_stream() << "& " << s.ule(c, c_val) << "\n";
verbose_stream() << "& " << s.ule(y, y_val) << "\n"; verbose_stream() << "& " << s.ule(y, y_val) << "\n";
verbose_stream() << "==> " << -a << " >= " << dd::val_pp(m, bound, false) << "\n"); verbose_stream() << "==> " << -a << " >= " << dd::val_pp(m, bound, false) << "\n");
if (propagate(x, core, a_l_b, conclusion)) // this is broken!
// creates e.g. the "conflict":
// 78: -1*v7*v1 <= 7 [ b:l_true p:l_true eval@0 pwatched ]
// 93: v7 <= 7 [ b:l_true p:l_true eval@0 pwatched ]
// -94: 8 > v1 [ b:l_true p:l_true eval@0 pwatched ]
// As lemma:
// -1*v7*v1 <= 7 & v7 <= 7 ==> 8 <= v1
// need to add at least v1 != 0 | v7 != 0 to the conclusion?
// (assignment v1 := 0, v7 := 0; so there is no need to propagate anything as the constraint is satisfied anyway.)
// Anyway, disable for now as the new bounds propagation should eventually cover this
if (false && propagate(x, core, a_l_b, conclusion)) {
verbose_stream() << "TODO: bound not covered by new impl\n";
std::abort();
return true; return true;
}
} }
// verbose_stream() << "TODO bound 1 " << a_l_b << " " << x_ge_bound << " " << b << " " << b_val << " " << y << "\n"; // verbose_stream() << "TODO bound 1 " << a_l_b << " " << x_ge_bound << " " << b << " " << b_val << " " << y << "\n";
} }