From 2fbb4cac9d910cadeee9d5b31b88b96d580b7093 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Fri, 13 Dec 2019 16:19:31 -1000 Subject: [PATCH] a fix in nex comparison and impovement of grobner stats Signed-off-by: Lev Nachmanson --- src/math/lp/nex_creator.h | 3 +- src/math/lp/nla_grobner.cpp | 70 +++++++++++++++++-------------------- src/math/lp/nla_grobner.h | 16 +++++---- 3 files changed, 43 insertions(+), 46 deletions(-) diff --git a/src/math/lp/nex_creator.h b/src/math/lp/nex_creator.h index b24348668..0caa51f9e 100644 --- a/src/math/lp/nex_creator.h +++ b/src/math/lp/nex_creator.h @@ -88,8 +88,9 @@ public: return wj != wk ? wj > wk : j > k; } + // just compare the underlying expressions 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())); + return gt(a.e(), b.e()); } void simplify_children_of_mul(vector & children, rational&); diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp index 6a766efe0..44b956d1f 100644 --- a/src/math/lp/nla_grobner.cpp +++ b/src/math/lp/nla_grobner.cpp @@ -32,20 +32,11 @@ grobner::grobner(core *c, intervals *s) void grobner::grobner_lemmas() { c().lp_settings().stats().m_grobner_calls++; - init(); - ptr_vector eqs; - unsigned next_weight = - (unsigned)(var_weight::MAX_DEFAULT_WEIGHT) + 1; // next weight using during perturbation phase. - do { - TRACE("grobner", tout << "before:\n"; display(tout);); - compute_basis(); - update_statistics(); - TRACE("grobner", tout << "after:\n"; display(tout);); - // if (find_conflict(eqs)) - // return; - } while (push_calculation_forward(eqs, next_weight)); + TRACE("grobner", tout << "before:\n"; display(tout);); + compute_basis(); + TRACE("grobner", tout << "after:\n"; display(tout);); } bool grobner::internalize_gb_eq(equation* ) { @@ -141,6 +132,7 @@ void grobner::add_row(unsigned i) { } void grobner::init() { + m_reported = 0; del_equations(0); SASSERT(m_equations_to_delete.size() == 0); @@ -417,7 +409,7 @@ bool grobner::simplify_source_target(equation * source, equation * target) { TRACE("grobner_d", tout << "no simplification\n";); return false; } - m_stats.m_simplify++; + m_stats.m_simplified++; bool result = false; do { if (simplify_target_monomials(source, target)) { @@ -429,6 +421,7 @@ bool grobner::simplify_source_target(equation * source, equation * target) { } while (!canceled()); if (result) { target->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; @@ -548,12 +541,9 @@ void 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.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 { - insert_to_simplify(eq); - } + m_stats.m_superposed++; + update_stats_max_degree_and_size(eq); + insert_to_simplify(eq); } void grobner::register_report() { @@ -603,6 +593,10 @@ bool grobner::find_b_c(const nex* ab, const nex* ac, nex_mul*& b, nex_mul*& c) { j++; } TRACE("nla_grobner", tout << "b=" << *b << ", c=" <<*c << "\n";); + // debug region + nex_mul *a = divide_ignore_coeffs_perform(m_nex_creator.clone(ab), b); + SASSERT(ab->get_degree() == a->get_degree() + b->get_degree()); + SASSERT(ac->get_degree() == a->get_degree() + c->get_degree()); return true; } @@ -646,7 +640,7 @@ bool grobner::compute_basis_step() { TRACE("grobner", tout << "cannot pick an equation\n";); return true; } - m_stats.m_num_processed++; + m_stats.m_compute_steps++; equation * new_eq = simplify_using_to_superpose(eq); if (new_eq != nullptr && eq != new_eq) { // equation was updated using non destructive updates @@ -683,7 +677,8 @@ void grobner::compute_basis(){ } } void grobner::compute_basis_init(){ - c().lp_settings().stats().m_grobner_basis_computatins++; + c().lp_settings().stats().m_grobner_basis_computatins++; + m_stats.reset(); } bool grobner::canceled() const { @@ -700,15 +695,19 @@ bool grobner::done() const { canceled() || m_reported > 0; } + bool grobner::compute_basis_loop(){ while (!done()) { if (compute_basis_step()) { TRACE("grobner", tout << "progress in compute_basis_step\n";); + TRACE("grobner_stats", print_stats(tout);); return true; } TRACE("grobner", tout << "continue compute_basis_loop\n";); + TRACE("grobner_stats", print_stats(tout);); } TRACE("grobner", tout << "return false from compute_basis_loop\n";); + TRACE("grobner_stats", print_stats(tout);); return false; } @@ -716,23 +715,6 @@ void grobner::set_gb_exhausted(){ m_nl_gb_exhausted = true; } -void grobner::update_statistics(){ - /* todo : implement - m_stats.m_gb_simplify += gb.m_stats.m_simplify; - m_stats.m_gb_superpose += gb.m_stats.m_superpose; - m_stats.m_gb_num_to_superpose += gb.m_stats.m_num_to_superpose; - m_stats.m_gb_compute_basis++;*/ -} - -bool grobner::push_calculation_forward(ptr_vector& eqs, unsigned & next_weight) { - return (!m_nl_gb_exhausted) && - try_to_modify_eqs(eqs, next_weight); -} - -bool grobner::try_to_modify_eqs(ptr_vector& eqs, unsigned& next_weight) { - // NOT_IMPLEMENTED_YET(); - return false; -} void grobner:: del_equations(unsigned old_size) { TRACE("grobner", ); @@ -748,6 +730,18 @@ void grobner:: del_equations(unsigned old_size) { m_equations_to_delete.shrink(old_size); } +std::ostream& grobner::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::update_stats_max_degree_and_size(const equation *e) { + m_stats.m_max_expr_size = std::max(m_stats.m_max_expr_size, e->expr()->size()); + m_stats.m_max_expr_degree = std::max(m_stats.m_max_expr_degree, e->expr()->get_degree()); +} + void grobner::display_equations(std::ostream & out, equation_set const & v, char const * header) const { out << header << "\n"; for (const equation* e : v) diff --git a/src/math/lp/nla_grobner.h b/src/math/lp/nla_grobner.h index b8c63f497..749e2f471 100644 --- a/src/math/lp/nla_grobner.h +++ b/src/math/lp/nla_grobner.h @@ -28,10 +28,11 @@ namespace nla { class core; struct grobner_stats { - long m_simplify; - long m_superpose; - long m_compute_basis; - long m_num_processed; + 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(); } }; @@ -101,8 +102,6 @@ private: void add_var_and_its_factors_to_q_and_collect_new_rows(lpvar j, std::queue& q); void init(); void compute_basis(); - void update_statistics(); - bool push_calculation_forward(ptr_vector& eqs, unsigned&); void compute_basis_init(); bool compute_basis_loop(); bool compute_basis_step(); @@ -128,7 +127,6 @@ private: void display_matrix(std::ostream & out) const; std::ostream& display(std::ostream & out) const; - bool try_to_modify_eqs(ptr_vector& eqs, unsigned& next_weight); bool internalize_gb_eq(equation*); void add_row(unsigned); void assert_eq_0(nex*, ci_dependency * dep); @@ -161,5 +159,9 @@ private: void register_report(); std::unordered_set get_vars_of_expr_with_opening_terms(const nex *e ); unsigned num_of_equations() const { return m_to_simplify.size() + m_to_superpose.size(); } + std::ostream& print_stats(std::ostream&) const; + template + std::ostream& print_stats_eqs(T&, std::ostream&) const; + void update_stats_max_degree_and_size(const equation *e); }; // end of grobner }