diff --git a/src/math/lp/horner.cpp b/src/math/lp/horner.cpp index 22dfdc159..fdb2eb092 100644 --- a/src/math/lp/horner.cpp +++ b/src/math/lp/horner.cpp @@ -99,6 +99,9 @@ bool horner::lemmas_on_row(const T& row) { create_sum_from_row(row, cn.get_nex_creator(), m_row_sum, m_fixed_var_constraints_for_row); set_active_vars_weights(); // without this call the comparisons will be incorrect nex* e = m_nex_creator.simplify(&m_row_sum); + TRACE("nla_horner", tout << "e = " << * e << "\n";); + if (e->get_degree() < 2) + return false; if (!e->is_sum()) return false; diff --git a/src/math/lp/nex.h b/src/math/lp/nex.h index 0b9d777c5..f08a3d03b 100644 --- a/src/math/lp/nex.h +++ b/src/math/lp/nex.h @@ -162,6 +162,13 @@ public: friend std::ostream& operator<<(std::ostream& out, const nex_pow & p) { out << p.to_string(); return out; } }; +inline unsigned get_degree_children(const vector& children) { + int degree = 0; + for (const auto& p : children) { + degree += p.e()->get_degree() * p.pow(); + } + return degree; +} class nex_mul : public nex { rational m_coeff; @@ -169,6 +176,9 @@ class nex_mul : public nex { public: nex_mul() : m_coeff(rational(1)) {} + template + nex_mul() : m_coeff() {} + const rational& coeff() const { return m_coeff; } @@ -258,13 +268,9 @@ public: } int get_degree() const { - int degree = 0; - for (const auto& p : *this) { - degree += p.e()->get_degree() * p.pow(); - } - return degree; - } - + return get_degree_children(children()); + } + bool is_linear() const { return get_degree() < 2; // todo: make it more efficient } diff --git a/src/math/lp/nex_creator.cpp b/src/math/lp/nex_creator.cpp index 94637d5dc..e9b1b7c1a 100644 --- a/src/math/lp/nex_creator.cpp +++ b/src/math/lp/nex_creator.cpp @@ -114,8 +114,69 @@ void nex_creator::simplify_children_of_mul(vector & children, rational& TRACE("nla_cn_details", print_vector(children, tout);); } +bool nex_creator:: less_than_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(); + auto it_b = b->begin(); + auto a_end = a.end(); + auto b_end = b->end(); + unsigned a_pow, b_pow; + int ret = - 1; + do { + 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())){ + ret = true; + break; + } + if (lt(it_b->e(), it_a->e())) { + ret = false; + break; + } -bool nex_creator::less_than_on_mul_mul_same_degree_iterate(const nex_mul* a, const nex_mul* b) const { + if (a_pow == b_pow) { + inside_a_p = inside_b_p = false; + it_a++; it_b++; + if (it_a == a_end) { + ret = false; + break; + } + if (it_b == b_end) { // it_a is not at the end + ret = false; + break; + } + // no iterator reached the end + continue; + } + if (a_pow > b_pow) { + it_a++; + if (it_a == a_end) { + ret = true; + break; + } + inside_a_p = false; + inside_b_p = true; + b_pow -= a_pow; + } else { + SASSERT(a_pow < b_pow); + a_pow -= b_pow; + it_b++; + if (it_b == b_end) { + ret = false; + break; + } + inside_a_p = true; + inside_b_p = false; + } + } while (true); + if (ret == -1) + ret = true; + TRACE("nla_cn_details", tout << "a = "; print_vector(a, tout) << (ret == 1?" < ":" >= ") << *b << "\n";); + return ret; +} + +bool nex_creator::less_than_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(); @@ -182,11 +243,29 @@ bool nex_creator::less_than_on_mul_mul_same_degree_iterate(const nex_mul* a, con return ret; } -bool nex_creator::less_than_on_mul_mul_same_degree(const nex_mul* a, const nex_mul* b) const { - SASSERT(a->get_degree() == b->get_degree()); - SASSERT(a->size() && b->size()); - return less_than_on_mul_mul_same_degree_iterate(a, b); +bool nex_creator::children_are_simplified(const vector& children) const { + for (auto c : children) + if (!is_simplified(c.e()) || c.pow() == 0) + return false; + return true; } +bool nex_creator::less_than_on_powers_mul(const vector& children, const nex_mul* b) const { + TRACE("nla_cn_details", 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(); + bool ret; + if (a_deg > b_deg) { + ret = true; + } else if (a_deg < b_deg) { + ret = false; + } else { + ret = less_than_on_powers_mul_same_degree(children, b); + } + return ret; + +} + bool nex_creator::less_than_on_mul_mul(const nex_mul* a, const nex_mul* b) const { TRACE("nla_cn_details", tout << "a = " << *a << " , b = " << *b << "\n";); @@ -230,6 +309,30 @@ bool nex_creator::less_than_on_var_nex(const nex_var* a, const nex* b) const { } } +bool nex_creator::lt_nex_powers(const vector& children, const nex* b) const { + switch(b->type()) { + case expr_type::SCALAR: return false; + case expr_type::VAR: + { + if (get_degree_children(children) > 1) + return true; + auto it = children.begin(); + const nex_pow & c = *it; + SASSERT(c.pow() == 1); + const nex * f = c.e(); + SASSERT(!f->is_scalar()); + return lt(f, b); + } + case expr_type::MUL: + return less_than_on_powers_mul(children, to_mul(b)); + case expr_type::SUM: + return lt_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 { switch(b->type()) { @@ -267,6 +370,40 @@ bool nex_creator::less_than_on_sum_sum(const nex_sum* a, const nex_sum* b) const } +// 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 { + TRACE("nla_cn_details_", 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); + break; + case expr_type::SCALAR: { + if (b->is_scalar()) + ret = to_scalar(a)->value() > to_scalar(b)->value(); + else + ret = false; // the scalars are the largest + break; + } + case expr_type::MUL: { + ret = lt_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); + } + default: + UNREACHABLE(); + return false; + } + TRACE("nla_cn_details_", tout << *a << (ret?" < ":" >= ") << *b << "\n";); + return ret; +} + bool nex_creator::lt(const nex* a, const nex* b) const { TRACE("nla_cn_details_", tout << *a << " ? " << *b << "\n";); if (a == b) @@ -296,11 +433,8 @@ bool nex_creator::lt(const nex* a, const nex* b) const { UNREACHABLE(); return false; } - TRACE("nla_cn_details_", tout << *a << (ret?" < ":" >= ") << *b << "\n";); - return ret; - } bool nex_creator::is_sorted(const nex_mul* e) const { @@ -513,7 +647,7 @@ bool nex_creator::fill_join_map_for_sum(ptr_vector & children, void nex_creator::sort_join_sum(ptr_vector & children) { TRACE("nla_cn_details", print_vector_of_ptrs(children, tout);); std::map map([this](const nex *a , const nex *b) - { return lt(a, b); }); + { return lt_for_sort_join_sum(a, b); }); std::unordered_set existing_nex; // handling (nex*) as numbers nex_scalar * common_scalar; fill_join_map_for_sum(children, map, existing_nex, common_scalar); @@ -526,6 +660,7 @@ void nex_creator::sort_join_sum(ptr_vector & children) { for (auto& p : map) { process_map_pair(p.first, p.second, children, existing_nex); } + TRACE("nla_cn_details", for (auto & p : map ) { tout << "(" << *p.first << ", " << p.second << ") ";}); } bool is_zero_scalar(nex *e) { diff --git a/src/math/lp/nex_creator.h b/src/math/lp/nex_creator.h index 6e7235fb3..c158fd15f 100644 --- a/src/math/lp/nex_creator.h +++ b/src/math/lp/nex_creator.h @@ -250,10 +250,14 @@ public: 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); + 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_mul_mul_same_degree_iterate(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; diff --git a/src/math/lp/nla_common.cpp b/src/math/lp/nla_common.cpp index 7fdb5ee61..85aee1ded 100644 --- a/src/math/lp/nla_common.cpp +++ b/src/math/lp/nla_common.cpp @@ -124,22 +124,6 @@ unsigned common::random() { // it also inserts variables into m_active_vars // and updates fixed_var_deps -nex * common::nexvar(lpvar j, nex_creator& cn, svector & fixed_vars_constraints) { - // todo: consider deepen the recursion - if (!c().is_monic_var(j)) { - c().insert_to_active_var_set(j); - return cn.mk_var(j); - } - const monic& m = c().emons()[j]; - nex_mul * e = cn.mk_mul(); - for (lpvar k : m.vars()) { - c().insert_to_active_var_set(k); - e->add_child(cn.mk_var(k)); - CTRACE("nla_horner", c().is_monic_var(k), c().print_var(k, tout) << "\n";); - } - return e; -} - nex * common::nexvar(const rational & coeff, lpvar j, nex_creator& cn, svector & fixed_vars_constraints) { if (!c().is_monic_var(j)) { @@ -148,7 +132,7 @@ nex * common::nexvar(const rational & coeff, lpvar j, nex_creator& cn, c().m_lar_solver.get_bound_constraint_witnesses_for_column(j, lc, uc); fixed_vars_constraints.push_back(lc); fixed_vars_constraints.push_back(uc); - return cn.mk_scalar(c().m_lar_solver.get_lower_bound(j).x); + return cn.mk_scalar(coeff * c().m_lar_solver.get_lower_bound(j).x); } c().insert_to_active_var_set(j); return cn.mk_mul(cn.mk_scalar(coeff), cn.mk_var(j)); @@ -156,15 +140,15 @@ nex * common::nexvar(const rational & coeff, lpvar j, nex_creator& cn, const monic& m = c().emons()[j]; nex_mul * e = cn.mk_mul(cn.mk_scalar(coeff)); for (lpvar k : m.vars()) { - if (c().var_is_fixed(j)) { + if (c().var_is_fixed(k)) { lp::constraint_index lc,uc; - c().m_lar_solver.get_bound_constraint_witnesses_for_column(j, lc, uc); + c().m_lar_solver.get_bound_constraint_witnesses_for_column(k, lc, uc); fixed_vars_constraints.push_back(lc); fixed_vars_constraints.push_back(uc); - e->coeff() *= c().m_lar_solver.get_lower_bound(j).x; + e->coeff() *= c().m_lar_solver.get_lower_bound(k).x; continue; } - c().insert_to_active_var_set(j); + c().insert_to_active_var_set(k); e->add_child(cn.mk_var(k)); CTRACE("nla_horner", c().is_monic_var(k), c().print_var(k, tout) << "\n";); } @@ -181,14 +165,40 @@ template void common::create_sum_from_row(const T& row, nex_creator SASSERT(row.size() > 1); sum.children().clear(); for (const auto &p : row) { - if (p.coeff().is_one()) { - nex* e = nexvar(p.var(), cn, fixed_vars_constraints); - sum.add_child(e); - } else { - nex* e = nexvar(p.coeff(), p.var(), cn, fixed_vars_constraints); - sum.add_child(e); + nex* e = nexvar(p.coeff(), p.var(), cn, fixed_vars_constraints); + sum.add_child(e); + } + TRACE("nla_horner", tout << "sum =" << sum << "\n";); +} + +template +common::ci_dependency* common::get_fixed_vars_dep_from_row(const T& row, ci_dependency_manager& dep_manager) { + TRACE("nla_horner", tout << "row="; m_core->print_term(row, tout) << "\n";); + ci_dependency* dep = nullptr; + for (const auto &p : row) { + lpvar j = p.var(); + + if (!c().is_monic_var(j)) { + if (c().var_is_fixed(j)) { + lp::constraint_index lc,uc; + c().m_lar_solver.get_bound_constraint_witnesses_for_column(j, lc, uc); + dep = dep_manager.mk_join(dep, dep_manager.mk_leaf(lc)); + dep = dep_manager.mk_join(dep, dep_manager.mk_leaf(uc)); + } else { + const monic& m = c().emons()[j]; + for (lpvar k : m.vars()) { + if (!c().var_is_fixed(k)) + continue; + lp::constraint_index lc,uc; + c().m_lar_solver.get_bound_constraint_witnesses_for_column(k, lc, uc); + c().m_lar_solver.get_bound_constraint_witnesses_for_column(k, lc, uc); + dep = dep_manager.mk_join(dep, dep_manager.mk_leaf(lc)); + dep = dep_manager.mk_join(dep, dep_manager.mk_leaf(uc)); + } + } } } + return dep; } void common::set_active_vars_weights() { @@ -198,6 +208,8 @@ void common::set_active_vars_weights() { } } + + var_weight common::get_var_weight(lpvar j) const { var_weight k; switch (c().m_lar_solver.get_column_type(j)) { diff --git a/src/math/lp/nla_common.h b/src/math/lp/nla_common.h index b833ae612..e8b810a6e 100644 --- a/src/math/lp/nla_common.h +++ b/src/math/lp/nla_common.h @@ -117,11 +117,13 @@ struct common { typedef dependency_manager ci_dependency_manager; typedef ci_dependency_manager::dependency ci_dependency; - nex* nexvar(lpvar j, nex_creator&, svector & fixed_vars_constraints); + // nex* nexvar(lpvar j, nex_creator&, svector & fixed_vars_constraints); nex* nexvar(const rational& coeff, lpvar j, nex_creator&, svector & fixed_vars_constraints); template void create_sum_from_row(const T&, nex_creator&, nex_sum&, svector & fixed_vars_constraints); + template + ci_dependency* get_fixed_vars_dep_from_row(const T&, ci_dependency_manager& dep_manager); void set_active_vars_weights(); var_weight get_var_weight(lpvar) const; };