From 2cd81851e7d1a206abf0121b90dfb1774e4f17d9 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Thu, 6 Jul 2017 21:29:09 -0700 Subject: [PATCH] solve more ilp smt Signed-off-by: Lev Nachmanson --- src/util/lp/int_solver.cpp | 23 ++++++++++--- src/util/lp/int_solver.h | 1 + src/util/lp/lp_core_solver_base.hpp | 52 ++++++++++++++++------------- 3 files changed, 47 insertions(+), 29 deletions(-) diff --git a/src/util/lp/int_solver.cpp b/src/util/lp/int_solver.cpp index ded1d94d8..30bfcae9b 100644 --- a/src/util/lp/int_solver.cpp +++ b/src/util/lp/int_solver.cpp @@ -281,9 +281,18 @@ bool int_solver::mk_gomory_cut(unsigned row_index, explanation & ex) { */ } + +void int_solver::init_check_data() { + init_inf_int_set(); + unsigned n = m_lar_solver->A_r().column_count(); + m_old_values_set.resize(n); + m_old_values_data.resize(n); +} + lia_move int_solver::check(lar_term& t, mpq& k, explanation& ex) { - lean_assert(is_feasible()); - init_inf_int_set(); + lean_assert(m_lar_solver->m_mpq_lar_core_solver.r_basis_is_OK()); + lean_assert(is_feasible()); + init_check_data(); lean_assert(inf_int_set_is_correct()); // currently it is a reimplementation of // final_check_status theory_arith::check_int_feasibility() @@ -298,9 +307,12 @@ lia_move int_solver::check(lar_term& t, mpq& k, explanation& ex) { */ m_lar_solver->pivot_fixed_vars_from_basis(); + lean_assert(m_lar_solver->m_mpq_lar_core_solver.r_basis_is_OK()); patch_int_infeasible_columns(); - fix_non_base_columns(); - lean_assert(is_feasible()); + lean_assert(m_lar_solver->m_mpq_lar_core_solver.r_basis_is_OK()); + fix_non_base_columns(); + lean_assert(m_lar_solver->m_mpq_lar_core_solver.r_basis_is_OK()); + lean_assert(is_feasible()); TRACE("arith_int_rows", trace_inf_rows();); if (find_inf_int_base_column() == -1) @@ -339,7 +351,8 @@ lia_move int_solver::check(lar_term& t, mpq& k, explanation& ex) { return lia_move::branch; } } - // return true; + lean_assert(m_lar_solver->m_mpq_lar_core_solver.r_basis_is_OK()); + // return true; return lia_move::give_up; } diff --git a/src/util/lp/int_solver.h b/src/util/lp/int_solver.h index edfba5e5b..8259ae128 100644 --- a/src/util/lp/int_solver.h +++ b/src/util/lp/int_solver.h @@ -98,5 +98,6 @@ private: void move_non_base_vars_to_bounds(); void branch_infeasible_int_var(unsigned); bool mk_gomory_cut(unsigned row_index, explanation & ex); + void init_check_data(); }; } diff --git a/src/util/lp/lp_core_solver_base.hpp b/src/util/lp/lp_core_solver_base.hpp index f3cee7fa8..08ba5d251 100644 --- a/src/util/lp/lp_core_solver_base.hpp +++ b/src/util/lp/lp_core_solver_base.hpp @@ -924,27 +924,32 @@ template void lp_core_solver_base::transpose_row m_A.transpose_rows(i, j); } // j is the new basic column, j_basic - the leaving column -template bool lp_core_solver_base::pivot_column_general(unsigned j, unsigned j_basic, indexed_vector & w) { - lean_assert(m_basis_heading[j] < 0); - lean_assert(m_basis_heading[j_basic] >= 0); - unsigned row_index = m_basis_heading[j_basic]; - change_basis(j, j_basic); - if (m_settings.m_simplex_strategy == simplex_strategy_enum::lu) { - if (m_factorization->need_to_refactor()) { - init_lu(); - } else { - m_factorization->prepare_entering(j, w); // to init vector w - m_factorization->replace_column(zero_of_type(), w, row_index); - } - if (m_factorization->get_status() != LU_status::OK) { - change_basis(j_basic, j); - init_lu(); - return false; - } - } else { // the tableau case - return pivot_column_tableau(j, row_index); - } - return true; +template bool lp_core_solver_base::pivot_column_general(unsigned j, unsigned j_basic, indexed_vector & w) { + lean_assert(m_basis_heading[j] < 0); + lean_assert(m_basis_heading[j_basic] >= 0); + unsigned row_index = m_basis_heading[j_basic]; + if (m_settings.m_simplex_strategy == simplex_strategy_enum::lu) { + if (m_factorization->need_to_refactor()) { + init_lu(); + } + else { + m_factorization->prepare_entering(j, w); // to init vector w + m_factorization->replace_column(zero_of_type(), w, row_index); + } + if (m_factorization->get_status() != LU_status::OK) { + init_lu(); + return false; + } + else { + change_basis(j, j_basic); + } + } + else { // the tableau case + if (pivot_column_tableau(j, row_index)) + change_basis(j, j_basic); + else return false; + } + return true; } template void lp_core_solver_base::pivot_fixed_vars_from_basis() { @@ -967,9 +972,8 @@ template void lp_core_solver_base::pivot_fixed_v if (j >= m_nbasis.size()) break; j++; - if (!pivot_column_general(jj, ii, w)) - return; // total failure - break; + if (pivot_column_general(jj, ii, w)) + break; } } }