mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-05 10:50:24 +00:00
Code Activity

remove an inifinite loop in basic_proportionality

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2018-08-29 10:49:07 +08:00
parent 64ecefdf07
commit dd0c8e4f6b
1 changed files with 20 additions and 20 deletions
Download patch file Download diff file Expand all files Collapse all files

40
src/util/lp/niil_solver.cpp
View file

@ -818,30 +818,30 @@ struct solver::imp {
const auto & m = m_monomials[i_mon]; const auto & m = m_monomials[i_mon];
int sign; int sign;
auto vars = reduce_monomial_to_minimal(m.m_vs, sign); auto vars = reduce_monomial_to_minimal(m.m_vs, sign);
auto vars_copy = vars;
auto v = lp::abs(m_lar_solver.get_column_value_rational(m.m_v)); auto v = lp::abs(m_lar_solver.get_column_value_rational(m.m_v));
// We cross out from vars the "large" variables represented by the mask // We cross out from vars the "large" variables represented by the mask
do { for (unsigned k = 0; k < mask.size(); k++) {
for (unsigned k = 0; k < mask.size(); k++) { if (mask[k] == 0) {
if (mask[k] == 0) { mask[k] = 1;
mask[k] = 1; TRACE("niil_solver", tout << "large[" << k << "] = " << large[k];);
TRACE("niil_solver", tout << "large[" << k << "] = " << large[k];); SASSERT(std::find(vars.begin(), vars.end(), vars_copy[large[k]]) != vars.end());
vars.erase(vars.begin() + large[k]); vars.erase(vars_copy[large[k]]);
std::sort(vars.begin(), vars.end()); std::sort(vars.begin(), vars.end());
// now the value of vars has to be v*sign // now the value of vars has to be v*sign
lpvar j; lpvar j;
if (find_compimenting_monomial(vars, j) && if (find_compimenting_monomial(vars, j) &&
large_lemma_for_proportion_case(m, mask, large, j)) { large_lemma_for_proportion_case(m, mask, large, j)) {
TRACE("niil_solver", print_explanation_and_lemma(tout);); TRACE("niil_solver", print_explanation_and_lemma(tout););
return true; return true;
}
} else {
SASSERT(mask[k] == 1);
mask[k] = 0;
vars.push_back(vars[large[k]]); // vars becomes unsorted
} }
} else {
SASSERT(mask[k] == 1);
mask[k] = 0;
vars.push_back(vars_copy[large[k]]); // vars becomes unsorted
} }
} while(true); }
TRACE("niil_solver", tout << "return false";); TRACE("niil_solver", tout << "return false";);
return false; // we exhausted the mask and did not find the compliment monomial return false; // we exhausted the mask and did not find the compliment monomial
} }