diff --git a/src/shell/lp_frontend.cpp b/src/shell/lp_frontend.cpp new file mode 100644 index 000000000..9fad426a0 --- /dev/null +++ b/src/shell/lp_frontend.cpp @@ -0,0 +1,111 @@ +/*++ +Copyright (c) 2016 Microsoft Corporation + +Author: + + Lev Nachmanson 2016-10-27 + +--*/ + +#include "lp_params.hpp" +#include "util/lp/lp_settings.h" +#include "util/lp/mps_reader.h" +#include "timeout.h" +#include "cancel_eh.h" +#include "scoped_timer.h" +#include "rlimit.h" +#include "gparams.h" +#include + +static lean::lp_solver* g_solver = 0; + +static void display_statistics() { + if (g_solver && g_solver->settings().print_statistics) { + // TBD display relevant information about statistics + } +} + +static void STD_CALL on_ctrl_c(int) { + signal (SIGINT, SIG_DFL); + #pragma omp critical (g_display_stats) + { + display_statistics(); + } + raise(SIGINT); +} + +static void on_timeout() { + #pragma omp critical (g_display_stats) + { + display_statistics(); + exit(0); + } +} + +struct front_end_resource_limit : public lean::lp_resource_limit { + reslimit& m_reslim; + + front_end_resource_limit(reslimit& lim): + m_reslim(lim) + {} + + virtual bool get_cancel_flag() { return !m_reslim.inc(); } +}; + +void run_solver(lp_params & params, char const * mps_file_name) { + + reslimit rlim; + unsigned timeout = gparams::get().get_uint("timeout", 0); + unsigned rlimit = gparams::get().get_uint("rlimit", 0); + front_end_resource_limit lp_limit(rlim); + + scoped_rlimit _rlimit(rlim, rlimit); + cancel_eh eh(rlim); + scoped_timer timer(timeout, &eh); + + std::string fn(mps_file_name); + lean::mps_reader reader(fn); + reader.set_message_stream(&std::cout); // can be redirected + reader.read(); + if (!reader.is_ok()) { + std::cerr << "cannot process " << mps_file_name << std::endl; + return; + } + lean::lp_solver * solver = reader.create_solver(false); // false - to create the primal solver + solver->settings().set_resource_limit(lp_limit); + g_solver = solver; + if (params.min()) { + solver->flip_costs(); + } + solver->settings().set_message_ostream(&std::cout); + solver->settings().report_frequency = params.rep_freq(); + solver->settings().print_statistics = params.print_stats(); + solver->settings().presolve_with_double_solver_for_lar = params.presolve_with_dbl(); + solver->find_maximal_solution(); + + *(solver->settings().get_message_ostream()) << "status is " << lp_status_to_string(solver->get_status()) << std::endl; + if (solver->get_status() == lean::OPTIMAL) { + if (params.min()) { + solver->flip_costs(); + } + solver->print_model(std::cout); + } + +// #pragma omp critical (g_display_stats) + { + display_statistics(); + register_on_timeout_proc(0); + g_solver = 0; + } + delete solver; +} + +unsigned read_mps_file(char const * mps_file_name) { + signal(SIGINT, on_ctrl_c); + register_on_timeout_proc(on_timeout); + lp_params p; + param_descrs r; + p.collect_param_descrs(r); + run_solver(p, mps_file_name); + return 0; +} diff --git a/src/shell/lp_frontend.h b/src/shell/lp_frontend.h index 68e6a736e..b24be811f 100644 --- a/src/shell/lp_frontend.h +++ b/src/shell/lp_frontend.h @@ -1,6 +1,5 @@ /* Copyright (c) 2013 Microsoft Corporation. All rights reserved. - Released under Apache 2.0 license as described in the file LICENSE. Author: Lev Nachmanson */