From c251151d6631bfaf11f9d8eae6cb20979d96ffc0 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Sat, 4 Mar 2023 15:15:08 -0800 Subject: [PATCH] rm_lu --- src/math/lp/lar_solver.cpp | 19 +----- src/math/lp/lp_primal_core_solver.h | 2 +- src/math/lp/lu.h | 59 ++---------------- src/test/lp/lp.cpp | 92 +---------------------------- 4 files changed, 9 insertions(+), 163 deletions(-) diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index 2e9541525d4..d9961eaa8ab 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -795,24 +795,7 @@ namespace lp { template void lar_solver::add_last_rows_to_lu(lp_primal_core_solver& s) { - auto& f = s.m_factorization; - if (f != nullptr) { - auto columns_to_replace = f->get_set_of_columns_to_replace_for_add_last_rows(s.m_basis_heading); - if (f->m_refactor_counter + columns_to_replace.size() >= 200 || f->has_dense_submatrix()) { - delete f; - f = nullptr; - } - else { - f->add_last_rows_to_B(s.m_basis_heading, columns_to_replace); - } - } - if (f == nullptr) { - init_factorization(f, s.m_A, s.m_basis, m_settings); - if (f->get_status() != LU_status::OK) { - delete f; - f = nullptr; - } - } + lp_assert(false); } diff --git a/src/math/lp/lp_primal_core_solver.h b/src/math/lp/lp_primal_core_solver.h index dc6cb2900e8..5332b4001da 100644 --- a/src/math/lp/lp_primal_core_solver.h +++ b/src/math/lp/lp_primal_core_solver.h @@ -418,7 +418,7 @@ class lp_primal_core_solver:public lp_core_solver_base { // returns the number of iterations unsigned solve(); - lu> * factorization() {return this->m_factorization;} + lu> * factorization() {return nullptr;} void delete_factorization(); diff --git a/src/math/lp/lu.h b/src/math/lp/lu.h index 191018100f8..bcbb850434d 100644 --- a/src/math/lp/lu.h +++ b/src/math/lp/lu.h @@ -305,66 +305,19 @@ class lu { void calculate_Lwave_Pwave_for_last_row(unsigned lowest_row_of_the_bump, T diagonal_element); void prepare_entering(unsigned entering, indexed_vector & w) { - init_vector_w(entering, w); + lp_assert(false); } - bool need_to_refactor() { return m_refactor_counter >= 200; } + bool need_to_refactor() { lp_assert(false); + return m_refactor_counter >= 200; } void adjust_dimension_with_matrix_A() { - lp_assert(m_A.row_count() >= m_dim); - m_dim = m_A.row_count(); - m_U.resize(m_dim); - m_Q.resize(m_dim); - m_R.resize(m_dim); - m_row_eta_work_vector.resize(m_dim); + lp_assert(false); } - std::unordered_set get_set_of_columns_to_replace_for_add_last_rows(const vector & heading) const { - std::unordered_set columns_to_replace; - unsigned m = m_A.row_count(); - unsigned m_prev = m_U.dimension(); - - lp_assert(m_A.column_count() == heading.size()); - - for (unsigned i = m_prev; i < m; i++) { - for (const row_cell & c : m_A.m_rows[i]) { - int h = heading[c.var()]; - if (h < 0) { - continue; - } - columns_to_replace.insert(c.var()); - } - } - return columns_to_replace; - } - void add_last_rows_to_B(const vector & heading, const std::unordered_set & columns_to_replace) { - unsigned m = m_A.row_count(); - lp_assert(m_A.column_count() == heading.size()); - adjust_dimension_with_matrix_A(); - m_w_for_extension.resize(m); - // At this moment the LU is correct - // for B extended by only by ones at the diagonal in the lower right corner - - for (unsigned j :columns_to_replace) { - lp_assert(heading[j] >= 0); - replace_column_with_only_change_at_last_rows(j, heading[j]); - if (get_status() == LU_status::Degenerated) - break; - } - } - // column j is a basis column, and there is a change in the last rows - void replace_column_with_only_change_at_last_rows(unsigned j, unsigned column_to_change_in_U) { - init_vector_w(j, m_w_for_extension); - replace_column(zero_of_type(), m_w_for_extension, column_to_change_in_U); - } - - bool has_dense_submatrix() const { - for (auto m : m_tail) - if (m->is_dense()) - return true; - return false; - } + + }; // end of lu diff --git a/src/test/lp/lp.cpp b/src/test/lp/lp.cpp index 189bd604b92..ceca92b4ecc 100644 --- a/src/test/lp/lp.cpp +++ b/src/test/lp/lp.cpp @@ -551,90 +551,7 @@ void change_basis(unsigned entering, unsigned leaving, vector& basis, #ifdef Z3DEBUG void test_small_lu(lp_settings & settings) { - std::cout << " test_small_lu" << std::endl; - static_matrix m(3, 6); - vector basis(3); - basis[0] = 0; - basis[1] = 1; - basis[2] = 3; - - m(0, 0) = 1; m(0, 2)= 3.9; m(2, 3) = 11; m(0, 5) = -3; - m(1, 1) = 4; m(1, 4) = 7; - m(2, 0) = 1.8; m(2, 2) = 5; m(2, 4) = 2; m(2, 5) = 8; - -#ifdef Z3DEBUG - print_matrix(m, std::cout); -#endif - vector heading = allocate_basis_heading(m.column_count()); - vector non_basic_columns; - init_basis_heading_and_non_basic_columns_vector(basis, heading, non_basic_columns); - lu> l(m, basis, settings); - lp_assert(l.is_correct(basis)); - indexed_vector w(m.row_count()); - std::cout << "entering 2, leaving 0" << std::endl; - l.prepare_entering(2, w); // to init vector w - l.replace_column(0, w, heading[0]); - change_basis(2, 0, basis, non_basic_columns, heading); - // #ifdef Z3DEBUG - // std::cout << "we were factoring " << std::endl; - // print_matrix(get_B(l)); - // #endif - lp_assert(l.is_correct(basis)); - std::cout << "entering 4, leaving 3" << std::endl; - l.prepare_entering(4, w); // to init vector w - l.replace_column(0, w, heading[3]); - change_basis(4, 3, basis, non_basic_columns, heading); - std::cout << "we were factoring " << std::endl; -#ifdef Z3DEBUG - { - auto bl = get_B(l, basis); - print_matrix(&bl, std::cout); - } -#endif - lp_assert(l.is_correct(basis)); - - std::cout << "entering 5, leaving 1" << std::endl; - l.prepare_entering(5, w); // to init vector w - l.replace_column(0, w, heading[1]); - change_basis(5, 1, basis, non_basic_columns, heading); - std::cout << "we were factoring " << std::endl; -#ifdef Z3DEBUG - { - auto bl = get_B(l, basis); - print_matrix(&bl, std::cout); - } -#endif - lp_assert(l.is_correct(basis)); - std::cout << "entering 3, leaving 2" << std::endl; - l.prepare_entering(3, w); // to init vector w - l.replace_column(0, w, heading[2]); - change_basis(3, 2, basis, non_basic_columns, heading); - std::cout << "we were factoring " << std::endl; -#ifdef Z3DEBUG - { - auto bl = get_B(l, basis); - print_matrix(&bl, std::cout); - } -#endif - lp_assert(l.is_correct(basis)); - - m.add_row(); - m.add_column(); - m.add_row(); - m.add_column(); - for (unsigned i = 0; i < m.column_count(); i++) { - m(3, i) = i; - m(4, i) = i * i; // to make the rows linearly independent - } - unsigned j = m.column_count() ; - basis.push_back(j-2); - heading.push_back(basis.size() - 1); - basis.push_back(j-1); - heading.push_back(basis.size() - 1); - auto columns_to_replace = l.get_set_of_columns_to_replace_for_add_last_rows(heading); - l.add_last_rows_to_B(heading, columns_to_replace); - lp_assert(l.is_correct(basis)); } #endif @@ -827,10 +744,7 @@ void test_larger_lu(lp_settings& settings) { void test_lu(lp_settings & settings) { - test_small_lu(settings); - test_larger_lu(settings); - test_larger_lu_with_holes(settings); - test_larger_lu_exp(settings); + } #endif @@ -1785,10 +1699,6 @@ void setup_args_parser(argument_parser & parser) { parser.add_option_with_after_string_with_help("--time_limit", "time limit in seconds"); parser.add_option_with_help_string("--mpq", "solve for rational numbers"); parser.add_option_with_after_string_with_help("--simplex_strategy", "sets simplex strategy for rational number"); - parser.add_option_with_help_string("--test_lu", "test the work of the factorization"); - parser.add_option_with_help_string("--test_small_lu", "test the work of the factorization on a smallish matrix"); - parser.add_option_with_help_string("--test_larger_lu", "test the work of the factorization"); - parser.add_option_with_help_string("--test_larger_lu_with_holes", "test the work of the factorization"); parser.add_option_with_help_string("--test_lp_0", "solve a small lp"); parser.add_option_with_help_string("--solve_some_mps", "solves a list of mps problems"); parser.add_option_with_after_string_with_help("--test_file_directory", "loads files from the directory for testing");