From 496a8c17aa1c12ca5a1fb167cd54c384b6723d33 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 31 Dec 2019 14:47:26 -0800 Subject: [PATCH] remove nex grobner Signed-off-by: Lev Nachmanson --- src/math/lp/CMakeLists.txt | 1 - src/math/lp/nla_core.cpp | 9 - src/math/lp/nla_core.h | 3 - src/math/lp/nla_grobner.cpp | 746 ------------------------------------ src/math/lp/nla_grobner.h | 224 ----------- src/math/lp/nla_settings.h | 15 +- src/smt/theory_lra.cpp | 1 - 7 files changed, 3 insertions(+), 996 deletions(-) delete mode 100644 src/math/lp/nla_grobner.cpp delete mode 100644 src/math/lp/nla_grobner.h diff --git a/src/math/lp/CMakeLists.txt b/src/math/lp/CMakeLists.txt index 8d3c3a31e..549c16b21 100644 --- a/src/math/lp/CMakeLists.txt +++ b/src/math/lp/CMakeLists.txt @@ -30,7 +30,6 @@ z3_add_component(lp nla_basics_lemmas.cpp nla_common.cpp nla_core.cpp - nla_grobner.cpp nla_intervals.cpp nla_monotone_lemmas.cpp nla_order_lemmas.cpp diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 50d2cc8f8..a10dad648 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -34,7 +34,6 @@ core::core(lp::lar_solver& s, reslimit & lim) : m_monotone(this), m_intervals(this, lim), m_horner(this, &m_intervals), - m_nex_grobner(this, &m_intervals), m_pdd_manager(s.number_of_vars()), m_pdd_grobner(lim, m_pdd_manager), m_emons(m_evars), @@ -1626,14 +1625,6 @@ void core::display_matrix_of_m_rows(std::ostream & out) const { } } -void core::init_nex_grobner(nex_creator & nc) { - m_nex_grobner.init(); - set_active_vars_weights(nc); - for (unsigned i : m_rows) { - m_nex_grobner.add_row(m_lar_solver.A_r().m_rows[i]); - } -} - void core::set_active_vars_weights(nex_creator& nc) { nc.set_number_of_vars(m_lar_solver.column_count()); for (lpvar j : active_var_set()) { diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index 633026ee2..d905415b1 100644 --- a/src/math/lp/nla_core.h +++ b/src/math/lp/nla_core.h @@ -29,7 +29,6 @@ #include "math/lp/nla_settings.h" #include "math/lp/nex.h" #include "math/lp/horner.h" -#include "math/lp/nla_grobner.h" #include "math/lp/nla_intervals.h" #include "math/grobner/pdd_grobner.h" @@ -95,7 +94,6 @@ public: intervals m_intervals; horner m_horner; nla_settings m_nla_settings; - grobner m_nex_grobner; dd::pdd_manager m_pdd_manager; dd::grobner m_pdd_grobner; @@ -405,7 +403,6 @@ public: void find_nl_cluster(); void prepare_rows_and_active_vars(); void add_var_and_its_factors_to_q_and_collect_new_rows(lpvar j, svector& q); - void init_nex_grobner(nex_creator&); std::unordered_set get_vars_of_expr_with_opening_terms(const nex* e); void display_matrix_of_m_rows(std::ostream & out) const; void set_active_vars_weights(nex_creator&); diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp deleted file mode 100644 index e9c0821ee..000000000 --- a/src/math/lp/nla_grobner.cpp +++ /dev/null @@ -1,746 +0,0 @@ -/*++ - Copyright (c) 2017 Microsoft Corporation - - Module Name: - - - - Abstract: - - - - Author: - Nikolaj Bjorner (nbjorner) - Lev Nachmanson (levnach) - - Revision History: - - - --*/ -#include "math/lp/nla_grobner.h" -#include "math/lp/nla_core.h" -#include "math/lp/factorization_factory_imp.h" -using namespace nla; - -grobner::grobner(core *c, intervals *s) - : common(c, s), - m_gc(m_nex_creator, c->m_reslim) { - std::function de; - de = [this](lp::explanation const& e, std::ostream& out) { m_core->print_explanation(e, out); }; - grobner_core::params p; - p.m_expr_size_limit = c->m_nla_settings.grobner_expr_size_limit(); - p.m_grobner_eqs_threshold = c->m_nla_settings.grobner_eqs_threshold(); - m_gc = de; - m_gc = p; -} - -void grobner::grobner_lemmas() { - c().lp_settings().stats().m_grobner_calls++; - m_reported = 0; - TRACE("grobner", tout << "before:\n"; display(tout);); - m_gc.compute_basis_loop(); - for (grobner_core::equation* e : m_gc.equations()) { - check_eq(e); - } - TRACE("grobner", tout << "after:\n"; display(tout);); -} - -void grobner::check_eq(grobner_core::equation* target) { - if (m_intervals->check_nex(target->expr(), target->dep())) { - TRACE("grobner", tout << "created a lemma for "; m_gc.display_equation(tout, *target) << "\n"; - tout << "vars = \n"; - for (lpvar j : get_vars_of_expr(target->expr())) { - c().print_var(j, tout); - } - tout << "\ntarget->expr() val = " << get_nex_val(target->expr(), [this](unsigned j) { return c().val(j); }) << "\n";); - c().lp_settings().stats().m_grobner_conflicts++; - } -} - -void grobner::add_row(const vector> & row) { - TRACE("grobner", tout << "adding row to gb\n"; c().m_lar_solver.print_row(row, tout) << '\n'; - for (auto p : row) c().print_var(p.var(), tout) << "\n"; ); - nex_creator::sum_factory sf(m_nex_creator); - u_dependency* dep = create_sum_from_row(row, m_nex_creator, sf, &m_gc.dep()); - nex* e = m_nex_creator.simplify(sf.mk()); - TRACE("grobner", tout << "e = " << *e << "\n";); - m_gc.assert_eq_0(e, dep); -} - -/// ------------------------------- -/// grobner_core - -/*** -The main algorithm maintains two sets (S, A), -where S is m_to_superpose, and A is m_to_simplify. -Initially S is empty and A contains the initial equations. - -Each step proceeds as follows: - - pick a in A, and remove a from A - - simplify a using S - - simplify S using a - - for s in S: - b = superpose(a, s) - add b to A - - add a to S - - simplify A using a -*/ - -void grobner::init() { - m_gc.reset(); -} - -bool grobner_core::compute_basis_loop() { - while (!done()) { - if (compute_basis_step()) { - TRACE("grobner", tout << "progress in compute_basis_step\n";); - return true; - } - TRACE("grobner", tout << "continue compute_basis_loop\n";); - } - TRACE("grobner", tout << "return false from compute_basis_loop\n";); - TRACE("grobner_stats", print_stats(tout);); - return false; -} - -// return true iff cannot pick_next() -bool grobner_core::compute_basis_step() { - equation* eq = pick_next(); - if (!eq) { - TRACE("grobner", tout << "cannot pick an equation\n";); - return true; - } - m_stats.m_compute_steps++; - simplify_eq_by_using_to_superpose(*eq); - if (equation_is_too_complex(eq)) { - return false; - } - if (!simplify_to_superpose_with_eq(eq)) { - return false; - } - TRACE("grobner", tout << "eq = "; display_equation(tout, *eq);); - superpose(eq); - if (equation_is_too_complex(eq)) { - TRACE("grobner", display_equation(tout, *eq) << " is too complex: deleting it\n;";); - del_equation(eq); - return false; - } - insert_to_superpose(eq); - simplify_m_to_simplify(eq); - TRACE("grobner", tout << "end of iteration:\n"; display(tout);); - return false; -} - -grobner_core::equation* grobner_core::pick_next() { - equation* r = nullptr; - ptr_buffer to_delete; - for (equation* curr : m_to_simplify) { - if (is_trivial(curr)) - to_delete.push_back(curr); - else if (is_simpler(curr, r)) { - TRACE("grobner", tout << "preferring " << *(curr->expr()) << "\n";);; - r = curr; - } - } - for (equation* e : to_delete) - del_equation(e); - if (r) - m_to_simplify.erase(r); - TRACE("grobner", tout << "selected equation: "; if (!r) tout << "\n"; else tout << *r->expr() << "\n";); - return r; -} - -void grobner_core::simplify_eq_by_using_to_superpose(equation& eq) { - bool simplified; - TRACE("grobner", tout << "simplifying: "; display_equation(tout, eq); tout << "using equalities of m_to_superpose of size " << m_to_superpose.size() << "\n";); - do { - simplified = false; - for (equation* p : m_to_superpose) { - if (simplify_source_target(*p, eq)) { - simplified = true; - } - if (canceled() || eq.expr()->is_scalar()) { - break; - } - } - } while (simplified && !eq.expr()->is_scalar()); - - TRACE("grobner", - if (simplified) { tout << "simplification result: "; display_equation(tout, eq); } - else { tout << "no simplification\n"; }); -} - -concat grobner_core::equations() { - return concat(m_to_superpose, m_to_simplify); -} - -void grobner_core::reset() { - del_equations(0); - m_nex_creator.pop(0); - SASSERT(m_equations_to_delete.empty()); - m_to_superpose.reset(); - m_to_simplify.reset(); - m_stats.reset(); -} - -// Return true if the equation is of the form 0 = 0. -bool grobner_core::is_trivial(equation* eq) const { - return eq->expr()->is_scalar() && eq->expr()->to_scalar().value().is_zero(); -} - -// returns true if eq1 is simpler than eq2 -bool grobner_core::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.gt(eq2->expr(), eq1->expr()); -} - -void grobner_core::del_equation(equation * eq) { - m_to_superpose.erase(eq); - m_to_simplify.erase(eq); - SASSERT(m_equations_to_delete[eq->m_bidx] == eq); - m_equations_to_delete[eq->m_bidx] = nullptr; - dealloc(eq); -} - -const nex* grobner_core::get_highest_monomial(const nex* e) const { - switch (e->type()) { - case expr_type::MUL: - return e; - case expr_type::SUM: - return e->to_sum()[0]; - case expr_type::VAR: - return e; - default: - TRACE("grobner", tout << *e << "\n";); - return nullptr; - } -} - -// source 3f + k + l = 0, so f = (-k - l)/3 -// target 2fg + 3fp + e = 0 -// target is replaced by 2(-k/3 - l/3)g + 3(-k/3 - l/3)p + e = -2/3kg -2/3lg - kp -lp + e - -bool grobner_core::simplify_target_monomials(equation const& source, equation& target) { - nex const* high_mon = get_highest_monomial(source.expr()); - if (high_mon == nullptr) - return false; - SASSERT(high_mon->all_factors_are_elementary()); - TRACE("grobner_d", tout << "source = "; display_equation(tout, source) << "target = "; display_equation(tout, target) << "high_mon = " << *high_mon << "\n";); - - nex * te = target.m_expr; - nex_sum * targ_sum; - if (te->is_sum()) { - targ_sum = to_sum(te); - } else if (te->is_mul()) { - targ_sum = m_nex_creator.mk_sum(te); - } else { - TRACE("grobner_d", tout << "return false\n";); - return false; - } - - return simplify_target_monomials_sum(source, target, *targ_sum, *high_mon); -} - -unsigned grobner_core::find_divisible(nex_sum const& targ_sum, const nex& high_mon) const { - unsigned j = 0; - for (auto t : targ_sum) { - if (divide_ignore_coeffs_check_only(*t, high_mon)) { - TRACE("grobner_d", tout << "yes div: " << *t << " / " << high_mon << "\n";); - return j; - } - ++j; - } - TRACE("grobner_d", tout << "no div: " << targ_sum << " / " << high_mon << "\n";); - return -1; -} - -bool grobner_core::simplify_target_monomials_sum(equation const& source, - equation& target, nex_sum& targ_sum, - const nex& high_mon) { - unsigned j = find_divisible(targ_sum, high_mon); - if (j + 1 == 0) - return false; - m_changed_leading_term = (j == 0); - unsigned targ_orig_size = targ_sum.size(); - simplify_target_monomials_sum_j(source, target, targ_sum, high_mon, j, false); // false to avoid divisibility test - for (j++; j < targ_orig_size; j++) { - simplify_target_monomials_sum_j(source, target, targ_sum, high_mon, j, true); - } - - TRACE("grobner_d", tout << "targ_sum = " << targ_sum << "\n";); - target.m_expr = m_nex_creator.simplify(&targ_sum); - target.m_dep = m_dep_manager.mk_join(source.dep(), target.dep()); - TRACE("grobner_d", tout << "target = "; display_equation(tout, target);); - - return true; -} - -bool grobner_core::divide_ignore_coeffs_check_only_nex_mul(nex_mul const& t, const nex& h) const { - TRACE("grobner_d", tout << "t = " << t << ", h=" << h << "\n";); - SASSERT(m_nex_creator.is_simplified(t) && m_nex_creator.is_simplified(h)); - unsigned j = 0; // points to t - for(unsigned k = 0; k < h.number_of_child_powers(); k++) { - lpvar h_var = h.get_child_exp(k)->to_var().var(); - bool p_swallowed = false; - for (; j < t.size() && !p_swallowed; j++) { - const nex_pow& tp = t[j]; - if (tp.e()->to_var().var() == h_var) { - if (tp.pow() >= h.get_child_pow(k)) { - p_swallowed = true; - } - } - } - if (!p_swallowed) { - TRACE("grobner_d", tout << "no div " << t << " / " << h << "\n";); - return false; - } - } - TRACE("grobner_d", tout << "division " << t << " / " << h << "\n";); - return true; -} - -// return true if h divides n -bool grobner_core::divide_ignore_coeffs_check_only(nex const& n , const nex& h) const { - if (n.is_mul()) - return divide_ignore_coeffs_check_only_nex_mul(n.to_mul(), h); - if (!n.is_var()) - return false; - - const nex_var& v = n.to_var(); - if (h.is_var()) { - return v.var() == h.to_var().var(); - } - - if (h.is_mul()) { - if (h.number_of_child_powers() > 1) - return false; - if (h.get_child_pow(0) != 1) - return false; - const nex* e = h.get_child_exp(0); - return e->is_var() && e->to_var().var() == v.var(); - } - - return false; -} - -nex_mul * grobner_core::divide_ignore_coeffs_perform_nex_mul(nex_mul const& t, const nex& h) { - - m_nex_creator.m_mk_mul.reset(); - - unsigned j = 0; // j points to t and k runs over h - for(unsigned k = 0; k < h.number_of_child_powers(); k++) { - lpvar h_var = to_var(h.get_child_exp(k))->var(); - for (; j < t.size(); j++) { - auto const &tp = t[j]; - if (tp.e()->to_var().var() == h_var) { - unsigned h_pow = h.get_child_pow(k); - SASSERT(tp.pow() >= h_pow); - j++; - if (tp.pow() > h_pow) { - m_nex_creator.m_mk_mul *= nex_pow(tp.e(), tp.pow() - h_pow); - } - break; - } else { - m_nex_creator.m_mk_mul *= tp; - } - } - } - for (; j < t.size(); j++) { - m_nex_creator.m_mk_mul *= t[j]; - } - - nex_mul* r = m_nex_creator.m_mk_mul.mk(); - TRACE("grobner", tout << "r = " << *r << " = " << t << " / " << h << "\n";); - TRACE("grobner_d", tout << "r = " << *r << " = " << t << " / " << h << "\n";); - return r; -} - -// perform the division t / h, but ignores the coefficients -// h does not change -nex_mul * grobner_core::divide_ignore_coeffs_perform(nex* e, const nex& h) { - if (e->is_mul()) - return divide_ignore_coeffs_perform_nex_mul(e->to_mul(), h); - SASSERT(e->is_var()); - return m_nex_creator.mk_mul(); // return the empty nex_mul -} - -// if targ_sum->children()[j] = c*high_mon*p, -// and b*high_mon + e = 0, so high_mon = -e/b -// then targ_sum->children()[j] = - (c/b) * e*p - - -void grobner_core::simplify_target_monomials_sum_j(equation const& source, equation& target, nex_sum& targ_sum, const nex& high_mon, unsigned j, bool test_divisibility) { - nex * ej = targ_sum[j]; - TRACE("grobner_d", tout << "high_mon = " << high_mon << ", ej = " << *ej << "\n";); - if (test_divisibility && !divide_ignore_coeffs_check_only(*ej, high_mon)) { - TRACE("grobner_d", tout << "no div\n";); - return; - } - nex_mul * ej_over_high_mon = divide_ignore_coeffs_perform(ej, high_mon); - TRACE("grobner_d", tout << "ej_over_high_mon = " << *ej_over_high_mon << "\n";); - rational c = ej->is_mul() ? to_mul(ej)->coeff() : rational(1); - TRACE("grobner_d", tout << "c = " << c << "\n";); - - nex_creator::sum_factory sf(m_nex_creator); - add_mul_skip_first(sf ,-c/high_mon.coeff(), source.expr(), ej_over_high_mon); - - targ_sum[j] = sf.mk(); - TRACE("grobner_d", tout << "targ_sum = " << targ_sum << "\n";); -} - -// return true iff simplified - -bool grobner_core::simplify_source_target(equation const& source, equation& target) { - TRACE("grobner", tout << "simplifying: "; display_equation(tout, target); tout << "\nusing: "; display_equation(tout, source);); - TRACE("grobner_d", tout << "simplifying: " << *(target.expr()) << " using " << *(source.expr()) << "\n";); - SASSERT(m_nex_creator.is_simplified(*source.expr()) && !equation_is_too_complex(&source)); - if (equation_is_too_complex(&target)) - return false; - SASSERT(m_nex_creator.is_simplified(*target.expr())); - if (target.expr()->is_scalar()) { - TRACE("grobner_d", tout << "no simplification\n";); - return false; - } - if (source.get_num_monomials() == 0) { - TRACE("grobner_d", tout << "no simplification\n";); - return false; - } - m_stats.m_simplified++; - bool result = false; - while (!canceled() && simplify_target_monomials(source, target)) { - TRACE("grobner", tout << "simplified target = "; display_equation(tout, target) << "\n";); - result = true; - } - if (result) { - target.m_dep = m_dep_manager.mk_join(target.dep(), source.dep()); - update_stats_max_degree_and_size(&target); - TRACE("grobner", tout << "simplified "; display_equation(tout, target) << "\n";); - TRACE("grobner_d", tout << "simplified to " << *(target.expr()) << "\n";); - return true; - } - TRACE("grobner_d", tout << "no simplification\n";); - return false; -} - -void grobner_core::process_simplified_target(equation* target, ptr_buffer& to_remove) { - if (is_trivial(target) || equation_is_too_complex(target)) { - to_remove.push_back(target); - } else if (m_changed_leading_term) { - insert_to_simplify(target); - to_remove.push_back(target); - } -} - - -bool grobner_core::simplify_to_superpose_with_eq(equation* eq) { - TRACE("grobner_d", tout << "eq->exp " << *(eq->expr()) << "\n";); - SASSERT(!equation_is_too_complex(eq)); - ptr_buffer to_remove; - ptr_buffer to_delete; - for (equation * target : m_to_superpose) { - if (canceled() || done()) - break; - m_changed_leading_term = false; - // if the leading term is simplified, then the equation has to be moved to m_to_simplify - if (simplify_source_target(*eq, *target)) { - process_simplified_target(target, to_remove); - } - if (is_trivial(target)||equation_is_too_complex(target)) { - to_delete.push_back(target); - } - else { - SASSERT(m_nex_creator.is_simplified(*target->expr())); - } - } - - for (equation* eq : to_remove) - m_to_superpose.erase(eq); - for (equation* eq : to_delete) - del_equation(eq); - return !canceled(); -} - -/* - Use the given equation to simplify m_to_simplify equations -*/ -void grobner_core::simplify_m_to_simplify(equation* eq) { - TRACE("grobner_d", tout << "eq->exp " << *(eq->expr()) << "\n";); - ptr_buffer to_delete; - for (equation* target : m_to_simplify) { - if (simplify_source_target(*eq, *target) && (is_trivial(target) || equation_is_too_complex(target))) - to_delete.push_back(target); - } - for (equation* eq : to_delete) - del_equation(eq); -} - -// if e is the sum then add to r all children of e multiplied by beta, except the first one -// which corresponds to the highest monomial, -// otherwise do nothing -void grobner_core::add_mul_skip_first(nex_creator::sum_factory& sf, const rational& beta, nex const*e, nex_mul* c) { - if (e->is_sum()) { - nex_sum const & es = e->to_sum(); - for (unsigned j = 1; j < es.size(); j++) { - sf += m_nex_creator.mk_mul(beta, es[j], c); - } - } else { - TRACE("grobner_d", tout << "e = " << *e << "\n";); - } -} - -// let e1: alpha*ab+q=0, and e2: beta*ac+e=0, then beta*qc - alpha*eb = 0 -nex * grobner_core::expr_superpose(nex const* e1, nex const* e2, const nex* ab, const nex* ac, nex_mul* b, nex_mul* c) { - TRACE("grobner", tout << "e1 = " << *e1 << "\ne2 = " << *e2 <<"\n";); - nex_creator::sum_factory sf(m_nex_creator); - rational alpha = - ab->coeff(); - TRACE("grobner", tout << "e2 *= " << alpha << "*(" << *b << ")\n";); - add_mul_skip_first(sf, alpha, e2, b); - rational beta = ac->coeff(); - TRACE("grobner", tout << "e1 *= " << beta << "*(" << *c << ")\n";); - add_mul_skip_first(sf, beta, e1, c); - nex * ret = m_nex_creator.simplify(sf.mk()); - TRACE("grobner", tout << "e1 = " << *e1 << "\ne2 = " << *e2 <<"\nsuperpose = " << *ret << "\n";); - CTRACE("grobner", ret->is_scalar(), tout << "\n";); - return ret; -} - -// let eq1: ab+q=0, and eq2: ac+e=0, then qc - eb = 0 -void grobner_core::superpose(equation * eq1, equation * eq2) { - TRACE("grobner_d", tout << "eq1="; display_equation(tout, *eq1) << "eq2="; display_equation(tout, *eq2);); - const nex * ab = get_highest_monomial(eq1->expr()); - const nex * ac = get_highest_monomial(eq2->expr()); - nex_mul *b = nullptr, *c = nullptr; - TRACE("grobner_d", tout << "ab="; if(ab) { tout << *ab; } else { tout << "null"; }; - tout << " , " << " ac="; if(ac) { tout << *ac; } else { tout << "null"; }; tout << "\n";); - if (!find_b_c(ab, ac, b, c)) { - TRACE("grobner_d", tout << "there is no non-trivial common divider, no superposing\n";); - return; - } - equation* eq = alloc(equation); - TRACE("grobner_d", tout << "eq1="; display_equation(tout, *eq1) << "eq2="; display_equation(tout, *eq2);); - 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.gt(eq->expr(), eq1->expr()) || m_nex_creator.gt(eq->expr(), eq2->expr()) || - equation_is_too_complex(eq)) { - TRACE("grobner", display_equation(tout, *eq) << " is too complex: deleting it\n;";); - del_equation(eq); - } else { - m_stats.m_superposed++; - update_stats_max_degree_and_size(eq); - insert_to_simplify(eq); - } -} - - - -// Let a be the greatest common divider of ab and bc, -// then ab/a is stored in b, and ac/a is stored in c -bool grobner_core::find_b_c(const nex* ab, const nex* ac, nex_mul*& b, nex_mul*& c) { - if (!find_b_c_check_only(ab, ac)) - return false; - nex_creator::mul_factory fb(m_nex_creator), fc(m_nex_creator); - unsigned ab_size = ab->number_of_child_powers(); - unsigned ac_size = ac->number_of_child_powers(); - unsigned i = 0, j = 0; - for (;;) { - const nex* m = ab->get_child_exp(i); - const nex* n = ac->get_child_exp(j); - if (m_nex_creator.gt(m, n)) { - fb *= nex_pow(const_cast(m), ab->get_child_pow(i)); - if (++i == ab_size) - break; - } else if (m_nex_creator.gt(n, m)) { - fc *= nex_pow(const_cast(n), ac->get_child_pow(j)); - if (++j == ac_size) - break; - } else { - unsigned b_pow = ab->get_child_pow(i); - unsigned c_pow = ac->get_child_pow(j); - if (b_pow > c_pow) { - fb *= nex_pow(const_cast(m), b_pow - c_pow); - } else if (c_pow > b_pow) { - fc *= nex_pow(const_cast(n), c_pow - b_pow); - } // otherwise the power are equal and no child added to either b or c - i++; j++; - - if (i == ab_size || j == ac_size) { - break; - } - } - } - while (i != ab_size) { - fb *= nex_pow(const_cast(ab->get_child_exp(i)), ab->get_child_pow(i)); - i++; - } - while (j != ac_size) { - fc *= nex_pow(const_cast(ac->get_child_exp(j)), ac->get_child_pow(j)); - j++; - } - b = fb.mk(); - c = fc.mk(); - TRACE("nla_grobner", tout << "b=" << *b << ", c=" <<*c << "\n";); - SASSERT(test_find_b_c(ab, ac, b, c)); - return true; -} - -// Finds out if ab and bc have a non-trivial common divider -bool grobner_core::find_b_c_check_only(const nex* ab, const nex* ac) const { - if (ab == nullptr || ac == nullptr) - return false; - SASSERT(m_nex_creator.is_simplified(*ab) && m_nex_creator.is_simplified(*ac)); - unsigned i = 0, j = 0; // i points to ab, j points to ac - for (;;) { - const nex* m = ab->get_child_exp(i); - const nex* n = ac->get_child_exp(j); - if (m_nex_creator.gt(m , n)) { - i++; - if (i == ab->number_of_child_powers()) - return false; - } else if (m_nex_creator.gt(n, m)) { - j++; - if (j == ac->number_of_child_powers()) - return false; - } else { - TRACE("grobner", tout << "found common " << *m << "\n";); - return true; - } - } - - TRACE("grobner", tout << "not found common " << " in " << *ab << " and " << *ac << "\n";); - return false; -} - -void grobner_core::superpose(equation * eq) { - for (equation * target : m_to_superpose) { - superpose(eq, target); - } -} - -bool grobner_core::canceled() { - return m_limit.get_cancel_flag(); -} - -bool grobner_core::done() { - return num_of_equations() >= m_params.m_grobner_eqs_threshold || canceled(); -} - -void grobner_core::del_equations(unsigned old_size) { - TRACE("grobner", ); - SASSERT(m_equations_to_delete.size() >= old_size); - for (unsigned i = m_equations_to_delete.size(); i-- > old_size; ) { - equation* eq = m_equations_to_delete[i]; - if (eq) - del_equation(eq); - } - m_equations_to_delete.shrink(old_size); -} - -std::ostream& grobner_core::print_stats(std::ostream & out) const { - return out << "stats:\nsteps = " << m_stats.m_compute_steps << "\nsimplified: " << - m_stats.m_simplified << "\nsuperposed: " << - m_stats.m_superposed << "\nexpr degree: " << m_stats.m_max_expr_degree << - "\nexpr size: " << m_stats.m_max_expr_size << "\n"; -} - -void grobner_core::update_stats_max_degree_and_size(const equation *e) { - if (m_stats.m_max_expr_size < e->expr()->size()) { - TRACE("grobner_stats_d", tout << "expr size = " << e->expr()->size() << "\n";); - TRACE("grobner_stats_d", display_equation(tout, *e);); - - m_stats.m_max_expr_size = e->expr()->size(); - } - auto deg = e->expr()->get_degree(); - if (m_stats.m_max_expr_degree < deg) { - TRACE("grobner_stats_d", tout << "expr degree = " << deg << "\n";); - m_stats.m_max_expr_degree = deg; - } -} - -void grobner_core::display_equations(std::ostream & out, equation_set const & v, char const * header) const { - out << header << "\n"; - for (const equation* e : v) - display_equation(out, *e); -} - -void grobner_core::display_equations_no_deps(std::ostream & out, equation_set const & v, char const * header) const { - out << header << "\n"; - for (const equation* e : v) - out << *(e->expr()) << "\n"; -} - -std::ostream& grobner_core::display_equation(std::ostream & out, const equation & eq) const { - out << "expr = " << *eq.expr() << "\n"; - return display_dependency(out, eq.dep()); -} - -std::ostream& grobner_core::display(std::ostream& out) const { - display_equations_no_deps(out, m_to_superpose, "m_to_superpose:"); - display_equations_no_deps(out, m_to_simplify, "m_to_simplify:"); - return out; -} - -void grobner_core::assert_eq_0(nex* e, u_dependency * dep) { - if (e == nullptr || is_zero_scalar(e)) - return; - equation * eq = alloc(equation); - init_equation(eq, e, dep); - TRACE("grobner", - display_equation(tout, *eq); - /*tout << "\nvars\n"; - for (unsigned j : get_vars_of_expr_with_opening_terms(e)) { - c().print_var(j, tout << "(") << ")\n"; - } */); - insert_to_simplify(eq); - update_stats_max_degree_and_size(eq); -} - -void grobner_core::init_equation(equation* eq, nex*e, u_dependency * dep) { - eq->m_bidx = m_equations_to_delete.size(); - eq->m_dep = dep; - eq->m_expr = e; - m_equations_to_delete.push_back(eq); - SASSERT(m_equations_to_delete[eq->m_bidx] == eq); -} - -grobner_core::~grobner_core() { - del_equations(0); -} - -std::ostream& grobner_core::display_dependency(std::ostream& out, u_dependency* dep) const { - svector expl; - m_dep_manager.linearize(dep, expl); - lp::explanation e(expl); - if (!expl.empty()) { - out << "constraints\n"; - m_print_explanation(e, out); - out << "\n"; - } else { - out << "no deps\n"; - } - return out; -} - -#ifdef Z3DEBUG -bool grobner_core::test_find_b(const nex* ab, const nex_mul* b) { - if (ab->is_var()) { - return b->size() == 0 || (b->get_degree() == 1 && b->get_child_exp(0)->to_var().var() == - ab->to_var().var()); - } - nex_mul& ab_clone = m_nex_creator.clone(ab)->to_mul(); - nex_mul * a= divide_ignore_coeffs_perform(&ab_clone, *b); - ab_clone.m_coeff = rational(1); - SASSERT(b->coeff().is_one()); - nex * m = m_nex_creator.mk_mul(a, m_nex_creator.clone(b)); - m = m_nex_creator.simplify(m); - return m_nex_creator.equal(m, &ab_clone); -} - -bool grobner_core::test_find_b_c(const nex* ab, const nex* ac, const nex_mul* b, const nex_mul* c) { - return test_find_b(ab, b) && test_find_b(ac, c); -} - -#endif diff --git a/src/math/lp/nla_grobner.h b/src/math/lp/nla_grobner.h deleted file mode 100644 index 81e429007..000000000 --- a/src/math/lp/nla_grobner.h +++ /dev/null @@ -1,224 +0,0 @@ -/*++ - Copyright (c) 2017 Microsoft Corporation - - Module Name: - - - - Abstract: - - - - Author: - Nikolaj Bjorner (nbjorner) - Lev Nachmanson (levnach) - - Revision History: - - - --*/ -#pragma once - -#include "math/lp/nla_common.h" -#include "math/lp/nex.h" -#include "math/lp/nex_creator.h" - -namespace nla { -class core; - -struct grobner_stats { - long m_simplified; - long m_superposed; - long m_compute_steps; - unsigned m_max_expr_size; - unsigned m_max_expr_degree; - void reset() { memset(this, 0, sizeof(grobner_stats)); } - grobner_stats() { reset(); } -}; - -template -class concat { - const A& m_a; // the first container - const B& m_b; // the second container -public: - class iterator { - const concat& m_c; - typename A::iterator m_a_it; - typename B::iterator m_b_it; - public: - iterator(const concat& c, bool begin): - m_c(c), m_a_it(begin? m_c.m_a.begin() : m_c.m_a.end()), m_b_it(begin? m_c.m_b.begin() : m_c.m_b.end()) {} - const C operator*() { return m_a_it != m_c.m_a.end() ? *m_a_it : *m_b_it; } - iterator& operator++() { - if (m_a_it != m_c.m_a.end()) - m_a_it++; - else - m_b_it++; - return *this; - } - iterator operator++(int) { iterator tmp = *this; ++*this; return tmp; } - bool operator==(iterator const& other) const { return m_a_it == other.m_a_it && m_b_it == other.m_b_it; } - bool operator!=(iterator const& other) const { return m_a_it != other.m_a_it || m_b_it != other.m_b_it; } - }; - - concat(const A& a, const B& b) : m_a(a), m_b(b) {} - iterator begin() { return iterator(*this, true); } - iterator end() { return iterator(*this, false); } - -}; - -class grobner_core { -public: - struct params { - unsigned m_grobner_eqs_threshold; - unsigned m_expr_size_limit; - }; - - class equation { - unsigned m_bidx; //!< position at m_equations_to_delete - nex * m_expr; // simplified expressionted monomials - u_dependency * m_dep; //!< justification for the equality - public: - unsigned get_num_monomials() const { - switch(m_expr->type()) { - case expr_type::VAR: return 1; - case expr_type::SCALAR: return 0; - case expr_type::MUL: return 1; - case expr_type::SUM: return m_expr->size(); - default: return 0; - } - } - // not guaranteed to return a nex_mul - nex const* get_monomial(unsigned idx) const { - switch(m_expr->type()) { - case expr_type::VAR: - case expr_type::SCALAR: UNREACHABLE();; - case expr_type::MUL: - SASSERT(idx == 0); - return m_expr; - case expr_type::SUM: - return m_expr->to_sum()[idx]; - default: return nullptr; - } - } - const nex* expr() const { return m_expr; } - u_dependency * dep() const { return m_dep; } - unsigned hash() const { return m_bidx; } - friend class grobner_core; - }; -private: - typedef obj_hashtable equation_set; - typedef ptr_vector equation_vector; - typedef std::function print_expl_t; - // fields - nex_creator& m_nex_creator; - reslimit& m_limit; - print_expl_t m_print_explanation; - equation_vector m_equations_to_delete; - grobner_stats m_stats; - equation_set m_to_superpose; - equation_set m_to_simplify; - region m_alloc; - mutable u_dependency_manager m_dep_manager; - nex_lt m_lt; - bool m_changed_leading_term; - params m_params; - -public: - grobner_core(nex_creator& nc, reslimit& lim) : - m_nex_creator(nc), - m_limit(lim), - m_dep_manager(), - m_changed_leading_term(false) - {} - - ~grobner_core(); - void reset(); - bool compute_basis_loop(); - void assert_eq_0(nex*, u_dependency * dep); - concat equations(); - u_dependency_manager& dep() const { return m_dep_manager; } - - void display_equations_no_deps(std::ostream& out, equation_set const& v, char const* header) const; - void display_equations(std::ostream& out, equation_set const& v, char const* header) const; - std::ostream& display_equation(std::ostream& out, const equation& eq) const; - std::ostream& display(std::ostream& out) const; - - void operator=(print_expl_t& pe) { m_print_explanation = pe; } - void operator=(params const& p) { m_params = p; } - -private: - bool compute_basis_step(); - - bool simplify_source_target(equation const& source, equation& target); - void simplify_eq_by_using_to_superpose(equation &); - bool simplify_target_monomials(equation const& source, equation& target); - void process_simplified_target(equation* target, ptr_buffer& to_remove); - bool simplify_to_superpose_with_eq(equation*); - void simplify_m_to_simplify(equation*); - equation* pick_next(); - bool canceled(); - void superpose(equation * eq1, equation * eq2); - void superpose(equation * eq); - 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_simpler(equation * eq1, equation * eq2); - void del_equations(unsigned old_size); - void del_equation(equation * eq); - void init_equation(equation* eq, nex*, u_dependency* d); - - void insert_to_simplify(equation *eq) { - TRACE("grobner", display_equation(tout, *eq);); - m_to_simplify.insert(eq); - } - void insert_to_superpose(equation *eq) { - SASSERT(m_nex_creator.is_simplified(*eq->expr())); - TRACE("grobner", display_equation(tout, *eq);); - m_to_superpose.insert(eq); - } - const nex * get_highest_monomial(const nex * e) const; - bool simplify_target_monomials_sum(equation const&, equation&, nex_sum&, const nex&); - unsigned find_divisible(nex_sum const&, const nex&) const; - void simplify_target_monomials_sum_j(equation const&, equation&, nex_sum&, const nex&, unsigned, bool); - bool divide_ignore_coeffs_check_only(nex const& , const nex&) const; - bool divide_ignore_coeffs_check_only_nex_mul(nex_mul const&, nex const&) const; - nex_mul * divide_ignore_coeffs_perform(nex* , const nex&); - nex_mul * divide_ignore_coeffs_perform_nex_mul(nex_mul const& , const nex&); - nex * expr_superpose(nex const* e1, nex const* e2, const nex* ab, const nex* ac, nex_mul* b, nex_mul* c); - void add_mul_skip_first(nex_creator::sum_factory& sf, const rational& beta, nex const*e, nex_mul* c); - bool done(); - unsigned num_of_equations() const { return m_to_simplify.size() + m_to_superpose.size(); } - void update_stats_max_degree_and_size(const equation*); - - std::ostream& print_stats(std::ostream&) const; - std::ostream& display_dependency(std::ostream& out, u_dependency*) const; - bool equation_is_too_complex(const equation* eq) const { - return eq->expr()->size() > m_params.m_expr_size_limit; - } -#ifdef Z3DEBUG - bool test_find_b_c(const nex* ab, const nex* ac, const nex_mul* b, const nex_mul* c); - bool test_find_b(const nex* ab, const nex_mul* b); -#endif -}; - -class grobner : common { - grobner_core m_gc; - unsigned m_reported; -public: - grobner(core *, intervals *); - void grobner_lemmas(); - ~grobner() {} -private: - void prepare_rows_and_active_vars(); - void add_var_and_its_factors_to_q_and_collect_new_rows(lpvar j, svector& q); - std::unordered_set get_vars_of_expr_with_opening_terms(const nex* e); - void display_matrix(std::ostream & out) const; - std::ostream& display(std::ostream& out) const { return m_gc.display(out); } -public: - void add_row(const vector> & row); - void check_eq(grobner_core::equation*); - void init(); - nex_creator& get_nex_creator() { return m_nex_creator; } -}; // end of grobner -} diff --git a/src/math/lp/nla_settings.h b/src/math/lp/nla_settings.h index 8f75466f8..c24ede8af 100644 --- a/src/math/lp/nla_settings.h +++ b/src/math/lp/nla_settings.h @@ -29,10 +29,7 @@ class nla_settings { unsigned m_horner_row_length_limit; // grobner fields bool m_run_grobner; - unsigned m_grobner_frequency; - unsigned m_grobner_eqs_threshold; unsigned m_grobner_row_length_limit; - unsigned m_grobner_expr_size_limit; public: nla_settings() : m_run_order(true), @@ -41,15 +38,9 @@ public: m_horner_frequency(4), m_horner_row_length_limit(10), m_run_grobner(true), - m_grobner_frequency(5), - m_grobner_eqs_threshold(512), - m_grobner_row_length_limit(10), - m_grobner_expr_size_limit(50) + m_grobner_row_length_limit(50) {} - unsigned grobner_eqs_threshold() const { return m_grobner_eqs_threshold; } - unsigned& grobner_eqs_threshold() { return m_grobner_eqs_threshold; } - bool run_order() const { return m_run_order; } bool& run_order() { return m_run_order; } @@ -65,9 +56,9 @@ public: unsigned& horner_row_length_limit() { return m_horner_row_length_limit; } bool run_grobner() const { return m_run_grobner; } - bool& run_grobner() { return m_run_grobner; } + bool& run_grobner() { return m_run_grobner; } unsigned grobner_row_length_limit() const { return m_grobner_row_length_limit; } - unsigned grobner_expr_size_limit() const { return m_grobner_expr_size_limit; } + unsigned& grobner_row_length_limit() { return m_grobner_row_length_limit; } }; } diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 89341a7f1..63e52eca1 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -453,7 +453,6 @@ class theory_lra::imp { m_nla->get_core()->m_nla_settings.horner_frequency() = nla.horner_frequency(); m_nla->get_core()->m_nla_settings.horner_row_length_limit() = nla.horner_row_length_limit(); m_nla->get_core()->m_nla_settings.run_grobner() = nla.grobner(); - m_nla->get_core()->m_nla_settings.grobner_eqs_threshold() = nla.grobner_eqs_threshold(); } }