From 74ecdf31912de82240c5d198bb5c13087156d6ff Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Thu, 6 Jun 2019 12:07:57 -0700 Subject: [PATCH] guery intervals Signed-off-by: Lev Nachmanson --- src/math/lp/nla_intervals.cpp | 57 ++++++++++++++++++++++++++++++++--- src/math/lp/nla_intervals.h | 45 +++++++++++++++------------ 2 files changed, 77 insertions(+), 25 deletions(-) diff --git a/src/math/lp/nla_intervals.cpp b/src/math/lp/nla_intervals.cpp index 721b10c9e..45f65fe66 100755 --- a/src/math/lp/nla_intervals.cpp +++ b/src/math/lp/nla_intervals.cpp @@ -69,7 +69,7 @@ bool intervals::check(monomial const& m) { return true; } -void intervals::set_interval(lpvar v, interval& b) { +void intervals::set_interval(lpvar v, interval& b) const { lp::constraint_index ci; rational val; bool is_strict; @@ -96,8 +96,38 @@ void intervals::set_interval(lpvar v, interval& b) { b.m_upper_dep = nullptr; } } + +rational sign(const rational& v) { return v.is_zero()? v : (rational(v.is_pos()? 1 : -1)); } + +void intervals::set_interval_signs(lpvar v, interval& b) const { + lp::constraint_index ci; + rational val; + bool is_strict; + if (ls().has_lower_bound(v, ci, val, is_strict)) { + m_config.set_lower(b, sign(val)); + m_config.set_lower_is_open(b, is_strict); + m_config.set_lower_is_inf(b, false); + b.m_lower_dep = mk_dep(ci); + } + else { + m_config.set_lower_is_open(b, true); + m_config.set_lower_is_inf(b, true); + b.m_lower_dep = nullptr; + } + if (ls().has_upper_bound(v, ci, val, is_strict)) { + m_config.set_upper(b, sign(val)); + m_config.set_upper_is_open(b, is_strict); + m_config.set_upper_is_inf(b, false); + b.m_upper_dep = mk_dep(ci); + } + else { + m_config.set_upper_is_open(b, true); + m_config.set_upper_is_inf(b, true); + b.m_upper_dep = nullptr; + } +} -intervals::ci_dependency *intervals::mk_dep(lp::constraint_index ci) { +intervals::ci_dependency *intervals::mk_dep(lp::constraint_index ci) const { return m_dep_manager.mk_leaf(ci); } @@ -116,14 +146,30 @@ lp::impq intervals::get_lower_bound_of_monomial(lpvar j) const { throw; } -bool intervals::product_has_upper_bound(int sign, const svector&) const { +bool intervals::product_has_upper_bound(int sign, const svector& vars) const { interval a; - SASSERT(false); + m_imanager.set(a, rational(sign).to_mpq()); + + for (lpvar j : vars) { + interval b, c; + set_interval_signs(j, b); + m_imanager.mul(a, b, c); + if (m_imanager.is_zero(c)) { + TRACE("nla_intervals", tout << "sign = " << sign << "\nproduct = "; + m_core->print_product_with_vars(vars, tout) << "collapsed to zero\n";); + return true; + } + m_imanager.set(a, c); + } + TRACE("nla_intervals", tout << "sign = " << sign << "\nproduct = "; + m_core->print_product_with_vars(vars, tout) << "has lower bound = " << + !m_imanager.upper_is_inf(a) << "\n";); + return !m_imanager.upper_is_inf(a); } bool intervals::monomial_has_lower_bound(lpvar j) const { const monomial& m = m_core->emons()[j]; - return product_has_upper_bound(1, m.vars()); + return product_has_upper_bound(-1, m.vars()); } bool intervals::monomial_has_upper_bound(lpvar j) const { @@ -131,5 +177,6 @@ bool intervals::monomial_has_upper_bound(lpvar j) const { return product_has_upper_bound(-1, m.vars()); } lp::lar_solver& intervals::ls() { return m_core->m_lar_solver; } +const lp::lar_solver& intervals::ls() const { return m_core->m_lar_solver; } } template class interval_manager; diff --git a/src/math/lp/nla_intervals.h b/src/math/lp/nla_intervals.h index c23621955..e40ca19e1 100755 --- a/src/math/lp/nla_intervals.h +++ b/src/math/lp/nla_intervals.h @@ -56,7 +56,6 @@ namespace nla { public: typedef unsynch_mpq_manager numeral_manager; - typedef mpq numeral; // Every configuration object must provide an interval type. // The actual fields are irrelevant, the interval manager @@ -68,8 +67,8 @@ namespace nla { m_lower_open(1), m_upper_open(1), m_lower_inf(1), m_upper_inf(1), m_lower_dep(nullptr), m_upper_dep(nullptr) {} - numeral m_lower; - numeral m_upper; + mpq m_lower; + mpq m_upper; unsigned m_lower_open:1; unsigned m_upper_open:1; unsigned m_lower_inf:1; @@ -86,31 +85,34 @@ namespace nla { i.m_upper_dep = hi; } - // Should be NOOPs for precise numeral types. + // Should be NOOPs for precise mpq types. // For imprecise types (e.g., floats) it should set the rounding mode. void round_to_minus_inf() {} void round_to_plus_inf() {} void set_rounding(bool to_plus_inf) {} // Getters - numeral const & lower(interval const & a) const { return a.m_lower; } - numeral const & upper(interval const & a) const { return a.m_upper; } - numeral & lower(interval & a) { return a.m_lower; } - numeral & upper(interval & a) { return a.m_upper; } + mpq const & lower(interval const & a) const { return a.m_lower; } + mpq const & upper(interval const & a) const { return a.m_upper; } + mpq & lower(interval & a) { return a.m_lower; } + mpq & upper(interval & a) { return a.m_upper; } bool lower_is_open(interval const & a) const { return a.m_lower_open; } bool upper_is_open(interval const & a) const { return a.m_upper_open; } bool lower_is_inf(interval const & a) const { return a.m_lower_inf; } bool upper_is_inf(interval const & a) const { return a.m_upper_inf; } + bool is_zero(interval const & a) const { + return unsynch_mpq_manager::is_zero(a.m_lower) + && unsynch_mpq_manager::is_zero(a.m_upper); } // Setters - void set_lower(interval & a, numeral const & n) { m_manager.set(a.m_lower, n); } - void set_upper(interval & a, numeral const & n) { m_manager.set(a.m_upper, n); } - void set_lower(interval & a, rational const & n) { set_lower(a, n.to_mpq()); } - void set_upper(interval & a, rational const & n) { set_upper(a, n.to_mpq()); } - void set_lower_is_open(interval & a, bool v) { a.m_lower_open = v; } - void set_upper_is_open(interval & a, bool v) { a.m_upper_open = v; } - void set_lower_is_inf(interval & a, bool v) { a.m_lower_inf = v; } - void set_upper_is_inf(interval & a, bool v) { a.m_upper_inf = v; } + void set_lower(interval & a, mpq const & n) const { m_manager.set(a.m_lower, n); } + void set_upper(interval & a, mpq const & n) const { m_manager.set(a.m_upper, n); } + void set_lower(interval & a, rational const & n) const { set_lower(a, n.to_mpq()); } + void set_upper(interval & a, rational const & n) const { set_upper(a, n.to_mpq()); } + void set_lower_is_open(interval & a, bool v) const { a.m_lower_open = v; } + 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; } // Reference to numeral manager numeral_manager & m() const { return m_manager; } @@ -138,21 +140,24 @@ namespace nla { small_object_allocator m_alloc; ci_value_manager m_val_manager; unsynch_mpq_manager m_num_manager; - ci_dependency_manager m_dep_manager; + mutable ci_dependency_manager m_dep_manager; im_config m_config; - interval_manager m_imanager; + mutable interval_manager m_imanager; region m_region; typedef interval_manager::interval interval; bool check(monomial const& m); - void set_interval(lpvar v, interval & b); + void set_interval(lpvar v, interval & b) const; - ci_dependency* mk_dep(lp::constraint_index ci); + void set_interval_signs(lpvar v, interval & b) const; + + ci_dependency* mk_dep(lp::constraint_index ci) const; bool check(lp::lar_term const& t); lp::lar_solver& ls(); + const lp::lar_solver& ls() const; public: intervals(core* c, reslimit& lim) : m_core(c),