From 78a4717c06d0eb6ce4466fc3135da5166130f80a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 18 May 2020 12:41:42 -0700 Subject: [PATCH] fix #4359 and regression to #3270 --- src/math/interval/dep_intervals.cpp | 12 ++++++++---- src/math/interval/dep_intervals.h | 25 ++++++++++++++----------- src/math/lp/monomial_bounds.cpp | 27 ++++++++++++++------------- src/math/lp/monomial_bounds.h | 2 +- 4 files changed, 37 insertions(+), 29 deletions(-) diff --git a/src/math/interval/dep_intervals.cpp b/src/math/interval/dep_intervals.cpp index 56f3e1a0c..7d543b0fb 100644 --- a/src/math/interval/dep_intervals.cpp +++ b/src/math/interval/dep_intervals.cpp @@ -101,12 +101,16 @@ std::ostream& dep_intervals::display(std::ostream& out, const interval& i) const out << rational(m_imanager.upper(i)) << (m_imanager.upper_is_open(i)? ")":"]"); } if (i.m_lower_dep) { - // out << "\nlower deps\n"; - // TBD: print_dependencies(i.m_lower_dep, out); + vector ex; + linearize(i.m_lower_dep, ex); + out << " ld"; + for (unsigned d : ex) out << " " << d; } if (i.m_upper_dep) { - // out << "\nupper deps\n"; - // TBD: print_dependencies(i.m_upper_dep, out); + vector ex; + linearize(i.m_upper_dep, ex); + out << " ud"; + for (unsigned d : ex) out << " " << d; } return out; } diff --git a/src/math/interval/dep_intervals.h b/src/math/interval/dep_intervals.h index e316c8095..edc2da146 100644 --- a/src/math/interval/dep_intervals.h +++ b/src/math/interval/dep_intervals.h @@ -55,13 +55,17 @@ private: }; void add_deps(interval const& a, interval const& b, interval_deps_combine_rule const& deps, interval& i) const { - i.m_lower_dep = lower_is_inf(i) ? nullptr : mk_dependency(a, b, deps.m_lower_combine); - i.m_upper_dep = upper_is_inf(i) ? nullptr : mk_dependency(a, b, deps.m_upper_combine); + auto lower_dep = lower_is_inf(i) ? nullptr : mk_dependency(a, b, deps.m_lower_combine); + auto upper_dep = upper_is_inf(i) ? nullptr : mk_dependency(a, b, deps.m_upper_combine); + i.m_lower_dep = lower_dep; + i.m_upper_dep = upper_dep; } void add_deps(interval const& a, interval_deps_combine_rule const& deps, interval& i) const { - i.m_lower_dep = lower_is_inf(i) ? nullptr : mk_dependency(a, deps.m_lower_combine); - i.m_upper_dep = upper_is_inf(i) ? nullptr : mk_dependency(a, deps.m_upper_combine); + auto lower_dep = lower_is_inf(i) ? nullptr : mk_dependency(a, deps.m_lower_combine); + auto upper_dep = upper_is_inf(i) ? nullptr : mk_dependency(a, deps.m_upper_combine); + i.m_lower_dep = lower_dep; + i.m_upper_dep = upper_dep; } @@ -221,14 +225,13 @@ public: if (r.is_zero()) return; m_imanager.mul(r.to_mpq(), a, b); if (wd == with_deps) { - if (r.is_pos()) { - b.m_lower_dep = a.m_lower_dep; - b.m_upper_dep = a.m_upper_dep; - } - else { - b.m_upper_dep = a.m_lower_dep; - b.m_lower_dep = a.m_upper_dep; + auto lower_dep = a.m_lower_dep; + auto upper_dep = a.m_upper_dep; + if (!r.is_pos()) { + std::swap(lower_dep, upper_dep); } + b.m_lower_dep = lower_dep; + b.m_upper_dep = upper_dep; } } diff --git a/src/math/lp/monomial_bounds.cpp b/src/math/lp/monomial_bounds.cpp index 2e219f5bd..89f4b04cf 100644 --- a/src/math/lp/monomial_bounds.cpp +++ b/src/math/lp/monomial_bounds.cpp @@ -17,13 +17,11 @@ namespace nla { common(c), dep(c->m_intervals.get_dep_intervals()) {} - bool monomial_bounds::operator()() { - bool propagated = false; + void monomial_bounds::operator()() { for (lpvar v : c().m_to_refine) { monic const& m = c().emons()[v]; - propagated |= propagate(m); + propagate(m); } - return propagated; } /** @@ -88,10 +86,10 @@ namespace nla { bool monomial_bounds::propagate_value(dep_interval& range, lpvar v, unsigned p) { SASSERT(p > 0); - if (p == 1) + if (p == 1) return propagate_value(range, v); - auto val = c().val(v); - val = power(val, p); + auto val_v = c().val(v); + auto val = power(val_v, p); rational r; if (dep.is_below(range, val)) { lp::explanation ex; @@ -101,21 +99,24 @@ namespace nla { lemma &= ex; return true; } - if (rational(dep.upper(range)).root(p, r)) { - { + else 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 + if ((p % 2 == 1) || val_v.is_pos()) { auto le = dep.upper_is_open(range) ? llc::LT : llc::LE; - new_lemma lemma(c(), "propagate value - root case - lower bound of range is below value"); + 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) { + if (p % 2 == 0 && val_v.is_neg()) { SASSERT(!r.is_neg()); auto ge = dep.upper_is_open(range) ? llc::GT : llc::GE; - new_lemma lemma(c(), "propagate value - root case - lower bound of range is below value"); + 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; } - return true; } // TBD: add bounds as long as difference to val is above some epsilon. } diff --git a/src/math/lp/monomial_bounds.h b/src/math/lp/monomial_bounds.h index e231e282c..e170cf507 100644 --- a/src/math/lp/monomial_bounds.h +++ b/src/math/lp/monomial_bounds.h @@ -28,6 +28,6 @@ namespace nla { bool is_zero(lpvar v) const; public: monomial_bounds(core* core); - bool operator()(); + void operator()(); }; }