mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

resurrect old bounds propagation

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-10-14 13:55:56 -07:00
parent a39d4adf5b
commit 5619ed0586
1 changed files with 20 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

30
src/math/lp/monomial_bounds.cpp
View file

@ -161,18 +161,28 @@ namespace nla {
return true;
}
if (rational(dep.upper(range)).root(p, r) && (p % 2 == 1 || c().has_upper_bound(v))) {
SASSERT(p % 2 == 1 || c().get_upper_bound(v) >= 0);
if (rational(dep.upper(range)).root(p, r)) {
// v = -2, [-4,-3]^3 < v^3 -> add bound v <= -3
// v = -2, [-1,+1]^2 < v^2 -> add bound v >= -1
++c().lra.settings().stats().m_nla_propagate_bounds;
auto le = dep.upper_is_open(range) ? llc::LT : llc::LE;
new_lemma lemma(c(), "propagate value - root case - upper bound of range is below value");
lemma &= ex;
if (p % 2 == 0)
lemma.explain_existing_upper_bound(v);
lemma |= ineq(v, le, r);
return true;
if ((p % 2 == 1) || c().val(v).is_pos()) {
++c().lra.settings().stats().m_nla_propagate_bounds;
auto le = dep.upper_is_open(range) ? llc::LT : llc::LE;
new_lemma lemma(c(), "propagate value - root case - upper bound of range is below value");
lemma &= ex;
lemma |= ineq(v, le, r);
return true;
}
if (p % 2 == 0 && c().val(v).is_neg()) {
++c().lra.settings().stats().m_nla_propagate_bounds;
SASSERT(!r.is_neg());
auto ge = dep.upper_is_open(range) ? llc::GT : llc::GE;
new_lemma lemma(c(), "propagate value - root case - upper bound of range is below negative value");
lemma &= ex;
lemma |= ineq(v, ge, -r);
return true;
}
}
}