mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-07 06:33:23 +00:00
Code Activity

Merge pull request #1281 from levnach/dev

Browse source 
add cancellation checks
This commit is contained in:
Christoph M. Wintersteiger 2017-10-05 16:29:46 +02:00 • committed by GitHub
commit d38e15eae7
3 changed files with 31 additions and 19 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -417,6 +417,8 @@ public:
for (unsigned i : m_rows_with_changed_bounds.m_index) { for (unsigned i : m_rows_with_changed_bounds.m_index) {
calculate_implied_bounds_for_row(i, bp); calculate_implied_bounds_for_row(i, bp);
if (settings().get_cancel_flag())
return;
} }
m_rows_with_changed_bounds.clear(); m_rows_with_changed_bounds.clear();
if (!use_tableau()) { if (!use_tableau()) {

45
src/util/lp/lp_primal_core_solver_tableau.h
View file

@ -176,25 +176,34 @@ unsigned lp_primal_core_solver<T, X>::solve_with_tableau() {
default: default:
break; // do nothing break; // do nothing
} }
} while (this->get_status() != FLOATING_POINT_ERROR } while (this->get_status() != FLOATING_POINT_ERROR
&& &&
this->get_status() != UNBOUNDED this->get_status() != UNBOUNDED
&& &&
this->get_status() != OPTIMAL this->get_status() != OPTIMAL
&& &&
this->get_status() != INFEASIBLE this->get_status() != INFEASIBLE
&& &&
this->iters_with_no_cost_growing() <= this->m_settings.max_number_of_iterations_with_no_improvements 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->total_iterations() <= this->m_settings.max_total_number_of_iterations
&& &&
!(this->current_x_is_feasible() && this->m_look_for_feasible_solution_only)); !(this->current_x_is_feasible() && this->m_look_for_feasible_solution_only)
&&
this->m_settings.get_cancel_flag() == false);
if (this->m_settings.get_cancel_flag()) {
this->set_status(CANCELLED);
}
SASSERT(this->get_status() == FLOATING_POINT_ERROR SASSERT(
|| this->get_status() == FLOATING_POINT_ERROR
this->current_x_is_feasible() == false ||
|| this->get_status() == CANCELLED
this->calc_current_x_is_feasible_include_non_basis()); ||
this->current_x_is_feasible() == false
||
this->calc_current_x_is_feasible_include_non_basis());
return this->total_iterations(); return this->total_iterations();
} }

3
src/util/lp/lp_settings.h
View file

@ -61,7 +61,8 @@ enum lp_status {
TIME_EXHAUSTED, TIME_EXHAUSTED,
ITERATIONS_EXHAUSTED, ITERATIONS_EXHAUSTED,
EMPTY, EMPTY,
UNSTABLE UNSTABLE,
CANCELLED
}; };
// when the ratio of the vector lenth to domain size to is greater than the return value we switch to solve_By_for_T_indexed_only // when the ratio of the vector lenth to domain size to is greater than the return value we switch to solve_By_for_T_indexed_only