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 10:06:18 -10:00
parent 060c1b0b0b
commit 617e1387f4
1 changed files with 10 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -643,27 +643,29 @@ 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;
int skipped = 0; bool skipped = false;
for(unsigned j = 0; j < children.size(); j++) { unsigned k = 0;
for (unsigned j = 0; j < children.size(); j++) {
nex* e = children[j] = simplify(children[j]); nex* e = children[j] = simplify(children[j]);
if (e->is_sum()) { if (e->is_sum()) {
skipped = true;
to_promote.push_back(e); to_promote.push_back(e);
} else if (is_zero_scalar(e)) { } else if (is_zero_scalar(e)) {
skipped ++; skipped = true;
continue; continue;
} else if (e->is_mul() && to_mul(e)->coeff().is_zero() ) { } else if (e->is_mul() && to_mul(e)->coeff().is_zero() ) {
skipped ++; skipped = true;
continue; continue;
}else { }else {
unsigned offset = to_promote.size() + skipped; if (skipped) {
if (offset) { children[k] = e;
children[j - offset] = e;
} }
k++;
} }
} }
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); children.shrink(k);
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())) {