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

scripts/mk_project.py

@@ -63,6 +63,7 @@ def init_project_def():
     add_lib('tab', ['muz', 'transforms'], 'muz/tab')
     add_lib('bmc', ['muz', 'transforms'], 'muz/bmc')
     add_lib('fp',  ['muz', 'pdr', 'clp', 'tab', 'rel', 'bmc'], 'muz/fp')
+    add_lib('opt', ['smt'], 'opt')
     add_lib('smtlogic_tactics', ['arith_tactics', 'bv_tactics', 'nlsat_tactic', 'smt_tactic', 'aig_tactic', 'fp', 'muz','qe'], 'tactic/smtlogics')
     add_lib('ufbv_tactic', ['normal_forms', 'core_tactics', 'macros', 'smt_tactic', 'rewriter'], 'tactic/ufbv')
     add_lib('portfolio', ['smtlogic_tactics', 'ufbv_tactic', 'fpa', 'aig_tactic', 'fp',  'qe','sls_tactic', 'subpaving_tactic'], 'tactic/portfolio')
@@ -70,7 +71,7 @@ def init_project_def():
     API_files = ['z3_api.h', 'z3_algebraic.h', 'z3_polynomial.h', 'z3_rcf.h']
     add_lib('api', ['portfolio', 'user_plugin', 'smtparser', 'realclosure'],
             includes2install=['z3.h', 'z3_v1.h', 'z3_macros.h'] + API_files)
