From 27a27f16ffc9432e6ad19d07dca5e1e4ce63ee6c Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 24 Sep 2019 12:04:13 -0700 Subject: [PATCH] change the representatition of nex_mul to use nex_pow Signed-off-by: Lev Nachmanson --- src/math/lp/CMakeLists.txt | 1 + src/math/lp/cross_nested.h | 25 ++--- src/math/lp/horner.cpp | 27 +++--- src/math/lp/nex.h | 182 +++++++++++++------------------------ src/math/lp/nex_creator.h | 20 ++-- src/math/lp/nla_grobner.h | 2 +- src/test/lp/lp.cpp | 17 ++++ 7 files changed, 125 insertions(+), 149 deletions(-) diff --git a/src/math/lp/CMakeLists.txt b/src/math/lp/CMakeLists.txt index eb6e36d7d..e9d6be0ad 100644 --- a/src/math/lp/CMakeLists.txt +++ b/src/math/lp/CMakeLists.txt @@ -26,6 +26,7 @@ z3_add_component(lp lp_utils.cpp matrix.cpp mon_eq.cpp + nex.cpp nla_basics_lemmas.cpp nla_common.cpp nla_core.cpp diff --git a/src/math/lp/cross_nested.h b/src/math/lp/cross_nested.h index 500e909b9..bf2a26ef2 100644 --- a/src/math/lp/cross_nested.h +++ b/src/math/lp/cross_nested.h @@ -125,10 +125,10 @@ public: nex* c_over_f = m_nex_creator.mk_div(*c, f); to_sum(c_over_f)->simplify(&c_over_f); - *c = m_nex_creator.mk_mul(f, c_over_f); + nex_mul* cm; + *c = cm = m_nex_creator.mk_mul(f, c_over_f); TRACE("nla_cn", tout << "common factor=" << *f << ", c=" << **c << "\ne = " << *m_e << "\n";); - - explore_expr_on_front_elem(&(*((*c)->children_ptr()))[1], front); + explore_expr_on_front_elem(cm->children()[1].ee(), front); return true; } @@ -405,7 +405,7 @@ public: 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)->children()[0]))->children()[1]; + nex **ptr_to_a = (to_mul(to_sum(e)->children()[0]))->children()[1].ee(); push_to_front(front, ptr_to_a); } @@ -419,7 +419,7 @@ public: if (b == nullptr) { e = m_nex_creator.mk_mul(m_nex_creator.mk_var(j), a); if (!to_sum(a)->is_linear()) - push_to_front(front, &(to_mul(e)->children()[1])); + push_to_front(front, to_mul(e)->children()[1].ee()); } else { update_front_with_split_with_non_empty_b(e, j, front, a, b); } @@ -458,8 +458,8 @@ public: } case expr_type::MUL: { - for (auto c: to_mul(e)->children()) - for ( lpvar j : get_vars_of_expr(c)) + for (auto &c: to_mul(e)->children()) + for ( lpvar j : get_vars_of_expr(c.e())) r.insert(j); } return r; @@ -479,7 +479,7 @@ public: bool done() const { return m_done; } #if Z3DEBUG - nex *clone (nex * a) { + nex *clone (const nex * a) { switch (a->type()) { case expr_type::VAR: { auto v = to_var(a); @@ -493,8 +493,8 @@ public: case expr_type::MUL: { auto m = to_mul(a); auto r = m_nex_creator.mk_mul(); - for (nex * e : m->children()) { - r->add_child(clone(e)); + for (const auto& p : m->children()) { + r->add_child_in_power(clone(p.e()), p.pow()); } return r; } @@ -524,6 +524,9 @@ public: nex * normalize_mul(nex_mul* a) { 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]); @@ -554,7 +557,7 @@ public: nex *rs = normalize_sum(r); SASSERT(rs->is_simplified()); return rs; - + */ } diff --git a/src/math/lp/horner.cpp b/src/math/lp/horner.cpp index ea78ab9ee..0119db847 100644 --- a/src/math/lp/horner.cpp +++ b/src/math/lp/horner.cpp @@ -193,11 +193,11 @@ interv horner::interval_of_mul_with_deps(const nex_mul* e) { SASSERT(e->is_mul()); auto & es = to_mul(e)->children(); - interv a = interval_of_expr_with_deps(es[0]); - TRACE("nla_horner_details", tout << "es[0]= "<< *es[0] << std::endl << "a = "; m_intervals.display(tout, a); ); + interv a = interval_of_expr_with_deps(es[0].e()); + TRACE("nla_horner_details", tout << "es[0]= "<< es[0] << std::endl << "a = "; m_intervals.display(tout, a); ); for (unsigned k = 1; k < es.size(); k++) { - interv b = interval_of_expr_with_deps(es[k]); - TRACE("nla_horner_details", tout << "es[" << k << "] "<< *es[k] << ", "; m_intervals.display(tout, b); ); + interv b = interval_of_expr_with_deps(es[k].e()); + TRACE("nla_horner_details", tout << "es[" << k << "] "<< es[k] << ", "; m_intervals.display(tout, b); ); interv c; interval_deps_combine_rule comb_rule; m_intervals.mul(a, b, c, comb_rule); @@ -224,11 +224,11 @@ interv horner::interval_of_mul(const nex_mul* e) { SASSERT(e->is_mul()); auto & es = to_mul(e)->children(); - interv a = interval_of_expr(es[0]); - TRACE("nla_horner_details", tout << "es[0]= "<< *es[0] << std::endl << "a = "; m_intervals.display(tout, a); ); + interv a = interval_of_expr(es[0].e()); + TRACE("nla_horner_details", tout << "es[0]= "<< es[0] << std::endl << "a = "; m_intervals.display(tout, a); ); for (unsigned k = 1; k < es.size(); k++) { - interv b = interval_of_expr(es[k]); - TRACE("nla_horner_details", tout << "es[" << k << "] "<< *es[k] << ", "; m_intervals.display(tout, b); ); + interv b = interval_of_expr(es[k].e()); + TRACE("nla_horner_details", tout << "es[" << k << "] "<< es[k] << ", "; m_intervals.display(tout, b); ); interv c; interval_deps_combine_rule comb_rule; m_intervals.mul(a, b, c, comb_rule); @@ -249,12 +249,13 @@ void horner::add_mul_to_vector(const nex_mul* e, vectorsize() > 0); if (e->size() == 1) { - add_linear_to_vector(*(e->children().begin()), v); + add_linear_to_vector(e->children().begin()->e(), v); return; } rational r; lpvar j = -1; - for (const nex * c : e->children()) { + for (const auto & p: e->children()) { + const nex * c = p.e(); switch (c->type()) { case expr_type::SCALAR: r = to_scalar(c)->value(); @@ -331,7 +332,8 @@ lp::lar_term horner::expression_to_normalized_term(const nex_sum* e, rational& a bool horner::mul_has_inf_interval(const nex_mul* e) const { bool has_inf = false; - for (const nex *c : e->children()) { + for (const auto & p : e->children()) { + const nex *c = p.e(); if (!c->is_elementary()) return false; if (has_zero_interval(c)) @@ -364,7 +366,8 @@ bool horner::has_zero_interval(const nex* e) const { } const nex* horner::get_zero_interval_child(const nex_mul* e) const { - for (auto * c : e->children()) { + for (const auto & p : e->children()) { + const nex * c = p.e(); if (has_zero_interval(c)) return c; } diff --git a/src/math/lp/nex.h b/src/math/lp/nex.h index f8b123ada..f3d29f9d0 100644 --- a/src/math/lp/nex.h +++ b/src/math/lp/nex.h @@ -43,7 +43,7 @@ inline std::ostream & operator<<(std::ostream& out, expr_type t) { } -// This class is needed in horner calculation with intervals +// This is the class of non-linear expressions class nex { public: virtual expr_type type() const = 0; @@ -72,14 +72,6 @@ public: virtual bool is_simplified() const { return true; } - virtual const ptr_vector * children_ptr() const { - UNREACHABLE(); - return nullptr; - } - virtual ptr_vector * children_ptr() { - UNREACHABLE(); - return nullptr; - } #ifdef Z3DEBUG virtual void sort() {}; #endif @@ -132,7 +124,8 @@ public: }; const nex_scalar * to_scalar(const nex* a); - +class nex_sum; +const nex_sum* to_sum(const nex*a); static bool ignored_child(nex* e, expr_type t) { switch(t) { case expr_type::MUL: @@ -144,77 +137,60 @@ static bool ignored_child(nex* e, expr_type t) { return false; } -static void promote_children_by_type(ptr_vector * children, expr_type t) { - ptr_vector to_promote; - int skipped = 0; - for(unsigned j = 0; j < children->size(); j++) { - nex** e = &(*children)[j]; - (*e)->simplify(e); - if ((*e)->type() == t) { - to_promote.push_back(*e); - } else if (ignored_child(*e, t)) { - skipped ++; - continue; - } else { - unsigned offset = to_promote.size() + skipped; - if (offset) { - (*children)[j - offset] = *e; - } - } - } - - children->shrink(children->size() - to_promote.size() - skipped); - - for (nex *e : to_promote) { - for (nex *ee : *(e->children_ptr())) { - if (!ignored_child(ee, t)) - children->push_back(ee); - } - } -} +void promote_children_of_sum(ptr_vector & children); +class nex_pow; +void promote_children_of_mul(vector & children); + +class nex_pow { + nex* m_e; + int m_power; +public: + explicit nex_pow(nex* e): m_e(e), m_power(1) {} + explicit nex_pow(nex* e, int p): m_e(e), m_power(p) {} + const nex * e() const { return m_e; } + nex * e() { return m_e; } + nex ** ee() { return & m_e; } + int pow() const { return m_power; } + int& pow() { return m_power; } + std::string to_string() const { std::stringstream s; s << "(" << *e() << ", " << pow() << ")"; + return s.str(); } + friend std::ostream& operator<<(std::ostream& out, const nex_pow & p) { out << p.to_string(); return out; } +}; class nex_mul : public nex { - ptr_vector m_children; + vector m_children; public: nex_mul() {} unsigned size() const { return m_children.size(); } expr_type type() const { return expr_type::MUL; } - ptr_vector& children() { return m_children;} - const ptr_vector& children() const { return m_children;} - const ptr_vector* children_ptr() const { return &m_children;} - ptr_vector* children_ptr() { return &m_children;} + 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]->is_scalar()); } + bool is_pure_monomial() const { return size() == 0 || (!m_children[0].e()->is_scalar()); } std::ostream & print(std::ostream& out) const { + bool first = true; - for (const nex* v : m_children) { - std::string s = v->str(); + for (const nex_pow& v : m_children) { + std::string s = v.to_string(); if (first) { first = false; - if (v->is_elementary()) - out << s; - else - out << "(" << s << ")"; + out << s; } else { - if (v->is_elementary()) { - if (s[0] == '-') { - out << "*(" << s << ")"; - } else { - out << "*" << s; - } - } else { - out << "*(" << s << ")"; - } + out << "*" << s; } } return out; } - void add_child(nex* e) { m_children.push_back(e); } + void add_child(nex* e) { + add_child_in_power(e, 1); + } + + void add_child_in_power(nex* e, int power) { m_children.push_back(nex_pow(e, power)); } bool contains(lpvar j) const { - for (const nex* c : children()) { - if (c->contains(j)) + for (const nex_pow& c : children()) { + if (c.e()->contains(j)) return true; } return false; @@ -228,34 +204,32 @@ public: void get_powers_from_mul(std::unordered_map & r) const { r.clear(); for (const auto & c : children()) { - if (!c->is_var()) { + if (!c.e()->is_var()) { continue; } - lpvar j = to_var(c)->var(); - auto it = r.find(j); - if (it == r.end()) { - r[j] = 1; - } else { - it->second++; - } + lpvar j = to_var(c.e())->var(); + SASSERT(r.find(j) == r.end()); + r[j] = c.pow(); } TRACE("nla_cn_details", tout << "powers of " << *this << "\n"; print_vector(r, tout)<< "\n";); } int get_degree() const { int degree = 0; - for (auto e : children()) { - degree += e->get_degree(); + for (const auto& p : children()) { + degree += p.e()->get_degree() * p.pow(); } return degree; } void simplify(nex **e) { + TRACE("nla_cn_details", tout << *this << "\n";); + TRACE("nla_cn_details", tout << "**e = " << **e << "\n";); *e = this; TRACE("nla_cn_details", tout << *this << "\n";); - promote_children_by_type(&m_children, expr_type::MUL); - if (size() == 1) - *e = m_children[0]; + promote_children_of_mul(m_children); + if (size() == 1 && m_children[0].pow() == 1) + *e = m_children[0].e(); TRACE("nla_cn_details", tout << *this << "\n";); SASSERT((*e)->is_simplified()); } @@ -263,7 +237,8 @@ public: virtual bool is_simplified() const { if (size() < 2) return false; - for (nex * e : children()) { + for (const auto &p : children()) { + const nex* e = p.e(); if (e->is_mul()) return false; if (e->is_scalar() && to_scalar(e)->value().is_one()) @@ -274,25 +249,17 @@ public: bool is_linear() const { SASSERT(is_simplified()); - if (children().size() > 2) - return false; - - SASSERT(children().size() == 2); - for (auto e : children()) { - if (e->is_scalar()) - return true; - } - return false; + return get_degree() < 2; // todo: make it more efficient } -#ifdef Z3DEBUG - virtual void sort() { - for (nex * c : m_children) { - c->sort(); - } - std::sort(m_children.begin(), m_children.end(), [](const nex* a, const nex* b) { return *a < *b; }); - } - #endif +// #ifdef Z3DEBUG +// virtual void sort() { +// for (nex * c : m_children) { +// c->sort(); +// } +// std::sort(m_children.begin(), m_children.end(), [](const nex* a, const nex* b) { return *a < *b; }); +// } +// #endif }; @@ -361,7 +328,7 @@ public: void simplify(nex **e) { *e = this; - promote_children_by_type(&m_children, expr_type::SUM); + promote_children_of_sum(m_children); if (size() == 1) *e = m_children[0]; } @@ -387,12 +354,15 @@ public: void add_child(nex* e) { m_children.push_back(e); } #ifdef Z3DEBUG virtual void sort() { + NOT_IMPLEMENTED_YET(); + /* for (nex * c : m_children) { c->sort(); } std::sort(m_children.begin(), m_children.end(), [](const nex* a, const nex* b) { return *a < *b; }); + */ } #endif }; @@ -449,30 +419,6 @@ inline bool operator<(const ptr_vector&a , const ptr_vector& b) { return false; } -inline bool operator<(const nex& a , const nex& b) { - int r = (int)(a.type()) - (int)(b.type()); - ptr_vector ch; - if (r) { - return r < 0; - } - switch (a.type()) { - case expr_type::VAR: { - return to_var(&a)->var() < to_var(&b)->var(); - } - case expr_type::SCALAR: { - return to_scalar(&a)->value() < to_scalar(&b)->value(); - } - case expr_type::MUL: { - return to_mul(&a)->children() < to_mul(&b)->children(); - } - case expr_type::SUM: { - return to_sum(&a)->children() < to_sum(&b)->children(); - } - default: - SASSERT(false); - return false; - } -} #endif } diff --git a/src/math/lp/nex_creator.h b/src/math/lp/nex_creator.h index 1d8330639..f2c6ebbf7 100644 --- a/src/math/lp/nex_creator.h +++ b/src/math/lp/nex_creator.h @@ -84,7 +84,7 @@ public: return r; } - nex_mul* mk_mul(const ptr_vector& v) { + nex_mul* mk_mul(const vector& v) { auto r = new nex_mul(); add_to_allocated(r); r->children() = v; @@ -129,10 +129,13 @@ public: nex * mk_div(const nex* a, lpvar j) { TRACE("nla_cn_details", tout << "a=" << *a << ", v" << j << "\n";); + NOT_IMPLEMENTED_YET(); + return nullptr; + /* SASSERT((a->is_mul() && a->contains(j)) || (a->is_var() && to_var(a)->var() == j)); if (a->is_var()) return mk_scalar(rational(1)); - ptr_vector bv; + ptr_vector bv; bool seenj = false; for (nex* c : to_mul(a)->children()) { if (!seenj) { @@ -153,11 +156,11 @@ public: } SASSERT(bv.size() == 0); - return mk_scalar(rational(1)); + return mk_scalar(rational(1));*/ } nex * mk_div(const nex* a, const nex* b) { - TRACE("nla_cn_details", tout << *a <<" / " << *b << "\n";); + TRACE("nla_cn_details", tout <<"(" << *a << ") / (" << *b << ")\n";); if (b->is_var()) { return mk_div(a, to_var(b)->var()); } @@ -176,15 +179,18 @@ public: return mk_scalar(rational(1)); } SASSERT(a->is_mul()); + const nex_mul* am = to_mul(a); bm->get_powers_from_mul(m_powers); + TRACE("nla_cn_details", print_vector(m_powers, tout);); nex_mul* ret = new nex_mul(); - for (auto e : am->children()) { + for (const nex_pow& p : am->children()) { + const nex *e = p.e(); TRACE("nla_cn_details", tout << "e=" << *e << "\n";); if (!e->is_var()) { SASSERT(e->is_scalar()); - ret->add_child(e); + ret->add_child(mk_scalar(to_scalar(e)->value())); TRACE("nla_cn_details", tout << "continue\n";); continue; } @@ -192,7 +198,7 @@ public: lpvar j = to_var(e)->var(); auto it = m_powers.find(j); if (it == m_powers.end()) { - ret->add_child(e); + ret->add_child(mk_var(j)); } else { it->second --; if (it->second == 0) diff --git a/src/math/lp/nla_grobner.h b/src/math/lp/nla_grobner.h index 8f5050ba3..8e9431e4c 100644 --- a/src/math/lp/nla_grobner.h +++ b/src/math/lp/nla_grobner.h @@ -151,7 +151,7 @@ private: nex* mk_monomial_in_row(rational, lpvar, ci_dependency*&); rational get_monomial_coeff(const nex_mul* m) { - const nex* a = m->children()[0]; + const nex* a = m->children()[0].e(); if (a->is_scalar()) return static_cast(a)->value(); return rational(1); diff --git a/src/test/lp/lp.cpp b/src/test/lp/lp.cpp index 3f052d548..44514dafc 100644 --- a/src/test/lp/lp.cpp +++ b/src/test/lp/lp.cpp @@ -73,6 +73,22 @@ void test_cn_on_expr(nex_sum *t, cross_nested& cn) { cn.run(t); } +void test_simplify(cross_nested& cn, nex_var* a, nex_var* b, nex_var* c) { + auto & r = cn.get_nex_creator(); + auto m = r.mk_mul(); m->add_child_in_power(c, 2); + TRACE("nla_cn", tout << "m = " << *m << "\n";); + auto n = r.mk_mul(a); + n->add_child_in_power(b, 7); + TRACE("nla_cn", tout << "n = " << *n << "\n";); + m->add_child_in_power(n, 3); + TRACE("nla_cn", tout << "m = " << *m << "\n";); + + nex * e = r.mk_sum(a, r.mk_sum(b, m)); + TRACE("nla_cn", tout << "e = " << *e << "\n";); + e->simplify(&e); + TRACE("nla_cn", tout << "simplified e = " << *e << "\n";); +} + void test_cn() { cross_nested cn( [](const nex* n) { @@ -91,6 +107,7 @@ void test_cn() { nex_var* e = cn.get_nex_creator().mk_var(4); nex_var* g = cn.get_nex_creator().mk_var(6); nex* min_1 = cn.get_nex_creator().mk_scalar(rational(-1)); + test_simplify(cn, a, b, c); // test_cn_on_expr(min_1*c*e + min_1*b*d + min_1*a*b + a*c); nex* bcd = cn.get_nex_creator().mk_mul(b, c, d); nex_mul* bcg = cn.get_nex_creator().mk_mul(b, c, g);