mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-11 21:50:52 +00:00
Code Activity

make lar_solver pretty printer const on the solver

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-04-14 15:37:46 -07:00
parent 5208b64a6b
commit 95cb828324
7 changed files with 32 additions and 22 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/math/lp/core_solver_pretty_printer.cpp
View file

@ -19,12 +19,12 @@ Revision History:
--*/ --*/
#include "math/lp/numeric_pair.h" #include "math/lp/numeric_pair.h"
#include "math/lp/core_solver_pretty_printer_def.h" #include "math/lp/core_solver_pretty_printer_def.h"
template lp::core_solver_pretty_printer<double, double>::core_solver_pretty_printer(lp::lp_core_solver_base<double, double> &, std::ostream & out); template lp::core_solver_pretty_printer<double, double>::core_solver_pretty_printer(const lp::lp_core_solver_base<double, double> &, std::ostream & out);
template void lp::core_solver_pretty_printer<double, double>::print(); template void lp::core_solver_pretty_printer<double, double>::print();
template lp::core_solver_pretty_printer<double, double>::~core_solver_pretty_printer(); template lp::core_solver_pretty_printer<double, double>::~core_solver_pretty_printer();
template lp::core_solver_pretty_printer<lp::mpq, lp::mpq>::core_solver_pretty_printer(lp::lp_core_solver_base<lp::mpq, lp::mpq> &, std::ostream & out); template lp::core_solver_pretty_printer<lp::mpq, lp::mpq>::core_solver_pretty_printer(const lp::lp_core_solver_base<lp::mpq, lp::mpq> &, std::ostream & out);
template void lp::core_solver_pretty_printer<lp::mpq, lp::mpq>::print(); template void lp::core_solver_pretty_printer<lp::mpq, lp::mpq>::print();
template lp::core_solver_pretty_printer<lp::mpq, lp::mpq>::~core_solver_pretty_printer(); template lp::core_solver_pretty_printer<lp::mpq, lp::mpq>::~core_solver_pretty_printer();
template lp::core_solver_pretty_printer<lp::mpq, lp::numeric_pair<lp::mpq> >::core_solver_pretty_printer(lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> > &, std::ostream & out); template lp::core_solver_pretty_printer<lp::mpq, lp::numeric_pair<lp::mpq> >::core_solver_pretty_printer(const lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> > &, std::ostream & out);
template lp::core_solver_pretty_printer<lp::mpq, lp::numeric_pair<lp::mpq> >::~core_solver_pretty_printer(); template lp::core_solver_pretty_printer<lp::mpq, lp::numeric_pair<lp::mpq> >::~core_solver_pretty_printer();
template void lp::core_solver_pretty_printer<lp::mpq, lp::numeric_pair<lp::mpq> >::print(); template void lp::core_solver_pretty_printer<lp::mpq, lp::numeric_pair<lp::mpq> >::print();

4
src/math/lp/core_solver_pretty_printer.h
View file

