From e2538afd32e776480cc4ee30ab85afd138a548e0 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 24 Mar 2020 10:31:14 -0700 Subject: [PATCH] better diagnostics in lar_solver and more efficient int_set::resize() Signed-off-by: Lev Nachmanson --- src/math/lp/int_set.h | 10 ++++++++-- src/math/lp/lar_solver.cpp | 2 +- 2 files changed, 9 insertions(+), 3 deletions(-) diff --git a/src/math/lp/int_set.h b/src/math/lp/int_set.h index 8f047dd2e..7a0561c85 100644 --- a/src/math/lp/int_set.h +++ b/src/math/lp/int_set.h @@ -63,11 +63,17 @@ public: void resize(unsigned size) { if (size < data_size()) { + bool copy = false; unsigned i = 0; for (unsigned j : m_index) { if (j < size) { - m_data[j] = i; - m_index[i++] = j; + if (copy) { + m_data[j] = i; + m_index[i] = j; + } + i++; + } else { + copy = true; } } m_index.shrink(i); diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index c27fd6bc9..4c5dd64d2 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -443,7 +443,6 @@ void lar_solver::set_costs_to_zero(const lar_term& term) { void lar_solver::prepare_costs_for_r_solver(const lar_term & term) { TRACE("lar_solver", print_term(term, tout << "prepare: ") << "\n";); - m_basic_columns_with_changed_cost.clear(); m_basic_columns_with_changed_cost.resize(m_mpq_lar_core_solver.m_r_x.size()); if (move_non_basic_columns_to_bounds()) find_feasible_solution(); @@ -1198,6 +1197,7 @@ void lar_solver::get_infeasibility_explanation_for_inf_sign( // (x, y) != (x', y') => (x + delta*y) != (x' + delta*y') void lar_solver::get_model(std::unordered_map & variable_values) const { + lp_assert(get_status() == lp_status::OPTIMAL || get_status() == lp_status::FEASIBLE); lp_assert(m_mpq_lar_core_solver.m_r_solver.calc_current_x_is_feasible_include_non_basis()); variable_values.clear(); mpq delta = m_mpq_lar_core_solver.find_delta_for_strict_bounds(mpq(1, 2)); // start from 0.5 to have less clashes