mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-22 13:53:39 +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 281882e3b1
commit a52c33a3e1
3 changed files with 49 additions and 29 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -281,9 +281,18 @@ bool int_solver::mk_gomory_cut(unsigned row_index, explanation & ex) {
*/ */
} }
lia_move int_solver::check(lar_term& t, mpq& k, explanation& ex) {
lean_assert(is_feasible()); void int_solver::init_check_data() {
init_inf_int_set(); 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(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()); 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,8 +307,11 @@ 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();
lean_assert(m_lar_solver->m_mpq_lar_core_solver.r_basis_is_OK());
fix_non_base_columns(); fix_non_base_columns();
lean_assert(m_lar_solver->m_mpq_lar_core_solver.r_basis_is_OK());
lean_assert(is_feasible()); lean_assert(is_feasible());
TRACE("arith_int_rows", trace_inf_rows();); TRACE("arith_int_rows", trace_inf_rows(););
@ -339,6 +351,7 @@ lia_move int_solver::check(lar_term& t, mpq& k, explanation& ex) {
return lia_move::branch; return lia_move::branch;
} }
} }
lean_assert(m_lar_solver->m_mpq_lar_core_solver.r_basis_is_OK());
// return true; // 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();
}; };
} }

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

@ -943,22 +943,28 @@ template <typename T, typename X> bool lp_core_solver_base<T, X>::pivot_column_g
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 { // the tableau case else {
return pivot_column_tableau(j, row_index); 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 <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() {
@ -981,10 +987,10 @@ 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;
} }
}
} }
template <typename T, typename X> bool template <typename T, typename X> bool