@ -32,7 +32,7 @@ template <typename T, typename X>
class core_solver_pretty_printer { class core_solver_pretty_printer {
std::ostream & m_out; std::ostream & m_out;
typedef std::string string; typedef std::string string;
lp_core_solver_base<T, X> & m_core_solver; const lp_core_solver_base<T, X> & m_core_solver;
vector<unsigned> m_column_widths; vector<unsigned> m_column_widths;
vector<vector<string>> m_A; vector<vector<string>> m_A;
vector<vector<string>> m_signs; vector<vector<string>> m_signs;
@ -62,7 +62,7 @@ class core_solver_pretty_printer {
vector<T> m_exact_column_norms; vector<T> m_exact_column_norms;
public: public:
core_solver_pretty_printer(lp_core_solver_base<T, X > & core_solver, std::ostream & out); core_solver_pretty_printer(const lp_core_solver_base<T, X > & core_solver, std::ostream & out);
void init_costs(); void init_costs();

10
src/math/lp/core_solver_pretty_printer_def.h
View file

@ -28,7 +28,7 @@ namespace lp {
template <typename T, typename X> template <typename T, typename X>
core_solver_pretty_printer<T, X>::core_solver_pretty_printer(lp_core_solver_base<T, X > & core_solver, std::ostream & out): core_solver_pretty_printer<T, X>::core_solver_pretty_printer(const lp_core_solver_base<T, X > & core_solver, std::ostream & out):
m_out(out), m_out(out),
m_core_solver(core_solver), m_core_solver(core_solver),
m_A(core_solver.m_A.row_count(), vector<string>(core_solver.m_A.column_count(), "")), m_A(core_solver.m_A.row_count(), vector<string>(core_solver.m_A.column_count(), "")),
@ -76,8 +76,6 @@ template <typename T, typename X> void core_solver_pretty_printer<T, X>::init_co
} }
template <typename T, typename X> core_solver_pretty_printer<T, X>::~core_solver_pretty_printer() { template <typename T, typename X> core_solver_pretty_printer<T, X>::~core_solver_pretty_printer() {
m_core_solver.m_w = m_w_buff;
m_core_solver.m_ed = m_ed_buff;
} }
template <typename T, typename X> void core_solver_pretty_printer<T, X>::init_rs_width() { template <typename T, typename X> void core_solver_pretty_printer<T, X>::init_rs_width() {
m_rs_width = static_cast<unsigned>(T_to_string(m_core_solver.get_cost()).size()); m_rs_width = static_cast<unsigned>(T_to_string(m_core_solver.get_cost()).size());
@ -119,16 +117,16 @@ template <typename T, typename X> void core_solver_pretty_printer<T, X>::init_m_
} }
} else { } else {
for (unsigned column = 0; column < ncols(); column++) { 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); string name = m_core_solver.column_name(column);
for (unsigned row = 0; row < nrows(); row ++) { for (unsigned row = 0; row < nrows(); row ++) {
set_coeff( set_coeff(
m_A[row], m_A[row],
m_signs[row], m_signs[row],
column, column,
m_core_solver.m_ed[row], m_ed_buff[row],
name); 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()) if (!m_core_solver.use_tableau())
m_exact_column_norms.push_back(current_column_norm() + T(1)); // a conversion missing 1 -> T m_exact_column_norms.push_back(current_column_norm() + T(1)); // a conversion missing 1 -> T

6
src/math/lp/hnf_cutter.h
View file

@ -81,7 +81,11 @@ private:
#endif #endif
void shrink_explanation(const svector<unsigned>& basis_rows); void shrink_explanation(const svector<unsigned>& basis_rows);
bool overflow() const; bool overflow() const;
lia_move create_cut(lar_term& t, mpq& k, explanation* ex, bool & upper, const vector<mpq> & x0); lia_move create_cut(lar_term& t, mpq& k, explanation* ex, bool & upper
#ifdef Z3DEBUG
, const vector<mpq> & x0
#endif
);
svector<unsigned> vars() const; svector<unsigned> vars() const;
}; };
} }

9
src/math/lp/lp_core_solver_base.cpp
View file

