mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 03:07:07 +00:00
Code Activity

set status to CANCELLED on the total_iterations threshold bailout

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2021-06-07 07:34:16 -07:00
parent b1002638ab
commit 3a5b88e52b
1 changed files with 22 additions and 23 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

45
src/math/lp/lp_primal_core_solver_tableau_def.h
View file

@ -179,34 +179,33 @@ unsigned lp_primal_core_solver<T, X>::solve_with_tableau() {
default:
break; // do nothing
}
if (this->m_settings.get_cancel_flag()
||
this->iters_with_no_cost_growing() > this->m_settings.max_number_of_iterations_with_no_improvements
||
this->total_iterations() > this->m_settings.max_total_number_of_iterations
) {
this->set_status(lp_status::CANCELLED);
break; // from the loop
}
} while (this->get_status() != lp_status::FLOATING_POINT_ERROR
&&
&&
this->get_status() != lp_status::UNBOUNDED
&&
&&
this->get_status() != lp_status::OPTIMAL
&&
&&
this->get_status() != lp_status::INFEASIBLE
&&
this->iters_with_no_cost_growing() <= this->m_settings.max_number_of_iterations_with_no_improvements
&&
this->total_iterations() <= this->m_settings.max_total_number_of_iterations
&&
!(this->current_x_is_feasible() && this->m_look_for_feasible_solution_only)
&&
this->m_settings.get_cancel_flag() == false);
&&
!(this->current_x_is_feasible() && this->m_look_for_feasible_solution_only)
);
if (this->m_settings.get_cancel_flag()) {
this->set_status(lp_status::CANCELLED);
}
lp_assert(
this->get_status() == lp_status::FLOATING_POINT_ERROR
||
this->get_status() == lp_status::CANCELLED
||
this->current_x_is_feasible() == false
||
this->calc_current_x_is_feasible_include_non_basis());
lp_assert(this->get_status() == lp_status::FLOATING_POINT_ERROR
||
this->get_status() == lp_status::CANCELLED
||
this->current_x_is_feasible() == false
||
this->calc_current_x_is_feasible_include_non_basis());
return this->total_iterations();
}