diff --git a/src/opt/opt_cmds.cpp b/src/opt/opt_cmds.cpp index b4b6d62f2..6c0aeb3d0 100644 --- a/src/opt/opt_cmds.cpp +++ b/src/opt/opt_cmds.cpp @@ -22,18 +22,32 @@ Notes: #include "opt_context.h" +class opt_context { + cmd_context& ctx; + scoped_ptr m_opt; +public: + opt_context(cmd_context& ctx): ctx(ctx) {} + opt::context& operator()() { + if (!m_opt) { + m_opt = alloc(opt::context, ctx.m()); + } + return *m_opt; + } +}; + + class assert_weighted_cmd : public cmd { - opt::context* m_opt_ctx; + opt_context* m_opt_ctx; unsigned m_idx; - expr_ref m_formula; + 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), - m_formula(ctx.m()), + m_formula(0), m_weight(0) {} @@ -42,6 +56,9 @@ public: } virtual void reset(cmd_context & ctx) { + if (m_formula) { + ctx.m().dec_ref(m_formula); + } m_idx = 0; m_formula = 0; } @@ -68,6 +85,7 @@ public: throw cmd_exception("Invalid type for expression. Expected Boolean type."); } m_formula = t; + ctx.m().inc_ref(t); ++m_idx; } @@ -76,7 +94,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); } @@ -91,10 +109,10 @@ public: // to do the feasibility check. class min_maximize_cmd : public cmd { bool m_is_max; - opt::context* m_opt_ctx; + 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) @@ -113,7 +131,7 @@ public: 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) { @@ -127,9 +145,9 @@ public: }; 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) {} @@ -145,9 +163,9 @@ public: 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); + (*m_opt_ctx)().add_hard_constraint(*it); } - m_opt_ctx->optimize(); + (*m_opt_ctx)().optimize(); } @@ -157,7 +175,7 @@ private: }; void install_opt_cmds(cmd_context & ctx) { - opt::context* opt_ctx = alloc(opt::context, ctx.m()); + 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)); diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index b02d78466..b11078b3f 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -73,8 +73,13 @@ namespace opt { if (is_sat != l_true) { return; } + for (unsigned i = 0; i < values.size(); ++i) { - // display + if (values[i]) { + std::cout << "objective function: " << mk_pp(m_objectives[i].get(), m) << " -> " << *values[i] << "\n"; + } else { + std::cout << "objective function: " << mk_pp(m_objectives[i].get(), m) << " -> unbounded\n"; + } } } diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp index 8f041e9c2..311d90275 100644 --- a/src/opt/opt_solver.cpp +++ b/src/opt/opt_solver.cpp @@ -7,6 +7,7 @@ namespace opt { opt_solver::opt_solver(ast_manager & m, params_ref const & p, symbol const & l): solver_na2as(m), + m_manager(m), m_params(p), m_context(m, m_params), m_objective_enabled(false) { @@ -48,6 +49,7 @@ namespace opt { smt::context& ctx = m_context.get_context(); smt::theory_id arith_id = m_context.m().get_family_id("arith"); smt::theory* arith_theory = ctx.get_theory(arith_id); + if (typeid(smt::theory_mi_arith) == typeid(*arith_theory)) { return dynamic_cast(*arith_theory); } @@ -64,8 +66,14 @@ namespace opt { lbool opt_solver::check_sat_core(unsigned num_assumptions, expr * const * assumptions) { TRACE("opt_solver_na2as", tout << "smt_opt_solver::check_sat_core: " << num_assumptions << "\n";); lbool r = m_context.check(num_assumptions, assumptions); - if (r == l_true &&& m_objective_enabled) { - VERIFY(get_optimizer().max_min(m_objective_var, false)); + if (r == l_true && m_objective_enabled) { + bool is_bounded = get_optimizer().max(m_objective_var); + if (is_bounded) { + m_objective_value = get_optimizer().get_objective_value(m_objective_var); + } else { + optional r; + m_objective_value = r; + } } return r; } @@ -123,4 +131,9 @@ namespace opt { void opt_solver::toggle_objective(bool enable) { m_objective_enabled = enable; } + + optional opt_solver::get_objective_value() { + return m_objective_value; + } + } diff --git a/src/opt/opt_solver.h b/src/opt/opt_solver.h index c9fd48ed2..0c8147f03 100644 --- a/src/opt/opt_solver.h +++ b/src/opt/opt_solver.h @@ -37,6 +37,8 @@ namespace opt { symbol m_logic; bool m_objective_enabled; smt::theory_var m_objective_var; + ast_manager& m_manager; + optional m_objective_value; public: opt_solver(ast_manager & m, params_ref const & p, symbol const & l); virtual ~opt_solver(); @@ -61,6 +63,8 @@ namespace opt { void set_objective(app* term); void toggle_objective(bool enable); + + optional get_objective_value(); private: smt::theory_opt& get_optimizer(); }; diff --git a/src/opt/optimize_objectives.cpp b/src/opt/optimize_objectives.cpp index 0d865d7f9..81d71e507 100644 --- a/src/opt/optimize_objectives.cpp +++ b/src/opt/optimize_objectives.cpp @@ -22,6 +22,7 @@ Notes: #include "optimize_objectives.h" #include "opt_solver.h" +#include "arith_decl_plugin.h" namespace opt { @@ -31,23 +32,47 @@ namespace opt { lbool mathsat_style_opt(opt_solver& s, expr_ref_vector& objectives, svector const& is_max, vector >& values) { - lbool is_sat; - is_sat = s.check_sat(0,0); - if (is_sat != l_true) { - return is_sat; + enable_trace("maximize"); + // First check_sat call for initialize theories + lbool is_sat = s.check_sat(0, 0); + if (is_sat == l_false) { + return l_false; } - // assume that s is instrumented to produce locally optimal assignments. + // Assume there is only one objective function + ast_manager& m = objectives.get_manager(); + arith_util autil(m); + app* objective = is_max[0] ? (app*) objectives[0].get() : autil.mk_uminus(objectives[0].get()); + s.set_objective(objective); + s.toggle_objective(true); + is_sat = s.check_sat(0, 0); + while (is_sat != l_false) { - model_ref model; - s.get_model(model); - // extract values for objectives. - // store them in values. - // assert there must be something better. - is_sat = s.check_sat(0,0); - } - return l_true; + // Extract values for objectives. + optional rat; + rat = s.get_objective_value(); + // Unbounded objective + if (!rat) { + values.reset(); + values.push_back(rat); + return l_true; + } + + // If values have initial data, they will be dropped. + values.reset(); + values.push_back(rat); + + // Assert there must be something better. + expr_ref_vector assumptions(m); + expr* bound = m.mk_fresh_const("bound", m.mk_bool_sort()); + assumptions.push_back(bound); + expr* r = autil.mk_numeral(*rat, false); + s.assert_expr(m.mk_eq(bound, is_max[0] ? autil.mk_gt(objectives[0].get(), r) : autil.mk_lt(objectives[0].get(), r))); + is_sat = s.check_sat(1, assumptions.c_ptr()); + } + + return l_true; } /** diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h index f007492a7..0f5f33756 100644 --- a/src/smt/theory_arith.h +++ b/src/smt/theory_arith.h @@ -855,6 +855,7 @@ namespace smt { theory_var pick_var_to_leave(theory_var x_j, bool inc, numeral & a_ij, inf_numeral & gain); template void add_tmp_row_entry(row & r, numeral const & coeff, theory_var v); + bool max_min(theory_var v, bool max); bool max_min(row & r, bool max); bool max_min(svector const & vars); @@ -991,8 +992,10 @@ namespace smt { // Optimization // // ----------------------------------- - virtual bool max_min(theory_var v, bool max); + virtual bool max(theory_var v) { return max_min(v, true); } virtual theory_var add_objective(app* term); + virtual optional get_objective_value(theory_var v); + inf_rational m_objective; // ----------------------------------- // diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h index 12658a979..87624acb6 100644 --- a/src/smt/theory_arith_aux.h +++ b/src/smt/theory_arith_aux.h @@ -956,7 +956,16 @@ namespace smt { template theory_var theory_arith::add_objective(app* term) { - return internalize_term(term); + return internalize_term_core(term); + } + + template + optional theory_arith::get_objective_value(theory_var v) { + optional rat; + if (m_objective.is_rational()) { + rat = m_objective.get_rational(); + }; + return rat; } /** @@ -1106,7 +1115,7 @@ namespace smt { \brief Maximize/Minimize the given variable. The bounds of v are update if procedure succeeds. */ template - bool theory_arith::max_min(theory_var v, bool max) { + bool theory_arith::max_min(theory_var v, bool max) { TRACE("maximize", tout << (max ? "maximizing" : "minimizing") << " v" << v << "...\n";); SASSERT(valid_row_assignment()); SASSERT(satisfy_bounds()); @@ -1130,7 +1139,10 @@ namespace smt { TRACE("maximize", tout << "v" << v << " " << (max ? "max" : "min") << " value is: " << get_value(v) << "\n"; display_row(tout, m_tmp_row, true); display_row_info(tout, m_tmp_row);); + m_objective = get_value(v); + mk_bound_from_row(v, get_value(v), max ? B_UPPER : B_LOWER, m_tmp_row); + return true; } return false; diff --git a/src/smt/theory_opt.h b/src/smt/theory_opt.h index f0759e9fc..4f742f73b 100644 --- a/src/smt/theory_opt.h +++ b/src/smt/theory_opt.h @@ -24,8 +24,9 @@ Notes: namespace smt { class theory_opt { public: - virtual bool max_min(theory_var v, bool max) { UNREACHABLE(); return false; }; + virtual bool max(theory_var v) { UNREACHABLE(); return false; }; virtual theory_var add_objective(app* term) { UNREACHABLE(); return null_theory_var; } + virtual optional get_objective_value(theory_var v) { UNREACHABLE(); optional r; return r;} }; }