missing file

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

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 <signal.h>
+
+static lean::lp_solver<double, double>* 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<reslimit> eh(rlim);
+    scoped_timer timer(timeout, &eh);
+
+    std::string fn(mps_file_name);
+    lean::mps_reader<double, double> 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<double, double> * 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;
+}

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
 */