mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 21:08:46 +00:00
Code Activity

Merge branch 'master' of https://github.com/levnach/z3

Browse source
This commit is contained in:
Lev Nachmanson 2017-07-06 20:47:19 -07:00
parent 9b1b096a16 055593469a
commit 7cd6dc1b5a
1 changed files with 9 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
src/util/lp/lp_core_solver_base.hpp
View file

@ -83,8 +83,8 @@ pivot_for_tableau_on_basis() {
// i is the pivot row, and j is the pivot column
template <typename T, typename X> void lp_core_solver_base<T, X>::
pivot_to_reduced_costs_tableau(unsigned i, unsigned j) {
if (j >= m_d.size())
return;
if (j >= m_d.size())
return;
T &a = m_d[j];
if (is_zero(a))
return;
@ -925,9 +925,9 @@ template <typename T, typename X> void lp_core_solver_base<T, X>::transpose_row
}
// j is the new basic column, j_basic - the leaving column
template <typename T, typename X> bool lp_core_solver_base<T, X>::pivot_column_general(unsigned j, unsigned j_basic, indexed_vector<T> & w) {
lean_assert(m_basis_heading[j] < 0);
lean_assert(m_basis_heading[j_basic] >= 0);
unsigned row_index = m_basis_heading[j_basic];
lean_assert(m_basis_heading[j] < 0);
lean_assert(m_basis_heading[j_basic] >= 0);
unsigned row_index = m_basis_heading[j_basic];
change_basis(j, j_basic);
if (m_settings.m_simplex_strategy == simplex_strategy_enum::lu) {
if (m_factorization->need_to_refactor()) {
@ -952,7 +952,7 @@ template <typename T, typename X> void lp_core_solver_base<T, X>::pivot_fixed_v
indexed_vector<T> w(m_basis.size()); // the buffer
unsigned i = 0; // points to basis
unsigned j = 0; // points to nonbasis
for (; i < m_basis.size() && j < m_nbasis.size(); i++) {
unsigned ii = m_basis[i];
unsigned jj;
@ -967,9 +967,9 @@ template <typename T, typename X> void lp_core_solver_base<T, X>::pivot_fixed_v
if (j >= m_nbasis.size())
break;
j++;
if (!pivot_column_general(jj, ii, w))
return; // total failure
break;
if (!pivot_column_general(jj, ii, w))
return; // total failure
break;
}
}
}