From 9fc84f13898774e24d7eff65fba60a26f09ad67d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 30 Oct 2013 13:23:04 -0700 Subject: [PATCH 1/3] adding timeout, parameters, statistics Signed-off-by: Nikolaj Bjorner --- src/cmd_context/cmd_context.cpp | 1 - src/opt/opt_cmds.cpp | 45 +++++++++++++++++++++++++++------ src/opt/opt_context.cpp | 29 ++++++++++++++++++--- src/opt/opt_context.h | 14 +++++----- 4 files changed, 69 insertions(+), 20 deletions(-) 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..01d8b833e 100644 --- a/src/opt/opt_cmds.cpp +++ b/src/opt/opt_cmds.cpp @@ -25,8 +25,6 @@ Notes: - 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 +32,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 +152,44 @@ 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 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..64905a9fa 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -35,16 +35,23 @@ Notes: namespace opt { + context::context(ast_manager& m): + m(m), + m_hard_constraints(m), + m_soft_constraints(m), + m_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(); @@ -140,5 +147,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..e2881906f 100644 --- a/src/opt/opt_context.h +++ b/src/opt/opt_context.h @@ -40,14 +40,10 @@ namespace opt { app_ref_vector m_objectives; svector m_is_max; ref m_solver; - + params_ref m_params; + 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 +65,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; From 946b888b32d79e783e9793ff8bcbd4c491f2858e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 30 Oct 2013 13:24:21 -0700 Subject: [PATCH 2/3] adding timeout, parameters, statistics Signed-off-by: Nikolaj Bjorner --- src/opt/opt_cmds.cpp | 7 +------ src/opt/opt_solver.cpp | 20 ++++++++++++++++++++ 2 files changed, 21 insertions(+), 6 deletions(-) diff --git a/src/opt/opt_cmds.cpp b/src/opt/opt_cmds.cpp index 01d8b833e..5acbec9dd 100644 --- a/src/opt/opt_cmds.cpp +++ b/src/opt/opt_cmds.cpp @@ -15,13 +15,8 @@ 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) 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" From 86151b4d520d50665a87109e9f1495aab2a4e30f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 30 Oct 2013 13:38:47 -0700 Subject: [PATCH 3/3] dealing with cancel Signed-off-by: Nikolaj Bjorner --- src/opt/opt_cmds.cpp | 7 ++++++- src/opt/opt_context.cpp | 9 +++++---- src/opt/opt_context.h | 3 ++- src/opt/optimize_objectives.cpp | 23 ++++++++++++----------- src/opt/optimize_objectives.h | 6 +++--- 5 files changed, 28 insertions(+), 20 deletions(-) diff --git a/src/opt/opt_cmds.cpp b/src/opt/opt_cmds.cpp index 5acbec9dd..bb8bf3e73 100644 --- a/src/opt/opt_cmds.cpp +++ b/src/opt/opt_cmds.cpp @@ -170,11 +170,16 @@ public: 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); + unsigned timeout = p.get_uint("timeout", UINT_MAX); ptr_vector::const_iterator it = ctx.begin_assertions(); ptr_vector::const_iterator end = ctx.end_assertions(); diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 64905a9fa..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" @@ -39,7 +38,8 @@ namespace opt { m(m), m_hard_constraints(m), m_soft_constraints(m), - m_objectives(m) + m_objectives(m), + m_opt_objectives(m) { m_params.set_bool("model", true); m_params.set_bool("unsat_core", true); @@ -83,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) { @@ -126,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) { diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h index e2881906f..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 { @@ -41,7 +42,7 @@ namespace opt { svector m_is_max; ref m_solver; params_ref m_params; - + optimize_objectives m_opt_objectives; public: context(ast_manager& m); 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);