diff --git a/src/math/lp/nex_creator.cpp b/src/math/lp/nex_creator.cpp index 8ac9f8214..bf83bf047 100644 --- a/src/math/lp/nex_creator.cpp +++ b/src/math/lp/nex_creator.cpp @@ -125,7 +125,7 @@ void nex_creator::simplify_children_of_mul(vector & children, rational& TRACE("grobner_d", print_vector(children, tout);); } -bool nex_creator:: less_than_on_powers_mul_same_degree(const vector& a, const nex_mul& b) const { +bool nex_creator:: gt_on_powers_mul_same_degree(const vector& a, const nex_mul& b) const { bool inside_a_p = false; // inside_a_p is true means we still compare the old position of it_a bool inside_b_p = false; // inside_b_p is true means we still compare the old position of it_b auto it_a = a.begin(); @@ -137,11 +137,11 @@ bool nex_creator:: less_than_on_powers_mul_same_degree(const vector& a, while (true) { if (!inside_a_p) { a_pow = it_a->pow(); } if (!inside_b_p) { b_pow = it_b->pow(); } - if (lt(it_a->e(), it_b->e())){ + if (gt(it_a->e(), it_b->e())){ ret = l_true; break; } - if (lt(it_b->e(), it_a->e())) { + if (gt(it_b->e(), it_a->e())) { ret = l_false; break; } @@ -184,7 +184,7 @@ bool nex_creator:: less_than_on_powers_mul_same_degree(const vector& a, return ret != l_false; } -bool nex_creator::less_than_on_mul_mul_same_degree(const nex_mul& a, const nex_mul& b) const { +bool nex_creator::gt_on_mul_mul_same_degree(const nex_mul& a, const nex_mul& b) const { bool inside_a_p = false; // inside_a_p is true means we still compare the old position of it_a bool inside_b_p = false; // inside_b_p is true means we still compare the old position of it_b auto it_a = a.begin(); @@ -196,11 +196,11 @@ bool nex_creator::less_than_on_mul_mul_same_degree(const nex_mul& a, const nex_m while (true) { if (!inside_a_p) { a_pow = it_a->pow(); } if (!inside_b_p) { b_pow = it_b->pow(); } - if (lt(it_a->e(), it_b->e())){ + if (gt(it_a->e(), it_b->e())){ ret = l_true; break; } - if (lt(it_b->e(), it_a->e())) { + if (gt(it_b->e(), it_a->e())) { ret = l_false; break; } @@ -255,40 +255,40 @@ bool nex_creator::children_are_simplified(const vector& children) const return true; } -bool nex_creator::less_than_on_powers_mul(const vector& children, const nex_mul& b) const { +bool nex_creator::gt_on_powers_mul(const vector& children, const nex_mul& b) const { TRACE("nex_less", 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 ? less_than_on_powers_mul_same_degree(children, b) : a_deg > b_deg; + return a_deg == b_deg ? gt_on_powers_mul_same_degree(children, b) : a_deg > b_deg; } -bool nex_creator::less_than_on_mul_mul(const nex_mul& a, const nex_mul& b) const { +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)); unsigned a_deg = a.get_degree(); unsigned b_deg = b.get_degree(); - return a_deg == b_deg ? less_than_on_mul_mul_same_degree(a, b) : a_deg > b_deg; + return a_deg == b_deg ? gt_on_mul_mul_same_degree(a, b) : a_deg > b_deg; } -bool nex_creator::less_than_on_var_nex(const nex_var* a, const nex* b) const { +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 less_than(a->var() , to_var(b)->var()); + return gt(a->var() , to_var(b)->var()); case expr_type::MUL: - return b->get_degree() <= 1 && less_than_on_var_nex(a, (*to_mul(b))[0].e()); + return b->get_degree() <= 1 && gt_on_var_nex(a, (*to_mul(b))[0].e()); case expr_type::SUM: - return !lt((*to_sum(b))[0], a); + return !gt((*to_sum(b))[0], a); default: UNREACHABLE(); return false; } } -bool nex_creator::lt_nex_powers(const vector& children, const nex* b) const { +bool nex_creator::gt_nex_powers(const vector& children, const nex* b) const { switch (b->type()) { case expr_type::SCALAR: return false; @@ -299,19 +299,19 @@ bool nex_creator::lt_nex_powers(const vector& children, const nex* b) c SASSERT(c.pow() == 1); const nex * f = c.e(); SASSERT(!f->is_scalar()); - return lt(f, b); + return gt(f, b); } case expr_type::MUL: - return less_than_on_powers_mul(children, *to_mul(b)); + return gt_on_powers_mul(children, *to_mul(b)); case expr_type::SUM: - return lt_nex_powers(children, (*to_sum(b))[0]); + return gt_nex_powers(children, (*to_sum(b))[0]); default: UNREACHABLE(); return false; } } -bool nex_creator::less_than_on_mul_nex(const nex_mul* a, const nex* b) const { +bool nex_creator::gt_on_mul_nex(const nex_mul* a, const nex* b) const { switch (b->type()) { case expr_type::SCALAR: return false; @@ -322,39 +322,39 @@ bool nex_creator::less_than_on_mul_nex(const nex_mul* a, const nex* b) const { SASSERT(c.pow() == 1); const nex * f = c.e(); SASSERT(!f->is_scalar()); - return lt(f, b); + return gt(f, b); } case expr_type::MUL: - return less_than_on_mul_mul(*a, *to_mul(b)); + return gt_on_mul_mul(*a, *to_mul(b)); case expr_type::SUM: - return lt(a, (*to_sum(b))[0]); + return gt(a, (*to_sum(b))[0]); default: UNREACHABLE(); return false; } } -bool nex_creator::less_than_on_sum_sum(const nex_sum* a, const nex_sum* b) const { +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 (lt((*a)[j], (*b)[j])) + if (gt((*a)[j], (*b)[j])) return true; - if (lt((*b)[j], (*a)[j])) + if (gt((*b)[j], (*a)[j])) return false; } return size > b->size(); } -// the only difference with lt() that it disregards the coefficient in nex_mul -bool nex_creator::lt_for_sort_join_sum(const nex* a, const nex* b) const { +// the only difference with gt() that it disregards the coefficient in nex_mul +bool nex_creator::gt_for_sort_join_sum(const nex* a, const nex* b) const { TRACE("grobner_d_", tout << *a << " ? " << *b << "\n";); if (a == b) return false; bool ret; switch (a->type()) { case expr_type::VAR: - ret = less_than_on_var_nex(to_var(a), b); + ret = gt_on_var_nex(to_var(a), b); break; case expr_type::SCALAR: if (b->is_scalar()) @@ -363,12 +363,12 @@ bool nex_creator::lt_for_sort_join_sum(const nex* a, const nex* b) const { ret = false; // the scalars are the largest break; case expr_type::MUL: - ret = lt_nex_powers(to_mul(a)->children(), b); + ret = gt_nex_powers(to_mul(a)->children(), b); break; case expr_type::SUM: if (b->is_sum()) - return less_than_on_sum_sum(to_sum(a), to_sum(b)); - return lt((*to_sum(a))[0], b); + return gt_on_sum_sum(to_sum(a), to_sum(b)); + return gt((*to_sum(a))[0], b); default: UNREACHABLE(); return false; @@ -377,26 +377,26 @@ bool nex_creator::lt_for_sort_join_sum(const nex* a, const nex* b) const { return ret; } -bool nex_creator::lt(const nex* a, const nex* b) const { +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()) { case expr_type::VAR: - ret = less_than_on_var_nex(to_var(a), b); + ret = gt_on_var_nex(to_var(a), b); break; case expr_type::SCALAR: ret = b->is_scalar() && to_scalar(a)->value() > to_scalar(b)->value(); // the scalars are the largest break; case expr_type::MUL: - ret = less_than_on_mul_nex(to_mul(a), b); + ret = gt_on_mul_nex(to_mul(a), b); break; case expr_type::SUM: if (b->is_sum()) - return less_than_on_sum_sum(to_sum(a), to_sum(b)); - return lt((*to_sum(a))[0], b); + return gt_on_sum_sum(to_sum(a), to_sum(b)); + return gt((*to_sum(a))[0], b); default: UNREACHABLE(); return false; @@ -407,7 +407,7 @@ bool nex_creator::lt(const nex* a, const nex* b) const { bool nex_creator::is_sorted(const nex_mul* e) const { for (unsigned j = 0; j < e->size() - 1; j++) { - if (!(less_than_on_nex_pow((*e)[j], (*e)[j+1]))) { + if (!(gt_on_nex_pow((*e)[j], (*e)[j+1]))) { TRACE("grobner_d", tout << "not sorted e " << * e << "\norder is incorrect " << (*e)[j] << " >= " << (*e)[j + 1]<< "\n";); @@ -427,7 +427,7 @@ bool nex_creator::mul_is_simplified(const nex_mul* e) const { TRACE("nla_cn", ); return false; } - std::set s([this](const nex* a, const nex* b) {return lt(a, b); }); + std::set s([this](const nex* a, const nex* b) {return gt(a, b); }); for (const auto &p : *e) { const nex* ee = p.e(); if (p.pow() == 0) { @@ -516,7 +516,7 @@ bool nex_creator::sum_is_simplified(const nex_sum* e) const { } void nex_creator::mul_to_powers(vector& children) { - std::map m([this](const nex* a, const nex* b) { return lt(a, b); }); + std::map m([this](const nex* a, const nex* b) { return gt(a, b); }); for (auto & p : children) { auto it = m.find(p.e()); @@ -532,7 +532,7 @@ void nex_creator::mul_to_powers(vector& children) { } std::sort(children.begin(), children.end(), [this](const nex_pow& a, const nex_pow& b) { - return less_than_on_nex_pow(a, b); + return gt_on_nex_pow(a, b); }); } @@ -561,7 +561,7 @@ nex* nex_creator::create_child_from_nex_and_coeff(nex *e, } em->add_child(mk_scalar(coeff)); std::sort(em->begin(), em->end(), [this](const nex_pow& a, - const nex_pow& b) {return less_than_on_nex_pow(a, b); }); + const nex_pow& b) {return gt_on_nex_pow(a, b); }); return em; } case expr_type::SUM: @@ -620,7 +620,7 @@ bool nex_creator::fill_join_map_for_sum( 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) - { return lt_for_sort_join_sum(a, b); }); + { return gt_for_sort_join_sum(a, b); }); std::unordered_set allocated_nexs; // handling (nex*) as numbers nex_scalar * common_scalar; fill_join_map_for_sum(children, map, allocated_nexs, common_scalar); @@ -888,7 +888,7 @@ bool nex_creator::equal(const nex* a, const nex* b) { nex * cb = cn.canonize(b); TRACE("grobner_d", tout << "a = " << *a << ", canonized a = " << *ca << "\n";); TRACE("grobner_d", tout << "b = " << *b << ", canonized b = " << *cb << "\n";); - return !(cn.lt(ca, cb) || cn.lt(cb, ca)); + return !(cn.gt(ca, cb) || cn.gt(cb, ca)); } #endif diff --git a/src/math/lp/nex_creator.h b/src/math/lp/nex_creator.h index d6e0b3c83..f85d4e518 100644 --- a/src/math/lp/nex_creator.h +++ b/src/math/lp/nex_creator.h @@ -81,14 +81,14 @@ private: public: nex* simplify(nex* e); - bool less_than(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; } - bool less_than_on_nex_pow(const nex_pow & a, const nex_pow& b) const { - return (a.pow() > b.pow()) || (a.pow() == b.pow() && lt(a.e(), b.e())); + 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 simplify_children_of_mul(vector & children, rational&); @@ -239,19 +239,19 @@ public: void simplify_children_of_sum(ptr_vector & children); bool eat_scalar_pow(rational& r, const nex_pow& p, unsigned); - void simplify_children_of_mul(vector & children, lt_on_vars lt, std::function mk_scalar); + void simplify_children_of_mul(vector & children, lt_on_vars, std::function mk_scalar); bool children_are_simplified(const vector& children) const; - bool lt(const nex* a, const nex* b) const; - bool lt_nex_powers(const vector&, const nex* b) const; - bool less_than_on_powers_mul(const vector&, const nex_mul& b) const; - bool less_than_on_powers_mul_same_degree(const vector&, const nex_mul& b) const; - bool lt_for_sort_join_sum(const nex* a, const nex* b) const; - bool less_than_on_mul_mul(const nex_mul& a, const nex_mul& b) const; - bool less_than_on_mul_mul_same_degree(const nex_mul& a, const nex_mul& b) const; - bool less_than_on_var_nex(const nex_var* a, const nex* b) const; - bool less_than_on_mul_nex(const nex_mul* a, const nex* b) const; - bool less_than_on_sum_sum(const nex_sum* a, const nex_sum* b) 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_on_powers_mul_same_degree(const vector&, 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_mul_mul_same_degree(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 fill_map_with_children(std::map & m, ptr_vector & children); void process_map_pair(nex *e, const rational& coeff, ptr_vector & children, std::unordered_set&); #ifdef Z3DEBUG diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp index 4538e9227..010ef94eb 100644 --- a/src/math/lp/nla_grobner.cpp +++ b/src/math/lp/nla_grobner.cpp @@ -164,14 +164,15 @@ bool nla_grobner::is_trivial(equation* eq) const { return eq->expr()->size() == 0; } -bool nla_grobner::is_better_choice(equation * eq1, equation * eq2) { +// returns true if eq1 is simpler than eq2 +bool nla_grobner::is_simpler(equation * eq1, equation * eq2) { if (!eq2) return true; if (is_trivial(eq1)) return true; if (is_trivial(eq2)) return false; - return m_nex_creator.lt(eq2->expr(), eq1->expr()); + return m_nex_creator.gt(eq2->expr(), eq1->expr()); } void nla_grobner::del_equation(equation * eq) { @@ -188,7 +189,7 @@ nla_grobner::equation* nla_grobner::pick_next() { for (equation * curr : m_to_simplify) { if (is_trivial(curr)) to_delete.push_back(curr); - else if (is_better_choice(curr, r)) { + else if (is_simpler(curr, r)) { TRACE("grobner", tout << "preferring "; display_equation(tout, *curr);); r = curr; } @@ -554,7 +555,7 @@ void nla_grobner::superpose(equation * eq1, equation * eq2) { } equation* eq = alloc(equation); init_equation(eq, expr_superpose( eq1->expr(), eq2->expr(), ab, ac, b, c), m_dep_manager.mk_join(eq1->dep(), eq2->dep())); - if (m_nex_creator.lt(eq->expr(), eq1->expr()) || m_nex_creator.lt(eq->expr(), eq2->expr())) { + if (m_nex_creator.gt(eq->expr(), eq1->expr()) || m_nex_creator.gt(eq->expr(), eq2->expr())) { TRACE("grobner", display_equation(tout, *eq) << " is too complex: deleting it\n;";); del_equation(eq); } else { @@ -580,11 +581,11 @@ bool nla_grobner::find_b_c(const nex* ab, const nex* ac, nex_mul*& b, nex_mul*& for (;;) { const nex* m = ab->get_child_exp(i); const nex* n = ac->get_child_exp(j); - if (m_nex_creator.lt(m, n)) { + if (m_nex_creator.gt(m, n)) { b->add_child_in_power(const_cast(m), ab->get_child_pow(i)); if (++i == ab_size) break; - } else if (m_nex_creator.lt(n, m)) { + } else if (m_nex_creator.gt(n, m)) { c->add_child_in_power(const_cast(n), ac->get_child_pow(j)); if (++j == ac_size) break; @@ -624,11 +625,11 @@ bool nla_grobner::find_b_c_check_only(const nex* ab, const nex* ac) const { for (;;) { const nex* m = ab->get_child_exp(i); const nex* n = ac->get_child_exp(j); - if (m_nex_creator.lt(m , n)) { + if (m_nex_creator.gt(m , n)) { i++; if (i == ab->number_of_child_powers()) return false; - } else if (m_nex_creator.lt(n, m)) { + } else if (m_nex_creator.gt(n, m)) { j++; if (j == ac->number_of_child_powers()) return false; diff --git a/src/math/lp/nla_grobner.h b/src/math/lp/nla_grobner.h index da82e584a..25d989840 100644 --- a/src/math/lp/nla_grobner.h +++ b/src/math/lp/nla_grobner.h @@ -125,7 +125,7 @@ private: bool find_b_c(const nex *ab, const nex* ac, nex_mul*& b, nex_mul*& c); bool find_b_c_check_only(const nex* ab, const nex* ac) const; bool is_trivial(equation* ) const; - bool is_better_choice(equation * eq1, equation * eq2); + 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;