Skip to content

Commit

Permalink
replace lp_assert(false) with UNREACHABLE
Browse files Browse the repository at this point in the history
  • Loading branch information
@levnach
levnach committed Mar 8, 2023
1 parent 3efe91c commit 8b0aa22
Show file tree
Hide file tree
Showing 23 changed files with 677 additions and 914 deletions.
2 changes: 1 addition & 1 deletion src/math/lp/core_solver_pretty_printer_def.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -139,7 +139,7 @@ template <typename T, typename X> void core_solver_pretty_printer<T, X>::adjust_
case column_type::free_column:
break;
default:
lp_assert(false);
UNREACHABLE();
break;
}
}
Expand Down
22 changes: 1 addition & 21 deletions src/math/lp/general_matrix.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -114,9 +114,6 @@ class general_matrix {
}
}

void copy_column_to_indexed_vector(unsigned entering, indexed_vector<mpq> &w ) const {
lp_assert(false); // not implemented
}
general_matrix operator*(const general_matrix & m) const {
lp_assert(m.row_count() == column_count());
general_matrix ret(row_count(), m.column_count());
Expand Down Expand Up @@ -172,24 +169,7 @@ class general_matrix {
return r;
}

// bool create_upper_triangle(general_matrix& m, vector<mpq>& x) {
// for (unsigned i = 1; i < m.row_count(); i++) {
// lp_assert(false); // to be continued
// }
// }

// bool solve_A_x_equal_b(const general_matrix& m, vector<mpq>& x, const vector<mpq>& b) const {
// auto m_copy = m;
// // for square matrices
// lp_assert(row_count() == b.size());
// lp_assert(x.size() == column_count());
// lp_assert(row_count() == column_count());
// x = b;
// create_upper_triangle(copy_of_m, x);
// solve_on_triangle(copy_of_m, x);
// }
//


void transpose_rows(unsigned i, unsigned l) {
lp_assert(i != l);
m_row_permutation.transpose_from_right(i, l);
Expand Down
2 changes: 1 addition & 1 deletion src/math/lp/lar_constraints.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -44,7 +44,7 @@ inline std::string lconstraint_kind_string(lconstraint_kind t) {
case EQ: return std::string("=");
case NE: return std::string("!=");
}
lp_unreachable();
UNREACHABLE();
return std::string(); // it is unreachable
}

Expand Down
4 changes: 2 additions & 2 deletions src/math/lp/lar_core_solver.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -159,7 +159,7 @@ class lar_core_solver {
case column_type::fixed:
return true;
default:
lp_assert(false);
UNREACHABLE();
}
return false;
}
Expand All @@ -174,7 +174,7 @@ class lar_core_solver {
case column_type::fixed:
return true;
default:
lp_assert(false);
UNREACHABLE();
}
return false;
}
Expand Down
16 changes: 8 additions & 8 deletions src/math/lp/lar_solver.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -466,7 +466,7 @@ namespace lp {


default:
lp_unreachable(); // wrong mode
UNREACHABLE(); // wrong mode
}
return false;
}
Expand Down Expand Up @@ -802,7 +802,7 @@ namespace lp {
case GT: return left_side_val > constr.rhs();
case EQ: return left_side_val == constr.rhs();
default:
lp_unreachable();
UNREACHABLE();
}
return false; // it is unreachable
}
Expand Down Expand Up @@ -857,7 +857,7 @@ namespace lp {
case EQ: lp_assert(rs != zero_of_type<mpq>());
break;
default:
lp_assert(false);
UNREACHABLE();
return false;
}
#endif
Expand Down Expand Up @@ -1816,7 +1816,7 @@ namespace lp {
adjust_initial_state_for_tableau_rows();
break;
case simplex_strategy_enum::tableau_costs:
lp_assert(false); // not implemented
UNREACHABLE(); // not implemented
case simplex_strategy_enum::undecided:
adjust_initial_state_for_tableau_rows();
break;
Expand Down Expand Up @@ -1905,7 +1905,7 @@ namespace lp {
}

default:
lp_unreachable();
UNREACHABLE();
}
if (m_mpq_lar_core_solver.m_r_upper_bounds[j] == m_mpq_lar_core_solver.m_r_lower_bounds[j]) {
m_mpq_lar_core_solver.m_column_types[j] = column_type::fixed;
Expand Down Expand Up @@ -1959,7 +1959,7 @@ namespace lp {
}

default:
lp_unreachable();
UNREACHABLE();
}

}
Expand Down Expand Up @@ -2009,7 +2009,7 @@ namespace lp {
}

