From a068ee9748ceb9b245a7f2f4e36a015d53ff9c4a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 18 Dec 2019 20:33:48 -0800 Subject: [PATCH] extract generic content from nla_intervals Signed-off-by: Nikolaj Bjorner --- src/math/interval/CMakeLists.txt | 1 + src/math/interval/dep_intervals.cpp | 266 ++++++++++++++++++++++++++++ src/math/interval/dep_intervals.h | 227 ++++++++++++++++++++++++ 3 files changed, 494 insertions(+) create mode 100644 src/math/interval/dep_intervals.cpp create mode 100644 src/math/interval/dep_intervals.h diff --git a/src/math/interval/CMakeLists.txt b/src/math/interval/CMakeLists.txt index 390529b9d..f79370891 100644 --- a/src/math/interval/CMakeLists.txt +++ b/src/math/interval/CMakeLists.txt @@ -1,6 +1,7 @@ z3_add_component(interval SOURCES interval_mpq.cpp + dep_intervals.cpp COMPONENT_DEPENDENCIES util ) diff --git a/src/math/interval/dep_intervals.cpp b/src/math/interval/dep_intervals.cpp new file mode 100644 index 000000000..fd4379954 --- /dev/null +++ b/src/math/interval/dep_intervals.cpp @@ -0,0 +1,266 @@ +/*++ + Copyright (c) 2017 Microsoft Corporation + + Module Name: + + dep_intervals.cpp + + Abstract: + + intervals with depedency tracking. + + Author: + Nikolaj Bjorner (nbjorner) + Lev Nachmanson (levnach) + + Revision History: + + extracted from nla_intervals.cpp + + --*/ + +#include "math/interval/interval_def.h" +#include "math/interval/dep_intervals.h" +#include "util/mpq.h" + + +typedef enum dep_intervals::with_deps_t e_with_deps; + +void dep_intervals::set_interval_for_scalar(interval& a, const rational& v) { + set_lower(a, v); + set_upper(a, v); + set_lower_is_open(a, false); + set_lower_is_inf(a, false); + set_upper_is_open(a, false); + set_upper_is_inf(a, false); +} + +template +void dep_intervals::copy_upper_bound(const interval& a, interval& i) const { + SASSERT(a.m_upper_inf == false); + i.m_upper_inf = false; + m_config.set_upper(i, a.m_upper); + i.m_upper_open = a.m_upper_open; + if (wd == with_deps) { + i.m_upper_dep = a.m_upper_dep; + } +} + +template +void dep_intervals::copy_lower_bound(const interval& a, interval& i) const { + SASSERT(a.m_lower_inf == false); + i.m_lower_inf = false; + m_config.set_lower(i, a.m_lower); + i.m_lower_open = a.m_lower_open; + if (wd == with_deps) { + i.m_lower_dep = a.m_lower_dep; + } +} + + + +void dep_intervals::set_zero_interval(interval& i, u_dependency* dep) const { + auto val = rational(0); + m_config.set_lower(i, val); + m_config.set_lower_is_open(i, false); + m_config.set_lower_is_inf(i, false); + m_config.set_upper(i, val); + m_config.set_upper_is_open(i, false); + m_config.set_upper_is_inf(i, false); + i.m_lower_dep = i.m_upper_dep = dep; +} + +void dep_intervals::set_zero_interval_deps_for_mult(interval& a) { + a.m_lower_dep = mk_join(a.m_lower_dep, a.m_upper_dep); + a.m_upper_dep = a.m_lower_dep; +} + +template +void dep_intervals::mul(const rational& r, const interval& a, interval& b) const { + 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; + } + } +} + +template +dep_intervals::interval dep_intervals::intersect(const interval& a, const interval& b) const { + interval i; + update_lower_for_intersection(a, b, i); + update_upper_for_intersection(a, b, i); + return i; +} + +template +void dep_intervals::update_lower_for_intersection(const interval& a, const interval& b, interval& i) const { + if (a.m_lower_inf) { + if (b.m_lower_inf) + return; + copy_lower_bound(b, i); + return; + } + if (b.m_lower_inf) { + SASSERT(!a.m_lower_inf); + copy_lower_bound(a, i); + return; + } + if (m_num_manager.lt(a.m_lower, b.m_lower)) { + copy_lower_bound(b, i); + return; + } + if (m_num_manager.gt(a.m_lower, b.m_lower)) { + copy_lower_bound(a, i); + return; + } + SASSERT(m_num_manager.eq(a.m_lower, b.m_lower)); + if (a.m_lower_open) { // we might consider to look at b.m_lower_open too here + copy_lower_bound(a, i); + return; + } + copy_lower_bound(b, i); +} + +template +void dep_intervals::update_upper_for_intersection(const interval& a, const interval& b, interval& i) const { + if (a.m_upper_inf) { + if (b.m_upper_inf) + return; + copy_upper_bound(b, i); + return; + } + if (b.m_upper_inf) { + SASSERT(!a.m_upper_inf); + copy_upper_bound(a, i); + return; + } + if (m_num_manager.gt(a.m_upper, b.m_upper)) { + copy_upper_bound(b, i); + return; + } + if (m_num_manager.lt(a.m_upper, b.m_upper)) { + copy_upper_bound(a, i); + return; + } + SASSERT(m_num_manager.eq(a.m_upper, b.m_upper)); + if (a.m_upper_open) { // we might consider to look at b.m_upper_open too here + copy_upper_bound(a, i); + return; + } + + copy_upper_bound(b, i); +} + + +void dep_intervals::add(const rational& r, interval& a) const { + if (!a.m_lower_inf) { + m_config.set_lower(a, a.m_lower + r); + } + if (!a.m_upper_inf) { + m_config.set_upper(a, a.m_upper + r); + } +} + +template +dep_intervals::interval dep_intervals::power(const interval& a, unsigned n) { + interval b; + if (with_deps == wd) { + interval_deps_combine_rule combine_rule; + m_imanager.power(a, n, b, combine_rule); + combine_deps(a, combine_rule, b); + } + else { + m_imanager.power(a, n, b); + } + TRACE("dep_intervals", tout << "power of "; display(tout, a) << " = "; + display(tout, b) << "\n"; ); + return b; +} + + +bool dep_intervals::separated_from_zero_on_lower(const interval& i) const { + if (lower_is_inf(i)) + return false; + if (unsynch_mpq_manager::is_neg(lower(i))) + return false; + if (unsynch_mpq_manager::is_zero(lower(i)) && !m_config.lower_is_open(i)) + return false; + return true; +} + +bool dep_intervals::separated_from_zero_on_upper(const interval& i) const { + if (upper_is_inf(i)) + return false; + if (unsynch_mpq_manager::is_pos(upper(i))) + return false; + if (unsynch_mpq_manager::is_zero(upper(i)) && !m_config.upper_is_open(i)) + return false; + return true; +} + +bool dep_intervals::check_interval_for_conflict_on_zero(const interval & i, u_dependency*& dep) { + return check_interval_for_conflict_on_zero_lower(i, dep) || check_interval_for_conflict_on_zero_upper(i, dep); +} + +bool dep_intervals::check_interval_for_conflict_on_zero_upper(const interval & i, u_dependency*& dep) { + if (!separated_from_zero_on_upper(i)) + return false; + TRACE("dep_intervals", display(tout, i);); + dep = m_dep_manager.mk_join(dep, i.m_upper_dep); + return true; +} + +bool dep_intervals::check_interval_for_conflict_on_zero_lower(const interval & i, u_dependency*& dep) { + if (!separated_from_zero_on_lower(i)) { + return false; + } + TRACE("dep_intervals", display(tout, i);); + dep = m_dep_manager.mk_join(dep, i.m_lower_dep); + return true; +} + + +std::ostream& dep_intervals::display(std::ostream& out, const interval& i) const { + if (m_imanager.lower_is_inf(i)) { + out << "(-oo"; + } else { + out << (m_imanager.lower_is_open(i)? "(":"[") << rational(m_imanager.lower(i)); + } + out << ","; + if (m_imanager.upper_is_inf(i)) { + out << "oo)"; + } else { + 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); + } + if (i.m_upper_dep) { + out << "\nupper deps\n"; + // TBD: print_dependencies(i.m_upper_dep, out); + } + return out; +} + + +bool dep_intervals::is_empty(interval const& a) const { + if (a.m_lower_inf || a.m_upper_inf) + return false; + if (m_num_manager.gt(a.m_lower, a.m_upper)) + return true; + if (m_num_manager.lt(a.m_lower, a.m_upper)) + return false; + if (a.m_lower_open || a.m_upper_open) + return true; + return false; +} + +template class interval_manager; diff --git a/src/math/interval/dep_intervals.h b/src/math/interval/dep_intervals.h new file mode 100644 index 000000000..c764f6cb1 --- /dev/null +++ b/src/math/interval/dep_intervals.h @@ -0,0 +1,227 @@ +/*++ + Copyright (c) 2017 Microsoft Corporation + + Module Name: + + dep_intervals.h + + Abstract: + + intervals with depedency tracking. + + Author: + Nikolaj Bjorner (nbjorner) + Lev Nachmanson (levnach) + + Revision History: + + extracted from nla_intervals.h + + --*/ + +#pragma once +#include "util/dependency.h" +#include "util/region.h" +#include "util/rational.h" +#include "util/rlimit.h" +#include "math/interval/interval.h" + +class dep_intervals { +public: + enum with_deps_t { with_deps, without_deps }; + +private: + class im_config { + unsynch_mpq_manager& m_manager; + u_dependency_manager& m_dep_manager; + + public: + typedef unsynch_mpq_manager numeral_manager; + typedef bound_deps deps_combine_rule; + + struct interval { + interval() : + m_lower(), m_upper(), + m_lower_open(1), m_upper_open(1), + m_lower_inf(1), m_upper_inf(1), + m_lower_dep(nullptr), m_upper_dep(nullptr) {} + mpq m_lower; + mpq m_upper; + unsigned m_lower_open : 1; + unsigned m_upper_open : 1; + unsigned m_lower_inf : 1; + unsigned m_upper_inf : 1; + u_dependency* m_lower_dep; // justification for the lower bound + u_dependency* m_upper_dep; // justification for the upper bound + }; + + void add_deps(interval const& a, interval const& b, interval_deps const& deps, interval& i) const { + i.m_lower_dep = lower_is_inf(i) ? nullptr : mk_dependency(a, b, deps.m_lower_deps); + i.m_upper_dep = upper_is_inf(i) ? nullptr : mk_dependency(a, b, deps.m_upper_deps); + } + + void add_deps(interval const& a, interval_deps const& deps, interval& i) const { + i.m_lower_dep = lower_is_inf(i) ? nullptr : mk_dependency(a, deps.m_lower_deps); + i.m_upper_dep = upper_is_inf(i) ? nullptr : mk_dependency(a, deps.m_upper_deps); + } + + + // 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 + 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_inf(interval const& a) const { return upper_is_inf(a) && lower_is_inf(a); } + bool is_zero(interval const& a) const { + return (!lower_is_inf(a)) && (!upper_is_inf(a)) && + (!lower_is_open(a)) && (!upper_is_open(a)) && + unsynch_mpq_manager::is_zero(a.m_lower) && + unsynch_mpq_manager::is_zero(a.m_upper); + } + + // Setters + 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; } + + im_config(numeral_manager& m, u_dependency_manager& d) :m_manager(m), m_dep_manager(d) {} + private: + u_dependency* mk_dependency(interval const& a, interval const& b, deps_combine_rule bd) const { + u_dependency* dep = nullptr; + if (dep_in_lower1(bd)) { + dep = m_dep_manager.mk_join(dep, a.m_lower_dep); + } + if (dep_in_lower2(bd)) { + dep = m_dep_manager.mk_join(dep, b.m_lower_dep); + } + if (dep_in_upper1(bd)) { + dep = m_dep_manager.mk_join(dep, a.m_upper_dep); + } + if (dep_in_upper2(bd)) { + dep = m_dep_manager.mk_join(dep, b.m_upper_dep); + } + return dep; + } + + u_dependency* mk_dependency(interval const& a, deps_combine_rule bd) const { + u_dependency* dep = nullptr; + if (dep_in_lower1(bd)) { + dep = m_dep_manager.mk_join(dep, a.m_lower_dep); + } + if (dep_in_upper1(bd)) { + dep = m_dep_manager.mk_join(dep, a.m_upper_dep); + } + return dep; + } + }; + + mutable unsynch_mpq_manager m_num_manager; + mutable u_dependency_manager m_dep_manager; + im_config m_config; + mutable interval_manager m_imanager; + + typedef interval_manager::interval interval; + + u_dependency* mk_leaf(unsigned d) { return m_dep_manager.mk_leaf(d); } + u_dependency* mk_join(u_dependency* a, u_dependency* b) { return m_dep_manager.mk_join(a, b); } + + template + void update_lower_for_intersection(const interval& a, const interval& b, interval& i) const; + + template + void update_upper_for_intersection(const interval& a, const interval& b, interval& i) const; + + void mul(const interval& a, const interval& b, interval& c, interval_deps& deps) { m_imanager.mul(a, b, c, deps); } + void add(const interval& a, const interval& b, interval& c, interval_deps& deps) { m_imanager.add(a, b, c, deps); } + + void combine_deps(interval const& a, interval const& b, interval_deps const& deps, interval& i) const { + SASSERT(&a != &i && &b != &i); + m_config.add_deps(a, b, deps, i); + } + + void combine_deps(interval const& a, interval_deps const& deps, interval& i) const { + SASSERT(&a != &i); + m_config.add_deps(a, deps, i); + } + +public: + u_dependency_manager& dep_manager() { return m_dep_manager; } + + dep_intervals(reslimit& lim) : + m_config(m_num_manager, m_dep_manager), + m_imanager(lim, im_config(m_num_manager, m_dep_manager)) + {} + + std::ostream& display(std::ostream& out, const interval& i) const; + void set_lower(interval& a, rational const& n) const { m_config.set_lower(a, n.to_mpq()); } + void set_upper(interval& a, rational const& n) const { m_config.set_upper(a, n.to_mpq()); } + void set_lower_is_open(interval& a, bool strict) { m_config.set_lower_is_open(a, strict); } + 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); } + 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); } + + template + void mul(const rational& r, const interval& a, interval& b) 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); } + + template + void set(interval& a, const interval& b) const { + m_imanager.set(a, b); + if (wd == with_deps) { + a.m_lower_dep = b.m_lower_dep; + a.m_upper_dep = b.m_upper_dep; + } + } + + template + interval power(const interval& a, unsigned n); + + template + void copy_upper_bound(const interval& a, interval& i) const; + + template + void copy_lower_bound(const interval& a, interval& i) const; + + template + interval intersect(const interval& a, const interval& b) const; + + void set_zero_interval_deps_for_mult(interval&); + void set_zero_interval(interval&, u_dependency* dep = nullptr) const; + bool is_inf(const interval& i) const { return m_config.is_inf(i); } + bool separated_from_zero_on_lower(const interval&) const; + bool separated_from_zero_on_upper(const interval&) const; + inline bool separated_from_zero(const interval& i) const { + return separated_from_zero_on_upper(i) || separated_from_zero_on_lower(i); + } + bool check_interval_for_conflict_on_zero(const interval& i, u_dependency*&); + bool check_interval_for_conflict_on_zero_lower(const interval& i, u_dependency*&); + bool check_interval_for_conflict_on_zero_upper(const interval& i, u_dependency*&); + mpq const& lower(interval const& a) const { return m_config.lower(a); } + mpq const& upper(interval const& a) const { return m_config.upper(a); } + bool is_empty(interval const& a) const; + void set_interval_for_scalar(interval&, const rational&); +};