mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity

small improvements in tableau in rows and bound propagation

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-04-13 11:54:52 -07:00
parent 90793931b1
commit 7caae3f5d2
4 changed files with 49 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/math/lp/bound_analyzer_on_row.h
View file

@ -60,8 +60,6 @@ public :
for (const auto & c : m_row) {
if ((m_column_of_l == -2) && (m_column_of_u == -2))
return;
if (c.coeff().is_big())
return;
analyze_bound_on_var_on_coeff(c.var(), c.coeff());
}
if (m_column_of_u >= 0)

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

@ -153,11 +153,20 @@ void lar_solver::analyze_new_bounds_on_row(
ra_pos.analyze();
}
bool lar_solver::row_has_a_big_num(unsigned i) const {
for (const auto& c : A_r().m_rows[i]) {
if (c.coeff().is_big())
return true;
}
return false;
}
void lar_solver::analyze_new_bounds_on_row_tableau(
unsigned row_index,
lp_bound_propagator & bp ) {
if (A_r().m_rows[row_index].size() > settings().max_row_length_for_bound_propagation)
if (A_r().m_rows[row_index].size() > settings().max_row_length_for_bound_propagation
|| row_has_a_big_num(row_index))
return;
lp_assert(use_tableau());
bound_analyzer_on_row<row_strip<mpq>>::analyze_row(A_r().m_rows[row_index],

2
src/math/lp/lar_solver.h
View file

@ -144,7 +144,7 @@ public:
bool column_is_free(unsigned j) const;
const lar_term & get_term(unsigned j) const;
bool row_has_a_big_num(unsigned i) const;
public:
// init region

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

@ -442,8 +442,43 @@ public:
void one_iteration();
void one_iteration_tableau();
// this version assumes that the leaving already has the right value, and does not update it
void update_x_tableau_rows(unsigned entering, unsigned leaving, const X& delta) {
this->add_delta_to_x(entering, delta);
if (!this->m_using_infeas_costs) {
for (const auto & c : this->m_A.m_columns[entering]) {
if (leaving != this->m_basis[c.var()]) {
this->add_delta_to_x_and_track_feasibility(this->m_basis[c.var()], - delta * this->m_A.get_val(c));
}
}
} else { // m_using_infeas_costs == true
lp_assert(this->column_is_feasible(entering));
lp_assert(this->m_costs[entering] == zero_of_type<T>());
// m_d[entering] can change because of the cost change for basic columns.
for (const auto & c : this->m_A.m_columns[entering]) {
unsigned j = this->m_basis[c.var()];
if (j != leaving)
this->add_delta_to_x(j, -delta * this->m_A.get_val(c));
update_inf_cost_for_column_tableau(j);
if (is_zero(this->m_costs[j]))
this->remove_column_from_inf_set(j);
else
this->insert_column_into_inf_set(j);
}
}
}
void update_basis_and_x_tableau_rows(int entering, int leaving, X const & tt) {
lp_assert(this->use_tableau());
lp_assert(entering != leaving);
update_x_tableau_rows(entering, leaving, tt);
this->pivot_column_tableau(entering, this->m_basis_heading[leaving]);
this->change_basis(entering, leaving);
}
void advance_on_entering_and_leaving_tableau_rows(int entering, int leaving, const X &theta ) {
this->update_basis_and_x_tableau(entering, leaving, theta);
update_basis_and_x_tableau_rows(entering, leaving, theta);
this->track_column_feasibility(entering);
}
@ -505,9 +540,9 @@ public:
}
const X& new_val_for_leaving = get_val_for_leaving(leaving);
X theta = (this->m_x[leaving] - new_val_for_leaving) / a_ent;
this->m_x[leaving] = new_val_for_leaving;
this->remove_column_from_inf_set(leaving);
advance_on_entering_and_leaving_tableau_rows(entering, leaving, theta );
lp_assert(this->m_x[leaving] == new_val_for_leaving);
lp_assert(this->column_is_feasible(leaving));
if (this->current_x_is_feasible())
this->set_status(lp_status::OPTIMAL);
}