diff --git a/src/math/lp/core_solver_pretty_printer.h b/src/math/lp/core_solver_pretty_printer.h index 353212dcd..5bf29d511 100644 --- a/src/math/lp/core_solver_pretty_printer.h +++ b/src/math/lp/core_solver_pretty_printer.h @@ -59,7 +59,7 @@ class core_solver_pretty_printer { unsigned m_artificial_start; indexed_vector m_w_buff; indexed_vector m_ed_buff; - vector m_exact_column_norms; + public: core_solver_pretty_printer(const lp_core_solver_base & core_solver, std::ostream & out); @@ -85,14 +85,7 @@ public: } unsigned get_column_width(unsigned column); - - unsigned regular_cell_width(unsigned row, unsigned column, const std::string & name) { - return regular_cell_string(row, column, name).size(); - } - - std::string regular_cell_string(unsigned row, unsigned column, std::string name); - - + void set_coeff(vector& row, vector & row_signs, unsigned col, const T & t, string name); void print_x(); @@ -105,12 +98,7 @@ public: void print_lows(); void print_upps(); - - string get_exact_column_norm_string(unsigned col) { - return T_to_string(m_exact_column_norms[col]); - } - - + void print_approx_norms(); void print(); diff --git a/src/math/lp/core_solver_pretty_printer_def.h b/src/math/lp/core_solver_pretty_printer_def.h index 2f1d99d22..931333ee7 100644 --- a/src/math/lp/core_solver_pretty_printer_def.h +++ b/src/math/lp/core_solver_pretty_printer_def.h @@ -37,9 +37,8 @@ core_solver_pretty_printer::core_solver_pretty_printer(const lp_core_solve m_signs(core_solver.m_A.row_count(), vector(core_solver.m_A.column_count(), " ")), m_costs(ncols(), ""), m_cost_signs(ncols(), " "), - m_rs(ncols(), zero_of_type()), - m_w_buff(core_solver.m_w), - m_ed_buff(core_solver.m_ed) { + m_rs(ncols(), zero_of_type()) + { m_lower_bounds_title = "low"; m_upp_bounds_title = "upp"; m_exact_norm_title = "exact cn"; @@ -80,13 +79,6 @@ template void core_solver_pretty_printer::init_rs } } -template T core_solver_pretty_printer::current_column_norm() { - T ret = zero_of_type(); - for (auto i : m_core_solver.m_ed.m_index) - ret += m_core_solver.m_ed[i] * m_core_solver.m_ed[i]; - return ret; -} - template void core_solver_pretty_printer::init_m_A_and_signs() { for (unsigned column = 0; column < ncols(); column++) { vector t(nrows(), zero_of_type()); @@ -167,13 +159,6 @@ template unsigned core_solver_pretty_printer:: ge return w; } -template std::string core_solver_pretty_printer::regular_cell_string(unsigned row, unsigned /* column */, std::string name) { - T t = fabs(m_core_solver.m_ed[row]); - if ( t == 1) return name; - return T_to_string(t) + name; -} - - template void core_solver_pretty_printer::set_coeff(vector& row, vector & row_signs, unsigned col, const T & t, string name) { if (numeric_traits::is_zero(t)) { return; diff --git a/src/math/lp/indexed_vector_def.h b/src/math/lp/indexed_vector_def.h index 1b904e14a..034325088 100644 --- a/src/math/lp/indexed_vector_def.h +++ b/src/math/lp/indexed_vector_def.h @@ -24,14 +24,6 @@ Revision History: #include "math/lp/lp_settings.h" namespace lp { -template -void print_sparse_vector(const vector & t, std::ostream & out) { - for (unsigned i = 0; i < t.size(); i++) { - if (is_zero(t[i]))continue; - out << "[" << i << "] = " << t[i] << ", "; - } - out << std::endl; -} void print_vector_as_doubles(const vector & t, std::ostream & out) { for (unsigned i = 0; i < t.size(); i++) diff --git a/src/math/lp/lp_core_solver_base.cpp b/src/math/lp/lp_core_solver_base.cpp index 14c454d6f..ccd6bf419 100644 --- a/src/math/lp/lp_core_solver_base.cpp +++ b/src/math/lp/lp_core_solver_base.cpp @@ -29,9 +29,7 @@ template lp::non_basic_column_value_position 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 bool lp::lp_core_solver_base::basis_heading_is_correct() const ; 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 &); -template void lp::lp_core_solver_base::restore_x(unsigned int, lp::mpq const&); template void lp::lp_core_solver_base::set_non_basic_x_to_correct_bounds(); template void lp::lp_core_solver_base::add_delta_to_entering(unsigned int, const lp::mpq&); template void lp::lp_core_solver_base >::init(); @@ -68,7 +66,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 >::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); template void lp::lp_core_solver_base >::transpose_rows_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 14cb60ebf..964e447a1 100644 --- a/src/math/lp/lp_core_solver_base.h +++ b/src/math/lp/lp_core_solver_base.h @@ -74,7 +74,6 @@ public: void set_using_infeas_costs(bool val) { m_using_infeas_costs = val; } vector m_columns_nz; // m_columns_nz[i] keeps an approximate value of non zeroes the i-th column vector m_rows_nz; // m_rows_nz[i] keeps an approximate value of non zeroes in the i-th row - indexed_vector m_pivot_row_of_B_1; // the pivot row of the reverse of B indexed_vector m_pivot_row; // this is the real pivot row of the simplex tableu static_matrix & m_A; // the matrix A // vector const & m_b; // the right side @@ -85,15 +84,11 @@ public: vector & m_costs; lp_settings & m_settings; - vector m_y; // the buffer for yB = cb const column_namer & m_column_names; - indexed_vector m_w; // the vector featuring in 24.3 of the Chvatal book vector m_d; // the vector of reduced costs - indexed_vector m_ed; // the solution of B*m_ed = a const vector & m_column_types; const vector & m_lower_bounds; const vector & m_upper_bounds; - vector m_copy_of_xB; unsigned m_basis_sort_counter; vector m_trace_of_basis_change_vector; // the even positions are entering, the odd positions are leaving bool m_tracing_basis_changes; @@ -162,10 +157,6 @@ public: return dot_product(m_costs, m_x); } - void copy_m_w(T * buffer); - - void restore_m_w(T * buffer); - void add_delta_to_entering(unsigned entering, const X & delta); const X & get_var_value(unsigned j) const { @@ -298,11 +289,6 @@ public: bool basis_heading_is_correct() const; - void restore_x(unsigned entering, X const & t); - - void fill_reduced_costs_from_m_y_by_rows(); - - void copy_rs_to_xB(vector & rs); virtual bool lower_bounds_are_set() const { return false; } X lower_bound_value(unsigned j) const { return m_lower_bounds[j]; } X upper_bound_value(unsigned j) const { return m_upper_bounds[j]; } @@ -316,10 +302,6 @@ public: std::string column_name(unsigned column) const; - void add_delta_to_xB(vector & del); - - void find_error_in_BxB(vector& rs); - bool snap_non_basic_x_to_bound() { bool ret = false; for (unsigned j : non_basis()) diff --git a/src/math/lp/lp_core_solver_base_def.h b/src/math/lp/lp_core_solver_base_def.h index 16f56bade..2d7296567 100644 --- a/src/math/lp/lp_core_solver_base_def.h +++ b/src/math/lp/lp_core_solver_base_def.h @@ -44,25 +44,19 @@ lp_core_solver_base(static_matrix & A, m_status(lp_status::FEASIBLE), m_inf_set(A.column_count()), m_using_infeas_costs(false), - m_pivot_row_of_B_1(A.row_count()), m_pivot_row(A.column_count()), m_A(A), - // m_b(b), m_basis(basis), m_nbasis(nbasis), m_basis_heading(heading), m_x(x), m_costs(costs), m_settings(settings), - m_y(m_m()), m_column_names(column_names), - m_w(m_m()), m_d(m_n()), - m_ed(m_m()), m_column_types(column_types), m_lower_bounds(lower_bound_values), m_upper_bounds(upper_bound_values), - m_copy_of_xB(m_m()), m_basis_sort_counter(0), m_tracing_basis_changes(false), m_pivoted_rows(nullptr), @@ -122,25 +116,6 @@ pretty_print(std::ostream & out) { } -template void lp_core_solver_base:: -copy_m_w(T * buffer) { - unsigned i = m_m(); - while (i --) { - buffer[i] = m_w[i]; - } -} - -template void lp_core_solver_base:: -restore_m_w(T * buffer) { - m_w.m_index.clear(); - unsigned i = m_m(); - while (i--) { - if (!is_zero(m_w[i] = buffer[i])) - m_w.m_index.push_back(i); - } -} - - template void lp_core_solver_base:: add_delta_to_entering(unsigned entering, const X& delta) { m_x[entering] += delta; @@ -443,73 +418,11 @@ template bool lp_core_solver_base:: return true; } -template void lp_core_solver_base:: -restore_x(unsigned entering, X const & t) { - if (is_zero(t)) return; - m_x[entering] -= t; - for (unsigned i : m_ed.m_index) { - m_x[m_basis[i]] = m_copy_of_xB[i]; - } -} - -template void lp_core_solver_base:: -fill_reduced_costs_from_m_y_by_rows() { - unsigned j = m_n(); - while (j--) { - if (m_basis_heading[j] < 0) - m_d[j] = m_costs[j]; - else - m_d[j] = numeric_traits::zero(); - } - - unsigned i = m_m(); - while (i--) { - const T & y = m_y[i]; - if (is_zero(y)) continue; - for (row_cell & c : m_A.m_rows[i]) { - j = c.var(); - if (m_basis_heading[j] < 0) { - m_d[j] -= y * c.coeff(); - } - } - } -} - -template void lp_core_solver_base:: -copy_rs_to_xB(vector & rs) { - unsigned j = m_m(); - while (j--) { - m_x[m_basis[j]] = rs[j]; - } -} - template std::string lp_core_solver_base:: column_name(unsigned column) const { return m_column_names.get_variable_name(column); } -template void lp_core_solver_base:: -add_delta_to_xB(vector & del) { - unsigned i = m_m(); - while (i--) { - this->m_x[this->m_basis[i]] -= del[i]; - } -} - -template void lp_core_solver_base:: -find_error_in_BxB(vector& rs){ - unsigned row = m_m(); - while (row--) { - auto &rsv = rs[row]; - for (auto & it : m_A.m_rows[row]) { - unsigned j = it.var(); - if (m_basis_heading[j] >= 0) { - rsv -= m_x[j] * it.coeff(); - } - } - } -} - template non_basic_column_value_position lp_core_solver_base:: get_non_basic_column_value_position(unsigned j) const { switch (m_column_types[j]) { @@ -543,9 +456,9 @@ template bool lp_core_solver_base::pivot_column_g lp_assert(m_basis_heading[j_basic] >= 0); unsigned row_index = m_basis_heading[j_basic]; // the tableau case - if (pivot_column_tableau(j, row_index)) - change_basis(j, j_basic); - else return false; + if (pivot_column_tableau(j, row_index)) + change_basis(j, j_basic); + else return false; return true; } diff --git a/src/math/lp/permutation_matrix.h b/src/math/lp/permutation_matrix.h index 8ec78c14a..35a58906a 100644 --- a/src/math/lp/permutation_matrix.h +++ b/src/math/lp/permutation_matrix.h @@ -22,7 +22,6 @@ Revision History: #include #include "util/debug.h" #include -#include "math/lp/sparse_vector.h" #include "math/lp/indexed_vector.h" #include "math/lp/lp_settings.h" #include "math/lp/matrix.h" diff --git a/src/math/lp/sparse_vector.h b/src/math/lp/sparse_vector.h deleted file mode 100644 index 3de701e10..000000000 --- a/src/math/lp/sparse_vector.h +++ /dev/null @@ -1,52 +0,0 @@ -/*++ -Copyright (c) 2017 Microsoft Corporation - -Module Name: - - - -Abstract: - - - -Author: - - Lev Nachmanson (levnach) - -Revision History: - - ---*/ - -#pragma once -#include "util/vector.h" -#include -#include "util/debug.h" -#include "math/lp/lp_utils.h" -#include "math/lp/lp_settings.h" -namespace lp { - -template -class sparse_vector { -public: - vector> m_data; - void push_back(unsigned index, T val) { - m_data.push_back(std::make_pair(index, val)); - } -#ifdef Z3DEBUG - T operator[] (unsigned i) const { - for (auto &t : m_data) { - if (t.first == i) return t.second; - } - return numeric_traits::zero(); - } -#endif - void divide(T const & a) { - for (auto & t : m_data) { t.second /= a; } - } - - unsigned size() const { - return m_data.size(); - } -}; -} diff --git a/src/math/lp/static_matrix.h b/src/math/lp/static_matrix.h index b9870ceb5..d7e4370a3 100644 --- a/src/math/lp/static_matrix.h +++ b/src/math/lp/static_matrix.h @@ -12,7 +12,6 @@ Author: #include #include #include -#include "math/lp/sparse_vector.h" #include "math/lp/indexed_vector.h" #include "math/lp/permutation_matrix.h" #include