From 5e40d64a8272c1d0ef0945751fb76966f5dd36a1 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Thu, 10 Oct 2019 15:59:28 -0700 Subject: [PATCH] port Grobner Signed-off-by: Lev Nachmanson --- src/math/grobner/grobner.cpp | 4 +- src/math/lp/nla_grobner.cpp | 150 ++++++++++++++++++++++++++++++++--- src/math/lp/nla_grobner.h | 10 ++- 3 files changed, 149 insertions(+), 15 deletions(-) diff --git a/src/math/grobner/grobner.cpp b/src/math/grobner/grobner.cpp index 74189351b..e2108b767 100644 --- a/src/math/grobner/grobner.cpp +++ b/src/math/grobner/grobner.cpp @@ -619,7 +619,9 @@ unsigned grobner::simplify_loop_on_target_monomials(equation const * source, equ /** \brief Simplify the target equation using the source as a rewrite rule. Return 0 if target was not simplified. - Return target if target was simplified but source->m_scope_lvl <= target->m_scope_lvl. + + LN. The rest of the comment seems to be incorrect: there is no m_scope_lvl + Return target if target was simplified Return new_equation if source->m_scope_lvl > target->m_scope_lvl, moreover target is freezed, and new_equation contains the result. */ grobner::equation * grobner::simplify_source_target(equation const * source, equation * target) { diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp index 0975b19a8..e382b2beb 100644 --- a/src/math/lp/nla_grobner.cpp +++ b/src/math/lp/nla_grobner.cpp @@ -25,7 +25,9 @@ nla_grobner::nla_grobner(core *c ) : common(c), m_nl_gb_exhausted(false), - m_dep_manager(m_val_manager, m_alloc) {} + m_dep_manager(m_val_manager, m_alloc), + m_changed_leading_term(false) +{} // Scan the grobner basis eqs for equations of the form x - k = 0 or x = 0 is found, and x is not fixed, // then assert bounds for x, and continue @@ -255,23 +257,149 @@ nla_grobner::equation* nla_grobner::simplify_using_processed(equation* eq) { } -nla_grobner::equation* nla_grobner::simplify_processed(equation* eq) { +unsigned nla_grobner::simplify_loop_on_target_monomials(equation const * source, equation * target, bool & result) { + unsigned i = 0; + unsigned n_sz = 0; + unsigned sz = target->m_exp->size(); NOT_IMPLEMENTED_YET(); - return nullptr; + /* + monomial const * LT = source->get_monomial(0); + ptr_vector & new_monomials = m_tmp_monomials; + new_monomials.reset(); + ptr_vector & rest = m_tmp_vars1; + + for (; i < sz; i++) { + monomial * curr = target->m_monomials[i]; + rest.reset(); + if (is_subset(LT, curr, rest)) { + if (i == 0) + m_changed_leading_term = true; + if (!result) { + // first time that source is being applied. + target->m_dep = m_dep_manager.mk_join(target->m_dep, source->m_dep); + } + result = true; + rational coeff = curr->m_coeff; + coeff /= LT->m_coeff; + coeff.neg(); + if (!rest.empty()) + target->m_lc = false; + mul_append(1, source, coeff, rest, new_monomials); + del_monomial(curr); + } + else { + target->m_monomials[n_sz++] = curr; + } + }*/ + return n_sz; } -nla_grobner::equation* nla_grobner::simplify_to_process(equation*) { - NOT_IMPLEMENTED_YET(); - return nullptr; + +nla_grobner::equation * nla_grobner::simplify_source_target(equation const * source, equation * target) { + TRACE("grobner", tout << "simplifying: "; display_equation(tout, *target); tout << "using: "; display_equation(tout, *source);); + if (source->get_num_monomials() == 0) + return nullptr; + m_stats.m_simplify++; + bool result = false; + do { + unsigned target_new_size = simplify_loop_on_target_monomials(source, target, result); + if (target_new_size < target->m_exp->size()) { + NOT_IMPLEMENTED_YET(); + /* + target->m_monomials.shrink(target_new_size); + target->m_monomials.append(m_tmp_monomials.size(), m_tmp_monomials.c_ptr()); + simplify_eq(target); + */ + } else { + NOT_IMPLEMENTED_YET(); + break; + } + } + while (!canceled()); + TRACE("grobner", tout << "result: "; display_equation(tout, *target);); + return result ? target : nullptr; +} + +void nla_grobner::process_simplified_target(ptr_buffer& to_insert, equation* new_target, equation*& target, ptr_buffer& to_remove) { + if (new_target != target) { + m_equations_to_unfreeze.push_back(target); + to_remove.push_back(target); + if (m_changed_leading_term) { + m_to_process.insert(new_target); + to_remove.push_back(target); + } + else { + to_insert.push_back(new_target); + } + target = new_target; + } + else { + if (m_changed_leading_term) { + m_to_process.insert(target); + to_remove.push_back(target); + } + } +} + +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(); + 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 + equation * new_target = simplify_source_target(eq, target); + if (new_target != nullptr) { + process_simplified_target(to_insert, new_target, target, to_remove); + } + if (is_trivial(target)) + to_delete.push_back(target); + } + for (equation* eq : to_insert) + m_processed.insert(eq); + for (equation* eq : to_remove) + m_processed.erase(eq); + for (equation* eq : to_delete) + del_equation(eq); + return !canceled(); +} + +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) { + equation * new_target = simplify_source_target(eq, target); + if (new_target != nullptr && new_target != target) { + m_equations_to_unfreeze.push_back(target); + to_insert.push_back(new_target); + to_remove.push_back(target); + target = new_target; + } + if (is_trivial(target)) + to_delete.push_back(target); + } + for (equation* eq : to_insert) + m_to_process.insert(eq); + for (equation* eq : to_remove) + m_to_process.erase(eq); + for (equation* eq : to_delete) + del_equation(eq); + } void nla_grobner::superpose(equation * eq1, equation * eq2) { - SASSERT(false); + NOT_IMPLEMENTED_YET(); } -void nla_grobner::superpose(equation * eq){ - SASSERT(false); +void nla_grobner::superpose(equation * eq) { + for (equation * target : m_processed) { + superpose(eq, target); + } } @@ -287,7 +415,7 @@ bool nla_grobner::compute_basis_step() { eq = new_eq; } if (canceled()) return false; - if (!simplify_processed(eq)) return false; + if (!simplify_processed_with_eq(eq)) return false; superpose(eq); m_processed.insert(eq); simplify_to_process(eq); @@ -474,7 +602,7 @@ nla_grobner::equation * nla_grobner::simplify(equation const * source, equation return nullptr; } -std::ostream& nla_grobner::display_equation(std::ostream & out, equation & eq) { +std::ostream& nla_grobner::display_equation(std::ostream & out, const equation & eq) { out << "m_exp = " << *eq.m_exp << "\n"; out << "dep = "; display_dependency(out, eq.m_dep) << "\n"; return out; diff --git a/src/math/lp/nla_grobner.h b/src/math/lp/nla_grobner.h index 6ffcea020..73a9d5f18 100644 --- a/src/math/lp/nla_grobner.h +++ b/src/math/lp/nla_grobner.h @@ -89,6 +89,7 @@ class nla_grobner : common { ci_value_manager m_val_manager; ci_dependency_manager m_dep_manager; nex_lt m_lt; + bool m_changed_leading_term; public: nla_grobner(core *core); void grobner_lemmas(); @@ -108,9 +109,12 @@ private: void compute_basis_init(); bool compute_basis_loop(); bool compute_basis_step(); + equation * simplify_source_target(equation const * source, equation * target); equation* simplify_using_processed(equation*); - equation* simplify_processed(equation*); - equation* simplify_to_process(equation*); + unsigned simplify_loop_on_target_monomials(equation const * source, equation * target, bool & result); + void process_simplified_target(ptr_buffer& to_insert, equation* new_target, equation*& target, ptr_buffer& to_remove); +bool simplify_processed_with_eq(equation*); + void simplify_to_process(equation*); equation* pick_next(); void set_gb_exhausted(); bool canceled() { return false; } // todo, implement @@ -121,7 +125,7 @@ private: 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; - std::ostream& display_equation(std::ostream & out, equation & eq); + std::ostream& display_equation(std::ostream & out, const equation & eq); void display_monomial(std::ostream & out, monomial const & m) const;