@ -53,8 +53,9 @@ template void lp::lp_core_solver_base<double, double>::snap_xN_to_bounds_and_fre
template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::snap_xN_to_bounds_and_free_columns_to_zeroes(); template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::snap_xN_to_bounds_and_free_columns_to_zeroes();
template void lp::lp_core_solver_base<double, double>::solve_Ax_eq_b(); template void lp::lp_core_solver_base<double, double>::solve_Ax_eq_b();
template void lp::lp_core_solver_base<double, double>::solve_Bd(unsigned int); template void lp::lp_core_solver_base<double, double>::solve_Bd(unsigned int);
template void lp::lp_core_solver_base<double, double>::solve_Bd(unsigned int, lp::indexed_vector<double>&, lp::indexed_vector<double>&) const;
template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq>>::solve_Bd(unsigned int, indexed_vector<lp::mpq>&); template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq>>::solve_Bd(unsigned int, indexed_vector<lp::mpq>&);
template void lp::lp_core_solver_base<double, double>::solve_yB(vector<double >&); template void lp::lp_core_solver_base<double, double>::solve_yB(vector<double >&) const;
template bool lp::lp_core_solver_base<double, double>::update_basis_and_x(int, int, double const&); template bool lp::lp_core_solver_base<double, double>::update_basis_and_x(int, int, double const&);
template void lp::lp_core_solver_base<double, double>::add_delta_to_entering(unsigned int, const double&); template void lp::lp_core_solver_base<double, double>::add_delta_to_entering(unsigned int, const double&);
template bool lp::lp_core_solver_base<lp::mpq, lp::mpq>::A_mult_x_is_off() const; template bool lp::lp_core_solver_base<lp::mpq, lp::mpq>::A_mult_x_is_off() const;
@ -71,7 +72,7 @@ template void lp::lp_core_solver_base<lp::mpq, lp::mpq>::restore_x(unsigned int,
template void lp::lp_core_solver_base<lp::mpq, lp::mpq>::set_non_basic_x_to_correct_bounds(); template void lp::lp_core_solver_base<lp::mpq, lp::mpq>::set_non_basic_x_to_correct_bounds();
template void lp::lp_core_solver_base<lp::mpq, lp::mpq>::solve_Ax_eq_b(); template void lp::lp_core_solver_base<lp::mpq, lp::mpq>::solve_Ax_eq_b();
template void lp::lp_core_solver_base<lp::mpq, lp::mpq>::solve_Bd(unsigned int); template void lp::lp_core_solver_base<lp::mpq, lp::mpq>::solve_Bd(unsigned int);
template void lp::lp_core_solver_base<lp::mpq, lp::mpq>::solve_yB(vector<lp::mpq>&); template void lp::lp_core_solver_base<lp::mpq, lp::mpq>::solve_yB(vector<lp::mpq>&) const;
template bool lp::lp_core_solver_base<lp::mpq, lp::mpq>::update_basis_and_x(int, int, lp::mpq const&); template bool lp::lp_core_solver_base<lp::mpq, lp::mpq>::update_basis_and_x(int, int, lp::mpq const&);
template void lp::lp_core_solver_base<lp::mpq, lp::mpq>::add_delta_to_entering(unsigned int, const lp::mpq&); template void lp::lp_core_solver_base<lp::mpq, lp::mpq>::add_delta_to_entering(unsigned int, const lp::mpq&);
template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::calculate_pivot_row_of_B_1(unsigned int); template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::calculate_pivot_row_of_B_1(unsigned int);
@ -113,7 +114,7 @@ template std::string lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq>
template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::pretty_print(std::ostream & out); template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::pretty_print(std::ostream & out);
template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::restore_state(lp::mpq*, lp::mpq*); template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::restore_state(lp::mpq*, lp::mpq*);
template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::save_state(lp::mpq*, lp::mpq*); template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::save_state(lp::mpq*, lp::mpq*);
template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::solve_yB(vector<lp::mpq>&); template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::solve_yB(vector<lp::mpq>&) const;
template void lp::lp_core_solver_base<double, double>::init_lu(); template void lp::lp_core_solver_base<double, double>::init_lu();
template void lp::lp_core_solver_base<lp::mpq, lp::mpq>::init_lu(); template void lp::lp_core_solver_base<lp::mpq, lp::mpq>::init_lu();
template int lp::lp_core_solver_base<double, double>::pivots_in_column_and_row_are_different(int, int) const; template int lp::lp_core_solver_base<double, double>::pivots_in_column_and_row_are_different(int, int) const;
@ -147,3 +148,5 @@ template bool lp::lp_core_solver_base<lp::mpq, lp::mpq >::infeasibility_costs_ar
template bool lp::lp_core_solver_base<double, double >::infeasibility_costs_are_correct() const; template bool lp::lp_core_solver_base<double, double >::infeasibility_costs_are_correct() const;
template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::calculate_pivot_row(unsigned int); template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::calculate_pivot_row(unsigned int);
template bool lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::remove_from_basis(unsigned int); template bool lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::remove_from_basis(unsigned int);
template void lp::lp_core_solver_base<rational, rational>::solve_Bd(unsigned int, lp::indexed_vector<rational>&, lp::indexed_vector<rational>&) const;
template void lp::lp_core_solver_base<rational, lp::numeric_pair<rational> >::solve_Bd(unsigned int, lp::indexed_vector<rational>&, lp::indexed_vector<rational>&) const;

10
src/math/lp/lp_core_solver_base.h
View file

@ -143,11 +143,13 @@ public:
return m_status; return m_status;
} }
void fill_cb(T * y); void fill_cb(T * y) const;
void fill_cb(vector<T> & y); void fill_cb(vector<T> & y) const;
void solve_yB(vector<T> & y); void solve_yB(vector<T> & y) const;
void solve_Bd(unsigned entering, indexed_vector<T> & d_buff, indexed_vector<T>& w_buff) const;
void solve_Bd(unsigned entering); void solve_Bd(unsigned entering);
@ -159,7 +161,7 @@ public:
void restore_state(T * w_buffer, T * d_buffer); void restore_state(T * w_buffer, T * d_buffer);
X get_cost() { X get_cost() const {
return dot_product(m_costs, m_x); return dot_product(m_costs, m_x);
} }

