mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 06:03:23 +00:00
Code Activity

fix feasibility tracking in lar_solver

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-05-02 18:44:42 -07:00
parent c74893016a
commit 218e155603
4 changed files with 10 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/theory_lra.cpp
View file

@ -3161,7 +3161,7 @@ public:
return l_false; return l_false;
case lp::lp_status::FEASIBLE: case lp::lp_status::FEASIBLE:
case lp::lp_status::OPTIMAL: case lp::lp_status::OPTIMAL:
SASSERT(lp().all_constraints_hold()); // SASSERT(lp().all_constraints_hold());
return l_true; return l_true;
case lp::lp_status::TIME_EXHAUSTED: case lp::lp_status::TIME_EXHAUSTED:

5
src/util/lp/lar_solver.cpp
View file

@ -880,12 +880,12 @@ void lar_solver::fix_Ax_b_on_rounded_row(unsigned i) {
if (A_r().m_rows.size() <= i) if (A_r().m_rows.size() <= i)
return; return;
unsigned bj = m_mpq_lar_core_solver.m_r_basis[i]; unsigned bj = m_mpq_lar_core_solver.m_r_basis[i];
auto& v = m_mpq_lar_core_solver.m_r_x[bj]; auto v = zero_of_type<impq>();
v = zero_of_type<numeric_pair<mpq>>();
for (const auto & c : A_r().m_rows[i]) { for (const auto & c : A_r().m_rows[i]) {
if (c.var() != bj) if (c.var() != bj)
v -= c.coeff() * m_mpq_lar_core_solver.m_r_x[c.var()]; v -= c.coeff() * m_mpq_lar_core_solver.m_r_x[c.var()];
} }
m_mpq_lar_core_solver.m_r_solver.update_x_with_feasibility_tracking(bj, v);
} }
void lar_solver::collect_rounded_rows_to_fix() { void lar_solver::collect_rounded_rows_to_fix() {
lp_assert(m_cube_rounded_rows.size() == 0); lp_assert(m_cube_rounded_rows.size() == 0);
@ -1622,6 +1622,7 @@ void lar_solver::clean_inf_set_of_r_solver_after_pop() {
m_mpq_lar_core_solver.m_r_solver.update_inf_cost_for_column_tableau(j); m_mpq_lar_core_solver.m_r_solver.update_inf_cost_for_column_tableau(j);
lp_assert(m_mpq_lar_core_solver.m_r_solver.reduced_costs_are_correct_tableau()); lp_assert(m_mpq_lar_core_solver.m_r_solver.reduced_costs_are_correct_tableau());
} }
SASSERT(m_mpq_lar_core_solver.m_r_solver.inf_set_is_correct());
} }
bool lar_solver::model_is_int_feasible() const { bool lar_solver::model_is_int_feasible() const {

6
src/util/lp/lp_core_solver_base.h
View file

@ -394,7 +394,7 @@ public:
bool make_column_feasible(unsigned j, numeric_pair<mpq> & delta) { bool make_column_feasible(unsigned j, numeric_pair<mpq> & delta) {
bool ret = false; bool ret = false;
lp_assert(m_basis_heading[j] < 0); lp_assert(m_basis_heading[j] < 0);
auto & x = m_x[j]; const auto & x = m_x[j];
switch (m_column_types[j]) { switch (m_column_types[j]) {
case column_type::fixed: case column_type::fixed:
lp_assert(m_lower_bounds[j] == m_upper_bounds[j]); lp_assert(m_lower_bounds[j] == m_upper_bounds[j]);
@ -429,7 +429,7 @@ public:
break; break;
} }
if (ret) if (ret)
add_delta_to_x_and_call_tracker(j, delta); add_delta_to_x_and_do_not_track_feasibility(j, delta);
return ret; return ret;
@ -694,7 +694,7 @@ public:
m_x[j] = v; m_x[j] = v;
} }
void add_delta_to_x_and_call_tracker(unsigned j, const X & delta) { void add_delta_to_x_and_do_not_track_feasibility(unsigned j, const X & delta) {
m_x[j] += delta; m_x[j] += delta;
} }

4
src/util/lp/lp_primal_core_solver_tableau_def.h
View file

@ -358,7 +358,7 @@ update_basis_and_x_tableau(int entering, int leaving, X const & tt) {
} }
template <typename T, typename X> void lp_primal_core_solver<T, X>:: template <typename T, typename X> void lp_primal_core_solver<T, X>::
update_x_tableau(unsigned entering, const X& delta) { update_x_tableau(unsigned entering, const X& delta) {
this->add_delta_to_x_and_call_tracker(entering, delta); this->add_delta_to_x_and_do_not_track_feasibility(entering, delta);
if (!this->m_using_infeas_costs) { if (!this->m_using_infeas_costs) {
for (const auto & c : this->m_A.m_columns[entering]) { for (const auto & c : this->m_A.m_columns[entering]) {
unsigned i = c.var(); unsigned i = c.var();
@ -371,7 +371,7 @@ update_x_tableau(unsigned entering, const X& delta) {
for (const auto & c : this->m_A.m_columns[entering]) { for (const auto & c : this->m_A.m_columns[entering]) {
unsigned i = c.var(); unsigned i = c.var();
unsigned j = this->m_basis[i]; unsigned j = this->m_basis[i];
this->add_delta_to_x_and_call_tracker(j, -delta * this->m_A.get_val(c)); this->add_delta_to_x_and_do_not_track_feasibility(j, -delta * this->m_A.get_val(c));
update_inf_cost_for_column_tableau(j); update_inf_cost_for_column_tableau(j);
if (is_zero(this->m_costs[j])) if (is_zero(this->m_costs[j]))
this->remove_column_from_inf_set(j); this->remove_column_from_inf_set(j);