From bfe73c01a6e3fbc309213832c051eeb093391b9e Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Mon, 6 Mar 2023 07:56:04 -0800 Subject: [PATCH] rm lu Signed-off-by: Lev Nachmanson --- src/math/lp/lar_core_solver.h | 41 --------------------------- src/math/lp/lar_solver.cpp | 5 ---- src/math/lp/lar_solver.h | 1 - src/math/lp/lp_core_solver_base.cpp | 14 --------- src/math/lp/lp_core_solver_base.h | 10 +------ src/math/lp/lp_core_solver_base_def.h | 40 -------------------------- 6 files changed, 1 insertion(+), 110 deletions(-) diff --git a/src/math/lp/lar_core_solver.h b/src/math/lp/lar_core_solver.h index 999eef13bc8..9168862c651 100644 --- a/src/math/lp/lar_core_solver.h +++ b/src/math/lp/lar_core_solver.h @@ -274,47 +274,6 @@ class lar_core_solver { } - - void prepare_solver_x_with_signature_tableau(const lar_solution_signature & signature) { - lp_assert(m_r_solver.inf_set_is_correct()); - for (auto &t : signature) { - unsigned j = t.first; - if (m_r_heading[j] >= 0) - continue; - auto pos_type = t.second; - numeric_pair delta; - if (!update_xj_and_get_delta(j, pos_type, delta)) - continue; - for (const auto & cc : m_r_solver.m_A.m_columns[j]){ - unsigned i = cc.var(); - unsigned jb = m_r_solver.m_basis[i]; - m_r_solver.add_delta_to_x_and_track_feasibility(jb, - delta * m_r_solver.m_A.get_val(cc)); - } - - } - lp_assert(m_r_solver.inf_set_is_correct()); - } - - - - bool adjust_x_of_column(unsigned j) { - /* - if (m_r_solver.m_basis_heading[j] >= 0) { - return false; - } - - if (m_r_solver.column_is_feasible(j)) { - return false; - } - - m_r_solver.snap_column_to_bound_tableau(j); - lp_assert(m_r_solver.column_is_feasible(j)); - m_r_solver.m_inf_set.erase(j); - */ - lp_assert(false); - return true; - } - bool r_basis_is_OK() const { #ifdef Z3DEBUG diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index d9961eaa8ab..48c575184ba 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -643,11 +643,6 @@ namespace lp { bool lar_solver::use_tableau_costs() const { return m_settings.simplex_strategy() == simplex_strategy_enum::tableau_costs; } - - void lar_solver::adjust_x_of_column(unsigned j) { - lp_assert(false); - } - bool lar_solver::row_is_correct(unsigned i) const { numeric_pair r = zero_of_type>(); for (const auto& c : A_r().m_rows[i]) { diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index 51365936819..09612d905e4 100644 --- a/src/math/lp/lar_solver.h +++ b/src/math/lp/lar_solver.h @@ -210,7 +210,6 @@ class lar_solver : public column_namer { void detect_rows_of_bound_change_column_for_nbasic_column_tableau(unsigned j); bool use_tableau_costs() const; void detect_rows_of_column_with_bound_change(unsigned j); - void adjust_x_of_column(unsigned j); bool tableau_with_costs() const; bool costs_are_used() const; void change_basic_columns_dependend_on_a_given_nb_column(unsigned j, const numeric_pair & delta); diff --git a/src/math/lp/lp_core_solver_base.cpp b/src/math/lp/lp_core_solver_base.cpp index 0d9f4297419..90101e998f5 100644 --- a/src/math/lp/lp_core_solver_base.cpp +++ b/src/math/lp/lp_core_solver_base.cpp @@ -24,7 +24,6 @@ Revision History: #include #include "math/lp/lp_core_solver_base_def.h" template bool lp::lp_core_solver_base::basis_heading_is_correct() const; -template void lp::lp_core_solver_base::calculate_pivot_row_when_pivot_row_of_B1_is_ready(unsigned); template bool lp::lp_core_solver_base::column_is_dual_feasible(unsigned int) const; template void lp::lp_core_solver_base::fill_reduced_costs_from_m_y_by_rows(); template lp::non_basic_column_value_position lp::lp_core_solver_base::get_non_basic_column_value_position(unsigned int) const; @@ -44,12 +43,9 @@ template bool lp::lp_core_solver_base::print_statistics_with_ite template bool lp::lp_core_solver_base >::print_statistics_with_iterations_and_nonzeroes_and_cost_and_check_that_the_time_is_over(char const*, std::ostream &); template void lp::lp_core_solver_base::restore_x(unsigned int, double const&); template void lp::lp_core_solver_base::set_non_basic_x_to_correct_bounds(); -template void lp::lp_core_solver_base::snap_xN_to_bounds_and_free_columns_to_zeroes(); -template void lp::lp_core_solver_base >::snap_xN_to_bounds_and_free_columns_to_zeroes(); template void lp::lp_core_solver_base::solve_Ax_eq_b(); template void lp::lp_core_solver_base::add_delta_to_entering(unsigned int, const double&); template bool lp::lp_core_solver_base::basis_heading_is_correct() const ; -template void lp::lp_core_solver_base::calculate_pivot_row_when_pivot_row_of_B1_is_ready(unsigned); template bool lp::lp_core_solver_base::column_is_dual_feasible(unsigned int) const; template void lp::lp_core_solver_base::fill_reduced_costs_from_m_y_by_rows(); template bool lp::lp_core_solver_base::print_statistics_with_iterations_and_nonzeroes_and_cost_and_check_that_the_time_is_over(char const*, std::ostream &); @@ -57,7 +53,6 @@ template void lp::lp_core_solver_base::restore_x(unsigned int, template void lp::lp_core_solver_base::set_non_basic_x_to_correct_bounds(); template void lp::lp_core_solver_base::solve_Ax_eq_b(); template void lp::lp_core_solver_base::add_delta_to_entering(unsigned int, const lp::mpq&); -template void lp::lp_core_solver_base >::calculate_pivot_row_when_pivot_row_of_B1_is_ready(unsigned); template void lp::lp_core_solver_base >::init(); template void lp::lp_core_solver_base >::init_basis_heading_and_non_basic_columns_vector(); template lp::lp_core_solver_base >::lp_core_solver_base(lp::static_matrix >&, @@ -85,18 +80,10 @@ template lp::lp_core_solver_base::lp_core_solver_base( template bool lp::lp_core_solver_base >::print_statistics_with_iterations_and_check_that_the_time_is_over(std::ostream &); template std::string lp::lp_core_solver_base::column_name(unsigned int) const; template void lp::lp_core_solver_base::pretty_print(std::ostream & out); -template void lp::lp_core_solver_base::restore_state(double*, double*); -template void lp::lp_core_solver_base::save_state(double*, double*); template std::string lp::lp_core_solver_base::column_name(unsigned int) const; template void lp::lp_core_solver_base::pretty_print(std::ostream & out); -template void lp::lp_core_solver_base::restore_state(lp::mpq*, lp::mpq*); -template void lp::lp_core_solver_base::save_state(lp::mpq*, lp::mpq*); template std::string lp::lp_core_solver_base >::column_name(unsigned int) const; template void lp::lp_core_solver_base >::pretty_print(std::ostream & out); -template void lp::lp_core_solver_base >::restore_state(lp::mpq*, lp::mpq*); -template void lp::lp_core_solver_base >::save_state(lp::mpq*, lp::mpq*); -template void lp::lp_core_solver_base::init_lu(); -template void lp::lp_core_solver_base::init_lu(); template int lp::lp_core_solver_base::pivots_in_column_and_row_are_different(int, int) const; template int lp::lp_core_solver_base >::pivots_in_column_and_row_are_different(int, int) const; template int lp::lp_core_solver_base::pivots_in_column_and_row_are_different(int, int) const; @@ -109,7 +96,6 @@ template bool lp::lp_core_solver_base::column_is_feasible(unsi // template void lp::lp_core_solver_base >::print_linear_combination_of_column_indices(vector, std::allocator > > const&, std::ostream&) const; template bool lp::lp_core_solver_base >::column_is_feasible(unsigned int) const; template bool lp::lp_core_solver_base >::snap_non_basic_x_to_bound(); -template void lp::lp_core_solver_base >::init_lu(); template void lp::lp_core_solver_base >::restore_x(unsigned int, lp::numeric_pair const&); template bool lp::lp_core_solver_base>::pivot_column_tableau(unsigned int, unsigned int); template bool lp::lp_core_solver_base::pivot_column_tableau(unsigned int, unsigned int); diff --git a/src/math/lp/lp_core_solver_base.h b/src/math/lp/lp_core_solver_base.h index 729792c1266..e54c884891b 100644 --- a/src/math/lp/lp_core_solver_base.h +++ b/src/math/lp/lp_core_solver_base.h @@ -156,10 +156,6 @@ class lp_core_solver_base { void pretty_print(std::ostream & out); - void save_state(T * w_buffer, T * d_buffer); - - void restore_state(T * w_buffer, T * d_buffer); - X get_cost() const { return dot_product(m_costs, m_x); } @@ -173,8 +169,6 @@ class lp_core_solver_base { void restore_m_ed(T * buffer); - void calculate_pivot_row_when_pivot_row_of_B1_is_ready(unsigned pivot_row); - void add_delta_to_entering(unsigned entering, const X & delta); const X & get_var_value(unsigned j) const { @@ -422,11 +416,9 @@ class lp_core_solver_base { void snap_non_basic_x_to_bound_and_free_to_zeroes(); void snap_xN_to_bounds_and_fill_xB(); - void snap_xN_to_bounds_and_free_columns_to_zeroes(); - + non_basic_column_value_position get_non_basic_column_value_position(unsigned j) const; - void init_lu(); int pivots_in_column_and_row_are_different(int entering, int leaving) const; void pivot_fixed_vars_from_basis(); bool remove_from_basis(unsigned j); diff --git a/src/math/lp/lp_core_solver_base_def.h b/src/math/lp/lp_core_solver_base_def.h index e470072e04c..bc902e8b052 100644 --- a/src/math/lp/lp_core_solver_base_def.h +++ b/src/math/lp/lp_core_solver_base_def.h @@ -136,17 +136,6 @@ pretty_print(std::ostream & out) { pp.print(); } -template void lp_core_solver_base:: -save_state(T * w_buffer, T * d_buffer) { - copy_m_w(w_buffer); - copy_m_ed(d_buffer); -} - -template void lp_core_solver_base:: -restore_state(T * w_buffer, T * d_buffer) { - restore_m_w(w_buffer); - restore_m_ed(d_buffer); -} template void lp_core_solver_base:: copy_m_w(T * buffer) { @@ -185,26 +174,6 @@ restore_m_ed(T * buffer) { -template void lp_core_solver_base:: -calculate_pivot_row_when_pivot_row_of_B1_is_ready(unsigned pivot_row) { - m_pivot_row.clear(); - - for (unsigned i : m_pivot_row_of_B_1.m_index) { - const T & pi_1 = m_pivot_row_of_B_1[i]; - if (numeric_traits::is_zero(pi_1)) { - continue; - } - for (auto & c : m_A.m_rows[i]) { - unsigned j = c.var(); - if (m_basis_heading[j] < 0) { - m_pivot_row.add_value_at_index_with_drop_tolerance(j, c.coeff() * pi_1); - } - } - } - if (precise()) { - m_rows_nz[pivot_row] = m_pivot_row.m_index.size(); - } -} template void lp_core_solver_base:: add_delta_to_entering(unsigned entering, const X& delta) { @@ -631,11 +600,6 @@ snap_xN_to_bounds_and_fill_xB() { solve_Ax_eq_b(); } -template void lp_core_solver_base:: -snap_xN_to_bounds_and_free_columns_to_zeroes() { - snap_non_basic_x_to_bound_and_free_to_zeroes(); - solve_Ax_eq_b(); -} template non_basic_column_value_position lp_core_solver_base:: @@ -661,10 +625,6 @@ get_non_basic_column_value_position(unsigned j) const { return at_lower_bound; } -template void lp_core_solver_base::init_lu() { - init_factorization(this->m_factorization, this->m_A, this->m_basis, this->m_settings); -} - template int lp_core_solver_base::pivots_in_column_and_row_are_different(int entering, int leaving) const { const T & column_p = this->m_ed[this->m_basis_heading[leaving]]; const T & row_p = this->m_pivot_row[entering];