From 999ca2ed7045be21f955e00d17df6ad5106413b0 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Sat, 15 Jun 2019 22:42:59 -0700 Subject: [PATCH] no intervals Signed-off-by: Lev Nachmanson --- src/math/lp/CMakeLists.txt | 1 - src/math/lp/nla_basics_lemmas.cpp | 2 +- src/math/lp/nla_core.cpp | 1 - src/math/lp/nla_core.h | 3 +- src/math/lp/nla_intervals.cpp | 248 ------------------------------ src/math/lp/nla_intervals.h | 181 ---------------------- src/math/lp/nla_solver.cpp | 2 +- src/math/lp/nla_solver.h | 2 +- 8 files changed, 4 insertions(+), 436 deletions(-) delete mode 100755 src/math/lp/nla_intervals.cpp delete mode 100755 src/math/lp/nla_intervals.h diff --git a/src/math/lp/CMakeLists.txt b/src/math/lp/CMakeLists.txt index 77c7422e5..647687b04 100644 --- a/src/math/lp/CMakeLists.txt +++ b/src/math/lp/CMakeLists.txt @@ -28,7 +28,6 @@ z3_add_component(lp nla_basics_lemmas.cpp nla_common.cpp nla_core.cpp - nla_intervals.cpp nla_monotone_lemmas.cpp nla_order_lemmas.cpp nla_solver.cpp diff --git a/src/math/lp/nla_basics_lemmas.cpp b/src/math/lp/nla_basics_lemmas.cpp index d74f7eade..23160c29c 100644 --- a/src/math/lp/nla_basics_lemmas.cpp +++ b/src/math/lp/nla_basics_lemmas.cpp @@ -251,7 +251,7 @@ bool basics::basic_lemma(bool derived) { if (basic_sign_lemma(derived)) return true; if (derived) - return c().m_intervals.get_lemmas(); + return false; // c().m_intervals.get_lemmas(); const auto& mon_inds_to_ref = c().m_to_refine; TRACE("nla_solver", tout << "mon_inds_to_ref = "; print_vector(mon_inds_to_ref, tout);); unsigned start = c().random(); diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index e00599f80..8548d17e4 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -25,7 +25,6 @@ core::core(lp::lar_solver& s, reslimit & lim) : m_evars(), m_lar_solver(s), m_tangents(this), - m_intervals(this, lim), m_basics(this), m_order(this), m_monotone(this), diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index 827141dde..e02a4bd43 100644 --- a/src/math/lp/nla_core.h +++ b/src/math/lp/nla_core.h @@ -27,7 +27,7 @@ #include "math/lp/nla_monotone_lemmas.h" #include "math/lp/emonomials.h" #include "math/lp/nla_settings.h" -#include "math/lp/nla_intervals.h" +// #include "math/lp/nla_intervals.h" namespace nla { template @@ -83,7 +83,6 @@ public: vector * m_lemma_vec; svector m_to_refine; tangents m_tangents; - intervals m_intervals; basics m_basics; order m_order; monotone m_monotone; diff --git a/src/math/lp/nla_intervals.cpp b/src/math/lp/nla_intervals.cpp deleted file mode 100755 index c08b0774f..000000000 --- a/src/math/lp/nla_intervals.cpp +++ /dev/null @@ -1,248 +0,0 @@ -#include "math/lp/nla_core.h" -#include "math/interval/interval_def.h" -#include "math/lp/nla_intervals.h" - -namespace nla { - -bool intervals::get_lemmas() { - m_region.reset(); - bool ret = false; - for (auto const& k : c().m_to_refine) { - if (get_lemma(c().emons()[k])) { - ret = true; - } - if (c().done()) - break; - } - return ret; -} -// create a product of interval signs together with the depencies -intervals::interval intervals::mul_signs_with_deps(const svector& vars) const { - interval a, b, c; - m_imanager.set(a, mpq(1)); - for (lpvar v : vars) { - set_var_interval_signs_with_deps(v, b); - interval_deps deps; - m_imanager.mul(a, b, c, deps); - m_imanager.set(a, c); - m_config.add_deps(a, b, deps, a); - if (m_imanager.is_zero(a)) - return a; - } - return a; -} - -bool intervals::get_lemma(monomial const& m) { - interval b, c, d; - interval a = mul(m.vars()); - lp::impq v(val(m.var())); - if (!m_imanager.lower_is_inf(a)) { - lp::impq lb(rational(a.m_lower)); - if (m_config.lower_is_open(a)) - lb.y = 1; - if (v < lb) { - interval signs_a = mul_signs_with_deps(m.vars()); - add_empty_lemma(); - svector expl; - m_dep_manager.linearize(signs_a.m_lower_dep, expl); - _().current_expl().add_expl(expl); - llc cmp = m_config.lower_is_open(a)? llc::GT: llc::GE; - mk_ineq(m.var(), cmp, lb.x); - TRACE("nla_solver", _().print_lemma(tout); ); - return true; - } - } - - if (!m_imanager.upper_is_inf(a)) { - lp::impq ub(rational(a.m_upper)); - if (m_config.upper_is_open(a)) - ub.y = 1; - if (v > ub) { - interval signs_a = mul_signs_with_deps(m.vars()); - add_empty_lemma(); - svector expl; - m_dep_manager.linearize(signs_a.m_upper_dep, expl); - _().current_expl().add_expl(expl); - llc cmp = m_config.upper_is_open(a)? llc::LT: llc::LE; - mk_ineq(m.var(), cmp, ub.x); - TRACE("nla_solver", _().print_lemma(tout); ); - return true; - } - } - return false; -} -void intervals::set_var_interval(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, val); - m_config.set_lower_is_open(b, is_strict); - m_config.set_lower_is_inf(b, false); - } - else { - m_config.set_lower_is_open(b, true); - m_config.set_lower_is_inf(b, true); - } - if (ls().has_upper_bound(v, ci, val, is_strict)) { - m_config.set_upper(b, val); - m_config.set_upper_is_open(b, is_strict); - m_config.set_upper_is_inf(b, false); - } - else { - m_config.set_upper_is_open(b, true); - m_config.set_upper_is_inf(b, true); - } -} - -rational sign(const rational& v) { return v.is_zero()? v : (rational(v.is_pos()? 1 : -1)); } - -void intervals::set_var_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); - } - else { - m_config.set_lower_is_open(b, true); - m_config.set_lower_is_inf(b, true); - } - 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); - } - else { - m_config.set_upper_is_open(b, true); - m_config.set_upper_is_inf(b, true); - } -} - -void intervals::set_var_interval_signs_with_deps(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) const { - return m_dep_manager.mk_leaf(ci); -} - -lp::impq intervals::get_upper_bound_of_monomial(lpvar j) const { - const monomial& m = m_core->emons()[j]; - interval a = mul(m.vars()); - SASSERT(!m_imanager.upper_is_inf(a)); - auto r = lp::impq(a.m_upper); - if (a.m_upper_open) - r.y = -1; - TRACE("nla_intervals_detail", m_core->print_monomial_with_vars(m, tout) << "upper = " << r << "\n";); - return r; -} -lp::impq intervals::get_lower_bound_of_monomial(lpvar j) const { - const monomial& m = m_core->emons()[j]; - interval a = mul(m.vars()); - SASSERT(!a.m_lower_inf); - auto r = lp::impq(a.m_lower); - if (a.m_lower_open) - r.y = 1; - TRACE("nla_intervals_detail", m_core->print_monomial_with_vars(m, tout) << "lower = " << r << "\n";); - return r; -} - -intervals::interval intervals::mul(const svector& vars) const { - interval a; - m_imanager.set(a, mpq(1)); - - for (lpvar j : vars) { - interval b, c; - set_var_interval(j, b); - if (m_imanager.is_zero(b)) { - return b; - } - m_imanager.mul(a, b, c); - m_imanager.set(a, c); - } - return a; -} - -intervals::interval intervals::mul_signs(const svector& vars) const { - interval a; - m_imanager.set(a, mpq(1)); - - for (lpvar j : vars) { - interval b, c; - set_var_interval_signs(j, b); - if (m_imanager.is_zero(b)) { - return b; - } - m_imanager.mul(a, b, c); - m_imanager.set(a, c); - } - return a; -} - -bool intervals::product_has_upper_bound(int sign, const svector& vars) const { - interval a = mul_signs(vars); - SASSERT(sign == 1 || sign == -1); - return sign == 1 ? !m_imanager.upper_is_inf(a) : !m_imanager.lower_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()); -} - -bool intervals::monomial_has_upper_bound(lpvar j) const { - const monomial& m = m_core->emons()[j]; - 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; } - -std::ostream& intervals::print_explanations(const svector &expl , std::ostream& out) const { - out << "interv expl:\n "; - for (auto ci : expl) - m_core->m_lar_solver.print_constraint_indices_only(ci, out); - return out; -} - -void intervals::get_explanation_of_upper_bound_for_monomial(lpvar j, svector& expl) const { - interval a = mul_signs_with_deps(m_core->emons()[j].vars()); - m_dep_manager.linearize(a.m_upper_dep, expl); - TRACE("nla_intervals", print_explanations(expl, tout);); -} -void intervals::get_explanation_of_lower_bound_for_monomial(lpvar j, svector& expl) const{ - interval a = mul_signs_with_deps(m_core->emons()[j].vars()); - m_dep_manager.linearize(a.m_lower_dep, expl); - TRACE("nla_intervals", print_explanations(expl, tout);); - // return m_intervals.get_explanation_of_lower_bound_for_monomial(j, expl ) -} -} -// instantiate the template -template class interval_manager; diff --git a/src/math/lp/nla_intervals.h b/src/math/lp/nla_intervals.h deleted file mode 100755 index 6c5e64548..000000000 --- a/src/math/lp/nla_intervals.h +++ /dev/null @@ -1,181 +0,0 @@ -/*++ - Copyright (c) 2017 Microsoft Corporation - - Module Name: - - - - Abstract: - - - - Author: - Nikolaj Bjorner (nbjorner) - Lev Nachmanson (levnach) - - Revision History: - - - --*/ -#pragma once -#include "util/dependency.h" -#include "util/small_object_allocator.h" -#include "math/lp/nla_common.h" -#include "math/lp/lar_solver.h" -#include "math/interval/interval.h" - - -namespace nla { -class core; - -class intervals : common { - class ci_value_manager { - public: - void inc_ref(lp::constraint_index const & v) { - } - - void dec_ref(lp::constraint_index const & v) { - } - }; - - struct ci_dependency_config { - typedef ci_value_manager value_manager; - typedef small_object_allocator allocator; - static const bool ref_count = false; - typedef lp::constraint_index value; - }; - - typedef dependency_manager ci_dependency_manager; - - typedef ci_dependency_manager::dependency ci_dependency; - - class im_config { - unsynch_mpq_manager& m_manager; - ci_dependency_manager& m_dep_manager; - - public: - typedef unsynch_mpq_manager numeral_manager; - - // Every configuration object must provide an interval type. - // The actual fields are irrelevant, the interval manager - // accesses interval data using the following API. - - 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; - ci_dependency * m_lower_dep; // justification for the lower bound - ci_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 { - ci_dependency* lo = mk_dependency(a, b, deps.m_lower_deps); - ci_dependency* hi = mk_dependency(a, b, deps.m_upper_deps); - i.m_lower_dep = lo; - i.m_upper_dep = hi; - } - - // 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_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, 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, ci_dependency_manager& d):m_manager(m), m_dep_manager(d) {} - private: - ci_dependency* mk_dependency(interval const& a, interval const& b, bound_deps bd) const { - ci_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; - } - }; - - small_object_allocator m_alloc; - ci_value_manager m_val_manager; - unsynch_mpq_manager m_num_manager; - mutable ci_dependency_manager m_dep_manager; - im_config m_config; - mutable interval_manager m_imanager; - region m_region; - - typedef interval_manager::interval interval; - - void set_var_interval(lpvar v, interval & b) const; - - void set_var_interval_signs(lpvar v, interval & b) const; - - void set_var_interval_signs_with_deps(lpvar v, interval & b) const; - - ci_dependency* mk_dep(lp::constraint_index ci) const; - - lp::lar_solver& ls(); - const lp::lar_solver& ls() const; -public: - intervals(core* c, reslimit& lim) : - common(c), - m_alloc("intervals"), - m_dep_manager(m_val_manager, m_alloc), - m_config(m_num_manager, m_dep_manager), - m_imanager(lim, im_config(m_num_manager, m_dep_manager)) - {} - bool get_lemmas(); - bool get_lemma(monomial const& m); - bool monomial_has_lower_bound(lpvar j) const; - bool monomial_has_upper_bound(lpvar j) const; - bool product_has_upper_bound(int sign, const svector&) const; - lp::impq get_upper_bound_of_monomial(lpvar j) const; - lp::impq get_lower_bound_of_monomial(lpvar j) const; - interval mul(const svector&) const; - interval mul_signs(const svector&) const; - interval mul_signs_with_deps(const svector&) const; - void get_explanation_of_upper_bound_for_monomial(lpvar j, svector& expl) const; - void get_explanation_of_lower_bound_for_monomial(lpvar j, svector& expl) const; - std::ostream& print_explanations(const svector &, std::ostream&) const; -}; -} // end of namespace nla diff --git a/src/math/lp/nla_solver.cpp b/src/math/lp/nla_solver.cpp index 97afcfb24..fca0c245d 100644 --- a/src/math/lp/nla_solver.cpp +++ b/src/math/lp/nla_solver.cpp @@ -24,7 +24,7 @@ #include "math/lp/var_eqs.h" #include "math/lp/factorization.h" #include "math/lp/nla_solver.h" -#include "math/lp/nla_intervals.h" +//#include "math/lp/nla_intervals.h" namespace nla { void solver::add_monomial(lpvar v, unsigned sz, lpvar const* vs) { diff --git a/src/math/lp/nla_solver.h b/src/math/lp/nla_solver.h index bf5d39671..4d7d7d041 100644 --- a/src/math/lp/nla_solver.h +++ b/src/math/lp/nla_solver.h @@ -26,7 +26,7 @@ Revision History: #include "math/lp/lar_solver.h" #include "math/lp/monomial.h" #include "math/lp/nla_core.h" -#include "math/lp/nla_intervals.h" +// #include "math/lp/nla_intervals.h" namespace nla {