Skip to content

Commit

Permalink
rm lu
Browse files Browse the repository at this point in the history 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
  • Loading branch information
@levnach
levnach committed Mar 8, 2023
1 parent 5f03c93 commit 62bd3bd
Show file tree
Hide file tree
Showing 11 changed files with 22 additions and 461 deletions.
241 changes: 3 additions & 238 deletions src/math/lp/lar_core_solver.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -190,16 +190,12 @@ class lar_core_solver {
m_r_upper_bounds.pop(k);
m_column_types.pop(k);

delete m_r_solver.m_factorization;
m_r_solver.m_factorization = nullptr;
m_r_x.resize(m_r_A.column_count());
m_r_solver.m_costs.resize(m_r_A.column_count());
m_r_solver.m_d.resize(m_r_A.column_count());

m_d_A.pop(k);
// doubles
delete m_d_solver.m_factorization;
m_d_solver.m_factorization = nullptr;

m_d_x.resize(m_d_A.column_count());
pop_basis(k);
Expand Down Expand Up @@ -294,172 +290,13 @@ class lar_core_solver {
unsigned jb = m_r_solver.m_basis[i];
m_r_solver.add_delta_to_x_and_track_feasibility(jb, - delta * m_r_solver.m_A.get_val(cc));
}
CASSERT("A_off", m_r_solver.A_mult_x_is_off() == false);

}
lp_assert(m_r_solver.inf_set_is_correct());
}


template <typename L, typename K>
void prepare_solver_x_with_signature(const lar_solution_signature & signature, lp_primal_core_solver<L,K> & s) {
for (auto &t : signature) {
unsigned j = t.first;
lp_assert(m_r_heading[j] < 0);
auto pos_type = t.second;
switch (pos_type) {
case at_lower_bound:
s.m_x[j] = s.m_lower_bounds[j];
break;
case at_fixed:
case at_upper_bound:
s.m_x[j] = s.m_upper_bounds[j];
break;
case free_of_bounds: {
s.m_x[j] = zero_of_type<K>();
continue;
}
case not_at_bound:
switch (m_column_types[j]) {
case column_type::free_column:
lp_assert(false); // unreachable
break;
case column_type::upper_bound:
s.m_x[j] = s.m_upper_bounds[j];
break;
case column_type::lower_bound:
s.m_x[j] = s.m_lower_bounds[j];
break;
case column_type::boxed:
if (settings().random_next() % 2) {
s.m_x[j] = s.m_lower_bounds[j];
} else {
s.m_x[j] = s.m_upper_bounds[j];
}
break;
case column_type::fixed:
s.m_x[j] = s.m_lower_bounds[j];
break;
default:
lp_assert(false);
}
break;
default:
lp_unreachable();
}
}

// lp_assert(is_zero_vector(s.m_b));
s.solve_Ax_eq_b();
}

template <typename L, typename K>
void catch_up_in_lu_in_reverse(const vector<unsigned> & trace_of_basis_change, lp_primal_core_solver<L,K> & cs) {
// recover the previous working basis
for (unsigned i = trace_of_basis_change.size(); i > 0; i-= 2) {
unsigned entering = trace_of_basis_change[i-1];
unsigned leaving = trace_of_basis_change[i-2];
cs.change_basis_unconditionally(entering, leaving);
}
cs.init_lu();
}

