From 43758cbc66a2f0fcdc7a8173e11f00581b95369c Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Thu, 18 Apr 2019 20:27:46 -0700 Subject: [PATCH] more efficiend handling of rounded in cube heuristic rows Signed-off-by: Lev Nachmanson --- src/util/lp/int_solver.cpp | 1 - src/util/lp/lar_solver.cpp | 19 ++++++++----------- src/util/lp/lar_solver.h | 11 +++-------- 3 files changed, 11 insertions(+), 20 deletions(-) diff --git a/src/util/lp/int_solver.cpp b/src/util/lp/int_solver.cpp index b539947c8..3b46b423b 100644 --- a/src/util/lp/int_solver.cpp +++ b/src/util/lp/int_solver.cpp @@ -266,7 +266,6 @@ lia_move int_solver::find_cube() { // it can happen that we found an integer solution here return !m_lar_solver->r_basis_has_inf_int()? lia_move::sat: lia_move::undef; } - m_lar_solver->x_shifted_in_cube() = true; m_lar_solver->pop(); m_lar_solver->round_to_integer_solution(); m_lar_solver->set_status(lp_status::FEASIBLE); diff --git a/src/util/lp/lar_solver.cpp b/src/util/lp/lar_solver.cpp index 4b2c717d9..6cee53cbb 100644 --- a/src/util/lp/lar_solver.cpp +++ b/src/util/lp/lar_solver.cpp @@ -27,8 +27,7 @@ void clear() {lp_assert(false); // not implemented } -lar_solver::lar_solver() : m_x_shifted_in_cube(false), - m_status(lp_status::UNKNOWN), +lar_solver::lar_solver() : m_status(lp_status::UNKNOWN), m_infeasible_column(-1), m_mpq_lar_core_solver(m_settings, *this), m_int_solver(nullptr), @@ -398,7 +397,7 @@ void lar_solver::pop(unsigned k) { m_settings.simplex_strategy() = m_simplex_strategy; lp_assert(sizes_are_correct()); lp_assert((!m_settings.use_tableau()) || m_mpq_lar_core_solver.m_r_solver.reduced_costs_are_correct_tableau()); - lp_assert(x_shifted_in_cube() || ax_is_correct()); + lp_assert(m_cube_rounded_rows.size() != 0 || ax_is_correct()); set_status(lp_status::UNKNOWN); } @@ -875,7 +874,7 @@ void lar_solver::update_x_and_inf_costs_for_columns_with_changed_bounds_tableau( } } -void lar_solver::fix_Ax_b_on_row(unsigned i) { +void lar_solver::fix_Ax_b_on_rounded_row(unsigned i) { unsigned bj = m_mpq_lar_core_solver.m_r_basis[i]; auto& v = m_mpq_lar_core_solver.m_r_x[bj]; v = zero_of_type>(); @@ -884,18 +883,16 @@ void lar_solver::fix_Ax_b_on_row(unsigned i) { v -= c.coeff() * m_mpq_lar_core_solver.m_r_x[c.var()]; } } -void lar_solver::fix_Ax_b() { - for (unsigned i = 0; i < A_r().row_count(); i++) { - fix_Ax_b_on_row(i); +void lar_solver::fix_Ax_b_on_rounded_rows() { + for (unsigned i : m_cube_rounded_rows) { + fix_Ax_b_on_rounded_row(i); } + m_cube_rounded_rows.clear(); lp_assert(ax_is_correct()); } void lar_solver::solve_with_core_solver() { - if (x_shifted_in_cube()) { - fix_Ax_b(); - x_shifted_in_cube() = false; - } + fix_Ax_b_on_rounded_rows(); if (!use_tableau()) add_last_rows_to_lu(m_mpq_lar_core_solver.m_r_solver); if (m_mpq_lar_core_solver.need_to_presolve_with_double_solver()) { diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h index 2eee63430..96e0795d8 100644 --- a/src/util/lp/lar_solver.h +++ b/src/util/lp/lar_solver.h @@ -88,9 +88,7 @@ class lar_solver : public column_namer { #endif //////////////////// fields ////////////////////////// - // it is set to true when during the cube heuristic the column values got shifted - // and in this case the tableau becames invalid - bool m_x_shifted_in_cube; + vector m_cube_rounded_rows; lp_settings m_settings; lp_status m_status; stacked_value m_simplex_strategy; @@ -119,9 +117,6 @@ public: indexed_vector m_column_buffer; // end of fields - bool x_shifted_in_cube() const { return m_x_shifted_in_cube; } - bool& x_shifted_in_cube() { return m_x_shifted_in_cube; } - unsigned terms_start_index() const { return m_terms_start_index; } const vector & terms() const { return m_terms; } lar_term const& term(unsigned i) const { return *m_terms[i]; } @@ -642,7 +637,7 @@ public: lar_term get_term_to_maximize(unsigned ext_j) const; void set_cut_strategy(unsigned cut_frequency); bool sum_first_coords(const lar_term& t, mpq & val) const; - void fix_Ax_b(); - void fix_Ax_b_on_row(unsigned); + void fix_Ax_b_on_rounded_rows(); + void fix_Ax_b_on_rounded_row(unsigned); }; }