mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-29 03:45:51 +00:00
Code Activity

format

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-08-04 09:20:36 -07:00 • committed by Lev Nachmanson
parent 0c98c755ba
commit c3a373e225
2 changed files with 12 additions and 17 deletions
Download patch file Download diff file Expand all files Collapse all files

13
src/math/lp/lar_solver.cpp
View file

@ -481,12 +481,9 @@ namespace lp {
bool lar_solver::remove_from_basis(unsigned j) {
lp_assert(is_base(j));
unsigned i = row_of_basic_column(j);
for (const auto & c : A_r().m_rows[i]) {
if (j != c.var() && !is_fixed(c.var())) {
for (const auto & c : A_r().m_rows[i])
if (j != c.var() && !is_fixed(c.var()))
return m_mpq_lar_core_solver.m_r_solver.remove_from_basis_core(c.var(), j);
}
}
return false;
}
@ -630,7 +627,7 @@ namespace lp {
}
void lar_solver::remove_fixed_vars_from_base() {
// this will allow to disable and restore the tracking of the touched rows
// this will allow to disable and restore the tracking of the touched rows
flet<indexed_uint_set*> f(m_mpq_lar_core_solver.m_r_solver.m_touched_rows, nullptr);
unsigned num = A_r().column_count();
unsigned_vector to_remove;
@ -1782,9 +1779,9 @@ namespace lp {
update_column_type_and_bound_with_ub(j, kind, right_side, constr_index);
else
update_column_type_and_bound_with_no_ub(j, kind, right_side, constr_index);
if (is_base(j) && column_is_fixed(j)) {
if (is_base(j) && column_is_fixed(j))
m_fixed_base_var_set.insert(j);
}
TRACE("lar_solver_feas", tout << "j = " << j << " became " << (this->column_is_feasible(j)?"feas":"non-feas") << ", and " << (this->column_is_bounded(j)? "bounded":"non-bounded") << std::endl;);
}

16
src/math/lp/lp_core_solver_base_def.h
View file

@ -405,16 +405,14 @@ template <typename T, typename X> void lp_core_solver_base<T, X>::transpose_row
}
// entering is the new base column, leaving - the column leaving the basis
template <typename T, typename X> bool lp_core_solver_base<T, X>::pivot_column_general(unsigned entering, unsigned leaving, indexed_vector<T> & w) {
lp_assert(m_basis_heading[entering] < 0);
lp_assert(m_basis_heading[leaving] >= 0);
unsigned row_index = m_basis_heading[leaving];
// the tableau case
if (pivot_column_tableau(entering, row_index))
change_basis(entering, leaving);
else
lp_assert(m_basis_heading[entering] < 0);
lp_assert(m_basis_heading[leaving] >= 0);
unsigned row_index = m_basis_heading[leaving];
// the tableau case
if (!pivot_column_tableau(entering, row_index))
return false;
return true;
change_basis(entering, leaving);
return true;
}