mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 19:52:29 +00:00
Code Activity

Merge pull request #1020 from levnach/master

Browse source 
allow more  failures when solving with doubles
This commit is contained in:
Nikolaj Bjorner 2017-05-11 18:23:32 -07:00 • committed by GitHub
commit 8c1da3f2b0
4 changed files with 12 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -253,7 +253,6 @@ public :
if (str)
strict = true;
}
bound /= l_coeff;
if (is_pos(l_coeff)) {
limit_j(m_column_of_l, bound, true, false, strict);

2
src/util/lp/lar_core_solver.h
View file

@ -599,7 +599,7 @@ public:
}
if (no_r_lu()) { // it is the case where m_d_solver gives a degenerated basis, we need to roll back
std::cout << "no_r_lu" << std::endl;
// std::cout << "no_r_lu" << std::endl;
catch_up_in_lu_in_reverse(changes_of_basis, m_r_solver);
m_r_solver.find_feasible_solution();
m_d_basis = m_r_basis;

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

@ -533,13 +533,19 @@ update_basis_and_x(int entering, int leaving, X const & tt) {
init_factorization(m_factorization, m_A, m_basis, m_settings);
if (!find_x_by_solving()) {
restore_x(entering, tt);
lean_assert(!A_mult_x_is_off());
if(A_mult_x_is_off()) {
m_status = FLOATING_POINT_ERROR;
m_iters_with_no_cost_growing++;
return false;
}
init_factorization(m_factorization, m_A, m_basis, m_settings);
m_iters_with_no_cost_growing++;
if (m_factorization->get_status() != LU_status::OK) {
std::stringstream s;
s << "failing refactor on off_result for entering = " << entering << ", leaving = " << leaving << " total_iterations = " << total_iterations();
throw_exception(s.str());
// s << "failing refactor on off_result for entering = " << entering << ", leaving = " << leaving << " total_iterations = " << total_iterations();
m_status = FLOATING_POINT_ERROR;
return false;
}
return false;
}

4
src/util/lp/lu.hpp
View file

@ -605,13 +605,13 @@ void lu<T, X>::process_column(int j) {
unsigned pi, pj;
bool success = m_U.get_pivot_for_column(pi, pj, m_settings.c_partial_pivoting, j);
if (!success) {
LP_OUT(m_settings, "get_pivot returned false: cannot find the pivot for column " << j << std::endl);
// LP_OUT(m_settings, "get_pivot returned false: cannot find the pivot for column " << j << std::endl);
m_failure = true;
return;
}
if (static_cast<int>(pi) == -1) {
LP_OUT(m_settings, "cannot find the pivot for column " << j << std::endl);
// LP_OUT(m_settings, "cannot find the pivot for column " << j << std::endl);
m_failure = true;
return;
}