diff --git a/src/math/lp/gomory.cpp b/src/math/lp/gomory.cpp index 382308e95..fbba6fa9f 100644 --- a/src/math/lp/gomory.cpp +++ b/src/math/lp/gomory.cpp @@ -375,7 +375,7 @@ bool gomory::is_gomory_cut_target(const row_strip& row) { return true; } -int gomory::find_column() { +int gomory::find_basic_var() { int result = -1; unsigned n = 0; bool boxed = false; @@ -426,17 +426,18 @@ int gomory::find_column() { return result; } -lia_move gomory::cut(lar_term & t, mpq & k, explanation* ex, bool& upper) { +lia_move gomory::operator()(lar_term & t, mpq & k, explanation* ex, bool& upper) { if (s.m_lar_solver->move_non_basic_columns_to_bounds()) { lp_status st = s.m_lar_solver->find_feasible_solution(); (void)st; lp_assert(st == lp_status::FEASIBLE || st == lp_status::OPTIMAL); } - int j = find_column(); + int j = find_basic_var(); if (j == -1) return lia_move::undef; - const row_strip& row = s.m_lar_solver->get_row(s.row_of_basic_column(j)); - SASSERT(s.m_lar_solver->row_is_correct(s.row_of_basic_column(j))); + unsigned r = s.row_of_basic_column(j); + const row_strip& row = s.m_lar_solver->get_row(r); + SASSERT(s.m_lar_solver->row_is_correct(r)); SASSERT(is_gomory_cut_target(row)); upper = true; return cut(t, k, ex, j, row); diff --git a/src/math/lp/gomory.h b/src/math/lp/gomory.h index dbc8120f8..c8f139ed9 100644 --- a/src/math/lp/gomory.h +++ b/src/math/lp/gomory.h @@ -22,17 +22,15 @@ Revision History: #include "math/lp/static_matrix.h" namespace lp { -class int_solver; -class gomory { - class int_solver& s; - int find_column(); - lia_move cut(lar_term & t, mpq & k, explanation* ex, unsigned basic_inf_int_j, const row_strip& row); - bool is_gomory_cut_target(const row_strip& row); - -public : - gomory(int_solver& s): s(s) {} - - lia_move cut(lar_term & t, mpq & k, explanation* ex, bool& upper); - ~gomory(); -}; + class int_solver; + class gomory { + class int_solver& s; + int find_basic_var(); + bool is_gomory_cut_target(const row_strip& row); + lia_move cut(lar_term & t, mpq & k, explanation* ex, unsigned basic_inf_int_j, const row_strip& row); + public: + gomory(int_solver& s): s(s) {} + ~gomory(); + lia_move operator()(lar_term & t, mpq & k, explanation* ex, bool& upper); + }; } diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp index 624213818..cc7d5f240 100644 --- a/src/math/lp/int_solver.cpp +++ b/src/math/lp/int_solver.cpp @@ -261,12 +261,13 @@ bool int_solver::should_gomory_cut() { lia_move int_solver::gomory_cut() { TRACE("int_solver", tout << "gomory " << m_number_of_calls << "\n";); - if (!should_gomory_cut()) - return lia_move::undef; - gomory gc(*this); - return gc.cut(m_t, m_k, m_ex, m_upper); - + if (should_gomory_cut()) { + return gc(m_t, m_k, m_ex, m_upper); + } + else { + return lia_move::undef; + } } void int_solver::try_add_term_to_A_for_hnf(unsigned i) {