From 35e3df49e2f9e12ec6970551d479d57531f309e6 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Tue, 28 Apr 2020 14:35:50 -0700
Subject: [PATCH] cosmitic changes in int_branch.cpp
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
src/math/lp/int_branch.cpp | 59 +++++++++++++++++++++-----------------
1 file changed, 33 insertions(+), 26 deletions(-)
diff --git a/src/math/lp/int_branch.cpp b/src/math/lp/int_branch.cpp
index a283497c4..3976a0d3c 100644
--- a/src/math/lp/int_branch.cpp
+++ b/src/math/lp/int_branch.cpp
@@ -50,7 +50,7 @@ lia_move int_branch::create_branch_on_column(int j) {
return lia_move::branch;
}
-
+
int int_branch::find_inf_int_base_column() {
int result = -1;
@@ -59,41 +59,48 @@ int int_branch::find_inf_int_base_column() {
mpq small_range_thresold(1024);
unsigned n = 0;
lar_core_solver & lcs = lra.m_mpq_lar_core_solver;
- bool small = false;
unsigned prev_usage;
- for (unsigned j : lra.r_basis()) {
- SASSERT(!lia.column_is_int_inf(j) || !lia.is_fixed(j));
+ unsigned k = 0;
+ unsigned usage;
+ unsigned j;
+ // this loop looks for a column with the most usages, but breaks when
+ // a column with a small span of bounds is found
+ for (; k < lra.r_basis().size(); k++) {
+ j = lra.r_basis()[k];
if (!lia.column_is_int_inf(j))
continue;
- bool boxed = lia.is_boxed(j);
- unsigned usage = 2 * lra.usage_in_terms(j);
- if (small) {
- if (!boxed)
- continue;
- new_range = lcs.m_r_upper_bounds()[j].x - lcs.m_r_lower_bounds()[j].x - rational(usage);
- if (new_range <= small_range_thresold) {
- if (new_range < range) {
- n = 1;
- result = j;
- range = new_range;
- } else if (new_range == range && lia.random() % (++n) == 0) {
- result = j;
- }
- }
- } else if (boxed && (
- (range = lcs.m_r_upper_bounds()[j].x - lcs.m_r_lower_bounds()[j].x - rational(usage))
- <= small_range_thresold)) {
- small = true;
+ usage = lra.usage_in_terms(j);
+ if (lia.is_boxed(j) && (range = lcs.m_r_upper_bounds()[j].x - lcs.m_r_lower_bounds()[j].x - rational(2*usage)) <= small_range_thresold) {
result = j;
+ k++;
n = 1;
- } else if (result == -1 || prev_usage < usage) {
+ break;
+ }
+ if (n == 0 || usage > prev_usage) {
result = j;
prev_usage = usage;
- n = 1;
- } else if (prev_usage == usage && lia.random() % (++n) == 0) {
+ n = 1;
+ } else if (usage == prev_usage && (lia.random() % (++n) == 0)) {
result = j;
}
}
+ SASSERT(k == lra.r_basis().size() || n == 1);
+ // this loop looks for boxed columns with a small span
+ for (; k < lra.r_basis().size(); k++) {
+ j = lra.r_basis()[k];
+ usage = lra.usage_in_terms(j);
+ if (!lia.column_is_int_inf(j) || !lia.is_boxed(j))
+ continue;
+ SASSERT(!lia.is_fixed(j));
+ new_range = lcs.m_r_upper_bounds()[j].x - lcs.m_r_lower_bounds()[j].x - rational(2*usage);
+ if (new_range < range) {
+ n = 1;
+ result = j;
+ range = new_range;
+ } else if (new_range == range && (lia.random() % (++n) == 0)) {
+ result = j;
+ }
+ }
return result;
}