mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-05 21:53:23 +00:00
Code Activity

merge fix for non-termination in pdd_grobner

Browse source
This commit is contained in:
Nikolaj Bjorner 2019-12-29 21:30:36 -08:00
parent 3b16f129bb
commit 57c66006ad
1 changed files with 2 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/math/grobner/pdd_grobner.cpp
View file

@ -194,8 +194,8 @@ namespace dd {
(simplify_linear_step(true) || (simplify_linear_step(true) ||
simplify_elim_pure_step() || simplify_elim_pure_step() ||
simplify_cc_step() || simplify_cc_step() ||
simplify_linear_step(false) ||
simplify_leaf_step() || simplify_leaf_step() ||
simplify_linear_step(false) ||
/*simplify_elim_dual_step() ||*/ /*simplify_elim_dual_step() ||*/
false)) { false)) {
DEBUG_CODE(invariant();); DEBUG_CODE(invariant(););
@ -334,7 +334,6 @@ namespace dd {
bool grobner::simplify_leaf_step() { bool grobner::simplify_leaf_step() {
TRACE("grobner", tout << "leaf\n";); TRACE("grobner", tout << "leaf\n";);
use_list_t use_list = get_use_list(); use_list_t use_list = get_use_list();
bool reduced = false;
equation_vector leaves; equation_vector leaves;
for (unsigned i = 0; i < m_to_simplify.size(); ++i) { for (unsigned i = 0; i < m_to_simplify.size(); ++i) {
equation* e = m_to_simplify[i]; equation* e = m_to_simplify[i];
@ -366,10 +365,9 @@ namespace dd {
pop_equation(e2); pop_equation(e2);
push_equation(to_simplify, e2); push_equation(to_simplify, e2);
} }
reduced = true;
} }
} }
return reduced; return false;
} }
/** /**