diff --git a/src/util/lp/int_solver.cpp b/src/util/lp/int_solver.cpp index f40fbfb42..90dfef767 100644 --- a/src/util/lp/int_solver.cpp +++ b/src/util/lp/int_solver.cpp @@ -21,7 +21,6 @@ void int_solver::fix_non_base_columns() { return; if (m_lar_solver->find_feasible_solution() == lp_status::INFEASIBLE) failed(); - init_inf_int_set(); lp_assert(is_feasible() && inf_int_set_is_correct()); } @@ -61,14 +60,22 @@ void int_solver::trace_inf_rows() const { ); } +int_set& int_solver::inf_int_set() { + return m_lar_solver->m_inf_int_set; +} + +const int_set& int_solver::inf_int_set() const { + return m_lar_solver->m_inf_int_set; +} + int int_solver::find_inf_int_base_column() { - if (m_inf_int_set.is_empty()) + if (inf_int_set().is_empty()) return -1; int j = find_inf_int_boxed_base_column_with_smallest_range(); if (j != -1) return j; - unsigned k = settings().random_next() % m_inf_int_set.m_index.size(); - return m_inf_int_set.m_index[k]; + unsigned k = settings().random_next() % inf_int_set().m_index.size(); + return inf_int_set().m_index[k]; } int int_solver::find_inf_int_boxed_base_column_with_smallest_range() { @@ -79,7 +86,7 @@ int int_solver::find_inf_int_boxed_base_column_with_smallest_range() { unsigned n = 0; lar_core_solver & lcs = m_lar_solver->m_mpq_lar_core_solver; - for (int j : m_inf_int_set.m_index) { + for (int j : inf_int_set().m_index) { lp_assert(is_base(j) && column_is_int_inf(j)); if (!is_boxed(j)) continue; @@ -331,7 +338,6 @@ lia_move int_solver::mk_gomory_cut(lar_term& t, mpq& k, explanation & expl) { } void int_solver::init_check_data() { - init_inf_int_set(); unsigned n = m_lar_solver->A_r().column_count(); m_old_values_set.resize(n); m_old_values_data.resize(n); @@ -402,12 +408,13 @@ lia_move int_solver::check(lar_term& t, mpq& k, explanation& ex) { if ((++m_branch_cut_counter) % settings().m_int_branch_cut_threshold == 0) { - move_non_base_vars_to_bounds(); + move_non_base_vars_to_bounds(); // todo track changed variables lp_status st = m_lar_solver->find_feasible_solution(); if (st != lp_status::FEASIBLE && st != lp_status::OPTIMAL) { return lia_move::give_up; } - init_inf_int_set(); // todo - can we avoid this call? + lp_assert(inf_int_set_is_correct()); + // init_inf_int_set(); // todo - can we avoid this call? int j = find_inf_int_base_column(); if (j != -1) { // setup the call for gomory cut @@ -862,7 +869,7 @@ void int_solver::display_column(std::ostream & out, unsigned j) const { bool int_solver::inf_int_set_is_correct() const { for (unsigned j = 0; j < m_lar_solver->A_r().column_count(); j++) { - if (m_inf_int_set.contains(j) != (is_int(j) && (!value_is_int(j)))) + if (inf_int_set().contains(j) != (is_int(j) && (!value_is_int(j)))) return false; } return true; @@ -872,20 +879,11 @@ bool int_solver::column_is_int_inf(unsigned j) const { return is_int(j) && (!value_is_int(j)); } -void int_solver::init_inf_int_set() { - m_inf_int_set.clear(); - m_inf_int_set.resize(m_lar_solver->A_r().column_count()); - for (unsigned j = 0; j < m_lar_solver->A_r().column_count(); j++) { - if (column_is_int_inf(j)) - m_inf_int_set.insert(j); - } -} - void int_solver::update_column_in_int_inf_set(unsigned j) { if (is_int(j) && (!value_is_int(j))) - m_inf_int_set.insert(j); + inf_int_set().insert(j); else - m_inf_int_set.erase(j); + inf_int_set().erase(j); } bool int_solver::is_base(unsigned j) const { diff --git a/src/util/lp/int_solver.h b/src/util/lp/int_solver.h index b5a7e74f5..104e9b321 100644 --- a/src/util/lp/int_solver.h +++ b/src/util/lp/int_solver.h @@ -34,13 +34,15 @@ public: lar_solver *m_lar_solver; int_set m_old_values_set; vector m_old_values_data; - int_set m_inf_int_set; unsigned m_branch_cut_counter; linear_combination_iterator* m_iter_on_gomory_row; unsigned m_gomory_cut_inf_column; bool m_found_free_var_in_gomory_row; + // methods int_solver(lar_solver* lp); + int_set& inf_int_set(); + const int_set& inf_int_set() const; // main function to check that solution provided by lar_solver is valid for integral values, // or provide a way of how it can be adjusted. lia_move check(lar_term& t, mpq& k, explanation& ex); @@ -96,7 +98,6 @@ private: const impq & get_value(unsigned j) const; void display_column(std::ostream & out, unsigned j) const; bool inf_int_set_is_correct() const; - void init_inf_int_set(); void update_column_in_int_inf_set(unsigned j); bool column_is_int_inf(unsigned j) const; void trace_inf_rows() const; diff --git a/src/util/lp/lar_solver.cpp b/src/util/lp/lar_solver.cpp index e8235c839..e7ef4f748 100644 --- a/src/util/lp/lar_solver.cpp +++ b/src/util/lp/lar_solver.cpp @@ -30,7 +30,17 @@ void clear() {lp_assert(false); // not implemented lar_solver::lar_solver() : m_status(lp_status::OPTIMAL), m_infeasible_column_index(-1), m_terms_start_index(1000000), - m_mpq_lar_core_solver(m_settings, *this) + m_mpq_lar_core_solver(m_settings, *this), + m_tracker_of_x_change([&](unsigned j, const impq & x){ + if (!var_is_int(j)) { + lp_assert(m_inf_int_set.contains(j) == false); + return; + } + if (m_mpq_lar_core_solver.m_r_x[j].is_int()) + m_inf_int_set.erase(j); + else + m_inf_int_set.insert(j); + }) { } @@ -279,6 +289,10 @@ lp_status lar_solver::get_status() const { return m_status;} void lar_solver::set_status(lp_status s) {m_status = s;} +bool lar_solver::has_int_var() const { + return m_mpq_lar_core_solver.m_r_solver.m_tracker_of_x_change != nullptr; +} + lp_status lar_solver::find_feasible_solution() { m_settings.st().m_make_feasible++; if (A_r().column_count() > m_settings.st().m_max_cols) @@ -288,6 +302,10 @@ lp_status lar_solver::find_feasible_solution() { if (strategy_is_undecided()) decide_on_strategy_and_adjust_initial_state(); + if (has_int_var()) { + m_inf_int_set.resize(A_r().column_count()); + } + m_mpq_lar_core_solver.m_r_solver.m_look_for_feasible_solution_only = true; return solve(); } @@ -1474,6 +1492,9 @@ var_index lar_solver::add_var(unsigned ext_j, bool is_int) { m_columns_to_ul_pairs.push_back(ul_pair(static_cast(-1))); add_non_basic_var_to_core_fields(ext_j, is_int); lp_assert(sizes_are_correct()); + if (is_int) { + m_mpq_lar_core_solver.m_r_solver.set_tracker_of_x(& m_tracker_of_x_change); + } return i; } diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h index 8189fb4b8..df4df5ca1 100644 --- a/src/util/lp/lar_solver.h +++ b/src/util/lp/lar_solver.h @@ -68,7 +68,8 @@ public: lar_core_solver m_mpq_lar_core_solver; unsigned constraint_count() const; const lar_base_constraint& get_constraint(unsigned ci) const; - + std::function m_tracker_of_x_change; + int_set m_inf_int_set; ////////////////// methods //////////////////////////////// static_matrix> & A_r(); static_matrix> const & A_r() const; @@ -473,5 +474,7 @@ public: t.clear(); t = lar_term(pol_after_subs, v); } + + bool has_int_var() const; }; } diff --git a/src/util/lp/lp_core_solver_base.h b/src/util/lp/lp_core_solver_base.h index 12c93ec93..0a07055a4 100644 --- a/src/util/lp/lp_core_solver_base.h +++ b/src/util/lp/lp_core_solver_base.h @@ -69,6 +69,12 @@ public: bool m_tracing_basis_changes; int_set* m_pivoted_rows; bool m_look_for_feasible_solution_only; + std::function * m_tracker_of_x_change; + + void set_tracker_of_x(std::function* tracker) { + m_tracker_of_x_change = tracker; + } + void start_tracing_basis_changes() { m_trace_of_basis_change_vector.resize(0); m_tracing_basis_changes = true; @@ -670,16 +676,20 @@ public: void update_column_in_inf_set(unsigned j) { if (column_is_feasible(j)) { - m_inf_set.erase(j); + remove_column_from_inf_set(j); } else { - m_inf_set.insert(j); + insert_column_into_inf_set(j); } } void insert_column_into_inf_set(unsigned j) { + if (m_tracker_of_x_change != nullptr) + (*m_tracker_of_x_change)(j, m_x[j]); m_inf_set.insert(j); lp_assert(!column_is_feasible(j)); } void remove_column_from_inf_set(unsigned j) { + if (m_tracker_of_x_change != nullptr) + (*m_tracker_of_x_change)(j, m_x[j]); m_inf_set.erase(j); lp_assert(column_is_feasible(j)); } diff --git a/src/util/lp/lp_core_solver_base.hpp b/src/util/lp/lp_core_solver_base.hpp index bd3410b45..5ac6c4c22 100644 --- a/src/util/lp/lp_core_solver_base.hpp +++ b/src/util/lp/lp_core_solver_base.hpp @@ -52,7 +52,8 @@ lp_core_solver_base(static_matrix & A, m_steepest_edge_coefficients(A.column_count()), m_tracing_basis_changes(false), m_pivoted_rows(nullptr), - m_look_for_feasible_solution_only(false) { + m_look_for_feasible_solution_only(false), + m_tracker_of_x_change(nullptr) { lp_assert(bounds_for_boxed_are_set_correctly()); init(); init_basis_heading_and_non_basic_columns_vector(); diff --git a/src/util/lp/lp_primal_core_solver.h b/src/util/lp/lp_primal_core_solver.h index 77784746a..7577516d2 100644 --- a/src/util/lp/lp_primal_core_solver.h +++ b/src/util/lp/lp_primal_core_solver.h @@ -779,7 +779,7 @@ public: if (this->m_basis_heading[j] < 0) continue; if (!this->column_is_feasible(j)) - this->m_inf_set.insert(j); + this->insert_column_into_inf_set(j); } } diff --git a/src/util/lp/lp_primal_core_solver.hpp b/src/util/lp/lp_primal_core_solver.hpp index b3d6921d9..27c92e5e0 100644 --- a/src/util/lp/lp_primal_core_solver.hpp +++ b/src/util/lp/lp_primal_core_solver.hpp @@ -1197,9 +1197,9 @@ lp_primal_core_solver::init_infeasibility_cost_for_column(unsigned j) { } if (numeric_traits::is_zero(this->m_costs[j])) { - this->m_inf_set.erase(j); + this->remove_column_from_inf_set(j); } else { - this->m_inf_set.insert(j); + this->insert_column_into_inf_set(j); } if (!this->m_settings.use_breakpoints_in_feasibility_search) { this->m_costs[j] = - this->m_costs[j]; diff --git a/src/util/lp/lp_primal_core_solver_tableau.hpp b/src/util/lp/lp_primal_core_solver_tableau.hpp index 3cacd2dbb..867c321ba 100644 --- a/src/util/lp/lp_primal_core_solver_tableau.hpp +++ b/src/util/lp/lp_primal_core_solver_tableau.hpp @@ -349,9 +349,9 @@ update_x_tableau(unsigned entering, const X& delta) { this->m_x[j] -= delta * this->m_A.get_val(c); update_inf_cost_for_column_tableau(j); if (is_zero(this->m_costs[j])) - this->m_inf_set.erase(j); + this->remove_column_from_inf_set(j); else - this->m_inf_set.insert(j); + this->insert_column_into_inf_set(j); } } lp_assert(this->A_mult_x_is_off() == false);