mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

fix a bug in :divide_ignore_coeffs_perform_nex_mul()

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-12-12 16:58:41 -10:00
parent 882b8ee63b
commit 1df6411580
2 changed files with 23 additions and 25 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

45
src/math/lp/nla_grobner.cpp
View file

@ -247,7 +247,7 @@ bool grobner::simplify_target_monomials(equation * source, equation * target) {
if (high_mon == nullptr) if (high_mon == nullptr)
return false; return false;
SASSERT(high_mon->all_factors_are_elementary()); SASSERT(high_mon->all_factors_are_elementary());
TRACE("grobner", tout << "source = "; display_equation(tout, *source) << "target = "; display_equation(tout, *target) << "high_mon = " << *high_mon << "\n";); TRACE("grobner_d", tout << "source = "; display_equation(tout, *source) << "target = "; display_equation(tout, *target) << "high_mon = " << *high_mon << "\n";);
nex * te = target->expr(); nex * te = target->expr();
nex_sum * targ_sum; nex_sum * targ_sum;
@ -256,7 +256,7 @@ bool grobner::simplify_target_monomials(equation * source, equation * target) {
} else if (te->is_mul()) { } else if (te->is_mul()) {
targ_sum = m_nex_creator.mk_sum(te); targ_sum = m_nex_creator.mk_sum(te);
} else { } else {
TRACE("grobner", tout << "return false\n";); TRACE("grobner_d", tout << "return false\n";);
return false; return false;
} }
@ -267,12 +267,12 @@ unsigned grobner::find_divisible(nex_sum* targ_sum, const nex* high_mon) const {
unsigned j = 0; unsigned j = 0;
for (auto t : *targ_sum) { for (auto t : *targ_sum) {
if (divide_ignore_coeffs_check_only(t, high_mon)) { if (divide_ignore_coeffs_check_only(t, high_mon)) {
TRACE("grobner", tout << "yes div: " << *t << " / " << *high_mon << "\n";); TRACE("grobner_d", tout << "yes div: " << *t << " / " << *high_mon << "\n";);
return j; return j;
} }
++j; ++j;
} }
TRACE("grobner", tout << "no div: " << *targ_sum << " / " << *high_mon << "\n";); TRACE("grobner_d", tout << "no div: " << *targ_sum << " / " << *high_mon << "\n";);
return -1; return -1;
} }
@ -284,8 +284,9 @@ bool grobner::simplify_target_monomials_sum(equation * source,
return false; return false;
m_changed_leading_term = (j == 0); m_changed_leading_term = (j == 0);
unsigned targ_orig_size = targ_sum->size(); unsigned targ_orig_size = targ_sum->size();
for (; j < targ_orig_size; j++) { simplify_target_monomials_sum_j(source, target, targ_sum, high_mon, j, false); // false to avoid divisibility test
simplify_target_monomials_sum_j(source, target, targ_sum, high_mon, j); for (j++; j < targ_orig_size; j++) {
simplify_target_monomials_sum_j(source, target, targ_sum, high_mon, j, true);
} }
TRACE("grobner_d", tout << "targ_sum = " << *targ_sum << "\n";); TRACE("grobner_d", tout << "targ_sum = " << *targ_sum << "\n";);
target->expr() = m_nex_creator.simplify(targ_sum); target->expr() = m_nex_creator.simplify(targ_sum);
@ -294,15 +295,8 @@ bool grobner::simplify_target_monomials_sum(equation * source,
return true; return true;
} }
nex_mul* grobner::divide_ignore_coeffs(nex* ej, const nex* h) {
TRACE("grobner", tout << "ej = " << *ej << " , h = " << *h << "\n";);
if (!divide_ignore_coeffs_check_only(ej, h))
return nullptr;
return divide_ignore_coeffs_perform(ej, h);
}
bool grobner::divide_ignore_coeffs_check_only_nex_mul(nex_mul* t , const nex* h) const { bool grobner::divide_ignore_coeffs_check_only_nex_mul(nex_mul* t , const nex* h) const {
TRACE("grobner", tout << "t = " << *t << ", h=" << *h << "\n";); TRACE("grobner_d", tout << "t = " << *t << ", h=" << *h << "\n";);
SASSERT(m_nex_creator.is_simplified(*t) && m_nex_creator.is_simplified(*h)); SASSERT(m_nex_creator.is_simplified(*t) && m_nex_creator.is_simplified(*h));
unsigned j = 0; // points to t unsigned j = 0; // points to t
for(unsigned k = 0; k < h->number_of_child_powers(); k++) { for(unsigned k = 0; k < h->number_of_child_powers(); k++) {
@ -317,11 +311,11 @@ bool grobner::divide_ignore_coeffs_check_only_nex_mul(nex_mul* t , const nex* h)
} }
} }
if (!p_swallowed) { if (!p_swallowed) {
TRACE("grobner", tout << "no div " << *t << " / " << *h << "\n";); TRACE("grobner_d", tout << "no div " << *t << " / " << *h << "\n";);
return false; return false;
} }
} }
TRACE("grobner", tout << "division " << *t << " / " << *h << "\n";); TRACE("grobner_d", tout << "division " << *t << " / " << *h << "\n";);
return true; return true;
} }
@ -351,7 +345,7 @@ bool grobner::divide_ignore_coeffs_check_only(nex* n , const nex* h) const {
nex_mul * grobner::divide_ignore_coeffs_perform_nex_mul(nex_mul* t, const nex* h) { nex_mul * grobner::divide_ignore_coeffs_perform_nex_mul(nex_mul* t, const nex* h) {
nex_mul * r = m_nex_creator.mk_mul(); nex_mul * r = m_nex_creator.mk_mul();
unsigned j = 0; // points to t unsigned j = 0; // points to t and k runs over h
for(unsigned k = 0; k < h->number_of_child_powers(); k++) { for(unsigned k = 0; k < h->number_of_child_powers(); k++) {
lpvar h_var = to_var(h->get_child_exp(k))->var(); lpvar h_var = to_var(h->get_child_exp(k))->var();
for (; j < t->size(); j++) { for (; j < t->size(); j++) {
@ -369,7 +363,12 @@ nex_mul * grobner::divide_ignore_coeffs_perform_nex_mul(nex_mul* t, const nex* h
} }
} }
} }
TRACE("grobner", tout << "r = " << *r << " = " << *t << " / " << *h << "\n";);
for (; j < t->size(); j++) {
r->add_child_in_power((*t)[j]);
}
TRACE("grobner_d", tout << "r = " << *r << " = " << *t << " / " << *h << "\n";);
return r; return r;
} }
@ -386,14 +385,14 @@ nex_mul * grobner::divide_ignore_coeffs_perform(nex* e, const nex* h) {
// and b*high_mon + e = 0, so high_mon = -e/b // and b*high_mon + e = 0, so high_mon = -e/b
// then targ_sum->children()[j] = - (c/b) * e*p // then targ_sum->children()[j] = - (c/b) * e*p
void grobner::simplify_target_monomials_sum_j(equation * source, equation *target, nex_sum* targ_sum, const nex* high_mon, unsigned j) { void grobner::simplify_target_monomials_sum_j(equation * source, equation *target, nex_sum* targ_sum, const nex* high_mon, unsigned j, bool test_divisibility) {
nex * ej = (*targ_sum)[j]; nex * ej = (*targ_sum)[j];
TRACE("grobner_d", tout << "high_mon = " << *high_mon << ", ej = " << *ej << "\n";); TRACE("grobner_d", tout << "high_mon = " << *high_mon << ", ej = " << *ej << "\n";);
nex_mul * ej_over_high_mon = divide_ignore_coeffs(ej, high_mon); if (test_divisibility && !divide_ignore_coeffs_check_only(ej, high_mon)) {
if (ej_over_high_mon == nullptr) {
TRACE("grobner_d", tout << "no div\n";); TRACE("grobner_d", tout << "no div\n";);
return; return;
} }
nex_mul * ej_over_high_mon = divide_ignore_coeffs_perform(ej, high_mon);
TRACE("grobner_d", tout << "ej_over_high_mon = " << *ej_over_high_mon << "\n";); TRACE("grobner_d", tout << "ej_over_high_mon = " << *ej_over_high_mon << "\n";);
rational c = ej->is_mul()? to_mul(ej)->coeff() : rational(1); rational c = ej->is_mul()? to_mul(ej)->coeff() : rational(1);
TRACE("grobner_d", tout << "c = " << c << "\n";); TRACE("grobner_d", tout << "c = " << c << "\n";);
@ -512,9 +511,9 @@ void grobner::add_mul_skip_first(nex_sum* r, const rational& beta, nex *e, nex_m
for (unsigned j = 1; j < es->size(); j++) { for (unsigned j = 1; j < es->size(); j++) {
r->add_child(m_nex_creator.mk_mul(beta, (*es)[j], c)); r->add_child(m_nex_creator.mk_mul(beta, (*es)[j], c));
} }
TRACE("grobner", tout << "r = " << *r << "\n";); TRACE("grobner_d", tout << "r = " << *r << "\n";);
} else { } else {
TRACE("grobner", tout << "e = " << *e << "\n";); TRACE("grobner_d", tout << "e = " << *e << "\n";);
} }
} }

