Skip to content

Commit c1b1a8c

Browse files
committed
remove term sorting by the span
Signed-off-by: Lev Nachmanson <[email protected]>
1 parent e532308 commit c1b1a8c

File tree

1 file changed

+5
-32
lines changed

1 file changed

+5
-32
lines changed

src/math/lp/dioph_eq.cpp

+5-32
Original file line numberDiff line numberDiff line change
@@ -1408,39 +1408,12 @@ namespace lp {
14081408
sorted_changed_terms.push_back(j);
14091409
}
14101410

1411-
bool sort_by_weight = true;
1412-
if (sort_by_weight)
1413-
// Sort by term_weight descending
1414-
std::sort(sorted_changed_terms.begin(), sorted_changed_terms.end(),
1415-
[this](unsigned j1, unsigned j2) {
1416-
return term_weight(lra.get_term(j1)) > term_weight(lra.get_term(j2) );
1417-
});
1418-
else {
1419-
std::sort(sorted_changed_terms.begin(), sorted_changed_terms.end(),
1420-
[this](unsigned j1, unsigned j2) {
1421-
// First check if both columns are boxed
1422-
bool j1_is_boxed = lia.is_boxed(j1);
1423-
bool j2_is_boxed = lia.is_boxed(j2);
1424-
1425-
// If one is boxed and the other isn't, prefer the boxed one
1426-
if (j1_is_boxed && !j2_is_boxed)
1427-
return true;
1428-
if (!j1_is_boxed && j2_is_boxed)
1429-
return false;
1430-
1431-
// If both are boxed, compare spans (prefer smaller spans)
1432-
if (j1_is_boxed && j2_is_boxed) {
1433-
mpq span1 = lra.bound_span_x(j1);
1434-
mpq span2 = lra.bound_span_x(j2);
1435-
if (span1 != span2)
1436-
return span1 < span2;
1437-
}
1411+
// Sort by term_weight descending
1412+
std::sort(sorted_changed_terms.begin(), sorted_changed_terms.end(),
1413+
[this](unsigned j1, unsigned j2) {
1414+
return term_weight(lra.get_term(j1)) > term_weight(lra.get_term(j2) );
1415+
});
14381416

1439-
// Fall back to weight comparison
1440-
return term_weight(lra.get_term(j1)) > term_weight(lra.get_term(j2));
1441-
});
1442-
}
1443-
14441417
lia_move r = lia_move::undef;
14451418
// Process sorted terms
14461419
TRACE("dio",

0 commit comments

Comments
 (0)