From 95cb82832474de4cd9b3c92601798a7c6027186d Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 14 Apr 2020 15:37:46 -0700 Subject: [PATCH] make lar_solver pretty printer const on the solver Signed-off-by: Lev Nachmanson --- src/math/lp/core_solver_pretty_printer.cpp | 6 +++--- src/math/lp/core_solver_pretty_printer.h | 4 ++-- src/math/lp/core_solver_pretty_printer_def.h | 10 ++++------ src/math/lp/hnf_cutter.h | 6 +++++- src/math/lp/lp_core_solver_base.cpp | 9 ++++++--- src/math/lp/lp_core_solver_base.h | 10 ++++++---- src/math/lp/lp_core_solver_base_def.h | 9 ++++++--- 7 files changed, 32 insertions(+), 22 deletions(-) diff --git a/src/math/lp/core_solver_pretty_printer.cpp b/src/math/lp/core_solver_pretty_printer.cpp index cd9c1a68b..74d2f6048 100644 --- a/src/math/lp/core_solver_pretty_printer.cpp +++ b/src/math/lp/core_solver_pretty_printer.cpp @@ -19,12 +19,12 @@ Revision History: --*/ #include "math/lp/numeric_pair.h" #include "math/lp/core_solver_pretty_printer_def.h" -template lp::core_solver_pretty_printer::core_solver_pretty_printer(lp::lp_core_solver_base &, std::ostream & out); +template lp::core_solver_pretty_printer::core_solver_pretty_printer(const lp::lp_core_solver_base &, std::ostream & out); template void lp::core_solver_pretty_printer::print(); template lp::core_solver_pretty_printer::~core_solver_pretty_printer(); -template lp::core_solver_pretty_printer::core_solver_pretty_printer(lp::lp_core_solver_base &, std::ostream & out); +template lp::core_solver_pretty_printer::core_solver_pretty_printer(const lp::lp_core_solver_base &, std::ostream & out); template void lp::core_solver_pretty_printer::print(); template lp::core_solver_pretty_printer::~core_solver_pretty_printer(); -template lp::core_solver_pretty_printer >::core_solver_pretty_printer(lp::lp_core_solver_base > &, std::ostream & out); +template lp::core_solver_pretty_printer >::core_solver_pretty_printer(const lp::lp_core_solver_base > &, std::ostream & out); template lp::core_solver_pretty_printer >::~core_solver_pretty_printer(); template void lp::core_solver_pretty_printer >::print(); diff --git a/src/math/lp/core_solver_pretty_printer.h b/src/math/lp/core_solver_pretty_printer.h index 61540c155..75e3c5ca8 100644 --- a/src/math/lp/core_solver_pretty_printer.h +++ b/src/math/lp/core_solver_pretty_printer.h @@ -32,7 +32,7 @@ template class core_solver_pretty_printer { std::ostream & m_out; typedef std::string string; - lp_core_solver_base & m_core_solver; + const lp_core_solver_base & m_core_solver; vector m_column_widths; vector> m_A; vector> m_signs; @@ -62,7 +62,7 @@ class core_solver_pretty_printer { vector m_exact_column_norms; public: - core_solver_pretty_printer(lp_core_solver_base & core_solver, std::ostream & out); + core_solver_pretty_printer(const lp_core_solver_base & core_solver, std::ostream & out); void init_costs(); diff --git a/src/math/lp/core_solver_pretty_printer_def.h b/src/math/lp/core_solver_pretty_printer_def.h index 866e3d828..f4c0b8d76 100644 --- a/src/math/lp/core_solver_pretty_printer_def.h +++ b/src/math/lp/core_solver_pretty_printer_def.h @@ -28,7 +28,7 @@ namespace lp { template -core_solver_pretty_printer::core_solver_pretty_printer(lp_core_solver_base & core_solver, std::ostream & out): +core_solver_pretty_printer::core_solver_pretty_printer(const lp_core_solver_base & core_solver, std::ostream & out): m_out(out), m_core_solver(core_solver), m_A(core_solver.m_A.row_count(), vector(core_solver.m_A.column_count(), "")), @@ -76,8 +76,6 @@ template void core_solver_pretty_printer::init_co } template core_solver_pretty_printer::~core_solver_pretty_printer() { - m_core_solver.m_w = m_w_buff; - m_core_solver.m_ed = m_ed_buff; } template void core_solver_pretty_printer::init_rs_width() { m_rs_width = static_cast(T_to_string(m_core_solver.get_cost()).size()); @@ -119,16 +117,16 @@ template void core_solver_pretty_printer::init_m_ } } else { for (unsigned column = 0; column < ncols(); column++) { - m_core_solver.solve_Bd(column); // puts the result into m_core_solver.m_ed + m_core_solver.solve_Bd(column, m_ed_buff, m_w_buff); // puts the result into m_core_solver.m_ed string name = m_core_solver.column_name(column); for (unsigned row = 0; row < nrows(); row ++) { set_coeff( m_A[row], m_signs[row], column, - m_core_solver.m_ed[row], + m_ed_buff[row], name); - m_rs[row] += m_core_solver.m_ed[row] * m_core_solver.m_x[column]; + m_rs[row] += m_ed_buff[row] * m_core_solver.m_x[column]; } if (!m_core_solver.use_tableau()) m_exact_column_norms.push_back(current_column_norm() + T(1)); // a conversion missing 1 -> T diff --git a/src/math/lp/hnf_cutter.h b/src/math/lp/hnf_cutter.h index dd0f7b093..0dd460774 100644 --- a/src/math/lp/hnf_cutter.h +++ b/src/math/lp/hnf_cutter.h @@ -81,7 +81,11 @@ private: #endif void shrink_explanation(const svector& basis_rows); bool overflow() const; - lia_move create_cut(lar_term& t, mpq& k, explanation* ex, bool & upper, const vector & x0); + lia_move create_cut(lar_term& t, mpq& k, explanation* ex, bool & upper +#ifdef Z3DEBUG + , const vector & x0 +#endif + ); svector vars() const; }; } diff --git a/src/math/lp/lp_core_solver_base.cpp b/src/math/lp/lp_core_solver_base.cpp index 6a711029e..1033fdf4f 100644 --- a/src/math/lp/lp_core_solver_base.cpp +++ b/src/math/lp/lp_core_solver_base.cpp @@ -53,8 +53,9 @@ template void lp::lp_core_solver_base::snap_xN_to_bounds_and_fre template void lp::lp_core_solver_base >::snap_xN_to_bounds_and_free_columns_to_zeroes(); template void lp::lp_core_solver_base::solve_Ax_eq_b(); template void lp::lp_core_solver_base::solve_Bd(unsigned int); +template void lp::lp_core_solver_base::solve_Bd(unsigned int, lp::indexed_vector&, lp::indexed_vector&) const; template void lp::lp_core_solver_base>::solve_Bd(unsigned int, indexed_vector&); -template void lp::lp_core_solver_base::solve_yB(vector&); +template void lp::lp_core_solver_base::solve_yB(vector&) const; template bool lp::lp_core_solver_base::update_basis_and_x(int, int, double const&); template void lp::lp_core_solver_base::add_delta_to_entering(unsigned int, const double&); template bool lp::lp_core_solver_base::A_mult_x_is_off() const; @@ -71,7 +72,7 @@ template void lp::lp_core_solver_base::restore_x(unsigned int, template void lp::lp_core_solver_base::set_non_basic_x_to_correct_bounds(); template void lp::lp_core_solver_base::solve_Ax_eq_b(); template void lp::lp_core_solver_base::solve_Bd(unsigned int); -template void lp::lp_core_solver_base::solve_yB(vector&); +template void lp::lp_core_solver_base::solve_yB(vector&) const; template bool lp::lp_core_solver_base::update_basis_and_x(int, int, lp::mpq const&); template void lp::lp_core_solver_base::add_delta_to_entering(unsigned int, const lp::mpq&); template void lp::lp_core_solver_base >::calculate_pivot_row_of_B_1(unsigned int); @@ -113,7 +114,7 @@ template std::string lp::lp_core_solver_base template void lp::lp_core_solver_base >::pretty_print(std::ostream & out); template void lp::lp_core_solver_base >::restore_state(lp::mpq*, lp::mpq*); template void lp::lp_core_solver_base >::save_state(lp::mpq*, lp::mpq*); -template void lp::lp_core_solver_base >::solve_yB(vector&); +template void lp::lp_core_solver_base >::solve_yB(vector&) const; template void lp::lp_core_solver_base::init_lu(); template void lp::lp_core_solver_base::init_lu(); template int lp::lp_core_solver_base::pivots_in_column_and_row_are_different(int, int) const; @@ -147,3 +148,5 @@ template bool lp::lp_core_solver_base::infeasibility_costs_ar template bool lp::lp_core_solver_base::infeasibility_costs_are_correct() const; template void lp::lp_core_solver_base >::calculate_pivot_row(unsigned int); template bool lp::lp_core_solver_base >::remove_from_basis(unsigned int); +template void lp::lp_core_solver_base::solve_Bd(unsigned int, lp::indexed_vector&, lp::indexed_vector&) const; +template void lp::lp_core_solver_base >::solve_Bd(unsigned int, lp::indexed_vector&, lp::indexed_vector&) const; diff --git a/src/math/lp/lp_core_solver_base.h b/src/math/lp/lp_core_solver_base.h index 06883bcd5..ddf2fd26c 100644 --- a/src/math/lp/lp_core_solver_base.h +++ b/src/math/lp/lp_core_solver_base.h @@ -143,11 +143,13 @@ public: return m_status; } - void fill_cb(T * y); + void fill_cb(T * y) const; - void fill_cb(vector & y); + void fill_cb(vector & y) const; - void solve_yB(vector & y); + void solve_yB(vector & y) const; + + void solve_Bd(unsigned entering, indexed_vector & d_buff, indexed_vector& w_buff) const; void solve_Bd(unsigned entering); @@ -159,7 +161,7 @@ public: void restore_state(T * w_buffer, T * d_buffer); - X get_cost() { + X get_cost() const { return dot_product(m_costs, m_x); } diff --git a/src/math/lp/lp_core_solver_base_def.h b/src/math/lp/lp_core_solver_base_def.h index 365dbc229..e8adb0d77 100644 --- a/src/math/lp/lp_core_solver_base_def.h +++ b/src/math/lp/lp_core_solver_base_def.h @@ -112,7 +112,7 @@ pivot_to_reduced_costs_tableau(unsigned i, unsigned j) { template void lp_core_solver_base:: -fill_cb(T * y){ +fill_cb(T * y) const { for (unsigned i = 0; i < m_m(); i++) { y[i] = m_costs[m_basis[i]]; } @@ -120,14 +120,14 @@ fill_cb(T * y){ template void lp_core_solver_base:: -fill_cb(vector & y){ +fill_cb(vector & y) const { for (unsigned i = 0; i < m_m(); i++) { y[i] = m_costs[m_basis[i]]; } } template void lp_core_solver_base:: -solve_yB(vector & y) { +solve_yB(vector & y) const { fill_cb(y); // now y = cB, that is the projection of costs to basis m_factorization->solve_yB_with_error_check(y, m_basis); } @@ -149,6 +149,9 @@ template void lp_core_solver_base::solve_Bd(unsig m_factorization->solve_Bd_faster(entering, column); } +template void lp_core_solver_base::solve_Bd(unsigned , indexed_vector& , indexed_vector &) const { + NOT_IMPLEMENTED_YET(); +} template void lp_core_solver_base:: solve_Bd(unsigned entering) {