From 527f0d124280c59641177087b9c5dd58d9af4c9d Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Sat, 4 Mar 2023 12:34:15 -0800 Subject: [PATCH] rm lu Signed-off-by: Lev Nachmanson --- src/math/lp/lar_solver.cpp | 13 +++---------- src/math/lp/lar_solver.h | 1 - src/math/lp/lp_core_solver_base_def.h | 3 +-- src/math/lp/lp_settings.h | 5 +---- 4 files changed, 5 insertions(+), 17 deletions(-) diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index c2a332ad31a..3339b55a5b7 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -45,8 +45,7 @@ namespace lp { delete t; } - bool lar_solver::use_lu() const { return false; } - + bool lar_solver::sizes_are_correct() const { lp_assert(strategy_is_undecided() || !m_mpq_lar_core_solver.need_to_presolve_with_double_solver() || A_r().column_count() == A_d().column_count()); lp_assert(A_r().column_count() == m_mpq_lar_core_solver.m_r_solver.m_column_types.size()); @@ -1622,8 +1621,7 @@ namespace lp { m_mpq_lar_core_solver.m_column_types.push_back(column_type::free_column); increase_by_one_columns_with_changed_bounds(); add_new_var_to_core_fields_for_mpq(false); // false for not adding a row - if (use_lu()) - add_new_var_to_core_fields_for_doubles(false); + } void lar_solver::add_new_var_to_core_fields_for_doubles(bool register_in_basis) { @@ -1785,8 +1783,6 @@ namespace lp { fill_last_row_of_A_r(A_r(), term); } m_mpq_lar_core_solver.m_r_solver.update_x(j, get_basic_var_value_from_row(A_r().row_count() - 1)); - if (use_lu()) - fill_last_row_of_A_d(A_d(), term); for (lar_term::ival c : *term) { unsigned j = c.column(); while (m_usage_in_terms.size() <= j) { @@ -1798,15 +1794,12 @@ namespace lp { } void lar_solver::add_basic_var_to_core_fields() { - bool use_lu = m_mpq_lar_core_solver.need_to_presolve_with_double_solver(); - lp_assert(!use_lu || A_r().column_count() == A_d().column_count()); m_mpq_lar_core_solver.m_column_types.push_back(column_type::free_column); increase_by_one_columns_with_changed_bounds(); m_incorrect_columns.increase_size_by_one(); m_rows_with_changed_bounds.increase_size_by_one(); add_new_var_to_core_fields_for_mpq(true); - if (use_lu) - add_new_var_to_core_fields_for_doubles(true); + } bool lar_solver::bound_is_integer_for_integer_column(unsigned j, const mpq& right_side) const { diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index 20556deab75..c1deb2fb1c8 100644 --- a/src/math/lp/lar_solver.h +++ b/src/math/lp/lar_solver.h @@ -166,7 +166,6 @@ class lar_solver : public column_namer { void adjust_initial_state_for_lu(); void adjust_initial_state_for_tableau_rows(); void fill_last_row_of_A_d(static_matrix & A, const lar_term* ls); - bool use_lu() const; bool sizes_are_correct() const; bool implied_bound_is_correctly_explained(implied_bound const & be, const vector> & explanation) const; diff --git a/src/math/lp/lp_core_solver_base_def.h b/src/math/lp/lp_core_solver_base_def.h index 40e0a527d41..93d5f430239 100644 --- a/src/math/lp/lp_core_solver_base_def.h +++ b/src/math/lp/lp_core_solver_base_def.h @@ -82,8 +82,7 @@ allocate_basis_heading() { // the rest of initialization will be handled by the template void lp_core_solver_base:: init() { allocate_basis_heading(); - if (m_settings.use_lu()) - init_factorization(m_factorization, m_A, m_basis, m_settings); + } // i is the pivot row, and j is the pivot column diff --git a/src/math/lp/lp_settings.h b/src/math/lp/lp_settings.h index 790354e5586..d6a78564d8f 100644 --- a/src/math/lp/lp_settings.h +++ b/src/math/lp/lp_settings.h @@ -339,10 +339,7 @@ struct lp_settings { m_simplex_strategy = s; } - bool use_lu() const { - return false; - } - + bool use_tableau() const { return true; }