mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-01-20 09:13:20 +00:00
Code Activity

fix a bug in the lar_solver::m_status update during push/pop

Browse source 
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
This commit is contained in:
Lev Nachmanson 2017-07-10 16:34:23 -07:00
parent 581098299b
commit 2fe846d9fc
19 changed files with 212 additions and 190 deletions
Download patch file Download diff file Expand all files Collapse all files

17
src/util/lp/int_solver.cpp
View file

@ -19,7 +19,7 @@ void int_solver::fix_non_base_columns() {
}
if (!change)
return;
if (m_lar_solver->find_feasible_solution() == INFEASIBLE)
if (m_lar_solver->find_feasible_solution() == lp_status::INFEASIBLE)
failed();
init_inf_int_set();
lp_assert(is_feasible() && inf_int_set_is_correct());
@ -109,14 +109,13 @@ int int_solver::find_inf_int_boxed_base_column_with_smallest_range() {
}
bool int_solver::mk_gomory_cut(unsigned row_index, explanation & ex) {
lp_assert(false);
return true;
auto row_it = m_lar_solver->get_iterator_on_row(row_index);
unsigned x_i = m_lar_solver->get_base_column_in_row(row_index);
lp_assert(column_is_int_inf(x_i));
/*
const auto & row = m_lar_solver->A_r().m_rows[row_index];
// The following assertion is wrong. It may be violated in mixed-integer problems.
// SASSERT(!all_coeff_int(r));
theory_var x_i = r.get_base_var();
SASSERT(is_int(x_i));
// The following assertion is wrong. It may be violated in mixed-real-interger problems.
// The check is_gomory_cut_target will discard rows where any variable contains infinitesimals.
@ -286,6 +285,8 @@ bool int_solver::mk_gomory_cut(unsigned row_index, explanation & ex) {
ante.eqs().size(), ante.eqs().c_ptr(), ante, l)));
return true;
*/
delete row_it;
return true;
}