default:
lp_unreachable();
UNREACHABLE();
}
}
void lar_solver::update_bound_with_no_ub_no_lb(var_index j, lconstraint_kind kind, const mpq& right_side, constraint_index ci) {
Expand Down Expand Up @@ -2050,7 +2050,7 @@ namespace lp {
}

default:
lp_unreachable();
UNREACHABLE();
}
}

Expand Down
2 changes: 1 addition & 1 deletion src/math/lp/lar_term.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -179,7 +179,7 @@ class lar_term {
return p.coeff().is_one();
}
}
lp_unreachable();
UNREACHABLE();
return false;
}

Expand Down
2 changes: 1 addition & 1 deletion src/math/lp/lia_move.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -45,7 +45,7 @@ inline std::string lia_move_to_string(lia_move m) {
case lia_move::unsat:
return "unsat";
default:
lp_assert(false);
UNREACHABLE();
};
return "strange";
}
Expand Down
3 changes: 0 additions & 3 deletions src/math/lp/lp_core_solver_base.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,6 @@ template bool lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::prin
template bool lp::lp_core_solver_base<lp::mpq, lp::mpq>::basis_heading_is_correct() const ;
template bool lp::lp_core_solver_base<lp::mpq, lp::mpq>::column_is_dual_feasible(unsigned int) const;
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>::set_non_basic_x_to_correct_bounds();
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> >::init();
template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::init_basis_heading_and_non_basic_columns_vector();
Expand Down Expand Up @@ -61,7 +60,6 @@ template bool lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::calc
template bool lp::lp_core_solver_base<lp::mpq, lp::mpq>::column_is_feasible(unsigned int) const;
// template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::print_linear_combination_of_column_indices(vector<std::pair<lp::mpq, unsigned int>, std::allocator<std::pair<lp::mpq, unsigned int> > > const&, std::ostream&) const;
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 bool lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq>>::pivot_column_tableau(unsigned int, unsigned int);
template bool lp::lp_core_solver_base<lp::mpq, lp::mpq>::pivot_column_tableau(unsigned int, unsigned int);
template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::transpose_rows_tableau(unsigned int, unsigned int);
Expand All @@ -70,6 +68,5 @@ template bool lp::lp_core_solver_base<lp::mpq, lp::mpq>::inf_set_is_correct() co
template bool lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::infeasibility_costs_are_correct() const;
template bool lp::lp_core_solver_base<lp::mpq, lp::mpq >::infeasibility_costs_are_correct() const;
template bool lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::remove_from_basis(unsigned int);
template bool lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::remove_from_basis(unsigned int, lp::numeric_pair<lp::mpq> const&);


