adding timeout, parameters, statistics

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

src/cmd_context/cmd_context.cpp

@@ -1119,7 +1119,6 @@ void cmd_context::insert_aux_pdecl(pdecl * p) {
 }
 
 void cmd_context::reset(bool finalize) {
-    m_check_sat_result = 0;
     m_logic = symbol::null;
     m_check_sat_result = 0;
     m_numeral_as_real = false;

src/opt/opt_cmds.cpp

@@ -25,8 +25,6 @@ Notes:
 
     - Deal with push/pop (later)
 
-    - Revisit weighted constraints if we want to group them using identifiers.
-
 --*/
 #include "opt_cmds.h"
 #include "cmd_context.h"
@@ -34,6 +32,8 @@ Notes:
 #include "opt_context.h"
 #include "cancel_eh.h"
 #include "scoped_ctrl_c.h"
+#include "scoped_timer.h"
+#include "parametric_cmd.h"
 
 
 class opt_context {
@@ -152,30 +152,44 @@ public:
     }
 };
 
-class optimize_cmd : public cmd {
+class optimize_cmd : public parametric_cmd {
     opt_context& m_opt_ctx;
 public:
     optimize_cmd(opt_context& opt_ctx):
-        cmd("optimize"),
+        parametric_cmd("optimize"),
         m_opt_ctx(opt_ctx)
     {}
-    virtual char const * get_descr(cmd_context & ctx) const { return "check sat modulo objective function";}
-    virtual unsigned get_arity() const { return 0; }
-    virtual void prepare(cmd_context & ctx) {}
+
+    virtual void init_pdescrs(cmd_context & ctx, param_descrs & p) {
+        insert_timeout(p);
+        insert_max_memory(p);
+        p.insert("print_statistics", CPK_BOOL, "(default: false) print statistics.");
+    }
+
+    virtual char const * get_main_descr() const { return "check sat modulo objective function";}
+    virtual char const * get_usage() const { return "(<keyword> <value>)*"; }
+    virtual void prepare(cmd_context & ctx) {
+        parametric_cmd::prepare(ctx);
+    }
     virtual void failure_cleanup(cmd_context & ctx) {
         reset(ctx);
     }
 
     virtual void execute(cmd_context & ctx) {
+        params_ref p = ctx.params().merge_default_params(ps());
         opt::context& opt = m_opt_ctx();
+        opt.updt_params(p);
+        unsigned timeout   = p.get_uint("timeout", UINT_MAX);
+
         ptr_vector<expr>::const_iterator it  = ctx.begin_assertions();
         ptr_vector<expr>::const_iterator end = ctx.end_assertions();
         for (; it != end; ++it) {
             opt.add_hard_constraint(*it);
         }
-        cancel_eh<opt::context> eh(opt);
+        cancel_eh<opt::context> eh(opt);        
         {
             scoped_ctrl_c ctrlc(eh);
+            scoped_timer timer(timeout, &eh);
             cmd_context::scoped_watch sw(ctx);
             try {
                 opt.optimize();
@@ -187,6 +201,21 @@ public:
                 ctx.regular_stream() << "(error: " << ex.msg() << "\")" << std::endl;
             }
         }
+        if (p.get_bool("print_statistics", false)) {
+            display_statistics(ctx);
+        }
+    }
+private:
+
+    void display_statistics(cmd_context& ctx) {
+        statistics stats;
+        unsigned long long max_mem = memory::get_max_used_memory();
+        unsigned long long mem = memory::get_allocation_size();
+        stats.update("time", ctx.get_seconds());
+        stats.update("memory", static_cast<double>(mem)/static_cast<double>(1024*1024));
+        stats.update("max memory", static_cast<double>(max_mem)/static_cast<double>(1024*1024));
+        m_opt_ctx().collect_statistics(stats);
+        stats.display_smt2(ctx.regular_stream());        
     }
 };
 

src/opt/opt_context.cpp

@@ -35,16 +35,23 @@ Notes:
 
 namespace opt {
 
+    context::context(ast_manager& m):
+        m(m),
+        m_hard_constraints(m),
+        m_soft_constraints(m),
+        m_objectives(m)
+    {
+        m_params.set_bool("model", true);
+        m_params.set_bool("unsat_core", true);
+    }
+
     void context::optimize() {
 
         expr_ref_vector const& fmls = m_soft_constraints;
 
         if (!m_solver) {
             symbol logic;
-            params_ref p;
-            p.set_bool("model", true);
-            p.set_bool("unsat_core", true);        
-            set_solver(alloc(opt_solver, m, p, logic));
+            set_solver(alloc(opt_solver, m, m_params, logic));
         }
         solver* s = m_solver.get();
 
@@ -140,5 +147,19 @@ namespace opt {
         m_is_max.push_back(is_max);
     }
 
+    void context::collect_statistics(statistics& stats) {
+        if (m_solver) {
+            m_solver->collect_statistics(stats);
+        }
+    }
+
+    void context::updt_params(params_ref& p) {
+        m_params.append(p);
+        if (m_solver) {
+            m_solver->updt_params(m_params);
+        }
+        
+    }
+
 
 }

src/opt/opt_context.h

@@ -40,14 +40,10 @@ namespace opt {
         app_ref_vector   m_objectives;
         svector<bool>    m_is_max;
         ref<solver>      m_solver;
-
+        params_ref       m_params;
+        
     public:
-        context(ast_manager& m):
-            m(m),
-            m_hard_constraints(m),
-            m_soft_constraints(m),
-            m_objectives(m)
-        {}
+        context(ast_manager& m);
 
         void add_soft_constraint(expr* f, rational const& w) {
             m_soft_constraints.push_back(f);
@@ -69,6 +65,10 @@ namespace opt {
         void cancel();
         void reset_cancel();
 
+        void collect_statistics(statistics& stats);
+
+        void updt_params(params_ref& p);
+
     private:
         bool is_maxsat_problem() const;