From 316a0470b180f342e7abb5ccb719bb76c6563ccf Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Mon, 30 Sep 2019 16:53:46 -0700 Subject: [PATCH] more fixes in simplifying nex expessions Signed-off-by: Lev Nachmanson --- src/math/lp/nex.h | 1 - src/math/lp/nex_creator.cpp | 84 +++++++++++++++++++++++++++++-------- src/math/lp/nex_creator.h | 6 ++- 3 files changed, 70 insertions(+), 21 deletions(-) diff --git a/src/math/lp/nex.h b/src/math/lp/nex.h index 71921e690..18c9666ca 100644 --- a/src/math/lp/nex.h +++ b/src/math/lp/nex.h @@ -50,7 +50,6 @@ inline std::ostream & operator<<(std::ostream& out, expr_type t) { } class nex; -bool less_than_nex_standard(const nex* a, const nex* b); class nex_scalar; // This is the class of non-linear expressions diff --git a/src/math/lp/nex_creator.cpp b/src/math/lp/nex_creator.cpp index 31a60c184..aaf685e88 100644 --- a/src/math/lp/nex_creator.cpp +++ b/src/math/lp/nex_creator.cpp @@ -116,7 +116,7 @@ void nex_creator::simplify_children_of_mul(vector & children) { TRACE("nla_cn_details", print_vector(children, tout);); } -bool nex_creator::less_than_on_mul(const nex_mul* a, const nex_mul* b, bool skip_scalar) { +bool nex_creator::less_than_on_mul(const nex_mul* a, const nex_mul* b, bool skip_scalar) const { // the scalar, if it is there, is at the beginning of the children() TRACE("nla_cn_details", tout << "a = " << *a << ", b = " << *b << ", skip_scalar = " << skip_scalar << "\n";); SASSERT(is_simplified(a) && is_simplified(b)); @@ -170,19 +170,20 @@ bool nex_creator::less_than_on_mul(const nex_mul* a, const nex_mul* b, bool skip continue; } if (a_pow < b_pow) { - inside_a_p = false; - inside_b_p = true; - b_pow -= a_pow; it_a++; if (it_a == a_end) return true; + inside_a_p = false; + inside_b_p = true; + b_pow -= a_pow; } else { - inside_a_p = true; - inside_b_p = false; - SASSERT(b_pow < a_pow); + SASSERT(a_pow > b_pow); + a_pow -= b_pow; it_b++; if (it_b == b_end) return false; + inside_a_p = true; + inside_b_p = false; } } return false; @@ -190,22 +191,68 @@ bool nex_creator::less_than_on_mul(const nex_mul* a, const nex_mul* b, bool skip } -bool nex_creator::lt(const nex* a, const nex* b, bool skip_scalar) { +bool nex_creator::less_than_on_var_nex(const nex_var* a, const nex* b, bool skip_scalar) const { + switch(b->type()) { + case expr_type::SCALAR: return false; + case expr_type::VAR: + return less_than(a->var() , to_var(b)->var()); + case expr_type::MUL: + { + nex_mul m; + m.add_child(const_cast(a)); + return less_than_on_mul(&m, to_mul(b), skip_scalar); + } + + case expr_type::SUM: + { + nex_sum m; + m.add_child(const_cast(a)); + return lt(&m, to_sum(b), skip_scalar); + } + default: + UNREACHABLE(); + return false; + } +} + + +bool nex_creator::less_than_on_mul_nex(const nex_mul* a, const nex* b, bool skip_scalar) const { + switch(b->type()) { + case expr_type::SCALAR: return false; + case expr_type::VAR: + { + nex_mul m; + m.add_child(const_cast(b)); + return less_than_on_mul(a, &m, skip_scalar); + } + case expr_type::MUL: + return less_than_on_mul(a, to_mul(b), skip_scalar); + case expr_type::SUM: + { + const nex* fc = *(to_sum(b)->children().begin()); + return lt(a, fc, skip_scalar); + } + default: + UNREACHABLE(); + return false; + } +} + +bool nex_creator::lt(const nex* a, const nex* b, bool skip_scalar) const { TRACE("nla_cn_details", tout << "a = " << *a << ", b = " << *b << ", skip_scalar = " << skip_scalar << "\n";); - 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 less_than(to_var(a)->var() , to_var(b)->var()); - } + case expr_type::VAR: + return less_than_on_var_nex(to_var(a), b, skip_scalar); + case expr_type::SCALAR: { - return to_scalar(a)->value() < to_scalar(b)->value(); + if (b->is_scalar()) + return + to_scalar(a)->value() < to_scalar(b)->value(); + return true; // the scalars are the smallest } case expr_type::MUL: { - return less_than_on_mul(to_mul(a), to_mul(b), skip_scalar); + return less_than_on_mul_nex(to_mul(a), b, skip_scalar); } case expr_type::SUM: { UNREACHABLE(); @@ -228,6 +275,7 @@ bool nex_creator::is_sorted(const nex_mul* e) const { return true; } + bool nex_creator::less_than_nex(const nex* a, const nex* b) const { int r = (int)(a->type()) - (int)(b->type()); if (r) { diff --git a/src/math/lp/nex_creator.h b/src/math/lp/nex_creator.h index df4d62eb8..ad95f08de 100644 --- a/src/math/lp/nex_creator.h +++ b/src/math/lp/nex_creator.h @@ -223,9 +223,11 @@ public: 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 lt(const nex* a, const nex* b, bool skip_scalar); + bool lt(const nex* a, const nex* b, bool skip_scalar) const; - bool less_than_on_mul(const nex_mul* a, const nex_mul* b, bool skip_scalar); + bool less_than_on_mul(const nex_mul* a, const nex_mul* b, bool skip_scalar) const; + bool less_than_on_var_nex(const nex_var* a, const nex* b, bool skip_scalar) const; + bool less_than_on_mul_nex(const nex_mul* a, const nex* b, bool skip_scalar) const; void fill_map_with_children(std::map & m, ptr_vector & children); }; }