From 2828126b725362ee08daf0cf8a774d0b09cc3dcb Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 3 Oct 2017 10:20:49 -0700 Subject: [PATCH 1/2] add cancellation checks Signed-off-by: Lev Nachmanson --- src/util/lp/lar_solver.h | 2 + src/util/lp/lp_primal_core_solver_tableau.h | 45 ++++++++++++--------- src/util/lp/lp_settings.h | 3 +- 3 files changed, 31 insertions(+), 19 deletions(-) diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h index 1ed30bd70..6d2cbea7d 100644 --- a/src/util/lp/lar_solver.h +++ b/src/util/lp/lar_solver.h @@ -417,6 +417,8 @@ public: for (unsigned i : m_rows_with_changed_bounds.m_index) { calculate_implied_bounds_for_row(i, bp); + if (settings().get_cancel_flag()) + return; } m_rows_with_changed_bounds.clear(); if (!use_tableau()) { diff --git a/src/util/lp/lp_primal_core_solver_tableau.h b/src/util/lp/lp_primal_core_solver_tableau.h index 5c7d4d2c2..d2b8c1a26 100644 --- a/src/util/lp/lp_primal_core_solver_tableau.h +++ b/src/util/lp/lp_primal_core_solver_tableau.h @@ -176,25 +176,34 @@ unsigned lp_primal_core_solver::solve_with_tableau() { default: break; // do nothing } - } while (this->get_status() != FLOATING_POINT_ERROR - && - this->get_status() != UNBOUNDED - && - this->get_status() != OPTIMAL - && - this->get_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)); + } while (this->get_status() != FLOATING_POINT_ERROR + && + this->get_status() != UNBOUNDED + && + this->get_status() != OPTIMAL + && + this->get_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) + && + m_settings.get_cancel_flag() == false); + + if (m_settings.get_cancel_flag()) { + this->set_status(CANCELLED); + } - SASSERT(this->get_status() == FLOATING_POINT_ERROR - || - this->current_x_is_feasible() == false - || - this->calc_current_x_is_feasible_include_non_basis()); + SASSERT( + this->get_status() == FLOATING_POINT_ERROR + || + this->get_status() == CANCELLED + || + this->current_x_is_feasible() == false + || + this->calc_current_x_is_feasible_include_non_basis()); return this->total_iterations(); } diff --git a/src/util/lp/lp_settings.h b/src/util/lp/lp_settings.h index 70a9f1504..a7e6e2665 100644 --- a/src/util/lp/lp_settings.h +++ b/src/util/lp/lp_settings.h @@ -61,7 +61,8 @@ enum lp_status { TIME_EXHAUSTED, ITERATIONS_EXHAUSTED, 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 From fd3d785a5b41715a5a1c61ea03038c550483030e Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 4 Oct 2017 14:49:45 -0700 Subject: [PATCH 2/2] add this-> Signed-off-by: Lev Nachmanson --- src/util/lp/lp_primal_core_solver_tableau.h | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/util/lp/lp_primal_core_solver_tableau.h b/src/util/lp/lp_primal_core_solver_tableau.h index d2b8c1a26..0c56f0ab9 100644 --- a/src/util/lp/lp_primal_core_solver_tableau.h +++ b/src/util/lp/lp_primal_core_solver_tableau.h @@ -190,10 +190,10 @@ unsigned lp_primal_core_solver::solve_with_tableau() { && !(this->current_x_is_feasible() && this->m_look_for_feasible_solution_only) && - m_settings.get_cancel_flag() == false); + this->m_settings.get_cancel_flag() == false); - if (m_settings.get_cancel_flag()) { - this->set_status(CANCELLED); + if (this->m_settings.get_cancel_flag()) { + this->set_status(CANCELLED); } SASSERT(