mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

try another sort in tightening

Browse source
This commit is contained in:
Lev Nachmanson 2025-02-07 14:54:26 -10:00 committed by Lev Nachmanson
parent 5b0b224a5c
commit b6701d57f9
1 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1348,7 +1348,7 @@ namespace lp {
// Look up j in columns_to_terms map // Look up j in columns_to_terms map
auto it = m_columns_to_terms.find(j); auto it = m_columns_to_terms.find(j);
if (it != m_columns_to_terms.end()) if (it != m_columns_to_terms.end())
weight += static_cast<unsigned>(it->second.size()); weight = std::max(weight, static_cast<unsigned>(it->second.size()));
} }
return weight; return weight;
} }
@ -1371,7 +1371,7 @@ namespace lp {
// Sort by term_weight descending // Sort by term_weight descending
std::sort(sorted_changed_terms.begin(), sorted_changed_terms.end(), std::sort(sorted_changed_terms.begin(), sorted_changed_terms.end(),
[this](unsigned j1, unsigned j2) { [this](unsigned j1, unsigned j2) {
return term_weight(lra.get_term(j1)) > term_weight(lra.get_term(j2)); return term_weight(lra.get_term(j1)) > term_weight(lra.get_term(j2) );
}); });
lia_move r = lia_move::undef; lia_move r = lia_move::undef;
@ -1603,8 +1603,8 @@ namespace lp {
} }
lia_move process_f() { lia_move process_f() {
while (rewrite_eqs()) { while (rewrite_eqs()) {}
}
if (m_conflict_index != UINT_MAX) { if (m_conflict_index != UINT_MAX) {
lra.stats().m_dio_rewrite_conflicts++; lra.stats().m_dio_rewrite_conflicts++;
return lia_move::conflict; return lia_move::conflict;