From 7f3bdea0d5aab4c9c30986ccbdf28745b96d45c4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 23 Jun 2020 19:28:07 -0700 Subject: [PATCH] unused methods Signed-off-by: Nikolaj Bjorner --- src/math/lp/lar_core_solver.h | 44 ++----- src/math/lp/lar_core_solver_def.h | 201 ++++++------------------------ 2 files changed, 45 insertions(+), 200 deletions(-) diff --git a/src/math/lp/lar_core_solver.h b/src/math/lp/lar_core_solver.h index 5a46159c4..0043ed23d 100644 --- a/src/math/lp/lar_core_solver.h +++ b/src/math/lp/lar_core_solver.h @@ -1,21 +1,9 @@ /*++ Copyright (c) 2017 Microsoft Corporation - -Module Name: - - - -Abstract: - - - Author: Lev Nachmanson (levnach) -Revision History: - - --*/ #pragma once #include "util/vector.h" @@ -51,9 +39,9 @@ public: stacked_vector> m_r_upper_bounds; static_matrix> m_r_A; stacked_vector m_r_pushed_basis; - vector m_r_basis; - vector m_r_nbasis; - vector m_r_heading; + vector m_r_basis; + vector m_r_nbasis; + vector m_r_heading; stacked_vector m_r_columns_nz; stacked_vector m_r_rows_nz; @@ -91,13 +79,6 @@ public: column_type get_column_type(unsigned j) { return m_column_types[j];} - void init_costs(bool first_time); - - void init_cost_for_column(unsigned j); - - // returns m_sign_of_alpha_r - int column_is_out_of_bounds(unsigned j); - void calculate_pivot_row(unsigned i); void print_pivot_row(std::ostream & out, unsigned row_index) const { @@ -112,8 +93,7 @@ public: for (unsigned j : m_r_solver.m_pivot_row.m_index) { m_r_solver.print_column_bound_info(j, out); } - m_r_solver.print_column_bound_info(m_r_solver.m_basis[row_index], out); - + m_r_solver.print_column_bound_info(m_r_solver.m_basis[row_index], out); } @@ -131,28 +111,20 @@ public: void prefix_d(); - unsigned m_m() const { - return m_r_A.row_count(); - } + unsigned m_m() const { return m_r_A.row_count(); } - unsigned m_n() const { - return m_r_A.column_count(); - } + unsigned m_n() const { return m_r_A.column_count(); } bool is_tiny() const { return this->m_m() < 10 && this->m_n() < 20; } bool is_empty() const { return this->m_m() == 0 && this->m_n() == 0; } template - int get_sign(const L & v) { - return v > zero_of_type() ? 1 : (v < zero_of_type() ? -1 : 0); - } - - + int get_sign(const L & v) { return v > zero_of_type() ? 1 : (v < zero_of_type() ? -1 : 0); } void fill_evidence(unsigned row); - unsigned get_number_of_non_ints() const; + unsigned get_number_of_non_ints() const; void solve(); diff --git a/src/math/lp/lar_core_solver_def.h b/src/math/lp/lar_core_solver_def.h index 77e5177de..06f414d11 100644 --- a/src/math/lp/lar_core_solver_def.h +++ b/src/math/lp/lar_core_solver_def.h @@ -1,33 +1,6 @@ /*++ Copyright (c) 2017 Microsoft Corporation -Module Name: - - - -Abstract: - - - -Author: - - Lev Nachmanson (levnach) - -Revision History: - - ---*/ -/*++ -Copyright (c) 2017 Microsoft Corporation - -Module Name: - - - -Abstract: - - - Author: Lev Nachmanson (levnach) @@ -42,137 +15,36 @@ Revision History: #include "math/lp/lar_solution_signature.h" namespace lp { lar_core_solver::lar_core_solver( - lp_settings & settings, - const column_namer & column_names - ): + lp_settings & settings, + const column_namer & column_names): m_infeasible_sum_sign(0), m_r_solver(m_r_A, - m_right_sides_dummy, - m_r_x, - m_r_basis, - m_r_nbasis, - m_r_heading, - m_costs_dummy, - m_column_types(), - m_r_lower_bounds(), - m_r_upper_bounds(), - settings, + m_right_sides_dummy, + m_r_x, + m_r_basis, + m_r_nbasis, + m_r_heading, + m_costs_dummy, + m_column_types(), + m_r_lower_bounds(), + m_r_upper_bounds(), + settings, column_names), m_d_solver(m_d_A, - m_d_right_sides_dummy, - m_d_x, - m_d_basis, - m_d_nbasis, - m_d_heading, - m_d_costs_dummy, - m_column_types(), - m_d_lower_bounds, - m_d_upper_bounds, - settings, - column_names){} - -void lar_core_solver::init_costs(bool first_time) { - lp_assert(false); // should not be called - // lp_assert(this->m_x.size() >= this->m_n()); - // lp_assert(this->m_column_types.size() >= this->m_n()); - // if (first_time) - // this->m_costs.resize(this->m_n()); - // X inf = this->m_infeasibility; - // this->m_infeasibility = zero_of_type(); - // for (unsigned j = this->m_n(); j--;) - // init_cost_for_column(j); - // if (!(first_time || inf >= this->m_infeasibility)) { - // LP_OUT(this->m_settings, "iter = " << this->total_iterations() << std::endl); - // LP_OUT(this->m_settings, "inf was " << T_to_string(inf) << " and now " << T_to_string(this->m_infeasibility) << std::endl); - // lp_assert(false); - // } - // if (inf == this->m_infeasibility) - // this->m_iters_with_no_cost_growing++; -} - - -void lar_core_solver::init_cost_for_column(unsigned j) { - /* - // If j is a breakpoint column, then we set the cost zero. - // When anylyzing an entering column candidate we update the cost of the breakpoints columns to get the left or the right derivative if the infeasibility function - const numeric_pair & x = this->m_x[j]; - // set zero cost for each non-basis column - if (this->m_basis_heading[j] < 0) { - this->m_costs[j] = numeric_traits::zero(); - return; - } - // j is a basis column - switch (this->m_column_types[j]) { - case fixed: - case column_type::boxed: - if (x > this->m_upper_bounds[j]) { - this->m_costs[j] = 1; - this->m_infeasibility += x - this->m_upper_bounds[j]; - } else if (x < this->m_lower_bounds[j]) { - this->m_infeasibility += this->m_lower_bounds[j] - x; - this->m_costs[j] = -1; - } else { - this->m_costs[j] = numeric_traits::zero(); - } - break; - case lower_bound: - if (x < this->m_lower_bounds[j]) { - this->m_costs[j] = -1; - this->m_infeasibility += this->m_lower_bounds[j] - x; - } else { - this->m_costs[j] = numeric_traits::zero(); - } - break; - case upper_bound: - if (x > this->m_upper_bounds[j]) { - this->m_costs[j] = 1; - this->m_infeasibility += x - this->m_upper_bounds[j]; - } else { - this->m_costs[j] = numeric_traits::zero(); - } - break; - case free_column: - this->m_costs[j] = numeric_traits::zero(); - break; - default: - lp_assert(false); - break; - }*/ -} - - -// returns m_sign_of_alpha_r -int lar_core_solver::column_is_out_of_bounds(unsigned j) { - /* - switch (this->m_column_type[j]) { - case fixed: - case column_type::boxed: - if (this->x_below_low_bound(j)) { - return -1; - } - if (this->x_above_upper_bound(j)) { - return 1; - } - return 0; - case lower_bound: - if (this->x_below_low_bound(j)) { - return -1; - } - return 0; - case upper_bound: - if (this->x_above_upper_bound(j)) { - return 1; - } - return 0; - default: - return 0; - break; - }*/ - lp_assert(false); - return true; -} - - + m_d_right_sides_dummy, + m_d_x, + m_d_basis, + m_d_nbasis, + m_d_heading, + m_d_costs_dummy, + m_column_types(), + m_d_lower_bounds, + m_d_upper_bounds, + settings, + column_names) { +} + + void lar_core_solver::calculate_pivot_row(unsigned i) { m_r_solver.calculate_pivot_row(i); @@ -180,8 +52,8 @@ void lar_core_solver::calculate_pivot_row(unsigned i) { - void lar_core_solver::prefix_r() { - if (!m_r_solver.m_settings.use_tableau()) { +void lar_core_solver::prefix_r() { + if (!m_r_solver.m_settings.use_tableau()) { m_r_solver.m_copy_of_xB.resize(m_r_solver.m_n()); m_r_solver.m_ed.resize(m_r_solver.m_m()); m_r_solver.m_pivot_row.resize(m_r_solver.m_n()); @@ -203,7 +75,7 @@ void lar_core_solver::calculate_pivot_row(unsigned i) { } } - void lar_core_solver::prefix_d() { +void lar_core_solver::prefix_d() { m_d_solver.m_b.resize(m_d_solver.m_m()); m_d_solver.m_breakpoint_indices_queue.resize(m_d_solver.m_n()); m_d_solver.m_copy_of_xB.resize(m_d_solver.m_n()); @@ -256,12 +128,12 @@ void lar_core_solver::fill_not_improvable_zero_sum() { } unsigned lar_core_solver::get_number_of_non_ints() const { - unsigned n = 0; - for (auto & x : m_r_solver.m_x) { - if (x.is_int() == false) - n++; - } - return n; + unsigned n = 0; + for (auto & x : m_r_solver.m_x) { + if (x.is_int() == false) + n++; + } + return n; } void lar_core_solver::solve() { @@ -309,7 +181,8 @@ void lar_core_solver::solve() { } if (m_r_solver.get_status() == lp_status::INFEASIBLE) { fill_not_improvable_zero_sum(); - } else if (m_r_solver.get_status() != lp_status::UNBOUNDED) { + } + else if (m_r_solver.get_status() != lp_status::UNBOUNDED) { m_r_solver.set_status(lp_status::OPTIMAL); } lp_assert(r_basis_is_OK());