From 060c1b0b0ba526d3142c73d4fc933d67c90d239b Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Wed, 11 Dec 2019 09:54:00 -1000
Subject: [PATCH] integrating NB suggestions
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
src/math/lp/nex_creator.cpp | 18 +++++++++---------
1 file changed, 9 insertions(+), 9 deletions(-)
diff --git a/src/math/lp/nex_creator.cpp b/src/math/lp/nex_creator.cpp
index 74f6c2ac6..75e533356 100644
--- a/src/math/lp/nex_creator.cpp
+++ b/src/math/lp/nex_creator.cpp
@@ -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) {
TRACE("grobner_d", print_vector(children, tout););
vector<nex_pow> to_promote;
- int skipped = 0;
- for(unsigned j = 0; j < children.size(); j++) {
- nex_pow& p = children[j];
+ bool skipped = false;
+ unsigned j = 0;
+ for (nex_pow& p : children) {
if (eat_scalar_pow(coeff, p, 1)) {
- skipped++;
+ skipped = true;
continue;
}
p.e() = simplify(p.e());
if ((p.e())->is_mul()) {
+ skipped = true;
to_promote.push_back(p);
} else {
- unsigned offset = to_promote.size() + skipped;
- if (offset) {
- children[j - offset] = p;
- }
+ if (skipped)
+ children[j] = p;
+ j++;
}
}
- children.shrink(children.size() - to_promote.size() - skipped);
+ children.shrink(j);
for (nex_pow & p : to_promote) {
TRACE("grobner_d", tout << p << "\n";);