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<dep_intervals::im_config>;
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 <typename T>
+ void get_upper_dep(const interval& a, T& expl) { linearize(a.m_upper_dep, expl); }
+ template <typename T>
+ 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); }