From c2235ef96f286ad751e863ffb9cec28a18e9ff75 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 22 Oct 2019 10:36:31 -0700 Subject: [PATCH] port Grobner Signed-off-by: Lev Nachmanson --- src/math/grobner/grobner.cpp | 72 ++++++++++++++++++------------------ src/math/grobner/grobner.h | 4 +- src/math/lp/nla_grobner.cpp | 34 ++++++++--------- src/math/lp/nla_grobner.h | 8 ++-- 4 files changed, 59 insertions(+), 59 deletions(-) diff --git a/src/math/grobner/grobner.cpp b/src/math/grobner/grobner.cpp index 183b7dd59..4dc6d5ffc 100644 --- a/src/math/grobner/grobner.cpp +++ b/src/math/grobner/grobner.cpp @@ -56,8 +56,8 @@ void grobner::del_equations(unsigned old_size) { } void grobner::del_equation(equation * eq) { - m_processed.erase(eq); - m_to_process.erase(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] = 0; del_monomials(eq->m_monomials); @@ -85,15 +85,15 @@ void grobner::unfreeze_equations(unsigned old_size) { it += old_size; for (; it != end; ++it) { equation * eq = *it; - m_to_process.insert(eq); + m_to_simplify.insert(eq); } m_equations_to_unfreeze.shrink(old_size); } void grobner::reset() { flush(); - m_processed.reset(); - m_to_process.reset(); + m_to_superpose.reset(); + m_to_simplify.reset(); m_equations_to_unfreeze.reset(); m_equations_to_delete.reset(); m_unsat = nullptr; @@ -172,8 +172,8 @@ void grobner::display_equations(std::ostream & out, equation_set const & v, char } void grobner::display(std::ostream & out) const { - display_equations(out, m_processed, "processed:"); - display_equations(out, m_to_process, "to process:"); + display_equations(out, m_to_superpose, "processed:"); + display_equations(out, m_to_simplify, "to process:"); } void grobner::set_weight(expr * n, int weight) { @@ -205,7 +205,7 @@ void grobner::update_order(equation_set & s, bool processed) { if (update_order(eq)) { if (processed) { to_remove.push_back(eq); - m_to_process.insert(eq); + m_to_simplify.insert(eq); } } } @@ -214,8 +214,8 @@ void grobner::update_order(equation_set & s, bool processed) { } void grobner::update_order() { - update_order(m_to_process, false); - update_order(m_processed, true); + update_order(m_to_simplify, false); + update_order(m_to_superpose, true); } bool grobner::var_lt::operator()(expr * v1, expr * v2) const { @@ -314,7 +314,7 @@ void grobner::assert_eq_0(unsigned num_monomials, monomial * const * monomials, equation * eq = alloc(equation); eq->m_monomials.swap(ms); init_equation(eq, ex); - m_to_process.insert(eq); + m_to_simplify.insert(eq); } } @@ -330,7 +330,7 @@ void grobner::assert_eq_0(unsigned num_monomials, rational const * coeffs, expr normalize_coeff(ms); \ eq->m_monomials.swap(ms); \ init_equation(eq, ex); \ - m_to_process.insert(eq); \ + m_to_simplify.insert(eq); \ } MK_EQ(coeffs[i]); @@ -380,7 +380,7 @@ void grobner::assert_monomial_tautology(expr * m) { eq->m_monomials.push_back(m1); normalize_coeff(eq->m_monomials); init_equation(eq, static_cast(nullptr)); \ - m_to_process.insert(eq); + m_to_simplify.insert(eq); } /** @@ -653,10 +653,10 @@ grobner::equation * grobner::simplify_source_target(equation const * source, equ grobner::equation * grobner::simplify_using_processed(equation * eq) { bool result = false; bool simplified; - TRACE("grobner", tout << "simplifying: "; display_equation(tout, *eq); tout << "using already processed equalities of size " << m_processed.size() << "\n";); + TRACE("grobner", tout << "simplifying: "; display_equation(tout, *eq); tout << "using already processed equalities of size " << m_to_superpose.size() << "\n";); do { simplified = false; - for (equation const* p : m_processed) { + for (equation const* p : m_to_superpose) { equation * new_eq = simplify_source_target(p, eq); if (new_eq) { result = true; @@ -696,7 +696,7 @@ bool grobner::is_better_choice(equation * eq1, equation * eq2) { grobner::equation * grobner::pick_next() { equation * r = nullptr; ptr_buffer to_delete; - for (equation * curr : m_to_process) { + for (equation * curr : m_to_simplify) { if (is_trivial(curr)) to_delete.push_back(curr); else if (is_better_choice(curr, r)) @@ -705,7 +705,7 @@ grobner::equation * grobner::pick_next() { for (equation * e : to_delete) del_equation(e); if (r) - m_to_process.erase(r); + m_to_simplify.erase(r); TRACE("grobner", tout << "selected equation: "; if (!r) tout << "\n"; else display_equation(tout, *r);); return r; } @@ -715,7 +715,7 @@ void grobner::process_simplified_target(ptr_buffer& to_insert, equatio m_equations_to_unfreeze.push_back(target); to_remove.push_back(target); if (m_changed_leading_term) { - m_to_process.insert(new_target); + m_to_simplify.insert(new_target); to_remove.push_back(target); } else { @@ -725,7 +725,7 @@ void grobner::process_simplified_target(ptr_buffer& to_insert, equatio } else { if (m_changed_leading_term) { - m_to_process.insert(target); + m_to_simplify.insert(target); to_remove.push_back(target); } } @@ -737,12 +737,12 @@ bool grobner::simplify_processed_with_eq(equation * eq) { ptr_buffer to_insert; ptr_buffer to_remove; ptr_buffer to_delete; - equation_set::iterator it = m_processed.begin(); - equation_set::iterator end = m_processed.end(); + equation_set::iterator it = m_to_superpose.begin(); + equation_set::iterator end = m_to_superpose.end(); for (; it != end && !m_manager.canceled(); ++it) { equation * target = *it; m_changed_leading_term = false; - // if the leading term is simplified, then the equation has to be moved to m_to_process + // if the leading term is simplified, then the equation has to be moved to m_to_simplify equation * new_target = simplify_source_target(eq, target); if (new_target != nullptr) { process_simplified_target(to_insert, new_target, target, to_remove); @@ -751,9 +751,9 @@ bool grobner::simplify_processed_with_eq(equation * eq) { to_delete.push_back(target); } for (equation* eq : to_insert) - m_processed.insert(eq); + m_to_superpose.insert(eq); for (equation* eq : to_remove) - m_processed.erase(eq); + m_to_superpose.erase(eq); for (equation* eq : to_delete) del_equation(eq); return !m_manager.canceled(); @@ -766,7 +766,7 @@ void grobner::simplify_to_process(equation * eq) { ptr_buffer to_insert; ptr_buffer to_remove; ptr_buffer to_delete; - for (equation* target : m_to_process) { + for (equation* target : m_to_simplify) { equation * new_target = simplify_source_target(eq, target); if (new_target != nullptr && new_target != target) { m_equations_to_unfreeze.push_back(target); @@ -778,9 +778,9 @@ void grobner::simplify_to_process(equation * eq) { to_delete.push_back(target); } for (equation* eq : to_insert) - m_to_process.insert(eq); + m_to_simplify.insert(eq); for (equation* eq : to_remove) - m_to_process.erase(eq); + m_to_simplify.erase(eq); for (equation* eq : to_delete) del_equation(eq); } @@ -860,15 +860,15 @@ void grobner::superpose(equation * eq1, equation * eq2) { new_eq->m_monomials.swap(new_monomials); init_equation(new_eq, m_dep_manager.mk_join(eq1->m_dep, eq2->m_dep)); new_eq->m_lc = false; - m_to_process.insert(new_eq); + m_to_simplify.insert(new_eq); } } /** - \brief Superpose the given equations with the equations in m_processed. + \brief Superpose the given equations with the equations in m_to_superpose. */ void grobner::superpose(equation * eq) { - for (equation * target : m_processed) { + for (equation * target : m_to_superpose) { superpose(eq, target); } } @@ -884,8 +884,8 @@ bool grobner::compute_basis_step() { return true; m_stats.m_num_processed++; #ifdef PROFILE_GB - if (m_stats.m_num_processed % 100 == 0) { - verbose_stream() << "[grobner] " << m_processed.size() << " " << m_to_process.size() << "\n"; + if (m_stats.m_num_to_superpose % 100 == 0) { + verbose_stream() << "[grobner] " << m_to_superpose.size() << " " << m_to_simplify.size() << "\n"; } #endif equation * new_eq = simplify_using_processed(eq); @@ -897,7 +897,7 @@ bool grobner::compute_basis_step() { if (m_manager.canceled()) return false; if (!simplify_processed_with_eq(eq)) return false; superpose(eq); - m_processed.insert(eq); + m_to_superpose.insert(eq); simplify_to_process(eq); TRACE("grobner", tout << "end of iteration:\n"; display(tout);); return false; @@ -917,12 +917,12 @@ void grobner::copy_to(equation_set const & s, ptr_vector & result) con } /** - \brief Copy the equations in m_processed and m_to_process to result. + \brief Copy the equations in m_to_superpose and m_to_simplify to result. \warning This equations can be deleted when compute_basis is invoked. */ void grobner::get_equations(ptr_vector & result) const { - copy_to(m_processed, result); - copy_to(m_to_process, result); + copy_to(m_to_superpose, result); + copy_to(m_to_simplify, result); } diff --git a/src/math/grobner/grobner.h b/src/math/grobner/grobner.h index 16abfc857..a53b59c42 100644 --- a/src/math/grobner/grobner.h +++ b/src/math/grobner/grobner.h @@ -97,8 +97,8 @@ protected: obj_map m_var2weight; var_lt m_var_lt; monomial_lt m_monomial_lt; - equation_set m_processed; - equation_set m_to_process; + equation_set m_to_superpose; + equation_set m_to_simplify; equation_vector m_equations_to_unfreeze; equation_vector m_equations_to_delete; bool m_changed_leading_term; // set to true, if the leading term was simplified. diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp index cfe27d01e..8164553cc 100644 --- a/src/math/lp/nla_grobner.cpp +++ b/src/math/lp/nla_grobner.cpp @@ -190,7 +190,7 @@ void nla_grobner::add_row(unsigned i) { } void nla_grobner::simplify_equations_to_process() { - for (equation *eq : m_to_process) { + for (equation *eq : m_to_simplify) { eq->exp() = m_nex_creator.simplify(eq->exp()); } } @@ -221,8 +221,8 @@ bool nla_grobner::is_better_choice(equation * eq1, equation * eq2) { void nla_grobner::del_equation(equation * eq) { NOT_IMPLEMENTED_YET(); /* - m_processed.erase(eq); - m_to_process.erase(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] = 0; del_monomials(eq->m_exp); @@ -233,7 +233,7 @@ void nla_grobner::del_equation(equation * eq) { nla_grobner::equation* nla_grobner::pick_next() { equation * r = nullptr; ptr_buffer to_delete; - for (equation * curr : m_to_process) { + for (equation * curr : m_to_simplify) { if (is_trivial(curr)) to_delete.push_back(curr); else if (is_better_choice(curr, r)) @@ -242,7 +242,7 @@ nla_grobner::equation* nla_grobner::pick_next() { for (equation * e : to_delete) del_equation(e); if (r) - m_to_process.erase(r); + m_to_simplify.erase(r); TRACE("grobner", tout << "selected equation: "; if (!r) tout << "\n"; else display_equation(tout, *r);); return r; } @@ -250,10 +250,10 @@ nla_grobner::equation* nla_grobner::pick_next() { nla_grobner::equation* nla_grobner::simplify_using_processed(equation* eq) { bool result = false; bool simplified; - TRACE("grobner", tout << "simplifying: "; display_equation(tout, *eq); tout << "using already processed equalities of size " << m_processed.size() << "\n";); + TRACE("grobner", tout << "simplifying: "; display_equation(tout, *eq); tout << "using already processed equalities of size " << m_to_superpose.size() << "\n";); do { simplified = false; - for (equation const* p : m_processed) { + for (equation const* p : m_to_superpose) { equation * new_eq = simplify_source_target(p, eq); if (new_eq) { result = true; @@ -443,12 +443,12 @@ bool nla_grobner::simplify_processed_with_eq(equation* eq) { ptr_buffer to_insert; ptr_buffer to_remove; ptr_buffer to_delete; - equation_set::iterator it = m_processed.begin(); - equation_set::iterator end = m_processed.end(); + equation_set::iterator it = m_to_superpose.begin(); + equation_set::iterator end = m_to_superpose.end(); for (; it != end && !canceled(); ++it) { equation * target = *it; m_changed_leading_term = false; - // if the leading term is simplified, then the equation has to be moved to m_to_process + // if the leading term is simplified, then the equation has to be moved to m_to_simplify equation * new_target = simplify_source_target(eq, target); if (new_target != nullptr) { process_simplified_target(to_insert, new_target, target, to_remove); @@ -459,7 +459,7 @@ bool nla_grobner::simplify_processed_with_eq(equation* eq) { for (equation* eq : to_insert) insert_processed(eq); for (equation* eq : to_remove) - m_processed.erase(eq); + m_to_superpose.erase(eq); for (equation* eq : to_delete) del_equation(eq); return !canceled(); @@ -469,7 +469,7 @@ void nla_grobner::simplify_to_process(equation* eq) { ptr_buffer to_insert; ptr_buffer to_remove; ptr_buffer to_delete; - for (equation* target : m_to_process) { + for (equation* target : m_to_simplify) { equation * new_target = simplify_source_target(eq, target); if (new_target != nullptr && new_target != target) { m_equations_to_unfreeze.push_back(target); @@ -483,7 +483,7 @@ void nla_grobner::simplify_to_process(equation* eq) { for (equation* eq : to_insert) insert_to_process(eq); for (equation* eq : to_remove) - m_to_process.erase(eq); + m_to_simplify.erase(eq); for (equation* eq : to_delete) del_equation(eq); @@ -500,7 +500,7 @@ void nla_grobner::superpose(equation * eq1, equation * eq2) { } void nla_grobner::superpose(equation * eq) { - for (equation * target : m_processed) { + for (equation * target : m_to_superpose) { superpose(eq, target); } } @@ -554,7 +554,7 @@ void nla_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_processed += gb.m_stats.m_num_processed; + m_stats.m_gb_num_to_superpose += gb.m_stats.m_num_to_superpose; m_stats.m_gb_compute_basis++;*/ } @@ -589,8 +589,8 @@ void copy_to(const T& source, V& target ) { } void nla_grobner::get_equations(ptr_vector& result) { - copy_to(m_processed, result); - copy_to(m_to_process, result); + copy_to(m_to_superpose, result); + copy_to(m_to_simplify, result); } diff --git a/src/math/lp/nla_grobner.h b/src/math/lp/nla_grobner.h index 8a39d8da1..1dd774d2b 100644 --- a/src/math/lp/nla_grobner.h +++ b/src/math/lp/nla_grobner.h @@ -84,8 +84,8 @@ class nla_grobner : common { lp::int_set m_rows; unsigned m_num_of_equations; grobner_stats m_stats; - equation_set m_processed; - equation_set m_to_process; + 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; @@ -145,8 +145,8 @@ bool simplify_processed_with_eq(equation*); void init_equation(equation* eq, nex*, ci_dependency* d); std::ostream& display_dependency(std::ostream& out, ci_dependency*); - void insert_to_process(equation *eq) { m_to_process.insert(eq); } - void insert_processed(equation *eq) { m_processed.insert(eq); } + void insert_to_process(equation *eq) { m_to_simplify.insert(eq); } + void insert_processed(equation *eq) { m_to_superpose.insert(eq); } void simplify_equations_to_process(); const nex_mul * get_highest_monomial(const nex * e) const; ci_dependency* dep_from_vector( svector & fixed_vars_constraints);