From c040a0b9a51756b68f4fcefb7a62b1869c67b14c Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Mon, 1 Jul 2019 13:18:26 -0700 Subject: [PATCH] save Signed-off-by: Lev Nachmanson --- src/math/lp/horner.cpp | 60 +++++++++-- src/math/lp/horner.h | 3 + src/math/lp/nla_core.cpp | 4 +- src/math/lp/nla_core.h | 2 + src/math/lp/nla_expr.h | 2 +- src/math/lp/nla_intervals.cpp | 184 +--------------------------------- src/math/lp/nla_intervals.h | 31 ++---- 7 files changed, 76 insertions(+), 210 deletions(-) diff --git a/src/math/lp/horner.cpp b/src/math/lp/horner.cpp index 2320aaf5d..5e1916267 100644 --- a/src/math/lp/horner.cpp +++ b/src/math/lp/horner.cpp @@ -23,7 +23,8 @@ namespace nla { typedef nla_expr nex; -horner::horner(core * c) : common(c) {} +typedef intervals::interval interv; +horner::horner(core * c) : common(c), m_intervals(c->reslim()) {} template bool horner::row_is_interesting(const T& row) const { @@ -39,7 +40,7 @@ void horner::lemma_on_row(const T& row) { if (!row_is_interesting(row)) return; nex e = create_expr_from_row(row); - TRACE("nla_cn", tout << "cn e = " << e << std::endl;); + TRACE("nla_cn", tout << "cross nested e = " << e << std::endl;); intervals::interval inter = interval_of_expr(e); check_interval_for_conflict(inter); } @@ -95,6 +96,7 @@ void process_mul_occurences(const nex& e, std::unordered_set& seen, std:: } } +// return a valid j if some variable appears more than once unsigned horner::random_most_occured_var(std::unordered_map& occurences) { unsigned max = 0; unsigned ret = -1; @@ -111,6 +113,8 @@ unsigned horner::random_most_occured_var(std::unordered_map& oc } } } + if (max <= 1) + return -1; SASSERT(ret + 1); return ret; } @@ -166,12 +170,13 @@ nex horner::split_with_var(const nex& e, lpvar j) { } if (b.is_undef()) { + SASSERT(b.children().size() == 0); nex r(expr_type::MUL); r.add_child(nex::var(j)); - r.add_child(a); + r.add_child(cross_nested_of_sum(a)); return r; } - return nex::sum(nex::mul(a, nex::var(j)), b); + return nex::sum(nex::mul(cross_nested_of_sum(a), nex::var(j)), b); } nex horner::cross_nested_of_sum(const nex& e) { @@ -180,6 +185,7 @@ nex horner::cross_nested_of_sum(const nex& e) { std::unordered_map occurences; get_occurences_map(e, occurences); lpvar j = random_most_occured_var(occurences); + if (j + 1 == 0) return e; TRACE("nla_cn", tout << "e = " << e << "\noccurences "; for (auto p : occurences){ @@ -202,13 +208,53 @@ template nex horner::create_expr_from_row(const T& row) { const auto &p = *row.begin(); return nex::mul(p.coeff(), nexvar(p.var())); } - SASSERT(false); } intervals::interval horner::interval_of_expr(const nex& e) { - - SASSERT(false); + interv a; + switch (e.type()) { + case expr_type::SCALAR: + m_intervals.set_lower(a, e.value()); + m_intervals.set_upper(a, e.value()); + return a; + case expr_type::SUM: + return interval_of_sum(e.children()); + case expr_type::MUL: + return interval_of_mul(e.children()); + case expr_type::VAR: + return interval_of_var(e.var()); + default: + TRACE("nla_cn", tout << e.type() << "\n";); + SASSERT(false); + return e; + } } + +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); + } +} + void horner::check_interval_for_conflict(const intervals::interval&) { SASSERT(false); } diff --git a/src/math/lp/horner.h b/src/math/lp/horner.h index f02bd5326..01c41d562 100644 --- a/src/math/lp/horner.h +++ b/src/math/lp/horner.h @@ -28,7 +28,9 @@ class core; class horner : common { + intervals m_intervals; public: + horner(core *core); void horner_lemmas(); template // T has an iterator of (coeff(), var()) @@ -44,5 +46,6 @@ public: std::unordered_map& ) const; 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&); }; // end of horner } diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index ac91066eb..60e46757f 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -30,7 +30,9 @@ core::core(lp::lar_solver& s, reslimit & lim) : m_order(this), m_monotone(this), m_horner(this), - m_emons(m_evars) {} + m_emons(m_evars), + m_reslim(lim) +{} bool core::compare_holds(const rational& ls, llc cmp, const rational& rs) const { switch(cmp) { diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index 306e9818f..bd0656303 100644 --- a/src/math/lp/nla_core.h +++ b/src/math/lp/nla_core.h @@ -93,6 +93,8 @@ private: emonomials m_emons; svector m_add_buffer; public: + reslimit m_reslim; + reslimit & reslim() { return m_reslim; } emonomials& emons() { return m_emons; } const emonomials& emons() const { return m_emons; } // constructor diff --git a/src/math/lp/nla_expr.h b/src/math/lp/nla_expr.h index 80b623666..cf19cfe32 100644 --- a/src/math/lp/nla_expr.h +++ b/src/math/lp/nla_expr.h @@ -61,7 +61,7 @@ public: expr_type& type() { return m_type; } const vector& children() const { return m_children; } vector& children() { return m_children; } - + const T& value() const { SASSERT(m_type == expr_type::SCALAR); return m_v; } std::string str() const { std::stringstream ss; ss << *this; return ss.str(); } std::ostream & print_sum(std::ostream& out) const { bool first = true; diff --git a/src/math/lp/nla_intervals.cpp b/src/math/lp/nla_intervals.cpp index 52a3cd375..27fdf3593 100644 --- a/src/math/lp/nla_intervals.cpp +++ b/src/math/lp/nla_intervals.cpp @@ -3,19 +3,7 @@ #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; @@ -32,102 +20,6 @@ intervals::interval intervals::mul_signs_with_deps(const svector& vars) c return a; } -void intervals::get_lemma_for_zero_interval(monomial const& m) { - if (val(m).is_zero()) return; - interval signs_a = mul_signs_with_deps(m.vars()); - add_empty_lemma(); - svector expl; - m_dep_manager.linearize(signs_a.m_lower_dep, expl); - TRACE("nla_solver", print_vector(expl, tout) << "\n";); - _().current_expl().add_expl(expl); - mk_ineq(m.var(), llc::EQ); - TRACE("nla_solver", _().print_lemma(tout); ); -} - -bool intervals::get_lemma_for_lower(const monomial& m, const interval& a) { - if (m_vars_pushed_up[m.var()] > 10) - return false; - lp::impq lb(rational(a.m_lower)); - if (m_config.lower_is_open(a)) - lb.y = 1; - - lp::impq v(val(m.var())); - if (v < lb) { - m_vars_pushed_up[m.var()] = m_vars_pushed_up[m.var()] + 1; - 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; - } - return false; -} - -bool intervals::get_lemma_for_upper(const monomial& m, const interval& a) { - if (m_vars_pushed_down[m.var()] > 10) - return false; - lp::impq ub(rational(a.m_upper)); - if (m_config.upper_is_open(a)) - ub.y = 1; - lp::impq v(val(m.var())); - if (v > ub) { - m_vars_pushed_down[m.var()] = m_vars_pushed_down[m.var()] + 1; - 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; -} -bool intervals::get_lemma(monomial const& m) { - interval b, c, d; - interval a = mul(m.vars()); - if (m_imanager.is_zero(a)) { - get_lemma_for_zero_interval(m); - return true; - } - if (!m_imanager.lower_is_inf(a)) { - return get_lemma_for_lower(m, a); - } - - if (!m_imanager.upper_is_inf(a)) { - return get_lemma_for_upper(m, a); - } - 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 { @@ -186,27 +78,7 @@ 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; -} - +*/ std::ostream& intervals::display(std::ostream& out, const interval& i) const { if (m_imanager.lower_is_inf(i)) { out << "(-oo"; @@ -222,7 +94,7 @@ 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)); @@ -260,55 +132,7 @@ bool intervals::product_has_upper_bound(int sign, const svector& vars) co 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 ) -} -void intervals::push() { - m_vars_pushed_up.push(); - m_vars_pushed_down.push(); -} -void intervals::pop(unsigned k) { - m_vars_pushed_up.pop(k); - m_vars_pushed_down.pop(k); -} - -void intervals::init() { - SASSERT(m_vars_pushed_down.size() == m_vars_pushed_up.size()); - unsigned n = c().m_lar_solver.number_of_vars(); - while (m_vars_pushed_up.size() < n) { - m_vars_pushed_up.push_back(0); - m_vars_pushed_down.push_back(0); - } -} +*/ } // instantiate the template diff --git a/src/math/lp/nla_intervals.h b/src/math/lp/nla_intervals.h index a720183f9..6c6a3c797 100644 --- a/src/math/lp/nla_intervals.h +++ b/src/math/lp/nla_intervals.h @@ -20,19 +20,12 @@ #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 { - // fields to throttle the propagation on intervals - lp::stacked_vector m_vars_pushed_up; - lp::stacked_vector m_vars_pushed_down; +class intervals { class ci_value_manager { public: void inc_ref(lp::constraint_index const & v) { @@ -93,8 +86,8 @@ class intervals : common { // 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 const & upper(interval const & a) const { return a.m_upper; } 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; } @@ -156,36 +149,32 @@ private: 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), + intervals(reslimit& lim) : 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); - void get_lemma_for_zero_interval(monomial const& m); - bool get_lemma_for_lower(monomial const& m, const interval& ); - bool get_lemma_for_upper(monomial const& m, const interval &); 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; - void push(); - void pop(unsigned k); - void init(); std::ostream& display(std::ostream& out, const intervals::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); } }; } // end of namespace nla