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

cosmitic changes in int_branch.cpp

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-04-28 14:35:50 -07:00
parent d5162d92ad
commit 35e3df49e2
1 changed files with 33 additions and 26 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

59
src/math/lp/int_branch.cpp
View file

@ -50,7 +50,7 @@ lia_move int_branch::create_branch_on_column(int j) {
return lia_move::branch; return lia_move::branch;
} }
int int_branch::find_inf_int_base_column() { int int_branch::find_inf_int_base_column() {
int result = -1; int result = -1;
@ -59,41 +59,48 @@ int int_branch::find_inf_int_base_column() {
mpq small_range_thresold(1024); mpq small_range_thresold(1024);
unsigned n = 0; unsigned n = 0;
lar_core_solver & lcs = lra.m_mpq_lar_core_solver; lar_core_solver & lcs = lra.m_mpq_lar_core_solver;
bool small = false;
unsigned prev_usage; unsigned prev_usage;
for (unsigned j : lra.r_basis()) { unsigned k = 0;
SASSERT(!lia.column_is_int_inf(j) || !lia.is_fixed(j)); 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)) if (!lia.column_is_int_inf(j))
continue; continue;
bool boxed = lia.is_boxed(j); usage = lra.usage_in_terms(j);
unsigned usage = 2 * 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) {
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;
result = j; result = j;
k++;
n = 1; n = 1;
} else if (result == -1 || prev_usage < usage) { break;
}
if (n == 0 || usage > prev_usage) {
result = j; result = j;
prev_usage = usage; prev_usage = usage;
n = 1; n = 1;
} else if (prev_usage == usage && lia.random() % (++n) == 0) { } else if (usage == prev_usage && (lia.random() % (++n) == 0)) {
result = j; 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; return result;
} }