From 090851559bd694a60b0530bfc017a6f5aa1fe526 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Fri, 27 Sep 2019 17:55:33 -0700 Subject: [PATCH] move sorting of nex expressions to nex_creator Signed-off-by: Lev Nachmanson --- src/math/lp/CMakeLists.txt | 2 +- src/math/lp/cross_nested.h | 6 +- src/math/lp/horner.cpp | 4 +- src/math/lp/nex.cpp | 198 ----------------------------------- src/math/lp/nex.h | 87 +--------------- src/math/lp/nex_creator.h | 201 ++++++++++++++++++------------------ src/math/lp/nla_grobner.cpp | 7 +- src/math/lp/nla_grobner.h | 40 +++---- src/test/lp/lp.cpp | 18 ++-- 9 files changed, 134 insertions(+), 429 deletions(-) delete mode 100644 src/math/lp/nex.cpp diff --git a/src/math/lp/CMakeLists.txt b/src/math/lp/CMakeLists.txt index e9d6be0ad..8d3c3a31e 100644 --- a/src/math/lp/CMakeLists.txt +++ b/src/math/lp/CMakeLists.txt @@ -26,7 +26,7 @@ z3_add_component(lp lp_utils.cpp matrix.cpp mon_eq.cpp - nex.cpp + nex_creator.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 2b47bbdfb..6f8139ac9 100644 --- a/src/math/lp/cross_nested.h +++ b/src/math/lp/cross_nested.h @@ -35,7 +35,7 @@ class cross_nested { int m_reported; bool m_random_bit; nex_creator m_nex_creator; - nex_lt m_lt; + const lt_on_vars& m_lt; std::function m_mk_scalar; #ifdef Z3DEBUG nex* m_e_clone; @@ -47,14 +47,12 @@ public: cross_nested(std::function call_on_result, std::function var_is_fixed, std::function random, - nex_lt lt): + lt_on_vars lt): m_call_on_result(call_on_result), m_var_is_fixed(var_is_fixed), m_random(random), m_done(false), m_reported(0), - m_nex_creator(lt), - m_lt(lt), m_mk_scalar([this]{return m_nex_creator.mk_scalar(rational(1));}) {} diff --git a/src/math/lp/horner.cpp b/src/math/lp/horner.cpp index 41aadb94d..f72206a9c 100644 --- a/src/math/lp/horner.cpp +++ b/src/math/lp/horner.cpp @@ -93,9 +93,7 @@ bool horner::lemmas_on_row(const T& row) { [this](const nex* n) { return check_cross_nested_expr(n); }, [this](unsigned j) { return c().var_is_fixed(j); }, [this]() { return c().random(); }, - [](const nex* a, const nex* b) { return - less_than_nex(a, b, [](lpvar j, lpvar k) { return j < k;}); } - ); + [](lpvar j, lpvar k) { return j < k;}); // todo : consider using weights here - the same way they are used in Grobner basis SASSERT (row_is_interesting(row)); create_sum_from_row(row, cn.get_nex_creator(), m_row_sum); diff --git a/src/math/lp/nex.cpp b/src/math/lp/nex.cpp deleted file mode 100644 index 866126870..000000000 --- a/src/math/lp/nex.cpp +++ /dev/null @@ -1,198 +0,0 @@ -/*++ - Copyright (c) 2017 Microsoft Corporation - - Module Name: - - - - Abstract: - - - - Author: - Lev Nachmanson (levnach) - - Revision History: - - - --*/ - -#include "math/lp/nex.h" -#include -namespace nla { - - -bool is_zero_scalar(nex* e) { - return e->is_scalar() && to_scalar(e)->value().is_zero(); -} - -void mul_to_powers(vector& children, nex_lt lt) { - std::map m(lt); - - for (auto & p : children) { - auto it = m.find(p.e()); - if (it == m.end()) { - m[p.e()] = p.pow(); - } else { - it->second+= p.pow(); - } - } - children.clear(); - for (auto & p : m) { - children.push_back(nex_pow(p.first, p.second)); - } - - std::sort(children.begin(), children.end(), [lt](const nex_pow& a, const nex_pow& b) { - return less_than(a, b, lt); - }); -} - -rational extract_coeff(const nex_mul* m) { - const nex* e = m->children().begin()->e(); - if (e->is_scalar()) - return to_scalar(e)->value(); - return rational(1); -} - - -bool sum_simplify_lt(const nex_mul* a, const nex_mul* b, const nex_lt& lt) { - NOT_IMPLEMENTED_YET(); -} - -// a + 3bc + 2bc => a + 5bc -void sort_join_sum(ptr_vector & children, nex_lt& lt, std::function mk_scalar) { - ptr_vector non_muls; - std::map> - m([lt](const nex_mul *a , const nex_mul *b) { return sum_simplify_lt(a, b, lt); }); - for (nex* e : children) { - SASSERT(e->is_simplified(lt)); - if (!e->is_mul()) { - non_muls.push_back(e); - } else { - nex_mul * em = to_mul(e); - rational r = extract_coeff(em); - auto it = m.find(em); - if (it == m.end()) { - m[em] = r; - } else { - it->second += r; - } - } - } - NOT_IMPLEMENTED_YET(); -} - -void simplify_children_of_sum(ptr_vector & children, nex_lt lt, std::function mk_scalar ) { - ptr_vector to_promote; - int skipped = 0; - for(unsigned j = 0; j < children.size(); j++) { - nex** e = &(children[j]); - (*e)->simplify(e, lt, mk_scalar); - if ((*e)->is_sum()) { - to_promote.push_back(*e); - } else if (is_zero_scalar(*e)) { - 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 : *(to_sum(e)->children_ptr())) { - if (!is_zero_scalar(ee)) - children.push_back(ee); - } - } - - sort_join_sum(children, lt, mk_scalar); -} - -bool eat_scalar_pow(nex_scalar *& r, nex_pow& p) { - if (!p.e()->is_scalar()) - return false; - nex_scalar *pe = to_scalar(p.e()); - if (r == nullptr) { - r = pe; - r->value() = r->value().expt(p.pow()); - } else { - r->value() *= pe->value().expt(p.pow()); - } - return true; -} - -void simplify_children_of_mul(vector & children, nex_lt lt, std::function mk_scalar) { - nex_scalar* r = nullptr; - TRACE("nla_cn_details", print_vector(children, tout);); - vector to_promote; - int skipped = 0; - for(unsigned j = 0; j < children.size(); j++) { - nex_pow& p = children[j]; - if (eat_scalar_pow(r, p)) { - skipped++; - continue; - } - (p.e())->simplify(p.ee(), lt, mk_scalar ); - if ((p.e())->is_mul()) { - to_promote.push_back(p); - } else { - unsigned offset = to_promote.size() + skipped; - if (offset) { - children[j - offset] = p; - } - } - } - - children.shrink(children.size() - to_promote.size() - skipped); - - for (nex_pow & p : to_promote) { - for (nex_pow& pp : to_mul(p.e())->children()) { - if (!eat_scalar_pow(r, pp)) - children.push_back(nex_pow(pp.e(), pp.pow() * p.pow())); - } - } - - if (r != nullptr) { - children.push_back(nex_pow(r)); - } - - mul_to_powers(children, lt); - - TRACE("nla_cn_details", print_vector(children, tout);); -} - -bool less_than_nex(const nex* a, const nex* b, lt_on_vars lt) { - int r = (int)(a->type()) - (int)(b->type()); - if (r) { - return r < 0; - } - SASSERT(a->type() == b->type()); - switch (a->type()) { - case expr_type::VAR: { - return lt(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: { - NOT_IMPLEMENTED_YET(); - return false; // to_mul(a)->children() < to_mul(b)->children(); - } - case expr_type::SUM: { - NOT_IMPLEMENTED_YET(); - return false; //to_sum(a)->children() < to_sum(b)->children(); - } - default: - SASSERT(false); - return false; - } - - return false; -} - -} diff --git a/src/math/lp/nex.h b/src/math/lp/nex.h index 2d4fc57a8..ce0a42ef1 100644 --- a/src/math/lp/nex.h +++ b/src/math/lp/nex.h @@ -79,13 +79,7 @@ public: virtual bool contains(lpvar j) const { return false; } virtual int get_degree() const = 0; // simplifies the expression and also assigns the address of "this" to *e - virtual void simplify(nex** e, nex_lt, std::function) = 0; - void simplify(nex** e, std::function mk_scalar) { return simplify(e, less_than_nex_standard, mk_scalar); } - virtual bool is_simplified(nex_lt) const { - return true; - } - - virtual bool is_simplified() const { return is_simplified(less_than_nex_standard); } + #ifdef Z3DEBUG virtual void sort() {}; @@ -116,7 +110,6 @@ public: bool contains(lpvar j) const { return j == m_j; } int get_degree() const { return 1; } bool virtual is_linear() const { return true; } - void simplify(nex** e, nex_lt, std::function) {*e = this;} }; class nex_scalar : public nex { @@ -134,18 +127,12 @@ public: int get_degree() const { return 0; } bool is_linear() const { return true; } - void simplify(nex** e, nex_lt, std::function) {*e = this;} - }; const nex_scalar * to_scalar(const nex* a); class nex_sum; const nex_sum* to_sum(const nex*a); -void simplify_children_of_sum(ptr_vector & children, nex_lt, std::function); -class nex_pow; -void simplify_children_of_mul(vector & children, nex_lt, std::function); - class nex_pow { nex* m_e; int m_power; @@ -153,7 +140,8 @@ 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 *& e() { return m_e; } + nex ** ee() { return & m_e; } int pow() const { return m_power; } int& pow() { return m_power; } @@ -169,10 +157,8 @@ public: friend std::ostream& operator<<(std::ostream& out, const nex_pow & p) { out << p.to_string(); return out; } }; +bool less_than_nex(const nex* a, const nex* b, const lt_on_vars& lt); -inline bool less_than(const nex_pow & a, const nex_pow& b, nex_lt lt) { - return (a.pow() < b.pow()) || (a.pow() == b.pow() && lt(a.e(), b.e())); -} class nex_mul : public nex { @@ -240,50 +226,6 @@ public: } return degree; } - // the second argument is the comparison less than operator - void simplify(nex **e, nex_lt lt, std::function mk_scalar) { - TRACE("nla_cn_details", tout << *this << "\n";); - TRACE("nla_cn_details", tout << "**e = " << **e << "\n";); - *e = this; - TRACE("nla_cn_details", tout << *this << "\n";); - simplify_children_of_mul(m_children, lt, mk_scalar); - if (size() == 1 && m_children[0].pow() == 1) - *e = m_children[0].e(); - TRACE("nla_cn_details", tout << *this << "\n";); - SASSERT((*e)->is_simplified(lt)); - } - - bool is_sorted(nex_lt lt) const { - for (unsigned j = 0; j < m_children.size() - 1; j++) { - if (!(less_than(m_children[j], m_children[j+1], lt))) - return false; - } - return true; - } - - virtual bool is_simplified(nex_lt lt) const { - if (size() == 1 && m_children.begin()->pow() == 1) - return false; - std::set s(lt); - for (const auto &p : children()) { - const nex* e = p.e(); - if (p.pow() == 0) - return false; - if (e->is_mul()) - return false; - if (e->is_scalar() && to_scalar(e)->value().is_one()) - return false; - - auto it = s.find(e); - if (it == s.end()) { - s.insert(e); - } else { - TRACE("nla_cn_details", tout << "not simplified " << *e << "\n";); - return false; - } - } - return is_sorted(lt); - } bool is_linear() const { // SASSERT(is_simplified()); @@ -364,24 +306,6 @@ public: return out; } - void simplify(nex **e, nex_lt lt, std::function mk_scalar) { - *e = this; - simplify_children_of_sum(m_children, lt, mk_scalar); - if (size() == 1) - *e = m_children[0]; - } - - virtual bool is_simplified() const { - if (size() < 2) return false; - for (nex * e : children()) { - if (e->is_sum()) - return false; - if (e->is_scalar() && to_scalar(e)->value().is_zero()) - return false; - } - return true; - } - int get_degree() const { int degree = 0; for (auto e : children()) { @@ -446,9 +370,6 @@ inline std::ostream& operator<<(std::ostream& out, const nex& e ) { return e.print(out); } - -bool less_than_nex(const nex* a, const nex* b, lt_on_vars lt); - 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); diff --git a/src/math/lp/nex_creator.h b/src/math/lp/nex_creator.h index c50623a8b..b2e9adec3 100644 --- a/src/math/lp/nex_creator.h +++ b/src/math/lp/nex_creator.h @@ -18,6 +18,7 @@ --*/ #pragma once +#include #include "math/lp/nex.h" namespace nla { @@ -33,17 +34,57 @@ struct occ { } }; +enum class var_weight { + FIXED = 0, + QUOTED_FIXED = 1, + BOUNDED = 2, + QUOTED_BOUNDED = 3, + NOT_FREE = 4, + QUOTED_NOT_FREE = 5, + FREE = 6, + QUOTED_FREE = 7, + MAX_DEFAULT_WEIGHT = 7 + }; -// the purpose of this class is to create nex objects, keep them, and delete them + +// the purpose of this class is to create nex objects, keep them, +// sort them, and delete them class nex_creator { - ptr_vector m_allocated; std::unordered_map m_occurences_map; std::unordered_map m_powers; - // the "less than" operator on expressions - nex_lt m_lt; + svector m_active_vars_weights; + public: + + nex* simplify(nex* e) { + NOT_IMPLEMENTED_YET(); + } + + rational extract_coeff_from_mul(const nex_mul* m); + + rational extract_coeff(const nex* ); + + bool is_simplified(const nex *e) { + NOT_IMPLEMENTED_YET(); + } + + bool less_than(lpvar j, lpvar k) const{ + unsigned wj = (unsigned)m_active_vars_weights[j]; + unsigned wk = (unsigned)m_active_vars_weights[k]; + return wj != wk ? wj < wk : j < k; + } + + bool less_than_nex(const nex* a, const nex* b) const; + + bool less_than_on_nex_pow(const nex_pow & a, const nex_pow& b) const { + return (a.pow() < b.pow()) || (a.pow() == b.pow() && less_than_nex(a.e(), b.e())); + } + + void simplify_children_of_mul(vector & children); + + nex * clone(const nex* a) { switch (a->type()) { case expr_type::VAR: { @@ -77,7 +118,7 @@ public: } return nullptr; } - nex_creator(nex_lt lt) : m_lt(lt) {} + 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; } @@ -162,104 +203,60 @@ public: return r; } - nex * mk_div(const nex* a, lpvar j) { - SASSERT(a->is_simplified(m_lt)); - TRACE("nla_cn_details", tout << "a=" << *a << ", v" << j << "\n";); - SASSERT((a->is_mul() && a->contains(j)) || (a->is_var() && to_var(a)->var() == j)); - if (a->is_var()) - return mk_scalar(rational(1)); - vector bv; - bool seenj = false; - for (auto& p : to_mul(a)->children()) { - const nex * c = p.e(); - int pow = p.pow(); - if (!seenj) { - if (c->contains(j)) { - if (!c->is_var()) { - bv.push_back(nex_pow(mk_div(c, j))); - if (pow != 1) { - bv.push_back(nex_pow(clone(c), pow)); - } - } else { - SASSERT(to_var(c)->var() == j); - if (p.pow() != 1) { - bv.push_back(nex_pow(mk_var(j), pow - 1)); - } - } - seenj = true; - } - } else { - bv.push_back(nex_pow(clone(c))); - } - } - if (bv.size() > 1) { - return mk_mul(bv); - } - if (bv.size() == 1 && bv.begin()->pow() == 1) { - return bv.begin()->e(); - } - if (bv.size() == 0) - return mk_scalar(rational(1)); - return mk_mul(bv); - } - - nex * mk_div(const nex* a, const nex* b) { - TRACE("nla_cn_details", tout <<"(" << *a << ") / (" << *b << ")\n";); - if (b->is_var()) { - return mk_div(a, to_var(b)->var()); - } - SASSERT(b->is_mul()); - const nex_mul *bm = to_mul(b); - if (a->is_sum()) { - nex_sum * r = mk_sum(); - const nex_sum * m = to_sum(a); - for (auto e : m->children()) { - r->add_child(mk_div(e, bm)); - } - TRACE("nla_cn_details", tout << *r << "\n";); - return r; - } - if (a->is_var() || (a->is_mul() && to_mul(a)->children().size() == 1)) { - 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 (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(mk_scalar(to_scalar(e)->value())); - TRACE("nla_cn_details", tout << "continue\n";); - continue; - } - SASSERT(e->is_var()); - lpvar j = to_var(e)->var(); - auto it = m_powers.find(j); - if (it == m_powers.end()) { - ret->add_child(mk_var(j)); - } else { - it->second --; - if (it->second == 0) - m_powers.erase(it); - } - TRACE("nla_cn_details", tout << *ret << "\n";); - } - SASSERT(m_powers.size() == 0); - if (ret->children().size() == 0) { - delete ret; - TRACE("nla_cn_details", tout << "return 1\n";); - return mk_scalar(rational(1)); - } - add_to_allocated(ret); - TRACE("nla_cn_details", tout << *ret << "\n";); - return ret; + nex * mk_div(const nex* a, lpvar j); + nex * mk_div(const nex* a, const nex* b); + + nex * simplify_mul(nex_mul *e); + bool is_sorted(const nex_mul * e) const; + bool mul_is_simplified(const nex_mul*e ) const; + + nex* simplify_sum(nex_sum *e); + + bool sum_is_simplified(nex_sum* e) const; + + void mul_to_powers(vector& children); + + nex* create_child_from_nex_and_coeff(nex *e, + const rational& coeff) ; + + void sort_join_sum(ptr_vector & children); + + void simplify_children_of_sum(ptr_vector & children); + + bool eat_scalar_pow(nex_scalar *& r, nex_pow& p); + void simplify_children_of_mul(vector & children, lt_on_vars lt, std::function mk_scalar); + +bool sum_simplify_lt(const nex* a, const nex* b); + +bool less_than_nex(const nex* a, const nex* b, const lt_on_vars& lt) { + int r = (int)(a->type()) - (int)(b->type()); + if (r) { + return r < 0; + } + SASSERT(a->type() == b->type()); + switch (a->type()) { + case expr_type::VAR: { + return lt(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: { + NOT_IMPLEMENTED_YET(); + return false; // to_mul(a)->children() < to_mul(b)->children(); + } + case expr_type::SUM: { + NOT_IMPLEMENTED_YET(); + return false; //to_sum(a)->children() < to_sum(b)->children(); + } + default: + SASSERT(false); + return false; } + return false; +} + bool mul_simplify_lt(const nex_mul* a, const nex_mul* b); + void fill_map_with_children(std::map & m, ptr_vector & children); }; } diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp index 9c36c96d7..a9b62bfe9 100644 --- a/src/math/lp/nla_grobner.cpp +++ b/src/math/lp/nla_grobner.cpp @@ -26,8 +26,11 @@ nla_grobner::nla_grobner(core *c common(c), m_nl_gb_exhausted(false), m_dep_manager(m_val_manager, m_alloc), - m_nex_creator([this](const nex* a, const nex* b) { return - this->less_than_on_expr(a, b); }) {} + m_nex_creator([this](lpvar a, lpvar b) { + if (m_active_vars_weights[a] != m_active_vars_weights[b]) + return m_active_vars_weights[a] < m_active_vars_weights[b]; + return a < b; + }) {} // Scan the grobner basis eqs for equations of the form x - k = 0 or x = 0 is found, and x is not fixed, // then assert bounds for x, and continue diff --git a/src/math/lp/nla_grobner.h b/src/math/lp/nla_grobner.h index 42b95bd7c..af0d63a77 100644 --- a/src/math/lp/nla_grobner.h +++ b/src/math/lp/nla_grobner.h @@ -36,17 +36,6 @@ struct grobner_stats { grobner_stats() { reset(); } }; -enum class var_weight { - FIXED = 0, - QUOTED_FIXED = 1, - BOUNDED = 2, - QUOTED_BOUNDED = 3, - NOT_FREE = 4, - QUOTED_NOT_FREE = 5, - FREE = 6, - QUOTED_FREE = 7, - MAX_DEFAULT_WEIGHT = 7 - }; class nla_grobner : common { @@ -90,7 +79,6 @@ class nla_grobner : common { equation_vector m_equations_to_delete; lp::int_set m_rows; lp::int_set m_active_vars; - svector m_active_vars_weights; unsigned m_num_of_equations; grobner_stats m_stats; equation_set m_processed; @@ -158,21 +146,21 @@ private: return rational(1); } - bool less_than_on_vars(lpvar a, lpvar b) const { - const auto &aw = m_active_vars_weights[a]; - const auto &ab = m_active_vars_weights[b]; - if (aw < ab) - return true; - if (aw > ab) - return false; - // aw == ab - return a < b; - } + // bool less_than_on_vars(lpvar a, lpvar b) const { + // const auto &aw = m_nex_creatorm_active_vars_weights[a]; + // const auto &ab = m_active_vars_weights[b]; + // if (aw < ab) + // return true; + // if (aw > ab) + // return false; + // // aw == ab + // return a < b; + // } - bool less_than_on_expr(const nex* a, const nex* b) const { - lt_on_vars lt = [this](lpvar j, lpvar k) {return less_than_on_vars(j, k);}; - return less_than_nex(a, b, lt); - } + // bool less_than_on_expr(const nex* a, const nex* b) const { + // lt_on_vars lt = [this](lpvar j, lpvar k) {return less_than_on_vars(j, k);}; + // return less_than_nex(a, b, lt); + // } }; // end of grobner diff --git a/src/test/lp/lp.cpp b/src/test/lp/lp.cpp index ace4f686d..21e419eeb 100644 --- a/src/test/lp/lp.cpp +++ b/src/test/lp/lp.cpp @@ -73,6 +73,8 @@ void test_cn_on_expr(nex_sum *t, cross_nested& cn) { cn.run(t); } +lt_on_vars lpvar_lt() { return [](lpvar a, lpvar b) { return a < b; };} + void test_simplify() { cross_nested cn( [](const nex* n) { @@ -80,9 +82,7 @@ void test_simplify() { return false; } , [](unsigned) { return false; }, - []{ return 1; }, - less_than_nex_standard - ); + []{ return 1; }, lpvar_lt()); enable_trace("nla_cn"); enable_trace("nla_cn_details"); nex_creator & r = cn.get_nex_creator(); @@ -104,11 +104,11 @@ void test_simplify() { nex * e = r.mk_sum(a, r.mk_sum(b, m)); TRACE("nla_cn", tout << "e = " << *e << "\n";); std::function mks = [&r] {return r.mk_scalar(rational(1)); }; - e->simplify(&e, mks); + e->simplify(&e, lpvar_lt(), mks); TRACE("nla_cn", tout << "simplified e = " << *e << "\n";); nex * l = r.mk_sum(e, r.mk_mul(r.mk_scalar(rational(3)), r.clone(e))); TRACE("nla_cn", tout << "sum l = " << *l << "\n";); - l->simplify(&l, mks); + l->simplify(&l, lpvar_lt(), mks); TRACE("nla_cn", tout << "simplified sum l = " << *l << "\n";); } @@ -119,9 +119,7 @@ void test_cn() { return false; } , [](unsigned) { return false; }, - []{ return 1; }, - less_than_nex_standard - ); + []{ return 1; }, lpvar_lt()); enable_trace("nla_cn"); enable_trace("nla_cn_details"); nex_var* a = cn.get_nex_creator().mk_var(0); @@ -147,8 +145,8 @@ void test_cn() { nex* _6aad = cn.get_nex_creator().mk_mul(cn.get_nex_creator().mk_scalar(rational(6)), a, a, d); #ifdef Z3DEBUG nex * clone = cn.get_nex_creator().clone(cn.get_nex_creator().mk_sum(_6aad, abcd, aaccd, add, eae, eac, ed)); - clone->simplify(&clone,[&cn] {return cn.get_nex_creator().mk_scalar(rational(1));}); - SASSERT(clone->is_simplified()); + clone->simplify(&clone, lpvar_lt(), [&cn] {return cn.get_nex_creator().mk_scalar(rational(1));}); + SASSERT(clone->is_simplified(lpvar_lt())); TRACE("nla_cn", tout << "clone = " << *clone << "\n";); #endif // test_cn_on_expr(cn.get_nex_creator().mk_sum(aad, abcd, aaccd, add, eae, eac, ed), cn);