mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-07 06:33:23 +00:00
Code Activity

move all gomory functionality into gomory class

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-02-08 15:03:58 -08:00
parent d44855f262
commit c12c9a75e6
3 changed files with 23 additions and 23 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/math/lp/gomory.cpp
View file

@ -375,7 +375,7 @@ bool gomory::is_gomory_cut_target(const row_strip<mpq>& row) {
return true; return true;
} }
int gomory::find_column() { int gomory::find_basic_var() {
int result = -1; int result = -1;
unsigned n = 0; unsigned n = 0;
bool boxed = false; bool boxed = false;
@ -426,17 +426,18 @@ int gomory::find_column() {
return result; 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()) { if (s.m_lar_solver->move_non_basic_columns_to_bounds()) {
lp_status st = s.m_lar_solver->find_feasible_solution(); lp_status st = s.m_lar_solver->find_feasible_solution();
(void)st; (void)st;
lp_assert(st == lp_status::FEASIBLE || st == lp_status::OPTIMAL); 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; if (j == -1) return lia_move::undef;
const row_strip<mpq>& row = s.m_lar_solver->get_row(s.row_of_basic_column(j)); unsigned r = s.row_of_basic_column(j);
SASSERT(s.m_lar_solver->row_is_correct(s.row_of_basic_column(j))); const row_strip<mpq>& row = s.m_lar_solver->get_row(r);
SASSERT(s.m_lar_solver->row_is_correct(r));
SASSERT(is_gomory_cut_target(row)); SASSERT(is_gomory_cut_target(row));
upper = true; upper = true;
return cut(t, k, ex, j, row); return cut(t, k, ex, j, row);

8
src/math/lp/gomory.h
View file

@ -25,14 +25,12 @@ namespace lp {
class int_solver; class int_solver;
class gomory { class gomory {
class int_solver& s; class int_solver& s;
int find_column(); int find_basic_var();
lia_move cut(lar_term & t, mpq & k, explanation* ex, unsigned basic_inf_int_j, const row_strip<mpq>& row);
bool is_gomory_cut_target(const row_strip<mpq>& row); bool is_gomory_cut_target(const row_strip<mpq>& row);
lia_move cut(lar_term & t, mpq & k, explanation* ex, unsigned basic_inf_int_j, const row_strip<mpq>& row);
public: public:
gomory(int_solver& s): s(s) {} gomory(int_solver& s): s(s) {}
lia_move cut(lar_term & t, mpq & k, explanation* ex, bool& upper);
~gomory(); ~gomory();
lia_move operator()(lar_term & t, mpq & k, explanation* ex, bool& upper);
}; };
} }

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

@ -261,12 +261,13 @@ bool int_solver::should_gomory_cut() {
lia_move int_solver::gomory_cut() { lia_move int_solver::gomory_cut() {
TRACE("int_solver", tout << "gomory " << m_number_of_calls << "\n";); TRACE("int_solver", tout << "gomory " << m_number_of_calls << "\n";);
if (!should_gomory_cut())
return lia_move::undef;
gomory gc(*this); 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) { void int_solver::try_add_term_to_A_for_hnf(unsigned i) {