From 3996f58a8e1d9ed62db9e91b6f6a56eacce3c8bd Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 19 Oct 2013 12:22:56 -0700 Subject: [PATCH] tidy & todo notes Signed-off-by: Nikolaj Bjorner --- src/opt/fu_malik.cpp | 6 +-- src/opt/fu_malik.h | 2 +- src/opt/opt_cmds.cpp | 85 ++++++++++++++++++++++++----------------- src/opt/opt_context.cpp | 19 +++++++++ src/opt/opt_context.h | 14 ++++++- src/smt/theory_opt.h | 4 +- 6 files changed, 86 insertions(+), 44 deletions(-) diff --git a/src/opt/fu_malik.cpp b/src/opt/fu_malik.cpp index f242c1a37..07d256d9e 100644 --- a/src/opt/fu_malik.cpp +++ b/src/opt/fu_malik.cpp @@ -37,13 +37,13 @@ namespace opt { class fu_malik { ast_manager& m; - ::solver& s; + solver& s; expr_ref_vector m_soft; expr_ref_vector m_aux; public: - fu_malik(ast_manager& m, ::solver& s, expr_ref_vector const& soft): + fu_malik(ast_manager& m, solver& s, expr_ref_vector const& soft): m(m), s(s), m_soft(soft), @@ -132,7 +132,7 @@ namespace opt { }; - lbool fu_malik_maxsat(::solver& s, expr_ref_vector& soft_constraints) { + lbool fu_malik_maxsat(solver& s, expr_ref_vector& soft_constraints) { ast_manager& m = soft_constraints.get_manager(); lbool is_sat = s.check_sat(0,0); if (!soft_constraints.empty() && is_sat == l_true) { diff --git a/src/opt/fu_malik.h b/src/opt/fu_malik.h index e46032adf..6bfe37f63 100644 --- a/src/opt/fu_malik.h +++ b/src/opt/fu_malik.h @@ -28,7 +28,7 @@ namespace opt { that are still consistent with the solver state. */ - lbool fu_malik_maxsat(::solver& s, expr_ref_vector& soft_constraints); + lbool fu_malik_maxsat(solver& s, expr_ref_vector& soft_constraints); }; #endif diff --git a/src/opt/opt_cmds.cpp b/src/opt/opt_cmds.cpp index 6c0aeb3d0..58a404328 100644 --- a/src/opt/opt_cmds.cpp +++ b/src/opt/opt_cmds.cpp @@ -14,12 +14,26 @@ 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 + + - Deal with push/pop (later) + + - Revisit weighted constraints if we want to group them using identifiers. + --*/ #include "opt_cmds.h" #include "cmd_context.h" #include "ast_pp.h" - #include "opt_context.h" +#include "cancel_eh.h" +#include "scoped_ctrl_c.h" class opt_context { @@ -37,13 +51,13 @@ public: class assert_weighted_cmd : public cmd { - opt_context* m_opt_ctx; - unsigned m_idx; - expr* m_formula; - rational m_weight; + opt_context& m_opt_ctx; + unsigned m_idx; + expr* 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), @@ -52,7 +66,7 @@ public: {} virtual ~assert_weighted_cmd() { - dealloc(m_opt_ctx); + dealloc(&m_opt_ctx); } virtual void reset(cmd_context & ctx) { @@ -94,7 +108,7 @@ public: } virtual void execute(cmd_context & ctx) { - (*m_opt_ctx)().add_soft_constraint(m_formula, m_weight); + m_opt_ctx().add_soft_constraint(m_formula, m_weight); reset(ctx); } @@ -103,23 +117,18 @@ public: }; -// what amounts to check-sat, but uses the *single* objective function. -// alternative is to register multiple objective functions using -// minimize/maximize and then use check-sat or some variant of it -// to do the feasibility check. class min_maximize_cmd : public cmd { - bool m_is_max; - opt_context* m_opt_ctx; + bool m_is_max; + 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_opt_ctx(opt_ctx) {} - virtual void reset(cmd_context & ctx) { - } + virtual void reset(cmd_context & ctx) { } virtual char const * get_usage() const { return ""; } virtual char const * get_descr(cmd_context & ctx) const { return "check sat modulo objective function";} @@ -129,9 +138,7 @@ 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) { - // 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); + m_opt_ctx().add_objective(t, m_is_max); } virtual void failure_cleanup(cmd_context & ctx) { @@ -140,14 +147,12 @@ public: virtual void execute(cmd_context & ctx) { } - - }; class optimize_cmd : public cmd { - opt_context* m_opt_ctx; + opt_context& m_opt_ctx; public: - optimize_cmd(opt_context* opt_ctx): + optimize_cmd(opt_context& opt_ctx): cmd("optimize"), m_opt_ctx(opt_ctx) {} @@ -159,25 +164,33 @@ public: } virtual void execute(cmd_context & ctx) { - + opt::context& opt = m_opt_ctx(); ptr_vector::const_iterator it = ctx.begin_assertions(); ptr_vector::const_iterator end = ctx.end_assertions(); for (; it != end; ++it) { - (*m_opt_ctx)().add_hard_constraint(*it); + opt.add_hard_constraint(*it); + } + cancel_eh eh(opt); + { + scoped_ctrl_c ctrlc(eh); + cmd_context::scoped_watch sw(ctx); + try { + opt.optimize(); + } + catch (z3_error& ex) { + ctx.regular_stream() << "(error: " << ex.msg() << "\")" << std::endl; + } + catch (z3_exception& ex) { + ctx.regular_stream() << "(error: " << ex.msg() << "\")" << std::endl; + } } - (*m_opt_ctx)().optimize(); - - } -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(min_maximize_cmd, ctx, opt_ctx, true)); - ctx.insert(alloc(min_maximize_cmd, ctx, opt_ctx, false)); - ctx.insert(alloc(optimize_cmd, opt_ctx)); + 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 index ac6e7f084..45b945d73 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -14,6 +14,13 @@ Author: Notes: + TODO: + + - there are race conditions for cancelation. + - it would also be a good idea to maintain a volatile bool to track + cancelation and then bail out of loops inside optimize() and derived + functions. + --*/ #include "opt_context.h" @@ -95,4 +102,16 @@ namespace opt { return true; } + void context::cancel() { + if (m_solver) { + m_solver->cancel(); + } + } + + void context::reset_cancel() { + if (m_solver) { + m_solver->reset_cancel(); + } + } + } diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h index 9e7658625..914ee3edb 100644 --- a/src/opt/opt_context.h +++ b/src/opt/opt_context.h @@ -14,6 +14,13 @@ Author: Notes: + TODO: + + - type check objective term and assertions. It should pass basic sanity being + integer, real (, bit-vector) or other supported objective function type. + + - add appropriate statistics tracking to opt::context + --*/ #ifndef _OPT_CONTEXT_H_ #define _OPT_CONTEXT_H_ @@ -31,7 +38,7 @@ namespace opt { expr_ref_vector m_objectives; svector m_is_max; - ref<::solver> m_solver; + ref m_solver; public: context(ast_manager& m): @@ -55,12 +62,15 @@ namespace opt { m_hard_constraints.push_back(f); } - void set_solver(::solver* s) { + void set_solver(solver* s) { m_solver = s; } void optimize(); + void cancel(); + void reset_cancel(); + private: bool is_maxsat_problem() const; diff --git a/src/smt/theory_opt.h b/src/smt/theory_opt.h index 4a558a09c..c3765a1fc 100644 --- a/src/smt/theory_opt.h +++ b/src/smt/theory_opt.h @@ -28,11 +28,11 @@ namespace smt { public: virtual bool maximize(theory_var v) { UNREACHABLE(); return false; }; virtual theory_var add_objective(app* term) { UNREACHABLE(); return null_theory_var; } - virtual inf_eps_rational get_objective_value(theory_var v) { + virtual inf_eps_rational get_objective_value(theory_var v) { UNREACHABLE(); inf_eps_rational r(rational(1), rational(0)); return r; - } + } }; }