81 changes: 1 addition & 80 deletions src/math/lp/lp_core_solver_base.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -173,8 +173,6 @@ class lp_core_solver_base {

void set_total_iterations(unsigned s) { m_total_iterations = s; }

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);
}
Expand Down Expand Up @@ -300,45 +298,6 @@ class lp_core_solver_base {

std::string column_name(unsigned column) const;

bool snap_non_basic_x_to_bound() {
bool ret = false;
for (unsigned j : non_basis())
ret = snap_column_to_bound(j) || ret;
return ret;
}

bool snap_column_to_bound(unsigned j) {
switch (m_column_types[j]) {
case column_type::fixed:
if (x_is_at_bound(j))
break;
m_x[j] = m_lower_bounds[j];
return true;
case column_type::boxed:
if (x_is_at_bound(j))
break; // we should preserve x if possible
// snap randomly
if (m_settings.random_next() % 2 == 1)
m_x[j] = m_lower_bounds[j];
else
m_x[j] = m_upper_bounds[j];
return true;
case column_type::lower_bound:
if (x_is_at_lower_bound(j))
break;
m_x[j] = m_lower_bounds[j];
return true;
case column_type::upper_bound:
if (x_is_at_upper_bound(j))
break;
m_x[j] = m_upper_bounds[j];
return true;
default:
break;
}
return false;
}

bool make_column_feasible(unsigned j, numeric_pair<mpq> & delta) {
bool ret = false;
lp_assert(m_basis_heading[j] < 0);
Expand Down Expand Up @@ -384,7 +343,6 @@ class lp_core_solver_base {
}

bool remove_from_basis(unsigned j);
bool remove_from_basis(unsigned j, const impq&);
bool pivot_column_general(unsigned j, unsigned j_basic, indexed_vector<T> & w);
void init_basic_part_of_basis_heading() {
unsigned m = m_basis.size();
Expand Down Expand Up @@ -456,31 +414,6 @@ class lp_core_solver_base {
change_basis_unconditionally(leaving, entering);
}

bool non_basic_column_is_set_correctly(unsigned j) const {
if (j >= this->m_n())
return false;
switch (this->m_column_types[j]) {
case column_type::fixed:
case column_type::boxed:
if (!this->x_is_at_bound(j))
return false;
break;
case column_type::lower_bound:
if (!this->x_is_at_lower_bound(j))
return false;
break;
case column_type::upper_bound:
if (!this->x_is_at_upper_bound(j))
return false;
break;
case column_type::free_column:
break;
default:
lp_assert(false);
break;
}
return true;
}
bool non_basic_columns_are_set_correctly() const {
for (unsigned j : this->m_nbasis)
if (!column_is_feasible(j)) {
Expand Down Expand Up @@ -540,13 +473,11 @@ class lp_core_solver_base {
out << "[-oo, oo]";
break;
default:
lp_assert(false);
UNREACHABLE();
}
return out << "\n";
}

bool column_is_free(unsigned j) const { return this->m_column_types[j] == column_type::free_column; }

bool column_is_fixed(unsigned j) const { return this->m_column_types[j] == column_type::fixed; }


Expand Down Expand Up @@ -579,16 +510,6 @@ class lp_core_solver_base {
}
}

// only check for basic columns
bool calc_current_x_is_feasible() const {
unsigned i = this->m_m();
while (i--) {
if (!column_is_feasible(m_basis[i]))
return false;
}
return true;
}

void transpose_rows_tableau(unsigned i, unsigned ii);

void pivot_to_reduced_costs_tableau(unsigned i, unsigned j);
Expand Down
40 changes: 4 additions & 36 deletions src/math/lp/lp_core_solver_base_def.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -166,26 +166,6 @@ print_statistics_with_cost_and_check_that_the_time_is_over(X cost, std::ostream
return time_is_over();
}

template <typename T, typename X> void lp_core_solver_base<T, X>::
set_non_basic_x_to_correct_bounds() {
for (unsigned j : non_basis()) {
switch (m_column_types[j]) {
case column_type::boxed:
m_x[j] = m_d[j] < 0? m_upper_bounds[j]: m_lower_bounds[j];
break;
case column_type::lower_bound:
m_x[j] = m_lower_bounds[j];
lp_assert(column_is_dual_feasible(j));
break;
case column_type::upper_bound:
m_x[j] = m_upper_bounds[j];
lp_assert(column_is_dual_feasible(j));
break;
default:
break;
}
}
}
template <typename T, typename X> bool lp_core_solver_base<T, X>::
column_is_dual_feasible(unsigned j) const {
switch (m_column_types[j]) {
Expand All @@ -201,9 +181,9 @@ column_is_dual_feasible(unsigned j) const {
case column_type::free_column:
return numeric_traits<X>::is_zero(m_d[j]);
default:
lp_unreachable();
UNREACHABLE();
}
lp_unreachable();
UNREACHABLE();
return false;
}
template <typename T, typename X> bool lp_core_solver_base<T, X>::
Expand Down Expand Up @@ -257,7 +237,7 @@ template <typename T, typename X> bool lp_core_solver_base<T, X>::column_is_feas
return true;
break;
default:
lp_unreachable();
UNREACHABLE();
}
return false; // it is unreachable
}
Expand Down Expand Up @@ -453,18 +433,6 @@ template <typename T, typename X> bool lp_core_solver_base<T, X>::remove_from_ba
return false;
}

template <typename T, typename X> bool lp_core_solver_base<T, X>::remove_from_basis(unsigned basic_j, const impq& val) {
indexed_vector<T> w(m_basis.size()); // the buffer
unsigned i = m_basis_heading[basic_j];
for (auto &c : m_A.m_rows[i]) {
if (c.var() == basic_j)
continue;
if (pivot_column_general(c.var(), basic_j, w))
return true;
}
return false;
}


template <typename T, typename X> bool
lp_core_solver_base<T, X>::infeasibility_costs_are_correct() const {
Expand Down Expand Up @@ -513,7 +481,7 @@ lp_core_solver_base<T, X>::infeasibility_cost_is_correct_for_column(unsigned j)
case column_type::free_column:
return is_zero(this->m_costs[j]);
default:
lp_assert(false);
UNREACHABLE();
return true;
}
}
Expand Down
Loading

0 comments on commit 8b0aa22

Please sign in to comment.