From f8059394e512c13a34a86b1101e952c6fb4d4481 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 16 Oct 2019 16:59:39 -0700 Subject: [PATCH] port Grobner Signed-off-by: Lev Nachmanson --- src/math/grobner/grobner.cpp | 41 ++++++++++++++++++------------------ src/math/grobner/grobner.h | 2 +- src/math/lp/nla_grobner.cpp | 21 +++++++++++------- src/math/lp/nla_grobner.h | 7 +++--- 4 files changed, 38 insertions(+), 33 deletions(-) diff --git a/src/math/grobner/grobner.cpp b/src/math/grobner/grobner.cpp index eecb68df4..4dd88d4e3 100644 --- a/src/math/grobner/grobner.cpp +++ b/src/math/grobner/grobner.cpp @@ -586,25 +586,20 @@ grobner::equation * grobner::copy_equation(equation const * eq) { // source 3f + k = 0, so f = -k/3 // target 2fg + e = 0 // target is replaced by 2(-k/3)g + e = -2/3kg + e -unsigned grobner::simplify_loop_on_target_monomials(equation const * source, equation * target, bool & result) { +bool grobner::simplify_target_monomials(equation const * source, equation * target) { unsigned i = 0; unsigned new_target_sz = 0; - unsigned sz = target->m_monomials.size(); + unsigned target_sz = target->m_monomials.size(); monomial const * LT = source->get_monomial(0); m_tmp_monomials.reset(); - for (; i < sz; i++) { + for (; i < target_sz; i++) { monomial * targ_i = target->m_monomials[i]; if (divide_ignore_coeffs(targ_i, LT)) { 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 = - targ_i->m_coeff / (LT->m_coeff); if (!m_tmp_vars1.empty()) target->m_lc = false; - mul_append_skip_first(source, coeff, m_tmp_vars1); + mul_append_skip_first(source, - targ_i->m_coeff / (LT->m_coeff), m_tmp_vars1); del_monomial(targ_i); } else { @@ -614,16 +609,20 @@ unsigned grobner::simplify_loop_on_target_monomials(equation const * source, equ new_target_sz++; } } - return new_target_sz; + if (new_target_sz < target_sz) { + target->m_monomials.shrink(new_target_sz); + target->m_monomials.append(m_tmp_monomials.size(), m_tmp_monomials.c_ptr()); + simplify_eq(target); + TRACE("grobner", tout << "result: "; display_equation(tout, *target);); + return true; + } + return false; } /** \brief Simplify the target equation using the source as a rewrite rule. Return 0 if target was not simplified. - 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) { TRACE("grobner", tout << "simplifying: "; display_equation(tout, *target); tout << "using: "; display_equation(tout, *source);); @@ -632,18 +631,18 @@ grobner::equation * grobner::simplify_source_target(equation const * source, equ 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_monomials.size()) { - target->m_monomials.shrink(target_new_size); - target->m_monomials.append(m_tmp_monomials.size(), m_tmp_monomials.c_ptr()); - simplify_eq(target); + if (simplify_target_monomials(source, target)) { + result = true; } else { break; } - } - while (!m_manager.canceled()); + } while (!m_manager.canceled()); TRACE("grobner", tout << "result: "; display_equation(tout, *target);); - return result ? target : nullptr; + if (result) { + target->m_dep = m_dep_manager.mk_join(target->m_dep, source->m_dep); + return target; + } + return nullptr; } /** diff --git a/src/math/grobner/grobner.h b/src/math/grobner/grobner.h index 6dcf7926c..16abfc857 100644 --- a/src/math/grobner/grobner.h +++ b/src/math/grobner/grobner.h @@ -166,7 +166,7 @@ protected: equation * copy_equation(equation const * eq); equation * simplify_source_target(equation const * source, equation * target); - unsigned simplify_loop_on_target_monomials(equation const * source, equation * target, bool&); + bool simplify_target_monomials(equation const * source, equation * target); equation * simplify_using_processed(equation * eq); diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp index 86f0ef822..39d7ec099 100644 --- a/src/math/lp/nla_grobner.cpp +++ b/src/math/lp/nla_grobner.cpp @@ -200,7 +200,7 @@ void nla_grobner::init() { } bool nla_grobner::is_trivial(equation* eq) const { - return eq->m_exp->size() == 0; + return eq->m_expr->size() == 0; } bool nla_grobner::is_better_choice(equation * eq1, equation * eq2) { @@ -210,7 +210,7 @@ bool nla_grobner::is_better_choice(equation * eq1, equation * eq2) { return true; if (is_trivial(eq2)) return false; - return m_nex_creator.lt(eq1->m_exp, eq2->m_exp); + return m_nex_creator.lt(eq1->m_expr, eq2->m_expr); } void nla_grobner::del_equation(equation * eq) { @@ -266,10 +266,15 @@ nla_grobner::equation* nla_grobner::simplify_using_processed(equation* eq) { } +// source 3f + k = 0, so f = -k/3 +// target 2fg + e = 0 +// target is replaced by 2(-k/3)g + e = -2/3kg + e unsigned nla_grobner::simplify_loop_on_target_monomials(equation const * source, equation * target, bool & result) { + TRACE("nla_grobner", tout << "source = " << *source->exp() << " , target = " << *target->exp() << "\n";); unsigned i = 0; - unsigned n_sz = 0; - unsigned sz = target->m_exp->size(); + unsigned new_target_sz = 0; + unsigned sz = target->exp()->size(); + //if (source->exp()->is_sum() && target->exp()->is_su NOT_IMPLEMENTED_YET(); /* monomial const * LT = source->get_monomial(0); @@ -300,7 +305,7 @@ unsigned nla_grobner::simplify_loop_on_target_monomials(equation const * source, target->m_monomials[n_sz++] = curr; } }*/ - return n_sz; + return 1; } @@ -312,7 +317,7 @@ nla_grobner::equation * nla_grobner::simplify_source_target(equation const * sou bool result = false; do { unsigned target_new_size = simplify_loop_on_target_monomials(source, target, result); - if (target_new_size < target->m_exp->size()) { + if (target_new_size < target->exp()->size()) { NOT_IMPLEMENTED_YET(); /* target->m_monomials.shrink(target_new_size); @@ -612,7 +617,7 @@ nla_grobner::equation * nla_grobner::simplify(equation const * source, equation } std::ostream& nla_grobner::display_equation(std::ostream & out, const equation & eq) { - out << "m_exp = " << *eq.m_exp << "\n"; + out << "m_exp = " << *eq.exp() << "\n"; out << "dep = "; display_dependency(out, eq.m_dep) << "\n"; return out; } @@ -635,7 +640,7 @@ void nla_grobner::init_equation(equation* eq, nex*e, ci_dependency * dep) { eq->m_bidx = bidx; eq->m_dep = dep; eq->m_lc = true; - eq->m_exp = e; + eq->exp() = 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 9b0a9633b..519a419c9 100644 --- a/src/math/lp/nla_grobner.h +++ b/src/math/lp/nla_grobner.h @@ -41,15 +41,16 @@ class nla_grobner : common { 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. - nex * m_exp; // simplified expressionted monomials + nex * m_expr; // simplified expressionted monomials ci_dependency * m_dep; //!< justification for the equality friend class nla_grobner; equation() {} public: - unsigned get_num_monomials() const { return m_exp->size(); } + unsigned get_num_monomials() const { return m_expr->size(); } nex_mul* const * get_monomial(unsigned idx) const { NOT_IMPLEMENTED_YET(); return nullptr; } - nex* & exp() { return m_exp; } + nex* & exp() { return m_expr; } + const nex* exp() const { return m_expr; } ci_dependency * get_dependency() const { return m_dep; } unsigned hash() const { return m_bidx; } bool is_linear_combination() const { return m_lc; }