mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 17:45:32 +00:00
Code Activity

nits

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-03-15 18:17:27 -07:00 • committed by Lev Nachmanson
parent 488c74d3cc
commit 00277ba3cf
1 changed files with 12 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

19
src/math/lp/dioph_eq.cpp
View file

@ -1397,7 +1397,7 @@ namespace lp {
std_vector<unsigned> sorted_changed_terms;
std_vector<unsigned> processed_terms;
m_tightened_columns.reset();
for (unsigned j: m_terms_to_tighten) {
for (unsigned j: m_terms_to_tighten) {
if (j >= lra.column_count() ||
!lra.column_has_term(j) ||
lra.column_is_free(j) ||
@ -1423,14 +1423,19 @@ namespace lp {
);
for (unsigned j : sorted_changed_terms) {
m_terms_to_tighten.remove(j);
r = tighten_bounds_for_term_column(j);
if (r != lia_move::undef) {
auto r0 = tighten_bounds_for_term_column(j);
if (r0 == lia_move::conflict) {
r = r0;
break;
}
}
else if (r0 == lia_move::continue_with_check)
r = r0;
else if (r0 == lia_move::branch && r == lia_move::undef)
r = r0;
}
for (unsigned j :processed_terms) {
for (unsigned j : processed_terms)
m_terms_to_tighten.remove(j);
}
TRACE("dio", tout << r << "\n");
return r;
}
@ -1802,10 +1807,10 @@ namespace lp {
lia_move ret = process_f(f_vector);
if (ret != lia_move::undef)
return ret;
TRACE("dio", print_S(tout););
ret = tighten_terms_with_S();
if (ret == lia_move::conflict)
lra.stats().m_dio_tighten_conflicts++;
TRACE("dio", print_S(tout););
return ret;
}