//basis_heading is the basis heading of the solver owning trace_of_basis_change
// here we compact the trace as we go to avoid unnecessary column changes
template <typename L, typename K>
void catch_up_in_lu(const vector<unsigned> & trace_of_basis_change, const vector<int> & basis_heading, lp_primal_core_solver<L,K> & cs) {
if (cs.m_factorization == nullptr || cs.m_factorization->m_refactor_counter + trace_of_basis_change.size()/2 >= 200) {
for (unsigned i = 0; i < trace_of_basis_change.size(); i+= 2) {
unsigned entering = trace_of_basis_change[i];
unsigned leaving = trace_of_basis_change[i+1];
cs.change_basis_unconditionally(entering, leaving);
}
if (cs.m_factorization != nullptr) {
delete cs.m_factorization;
cs.m_factorization = nullptr;
}
} else {
indexed_vector<L> w(cs.m_A.row_count());
// the queues of delayed indices
std::queue<unsigned> entr_q, leav_q;
auto * l = cs.m_factorization;
lp_assert(l->get_status() == LU_status::OK);
for (unsigned i = 0; i < trace_of_basis_change.size(); i+= 2) {
unsigned entering = trace_of_basis_change[i];
unsigned leaving = trace_of_basis_change[i+1];
bool good_e = basis_heading[entering] >= 0 && cs.m_basis_heading[entering] < 0;
bool good_l = basis_heading[leaving] < 0 && cs.m_basis_heading[leaving] >= 0;
if (!good_e && !good_l) continue;
if (good_e && !good_l) {
while (!leav_q.empty() && cs.m_basis_heading[leav_q.front()] < 0)
leav_q.pop();
if (!leav_q.empty()) {
leaving = leav_q.front();
leav_q.pop();
} else {
entr_q.push(entering);
continue;
}
} else if (!good_e && good_l) {
while (!entr_q.empty() && cs.m_basis_heading[entr_q.front()] >= 0)
entr_q.pop();
if (!entr_q.empty()) {
entering = entr_q.front();
entr_q.pop();
} else {
leav_q.push(leaving);
continue;
}
}
lp_assert(cs.m_basis_heading[entering] < 0);
lp_assert(cs.m_basis_heading[leaving] >= 0);
if (l->get_status() == LU_status::OK) {
l->prepare_entering(entering, w); // to init vector w
l->replace_column(zero_of_type<L>(), w, cs.m_basis_heading[leaving]);
}
cs.change_basis_unconditionally(entering, leaving);
}
if (l->get_status() != LU_status::OK) {
delete l;
cs.m_factorization = nullptr;
}
}
if (cs.m_factorization == nullptr) {
if (numeric_traits<L>::precise())
init_factorization(cs.m_factorization, cs.m_A, cs.m_basis, settings());
}
}

bool no_r_lu() const {
return m_r_solver.m_factorization == nullptr || m_r_solver.m_factorization->get_status() == LU_status::Degenerated;
}

void solve_on_signature_tableau(const lar_solution_signature & signature, const vector<unsigned> & changes_of_basis) {
r_basis_is_OK();
bool r = catch_up_in_lu_tableau(changes_of_basis, m_d_solver.m_basis_heading);

if (!r) { // it is the case where m_d_solver gives a degenerated basis
prepare_solver_x_with_signature_tableau(signature); // still are going to use the signature partially
m_r_solver.find_feasible_solution();
m_d_basis = m_r_basis;
m_d_heading = m_r_heading;
m_d_nbasis = m_r_nbasis;
delete m_d_solver.m_factorization;
m_d_solver.m_factorization = nullptr;
}
else {
prepare_solver_x_with_signature_tableau(signature);
m_r_solver.start_tracing_basis_changes();
m_r_solver.find_feasible_solution();
if (settings().get_cancel_flag())
return;
m_r_solver.stop_tracing_basis_changes();
// and now catch up in the double solver
lp_assert(m_r_solver.total_iterations() >= m_r_solver.m_trace_of_basis_change_vector.size() /2);
catch_up_in_lu(m_r_solver.m_trace_of_basis_change_vector, m_r_solver.m_basis_heading, m_d_solver);
}
lp_assert(r_basis_is_OK());
}


