From e3a852288567912bfda7675cbccb50920f41d313 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 2 Jul 2019 10:37:41 -0700 Subject: [PATCH] work on horner Signed-off-by: Lev Nachmanson --- src/math/lp/horner.cpp | 62 +++++++++++++++++++++-------------- src/math/lp/horner.h | 4 +++ src/math/lp/nla_intervals.cpp | 58 +++++++++----------------------- src/math/lp/nla_intervals.h | 32 +++++++++++------- 4 files changed, 76 insertions(+), 80 deletions(-) diff --git a/src/math/lp/horner.cpp b/src/math/lp/horner.cpp index 5e1916267..5f9ceb5c2 100644 --- a/src/math/lp/horner.cpp +++ b/src/math/lp/horner.cpp @@ -24,7 +24,7 @@ namespace nla { typedef nla_expr nex; typedef intervals::interval interv; -horner::horner(core * c) : common(c), m_intervals(c->reslim()) {} +horner::horner(core * c) : common(c), m_intervals(c, c->reslim()) {} template bool horner::row_is_interesting(const T& row) const { @@ -209,7 +209,9 @@ template nex horner::create_expr_from_row(const T& row) { return nex::mul(p.coeff(), nexvar(p.var())); } SASSERT(false); + return e; } + intervals::interval horner::interval_of_expr(const nex& e) { interv a; switch (e.type()) { @@ -222,37 +224,47 @@ intervals::interval horner::interval_of_expr(const nex& e) { case expr_type::MUL: return interval_of_mul(e.children()); case expr_type::VAR: - return interval_of_var(e.var()); + set_var_interval(e.var(), a); + return a; default: TRACE("nla_cn", tout << e.type() << "\n";); SASSERT(false); - return e; + return interv(); } } +template +interv horner::interval_of_mul(const vector>& es) { + interv a = interval_of_expr(es[0]); + for (unsigned k = 1; k < es.size(); k++) { + interv b = interval_of_expr(es[k]); + if (m_intervals.is_zero(b)) { + return b; + } + interv c; + interval_deps deps; + m_intervals.mul(a, b, c, deps); + m_intervals.set(a, c); + m_intervals.add_deps(a, b, deps, a); + if (m_intervals.is_zero(a)) + return a; + } + return a; +} +template +interv horner::interval_of_sum(const vector>& es) { + interv a = interval_of_expr(es[0]); + for (unsigned k = 1; k < es.size(); k++) { + interv b = interval_of_expr(es[k]); + interv c; + m_intervals.add(a, b, c); + m_intervals.set(a, c); + } + return a; +} +// sets the dependencies also void horner::set_var_interval(lpvar v, interv& b) { - const auto& ls = c().m_lar_solver; - lp::constraint_index ci; - rational val; - bool is_strict; - if (ls.has_lower_bound(v, ci, val, is_strict)) { - m_intervals.set_lower(b, val); - m_intervals.set_lower_is_open(b, is_strict); - m_intervals.set_lower_is_inf(b, false); - } - else { - m_intervals.set_lower_is_open(b, true); - m_intervals.set_lower_is_inf(b, true); - } - if (ls.has_upper_bound(v, ci, val, is_strict)) { - m_intervals.set_upper(b, val); - m_intervals.set_upper_is_open(b, is_strict); - m_intervals.set_upper_is_inf(b, false); - } - else { - m_intervals.set_upper_is_open(b, true); - m_intervals.set_upper_is_inf(b, true); - } + m_intervals.set_var_interval_with_deps(v, b); } void horner::check_interval_for_conflict(const intervals::interval&) { diff --git a/src/math/lp/horner.h b/src/math/lp/horner.h index 01c41d562..9a06b294f 100644 --- a/src/math/lp/horner.h +++ b/src/math/lp/horner.h @@ -47,5 +47,9 @@ public: unsigned random_most_occured_var(std::unordered_map& occurences); nla_expr split_with_var(const nla_expr &, lpvar); void set_var_interval(lpvar j, intervals::interval&); + template + intervals::interval interval_of_sum(const vector>&); + template + intervals::interval interval_of_mul(const vector>&); }; // end of horner } diff --git a/src/math/lp/nla_intervals.cpp b/src/math/lp/nla_intervals.cpp index 27fdf3593..80233e63e 100644 --- a/src/math/lp/nla_intervals.cpp +++ b/src/math/lp/nla_intervals.cpp @@ -45,13 +45,13 @@ void intervals::set_var_interval_signs(lpvar v, interval& b) const { m_config.set_upper_is_inf(b, true); } } - -void intervals::set_var_interval_signs_with_deps(lpvar v, interval& b) const { +*/ +void intervals::set_var_interval_with_deps(lpvar v, interval& b) { 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(b, 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); @@ -62,7 +62,7 @@ void intervals::set_var_interval_signs_with_deps(lpvar v, interval& b) const { 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(b, 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); @@ -78,7 +78,7 @@ intervals::ci_dependency *intervals::mk_dep(lp::constraint_index ci) const { return m_dep_manager.mk_leaf(ci); } -*/ + std::ostream& intervals::display(std::ostream& out, const interval& i) const { if (m_imanager.lower_is_inf(i)) { out << "(-oo"; @@ -94,46 +94,18 @@ std::ostream& intervals::display(std::ostream& out, const interval& i) const { return out; } -/* -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; +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; } -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); -} -*/ -} +} // end of nla namespace // instantiate the template template class interval_manager; diff --git a/src/math/lp/nla_intervals.h b/src/math/lp/nla_intervals.h index 6c6a3c797..086b5794e 100644 --- a/src/math/lp/nla_intervals.h +++ b/src/math/lp/nla_intervals.h @@ -20,12 +20,15 @@ #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 { +class intervals : common { class ci_value_manager { public: void inc_ref(lp::constraint_index const & v) { @@ -86,8 +89,8 @@ class intervals { // Getters mpq const & lower(interval const & a) const { return a.m_lower; } - mpq & lower(interval & a) { 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; } @@ -145,24 +148,21 @@ private: void set_var_interval_signs(lpvar v, interval & b) const; - void set_var_interval_signs_with_deps(lpvar v, interval & b) const; + void set_var_interval_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(reslimit& lim) : + 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 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; @@ -175,6 +175,14 @@ 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); } -}; - + bool is_zero(const interval& a) const { return m_config.is_zero(a); } + 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); } + void set(interval& a, const interval& b) { m_imanager.set(a, b); } + void mul(const interval& a, const interval& b, interval& c, interval_deps& deps) { m_imanager.mul(a, b, c, deps); } + void add_deps(interval const& a, interval const& b, interval_deps const& deps, interval& i) const { + m_config.add_deps(a, b, deps, i); + } + void set_var_interval_with_deps(lpvar, interval &); +}; // end of intervals } // end of namespace nla