mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-20 11:22:04 +00:00
Code Activity

fix #2949 fix #2955 experiment with cut selection

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-02-08 10:41:35 -08:00
parent f29b455611
commit 094f203167
1 changed files with 7 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

18
src/math/lp/int_solver.cpp
View file

@ -45,10 +45,8 @@ int int_solver::find_gomory_cut_column() {
mpq min_range; mpq min_range;
// Prefer smaller row size // Prefer smaller row size
#if 0
// Prefer boxed to non-boxed // Prefer boxed to non-boxed
// Prefer smaller ranges // Prefer smaller ranges
#endif
for (unsigned j : m_lar_solver->r_basis()) { for (unsigned j : m_lar_solver->r_basis()) {
if (!column_is_int_inf(j)) if (!column_is_int_inf(j))
@ -56,7 +54,7 @@ int int_solver::find_gomory_cut_column() {
const row_strip<mpq>& row = m_lar_solver->get_row(row_of_basic_column(j)); const row_strip<mpq>& row = m_lar_solver->get_row(row_of_basic_column(j));
if (!is_gomory_cut_target(row)) if (!is_gomory_cut_target(row))
continue; continue;
#if 1
if (is_boxed(j) && (min_row_size == UINT_MAX || 4*row.size() < 5*min_row_size)) { if (is_boxed(j) && (min_row_size == UINT_MAX || 4*row.size() < 5*min_row_size)) {
lar_core_solver & lcs = m_lar_solver->m_mpq_lar_core_solver; lar_core_solver & lcs = m_lar_solver->m_mpq_lar_core_solver;
auto new_range = lcs.m_r_upper_bounds()[j].x - lcs.m_r_lower_bounds()[j].x; auto new_range = lcs.m_r_upper_bounds()[j].x - lcs.m_r_lower_bounds()[j].x;
@ -76,7 +74,6 @@ int int_solver::find_gomory_cut_column() {
continue; continue;
} }
} }
#endif
if (min_row_size == UINT_MAX || (4*row.size() < 5*min_row_size && random() % (++n) == 0)) { if (min_row_size == UINT_MAX || (4*row.size() < 5*min_row_size && random() % (++n) == 0)) {
result = j; result = j;
n = 1; n = 1;
@ -191,12 +188,8 @@ lia_move int_solver::mk_gomory_cut( unsigned inf_col, const row_strip<mpq> & row
lia_move int_solver::proceed_with_gomory_cut(unsigned j) { lia_move int_solver::proceed_with_gomory_cut(unsigned j) {
const row_strip<mpq>& row = m_lar_solver->get_row(row_of_basic_column(j)); const row_strip<mpq>& row = m_lar_solver->get_row(row_of_basic_column(j));
SASSERT(m_lar_solver->row_is_correct(row_of_basic_column(j))); SASSERT(m_lar_solver->row_is_correct(row_of_basic_column(j)));
SASSERT(is_gomory_cut_target(row));
if (!is_gomory_cut_target(row))
return create_branch_on_column(j);
m_upper = true; m_upper = true;
return mk_gomory_cut(j, row); return mk_gomory_cut(j, row);
} }
@ -353,13 +346,12 @@ lia_move int_solver::gomory_cut() {
lp_assert(st == lp_status::FEASIBLE || st == lp_status::OPTIMAL); lp_assert(st == lp_status::FEASIBLE || st == lp_status::OPTIMAL);
} }
// int j = find_inf_int_base_column();
int j = find_gomory_cut_column(); int j = find_gomory_cut_column();
if (j == -1) { if (j != -1) {
return proceed_with_gomory_cut(j);
}
j = find_inf_int_nbasis_column(); j = find_inf_int_nbasis_column();
return j == -1? lia_move::sat : create_branch_on_column(j); return j == -1? lia_move::sat : create_branch_on_column(j);
}
return proceed_with_gomory_cut(j);
} }
void int_solver::try_add_term_to_A_for_hnf(unsigned i) { void int_solver::try_add_term_to_A_for_hnf(unsigned i) {