From 18815e3e53317d46443a86d09df20b7befe65a19 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 3 Dec 2013 13:36:25 -0800 Subject: [PATCH] reorganizing input Signed-off-by: Nikolaj Bjorner --- src/opt/objective_ast.cpp | 54 -------- src/opt/objective_ast.h | 108 --------------- src/opt/objective_decl_plugin.cpp | 89 ------------- src/opt/objective_decl_plugin.h | 71 ---------- src/opt/opt_cmds.cpp | 214 +++++++++++++----------------- src/opt/opt_context.cpp | 152 ++++++++++----------- src/opt/opt_context.h | 41 ++++-- src/opt/opt_params.pyg | 2 +- 8 files changed, 192 insertions(+), 539 deletions(-) delete mode 100644 src/opt/objective_ast.cpp delete mode 100644 src/opt/objective_ast.h delete mode 100644 src/opt/objective_decl_plugin.cpp delete mode 100644 src/opt/objective_decl_plugin.h diff --git a/src/opt/objective_ast.cpp b/src/opt/objective_ast.cpp deleted file mode 100644 index 79d2516d6..000000000 --- a/src/opt/objective_ast.cpp +++ /dev/null @@ -1,54 +0,0 @@ -/*++ -Copyright (c) 2013 Microsoft Corporation - -Module Name: - - objective_ast.h - -Abstract: - Abstract data-type for compound objectives. - -Author: - - Anh-Dung Phan (t-anphan) 2013-11-26 - -Notes: - ---*/ - -#include"objective_ast.h" - -namespace opt { - - objective* objective::mk_max(expr_ref& e) { return alloc(min_max_objective, MAXIMIZE, e); }; - objective* objective::mk_min(expr_ref& e) { return alloc(min_max_objective, MINIMIZE, e); }; - objective* objective::mk_maxsat(symbol id) { return alloc(maxsat_objective, id); }; - - objective* objective::mk_lex(unsigned sz, objective * const* children) { - return alloc(compound_objective, LEX, sz, children); - }; - - objective* objective::mk_box(unsigned sz, objective * const* children) { - return alloc(compound_objective, BOX, sz, children); - }; - - objective* objective::mk_pareto(unsigned sz, objective * const* children) { - return alloc(compound_objective, PARETO, sz, children); - }; - - compound_objective& objective::get_compound() { - SASSERT(m_type == LEX || m_type == BOX || m_type == PARETO); - return dynamic_cast(*this); - } - - min_max_objective& objective::get_min_max() { - SASSERT(m_type == MAXIMIZE || m_type == MINIMIZE); - return dynamic_cast(*this); - } - - maxsat_objective& objective::get_maxsat() { - SASSERT(m_type == MAXSAT); - return dynamic_cast(*this); - } - -}; diff --git a/src/opt/objective_ast.h b/src/opt/objective_ast.h deleted file mode 100644 index 31a2bf543..000000000 --- a/src/opt/objective_ast.h +++ /dev/null @@ -1,108 +0,0 @@ -/*++ -Copyright (c) 2013 Microsoft Corporation - -Module Name: - - objective_ast.h - -Abstract: - Abstract data-type for compound objectives. - -Author: - - Nikolaj Bjorner (nbjorner) 2013-11-21 - -Notes: - ---*/ -#ifndef __OBJECTIVE_AST_H_ -#define __OBJECTIVE_AST_H_ - -#include"ast.h" - -namespace opt { - - enum objective_t { - MINIMIZE, - MAXIMIZE, - MAXSAT, - LEX, - BOX, - PARETO - }; - - class compound_objective; - class min_max_objective; - class maxsat_objective; - - class objective { - objective_t m_type; - public: - objective(objective_t ty): - m_type(ty) - {} - virtual ~objective() {} - - objective_t type() const { return m_type; } - - // constructors; - static objective* mk_max(expr_ref& e); - static objective* mk_min(expr_ref& e); - static objective* mk_maxsat(symbol id); - - static objective* mk_lex(unsigned sz, objective * const* children); - static objective* mk_box(unsigned sz, objective * const* children); - static objective* mk_pareto(unsigned sz, objective * const* children); - - // accessors (implicit cast operations) - compound_objective& get_compound(); - min_max_objective& get_min_max(); - maxsat_objective& get_maxsat(); - }; - - class compound_objective : public objective { - ptr_vector m_children; - public: - compound_objective(objective_t t, unsigned sz, objective * const* children): - objective(t), - m_children(sz, children) {} - - virtual ~compound_objective() { - ptr_vector::iterator it = m_children.begin(), end = m_children.end(); - for (; it != end; ++it) { - dealloc(*it); - } - } - - objective *const* children() const { return m_children.c_ptr(); } - - unsigned num_children() const { return m_children.size(); } - }; - - class min_max_objective : public objective { - bool m_is_max; - expr_ref m_expr; - public: - min_max_objective(bool is_max, expr_ref& e): - objective(is_max ? MAXIMIZE : MINIMIZE), - m_is_max(is_max), - m_expr(e) {} - - virtual ~min_max_objective() {} - - expr* term() { return m_expr; } - bool is_max() const { return m_is_max; } - }; - - class maxsat_objective : public objective { - symbol m_id; - public: - maxsat_objective(symbol const& id): objective(MAXSAT), m_id(id) {} - virtual ~maxsat_objective() {} - - symbol const& get_id() const { return m_id; } - }; - -}; - -#endif diff --git a/src/opt/objective_decl_plugin.cpp b/src/opt/objective_decl_plugin.cpp deleted file mode 100644 index 9bca883ff..000000000 --- a/src/opt/objective_decl_plugin.cpp +++ /dev/null @@ -1,89 +0,0 @@ -/*++ -Copyright (c) 2013 Microsoft Corporation - -Module Name: - - objective_decl_plugin.cpp - -Abstract: - Abstract data-type for compound objectives. - -Author: - - Nikolaj Bjorner (nbjorner) 2013-11-21 - -Notes: - ---*/ - -#include "objective_decl_plugin.h" - -namespace opt{ - objective_decl_plugin::objective_decl_plugin() {} - - objective_decl_plugin::~objective_decl_plugin() {} - - sort * objective_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) { - SASSERT(k == OBJECTIVE_SORT); - SASSERT(num_parameters == 0); - return m_manager->mk_sort(symbol("objective"), sort_info(get_family_id(), k)); - } - - symbol objective_decl_plugin::get_name(obj_kind k) const { - switch(k) { - case OP_MINIMIZE: return symbol("minimize"); - case OP_MAXIMIZE: return symbol("maximize"); - case OP_LEX: return symbol("lex"); - case OP_BOX: return symbol("box"); - case OP_PARETO: return symbol("pareto"); - default: - UNREACHABLE(); - return symbol(); - } - } - - func_decl * objective_decl_plugin::mk_func_decl( - decl_kind k, unsigned num_parameters, parameter const * parameters, - unsigned arity, sort * const * domain, sort * range) { - SASSERT(num_parameters == 0); - symbol name = get_name(static_cast(k)); - func_decl_info info(get_family_id(), k, num_parameters, parameters); - range = mk_sort(OBJECTIVE_SORT, 0, 0); - return m_manager->mk_func_decl(name, arity, domain, range, info); - } - - void objective_decl_plugin::get_op_names(svector & op_names, symbol const & logic) { - if (logic == symbol::null) { - op_names.push_back(builtin_name(get_name(OP_MAXIMIZE).bare_str(), OP_MAXIMIZE)); - op_names.push_back(builtin_name(get_name(OP_MINIMIZE).bare_str(), OP_MINIMIZE)); - op_names.push_back(builtin_name(get_name(OP_LEX).bare_str(), OP_LEX)); - op_names.push_back(builtin_name(get_name(OP_BOX).bare_str(), OP_BOX)); - op_names.push_back(builtin_name(get_name(OP_PARETO).bare_str(), OP_PARETO)); - } - } - - - objective_util::objective_util(ast_manager& m): m(m), m_fid(m.get_family_id("objective")) {} - - app* objective_util::mk_max(expr_ref& e) { - expr* es[1] = { e }; - return m.mk_app(m_fid, OP_MAXIMIZE, 0, 0, 1, es); - } - app* objective_util::mk_min(expr_ref& e) { - expr* es[1] = { e }; - return m.mk_app(m_fid, OP_MINIMIZE, 0, 0, 1, es); - } - app* objective_util::mk_maxsat(symbol id) { - return m.mk_const(id, m.mk_sort(m_fid, OBJECTIVE_SORT, 0, 0)); - } - app* objective_util::mk_lex(unsigned sz, expr * const * children) { - return m.mk_app(m_fid, OP_LEX, 0, 0, sz, children); - } - app* objective_util::mk_box(unsigned sz, expr * const * children) { - return m.mk_app(m_fid, OP_BOX, 0, 0, sz, children); - } - app* objective_util::mk_pareto(unsigned sz, expr * const * children) { - return m.mk_app(m_fid, OP_PARETO, 0, 0, sz, children); - } - -} diff --git a/src/opt/objective_decl_plugin.h b/src/opt/objective_decl_plugin.h deleted file mode 100644 index 40b301ea8..000000000 --- a/src/opt/objective_decl_plugin.h +++ /dev/null @@ -1,71 +0,0 @@ -/*++ -Copyright (c) 2013 Microsoft Corporation - -Module Name: - - objective_decl_plugin.h - -Abstract: - Abstract data-type for compound objectives. - -Author: - - Nikolaj Bjorner (nbjorner) 2013-11-21 - -Notes: - ---*/ -#ifndef __OBJECTIVE_DECL_PLUGIN_H_ -#define __OBJECTIVE_DECL_PLUGIN_H_ - -#include"ast.h" - -namespace opt { - - enum obj_kind { - OP_MINIMIZE, - OP_MAXIMIZE, - OP_LEX, - OP_BOX, - OP_PARETO, - LAST_OBJ_OP - }; - - enum objective_sort_kind { - OBJECTIVE_SORT - }; - - class objective_decl_plugin : public decl_plugin { - public: - objective_decl_plugin(); - virtual ~objective_decl_plugin(); - - virtual sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters); - - virtual decl_plugin * mk_fresh() { return alloc(objective_decl_plugin); } - - virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, - unsigned arity, sort * const * domain, sort * range); - - virtual void get_op_names(svector & op_names, symbol const & logic); - - private: - symbol objective_decl_plugin::get_name(obj_kind k) const; - }; - - class objective_util { - ast_manager& m; - family_id m_fid; - public: - objective_util(ast_manager& m); - family_id get_family_id() const { return m_fid; } - app* mk_max(expr_ref& e); - app* mk_min(expr_ref& e); - app* mk_maxsat(symbol id); - app* mk_lex(unsigned sz, expr * const * children); - app* mk_box(unsigned sz, expr * const * children); - app* mk_pareto(unsigned sz, expr * const * children); - }; -}; - -#endif diff --git a/src/opt/opt_cmds.cpp b/src/opt/opt_cmds.cpp index 35e6ff9f0..db5906135 100644 --- a/src/opt/opt_cmds.cpp +++ b/src/opt/opt_cmds.cpp @@ -29,8 +29,6 @@ Notes: #include "scoped_ctrl_c.h" #include "scoped_timer.h" #include "parametric_cmd.h" -#include "objective_ast.h" -#include "objective_decl_plugin.h" class opt_context { cmd_context& ctx; @@ -41,21 +39,10 @@ public: opt_context(cmd_context& ctx): ctx(ctx) {} opt::context& operator()() { if (!m_opt) { - decl_plugin * p = alloc(opt::objective_decl_plugin); - ctx.register_plugin(symbol("objective"), p, true); m_opt = alloc(opt::context, ctx.m()); } return *m_opt; - } - - bool contains(symbol const& s) const { return m_ids.contains(s); } - - void insert(symbol const& s) { m_ids.insert(s); } - - sort* obj_sort(cmd_context& ctx) { - return ctx.m().mk_sort(ctx.m().get_family_id(symbol("objective")), opt::OBJECTIVE_SORT); - } - + } }; @@ -76,7 +63,6 @@ public: {} virtual ~assert_weighted_cmd() { - dealloc(&m_opt_ctx); } virtual void reset(cmd_context & ctx) { @@ -128,10 +114,81 @@ public: virtual void execute(cmd_context & ctx) { m_opt_ctx().add_soft_constraint(m_formula, m_weight, m_id); - if (!m_opt_ctx.contains(m_id)) { - ctx.insert(m_id, 0, ctx.m().mk_const(m_id, m_opt_ctx.obj_sort(ctx))); - m_opt_ctx.insert(m_id); + reset(ctx); + } + + virtual void finalize(cmd_context & ctx) { + } + +}; + + +class assert_soft_cmd : public parametric_cmd { + opt_context& m_opt_ctx; + unsigned m_idx; + expr* m_formula; + +public: + assert_soft_cmd(cmd_context& ctx, opt_context& opt_ctx): + parametric_cmd("assert-soft"), + m_opt_ctx(opt_ctx), + m_idx(0), + m_formula(0) + {} + + virtual ~assert_soft_cmd() { + } + + virtual void reset(cmd_context & ctx) { + m_idx = 0; + m_formula = 0; + } + + virtual char const * get_usage() const { return " [:weight ] [:id ]"; } + virtual char const * get_main_descr() const { return "assert soft constraint with optional weight and identifier"; } + + // 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 parametric_cmd::next_arg_kind(ctx); + } + + virtual void init_pdescrs(cmd_context & ctx, param_descrs & p) { + p.insert("weight", CPK_UINT, "(default: 1) penalty of not satisfying constraint."); + p.insert("dweight", CPK_DOUBLE, "(default: 1.0) penalty as double of not satisfying constraint."); + p.insert("id", CPK_SYMBOL, "(default: null) partition identifier for soft constraints."); + } + + 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) { + symbol w("weight"); + rational weight = rational(ps().get_uint(symbol("weight"), 0)); + if (weight.is_zero()) { + double d = ps().get_double(symbol("dweight"), 0.0); + if (d != 0.0) { + std::stringstream strm; + strm << d; + weight = rational(strm.str().c_str()); + } + } + if (weight.is_zero()) { + weight = rational::one(); + } + symbol id = ps().get_sym(symbol("id"), symbol::null); + m_opt_ctx().add_soft_constraint(m_formula, weight, id); reset(ctx); } @@ -183,6 +240,10 @@ public: m_opt_ctx(opt_ctx) {} + virtual ~optimize_cmd() { + dealloc(&m_opt_ctx); + } + virtual void init_pdescrs(cmd_context & ctx, param_descrs & p) { insert_timeout(p); insert_max_memory(p); @@ -263,6 +324,19 @@ private: }; + +void install_opt_cmds(cmd_context & ctx) { + opt_context* opt_ctx = alloc(opt_context, ctx); + ctx.insert(alloc(assert_weighted_cmd, ctx, *opt_ctx)); + ctx.insert(alloc(assert_soft_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)); +} + +#if 0 + ctx.insert(alloc(execute_cmd, *opt_ctx)); + class execute_cmd : public parametric_cmd { protected: expr * m_objective; @@ -365,108 +439,4 @@ private: stats.display_smt2(ctx.regular_stream()); } }; - -void install_opt_cmds(cmd_context & ctx) { - opt_context* opt_ctx = alloc(opt_context, ctx); - ctx.insert(alloc(assert_weighted_cmd, ctx, *opt_ctx)); - ctx.insert(alloc(execute_cmd, *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)); -} - -#if 0 - - expr_ref sexpr2expr(cmd_context & ctx, sexpr& s) { - expr_ref result(ctx.m()); - switch(s.get_kind()) { - case sexpr::COMPOSITE: { - sexpr& h = *s.get_child(0); - if (!h.is_symbol()) { - throw cmd_exception("invalid head symbol", s.get_line(), s.get_pos()); - } - symbol sym = h.get_symbol(); - expr_ref_vector args(ctx.m()); - for (unsigned i = 1; i < s.get_num_children(); ++i) { - args.push_back(sexpr2expr(ctx, *s.get_child(i))); - } - ctx.mk_app(sym, args.size(), args.c_ptr(), 0, 0, 0, result); - return result; - } - case sexpr::NUMERAL: - case sexpr::BV_NUMERAL: - // TBD: handle numerals - case sexpr::STRING: - case sexpr::KEYWORD: - throw cmd_exception("non-supported expression", s.get_line(), s.get_pos()); - case sexpr::SYMBOL: - ctx.mk_const(s.get_symbol(), result); - return result; - } - return result; - } - - opt::objective_t get_objective_type(sexpr& s) { - if (!s.is_symbol()) - throw cmd_exception("invalid objective, symbol expected", s.get_line(), s.get_pos()); - symbol const & sym = s.get_symbol(); - if (sym == symbol("maximize")) return opt::MAXIMIZE; - if (sym == symbol("minimize")) return opt::MINIMIZE; - if (sym == symbol("lex")) return opt::LEX; - if (sym == symbol("box")) return opt::BOX; - if (sym == symbol("pareto")) return opt::PARETO; - throw cmd_exception("invalid objective, unexpected input", s.get_line(), s.get_pos()); - } - - opt::objective* sexpr2objective(cmd_context & ctx, sexpr& s) { - if (s.is_symbol()) - throw cmd_exception("invalid objective, more arguments expected ", s.get_symbol(), s.get_line(), s.get_pos()); - if (s.is_composite()) { - sexpr * head = s.get_child(0); - opt::objective_t type = get_objective_type(*head); - switch(type) { - case opt::MAXIMIZE: - case opt::MINIMIZE: { - if (s.get_num_children() != 2) - throw cmd_exception("invalid objective, wrong number of arguments ", s.get_line(), s.get_pos()); - sexpr * arg = s.get_child(1); - expr_ref term(sexpr2expr(ctx, *arg), ctx.m()); - if (type == opt::MAXIMIZE) - return opt::objective::mk_max(term); - else - return opt::objective::mk_min(term); - } - case opt::MAXSAT: { - if (s.get_num_children() != 2) - throw cmd_exception("invalid objective, wrong number of arguments ", s.get_line(), s.get_pos()); - sexpr * arg = s.get_child(1); - if (!arg->is_symbol()) - throw cmd_exception("invalid objective, symbol expected", s.get_line(), s.get_pos()); - symbol const & id = arg->get_symbol(); - // TODO: check whether id is declared via assert-weighted - return opt::objective::mk_maxsat(id); - } - case opt::LEX: - case opt::BOX: - case opt::PARETO: { - if (s.get_num_children() <= 2) - throw cmd_exception("invalid objective, wrong number of arguments ", s.get_line(), s.get_pos()); - unsigned num_children = s.get_num_children(); - ptr_vector args; - for (unsigned i = 1; i < num_children; i++) - args.push_back(sexpr2objective(ctx, *s.get_child(i))); - switch(type) { - case opt::LEX: - return opt::objective::mk_lex(args.size(), args.c_ptr()); - case opt::BOX: - return opt::objective::mk_box(args.size(), args.c_ptr()); - case opt::PARETO: - return opt::objective::mk_pareto(args.size(), args.c_ptr()); - } - } - } - } - return 0; - } - #endif diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 6858b3fbc..95e2c4f16 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -27,9 +27,7 @@ namespace opt { context::context(ast_manager& m): m(m), m_hard_constraints(m), - m_optsmt(m), - m_objs(m), - m_obj_util(m) + m_optsmt(m) { m_params.set_bool("model", true); m_params.set_bool("unsat_core", true); @@ -48,35 +46,36 @@ namespace opt { if (!m_maxsmts.find(id, ms)) { ms = alloc(maxsmt, m); m_maxsmts.insert(id, ms); + m_objectives.push_back(objective(m, id)); } ms->add(f, w); } - lbool context::execute(expr* _obj, bool committed) { - SASSERT(is_app(_obj)); - app* obj = to_app(_obj); + void context::add_objective(app* t, bool is_max) { + app_ref tr(m); + m_objectives.push_back(objective(is_max, tr)); + } - if (obj->get_family_id() == null_family_id) { - return execute_maxsat(obj, committed); - } - if (obj->get_family_id() != m_obj_util.get_family_id()) { - return execute_min_max(obj, committed, true); + lbool context::optimize() { + opt_solver& s = get_solver(); + solver::scoped_push _sp(s); + for (unsigned i = 0; i < m_hard_constraints.size(); ++i) { + s.assert_expr(m_hard_constraints[i].get()); } - switch (obj->get_decl_kind()) { - case OP_MINIMIZE: - return execute_min_max(to_app(obj->get_arg(0)), committed, false); - case OP_MAXIMIZE: - return execute_min_max(to_app(obj->get_arg(0)), committed, true); - case OP_LEX: - return execute_lex(obj); - case OP_BOX: - return execute_box(obj); - case OP_PARETO: - return execute_pareto(obj); - default: - UNREACHABLE(); - return l_undef; + if (m_objectives.size() == 1) { + return execute(m_objectives[0], false); + } + + symbol pri = m_params.get_sym("priority", symbol("lex")); + if (pri == symbol("pareto")) { + return execute_pareto(); + } + else if (pri == symbol("box")) { + return execute_box(); + } + else { + return execute_lex(); } } @@ -89,35 +88,44 @@ namespace opt { } - lbool context::execute_maxsat(app* obj, bool committed) { + lbool context::execute_maxsat(symbol const& id, bool committed) { maxsmt* ms; - VERIFY(m_maxsmts.find(obj->get_decl()->get_name(), ms)); + VERIFY(m_maxsmts.find(id, ms)); lbool result = (*ms)(get_solver()); if (committed) ms->commit_assignment(); return result; } + + lbool context::execute(objective const& obj, bool committed) { + switch(obj.m_type) { + case O_MAXIMIZE: return execute_min_max(obj.m_term, committed, true); + case O_MINIMIZE: return execute_min_max(obj.m_term, committed, false); + case O_MAXSMT: return execute_maxsat(obj.m_id, committed); + default: UNREACHABLE(); return l_undef; + } + } - lbool context::execute_lex(app* obj) { + lbool context::execute_lex() { lbool r = l_true; - for (unsigned i = 0; r == l_true && i < obj->get_num_args(); ++i) { - r = execute(obj->get_arg(i), true); + for (unsigned i = 0; r == l_true && i < m_objectives.size(); ++i) { + r = execute(m_objectives[i], true); } return r; } - lbool context::execute_box(app* obj) { + lbool context::execute_box() { lbool r = l_true; - for (unsigned i = 0; r == l_true && i < obj->get_num_args(); ++i) { + for (unsigned i = 0; r == l_true && i < m_objectives.size(); ++i) { push(); - r = execute(obj->get_arg(i), false); + r = execute(m_objectives[i], false); pop(1); } return r; } - lbool context::execute_pareto(app* obj) { + lbool context::execute_pareto() { // TODO: record a stream of results from pareto front - return execute_lex(obj); + return execute_lex(); } opt_solver& context::get_solver() { @@ -132,60 +140,42 @@ namespace opt { get_solver().pop(sz); } - lbool context::optimize(expr* objective) { - if (!objective) { - return optimize(); - } - opt_solver& s = get_solver(); - solver::scoped_push _sp(s); - for (unsigned i = 0; i < m_hard_constraints.size(); ++i) { - s.assert_expr(m_hard_constraints[i].get()); - } - return execute(objective, false); - } - - lbool context::optimize() { - // Construct objectives - expr_ref_vector objectives(m); - expr_ref objective(m); - map_t::iterator it = m_maxsmts.begin(), end = m_maxsmts.end(); - for (; it != end; ++it) { - objectives.push_back(m_obj_util.mk_maxsat(it->m_key)); - } - for (unsigned i = 0; i < m_objs.size(); ++i) { - expr_ref e(m_objs[i].get(), m); - app * o = m_ismaxs[i] ? m_obj_util.mk_max(e) : m_obj_util.mk_min(e); - objectives.push_back(o); - } - if (m_params.get_bool("pareto", false)) { - objective = m_obj_util.mk_pareto(objectives.size(), objectives.c_ptr()); - } - else { - objective = m_obj_util.mk_box(objectives.size(), objectives.c_ptr()); - } - return optimize(objective); - } - void context::display_assignment(std::ostream& out) { - map_t::iterator it = m_maxsmts.begin(), end = m_maxsmts.end(); - for (; it != end; ++it) { - maxsmt* ms = it->m_value; - if (it->m_key != symbol::null) { - out << it->m_key << " : "; + for (unsigned i = 0; i < m_objectives.size(); ++i) { + objective const& obj = m_objectives[i]; + switch(obj.m_type) { + case O_MAXSMT: { + symbol s = obj.m_id; + if (s != symbol::null) { + out << s << " : "; + } + maxsmt* ms = m_maxsmts.find(s); + out << ms->get_value() << "\n"; + break; + } + default: + break; } - out << ms->get_value() << "\n"; } m_optsmt.display_assignment(out); } void context::display_range_assignment(std::ostream& out) { - map_t::iterator it = m_maxsmts.begin(), end = m_maxsmts.end(); - for (; it != end; ++it) { - maxsmt* ms = it->m_value; - if (it->m_key != symbol::null) { - out << it->m_key << " : "; + for (unsigned i = 0; i < m_objectives.size(); ++i) { + objective const& obj = m_objectives[i]; + switch(obj.m_type) { + case O_MAXSMT: { + symbol s = obj.m_id; + if (s != symbol::null) { + out << s << " : "; + } + maxsmt* ms = m_maxsmts.find(s); + out << "[" << ms->get_lower() << ":" << ms->get_upper() << "]\n"; + break; + } + default: + break; } - out << "[" << ms->get_lower() << ":" << ms->get_upper() << "]\n"; } m_optsmt.display_range_assignment(out); } diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h index 473abbb09..7bb3f86ed 100644 --- a/src/opt/opt_context.h +++ b/src/opt/opt_context.h @@ -29,7 +29,6 @@ Notes: #include "opt_solver.h" #include "optsmt.h" #include "maxsmt.h" -#include "objective_decl_plugin.h" namespace opt { @@ -37,24 +36,40 @@ namespace opt { class context { typedef map map_t; + enum objective_t { + O_MAXIMIZE, + O_MINIMIZE, + O_MAXSMT + }; + struct objective { + objective_t m_type; + app_ref m_term; // for maximize, minimize + symbol m_id; // for maxsmt + objective(bool is_max, app_ref& t): + m_type(is_max?O_MAXIMIZE:O_MINIMIZE), + m_term(t), + m_id() + {} + objective(ast_manager& m, symbol id): + m_type(O_MAXSMT), + m_term(m), + m_id(id) + {} + }; ast_manager& m; expr_ref_vector m_hard_constraints; ref m_solver; params_ref m_params; - optsmt m_optsmt; + optsmt m_optsmt; map_t m_maxsmts; - expr_ref_vector m_objs; - svector m_ismaxs; - objective_util m_obj_util; + vector m_objectives; public: context(ast_manager& m); ~context(); void add_soft_constraint(expr* f, rational const& w, symbol const& id); - void add_objective(app* t, bool is_max) { m_objs.push_back(t); m_ismaxs.push_back(is_max); } + void add_objective(app* t, bool is_max); void add_hard_constraint(expr* f) { m_hard_constraints.push_back(f); } - - lbool optimize(expr* objective); lbool optimize(); void set_cancel(bool f); @@ -68,12 +83,12 @@ namespace opt { private: void validate_feasibility(maxsmt& ms); - lbool execute(expr* obj, bool committed); + lbool execute(objective const& obj, bool committed); lbool execute_min_max(app* obj, bool committed, bool is_max); - lbool execute_maxsat(app* obj, bool committed); - lbool execute_lex(app* obj); - lbool execute_box(app* obj); - lbool execute_pareto(app* obj); + lbool execute_maxsat(symbol const& s, bool committed); + lbool execute_lex(); + lbool execute_box(); + lbool execute_pareto(); void push(); void pop(unsigned sz); diff --git a/src/opt/opt_params.pyg b/src/opt/opt_params.pyg index 4da07f305..40ff00a89 100644 --- a/src/opt/opt_params.pyg +++ b/src/opt/opt_params.pyg @@ -4,7 +4,7 @@ def_module_params('opt', params=(('timeout', UINT, UINT_MAX, 'set timeout'), ('engine', SYMBOL, 'basic', "select optimization engine: 'basic', 'farkas', 'symba'"), ('maxsat_engine', SYMBOL, 'fu_malik', "select engine for non-weighted maxsat: 'fu_malik', 'core_maxsat'"), - ('pareto', BOOL, False, 'return a Pareto front (as opposed to a bounding box)'), + ('priority', SYMBOL, 'lex', "select how to priortize objectives: 'lex' (lexicographic), 'pareto', or 'box'"), ('dump_benchmarks', BOOL, False, 'dump benchmarks for profiling'), ('debug_conflict', BOOL, False, 'debug conflict resolution'), ))