From 9fc84f13898774e24d7eff65fba60a26f09ad67d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 30 Oct 2013 13:23:04 -0700 Subject: [PATCH] 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;