From f4e2b232380f16b11e86280231eeedce3e0e05d9 Mon Sep 17 00:00:00 2001 From: Anh-Dung Phan Date: Wed, 16 Oct 2013 17:56:35 -0700 Subject: [PATCH] Create placeholders to optimization methods --- scripts/mk_util.py | 2 +- src/opt/opt_cmds.cpp | 100 +++++++++++--------------------- src/opt/opt_context.cpp | 94 ++++++++++++++++++++++++++++++ src/opt/opt_context.h | 66 +++++++++++++++++++++ src/opt/optimize_objectives.cpp | 60 +++++++++++++++++++ src/opt/optimize_objectives.h | 35 +++++++++++ src/opt/plan.txt | 8 +++ src/opt/weighted_maxsat.cpp | 33 +++++++++++ src/opt/weighted_maxsat.h | 33 +++++++++++ 9 files changed, 363 insertions(+), 68 deletions(-) create mode 100644 src/opt/opt_context.cpp create mode 100644 src/opt/opt_context.h create mode 100644 src/opt/optimize_objectives.cpp create mode 100644 src/opt/optimize_objectives.h create mode 100644 src/opt/weighted_maxsat.cpp create mode 100644 src/opt/weighted_maxsat.h diff --git a/scripts/mk_util.py b/scripts/mk_util.py index b65af4335..98f213dd5 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -59,7 +59,7 @@ SHOW_CPPS = True VS_X64 = False ONLY_MAKEFILES = False Z3PY_SRC_DIR=None -VS_PROJ = True +VS_PROJ = False TRACE = False DOTNET_ENABLED=False JAVA_ENABLED=False diff --git a/src/opt/opt_cmds.cpp b/src/opt/opt_cmds.cpp index 8c0a458d5..b4b6d62f2 100644 --- a/src/opt/opt_cmds.cpp +++ b/src/opt/opt_cmds.cpp @@ -18,37 +18,18 @@ Notes: #include "opt_cmds.h" #include "cmd_context.h" #include "ast_pp.h" -#include "smt_solver.h" -#include "fu_malik.h" -class opt_context { - ast_manager& m; - expr_ref_vector m_formulas; - vector m_weights; +#include "opt_context.h" -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; + 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): + assert_weighted_cmd(cmd_context& ctx, opt::context* opt_ctx): cmd("assert-weighted"), m_opt_ctx(opt_ctx), m_idx(0), @@ -95,12 +76,11 @@ public: } virtual void execute(cmd_context & ctx) { - m_opt_ctx->add_formula(m_formula, m_weight); + m_opt_ctx->add_soft_constraint(m_formula, m_weight); reset(ctx); } virtual void finalize(cmd_context & ctx) { - std::cout << "FINALIZE\n"; } }; @@ -111,19 +91,16 @@ public: // to do the feasibility check. class min_maximize_cmd : public cmd { bool m_is_max; - expr_ref m_term; - opt_context* m_opt_ctx; + opt::context* m_opt_ctx; public: - min_maximize_cmd(cmd_context& ctx, opt_context* opt_ctx, bool is_max): + min_maximize_cmd(cmd_context& ctx, opt::context* opt_ctx, bool is_max): cmd(is_max?"maximize":"minimize"), m_is_max(is_max), - m_term(ctx.m()), m_opt_ctx(opt_ctx) {} virtual void reset(cmd_context & ctx) { - m_term = 0; } virtual char const * get_usage() const { return ""; } @@ -134,7 +111,9 @@ public: virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { return CPK_EXPR; } virtual void set_next_arg(cmd_context & ctx, expr * t) { - m_term = t; + // TODO: type check objective term. It should pass basic sanity being + // integer, real (, bit-vector) or other supported objective function type. + m_opt_ctx->add_objective(t, m_is_max); } virtual void failure_cleanup(cmd_context & ctx) { @@ -142,58 +121,45 @@ public: } virtual void execute(cmd_context & ctx) { - ast_manager& m = m_term.get_manager(); - std::cout << "TODO: " << mk_pp(m_term, ctx.m()) << "\n"; - // Here is how to retrieve the soft constraints - expr_ref_vector const& fmls = m_opt_ctx->formulas(); - vector const& ws = m_opt_ctx->weights(); + } - // TODO: move most functionaltiy to separate module, because it is going to grow.. - ref s; - symbol logic; - params_ref p; - p.set_bool("model", true); - p.set_bool("unsat_core", true); - s = mk_smt_solver(m, p, logic); + +}; + +class optimize_cmd : public cmd { + opt::context* m_opt_ctx; +public: + optimize_cmd(opt::context* opt_ctx): + 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 failure_cleanup(cmd_context & ctx) { + reset(ctx); + } + + virtual void execute(cmd_context & ctx) { ptr_vector::const_iterator it = ctx.begin_assertions(); ptr_vector::const_iterator end = ctx.end_assertions(); for (; it != end; ++it) { - s->assert_expr(*it); - } - expr_ref_vector fmls_copy(fmls); - if (is_maxsat_problem(ws)) { - lbool is_sat = opt::fu_malik_maxsat(*s, fmls_copy); - std::cout << "is-sat: " << is_sat << "\n"; - if (is_sat == l_true) { - for (unsigned i = 0; i < fmls_copy.size(); ++i) { - std::cout << mk_pp(fmls_copy[i].get(), m) << "\n"; - } - } - } - else { - NOT_IMPLEMENTED_YET(); + m_opt_ctx->add_hard_constraint(*it); } + m_opt_ctx->optimize(); - // handle optimization criterion. + } - private: - bool is_maxsat_problem(vector const& ws) const { - for (unsigned i = 0; i < ws.size(); ++i) { - if (!ws[i].is_one()) { - return false; - } - } - return true; - } }; void install_opt_cmds(cmd_context & ctx) { - opt_context* opt_ctx = alloc(opt_context, ctx.m()); + 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)); + ctx.insert(alloc(optimize_cmd, opt_ctx)); } diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp new file mode 100644 index 000000000..dbbcffa7c --- /dev/null +++ b/src/opt/opt_context.cpp @@ -0,0 +1,94 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + opt_context.cpp + +Abstract: + Facility for running optimization problem. + +Author: + + Anh-Dung Phan (t-anphan) 2013-10-16 + +Notes: + +--*/ + + +#include "opt_context.h" +#include "smt_solver.h" +#include "fu_malik.h" +#include "weighted_maxsat.h" +#include "optimize_objectives.h" +#include "ast_pp.h" + +namespace opt { + + void context::optimize() { + + expr_ref_vector const& fmls = m_soft_constraints; + + ref s; + symbol logic; + params_ref p; + p.set_bool("model", true); + p.set_bool("unsat_core", true); + s = mk_smt_solver(m, p, logic); + + for (unsigned i = 0; i < m_hard_constraints.size(); ++i) { + s->assert_expr(m_hard_constraints[i].get()); + } + + expr_ref_vector fmls_copy(fmls); + lbool is_sat; + if (!fmls.empty()) { + if (is_maxsat_problem()) { + is_sat = opt::fu_malik_maxsat(*s, fmls_copy); + } + else { + is_sat = weighted_maxsat(*s, fmls_copy, m_weights); + } + std::cout << "is-sat: " << is_sat << "\n"; + if (is_sat != l_true) { + return; + } + for (unsigned i = 0; i < fmls_copy.size(); ++i) { + std::cout << "Satisfying soft constraint: " << mk_pp(fmls_copy[i].get(), m) << "\n"; + } + } + + if (!m_objectives.empty()) { + vector > values; + for (unsigned i = 0; i < fmls_copy.size(); ++i) { + s->assert_expr(fmls_copy[i].get()); + } + is_sat = optimize_objectives(*s, m_objectives, m_is_max, values); + std::cout << "is-sat: " << is_sat << "\n"; + if (is_sat != l_true) { + return; + } + for (unsigned i = 0; i < values.size(); ++i) { + // display + } + } + + if (m_objectives.empty() && m_soft_constraints.empty()) { + is_sat = s->check_sat(0,0); + std::cout << "nothing to optimize: is-sat " << is_sat << "\n"; + } + + } + + bool context::is_maxsat_problem() const { + vector const& ws = m_weights; + for (unsigned i = 0; i < ws.size(); ++i) { + if (!ws[i].is_one()) { + return false; + } + } + return true; + } + +} diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h new file mode 100644 index 000000000..9e226389e --- /dev/null +++ b/src/opt/opt_context.h @@ -0,0 +1,66 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + opt_context.h + +Abstract: + Facility for running optimization problem. + +Author: + + Anh-Dung Phan (t-anphan) 2013-10-16 + +Notes: + +--*/ +#ifndef _OPT_CONTEXT_H_ +#define _OPT_CONTEXT_H_ + +#include "ast.h" + +namespace opt { + + class context { + ast_manager& m; + expr_ref_vector m_hard_constraints; + expr_ref_vector m_soft_constraints; + vector m_weights; + + expr_ref_vector m_objectives; + svector m_is_max; + + public: + context(ast_manager& m): + m(m), + m_hard_constraints(m), + m_soft_constraints(m), + m_objectives(m) + {} + + void add_soft_constraint(expr* f, rational const& w) { + m_soft_constraints.push_back(f); + m_weights.push_back(w); + } + + void add_objective(expr* t, bool is_max) { + m_objectives.push_back(t); + m_is_max.push_back(is_max); + } + + void add_hard_constraint(expr* f) { + m_hard_constraints.push_back(f); + } + + void optimize(); + + private: + bool is_maxsat_problem() const; + + }; + + +} + +#endif \ No newline at end of file diff --git a/src/opt/optimize_objectives.cpp b/src/opt/optimize_objectives.cpp new file mode 100644 index 000000000..6f7f5c85e --- /dev/null +++ b/src/opt/optimize_objectives.cpp @@ -0,0 +1,60 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + optimize_objectives.cpp + +Abstract: + + Objective optimization method. + +Author: + + Anh-Dung Phan (t-anphan) 2013-10-16 + +Notes: + +--*/ + + +#include "optimize_objectives.h" + +namespace opt { + + /* + Enumerate locally optimal assignments until fixedpoint. + */ + lbool mathsat_style_opt(solver& s, + expr_ref_vector& objectives, svector const& is_max, + vector >& values) { + lbool is_sat; + is_sat = s.check_sat(0,0); + if (is_sat != l_true) { + return is_sat; + } + // assume that s is instrumented to produce locally optimal assignments. + + while (is_sat != l_false) { + model_ref model; + s.get_model(model); + // extract values for objectives. + // store them in values. + // assert there must be something better. + is_sat = s.check_sat(0,0); + } + return l_true; + + } + + /** + Takes solver with hard constraints added. + Returns an optimal assignment to objective functions. + */ + + lbool optimize_objectives(solver& s, + expr_ref_vector& objectives, svector const& is_max, + vector >& values) { + return mathsat_style_opt(s, objectives, is_max, values); + } +} diff --git a/src/opt/optimize_objectives.h b/src/opt/optimize_objectives.h new file mode 100644 index 000000000..a6c8e3602 --- /dev/null +++ b/src/opt/optimize_objectives.h @@ -0,0 +1,35 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + optimize_objectives.h + +Abstract: + + Objective optimization method. + +Author: + + Anh-Dung Phan (t-anphan) 2013-10-16 + +Notes: + +--*/ +#ifndef _OPT_OBJECTIVES_H_ +#define _OPT_OBJECTIVES_H_ + +#include "solver.h" + +namespace opt { + /** + Takes solver with hard constraints added. + Returns an optimal assignment to objective functions. + */ + + lbool optimize_objectives(solver& s, + expr_ref_vector& objectives, svector const& is_max, + vector >& values); +}; + +#endif \ No newline at end of file diff --git a/src/opt/plan.txt b/src/opt/plan.txt index f728747ed..aabad6cc3 100644 --- a/src/opt/plan.txt +++ b/src/opt/plan.txt @@ -7,3 +7,11 @@ Similar to muz\fp\dl_cmds: Identifier is optional and used to group constraints together. The F# sample illustrates what is meant. +Next steps: + - replace solver by opt_solver. + - create a file called opt_solver, copy most from smt_solver into it. + Add some functions to enable/disable post-optimization on feasiable state. + - Add methods to theory_arith.h to enable/disable post-optimization + - Add method(s) to theory_arith.h to register objective functions. + - Add post-optimization step to theory_arith_core.h + - (Figure out how to do multi-objective in this framework directly besides naive loop) diff --git a/src/opt/weighted_maxsat.cpp b/src/opt/weighted_maxsat.cpp new file mode 100644 index 000000000..832793e32 --- /dev/null +++ b/src/opt/weighted_maxsat.cpp @@ -0,0 +1,33 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + weighted_maxsat.h + +Abstract: + Weighted MAXSAT module + +Author: + + Anh-Dung Phan (t-anphan) 2013-10-16 + +Notes: + +--*/ + +#include "weighted_maxsat.h" + +namespace opt { + /** + Takes solver with hard constraints added. + Returns a maximal satisfying subset of weighted soft_constraints + that are still consistent with the solver state. + */ + + lbool weighted_maxsat(solver& s, expr_ref_vector& soft_constraints, vector const& weights) { + NOT_IMPLEMENTED_YET(); + return l_false; + } +}; + diff --git a/src/opt/weighted_maxsat.h b/src/opt/weighted_maxsat.h new file mode 100644 index 000000000..542d0bafc --- /dev/null +++ b/src/opt/weighted_maxsat.h @@ -0,0 +1,33 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + weighted_maxsat.h + +Abstract: + Weighted MAXSAT module + +Author: + + Anh-Dung Phan (t-anphan) 2013-10-16 + +Notes: + +--*/ +#ifndef _OPT_WEIGHTED_MAX_SAT_H_ +#define _OPT_WEIGHTED_MAX_SAT_H_ + +#include "solver.h" + +namespace opt { + /** + Takes solver with hard constraints added. + Returns a maximal satisfying subset of weighted soft_constraints + that are still consistent with the solver state. + */ + + lbool weighted_maxsat(solver& s, expr_ref_vector& soft_constraints, vector const& weights); +}; + +#endif