mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

out of memory in horner::split_with_var()

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-07-02 17:00:15 -07:00
parent 7bac714762
commit d7265ab4d0
5 changed files with 94 additions and 25 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

46
src/math/lp/horner.cpp
View file

@ -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<lpvar, unsigned>& oc
// j -> the number of expressions j appears in
void horner::get_occurences_map(const nla_expr<rational>& e, std::unordered_map<lpvar, unsigned>& 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<lpvar> seen;
@ -141,13 +140,16 @@ void horner::get_occurences_map(const nla_expr<rational>& 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<lpvar, unsigned> occurences;
@ -192,7 +195,9 @@ nex horner::cross_nested_of_sum(const nex& e) {
tout << "(v"<<p.first << ", "<< p.second<<")";
}
tout << std::endl << "most occured = v" << j << std::endl;);
return split_with_var(e, j);
nex ret = split_with_var(e, j);
TRACE("nla_cn", tout << "ret =" << ret << "\n";);
return ret;
}
template <typename T> nex horner::create_expr_from_row(const T& row) {
@ -213,11 +218,18 @@ template <typename T> 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 <typename T>
interv horner::interval_of_mul(const vector<nla_expr<T>>& es) {
interv horner::interval_of_mul(const vector<nla_expr<T>>& 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<nla_expr<T>>& 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 <typename T>
interv horner::interval_of_sum(const vector<nla_expr<T>>& 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<nla_expr<T>>& 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);
}
}

2
src/math/lp/horner.h
View file

@ -40,6 +40,8 @@ public:
template <typename T> nla_expr<rational> create_expr_from_row(const T&);
intervals::interval interval_of_expr(const nla_expr<rational>& 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<rational> nexvar(lpvar j) const;
nla_expr<rational> cross_nested_of_sum(const nla_expr<rational>&);
void get_occurences_map(const nla_expr<rational>& e,

20
src/math/lp/nla_expr.h
View file

@ -207,19 +207,29 @@ public:
return m_j == j;
if (is_mul()) {
for (const nla_expr<T>& c : children()) {
if (c.is_var() && c.var() == j) return true;
if (c.contains(j))
return true;
}
}
return false;
}
}
};
template <typename T>
nla_expr<T> operator/(const nla_expr<T>& 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<T>::scalar(T(1));
nla_expr<T> b;
bool seenj = false;
for (const nla_expr<T>& 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) {

37
src/math/lp/nla_intervals.cpp
View file

@ -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<lp::constraint_index> 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<lp::constraint_index> 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);
}

14
src/math/lp/nla_intervals.h
View file

@ -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