Merge branch 'opt' of https://git01.codeplex.com/z3 into opt

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

@@ -15,18 +15,11 @@ Author:
 Notes:
 
     TODO:
-    - integrate with parameters. 
-      Parameter infrastructure lets us control setttings, such as 
-      timeouts and control which backend optimization approach to 
-      use during experiments.
 
-    - Display statistics properly on exit when configured to do so.
-      Also add appropriate statistics tracking to opt::context
+    - Add appropriate statistics tracking to opt::context
 
     - 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 +27,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 +147,49 @@ 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 cmd_arg_kind next_arg_kind(cmd_context & ctx) const {
+        return parametric_cmd::next_arg_kind(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

@@ -26,7 +26,6 @@ Notes:
 #include "opt_context.h"
 #include "fu_malik.h"
 #include "weighted_maxsat.h"
-#include "optimize_objectives.h"
 #include "ast_pp.h"
 #include "opt_solver.h"
 #include "arith_decl_plugin.h"
@@ -35,16 +34,24 @@ Notes:
 
 namespace opt {
 
+    context::context(ast_manager& m):
+        m(m),
+        m_hard_constraints(m),
+        m_soft_constraints(m),
+        m_objectives(m),
+        m_opt_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();
 
@@ -76,8 +83,7 @@ namespace opt {
             for (unsigned i = 0; i < fmls_copy.size(); ++i) {
                 s->assert_expr(fmls_copy[i].get());
             }
-            optimize_objectives obj(m, get_opt_solver(*s)); // TBD: make an attribute
-            is_sat = obj(m_objectives, values);
+            is_sat = m_opt_objectives(get_opt_solver(*s), m_objectives, values);
             std::cout << "is-sat: " << is_sat << std::endl;
 
             if (is_sat != l_true) {
@@ -119,12 +125,14 @@ namespace opt {
         if (m_solver) {
             m_solver->cancel();
         }
+        m_opt_objectives.set_cancel(true);
     }
 
     void context::reset_cancel() {
         if (m_solver) {
             m_solver->reset_cancel();
         }
+        m_opt_objectives.set_cancel(false);
     }
 
     void context::add_objective(app* t, bool is_max) {
@@ -140,5 +148,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

@@ -27,6 +27,7 @@ Notes:
 
 #include "ast.h"
 #include "solver.h"
+#include "optimize_objectives.h"
 
 namespace opt {
 
@@ -40,14 +41,10 @@ namespace opt {
         app_ref_vector   m_objectives;
         svector<bool>    m_is_max;
         ref<solver>      m_solver;
-
+        params_ref       m_params;
+        optimize_objectives m_opt_objectives;
     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 +66,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;
 

src/opt/opt_solver.cpp

@@ -1,3 +1,23 @@
+/*++
+Copyright (c) 2013 Microsoft Corporation
+
+Module Name:
+
+    opt_solver.cpp
+
+Abstract:
+
+    Wraps smt::kernel as a solver for optimization
+
+Author:
+
+    Anh-Dung Phan (t-anphan) 2013-10-16
+
+Notes:
+
+    Based directly on smt_solver.
+   
+--*/
 #include"reg_decl_plugins.h"
 #include"opt_solver.h"
 #include"smt_context.h"

src/opt/optimize_objectives.cpp

@@ -67,28 +67,28 @@ namespace opt {
         ast_manager& m = objectives.get_manager();
         arith_util autil(m);
 
-        s.reset_objectives();
+        s->reset_objectives();
         values.reset();
         // First check_sat call to initialize theories
-        lbool is_sat = s.check_sat(0, 0);
+        lbool is_sat = s->check_sat(0, 0);
         if (is_sat == l_false) {
             return is_sat;
         }
 
-        opt_solver::scoped_push _push(s);
+        opt_solver::scoped_push _push(*s);
 
-        opt_solver::toggle_objective _t(s, true);
+        opt_solver::toggle_objective _t(*s, true);
 
         for (unsigned i = 0; i < objectives.size(); ++i) {
-            s.add_objective(objectives[i].get());
+            s->add_objective(objectives[i].get());
             values.push_back(inf_eps(rational(-1),inf_rational(0)));
         }
 
-        is_sat = s.check_sat(0, 0);
+        is_sat = s->check_sat(0, 0);
         
                 
         while (is_sat == l_true && !m_cancel) {
-            set_max(values, s.get_objective_values());
+            set_max(values, s->get_objective_values());
             IF_VERBOSE(1, 
                        for (unsigned i = 0; i < values.size(); ++i) {
                            verbose_stream() << values[i] << " ";
@@ -99,11 +99,11 @@ namespace opt {
 
             for (unsigned i = 0; i < objectives.size(); ++i) {
                 inf_eps const& v = values[i];
-                disj.push_back(s.block_lower_bound(i, v));
+                disj.push_back(s->block_lower_bound(i, v));
             }
             constraint = m.mk_or(disj.size(), disj.c_ptr());
-            s.assert_expr(constraint);
-            is_sat = s.check_sat(0, 0);
+            s->assert_expr(constraint);
+            is_sat = s->check_sat(0, 0);
         }      
 
         
@@ -117,7 +117,8 @@ namespace opt {
        Takes solver with hard constraints added.
        Returns an optimal assignment to objective functions.
     */
-    lbool optimize_objectives::operator()(app_ref_vector& objectives, vector<inf_eps>& values) {
+    lbool optimize_objectives::operator()(opt_solver& solver, app_ref_vector& objectives, vector<inf_eps>& values) {
+        s = &solver;
         return basic_opt(objectives, values);
     }
 

src/opt/optimize_objectives.h

@@ -29,12 +29,12 @@ namespace opt {
 
     class optimize_objectives {
         ast_manager& m;
-        opt_solver& s;
+        opt_solver*  s;
         volatile bool m_cancel;
     public:
-        optimize_objectives(ast_manager& m, opt_solver& s): m(m), s(s), m_cancel(false) {}
+        optimize_objectives(ast_manager& m): m(m), s(0), m_cancel(false) {}
 
-        lbool operator()(app_ref_vector& objectives, vector<inf_eps>& values);
+        lbool operator()(opt_solver& s, app_ref_vector& objectives, vector<inf_eps>& values);
 
         void set_cancel(bool f);