From bda29ca26a05b71d41d3be2de465c7fef4125716 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 13 May 2020 10:37:46 -0700 Subject: [PATCH] outline for monomial bound propagation Signed-off-by: Nikolaj Bjorner --- src/math/interval/dep_intervals.cpp | 21 ++++++++ src/math/interval/dep_intervals.h | 10 ++++ src/math/lp/CMakeLists.txt | 1 + src/math/lp/monomial_bounds.cpp | 82 +++++++++++++++++++++++++++++ src/math/lp/monomial_bounds.h | 27 ++++++++++ src/math/lp/nla_core.h | 7 +++ 6 files changed, 148 insertions(+) create mode 100644 src/math/lp/monomial_bounds.cpp create mode 100644 src/math/lp/monomial_bounds.h diff --git a/src/math/interval/dep_intervals.cpp b/src/math/interval/dep_intervals.cpp index adb93beef..860647883 100644 --- a/src/math/interval/dep_intervals.cpp +++ b/src/math/interval/dep_intervals.cpp @@ -122,4 +122,25 @@ bool dep_intervals::is_empty(interval const& a) const { return false; } +bool dep_intervals::is_above(const interval& i, const rational& r) const { + if (lower_is_inf(i)) + return false; + if (m_num_manager.lt(lower(i), r.to_mpq())) + return false; + if (m_num_manager.eq(lower(i), r.to_mpq()) && !m_config.lower_is_open(i)) + return false; + return true; +} + +bool dep_intervals::is_below(const interval& i, const rational& r) const { + if (upper_is_inf(i)) + return false; + if (m_num_manager.lt(upper(i), r.to_mpq())) + return false; + if (m_num_manager.eq(upper(i), r.to_mpq()) && !m_config.upper_is_open(i)) + return false; + return true; +} + + template class interval_manager; diff --git a/src/math/interval/dep_intervals.h b/src/math/interval/dep_intervals.h index fa294c9ba..f2fca6131 100644 --- a/src/math/interval/dep_intervals.h +++ b/src/math/interval/dep_intervals.h @@ -97,6 +97,8 @@ private: void set_upper_is_open(interval& a, bool v) const { a.m_upper_open = v; } void set_lower_is_inf(interval& a, bool v) const { a.m_lower_inf = v; } void set_upper_is_inf(interval& a, bool v) const { a.m_upper_inf = v; } + void set_lower_dep(interval& a, u_dependency* d) const { a.m_lower_dep = d; } + void set_upper_dep(interval& a, u_dependency* d) const { a.m_upper_dep = d; } // Reference to numeral manager numeral_manager& m() const { return m_manager; } @@ -190,11 +192,19 @@ public: void set_lower_is_inf(interval& a, bool inf) { m_config.set_lower_is_inf(a, inf); } void set_upper_is_open(interval& a, bool strict) { m_config.set_upper_is_open(a, strict); } void set_upper_is_inf(interval& a, bool inf) { m_config.set_upper_is_inf(a, inf); } + void set_lower_dep(interval& a, u_dependency* d) const { m_config.set_lower_dep(a, d); } + void set_upper_dep(interval& a, u_dependency* d) const { m_config.set_upper_dep(a, d); } bool is_zero(const interval& a) const { return m_config.is_zero(a); } bool upper_is_inf(const interval& a) const { return m_config.upper_is_inf(a); } bool lower_is_inf(const interval& a) const { return m_config.lower_is_inf(a); } bool lower_is_open(const interval& a) const { return m_config.lower_is_open(a); } bool upper_is_open(const interval& a) const { return m_config.upper_is_open(a); } + template + void get_upper_dep(const interval& a, T& expl) { linearize(a.m_upper_dep, expl); } + template + void get_lower_dep(const interval& a, T& expl) { linearize(a.m_lower_dep, expl); } + bool is_above(const interval& a, const rational& r) const; + bool is_below(const interval& a, const rational& r) const; void add(const rational& r, interval& a) const; void mul(const interval& a, const interval& b, interval& c) { m_imanager.mul(a, b, c); } void add(const interval& a, const interval& b, interval& c) { m_imanager.add(a, b, c); } diff --git a/src/math/lp/CMakeLists.txt b/src/math/lp/CMakeLists.txt index f27815e34..34892c7e0 100644 --- a/src/math/lp/CMakeLists.txt +++ b/src/math/lp/CMakeLists.txt @@ -30,6 +30,7 @@ z3_add_component(lp lp_utils.cpp matrix.cpp mon_eq.cpp + monomial_bounds.cpp nex_creator.cpp nla_basics_lemmas.cpp nla_common.cpp diff --git a/src/math/lp/monomial_bounds.cpp b/src/math/lp/monomial_bounds.cpp new file mode 100644 index 000000000..71c0595a0 --- /dev/null +++ b/src/math/lp/monomial_bounds.cpp @@ -0,0 +1,82 @@ +/*++ + Copyright (c) 2020 Microsoft Corporation + + Author: + Nikolaj Bjorner (nbjorner) + Lev Nachmanson (levnach) + + --*/ +#pragma once + +#include "math/lp/monomial_bounds.h" +#include "math/lp/nla_core.h" +#include "math/lp/nla_intervals.h" + +namespace nla { + + monomial_bounds::monomial_bounds(core* c):common(c) {} + + bool monomial_bounds::operator()() { + bool propagated = false; + for (lpvar v : c().m_to_refine) { + monic const& m = c().emons()[v]; + if (propagate_up(m)) + propagated = true; + } + return propagated; + } + + bool monomial_bounds::propagate_up(monic const& m) { + auto & intervals = c().m_intervals; + auto & dep_intervals = intervals.get_dep_intervals(); + scoped_dep_interval product(dep_intervals), di(dep_intervals); + lpvar v = m.vars()[0]; + var2interval(v, product); + for (unsigned i = 1; i < m.size(); ++i) { + var2interval(m.vars()[i], di); + dep_intervals.mul(product, di, product); + } + if (dep_intervals.is_below(product, c().val(m.var()))) { + lp::explanation ex; + dep_intervals.get_upper_dep(product, ex); + new_lemma lemma(c(), "propagate up - upper bound of product is below value"); + lemma &= ex; + auto const& upper = dep_intervals.upper(product); + auto cmp = dep_intervals.upper_is_open(product) ? llc::LT : llc::LE; + lemma |= ineq(m.var(), cmp, upper); + return true; + } + else if (dep_intervals.is_above(product, c().val(m.var()))) { + lp::explanation ex; + dep_intervals.get_lower_dep(product, ex); + new_lemma lemma(c(), "propagate up - lower bound of product is above value"); + lemma &= ex; + auto const& lower = dep_intervals.upper(product); + auto cmp = dep_intervals.lower_is_open(product) ? llc::GT : llc::GE; + lemma |= ineq(m.var(), cmp, lower); + return true; + } + else { + return false; + } + } + + void monomial_bounds::var2interval(lpvar v, scoped_dep_interval& i) { + auto & intervals = c().m_intervals; + auto & dep_intervals = intervals.get_dep_intervals(); + lp::constraint_index ci; + rational bound; + bool is_strict; + if (c().has_lower_bound(v, ci, bound, is_strict)) { + dep_intervals.set_lower_is_open(i, is_strict); + dep_intervals.set_lower(i, bound); + dep_intervals.set_lower_dep(i, dep_intervals.mk_leaf(ci)); + } + if (c().has_upper_bound(v, ci, bound, is_strict)) { + dep_intervals.set_upper_is_open(i, is_strict); + dep_intervals.set_upper(i, bound); + dep_intervals.set_upper_dep(i, dep_intervals.mk_leaf(ci)); + } + } +} + diff --git a/src/math/lp/monomial_bounds.h b/src/math/lp/monomial_bounds.h new file mode 100644 index 000000000..146514f92 --- /dev/null +++ b/src/math/lp/monomial_bounds.h @@ -0,0 +1,27 @@ +/*++ + Copyright (c) 2020 Microsoft Corporation + + Author: + Nikolaj Bjorner (nbjorner) + Lev Nachmanson (levnach) + + --*/ +#pragma once + +#include "math/lp/nla_common.h" +#include "math/lp/nla_intervals.h" +#include "math/lp/nex.h" +#include "math/lp/cross_nested.h" +#include "math/lp/u_set.h" + +namespace nla { + class core; + + class monomial_bounds : common { + void var2interval(lpvar v, scoped_dep_interval& i); + bool propagate_up(monic const& m); + public: + monomial_bounds(core* core); + bool operator()(); + }; +} diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index 9598f3374..c70f32fe6 100644 --- a/src/math/lp/nla_core.h +++ b/src/math/lp/nla_core.h @@ -321,6 +321,13 @@ public: } const rational& get_upper_bound(unsigned j) const; const rational& get_lower_bound(unsigned j) const; + bool has_lower_bound(lp::var_index var, lp::constraint_index& ci, lp::mpq& value, bool& is_strict) const { + return m_lar_solver.has_lower_bound(var, ci, value, is_strict); + } + bool has_upper_bound(lp::var_index var, lp::constraint_index& ci, lp::mpq& value, bool& is_strict) const { + return m_lar_solver.has_upper_bound(var, ci, value, is_strict); + } + bool zero_is_an_inner_point_of_bounds(lpvar j) const; bool var_is_int(lpvar j) const { return m_lar_solver.column_is_int(j); }