diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 023b30903..01536d78e 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/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; diff --git a/src/opt/opt_cmds.cpp b/src/opt/opt_cmds.cpp index aa02eae4f..bb8bf3e73 100644 --- a/src/opt/opt_cmds.cpp +++ b/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 "( )*"; } + 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::const_iterator it = ctx.begin_assertions(); ptr_vector::const_iterator end = ctx.end_assertions(); for (; it != end; ++it) { opt.add_hard_constraint(*it); } - cancel_eh eh(opt); + cancel_eh 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(mem)/static_cast(1024*1024)); + stats.update("max memory", static_cast(max_mem)/static_cast(1024*1024)); + m_opt_ctx().collect_statistics(stats); + stats.display_smt2(ctx.regular_stream()); } }; diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index d3a034e8f..781b6582e 100644 --- a/src/opt/opt_context.cpp +++ b/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); + } + + } + } diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h index 866bdf7d3..c71b941c7 100644 --- a/src/opt/opt_context.h +++ b/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 m_is_max; ref 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; diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp index 5cde65cdb..64d8a32be 100644 --- a/src/opt/opt_solver.cpp +++ b/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" diff --git a/src/opt/optimize_objectives.cpp b/src/opt/optimize_objectives.cpp index 8ae2cd0a4..d310abba6 100644 --- a/src/opt/optimize_objectives.cpp +++ b/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& values) { + lbool optimize_objectives::operator()(opt_solver& solver, app_ref_vector& objectives, vector& values) { + s = &solver; return basic_opt(objectives, values); } diff --git a/src/opt/optimize_objectives.h b/src/opt/optimize_objectives.h index 449b39df5..bacc27b09 100644 --- a/src/opt/optimize_objectives.h +++ b/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& values); + lbool operator()(opt_solver& s, app_ref_vector& objectives, vector& values); void set_cancel(bool f);