From d7265ab4d098214f70427b3c9a8379c2611190da Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 2 Jul 2019 17:00:15 -0700 Subject: [PATCH] out of memory in horner::split_with_var() Signed-off-by: Lev Nachmanson --- src/math/lp/horner.cpp | 46 ++++++++++++++++++++++------------- src/math/lp/horner.h | 2 ++ src/math/lp/nla_expr.h | 20 +++++++++++---- src/math/lp/nla_intervals.cpp | 37 +++++++++++++++++++++++++++- src/math/lp/nla_intervals.h | 14 +++++++++-- 5 files changed, 94 insertions(+), 25 deletions(-) diff --git a/src/math/lp/horner.cpp b/src/math/lp/horner.cpp index 7d3042abf..d96e87dd6 100644 --- a/src/math/lp/horner.cpp +++ b/src/math/lp/horner.cpp @@ -57,8 +57,6 @@ void horner::horner_lemmas() { for (unsigned i = 0; i < s && !done(); i++) { lemma_on_row(m.m_rows[((i + r) %s)]); } - - SASSERT(false); } nex horner::nexvar(lpvar j) const { @@ -122,6 +120,7 @@ unsigned horner::random_most_occured_var(std::unordered_map& oc // j -> the number of expressions j appears in void horner::get_occurences_map(const nla_expr& e, std::unordered_map& occurences) const { + TRACE("nla_cn", tout << "e = " << e << std::endl;); SASSERT(e.type() == expr_type::SUM); for (const auto & ce : e.children()) { std::unordered_set seen; @@ -141,13 +140,16 @@ void horner::get_occurences_map(const nla_expr& e, std::unordered_map< } } else if (ce.type() == expr_type::VAR) { process_var_occurences(ce.var(), seen, occurences); - } else { + } else if (ce.type() == expr_type::SCALAR) { + } else { + TRACE("nla_cn", tout << "unexpected expression ce = " << ce << std::endl;); SASSERT(false); } } } nex horner::split_with_var(const nex& e, lpvar j) { + TRACE("nla_cn", tout << "e = " << e << ", j = v" << j << "\n";); if (!e.is_sum()) return e; nex a, b; @@ -180,6 +182,7 @@ nex horner::split_with_var(const nex& e, lpvar j) { } nex horner::cross_nested_of_sum(const nex& e) { + TRACE("nla_cn", ); if (!e.is_sum()) return e; std::unordered_map occurences; @@ -192,7 +195,9 @@ nex horner::cross_nested_of_sum(const nex& e) { tout << "(v"< nex horner::create_expr_from_row(const T& row) { @@ -213,11 +218,18 @@ template nex horner::create_expr_from_row(const T& row) { } intervals::interval horner::interval_of_expr(const nex& e) { + TRACE("nla_cn", tout << e.type() << " e=" << e << std::endl;); interv a; switch (e.type()) { case expr_type::SCALAR: m_intervals.set_lower(a, e.value()); m_intervals.set_upper(a, e.value()); + m_intervals.set_lower_is_open(a, false); + m_intervals.set_lower_is_inf(a, false); + m_intervals.set_upper_is_open(a, false); + m_intervals.set_upper_is_inf(a, false); + + TRACE("nla_cn", tout << "e.value() = " << e.value() << "\n"; m_intervals.display(tout, a) << '\n';); return a; case expr_type::SUM: return interval_of_sum(e.children()); @@ -225,6 +237,7 @@ intervals::interval horner::interval_of_expr(const nex& e) { return interval_of_mul(e.children()); case expr_type::VAR: set_var_interval(e.var(), a); + TRACE("nla_cn", tout << "a = "; m_intervals.display(tout, a) << "\n";); return a; default: TRACE("nla_cn", tout << e.type() << "\n";); @@ -233,16 +246,17 @@ intervals::interval horner::interval_of_expr(const nex& e) { } } template -interv horner::interval_of_mul(const vector>& es) { +interv horner::interval_of_mul(const vector>& es) { interv a = interval_of_expr(es[0]); if (m_intervals.is_zero(a)) { - TRACE("nla_cn", tout << "interv = "; m_intervals.display(tout, a); tout << "\n";); - return a; + TRACE("nla_cn", tout << "got zero\n";); + return a; } + TRACE("nla_cn", tout << "es[0]= "<< es[0] << std::endl << "a = "; m_intervals.display(tout, a); tout << "\n";); for (unsigned k = 1; k < es.size(); k++) { interv b = interval_of_expr(es[k]); if (m_intervals.is_zero(b)) { - TRACE("nla_cn", tout << "interv = "; m_intervals.display(tout, b); tout << "\n";); + TRACE("nla_cn", tout << "got zero\n";); return b; } interv c; @@ -250,26 +264,25 @@ interv horner::interval_of_mul(const vector>& es) { m_intervals.mul(a, b, c, deps); m_intervals.set(a, c); m_intervals.add_deps(a, b, deps, a); + TRACE("nla_cn", tout << "a = "; m_intervals.display(tout, a); tout << "\n";); } - TRACE("nla_cn", tout << "interv = "; m_intervals.display(tout, a); tout << "\n";); return a; } template interv horner::interval_of_sum(const vector>& es) { - TRACE("nla_cn", tout << "es[0]= " << es[0] << "\n";); interv a = interval_of_expr(es[0]); - TRACE("nla_cn", tout << "interv = "; m_intervals.display(tout, a); tout << "\n";); + TRACE("nla_cn", tout << "es[0]= " << es[0] << "\n"; m_intervals.display(tout, a) << "\n";); if (m_intervals.is_inf(a)) { return a; } for (unsigned k = 1; k < es.size(); k++) { - TRACE("nla_cn", tout << "es[k]= " << es[k] << "\n";); + TRACE("nla_cn", tout << "es[" << k << "]= " << es[k] << "\n";); interv b = interval_of_expr(es[k]); - TRACE("nla_cn", tout << "interv = "; m_intervals.display(tout, a); tout << "\n";); if (m_intervals.is_inf(b)) { - return a; + TRACE("nla_cn", tout << "got inf\n";); + return b; } interv c; interval_deps deps; @@ -278,10 +291,10 @@ interv horner::interval_of_sum(const vector>& es) { m_intervals.add_deps(a, b, deps, a); TRACE("nla_cn", tout << "interv = "; m_intervals.display(tout, a); tout << "\n";); if (m_intervals.is_inf(a)) { + TRACE("nla_cn", tout << "got infinity\n";); return a; } } - TRACE("nla_cn", tout << "interv = "; m_intervals.display(tout, a); tout << "\n";); return a; } // sets the dependencies also @@ -292,7 +305,6 @@ void horner::set_var_interval(lpvar v, interv& b) { } void horner::check_interval_for_conflict(const intervals::interval& i) { - TRACE("nla_cn", tout << "interval = "; m_intervals.display(tout, i); ); - SASSERT(false); + m_intervals.check_interval_for_conflict_on_zero(i); } } diff --git a/src/math/lp/horner.h b/src/math/lp/horner.h index 9a06b294f..5e88e5529 100644 --- a/src/math/lp/horner.h +++ b/src/math/lp/horner.h @@ -40,6 +40,8 @@ public: template nla_expr create_expr_from_row(const T&); intervals::interval interval_of_expr(const nla_expr& e); void check_interval_for_conflict(const intervals::interval&); + bool check_interval_for_conflict_lower_bound(const intervals::interval&); + bool check_interval_for_conflict_upper_bound(const intervals::interval&); nla_expr nexvar(lpvar j) const; nla_expr cross_nested_of_sum(const nla_expr&); void get_occurences_map(const nla_expr& e, diff --git a/src/math/lp/nla_expr.h b/src/math/lp/nla_expr.h index cf19cfe32..12405572b 100644 --- a/src/math/lp/nla_expr.h +++ b/src/math/lp/nla_expr.h @@ -207,19 +207,29 @@ public: return m_j == j; if (is_mul()) { for (const nla_expr& c : children()) { - if (c.is_var() && c.var() == j) return true; + if (c.contains(j)) + return true; } } return false; - } - + } }; template nla_expr operator/(const nla_expr& a, lpvar j) { - SASSERT(a.is_mul()); + SASSERT((a.is_mul() && a.contains(j)) || (a.is_var() && a.var() == j)); + if (a.is_var()) + return nla_expr::scalar(T(1)); nla_expr b; + bool seenj = false; for (const nla_expr& c : a.children()) { - if (c.is_var() && c.var() == j) continue; + if (!seenj) { + if (c.contains(j)) { + if (!c.is_var()) + b.add_child(c / j); + seenj = true; + continue; + } + } b.add_child(c); } if (b.children().size() > 1) { diff --git a/src/math/lp/nla_intervals.cpp b/src/math/lp/nla_intervals.cpp index 80233e63e..0fbf3607a 100644 --- a/src/math/lp/nla_intervals.cpp +++ b/src/math/lp/nla_intervals.cpp @@ -1,6 +1,7 @@ #include "math/lp/nla_core.h" #include "math/interval/interval_def.h" #include "math/lp/nla_intervals.h" +#include "util/mpq.h" namespace nla { /* @@ -73,7 +74,41 @@ void intervals::set_var_interval_with_deps(lpvar v, interval& b) { b.m_upper_dep = nullptr; } } - + +void intervals::check_interval_for_conflict_on_zero(const interval & i) { + if (check_interval_for_conflict_on_zero_lower(i)) + return; + check_interval_for_conflict_on_zero_upper(i); +} + +bool intervals::check_interval_for_conflict_on_zero_upper(const interval & i) { + 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; + add_empty_lemma(); + svector expl; + m_dep_manager.linearize(i.m_upper_dep, expl); + _().current_expl().add_expl(expl); + return true; +} + +bool intervals::check_interval_for_conflict_on_zero_lower(const interval & i) { + if (lower_is_inf(i)) + return false; + if (unsynch_mpq_manager::is_pos(lower(i))) + return false; + if (unsynch_mpq_manager::is_zero(lower(i)) && !m_config.lower_is_open(i)) + return false; + add_empty_lemma(); + svector expl; + m_dep_manager.linearize(i.m_lower_dep, expl); + _().current_expl().add_expl(expl); + return true; +} + intervals::ci_dependency *intervals::mk_dep(lp::constraint_index ci) const { return m_dep_manager.mk_leaf(ci); } diff --git a/src/math/lp/nla_intervals.h b/src/math/lp/nla_intervals.h index 9f37026f3..8f606fffa 100644 --- a/src/math/lp/nla_intervals.h +++ b/src/math/lp/nla_intervals.h @@ -98,8 +98,10 @@ class intervals : common { 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 unsynch_mpq_manager::is_zero(a.m_lower) - && unsynch_mpq_manager::is_zero(a.m_upper); } + 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 @@ -186,7 +188,15 @@ public: void add_deps(interval const& a, interval const& b, interval_deps const& deps, interval& i) const { m_config.add_deps(a, b, deps, i); } + + 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); } void set_var_interval_with_deps(lpvar, interval &); bool is_inf(const interval& i) const { return m_config.is_inf(i); } + void check_interval_for_conflict_on_zero(const interval & i); + bool check_interval_for_conflict_on_zero_lower(const interval & i); + bool check_interval_for_conflict_on_zero_upper(const interval & i); + mpq const & lower(interval const & a) const { return m_config.lower(a); } + mpq const & upper(interval const & a) const { return m_config.upper(a); } }; // end of intervals } // end of namespace nla