mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-09 04:31:24 +00:00
Code Activity

small changes in one_iteration_tableau_rows

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-04-12 14:08:35 -07:00
parent 9223f611ba
commit 90793931b1
2 changed files with 26 additions and 18 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/math/lp/lp_core_solver_base.h
View file

@ -685,6 +685,11 @@ public:
return m_inf_set.contains(j); return m_inf_set.contains(j);
} }
bool column_is_base(unsigned j) const {
return m_basis_heading[j] >= 0;
}
void update_x_with_feasibility_tracking(unsigned j, const X & v) { void update_x_with_feasibility_tracking(unsigned j, const X & v) {
TRACE("lar_solver", tout << "j = " << j << ", v = " << v << "\n";); TRACE("lar_solver", tout << "j = " << j << ", v = " << v << "\n";);
m_x[j] = v; m_x[j] = v;

57
src/math/lp/lp_primal_core_solver.h
View file

@ -447,46 +447,47 @@ public:
this->track_column_feasibility(entering); this->track_column_feasibility(entering);
} }
int find_smallest_inf_column() {
int find_leaving_tableau_rows(X & new_val_for_leaving) {
int j = -1; int j = -1;
for (unsigned k : this->m_inf_set) { for (unsigned k : this->m_inf_set) {
if (k < static_cast<unsigned>(j)) if (k < static_cast<unsigned>(j)) {
j = static_cast<int>(k); j = k;
} }
if (j == -1)
return -1;
lp_assert(!this->column_is_feasible(j));
switch (this->m_column_types[j]) {
case column_type::fixed:
case column_type::upper_bound:
new_val_for_leaving = this->m_upper_bounds[j];
break;
case column_type::lower_bound:
new_val_for_leaving = this->m_lower_bounds[j];
break;
case column_type::boxed:
if (this->x_above_upper_bound(j))
new_val_for_leaving = this->m_upper_bounds[j];
else
new_val_for_leaving = this->m_lower_bounds[j];
break;
default:
lp_assert(false);
new_val_for_leaving = numeric_traits<X>::zero(); // does not matter
} }
return j; return j;
} }
const X& get_val_for_leaving(unsigned j) const {
lp_assert(!this->column_is_feasible(j));
switch (this->m_column_types[j]) {
case column_type::fixed:
case column_type::upper_bound:
return this->m_upper_bounds[j];
case column_type::lower_bound:
return this->m_lower_bounds[j];
break;
case column_type::boxed:
if (this->x_above_upper_bound(j))
return this->m_upper_bounds[j];
else
return this->m_lower_bounds[j];
break;
default:
UNREACHABLE();
return this->m_lower_bounds[j];
}
}
void one_iteration_tableau_rows() { void one_iteration_tableau_rows() {
X new_val_for_leaving; int leaving = find_smallest_inf_column();
int leaving = find_leaving_tableau_rows(new_val_for_leaving);
if (leaving == -1) { if (leaving == -1) {
this->set_status(lp_status::OPTIMAL); this->set_status(lp_status::OPTIMAL);
return; return;
} }
SASSERT(this->column_is_base(leaving));
if (!m_bland_mode_tableau) { if (!m_bland_mode_tableau) {
if (m_left_basis_tableau.contains(leaving)) { if (m_left_basis_tableau.contains(leaving)) {
if (++m_left_basis_repeated > m_bland_mode_threshold) { if (++m_left_basis_repeated > m_bland_mode_threshold) {
@ -502,9 +503,11 @@ public:
this->set_status(lp_status::INFEASIBLE); this->set_status(lp_status::INFEASIBLE);
return; return;
} }
const X& new_val_for_leaving = get_val_for_leaving(leaving);
X theta = (this->m_x[leaving] - new_val_for_leaving) / a_ent; X theta = (this->m_x[leaving] - new_val_for_leaving) / a_ent;
advance_on_entering_and_leaving_tableau_rows(entering, leaving, theta ); advance_on_entering_and_leaving_tableau_rows(entering, leaving, theta );
lp_assert(this->m_x[leaving] == new_val_for_leaving); lp_assert(this->m_x[leaving] == new_val_for_leaving);
lp_assert(this->column_is_feasible(leaving));
if (this->current_x_is_feasible()) if (this->current_x_is_feasible())
this->set_status(lp_status::OPTIMAL); this->set_status(lp_status::OPTIMAL);
} }