diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp index 972324b17..3f406c70a 100644 --- a/src/math/lp/nla_grobner.cpp +++ b/src/math/lp/nla_grobner.cpp @@ -199,7 +199,6 @@ bool grobner_core::compute_basis_loop() { } TRACE("grobner", tout << "return false from compute_basis_loop\n";); TRACE("grobner_stats", print_stats(tout);); - set_gb_exhausted(); return false; } @@ -212,14 +211,13 @@ bool grobner_core::compute_basis_step() { } m_stats.m_compute_steps++; simplify_using_to_superpose(*eq); - if (canceled()) return false; - if (!simplify_to_superpose_with_eq(eq)) - return false; - TRACE("grobner", tout << "eq = "; display_equation(tout, *eq);); - superpose(eq); - insert_to_superpose(eq); - simplify_m_to_simplify(eq); - TRACE("grobner", tout << "end of iteration:\n"; display(tout);); + if (!canceled() && simplify_to_superpose_with_eq(eq)) { + TRACE("grobner", tout << "eq = "; display_equation(tout, *eq);); + superpose(eq); + insert_to_superpose(eq); + simplify_m_to_simplify(eq); + TRACE("grobner", tout << "end of iteration:\n"; display(tout);); + } return false; } @@ -241,6 +239,7 @@ grobner_core::equation* grobner_core::pick_next() { TRACE("grobner", tout << "selected equation: "; if (!r) tout << "\n"; else display_equation(tout, *r);); return r; } + grobner_core::equation_set const& grobner_core::equations() { m_all_eqs.reset(); for (auto e : m_to_simplify) m_all_eqs.insert(e); @@ -250,7 +249,7 @@ grobner_core::equation_set const& grobner_core::equations() { void grobner_core::reset() { del_equations(0); - SASSERT(m_equations_to_delete.size() == 0); + SASSERT(m_equations_to_delete.empty()); m_to_superpose.reset(); m_to_simplify.reset(); m_stats.reset(); @@ -317,15 +316,15 @@ const nex* grobner_core::get_highest_monomial(const nex* e) const { // 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 * source, equation * target) { +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->expr(); - nex_sum * targ_sum; + nex * te = target->m_expr; + nex_sum * targ_sum; if (te->is_sum()) { targ_sum = to_sum(te); } else if (te->is_mul()) { @@ -351,7 +350,7 @@ unsigned grobner_core::find_divisible(nex_sum const& targ_sum, const nex& high_m return -1; } -bool grobner_core::simplify_target_monomials_sum(equation * source, +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); @@ -364,13 +363,13 @@ bool grobner_core::simplify_target_monomials_sum(equation * source, simplify_target_monomials_sum_j(source, target, targ_sum, high_mon, j, true); } TRACE("grobner_d", tout << "targ_sum = " << *targ_sum << "\n";); - target->expr() = m_nex_creator.simplify(targ_sum); - target->dep() = m_dep_manager.mk_join(source->dep(), target->dep()); + 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 { +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 @@ -445,9 +444,7 @@ nex_mul * grobner_core::divide_ignore_coeffs_perform_nex_mul(nex_mul const& t, c } nex_mul* r = m_nex_creator.m_mk_mul.mk(); - TRACE("grobner", tout << "r = " << *r << " = " << t << " / " << h << "\n";); - - + TRACE("grobner", tout << "r = " << *r << " = " << t << " / " << h << "\n";); TRACE("grobner_d", tout << "r = " << *r << " = " << t << " / " << h << "\n";); return r; } @@ -465,7 +462,7 @@ nex_mul * grobner_core::divide_ignore_coeffs_perform(nex* e, const nex& h) { // 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 * source, equation *target, nex_sum* targ_sum, const nex& high_mon, unsigned j, bool test_divisibility) { +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)) { @@ -474,7 +471,7 @@ void grobner_core::simplify_target_monomials_sum_j(equation * source, equation * } 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); + 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); @@ -485,7 +482,7 @@ void grobner_core::simplify_target_monomials_sum_j(equation * source, equation * } // return true iff simplified -bool grobner_core::simplify_source_target(equation * source, equation * target) { +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())); @@ -510,7 +507,7 @@ bool grobner_core::simplify_source_target(equation * source, equation * target) } while (!canceled()); if (result) { - target->dep() = m_dep_manager.mk_join(target->dep(), source->dep()); + 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";); @@ -577,9 +574,9 @@ void grobner_core::simplify_m_to_simplify(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 *e, nex_mul* c) { +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 & es = e->to_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); } @@ -590,7 +587,7 @@ void grobner_core::add_mul_skip_first(nex_creator::sum_factory& sf, const ration // let e1: alpha*ab+q=0, and e2: beta*ac+e=0, then beta*qc - alpha*eb = 0 -nex * grobner_core::expr_superpose(nex* e1, nex* e2, const nex* ab, const nex* ac, nex_mul* b, nex_mul* c) { +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(); @@ -621,7 +618,7 @@ void grobner_core::superpose(equation * eq1, equation * eq2) { init_equation(eq, expr_superpose( eq1->expr(), eq2->expr(), ab, ac, b, c), m_dep_manager.mk_join(eq1->dep(), eq2->dep())); m_stats.m_superposed++; update_stats_max_degree_and_size(eq); - eq->expr() = m_nex_creator.simplify(eq->expr()); + eq->m_expr = m_nex_creator.simplify(eq->m_expr); insert_to_simplify(eq); } @@ -722,18 +719,12 @@ bool grobner_core::done() { return num_of_equations() >= m_grobner_eqs_threshold || canceled(); } -void grobner_core::set_gb_exhausted(){ - m_nl_gb_exhausted = true; -} void grobner_core::del_equations(unsigned old_size) { TRACE("grobner", ); SASSERT(m_equations_to_delete.size() >= old_size); - equation_vector::iterator it = m_equations_to_delete.begin(); - equation_vector::iterator end = m_equations_to_delete.end(); - it += old_size; - for (; it != end; ++it) { - equation * eq = *it; + for (unsigned i = m_equations_to_delete.size(); i-- > old_size; ) { + equation* eq = m_equations_to_delete[i]; if (eq) del_equation(eq); } @@ -772,7 +763,6 @@ std::ostream& grobner_core::display(std::ostream& out) const { void grobner_core::assert_eq_0(nex* e, common::ci_dependency * dep) { if (e == nullptr || is_zero_scalar(e)) return; - m_tmp_var_set.clear(); equation * eq = alloc(equation); init_equation(eq, e, dep); TRACE("grobner", @@ -786,8 +776,8 @@ void grobner_core::assert_eq_0(nex* e, common::ci_dependency * dep) { void grobner_core::init_equation(equation* eq, nex*e, common::ci_dependency * dep) { eq->m_bidx = m_equations_to_delete.size(); - eq->dep() = dep; - eq->expr() = e; + eq->m_dep = dep; + eq->m_expr = e; m_equations_to_delete.push_back(eq); SASSERT(m_equations_to_delete[eq->m_bidx] == eq); } diff --git a/src/math/lp/nla_grobner.h b/src/math/lp/nla_grobner.h index 0b04b032a..4e9d1ae25 100644 --- a/src/math/lp/nla_grobner.h +++ b/src/math/lp/nla_grobner.h @@ -41,7 +41,7 @@ public: class equation { unsigned m_bidx; //!< position at m_equations_to_delete nex * m_expr; // simplified expressionted monomials - common::ci_dependency * m_dep; //!< justification for the equality + common::ci_dependency * m_dep; //!< justification for the equality public: unsigned get_num_monomials() const { switch(m_expr->type()) { @@ -52,7 +52,7 @@ public: default: return 0; } } - // can return not a nex_mul + // not guaranteed to return a nex_mul nex const* get_monomial(unsigned idx) const { switch(m_expr->type()) { case expr_type::VAR: @@ -62,15 +62,12 @@ public: return m_expr; case expr_type::SUM: return m_expr->to_sum()[idx]; - default: return 0; + default: return nullptr; } } - nex* & expr() { return m_expr; } - const nex* expr() const { return m_expr; } + const nex* expr() const { return m_expr; } common::ci_dependency * dep() const { return m_dep; } - common::ci_dependency *& dep() { return m_dep; } unsigned hash() const { return m_bidx; } - friend class grobner; friend class grobner_core; }; private: @@ -85,9 +82,6 @@ private: grobner_stats m_stats; equation_set m_to_superpose; equation_set m_to_simplify; - bool m_nl_gb_exhausted; - ptr_vector m_allocated; - lp::int_set m_tmp_var_set; region m_alloc; common::ci_value_manager m_val_manager; mutable common::ci_dependency_manager m_dep_manager; @@ -99,7 +93,6 @@ public: grobner_core(nex_creator& nc, reslimit& lim, unsigned eqs_threshold) : m_nex_creator(nc), m_limit(lim), - m_nl_gb_exhausted(false), m_dep_manager(m_val_manager, m_alloc), m_changed_leading_term(false), m_grobner_eqs_threshold(eqs_threshold) @@ -120,14 +113,13 @@ public: private: bool compute_basis_step(); - bool simplify_source_target(equation * source, equation * target); + bool simplify_source_target(equation const* source, equation * target); void simplify_using_to_superpose(equation &); - bool simplify_target_monomials(equation * source, equation * target); + 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(); - void set_gb_exhausted(); bool canceled(); void superpose(equation * eq1, equation * eq2); void superpose(equation * eq); @@ -139,7 +131,6 @@ private: void del_equation(equation * eq); void init_equation(equation* eq, nex*, common::ci_dependency* d); - std::ostream& display_dependency(std::ostream& out, common::ci_dependency*) const; void insert_to_simplify(equation *eq) { TRACE("grobner", display_equation(tout, *eq);); m_to_simplify.insert(eq); @@ -150,19 +141,22 @@ private: m_to_superpose.insert(eq); } const nex * get_highest_monomial(const nex * e) const; - bool simplify_target_monomials_sum(equation *, equation *, nex_sum*, const nex&); + 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 *, equation *, nex_sum*, const nex&, unsigned, bool); + 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* e1, nex* 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 *e, nex_mul* c); + 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(); } - std::ostream& print_stats(std::ostream&) const; void update_stats_max_degree_and_size(const equation*); + + std::ostream& print_stats(std::ostream&) const; + std::ostream& display_dependency(std::ostream& out, common::ci_dependency*) const; + #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);