Skip to content

Commit e846c2a

Browse files
committed
try another sorting of terms to tighten
Signed-off-by: Lev Nachmanson <[email protected]>
1 parent 364abb6 commit e846c2a

File tree

1 file changed

+33
-5
lines changed

1 file changed

+33
-5
lines changed

src/math/lp/dioph_eq.cpp

+33-5
Original file line numberDiff line numberDiff line change
@@ -1389,11 +1389,39 @@ namespace lp {
13891389
}
13901390
sorted_changed_terms.push_back(j);
13911391
}
1392-
// Sort by term_weight descending
1393-
std::sort(sorted_changed_terms.begin(), sorted_changed_terms.end(),
1394-
[this](unsigned j1, unsigned j2) {
1395-
return term_weight(lra.get_term(j1)) > term_weight(lra.get_term(j2) );
1396-
});
1392+
1393+
bool sort_by_weight = false;
1394+
if (sort_by_weight)
1395+
// Sort by term_weight descending
1396+
std::sort(sorted_changed_terms.begin(), sorted_changed_terms.end(),
1397+
[this](unsigned j1, unsigned j2) {
1398+
return term_weight(lra.get_term(j1)) > term_weight(lra.get_term(j2) );
1399+
});
1400+
else {
1401+
std::sort(sorted_changed_terms.begin(), sorted_changed_terms.end(),
1402+
[this](unsigned j1, unsigned j2) {
1403+
// First check if both columns are boxed
1404+
bool j1_is_boxed = lia.is_boxed(j1);
1405+
bool j2_is_boxed = lia.is_boxed(j2);
1406+
1407+
// If one is boxed and the other isn't, prefer the boxed one
1408+
if (j1_is_boxed && !j2_is_boxed)
1409+
return true;
1410+
if (!j1_is_boxed && j2_is_boxed)
1411+
return false;
1412+
1413+
// If both are boxed, compare spans (prefer smaller spans)
1414+
if (j1_is_boxed && j2_is_boxed) {
1415+
mpq span1 = lra.bound_span_x(j1);
1416+
mpq span2 = lra.bound_span_x(j2);
1417+
if (span1 != span2)
1418+
return span1 < span2;
1419+
}
1420+
1421+
// Fall back to weight comparison
1422+
return term_weight(lra.get_term(j1)) > term_weight(lra.get_term(j2));
1423+
});
1424+
}
13971425

13981426
lia_move r = lia_move::undef;
13991427
// Process sorted terms

0 commit comments

Comments
 (0)