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

dev(lp): move some dummy field from lar_solver to lar_core_solver

Browse source 
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
This commit is contained in:
Lev Nachmanson 2016-05-20 14:30:32 -07:00 committed by Leonardo de Moura
parent 0bb21914e6
commit 1529eb1e41
5 changed files with 25 additions and 36 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -20,14 +20,12 @@ lar_core_solver<T, X>::lar_core_solver(std::vector<X> & x, std::vector<column_ty
std::vector<unsigned> & basis, std::vector<unsigned> & basis,
static_matrix<T, X> & A, static_matrix<T, X> & A,
lp_settings & settings, lp_settings & settings,
std::unordered_map<unsigned, std::string> & column_names, std::unordered_map<unsigned, std::string> & column_names):
std::vector<X> & right_side,
std::vector<T> & costs) : // right_side and costs are redundant
lp_core_solver_base<T, X>(A, lp_core_solver_base<T, X>(A,
right_side, m_right_sides_dummy,
basis, basis,
x, x,
costs, m_costs_dummy,
settings, settings,
column_names, column_names,
column_types, column_types,

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

@ -26,16 +26,17 @@ class lar_core_solver : public lp_core_solver_base<T, X> {
binary_heap_priority_queue<X> m_breakpoint_indices_queue; binary_heap_priority_queue<X> m_breakpoint_indices_queue;
std::vector<std::pair<mpq, unsigned>> m_infeasible_row; std::vector<std::pair<mpq, unsigned>> m_infeasible_row;
int m_infeasible_row_sign = 0; int m_infeasible_row_sign = 0;
// with a breakpoint at this delta std::vector<X> m_right_sides_dummy;
std::vector<T> m_costs_dummy;
public: public:
lar_core_solver(std::vector<X> & x, std::vector<column_type> & column_types, lar_core_solver(std::vector<X> & x,
std::vector<X> & low_bounds, std::vector<X> & upper_bounds, std::vector<column_type> & column_types,
std::vector<X> & low_bounds,
std::vector<X> & upper_bounds,
std::vector<unsigned> & basis, std::vector<unsigned> & basis,
static_matrix<T, X> & A, static_matrix<T, X> & A,
lp_settings & settings, lp_settings & settings,
std::unordered_map<unsigned, std::string> & column_names, std::unordered_map<unsigned, std::string> & column_names);
std::vector<X> & right_side,
std::vector<T> & costs);
int get_infeasible_row_sign() const { return m_infeasible_row_sign; } int get_infeasible_row_sign() const { return m_infeasible_row_sign; }

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

@ -10,7 +10,14 @@
#include <vector> #include <vector>
#include <functional> #include <functional>
#include "util/lp/lar_core_solver.cpp" #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 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> > >&);
template void lean::lar_core_solver<lean::mpq, lean::numeric_pair<lean::mpq> >::solve(); template void lean::lar_core_solver<lean::mpq, lean::numeric_pair<lean::mpq> >::solve();
template void lean::lar_core_solver<lean::mpq, lean::numeric_pair<lean::mpq> >::prefix(); template void lean::lar_core_solver<lean::mpq, lean::numeric_pair<lean::mpq> >::prefix();
template void lean::lar_core_solver<lean::mpq, lean::numeric_pair<lean::mpq> >::print_column_info(unsigned int, std::ostream & out); template void lean::lar_core_solver<lean::mpq, lean::numeric_pair<lean::mpq> >::print_column_info(unsigned int, std::ostream & out);

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

@ -427,12 +427,6 @@ void lar_solver::update_column_info_of_normalized_constraints() {
update_column_info_of_normalized_constraint(it.second); update_column_info_of_normalized_constraint(it.second);
} }
template <typename V>
void lar_solver::init_right_sides_with_zeros(std::vector<V> & rs) {
rs.clear();
rs.resize(m_basis.size(), zero_of_type<V>());
}
mpq lar_solver::sum_of_right_sides_of_evidence(const buffer<std::pair<mpq, unsigned>> & evidence) { mpq lar_solver::sum_of_right_sides_of_evidence(const buffer<std::pair<mpq, unsigned>> & evidence) {
mpq ret = numeric_traits<mpq>::zero(); mpq ret = numeric_traits<mpq>::zero();
for (auto & it : evidence) { for (auto & it : evidence) {
@ -464,7 +458,6 @@ void lar_solver::prepare_independently_of_numeric_type() {
template <typename U, typename V> template <typename U, typename V>
void lar_solver::prepare_core_solver_fields(static_matrix<U, V> & A, std::vector<V> & x, void lar_solver::prepare_core_solver_fields(static_matrix<U, V> & A, std::vector<V> & x,
std::vector<V> & right_side_vector,
std::vector<V> & low_bound, std::vector<V> & low_bound,
std::vector<V> & upper_bound) { std::vector<V> & upper_bound) {
create_matrix_A(A); create_matrix_A(A);
@ -472,14 +465,12 @@ void lar_solver::prepare_core_solver_fields(static_matrix<U, V> & A, std::vector
if (m_status == INFEASIBLE) { if (m_status == INFEASIBLE) {
lean_assert(false); // not implemented lean_assert(false); // not implemented
} }
init_right_sides_with_zeros(right_side_vector);
resize_x_and_init_with_zeros(x, A.column_count()); resize_x_and_init_with_zeros(x, A.column_count());
lean_assert(m_basis.size() == A.row_count()); lean_assert(m_basis.size() == A.row_count());
} }
template <typename U, typename V> template <typename U, typename V>
void lar_solver::prepare_core_solver_fields_with_signature(static_matrix<U, V> & A, std::vector<V> & x, void lar_solver::prepare_core_solver_fields_with_signature(static_matrix<U, V> & A, std::vector<V> & x,
std::vector<V> & right_side_vector,
std::vector<V> & low_bound, std::vector<V> & low_bound,
std::vector<V> & upper_bound, const lar_solution_signature & signature) { std::vector<V> & upper_bound, const lar_solution_signature & signature) {
create_matrix_A(A); create_matrix_A(A);
@ -487,15 +478,16 @@ void lar_solver::prepare_core_solver_fields_with_signature(static_matrix<U, V> &
if (m_status == INFEASIBLE) { if (m_status == INFEASIBLE) {
lean_assert(false); // not implemented lean_assert(false); // not implemented
} }
init_right_sides_with_zeros(right_side_vector);
resize_x_and_init_with_signature(x, low_bound, upper_bound, signature); resize_x_and_init_with_signature(x, low_bound, upper_bound, signature);
} }
void lar_solver::find_solution_signature_with_doubles(lar_solution_signature & signature) { void lar_solver::find_solution_signature_with_doubles(lar_solution_signature & signature) {
static_matrix<double, double> A; static_matrix<double, double> A;
std::vector<double> x, right_side_vector, low_bounds, upper_bounds; std::vector<double> x, low_bounds, upper_bounds;
prepare_core_solver_fields<double, double>(A, x, right_side_vector, low_bounds, upper_bounds); prepare_core_solver_fields<double, double>(A, x, low_bounds, upper_bounds);
std::vector<double> column_scale_vector; std::vector<double> column_scale_vector;
std::vector<double> right_side_vector(A.row_count(), 0);
scaler<double, double > scaler(right_side_vector, A, m_settings.scaling_minimum, m_settings.scaling_maximum, column_scale_vector, this->m_settings); scaler<double, double > scaler(right_side_vector, A, m_settings.scaling_minimum, m_settings.scaling_maximum, column_scale_vector, this->m_settings);
if (!scaler.scale()) { if (!scaler.scale()) {
// the scale did not succeed, unscaling // the scale did not succeed, unscaling
@ -526,7 +518,7 @@ void lar_solver::extract_signature_from_lp_core_solver(lp_primal_core_solver<U,
} }
void lar_solver::solve_on_signature(const lar_solution_signature & signature) { void lar_solver::solve_on_signature(const lar_solution_signature & signature) {
prepare_core_solver_fields_with_signature(m_A, m_x, m_right_side_vector, m_low_bounds, m_upper_bounds, signature); prepare_core_solver_fields_with_signature(m_A, m_x, m_low_bounds, m_upper_bounds, signature);
solve_with_core_solver(); solve_with_core_solver();
} }
@ -539,7 +531,7 @@ void lar_solver::solve() {
solve_on_signature(solution_signature); solve_on_signature(solution_signature);
return; return;
} }
prepare_core_solver_fields(m_A, m_x, m_right_side_vector, m_low_bounds, m_upper_bounds); prepare_core_solver_fields(m_A, m_x, m_low_bounds, m_upper_bounds);
solve_with_core_solver(); solve_with_core_solver();
} }

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

@ -66,8 +66,6 @@ class lar_solver {
std::vector<unsigned> m_basis; std::vector<unsigned> m_basis;
std::vector<numeric_pair<mpq>> m_x; // the solution std::vector<numeric_pair<mpq>> m_x; // the solution
std::unordered_map<unsigned, std::string> m_column_names; std::unordered_map<unsigned, std::string> m_column_names;
std::vector<numeric_pair<mpq>> m_right_side_vector; // this vector will be all zeroes, it might change when the optimization with fixed variables will used
std::vector<mpq> m_costs;
canonic_left_side * m_infeasible_canonic_left_side = nullptr; // such can be found at the initialization step canonic_left_side * m_infeasible_canonic_left_side = nullptr; // such can be found at the initialization step
canonic_left_side * create_or_fetch_existing_left_side(const buffer<std::pair<mpq, var_index>>& left_side_par); canonic_left_side * create_or_fetch_existing_left_side(const buffer<std::pair<mpq, var_index>>& left_side_par);
@ -150,9 +148,7 @@ public:
m_basis, m_basis,
m_A, m_A,
m_settings, m_settings,
m_column_names, m_column_names) {
m_right_side_vector,
m_costs) {
} }
@ -178,21 +174,16 @@ public:
void update_column_info_of_normalized_constraints(); void update_column_info_of_normalized_constraints();
template <typename V>
void init_right_sides_with_zeros(std::vector<V> & rs);
mpq sum_of_right_sides_of_evidence(const buffer<std::pair<mpq, unsigned>> & evidence); mpq sum_of_right_sides_of_evidence(const buffer<std::pair<mpq, unsigned>> & evidence);
void prepare_independently_of_numeric_type(); void prepare_independently_of_numeric_type();
template <typename U, typename V> template <typename U, typename V>
void prepare_core_solver_fields(static_matrix<U, V> & A, std::vector<V> & x, void prepare_core_solver_fields(static_matrix<U, V> & A, std::vector<V> & x,
std::vector<V> & right_side_vector,
std::vector<V> & low_bound, std::vector<V> & low_bound,
std::vector<V> & upper_bound); std::vector<V> & upper_bound);
template <typename U, typename V> template <typename U, typename V>
void prepare_core_solver_fields_with_signature(static_matrix<U, V> & A, std::vector<V> & x, void prepare_core_solver_fields_with_signature(static_matrix<U, V> & A, std::vector<V> & x,
std::vector<V> & right_side_vector,
std::vector<V> & low_bound, std::vector<V> & low_bound,
std::vector<V> & upper_bound, const lar_solution_signature & signature); std::vector<V> & upper_bound, const lar_solution_signature & signature);