From 14094bb052acea03f536f446abddc563e4ae5598 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 14 Dec 2019 19:02:25 -0800 Subject: [PATCH] code review (#98) * streamline type conversions Signed-off-by: Nikolaj Bjorner * nits Signed-off-by: Nikolaj Bjorner * updates Signed-off-by: Nikolaj Bjorner * na Signed-off-by: Nikolaj Bjorner * use fixed array allocation for sum Signed-off-by: Nikolaj Bjorner * use fixed array allocation for sum Signed-off-by: Nikolaj Bjorner * revert creation time allocation Signed-off-by: Nikolaj Bjorner * fix assertion Signed-off-by: Nikolaj Bjorner * separate grobner_core Signed-off-by: Nikolaj Bjorner * grobner_core simplifications Signed-off-by: Nikolaj Bjorner --- src/math/lp/cross_nested.h | 76 ++--- src/math/lp/horner.cpp | 4 +- src/math/lp/horner.h | 2 +- src/math/lp/nex.h | 110 +++---- src/math/lp/nex_creator.cpp | 263 +++++++--------- src/math/lp/nex_creator.h | 211 ++++++++----- src/math/lp/nla_common.cpp | 17 +- src/math/lp/nla_common.h | 2 +- src/math/lp/nla_core.h | 2 +- src/math/lp/nla_grobner.cpp | 570 +++++++++++++++++----------------- src/math/lp/nla_grobner.h | 127 +++++--- src/math/lp/nla_intervals.cpp | 18 +- 12 files changed, 685 insertions(+), 717 deletions(-) diff --git a/src/math/lp/cross_nested.h b/src/math/lp/cross_nested.h index 6c897073d..ddf23fb2d 100644 --- a/src/math/lp/cross_nested.h +++ b/src/math/lp/cross_nested.h @@ -90,18 +90,18 @@ public: } } if (have_factor == false) return nullptr; - nex_mul* f = m_nex_creator.mk_mul(); + m_nex_creator.m_mk_mul.reset(); for (const auto & p : m_nex_creator.occurences_map()) { // randomize here: todo if (p.second.m_occs == size) { - f->add_child_in_power(m_nex_creator.mk_var(p.first), p.second.m_power); + m_nex_creator.m_mk_mul *= nex_pow(m_nex_creator.mk_var(p.first), p.second.m_power); } } - return f; + return m_nex_creator.m_mk_mul.mk(); } static bool has_common_factor(const nex_sum* c) { TRACE("nla_cn", tout << "c=" << *c << "\n";); - auto & ch = c->children(); + auto & ch = *c; auto common_vars = get_vars_of_expr(ch[0]); for (lpvar j : common_vars) { bool divides_the_rest = true; @@ -195,10 +195,10 @@ public: clear_maps(); for (const auto * ce : *e) { if (ce->is_mul()) { - to_mul(ce)->get_powers_from_mul(m_nex_creator.powers()); + ce->to_mul().get_powers_from_mul(m_nex_creator.powers()); update_occurences_with_powers(); } else if (ce->is_var()) { - add_var_occs(to_var(ce)->var()); + add_var_occs(ce->to_var().var()); } } remove_singular_occurences(); @@ -317,9 +317,7 @@ public: } } TRACE("nla_cn_details", tout << "occs="; dump_occurences(tout, m_nex_creator.occurences_map()) << "\n";); - } - - + } void remove_singular_occurences() { svector r; @@ -369,27 +367,28 @@ public: return ret; } - static bool is_divisible_by_var(nex* ce, lpvar j) { + static bool is_divisible_by_var(nex const* ce, lpvar j) { return (ce->is_mul() && to_mul(ce)->contains(j)) || (ce->is_var() && to_var(ce)->var() == j); } // all factors of j go to a, the rest to b - void pre_split(nex_sum * e, lpvar j, nex_sum*& a, nex*& b) { + void pre_split(nex_sum * e, lpvar j, nex_sum const*& a, nex const*& b) { TRACE("nla_cn_details", tout << "e = " << * e << ", j = " << m_nex_creator.ch(j) << std::endl;); SASSERT(m_nex_creator.is_simplified(*e)); - a = m_nex_creator.mk_sum(); + nex_creator::sum_factory sf(m_nex_creator); m_b_split_vec.clear(); - for (nex * ce: *e) { + for (nex const* ce: *e) { TRACE("nla_cn_details", tout << "ce = " << *ce << "\n";); if (is_divisible_by_var(ce, j)) { - a->add_child(m_nex_creator.mk_div(*ce , j)); + sf += m_nex_creator.mk_div(*ce , j); } else { - m_b_split_vec.push_back(ce); + m_b_split_vec.push_back(const_cast(ce)); } } + a = sf.mk(); TRACE("nla_cn_details", tout << "a = " << *a << "\n";); SASSERT(a->size() >= 2 && m_b_split_vec.size()); - a = to_sum(m_nex_creator.simplify_sum(a)); + a = to_sum(m_nex_creator.simplify_sum(const_cast(a))); if (m_b_split_vec.size() == 1) { b = m_b_split_vec[0]; @@ -401,11 +400,11 @@ public: } } - void update_front_with_split_with_non_empty_b(nex* &e, lpvar j, vector & front, nex_sum* a, nex* b) { + void update_front_with_split_with_non_empty_b(nex* &e, lpvar j, vector & front, nex_sum const* a, nex const* b) { TRACE("nla_cn_details", tout << "b = " << *b << "\n";); e = m_nex_creator.mk_sum(m_nex_creator.mk_mul(m_nex_creator.mk_var(j), a), b); // e = j*a + b if (!a->is_linear()) { - nex **ptr_to_a = ((*to_mul((*to_sum(e))[0])))[1].ee(); + nex **ptr_to_a = e->to_sum()[0]->to_mul()[1].ee(); push_to_front(front, ptr_to_a); } @@ -415,7 +414,7 @@ public: } } - void update_front_with_split(nex* & e, lpvar j, vector & front, nex_sum* a, nex* b) { + void update_front_with_split(nex* & e, lpvar j, vector & front, nex_sum const* a, nex const* b) { if (b == nullptr) { e = m_nex_creator.mk_mul(m_nex_creator.mk_var(j), a); if (!to_sum(a)->is_linear()) @@ -428,7 +427,7 @@ public: bool split_with_var(nex*& e, lpvar j, vector & front) { SASSERT(e->is_sum()); TRACE("nla_cn", tout << "e = " << *e << ", j=" << nex_creator::ch(j) << "\n";); - nex_sum* a; nex * b; + nex_sum const* a; nex const* b; pre_split(to_sum(e), j, a, b); /* When we have e without a non-trivial common factor then @@ -451,6 +450,7 @@ public: } bool done() const { return m_done; } + #if Z3DEBUG nex * normalize_sum(nex_sum* a) { NOT_IMPLEMENTED_YET(); @@ -461,41 +461,7 @@ public: TRACE("nla_cn", tout << *a << "\n";); NOT_IMPLEMENTED_YET(); return nullptr; - /* - int sum_j = -1; - for (unsigned j = 0; j < a->size(); j ++) { - a->children()[j] = normalize(a->children()[j]); - if (a->children()[j]->is_sum()) - sum_j = j; - } - - if (sum_j == -1) { - nex * r; - a->simplify(&r); - SASSERT(r->is_simplified()); - return r; - } - - nex_sum *r = m_nex_creator.mk_sum(); - nex_sum *as = to_sum(a->children()[sum_j]); - for (unsigned k = 0; k < as->size(); k++) { - nex_mul *b = m_nex_creator.mk_mul(as->children()[k]); - for (unsigned j = 0; j < a->size(); j ++) { - if ((int)j != sum_j) - b->add_child(a->children()[j]); - } - nex *e; - b->simplify(&e); - r->add_child(e); - } - TRACE("nla_cn", tout << *r << "\n";); - nex *rs = normalize_sum(r); - SASSERT(rs->is_simplified()); - return rs; - */ - } - - + } nex * normalize(nex* a) { if (a->is_elementary()) diff --git a/src/math/lp/horner.cpp b/src/math/lp/horner.cpp index ba9ca5aef..7b968e236 100644 --- a/src/math/lp/horner.cpp +++ b/src/math/lp/horner.cpp @@ -25,7 +25,7 @@ namespace nla { typedef intervals::interval interv; -horner::horner(core * c, intervals * i) : common(c, i), m_fixed_as_scalars(false) {} +horner::horner(core * c, intervals * i) : common(c, i), m_row_sum(m_nex_creator), m_fixed_as_scalars(false) {} template bool horner::row_has_monomial_to_refine(const T& row) const { @@ -80,7 +80,7 @@ bool horner::lemmas_on_row(const T& row) { c().clear_and_resize_active_var_set(); create_sum_from_row(row, cn.get_nex_creator(), m_row_sum, m_fixed_as_scalars, nullptr); set_active_vars_weights(); // without this call the comparisons will be incorrect - nex* e = m_nex_creator.simplify(&m_row_sum); + nex* e = m_nex_creator.simplify(m_row_sum.mk()); TRACE("nla_horner", tout << "e = " << * e << "\n";); if (e->get_degree() < 2) return false; diff --git a/src/math/lp/horner.h b/src/math/lp/horner.h index 7f561b1f3..ffb40877d 100644 --- a/src/math/lp/horner.h +++ b/src/math/lp/horner.h @@ -30,7 +30,7 @@ class core; class horner : common { - nex_sum m_row_sum; + nex_creator::sum_factory m_row_sum; unsigned m_row_index; bool m_fixed_as_scalars; public: diff --git a/src/math/lp/nex.h b/src/math/lp/nex.h index 14573c769..592fcb834 100644 --- a/src/math/lp/nex.h +++ b/src/math/lp/nex.h @@ -20,7 +20,6 @@ #include #include "math/lp/nla_defs.h" #include -#include namespace nla { class nex; typedef std::function nex_lt; @@ -141,14 +140,18 @@ public: }; class nex_pow { - nex* m_e; + friend class cross_nested; + friend class nex_creator; + + nex const* m_e; unsigned m_power; + nex ** ee() const { return & const_cast(m_e); } + nex *& e() { return const_cast(m_e); } + public: - explicit nex_pow(nex* e, unsigned p): m_e(e), m_power(p) {} + explicit nex_pow(nex const* e, unsigned p): m_e(e), m_power(p) {} const nex * e() const { return m_e; } - nex *& e() { return m_e; } - nex ** ee() { return & m_e; } unsigned pow() const { return m_power; } std::ostream& print(std::ostream& s) const { @@ -168,6 +171,7 @@ public: } return s; } + std::string to_string() const { std::stringstream s; print(s); @@ -177,16 +181,24 @@ public: }; inline unsigned get_degree_children(const vector& children) { - int degree = 0; + int degree = 0; for (const auto& p : children) { - degree += p.e()->get_degree() * p.pow(); + degree += p.e()->get_degree() * p.pow(); } return degree; } class nex_mul : public nex { + friend class nex_creator; + friend class cross_nested; + friend class grobner_core; // only debug. rational m_coeff; vector m_children; + + nex_pow* begin() { return m_children.begin(); } + nex_pow* end() { return m_children.end(); } + nex_pow& operator[](unsigned j) { return m_children[j]; } + public: const nex* get_child_exp(unsigned j) const override { return m_children[j].e(); } unsigned get_child_pow(unsigned j) const override { return m_children[j].pow(); } @@ -194,26 +206,19 @@ public: unsigned number_of_child_powers() const { return m_children.size(); } nex_mul() : m_coeff(1) {} + nex_mul(rational const& c, vector const& args) : m_coeff(c), m_children(args) {} - const rational& coeff() const { - return m_coeff; - } - - rational& coeff() { - return m_coeff; - } + const rational& coeff() const { return m_coeff; } unsigned size() const override { return m_children.size(); } expr_type type() const override { return expr_type::MUL; } - vector& children() { return m_children;} - const vector& children() const { return m_children;} // A monomial is 'pure' if does not have a numeric coefficient. bool is_pure_monomial() const { return size() == 0 || !m_children[0].e()->is_scalar(); } std::ostream & print(std::ostream& out) const override { bool first = true; if (!m_coeff.is_one()) { - out << m_coeff; + out << m_coeff << " "; first = false; } for (const nex_pow& v : m_children) { @@ -227,37 +232,9 @@ public: return out; } - void add_child(const rational& r) { - m_coeff *= r; - } - - void add_child(nex* e) { - if (e->is_scalar()) { - m_coeff *= e->to_scalar().value(); - return; - } - add_child_in_power(e, 1); - } - - void add_child_in_power(nex_pow& p) { - add_child_in_power(p.e(), p.pow()); - } - const nex_pow& operator[](unsigned j) const { return m_children[j]; } - nex_pow& operator[](unsigned j) { return m_children[j]; } const nex_pow* begin() const { return m_children.begin(); } const nex_pow* end() const { return m_children.end(); } - nex_pow* begin() { return m_children.begin(); } - nex_pow* end() { return m_children.end(); } - - void add_child_in_power(nex* e, int power) { - if (e->is_scalar()) { - m_coeff *= (e->to_scalar().value()).expt(power); - } - else { - m_children.push_back(nex_pow(e, power)); - } - } bool contains(lpvar j) const { for (const nex_pow& c : *this) { @@ -281,8 +258,12 @@ public: } unsigned get_degree() const override { - return get_degree_children(children()); - } + int degree = 0; + for (const auto& p : *this) { + degree += p.e()->get_degree() * p.pow(); + } + return degree; + } bool is_linear() const override { return get_degree() < 2; // todo: make it more efficient @@ -303,14 +284,19 @@ public: class nex_sum : public nex { + friend class nex_creator; + friend class cross_nested; + friend class grobner_core; ptr_vector m_children; -public: - nex_sum() {} - nex_sum(ptr_vector const& ch) : m_children(ch) {} + nex*& operator[](unsigned j) { return m_children[j]; } + +public: + + nex_sum(ptr_vector const& ch) : m_children(ch) {} + expr_type type() const override { return expr_type::SUM; } - ptr_vector& children() { return m_children; } - const ptr_vector& children() const { return m_children; } + unsigned size() const override { return m_children.size(); } bool is_linear() const override { @@ -339,7 +325,7 @@ public: std::ostream & print(std::ostream& out) const override { bool first = true; - for (const nex* v : m_children) { + for (const nex* v : *this) { std::string s = v->str(); if (first) { first = false; @@ -369,12 +355,10 @@ public: } return degree; } - const nex* operator[](unsigned j) const { return m_children[j]; } - nex*& operator[](unsigned j) { return m_children[j]; } - const ptr_vector::const_iterator begin() const { return m_children.begin(); } - const ptr_vector::const_iterator end() const { return m_children.end(); } + nex const* operator[](unsigned j) const { return m_children[j]; } + const nex * const* begin() const { return m_children.c_ptr(); } + const nex * const* end() const { return m_children.c_ptr() + m_children.size(); } - void add_child(nex* e) { m_children.push_back(e); } #ifdef Z3DEBUG void sort() override { NOT_IMPLEMENTED_YET(); @@ -413,20 +397,14 @@ inline std::ostream& operator<<(std::ostream& out, const nex& e ) { return e.print(out); } -// inline bool less_than_nex_standard(const nex* a, const nex* b) { -// lt_on_vars lt = [](lpvar j, lpvar k) { return j < k; }; -// return less_than_nex(a, b, lt); -// } - inline rational get_nex_val(const nex* e, std::function var_val) { switch (e->type()) { case expr_type::SCALAR: return to_scalar(e)->value(); case expr_type::SUM: { rational r(0); - for (nex* c: e->to_sum()) { + for (nex const* c: e->to_sum()) r += get_nex_val(c, var_val); - } return r; } case expr_type::MUL: { @@ -470,7 +448,7 @@ inline std::unordered_set get_vars_of_expr(const nex *e ) { } } -inline bool is_zero_scalar(nex *e) { +inline bool is_zero_scalar(nex const*e) { return e->is_scalar() && e->to_scalar().value().is_zero(); } } diff --git a/src/math/lp/nex_creator.cpp b/src/math/lp/nex_creator.cpp index 7dd6b4dd0..111592eeb 100644 --- a/src/math/lp/nex_creator.cpp +++ b/src/math/lp/nex_creator.cpp @@ -30,7 +30,7 @@ nex * nex_creator::mk_div(const nex& a, lpvar j) { SASSERT(a.is_mul() || (a.is_var() && a.to_var().var() == j)); if (a.is_var()) return mk_scalar(rational(1)); - vector bv; + mul_factory mf(*this); bool seenj = false; auto ma = a.to_mul(); for (auto& p : ma) { @@ -39,54 +39,41 @@ nex * nex_creator::mk_div(const nex& a, lpvar j) { if (!seenj && c->contains(j)) { SASSERT(!c->is_var() || c->to_var().var() == j); if (!c->is_var()) { - bv.push_back(nex_pow(mk_div(*c, j), 1)); + mf *= nex_pow(mk_div(*c, j), 1); } if (pow != 1) { - bv.push_back(nex_pow(clone(c), pow - 1)); + mf *= nex_pow(clone(c), pow - 1); } seenj = true; } else { - bv.push_back(nex_pow(clone(c), pow)); + mf *= nex_pow(clone(c), pow); } } - if (bv.size() == 1 && bv.begin()->pow() == 1 && ma.coeff().is_one()) { - return bv.begin()->e(); - } - if (bv.empty()) { - return mk_scalar(rational(ma.coeff())); - } - - auto m = mk_mul(bv); - m->coeff() = ma.coeff(); - return m; - + mf *= ma.coeff(); + return mf.mk_reduced(); } -// TBD: describe what this does +// return true if p is a constant, update r with value of p raised to pow. bool nex_creator::eat_scalar_pow(rational& r, const nex_pow& p, unsigned pow) { - if (p.e()->is_mul()) { - const nex_mul & m = p.e()->to_mul(); - if (m.size() == 0) { - const rational& coeff = m.coeff(); - if (coeff.is_one()) - return true; - r *= coeff.expt(p.pow() * pow); - return true; + if (p.e()->is_mul() && p.e()->to_mul().size() == 0) { + auto const& m = p.e()->to_mul(); + if (!m.coeff().is_one()) { + r *= m.coeff().expt(p.pow() * pow); } - return false; + return true; } if (!p.e()->is_scalar()) return false; const nex_scalar &pe = p.e()->to_scalar(); - if (pe.value().is_one()) - return true; // r does not change here - r *= pe.value().expt(p.pow() * pow); + if (!pe.value().is_one()) { + r *= pe.value().expt(p.pow() * pow); + } return true; } void nex_creator::simplify_children_of_mul(vector & children, rational& coeff) { - TRACE("grobner_d", print_vector(children, tout);); + TRACE("grobner_d", print_vector(children, tout << "children_of_mul: "); tout << "\n";); vector to_promote; unsigned j = 0; for (nex_pow& p : children) { @@ -163,14 +150,6 @@ bool nex_creator::children_are_simplified(const vector& children) const return true; } -bool nex_creator::gt_on_powers_mul(const vector& children, const nex_mul& b) const { - TRACE("nex_gt", tout << "children = "; print_vector(children, tout) << " , b = " << b << "\n";); - SASSERT(children_are_simplified(children) && is_simplified(b)); - unsigned a_deg = get_degree_children(children); - unsigned b_deg = b.get_degree(); - return a_deg == b_deg ? gt_on_powers_mul_same_degree(children, b) : a_deg > b_deg; -} - bool nex_creator::gt_on_mul_mul(const nex_mul& a, const nex_mul& b) const { TRACE("grobner_d", tout << "a = " << a << " , b = " << b << "\n";); SASSERT(is_simplified(a) && is_simplified(b)); @@ -179,72 +158,52 @@ bool nex_creator::gt_on_mul_mul(const nex_mul& a, const nex_mul& b) const { return a_deg == b_deg ? gt_on_powers_mul_same_degree(a, b) : a_deg > b_deg; } -bool nex_creator::gt_on_var_nex(const nex_var* a, const nex* b) const { - switch (b->type()) { +bool nex_creator::gt_on_var_nex(const nex_var& a, const nex& b) const { + switch (b.type()) { case expr_type::SCALAR: return true; case expr_type::VAR: - return gt(a->var() , to_var(b)->var()); + return gt(a.var(), b.to_var().var()); case expr_type::MUL: - return b->get_degree() <= 1 && gt_on_var_nex(a, (*to_mul(b))[0].e()); + return b.get_degree() <= 1 && gt_on_var_nex(a, *b.to_mul()[0].e()); case expr_type::SUM: - SASSERT(b->size() > 1); - return gt(a, (*to_sum(b))[0]); + SASSERT(b.size() > 1); + return gt(&a, b.to_sum()[0]); default: UNREACHABLE(); return false; } } -bool nex_creator::gt_nex_powers(const vector& children, const nex* b) const { - switch (b->type()) { +bool nex_creator::gt_on_mul_nex(nex_mul const& m, nex const& b) const { + switch (b.type()) { case expr_type::SCALAR: return false; case expr_type::VAR: - if (get_degree_children(children) > 1) + if (m.get_degree() > 1) return true; - SASSERT(children[0].pow() == 1); - SASSERT(!children[0].e()->is_scalar()); - return gt(children[0].e(), b); + SASSERT(m[0].pow() == 1); + SASSERT(!m[0].e()->is_scalar()); + return gt(m[0].e(), &b); case expr_type::MUL: - return gt_on_powers_mul(children, *to_mul(b)); + return gt_on_mul_mul(m, b.to_mul()); case expr_type::SUM: - return gt_nex_powers(children, (*to_sum(b))[0]); + return gt_on_mul_nex(m, *b.to_sum()[0]); default: UNREACHABLE(); return false; } } -bool nex_creator::gt_on_mul_nex(const nex_mul* a, const nex* b) const { - switch (b->type()) { - case expr_type::SCALAR: - return false; - case expr_type::VAR: - if (a->get_degree() > 1) - return true; - SASSERT(a->begin()->pow() == 1); - SASSERT(!a->begin()->e()->is_scalar()); - return gt(a->begin()->e(), b); - case expr_type::MUL: - return gt_on_mul_mul(*a, *to_mul(b)); - case expr_type::SUM: - return gt(a, (*to_sum(b))[0]); - default: - UNREACHABLE(); - return false; - } -} - -bool nex_creator::gt_on_sum_sum(const nex_sum* a, const nex_sum* b) const { - unsigned size = std::min(a->size(), b->size()); +bool nex_creator::gt_on_sum_sum(const nex_sum& a, const nex_sum& b) const { + unsigned size = std::min(a.size(), b.size()); for (unsigned j = 0; j < size; j++) { - if (gt((*a)[j], (*b)[j])) + if (gt(a[j], b[j])) return true; - if (gt((*b)[j], (*a)[j])) + if (gt(b[j], a[j])) return false; } - return a->size() > size; + return a.size() > size; } // the only difference with gt() that it disregards the coefficient in nex_mul @@ -255,21 +214,21 @@ bool nex_creator::gt_for_sort_join_sum(const nex* a, const nex* b) const { bool ret; switch (a->type()) { case expr_type::VAR: - ret = gt_on_var_nex(to_var(a), b); + ret = gt_on_var_nex(a->to_var(), *b); break; case expr_type::SCALAR: if (b->is_scalar()) - ret = to_scalar(a)->value() > to_scalar(b)->value(); + ret = a->to_scalar().value() > b->to_scalar().value(); else ret = false; // the scalars are the largest break; case expr_type::MUL: - ret = gt_nex_powers(to_mul(a)->children(), b); + ret = gt_on_mul_nex(a->to_mul(), *b); break; case expr_type::SUM: if (b->is_sum()) - return gt_on_sum_sum(to_sum(a), to_sum(b)); - return gt((*to_sum(a))[0], b); + return gt_on_sum_sum(a->to_sum(), b->to_sum()); + return gt(a->to_sum()[0], b); default: UNREACHABLE(); return false; @@ -278,31 +237,31 @@ bool nex_creator::gt_for_sort_join_sum(const nex* a, const nex* b) const { return ret; } -bool nex_creator::gt(const nex* a, const nex* b) const { - TRACE("grobner_d_", tout << *a << " ? " << *b << "\n";); - if (a == b) +bool nex_creator::gt(const nex& a, const nex& b) const { + TRACE("grobner_d_", tout << a << " ? " << b << "\n";); + if (&a == &b) return false; bool ret; - switch (a->type()) { + switch (a.type()) { case expr_type::VAR: - ret = gt_on_var_nex(to_var(a), b); + ret = gt_on_var_nex(a.to_var(), b); break; case expr_type::SCALAR: - ret = b->is_scalar() && to_scalar(a)->value() > to_scalar(b)->value(); + ret = b.is_scalar() && a.to_scalar().value() > b.to_scalar().value(); // the scalars are the largest break; case expr_type::MUL: - ret = gt_on_mul_nex(to_mul(a), b); + ret = gt_on_mul_nex(a.to_mul(), b); break; case expr_type::SUM: - if (b->is_sum()) - return gt_on_sum_sum(to_sum(a), to_sum(b)); - return gt((*to_sum(a))[0], b); + if (b.is_sum()) + return gt_on_sum_sum(a.to_sum(), b.to_sum()); + return gt(*a.to_sum()[0], b); default: UNREACHABLE(); return false; } - TRACE("grobner_d_", tout << *a << (ret?" < ":" >= ") << *b << "\n";); + TRACE("grobner_d_", tout << a << (ret?" < ":" >= ") << b << "\n";); return ret; } @@ -357,8 +316,8 @@ bool nex_creator::mul_is_simplified(const nex_mul& e) const { nex * nex_creator::simplify_mul(nex_mul *e) { TRACE("grobner_d", tout << *e << "\n";); - rational& coeff = e->coeff(); - simplify_children_of_mul(e->children(), coeff); + rational& coeff = e->m_coeff; + simplify_children_of_mul(e->m_children, coeff); if (e->size() == 1 && (*e)[0].pow() == 1 && coeff.is_one()) return (*e)[0].e(); @@ -371,14 +330,14 @@ nex * nex_creator::simplify_mul(nex_mul *e) { nex* nex_creator::simplify_sum(nex_sum *e) { TRACE("grobner_d", tout << "was e = " << *e << "\n";); - simplify_children_of_sum(e->children()); + simplify_children_of_sum(*e); nex *r; if (e->size() == 1) { - r = (*e)[0]; + r = const_cast((*e)[0]); } else if (e->size() == 0) { r = mk_scalar(rational(0)); } else { - r = e; + r = const_cast(e); } TRACE("grobner_d", tout << "became r = " << *r << "\n";); return r; @@ -387,7 +346,7 @@ nex* nex_creator::simplify_sum(nex_sum *e) { bool nex_creator::sum_is_simplified(const nex_sum& e) const { if (e.size() < 2) return false; bool scalar = false; - for (nex * ee : e) { + for (nex const* ee : e) { TRACE("nla_cn_details", tout << "ee = " << *ee << "\n";); if (ee->is_sum()) { TRACE("nla_cn", tout << "not simplified e = " << e << "\n" @@ -438,7 +397,7 @@ void nex_creator::mul_to_powers(vector& children) { } // returns true if the key exists already -bool nex_creator::register_in_join_map(std::map& map, nex* e, const rational& r) const{ +bool nex_creator::register_in_join_map(std::map& map, nex const* e, const rational& r) const{ TRACE("grobner_d", tout << *e << ", r = " << r << std::endl;); auto map_it = map.find(e); if (map_it == map.end()) { @@ -453,12 +412,12 @@ bool nex_creator::register_in_join_map(std::map& map, ne } bool nex_creator::fill_join_map_for_sum( - ptr_vector & children, - std::map& map, - std::unordered_set& existing_nex, + nex_sum & sum, + std::map& map, + std::unordered_set& existing_nex, rational& common_scalar) { bool simplified = false; - for (auto e : children) { + for (auto e : sum) { if (e->is_scalar()) { simplified = true; common_scalar += e->to_scalar().value(); @@ -466,7 +425,7 @@ bool nex_creator::fill_join_map_for_sum( } existing_nex.insert(e); if (e->is_mul()) { - nex_mul * m = to_mul(e); + nex_mul const * m = to_mul(e); simplified |= register_in_join_map(map, m, m->coeff()); } else { SASSERT(e->is_var()); @@ -476,34 +435,33 @@ bool nex_creator::fill_join_map_for_sum( return simplified; } // a + 3bc + 2bc => a + 5bc -void nex_creator::sort_join_sum(ptr_vector & children) { - TRACE("grobner_d", print_vector_of_ptrs(children, tout);); - std::map map([this](const nex *a , const nex *b) +void nex_creator::sort_join_sum(nex_sum& sum) { + TRACE("grobner_d", tout << sum << "\n";); + std::map map([this](const nex *a , const nex *b) { return gt_for_sort_join_sum(a, b); }); - std::unordered_set allocated_nexs; // handling (nex*) as numbers + std::unordered_set allocated_nexs; // handling (nex*) as numbers rational common_scalar(0); - fill_join_map_for_sum(children, map, allocated_nexs, common_scalar); + fill_join_map_for_sum(sum, map, allocated_nexs, common_scalar); TRACE("grobner_d", for (auto & p : map ) { tout << "(" << *p.first << ", " << p.second << ") ";}); - children.clear(); + sum.m_children.reset(); for (auto& p : map) { - process_map_pair(p.first, p.second, children, allocated_nexs); + process_map_pair(const_cast(p.first), p.second, sum, allocated_nexs); } if (!common_scalar.is_zero()) { - children.push_back(mk_scalar(common_scalar)); + sum.m_children.push_back(mk_scalar(common_scalar)); } TRACE("grobner_d", tout << "map="; for (auto & p : map ) tout << "(" << *p.first << ", " << p.second << ") "; - tout << "\nchildren="; print_vector_of_ptrs(children, tout) << "\n";); + tout << "\nchildren=" << sum << "\n";); } -void nex_creator::simplify_children_of_sum(ptr_vector & children) { - TRACE("grobner_d", print_vector_of_ptrs(children, tout);); +void nex_creator::simplify_children_of_sum(nex_sum& s) { ptr_vector to_promote; - unsigned k = 0; - for (unsigned j = 0; j < children.size(); j++) { - nex* e = children[j] = simplify(children[j]); + unsigned k = 0; + for (unsigned j = 0; j < s.size(); j++) { + nex* e = s[j] = simplify(s[j]); if (e->is_sum()) { to_promote.push_back(e); } else if (is_zero_scalar(e)) { @@ -511,21 +469,19 @@ void nex_creator::simplify_children_of_sum(ptr_vector & children) { } else if (e->is_mul() && to_mul(e)->coeff().is_zero() ) { continue; } else { - children[k++] = e; + s.m_children[k++] = e; } } - - TRACE("grobner_d", print_vector_of_ptrs(children, tout);); - children.shrink(k); - + s.m_children.shrink(k); + for (nex *e : to_promote) { - for (nex *ee : e->to_sum()) { + for (nex const*ee : e->to_sum()) { if (!is_zero_scalar(ee)) - children.push_back(ee); + s.m_children.push_back(const_cast(ee)); } } - - sort_join_sum(children); + + sort_join_sum(s); } @@ -544,10 +500,11 @@ bool nex_mul::all_factors_are_elementary() const { } nex * nex_creator::mk_div_sum_by_mul(const nex_sum& m, const nex_mul& b) { - nex_sum * r = mk_sum(); + sum_factory sf(*this); for (auto e : m) { - r->add_child(mk_div_by_mul(*e, b)); + sf += mk_div_by_mul(*e, b); } + nex* r = sf.mk(); TRACE("grobner_d", tout << *r << "\n";); return r; } @@ -555,12 +512,12 @@ nex * nex_creator::mk_div_sum_by_mul(const nex_sum& m, const nex_mul& b) { nex * nex_creator::mk_div_mul_by_mul(const nex_mul& a, const nex_mul& b) { SASSERT(a.all_factors_are_elementary() && b.all_factors_are_elementary()); b.get_powers_from_mul(m_powers); - nex_mul* ret = new nex_mul(); + m_mk_mul.reset(); for (auto& p_from_a : a) { TRACE("grobner_d", tout << "p_from_a = " << p_from_a << "\n";); const nex* e = p_from_a.e(); if (e->is_scalar()) { - ret->add_child_in_power(clone(e), p_from_a.pow()); + m_mk_mul *= nex_pow(clone(e), p_from_a.pow()); TRACE("grobner_d", tout << "processed scalar\n";); continue; } @@ -568,13 +525,13 @@ nex * nex_creator::mk_div_mul_by_mul(const nex_mul& a, const nex_mul& b) { lpvar j = to_var(e)->var(); auto it = m_powers.find(j); if (it == m_powers.end()) { - ret->add_child_in_power(clone(e), p_from_a.pow()); + m_mk_mul *= nex_pow(clone(e), p_from_a.pow()); } else { unsigned pa = p_from_a.pow(); unsigned& pb = it->second; SASSERT(pa); if (pa > pb) { - ret->add_child_in_power(mk_var(j), pa - pb); + m_mk_mul *= nex_pow(mk_var(j), pa - pb); m_powers.erase(it); } else if (pa == pb) { m_powers.erase(it); @@ -584,17 +541,11 @@ nex * nex_creator::mk_div_mul_by_mul(const nex_mul& a, const nex_mul& b) { // but the key j in m_powers remains pb -= pa; } - } - TRACE("grobner_d", tout << *ret << "\n";); + } } SASSERT(m_powers.size() == 0); - if (ret->size() == 0) { - delete ret; - TRACE("grobner_d", tout << "return scalar\n";); - return mk_scalar(a.coeff() / b.coeff()); - } - ret->coeff() = a.coeff() / b.coeff(); - add_to_allocated(ret); + m_mk_mul *= (a.coeff() / b.coeff()); + nex* ret = m_mk_mul.mk_reduced(); TRACE("grobner_d", tout << *ret << "\n";); return ret; } @@ -634,7 +585,7 @@ nex* nex_creator::simplify(nex* e) { } // adds to children the corrected expression and also adds to allocated the new expressions -void nex_creator::process_map_pair(nex *e, const rational& coeff, ptr_vector & children, std::unordered_set& allocated_nexs) { +void nex_creator::process_map_pair(nex*e, const rational& coeff, nex_sum & sum, std::unordered_set& allocated_nexs) { TRACE("grobner_d", tout << "e=" << *e << " , coeff= " << coeff << "\n";); if (coeff.is_zero()) { TRACE("grobner_d", tout << "did nothing\n";); @@ -645,14 +596,17 @@ void nex_creator::process_map_pair(nex *e, const rational& coeff, ptr_vectoris_mul()) { - e->to_mul().coeff() = coeff; - children.push_back(simplify(e)); + e->to_mul().m_coeff = coeff; + sum.m_children.push_back(simplify(e)); } else { SASSERT(e->is_var()); if (coeff.is_one()) { - children.push_back(e); + sum.m_children.push_back(e); } else { - children.push_back(mk_mul(mk_scalar(coeff), e)); + mul_factory mf(*this); + mf *= coeff; + mf *= e; + sum.m_children.push_back(mf.mk()); } } } @@ -684,20 +638,21 @@ nex* nex_creator::canonize_mul(nex_mul *a) { SASSERT(np.pow()); unsigned power = np.pow(); nex_sum const& s = np.e()->to_sum(); // s is going to explode - nex_sum * r = mk_sum(); + sum_factory sf(*this); nex *sclone = power > 1 ? clone(&s) : nullptr; - for (nex *e : s) { - nex_mul *m = mk_mul(); + for (nex const*e : s) { + mul_factory mf(*this); if (power > 1) - m->add_child_in_power(sclone, power - 1); - m->add_child(e); + mf *= nex_pow(sclone, power - 1); + mf *= nex_pow(e, 1); for (unsigned k = 0; k < a->size(); k++) { if (k == j) continue; - m->add_child_in_power(clone((*a)[k].e()), (*a)[k].pow()); + mf *= nex_pow(clone((*a)[k].e()), (*a)[k].pow()); } - r->add_child(m); + sf += mf.mk(); } + nex* r = sf.mk(); TRACE("grobner_d", tout << "canonized a = " << *r << "\n";); return canonize(r); } diff --git a/src/math/lp/nex_creator.h b/src/math/lp/nex_creator.h index 0caa51f9e..825c0c463 100644 --- a/src/math/lp/nex_creator.h +++ b/src/math/lp/nex_creator.h @@ -19,6 +19,7 @@ --*/ #pragma once #include +#include #include "util/map.h" #include "math/lp/nex.h" namespace nla { @@ -59,7 +60,7 @@ class nex_creator { public: static std::string ch(unsigned j) { std::stringstream s; - s << "v" << j; + s << "v" << j; return s.str(); } @@ -71,51 +72,76 @@ public: unsigned get_number_of_vars() const { return m_active_vars_weights.size(); } - + void set_var_weight(unsigned j, unsigned weight) { m_active_vars_weights[j] = weight; } private: - svector& active_vars_weights() { return m_active_vars_weights;} - const svector& active_vars_weights() const { return m_active_vars_weights;} + svector& active_vars_weights() { return m_active_vars_weights; } + const svector& active_vars_weights() const { return m_active_vars_weights; } + + nex_mul* mk_mul(const vector& v) { + auto r = alloc(nex_mul, rational::zero(), v); + add_to_allocated(r); + return r; + } + + void mul_args() { } + + template + void mul_args(K e) { + m_mk_mul *= e; + } + + template + void mul_args(K e, Args ... es) { + m_mk_mul *= e; + mul_args(es...); + } + + template + void add_sum(T) { } + + template + void add_sum(T& r, K e, Args ... es) { + r += e; + add_sum(r, es ...); + } + + + public: nex* simplify(nex* e); - - bool gt(lpvar j, lpvar k) const{ + + bool gt(lpvar j, lpvar k) const { unsigned wj = m_active_vars_weights[j]; unsigned wk = m_active_vars_weights[k]; return wj != wk ? wj > wk : j > k; } + + void simplify_children_of_mul(vector& children, rational&); - // just compare the underlying expressions - bool gt_on_nex_pow(const nex_pow & a, const nex_pow& b) const { - return gt(a.e(), b.e()); - } - - void simplify_children_of_mul(vector & children, rational&); - - nex * clone(const nex* a) { + nex* clone(const nex* a) { switch (a->type()) { - case expr_type::VAR: + case expr_type::VAR: return mk_var(to_var(a)->var()); - case expr_type::SCALAR: + case expr_type::SCALAR: return mk_scalar(to_scalar(a)->value()); case expr_type::MUL: { - auto m = to_mul(a); - auto r = mk_mul(); - for (const auto& p : m->children()) { - r->add_child_in_power(clone(p.e()), p.pow()); + mul_factory mf(*this); + for (const auto& p : a->to_mul()) { + mf *= nex_pow(clone(p.e()), p.pow()); } - r->coeff() = m->coeff(); - return r; + mf *= a->to_mul().coeff(); + return mf.mk(); } case expr_type::SUM: { - auto r = mk_sum(); - for (nex * e : *to_sum(a)) { - r->add_child(clone(e)); + sum_factory sf(*this); + for (nex const* e : a->to_sum()) { + sf += clone(e); } - return r; + return sf.mk(); } default: UNREACHABLE(); @@ -126,86 +152,110 @@ public: const std::unordered_map& occurences_map() const { return m_occurences_map; } std::unordered_map& occurences_map() { return m_occurences_map; } - const std::unordered_map & powers() const { return m_powers; } - std::unordered_map & powers() { return m_powers; } - + const std::unordered_map& powers() const { return m_powers; } + std::unordered_map& powers() { return m_powers; } + void add_to_allocated(nex* r) { m_allocated.push_back(r); } + // NSB: we can use region allocation, but still need to invoke destructor + // because of 'rational' (and m_children in nex_mul unless we get rid of this) void pop(unsigned sz) { - for (unsigned j = sz; j < m_allocated.size(); j ++) - delete m_allocated[j]; + for (unsigned j = sz; j < m_allocated.size(); j++) + dealloc(m_allocated[j]); m_allocated.resize(sz); } void clear() { - for (auto e: m_allocated) - delete e; + for (auto e : m_allocated) + dealloc(e); m_allocated.clear(); } + nex_creator() : m_mk_mul(*this) {} + ~nex_creator() { clear(); } unsigned size() const { return m_allocated.size(); } + class mul_factory { + nex_creator& c; + rational m_coeff; + vector m_args; + public: + mul_factory(nex_creator& c) :c(c), m_coeff(1) {} + void reset() { m_coeff = rational::one(); m_args.reset(); } + void operator*=(rational const& coeff) { m_coeff *= coeff; } + void operator*=(nex_pow const& p) { m_args.push_back(p); } + void operator*=(nex const* n) { m_args.push_back(nex_pow(n, 1)); } + bool empty() const { return m_args.empty(); } + nex_mul* mk() { + auto r = alloc(nex_mul, m_coeff, m_args); + c.add_to_allocated(r); + return r; + } + nex* mk_reduced() { + if (m_args.empty()) return c.mk_scalar(m_coeff); + if (m_coeff.is_one() && m_args.size() == 1 && m_args[0].pow() == 1) return m_args[0].e(); + return mk(); + } + }; + + class sum_factory { + nex_creator& c; + ptr_vector m_args; + public: + sum_factory(nex_creator& c) :c(c) {} + void reset() { m_args.reset(); } + void operator+=(nex const* n) { m_args.push_back(const_cast(n)); } + void operator+=(nex* n) { m_args.push_back(n); } + bool empty() const { return m_args.empty(); } + nex_sum* mk() { return c.mk_sum(m_args); } + }; + + mul_factory m_mk_mul; + nex_sum* mk_sum() { - auto r = new nex_sum(); - add_to_allocated(r); - return r; - } - template - void add_children(T) { } - - template - void add_children(T r, K e, Args ... es) { - r->add_child(e); - add_children(r, es ...); + ptr_vector v0; + return mk_sum(v0); } - nex_sum* mk_sum(const ptr_vector& v) { - auto r = new nex_sum(v); + nex_sum* mk_sum(const ptr_vector& v) { + auto r = alloc(nex_sum, v); add_to_allocated(r); return r; } - - nex_mul* mk_mul(const vector& v) { - auto r = new nex_mul(); - add_to_allocated(r); - r->children() = v; - return r; - } template nex_sum* mk_sum(K e, Args... es) { - auto r = new nex_sum(); - add_to_allocated(r); - r->add_child(e); - add_children(r, es...); - return r; + sum_factory sf(*this); + sf += e; + add_sum(sf, es...); + return sf.mk(); } nex_var* mk_var(lpvar j) { - auto r = new nex_var(j); + auto r = alloc(nex_var, j); add_to_allocated(r); return r; } nex_mul* mk_mul() { - auto r = new nex_mul(); + auto r = alloc(nex_mul); add_to_allocated(r); return r; } template nex_mul* mk_mul(K e, Args... es) { - auto r = new nex_mul(); - add_to_allocated(r); - add_children(r, e, es...); - return r; + m_mk_mul.reset(); + m_mk_mul *= e; + mul_args(es...); + return m_mk_mul.mk(); } nex_scalar* mk_scalar(const rational& v) { - auto r = new nex_scalar(v); + auto r = alloc(nex_scalar, v); add_to_allocated(r); return r; } @@ -227,30 +277,31 @@ public: void mul_to_powers(vector& children); - - void sort_join_sum(ptr_vector & children); - bool fill_join_map_for_sum(ptr_vector & children, - std::map& map, - std::unordered_set& existing_nex, + void sort_join_sum(nex_sum & sum); + bool fill_join_map_for_sum(nex_sum & sum, + std::map& map, + std::unordered_set& existing_nex, rational& common_scalar); - bool register_in_join_map(std::map&, nex*, const rational&) const; + bool register_in_join_map(std::map&, nex const*, const rational&) const; - void simplify_children_of_sum(ptr_vector & children); + void simplify_children_of_sum(nex_sum & sum); bool eat_scalar_pow(rational& r, const nex_pow& p, unsigned); bool children_are_simplified(const vector& children) const; - bool gt(const nex* a, const nex* b) const; - bool gt_nex_powers(const vector&, const nex* b) const; - bool gt_on_powers_mul(const vector&, const nex_mul& b) const; + bool gt(const nex& a, const nex& b) const; + bool gt(const nex* a, const nex* b) const { return gt(*a, *b); } template bool gt_on_powers_mul_same_degree(const T&, const nex_mul& b) const; bool gt_for_sort_join_sum(const nex* a, const nex* b) const; - bool gt_on_mul_mul(const nex_mul& a, const nex_mul& b) const; - bool gt_on_var_nex(const nex_var* a, const nex* b) const; - bool gt_on_mul_nex(const nex_mul* a, const nex* b) const; - bool gt_on_sum_sum(const nex_sum* a, const nex_sum* b) const; - void process_map_pair(nex *e, const rational& coeff, ptr_vector & children, std::unordered_set&); + bool gt_on_mul_mul(const nex_mul& a, const nex_mul& b) const; + bool gt_on_sum_sum(const nex_sum& a, const nex_sum& b) const; + bool gt_on_var_nex(const nex_var& a, const nex& b) const; + bool gt_on_mul_nex(nex_mul const&, const nex& b) const; + bool gt_on_nex_pow(const nex_pow& a, const nex_pow& b) const { + return (a.pow() > b.pow()) || (a.pow() == b.pow() && gt(a.e(), b.e())); + } + void process_map_pair(nex*e, const rational& coeff, nex_sum & sum, std::unordered_set&); #ifdef Z3DEBUG static bool equal(const nex*, const nex* ); diff --git a/src/math/lp/nla_common.cpp b/src/math/lp/nla_common.cpp index a5473f8f1..3ce457b55 100644 --- a/src/math/lp/nla_common.cpp +++ b/src/math/lp/nla_common.cpp @@ -139,7 +139,8 @@ nex * common::nexvar(const rational & coeff, lpvar j, nex_creator& cn, bool fixe return cn.mk_mul(cn.mk_scalar(coeff), cn.mk_var(j)); } const monic& m = c().emons()[j]; - nex_mul * e = cn.mk_mul(cn.mk_scalar(coeff)); + nex_creator::mul_factory mf(cn); + mf *= coeff; for (lpvar k : m.vars()) { if (fixed_as_scalars && c().var_is_fixed(k)) { auto & b = c().m_lar_solver.get_lower_bound(k).x; @@ -147,13 +148,14 @@ nex * common::nexvar(const rational & coeff, lpvar j, nex_creator& cn, bool fixe TRACE("nla_grobner", tout << "[" << k << "] is fixed to zero\n";); return nullptr; } - e->coeff() *= b; + mf *= b; continue; } c().insert_to_active_var_set(k); - e->add_child(cn.mk_var(k)); + mf *= cn.mk_var(k); CTRACE("nla_grobner", c().is_monic_var(k), c().print_var(k, tout) << "\n";); } + nex* e = mf.mk(); TRACE("nla_grobner", tout << *e;); return e; } @@ -161,7 +163,7 @@ nex * common::nexvar(const rational & coeff, lpvar j, nex_creator& cn, bool fixe template common::ci_dependency* common::create_sum_from_row(const T& row, nex_creator& cn, - nex_sum& sum, + nex_creator::sum_factory& sum, bool fixed_as_scalars, ci_dependency_manager* dep_manager ) { @@ -169,7 +171,7 @@ template common::ci_dependency* common::create_sum_from_row(const T TRACE("nla_horner", tout << "row="; m_core->print_term(row, tout) << "\n";); ci_dependency * dep = nullptr; SASSERT(row.size() > 1); - sum.children().clear(); + sum.reset(); for (const auto &p : row) { nex* e = nexvar(p.coeff(), p.var(), cn, fixed_as_scalars); if (!e) @@ -181,10 +183,9 @@ template common::ci_dependency* common::create_sum_from_row(const T dep = dep_manager->mk_join(dep, dep_manager->mk_leaf(lc)); if (uc + 1) dep = dep_manager->mk_join(dep, dep_manager->mk_leaf(uc)); - sum.add_child(e); + sum += e; } } - TRACE("nla_grobner", tout << "sum =" << sum << "\ndep="; m_intervals->print_dependencies(dep, tout);); return dep; } @@ -255,6 +256,6 @@ var_weight common::get_var_weight(lpvar j) const { } -template nla::common::ci_dependency* nla::common::create_sum_from_row, true, unsigned int> >(old_vector, true, unsigned int> const&, nla::nex_creator&, nla::nex_sum&, bool, ci_dependency_manager*); +template nla::common::ci_dependency* nla::common::create_sum_from_row, true, unsigned int> >(old_vector, true, unsigned int> const&, nla::nex_creator&, nla::nex_creator::sum_factory&, bool, ci_dependency_manager*); template dependency_manager::dependency* nla::common::get_fixed_vars_dep_from_row, true, unsigned int> >(old_vector, true, unsigned int> const&, dependency_manager&); diff --git a/src/math/lp/nla_common.h b/src/math/lp/nla_common.h index 634c2baf7..b0ed12bc8 100644 --- a/src/math/lp/nla_common.h +++ b/src/math/lp/nla_common.h @@ -122,7 +122,7 @@ struct common { // nex* nexvar(lpvar j, nex_creator&, svector & fixed_vars_constraints); nex* nexvar(const rational& coeff, lpvar j, nex_creator&, bool); template - ci_dependency* create_sum_from_row(const T&, nex_creator&, nex_sum&, bool, ci_dependency_manager*); + ci_dependency* create_sum_from_row(const T&, nex_creator&, nex_creator::sum_factory&, bool, ci_dependency_manager*); template ci_dependency* get_fixed_vars_dep_from_row(const T&, ci_dependency_manager& dep_manager); void set_active_vars_weights(); diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index 5f3a6ef58..fcab27135 100644 --- a/src/math/lp/nla_core.h +++ b/src/math/lp/nla_core.h @@ -90,7 +90,7 @@ public: intervals m_intervals; horner m_horner; nla_settings m_nla_settings; - grobner m_grobner; + grobner m_grobner; private: emonics m_emons; svector m_add_buffer; diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp index fe6bc0e5c..972324b17 100644 --- a/src/math/lp/nla_grobner.cpp +++ b/src/math/lp/nla_grobner.cpp @@ -24,27 +24,60 @@ using namespace nla; grobner::grobner(core *c, intervals *s) : common(c, s), - m_nl_gb_exhausted(false), - m_dep_manager(m_val_manager, m_alloc), - m_changed_leading_term(false), - m_look_for_fixed_vars_in_rows(false) -{} + m_gc(m_nex_creator, + c->m_reslim, + c->m_nla_settings.grobner_eqs_threshold() + ), + m_look_for_fixed_vars_in_rows(false) { + std::function de; + de = [this](lp::explanation const& e, std::ostream& out) { m_core->print_explanation(e, out); }; + m_gc = de; +} void grobner::grobner_lemmas() { c().lp_settings().stats().m_grobner_calls++; init(); - ptr_vector eqs; + ptr_vector eqs; TRACE("grobner", tout << "before:\n"; display(tout);); compute_basis(); TRACE("grobner", tout << "after:\n"; display(tout);); } -bool grobner::internalize_gb_eq(equation* ) { - NOT_IMPLEMENTED_YET(); - return false; +void grobner::check_eq(grobner_core::equation* target) { + if (m_intervals->check_nex(target->expr(), target->dep())) { + TRACE("grobner", tout << "created a lemma for "; m_gc.display_equation(tout, *target) << "\n"; + tout << "vars = \n"; + for (lpvar j : get_vars_of_expr(target->expr())) { + c().print_var(j, tout); + } + tout << "\ntarget->expr() val = " << get_nex_val(target->expr(), [this](unsigned j) { return c().val(j); }) << "\n";); + register_report(); + } } -void grobner::add_var_and_its_factors_to_q_and_collect_new_rows(lpvar j, std::queue & q) { +void grobner::register_report() { + m_reported++; +} + +void grobner::compute_basis(){ + compute_basis_init(); + if (m_rows.size() < 2) { + TRACE("nla_grobner", tout << "there are only " << m_rows.size() << " rows, exiting compute_basis()\n";); + return; + } + m_gc.compute_basis_loop(); + + TRACE("grobner", display(tout);); + for (grobner_core::equation* e : m_gc.equations()) { + check_eq(e); + } +} + +void grobner::compute_basis_init(){ + c().lp_settings().stats().m_grobner_basis_computatins++; +} + +void grobner::add_var_and_its_factors_to_q_and_collect_new_rows(lpvar j, svector & q) { if (c().active_var_set_contains(j) || c().var_is_fixed(j)) return; TRACE("grobner", tout << "j = " << j << ", "; c().print_var(j, tout) << "\n";); const auto& matrix = c().m_lar_solver.A_r(); @@ -69,22 +102,22 @@ void grobner::add_var_and_its_factors_to_q_and_collect_new_rows(lpvar j, std::qu const monic& m = c().emons()[j]; for (auto fcn : factorization_factory_imp(m, c())) { for (const factor& fc: fcn) { - q.push(var(fc)); + q.push_back(var(fc)); } } } void grobner::find_nl_cluster() { prepare_rows_and_active_vars(); - std::queue q; + svector q; for (lpvar j : c().m_to_refine) { TRACE("grobner", c().print_monic(c().emons()[j], tout) << "\n";); - q.push(j); + q.push_back(j); } - + while (!q.empty()) { - lpvar j = q.front(); - q.pop(); + lpvar j = q.back(); + q.pop_back(); add_var_and_its_factors_to_q_and_collect_new_rows(j, q); } set_active_vars_weights(); @@ -97,6 +130,29 @@ void grobner::prepare_rows_and_active_vars() { c().clear_and_resize_active_var_set(); } + +std::unordered_set grobner::get_vars_of_expr_with_opening_terms(const nex *e ) { + auto ret = get_vars_of_expr(e); + auto & ls = c().m_lar_solver; + do { + svector added; + for (lpvar j : ret) { + if (ls.column_corresponds_to_term(j)) { + const auto & t = c().m_lar_solver.get_term(ls.local_to_external(j)); + for (auto p : t) { + if (ret.find(p.var()) == ret.end()) + added.push_back(p.var()); + } + } + } + if (added.size() == 0) + return ret; + for (lpvar j: added) + ret.insert(j); + added.clear(); + } while (true); +} + void grobner::display_matrix(std::ostream & out) const { const auto& matrix = c().m_lar_solver.A_r(); out << m_rows.size() << " rows" <<"\n"; @@ -107,56 +163,106 @@ void grobner::display_matrix(std::ostream & out) const { } } -std::ostream & grobner::display(std::ostream & out) const { - display_equations(out, m_to_superpose, "m_to_superpose:"); - display_equations(out, m_to_simplify, "m_to_simplify:"); - return out; -} - -common::ci_dependency* grobner::dep_from_vector(svector & cs) { - ci_dependency * d = nullptr; - for (auto c : cs) - d = m_dep_manager.mk_join(d, m_dep_manager.mk_leaf(c)); - return d; -} - -void grobner::add_row(unsigned i) { - const auto& row = c().m_lar_solver.A_r().m_rows[i]; - TRACE("grobner", tout << "adding row to gb\n"; c().m_lar_solver.print_row(row, tout) << '\n'; - for (auto p : row) c().print_var(p.var(), tout) << "\n"; ); - nex_sum * ns = m_nex_creator.mk_sum(); - ci_dependency* dep = create_sum_from_row(row, m_nex_creator, *ns, m_look_for_fixed_vars_in_rows, &m_dep_manager); - nex* e = m_nex_creator.simplify(ns); - TRACE("grobner", tout << "e = " << *e << "\n";); - assert_eq_0(e, dep); -} - void grobner::init() { - - m_reported = 0; - del_equations(0); - SASSERT(m_equations_to_delete.size() == 0); - m_to_superpose.reset(); - m_to_simplify.reset(); + m_gc.reset(); + m_reported = 0; find_nl_cluster(); c().clear_and_resize_active_var_set(); TRACE("grobner", tout << "m_rows.size() = " << m_rows.size() << "\n";); for (unsigned i : m_rows) { add_row(i); } - for (equation* eq : m_to_simplify) { - eq->expr() = m_nex_creator.simplify(eq->expr()); - } } -bool grobner::is_trivial(equation* eq) const { +void grobner::add_row(unsigned i) { + const auto& row = c().m_lar_solver.A_r().m_rows[i]; + TRACE("grobner", tout << "adding row to gb\n"; c().m_lar_solver.print_row(row, tout) << '\n'; + for (auto p : row) c().print_var(p.var(), tout) << "\n"; ); + nex_creator::sum_factory sf(m_nex_creator); + ci_dependency* dep = create_sum_from_row(row, m_nex_creator, sf, m_look_for_fixed_vars_in_rows, &m_gc.dep()); + nex* e = m_nex_creator.simplify(sf.mk()); + TRACE("grobner", tout << "e = " << *e << "\n";); + m_gc.assert_eq_0(e, dep); +} + +/// ------------------------------- +/// grobner_core + +bool grobner_core::compute_basis_loop() { + while (!done()) { + if (compute_basis_step()) { + TRACE("grobner", tout << "progress in compute_basis_step\n";); + return true; + } + TRACE("grobner", tout << "continue compute_basis_loop\n";); + } + TRACE("grobner", tout << "return false from compute_basis_loop\n";); + TRACE("grobner_stats", print_stats(tout);); + set_gb_exhausted(); + return false; +} + +// return true iff cannot pick_next() +bool grobner_core::compute_basis_step() { + equation* eq = pick_next(); + if (!eq) { + TRACE("grobner", tout << "cannot pick an equation\n";); + return true; + } + m_stats.m_compute_steps++; + simplify_using_to_superpose(*eq); + if (canceled()) return false; + if (!simplify_to_superpose_with_eq(eq)) + return false; + TRACE("grobner", tout << "eq = "; display_equation(tout, *eq);); + superpose(eq); + insert_to_superpose(eq); + simplify_m_to_simplify(eq); + TRACE("grobner", tout << "end of iteration:\n"; display(tout);); + return false; +} + +grobner_core::equation* grobner_core::pick_next() { + equation* r = nullptr; + ptr_buffer to_delete; + for (equation* curr : m_to_simplify) { + if (is_trivial(curr)) + to_delete.push_back(curr); + else if (is_simpler(curr, r)) { + TRACE("grobner", tout << "preferring "; display_equation(tout, *curr);); + r = curr; + } + } + for (equation* e : to_delete) + del_equation(e); + if (r) + m_to_simplify.erase(r); + TRACE("grobner", tout << "selected equation: "; if (!r) tout << "\n"; else display_equation(tout, *r);); + return r; +} +grobner_core::equation_set const& grobner_core::equations() { + m_all_eqs.reset(); + for (auto e : m_to_simplify) m_all_eqs.insert(e); + for (auto e : m_to_superpose) m_all_eqs.insert(e); + return m_all_eqs; +} + +void grobner_core::reset() { + del_equations(0); + SASSERT(m_equations_to_delete.size() == 0); + m_to_superpose.reset(); + m_to_simplify.reset(); + m_stats.reset(); +} + +bool grobner_core::is_trivial(equation* eq) const { SASSERT(m_nex_creator.is_simplified(*eq->expr())); return eq->expr()->size() == 0; } // returns true if eq1 is simpler than eq2 -bool grobner::is_simpler(equation * eq1, equation * eq2) { +bool grobner_core::is_simpler(equation * eq1, equation * eq2) { if (!eq2) return true; if (is_trivial(eq1)) @@ -166,7 +272,7 @@ bool grobner::is_simpler(equation * eq1, equation * eq2) { return m_nex_creator.gt(eq2->expr(), eq1->expr()); } -void grobner::del_equation(equation * eq) { +void grobner_core::del_equation(equation * eq) { m_to_superpose.erase(eq); m_to_simplify.erase(eq); SASSERT(m_equations_to_delete[eq->m_bidx] == eq); @@ -174,56 +280,33 @@ void grobner::del_equation(equation * eq) { dealloc(eq); } -grobner::equation* grobner::pick_next() { - equation * r = nullptr; - ptr_buffer to_delete; - for (equation * curr : m_to_simplify) { - if (is_trivial(curr)) - to_delete.push_back(curr); - else if (is_simpler(curr, r)) { - TRACE("grobner", tout << "preferring "; display_equation(tout, *curr);); - r = curr; - } - } - for (equation * e : to_delete) - del_equation(e); - if (r) - m_to_simplify.erase(r); - TRACE("grobner", tout << "selected equation: "; if (!r) tout << "\n"; else display_equation(tout, *r);); - return r; -} - -grobner::equation* grobner::simplify_using_to_superpose(equation* eq) { +void grobner_core::simplify_using_to_superpose(equation& eq) { bool result = false; bool simplified; - TRACE("grobner", tout << "simplifying: "; display_equation(tout, *eq); tout << "using equalities of m_to_superpose of size " << m_to_superpose.size() << "\n";); + TRACE("grobner", tout << "simplifying: "; display_equation(tout, eq); tout << "using equalities of m_to_superpose of size " << m_to_superpose.size() << "\n";); do { simplified = false; for (equation* p : m_to_superpose) { - if (simplify_source_target(p, eq)) { + if (simplify_source_target(p, &eq)) { result = true; simplified = true; } - if (canceled()) { - return nullptr; - } - if (eq->expr()->is_scalar()) { + if (canceled() || eq.expr()->is_scalar()) { break; } } } - while (simplified && !eq->expr()->is_scalar()); + while (simplified && !eq.expr()->is_scalar()); - TRACE("grobner", tout << "simplification result: "; display_equation(tout, *eq);); - return result ? eq : nullptr; + TRACE("grobner", tout << "simplification result: "; display_equation(tout, eq);); } -const nex* grobner::get_highest_monomial(const nex* e) const { +const nex* grobner_core::get_highest_monomial(const nex* e) const { switch (e->type()) { case expr_type::MUL: - return to_mul(e); + return e; case expr_type::SUM: - return *(to_sum(e)->begin()); + return e->to_sum()[0]; case expr_type::VAR: return e; default: @@ -234,8 +317,8 @@ const nex* grobner::get_highest_monomial(const nex* e) const { // source 3f + k + l = 0, so f = (-k - l)/3 // target 2fg + 3fp + e = 0 // target is replaced by 2(-k/3 - l/3)g + 3(-k/3 - l/3)p + e = -2/3kg -2/3lg - kp -lp + e -bool grobner::simplify_target_monomials(equation * source, equation * target) { - auto * high_mon = get_highest_monomial(source->expr()); +bool grobner_core::simplify_target_monomials(equation * source, equation * target) { + nex const* high_mon = get_highest_monomial(source->expr()); if (high_mon == nullptr) return false; SASSERT(high_mon->all_factors_are_elementary()); @@ -252,26 +335,26 @@ bool grobner::simplify_target_monomials(equation * source, equation * target) { return false; } - return simplify_target_monomials_sum(source, target, targ_sum, high_mon); + return simplify_target_monomials_sum(source, target, targ_sum, *high_mon); } -unsigned grobner::find_divisible(nex_sum* targ_sum, const nex* high_mon) const { +unsigned grobner_core::find_divisible(nex_sum const& targ_sum, const nex& high_mon) const { unsigned j = 0; - for (auto t : *targ_sum) { + for (auto t : targ_sum) { if (divide_ignore_coeffs_check_only(t, high_mon)) { - TRACE("grobner_d", tout << "yes div: " << *t << " / " << *high_mon << "\n";); + TRACE("grobner_d", tout << "yes div: " << *t << " / " << high_mon << "\n";); return j; } ++j; } - TRACE("grobner_d", tout << "no div: " << *targ_sum << " / " << *high_mon << "\n";); + TRACE("grobner_d", tout << "no div: " << targ_sum << " / " << high_mon << "\n";); return -1; } -bool grobner::simplify_target_monomials_sum(equation * source, +bool grobner_core::simplify_target_monomials_sum(equation * source, equation * target, nex_sum* targ_sum, - const nex* high_mon) { - unsigned j = find_divisible(targ_sum, high_mon); + const nex& high_mon) { + unsigned j = find_divisible(*targ_sum, high_mon); if (j + 1 == 0) return false; m_changed_leading_term = (j == 0); @@ -287,88 +370,93 @@ bool grobner::simplify_target_monomials_sum(equation * source, return true; } -bool grobner::divide_ignore_coeffs_check_only_nex_mul(nex_mul* t , const nex* h) const { - TRACE("grobner_d", tout << "t = " << *t << ", h=" << *h << "\n";); - SASSERT(m_nex_creator.is_simplified(*t) && m_nex_creator.is_simplified(*h)); +bool grobner_core::divide_ignore_coeffs_check_only_nex_mul(nex_mul const& t , const nex& h) const { + TRACE("grobner_d", tout << "t = " << t << ", h=" << h << "\n";); + SASSERT(m_nex_creator.is_simplified(t) && m_nex_creator.is_simplified(h)); unsigned j = 0; // points to t - for(unsigned k = 0; k < h->number_of_child_powers(); k++) { - lpvar h_var = to_var(h->get_child_exp(k))->var(); + for(unsigned k = 0; k < h.number_of_child_powers(); k++) { + lpvar h_var = h.get_child_exp(k)->to_var().var(); bool p_swallowed = false; - for (; j < t->size() && !p_swallowed; j++) { - auto &tp = (*t)[j]; + for (; j < t.size() && !p_swallowed; j++) { + const nex_pow& tp = t[j]; if (tp.e()->to_var().var() == h_var) { - if (tp.pow() >= h->get_child_pow(k)) { + if (tp.pow() >= h.get_child_pow(k)) { p_swallowed = true; } } } if (!p_swallowed) { - TRACE("grobner_d", tout << "no div " << *t << " / " << *h << "\n";); + TRACE("grobner_d", tout << "no div " << t << " / " << h << "\n";); return false; } } - TRACE("grobner_d", tout << "division " << *t << " / " << *h << "\n";); + TRACE("grobner_d", tout << "division " << t << " / " << h << "\n";); return true; } // return true if h divides t -bool grobner::divide_ignore_coeffs_check_only(nex* n , const nex* h) const { +bool grobner_core::divide_ignore_coeffs_check_only(nex const* n , const nex& h) const { if (n->is_mul()) - return divide_ignore_coeffs_check_only_nex_mul(to_mul(n), h); + return divide_ignore_coeffs_check_only_nex_mul(n->to_mul(), h); if (!n->is_var()) return false; const nex_var * v = to_var(n); - if (h->is_var()) { - return v->var() == h->to_var().var(); + if (h.is_var()) { + return v->var() == h.to_var().var(); } - if (h->is_mul() || h->is_var()) { - if (h->number_of_child_powers() > 1) + if (h.is_mul()) { + if (h.number_of_child_powers() > 1) return false; - if (h->get_child_pow(0) != 1) + if (h.get_child_pow(0) != 1) return false; - const nex* e = h->get_child_exp(0); + const nex* e = h.get_child_exp(0); return e->is_var() && e->to_var().var() == v->var(); } return false; } -nex_mul * grobner::divide_ignore_coeffs_perform_nex_mul(nex_mul* t, const nex* h) { - nex_mul * r = m_nex_creator.mk_mul(); +nex_mul * grobner_core::divide_ignore_coeffs_perform_nex_mul(nex_mul const& t, const nex& h) { + + m_nex_creator.m_mk_mul.reset(); + unsigned j = 0; // j points to t and k runs over h - for(unsigned k = 0; k < h->number_of_child_powers(); k++) { - lpvar h_var = to_var(h->get_child_exp(k))->var(); - for (; j < t->size(); j++) { - auto &tp = (*t)[j]; + for(unsigned k = 0; k < h.number_of_child_powers(); k++) { + lpvar h_var = to_var(h.get_child_exp(k))->var(); + for (; j < t.size(); j++) { + auto const &tp = t[j]; if (tp.e()->to_var().var() == h_var) { - unsigned h_pow = h->get_child_pow(k); + unsigned h_pow = h.get_child_pow(k); SASSERT(tp.pow() >= h_pow); j++; if (tp.pow() > h_pow) { - r->add_child_in_power(tp.e(), tp.pow() - h_pow); + m_nex_creator.m_mk_mul *= nex_pow(tp.e(), tp.pow() - h_pow); } break; } else { - r->add_child_in_power(tp); + m_nex_creator.m_mk_mul *= tp; } } } - - for (; j < t->size(); j++) { - r->add_child_in_power((*t)[j]); + for (; j < t.size(); j++) { + m_nex_creator.m_mk_mul *= t[j]; } + + nex_mul* r = m_nex_creator.m_mk_mul.mk(); + TRACE("grobner", tout << "r = " << *r << " = " << t << " / " << h << "\n";); + - TRACE("grobner_d", tout << "r = " << *r << " = " << *t << " / " << *h << "\n";); + TRACE("grobner_d", tout << "r = " << *r << " = " << t << " / " << h << "\n";); return r; } // perform the division t / h, but ignores the coefficients // h does not change -nex_mul * grobner::divide_ignore_coeffs_perform(nex* e, const nex* h) { +nex_mul * grobner_core::divide_ignore_coeffs_perform(nex* e, const nex& h) { if (e->is_mul()) - return divide_ignore_coeffs_perform_nex_mul(to_mul(e), h); + return divide_ignore_coeffs_perform_nex_mul(e->to_mul(), h); SASSERT(e->is_var()); return m_nex_creator.mk_mul(); // return the empty nex_mul } @@ -377,9 +465,9 @@ nex_mul * grobner::divide_ignore_coeffs_perform(nex* e, const nex* h) { // and b*high_mon + e = 0, so high_mon = -e/b // then targ_sum->children()[j] = - (c/b) * e*p -void grobner::simplify_target_monomials_sum_j(equation * source, equation *target, nex_sum* targ_sum, const nex* high_mon, unsigned j, bool test_divisibility) { +void grobner_core::simplify_target_monomials_sum_j(equation * source, equation *target, nex_sum* targ_sum, const nex& high_mon, unsigned j, bool test_divisibility) { nex * ej = (*targ_sum)[j]; - TRACE("grobner_d", tout << "high_mon = " << *high_mon << ", ej = " << *ej << "\n";); + TRACE("grobner_d", tout << "high_mon = " << high_mon << ", ej = " << *ej << "\n";); if (test_divisibility && !divide_ignore_coeffs_check_only(ej, high_mon)) { TRACE("grobner_d", tout << "no div\n";); return; @@ -388,15 +476,16 @@ void grobner::simplify_target_monomials_sum_j(equation * source, equation *targe TRACE("grobner_d", tout << "ej_over_high_mon = " << *ej_over_high_mon << "\n";); rational c = ej->is_mul()? to_mul(ej)->coeff() : rational(1); TRACE("grobner_d", tout << "c = " << c << "\n";); - - nex_sum * ej_sum = m_nex_creator.mk_sum(); - (*targ_sum)[j] = ej_sum; - add_mul_skip_first(ej_sum ,-c/high_mon->coeff(), source->expr(), ej_over_high_mon); + + nex_creator::sum_factory sf(m_nex_creator); + add_mul_skip_first(sf ,-c/high_mon.coeff(), source->expr(), ej_over_high_mon); + + (*targ_sum)[j] = sf.mk(); TRACE("grobner_d", tout << "targ_sum = " << *targ_sum << "\n";); } // return true iff simplified -bool grobner::simplify_source_target(equation * source, equation * target) { +bool grobner_core::simplify_source_target(equation * source, equation * target) { TRACE("grobner", tout << "simplifying: "; display_equation(tout, *target); tout << "\nusing: "; display_equation(tout, *source);); TRACE("grobner_d", tout << "simplifying: " << *(target->expr()) << " using " << *(source->expr()) << "\n";); SASSERT(m_nex_creator.is_simplified(*source->expr())); @@ -418,7 +507,8 @@ bool grobner::simplify_source_target(equation * source, equation * target) { } else { break; } - } while (!canceled()); + } + while (!canceled()); if (result) { target->dep() = m_dep_manager.mk_join(target->dep(), source->dep()); update_stats_max_degree_and_size(target); @@ -430,9 +520,7 @@ bool grobner::simplify_source_target(equation * source, equation * target) { return false; } - - -void grobner::process_simplified_target(equation* target, ptr_buffer& to_remove) { +void grobner_core::process_simplified_target(equation* target, ptr_buffer& to_remove) { if (is_trivial(target)) { to_remove.push_back(target); } else if (m_changed_leading_term) { @@ -441,19 +529,8 @@ void grobner::process_simplified_target(equation* target, ptr_buffer& } } -void grobner::check_eq(equation* target) { - if (m_intervals->check_nex(target->expr(), target->dep())) { - TRACE("grobner", tout << "created a lemma for "; display_equation(tout, *target) << "\n"; - tout << "vars = \n"; - for (lpvar j : get_vars_of_expr(target->expr())) { - c().print_var(j, tout); - } - tout << "\ntarget->expr() val = " << get_nex_val(target->expr(), [this](unsigned j) { return c().val(j); }) << "\n";); - register_report(); - } -} -bool grobner::simplify_to_superpose_with_eq(equation* eq) { +bool grobner_core::simplify_to_superpose_with_eq(equation* eq) { TRACE("grobner_d", tout << "eq->exp " << *(eq->expr()) << "\n";); ptr_buffer to_insert; @@ -486,7 +563,7 @@ bool grobner::simplify_to_superpose_with_eq(equation* eq) { /* Use the given equation to simplify m_to_simplify equations */ -void grobner::simplify_m_to_simplify(equation* eq) { +void grobner_core::simplify_m_to_simplify(equation* eq) { TRACE("grobner_d", tout << "eq->exp " << *(eq->expr()) << "\n";); ptr_buffer to_delete; for (equation* target : m_to_simplify) { @@ -500,13 +577,12 @@ void grobner::simplify_m_to_simplify(equation* eq) { // if e is the sum then add to r all children of e multiplied by beta, except the first one // which corresponds to the highest monomial, // otherwise do nothing -void grobner::add_mul_skip_first(nex_sum* r, const rational& beta, nex *e, nex_mul* c) { +void grobner_core::add_mul_skip_first(nex_creator::sum_factory& sf, const rational& beta, nex *e, nex_mul* c) { if (e->is_sum()) { - nex_sum *es = to_sum(e); - for (unsigned j = 1; j < es->size(); j++) { - r->add_child(m_nex_creator.mk_mul(beta, (*es)[j], c)); + nex_sum & es = e->to_sum(); + for (unsigned j = 1; j < es.size(); j++) { + sf += m_nex_creator.mk_mul(beta, es[j], c); } - TRACE("grobner_d", tout << "r = " << *r << "\n";); } else { TRACE("grobner_d", tout << "e = " << *e << "\n";); } @@ -514,23 +590,23 @@ void grobner::add_mul_skip_first(nex_sum* r, const rational& beta, nex *e, nex_m // let e1: alpha*ab+q=0, and e2: beta*ac+e=0, then beta*qc - alpha*eb = 0 -nex * grobner::expr_superpose(nex* e1, nex* e2, const nex* ab, const nex* ac, nex_mul* b, nex_mul* c) { +nex * grobner_core::expr_superpose(nex* e1, nex* e2, const nex* ab, const nex* ac, nex_mul* b, nex_mul* c) { TRACE("grobner", tout << "e1 = " << *e1 << "\ne2 = " << *e2 <<"\n";); - nex_sum * r = m_nex_creator.mk_sum(); + nex_creator::sum_factory sf(m_nex_creator); rational alpha = - ab->coeff(); TRACE("grobner", tout << "e2 *= " << alpha << "*(" << *b << ")\n";); - add_mul_skip_first(r, alpha, e2, b); + add_mul_skip_first(sf, alpha, e2, b); rational beta = ac->coeff(); TRACE("grobner", tout << "e1 *= " << beta << "*(" << *c << ")\n";); - add_mul_skip_first(r, beta, e1, c); - nex * ret = m_nex_creator.simplify(r); + add_mul_skip_first(sf, beta, e1, c); + nex * ret = m_nex_creator.simplify(sf.mk()); TRACE("grobner", tout << "e1 = " << *e1 << "\ne2 = " << *e2 <<"\nsuperpose = " << *ret << "\n";); CTRACE("grobner", ret->is_scalar(), tout << "\n";); return ret; } // let eq1: ab+q=0, and eq2: ac+e=0, then qc - eb = 0 -void grobner::superpose(equation * eq1, equation * eq2) { +void grobner_core::superpose(equation * eq1, equation * eq2) { TRACE("grobner", tout << "eq1="; display_equation(tout, *eq1) << "eq2="; display_equation(tout, *eq2);); const nex * ab = get_highest_monomial(eq1->expr()); const nex * ac = get_highest_monomial(eq2->expr()); @@ -545,18 +621,18 @@ void grobner::superpose(equation * eq1, equation * eq2) { init_equation(eq, expr_superpose( eq1->expr(), eq2->expr(), ab, ac, b, c), m_dep_manager.mk_join(eq1->dep(), eq2->dep())); m_stats.m_superposed++; update_stats_max_degree_and_size(eq); + eq->expr() = m_nex_creator.simplify(eq->expr()); insert_to_simplify(eq); } -void grobner::register_report() { - m_reported++; -} + + // Let a be the greatest common divider of ab and bc, // then ab/a is stored in b, and ac/a is stored in c -bool grobner::find_b_c(const nex* ab, const nex* ac, nex_mul*& b, nex_mul*& c) { +bool grobner_core::find_b_c(const nex* ab, const nex* ac, nex_mul*& b, nex_mul*& c) { if (!find_b_c_check_only(ab, ac)) return false; - b = m_nex_creator.mk_mul(); c = m_nex_creator.mk_mul(); + nex_creator::mul_factory fb(m_nex_creator), fc(m_nex_creator); unsigned ab_size = ab->number_of_child_powers(); unsigned ac_size = ac->number_of_child_powers(); unsigned i = 0, j = 0; @@ -564,20 +640,20 @@ bool grobner::find_b_c(const nex* ab, const nex* ac, nex_mul*& b, nex_mul*& c) { const nex* m = ab->get_child_exp(i); const nex* n = ac->get_child_exp(j); if (m_nex_creator.gt(m, n)) { - b->add_child_in_power(const_cast(m), ab->get_child_pow(i)); + fb *= (nex_pow(const_cast(m), ab->get_child_pow(i))); if (++i == ab_size) break; } else if (m_nex_creator.gt(n, m)) { - c->add_child_in_power(const_cast(n), ac->get_child_pow(j)); + fc *= (nex_pow(const_cast(n), ac->get_child_pow(j))); if (++j == ac_size) break; } else { unsigned b_pow = ab->get_child_pow(i); unsigned c_pow = ac->get_child_pow(j); if (b_pow > c_pow) { - b->add_child_in_power(const_cast(m), b_pow - c_pow); + fb *= (nex_pow(const_cast(m), b_pow - c_pow)); } else if (c_pow > b_pow) { - c->add_child_in_power(const_cast(n), c_pow - b_pow); + fc *= (nex_pow(const_cast(n), c_pow - b_pow)); } // otherwise the power are equal and no child added to either b or c i++; j++; @@ -587,16 +663,18 @@ bool grobner::find_b_c(const nex* ab, const nex* ac, nex_mul*& b, nex_mul*& c) { } } while (i != ab_size) { - b->add_child_in_power(const_cast(ab->get_child_exp(i)), ab->get_child_pow(i)); + fb *= (nex_pow(const_cast(ab->get_child_exp(i)), ab->get_child_pow(i))); i++; } while (j != ac_size) { - c->add_child_in_power(const_cast(ac->get_child_exp(j)), ac->get_child_pow(j)); + fc *= (nex_pow(const_cast(ac->get_child_exp(j)), ac->get_child_pow(j))); j++; } + b = fb.mk(); + c = fc.mk(); TRACE("nla_grobner", tout << "b=" << *b << ", c=" <<*c << "\n";); // debug region - nex_mul *a = divide_ignore_coeffs_perform(m_nex_creator.clone(ab), b); + nex_mul *a = divide_ignore_coeffs_perform(m_nex_creator.clone(ab), *b); SASSERT(ab->get_degree() == a->get_degree() + b->get_degree()); SASSERT(ac->get_degree() == a->get_degree() + c->get_degree()); SASSERT(test_find_b_c(ab, ac, b, c)); @@ -604,7 +682,7 @@ bool grobner::find_b_c(const nex* ab, const nex* ac, nex_mul*& b, nex_mul*& c) { } // Finds out if ab and bc have a non-trivial common divider -bool grobner::find_b_c_check_only(const nex* ab, const nex* ac) const { +bool grobner_core::find_b_c_check_only(const nex* ab, const nex* ac) const { if (ab == nullptr || ac == nullptr) return false; SASSERT(m_nex_creator.is_simplified(*ab) && m_nex_creator.is_simplified(*ac)); @@ -630,94 +708,25 @@ bool grobner::find_b_c_check_only(const nex* ab, const nex* ac) const { return false; } -void grobner::superpose(equation * eq) { +void grobner_core::superpose(equation * eq) { for (equation * target : m_to_superpose) { superpose(eq, target); } } -// return true iff cannot pick_next() -bool grobner::compute_basis_step() { - equation * eq = pick_next(); - if (!eq) { - TRACE("grobner", tout << "cannot pick an equation\n";); - return true; - } - m_stats.m_compute_steps++; - equation * new_eq = simplify_using_to_superpose(eq); - if (new_eq != nullptr && eq != new_eq) { - // equation was updated using non destructive updates - eq = new_eq; - } - if (canceled()) return false; - if (!simplify_to_superpose_with_eq(eq)) - return false; - TRACE("grobner", tout << "eq = "; display_equation(tout, *eq);); - superpose(eq); - insert_to_superpose(eq); - simplify_m_to_simplify(eq); - TRACE("grobner", tout << "end of iteration:\n"; display(tout);); - return false; +bool grobner_core::canceled() { + return m_limit.get_cancel_flag(); } -void grobner::compute_basis(){ - compute_basis_init(); - if (m_rows.size() < 2) { - TRACE("nla_grobner", tout << "there are only " << m_rows.size() << " rows, exiting compute_basis()\n";); - return; - } - if (!compute_basis_loop()) { - TRACE("grobner", tout << "false from compute_basis_loop\n";); - set_gb_exhausted(); - } else { - TRACE("grobner", display(tout);); - for (equation* e : m_to_simplify) { - check_eq(e); - } - for (equation* e : m_to_superpose) { - check_eq(e); - } - } -} -void grobner::compute_basis_init(){ - c().lp_settings().stats().m_grobner_basis_computatins++; - m_stats.reset(); -} - -bool grobner::canceled() const { - return c().lp_settings().get_cancel_flag(); +bool grobner_core::done() { + return num_of_equations() >= m_grobner_eqs_threshold || canceled(); } -bool grobner::done() const { - CTRACE("grobner", (num_of_equations() >= c().m_nla_settings.grobner_eqs_threshold()), - tout << "m_num_of_equations = " << num_of_equations() << "\n";); - CTRACE("grobner", canceled(), tout << "canceled\n";); - CTRACE("grobner", m_reported > 0, tout << "m_reported = " << m_reported;); - return - num_of_equations() >= c().m_nla_settings.grobner_eqs_threshold() || - canceled() || m_reported > 0; -} - - -bool grobner::compute_basis_loop(){ - while (!done()) { - if (compute_basis_step()) { - TRACE("grobner", tout << "progress in compute_basis_step\n";); - return true; - } - TRACE("grobner", tout << "continue compute_basis_loop\n";); - } - TRACE("grobner", tout << "return false from compute_basis_loop\n";); - TRACE("grobner_stats", print_stats(tout);); - return false; -} - -void grobner::set_gb_exhausted(){ +void grobner_core::set_gb_exhausted(){ m_nl_gb_exhausted = true; } - -void grobner:: del_equations(unsigned old_size) { +void grobner_core::del_equations(unsigned old_size) { TRACE("grobner", ); SASSERT(m_equations_to_delete.size() >= old_size); equation_vector::iterator it = m_equations_to_delete.begin(); @@ -731,53 +740,36 @@ void grobner:: del_equations(unsigned old_size) { m_equations_to_delete.shrink(old_size); } -std::ostream& grobner::print_stats(std::ostream & out) const { +std::ostream& grobner_core::print_stats(std::ostream & out) const { return out << "stats:\nsteps = " << m_stats.m_compute_steps << "\nsimplified: " << m_stats.m_simplified << "\nsuperposed: " << m_stats.m_superposed << "\nexpr degree: " << m_stats.m_max_expr_degree << "\nexpr size: " << m_stats.m_max_expr_size << "\n"; } -void grobner::update_stats_max_degree_and_size(const equation *e) { +void grobner_core::update_stats_max_degree_and_size(const equation *e) { m_stats.m_max_expr_size = std::max(m_stats.m_max_expr_size, e->expr()->size()); m_stats.m_max_expr_degree = std::max(m_stats.m_max_expr_degree, e->expr()->get_degree()); } -void grobner::display_equations(std::ostream & out, equation_set const & v, char const * header) const { +void grobner_core::display_equations(std::ostream & out, equation_set const & v, char const * header) const { out << header << "\n"; for (const equation* e : v) display_equation(out, *e); } -std::ostream& grobner::display_equation(std::ostream & out, const equation & eq) const { +std::ostream& grobner_core::display_equation(std::ostream & out, const equation & eq) const { out << "expr = " << *eq.expr() << "\n"; - display_dependency(out, eq.dep()); + return display_dependency(out, eq.dep()); +} + +std::ostream& grobner_core::display(std::ostream& out) const { + display_equations(out, m_to_superpose, "m_to_superpose:"); + display_equations(out, m_to_simplify, "m_to_simplify:"); return out; } -std::unordered_set grobner::get_vars_of_expr_with_opening_terms(const nex *e ) { - auto ret = get_vars_of_expr(e); - auto & ls = c().m_lar_solver; - do { - svector added; - for (lpvar j : ret) { - if (ls.column_corresponds_to_term(j)) { - const auto & t = c().m_lar_solver.get_term(ls.local_to_external(j)); - for (auto p : t) { - if (ret.find(p.var()) == ret.end()) - added.push_back(p.var()); - } - } - } - if (added.size() == 0) - return ret; - for (lpvar j: added) - ret.insert(j); - added.clear(); - } while (true); -} - -void grobner::assert_eq_0(nex* e, ci_dependency * dep) { +void grobner_core::assert_eq_0(nex* e, common::ci_dependency * dep) { if (e == nullptr || is_zero_scalar(e)) return; m_tmp_var_set.clear(); @@ -785,14 +777,14 @@ void grobner::assert_eq_0(nex* e, ci_dependency * dep) { init_equation(eq, e, dep); TRACE("grobner", display_equation(tout, *eq); - tout << "\nvars\n"; + /*tout << "\nvars\n"; for (unsigned j : get_vars_of_expr_with_opening_terms(e)) { c().print_var(j, tout << "(") << ")\n"; - }); + } */); insert_to_simplify(eq); } -void grobner::init_equation(equation* eq, nex*e, ci_dependency * dep) { +void grobner_core::init_equation(equation* eq, nex*e, common::ci_dependency * dep) { eq->m_bidx = m_equations_to_delete.size(); eq->dep() = dep; eq->expr() = e; @@ -800,17 +792,17 @@ void grobner::init_equation(equation* eq, nex*e, ci_dependency * dep) { SASSERT(m_equations_to_delete[eq->m_bidx] == eq); } -grobner::~grobner() { +grobner_core::~grobner_core() { del_equations(0); } -std::ostream& grobner::display_dependency(std::ostream& out, ci_dependency* dep) const { +std::ostream& grobner_core::display_dependency(std::ostream& out, common::ci_dependency* dep) const { svector expl; m_dep_manager.linearize(dep, expl); lp::explanation e(expl); if (!expl.empty()) { out << "constraints\n"; - m_core->print_explanation(e, out); + m_print_explanation(e, out); out << "\n"; } else { out << "no deps\n"; @@ -818,17 +810,17 @@ std::ostream& grobner::display_dependency(std::ostream& out, ci_dependency* dep) return out; } #ifdef Z3DEBUG -bool grobner::test_find_b(const nex* ab, const nex_mul* b) { +bool grobner_core::test_find_b(const nex* ab, const nex_mul* b) { nex_mul& ab_clone = m_nex_creator.clone(ab)->to_mul(); - nex_mul * a= divide_ignore_coeffs_perform(&ab_clone, b); - ab_clone.coeff() = rational(1); + nex_mul * a= divide_ignore_coeffs_perform(&ab_clone, *b); + ab_clone.m_coeff = rational(1); SASSERT(b->coeff().is_one()); nex * m = m_nex_creator.mk_mul(a, m_nex_creator.clone(b)); m = m_nex_creator.simplify(m); return m_nex_creator.equal(m, &ab_clone); } -bool grobner::test_find_b_c(const nex* ab, const nex* ac, const nex_mul* b, const nex_mul* c) { +bool grobner_core::test_find_b_c(const nex* ab, const nex* ac, const nex_mul* b, const nex_mul* c) { return test_find_b(ab, b) && test_find_b(ac, c); } diff --git a/src/math/lp/nla_grobner.h b/src/math/lp/nla_grobner.h index 575cb5be0..0b04b032a 100644 --- a/src/math/lp/nla_grobner.h +++ b/src/math/lp/nla_grobner.h @@ -22,7 +22,6 @@ #include "math/lp/nla_common.h" #include "math/lp/nex.h" #include "math/lp/nex_creator.h" -//#include "util/dependency.h" namespace nla { class core; @@ -37,11 +36,12 @@ struct grobner_stats { grobner_stats() { reset(); } }; -class grobner : common { +class grobner_core { +public: class equation { unsigned m_bidx; //!< position at m_equations_to_delete nex * m_expr; // simplified expressionted monomials - ci_dependency * m_dep; //!< justification for the equality + common::ci_dependency * m_dep; //!< justification for the equality public: unsigned get_num_monomials() const { switch(m_expr->type()) { @@ -67,18 +67,21 @@ class grobner : common { } nex* & expr() { return m_expr; } const nex* expr() const { return m_expr; } - ci_dependency * dep() const { return m_dep; } - ci_dependency *& dep() { return m_dep; } + common::ci_dependency * dep() const { return m_dep; } + common::ci_dependency *& dep() { return m_dep; } unsigned hash() const { return m_bidx; } friend class grobner; + friend class grobner_core; }; - +private: typedef obj_hashtable equation_set; typedef ptr_vector equation_vector; - + typedef std::function print_expl_t; // fields + nex_creator& m_nex_creator; + reslimit& m_limit; + print_expl_t m_print_explanation; equation_vector m_equations_to_delete; - lp::int_set m_rows; grobner_stats m_stats; equation_set m_to_superpose; equation_set m_to_simplify; @@ -86,34 +89,46 @@ class grobner : common { ptr_vector m_allocated; lp::int_set m_tmp_var_set; region m_alloc; - ci_value_manager m_val_manager; - mutable ci_dependency_manager m_dep_manager; + common::ci_value_manager m_val_manager; + mutable common::ci_dependency_manager m_dep_manager; nex_lt m_lt; bool m_changed_leading_term; - unsigned m_reported; - bool m_look_for_fixed_vars_in_rows; + equation_set m_all_eqs; + unsigned m_grobner_eqs_threshold; public: - grobner(core *, intervals *); - void grobner_lemmas(); - ~grobner(); -private: - void find_nl_cluster(); - void prepare_rows_and_active_vars(); - void add_var_and_its_factors_to_q_and_collect_new_rows(lpvar j, std::queue& q); - void init(); - void compute_basis(); - void compute_basis_init(); + grobner_core(nex_creator& nc, reslimit& lim, unsigned eqs_threshold) : + m_nex_creator(nc), + m_limit(lim), + m_nl_gb_exhausted(false), + m_dep_manager(m_val_manager, m_alloc), + m_changed_leading_term(false), + m_grobner_eqs_threshold(eqs_threshold) + {} + + ~grobner_core(); + void reset(); bool compute_basis_loop(); + void assert_eq_0(nex*, common::ci_dependency * dep); + equation_set const& equations(); + common::ci_dependency_manager& dep() const { return m_dep_manager; } + + void display_equations(std::ostream& out, equation_set const& v, char const* header) const; + std::ostream& display_equation(std::ostream& out, const equation& eq) const; + std::ostream& display(std::ostream& out) const; + + void operator=(print_expl_t& pe) { m_print_explanation = pe; } + +private: bool compute_basis_step(); bool simplify_source_target(equation * source, equation * target); - equation* simplify_using_to_superpose(equation*); + void simplify_using_to_superpose(equation &); bool simplify_target_monomials(equation * source, equation * target); void process_simplified_target(equation* target, ptr_buffer& to_remove); bool simplify_to_superpose_with_eq(equation*); void simplify_m_to_simplify(equation*); equation* pick_next(); void set_gb_exhausted(); - bool canceled() const; + bool canceled(); void superpose(equation * eq1, equation * eq2); void superpose(equation * eq); bool find_b_c(const nex *ab, const nex* ac, nex_mul*& b, nex_mul*& c); @@ -122,42 +137,29 @@ private: bool is_simpler(equation * eq1, equation * eq2); void del_equations(unsigned old_size); void del_equation(equation * eq); - void display_equations(std::ostream & out, equation_set const & v, char const * header) const; - std::ostream& display_equation(std::ostream & out, const equation & eq) const; - - void display_matrix(std::ostream & out) const; - std::ostream& display(std::ostream & out) const; - bool internalize_gb_eq(equation*); - void add_row(unsigned); - void assert_eq_0(nex*, ci_dependency * dep); - void init_equation(equation* eq, nex*, ci_dependency* d); + void init_equation(equation* eq, nex*, common::ci_dependency* d); - std::ostream& display_dependency(std::ostream& out, ci_dependency*) const; + std::ostream& display_dependency(std::ostream& out, common::ci_dependency*) const; void insert_to_simplify(equation *eq) { - TRACE("nla_grobner", display_equation(tout, *eq);); + TRACE("grobner", display_equation(tout, *eq);); m_to_simplify.insert(eq); } void insert_to_superpose(equation *eq) { SASSERT(m_nex_creator.is_simplified(*eq->expr())); - TRACE("nla_grobner", display_equation(tout, *eq);); + TRACE("grobner", display_equation(tout, *eq);); m_to_superpose.insert(eq); } - void simplify_equations_in_m_to_simplify(); const nex * get_highest_monomial(const nex * e) const; - ci_dependency* dep_from_vector(svector & fixed_vars_constraints); - bool simplify_target_monomials_sum(equation *, equation *, nex_sum*, const nex*); - unsigned find_divisible(nex_sum*, const nex*) const; - void simplify_target_monomials_sum_j(equation *, equation *, nex_sum*, const nex*, unsigned, bool); - bool divide_ignore_coeffs_check_only(nex* , const nex*) const; - bool divide_ignore_coeffs_check_only_nex_mul(nex_mul* , const nex*) const; - nex_mul * divide_ignore_coeffs_perform(nex* , const nex*); - nex_mul * divide_ignore_coeffs_perform_nex_mul(nex_mul* , const nex*); + bool simplify_target_monomials_sum(equation *, equation *, nex_sum*, const nex&); + unsigned find_divisible(nex_sum const&, const nex&) const; + void simplify_target_monomials_sum_j(equation *, equation *, nex_sum*, const nex&, unsigned, bool); + bool divide_ignore_coeffs_check_only(nex const* , const nex&) const; + bool divide_ignore_coeffs_check_only_nex_mul(nex_mul const&, nex const&) const; + nex_mul * divide_ignore_coeffs_perform(nex* , const nex&); + nex_mul * divide_ignore_coeffs_perform_nex_mul(nex_mul const& , const nex&); nex * expr_superpose(nex* e1, nex* e2, const nex* ab, const nex* ac, nex_mul* b, nex_mul* c); - void add_mul_skip_first(nex_sum* r, const rational& beta, nex *e, nex_mul* c); - bool done() const; - void check_eq(equation*); - void register_report(); - std::unordered_set get_vars_of_expr_with_opening_terms(const nex *e ); + void add_mul_skip_first(nex_creator::sum_factory& sf, const rational& beta, nex *e, nex_mul* c); + bool done(); unsigned num_of_equations() const { return m_to_simplify.size() + m_to_superpose.size(); } std::ostream& print_stats(std::ostream&) const; void update_stats_max_degree_and_size(const equation*); @@ -165,5 +167,30 @@ private: bool test_find_b_c(const nex* ab, const nex* ac, const nex_mul* b, const nex_mul* c); bool test_find_b(const nex* ab, const nex_mul* b); #endif +}; + +class grobner : common { + grobner_core m_gc; + unsigned m_reported; + lp::int_set m_rows; + bool m_look_for_fixed_vars_in_rows; +public: + grobner(core *, intervals *); + void grobner_lemmas(); + ~grobner() {} +private: + void find_nl_cluster(); + void prepare_rows_and_active_vars(); + void add_var_and_its_factors_to_q_and_collect_new_rows(lpvar j, svector& q); + void init(); + void compute_basis(); + void compute_basis_init(); + std::unordered_set grobner::get_vars_of_expr_with_opening_terms(const nex* e); + void display_matrix(std::ostream & out) const; + std::ostream& display(std::ostream& out) const { return m_gc.display(out); } + void add_row(unsigned); + void check_eq(grobner_core::equation*); + void register_report(); + }; // end of grobner } diff --git a/src/math/lp/nla_intervals.cpp b/src/math/lp/nla_intervals.cpp index 73df2ab9b..8e1ef40d2 100644 --- a/src/math/lp/nla_intervals.cpp +++ b/src/math/lp/nla_intervals.cpp @@ -129,7 +129,7 @@ intervals::interv intervals::interval_of_expr(const nex* e, unsigned power) { } const nex* intervals::get_inf_interval_child(const nex_sum* e) const { - for (auto * c : e->children()) { + for (auto * c : *e) { if (has_inf_interval(c)) return c; } @@ -138,7 +138,7 @@ const nex* intervals::get_inf_interval_child(const nex_sum* e) const { bool intervals::mul_has_inf_interval(const nex_mul* e) const { bool has_inf = false; - for (const auto & p : e->children()) { + for (const auto & p : *e) { const nex *c = p.e(); if (!c->is_elementary()) return false; @@ -157,7 +157,7 @@ bool intervals::has_inf_interval(const nex* e) const { } if (e->is_scalar()) return false; - for (auto * c : to_sum(e)->children()) { + for (auto * c : e->to_sum()) { if (has_inf_interval(c)) return true; } @@ -166,13 +166,11 @@ bool intervals::has_inf_interval(const nex* e) const { bool intervals::has_zero_interval(const nex* e) const { SASSERT(!e->is_scalar() || !to_scalar(e)->value().is_zero()); - if (! e->is_var()) - return false; - return m_core->var_is_fixed_to_zero(to_var(e)->var()); + return e->is_var() && m_core->var_is_fixed_to_zero(e->to_var().var()); } const nex* intervals::get_zero_interval_child(const nex_mul* e) const { - for (const auto & p : e->children()) { + for (const auto & p : *e) { const nex * c = p.e(); if (has_zero_interval(c)) return c; @@ -279,7 +277,7 @@ intervals::interv intervals::interval_of_sum_no_term_with_deps(const nex_sum* e) if (inf_e) { return interv(); } - auto & es = e->children(); + auto & es = *e; interv a = interval_of_expr_with_deps(es[0], 1); for (unsigned k = 1; k < es.size(); k++) { TRACE("nla_intervals_details_sum", tout << "es[" << k << "]= " << *es[k] << "\n";); @@ -303,7 +301,7 @@ intervals::interv intervals::interval_of_sum_no_term(const nex_sum* e) { if (inf_e) { return interv(); } - auto & es = e->children(); + auto & es = *e; interv a = interval_of_expr(es[0], 1); for (unsigned k = 1; k < es.size(); k++) { TRACE("nla_intervals_details_sum", tout << "es[" << k << "]= " << *es[k] << "\n";); @@ -351,7 +349,7 @@ lp::lar_term intervals::expression_to_normalized_term(const nex_sum* e, rational vector> v; b = rational(0); unsigned a_index; - for (const nex* c : e->children()) { + for (const nex* c : *e) { if (c->is_scalar()) { b += to_scalar(c)->value(); } else {