bool adjust_x_of_column(unsigned j) {
/*
if (m_r_solver.m_basis_heading[j] >= 0) {
Expand All @@ -478,58 +315,6 @@ class lar_core_solver {
return true;
}


bool catch_up_in_lu_tableau(const vector<unsigned> & trace_of_basis_change, const vector<int> & basis_heading) {
lp_assert(r_basis_is_OK());
// the queues of delayed indices
std::queue<unsigned> entr_q, leav_q;
for (unsigned i = 0; i < trace_of_basis_change.size(); i+= 2) {
unsigned entering = trace_of_basis_change[i];
unsigned leaving = trace_of_basis_change[i+1];
bool good_e = basis_heading[entering] >= 0 && m_r_solver.m_basis_heading[entering] < 0;
bool good_l = basis_heading[leaving] < 0 && m_r_solver.m_basis_heading[leaving] >= 0;
if (!good_e && !good_l) continue;
if (good_e && !good_l) {
while (!leav_q.empty() && m_r_solver.m_basis_heading[leav_q.front()] < 0)
leav_q.pop();
if (!leav_q.empty()) {
leaving = leav_q.front();
leav_q.pop();
} else {
entr_q.push(entering);
continue;
}
} else if (!good_e && good_l) {
while (!entr_q.empty() && m_r_solver.m_basis_heading[entr_q.front()] >= 0)
entr_q.pop();
if (!entr_q.empty()) {
entering = entr_q.front();
entr_q.pop();
} else {
leav_q.push(leaving);
continue;
}
}
lp_assert(m_r_solver.m_basis_heading[entering] < 0);
lp_assert(m_r_solver.m_basis_heading[leaving] >= 0);
m_r_solver.change_basis_unconditionally(entering, leaving);
if(!m_r_solver.pivot_column_tableau(entering, m_r_solver.m_basis_heading[entering])) {
// unroll the last step
m_r_solver.change_basis_unconditionally(leaving, entering);
#ifdef Z3DEBUG
bool t =
#endif
m_r_solver.pivot_column_tableau(leaving, m_r_solver.m_basis_heading[leaving]);
#ifdef Z3DEBUG
lp_assert(t);
#endif
return false;
}
}
lp_assert(r_basis_is_OK());
return true;
}


bool r_basis_is_OK() const {
#ifdef Z3DEBUG
Expand Down Expand Up @@ -598,27 +383,7 @@ class lar_core_solver {
}


// returns the trace of basis changes
vector<unsigned> find_solution_signature_with_doubles(lar_solution_signature & signature) {
if (m_d_solver.m_factorization == nullptr || m_d_solver.m_factorization->get_status() != LU_status::OK) {
vector<unsigned> ret;
return ret;
}
get_bounds_for_double_solver();

extract_signature_from_lp_core_solver(m_r_solver, signature);
prepare_solver_x_with_signature(signature, m_d_solver);
m_d_solver.start_tracing_basis_changes();
m_d_solver.find_feasible_solution();
if (settings().get_cancel_flag())
return vector<unsigned>();

m_d_solver.stop_tracing_basis_changes();
extract_signature_from_lp_core_solver(m_d_solver, signature);
return m_d_solver.m_trace_of_basis_change_vector;
}



bool lower_bound_is_set(unsigned j) const {
switch (m_column_types[j]) {
case column_type::free_column:
Expand Down
28 changes: 7 additions & 21 deletions src/math/lp/lar_core_solver_def.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -78,7 +78,6 @@ void lar_core_solver::prefix_d() {
}

void lar_core_solver::fill_not_improvable_zero_sum_from_inf_row() {
CASSERT("A_off", m_r_solver.A_mult_x_is_off() == false);
unsigned bj = m_r_basis[m_r_solver.m_inf_row_index_for_tableau];
m_infeasible_sum_sign = m_r_solver.inf_sign_of_column(bj);
m_infeasible_linear_combination.clear();
Expand Down Expand Up @@ -127,29 +126,16 @@ void lar_core_solver::solve() {
return;
}
++settings().stats().m_need_to_solve_inf;
CASSERT("A_off", !m_r_solver.A_mult_x_is_off());
lp_assert( r_basis_is_OK());
if (need_to_presolve_with_double_solver()) {
TRACE("lar_solver", tout << "presolving\n";);
prefix_d();
lar_solution_signature solution_signature;
vector<unsigned> changes_of_basis = find_solution_signature_with_doubles(solution_signature);
if (m_d_solver.get_status() == lp_status::TIME_EXHAUSTED) {
m_r_solver.set_status(lp_status::TIME_EXHAUSTED);
return;
}
solve_on_signature_tableau(solution_signature, changes_of_basis);

lp_assert( r_basis_is_OK());
} else {


if (m_r_solver.m_look_for_feasible_solution_only) //todo : should it be set?
m_r_solver.find_feasible_solution();
else {
m_r_solver.solve();
}
lp_assert(r_basis_is_OK());
if (m_r_solver.m_look_for_feasible_solution_only) //todo : should it be set?
m_r_solver.find_feasible_solution();
else {
m_r_solver.solve();
}
lp_assert(r_basis_is_OK());

switch (m_r_solver.get_status())
{
case lp_status::INFEASIBLE:
Expand Down
11 changes: 0 additions & 11 deletions src/math/lp/lp_core_solver_base.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -23,8 +23,6 @@ Revision History:
#include "util/vector.h"
#include <functional>
#include "math/lp/lp_core_solver_base_def.h"
template bool lp::lp_core_solver_base<double, double>::A_mult_x_is_off() const;
template bool lp::lp_core_solver_base<double, double>::A_mult_x_is_off_on_index(const vector<unsigned> &) const;
template bool lp::lp_core_solver_base<double, double>::basis_heading_is_correct() const;
template void lp::lp_core_solver_base<double, double>::calculate_pivot_row_when_pivot_row_of_B1_is_ready(unsigned);
template bool lp::lp_core_solver_base<double, double>::column_is_dual_feasible(unsigned int) const;
Expand All @@ -33,7 +31,6 @@ template bool lp::lp_core_solver_base<double, double>::find_x_by_solving();
template lp::non_basic_column_value_position lp::lp_core_solver_base<double, double>::get_non_basic_column_value_position(unsigned int) const;
template lp::non_basic_column_value_position lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::get_non_basic_column_value_position(unsigned int) const;
template lp::non_basic_column_value_position lp::lp_core_solver_base<lp::mpq, lp::mpq>::get_non_basic_column_value_position(unsigned int) const;
template void lp::lp_core_solver_base<double, double>::init_reduced_costs_for_one_iteration();
template lp::lp_core_solver_base<double, double>::lp_core_solver_base(
lp::static_matrix<double, double>&, // vector<double>&,
vector<unsigned>&,
Expand All @@ -51,26 +48,20 @@ template void lp::lp_core_solver_base<double, double>::set_non_basic_x_to_correc
template void lp::lp_core_solver_base<double, double>::snap_xN_to_bounds_and_free_columns_to_zeroes();
template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::snap_xN_to_bounds_and_free_columns_to_zeroes();
template void lp::lp_core_solver_base<double, double>::solve_Ax_eq_b();
template void lp::lp_core_solver_base<double, double>::solve_yB(vector<double >&) const;
template void lp::lp_core_solver_base<double, double>::add_delta_to_entering(unsigned int, const double&);
template bool lp::lp_core_solver_base<lp::mpq, lp::mpq>::A_mult_x_is_off() const;
template bool lp::lp_core_solver_base<lp::mpq, lp::mpq>::A_mult_x_is_off_on_index(const vector<unsigned> &) const;
template bool lp::lp_core_solver_base<lp::mpq, lp::mpq>::basis_heading_is_correct() const ;
template void lp::lp_core_solver_base<lp::mpq, lp::mpq>::calculate_pivot_row_when_pivot_row_of_B1_is_ready(unsigned);
template bool lp::lp_core_solver_base<lp::mpq, lp::mpq>::column_is_dual_feasible(unsigned int) const;
template void lp::lp_core_solver_base<lp::mpq, lp::mpq>::fill_reduced_costs_from_m_y_by_rows();
template bool lp::lp_core_solver_base<lp::mpq, lp::mpq>::find_x_by_solving();
template void lp::lp_core_solver_base<lp::mpq, lp::mpq>::init_reduced_costs_for_one_iteration();
template bool lp::lp_core_solver_base<lp::mpq, lp::mpq>::print_statistics_with_iterations_and_nonzeroes_and_cost_and_check_that_the_time_is_over(char const*, std::ostream &);
template void lp::lp_core_solver_base<lp::mpq, lp::mpq>::restore_x(unsigned int, lp::mpq const&);
template void lp::lp_core_solver_base<lp::mpq, lp::mpq>::set_non_basic_x_to_correct_bounds();
template void lp::lp_core_solver_base<lp::mpq, lp::mpq>::solve_Ax_eq_b();
template void lp::lp_core_solver_base<lp::mpq, lp::mpq>::solve_yB(vector<lp::mpq>&) const;
template void lp::lp_core_solver_base<lp::mpq, lp::mpq>::add_delta_to_entering(unsigned int, const lp::mpq&);
template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::calculate_pivot_row_when_pivot_row_of_B1_is_ready(unsigned);
template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::init();
template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::init_basis_heading_and_non_basic_columns_vector();
template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::init_reduced_costs_for_one_iteration();
template lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::lp_core_solver_base(lp::static_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >&,
// vector<lp::numeric_pair<lp::mpq> >&,
vector<unsigned int >&, vector<unsigned> &, vector<int> &, vector<lp::numeric_pair<lp::mpq> >&, vector<lp::mpq>&, lp::lp_settings&, const column_namer&, const vector<lp::column_type >&,
Expand Down Expand Up @@ -106,7 +97,6 @@ template std::string lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq>
template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::pretty_print(std::ostream & out);
template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::restore_state(lp::mpq*, lp::mpq*);
template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::save_state(lp::mpq*, lp::mpq*);
template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::solve_yB(vector<lp::mpq>&) const;
template void lp::lp_core_solver_base<double, double>::init_lu();
template void lp::lp_core_solver_base<lp::mpq, lp::mpq>::init_lu();
template int lp::lp_core_solver_base<double, double>::pivots_in_column_and_row_are_different(int, int) const;
Expand All @@ -122,7 +112,6 @@ template bool lp::lp_core_solver_base<lp::mpq, lp::mpq>::column_is_feasible(unsi
template bool lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::column_is_feasible(unsigned int) const;
template bool lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::snap_non_basic_x_to_bound();
template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::init_lu();
template bool lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::A_mult_x_is_off_on_index(vector<unsigned int> const&) const;
template bool lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::find_x_by_solving();
template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::restore_x(unsigned int, lp::numeric_pair<lp::mpq> const&);
template bool lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq>>::pivot_column_tableau(unsigned int, unsigned int);
Expand Down
Loading

0 comments on commit 62bd3bd

Please sign in to comment.