diff --git a/src/math/lp/gomory.cpp b/src/math/lp/gomory.cpp index 44f801ae8..ac479d1a2 100644 --- a/src/math/lp/gomory.cpp +++ b/src/math/lp/gomory.cpp @@ -355,7 +355,7 @@ public: }; lia_move gomory::cut(lar_term & t, mpq & k, explanation* ex, unsigned basic_inf_int_j, const row_strip& row) { - create_cut cc(t, k, ex, basic_inf_int_j, row, s); + create_cut cc(t, k, ex, basic_inf_int_j, row, lia); return cc.cut(); } @@ -364,10 +364,10 @@ bool gomory::is_gomory_cut_target(const row_strip& row) { unsigned j; for (const auto & p : row) { j = p.var(); - if (!s.is_base(j) && (!s.at_bound(j) || !is_zero(s.get_value(j).y))) { + if (!lia.is_base(j) && (!lia.at_bound(j) || !is_zero(lia.get_value(j).y))) { TRACE("gomory_cut", tout << "row is not gomory cut target:\n"; - s.display_column(tout, j); - tout << "infinitesimal: " << !is_zero(s.get_value(j).y) << "\n";); + lia.display_column(tout, j); + tout << "infinitesimal: " << !is_zero(lia.get_value(j).y) << "\n";); return false; } } @@ -388,17 +388,17 @@ int gomory::find_basic_var() { // Prefer boxed to non-boxed // Prefer smaller ranges - for (unsigned j : s.lra.r_basis()) { - if (!s.column_is_int_inf(j)) + for (unsigned j : lra.r_basis()) { + if (!lia.column_is_int_inf(j)) continue; - const row_strip& row = s.lra.get_row(s.row_of_basic_column(j)); + const row_strip& row = lra.get_row(lia.row_of_basic_column(j)); if (!is_gomory_cut_target(row)) continue; #if 0 if (is_boxed(j) && (min_row_size == UINT_MAX || 4*row.size() < 5*min_row_size)) { lar_core_solver & lcs = lra.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 = lclia.m_r_upper_bounds()[j].x - lclia.m_r_lower_bounds()[j].x; if (!boxed) { result = j; n = 1; @@ -419,7 +419,7 @@ int gomory::find_basic_var() { if (min_row_size == UINT_MAX || 2*row.size() < min_row_size || - (4*row.size() < 5*min_row_size && s.random() % (++n) == 0)) { + (4*row.size() < 5*min_row_size && lia.random() % (++n) == 0)) { result = j; n = 1; min_row_size = std::min(min_row_size, row.size()); @@ -428,24 +428,24 @@ int gomory::find_basic_var() { return result; } -lia_move gomory::operator()(lar_term & t, mpq & k, explanation* ex, bool& upper) { - if (s.lra.move_non_basic_columns_to_bounds()) { - lp_status st = s.lra.find_feasible_solution(); +lia_move gomory::operator()() { + if (lra.move_non_basic_columns_to_bounds()) { + lp_status st = lra.find_feasible_solution(); (void)st; lp_assert(st == lp_status::FEASIBLE || st == lp_status::OPTIMAL); } int j = find_basic_var(); if (j == -1) return lia_move::undef; - unsigned r = s.row_of_basic_column(j); - const row_strip& row = s.lra.get_row(r); - SASSERT(s.lra.row_is_correct(r)); + unsigned r = lia.row_of_basic_column(j); + const row_strip& row = lra.get_row(r); + SASSERT(lra.row_is_correct(r)); SASSERT(is_gomory_cut_target(row)); - upper = true; - return cut(t, k, ex, j, row); + lia.m_upper = true; + return cut(lia.m_t, lia.m_k, lia.m_ex, j, row); } -gomory::~gomory() { } +gomory::gomory(int_solver& lia): lia(lia), lra(lia.lra) { } } diff --git a/src/math/lp/gomory.h b/src/math/lp/gomory.h index c8f139ed9..58f1288d6 100644 --- a/src/math/lp/gomory.h +++ b/src/math/lp/gomory.h @@ -23,14 +23,16 @@ Revision History: namespace lp { class int_solver; + class lar_solver; class gomory { - class int_solver& s; + class int_solver& lia; + class lar_solver& lra; 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); + gomory(int_solver& lia); + ~gomory() {} + lia_move operator()(); }; } diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp index 080183142..d41c8d024 100644 --- a/src/math/lp/int_solver.cpp +++ b/src/math/lp/int_solver.cpp @@ -3,25 +3,33 @@ Author: Lev Nachmanson */ +#include #include "math/lp/int_solver.h" #include "math/lp/lar_solver.h" #include "math/lp/lp_utils.h" -#include #include "math/lp/monic.h" #include "math/lp/gomory.h" #include "math/lp/int_branch.h" #include "math/lp/int_gcd_test.h" #include "math/lp/int_cube.h" + namespace lp { +int_solver::int_solver(lar_solver& lar_slv) : + lra(lar_slv), + m_number_of_calls(0), + m_hnf_cutter(settings()), + m_hnf_cut_period(settings().hnf_cut_period()) { + lra.set_int_solver(this); +} + // this will allow to enable and disable tracking of the pivot rows struct check_return_helper { lar_solver& lra; bool m_track_pivoted_rows; check_return_helper(lar_solver& ls) : lra(ls), - m_track_pivoted_rows(lra.get_track_pivoted_rows()) - { + m_track_pivoted_rows(lra.get_track_pivoted_rows()) { TRACE("pivoted_rows", tout << "pivoted rows = " << lra.m_mpq_lar_core_solver.m_r_solver.m_pivoted_rows->size() << std::endl;); lra.set_track_pivoted_rows(false); } @@ -42,9 +50,9 @@ lia_move int_solver::check(lp::explanation * e) { m_upper = false; lia_move r = lia_move::undef; - gomory gc(*this); - int_cube cube(*this); - int_branch branch(*this); + gomory gc(*this); + int_cube cube(*this); + int_branch branch(*this); int_gcd_test gcd(*this); if (should_run_gcd_test()) r = gcd(); @@ -59,7 +67,7 @@ lia_move int_solver::check(lp::explanation * e) { ++m_number_of_calls; if (r == lia_move::undef && should_find_cube()) r = cube(); if (r == lia_move::undef && should_hnf_cut()) r = hnf_cut(); - if (r == lia_move::undef && should_gomory_cut()) r = gc(m_t, m_k, m_ex, m_upper); + if (r == lia_move::undef && should_gomory_cut()) r = gc(); if (r == lia_move::undef) r = branch(); return r; } @@ -140,6 +148,10 @@ const impq& int_solver::upper_bound(unsigned j) const { return lra.column_upper_bound(j); } +const impq& int_solver::lower_bound(unsigned j) const { + return lra.column_lower_bound(j); +} + bool int_solver::is_term(unsigned j) const { return lra.column_corresponds_to_term(j); } @@ -148,7 +160,6 @@ unsigned int_solver::column_count() const { return lra.column_count(); } - bool int_solver::should_find_cube() { return m_number_of_calls % settings().m_int_find_cube_period == 0; } @@ -311,17 +322,6 @@ lia_move int_solver::patch_nbasic_columns() { return lia_move::undef; } -// TBD: move to gcd-test - - -int_solver::int_solver(lar_solver& lar_slv) : - lra(lar_slv), - m_number_of_calls(0), - m_hnf_cutter(settings()), - m_hnf_cut_period(settings().hnf_cut_period()) { - lra.set_int_solver(this); -} - bool int_solver::has_lower(unsigned j) const { switch (lra.m_mpq_lar_core_solver.m_column_types()[j]) { @@ -616,10 +616,6 @@ bool int_solver::non_basic_columns_are_at_bounds() const { } return true; } - -const impq& int_solver::lower_bound(unsigned j) const { - return lra.column_lower_bound(j); -} } diff --git a/src/math/lp/int_solver.h b/src/math/lp/int_solver.h index 735ab46b3..7ebc9ce5d 100644 --- a/src/math/lp/int_solver.h +++ b/src/math/lp/int_solver.h @@ -30,28 +30,24 @@ Revision History: namespace lp { class lar_solver; -template -struct lp_constraint; - - class int_solver { + friend class create_cut; friend class gomory; friend class int_cube; friend class int_branch; friend class int_gcd_test; -public: - // fields + lar_solver& lra; unsigned m_number_of_calls; - lar_term m_t; // the term to return in the cut - mpq m_k; // the right side of the cut - explanation *m_ex; // the conflict explanation - bool m_upper; // we have a cut m_t*x <= k if m_upper is true nad m_t*x >= k otherwise + lar_term m_t; // the term to return in the cut + mpq m_k; // the right side of the cut + explanation *m_ex; // the conflict explanation + bool m_upper; // we have a cut m_t*x <= k if m_upper is true nad m_t*x >= k otherwise hnf_cutter m_hnf_cutter; unsigned m_hnf_cut_period; - // methods - int_solver(lar_solver& lp); +public: + int_solver(lar_solver& lp); // main function to check that the solution provided by lar_solver is valid for integral values, // or provide a way of how it can be adjusted. @@ -59,7 +55,7 @@ public: lar_term const& get_term() const { return m_t; } mpq const& get_offset() const { return m_k; } bool is_upper() const { return m_upper; } - lia_move check_wrapper(lar_term& t, mpq& k, explanation& ex); + //lia_move check_wrapper(lar_term& t, mpq& k, explanation& ex); bool is_base(unsigned j) const; bool is_real(unsigned j) const; const impq & lower_bound(unsigned j) const; @@ -109,7 +105,6 @@ public: unsigned column_count() const; bool all_columns_are_bounded() const; void find_feasible_solution(); - lia_move run_gcd_test(); lia_move hnf_cut(); lia_move make_hnf_cut(); bool init_terms_for_hnf_cut();