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

integrating NB suggestions

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

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

@ -89,26 +89,26 @@ 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;
int skipped = 0; bool skipped = false;
for(unsigned j = 0; j < children.size(); j++) { unsigned j = 0;
nex_pow& p = children[j]; for (nex_pow& p : children) {
if (eat_scalar_pow(coeff, p, 1)) { if (eat_scalar_pow(coeff, p, 1)) {
skipped++; skipped = true;
continue; continue;
} }
p.e() = simplify(p.e()); p.e() = simplify(p.e());
if ((p.e())->is_mul()) { if ((p.e())->is_mul()) {
skipped = true;
to_promote.push_back(p); to_promote.push_back(p);
} else { } else {
unsigned offset = to_promote.size() + skipped; if (skipped)
if (offset) { children[j] = p;
children[j - offset] = p; j++;
}
} }
} }
children.shrink(children.size() - to_promote.size() - skipped); children.shrink(j);
for (nex_pow & p : to_promote) { for (nex_pow & p : to_promote) {
TRACE("grobner_d", tout << p << "\n";); TRACE("grobner_d", tout << p << "\n";);