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

revert the simplification loops

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-12-11 09:50:19 -10:00
parent bc302285a1
commit da8a7e256f
1 changed files with 22 additions and 18 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

40
src/math/lp/nex_creator.cpp
View file

@ -89,8 +89,8 @@ bool nex_creator::eat_scalar_pow(rational& r, const nex_pow& p, unsigned pow) {
void nex_creator::simplify_children_of_mul(vector<nex_pow> & children, rational& coeff) { void nex_creator::simplify_children_of_mul(vector<nex_pow> & children, rational& coeff) {
TRACE("grobner_d", print_vector(children, tout);); TRACE("grobner_d", print_vector(children, tout););
vector<nex_pow> to_promote; vector<nex_pow> to_promote;
bool skipped = false; int skipped = 0;
for (nex_pow& p : children.size()) { for(unsigned j = 0; j < children.size(); j++) {
nex_pow& p = children[j]; nex_pow& p = children[j];
if (eat_scalar_pow(coeff, p, 1)) { if (eat_scalar_pow(coeff, p, 1)) {
skipped++; skipped++;
@ -112,13 +112,13 @@ void nex_creator::simplify_children_of_mul(vector<nex_pow> & children, rational&
for (nex_pow & p : to_promote) { for (nex_pow & p : to_promote) {
TRACE("grobner_d", tout << p << "\n";); TRACE("grobner_d", tout << p << "\n";);
nex_mul & pm = *to_mul(p.e()); nex_mul *pm = to_mul(p.e());
for (nex_pow & pp : pm) { for (nex_pow& pp : *pm) {
TRACE("grobner_d", tout << pp << "\n";); TRACE("grobner_d", tout << pp << "\n";);
if (!eat_scalar_pow(coeff, pp, p.pow())) if (!eat_scalar_pow(coeff, pp, p.pow()))
children.push_back(nex_pow(pp.e(), pp.pow() * p.pow())); children.push_back(nex_pow(pp.e(), pp.pow() * p.pow()));
} }
coeff *= pm.coeff().expt(p.pow()); coeff *= pm->coeff().expt(p.pow());
} }
mul_to_powers(children); mul_to_powers(children);
@ -643,24 +643,28 @@ void nex_creator::sort_join_sum(ptr_vector<nex> & children) {
void nex_creator::simplify_children_of_sum(ptr_vector<nex> & children) { void nex_creator::simplify_children_of_sum(ptr_vector<nex> & children) {
TRACE("grobner_d", print_vector_of_ptrs(children, tout);); TRACE("grobner_d", print_vector_of_ptrs(children, tout););
ptr_vector<nex> to_promote; ptr_vector<nex> to_promote;
bool skipped = false; int skipped = 0;
unsigned j = 0; for(unsigned j = 0; j < children.size(); j++) {
for (nex* e : children) { nex* e = children[j] = simplify(children[j]);
e = simplify(e);
if (e->is_sum()) { if (e->is_sum()) {
to_promote.push_back(e); } to_promote.push_back(e);
else if (is_zero_scalar(e) || (e->is_mul() && e->to_mul().coeff().is_zero())) { } else if (is_zero_scalar(e)) {
skipped = true; skipped ++;
continue; continue;
} } else if (e->is_mul() && to_mul(e)->coeff().is_zero() ) {
else { skipped ++;
if (skipped) continue;
children[j] = e; }else {
j++; unsigned offset = to_promote.size() + skipped;
if (offset) {
children[j - offset] = e;
}
} }
} }
children.shrink(j);
TRACE("grobner_d", print_vector_of_ptrs(children, tout);); TRACE("grobner_d", print_vector_of_ptrs(children, tout););
children.shrink(children.size() - to_promote.size() - skipped);
for (nex *e : to_promote) { for (nex *e : to_promote) {
for (nex *ee : *(to_sum(e)->children_ptr())) { for (nex *ee : *(to_sum(e)->children_ptr())) {
if (!is_zero_scalar(ee)) if (!is_zero_scalar(ee))