-    add_exe('shell', ['api', 'sat', 'extra_cmds'], exe_name='z3')
+    add_exe('shell', ['api', 'sat', 'extra_cmds','opt'], exe_name='z3')
     add_exe('test', ['api', 'fuzzing'], exe_name='test-z3', install=False)
     add_dll('api_dll', ['api', 'sat', 'extra_cmds'], 'api/dll', 
             reexports=['api'], 

src/cmd_context/cmd_context.cpp

@@ -335,10 +335,10 @@ cmd_context::~cmd_context() {
     if (m_main_ctx) {
         set_verbose_stream(std::cerr);
     }
-    reset(true); 
     finalize_cmds();
     finalize_tactic_cmds();
     finalize_probes();
+    reset(true); 
     m_solver = 0;
     m_check_sat_result = 0;
 }

src/opt/opt_cmds.cpp

@@ -0,0 +1,150 @@
+/*++
+Copyright (c) 2013 Microsoft Corporation
+
+Module Name:
+
+    opt_cmds.cpp
+
+Abstract:
+    Commands for optimization benchmarks
+
+Author:
+
+    Anh-Phan Dung (t-anphan) 2013-10-14
+
+Notes:
+
+--*/
+#include "opt_cmds.h"
+#include "cmd_context.h"
+#include "ast_pp.h"
+
+class opt_context {
+    ast_manager& m;
+    expr_ref_vector m_formulas;
+    vector<rational> m_weights;
+public:
+    opt_context(ast_manager& m):
+        m(m),
+        m_formulas(m)        
+    {}
+
+    void add_formula(expr* f, rational const& w) {
+        m_formulas.push_back(f);
+        m_weights.push_back(w);
+    }
+        
+    expr_ref_vector const& formulas() const { return m_formulas; }
+    vector<rational> const& weights() const { return m_weights; }
+};
+
+class assert_weighted_cmd : public cmd {
+    opt_context* m_opt_ctx;
+    unsigned   m_idx;
+    expr_ref   m_formula;
+    rational   m_weight;
+public:
+    assert_weighted_cmd(cmd_context& ctx, opt_context* opt_ctx):
+        cmd("assert-weighted"),
+        m_opt_ctx(opt_ctx),
+        m_idx(0),
+        m_formula(ctx.m()),
+        m_weight(0)
+    {}
+
+    virtual ~assert_weighted_cmd() {
+        dealloc(m_opt_ctx);
+    }
+
+    virtual void reset(cmd_context & ctx) { 
+        m_idx = 0; 
+        m_formula = 0;
+    }
+    virtual char const * get_usage() const { return "<formula> <rational-weight>"; }
+    virtual char const * get_descr(cmd_context & ctx) const { return "assert soft constraint with weight"; }
+    virtual unsigned get_arity() const { return 2; }
+
+    // command invocation
+    virtual void prepare(cmd_context & ctx) {}
+    virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { if (m_idx == 0) return CPK_EXPR; return CPK_NUMERAL; }
+    virtual void set_next_arg(cmd_context & ctx, rational const & val) { 
+        SASSERT(m_idx == 1);
+        if (!val.is_pos()) {
+            throw cmd_exception("Invalid weight. Weights must be positive.");
+        }
+        m_weight = val;
+        ++m_idx;
+    }
+
+    virtual void set_next_arg(cmd_context & ctx, expr * t) {
+        SASSERT(m_idx == 0);
+        if (!ctx.m().is_bool(t)) {
+            throw cmd_exception("Invalid type for expression. Expected Boolean type.");
+        }
+        m_formula = t;
+        ++m_idx;
+    }
+
+    virtual void failure_cleanup(cmd_context & ctx) {
+        reset(ctx);
+    }
+
+    virtual void execute(cmd_context & ctx) {
+        std::cout << "TODO: " << mk_pp(m_formula, ctx.m()) << " " << m_weight << "\n";
+        m_opt_ctx->add_formula(m_formula, m_weight);
+        reset(ctx);
+    }
+
+    virtual void finalize(cmd_context & ctx) { 
+        std::cout << "FINALIZE\n";
+    }
+
+};
+
+// what amounts to check-sat, but uses the *single* objective function.
+// alternative is to register multiple objective functions using
+// minimize/maximize and then use check-sat or some variant of it 
+// to do the feasibility check.
+class min_maximize_cmd : public cmd {
+    bool m_is_max;
+    opt_context* m_opt_ctx;
+public:
+    min_maximize_cmd(cmd_context& ctx, opt_context* opt_ctx, bool is_max):
+        cmd(is_max?"maximize":"minimize"),
+        m_is_max(is_max),
+        m_opt_ctx(opt_ctx)
+    {}
+
+    virtual char const * get_usage() const { return "<term>"; }
+    virtual char const * get_descr(cmd_context & ctx) const { return "check sat modulo objective function";}
+    virtual unsigned get_arity() const { return 1; }
+
+    // etc. TODO: Phan, add the appropriate callbacks as a warmup.
+
+    virtual void execute(cmd_context & ctx) {
+        // here is how to retrieve the soft constraints:
+        m_opt_ctx->formulas();
+        m_opt_ctx->weights();
+        get_background(ctx);
+        // reset m_opt_ctx?
+    }
+
+private:
+    void get_background(cmd_context& ctx) {
+        ptr_vector<expr>::const_iterator it  = ctx.begin_assertions();
+        ptr_vector<expr>::const_iterator end = ctx.end_assertions();
+        for (; it != end; ++it) {
+            // need a solver object that supports soft constraints
+            // m_solver.assert_expr(*it);
+        }
+    }
+
+};
+
+
+void install_opt_cmds(cmd_context & ctx) {
+    opt_context* opt_ctx = alloc(opt_context, ctx.m());
+    ctx.insert(alloc(assert_weighted_cmd, ctx, opt_ctx));
+    ctx.insert(alloc(min_maximize_cmd, ctx, opt_ctx, true));
+    ctx.insert(alloc(min_maximize_cmd, ctx, opt_ctx, false));
+}

src/opt/opt_cmds.h

@@ -0,0 +1,28 @@
+/*++
+Copyright (c) 2013 Microsoft Corporation
+
+Module Name:
+
+    opt_cmds.h
+
+Abstract:
+    Commands for optimization benchmarks
+
+Author:
+
+    Anh-Phan Dung (t-anphan) 2013-10-14
+
+Notes:
+
+--*/
+#ifndef _OPT_CMDS_H_
+#define _OPT_CMDS_H_
+
+#include "ast.h"
+
+class cmd_context;
+
+void install_opt_cmds(cmd_context & ctx);
+
+
+#endif

src/shell/smtlib_frontend.cpp

@@ -26,6 +26,7 @@ Revision History:
 #include"smt2parser.h"
 #include"dl_cmds.h"
 #include"dbg_cmds.h"
+#include"opt_cmds.h"
 #include"polynomial_cmds.h"
 #include"subpaving_cmds.h"
 #include"smt_strategic_solver.h"
@@ -110,6 +111,7 @@ unsigned read_smtlib2_commands(char const * file_name) {
     install_dbg_cmds(ctx);
     install_polynomial_cmds(ctx);
     install_subpaving_cmds(ctx);
+    install_opt_cmds(ctx);
 
     g_cmd_context = &ctx;
     signal(SIGINT, on_ctrl_c);