From 504c603af4aa4a3843f579d7aa16255cdec8d549 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Mon, 25 Jan 2016 14:49:23 -0800 Subject: [PATCH] chore(lp): use std::ostream for printing routines Signed-off-by: Lev Nachmanson --- src/tests/util/lp/lp.cpp | 38 ++++---- src/util/lp/binary_heap_priority_queue.cpp | 13 +-- src/util/lp/binary_heap_priority_queue.h | 2 +- src/util/lp/binary_heap_upair_queue.cpp | 12 +-- src/util/lp/core_solver_pretty_printer.cpp | 96 ++++++++++--------- src/util/lp/core_solver_pretty_printer.h | 6 +- .../core_solver_pretty_printer_instances.cpp | 6 +- src/util/lp/eta_matrix.h | 4 +- src/util/lp/indexed_vector.cpp | 34 +++---- src/util/lp/indexed_vector.h | 10 +- src/util/lp/lar_core_solver.cpp | 75 ++++++--------- src/util/lp/lar_core_solver.h | 12 +-- src/util/lp/lar_core_solver_instances.cpp | 4 +- src/util/lp/lar_solver.cpp | 74 +++++--------- src/util/lp/lar_solver.h | 10 +- src/util/lp/lp_core_solver_base.cpp | 12 +-- src/util/lp/lp_core_solver_base.h | 2 +- src/util/lp/lp_core_solver_base_instances.cpp | 6 +- src/util/lp/lp_dual_core_solver.cpp | 38 ++------ src/util/lp/lp_dual_core_solver.h | 2 +- src/util/lp/lp_dual_simplex.cpp | 15 +-- src/util/lp/lp_primal_core_solver.cpp | 35 +++---- src/util/lp/lp_primal_core_solver.h | 4 +- src/util/lp/lp_primal_simplex.cpp | 18 ---- src/util/lp/lp_primal_simplex.h | 4 - src/util/lp/lp_settings.h | 6 +- src/util/lp/lp_solver.cpp | 34 +++---- src/util/lp/lp_solver.h | 10 +- src/util/lp/lu.cpp | 45 ++++----- src/util/lp/lu.h | 12 +-- src/util/lp/lu_instances.cpp | 6 +- src/util/lp/matrix.cpp | 20 ++-- src/util/lp/matrix.h | 8 +- src/util/lp/matrix_instances.cpp | 2 +- src/util/lp/permutation_matrix.cpp | 12 +-- src/util/lp/permutation_matrix.h | 2 +- src/util/lp/row_eta_matrix.h | 4 +- src/util/lp/sparse_matrix.cpp | 8 +- src/util/lp/sparse_matrix.h | 2 +- 39 files changed, 288 insertions(+), 415 deletions(-) diff --git a/src/tests/util/lp/lp.cpp b/src/tests/util/lp/lp.cpp index 273b1b0680..b90eab80cb 100644 --- a/src/tests/util/lp/lp.cpp +++ b/src/tests/util/lp/lp.cpp @@ -179,7 +179,7 @@ void test_small_lu(lp_settings & settings) { m(2, 0) = 1.8; m(2, 2) = 5; m(2, 4) = 2; m(2, 5) = 8; #ifdef LEAN_DEBUG - print_matrix(m); + print_matrix(m, std::cout); #endif vector heading = allocate_basis_heading(m.column_count()); vector non_basic_columns; @@ -202,7 +202,7 @@ void test_small_lu(lp_settings & settings) { l.change_basis(4, 3); cout << "we were factoring " << std::endl; #ifdef LEAN_DEBUG - print_matrix(get_B(l)); + print_matrix(get_B(l), std::cout); #endif lean_assert(l.is_correct()); @@ -212,7 +212,7 @@ void test_small_lu(lp_settings & settings) { l.change_basis(5, 1); cout << "we were factoring " << std::endl; #ifdef LEAN_DEBUG - print_matrix(get_B(l)); + print_matrix(get_B(l), std::cout); #endif lean_assert(l.is_correct()); cout << "entering 3, leaving 2" << std::endl; @@ -221,7 +221,7 @@ void test_small_lu(lp_settings & settings) { l.change_basis(3, 2); cout << "we were factoring " << std::endl; #ifdef LEAN_DEBUG - print_matrix(get_B(l)); + print_matrix(get_B(l),std::cout); #endif lean_assert(l.is_correct()); } @@ -341,7 +341,7 @@ void test_larger_lu_with_holes(lp_settings & settings) { m(5, 4) = 28; m(5, 5) = -18; m(5, 6) = 19; m(5, 7) = 25; /* */ m(6, 5) = 20; m(6, 6) = -21; /* */ m(7, 5) = 22; m(7, 6) = 23; m(7, 7) = 24; m(7, 8) = 88; - print_matrix(m); + print_matrix(m, std::cout); vector heading = allocate_basis_heading(m.column_count()); vector non_basic_columns; init_basis_heading_and_non_basic_columns_vector(basis, m.row_count(), heading, m.column_count(), non_basic_columns); @@ -351,7 +351,7 @@ void test_larger_lu_with_holes(lp_settings & settings) { auto lp = l.get_lp_matrix(i); lp->set_number_of_columns(m.row_count()); lp->set_number_of_rows(m.row_count()); - print_matrix(* lp); + print_matrix(* lp, std::cout); } dense_matrix left_side = l.get_left_side(); @@ -381,7 +381,7 @@ void test_larger_lu(lp_settings& settings) { fill_larger_sparse_matrix(m); - print_matrix(m); + print_matrix(m, std::cout); vector heading = allocate_basis_heading(m.column_count()); vector non_basic_columns; @@ -399,9 +399,9 @@ void test_larger_lu(lp_settings& settings) { dense_matrix right_side = l.get_right_side(); if (!(left_side == right_side)) { cout << "left side" << std::endl; - print_matrix(left_side); + print_matrix(left_side, std::cout); cout << "right side" << std::endl; - print_matrix(right_side); + print_matrix(right_side, std::cout); std::cout << "different sides" << std::endl; cout << "initial factorization is incorrect" << std::endl; @@ -480,7 +480,7 @@ void test_lp_1() { m(2, 0) = 2; m(2, 1) = -1; m(2, 2) = 2; m(2, 5) = 1; m(3, 0) = 2; m(3, 1) = 3; m(3, 2) = -1; m(3, 6) = 1; #ifdef LEAN_DEBUG - print_matrix(m); + print_matrix(m, std::cout); #endif std::vector x_star(7); x_star[0] = 0; x_star[1] = 0; x_star[2] = 0; @@ -536,7 +536,7 @@ void test_swap_rows_with_permutation(sparse_matrix& m){ unsigned dim = m.row_count(); dense_matrix original(m); permutation_matrix q(dim); - print_matrix(m); + print_matrix(m, std::cout); lean_assert(original == q * m); for (int i = 0; i < 100; i++) { unsigned row1 = my_random() % dim; @@ -546,7 +546,7 @@ void test_swap_rows_with_permutation(sparse_matrix& m){ m.swap_rows(row1, row2); q.transpose_from_left(row1, row2); lean_assert(original == q * m); - print_matrix(m); + print_matrix(m, std::cout); cout << std::endl; } } @@ -560,7 +560,7 @@ void test_swap_cols_with_permutation(sparse_matrix& m){ unsigned dim = m.row_count(); dense_matrix original(m); permutation_matrix q(dim); - print_matrix(m); + print_matrix(m, std::cout); lean_assert(original == q * m); for (int i = 0; i < 100; i++) { unsigned row1 = my_random() % dim; @@ -570,7 +570,7 @@ void test_swap_cols_with_permutation(sparse_matrix& m){ m.swap_rows(row1, row2); q.transpose_from_right(row1, row2); lean_assert(original == q * m); - print_matrix(m); + print_matrix(m, std::cout); cout << std::endl; } } @@ -657,7 +657,7 @@ void test_pivot_like_swaps_and_pivot(){ m(target_row, 5) = 0; m(pivot_row, 6) = 0; #ifdef LEAN_DEBUG - print_matrix(m); + print_matrix(m, std::cout); #endif for (unsigned j = 0; j < m.dimension(); j++) { @@ -1005,6 +1005,8 @@ void update_settings(argument_parser & args_parser, lp_settings& settings) { unsigned n; if (get_int_from_args_parser("--rep_frq", args_parser, n)) settings.report_frequency = n; + else + settings.report_frequency = 1000; if (get_int_from_args_parser("--percent_for_enter", args_parser, n)) settings.percent_of_entering_to_check = n; @@ -1733,7 +1735,7 @@ void test_init_U() { m(1, 0) = 20; m(1, 1) = 21; m(1, 2) = 22; m(1, 3) = 23; m(1, 5) = 24; m(2, 0) = 30; m(2, 1) = 31; m(2, 2) = 32; m(2, 3) = 33; m(2, 6) = 34; #ifdef LEAN_DEBUG - print_matrix(m); + print_matrix(m, std::cout); #endif std::vector basis(3); basis[0] = 1; @@ -2427,7 +2429,7 @@ void test_square_dense_submatrix() { for (unsigned i = index_start; i < parent_dim; i++) for (unsigned j = index_start; j < parent_dim; j++) m[i-index_start][j-index_start] = d[i][j]; - print_matrix(m); + print_matrix(m, std::cout); #endif for (unsigned i = index_start; i < parent_dim; i++) for (unsigned j = index_start; j < parent_dim; j++) @@ -2437,7 +2439,7 @@ void test_square_dense_submatrix() { for (unsigned j = index_start; j < parent_dim; j++) m[i-index_start][j-index_start] = d[i][j]; - print_matrix(m); + print_matrix(m, std::cout); std::cout << std::endl; #endif } diff --git a/src/util/lp/binary_heap_priority_queue.cpp b/src/util/lp/binary_heap_priority_queue.cpp index f97ab50c04..881221bb39 100644 --- a/src/util/lp/binary_heap_priority_queue.cpp +++ b/src/util/lp/binary_heap_priority_queue.cpp @@ -42,13 +42,6 @@ template bool binary_heap_priority_queue::is_consistent() const for (int k = 0; k < 2; k++) { if (ch > m_heap_size) break; if (!(m_priorities[m_heap[i]] <= m_priorities[m_heap[ch]])){ - std::cout << "m_heap_size = " << m_heap_size << std::endl; - std::cout << "i = " << i << std::endl; - std::cout << "m_heap[i] = " << m_heap[i] << std::endl; - std::cout << "ch = " << ch << std::endl; - std::cout << "m_heap[ch] = " << m_heap[ch] << std::endl; - std::cout << "m_priorities[m_heap[i]] = " << m_priorities[m_heap[i]] << std::endl; - std::cout << "m_priorities[m_heap[ch]] = " << m_priorities[m_heap[ch]]<< std::endl; return false; } ch++; @@ -182,7 +175,7 @@ template unsigned binary_heap_priority_queue::dequeue() { return ret; } #ifdef LEAN_DEBUG -template void binary_heap_priority_queue::print() { +template void binary_heap_priority_queue::print(std::ostream & out) { std::vector index; std::vector prs; while (size()) { @@ -190,9 +183,9 @@ template void binary_heap_priority_queue::print() { int j = dequeue_and_get_priority(prior); index.push_back(j); prs.push_back(prior); - std::cout << "(" << j << ", " << prior << ")"; + out << "(" << j << ", " << prior << ")"; } - std::cout << std::endl; + out << std::endl; // restore the queue for (int i = 0; i < index.size(); i++) enqueue(index[i], prs[i]); diff --git a/src/util/lp/binary_heap_priority_queue.h b/src/util/lp/binary_heap_priority_queue.h index 6b787dd780..f581c909da 100644 --- a/src/util/lp/binary_heap_priority_queue.h +++ b/src/util/lp/binary_heap_priority_queue.h @@ -55,7 +55,7 @@ public: /// return the first element of the queue and removes it from the queue unsigned dequeue(); #ifdef LEAN_DEBUG - void print(); + void print(std::ostream & out); #endif }; } diff --git a/src/util/lp/binary_heap_upair_queue.cpp b/src/util/lp/binary_heap_upair_queue.cpp index 8cf51c79a8..c012b99ce9 100644 --- a/src/util/lp/binary_heap_upair_queue.cpp +++ b/src/util/lp/binary_heap_upair_queue.cpp @@ -88,14 +88,10 @@ template bool binary_heap_upair_queue::pair_to_index_is_a_biject std::set tmp; for (auto p : m_pairs_to_index) { unsigned j = p.second; - auto it = tmp.find(j); - if (it != tmp.end()) { - std::cout << "for pair (" << p.first.first << ", " << p.first.second << "), the index " << j - << " is already inside " << std::endl; - lean_assert(false); - } else { - tmp.insert(j); - } + unsigned size = tmp.size(); + tmp.insert(j); + if (tmp.size() == size) + return false; } return true; } diff --git a/src/util/lp/core_solver_pretty_printer.cpp b/src/util/lp/core_solver_pretty_printer.cpp index 865979ac1d..8b4c9ee0ad 100644 --- a/src/util/lp/core_solver_pretty_printer.cpp +++ b/src/util/lp/core_solver_pretty_printer.cpp @@ -10,13 +10,15 @@ namespace lean { template -core_solver_pretty_printer::core_solver_pretty_printer(lp_core_solver_base & core_solver): m_core_solver(core_solver), - m_column_widths(core_solver.m_A.column_count(), 0), - m_A(core_solver.m_A.row_count(), vector(core_solver.m_A.column_count(), "")), - 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()) { +core_solver_pretty_printer::core_solver_pretty_printer(lp_core_solver_base & core_solver, std::ostream & out): + m_out(out), + m_core_solver(core_solver), + m_column_widths(core_solver.m_A.column_count(), 0), + m_A(core_solver.m_A.row_count(), vector(core_solver.m_A.column_count(), "")), + 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 = new T[m_core_solver.m_m]; m_ed_buff = new T[m_core_solver.m_m]; m_core_solver.save_state(m_w_buff, m_ed_buff); @@ -167,17 +169,17 @@ template void core_solver_pretty_printer::print_x } int blanks = m_title_width + 1 - m_x_title.size(); - std::cout << m_x_title; - print_blanks(blanks); + m_out << m_x_title; + print_blanks(blanks, m_out); auto bh = m_core_solver.m_x; for (unsigned i = 0; i < ncols(); i++) { string s = T_to_string(bh[i]); int blanks = m_column_widths[i] - s.size(); - print_blanks(blanks); - std::cout << s << " "; // the column interval + print_blanks(blanks, m_out); + m_out << s << " "; // the column interval } - std::cout << std::endl; + m_out << std::endl; } template std::string core_solver_pretty_printer::get_low_bound_string(unsigned j) { @@ -213,16 +215,16 @@ template void core_solver_pretty_printer::print_l return; } int blanks = m_title_width + 1 - m_low_bounds_title.size(); - std::cout << m_low_bounds_title; - print_blanks(blanks); + m_out << m_low_bounds_title; + print_blanks(blanks, m_out); for (unsigned i = 0; i < ncols(); i++) { string s = get_low_bound_string(i); int blanks = m_column_widths[i] - s.size(); - print_blanks(blanks); - std::cout << s << " "; // the column interval + print_blanks(blanks, m_out); + m_out << s << " "; // the column interval } - std::cout << std::endl; + m_out << std::endl; } template void core_solver_pretty_printer::print_upps() { @@ -230,42 +232,42 @@ template void core_solver_pretty_printer::print_u return; } int blanks = m_title_width + 1 - m_upp_bounds_title.size(); - std::cout << m_upp_bounds_title; - print_blanks(blanks); + m_out << m_upp_bounds_title; + print_blanks(blanks, m_out); for (unsigned i = 0; i < ncols(); i++) { string s = get_upp_bound_string(i); int blanks = m_column_widths[i] - s.size(); - print_blanks(blanks); - std::cout << s << " "; // the column interval + print_blanks(blanks, m_out); + m_out << s << " "; // the column interval } - std::cout << std::endl; + m_out << std::endl; } template void core_solver_pretty_printer::print_exact_norms() { int blanks = m_title_width + 1 - m_exact_norm_title.size(); - std::cout << m_exact_norm_title; - print_blanks(blanks); + m_out << m_exact_norm_title; + print_blanks(blanks, m_out); for (unsigned i = 0; i < ncols(); i++) { string s = get_exact_column_norm_string(i); int blanks = m_column_widths[i] - s.size(); - print_blanks(blanks); - std::cout << s << " "; + print_blanks(blanks, m_out); + m_out << s << " "; } - std::cout << std::endl; + m_out << std::endl; } template void core_solver_pretty_printer::print_approx_norms() { int blanks = m_title_width + 1 - m_approx_norm_title.size(); - std::cout << m_approx_norm_title; - print_blanks(blanks); + m_out << m_approx_norm_title; + print_blanks(blanks, m_out); for (unsigned i = 0; i < ncols(); i++) { string s = T_to_string(m_core_solver.m_column_norms[i]); int blanks = m_column_widths[i] - s.size(); - print_blanks(blanks); - std::cout << s << " "; + print_blanks(blanks, m_out); + m_out << s << " "; } - std::cout << std::endl; + m_out << std::endl; } template void core_solver_pretty_printer::print() { @@ -280,13 +282,13 @@ template void core_solver_pretty_printer::print() print_upps(); print_exact_norms(); print_approx_norms(); - std::cout << std::endl; + m_out << std::endl; } template void core_solver_pretty_printer::print_basis_heading() { int blanks = m_title_width + 1 - m_basis_heading_title.size(); - std::cout << m_basis_heading_title; - print_blanks(blanks); + m_out << m_basis_heading_title; + print_blanks(blanks, m_out); if (ncols() == 0) { return; @@ -295,16 +297,16 @@ template void core_solver_pretty_printer::print_b for (unsigned i = 0; i < ncols(); i++) { string s = T_to_string(bh[i]); int blanks = m_column_widths[i] - s.size(); - print_blanks(blanks); - std::cout << s << " "; // the column interval + print_blanks(blanks, m_out); + m_out << s << " "; // the column interval } - std::cout << std::endl; + m_out << std::endl; } template void core_solver_pretty_printer::print_cost() { int blanks = m_title_width + 1 - m_cost_title.size(); - std::cout << m_cost_title; - print_blanks(blanks); + m_out << m_cost_title; + print_blanks(blanks, m_out); print_given_rows(m_costs, m_cost_signs, m_core_solver.get_cost()); } @@ -314,23 +316,23 @@ template void core_solver_pretty_printer::print_g string s = row[col]; int number_of_blanks = width - s.size(); lean_assert(number_of_blanks >= 0); - print_blanks(number_of_blanks); - std::cout << s << ' '; + print_blanks(number_of_blanks, m_out); + m_out << s << ' '; if (col < row.size() - 1) { - std::cout << signs[col + 1] << ' '; + m_out << signs[col + 1] << ' '; } } - std::cout << '='; + m_out << '='; string rs = T_to_string(rst); int nb = m_rs_width - rs.size(); lean_assert(nb >= 0); - print_blanks(nb + 1); - std::cout << rs << std::endl; + print_blanks(nb + 1, m_out); + m_out << rs << std::endl; } template void core_solver_pretty_printer::print_row(unsigned i){ - print_blanks(m_title_width + 1); + print_blanks(m_title_width + 1, m_out); auto row = m_A[i]; auto sign_row = m_signs[i]; auto rs = m_rs[i]; diff --git a/src/util/lp/core_solver_pretty_printer.h b/src/util/lp/core_solver_pretty_printer.h index 37f285a219..484e9817d1 100644 --- a/src/util/lp/core_solver_pretty_printer.h +++ b/src/util/lp/core_solver_pretty_printer.h @@ -9,12 +9,14 @@ #include #include #include +#include #include "util/lp/lp_settings.h" namespace lean { template class lp_core_solver_base; // forward definition template class core_solver_pretty_printer { + std::ostream & m_out; template using vector = std::vector; typedef std::string string; lp_core_solver_base & m_core_solver; @@ -47,7 +49,7 @@ class core_solver_pretty_printer { vector m_exact_column_norms; public: - core_solver_pretty_printer(lp_core_solver_base & core_solver); + core_solver_pretty_printer(lp_core_solver_base & core_solver, std::ostream & out); void init_costs(); @@ -104,7 +106,7 @@ public: void print_basis_heading(); void print_bottom_line() { - std::cout << "----------------------" << std::endl; + m_out << "----------------------" << std::endl; } void print_cost(); diff --git a/src/util/lp/core_solver_pretty_printer_instances.cpp b/src/util/lp/core_solver_pretty_printer_instances.cpp index f43b83f7ab..92c10d1ba2 100644 --- a/src/util/lp/core_solver_pretty_printer_instances.cpp +++ b/src/util/lp/core_solver_pretty_printer_instances.cpp @@ -6,12 +6,12 @@ */ #include "util/lp/numeric_pair.h" #include "util/lp/core_solver_pretty_printer.cpp" -template lean::core_solver_pretty_printer::core_solver_pretty_printer(lean::lp_core_solver_base &); +template lean::core_solver_pretty_printer::core_solver_pretty_printer(lean::lp_core_solver_base &, std::ostream & out); template void lean::core_solver_pretty_printer::print(); template lean::core_solver_pretty_printer::~core_solver_pretty_printer(); -template lean::core_solver_pretty_printer::core_solver_pretty_printer(lean::lp_core_solver_base &); +template lean::core_solver_pretty_printer::core_solver_pretty_printer(lean::lp_core_solver_base &, std::ostream & out); template void lean::core_solver_pretty_printer::print(); template lean::core_solver_pretty_printer::~core_solver_pretty_printer(); -template lean::core_solver_pretty_printer >::core_solver_pretty_printer(lean::lp_core_solver_base > &); +template lean::core_solver_pretty_printer >::core_solver_pretty_printer(lean::lp_core_solver_base > &, std::ostream & out); template lean::core_solver_pretty_printer >::~core_solver_pretty_printer(); template void lean::core_solver_pretty_printer >::print(); diff --git a/src/util/lp/eta_matrix.h b/src/util/lp/eta_matrix.h index 69cbf2e9cd..558af14724 100644 --- a/src/util/lp/eta_matrix.h +++ b/src/util/lp/eta_matrix.h @@ -34,8 +34,8 @@ public: m_column_index(column_index) { } - void print() { - print_matrix(*this); + void print(std::ostream & out) { + print_matrix(*this, out); } bool is_unit() { diff --git a/src/util/lp/indexed_vector.cpp b/src/util/lp/indexed_vector.cpp index eccd782a02..60b3f17ab4 100644 --- a/src/util/lp/indexed_vector.cpp +++ b/src/util/lp/indexed_vector.cpp @@ -9,32 +9,32 @@ namespace lean { template -void print_vector(const std::vector & t) { +void print_vector(const std::vector & t, std::ostream & out) { for (unsigned i = 0; i < t.size(); i++) - std::cout << t[i] << " "; - std::cout << std::endl; + out << t[i] << " "; + out << std::endl; } template -void print_vector(const buffer & t) { +void print_vector(const buffer & t, std::ostream & out) { for (unsigned i = 0; i < t.size(); i++) - std::cout << t[i] << " "; - std::cout << std::endl; + out << t[i] << " "; + out << std::endl; } template -void print_sparse_vector(const std::vector & t) { +void print_sparse_vector(const std::vector & t, std::ostream & out) { for (unsigned i = 0; i < t.size(); i++) { if (is_zero(t[i]))continue; - std::cout << "[" << i << "] = " << t[i] << ", "; + out << "[" << i << "] = " << t[i] << ", "; } - std::cout << std::endl; + out << std::endl; } -void print_vector(const std::vector & t) { +void print_vector(const std::vector & t, std::ostream & out) { for (unsigned i = 0; i < t.size(); i++) - std::cout << t[i].get_double() << std::setprecision(3) << " "; - std::cout << std::endl; + out << t[i].get_double() << std::setprecision(3) << " "; + out << std::endl; } template @@ -81,13 +81,13 @@ bool indexed_vector::is_OK() const { return size == m_index.size(); } template -void indexed_vector::print() { - std::cout << "m_index " << std::endl; +void indexed_vector::print(std::ostream & out) { + out << "m_index " << std::endl; for (unsigned i = 0; i < m_index.size(); i++) { - std::cout << m_index[i] << " "; + out << m_index[i] << " "; } - std::cout << std::endl; - print_vector(m_data); + out << std::endl; + print_vector(m_data, out); } #endif diff --git a/src/util/lp/indexed_vector.h b/src/util/lp/indexed_vector.h index 6d0c02876b..b06ea919e2 100644 --- a/src/util/lp/indexed_vector.h +++ b/src/util/lp/indexed_vector.h @@ -21,11 +21,11 @@ #include namespace lean { -template void print_vector(const std::vector & t); -template void print_vector(const buffer & t); -template void print_sparse_vector(const std::vector & t); +template void print_vector(const std::vector & t, std::ostream & out); +template void print_vector(const buffer & t, std::ostream & out); +template void print_sparse_vector(const std::vector & t, std::ostream & out); -void print_vector(const std::vector & t); +void print_vector(const std::vector & t, std::ostream & out); template class indexed_vector { public: @@ -60,7 +60,7 @@ public: void erase_from_index(unsigned j); #ifdef LEAN_DEBUG bool is_OK() const; - void print(); + void print(std::ostream & out); #endif }; } diff --git a/src/util/lp/lar_core_solver.cpp b/src/util/lp/lar_core_solver.cpp index 82c9d80ff2..d5c8b206ba 100644 --- a/src/util/lp/lar_core_solver.cpp +++ b/src/util/lp/lar_core_solver.cpp @@ -33,7 +33,7 @@ lar_core_solver::lar_core_solver(std::vector & x, std::vector void lar_core_solver::init_costs() { +template void lar_core_solver::init_costs() { lean_assert(this->m_x.size() >= this->m_n); lean_assert(this->m_column_type.size() >= this->m_n); X inf = m_infeasibility; @@ -42,8 +42,8 @@ template void lar_core_solver::init_costs() { init_cost_for_column(j); if (!(this->m_total_iterations ==0 || inf >= m_infeasibility)) { std::cout << "inf was " << T_to_string(inf) << " and now " << T_to_string(m_infeasibility) << std::endl; + lean_unreachable(); } - lean_assert(this->m_total_iterations ==0 || inf >= m_infeasibility); if (inf == m_infeasibility) this->m_iters_with_no_cost_growing++; } @@ -171,7 +171,7 @@ template void lar_core_solver::calculate_pivot this->calculate_pivot_row_when_pivot_row_of_B1_is_ready(); } - +#ifdef LEAN_DEBUG template X lar_core_solver::get_deb_inf_column(unsigned j) { const X & x = this->m_x[j]; switch (this->m_column_type[j]) { @@ -206,31 +206,28 @@ template X lar_core_solver::get_deb_inf() { X ret = zero_of_type(); for (unsigned j = 0; j < this->m_n; j++) { X d = get_deb_inf_column(j); - // if (! numeric_traits::is_zero(d)) { - // std::cout << "column " << j << ", " << this->column_name(j) << " inf is " << d.get_double() << std::endl; - // } ret += d; } return ret; } -template bool lar_core_solver::debug_profit_delta(unsigned j, const T & delta) { +template bool lar_core_solver::debug_profit_delta(unsigned j, const T & delta, std::ostream & out) { this->update_x(j, delta); bool ret = m_infeasibility > get_deb_inf(); if (ret) { - std::cout << "found profit for " << this->column_name(j) << " and delta = " << delta.get_double() << std::endl; - std::cout << "improvement = " << (m_infeasibility - get_deb_inf()).get_double() << std::endl; + out << "found profit for " << this->column_name(j) << " and delta = " << delta.get_double() << std::endl; + out << "improvement = " << (m_infeasibility - get_deb_inf()).get_double() << std::endl; } return ret; } -template bool lar_core_solver::debug_profit(unsigned j) { +template bool lar_core_solver::debug_profit(unsigned j, std::ostream & out) { if (this->m_column_type[j] == fixed) return false; T delta = numeric_traits::one() / 10000000; delta /= 10000000; - return debug_profit_delta(j, -delta) || debug_profit_delta(j, delta); + return debug_profit_delta(j, -delta, out) || debug_profit_delta(j, delta, out); } - +#endif template int lar_core_solver::choose_column_entering_basis() { unsigned offset = my_random() % this->m_non_basic_columns.size(); unsigned initial_offset_in_non_basis = offset; @@ -253,7 +250,6 @@ template void lar_core_solver::one_iteration() } int entering = choose_column_entering_basis(); if (entering == -1) { - std::cout << "cannot choose entering" << std::endl; decide_on_status_when_cannot_enter(); } else { advance_on_entering(entering); @@ -266,7 +262,6 @@ template void lar_core_solver::decide_on_statu this->m_status = INFEASIBLE; else this->m_status = FEASIBLE; - std::cout << "status is " << lp_status_to_string(this->m_status) << std::endl; } // j is the basic column, x is the value at x[j] @@ -339,27 +334,27 @@ template std::string lar_core_solver::break_typ return "type is not found"; } -template void lar_core_solver::print_breakpoint(const breakpoint * b) { - std::cout << "(" << this->column_name(b->m_j) << "," << break_type_to_string(b->m_type) << "," << T_to_string(b->m_delta) << ")" << std::endl; +template void lar_core_solver::print_breakpoint(const breakpoint * b, std::ostream & out) { + out << "(" << this->column_name(b->m_j) << "," << break_type_to_string(b->m_type) << "," << T_to_string(b->m_delta) << ")" << std::endl; print_bound_info_and_x(b->m_j); } -template void lar_core_solver::print_bound_info_and_x(unsigned j) { - std::cout << "type of " << this->column_name(j) << " is " << column_type_to_string(this->m_column_type[j]) << std::endl; - std::cout << "x[" << this->column_name(j) << "] = " << this->m_x[j] << std::endl; +template void lar_core_solver::print_bound_info_and_x(unsigned j, std::ostream & out) { + out << "type of " << this->column_name(j) << " is " << column_type_to_string(this->m_column_type[j]) << std::endl; + out << "x[" << this->column_name(j) << "] = " << this->m_x[j] << std::endl; switch (this->m_column_type[j]) { case fixed: case boxed: - std::cout << "[" << this->m_low_bound_values[j] << "," << this->m_upper_bound_values[j] << "]" << std::endl; + out << "[" << this->m_low_bound_values[j] << "," << this->m_upper_bound_values[j] << "]" << std::endl; break; case low_bound: - std::cout << "[" << this->m_low_bound_values[j] << ", inf" << std::endl; + out << "[" << this->m_low_bound_values[j] << ", inf" << std::endl; break; case upper_bound: - std::cout << "inf ," << this->m_upper_bound_values[j] << "]" << std::endl; + out << "inf ," << this->m_upper_bound_values[j] << "]" << std::endl; break; case free_column: - std::cout << "inf, inf" << std::endl; + out << "inf, inf" << std::endl; break; default: lean_assert(false); @@ -393,16 +388,16 @@ template void lar_core_solver::advance_on_ente advance_on_sorted_breakpoints(entering); } -template void lar_core_solver::print_cost() { - std::cout << "reduced costs " << std::endl; +template void lar_core_solver::print_cost(std::ostream & out) { + out << "reduced costs " << std::endl; for (unsigned j = 0; j < this->m_n; j++) { if (numeric_traits::is_zero(this->m_d[j])) continue; - std::cout << T_to_string(this->m_d[j]) << this->column_name(j) << " "; + out << T_to_string(this->m_d[j]) << this->column_name(j) << " "; } - std::cout << std::endl; + out << std::endl; } -template void lar_core_solver::update_basis_and_x_with_comparison(unsigned entering, unsigned leaving, X delta) { +template void lar_core_solver::update_basis_and_x_with_comparison(unsigned entering, unsigned leaving, X delta) { if (entering != leaving) this->update_basis_and_x(entering, leaving, delta); else @@ -487,30 +482,22 @@ template bool lar_core_solver::find_evidence_r } -template bool lar_core_solver::done() { +template bool lar_core_solver::done() { if (this->m_status == OPTIMAL) return true; if (this->m_status == INFEASIBLE) { if (this->m_settings.row_feasibility == false) { - if (find_evidence_row()) { - std::cout << "found evidence" << std::endl; - } else { - std::cout << "did not find evidence" << std::endl; - std::cout << "started feasibility_loop at iteration " << this->m_total_iterations << std::endl; - unsigned iters = this->m_total_iterations; + if (!find_evidence_row()) { this->m_status = FEASIBLE; row_feasibility_loop(); - std::cout << "made another " << this->m_total_iterations - iters << ", percentage is " << 100.0 * (this->m_total_iterations - iters) / this->m_total_iterations << std::endl; } } return true; } if (this->m_iters_with_no_cost_growing >= this->m_settings.max_number_of_iterations_with_no_improvements) { - std::cout << "m_iters_with_no_cost_growing = " << this->m_iters_with_no_cost_growing << std::endl; this->m_status = ITERATIONS_EXHAUSTED; return true; } if (this->m_total_iterations >= this->m_settings.max_total_number_of_iterations) { - std::cout << "max_total_number_of_iterations " << this->m_total_iterations << " is reached " << std::endl; this->m_status = ITERATIONS_EXHAUSTED; return true; } return false; @@ -789,26 +776,24 @@ template void lar_core_solver::solve() { lean_assert(non_basis_columns_are_set_correctly()); if (this->m_settings.row_feasibility) { - std::cout << "optimizing by rows " << std::endl; row_feasibility_loop(); } else { - std::cout << "optimizing total infeasibility" << std::endl; feasibility_loop(); } } -template void lar_core_solver::print_column_info(unsigned j) { - std::cout << "type = " << column_type_to_string(this->m_column_type[j]) << std::endl; +template void lar_core_solver::print_column_info(unsigned j, std::ostream & out) { + out << "type = " << column_type_to_string(this->m_column_type[j]) << std::endl; switch (this->m_column_type[j]) { case fixed: case boxed: - std::cout << "(" << this->m_low_bound_values[j] << ", " << this->m_upper_bound_values[j] << ")" << std::endl; + out << "(" << this->m_low_bound_values[j] << ", " << this->m_upper_bound_values[j] << ")" << std::endl; break; case low_bound: - std::cout << this->m_low_bound_values[j] << std::endl; + out << this->m_low_bound_values[j] << std::endl; break; case upper_bound: - std::cout << this->m_upper_bound_values[j] << std::endl; + out << this->m_upper_bound_values[j] << std::endl; break; default: lean_unreachable(); diff --git a/src/util/lp/lar_core_solver.h b/src/util/lp/lar_core_solver.h index ce2ea4060f..f74a85f430 100644 --- a/src/util/lp/lar_core_solver.h +++ b/src/util/lp/lar_core_solver.h @@ -62,9 +62,9 @@ public: X get_deb_inf(); - bool debug_profit_delta(unsigned j, const T & delta); + bool debug_profit_delta(unsigned j, const T & delta, std::ostream & out); - bool debug_profit(unsigned j); + bool debug_profit(unsigned j, std::ostream & out); int choose_column_entering_basis(); @@ -86,9 +86,9 @@ public: std::string break_type_to_string(breakpoint_type type); - void print_breakpoint(const breakpoint * b); + void print_breakpoint(const breakpoint * b, std::ostream & out); - void print_bound_info_and_x(unsigned j); + void print_bound_info_and_x(unsigned j, std::ostream & out); void clear_breakpoints(); @@ -96,7 +96,7 @@ public: void advance_on_entering(unsigned entering); - void print_cost(); + void print_cost(std::ostream & out); void update_basis_and_x_with_comparison(unsigned entering, unsigned leaving, X delta); @@ -171,6 +171,6 @@ public: bool low_bounds_are_set() const { return true; } - void print_column_info(unsigned j); + void print_column_info(unsigned j, std::ostream & out); }; } diff --git a/src/util/lp/lar_core_solver_instances.cpp b/src/util/lp/lar_core_solver_instances.cpp index 387890619c..e3852483a0 100644 --- a/src/util/lp/lar_core_solver_instances.cpp +++ b/src/util/lp/lar_core_solver_instances.cpp @@ -8,6 +8,8 @@ template lean::lar_core_solver >::lar_core_solver(std::vector, std::allocator > >&, std::vector >&, std::vector, std::allocator > >&, std::vector, std::allocator > >&, std::vector >&, lean::static_matrix >&, lean::lp_settings&, std::unordered_map, std::equal_to, std::allocator > >&, std::vector, std::allocator > >&, std::vector >&); template void lean::lar_core_solver >::solve(); template void lean::lar_core_solver >::prefix(); -template void lean::lar_core_solver >::print_column_info(unsigned int); +template void lean::lar_core_solver >::print_column_info(unsigned int, std::ostream & out); +#ifdef LEAN_DEBUG template lean::numeric_pair lean::lar_core_solver >::get_deb_inf(); +#endif template bool lean::lar_core_solver >::is_empty() const; diff --git a/src/util/lp/lar_solver.cpp b/src/util/lp/lar_solver.cpp index c234e2430e..585fd7e55a 100644 --- a/src/util/lp/lar_solver.cpp +++ b/src/util/lp/lar_solver.cpp @@ -306,10 +306,7 @@ var_index lar_solver::add_var(std::string s) { } constraint_index lar_solver::add_constraint(const buffer>& left_side, lconstraint_kind kind_par, mpq right_side_par) { - if (left_side.size() == 0) { - std::cout << "cannot add a constraint without left side" << std::endl; - return (constraint_index)(-1); - } + lean_assert(left_side.size()); constraint_index i = m_available_constr_index++; lar_constraint original_constr(left_side, kind_par, right_side_par, i); canonic_left_side * ls = create_or_fetch_existing_left_side(left_side); @@ -317,7 +314,6 @@ constraint_index lar_solver::add_constraint(const buffer>& auto kind = ratio.is_neg()? flip_kind(kind_par): kind_par; mpq right_side = right_side_par / ratio; lar_normalized_constraint normalized_constraint(ls, ratio, kind, right_side, original_constr); - m_normalized_constraints[i] = normalized_constraint; return i; } @@ -327,8 +323,6 @@ bool lar_solver::all_constraints_hold() { get_model(var_map); for ( auto & it : m_normalized_constraints ) if (!constraint_holds(it.second.m_origin_constraint, var_map)) { - print_constraint(&it.second.m_origin_constraint); - std::cout << std::endl; return false; } return true; @@ -362,9 +356,7 @@ bool lar_solver::the_relations_are_of_same_type(const buffer for (auto & it : evidence) { mpq coeff = it.first; constraint_index con_ind = it.second; - std::cout << coeff.get_double() << std::endl; lar_constraint & constr = m_normalized_constraints[con_ind].m_origin_constraint; - print_constraint(&constr); std::cout << std::endl; lconstraint_kind kind = coeff.is_pos()? constr.m_kind: flip_kind(constr.m_kind); if (kind == GT || kind == LT) @@ -553,7 +545,6 @@ lp_status lar_solver::check() { } void lar_solver::get_infeasibility_evidence(buffer> & evidence){ if (!m_mpq_core_solver.get_infeasible_row_sign()) { - std::cout << "don't have the infeasibility evidence" << std::endl; return; } // the infeasibility sign @@ -629,7 +620,6 @@ void lar_solver::get_model(std::unordered_map & variable_values) mpq delta = find_delta_for_strict_bounds(); for (auto & it : m_map_from_var_index_to_left_side) { numeric_pair & rp = m_x[it.second->m_column_index]; - // std::cout << it.second->m_column_info.get_name() << " = " << rp << std::endl; variable_values[it.first] = rp.x + delta * rp.y; } } @@ -643,17 +633,17 @@ std::string lar_solver::get_variable_name(var_index vi) { } // ********** print region start -void lar_solver::print_constraint(constraint_index ci) { +void lar_solver::print_constraint(constraint_index ci, std::ostream & out) { if (m_normalized_constraints.size() <= ci) { std::string s = "constraint " + T_to_string(ci) + " is not found"; - std::cout << s << std::endl; + out << s << std::endl; return; } - print_constraint(&m_normalized_constraints[ci]); + print_constraint(&m_normalized_constraints[ci], out); } -void lar_solver::print_canonic_left_side(const canonic_left_side & c) { +void lar_solver::print_canonic_left_side(const canonic_left_side & c, std::ostream & out) { bool first = true; for (auto it : c.m_coeffs) { auto val = it.first; @@ -661,19 +651,19 @@ void lar_solver::print_canonic_left_side(const canonic_left_side & c) { first = false; } else { if (val.is_pos()) { - std::cout << " + "; + out << " + "; } else { - std::cout << " - "; + out << " - "; val = -val; } } if (val != numeric_traits::one()) - std::cout << T_to_string(val); - std::cout << m_map_from_var_index_to_left_side[it.second]->m_column_info.get_name(); + out << T_to_string(val); + out << m_map_from_var_index_to_left_side[it.second]->m_column_info.get_name(); } } -void lar_solver::print_left_side_of_constraint(const lar_base_constraint * c) { +void lar_solver::print_left_side_of_constraint(const lar_base_constraint * c, std::ostream & out) { bool first = true; for (auto it : c->get_left_side_coefficients()) { auto val = it.first; @@ -682,60 +672,40 @@ void lar_solver::print_left_side_of_constraint(const lar_base_constraint * c) { first = false; } else { if (val.is_pos()) { - std::cout << " + "; + out << " + "; } else { - std::cout << " - "; + out << " - "; val = -val; } } if (val != numeric_traits::one()) - std::cout << val; - std::cout << m_map_from_var_index_to_left_side[it.second]->m_column_info.get_name(); + out << val; + out << m_map_from_var_index_to_left_side[it.second]->m_column_info.get_name(); } } -numeric_pair lar_solver::get_infeasibility_from_core_solver(std::unordered_map & solution) { - prepare_independently_of_numeric_type(); - prepare_core_solver_fields(m_A, m_x, m_right_side_vector, m_low_bounds, m_upper_bounds); - m_mpq_core_solver.prefix(); // just to fill the core solver - - for (auto ls : m_canonic_left_sides) { - lean_assert(valid_index(ls->m_column_index)); - m_x[ls->m_column_index] = numeric_pair(get_canonic_left_side_val(ls, solution), 0); - } - return m_mpq_core_solver.get_deb_inf(); -} - -void lar_solver::print_info_on_column(unsigned j) { +void lar_solver::print_info_on_column(unsigned j, std::ostream & out) { for (auto ls : m_canonic_left_sides) { if (static_cast(ls->m_column_index) == j) { auto & ci = ls->m_column_info; if (ci.low_bound_is_set()) { - std::cout << "l = " << ci.get_low_bound(); + out << "l = " << ci.get_low_bound(); } if (ci.upper_bound_is_set()) { - std::cout << "u = " << ci.get_upper_bound(); + out << "u = " << ci.get_upper_bound(); } - std::cout << std::endl; - m_mpq_core_solver.print_column_info(j); + out << std::endl; + m_mpq_core_solver.print_column_info(j, out); } } } mpq lar_solver::get_infeasibility_of_solution(std::unordered_map & solution) { - std::cout << "solution" << std::endl; - for (auto it : solution) { - std::cout << it.first << " = " << it.second.get_double() << std::endl; - } mpq ret = numeric_traits::zero(); for (auto it : m_normalized_constraints) { ret += get_infeasibility_of_constraint(it.second, solution); } - std::cout << "ret = " << ret.get_double() << std::endl; - auto core_inf = get_infeasibility_from_core_solver(solution); - std::cout << "core inf = " << T_to_string(core_inf) << std::endl; - lean_assert(numeric_pair(ret, 0) == core_inf); return ret; } @@ -783,9 +753,9 @@ mpq lar_solver::get_left_side_val(const lar_constraint & cns, const std::unorde return ret; } -void lar_solver::print_constraint(const lar_base_constraint * c) { - print_left_side_of_constraint(c); - std::cout <<" " << lconstraint_kind_string(c->m_kind) << " " << c->m_right_side; +void lar_solver::print_constraint(const lar_base_constraint * c, std::ostream & out) { + print_left_side_of_constraint(c, out); + out <<" " << lconstraint_kind_string(c->m_kind) << " " << c->m_right_side; } } diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h index 9b6f3d8791..d72f13f6ef 100644 --- a/src/util/lp/lar_solver.h +++ b/src/util/lp/lar_solver.h @@ -217,15 +217,15 @@ public: std::string get_variable_name(var_index vi); - void print_constraint(constraint_index ci); + void print_constraint(constraint_index ci, std::ostream & out); - void print_canonic_left_side(const canonic_left_side & c); + void print_canonic_left_side(const canonic_left_side & c, std::ostream & out); - void print_left_side_of_constraint(const lar_base_constraint * c); + void print_left_side_of_constraint(const lar_base_constraint * c, std::ostream & out); numeric_pair get_infeasibility_from_core_solver(std::unordered_map & solution); - void print_info_on_column(unsigned j); + void print_info_on_column(unsigned j, std::ostream & out); mpq get_infeasibility_of_solution(std::unordered_map & solution); @@ -235,7 +235,7 @@ public: mpq get_left_side_val(const lar_constraint & cns, const std::unordered_map & var_map); - void print_constraint(const lar_base_constraint * c); + void print_constraint(const lar_base_constraint * c, std::ostream & out); unsigned get_total_iterations() const { return m_mpq_core_solver.m_total_iterations; } }; } diff --git a/src/util/lp/lp_core_solver_base.cpp b/src/util/lp/lp_core_solver_base.cpp index 9f8bf8ae69..0dc5929477 100644 --- a/src/util/lp/lp_core_solver_base.cpp +++ b/src/util/lp/lp_core_solver_base.cpp @@ -133,8 +133,8 @@ solve_Bd(unsigned entering) { } template void lp_core_solver_base:: -pretty_print() { - core_solver_pretty_printer pp(*this); +pretty_print(std::ostream & out) { + core_solver_pretty_printer pp(*this, out); pp.print(); } @@ -197,7 +197,7 @@ A_mult_x_is_off() { X delta = abs(m_b[i] - m_A.dot_product_with_row(i, m_x)); X eps = feps * (one + T(0.1) * abs(m_b[i])); - if (delta >eps) { + if (delta > eps) { std::cout << "x is off ("; std::cout << "m_b[" << i << "] = " << m_b[i] << " "; std::cout << "left side = " << m_A.dot_product_with_row(i, m_x) << ' '; @@ -373,7 +373,6 @@ template bool lp_core_solver_base:: time_is_over() { int span_in_mills = get_millisecond_span(m_start_time); if (span_in_mills / 1000.0 > m_settings.time_limit) { - std::cout << "time is over" << std::endl; return true; } return false; @@ -397,10 +396,6 @@ template bool lp_core_solver_base:: find_x_by_solving() { solve_Ax_eq_b(); bool ret= !A_mult_x_is_off(); - if (ret) - std::cout << "find_x_by_solving succeeded" << std::endl; - else - std::cout << "find_x_by_solving did not succeed" << std::endl; return ret; } @@ -523,7 +518,6 @@ restore_x_and_refactor(int entering, int leaving, X const & t) { template void lp_core_solver_base:: restore_x(unsigned entering, X const & t) { if (is_zero(t)) return; - std::cout << "calling restore for entering " << entering << std::endl; m_x[entering] -= t; for (unsigned i : m_index_of_ed) { m_x[m_basis[i]] = m_copy_of_xB[i]; diff --git a/src/util/lp/lp_core_solver_base.h b/src/util/lp/lp_core_solver_base.h index 68847c43d2..3b8102d962 100644 --- a/src/util/lp/lp_core_solver_base.h +++ b/src/util/lp/lp_core_solver_base.h @@ -100,7 +100,7 @@ public: void solve_Bd(unsigned entering); - void pretty_print(); + void pretty_print(std::ostream & out); void save_state(T * w_buffer, T * d_buffer); diff --git a/src/util/lp/lp_core_solver_base_instances.cpp b/src/util/lp/lp_core_solver_base_instances.cpp index 7273555d6c..3c54e6df13 100644 --- a/src/util/lp/lp_core_solver_base_instances.cpp +++ b/src/util/lp/lp_core_solver_base_instances.cpp @@ -55,15 +55,15 @@ template void lean::lp_core_solver_base template lean::lp_core_solver_base::lp_core_solver_base(lean::static_matrix&, std::vector >&, std::vector >&, std::vector >&, std::vector >&, lean::lp_settings&, std::unordered_map, std::equal_to, std::allocator > > const&, std::vector >&, std::vector >&, std::vector >&); template bool lean::lp_core_solver_base >::print_statistics_with_iterations_and_check_that_the_time_is_over(unsigned int); template std::string lean::lp_core_solver_base::column_name(unsigned int) const; -template void lean::lp_core_solver_base::pretty_print(); +template void lean::lp_core_solver_base::pretty_print(std::ostream & out); template void lean::lp_core_solver_base::restore_state(double*, double*); template void lean::lp_core_solver_base::save_state(double*, double*); template std::string lean::lp_core_solver_base::column_name(unsigned int) const; -template void lean::lp_core_solver_base::pretty_print(); +template void lean::lp_core_solver_base::pretty_print(std::ostream & out); template void lean::lp_core_solver_base::restore_state(lean::mpq*, lean::mpq*); template void lean::lp_core_solver_base::save_state(lean::mpq*, lean::mpq*); template std::string lean::lp_core_solver_base >::column_name(unsigned int) const; -template void lean::lp_core_solver_base >::pretty_print(); +template void lean::lp_core_solver_base >::pretty_print(std::ostream & out); template void lean::lp_core_solver_base >::restore_state(lean::mpq*, lean::mpq*); template void lean::lp_core_solver_base >::save_state(lean::mpq*, lean::mpq*); template void lean::lp_core_solver_base >::solve_yB(std::vector >&); diff --git a/src/util/lp/lp_dual_core_solver.cpp b/src/util/lp/lp_dual_core_solver.cpp index 117f566538..c12c09037a 100644 --- a/src/util/lp/lp_dual_core_solver.cpp +++ b/src/util/lp/lp_dual_core_solver.cpp @@ -56,12 +56,12 @@ template void lp_dual_core_solver::fill_non_basis } } -template void lp_dual_core_solver::print_nb() { - std::cout << "this is nb " << std::endl; +template void lp_dual_core_solver::print_nb(std::ostream & out) { + out << "this is nb " << std::endl; for (auto l : this->m_factorization->m_non_basic_columns) { - std::cout << l << " "; + out << l << " "; } - std::cout << std::endl; + out << std::endl; } template void lp_dual_core_solver::restore_non_basis() { @@ -83,7 +83,9 @@ template bool lp_dual_core_solver::update_basis(i if (!(this->m_refactor_counter++ >= 200)) { this->m_factorization->replace_column(leaving, this->m_ed[this->m_factorization->basis_heading(leaving)], this->m_w); if (this->m_factorization->get_status() != LU_status::OK) { +#ifdef LEAN_DEBUG std::cout << "failed on replace_column( " << leaving << ", " << this->m_ed[this->m_factorization->basis_heading(leaving)] << ") total_iterations = " << this->m_total_iterations << std::endl; +#endif init_factorization(this->m_factorization, this->m_A, this->m_basis, this->m_basis_heading, this->m_settings, this->m_non_basic_columns); this->m_iters_with_no_cost_growing++; this->m_status = UNSTABLE; @@ -94,7 +96,9 @@ template bool lp_dual_core_solver::update_basis(i this->m_factorization->change_basis(entering, leaving); init_factorization(this->m_factorization, this->m_A, this->m_basis, this->m_basis_heading, this->m_settings, this->m_non_basic_columns); if (this->m_factorization->get_status() != LU_status::OK) { +#ifdef LEAN_DEBUG std::cout << "failing refactor for entering = " << entering << ", leaving = " << leaving << " total_iterations = " << this->m_total_iterations << std::endl; +#endif this->m_iters_with_no_cost_growing++; return false; } @@ -157,14 +161,6 @@ template T lp_dual_core_solver::get_edge_steepnes return del / this->m_betas[this->m_basis_heading[p]]; } -//template void lp_dual_core_solver::print_x_and_low_bound(unsigned p) { -// std::cout << "x l[" << p << "] = " << this->m_x[p] << " " << this->m_low_bound_values[p] << std::endl; -// } -//template void lp_dual_core_solver::print_x_and_upper_bound(unsigned p) { -// std::cout << "x u[" << p << "] = " << this->m_x[p] << " " << this->m_upper_bound_values[p] << std::endl; -// } - -// returns the template T lp_dual_core_solver::pricing_for_row(unsigned i) { unsigned p = this->m_basis[i]; switch (this->m_column_type[p]) { @@ -172,22 +168,16 @@ template T lp_dual_core_solver::pricing_for_row(u case boxed: if (this->x_below_low_bound(p)) { T del = get_edge_steepness_for_low_bound(p); - // std::cout << "case boxed low_bound in pricing" << std::endl; - // print_x_and_low_bound(p); return del; } if (this->x_above_upper_bound(p)) { T del = get_edge_steepness_for_upper_bound(p); - // std::cout << "case boxed at upper_bound in pricing" << std::endl; - // print_x_and_upper_bound(p); return del; } return numeric_traits::zero(); case low_bound: if (this->x_below_low_bound(p)) { T del = get_edge_steepness_for_low_bound(p); - // std::cout << "case low_bound in pricing" << std::endl; - // print_x_and_low_bound(p); return del; } return numeric_traits::zero(); @@ -195,8 +185,6 @@ template T lp_dual_core_solver::pricing_for_row(u case upper_bound: if (this->x_above_upper_bound(p)) { T del = get_edge_steepness_for_upper_bound(p); - // std::cout << "case upper_bound in pricing" << std::endl; - // print_x_and_upper_bound(p); return del; } return numeric_traits::zero(); @@ -250,9 +238,6 @@ template void lp_dual_core_solver::pricing_loop(u steepest_edge_max = numeric_traits::zero(); rows_left = number_of_rows_to_try; goto loop_start; - // if (this->m_total_iterations % 80 == 0) { - // std::cout << "m_delta = " << m_delta << std::endl; - // } } } @@ -362,7 +347,6 @@ template T lp_dual_core_solver::get_delta() { } template void lp_dual_core_solver::restore_d() { - std::cout << "restore_d" << std::endl; this->m_d[m_p] = numeric_traits::zero(); for (auto j : non_basis()) { this->m_d[j] += m_theta_D * this->m_pivot_row[j]; @@ -457,12 +441,10 @@ template void lp_dual_core_solver::init_beta_prec } template void lp_dual_core_solver::init_betas_precisely() { - std::cout << "init beta precisely..." << std::endl; unsigned i = this->m_m; while (i--) { init_beta_precisely(i); } - std::cout << "done" << std::endl; } // step 7 of the algorithm from Progress @@ -483,7 +465,6 @@ template bool lp_dual_core_solver::basis_change_a } template void lp_dual_core_solver::revert_to_previous_basis() { - std::cout << "recovering basis p = " << m_p << " q = " << m_q << std::endl; this->m_factorization->change_basis(m_p, m_q); init_factorization(this->m_factorization, this->m_A, this->m_basis, this->m_basis_heading, this->m_settings, this->m_non_basic_columns); if (this->m_factorization->get_status() != LU_status::OK) { @@ -535,12 +516,9 @@ template bool lp_dual_core_solver::delta_keeps_th } template void lp_dual_core_solver::set_status_to_tentative_dual_unbounded_or_dual_unbounded() { - std::cout << "cost = " << this->get_cost() << std::endl; if (this->m_status == TENTATIVE_DUAL_UNBOUNDED) { - std::cout << "setting status to DUAL_UNBOUNDED" << std::endl; this->m_status = DUAL_UNBOUNDED; } else { - std::cout << "setting to TENTATIVE_DUAL_UNBOUNDED" << std::endl; this->m_status = TENTATIVE_DUAL_UNBOUNDED; } } diff --git a/src/util/lp/lp_dual_core_solver.h b/src/util/lp/lp_dual_core_solver.h index 9f16010391..ed05226da1 100644 --- a/src/util/lp/lp_dual_core_solver.h +++ b/src/util/lp/lp_dual_core_solver.h @@ -49,7 +49,7 @@ public: void fill_non_basis_with_only_able_to_enter_columns(); - void print_nb(); + void print_nb(std::ostream & out); void restore_non_basis(); diff --git a/src/util/lp/lp_dual_simplex.cpp b/src/util/lp/lp_dual_simplex.cpp index e6b572e4ad..46bc0e3485 100644 --- a/src/util/lp/lp_dual_simplex.cpp +++ b/src/util/lp/lp_dual_simplex.cpp @@ -12,24 +12,19 @@ template void lp_dual_simplex::decide_on_status_a case OPTIMAL: if (this->m_settings.abs_val_is_smaller_than_artificial_tolerance(m_core_solver->get_cost())) { this->m_status = FEASIBLE; - std::cout << "status is FEASIBLE" << std::endl; } else { - std::cout << "status is UNBOUNDED" << std::endl; this->m_status = UNBOUNDED; } break; case DUAL_UNBOUNDED: lean_unreachable(); case ITERATIONS_EXHAUSTED: - std::cout << "status is ITERATIONS_EXHAUSTED" << std::endl; this->m_status = ITERATIONS_EXHAUSTED; break; case TIME_EXHAUSTED: - std::cout << "status is TIME_EXHAUSTED" << std::endl; this->m_status = TIME_EXHAUSTED; break; case FLOATING_POINT_ERROR: - std::cout << "status is FLOATING_POINT_ERROR" << std::endl; this->m_status = FLOATING_POINT_ERROR; break; default: @@ -79,12 +74,8 @@ template void lp_dual_simplex::fix_structural_for default: lean_unreachable(); } - T cost_was = this->m_costs[j]; + // T cost_was = this->m_costs[j]; this->set_scaled_cost(j); - bool in_basis = m_core_solver->m_factorization->m_basis_heading[j] >= 0; - if (in_basis && cost_was != this->m_costs[j]) { - std::cout << "cost change in basis" << std::endl; - } } template void lp_dual_simplex::unmark_boxed_and_fixed_columns_and_fix_structural_costs() { @@ -157,11 +148,10 @@ template void lp_dual_simplex::stage1() { m_core_solver->fill_reduced_costs_from_m_y_by_rows(); m_core_solver->start_with_initial_basis_and_make_it_dual_feasible(); if (this->m_settings.abs_val_is_smaller_than_artificial_tolerance(m_core_solver->get_cost())) { - std::cout << "skipping stage 1" << std::endl; + // skipping stage 1 m_core_solver->set_status(OPTIMAL); m_core_solver->m_total_iterations = 0; } else { - std::cout << "stage 1" << std::endl; m_core_solver->solve(); } decide_on_status_after_stage1(); @@ -169,7 +159,6 @@ template void lp_dual_simplex::stage1() { } template void lp_dual_simplex::stage2() { - std::cout << "starting stage2" << std::endl; unmark_boxed_and_fixed_columns_and_fix_structural_costs(); restore_right_sides(); solve_for_stage2(); diff --git a/src/util/lp/lp_primal_core_solver.cpp b/src/util/lp/lp_primal_core_solver.cpp index 7ae9540ea5..ff5b618668 100644 --- a/src/util/lp/lp_primal_core_solver.cpp +++ b/src/util/lp/lp_primal_core_solver.cpp @@ -4,10 +4,7 @@ Author: Lev Nachmanson */ - - - - +#include #include "util/lp/lp_primal_core_solver.h" namespace lean { @@ -269,7 +266,7 @@ template void lp_primal_core_solver::init_lu() this->m_refactor_counter = 0; } -template bool lp_primal_core_solver::initial_x_is_correct() { +template bool lp_primal_core_solver::initial_x_is_correct() { std::set basis_set; for (int i = 0; i < this->m_A.row_count(); i++) { basis_set.insert(this->m_basis[i]); @@ -539,17 +536,17 @@ template unsigned lp_primal_core_solver::get_n return std::max(static_cast(my_random() % ret), 1u); } -template void lp_primal_core_solver::print_column_norms() { - std::cout << " column norms " << std::endl; +template void lp_primal_core_solver::print_column_norms(std::ostream & out) { + out << " column norms " << std::endl; for (unsigned j = 0; j < this->m_n; j++) { - std::cout << this->m_column_norms[j] << " "; + out << this->m_column_norms[j] << " "; } - std::cout << std::endl; - std::cout << std::endl; + out << std::endl; + out << std::endl; } // returns the number of iterations -template unsigned lp_primal_core_solver::solve() { +template unsigned lp_primal_core_solver::solve() { init_run(); lean_assert(!this->A_mult_x_is_off()); do { @@ -902,17 +899,15 @@ template bool lp_primal_core_solver::can_enter -template bool lp_primal_core_solver::done() { +template bool lp_primal_core_solver::done() { if (this->m_status == OPTIMAL ||this->m_status == FLOATING_POINT_ERROR) return true; if (this->m_status == INFEASIBLE) { return true; } if (this->m_iters_with_no_cost_growing >= this->m_settings.max_number_of_iterations_with_no_improvements) { - std::cout << "m_iters_with_no_cost_growing = " << this->m_iters_with_no_cost_growing << std::endl; this->m_status = ITERATIONS_EXHAUSTED; return true; } if (this->m_total_iterations >= this->m_settings.max_total_number_of_iterations) { - std::cout << "max_total_number_of_iterations " << this->m_total_iterations << " is reached " << std::endl; this->m_status = ITERATIONS_EXHAUSTED; return true; } return false; @@ -931,21 +926,21 @@ template void lp_primal_core_solver::init_infe m_using_inf_costs = true; } -template void lp_primal_core_solver::print_column(unsigned j) { - std::cout << this->column_name(j) << " " << j << " " << column_type_to_string(this->m_column_type[j]) << " x = " << this->m_x[j] << " " << "c = " << this->m_costs[j];; +template void lp_primal_core_solver::print_column(unsigned j, std::ostream & out) { + out << this->column_name(j) << " " << j << " " << column_type_to_string(this->m_column_type[j]) << " x = " << this->m_x[j] << " " << "c = " << this->m_costs[j];; switch (this->m_column_type[j]) { case fixed: case boxed: - std::cout << "( " << this->m_low_bound_values[j] << " " << this->m_x[j] << " " << this->m_upper_bound_values[j] << ")" << std::endl; + out << "( " << this->m_low_bound_values[j] << " " << this->m_x[j] << " " << this->m_upper_bound_values[j] << ")" << std::endl; break; case upper_bound: - std::cout << "( _" << this->m_x[j] << " " << this->m_upper_bound_values[j] << ")" << std::endl; + out << "( _" << this->m_x[j] << " " << this->m_upper_bound_values[j] << ")" << std::endl; break; case low_bound: - std::cout << "( " << this->m_low_bound_values[j] << " " << this->m_x[j] << " " << "_ )" << std::endl; + out << "( " << this->m_low_bound_values[j] << " " << this->m_x[j] << " " << "_ )" << std::endl; break; case free_column: - std::cout << "( _" << this->m_x[j] << "_)" << std::endl; + out << "( _" << this->m_x[j] << "_)" << std::endl; default: lean_unreachable(); } diff --git a/src/util/lp/lp_primal_core_solver.h b/src/util/lp/lp_primal_core_solver.h index 4e885ec85a..221d00a5be 100644 --- a/src/util/lp/lp_primal_core_solver.h +++ b/src/util/lp/lp_primal_core_solver.h @@ -166,7 +166,7 @@ public: unsigned get_number_of_non_basic_column_to_try_for_enter(); - void print_column_norms(); + void print_column_norms(std::ostream & out); void set_current_x_is_feasible() { m_current_x_is_feasible = calc_current_x_is_feasible(); } // returns the number of iterations @@ -400,7 +400,7 @@ public: void init_infeasibility_costs(); - void print_column(unsigned j); + void print_column(unsigned j, std::ostream & out); void init_infeasibility_cost_for_column(unsigned j); diff --git a/src/util/lp/lp_primal_simplex.cpp b/src/util/lp/lp_primal_simplex.cpp index 440c46808d..b668b543ed 100644 --- a/src/util/lp/lp_primal_simplex.cpp +++ b/src/util/lp/lp_primal_simplex.cpp @@ -40,23 +40,6 @@ template void lp_primal_simplex::set_scaled_costs } } -template void lp_primal_simplex::stage_two() { - std::cout << "starting stage 2" << std::endl; - lean_assert(!m_core_solver->A_mult_x_is_off()); - int j = this->m_A->column_count() - 1; - unsigned core_solver_cols = this->number_of_core_structurals(); - - while (j >= core_solver_cols) { - this->m_costs[j--] = numeric_traits::zero(); - } - - set_scaled_costs(); - m_core_solver->set_status(lp_status::FEASIBLE); - this->m_second_stage_iterations = m_core_solver->solve(); - this->m_status = m_core_solver->get_status(); - // std::cout << "status is " << lp_status_to_string(this->m_status) << std::endl; -} - template column_info * lp_primal_simplex::get_or_create_column_info(unsigned column) { auto it = this->m_columns.find(column); return (it == this->m_columns.end())? ( this->m_columns[column] = new column_info) : it->second; @@ -240,7 +223,6 @@ template void lp_primal_simplex::fill_A_x_and_bas } template void lp_primal_simplex::solve_with_total_inf() { - std::cout << "starting solve_with_total_inf()" << std::endl; int total_vars = this->m_A->column_count() + this->row_count(); m_low_bounds.clear(); m_low_bounds.resize(total_vars, zero_of_type()); // low bounds are shifted ot zero diff --git a/src/util/lp/lp_primal_simplex.h b/src/util/lp/lp_primal_simplex.h index 5e801890de..5706c30120 100644 --- a/src/util/lp/lp_primal_simplex.h +++ b/src/util/lp/lp_primal_simplex.h @@ -30,13 +30,9 @@ private: void refactor(); void set_scaled_costs(); - - void stage_two(); public: lp_primal_simplex() {} - - column_info * get_or_create_column_info(unsigned column); void set_status(lp_status status) { diff --git a/src/util/lp/lp_settings.h b/src/util/lp/lp_settings.h index 1f3a25a997..02d265065e 100644 --- a/src/util/lp/lp_settings.h +++ b/src/util/lp/lp_settings.h @@ -150,7 +150,7 @@ struct lp_settings { // the method of lar solver to use bool row_feasibility = true; bool use_double_solver_for_lar = true; - int report_frequency = 1000; + int report_frequency = 10000000; unsigned column_norms_update_frequency = 1000; bool scale_with_ratio = true; double density_threshold = 0.7; // need to tune it up, todo @@ -205,8 +205,8 @@ X max_abs_in_vector(std::vector& t){ r = std::max(abs(v) , r); return r; } -inline void print_blanks(int n) { - while (n--) {std::cout << ' '; } +inline void print_blanks(int n, std::ostream & out) { + while (n--) {out << ' '; } } } diff --git a/src/util/lp/lp_solver.cpp b/src/util/lp/lp_solver.cpp index 83f0a491b4..620a207f74 100644 --- a/src/util/lp/lp_solver.cpp +++ b/src/util/lp/lp_solver.cpp @@ -96,35 +96,35 @@ template void lp_solver::scale() { } -template void lp_solver::print_rows_scale_stats() { - std::cout << "rows max" << std::endl; +template void lp_solver::print_rows_scale_stats(std::ostream & out) { + out << "rows max" << std::endl; for (unsigned i = 0; i < m_A->row_count(); i++) { - print_row_scale_stats(i); + print_row_scale_stats(i, out); } - std::cout << std::endl; + out << std::endl; } -template void lp_solver::print_columns_scale_stats() { - std::cout << "columns max" << std::endl; +template void lp_solver::print_columns_scale_stats(std::ostream & out) { + out << "columns max" << std::endl; for (unsigned i = 0; i < m_A->column_count(); i++) { - print_column_scale_stats(i); + print_column_scale_stats(i, out); } - std::cout << std::endl; + out << std::endl; } -template void lp_solver::print_row_scale_stats(unsigned i) { - std::cout << "(" << std::min(m_A->get_min_abs_in_row(i), abs(m_b[i])) << " "; - std::cout << std::max(m_A->get_max_abs_in_row(i), abs(m_b[i])) << ")"; +template void lp_solver::print_row_scale_stats(unsigned i, std::ostream & out) { + out << "(" << std::min(m_A->get_min_abs_in_row(i), abs(m_b[i])) << " "; + out << std::max(m_A->get_max_abs_in_row(i), abs(m_b[i])) << ")"; } -template void lp_solver::print_column_scale_stats(unsigned j) { - std::cout << "(" << m_A->get_min_abs_in_row(j) << " "; - std::cout << m_A->get_max_abs_in_column(j) << ")"; +template void lp_solver::print_column_scale_stats(unsigned j, std::ostream & out) { + out << "(" << m_A->get_min_abs_in_row(j) << " "; + out << m_A->get_max_abs_in_column(j) << ")"; } -template void lp_solver::print_scale_stats() { - print_rows_scale_stats(); - print_columns_scale_stats(); +template void lp_solver::print_scale_stats(std::ostream & out) { + print_rows_scale_stats(out); + print_columns_scale_stats(out); } template void lp_solver::get_max_abs_in_row(std::unordered_map & row_map) { diff --git a/src/util/lp/lp_solver.h b/src/util/lp/lp_solver.h index b2aca9c587..bf8a6c2e5b 100644 --- a/src/util/lp/lp_solver.h +++ b/src/util/lp/lp_solver.h @@ -143,15 +143,15 @@ protected: void scale(); - void print_rows_scale_stats(); + void print_rows_scale_stats(std::ostream & out); - void print_columns_scale_stats(); + void print_columns_scale_stats(std::ostream & out); - void print_row_scale_stats(unsigned i); + void print_row_scale_stats(unsigned i, std::ostream & out); - void print_column_scale_stats(unsigned j); + void print_column_scale_stats(unsigned j, std::ostream & out); - void print_scale_stats(); + void print_scale_stats(std::ostream & out); void get_max_abs_in_row(std::unordered_map & row_map); diff --git a/src/util/lp/lu.cpp b/src/util/lp/lu.cpp index b005957e4f..ea58c323d3 100644 --- a/src/util/lp/lu.cpp +++ b/src/util/lp/lu.cpp @@ -9,7 +9,7 @@ namespace lean { #ifdef LEAN_DEBUG template // print the nr x nc submatrix at the top left corner -void print_submatrix(sparse_matrix & m, unsigned mr, unsigned nc) { +void print_submatrix(sparse_matrix & m, unsigned mr, unsigned nc, std::ostream & out) { std::vector> A; std::vector widths; for (unsigned i = 0; i < m.row_count() && i < mr ; i++) { @@ -23,11 +23,11 @@ void print_submatrix(sparse_matrix & m, unsigned mr, unsigned nc) { widths.push_back(get_width_of_column(j, A)); } - print_matrix_with_widths(A, widths); + print_matrix_with_widths(A, widths, out); } template -void print_matrix(static_matrix &m) { +void print_matrix(static_matrix &m, std::ostream & out) { std::vector> A; std::vector widths; std::set> domain = m.get_domain(); @@ -42,11 +42,11 @@ void print_matrix(static_matrix &m) { widths.push_back(get_width_of_column(j, A)); } - print_matrix_with_widths(A, widths); + print_matrix_with_widths(A, widths, out); } template -void print_matrix(sparse_matrix& m) { +void print_matrix(sparse_matrix& m, std::ostream & out) { std::vector> A; std::vector widths; for (unsigned i = 0; i < m.row_count(); i++) { @@ -60,7 +60,7 @@ void print_matrix(sparse_matrix& m) { widths.push_back(get_width_of_column(j, A)); } - print_matrix_with_widths(A, widths); + print_matrix_with_widths(A, widths, out); } #endif @@ -177,15 +177,9 @@ void lu::solve_By_when_y_is_ready(std::vector & y) { } } } + template -void lu::print_basis(std::ofstream & f) { - f << "basis_start" << std::endl; - for (unsigned j : m_basis) - f << j << std::endl; - f << "basis_end" << std::endl; -} -template -void lu::print_matrix_compact(std::ofstream & f) { +void lu::print_matrix_compact(std::ostream & f) { f << "matrix_start" << std::endl; f << "nrows " << m_A.row_count() << std::endl; f << "ncolumns " << m_A.column_count() << std::endl; @@ -371,29 +365,27 @@ eta_matrix * lu::get_eta_matrix_for_pivot(unsigned j, sparse_matrix< } template -void lu::print_basis() { - std::cout << "basis "; +void lu::print_basis(std::ostream & out) { + out << "basis "; for (unsigned i = 0; i < m_dim; i++) { - std::cout << m_basis[i] << " "; + out << m_basis[i] << " "; } - std::cout << std::endl; + out << std::endl; } template -void lu::print_basis_heading() { - print_basis(); +void lu::print_basis_heading(std::ostream & out) { + print_basis(out); for (unsigned i = 0; i < m_A.column_count(); i++) { - std::cout << m_basis_heading[i] << ","; + out << m_basis_heading[i] << ","; } - std::cout << std::endl; + out << std::endl; } // see page 407 of Chvatal template unsigned lu::transform_U_to_V_by_replacing_column(unsigned leaving, indexed_vector & w) { int leaving_column = m_basis_heading[leaving]; - // std::cout << "leaving_column = " << leaving_column << std::endl; unsigned column_to_replace = m_R.apply_reverse(leaving_column); - // std::cout << "leaving_column modified = " << column_to_replace << std::endl; m_U.replace_column(column_to_replace, w, m_settings); return column_to_replace; } @@ -427,7 +419,6 @@ void lu::check_apply_lp_lists_to_w(T * w) { } } -// provide some access operators for testing #endif template void lu::process_column(int j) { @@ -557,7 +548,6 @@ void lu::create_initial_factorization(){ return; } j++; - // std::cout << "switching to dense factoring for " << j << endl; m_dense_LU = new square_dense_submatrix(&m_U, j); for (; j < m_dim; j++) { pivot_in_dense_mode(j); @@ -655,9 +645,8 @@ row_eta_matrix *lu::get_row_eta_matrix_and_set_row_vector(unsigned r !is_zero(pivot_elem_for_checking) && #endif !m_settings.abs_val_is_smaller_than_pivot_tolerance((m_row_eta_work_vector[lowest_row_of_the_bump] - pivot_elem_for_checking) / denom)) { - // std::cout << "m_row_eta_work_vector[" << lowest_row_of_the_bump << "] = " << T_to_string(m_row_eta_work_vector[lowest_row_of_the_bump]) << ", but pivot = " << T_to_string(pivot_elem_for_checking) << endl; set_status(LU_status::Degenerated); - // std::cout << "diagonal element is off" << endl; + std::cout << "diagonal element is off" << std::endl; return nullptr; } #ifdef LEAN_DEBUG diff --git a/src/util/lp/lu.h b/src/util/lp/lu.h index c235947d77..2876503e54 100644 --- a/src/util/lp/lu.h +++ b/src/util/lp/lu.h @@ -28,10 +28,10 @@ template // print the nr x nc submatrix at the top left void print_submatrix(sparse_matrix & m, unsigned mr, unsigned nc); template -void print_matrix(static_matrix &m); +void print_matrix(static_matrix &m, std::ostream & out); template -void print_matrix(sparse_matrix& m); +void print_matrix(sparse_matrix& m, std::ostream & out); #endif template @@ -133,8 +133,8 @@ public: void solve_By_when_y_is_ready(std::vector & y); void print_indexed_vector(indexed_vector & w, std::ofstream & f); - void print_basis(std::ofstream & f); - void print_matrix_compact(std::ofstream & f); + void print_basis(std::ostream & f); + void print_matrix_compact(std::ostream & f); void print(indexed_vector & w); void solve_Bd(unsigned a_column, std::vector & d, indexed_vector & w); @@ -185,9 +185,7 @@ public: // we're processing the column j now eta_matrix * get_eta_matrix_for_pivot(unsigned j, sparse_matrix& copy_of_U); - void print_basis(); - - void print_basis_heading(); + void print_basis_heading(std::ostream & out); // see page 407 of Chvatal unsigned transform_U_to_V_by_replacing_column(unsigned leaving, indexed_vector & w); diff --git a/src/util/lp/lu_instances.cpp b/src/util/lp/lu_instances.cpp index 7b76005d92..840fd11a5c 100644 --- a/src/util/lp/lu_instances.cpp +++ b/src/util/lp/lu_instances.cpp @@ -29,9 +29,9 @@ template void lean::init_factorization(lean::lu* template void lean::init_factorization(lean::lu*&, lean::static_matrix&, std::vector >&, std::vector >&, lean::lp_settings&, std::vector >&); template void lean::init_factorization >(lean::lu >*&, lean::static_matrix >&, std::vector >&, std::vector >&, lean::lp_settings&, std::vector >&); #ifdef LEAN_DEBUG -template void lean::print_matrix(lean::sparse_matrix&); -template void lean::print_matrix(lean::sparse_matrix&); -template void lean::print_matrix(lean::static_matrix&); +template void lean::print_matrix(lean::sparse_matrix&, std::ostream & out); +template void lean::print_matrix(lean::sparse_matrix&, std::ostream & out); +template void lean::print_matrix(lean::static_matrix&, std::ostream & out); template bool lean::lu::is_correct(); template lean::dense_matrix lean::get_B(lean::lu&); #endif diff --git a/src/util/lp/matrix.cpp b/src/util/lp/matrix.cpp index 3656b71032..d75d2d23c9 100644 --- a/src/util/lp/matrix.cpp +++ b/src/util/lp/matrix.cpp @@ -64,31 +64,31 @@ unsigned get_width_of_column(unsigned j, std::vector> & return r; } -void print_matrix_with_widths(std::vector> & A, std::vector & ws) { +void print_matrix_with_widths(std::vector> & A, std::vector & ws, std::ostream & out) { for (unsigned i = 0; i < A.size(); i++) { for (unsigned j = 0; j < A[i].size(); j++) { - print_blanks(ws[j] - A[i][j].size()); - std::cout << A[i][j] << " "; + print_blanks(ws[j] - A[i][j].size(), out); + out << A[i][j] << " "; } - std::cout << std::endl; + out << std::endl; } } -void print_string_matrix(std::vector> & A) { +void print_string_matrix(std::vector> & A, std::ostream & out) { std::vector widths; for (unsigned j = 0; j < A[0].size(); j++) { widths.push_back(get_width_of_column(j, A)); } - print_matrix_with_widths(A, widths); - std::cout << std::endl; + print_matrix_with_widths(A, widths, out); + out << std::endl; } template -void print_matrix(matrix const & m) { +void print_matrix(matrix const & m, std::ostream & out) { if (&m == nullptr) { - std::cout << "null" << std::endl; + out << "null" << std::endl; return; } std::vector> A(m.row_count()); @@ -98,7 +98,7 @@ void print_matrix(matrix const & m) { } } - print_string_matrix(A); + print_string_matrix(A, out); } } diff --git a/src/util/lp/matrix.h b/src/util/lp/matrix.h index 6d806352ba..cd1a6410ad 100644 --- a/src/util/lp/matrix.h +++ b/src/util/lp/matrix.h @@ -36,13 +36,13 @@ void apply_to_vector(matrix & m, T * w); - unsigned get_width_of_column(unsigned j, std::vector> & A); - void print_matrix_with_widths(std::vector> & A, std::vector & ws); - void print_string_matrix(std::vector> & A); +unsigned get_width_of_column(unsigned j, std::vector> & A); +void print_matrix_with_widths(std::vector> & A, std::vector & ws, std::ostream & out); +void print_string_matrix(std::vector> & A); template -void print_matrix(matrix const & m); +void print_matrix(matrix const & m, std::ostream & out); } #endif diff --git a/src/util/lp/matrix_instances.cpp b/src/util/lp/matrix_instances.cpp index 3929178935..db1f667e96 100644 --- a/src/util/lp/matrix_instances.cpp +++ b/src/util/lp/matrix_instances.cpp @@ -6,6 +6,6 @@ */ #ifdef LEAN_DEBUG #include "util/lp/matrix.cpp" -template void lean::print_matrix(lean::matrix const&); +template void lean::print_matrix(lean::matrix const&, std::ostream & out); template bool lean::matrix::is_equal(lean::matrix const&); #endif diff --git a/src/util/lp/permutation_matrix.cpp b/src/util/lp/permutation_matrix.cpp index 1efb57bb6c..58b421ce5c 100644 --- a/src/util/lp/permutation_matrix.cpp +++ b/src/util/lp/permutation_matrix.cpp @@ -28,17 +28,17 @@ template void permutation_matrix::init(unsigned l } #ifdef LEAN_DEBUG -template void permutation_matrix::print() const { - std::cout << "["; +template void permutation_matrix::print(std::ostream & out) const { + out << "["; for (unsigned i = 0; i < m_length; i++) { - std::cout << m_permutation[i]; + out << m_permutation[i]; if (i < m_length - 1) { - std::cout << ","; + out << ","; } else { - std::cout << "]"; + out << "]"; } } - std::cout << std::endl; + out << std::endl; } #endif diff --git a/src/util/lp/permutation_matrix.h b/src/util/lp/permutation_matrix.h index 2f3931c5f4..ebbdff07b6 100644 --- a/src/util/lp/permutation_matrix.h +++ b/src/util/lp/permutation_matrix.h @@ -63,7 +63,7 @@ namespace lean { permutation_matrix get_inverse() const { return permutation_matrix(m_length, m_rev); } - void print() const; + void print(std::ostream & out) const; #endif ref operator[](unsigned i) { return ref(*this, i); } diff --git a/src/util/lp/row_eta_matrix.h b/src/util/lp/row_eta_matrix.h index 7f41febe29..ec6d819e7d 100644 --- a/src/util/lp/row_eta_matrix.h +++ b/src/util/lp/row_eta_matrix.h @@ -46,8 +46,8 @@ public: lean_assert(dim > 0); } - void print() { - print_matrix(*this); + void print(std::ostream & out) { + print_matrix(*this, out); } const T & get_diagonal_element() const { diff --git a/src/util/lp/sparse_matrix.cpp b/src/util/lp/sparse_matrix.cpp index 16252613d5..fdee736d58 100644 --- a/src/util/lp/sparse_matrix.cpp +++ b/src/util/lp/sparse_matrix.cpp @@ -858,10 +858,10 @@ bool sparse_matrix::really_best_pivot(unsigned i, unsigned j, T const & c_ return true; } template -void sparse_matrix::print_active_matrix(unsigned k) { - std::cout << "active matrix for k = " << k << std::endl; +void sparse_matrix::print_active_matrix(unsigned k, std::ostream & out) { + out << "active matrix for k = " << k << std::endl; if (k >= dimension()) { - std::cout << "empty" << std::endl; + out << "empty" << std::endl; return; } unsigned dim = dimension() - k; @@ -879,7 +879,7 @@ void sparse_matrix::print_active_matrix(unsigned k) { b.set_elem(row_ex - k, i -k, v); } } - print_matrix(b); + print_matrix(b, out); } template diff --git a/src/util/lp/sparse_matrix.h b/src/util/lp/sparse_matrix.h index bb54ea8c22..2e1511c9bf 100644 --- a/src/util/lp/sparse_matrix.h +++ b/src/util/lp/sparse_matrix.h @@ -330,7 +330,7 @@ public: #ifdef LEAN_DEBUG bool can_improve_score_for_row(unsigned row, unsigned score, T const & c_partial_pivoting, unsigned k); bool really_best_pivot(unsigned i, unsigned j, T const & c_partial_pivoting, unsigned k); - void print_active_matrix(unsigned k); + void print_active_matrix(unsigned k, std::ostream & out); #endif bool pivot_queue_is_correct_for_row(unsigned i, unsigned k);