3
src/math/lp/nla_grobner.h
View file

@ -149,8 +149,7 @@ private:
ci_dependency* dep_from_vector(svector<lp::constraint_index> & fixed_vars_constraints); ci_dependency* dep_from_vector(svector<lp::constraint_index> & fixed_vars_constraints);
bool simplify_target_monomials_sum(equation *, equation *, nex_sum*, const nex*); bool simplify_target_monomials_sum(equation *, equation *, nex_sum*, const nex*);
unsigned find_divisible(nex_sum*, const nex*) const; unsigned find_divisible(nex_sum*, const nex*) const;
void simplify_target_monomials_sum_j(equation *, equation *, nex_sum*, const nex*, unsigned); void simplify_target_monomials_sum_j(equation *, equation *, nex_sum*, const nex*, unsigned, bool);
nex_mul * divide_ignore_coeffs(nex* ej, const nex*);
bool divide_ignore_coeffs_check_only(nex* , const nex*) const; bool divide_ignore_coeffs_check_only(nex* , const nex*) const;
bool divide_ignore_coeffs_check_only_nex_mul(nex_mul* , const nex*) const; bool divide_ignore_coeffs_check_only_nex_mul(nex_mul* , const nex*) const;
nex_mul * divide_ignore_coeffs_perform(nex* , const nex*); nex_mul * divide_ignore_coeffs_perform(nex* , const nex*);