michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

chore(lp): improve formatting

Browse source 
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
This commit is contained in:
Lev Nachmanson 2016-01-21 11:03:55 -08:00 committed by Leonardo de Moura
parent 28bf891b7f
commit e9cd621855
17 changed files with 1264 additions and 1263 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/util/lp/binary_heap_priority_queue.cpp
View file

@ -148,7 +148,7 @@ template <typename T> unsigned binary_heap_priority_queue<T>::dequeue_and_get_pr
return ret;
}
template <typename T> void binary_heap_priority_queue<T>::fix_heap_under(unsigned i) {
template <typename T> void binary_heap_priority_queue<T>::fix_heap_under(unsigned i) {
while (true) {
int smallest = i;
int l = i << 1;
@ -165,7 +165,7 @@ template <typename T> unsigned binary_heap_priority_queue<T>::dequeue_and_get_pr
}
}
template <typename T> void binary_heap_priority_queue<T>::put_the_last_at_the_top_and_fix_the_heap() {
template <typename T> void binary_heap_priority_queue<T>::put_the_last_at_the_top_and_fix_the_heap() {
if (m_heap_size > 1) {
put_at(1, m_heap[m_heap_size--]);
fix_heap_under(1);
@ -174,7 +174,7 @@ template <typename T> unsigned binary_heap_priority_queue<T>::dequeue_and_get_pr
}
}
/// return the first element of the queue and removes it from the queue
template <typename T> unsigned binary_heap_priority_queue<T>::dequeue() {
template <typename T> unsigned binary_heap_priority_queue<T>::dequeue() {
lean_assert(m_heap_size);
int ret = m_heap[1];
put_the_last_at_the_top_and_fix_the_heap();
@ -182,7 +182,7 @@ template <typename T> unsigned binary_heap_priority_queue<T>::dequeue_and_get_pr
return ret;
}
#ifdef LEAN_DEBUG
template <typename T> void binary_heap_priority_queue<T>::print() {
template <typename T> void binary_heap_priority_queue<T>::print() {
std::vector<int> index;
std::vector<T> prs;
while (size()) {

48
src/util/lp/core_solver_pretty_printer.cpp
View file

@ -30,7 +30,7 @@ core_solver_pretty_printer<T, X>::core_solver_pretty_printer(lp_core_solver_base
m_title_width = std::max(std::max(m_cost_title.size(), std::max(m_basis_heading_title.size(), m_x_title.size())), m_approx_norm_title.size());
}
template <typename T, typename X> void core_solver_pretty_printer<T, X>:: init_costs() {
template <typename T, typename X> void core_solver_pretty_printer<T, X>::init_costs() {
vector<T> local_y(m_core_solver.m_m);
m_core_solver.solve_yB(local_y);
for (unsigned i = 0; i < ncols(); i++) {
@ -41,12 +41,12 @@ core_solver_pretty_printer<T, X>::core_solver_pretty_printer(lp_core_solver_base
}
}
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.restore_state(m_w_buff, m_ed_buff);
delete [] m_w_buff;
delete [] 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 = T_to_string(m_core_solver.get_cost()).size();
for (unsigned i = 0; i < nrows(); i++) {
auto wt = T_to_string(m_rs[i]).size();
@ -56,14 +56,14 @@ core_solver_pretty_printer<T, X>::core_solver_pretty_printer(lp_core_solver_base
}
}
template <typename T, typename X> T core_solver_pretty_printer<T, X>:: current_column_norm() {
template <typename T, typename X> T core_solver_pretty_printer<T, X>::current_column_norm() {
T ret = zero_of_type<T>();
for (T & ed : m_core_solver.m_ed)
ret += ed * ed;
return ret;
}
template <typename T, typename X> void core_solver_pretty_printer<T, X>:: init_m_A_and_signs() {
template <typename T, typename X> void core_solver_pretty_printer<T, X>::init_m_A_and_signs() {
for (unsigned column = 0; column < ncols(); column++) {
m_core_solver.solve_Bd(column); // puts the result into m_core_solver.m_ed
string name = m_core_solver.column_name(column);
@ -80,21 +80,21 @@ core_solver_pretty_printer<T, X>::core_solver_pretty_printer(lp_core_solver_base
}
}
template <typename T, typename X> void core_solver_pretty_printer<T, X>:: init_column_widths() {
template <typename T, typename X> void core_solver_pretty_printer<T, X>::init_column_widths() {
for (unsigned i = 0; i < ncols(); i++) {
m_column_widths[i] = get_column_width(i);
}
}
template <typename T, typename X> void core_solver_pretty_printer<T, X>:: adjust_width_with_low_bound(unsigned column, unsigned & w) {
template <typename T, typename X> void core_solver_pretty_printer<T, X>::adjust_width_with_low_bound(unsigned column, unsigned & w) {
if (!m_core_solver.low_bounds_are_set()) return;
w = std::max(w, (unsigned)T_to_string(m_core_solver.low_bound_value(column)).size());
}
template <typename T, typename X> void core_solver_pretty_printer<T, X>:: adjust_width_with_upper_bound(unsigned column, unsigned & w) {
template <typename T, typename X> void core_solver_pretty_printer<T, X>::adjust_width_with_upper_bound(unsigned column, unsigned & w) {
w = std::max(w, (unsigned)T_to_string(m_core_solver.upper_bound_value(column)).size());
}
template <typename T, typename X> void core_solver_pretty_printer<T, X>:: adjust_width_with_bounds(unsigned column, unsigned & w) {
template <typename T, typename X> void core_solver_pretty_printer<T, X>::adjust_width_with_bounds(unsigned column, unsigned & w) {
switch (m_core_solver.get_column_type(column)) {
case fixed:
case boxed:
@ -116,7 +116,7 @@ core_solver_pretty_printer<T, X>::core_solver_pretty_printer(lp_core_solver_base
}
template <typename T, typename X> unsigned core_solver_pretty_printer<T, X>:: get_column_width(unsigned column) {
template <typename T, typename X> unsigned core_solver_pretty_printer<T, X>:: get_column_width(unsigned column) {
unsigned w = std::max(m_costs[column].size(), T_to_string(m_core_solver.m_x[column]).size());
adjust_width_with_bounds(column, w);
adjust_width_with_basis_heading(column, w);
@ -131,14 +131,14 @@ core_solver_pretty_printer<T, X>::core_solver_pretty_printer(lp_core_solver_base
return w;
}
template <typename T, typename X> std::string core_solver_pretty_printer<T, X>::regular_cell_string(unsigned row, unsigned column, std::string name) {
template <typename T, typename X> std::string core_solver_pretty_printer<T, X>::regular_cell_string(unsigned row, unsigned column, std::string name) {
T t = fabs(m_core_solver.m_ed[row]);
if ( t == 1) return name;
return T_to_string(t) + name;
}
template <typename T, typename X> void core_solver_pretty_printer<T, X>:: set_coeff(vector<string>& row, vector<string> & row_signs, unsigned col, const T & t, string name) {
template <typename T, typename X> void core_solver_pretty_printer<T, X>::set_coeff(vector<string>& row, vector<string> & row_signs, unsigned col, const T & t, string name) {
if (numeric_traits<T>::is_zero(t)) {
return;
}
@ -161,7 +161,7 @@ core_solver_pretty_printer<T, X>::core_solver_pretty_printer(lp_core_solver_base
}
}
template <typename T, typename X> void core_solver_pretty_printer<T, X>:: print_x() {
template <typename T, typename X> void core_solver_pretty_printer<T, X>::print_x() {
if (ncols() == 0) {
return;
}
@ -180,7 +180,7 @@ core_solver_pretty_printer<T, X>::core_solver_pretty_printer(lp_core_solver_base
std::cout << std::endl;
}
template <typename T, typename X> std::string core_solver_pretty_printer<T, X>::get_low_bound_string(unsigned j) {
template <typename T, typename X> std::string core_solver_pretty_printer<T, X>::get_low_bound_string(unsigned j) {
switch (m_core_solver.get_column_type(j)){
case boxed:
case low_bound:
@ -195,7 +195,7 @@ core_solver_pretty_printer<T, X>::core_solver_pretty_printer(lp_core_solver_base
}
}
template <typename T, typename X> std::string core_solver_pretty_printer<T, X>::get_upp_bound_string(unsigned j) {
template <typename T, typename X> std::string core_solver_pretty_printer<T, X>::get_upp_bound_string(unsigned j) {
switch (m_core_solver.get_column_type(j)){
case boxed:
case upper_bound:
@ -208,7 +208,7 @@ core_solver_pretty_printer<T, X>::core_solver_pretty_printer(lp_core_solver_base
}
template <typename T, typename X> void core_solver_pretty_printer<T, X>:: print_lows() {
template <typename T, typename X> void core_solver_pretty_printer<T, X>::print_lows() {
if (ncols() == 0) {
return;
}
@ -225,7 +225,7 @@ core_solver_pretty_printer<T, X>::core_solver_pretty_printer(lp_core_solver_base
std::cout << std::endl;
}
template <typename T, typename X> void core_solver_pretty_printer<T, X>:: print_upps() {
template <typename T, typename X> void core_solver_pretty_printer<T, X>::print_upps() {
if (ncols() == 0) {
return;
}
@ -242,7 +242,7 @@ core_solver_pretty_printer<T, X>::core_solver_pretty_printer(lp_core_solver_base
std::cout << std::endl;
}
template <typename T, typename X> void core_solver_pretty_printer<T, X>:: print_exact_norms() {
template <typename T, typename X> void core_solver_pretty_printer<T, X>::print_exact_norms() {
int blanks = m_title_width + 1 - m_exact_norm_title.size();
std::cout << m_exact_norm_title;
print_blanks(blanks);
@ -255,7 +255,7 @@ core_solver_pretty_printer<T, X>::core_solver_pretty_printer(lp_core_solver_base
std::cout << std::endl;
}
template <typename T, typename X> void core_solver_pretty_printer<T, X>:: print_approx_norms() {
template <typename T, typename X> void core_solver_pretty_printer<T, X>::print_approx_norms() {
int blanks = m_title_width + 1 - m_approx_norm_title.size();
std::cout << m_approx_norm_title;
print_blanks(blanks);
@ -268,7 +268,7 @@ core_solver_pretty_printer<T, X>::core_solver_pretty_printer(lp_core_solver_base
std::cout << std::endl;
}
template <typename T, typename X> void core_solver_pretty_printer<T, X>:: print() {
template <typename T, typename X> void core_solver_pretty_printer<T, X>::print() {
for (unsigned i = 0; i < nrows(); i++) {
print_row(i);
}
@ -283,7 +283,7 @@ core_solver_pretty_printer<T, X>::core_solver_pretty_printer(lp_core_solver_base
std::cout << std::endl;
}
template <typename T, typename X> void core_solver_pretty_printer<T, X>:: print_basis_heading() {
template <typename T, typename X> void core_solver_pretty_printer<T, X>::print_basis_heading() {
int blanks = m_title_width + 1 - m_basis_heading_title.size();
std::cout << m_basis_heading_title;
print_blanks(blanks);
@ -301,14 +301,14 @@ core_solver_pretty_printer<T, X>::core_solver_pretty_printer(lp_core_solver_base
std::cout << std::endl;
}
template <typename T, typename X> void core_solver_pretty_printer<T, X>:: print_cost() {
template <typename T, typename X> void core_solver_pretty_printer<T, X>::print_cost() {
int blanks = m_title_width + 1 - m_cost_title.size();
std::cout << m_cost_title;
print_blanks(blanks);
print_given_rows(m_costs, m_cost_signs, m_core_solver.get_cost());
}
template <typename T, typename X> void core_solver_pretty_printer<T, X>:: print_given_rows(vector<string> & row, vector<string> & signs, X rst) {
template <typename T, typename X> void core_solver_pretty_printer<T, X>::print_given_rows(vector<string> & row, vector<string> & signs, X rst) {
for (unsigned col = 0; col < row.size(); col++) {
unsigned width = m_column_widths[col];
string s = row[col];
@ -329,7 +329,7 @@ core_solver_pretty_printer<T, X>::core_solver_pretty_printer(lp_core_solver_base
std::cout << rs << std::endl;
}
template <typename T, typename X> void core_solver_pretty_printer<T, X>:: print_row(unsigned i){
template <typename T, typename X> void core_solver_pretty_printer<T, X>::print_row(unsigned i){
print_blanks(m_title_width + 1);
auto row = m_A[i];
auto sign_row = m_signs[i];

28
src/util/lp/dense_matrix.cpp
View file

@ -28,7 +28,7 @@ template <typename T, typename X> dense_matrix<T,X> dense_matrix<T,X>::operator*
*this = c;
return *this;
}
template <typename T, typename X> dense_matrix<T,X>&
template <typename T, typename X> dense_matrix<T,X>&
dense_matrix<T,X>::operator=(matrix<T, X> const & other){
if ( this == & other)
return *this;
@ -39,7 +39,7 @@ template <typename T, typename X> dense_matrix<T,X> dense_matrix<T,X>::operator*
return *this;
}
template <typename T, typename X> dense_matrix<T,X>&
template <typename T, typename X> dense_matrix<T,X>&
dense_matrix<T,X>::operator=(dense_matrix const & other){
if ( this == & other)
return *this;
@ -53,14 +53,14 @@ template <typename T, typename X> dense_matrix<T,X> dense_matrix<T,X>::operator*
return *this;
}
template <typename T, typename X> dense_matrix<T,X>::dense_matrix(dense_matrix<T, X> const & other) : m_m(other.row_count()), m_n(other.column_count()) {
template <typename T, typename X> dense_matrix<T,X>::dense_matrix(dense_matrix<T, X> const & other) : m_m(other.row_count()), m_n(other.column_count()) {
m_values = new T[m_m * m_n];
for (unsigned i = 0; i < m_m; i ++)
for (unsigned j = 0; j < m_n; j++)
m_values[i * m_n + j] = other.get_elem(i, j);
}
template <typename T, typename X> dense_matrix<T,X>::dense_matrix(matrix<T, X> const & other) :
template <typename T, typename X> dense_matrix<T,X>::dense_matrix(matrix<T, X> const & other) :
m_m(other.row_count()),
m_n(other.column_count()) {
m_values = new T[m_m * m_n];
@ -69,7 +69,7 @@ template <typename T, typename X> dense_matrix<T,X> dense_matrix<T,X>::operator*
m_values[i * m_n + j] = other.get_elem(i, j);
}
template <typename T, typename X> void dense_matrix<T, X>:: apply_from_right(T * w) {
template <typename T, typename X> void dense_matrix<T, X>::apply_from_right(T * w) {
T * t = new T[m_m];
for (int i = 0; i < m_m; i ++) {
T v = numeric_traits<T>::zero();
@ -85,7 +85,7 @@ template <typename T, typename X> dense_matrix<T,X> dense_matrix<T,X>::operator*
delete [] t;
}
template <typename T, typename X> void dense_matrix<T, X>:: apply_from_right(std::vector <T> & w) {
template <typename T, typename X> void dense_matrix<T, X>::apply_from_right(std::vector <T> & w) {
T * t = new T[m_m];
for (int i = 0; i < m_m; i ++) {
T v = numeric_traits<T>::zero();
@ -100,7 +100,7 @@ template <typename T, typename X> dense_matrix<T,X> dense_matrix<T,X>::operator*
}
delete [] t;
}
template <typename T, typename X> T* dense_matrix<T, X>::
template <typename T, typename X> T* dense_matrix<T, X>::
apply_from_left_with_different_dims(std::vector<T> & w) {
T * t = new T[m_m];
for (int i = 0; i < m_m; i ++) {
@ -114,7 +114,7 @@ template <typename T, typename X> dense_matrix<T,X> dense_matrix<T,X>::operator*
return t;
}
template <typename T, typename X> void dense_matrix<T, X>:: apply_from_left(std::vector<T> & w) {
template <typename T, typename X> void dense_matrix<T, X>::apply_from_left(std::vector<T> & w) {
T * t = new T[m_m];
for (int i = 0; i < m_m; i ++) {
T v = numeric_traits<T>::zero();
@ -130,7 +130,7 @@ template <typename T, typename X> dense_matrix<T,X> dense_matrix<T,X>::operator*
delete [] t;
}
template <typename T, typename X> void dense_matrix<T, X>:: apply_from_left(X * w, lp_settings & ) {
template <typename T, typename X> void dense_matrix<T, X>::apply_from_left(X * w, lp_settings & ) {
T * t = new T[m_m];
for (int i = 0; i < m_m; i ++) {
T v = numeric_traits<T>::zero();
@ -146,7 +146,7 @@ template <typename T, typename X> dense_matrix<T,X> dense_matrix<T,X>::operator*
delete [] t;
}
template <typename T, typename X> void dense_matrix<T, X>:: apply_from_left_to_X(std::vector<X> & w, lp_settings & ) {
template <typename T, typename X> void dense_matrix<T, X>::apply_from_left_to_X(std::vector<X> & w, lp_settings & ) {
std::vector<X> t(m_m);
for (int i = 0; i < m_m; i ++) {
X v = zero_of_type<X>();
@ -163,7 +163,7 @@ template <typename T, typename X> dense_matrix<T,X> dense_matrix<T,X>::operator*
// This method pivots row i to row i0 by muliplying row i by
// alpha and adding it to row i0.
template <typename T, typename X> void dense_matrix<T, X>:: pivot_row_to_row(unsigned i, T alpha, unsigned i0,
template <typename T, typename X> void dense_matrix<T, X>::pivot_row_to_row(unsigned i, T alpha, unsigned i0,
double & pivot_epsilon) {
thread_local T _0 = numeric_traits<T>::zero();
for (unsigned j = 0; j < m_n; j++) {
@ -174,7 +174,7 @@ template <typename T, typename X> dense_matrix<T,X> dense_matrix<T,X>::operator*
}
}
template <typename T, typename X> void dense_matrix<T, X>:: swap_columns(unsigned a, unsigned b) {
template <typename T, typename X> void dense_matrix<T, X>::swap_columns(unsigned a, unsigned b) {
for (unsigned i = 0; i < m_m; i++) {
T t = get_elem(i, a);
set_elem(i, a, get_elem(i, b));
@ -182,7 +182,7 @@ template <typename T, typename X> dense_matrix<T,X> dense_matrix<T,X>::operator*
}
}
template <typename T, typename X> void dense_matrix<T, X>:: swap_rows(unsigned a, unsigned b) {
template <typename T, typename X> void dense_matrix<T, X>::swap_rows(unsigned a, unsigned b) {
for (unsigned i = 0; i < m_n; i++) {
T t = get_elem(a, i);
set_elem(a, i, get_elem(b, i));
@ -190,7 +190,7 @@ template <typename T, typename X> dense_matrix<T,X> dense_matrix<T,X>::operator*
}
}
template <typename T, typename X> void dense_matrix<T, X>:: multiply_row_by_constant(unsigned row, T & t) {
template <typename T, typename X> void dense_matrix<T, X>::multiply_row_by_constant(unsigned row, T & t) {
for (unsigned i = 0; i < m_n; i++) {
set_elem(row, i, t * get_elem(row, i));
}

14
src/util/lp/indexed_vector.cpp
View file

@ -37,38 +37,38 @@ void print_vector(const std::vector<mpq> & t) {
std::cout << std::endl;
}
template <typename T>
template <typename T>
void indexed_vector<T>::resize(unsigned data_size) {
m_index.clear();
m_data.resize(data_size, numeric_traits<T>::zero());
}
template <typename T>
template <typename T>
void indexed_vector<T>::set_value(T value, unsigned index) {
m_data[index] = value;
m_index.push_back(index);
}
template <typename T>
template <typename T>
void indexed_vector<T>::clear() {
for (unsigned i : m_index)
m_data[i] = numeric_traits<T>::zero();
m_index.clear();
}
template <typename T>
template <typename T>
void indexed_vector<T>::clear_all() {
unsigned i = m_data.size();
while (i--) m_data[i] = numeric_traits<T>::zero();
m_index.clear();
}
template <typename T>
template <typename T>
void indexed_vector<T>::erase_from_index(unsigned j) {
auto it = std::find(m_index.begin(), m_index.end(), j);
if (it != m_index.end()) m_index.erase(it);
}
#ifdef LEAN_DEBUG
template <typename T>
template <typename T>
bool indexed_vector<T>::is_OK() const {
int size = 0;
for (unsigned i = 0; i < m_data.size(); i++) {
@ -80,7 +80,7 @@ void print_vector(const std::vector<mpq> & t) {
}
return size == m_index.size();
}
template <typename T>
template <typename T>
void indexed_vector<T>::print() {
std::cout << "m_index " << std::endl;
for (unsigned i = 0; i < m_index.size(); i++) {

2
src/util/lp/lar_core_solver.cpp
View file

@ -327,7 +327,7 @@ template <typename T, typename X> void lar_core_solver<T, X>::try_add_breakpo
}
}
template <typename T, typename X> std::string lar_core_solver<T, X>:: break_type_to_string(breakpoint_type type) {
template <typename T, typename X> std::string lar_core_solver<T, X>::break_type_to_string(breakpoint_type type) {
switch (type){
case low_break: return "low_break";
case upper_break: return "upper_break";

28
src/util/lp/lp_dual_core_solver.cpp
View file

@ -78,7 +78,7 @@ template <typename T, typename X> void lp_dual_core_solver<T, X>::restore_non_ba
}
}
template <typename T, typename X> bool lp_dual_core_solver<T, X>:: update_basis(int entering, int leaving) {
template <typename T, typename X> bool lp_dual_core_solver<T, X>::update_basis(int entering, int leaving) {
// the second argument is the element of the entering column from the pivot row - its value should be equal to the low diagonal element of the bump after all pivoting is done
if (!(this->m_refactor_counter++ >= 200)) {
this->m_factorization->replace_column(leaving, this->m_ed[this->m_factorization->basis_heading(leaving)], this->m_w);
@ -132,7 +132,7 @@ template <typename T, typename X> void lp_dual_core_solver<T, X>::start_with_ini
adjust_xb_for_changed_xn_and_init_betas();
}
template <typename T, typename X> bool lp_dual_core_solver<T, X>:: done() {
template <typename T, typename X> bool lp_dual_core_solver<T, X>::done() {
if (this->m_status == OPTIMAL) {
return true;
}
@ -157,10 +157,10 @@ template <typename T, typename X> T lp_dual_core_solver<T, X>::get_edge_steepnes
return del / this->m_betas[this->m_basis_heading[p]];
}
// template <typename T, typename X> void lp_dual_core_solver<T, X>::print_x_and_low_bound(unsigned p) {
//template <typename T, typename X> void lp_dual_core_solver<T, X>::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 <typename T, typename X> void lp_dual_core_solver<T, X>::print_x_and_upper_bound(unsigned p) {
//template <typename T, typename X> void lp_dual_core_solver<T, X>::print_x_and_upper_bound(unsigned p) {
// std::cout << "x u[" << p << "] = " << this->m_x[p] << " " << this->m_upper_bound_values[p] << std::endl;
// }
@ -256,7 +256,7 @@ template <typename T, typename X> void lp_dual_core_solver<T, X>::pricing_loop(u
}
}
template <typename T, typename X> bool lp_dual_core_solver<T, X>:: advance_on_known_p() {
template <typename T, typename X> bool lp_dual_core_solver<T, X>::advance_on_known_p() {
if (done()) {
return true;
}
@ -271,7 +271,7 @@ template <typename T, typename X> bool lp_dual_core_solver<T, X>:: advance_on_kn
return basis_change_and_update();
}
template <typename T, typename X> int lp_dual_core_solver<T, X>:: define_sign_of_alpha_r() {
template <typename T, typename X> int lp_dual_core_solver<T, X>::define_sign_of_alpha_r() {
switch (this->m_column_type[m_p]) {
case boxed:
case fixed:
@ -297,7 +297,7 @@ template <typename T, typename X> int lp_dual_core_solver<T, X>:: define_sign_of
}
}
template <typename T, typename X> bool lp_dual_core_solver<T, X>:: can_be_breakpoint(unsigned j) {
template <typename T, typename X> bool lp_dual_core_solver<T, X>::can_be_breakpoint(unsigned j) {
if (this->pivot_row_element_is_too_small_for_ratio_test(j)) return false;
switch (this->m_column_type[j]) {
case low_bound:
@ -369,7 +369,7 @@ template <typename T, typename X> void lp_dual_core_solver<T, X>::restore_d() {
}
}
template <typename T, typename X> bool lp_dual_core_solver<T, X>:: d_is_correct() {
template <typename T, typename X> bool lp_dual_core_solver<T, X>::d_is_correct() {
this->solve_yB(this->m_y);
for (auto j : non_basis()) {
T d = this->m_costs[j] - this->m_A.dot_product_with_column(this->m_y, j);
@ -466,7 +466,7 @@ template <typename T, typename X> void lp_dual_core_solver<T, X>::init_betas_pre
}
// step 7 of the algorithm from Progress
template <typename T, typename X> bool lp_dual_core_solver<T, X>:: basis_change_and_update() {
template <typename T, typename X> bool lp_dual_core_solver<T, X>::basis_change_and_update() {
update_betas();
update_d_and_xB();
m_theta_P = m_delta / this->m_ed[m_r];
@ -501,7 +501,7 @@ template <typename T, typename X> void lp_dual_core_solver<T, X>::revert_to_prev
}
template <typename T, typename X> bool lp_dual_core_solver<T, X>:: problem_is_dual_feasible() {
template <typename T, typename X> bool lp_dual_core_solver<T, X>::problem_is_dual_feasible() {
for (unsigned j : non_basis()){
if (!this->column_is_dual_feasible(j)) {
std::cout << "column " << j << " is not dual feasible" << std::endl;
@ -516,7 +516,7 @@ template <typename T, typename X> bool lp_dual_core_solver<T, X>:: problem_is_du
return true;
}
template <typename T, typename X> unsigned lp_dual_core_solver<T, X>:: get_number_of_rows_to_try_for_leaving() {
template <typename T, typename X> unsigned lp_dual_core_solver<T, X>::get_number_of_rows_to_try_for_leaving() {
unsigned s = this->m_m;
if (this->m_m > 300) {
s = (unsigned)(s / this->m_settings.percent_of_entering_to_check * 100);
@ -524,7 +524,7 @@ template <typename T, typename X> unsigned lp_dual_core_solver<T, X>:: get_numbe
return my_random() % s + 1;
}
template <typename T, typename X> bool lp_dual_core_solver<T, X>:: delta_keeps_the_sign(int initial_delta_sign, const T & delta) {
template <typename T, typename X> bool lp_dual_core_solver<T, X>::delta_keeps_the_sign(int initial_delta_sign, const T & delta) {
if (numeric_traits<T>::precise())
return ((delta > numeric_traits<T>::zero()) && (initial_delta_sign == 1)) ||
((delta < numeric_traits<T>::zero()) && (initial_delta_sign == -1));
@ -560,7 +560,7 @@ template <typename T, typename X> T lp_dual_core_solver<T, X>::delta_lost_on_fli
return ret;
}
template <typename T, typename X> bool lp_dual_core_solver<T, X>:: tight_breakpoinst_are_all_boxed() {
template <typename T, typename X> bool lp_dual_core_solver<T, X>::tight_breakpoinst_are_all_boxed() {
if (this->m_column_type[m_q] != boxed) return false;
for (auto j : m_tight_set) {
if (this->m_column_type[j] != boxed) return false;
@ -636,7 +636,7 @@ template <typename T, typename X> void lp_dual_core_solver<T, X>::erase_tight_br
}
}
template <typename T, typename X> bool lp_dual_core_solver<T, X>:: ratio_test() {
template <typename T, typename X> bool lp_dual_core_solver<T, X>::ratio_test() {
m_sign_of_alpha_r = define_sign_of_alpha_r();
fill_breakpoint_set();
m_flipped_boxed.clear();

42
src/util/lp/lp_dual_simplex.cpp
View file

@ -7,7 +7,7 @@
#include "util/lp/lp_dual_simplex.h"
namespace lean {
template <typename T, typename X> void lp_dual_simplex<T, X>:: decide_on_status_after_stage1() {
template <typename T, typename X> void lp_dual_simplex<T, X>::decide_on_status_after_stage1() {
switch (m_core_solver->get_status()) {
case OPTIMAL:
if (this->m_settings.abs_val_is_smaller_than_artificial_tolerance(m_core_solver->get_cost())) {
@ -37,7 +37,7 @@ template <typename T, typename X> void lp_dual_simplex<T, X>:: decide_on_status_
}
}
template <typename T, typename X> void lp_dual_simplex<T, X>:: fix_logical_for_stage2(unsigned j) {
template <typename T, typename X> void lp_dual_simplex<T, X>::fix_logical_for_stage2(unsigned j) {
lean_assert(j >= this->number_of_core_structurals());
switch (m_column_types_of_logicals[j - this->number_of_core_structurals()]) {
case low_bound:
@ -55,7 +55,7 @@ template <typename T, typename X> void lp_dual_simplex<T, X>:: fix_logical_for_s
}
}
template <typename T, typename X> void lp_dual_simplex<T, X>:: fix_structural_for_stage2(unsigned j) {
template <typename T, typename X> void lp_dual_simplex<T, X>::fix_structural_for_stage2(unsigned j) {
column_info<T> * ci = this->m_columns[this->m_core_solver_columns_to_external_columns[j]];
switch (ci->get_column_type()) {
case low_bound:
@ -87,7 +87,7 @@ template <typename T, typename X> void lp_dual_simplex<T, X>:: fix_structural_fo
}
}
template <typename T, typename X> void lp_dual_simplex<T, X>:: unmark_boxed_and_fixed_columns_and_fix_structural_costs() {
template <typename T, typename X> void lp_dual_simplex<T, X>::unmark_boxed_and_fixed_columns_and_fix_structural_costs() {
unsigned j = this->m_A->column_count();
while (j-- > this->number_of_core_structurals()) {
fix_logical_for_stage2(j);
@ -98,14 +98,14 @@ template <typename T, typename X> void lp_dual_simplex<T, X>:: unmark_boxed_and_
}
}
template <typename T, typename X> void lp_dual_simplex<T, X>:: restore_right_sides() {
template <typename T, typename X> void lp_dual_simplex<T, X>::restore_right_sides() {
unsigned i = this->m_A->row_count();
while (i--) {
this->m_b[i] = m_b_copy[i];
}
}
template <typename T, typename X> void lp_dual_simplex<T, X>:: solve_for_stage2() {
template <typename T, typename X> void lp_dual_simplex<T, X>::solve_for_stage2() {
m_core_solver->restore_non_basis();
m_core_solver->solve_yB(m_core_solver->m_y);
m_core_solver->fill_reduced_costs_from_m_y_by_rows();
@ -131,14 +131,14 @@ template <typename T, typename X> void lp_dual_simplex<T, X>:: solve_for_stage2(
this->m_second_stage_iterations = m_core_solver->m_total_iterations;
}
template <typename T, typename X> void lp_dual_simplex<T, X>:: fill_x_with_zeros() {
template <typename T, typename X> void lp_dual_simplex<T, X>::fill_x_with_zeros() {
unsigned j = this->m_A->column_count();
while (j--) {
this->m_x[j] = numeric_traits<T>::zero();
}
}
template <typename T, typename X> void lp_dual_simplex<T, X>:: stage1() {
template <typename T, typename X> void lp_dual_simplex<T, X>::stage1() {
lean_assert(m_core_solver == nullptr);
this->m_x.resize(this->m_A->column_count(), numeric_traits<T>::zero());
this->print_statistics_on_A();
@ -168,14 +168,14 @@ template <typename T, typename X> void lp_dual_simplex<T, X>:: stage1() {
this->m_first_stage_iterations = m_core_solver->m_total_iterations;
}
template <typename T, typename X> void lp_dual_simplex<T, X>:: stage2() {
template <typename T, typename X> void lp_dual_simplex<T, X>::stage2() {
std::cout << "starting stage2" << std::endl;
unmark_boxed_and_fixed_columns_and_fix_structural_costs();
restore_right_sides();
solve_for_stage2();
}
template <typename T, typename X> void lp_dual_simplex<T, X>:: fill_first_stage_solver_fields() {
template <typename T, typename X> void lp_dual_simplex<T, X>::fill_first_stage_solver_fields() {
unsigned slack_var = this->number_of_core_structurals();
unsigned artificial = this->number_of_core_structurals() + this->m_slacks;
@ -185,7 +185,7 @@ template <typename T, typename X> void lp_dual_simplex<T, X>:: fill_first_stage_
fill_costs_and_bounds_and_column_types_for_the_first_stage_solver();
}
template <typename T, typename X> column_type lp_dual_simplex<T, X>:: get_column_type(unsigned j) {
template <typename T, typename X> column_type lp_dual_simplex<T, X>::get_column_type(unsigned j) {
lean_assert(j < this->m_A->column_count());
if (j >= this->number_of_core_structurals()) {
return m_column_types_of_logicals[j - this->number_of_core_structurals()];
@ -193,7 +193,7 @@ template <typename T, typename X> column_type lp_dual_simplex<T, X>:: get_column
return this->m_columns[this->m_core_solver_columns_to_external_columns[j]]->get_column_type();
}
template <typename T, typename X> void lp_dual_simplex<T, X>:: fill_costs_bounds_types_and_can_enter_basis_for_the_first_stage_solver_structural_column(unsigned j) {
template <typename T, typename X> void lp_dual_simplex<T, X>::fill_costs_bounds_types_and_can_enter_basis_for_the_first_stage_solver_structural_column(unsigned j) {
// see 4.7 in the dissertation of Achim Koberstein
lean_assert(this->m_core_solver_columns_to_external_columns.find(j) !=
this->m_core_solver_columns_to_external_columns.end());
@ -231,7 +231,7 @@ template <typename T, typename X> void lp_dual_simplex<T, X>:: fill_costs_bounds
m_column_types_of_core_solver[j] = boxed;
}
template <typename T, typename X> void lp_dual_simplex<T, X>:: fill_costs_bounds_types_and_can_enter_basis_for_the_first_stage_solver_logical_column(unsigned j) {
template <typename T, typename X> void lp_dual_simplex<T, X>::fill_costs_bounds_types_and_can_enter_basis_for_the_first_stage_solver_logical_column(unsigned j) {
this->m_costs[j] = 0;
lean_assert(get_column_type(j) != upper_bound);
if ((m_can_enter_basis[j] = (get_column_type(j) == low_bound))) {
@ -245,7 +245,7 @@ template <typename T, typename X> void lp_dual_simplex<T, X>:: fill_costs_bounds
}
}
template <typename T, typename X> void lp_dual_simplex<T, X>:: fill_costs_and_bounds_and_column_types_for_the_first_stage_solver() {
template <typename T, typename X> void lp_dual_simplex<T, X>::fill_costs_and_bounds_and_column_types_for_the_first_stage_solver() {
unsigned j = this->m_A->column_count();
while (j-- > this->number_of_core_structurals()) { // go over logicals here
fill_costs_bounds_types_and_can_enter_basis_for_the_first_stage_solver_logical_column(j);
@ -256,7 +256,7 @@ template <typename T, typename X> void lp_dual_simplex<T, X>:: fill_costs_and_bo
}
}
template <typename T, typename X> void lp_dual_simplex<T, X>:: fill_first_stage_solver_fields_for_row_slack_and_artificial(unsigned row,
template <typename T, typename X> void lp_dual_simplex<T, X>::fill_first_stage_solver_fields_for_row_slack_and_artificial(unsigned row,
unsigned & slack_var,
unsigned & artificial) {
lean_assert(row < this->row_count());
@ -283,7 +283,7 @@ template <typename T, typename X> void lp_dual_simplex<T, X>:: fill_first_stage_
this->m_costs[artificial] = numeric_traits<T>::zero();
artificial++;
} else {
// we can put a slack_var into the basis, and atemplate <typename T, typename X> void lp_dual_simplex<T, X>:: adding an artificial variable
// we can put a slack_var into the basis, and atemplate <typename T, typename X> void lp_dual_simplex<T, X>::adding an artificial variable
this->m_basis[row] = slack_var;
this->m_costs[slack_var] = numeric_traits<T>::zero();
}
@ -301,7 +301,7 @@ template <typename T, typename X> void lp_dual_simplex<T, X>:: fill_first_stage_
this->m_costs[artificial] = numeric_traits<T>::zero();
artificial++;
} else {
// we can put slack_var into the basis, and atemplate <typename T, typename X> void lp_dual_simplex<T, X>:: adding an artificial variable
// we can put slack_var into the basis, and atemplate <typename T, typename X> void lp_dual_simplex<T, X>::adding an artificial variable
this->m_basis[row] = slack_var;
this->m_costs[slack_var] = numeric_traits<T>::zero();
}
@ -310,7 +310,7 @@ template <typename T, typename X> void lp_dual_simplex<T, X>:: fill_first_stage_
}
}
template <typename T, typename X> void lp_dual_simplex<T, X>:: augment_matrix_A_and_fill_x_and_allocate_some_fields() {
template <typename T, typename X> void lp_dual_simplex<T, X>::augment_matrix_A_and_fill_x_and_allocate_some_fields() {
this->count_slacks_and_artificials();
this->m_A->add_columns_at_the_end(this->m_slacks + this->m_artificials);
unsigned n = this->m_A->column_count();
@ -325,14 +325,14 @@ template <typename T, typename X> void lp_dual_simplex<T, X>:: augment_matrix_A_
template <typename T, typename X> void lp_dual_simplex<T, X>:: copy_m_b_aside_and_set_it_to_zeros() {
template <typename T, typename X> void lp_dual_simplex<T, X>::copy_m_b_aside_and_set_it_to_zeros() {
for (int i = 0; i < this->m_b.size(); i++) {
m_b_copy.push_back(this->m_b[i]);
this->m_b[i] = numeric_traits<T>::zero(); // preparing for the first stage
}
}
template <typename T, typename X> void lp_dual_simplex<T, X>:: find_maximal_solution(){
template <typename T, typename X> void lp_dual_simplex<T, X>::find_maximal_solution(){
if (this->problem_is_empty()) {
this->m_status = lp_status::EMPTY;
return;
@ -358,7 +358,7 @@ template <typename T, typename X> void lp_dual_simplex<T, X>:: find_maximal_solu
}
template <typename T, typename X> T lp_dual_simplex<T, X>:: get_current_cost() const {
template <typename T, typename X> T lp_dual_simplex<T, X>::get_current_cost() const {
T ret = numeric_traits<T>::zero();
for (auto it : this->m_columns) {
ret += this->get_column_cost_value(it.first, it.second);

106
src/util/lp/lp_primal_core_solver.cpp
View file

@ -67,7 +67,7 @@ int lp_primal_core_solver<T, X>::choose_entering_column(unsigned number_of_benef
template <typename T, typename X> int
lp_primal_core_solver<T, X>:: find_leaving_and_t_precisely(unsigned entering, X & t){
lp_primal_core_solver<T, X>::find_leaving_and_t_precisely(unsigned entering, X & t){
int leaving = -1;
T abs_of_d_of_leaving = numeric_traits<T>::zero();
for (unsigned i = 0; i < this->m_m; i++) {
@ -83,7 +83,7 @@ lp_primal_core_solver<T, X>:: find_leaving_and_t_precisely(unsigned entering, X
return leaving;
}
template <typename T, typename X> X lp_primal_core_solver<T, X>:: get_harris_theta() {
template <typename T, typename X> X lp_primal_core_solver<T, X>::get_harris_theta() {
X theta = positive_infinity();
unsigned i = this->m_m;
while (i--) {
@ -95,7 +95,7 @@ template <typename T, typename X> X lp_primal_core_solver<T, X>:: get_harris_
}
template <typename T, typename X> int lp_primal_core_solver<T, X>:: find_leaving_on_harris_theta(X const & harris_theta, X & t) {
template <typename T, typename X> int lp_primal_core_solver<T, X>::find_leaving_on_harris_theta(X const & harris_theta, X & t) {
int leaving = -1;
T pivot_abs_max;
// we know already that there is no bound flip on entering
@ -135,7 +135,7 @@ template <typename T, typename X> int lp_primal_core_solver<T, X>:: find_leav
}
template <typename T, typename X> bool lp_primal_core_solver<T, X>:: try_jump_to_another_bound_on_entering(unsigned entering, const X & theta, X & t) {
template <typename T, typename X> bool lp_primal_core_solver<T, X>::try_jump_to_another_bound_on_entering(unsigned entering, const X & theta, X & t) {
if (this->m_column_type[entering] != boxed)
return false;
@ -156,7 +156,7 @@ template <typename T, typename X> bool lp_primal_core_solver<T, X>:: try_jump
return false;
}
template <typename T, typename X> int lp_primal_core_solver<T, X>:: find_leaving_and_t(unsigned entering, X & t){
template <typename T, typename X> int lp_primal_core_solver<T, X>::find_leaving_and_t(unsigned entering, X & t){
if (numeric_traits<T>::precise()) return find_leaving_and_t_precisely(entering, t);
X theta = get_harris_theta();
lean_assert(theta >= zero_of_type<X>());
@ -170,7 +170,7 @@ template <typename T, typename X> int lp_primal_core_solver<T, X>:: find_leav
// x[j] + t * m >= m_low_bound_values[j] ( if m < 0 )
// or
// x[j] + t * m <= this->m_upper_bound_values[j] ( if m > 0)
template <typename T, typename X> void lp_primal_core_solver<T, X>:: get_bound_on_variable_and_update_leaving_precisely(unsigned j, int & leaving, T m, X & t, T & abs_of_d_of_leaving) {
template <typename T, typename X> void lp_primal_core_solver<T, X>::get_bound_on_variable_and_update_leaving_precisely(unsigned j, int & leaving, T m, X & t, T & abs_of_d_of_leaving) {
lean_assert(leaving == -1 || t > zero_of_type<X>());
if (m > 0) {
if (this->m_column_type[j] != boxed) {
@ -199,7 +199,7 @@ template <typename T, typename X> void lp_primal_core_solver<T, X>:: get_boun
}
}
template <typename T, typename X> X lp_primal_core_solver<T, X>:: get_max_bound(std::vector<X> & b) {
template <typename T, typename X> X lp_primal_core_solver<T, X>::get_max_bound(std::vector<X> & b) {
X ret = zero_of_type<X>();
for (auto & v : b) {
X a = abs(v);
@ -209,7 +209,7 @@ template <typename T, typename X> X lp_primal_core_solver<T, X>:: get_max_bou
}
// stage1 constructor
template <typename T, typename X> lp_primal_core_solver<T, X>:: lp_primal_core_solver(static_matrix<T, X> & A,
template <typename T, typename X> lp_primal_core_solver<T, X>:: lp_primal_core_solver(static_matrix<T, X> & A,
std::vector<X> & b, // the right side vector
std::vector<X> & x, // the number of elements in x needs to be at least as large as the number of columns in A
std::vector<unsigned> & basis,
@ -264,12 +264,12 @@ lp_primal_core_solver(static_matrix<T, X> & A,
#endif
}
template <typename T, typename X> void lp_primal_core_solver<T, X>:: init_lu() {
template <typename T, typename X> void lp_primal_core_solver<T, X>::init_lu() {
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_refactor_counter = 0;
}
template <typename T, typename X> bool lp_primal_core_solver<T, X>:: initial_x_is_correct() {
template <typename T, typename X> bool lp_primal_core_solver<T, X>::initial_x_is_correct() {
std::set<unsigned> basis_set;
for (int i = 0; i < this->m_A.row_count(); i++) {
basis_set.insert(this->m_basis[i]);
@ -302,24 +302,24 @@ template <typename T, typename X> bool lp_primal_core_solver<T, X>:: initial_
}
#ifdef LEAN_DEBUG
template <typename T, typename X> void lp_primal_core_solver<T, X>:: check_Ax_equal_b() {
template <typename T, typename X> void lp_primal_core_solver<T, X>::check_Ax_equal_b() {
dense_matrix<T, X> d(this->m_A);
T * ls = d.apply_from_left_with_different_dims(this->m_x);
lean_assert(vectors_are_equal<T>(ls, this->m_b, this->m_m));
delete [] ls;
}
template <typename T, typename X> void lp_primal_core_solver<T, X>:: check_the_bounds() {
template <typename T, typename X> void lp_primal_core_solver<T, X>::check_the_bounds() {
for (unsigned i = 0; i < this->m_n; i++) {
check_bound(i);
}
}
template <typename T, typename X> void lp_primal_core_solver<T, X>:: check_bound(unsigned i) {
template <typename T, typename X> void lp_primal_core_solver<T, X>::check_bound(unsigned i) {
lean_assert (!(column_has_low_bound(i) && (numeric_traits<T>::zero() > this->m_x[i])));
lean_assert (!(column_has_upper_bound(i) && (this->m_upper_bound_values[i] < this->m_x[i])));
}
template <typename T, typename X> void lp_primal_core_solver<T, X>:: check_correctness() {
template <typename T, typename X> void lp_primal_core_solver<T, X>::check_correctness() {
check_the_bounds();
check_Ax_equal_b();
}
@ -327,7 +327,7 @@ template <typename T, typename X> void lp_primal_core_solver<T, X>:: check_co
// from page 183 of Istvan Maros's book
// the basis structures have not changed yet
template <typename T, typename X> void lp_primal_core_solver<T, X>:: update_reduced_costs_from_pivot_row(unsigned entering, unsigned leaving) {
template <typename T, typename X> void lp_primal_core_solver<T, X>::update_reduced_costs_from_pivot_row(unsigned entering, unsigned leaving) {
// the basis heading has changed already
#ifdef LEAN_DEBUG
auto & basis_heading = this->m_factorization->m_basis_heading;
@ -352,7 +352,7 @@ template <typename T, typename X> void lp_primal_core_solver<T, X>:: update_r
// return 0 if the reduced cost at entering is close enough to the refreshed
// 1 if it is way off, and 2 if it is unprofitable
template <typename T, typename X> int lp_primal_core_solver<T, X>:: refresh_reduced_cost_at_entering_and_check_that_it_is_off(unsigned entering) {
template <typename T, typename X> int lp_primal_core_solver<T, X>::refresh_reduced_cost_at_entering_and_check_that_it_is_off(unsigned entering) {
T reduced_at_entering_was = this->m_d[entering]; // can benefit from going over non-zeros of m_ed
lean_assert(abs(reduced_at_entering_was) > m_epsilon_of_reduced_cost);
T refreshed_cost = this->m_costs[entering];
@ -382,7 +382,7 @@ template <typename T, typename X> int lp_primal_core_solver<T, X>:: refresh_r
return 0;
}
template <typename T, typename X> void lp_primal_core_solver<T, X>:: normalize_costs_and_backup_costs() {
template <typename T, typename X> void lp_primal_core_solver<T, X>::normalize_costs_and_backup_costs() {
T cost_max = std::max(max_abs_in_vector(this->m_costs), T(1));
lean_assert(m_costs_backup.size() == 0);
for (unsigned j = 0; j < this->m_costs.size(); j++)
@ -390,7 +390,7 @@ template <typename T, typename X> void lp_primal_core_solver<T, X>:: normaliz
m_using_inf_costs = false;
}
template <typename T, typename X> void lp_primal_core_solver<T, X>:: init_run() {
template <typename T, typename X> void lp_primal_core_solver<T, X>::init_run() {
this->m_start_time = get_millisecond_count();
this->m_total_iterations = 0;
this->m_iters_with_no_cost_growing = 0;
@ -399,7 +399,7 @@ template <typename T, typename X> void lp_primal_core_solver<T, X>:: init_run
init_reduced_costs();
}
template <typename T, typename X> int lp_primal_core_solver<T, X>:: pivots_in_column_and_row_are_different(int entering, int leaving) const {
template <typename T, typename X> int lp_primal_core_solver<T, X>::pivots_in_column_and_row_are_different(int entering, int leaving) const {
const T & column_p = this->m_ed[this->m_basis_heading[leaving]];
const T & row_p = this->m_pivot_row[entering];
if (is_zero(column_p) || is_zero(row_p)) return true; // pivots cannot be zero
@ -417,14 +417,14 @@ template <typename T, typename X> int lp_primal_core_solver<T, X>:: pivots_in
return 0;
}
template <typename T, typename X> void lp_primal_core_solver<T, X>:: calc_working_vector_beta_for_column_norms(){
template <typename T, typename X> void lp_primal_core_solver<T, X>::calc_working_vector_beta_for_column_norms(){
unsigned i = this->m_m;
while (i--)
m_beta[i] = this->m_ed[i];
this->m_factorization->solve_yB(m_beta);
}
template <typename T, typename X>void lp_primal_core_solver<T, X>:: advance_on_entering_and_leaving(int entering, int leaving, X & t) {
template <typename T, typename X>void lp_primal_core_solver<T, X>::advance_on_entering_and_leaving(int entering, int leaving, X & t) {
lean_assert(t >= zero_of_type<X>());
lean_assert(leaving >= 0 && entering >= 0);
lean_assert(entering != leaving || !is_zero(t)); // otherwise nothing changes
@ -489,7 +489,7 @@ template <typename T, typename X>void lp_primal_core_solver<T, X>:: advance_on_e
// this->init_reduced_costs_for_one_iteration();
// }
template <typename T, typename X> void lp_primal_core_solver<T, X>:: advance_on_entering(int entering) {
template <typename T, typename X> void lp_primal_core_solver<T, X>::advance_on_entering(int entering) {
lean_assert(entering > -1);
this->solve_Bd(entering);
int refresh_result = refresh_reduced_cost_at_entering_and_check_that_it_is_off(entering);
@ -524,12 +524,12 @@ template <typename T, typename X> void lp_primal_core_solver<T, X>:: advance_
advance_on_entering_and_leaving(entering, leaving, t);
}
template <typename T, typename X> void lp_primal_core_solver<T, X>:: push_forward_offset_in_non_basis(unsigned & offset_in_nb) {
template <typename T, typename X> void lp_primal_core_solver<T, X>::push_forward_offset_in_non_basis(unsigned & offset_in_nb) {
if (++offset_in_nb == this->m_non_basic_columns.size())
offset_in_nb = 0;
}
template <typename T, typename X> unsigned lp_primal_core_solver<T, X>:: get_number_of_non_basic_column_to_try_for_enter() {
template <typename T, typename X> unsigned lp_primal_core_solver<T, X>::get_number_of_non_basic_column_to_try_for_enter() {
unsigned ret = this->m_factorization->m_non_basic_columns.size();
if (this->m_status == TENTATIVE_UNBOUNDED)
return ret; // we really need to find entering with a large reduced cost
@ -539,7 +539,7 @@ template <typename T, typename X> unsigned lp_primal_core_solver<T, X>:: get_
return std::max(static_cast<unsigned>(my_random() % ret), 1u);
}
template <typename T, typename X> void lp_primal_core_solver<T, X>:: print_column_norms() {
template <typename T, typename X> void lp_primal_core_solver<T, X>::print_column_norms() {
std::cout << " column norms " << std::endl;
for (unsigned j = 0; j < this->m_n; j++) {
std::cout << this->m_column_norms[j] << " ";
@ -549,7 +549,7 @@ template <typename T, typename X> void lp_primal_core_solver<T, X>:: print_co
}
// returns the number of iterations
template <typename T, typename X> unsigned lp_primal_core_solver<T, X>:: solve() {
template <typename T, typename X> unsigned lp_primal_core_solver<T, X>::solve() {
init_run();
lean_assert(!this->A_mult_x_is_off());
do {
@ -611,7 +611,7 @@ template <typename T, typename X> unsigned lp_primal_core_solver<T, X>:: solv
return this->m_total_iterations;
}
template <typename T, typename X> void lp_primal_core_solver<T, X>:: delete_factorization() {
template <typename T, typename X> void lp_primal_core_solver<T, X>::delete_factorization() {
if (this->m_factorization != nullptr) {
delete this->m_factorization;
this->m_factorization = nullptr;
@ -619,14 +619,14 @@ template <typename T, typename X> void lp_primal_core_solver<T, X>:: delete_f
}
// according to Swietanowski, " A new steepest edge approximation for the simplex method for linear programming"
template <typename T, typename X> void lp_primal_core_solver<T, X>:: init_column_norms() {
template <typename T, typename X> void lp_primal_core_solver<T, X>::init_column_norms() {
m_column_norm_update_counter = 0;
for (unsigned j : this->m_non_basic_columns)
this->m_column_norms[j] = 1;
}
// debug only
template <typename T, typename X> T lp_primal_core_solver<T, X>:: calculate_column_norm_exactly(unsigned j) {
template <typename T, typename X> T lp_primal_core_solver<T, X>::calculate_column_norm_exactly(unsigned j) {
indexed_vector<T> w(this->m_m);
this->m_A.copy_column_to_vector(j, w);
std::vector<T> d(this->m_m);
@ -637,7 +637,7 @@ template <typename T, typename X> T lp_primal_core_solver<T, X>:: calculate_c
return ret+1;
}
template <typename T, typename X> void lp_primal_core_solver<T, X>:: update_or_init_column_norms(unsigned entering, unsigned leaving) {
template <typename T, typename X> void lp_primal_core_solver<T, X>::update_or_init_column_norms(unsigned entering, unsigned leaving) {
if (++m_column_norm_update_counter == this->m_settings.column_norms_update_frequency) {
init_column_norms();
} else {
@ -646,7 +646,7 @@ template <typename T, typename X> void lp_primal_core_solver<T, X>:: update_o
}
// following Swietanowski - A new steepest ...
template <typename T, typename X> void lp_primal_core_solver<T, X>:: update_column_norms(unsigned entering, unsigned leaving) {
template <typename T, typename X> void lp_primal_core_solver<T, X>::update_column_norms(unsigned entering, unsigned leaving) {
T pivot = this->m_pivot_row[entering];
T g_ent = std::max(calculate_norm_of_entering_exactly() / pivot /pivot, T(0.000001));
this->m_column_norms[leaving] = g_ent;
@ -667,7 +667,7 @@ template <typename T, typename X> void lp_primal_core_solver<T, X>:: update_c
}
}
template <typename T, typename X> T lp_primal_core_solver<T, X>:: calculate_norm_of_entering_exactly() {
template <typename T, typename X> T lp_primal_core_solver<T, X>::calculate_norm_of_entering_exactly() {
T r = numeric_traits<T>::one();
unsigned i = this->m_m;
while (i--) {
@ -678,13 +678,13 @@ template <typename T, typename X> T lp_primal_core_solver<T, X>:: calculate_n
}
// calling it stage1 is too cryptic
template <typename T, typename X> void lp_primal_core_solver<T, X>:: find_feasible_solution() {
template <typename T, typename X> void lp_primal_core_solver<T, X>::find_feasible_solution() {
m_exit_on_feasible_solution = true;
this->snap_xN_to_bounds_and_free_columns_to_zeroes();
solve();
}
template <typename T, typename X> void lp_primal_core_solver<T, X>:: calculate_infeasibility() {
template <typename T, typename X> void lp_primal_core_solver<T, X>::calculate_infeasibility() {
m_infeasibility = zero_of_type<X>();
unsigned i = this->m_m;
while (i--) {
@ -692,7 +692,7 @@ template <typename T, typename X> void lp_primal_core_solver<T, X>:: calculat
}
}
template <typename T, typename X> void lp_primal_core_solver<T, X>:: add_column_infeasibility(unsigned j) {
template <typename T, typename X> void lp_primal_core_solver<T, X>::add_column_infeasibility(unsigned j) {
const X & x = this->m_x[j];
switch (this->m_column_type[j]) {
case fixed:
@ -718,7 +718,7 @@ template <typename T, typename X> void lp_primal_core_solver<T, X>:: add_colu
}
}
template <typename T, typename X> void lp_primal_core_solver<T, X>:: one_iteration() {
template <typename T, typename X> void lp_primal_core_solver<T, X>::one_iteration() {
this->m_total_iterations++;
unsigned number_of_benefitial_columns_to_go_over = get_number_of_non_basic_column_to_try_for_enter();
int entering = choose_entering_column(number_of_benefitial_columns_to_go_over);
@ -728,7 +728,7 @@ template <typename T, typename X> void lp_primal_core_solver<T, X>:: one_iter
advance_on_entering(entering);
}
template <typename T, typename X> void lp_primal_core_solver<T, X>:: fill_breakpoints_array(unsigned entering) {
template <typename T, typename X> void lp_primal_core_solver<T, X>::fill_breakpoints_array(unsigned entering) {
clear_breakpoints();
for (unsigned i = this->m_m; i--;)
try_add_breakpoint_in_row(i);
@ -741,7 +741,7 @@ template <typename T, typename X> void lp_primal_core_solver<T, X>:: fill_bre
}
}
template <typename T, typename X> void lp_primal_core_solver<T, X>:: try_add_breakpoint_in_row(unsigned i) {
template <typename T, typename X> void lp_primal_core_solver<T, X>::try_add_breakpoint_in_row(unsigned i) {
lean_assert(i < this->m_m);
const T & d = this->m_ed[i]; // the coefficient before m_entering in the i-th row
if (d == 0) return; // the change of x[m_entering] will not change the corresponding basis x
@ -769,12 +769,12 @@ template <typename T, typename X> void lp_primal_core_solver<T, X>:: try_add_
}
}
template <typename T, typename X> void lp_primal_core_solver<T, X>:: clear_breakpoints() {
template <typename T, typename X> void lp_primal_core_solver<T, X>::clear_breakpoints() {
m_breakpoints.clear();
m_breakpoint_indices_queue.clear();// m_breakpoints.clear();
}
template <typename T, typename X> void lp_primal_core_solver<T, X>:: change_slope_on_breakpoint(unsigned entering, breakpoint<X> * b, T & slope_at_entering) {
template <typename T, typename X> void lp_primal_core_solver<T, X>::change_slope_on_breakpoint(unsigned entering, breakpoint<X> * b, T & slope_at_entering) {
if (b->m_j == entering) {
lean_assert(b->m_type != fixed_break && (!is_zero(b->m_delta)));
slope_at_entering += m_sign_of_entering_delta;
@ -805,7 +805,7 @@ template <typename T, typename X> void lp_primal_core_solver<T, X>:: change_s
}
template <typename T, typename X> void lp_primal_core_solver<T, X>:: advance_on_sorted_breakpoints(unsigned entering) {
template <typename T, typename X> void lp_primal_core_solver<T, X>::advance_on_sorted_breakpoints(unsigned entering) {
T slope_at_entering = this->m_d[entering];
breakpoint<X> * last_bp = nullptr;
while (m_breakpoint_indices_queue.is_empty() == false) {
@ -825,13 +825,13 @@ template <typename T, typename X> void lp_primal_core_solver<T, X>:: advance_
update_basis_and_x_with_comparison(entering, last_bp->m_j, last_bp->m_delta);
}
template <typename T, typename X> void lp_primal_core_solver<T, X>:: update_basis_and_x_with_comparison(unsigned entering, unsigned leaving, X delta) {
template <typename T, typename X> void lp_primal_core_solver<T, X>::update_basis_and_x_with_comparison(unsigned entering, unsigned leaving, X delta) {
if (entering != leaving)
this->update_basis_and_x(entering, leaving, delta);
else
this->update_x(entering, delta);
}
template <typename T, typename X> bool lp_primal_core_solver<T, X>:: column_is_feasible(unsigned j) const {
template <typename T, typename X> bool lp_primal_core_solver<T, X>::column_is_feasible(unsigned j) const {
const X& x = this->m_x[j];
switch (this->m_column_type[j]) {
case fixed:
@ -866,7 +866,7 @@ template <typename T, typename X> bool lp_primal_core_solver<T, X>:: column_i
}
}
template <typename T, typename X> bool lp_primal_core_solver<T, X>:: calc_current_x_is_feasible() const {
template <typename T, typename X> bool lp_primal_core_solver<T, X>::calc_current_x_is_feasible() const {
unsigned i = this->m_m;
while (i--) {
if (!column_is_feasible(this->m_basis[i]))
@ -876,7 +876,7 @@ template <typename T, typename X> bool lp_primal_core_solver<T, X>:: calc_curren
}
template <typename T, typename X> bool lp_primal_core_solver<T, X>:: can_enter_basis(unsigned j) {
template <typename T, typename X> bool lp_primal_core_solver<T, X>::can_enter_basis(unsigned j) {
switch (this->m_column_type[j]) {
case low_bound:
lean_assert(this->x_is_at_low_bound(j));
@ -902,7 +902,7 @@ template <typename T, typename X> bool lp_primal_core_solver<T, X>:: can_ente
template <typename T, typename X> bool lp_primal_core_solver<T, X>:: done() {
template <typename T, typename X> bool lp_primal_core_solver<T, X>::done() {
if (this->m_status == OPTIMAL ||this->m_status == FLOATING_POINT_ERROR) return true;
if (this->m_status == INFEASIBLE) {
return true;
@ -918,7 +918,7 @@ template <typename T, typename X> bool lp_primal_core_solver<T, X>:: done() {
return false;
}
template <typename T, typename X> void lp_primal_core_solver<T, X>:: init_infeasibility_costs() {
template <typename T, typename X> void lp_primal_core_solver<T, X>::init_infeasibility_costs() {
lean_assert(this->m_x.size() >= this->m_n);
lean_assert(this->m_column_type.size() >= this->m_n);
// X inf = m_infeasibility;
@ -931,7 +931,7 @@ template <typename T, typename X> void lp_primal_core_solver<T, X>:: init_inf
m_using_inf_costs = true;
}
template <typename T, typename X> void lp_primal_core_solver<T, X>:: print_column(unsigned j) {
template <typename T, typename X> void lp_primal_core_solver<T, X>::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];;
switch (this->m_column_type[j]) {
case fixed:
@ -951,7 +951,7 @@ template <typename T, typename X> void lp_primal_core_solver<T, X>:: print_colum
}
}
template <typename T, typename X> void lp_primal_core_solver<T, X>:: init_infeasibility_cost_for_column(unsigned j) {
template <typename T, typename X> void lp_primal_core_solver<T, X>::init_infeasibility_cost_for_column(unsigned j) {
// we are going to maximize the cost
// When j is feasible, even at the boundary, then we set the cost of the column to zero.
const X & x = this->m_x[j];
@ -1000,14 +1000,14 @@ template <typename T, typename X> void lp_primal_core_solver<T, X>:: init_inf
}
}
template <typename T, typename X> void lp_primal_core_solver<T, X>:: add_breakpoint(unsigned j, X delta, breakpoint_type type) {
template <typename T, typename X> void lp_primal_core_solver<T, X>::add_breakpoint(unsigned j, X delta, breakpoint_type type) {
m_breakpoints.push_back(breakpoint<X>(j, delta, type));
m_breakpoint_indices_queue.enqueue(m_breakpoint_indices_queue.size(), abs(delta));
}
// j is the basic column, x is the value at x[j]
// d is the coefficient before m_entering in the row with j as the basis column
template <typename T, typename X> void lp_primal_core_solver<T, X>:: try_add_breakpoint(unsigned j, const X & x, const T & d, breakpoint_type break_type, const X & break_value) {
template <typename T, typename X> void lp_primal_core_solver<T, X>::try_add_breakpoint(unsigned j, const X & x, const T & d, breakpoint_type break_type, const X & break_value) {
X diff = x - break_value;
if (is_zero(diff)) {
switch (break_type) {
@ -1028,12 +1028,12 @@ template <typename T, typename X> void lp_primal_core_solver<T, X>:: try_add_
if (same_sign_with_entering_delta(delta_j))
add_breakpoint(j, delta_j, break_type);
}
template <typename T, typename X> void lp_primal_core_solver<T, X>:: init_costs_from_backup() {
template <typename T, typename X> void lp_primal_core_solver<T, X>::init_costs_from_backup() {
this->m_costs = m_costs_backup;
m_using_inf_costs = false;
}
template <typename T, typename X> void lp_primal_core_solver<T, X>:: init_reduced_costs() {
template <typename T, typename X> void lp_primal_core_solver<T, X>::init_reduced_costs() {
lean_assert(m_current_x_is_feasible == calc_current_x_is_feasible());
if (get_current_x_is_infeasible()) {
init_infeasibility_costs();

2
src/util/lp/lp_primal_core_solver_instances.cpp
View file

@ -7,7 +7,7 @@
#include "util/lp/lar_solver.h"
#include "util/lp/lp_primal_core_solver.cpp"
namespace lean {
// template void lar_solver::find_solution_signature_with_doubles(lar_solution_signature&);
//template void lar_solver::find_solution_signature_with_doubles(lar_solution_signature&);
template void lp_primal_core_solver<double, double>::find_feasible_solution();
template lp_primal_core_solver<double, double>::lp_primal_core_solver(static_matrix<double, double>&, std::vector<double, std::allocator<double> >&, std::vector<double, std::allocator<double> >&, std::vector<unsigned int, std::allocator<unsigned int> >&, std::vector<double, std::allocator<double> >&, std::vector<column_type, std::allocator<column_type> >&, std::vector<double, std::allocator<double> >&, lp_settings&, std::unordered_map<unsigned int, std::string, std::hash<unsigned int>, std::equal_to<unsigned int>, std::allocator<std::pair<unsigned int const, std::string> > > const&);
template lp_primal_core_solver<double, double>::lp_primal_core_solver(static_matrix<double, double>&, std::vector<double, std::allocator<double> >&, std::vector<double, std::allocator<double> >&, std::vector<unsigned int, std::allocator<unsigned int> >&, std::vector<double, std::allocator<double> >&, std::vector<column_type, std::allocator<column_type> >&, std::vector<double, std::allocator<double> >&, std::vector<double, std::allocator<double> >&, lp_settings&, std::unordered_map<unsigned int, std::string, std::hash<unsigned int>, std::equal_to<unsigned int>, std::allocator<std::pair<unsigned int const, std::string> > > const&);

30
src/util/lp/lp_primal_simplex.cpp
View file

@ -7,7 +7,7 @@
#include "util/lp/lp_primal_simplex.h"
namespace lean {
template <typename T, typename X> void lp_primal_simplex<T, X>:: fill_costs_and_x_for_first_stage_solver(unsigned original_number_of_columns) {
template <typename T, typename X> void lp_primal_simplex<T, X>::fill_costs_and_x_for_first_stage_solver(unsigned original_number_of_columns) {
unsigned slack_var = original_number_of_columns;
unsigned artificial = original_number_of_columns + this->m_slacks;
@ -16,7 +16,7 @@ template <typename T, typename X> void lp_primal_simplex<T, X>:: fill_costs_and_
}
}
template <typename T, typename X> void lp_primal_simplex<T, X>:: init_buffer(unsigned k, std::vector<T> & r) {
template <typename T, typename X> void lp_primal_simplex<T, X>::init_buffer(unsigned k, std::vector<T> & r) {
for (unsigned i = 0; i < k; i++) {
r[i] = 0;
}
@ -26,21 +26,21 @@ template <typename T, typename X> void lp_primal_simplex<T, X>:: init_buffer(uns
}
}
template <typename T, typename X> void lp_primal_simplex<T, X>:: refactor() {
template <typename T, typename X> void lp_primal_simplex<T, X>::refactor() {
m_core_solver->init_lu();
if (m_core_solver->factorization()->get_status() != LU_status::OK) {
throw exception("cannot refactor");
}
}
template <typename T, typename X> void lp_primal_simplex<T, X>:: set_scaled_costs() {
template <typename T, typename X> void lp_primal_simplex<T, X>::set_scaled_costs() {
unsigned j = this->number_of_core_structurals();
while (j-- > 0) {
this->set_scaled_cost(j);
}
}
template <typename T, typename X> void lp_primal_simplex<T, X>:: stage_two() {
template <typename T, typename X> void lp_primal_simplex<T, X>::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;
@ -62,7 +62,7 @@ template <typename T, typename X> column_info<T> * lp_primal_simplex<T, X>::
return (it == this->m_columns.end())? ( this->m_columns[column] = new column_info<T>) : it->second;
}
template <typename T, typename X> void lp_primal_simplex<T, X>:: fill_acceptable_values_for_x() {
template <typename T, typename X> void lp_primal_simplex<T, X>::fill_acceptable_values_for_x() {
for (auto t : this->m_core_solver_columns_to_external_columns) {
this->m_x[t.first] = numeric_traits<T>::zero();
lean_assert(this->m_x[t.first] >= 0);
@ -70,12 +70,12 @@ template <typename T, typename X> void lp_primal_simplex<T, X>:: fill_acceptable
}
template <typename T, typename X> void lp_primal_simplex<T, X>:: set_zero_bound(bool * bound_is_set, T * bounds, unsigned i) {
template <typename T, typename X> void lp_primal_simplex<T, X>::set_zero_bound(bool * bound_is_set, T * bounds, unsigned i) {
bound_is_set[i] = true;
bounds[i] = numeric_traits<T>::zero();
}
template <typename T, typename X> void lp_primal_simplex<T, X>:: fill_costs_and_x_for_first_stage_solver_for_row(
template <typename T, typename X> void lp_primal_simplex<T, X>::fill_costs_and_x_for_first_stage_solver_for_row(
int row,
unsigned & slack_var,
unsigned & artificial) {
@ -113,7 +113,7 @@ template <typename T, typename X> void lp_primal_simplex<T, X>:: fill_costs_and_
this->m_x[artificial] = rs;
artificial++;
} else {
// we can put a slack_var into the basis, and atemplate <typename T, typename X> void lp_primal_simplex<T, X>:: adding an artificial variable
// we can put a slack_var into the basis, and atemplate <typename T, typename X> void lp_primal_simplex<T, X>::adding an artificial variable
this->m_basis[row] = slack_var;
this->m_x[slack_var] = - rs;
}
@ -133,7 +133,7 @@ template <typename T, typename X> void lp_primal_simplex<T, X>:: fill_costs_and_
this->m_x[artificial] = - rs;
this->m_basis[row] = artificial++;
} else {
// we can put slack_var into the basis, and atemplate <typename T, typename X> void lp_primal_simplex<T, X>:: adding an artificial variable
// we can put slack_var into the basis, and atemplate <typename T, typename X> void lp_primal_simplex<T, X>::adding an artificial variable
this->m_basis[row] = slack_var;
this->m_x[slack_var] = rs;
}
@ -154,7 +154,7 @@ template <typename T, typename X> std::string lp_primal_simplex<T, X>::name_o
}
template <typename T, typename X> void lp_primal_simplex<T, X>:: set_core_solver_bounds() {
template <typename T, typename X> void lp_primal_simplex<T, X>::set_core_solver_bounds() {
unsigned total_vars = this->m_A->column_count() + this->m_slacks + this->m_artificials;
this->m_column_types.resize(total_vars);
this->m_upper_bounds.resize(total_vars);
@ -177,7 +177,7 @@ template <typename T, typename X> void lp_primal_simplex<T, X>:: set_core_solver
}
template <typename T, typename X> void lp_primal_simplex<T, X>:: find_maximal_solution() {
template <typename T, typename X> void lp_primal_simplex<T, X>::find_maximal_solution() {
int preprocessing_start_time = get_millisecond_count();
if (this->problem_is_empty()) {
this->m_status = lp_status::EMPTY;
@ -199,12 +199,12 @@ template <typename T, typename X> void lp_primal_simplex<T, X>:: find_maximal_so
solve_with_total_inf();
}
template <typename T, typename X> void lp_primal_simplex<T, X>:: fill_A_x_and_basis_for_stage_one_total_inf() {
template <typename T, typename X> void lp_primal_simplex<T, X>::fill_A_x_and_basis_for_stage_one_total_inf() {
for (unsigned row = 0; row < this->row_count(); row++)
fill_A_x_and_basis_for_stage_one_total_inf_for_row(row);
}
template <typename T, typename X> void lp_primal_simplex<T, X>:: fill_A_x_and_basis_for_stage_one_total_inf_for_row(unsigned row) {
template <typename T, typename X> void lp_primal_simplex<T, X>::fill_A_x_and_basis_for_stage_one_total_inf_for_row(unsigned row) {
lean_assert(row < this->row_count());
auto ext_row_it = this->m_core_solver_rows_to_external_rows.find(row);
lean_assert(ext_row_it != this->m_core_solver_rows_to_external_rows.end());
@ -239,7 +239,7 @@ template <typename T, typename X> void lp_primal_simplex<T, X>:: fill_A_x_and_ba
}
}
template <typename T, typename X> void lp_primal_simplex<T, X>:: solve_with_total_inf() {
template <typename T, typename X> void lp_primal_simplex<T, X>::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();

2
src/util/lp/lu.cpp
View file

@ -221,7 +221,7 @@ void lu<T, X>::solve_Bd(unsigned a_column, std::vector<T> & d, indexed_vector<T>
}
template <typename T, typename X>
void lu<T, X>:: solve_yB_internal(std::vector<T>& y) {
void lu<T, X>::solve_yB_internal(std::vector<T>& y) {
// first solve yU = cb*R(-1)
m_R.apply_reverse_from_right(y); // got y = cb*R(-1)
m_U.solve_y_U(y); // got y*U=cb*R(-1)

32
src/util/lp/permutation_matrix.cpp
View file

@ -42,8 +42,8 @@ template <typename T, typename X> void permutation_matrix<T, X>::print() const {
}
#endif
template <typename T, typename X> template <typename L>
void permutation_matrix<T, X>:: apply_from_left_perm(std::vector<L> & w) {
template <typename T, typename X>template <typename L>
void permutation_matrix<T, X>::apply_from_left_perm(std::vector<L> & w) {
#ifdef LEAN_DEBUG
// dense_matrix<L, X> deb(*this);
// L * deb_w = clone_vector<L>(w, row_count());
@ -64,8 +64,8 @@ void permutation_matrix<T, X>:: apply_from_left_perm(std::vector<L> & w) {
#endif
}
template <typename T, typename X> template <typename L>
void permutation_matrix<T, X>:: apply_from_left_perm(indexed_vector<L> & w, lp_settings &) {
template <typename T, typename X>template <typename L>
void permutation_matrix<T, X>::apply_from_left_perm(indexed_vector<L> & w, lp_settings &) {
#ifdef LEAN_DEBUG
// dense_matrix<T, L> deb(*this);
// T * deb_w = clone_vector<T>(w.m_data, row_count());
@ -89,7 +89,7 @@ void permutation_matrix<T, X>:: apply_from_left_perm(indexed_vector<L> & w, lp_s
}
template <typename T, typename X> void permutation_matrix<T, X>:: apply_from_right(std::vector<T> & w) {
template <typename T, typename X> void permutation_matrix<T, X>::apply_from_right(std::vector<T> & w) {
#ifdef LEAN_DEBUG
// dense_matrix<T, X> deb(*this);
// T * deb_w = clone_vector<T>(w, row_count());
@ -110,8 +110,8 @@ template <typename T, typename X> void permutation_matrix<T, X>:: apply_from_rig
#endif
}
template <typename T, typename X> template <typename L>
void permutation_matrix<T, X>:: copy_aside(std::vector<L> & t, std::vector<unsigned> & tmp_index, indexed_vector<L> & w) {
template <typename T, typename X> template <typename L>
void permutation_matrix<T, X>::copy_aside(std::vector<L> & t, std::vector<unsigned> & tmp_index, indexed_vector<L> & w) {
for (unsigned i = t.size(); i > 0;) {
i--;
unsigned j = w.m_index[i];
@ -120,8 +120,8 @@ void permutation_matrix<T, X>:: copy_aside(std::vector<L> & t, std::vector<unsig
}
}
template <typename T, typename X> template <typename L>
void permutation_matrix<T, X>:: clear_data(indexed_vector<L> & w) {
template <typename T, typename X> template <typename L>
void permutation_matrix<T, X>::clear_data(indexed_vector<L> & w) {
// clear old non-zeroes
for (unsigned i = w.m_index.size(); i > 0;) {
i--;
@ -130,7 +130,7 @@ void permutation_matrix<T, X>:: clear_data(indexed_vector<L> & w) {
}
}
template <typename T, typename X> template <typename L>
template <typename T, typename X>template <typename L>
void permutation_matrix<T, X>::apply_reverse_from_left(indexed_vector<L> & w) {
// the result will be w = p(-1) * w
#ifdef LEAN_DEBUG
@ -157,7 +157,7 @@ void permutation_matrix<T, X>::apply_reverse_from_left(indexed_vector<L> & w) {
#endif
}
template <typename T, typename X> template <typename L>
template <typename T, typename X>template <typename L>
void permutation_matrix<T, X>::apply_reverse_from_left(std::vector<L> & w) {
// the result will be w = p(-1) * w
#ifdef LEAN_DEBUG
@ -179,8 +179,8 @@ void permutation_matrix<T, X>::apply_reverse_from_left(std::vector<L> & w) {
#endif
}
template <typename T, typename X> template <typename L>
void permutation_matrix<T, X>:: apply_reverse_from_right(std::vector<L> & w) {
template <typename T, typename X>template <typename L>
void permutation_matrix<T, X>::apply_reverse_from_right(std::vector<L> & w) {
// the result will be w = w * p(-1)
#ifdef LEAN_DEBUG
// dense_matrix<T, X> deb(get_reverse());
@ -202,7 +202,7 @@ void permutation_matrix<T, X>:: apply_reverse_from_right(std::vector<L> & w) {
#endif
}
template <typename T, typename X> void permutation_matrix<T, X>:: transpose_from_left(unsigned i, unsigned j) {
template <typename T, typename X> void permutation_matrix<T, X>::transpose_from_left(unsigned i, unsigned j) {
// the result will be this = (i,j)*this
lean_assert(i < m_length && j < m_length && i != j);
auto pi = m_rev[i];
@ -211,7 +211,7 @@ template <typename T, typename X> void permutation_matrix<T, X>:: transpose_from
set_val(pj, i);
}
template <typename T, typename X> void permutation_matrix<T, X>:: transpose_from_right(unsigned i, unsigned j) {
template <typename T, typename X> void permutation_matrix<T, X>::transpose_from_right(unsigned i, unsigned j) {
// the result will be this = this * (i,j)
lean_assert(i < m_length && j < m_length && i != j);
auto pi = m_permutation[i];
@ -256,7 +256,7 @@ template <typename T, typename X> void permutation_matrix<T, X>::multiply_by_rev
delete clone;
}
template <typename T, typename X> void permutation_matrix<T, X>:: multiply_by_permutation_reverse_from_left(permutation_matrix<T, X> & r){ // todo : condensed permutations?
template <typename T, typename X> void permutation_matrix<T, X>::multiply_by_permutation_reverse_from_left(permutation_matrix<T, X> & r){ // todo : condensed permutations?
// the result is this = r(-1)*this
auto clone = clone_m_permutation();
// the result is this = this*q(-1)

10
src/util/lp/row_eta_matrix.cpp
View file

@ -47,7 +47,7 @@ template <typename T, typename X>
lean_assert(check_vector_for_small_values(w, settings));
}
template <typename T, typename X>
template <typename T, typename X>
void row_eta_matrix<T, X>::apply_from_left_local_to_X(indexed_vector<X> & w, lp_settings & settings) {
auto w_at_row = w[m_row];
bool was_zero_at_m_row = is_zero(w_at_row);
@ -69,7 +69,7 @@ template <typename T, typename X>
lean_assert(check_vector_for_small_values(w, settings));
}
template <typename T, typename X>
template <typename T, typename X>
void row_eta_matrix<T, X>::apply_from_right(std::vector<T> & w) {
T w_row = w[m_row];
if (numeric_traits<T>::is_zero(w_row)) return;
@ -87,7 +87,7 @@ template <typename T, typename X>
#endif
}
template <typename T, typename X>
template <typename T, typename X>
void row_eta_matrix<T, X>::apply_from_right(indexed_vector<T> & w) {
T w_row = w[m_row];
if (numeric_traits<T>::is_zero(w_row)) return;
@ -118,7 +118,7 @@ template <typename T, typename X>
#endif
}
template <typename T, typename X>
template <typename T, typename X>
void row_eta_matrix<T, X>::conjugate_by_permutation(permutation_matrix<T, X> & p) {
// this = p * this * p(-1)
#ifdef LEAN_DEBUG
@ -138,7 +138,7 @@ template <typename T, typename X>
#endif
}
#ifdef LEAN_DEBUG
template <typename T, typename X>
template <typename T, typename X>
T row_eta_matrix<T, X>::get_elem(unsigned row, unsigned col) const {
if (row == m_row){
if (col == row) {

2092
src/util/lp/sparse_matrix.cpp
View file

File diff suppressed because it is too large Load diff

18
src/util/lp/sparse_matrix_instances.cpp
View file

@ -7,14 +7,14 @@
#include "util/lp/lu.h"
#include "util/lp/sparse_matrix.cpp"
namespace lean {
template double sparse_matrix<double, double>::dot_product_with_row<double>(unsigned int, std::vector<double> const&) const;
template void sparse_matrix<double, double>::add_new_element(unsigned int, unsigned int, double);
template void sparse_matrix<double, double>::divide_row_by_constant(unsigned int, double&, lp_settings&);
template void sparse_matrix<double, double>::fill_eta_matrix(unsigned int, eta_matrix<double, double>**);
template const double & sparse_matrix<double, double>::get(unsigned int, unsigned int) const;
template unsigned sparse_matrix<double, double>::get_number_of_nonzeroes() const;
template unsigned sparse_matrix<double, double>::get_number_of_nonzeroes_below_row(unsigned int) const;
template bool sparse_matrix<double, double>::get_pivot_for_column(unsigned int&, unsigned int&, double const&, unsigned int);
template double sparse_matrix<double, double>::dot_product_with_row<double>(unsigned int, std::vector<double> const&) const;
template void sparse_matrix<double, double>::add_new_element(unsigned int, unsigned int, double);
template void sparse_matrix<double, double>::divide_row_by_constant(unsigned int, double&, lp_settings&);
template void sparse_matrix<double, double>::fill_eta_matrix(unsigned int, eta_matrix<double, double>**);
template const double & sparse_matrix<double, double>::get(unsigned int, unsigned int) const;
template unsigned sparse_matrix<double, double>::get_number_of_nonzeroes() const;
template unsigned sparse_matrix<double, double>::get_number_of_nonzeroes_below_row(unsigned int) const;
template bool sparse_matrix<double, double>::get_pivot_for_column(unsigned int&, unsigned int&, double const&, unsigned int);
template unsigned sparse_matrix<double, double>::lowest_row_in_column(unsigned int);
template bool sparse_matrix<double, double>::pivot_row_to_row(unsigned int, double, unsigned int, lp_settings&);
template bool sparse_matrix<double, double>::pivot_with_eta(unsigned int, eta_matrix<double, double>*, lp_settings&);
@ -70,7 +70,7 @@ template sparse_matrix<mpq, numeric_pair<mpq>>::sparse_matrix(static_matrix<mpq,
template void sparse_matrix<double, double>::double_solve_U_y<double>(std::vector<double>&);
template void sparse_matrix<mpq, mpq>::double_solve_U_y<mpq>(std::vector<mpq>&);
template void sparse_matrix<mpq, numeric_pair<mpq>>::double_solve_U_y<mpq>(std::vector<mpq>&);
template void sparse_matrix<mpq, numeric_pair<mpq> >::double_solve_U_y<numeric_pair<mpq> >(std::vector<numeric_pair<mpq>>&);
template void sparse_matrix<mpq, numeric_pair<mpq> >::double_solve_U_y<numeric_pair<mpq> >(std::vector<numeric_pair<mpq>>&);
/////////////////////
/*

2
src/util/lp/square_dense_submatrix.cpp
View file

@ -286,7 +286,7 @@ void square_dense_submatrix<T, X>::apply_from_left_to_vector(std::vector<L> & w)
#endif
}
template <typename T, typename X> bool square_dense_submatrix<T, X>::is_L_matrix() const {
template <typename T, typename X> bool square_dense_submatrix<T, X>::is_L_matrix() const {
#ifdef LEAN_DEBUG
lean_assert(m_row_permutation.is_identity());
for (unsigned i = 0; i < m_parent->dimension(); i++) {

63
src/util/lp/static_matrix.cpp
View file

@ -33,7 +33,7 @@ static_matrix<T, X>::static_matrix(static_matrix const &A, unsigned * basis) :
}
}
template <typename T, typename X> void static_matrix<T, X>:: clear() {
template <typename T, typename X> void static_matrix<T, X>::clear() {
m_work_pivot_vector.clear();
m_rows.clear();
m_columns.clear();
@ -42,11 +42,11 @@ template <typename T, typename X> void static_matrix<T, X>:: clear() {
#endif
}
template <typename T, typename X> void static_matrix<T, X>:: init_work_pivot_vector(unsigned m) {
template <typename T, typename X> void static_matrix<T, X>::init_work_pivot_vector(unsigned m) {
while (m--) m_work_pivot_vector.push_back(numeric_traits<T>::zero());
}
template <typename T, typename X> void static_matrix<T, X>:: init_empty_matrix(unsigned m, unsigned n) {
template <typename T, typename X> void static_matrix<T, X>::init_empty_matrix(unsigned m, unsigned n) {
init_work_pivot_vector(m);
init_row_columns(m, n);
}
@ -61,7 +61,7 @@ template <typename L>
return ret;
};
template <typename T, typename X> unsigned static_matrix<T, X>:: lowest_row_in_column(unsigned col) {
template <typename T, typename X> unsigned static_matrix<T, X>::lowest_row_in_column(unsigned col) {
lean_assert(col < column_count());
column_strip & colstrip = m_columns[col];
lean_assert(colstrip.size() > 0);
@ -74,7 +74,7 @@ template <typename T, typename X> unsigned static_matrix<T, X>:: lowest_row_i
return ret;
}
template <typename T, typename X> T static_matrix<T, X>:: dot_product_with_column(const std::vector<T> & y, unsigned j) const {
template <typename T, typename X> T static_matrix<T, X>::dot_product_with_column(const std::vector<T> & y, unsigned j) const {
lean_assert(j < column_count());
T ret = numeric_traits<T>::zero();
for (auto & it : m_columns[j]) {
@ -83,12 +83,12 @@ template <typename T, typename X> T static_matrix<T, X>:: dot_product_with_co
return ret;
}
template <typename T, typename X> void static_matrix<T, X>:: add_columns_at_the_end(unsigned delta) {
template <typename T, typename X> void static_matrix<T, X>::add_columns_at_the_end(unsigned delta) {
for (unsigned i = 0; i < delta; i++)
add_column();
}
template <typename T, typename X> void static_matrix<T, X>:: forget_last_columns(unsigned how_many_to_forget) {
template <typename T, typename X> void static_matrix<T, X>::forget_last_columns(unsigned how_many_to_forget) {
lean_assert(m_columns.size() >= how_many_to_forget);
unsigned j = column_count() - 1;
for (; how_many_to_forget > 0; how_many_to_forget--) {
@ -96,7 +96,7 @@ template <typename T, typename X> void static_matrix<T, X>:: forget_last_colu
}
}
template <typename T, typename X> void static_matrix<T, X>:: remove_last_column(unsigned j) {
template <typename T, typename X> void static_matrix<T, X>::remove_last_column(unsigned j) {
column_strip & col = m_columns.back();
for (auto & it : col) {
auto & row = m_rows[it.m_i];
@ -113,7 +113,7 @@ template <typename T, typename X> void static_matrix<T, X>:: remove_last_colu
}
template <typename T, typename X>
void static_matrix<T, X>:: scale_row(unsigned row, T const & alpha) {
void static_matrix<T, X>::scale_row(unsigned row, T const & alpha) {
for (auto & t : m_rows[row]) {
t.set_val(t.get_val() * alpha);
m_columns[t.m_j][t.m_offset].m_value *= alpha;
@ -121,7 +121,7 @@ void static_matrix<T, X>:: scale_row(unsigned row, T const & alpha) {
}
template <typename T, typename X>
void static_matrix<T, X>:: divide_row_by_constant(unsigned row, T const & alpha) {
void static_matrix<T, X>::divide_row_by_constant(unsigned row, T const & alpha) {
for (auto & t : m_rows[row]) {
t.set_val(t.get_val() / alpha);
m_columns[t.m_j][t.m_offset].m_value /= alpha;
@ -129,7 +129,7 @@ void static_matrix<T, X>:: divide_row_by_constant(unsigned row, T const & alpha)
}
template <typename T, typename X>
void static_matrix<T, X>:: scale_column(unsigned column, T const & alpha) {
void static_matrix<T, X>::scale_column(unsigned column, T const & alpha) {
for (auto & t : m_columns[column]) {
t.m_value *= alpha;
auto & r = m_rows[t.m_i][t.m_offset];
@ -138,7 +138,7 @@ void static_matrix<T, X>:: scale_column(unsigned column, T const & alpha) {
}
#ifdef LEAN_DEBUG
template <typename T, typename X> void static_matrix<T, X>:: regen_domain() {
template <typename T, typename X> void static_matrix<T, X>::regen_domain() {
m_domain.clear();
for (int i = 0; i < m_rows.size(); i++){
for (auto & t : m_rows[i]) {
@ -148,7 +148,7 @@ template <typename T, typename X> void static_matrix<T, X>:: regen_domain() {
}
#endif
template <typename T, typename X> void static_matrix<T, X>:: set(unsigned row, unsigned col, T const & val) {
template <typename T, typename X> void static_matrix<T, X>::set(unsigned row, unsigned col, T const & val) {
if (numeric_traits<T>::is_zero(val)) return;
lean_assert(row < row_count() && col < column_count());
#ifdef LEAN_DEBUG
@ -174,14 +174,15 @@ std::set<pair<unsigned, unsigned>> static_matrix<T, X>::get_domain() {
}
template <typename T, typename X> void static_matrix<T, X>:: copy_column_to_vector (unsigned j, indexed_vector<T> & v) const {
template <typename T, typename X> void static_matrix<T, X>::copy_column_to_vector (unsigned j, indexed_vector<T> & v) const {
lean_assert(j < m_columns.size());
for (auto & it : m_columns[j]) {
if (!is_zero(it.m_value))
v.set_value(it.m_value, it.m_i);
}
}
template <typename T, typename X> void static_matrix<T, X>:: copy_column_to_vector (unsigned j, std::vector<T> & v) const {
template <typename T, typename X> void static_matrix<T, X>::copy_column_to_vector (unsigned j, std::vector<T> & v) const {
v.resize(row_count(), numeric_traits<T>::zero());
for (auto & it : m_columns[j]) {
if (!is_zero(it.m_value))
@ -189,13 +190,13 @@ template <typename T, typename X> void static_matrix<T, X>:: copy_column_to_v
}
}
template <typename T, typename X> void static_matrix<T, X>:: add_column_to_vector (const T & a, unsigned j, T * v) const {
template <typename T, typename X> void static_matrix<T, X>::add_column_to_vector (const T & a, unsigned j, T * v) const {
for (auto & it : m_columns[j]) {
v[it.m_i] += a * it.m_value;
}
}
template <typename T, typename X> T static_matrix<T, X>:: get_max_abs_in_row(unsigned row) const {
template <typename T, typename X> T static_matrix<T, X>::get_max_abs_in_row(unsigned row) const {
T ret = numeric_traits<T>::zero();
for (auto & t : m_rows[row]) {
T a = abs(t.get_val());
@ -206,7 +207,7 @@ template <typename T, typename X> T static_matrix<T, X>:: get_max_abs_in_row(
return ret;
}
template <typename T, typename X> T static_matrix<T, X>:: get_min_abs_in_row(unsigned row) const {
template <typename T, typename X> T static_matrix<T, X>::get_min_abs_in_row(unsigned row) const {
bool first_time = true;
T ret = numeric_traits<T>::zero();
for (auto & t : m_rows[row]) {
@ -222,7 +223,7 @@ template <typename T, typename X> T static_matrix<T, X>:: get_min_abs_in_row(
}
template <typename T, typename X> T static_matrix<T, X>:: get_max_abs_in_column(unsigned column) const {
template <typename T, typename X> T static_matrix<T, X>::get_max_abs_in_column(unsigned column) const {
T ret = numeric_traits<T>::zero();
for (auto & t : m_columns[column]) {
T a = abs(t.m_value);
@ -233,7 +234,7 @@ template <typename T, typename X> T static_matrix<T, X>:: get_max_abs_in_colu
return ret;
}
template <typename T, typename X> T static_matrix<T, X>:: get_min_abs_in_column(unsigned column) const {
template <typename T, typename X> T static_matrix<T, X>::get_min_abs_in_column(unsigned column) const {
bool first_time = true;
T ret = numeric_traits<T>::zero();
for (auto & t : m_columns[column]) {
@ -249,7 +250,7 @@ template <typename T, typename X> T static_matrix<T, X>:: get_min_abs_in_col
}
#ifdef LEAN_DEBUG
template <typename T, typename X> void static_matrix<T, X>:: check_consistency() {
template <typename T, typename X> void static_matrix<T, X>::check_consistency() {
std::unordered_map<std::pair<unsigned, unsigned>, T> by_rows;
for (int i = 0; i < m_rows.size(); i++){
for (auto & t : m_rows[i]) {
@ -281,7 +282,7 @@ template <typename T, typename X> void static_matrix<T, X>:: check_consistenc
#endif
template <typename T, typename X> void static_matrix<T, X>:: cross_out_row(unsigned k) {
template <typename T, typename X> void static_matrix<T, X>::cross_out_row(unsigned k) {
#ifdef LEAN_DEBUG
check_consistency();
#endif
@ -295,7 +296,7 @@ template <typename T, typename X> void static_matrix<T, X>:: cross_out_row(un
}
template <typename T, typename X> void static_matrix<T, X>:: fix_row_indices_in_each_column_for_crossed_row(unsigned k) {
template <typename T, typename X> void static_matrix<T, X>::fix_row_indices_in_each_column_for_crossed_row(unsigned k) {
for (unsigned j = 0; j < m_columns.size(); j++) {
auto & col = m_columns[j];
for (int i = 0; i < col.size(); i++) {
@ -306,13 +307,13 @@ template <typename T, typename X> void static_matrix<T, X>:: fix_row_indices_
}
}
template <typename T, typename X> void static_matrix<T, X>:: cross_out_row_from_columns(unsigned k, row_strip & row) {
template <typename T, typename X> void static_matrix<T, X>::cross_out_row_from_columns(unsigned k, row_strip & row) {
for (auto & t : row) {
cross_out_row_from_column(t.m_j, k);
}
}
template <typename T, typename X> void static_matrix<T, X>:: cross_out_row_from_column(unsigned col, unsigned k) {
template <typename T, typename X> void static_matrix<T, X>::cross_out_row_from_column(unsigned col, unsigned k) {
auto & s = m_columns[col];
for (unsigned i = 0; i < s.size(); i++) {
if (s[i].m_i == k) {
@ -322,7 +323,7 @@ template <typename T, typename X> void static_matrix<T, X>:: cross_out_row_fr
}
}
template <typename T, typename X> T static_matrix<T, X>:: get_elem(unsigned i, unsigned j) const { // should not be used in efficient code !!!!
template <typename T, typename X> T static_matrix<T, X>::get_elem(unsigned i, unsigned j) const { // should not be used in efficient code !!!!
for (auto & t : m_rows[i]) {
if (t.m_j == j) {
return t.get_val();
@ -332,20 +333,20 @@ template <typename T, typename X> T static_matrix<T, X>:: get_elem(unsigned i
}
template <typename T, typename X> void static_matrix<T, X>:: scan_row_to_work_vector(unsigned i) {
template <typename T, typename X> void static_matrix<T, X>::scan_row_to_work_vector(unsigned i) {
for (auto & rc : m_rows[i]) {
m_work_pivot_vector[rc.m_j] = rc.get_val();
}
}
template <typename T, typename X> void static_matrix<T, X>:: clean_row_work_vector(unsigned i) {
template <typename T, typename X> void static_matrix<T, X>::clean_row_work_vector(unsigned i) {
for (auto & rc : m_rows[i]) {
m_work_pivot_vector[rc.m_j] = numeric_traits<T>::zero();
}
}
template <typename T, typename X> T static_matrix<T, X>:: get_balance() const {
template <typename T, typename X> T static_matrix<T, X>::get_balance() const {
T ret = zero_of_type<T>();
for (unsigned i = 0; i < row_count(); i++) {
ret += get_row_balance(i);
@ -353,7 +354,7 @@ template <typename T, typename X> T static_matrix<T, X>:: get_balance() const
return ret;
}
template <typename T, typename X> T static_matrix<T, X>:: get_row_balance(unsigned row) const {
template <typename T, typename X> T static_matrix<T, X>::get_row_balance(unsigned row) const {
T ret = zero_of_type<T>();
for (auto & t : m_rows[row]) {
if (numeric_traits<T>::is_zero(t.get_val())) continue;
@ -364,7 +365,7 @@ template <typename T, typename X> T static_matrix<T, X>:: get_row_balance(uns
return ret;
}
#ifdef LEAN_DEBUG
template <typename T, typename X> bool static_matrix<T, X>:: col_val_equal_to_row_val() const {
template <typename T, typename X> bool static_matrix<T, X>::col_val_equal_to_row_val() const {
for (auto & r : m_rows) {
for (auto & rc : r) {
lean_assert(rc.get_val() == m_columns[rc.m_j][rc.m_offset].m_value);