9
src/math/lp/lp_core_solver_base_def.h
View file

@ -112,7 +112,7 @@ pivot_to_reduced_costs_tableau(unsigned i, unsigned j) {
template <typename T, typename X> void lp_core_solver_base<T, X>:: template <typename T, typename X> void lp_core_solver_base<T, X>::
fill_cb(T * y){ fill_cb(T * y) const {
for (unsigned i = 0; i < m_m(); i++) { for (unsigned i = 0; i < m_m(); i++) {
y[i] = m_costs[m_basis[i]]; y[i] = m_costs[m_basis[i]];
} }
@ -120,14 +120,14 @@ fill_cb(T * y){
template <typename T, typename X> void lp_core_solver_base<T, X>:: template <typename T, typename X> void lp_core_solver_base<T, X>::
fill_cb(vector<T> & y){ fill_cb(vector<T> & y) const {
for (unsigned i = 0; i < m_m(); i++) { for (unsigned i = 0; i < m_m(); i++) {
y[i] = m_costs[m_basis[i]]; y[i] = m_costs[m_basis[i]];
} }
} }
template <typename T, typename X> void lp_core_solver_base<T, X>:: template <typename T, typename X> void lp_core_solver_base<T, X>::
solve_yB(vector<T> & y) { solve_yB(vector<T> & y) const {
fill_cb(y); // now y = cB, that is the projection of costs to basis fill_cb(y); // now y = cB, that is the projection of costs to basis
m_factorization->solve_yB_with_error_check(y, m_basis); m_factorization->solve_yB_with_error_check(y, m_basis);
} }
@ -149,6 +149,9 @@ template <typename T, typename X> void lp_core_solver_base<T, X>::solve_Bd(unsig
m_factorization->solve_Bd_faster(entering, column); m_factorization->solve_Bd_faster(entering, column);
} }
template <typename T, typename X> void lp_core_solver_base<T, X>::solve_Bd(unsigned , indexed_vector<T>& , indexed_vector<T> &) const {
NOT_IMPLEMENTED_YET();
}
template <typename T, typename X> void lp_core_solver_base<T, X>:: template <typename T, typename X> void lp_core_solver_base<T, X>::
solve_Bd(unsigned entering) { solve_Bd(unsigned entering) {