From 726f66a77c19d41284d9793463f7925c2e2b3216 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 14 Oct 2013 17:08:24 -0700 Subject: [PATCH] initial opt commands Signed-off-by: Nikolaj Bjorner --- scripts/mk_project.py | 3 +- src/cmd_context/cmd_context.cpp | 2 +- src/opt/opt_cmds.cpp | 150 ++++++++++++++++++++++++++++++++ src/opt/opt_cmds.h | 28 ++++++ src/shell/smtlib_frontend.cpp | 2 + 5 files changed, 183 insertions(+), 2 deletions(-) create mode 100644 src/opt/opt_cmds.cpp create mode 100644 src/opt/opt_cmds.h diff --git a/scripts/mk_project.py b/scripts/mk_project.py index 6054f4769..ccae41dcb 100644 --- a/scripts/mk_project.py +++ b/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'], diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 261af3092..023b30903 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/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; } diff --git a/src/opt/opt_cmds.cpp b/src/opt/opt_cmds.cpp new file mode 100644 index 000000000..e4a64ae6c --- /dev/null +++ b/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 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 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 " "; } + 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 ""; } + 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::const_iterator it = ctx.begin_assertions(); + ptr_vector::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)); +} diff --git a/src/opt/opt_cmds.h b/src/opt/opt_cmds.h new file mode 100644 index 000000000..0ba028c63 --- /dev/null +++ b/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 diff --git a/src/shell/smtlib_frontend.cpp b/src/shell/smtlib_frontend.cpp index b5d8635da..2ec1e200a 100644 --- a/src/shell/smtlib_frontend.cpp +++ b/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);