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

try another sorting of terms to tighten

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-03-14 09:30:32 -07:00 • committed by Lev Nachmanson
parent ec7c61569d
commit 50418fa170
1 changed files with 33 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1389,11 +1389,39 @@ namespace lp {
}
sorted_changed_terms.push_back(j);
}
// Sort by term_weight descending
std::sort(sorted_changed_terms.begin(), sorted_changed_terms.end(),
[this](unsigned j1, unsigned j2) {
return term_weight(lra.get_term(j1)) > term_weight(lra.get_term(j2) );
});
bool sort_by_weight = false;
if (sort_by_weight)
// Sort by term_weight descending
std::sort(sorted_changed_terms.begin(), sorted_changed_terms.end(),
[this](unsigned j1, unsigned j2) {
return term_weight(lra.get_term(j1)) > term_weight(lra.get_term(j2) );
});
else {
std::sort(sorted_changed_terms.begin(), sorted_changed_terms.end(),
[this](unsigned j1, unsigned j2) {
// First check if both columns are boxed
bool j1_is_boxed = lia.is_boxed(j1);
bool j2_is_boxed = lia.is_boxed(j2);
// If one is boxed and the other isn't, prefer the boxed one
if (j1_is_boxed && !j2_is_boxed)
return true;
if (!j1_is_boxed && j2_is_boxed)
return false;
// If both are boxed, compare spans (prefer smaller spans)
if (j1_is_boxed && j2_is_boxed) {
mpq span1 = lra.bound_span_x(j1);
mpq span2 = lra.bound_span_x(j2);
if (span1 != span2)
return span1 < span2;
}
// Fall back to weight comparison
return term_weight(lra.get_term(j1)) > term_weight(lra.get_term(j2));
});
}
lia_move r = lia_move::undef;
// Process sorted terms