mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 05:48:44 +00:00
Code Activity

solve more ilp smt

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2017-07-06 21:29:09 -07:00
parent 7cd6dc1b5a
commit 2cd81851e7
3 changed files with 47 additions and 29 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -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) { lia_move int_solver::check(lar_term& t, mpq& k, explanation& ex) {
lean_assert(is_feasible()); lean_assert(m_lar_solver->m_mpq_lar_core_solver.r_basis_is_OK());
init_inf_int_set(); lean_assert(is_feasible());
init_check_data();
lean_assert(inf_int_set_is_correct()); lean_assert(inf_int_set_is_correct());
// currently it is a reimplementation of // currently it is a reimplementation of
// final_check_status theory_arith<Ext>::check_int_feasibility() // final_check_status theory_arith<Ext>::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(); 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(); patch_int_infeasible_columns();
fix_non_base_columns(); lean_assert(m_lar_solver->m_mpq_lar_core_solver.r_basis_is_OK());
lean_assert(is_feasible()); 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();); TRACE("arith_int_rows", trace_inf_rows(););
if (find_inf_int_base_column() == -1) 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 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; return lia_move::give_up;
} }

1
src/util/lp/int_solver.h
View file

@ -98,5 +98,6 @@ private:
void move_non_base_vars_to_bounds(); void move_non_base_vars_to_bounds();
void branch_infeasible_int_var(unsigned); void branch_infeasible_int_var(unsigned);
bool mk_gomory_cut(unsigned row_index, explanation & ex); bool mk_gomory_cut(unsigned row_index, explanation & ex);
void init_check_data();
}; };
} }

52
src/util/lp/lp_core_solver_base.hpp
View file

@ -924,27 +924,32 @@ template <typename T, typename X> void lp_core_solver_base<T, X>::transpose_row
m_A.transpose_rows(i, j); m_A.transpose_rows(i, j);
} }
// j is the new basic column, j_basic - the leaving column // j is the new basic column, j_basic - the leaving column
template <typename T, typename X> bool lp_core_solver_base<T, X>::pivot_column_general(unsigned j, unsigned j_basic, indexed_vector<T> & w) { template <typename T, typename X> bool lp_core_solver_base<T, X>::pivot_column_general(unsigned j, unsigned j_basic, indexed_vector<T> & w) {
lean_assert(m_basis_heading[j] < 0); lean_assert(m_basis_heading[j] < 0);
lean_assert(m_basis_heading[j_basic] >= 0); lean_assert(m_basis_heading[j_basic] >= 0);
unsigned row_index = m_basis_heading[j_basic]; 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_settings.m_simplex_strategy == simplex_strategy_enum::lu) { if (m_factorization->need_to_refactor()) {
if (m_factorization->need_to_refactor()) { init_lu();
init_lu(); }
} else { else {
m_factorization->prepare_entering(j, w); // to init vector w m_factorization->prepare_entering(j, w); // to init vector w
m_factorization->replace_column(zero_of_type<T>(), w, row_index); m_factorization->replace_column(zero_of_type<T>(), w, row_index);
} }
if (m_factorization->get_status() != LU_status::OK) { if (m_factorization->get_status() != LU_status::OK) {
change_basis(j_basic, j); init_lu();
init_lu(); return false;
return false; }
} else {
} else { // the tableau case change_basis(j, j_basic);
return pivot_column_tableau(j, row_index); }
} }
return true; else { // the tableau case
if (pivot_column_tableau(j, row_index))
change_basis(j, j_basic);
else return false;
}
return true;
} }
template <typename T, typename X> void lp_core_solver_base<T, X>::pivot_fixed_vars_from_basis() { template <typename T, typename X> void lp_core_solver_base<T, X>::pivot_fixed_vars_from_basis() {
@ -967,9 +972,8 @@ template <typename T, typename X> void lp_core_solver_base<T, X>::pivot_fixed_v
if (j >= m_nbasis.size()) if (j >= m_nbasis.size())
break; break;
j++; j++;
if (!pivot_column_general(jj, ii, w)) if (pivot_column_general(jj, ii, w))
return; // total failure break;
break;
} }
} }
} }