max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

dev(lp): speed up primal with sorted list

Browse source 
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
This commit is contained in:
Lev Nachmanson 2016-02-03 16:45:51 -08:00 • committed by Leonardo de Moura
parent ff8213a6a9
commit a7e3befd21
56 changed files with 219 additions and 132 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/tests/util/lp/lp.cpp
View file

@ -221,7 +221,7 @@ void test_small_lu(lp_settings & settings) {
l.change_basis(3, 2);
cout << "we were factoring " << std::endl;
#ifdef LEAN_DEBUG
print_matrix(get_B(l),std::cout);
print_matrix(get_B(l), std::cout);
#endif
lean_assert(l.is_correct());
}
@ -2082,7 +2082,7 @@ int my_readdir(DIR *dirp, struct dirent *
#endif
, struct dirent **result) {
#ifdef LEAN_WINDOWS
*result = readdir(dirp);
*result = readdir(dirp); // NOLINT
return *result != nullptr? 0 : 1;
#else
return readdir_r(dirp, entry, result);

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

@ -4,6 +4,7 @@
Author: Lev Nachmanson
*/
#include <vector>
#include "util/lp/binary_heap_priority_queue.h"
namespace lean {
// is is the child place in heap
@ -190,5 +191,5 @@ template <typename T> void binary_heap_priority_queue<T>::print(std::ostream & o
for (int i = 0; i < index.size(); i++)
enqueue(index[i], prs[i]);
}
#endif
#endif
}

2
src/util/lp/binary_heap_priority_queue.h
View file

@ -40,7 +40,7 @@ public:
void put_to_heap(unsigned i, unsigned o);
void enqueue_new(unsigned o, const T& priority);
// This method can work with an element that is already in the queue.
// In this case the priority will be changed and the queue adjusted.
void enqueue(unsigned o, const T & priority);

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

@ -5,7 +5,7 @@
Author: Lev Nachmanson
*/
#include <set>
#include "util/lp/binary_heap_upair_queue.h"
namespace lean {
template <typename T> binary_heap_upair_queue<T>::binary_heap_upair_queue(unsigned size) : m_q(size), m_pairs(size) {

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

@ -4,6 +4,8 @@
Author: Lev Nachmanson
*/
#include <string>
#include <algorithm>
#include "util/lp/lp_core_solver_base.h"
#include "util/lp/core_solver_pretty_printer.h"
namespace lean {

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

@ -5,15 +5,16 @@
Author: Lev Nachmanson
*/
#ifdef LEAN_DEBUG
#include <vector>
#include "util/lp/dense_matrix.h"
namespace lean {
template <typename T, typename X> dense_matrix<T,X>::dense_matrix(unsigned m, unsigned n) : m_m(m), m_n(n) {
template <typename T, typename X> dense_matrix<T, X>::dense_matrix(unsigned m, unsigned n) : m_m(m), m_n(n) {
m_values = new T[m * n];
for (unsigned i = 0; i < m * n; i ++)
m_values[i] = numeric_traits<T>::zero();
}
template <typename T, typename X> dense_matrix<T,X> dense_matrix<T,X>::operator*=(matrix<T, X> const & a){
template <typename T, typename X> dense_matrix<T, X> dense_matrix<T, X>::operator*=(matrix<T, X> const & a) {
lean_assert(column_count() == a.row_count());
dense_matrix c(row_count(), a.column_count());
for (unsigned i = 0; i < row_count(); i++) {
@ -28,8 +29,8 @@ 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>&
dense_matrix<T,X>::operator=(matrix<T, X> const & other){
template <typename T, typename X> dense_matrix<T, X>&
dense_matrix<T, X>::operator=(matrix<T, X> const & other){
if ( this == & other)
return *this;
m_values = new T[m_m * m_n];
@ -39,8 +40,8 @@ dense_matrix<T,X>::operator=(matrix<T, X> const & other){
return *this;
}
template <typename T, typename X> dense_matrix<T,X>&
dense_matrix<T,X>::operator=(dense_matrix const & other){
template <typename T, typename X> dense_matrix<T, X>&
dense_matrix<T, X>::operator=(dense_matrix const & other){
if ( this == & other)
return *this;
m_m = other.m_m;
@ -53,14 +54,14 @@ dense_matrix<T,X>::operator=(dense_matrix const & other){
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];

1
src/util/lp/dense_matrix.h
View file

@ -6,6 +6,7 @@
*/
#pragma once
#ifdef LEAN_DEBUG
#include <vector>
#include "util/numerics/double.h"
#include "util/lp/matrix.h"
namespace lean {

3
src/util/lp/dense_matrix_instances.cpp
View file

@ -5,9 +5,10 @@
Author: Lev Nachmanson
*/
#ifdef LEAN_DEBUG
#include <vector>
#include "util/lp/dense_matrix.cpp"
template lean::dense_matrix<double, double> lean::operator*<double, double>(lean::matrix<double, double>&, lean::matrix<double, double>&);
template void lean::dense_matrix<double, double>::apply_from_left(std::vector<double, std::allocator<double> >&);
template void lean::dense_matrix<double, double>::apply_from_left(std::vector<double> &);
template lean::dense_matrix<double, double>::dense_matrix(lean::matrix<double, double> const&);
template lean::dense_matrix<double, double>::dense_matrix(unsigned int, unsigned int);
template lean::dense_matrix<double, double>& lean::dense_matrix<double, double>::operator=(lean::dense_matrix<double, double> const&);

4
src/util/lp/eta_matrix.cpp
View file

@ -15,7 +15,7 @@ template <typename T, typename X>
void eta_matrix<T, X>::apply_from_left(std::vector<X> & w, lp_settings & ) {
auto w_at_column_index = w[m_column_index];
w[m_column_index] /= m_diagonal_element;
for (auto & it: m_column_vector.m_data) {
for (auto & it : m_column_vector.m_data) {
w[it.first] += w_at_column_index * it.second;
}
}
@ -57,7 +57,7 @@ void eta_matrix<T, X>::apply_from_right(std::vector<T> & w) {
// deb.apply_from_right(clone_w);
#endif
T t = w[m_column_index] / m_diagonal_element;
for (auto & it :m_column_vector.m_data) {
for (auto & it : m_column_vector.m_data) {
t += w[it.first] * it.second;
}
w[m_column_index] = t;

4
src/util/lp/eta_matrix_instances.cpp
View file

@ -4,6 +4,8 @@
Author: Lev Nachmanson
*/
#include <memory>
#include <vector>
#include "util/lp/numeric_pair.h"
#include "util/lp/eta_matrix.cpp"
#ifdef LEAN_DEBUG
@ -18,7 +20,7 @@ template void lean::eta_matrix<lean::mpq, lean::mpq>::apply_from_left(std::vecto
template void lean::eta_matrix<lean::mpq, lean::mpq>::apply_from_right(std::vector<lean::mpq, std::allocator<lean::mpq> >&);
template void lean::eta_matrix<lean::mpq, lean::mpq>::conjugate_by_permutation(lean::permutation_matrix<lean::mpq, lean::mpq>&);
template void lean::eta_matrix<lean::mpq, lean::numeric_pair<lean::mpq> >::apply_from_left(std::vector<lean::numeric_pair<lean::mpq>, std::allocator<lean::numeric_pair<lean::mpq> > >&, lean::lp_settings&);
template void lean::eta_matrix<lean::mpq, lean::numeric_pair<lean::mpq> >::apply_from_right(std::vector<lean::mpq, std::allocator<lean::mpq> >&);
template void lean::eta_matrix<lean::mpq, lean::numeric_pair<lean::mpq> >::apply_from_right(std::vector<lean::mpq>&);
template void lean::eta_matrix<lean::mpq, lean::numeric_pair<lean::mpq> >::conjugate_by_permutation(lean::permutation_matrix<lean::mpq, lean::numeric_pair<lean::mpq> >&);
template void lean::eta_matrix<double, double>::apply_from_left_local<double>(lean::indexed_vector<double>&, lean::lp_settings&);
template void lean::eta_matrix<lean::mpq, lean::mpq>::apply_from_left_local<lean::mpq>(lean::indexed_vector<lean::mpq>&, lean::lp_settings&);

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

@ -4,7 +4,7 @@
Author: Lev Nachmanson
*/
#include <vector>
#include "util/lp/indexed_vector.h"
namespace lean {
@ -37,38 +37,38 @@ void print_vector(const std::vector<mpq> & t, std::ostream & out) {
out << 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 @@ bool indexed_vector<T>::is_OK() const {
}
return size == m_index.size();
}
template <typename T>
template <typename T>
void indexed_vector<T>::print(std::ostream & out) {
out << "m_index " << std::endl;
for (unsigned i = 0; i < m_index.size(); i++) {

2
src/util/lp/indexed_vector.h
View file

@ -24,7 +24,7 @@ namespace lean {
template <typename T> void print_vector(const std::vector<T> & t, std::ostream & out);
template <typename T> void print_vector(const buffer<T> & t, std::ostream & out);
template <typename T> void print_sparse_vector(const std::vector<T> & t, std::ostream & out);
void print_vector(const std::vector<mpq> & t, std::ostream & out);
template <typename T>
class indexed_vector {

6
src/util/lp/lar_constraints.cpp
View file

@ -4,7 +4,7 @@
Author: Lev Nachmanson
*/
#include <utility>
#include "util/lp/lar_constraints.h"
namespace lean {
@ -18,7 +18,7 @@ lar_constraint::lar_constraint(const buffer<std::pair<mpq, var_index>> & left_si
}
}
}
lar_constraint::lar_constraint(const lar_base_constraint & c): lar_base_constraint(c.m_kind, c.m_right_side, c.m_index) {
for (auto t : c.get_left_side_coefficients())
m_left_side.insert(std::make_pair(t.second, t.first));
@ -44,4 +44,4 @@ buffer<std::pair<mpq, var_index>> lar_normalized_constraint::get_left_side_coeff

1
src/util/lp/lar_constraints.h
View file

@ -7,6 +7,7 @@
#pragma once
#include <vector>
#include <utility>
#include "util/debug.h"
#include "util/buffer.h"
#include "util/numerics/numeric_traits.h"

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

@ -10,6 +10,8 @@
Author: Lev Nachmanson
*/
#include <string>
#include <vector>
#include "util/lp/lar_core_solver.h"
namespace lean {
template <typename T, typename X>
@ -322,7 +324,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";

4
src/util/lp/lar_core_solver.h
View file

@ -46,7 +46,7 @@ public:
void init_costs();
void init_cost_for_column(unsigned j);
void init_local();
// returns m_sign_of_alpha_r
@ -120,7 +120,7 @@ public:
void prefix();
bool is_tiny() const { return this->m_m < 10 && this->m_n < 20; }
bool is_empty() const { return this->m_m == 0 || this->m_n == 0; }
void feasibility_loop();

5
src/util/lp/lar_core_solver_instances.cpp
View file

@ -4,6 +4,11 @@
Author: Lev Nachmanson
*/
#include <utility>
#include <memory>
#include <string>
#include <vector>
#include <functional>
#include "util/lp/lar_core_solver.cpp"
template lean::lar_core_solver<lean::mpq, lean::numeric_pair<lean::mpq> >::lar_core_solver(std::vector<lean::numeric_pair<lean::mpq>, std::allocator<lean::numeric_pair<lean::mpq> > >&, std::vector<lean::column_type, std::allocator<lean::column_type> >&, std::vector<lean::numeric_pair<lean::mpq>, std::allocator<lean::numeric_pair<lean::mpq> > >&, std::vector<lean::numeric_pair<lean::mpq>, std::allocator<lean::numeric_pair<lean::mpq> > >&, std::vector<unsigned int, std::allocator<unsigned int> >&, lean::static_matrix<lean::mpq, lean::numeric_pair<lean::mpq> >&, lean::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> > >&, std::vector<lean::numeric_pair<lean::mpq>, std::allocator<lean::numeric_pair<lean::mpq> > >&, std::vector<lean::mpq, std::allocator<lean::mpq> >&);
template void lean::lar_core_solver<lean::mpq, lean::numeric_pair<lean::mpq> >::solve();

4
src/util/lp/lar_solver.cpp
View file

@ -4,7 +4,9 @@
Author: Lev Nachmanson
*/
#include <string>
#include <algorithm>
#include <vector>
#include "util/lp/lar_solver.h"
namespace lean {
double conversion_helper <double>::get_low_bound(const column_info<mpq> & ci) {

2
src/util/lp/lar_solver.h
View file

@ -170,7 +170,7 @@ public:
bool the_righ_sides_do_not_sum_to_zero(const buffer<pair<mpq, unsigned>> & evidence);
bool the_evidence_is_correct();
void update_column_info_of_normalized_constraints();
template <typename V>

6
src/util/lp/lp_core_solver_base.cpp
View file

@ -4,6 +4,9 @@
Author: Lev Nachmanson
*/
#include <set>
#include <string>
#include <vector>
#include "util/lp/lp_core_solver_base.h"
namespace lean {
void init_basic_part_of_basis_heading(std::vector<unsigned> & basis, unsigned m, std::vector<int> & basis_heading) {
@ -63,7 +66,8 @@ lp_core_solver_base(static_matrix<T, X> & A,
m_low_bound_values(low_bound_values),
m_upper_bound_values(upper_bound_values),
m_column_norms(m_n, T(1)),
m_copy_of_xB(m_m) {
m_copy_of_xB(m_m),
m_steepest_edge_coefficients(A.column_count()) {
if (m_m) {
lean_assert(m_A.col_val_equal_to_row_val());
init();

9
src/util/lp/lp_core_solver_base.h
View file

@ -59,6 +59,9 @@ public:
std::vector<T> m_column_norms; // the approximate squares of column norms that help choosing a profitable column
std::vector<X> m_copy_of_xB;
unsigned m_refactor_counter = 200;
unsigned m_sort_counter = 0;
std::vector<T> m_steepest_edge_coefficients;
lp_core_solver_base(static_matrix<T, X> & A,
std::vector<X> & b, // the right side vector
std::vector<unsigned> & basis,
@ -69,7 +72,7 @@ public:
std::vector<column_type> & column_types,
std::vector<X> & low_bound_values,
std::vector<X> & upper_bound_values);
void allocate_basis_heading();
void init();
@ -144,7 +147,7 @@ public:
bool print_statistics_and_check_that_the_time_is_over(unsigned total_iterations);
void set_non_basic_x_to_correct_bounds();
bool at_bound(const X &x, const X & bound) const {
return !below_bound(x, bound) && !above_bound(x, bound);
}
@ -171,7 +174,7 @@ public:
return below_bound(m_x[p], m_upper_bound_values[p]);
}
bool x_above_upper_bound(unsigned p) {
return above_bound(m_x[p], m_upper_bound_values[p]);
}

5
src/util/lp/lp_core_solver_base_instances.cpp
View file

@ -4,6 +4,11 @@
Author: Lev Nachmanson
*/
#include <utility>
#include <memory>
#include <string>
#include <vector>
#include <functional>
#include "util/lp/lp_core_solver_base.cpp"
template bool lean::lp_core_solver_base<double, double>::A_mult_x_is_off();
template bool lean::lp_core_solver_base<double, double>::basis_heading_is_correct();

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

@ -4,6 +4,9 @@
Author: Lev Nachmanson
*/
#include <algorithm>
#include <string>
#include <vector>
#include "util/lp/lp_dual_core_solver.h"
namespace lean {
@ -243,7 +246,7 @@ template <typename T, typename X> bool lp_dual_core_solver<T, X>::advance_on_kno
return true;
}
calculate_beta_r_precisely();
this->solve_Bd(m_q); //FTRAN
this->solve_Bd(m_q); // FTRAN
int pivot_compare_result = this->pivots_in_column_and_row_are_different(m_q, m_p);
if (!pivot_compare_result){;}
else if (pivot_compare_result == 2) { // the sign is changed, cannot continue
@ -461,20 +464,20 @@ template <typename T, typename X> bool lp_dual_core_solver<T, X>::basis_change_a
}
if (snap_runaway_nonbasic_column(m_p)) {
if(!this->find_x_by_solving()) {
if (!this->find_x_by_solving()) {
revert_to_previous_basis();
this->m_iters_with_no_cost_growing++;
return false;
}
}
if (!problem_is_dual_feasible() ) {
if (!problem_is_dual_feasible()) {
// todo : shift the costs!!!!
revert_to_previous_basis();
this->m_iters_with_no_cost_growing++;
return false;
}
lean_assert(d_is_correct());
return true;
}
@ -517,7 +520,7 @@ template <typename T, typename X> bool lp_dual_core_solver<T, X>::snap_runaway_n
switch (this->m_column_type[j]) {
case fixed:
case low_bound:
if (! this->x_is_at_low_bound(j)) {
if (!this->x_is_at_low_bound(j)) {
this->m_x[j] = this->m_low_bound_values[j];
return true;
}
@ -526,12 +529,12 @@ template <typename T, typename X> bool lp_dual_core_solver<T, X>::snap_runaway_n
{
bool closer_to_low_bound = abs(this->m_low_bound_values[j] - this->m_x[j]) < abs(this->m_upper_bound_values[j] - this->m_x[j]);
if (closer_to_low_bound) {
if (! this->x_is_at_low_bound(j)) {
if (!this->x_is_at_low_bound(j)) {
this->m_x[j] = this->m_low_bound_values[j];
return true;
}
} else {
if (! this->x_is_at_upper_bound(j)) {
if (!this->x_is_at_upper_bound(j)) {
this->m_x[j] = this->m_low_bound_values[j];
return true;
}
@ -539,7 +542,7 @@ template <typename T, typename X> bool lp_dual_core_solver<T, X>::snap_runaway_n
}
break;
case upper_bound:
if (! this->x_is_at_upper_bound(j)) {
if (!this->x_is_at_upper_bound(j)) {
this->m_x[j] = this->m_upper_bound_values[j];
return true;
}

2
src/util/lp/lp_dual_core_solver.h
View file

@ -118,7 +118,7 @@ public:
bool snap_runaway_nonbasic_column(unsigned);
bool snap_runaway_nonbasic_columns();
unsigned get_number_of_rows_to_try_for_leaving();
void update_a_wave(const T & del, unsigned j) {

5
src/util/lp/lp_dual_core_solver_instances.cpp
View file

@ -4,6 +4,11 @@
Author: Lev Nachmanson
*/
#include <utility>
#include <memory>
#include <string>
#include <vector>
#include <functional>
#include "util/lp/lp_dual_core_solver.cpp"
template lean::lp_dual_core_solver<lean::mpq, lean::mpq>::lp_dual_core_solver(lean::static_matrix<lean::mpq, lean::mpq>&, std::vector<bool, std::allocator<bool> >&, std::vector<lean::mpq, std::allocator<lean::mpq> >&, std::vector<lean::mpq, std::allocator<lean::mpq> >&, std::vector<unsigned int, std::allocator<unsigned int> >&, std::vector<lean::mpq, std::allocator<lean::mpq> >&, std::vector<lean::column_type, std::allocator<lean::column_type> >&, std::vector<lean::mpq, std::allocator<lean::mpq> >&, std::vector<lean::mpq, std::allocator<lean::mpq> >&, lean::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 void lean::lp_dual_core_solver<lean::mpq, lean::mpq>::start_with_initial_basis_and_make_it_dual_feasible();

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

@ -4,7 +4,12 @@
Author: Lev Nachmanson
*/
#include <list>
#include <vector>
#include <fstream>
#include <algorithm>
#include <set>
#include <string>
#include "util/lp/lp_primal_core_solver.h"
namespace lean {
@ -15,35 +20,37 @@ template <typename T, typename X>
void lp_primal_core_solver<T, X>::sort_non_basis() {
for (unsigned j : this->m_non_basic_columns) {
T const & da = this->m_d[j];
m_steepest_edge_coefficients[j] = da * da / this->m_column_norms[j];
this->m_steepest_edge_coefficients[j] = da * da / this->m_column_norms[j];
}
std::sort(this->m_non_basic_columns.begin(), this->m_non_basic_columns.end(), [this](unsigned a, unsigned b) {
return m_steepest_edge_coefficients[a] > m_steepest_edge_coefficients[b];
return this->m_steepest_edge_coefficients[a] > this->m_steepest_edge_coefficients[b];
});
m_non_basis_list.clear();
// reinit m_basis_heading
for (int j = 0; j < this->m_non_basic_columns.size(); j++)
this->m_basis_heading[this->m_non_basic_columns[j]] = - j - 1;
for (int j = 0; j < this->m_non_basic_columns.size(); j++) {
unsigned col = this->m_non_basic_columns[j];
this->m_basis_heading[col] = - j - 1;
m_non_basis_list.push_back(col);
}
}
template <typename T, typename X>
int lp_primal_core_solver<T, X>::choose_entering_column(unsigned number_of_benefitial_columns_to_go_over) { // at this moment m_y = cB * B(-1)
lean_assert(number_of_benefitial_columns_to_go_over);
if (m_sort_columns_counter == 0) {
if (this->m_sort_counter == 0) {
sort_non_basis();
m_sort_columns_counter = 20;
this->m_sort_counter = 20;
} else {
m_sort_columns_counter--;
this->m_sort_counter--;
}
lean_assert(m_sort_columns_counter>=0);
unsigned offset_in_nb = 0;
unsigned initial_offset_in_non_basis = offset_in_nb;
lean_assert(this->m_sort_counter >=0);
T steepest_edge = zero_of_type<T>();
int entering = -1;
do {
unsigned j = this->m_non_basic_columns[offset_in_nb];
push_forward_offset_in_non_basis(offset_in_nb);
std::list<unsigned>::iterator entering_iter = m_non_basis_list.end();
for (auto non_basis_iter= m_non_basis_list.begin(); number_of_benefitial_columns_to_go_over && non_basis_iter != m_non_basis_list.end(); ++non_basis_iter) {
unsigned j = *non_basis_iter;
if (m_forbidden_enterings.find(j) != m_forbidden_enterings.end()) {
continue;
}
@ -76,14 +83,19 @@ int lp_primal_core_solver<T, X>::choose_entering_column(unsigned number_of_benef
T t = dj * dj / this->m_column_norms[j];
if (t > steepest_edge) {
steepest_edge = t;
entering = j;
entering_iter = non_basis_iter;
if (number_of_benefitial_columns_to_go_over)
number_of_benefitial_columns_to_go_over--;
}
} while (number_of_benefitial_columns_to_go_over && initial_offset_in_non_basis != offset_in_nb);
if (entering != -1)
}// while (number_of_benefitial_columns_to_go_over && initial_offset_in_non_basis != offset_in_nb);
if (entering_iter != m_non_basis_list.end()) {
unsigned entering = *entering_iter;
m_sign_of_entering_delta = this->m_d[entering] > 0? 1 : -1;
return entering;
m_non_basis_list.erase(entering_iter);
m_non_basis_list.push_back(entering);
return entering;
}
return -1;
}
@ -249,8 +261,7 @@ template <typename T, typename X> lp_primal_core_solver<T, X>:: lp_primal_core
column_type_array,
low_bound_values,
upper_bound_values),
m_beta(A.row_count()),
m_steepest_edge_coefficients(A.column_count()) {
m_beta(A.row_count()) {
this->m_status = UNKNOWN;
this->m_column_norm_update_counter = settings.column_norms_update_frequency;
}
@ -275,8 +286,7 @@ lp_primal_core_solver(static_matrix<T, X> & A,
column_type_array,
m_low_bound_values_dummy,
upper_bound_values),
m_beta(A.row_count()),
m_steepest_edge_coefficients(A.column_count()) {
m_beta(A.row_count()) {
m_converted_harris_eps = convert_struct<T, double>::convert(this->m_settings.harris_feasibility_tolerance);
lean_assert(initial_x_is_correct());
m_low_bound_values_dummy.resize(A.column_count(), zero_of_type<T>());
@ -426,6 +436,7 @@ template <typename T, typename X> void lp_primal_core_solver<T, X>::calc_work
}
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(m_non_basis_list.back() == entering);
lean_assert(t >= zero_of_type<X>());
lean_assert(leaving >= 0 && entering >= 0);
lean_assert(entering != leaving || !is_zero(t)); // otherwise nothing changes
@ -482,6 +493,9 @@ template <typename T, typename X>void lp_primal_core_solver<T, X>::advance_on_en
update_reduced_costs_from_pivot_row(entering, leaving);
lean_assert(!need_to_switch_costs());
m_forbidden_enterings.clear();
std::list<unsigned>::iterator it = m_non_basis_list.end();
it--;
* it = static_cast<unsigned>(leaving);
}
// void recalc_reduced_costs() {

9
src/util/lp/lp_primal_core_solver.h
View file

@ -6,7 +6,7 @@
*/
#pragma once
#include <list>
#include "util/numerics/double.h"
#include "util/lp/lu.h"
#include "util/lp/lp_solver.h"
@ -30,7 +30,7 @@ namespace lean {
// The right side b is given implicitly by x and the basis
template <typename T, typename X>
class lp_primal_core_solver:public lp_core_solver_base<T, X> {
public:
public:
// m_sign_of_entering is set to 1 if the entering variable needs
// to grow and is set to -1 otherwise
unsigned m_column_norm_update_counter;
@ -48,8 +48,7 @@ public:
std::vector<T> m_costs_backup;
bool m_current_x_is_feasible;
T m_converted_harris_eps = convert_struct<T, double>::convert(this->m_settings.harris_feasibility_tolerance);
unsigned m_sort_columns_counter = 0;
std::vector<T> m_steepest_edge_coefficients;
std::list<unsigned> m_non_basis_list;
void sort_non_basis();
int choose_entering_column(unsigned number_of_benefitial_columns_to_go_over);
@ -72,7 +71,7 @@ public:
void limit_theta_on_basis_column_for_inf_case_m_neg_upper_bound(unsigned j, const T & m, X & theta) {
lean_assert(m < 0 && this->m_column_type[j] == upper_bound);
limit_inf_on_upper_bound_m_neg(m, this->m_x[j], this->m_upper_bound_values[j], theta);
}
}
void limit_theta_on_basis_column_for_inf_case_m_neg_low_bound(unsigned j, const T & m, X & theta) {

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

@ -4,10 +4,14 @@
Author: Lev Nachmanson
*/
#include <utility>
#include <memory>
#include <string>
#include <vector>
#include <functional>
#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 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&);
@ -15,6 +19,4 @@ template lp_primal_core_solver<double, double>::lp_primal_core_solver(static_mat
template unsigned lp_primal_core_solver<double, double>::solve();
template lp_primal_core_solver<mpq, mpq>::lp_primal_core_solver(static_matrix<mpq, mpq>&, std::vector<mpq, std::allocator<mpq> >&, std::vector<mpq, std::allocator<mpq> >&, std::vector<unsigned int, std::allocator<unsigned int> >&, std::vector<mpq, std::allocator<mpq> >&, std::vector<column_type, std::allocator<column_type> >&, std::vector<mpq, std::allocator<mpq> >&, std::vector<mpq, std::allocator<mpq> >&, 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 unsigned lp_primal_core_solver<mpq, mpq>::solve();
//template void lp_primal_simplex<double, double>::solve_with_total_inf();
//template void lp_primal_simplex<mpq, mpq>::solve_with_total_inf();
}

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

@ -4,6 +4,8 @@
Author: Lev Nachmanson
*/
#include <string>
#include <vector>
#include "util/lp/lp_primal_simplex.h"
namespace lean {

5
src/util/lp/lp_primal_simplex_instances.cpp
View file

@ -4,6 +4,11 @@
Author: Lev Nachmanson
*/
#include <utility>
#include <memory>
#include <string>
#include <vector>
#include <functional>
#include "util/lp/lp_primal_simplex.cpp"
template bool lean::lp_primal_simplex<double, double>::bounds_hold(std::unordered_map<std::string, double, std::hash<std::string>, std::equal_to<std::string>, std::allocator<std::pair<std::string const, double> > > const&);
template bool lean::lp_primal_simplex<double, double>::row_constraints_hold(std::unordered_map<std::string, double, std::hash<std::string>, std::equal_to<std::string>, std::allocator<std::pair<std::string const, double> > > const&);

4
src/util/lp/lp_settings.cpp
View file

@ -5,6 +5,8 @@
Author: Lev Nachmanson
*/
#include <cmath>
#include <string>
#include <vector>
#include "util/numerics/double.h"
#include "util/lp/lp_settings.h"
namespace lean {
@ -77,7 +79,7 @@ void my_random_init(unsigned * seed) {
}
unsigned my_random() {
#ifdef LEAN_WINDOWS
return rand();
return rand(); // NOLINT
#else
return lrand48();
#endif

1
src/util/lp/lp_settings.h
View file

@ -6,6 +6,7 @@
*/
#pragma once
#include <vector>
#include <string>
#include <algorithm>
#include <limits>

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

@ -4,5 +4,7 @@
Author: Lev Nachmanson
*/
#include <vector>
#include <memory>
#include "util/lp/lp_settings.cpp"
template bool lean::vectors_are_equal<double>(std::vector<double, std::allocator<double> > const&, std::vector<double, std::allocator<double> > const&);

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

@ -4,7 +4,9 @@
Author: Lev Nachmanson
*/
#include <string>
#include <algorithm>
#include <vector>
#include "util/lp/lp_solver.h"
namespace lean {
template <typename T, typename X> column_info<T> * lp_solver<T, X>::get_or_create_column_info(unsigned column) {
@ -373,10 +375,10 @@ template <typename T, typename X> void lp_solver<T, X>::cleanup() {
while ((d = try_to_remove_some_rows()))
n += d;
if (n == 1)
std::cout << "deleted one row" << std::endl;
else if (n)
std::cout << "deleted " << n << " rows" << std::endl;
// if (n == 1)
// std::cout << "deleted one row" << std::endl;
// else if (n)
// std::cout << "deleted " << n << " rows" << std::endl;
}
template <typename T, typename X> void lp_solver<T, X>::map_external_rows_to_core_solver_rows() {
@ -532,7 +534,7 @@ template <typename T, typename X> T lp_solver<T, X>::get_column_value_with_co
return numeric_traits<T>::zero(); // returns zero for out of boundary columns
}
template <typename T, typename X> void lp_solver<T, X>::set_scaled_cost(unsigned j) {
// grab original costs but modify it with the column scales
lean_assert(j < this->m_column_scale.size());

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

@ -4,7 +4,7 @@
Author: Lev Nachmanson
*/
#include <string>
#include "util/lp/lp_solver.cpp"
template void lean::lp_solver<double, double>::add_constraint(lean::lp_relation, double, unsigned int);
template void lean::lp_solver<double, double>::cleanup();

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

@ -4,7 +4,10 @@
Author: Lev Nachmanson
*/
#include <string>
#include <algorithm>
#include <set>
#include <vector>
#include "util/lp/lu.h"
namespace lean {
#ifdef LEAN_DEBUG
@ -75,7 +78,7 @@ X dot_product(const std::vector<T> & a, const std::vector<X> & b, unsigned l) {
template <typename T, typename X>
one_elem_on_diag<T,X>::one_elem_on_diag(const one_elem_on_diag & o) {
one_elem_on_diag<T, X>::one_elem_on_diag(const one_elem_on_diag & o) {
m_i = o.m_i;
m_val = o.m_val;
#ifdef LEAN_DEBUG
@ -710,7 +713,7 @@ void lu<T, X>::calculate_Lwave_Pwave_for_bump(unsigned replaced_column, unsigned
calculate_Lwave_Pwave_for_last_row(lowest_row_of_the_bump, diagonal_elem);
// lean_assert(m_U.is_upper_triangular_and_maximums_are_set_correctly_in_rows(m_settings));
}
template <typename T, typename X>
void lu<T, X>::calculate_Lwave_Pwave_for_last_row(unsigned lowest_row_of_the_bump, T diagonal_element) {
auto l = new one_elem_on_diag<T, X>(lowest_row_of_the_bump, diagonal_element);

4
src/util/lp/lu.h
View file

@ -132,7 +132,7 @@ public:
template <typename L>
void solve_By_when_y_is_ready(std::vector<L> & y);
void print_indexed_vector(indexed_vector<T> & w, std::ofstream & f);
void print_basis(std::ostream & f);
void print_matrix_compact(std::ostream & f);
@ -275,7 +275,7 @@ public:
init_vector_w(entering, w);
}
}; // end of lu
template <typename T, typename X>
void init_factorization(lu<T, X>* & factorization, static_matrix<T, X> & m_A, std::vector<unsigned> & m_basis, std::vector<int> & m_basis_heading, lp_settings &m_settings, std::vector<unsigned> & non_basic_columns);

7
src/util/lp/lu_instances.cpp
View file

@ -4,7 +4,10 @@
Author: Lev Nachmanson
*/
#include <utility>
#include <memory>
#include <string>
#include <vector>
#include "util/lp/lu.cpp"
template double lean::dot_product<double, double>(std::vector<double, std::allocator<double> > const&, std::vector<double, std::allocator<double> > const&, unsigned int);
template void lean::lu<double, double>::change_basis(unsigned int, unsigned int);
@ -45,4 +48,4 @@ template void lean::lu<lean::mpq, lean::numeric_pair<lean::mpq> >::solve_yB(std:
template void lean::lu<lean::mpq, lean::numeric_pair<lean::mpq> >::solve_By(std::vector<lean::numeric_pair<lean::mpq>, std::allocator<lean::numeric_pair<lean::mpq> > >&);
template void lean::lu<double, double>::init_vector_w(unsigned int, lean::indexed_vector<double>&);
template lean::numeric_pair<lean::mpq> lean::dot_product<lean::mpq, lean::numeric_pair<lean::mpq> >(std::vector<lean::mpq, std::allocator<lean::mpq> > const&, std::vector<lean::numeric_pair<lean::mpq>, std::allocator<lean::numeric_pair<lean::mpq> > > const&, unsigned int);
template bool lean::lu<double, double>::pivot_the_row(int);
template bool lean::lu<double, double>::pivot_the_row(int); // NOLINT

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

@ -5,6 +5,8 @@
Author: Lev Nachmanson
*/
#ifdef LEAN_DEBUG
#include <vector>
#include <string>
#include "util/lp/matrix.h"
namespace lean {
template <typename T, typename X>

1
src/util/lp/matrix.h
View file

@ -39,7 +39,6 @@ void apply_to_vector(matrix<T, X> & m, T * w);
unsigned get_width_of_column(unsigned j, std::vector<std::vector<std::string>> & A);
void print_matrix_with_widths(std::vector<std::vector<std::string>> & A, std::vector<unsigned> & ws, std::ostream & out);
void print_string_matrix(std::vector<std::vector<std::string>> & A);
template <typename T, typename X>
void print_matrix(matrix<T, X> const & m, std::ostream & out);

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

@ -4,6 +4,7 @@
Author: Lev Nachmanson
*/
#include <vector>
#include "util/lp/permutation_matrix.h"
namespace lean {
template <typename T, typename X> permutation_matrix<T, X>::permutation_matrix(unsigned length): m_length(length), m_permutation(length), m_rev(length) {

12
src/util/lp/permutation_matrix.h
View file

@ -96,7 +96,7 @@ namespace lean {
template <typename L>
void apply_reverse_from_left(std::vector<L> & w);
template <typename L>
void apply_reverse_from_right(std::vector<L> & w) ;
void apply_reverse_from_right(std::vector<L> & w);
void set_val(unsigned i, unsigned pi) {
lean_assert(i < m_length && pi < m_length); m_permutation[i] = pi; m_rev[pi] = i; }
@ -144,16 +144,16 @@ namespace lean {
permutation_matrix<T, X> m_current;
unsigned m_last;
public:
permutation_generator(unsigned n);
permutation_generator(unsigned n);
permutation_generator(const permutation_generator & o);
bool move_next();
~permutation_generator() {
if (m_lower != nullptr) {
delete m_lower;
}
}
permutation_matrix<T, X> *current() {
return &m_current;
}
@ -161,12 +161,12 @@ namespace lean {
template <typename T, typename X>
inline unsigned number_of_inversions(permutation_matrix<T, X> & p);
template <typename T, typename X>
int sign(permutation_matrix<T, X> & p) {
return is_even(number_of_inversions(p))? 1: -1;
}
template <typename T, typename X>
T det_val_on_perm(permutation_matrix<T, X>* u, const matrix<T, X>& m);

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

@ -4,6 +4,8 @@
Author: Lev Nachmanson
*/
#include <memory>
#include <vector>
#include "util/lp/permutation_matrix.cpp"
#include "util/lp/numeric_pair.h"
template void lean::permutation_matrix<double, double>::apply_from_right(std::vector<double, std::allocator<double> >&);

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

@ -4,7 +4,7 @@
Author: Lev Nachmanson
*/
#include <vector>
#include "util/lp/row_eta_matrix.h"
namespace lean {
template <typename T, typename X>
@ -15,7 +15,7 @@ void row_eta_matrix<T, X>::apply_from_left(std::vector<X> & w, lp_settings &) {
// deb.apply_from_left(clone_w, settings);
// #endif
auto w_at_row = w[m_row];
for (auto & it :m_row_vector.m_data) {
for (auto & it : m_row_vector.m_data) {
w_at_row += w[it.first] * it.second;
}
w[m_row] = w_at_row;

3
src/util/lp/row_eta_matrix_instances.cpp
View file

@ -4,7 +4,8 @@
Author: Lev Nachmanson
*/
#include <vector>
#include <memory>
#include "util/lp/row_eta_matrix.cpp"
#include "util/lp/lu.h"
namespace lean {

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

@ -4,7 +4,7 @@
Author: Lev Nachmanson
*/
#include <algorithm>
#include "util/lp/scaler.h"
#include "util/lp/numeric_pair.h"
namespace lean {

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

@ -5,7 +5,7 @@
Author: Lev Nachmanson
*/
#include <vector>
#include "util/lp/sparse_matrix.h"
namespace lean {
template <typename T, typename X>
@ -798,7 +798,7 @@ bool sparse_matrix<T, X>::shorten_active_matrix(unsigned row, eta_matrix<T, X> *
if (eta_matrix == nullptr) return true;
// it looks like double work, but the pivot scores have changed for all rows
// touched by eta_matrix
for (auto & it: eta_matrix->m_column_vector.m_data) {
for (auto & it : eta_matrix->m_column_vector.m_data) {
unsigned row = adjust_row(it.first);
auto & row_values = m_rows[row];
unsigned rnz = row_values.size();

2
src/util/lp/sparse_matrix.h
View file

@ -109,7 +109,7 @@ public:
void set_with_no_adjusting(unsigned row, unsigned col, T val);
void set(unsigned row, unsigned col, T val);
T const & get_not_adjusted(unsigned row, unsigned col) const;
T const & get(unsigned row, unsigned col) const;

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

@ -4,6 +4,8 @@
Author: Lev Nachmanson
*/
#include <vector>
#include <memory>
#include "util/lp/lu.h"
#include "util/lp/sparse_matrix.cpp"
namespace lean {

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

@ -4,7 +4,7 @@
Author: Lev Nachmanson
*/
#include <vector>
#include "util/lp/square_dense_submatrix.h"
namespace lean {
template <typename T, typename X>
@ -157,7 +157,7 @@ template <typename T, typename X> void square_dense_submatrix<T, X>::push_new
}
}
}
template <typename T, typename X>
template <typename T, typename X>
template <typename L>
L square_dense_submatrix<T, X>::row_by_vector_product(unsigned i, const std::vector<L> & v) {
lean_assert(i >= m_index_start);
@ -170,7 +170,7 @@ L square_dense_submatrix<T, X>::row_by_vector_product(unsigned i, const std::vec
return r;
}
template <typename T, typename X>
template <typename T, typename X>
template <typename L>
L square_dense_submatrix<T, X>::column_by_vector_product(unsigned j, const std::vector<L> & v) {
lean_assert(j >= m_index_start);
@ -181,7 +181,7 @@ L square_dense_submatrix<T, X>::column_by_vector_product(unsigned j, const std::
r += m_v[offset] * v[adjust_row_inverse(m_index_start + i)];
return r;
}
template <typename T, typename X>
template <typename T, typename X>
template <typename L>
L square_dense_submatrix<T, X>::row_by_indexed_vector_product(unsigned i, const indexed_vector<L> & v) {
lean_assert(i >= m_index_start);
@ -193,7 +193,7 @@ L square_dense_submatrix<T, X>::row_by_indexed_vector_product(unsigned i, const
r += m_v[row_offset + j] * v[adjust_column_inverse(m_index_start + j)];
return r;
}
template <typename T, typename X>
template <typename T, typename X>
template <typename L>
void square_dense_submatrix<T, X>::apply_from_left_local(indexed_vector<L> & w, lp_settings & settings) {
#ifdef LEAN_DEBUG

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

@ -96,7 +96,7 @@ public:
void update_existing_or_delete_in_parent_matrix_for_row(unsigned i, lp_settings & settings);
void push_new_elements_to_parent_matrix(lp_settings & settings);
template <typename L>
L row_by_vector_product(unsigned i, const std::vector<L> & v);

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

@ -4,6 +4,8 @@
Author: Lev Nachmanson
*/
#include <memory>
#include <vector>
#include "util/lp/square_dense_submatrix.cpp"
template void lean::square_dense_submatrix<double, double>::init(lean::sparse_matrix<double, double>*, unsigned int);
template lean::square_dense_submatrix<double, double>::square_dense_submatrix(lean::sparse_matrix<double, double>*, unsigned int);

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

@ -4,7 +4,9 @@
Author: Lev Nachmanson
*/
#include <vector>
#include <utility>
#include <set>
#include "util/lp/static_matrix.h"
namespace lean {
@ -19,7 +21,7 @@ void static_matrix<T, X>::init_row_columns(unsigned m, unsigned n) {
m_columns.push_back(column_strip());
}
}
// constructor that copies columns of the basis from A
template <typename T, typename X>
static_matrix<T, X>::static_matrix(static_matrix const &A, unsigned * basis) :
@ -32,7 +34,7 @@ static_matrix<T, X>::static_matrix(static_matrix const &A, unsigned * basis) :
}
}
}
template <typename T, typename X> void static_matrix<T, X>::clear() {
m_work_pivot_vector.clear();
m_rows.clear();
@ -45,12 +47,12 @@ template <typename T, typename X> void static_matrix<T, X>::clear() {
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) {
init_work_pivot_vector(m);
init_row_columns(m, n);
}
template <typename T, typename X>
template <typename T, typename X>
template <typename L>
L static_matrix<T, X>::dot_product_with_row(unsigned row, const std::vector<L> & w) {
L ret = zero_of_type<L>();
@ -127,7 +129,7 @@ void static_matrix<T, X>::divide_row_by_constant(unsigned row, T const & alpha)
m_columns[t.m_j][t.m_offset].m_value /= alpha;
}
}
template <typename T, typename X>
void static_matrix<T, X>::scale_column(unsigned column, T const & alpha) {
for (auto & t : m_columns[column]) {
@ -181,7 +183,7 @@ template <typename T, typename X> void static_matrix<T, X>::copy_column_to_ve
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 {
v.resize(row_count(), numeric_traits<T>::zero());
for (auto & it : m_columns[j]) {
@ -195,7 +197,7 @@ template <typename T, typename X> void static_matrix<T, X>::add_column_to_vec
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 {
T ret = numeric_traits<T>::zero();
for (auto & t : m_rows[row]) {
@ -206,7 +208,7 @@ template <typename T, typename X> T static_matrix<T, X>::get_max_abs_in_row(u
}
return ret;
}
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();
@ -248,7 +250,7 @@ template <typename T, typename X> T static_matrix<T, X>::get_min_abs_in_colu
}
return ret;
}
#ifdef LEAN_DEBUG
template <typename T, typename X> void static_matrix<T, X>::check_consistency() {
std::unordered_map<std::pair<unsigned, unsigned>, T> by_rows;
@ -312,7 +314,7 @@ template <typename T, typename X> void static_matrix<T, X>::cross_out_row_fro
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) {
auto & s = m_columns[col];
for (unsigned i = 0; i < s.size(); i++) {
@ -338,13 +340,13 @@ template <typename T, typename X> void static_matrix<T, X>::scan_row_to_work_
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) {
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 {
T ret = zero_of_type<T>();

6
src/util/lp/static_matrix.h
View file

@ -147,9 +147,9 @@ public:
std::set<pair<unsigned, unsigned>> get_domain();
void copy_column_to_vector (unsigned j, indexed_vector<T> & v) const;
void copy_column_to_vector (unsigned j, std::vector<T> & v) const;
void add_column_to_vector (const T & a, unsigned j, T * v) const;
T get_max_abs_in_row(unsigned row) const;
@ -172,7 +172,7 @@ public:
void cross_out_row_from_column(unsigned col, unsigned k);
T get_elem(unsigned i, unsigned j) const;
T get_elem(unsigned i, unsigned j) const;
unsigned number_of_non_zeroes_in_column(unsigned j) const { return m_columns[j].size(); }

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

@ -4,7 +4,9 @@
Author: Lev Nachmanson
*/
#include <vector>
#include <memory>
#include <set>
#include "util/lp/static_matrix.cpp"
#include "util/lp/lp_core_solver_base.h"
#include "util/lp/lp_dual_core_solver.h"
@ -63,10 +65,10 @@ template void static_matrix<mpq, mpq>::set(unsigned int, unsigned int, mpq const
template static_matrix<mpq, mpq>::static_matrix(unsigned int, unsigned int);
#ifdef LEAN_DEBUG
template bool static_matrix<mpq, numeric_pair<mpq> >::col_val_equal_to_row_val() const;
#endif
#endif
template void static_matrix<mpq, numeric_pair<mpq> >::copy_column_to_vector(unsigned int, indexed_vector<mpq>&) const;
template mpq static_matrix<mpq, numeric_pair<mpq> >::dot_product_with_column(std::vector<mpq, std::allocator<mpq> > const&, unsigned int) const;
template mpq static_matrix<mpq, numeric_pair<mpq> >::get_elem(unsigned int, unsigned int) const;
template void static_matrix<mpq, numeric_pair<mpq> >::init_empty_matrix(unsigned int, unsigned int);
template void static_matrix<mpq, numeric_pair<mpq> >::set(unsigned int, unsigned int, mpq const&);
}
}

1
src/util/lp/tail_matrix.h
View file

@ -6,6 +6,7 @@
*/
#pragma once
#include <vector>
#include "util/lp/indexed_vector.h"
#include "util/lp/matrix.h"
// These matrices appear at the end of the list