diff --git a/src/math/lp/nex_creator.cpp b/src/math/lp/nex_creator.cpp index b4311b186..59ad8bd9c 100644 --- a/src/math/lp/nex_creator.cpp +++ b/src/math/lp/nex_creator.cpp @@ -65,6 +65,17 @@ nex * nex_creator::mk_div(const nex* a, lpvar j) { } bool nex_creator::eat_scalar_pow(rational& r, const nex_pow& p, unsigned pow) { + if (p.e()->is_mul()) { + const nex_mul *m = to_mul(p.e()); + if (m->size() == 0) { + const rational& coeff = m->coeff(); + if (coeff.is_one()) + return true; + r *= coeff.expt(p.pow() * pow); + return true; + } + return false; + } if (!p.e()->is_scalar()) return false; const nex_scalar *pe = to_scalar(p.e()); diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp index 8013b41cb..26cd9db4b 100644 --- a/src/math/lp/nla_grobner.cpp +++ b/src/math/lp/nla_grobner.cpp @@ -130,45 +130,6 @@ void nla_grobner::process_var(nex_mul* m, lpvar j, ci_dependency* & dep, rationa } } -/** - \brief Create a new monomial using the given coeff and m. Fixed - variables in m are substituted by their values. The arg dep is - updated to store these dependencies. The set already_found is - updated with the fixed variables in m. A variable is only - added to dep if it is not already in already_found. - - Return null if the monomial was simplified to 0. -*/ -nex * nla_grobner::mk_monomial_in_row(rational coeff, lpvar j, ci_dependency * & dep) { - NOT_IMPLEMENTED_YET(); - return nullptr; - /* - ptr_buffer vars; - rational r; - - if (c().is_monic_var(j)) { - coeff *= get_monomial_coeff(m); - m = get_monomial_body(m); - if (m_util.is_mul(m)) { - SASSERT(is_pure_monomial(m)); - for (unsigned i = 0; i < to_app(m)->get_num_args(); i++) { - expr * arg = to_app(m)->get_arg(i); - process_var(arg); - } - } - else { - process_var(m); - } - } - else { - process_var(m); - } - if (!coeff.is_zero()) - return gb.mk_monomial(coeff, vars.size(), vars.c_ptr()); - else - return nullptr; - */ -} common::ci_dependency* nla_grobner::dep_from_vector(svector & cs) { ci_dependency * d = nullptr; @@ -319,8 +280,8 @@ bool nla_grobner::simplify_target_monomials_sum_check_only(nex_sum* targ_sum, } -bool nla_grobner::simplify_target_monomials_sum(equation const * source, - equation *target, nex_sum* targ_sum, +bool nla_grobner::simplify_target_monomials_sum(equation * source, + equation * target, nex_sum* targ_sum, const nex_mul* high_mon) { if (!simplify_target_monomials_sum_check_only(targ_sum, high_mon)) return false; @@ -328,6 +289,8 @@ bool nla_grobner::simplify_target_monomials_sum(equation const * source, for (unsigned j = 0; j < targ_orig_size; j++) { simplify_target_monomials_sum_j(source, target, targ_sum, high_mon, j); } + target->exp() = m_nex_creator.simplify(targ_sum); + TRACE("grobner", tout << "target = "; display_equation(tout, *target);); return true; } @@ -388,48 +351,22 @@ nex_mul * nla_grobner::divide_ignore_coeffs_perform(nex_mul* t, const nex_mul* h return r; } -bool nla_grobner::simplify_target_monomials_sum_j(equation const * source, equation *target, nex_sum* targ_sum, const nex_mul* high_mon, unsigned j) { +// if targ_sum->children()[j] = c*high_mon*p, +// and b*high_mon + e = 0, so high_mon = -e/b +// then targ_sum->children()[j] = - (c/b) * e*p + +void nla_grobner::simplify_target_monomials_sum_j(equation * source, equation *target, nex_sum* targ_sum, const nex_mul* high_mon, unsigned j) { nex * ej = (*targ_sum)[j]; - nex * ej_over_high_mon = divide_ignore_coeffs(ej, high_mon); - if (ej_over_high_mon == nullptr) - return false; - - NOT_IMPLEMENTED_YET(); - return false; - /* - unsigned i = 0; - unsigned new_target_sz = 0; - unsigned target_sz = target->m_monomials.size(); - monomial const * LT = source->get_monomial(0); - m_tmp_monomials.reset(); - 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 (!m_tmp_vars1.empty()) - target->m_lc = false; - mul_append_skip_first(source, - targ_i->m_coeff / (LT->m_coeff), m_tmp_vars1); - del_monomial(targ_i); - } - else { - if (i != new_target_sz) { - target->m_monomials[new_target_sz] = targ_i; - } - new_target_sz++; - } + nex_mul * ej_over_high_mon = divide_ignore_coeffs(ej, high_mon); + if (ej_over_high_mon == nullptr) { + return; } - 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; - */ - return false; + rational c = ej->is_mul()? to_mul(ej)->coeff() : rational(1); + nex_sum * ej_sum = m_nex_creator.mk_sum(); + (*targ_sum)[j] = ej_sum; + add_mul_skip_first(ej_sum ,-c/high_mon->coeff(), source->exp(), ej_over_high_mon); + TRACE("grobner", tout << "targ_sum = " << *targ_sum << "\n";); } @@ -441,6 +378,7 @@ nla_grobner::equation * nla_grobner::simplify_source_target(equation * source, e bool result = false; do { if (simplify_target_monomials(source, target)) { + TRACE("grobner", tout << "simplified target = ";display_equation(tout, *target) << "\n";); result = true; } else { break; @@ -527,7 +465,8 @@ void nla_grobner::simplify_to_process(equation* eq) { // if e is the sum adds to r all children of e multiplied by beta, except the first one // which corresponds to the highest monomial void nla_grobner::add_mul_skip_first(nex_sum* r, const rational& beta, nex *e, nex_mul* c) { - if (e->is_sum()) { + SASSERT(e->is_sum()); + if (e->is_sum()) { nex_sum *es = to_sum(e); for (unsigned j = 1; j < es->size(); j++) { r->add_child(m_nex_creator.mk_mul(beta, (*es)[j], c)); diff --git a/src/math/lp/nla_grobner.h b/src/math/lp/nla_grobner.h index 8026d9c04..fb3201e47 100644 --- a/src/math/lp/nla_grobner.h +++ b/src/math/lp/nla_grobner.h @@ -141,9 +141,6 @@ bool simplify_processed_with_eq(equation*); void assert_eq_0(nex*, ci_dependency * dep); void process_var(nex_mul*, lpvar j, ci_dependency *& dep, rational&); - nex* mk_monomial_in_row(rational, lpvar, ci_dependency*&); - - void init_equation(equation* eq, nex*, ci_dependency* d); std::ostream& display_dependency(std::ostream& out, ci_dependency*); @@ -152,9 +149,9 @@ bool simplify_processed_with_eq(equation*); void simplify_equations_to_process(); nex_mul * get_highest_monomial(nex * e) const; ci_dependency* dep_from_vector( svector & fixed_vars_constraints); - bool simplify_target_monomials_sum(equation const *, equation *, nex_sum*, const nex_mul*); + bool simplify_target_monomials_sum(equation *, equation *, nex_sum*, const nex_mul*); bool simplify_target_monomials_sum_check_only(nex_sum*, const nex_mul*); - bool simplify_target_monomials_sum_j(equation const *, equation *, nex_sum*, const nex_mul*, unsigned); + void simplify_target_monomials_sum_j(equation *, equation *, nex_sum*, const nex_mul*, unsigned); nex_mul * divide_ignore_coeffs(nex* ej, const nex_mul*); bool divide_ignore_coeffs_check_only(nex_mul* , const nex_mul*); nex_mul * divide_ignore_coeffs_perform(nex_mul* , const nex_mul*);