From 7758b519bc093e37f70b769f90e36e7d76163377 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Sun, 5 Dec 2021 16:38:37 -1000 Subject: [PATCH] Handle correctly cancelled run (#5695) * remove the bound on total iterations in simplex Signed-off-by: Lev Nachmanson * remove unncesseray checks in get_freedom_interval_for_column() Signed-off-by: Lev Nachmanson * fix the build of test-z3 Signed-off-by: Lev Nachmanson * Revert "remove unncesseray checks in get_freedom_interval_for_column()" This reverts commit 6770ed85e3a09c2f0373464d77305438522a03cb. * optimize get_freedom_interval_for_column() for feasible case Signed-off-by: Lev Nachmanson * add function lar_solver::status_feasible Signed-off-by: Lev Nachmanson * rename status_is_feasible() to is_feasible() Signed-off-by: Lev Nachmanson * fix the linux build Signed-off-by: Lev Nachmanson --- src/math/lp/int_solver.cpp | 6 +- src/math/lp/lar_core_solver_def.h | 12 +++- src/math/lp/lar_solver.cpp | 12 ++++ src/math/lp/lar_solver.h | 2 + src/math/lp/lp_dual_core_solver_def.h | 7 +-- src/math/lp/lp_dual_simplex_def.h | 3 - src/math/lp/lp_primal_core_solver_def.h | 8 +-- .../lp/lp_primal_core_solver_tableau_def.h | 4 +- src/math/lp/lp_settings.h | 2 - src/math/lp/lp_settings_def.h | 2 - src/math/lp/lp_solver.h | 8 +-- src/smt/theory_lra.cpp | 2 +- src/test/lp/lp.cpp | 59 +++++++------------ 13 files changed, 55 insertions(+), 72 deletions(-) diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp index 39ef072b0..3aaf8f29e 100644 --- a/src/math/lp/int_solver.cpp +++ b/src/math/lp/int_solver.cpp @@ -324,6 +324,7 @@ static void set_upper(impq & u, bool & inf_u, impq const & v) { } } +// this function assumes that all basic columns dependend on j are feasible bool int_solver::get_freedom_interval_for_column(unsigned j, bool & inf_l, impq & l, bool & inf_u, impq & u, mpq & m) { if (lrac.m_r_heading[j] >= 0) // the basic var return false; @@ -360,13 +361,12 @@ bool int_solver::get_freedom_interval_for_column(unsigned j, bool & inf_l, impq const mpq & a = c.coeff(); unsigned i = lrac.m_r_basis[row_index]; impq const & xi = get_value(i); - + lp_assert(lrac.m_r_solver.column_is_feasible(i)); if (column_is_int(i) && !a.is_int()) m = lcm(m, denominator(a)); + if (!inf_l && !inf_u) { - if (l > u) - break; if (l == u) continue; } diff --git a/src/math/lp/lar_core_solver_def.h b/src/math/lp/lar_core_solver_def.h index 06f414d11..f20aa7e6b 100644 --- a/src/math/lp/lar_core_solver_def.h +++ b/src/math/lp/lar_core_solver_def.h @@ -179,11 +179,17 @@ void lar_core_solver::solve() { } lp_assert(!settings().use_tableau() || r_basis_is_OK()); } - if (m_r_solver.get_status() == lp_status::INFEASIBLE) { + switch (m_r_solver.get_status()) + { + case lp_status::INFEASIBLE: fill_not_improvable_zero_sum(); - } - else if (m_r_solver.get_status() != lp_status::UNBOUNDED) { + break; + case lp_status::CANCELLED: + case lp_status::UNBOUNDED: // do nothing in these cases + break; + default: // adjust the status to optimal m_r_solver.set_status(lp_status::OPTIMAL); + break; } lp_assert(r_basis_is_OK()); lp_assert(m_r_solver.non_basic_columns_are_set_correctly()); diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index 561a94e99..f78dab119 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -798,6 +798,18 @@ namespace lp { } + // this function just looks at the status + bool lar_solver::is_feasible() const { + switch (this->get_status()) { + case lp_status::OPTIMAL: + case lp_status::FEASIBLE: + case lp_status::UNBOUNDED: + return true; + default: + return false; + } + } + numeric_pair lar_solver::get_basic_var_value_from_row(unsigned i) { numeric_pair r = zero_of_type>(); diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index 9dd180395..1cd776cc2 100644 --- a/src/math/lp/lar_solver.h +++ b/src/math/lp/lar_solver.h @@ -296,6 +296,8 @@ class lar_solver : public column_namer { mutable mpq m_delta; public: + // this function just looks at the status + bool is_feasible() const; const map, default_eq>& fixed_var_table_int() const { return m_fixed_var_table_int; } diff --git a/src/math/lp/lp_dual_core_solver_def.h b/src/math/lp/lp_dual_core_solver_def.h index 1e6553458..4a847fe85 100644 --- a/src/math/lp/lp_dual_core_solver_def.h +++ b/src/math/lp/lp_dual_core_solver_def.h @@ -100,10 +100,7 @@ template bool lp_dual_core_solver::done() { if (this->get_status() == lp_status::OPTIMAL) { return true; } - if (this->total_iterations() > this->m_settings.max_total_number_of_iterations) { // debug !!!! - this->set_status(lp_status::ITERATIONS_EXHAUSTED); - return true; - } + return false; // todo, need to be more cases } @@ -747,6 +744,6 @@ template void lp_dual_core_solver::solve() { // s one_iteration(); } while (this->get_status() != lp_status::FLOATING_POINT_ERROR && this->get_status() != lp_status::DUAL_UNBOUNDED && this->get_status() != lp_status::OPTIMAL && 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); + ); } } diff --git a/src/math/lp/lp_dual_simplex_def.h b/src/math/lp/lp_dual_simplex_def.h index 1b12106ea..34079cd94 100644 --- a/src/math/lp/lp_dual_simplex_def.h +++ b/src/math/lp/lp_dual_simplex_def.h @@ -31,9 +31,6 @@ template void lp_dual_simplex::decide_on_status_a break; case lp_status::DUAL_UNBOUNDED: lp_unreachable(); - case lp_status::ITERATIONS_EXHAUSTED: - this->m_status = lp_status::ITERATIONS_EXHAUSTED; - break; case lp_status::TIME_EXHAUSTED: this->m_status = lp_status::TIME_EXHAUSTED; break; diff --git a/src/math/lp/lp_primal_core_solver_def.h b/src/math/lp/lp_primal_core_solver_def.h index aeaf485a7..75eff208a 100644 --- a/src/math/lp/lp_primal_core_solver_def.h +++ b/src/math/lp/lp_primal_core_solver_def.h @@ -956,8 +956,6 @@ template unsigned lp_primal_core_solver::solve() && 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)); lp_assert(this->get_status() == lp_status::FLOATING_POINT_ERROR @@ -1097,10 +1095,8 @@ template bool lp_primal_core_solver::done() { return true; } if (this->m_iters_with_no_cost_growing >= this->m_settings.max_number_of_iterations_with_no_improvements) { - this->get_status() = lp_status::ITERATIONS_EXHAUSTED; return true; - } - if (this->total_iterations() >= this->m_settings.max_total_number_of_iterations) { - this->get_status() = lp_status::ITERATIONS_EXHAUSTED; return true; + this->set_status(lp_status::CANCELLED); + return true; } return false; } diff --git a/src/math/lp/lp_primal_core_solver_tableau_def.h b/src/math/lp/lp_primal_core_solver_tableau_def.h index 115e1a344..03f07115b 100644 --- a/src/math/lp/lp_primal_core_solver_tableau_def.h +++ b/src/math/lp/lp_primal_core_solver_tableau_def.h @@ -182,9 +182,7 @@ unsigned lp_primal_core_solver::solve_with_tableau() { 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 } diff --git a/src/math/lp/lp_settings.h b/src/math/lp/lp_settings.h index 7a0fef5c7..2be55dcb1 100644 --- a/src/math/lp/lp_settings.h +++ b/src/math/lp/lp_settings.h @@ -71,7 +71,6 @@ enum class lp_status { FEASIBLE, FLOATING_POINT_ERROR, TIME_EXHAUSTED, - ITERATIONS_EXHAUSTED, EMPTY, UNSTABLE, CANCELLED @@ -210,7 +209,6 @@ public: double harris_feasibility_tolerance { 1e-7 }; // page 179 of Istvan Maros double ignore_epsilon_of_harris { 10e-5 }; unsigned max_number_of_iterations_with_no_improvements { 2000000 }; - unsigned max_total_number_of_iterations { 20000000 }; double time_limit; // the maximum time limit of the total run time in seconds // dual section double dual_feasibility_tolerance { 1e-7 }; // page 71 of the PhD thesis of Achim Koberstein diff --git a/src/math/lp/lp_settings_def.h b/src/math/lp/lp_settings_def.h index 247cb98d3..4c783049c 100644 --- a/src/math/lp/lp_settings_def.h +++ b/src/math/lp/lp_settings_def.h @@ -45,7 +45,6 @@ const char* lp_status_to_string(lp_status status) { case lp_status::FEASIBLE: return "FEASIBLE"; case lp_status::FLOATING_POINT_ERROR: return "FLOATING_POINT_ERROR"; case lp_status::TIME_EXHAUSTED: return "TIME_EXHAUSTED"; - case lp_status::ITERATIONS_EXHAUSTED: return "ITERATIONS_EXHAUSTED"; case lp_status::EMPTY: return "EMPTY"; case lp_status::UNSTABLE: return "UNSTABLE"; default: @@ -62,7 +61,6 @@ lp_status lp_status_from_string(std::string status) { if (status == "FEASIBLE") return lp_status::FEASIBLE; if (status == "FLOATING_POINT_ERROR") return lp_status::FLOATING_POINT_ERROR; if (status == "TIME_EXHAUSTED") return lp_status::TIME_EXHAUSTED; - if (status == "ITERATIONS_EXHAUSTED") return lp_status::ITERATIONS_EXHAUSTED; if (status == "EMPTY") return lp_status::EMPTY; lp_unreachable(); return lp_status::UNKNOWN; // it is unreachable diff --git a/src/math/lp/lp_solver.h b/src/math/lp/lp_solver.h index 9b0b8fb0a..68beca06f 100644 --- a/src/math/lp/lp_solver.h +++ b/src/math/lp/lp_solver.h @@ -158,13 +158,7 @@ public: m_settings.time_limit = time_limit_in_seconds; } - void set_max_iterations_per_stage(unsigned max_iterations) { - m_settings.max_total_number_of_iterations = max_iterations; - } - - unsigned get_max_iterations_per_stage() const { - return m_settings.max_total_number_of_iterations; - } + protected: bool problem_is_empty(); diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index e89508b1c..5c2f5bf1b 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -3095,7 +3095,7 @@ public: default: TRACE("arith", tout << "status treated as inconclusive: " << status << "\n";); // TENTATIVE_UNBOUNDED, UNBOUNDED, TENTATIVE_DUAL_UNBOUNDED, DUAL_UNBOUNDED, - // FLOATING_POINT_ERROR, TIME_EXAUSTED, ITERATIONS_EXHAUSTED, EMPTY, UNSTABLE + // FLOATING_POINT_ERROR, TIME_EXAUSTED, EMPTY, UNSTABLE return l_undef; } } diff --git a/src/test/lp/lp.cpp b/src/test/lp/lp.cpp index 9d24d2787..d7329309c 100644 --- a/src/test/lp/lp.cpp +++ b/src/test/lp/lp.cpp @@ -1396,10 +1396,7 @@ void update_settings(argument_parser & args_parser, lp_settings& settings) { } template -void setup_solver(unsigned max_iterations, unsigned time_limit, bool look_for_min, argument_parser & args_parser, lp_solver * solver) { - if (max_iterations > 0) - solver->set_max_iterations_per_stage(max_iterations); - +void setup_solver(unsigned time_limit, bool look_for_min, argument_parser & args_parser, lp_solver * solver) { if (time_limit > 0) solver->set_time_limit(time_limit); @@ -1429,7 +1426,7 @@ void compare_solutions(mps_reader & reader, lp_solver reader(file_name); reader.read(); if (!reader.is_ok()) { @@ -1438,7 +1435,7 @@ void solve_mps_double(std::string file_name, bool look_for_min, unsigned max_ite } lp_solver * solver = reader.create_solver(dual); - setup_solver(max_iterations, time_limit, look_for_min, args_parser, solver); + setup_solver(time_limit, look_for_min, args_parser, solver); stopwatch sw; sw.start(); if (dual) { @@ -1461,7 +1458,7 @@ void solve_mps_double(std::string file_name, bool look_for_min, unsigned max_ite std::cout << "processed in " << span / 1000.0 << " seconds, running for " << solver->m_total_iterations << " iterations" << " one iter for " << (double)span/solver->m_total_iterations << " ms" << std::endl; if (compare_with_primal) { auto * primal_solver = reader.create_solver(false); - setup_solver(max_iterations, time_limit, look_for_min, args_parser, primal_solver); + setup_solver(time_limit, look_for_min, args_parser, primal_solver); primal_solver->find_maximal_solution(); if (solver->get_status() != primal_solver->get_status()) { std::cout << "statuses are different: dual " << lp_status_to_string(solver->get_status()) << " primal = " << lp_status_to_string(primal_solver->get_status()) << std::endl; @@ -1489,12 +1486,12 @@ void solve_mps_double(std::string file_name, bool look_for_min, unsigned max_ite delete solver; } -void solve_mps_rational(std::string file_name, bool look_for_min, unsigned max_iterations, unsigned time_limit, bool dual, argument_parser & args_parser) { +void solve_mps_rational(std::string file_name, bool look_for_min, unsigned time_limit, bool dual, argument_parser & args_parser) { mps_reader reader(file_name); reader.read(); if (reader.is_ok()) { auto * solver = reader.create_solver(dual); - setup_solver(max_iterations, time_limit, look_for_min, args_parser, solver); + setup_solver(time_limit, look_for_min, args_parser, solver); stopwatch sw; sw.start(); solver->find_maximal_solution(); @@ -1516,27 +1513,27 @@ void solve_mps_rational(std::string file_name, bool look_for_min, unsigned max_i std::cout << "cannot process " << file_name << std::endl; } } -void get_time_limit_and_max_iters_from_parser(argument_parser & args_parser, unsigned & time_limit, unsigned & max_iters); // forward definition +void get_time_limit_and_max_iters_from_parser(argument_parser & args_parser, unsigned & time_limit); // forward definition -void solve_mps(std::string file_name, bool look_for_min, unsigned max_iterations, unsigned time_limit, bool solve_for_rational, bool dual, bool compare_with_primal, argument_parser & args_parser) { +void solve_mps(std::string file_name, bool look_for_min, unsigned time_limit, bool solve_for_rational, bool dual, bool compare_with_primal, argument_parser & args_parser) { if (!solve_for_rational) { std::cout << "solving " << file_name << std::endl; - solve_mps_double(file_name, look_for_min, max_iterations, time_limit, dual, compare_with_primal, args_parser); + solve_mps_double(file_name, look_for_min, time_limit, dual, compare_with_primal, args_parser); } else { std::cout << "solving " << file_name << " in rationals " << std::endl; - solve_mps_rational(file_name, look_for_min, max_iterations, time_limit, dual, args_parser); + solve_mps_rational(file_name, look_for_min, time_limit, dual, args_parser); } } void solve_mps(std::string file_name, argument_parser & args_parser) { bool look_for_min = args_parser.option_is_used("--min"); - unsigned max_iterations, time_limit; + unsigned time_limit; bool solve_for_rational = args_parser.option_is_used("--mpq"); bool dual = args_parser.option_is_used("--dual"); bool compare_with_primal = args_parser.option_is_used("--compare_with_primal"); - get_time_limit_and_max_iters_from_parser(args_parser, time_limit, max_iterations); - solve_mps(file_name, look_for_min, max_iterations, time_limit, solve_for_rational, dual, compare_with_primal, args_parser); + get_time_limit_and_max_iters_from_parser(args_parser, time_limit); + solve_mps(file_name, look_for_min, time_limit, solve_for_rational, dual, compare_with_primal, args_parser); } void solve_mps_in_rational(std::string file_name, bool dual, argument_parser & /*args_parser*/) { @@ -1903,7 +1900,7 @@ void process_test_file(std::string test_dir, std::string test_file_name, argumen void solve_some_mps(argument_parser & args_parser) { unsigned max_iters, time_limit; - get_time_limit_and_max_iters_from_parser(args_parser, time_limit, max_iters); + get_time_limit_and_max_iters_from_parser(args_parser, time_limit); unsigned successes = 0; unsigned failures = 0; unsigned inconclusives = 0; @@ -1935,7 +1932,7 @@ void solve_some_mps(argument_parser & args_parser) { return; } if (!solve_for_rational) { - solve_mps(file_names[6], false, 0, time_limit, false, dual, compare_with_primal, args_parser); + solve_mps(file_names[6], false, time_limit, false, dual, compare_with_primal, args_parser); solve_mps_with_known_solution(file_names[3], nullptr, lp_status::INFEASIBLE, dual); // chvatal: 135(d) std::unordered_map sol; sol["X1"] = 0; @@ -1960,11 +1957,11 @@ void solve_some_mps(argument_parser & args_parser) { solve_mps_with_known_solution(file_names[4], &sol, lp_status::OPTIMAL, dual); // chvatal: 135(e) solve_mps_with_known_solution(file_names[2], nullptr, lp_status::UNBOUNDED, dual); // chvatal: 135(c) solve_mps_with_known_solution(file_names[1], nullptr, lp_status::UNBOUNDED, dual); // chvatal: 135(b) - solve_mps(file_names[8], false, 0, time_limit, false, dual, compare_with_primal, args_parser); + solve_mps(file_names[8], false, time_limit, false, dual, compare_with_primal, args_parser); // return; for (auto& s : file_names) { try { - solve_mps(s, minimums.find(s) != minimums.end(), max_iters, time_limit, false, dual, compare_with_primal, args_parser); + solve_mps(s, minimums.find(s) != minimums.end(), time_limit, false, dual, compare_with_primal, args_parser); } catch(const char *s){ std::cout<< "exception: "<< s << std::endl; @@ -2315,14 +2312,7 @@ void finalize(unsigned ret) { // return ret; } -void get_time_limit_and_max_iters_from_parser(argument_parser & args_parser, unsigned & time_limit, unsigned & max_iters) { - std::string s = args_parser.get_option_value("--max_iters"); - if (!s.empty()) { - max_iters = atoi(s.c_str()); - } else { - max_iters = 0; - } - +void get_time_limit_and_max_iters_from_parser(argument_parser & args_parser, unsigned & time_limit) { std::string time_limit_string = args_parser.get_option_value("--time_limit"); if (!time_limit_string.empty()) { time_limit = atoi(time_limit_string.c_str()); @@ -2504,7 +2494,7 @@ void process_test_file(std::string test_dir, std::string test_file_name, argumen if (args_parser.option_is_used("--lar")) test_lar_on_file(input_file_name, args_parser); else - solve_mps(input_file_name, minimize, max_iters, time_limit, use_mpq, dual, false, args_parser); + solve_mps(input_file_name, minimize, time_limit, use_mpq, dual, false, args_parser); } catch(...) { std::cout << "catching the failure" << std::endl; @@ -2624,7 +2614,7 @@ void test_files_from_directory(std::string test_file_dir, argument_parser & args vector> files = get_file_list_of_dir(test_file_dir); std::sort(files.begin(), files.end(), sort_pred()); unsigned max_iters, time_limit; - get_time_limit_and_max_iters_from_parser(args_parser, time_limit, max_iters); + get_time_limit_and_max_iters_from_parser(args_parser, time_limit); unsigned successes = 0, failures = 0, inconclusives = 0; for (auto & t : files) { process_test_file(test_file_dir, t.first, args_parser, out_dir, max_iters, time_limit, successes, failures, inconclusives); @@ -2651,10 +2641,6 @@ void run_lar_solver(argument_parser & args_parser, lar_solver * solver, mps_read solver->settings().presolve_with_double_solver_for_lar = true; } - std::string iter = args_parser.get_option_value("--max_iters"); - if (!iter.empty()) { - solver->settings().max_total_number_of_iterations = atoi(iter.c_str()); - } if (args_parser.option_is_used("--compare_with_primal")){ if (reader == nullptr) { std::cout << "cannot compare with primal, the reader is null " << std::endl; @@ -4074,14 +4060,13 @@ void test_lp_local(int argn, char**argv) { ret = 0; return finalize(ret); } - unsigned max_iters; unsigned time_limit; - get_time_limit_and_max_iters_from_parser(args_parser, time_limit, max_iters); + get_time_limit_and_max_iters_from_parser(args_parser, time_limit); bool dual = args_parser.option_is_used("--dual"); bool solve_for_rational = args_parser.option_is_used("--mpq"); std::string file_name = args_parser.get_option_value("--file"); if (!file_name.empty()) { - solve_mps(file_name, args_parser.option_is_used("--min"), max_iters, time_limit, solve_for_rational, dual, args_parser.option_is_used("--compare_with_primal"), args_parser); + solve_mps(file_name, args_parser.option_is_used("--min"), time_limit, solve_for_rational, dual, args_parser.option_is_used("--compare_with_primal"), args_parser); ret = 0; return finalize(ret); }