From 29cc2c59761e71b8582518357e96b95bcae5f71e Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 17 Sep 2019 16:51:32 -0700 Subject: [PATCH] port grobner basis Signed-off-by: Lev Nachmanson --- src/math/lp/nla_grobner.cpp | 131 +++++++++++++++++++++++++++++++++--- src/math/lp/nla_grobner.h | 46 ++++++++++--- 2 files changed, 158 insertions(+), 19 deletions(-) diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp index 72fcc671a..d32fc8be1 100644 --- a/src/math/lp/nla_grobner.cpp +++ b/src/math/lp/nla_grobner.cpp @@ -127,9 +127,52 @@ void nla_grobner::init() { find_nl_cluster(); } -equation* nla_grobner::pick_next() { +bool nla_grobner::is_trivial(equation* eq) const { + return eq->m_monomials.empty(); +} + +bool nla_grobner:: is_better_choice(equation * eq1, equation * eq2) { + if (!eq2) + return true; + if (is_trivial(eq1)) + return true; + if (is_trivial(eq2)) + return false; + if (eq1->m_monomials[0]->get_degree() < eq2->m_monomials[0]->get_degree()) + return true; + if (eq1->m_monomials[0]->get_degree() > eq2->m_monomials[0]->get_degree()) + return false; + return eq1->m_monomials.size() < eq2->m_monomials.size(); + +} + +void nla_grobner::del_equation(equation * eq) { SASSERT(false); - return nullptr; + /* + m_processed.erase(eq); + m_to_process.erase(eq); + SASSERT(m_equations_to_delete[eq->m_bidx] == eq); + m_equations_to_delete[eq->m_bidx] = 0; + del_monomials(eq->m_monomials); + dealloc(eq); + */ +} + +equation* nla_grobner::pick_next() { + equation * r = nullptr; + ptr_buffer to_delete; + for (equation * curr : m_to_process) { + if (is_trivial(curr)) + to_delete.push_back(curr); + else if (is_better_choice(curr, r)) + r = curr; + } + for (equation * e : to_delete) + del_equation(e); + if (r) + m_to_process.erase(r); + TRACE("grobner", tout << "selected equation: "; if (!r) tout << "\n"; else display_equation(tout, *r);); + return r; } equation* nla_grobner::simplify_using_processed(equation* eq) { @@ -197,31 +240,101 @@ bool nla_grobner::compute_basis_loop(){ return false; } -void nla_grobner::set_gb_exhausted(){ SASSERT(false); } - -void nla_grobner::update_statistics(){ - SASSERT(false); +void nla_grobner::set_gb_exhausted(){ + NOT_IMPLEMENTED_YET(); } -bool nla_grobner::find_conflict(){ SASSERT(false); +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_compute_basis++;*/ +} + +// Scan the grobner basis eqs, and look for inconsistencies. + +bool nla_grobner::find_conflict(ptr_vector& eqs){ + eqs.reset(); + get_equations(eqs); + TRACE("grobner_bug", tout << "after gb\n";); + for (equation* eq : eqs) { + TRACE("grobner_bug", display_equation(tout, *eq);); + if (is_inconsistent(eq) || is_inconsistent2(eq)) + return true; + } return false; } -bool nla_grobner::push_calculation_forward(){ SASSERT(false); +bool nla_grobner::is_inconsistent(equation*) { + NOT_IMPLEMENTED_YET(); + return false; +} + +bool nla_grobner::is_inconsistent2(equation*) { + NOT_IMPLEMENTED_YET(); + return false; +} + +template +void copy_to(const T& source, V& target ) { + for (auto e : source) + target.push_back(e); +} + +void nla_grobner::get_equations(ptr_vector& result) { + copy_to(m_processed, result); + copy_to(m_to_process, result); +} + + +bool nla_grobner::push_calculation_forward(){ + NOT_IMPLEMENTED_YET(); return false; } void nla_grobner::grobner_lemmas() { c().lp_settings().stats().m_grobner_calls++; init(); + + ptr_vector eqs; + do { TRACE("nla_gb", tout << "before:\n"; display(tout);); compute_basis(); update_statistics(); TRACE("nla_gb", tout << "after:\n"; display(tout);); - if (find_conflict()) + if (find_conflict(eqs)) return; } while(push_calculation_forward()); } +void nla_grobner:: del_equations(unsigned old_size) { + 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; + if (eq) + del_equation(eq); + } + m_equations_to_delete.shrink(old_size); +} + +void nla_grobner::display_equations(std::ostream & out, equation_set const & v, char const * header) const { + NOT_IMPLEMENTED_YET(); +} +void nla_grobner::display_equation(std::ostream & out, equation const & eq) const { + NOT_IMPLEMENTED_YET(); +} + +void nla_grobner::display_monomial(std::ostream & out, monomial const & m) const { + NOT_IMPLEMENTED_YET(); +} + +void nla_grobner::display(std::ostream & out) const { + NOT_IMPLEMENTED_YET(); +} + } // end of nla namespace diff --git a/src/math/lp/nla_grobner.h b/src/math/lp/nla_grobner.h index 4453dbba0..c0b60d824 100644 --- a/src/math/lp/nla_grobner.h +++ b/src/math/lp/nla_grobner.h @@ -36,6 +36,18 @@ struct grobner_stats { }; struct monomial { + rational m_coeff; + svector m_vars; //!< sorted variables + + friend class grobner; + friend struct monomial_lt; + + monomial() {} +public: + rational const & get_coeff() const { return m_coeff; } + unsigned get_degree() const { return m_vars.size(); } + unsigned get_size() const { return get_degree(); } + lpvar get_var(unsigned idx) const { return m_vars[idx]; } }; class equation { @@ -43,8 +55,8 @@ class equation { unsigned m_bidx:31; //!< position at m_equations_to_delete unsigned m_lc:1; //!< true if equation if a linear combination of the input equations. ptr_vector m_monomials; //!< sorted monomials - v_dependency * m_dep; //!< justification for the equality - friend class grobner; + v_dependency * m_dep; //!< justification for the equality + friend class nla_grobner; equation() {} public: unsigned get_num_monomials() const { return m_monomials.size(); } @@ -70,14 +82,15 @@ enum class var_weight { class nla_grobner : common { typedef obj_hashtable equation_set; typedef ptr_vector equation_vector; - equation_vector m_equations_to_unfreeze; - equation_vector m_equations_to_delete; - lp::int_set m_rows; - lp::int_set m_active_vars; - svector m_active_vars_weights; - unsigned m_num_of_equations; - grobner_stats m_stats; + // fields + equation_vector m_equations_to_unfreeze; + equation_vector m_equations_to_delete; + lp::int_set m_rows; + lp::int_set m_active_vars; + svector m_active_vars_weights; + unsigned m_num_of_equations; + grobner_stats m_stats; equation_set m_processed; equation_set m_to_process; public: @@ -93,7 +106,9 @@ private: var_weight get_var_weight(lpvar) const; void compute_basis(); void update_statistics(); - bool find_conflict(); + bool find_conflict(ptr_vector& eqs); + bool is_inconsistent(equation*); + bool is_inconsistent2(equation*); bool push_calculation_forward(); void compute_basis_init(); bool compute_basis_loop(); @@ -106,5 +121,16 @@ private: bool canceled() { return false; } // todo, implement void superpose(equation * eq1, equation * eq2); void superpose(equation * eq); + bool is_trivial(equation* ) const; + bool is_better_choice(equation * eq1, equation * eq2); + void del_equations(unsigned old_size); + void del_equation(equation * eq); + void display_equations(std::ostream & out, equation_set const & v, char const * header) const; + void display_equation(std::ostream & out, equation const & eq) const; + + void display_monomial(std::ostream & out, monomial const & m) const; + + void display(std::ostream & out) const; + void get_equations(ptr_vector& eqs); }; // end of grobner }