diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index ff49a5c8d..095c8f1f6 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -29,6 +29,9 @@ Notes: #include "optimize_objectives.h" #include "ast_pp.h" #include "opt_solver.h" +#include "arith_decl_plugin.h" +#include "th_rewriter.h" + namespace opt { @@ -74,7 +77,7 @@ namespace opt { } // SASSERT(instanceof(*s, opt_solver)); // if (!instsanceof ...) { throw ... invalid usage ..} - is_sat = optimize_objectives(dynamic_cast(*s), m_objectives, m_is_max, values); + is_sat = optimize_objectives(dynamic_cast(*s), m_objectives, values); std::cout << "is-sat: " << is_sat << "\n"; if (is_sat != l_true) { @@ -82,6 +85,9 @@ namespace opt { } for (unsigned i = 0; i < values.size(); ++i) { + if (!m_is_max[i]) { + values[i].neg(); + } std::cout << "objective function: " << mk_pp(m_objectives[i].get(), m) << " -> " << values[i].to_string() << "\n"; } } @@ -115,4 +121,18 @@ namespace opt { } } + void context::add_objective(app* t, bool is_max) { + expr_ref t1(t, m), t2(m); + th_rewriter rw(m); + if (!is_max) { + arith_util a(m); + t1 = a.mk_uminus(t); + } + rw(t1, t2); + SASSERT(is_app(t2)); + m_objectives.push_back(to_app(t2)); + m_is_max.push_back(is_max); + } + + } diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h index a08260cb1..a388bc952 100644 --- a/src/opt/opt_context.h +++ b/src/opt/opt_context.h @@ -52,10 +52,7 @@ namespace opt { m_weights.push_back(w); } - void add_objective(app* t, bool is_max) { - m_objectives.push_back(t); - m_is_max.push_back(is_max); - } + void add_objective(app* t, bool is_max); void add_hard_constraint(expr* f) { m_hard_constraints.push_back(f); diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp index 220ae0143..edeaf0441 100644 --- a/src/opt/opt_solver.cpp +++ b/src/opt/opt_solver.cpp @@ -66,12 +66,16 @@ namespace opt { TRACE("opt_solver_na2as", tout << "opt_opt_solver::check_sat_core: " << num_assumptions << "\n";); lbool r = m_context.check(num_assumptions, assumptions); if (r == l_true && m_objective_enabled) { - bool is_bounded = get_optimizer().maximize(m_objective_var); - if (is_bounded) { - m_objective_value = get_optimizer().get_objective_value(m_objective_var); - } else { - inf_eps_rational r(rational(1), inf_rational(0)); - m_objective_value = r; + m_objective_values.reset(); + for (unsigned i = 0; i < m_objective_vars.size(); ++i) { + smt::theory_var v = m_objective_vars[i]; + bool is_bounded = get_optimizer().maximize(v); + if (is_bounded) { + m_objective_values.push_back(get_optimizer().get_objective_value(v)); + } else { + inf_eps_rational r(rational(1), inf_rational(0)); + m_objective_values.push_back(r); + } } } return r; @@ -123,16 +127,27 @@ namespace opt { m_context.display(out); } - void opt_solver::set_objective(app* term) { - m_objective_var = get_optimizer().add_objective(term); + smt::theory_var opt_solver::add_objective(app* term) { + m_objective_vars.push_back(get_optimizer().add_objective(term)); + return m_objective_vars.back(); } - void opt_solver::toggle_objective(bool enable) { - m_objective_enabled = enable; + vector const& opt_solver::get_objective_values() { + return m_objective_values; } - inf_eps_rational opt_solver::get_objective_value() { - return m_objective_value; + void opt_solver::reset_objectives() { + m_objective_vars.reset(); + m_objective_values.reset(); } + opt_solver::toggle_objective::toggle_objective(opt_solver& s, bool new_value): s(s), m_old_value(s.m_objective_enabled) { + s.m_objective_enabled = new_value; + } + + opt_solver::toggle_objective::~toggle_objective() { + s.m_objective_enabled = m_old_value; + } + + } diff --git a/src/opt/opt_solver.h b/src/opt/opt_solver.h index 9b59bf93b..ce07233e3 100644 --- a/src/opt/opt_solver.h +++ b/src/opt/opt_solver.h @@ -1,21 +1,22 @@ /*++ -Copyright (c) 2012 Microsoft Corporation +Copyright (c) 2013 Microsoft Corporation Module Name: - smt_solver.h + opt_solver.h Abstract: - Wraps smt::kernel as a solver for the external API and cmd_context. + Wraps smt::kernel as a solver for optimization Author: - Leonardo (leonardo) 2012-10-21 + Anh-Dung Phan (t-anphan) 2013-10-16 Notes: + + Based directly on smt_solver. - Variant of smt_solver that exposes kernel object. --*/ #ifndef _OPT_SOLVER_H_ #define _OPT_SOLVER_H_ @@ -33,13 +34,16 @@ Notes: namespace opt { class opt_solver : public solver_na2as { + public: + typedef inf_eps_rational inf_value; + private: smt_params m_params; smt::kernel m_context; progress_callback * m_callback; symbol m_logic; bool m_objective_enabled; - smt::theory_var m_objective_var; - inf_eps_rational m_objective_value; + svector m_objective_vars; + vector m_objective_values; public: opt_solver(ast_manager & m, params_ref const & p, symbol const & l); virtual ~opt_solver(); @@ -62,10 +66,18 @@ namespace opt { virtual expr * get_assertion(unsigned idx) const; virtual void display(std::ostream & out) const; - void set_objective(app* term); - void toggle_objective(bool enable); + smt::theory_var add_objective(app* term); + void reset_objectives(); + + vector const& get_objective_values(); - inf_eps_rational get_objective_value(); + class toggle_objective { + opt_solver& s; + bool m_old_value; + public: + toggle_objective(opt_solver& s, bool new_value); + ~toggle_objective(); + }; private: smt::theory_opt& get_optimizer(); }; diff --git a/src/opt/optimize_objectives.cpp b/src/opt/optimize_objectives.cpp index e167922cc..ef247ee3c 100644 --- a/src/opt/optimize_objectives.cpp +++ b/src/opt/optimize_objectives.cpp @@ -15,6 +15,26 @@ Author: Notes: + + Suppose we obtain solution t1 = k1, ..., tn = kn-epsilon + Assert: + t1 > k1 \/ t2 > k2 \/ ... \/ tn >= kn + If this solution is satisfiable, then for each t_i, maximize the + assignment and assert the new frontier. + Claim: we don't necessarily have to freeze assignments of + t_i when optimizing assignment for t_j + because the state will always satisfy the disjunction. + If one of the k_i is unbounded, then omit a disjunction for it. + Claim: the end result (when the constraints are no longer feasible) + is Pareto optimal, but convergence will probably not be as fast + as when fixing one parameter at a time. + E.g., a different approach is first to find a global maximal for one + variable. Then add a method to "freeze" that variable at the extremum if it is finite. + To do this, add lower and upper bounds for that variable using infinitesimals. + If the variable is unbounded, then this is of course not sufficient by itself. + + + --*/ #ifndef _OPT_OBJECTIVE_H_ @@ -31,13 +51,14 @@ namespace opt { */ lbool mathsat_style_opt( opt_solver& s, - app_ref_vector& objectives, - svector const& is_max, + app_ref_vector const& objectives, vector >& values) { - SASSERT(is_max.size() == objectives.size()); + ast_manager& m = objectives.get_manager(); + arith_util autil(m); - // First check_sat call for initialize theories + s.reset_objectives(); + // First check_sat call to initialize theories lbool is_sat = s.check_sat(0, 0); if (is_sat == l_false) { return is_sat; @@ -45,38 +66,41 @@ namespace opt { s.push(); - // Temporarily ignore the assertion to run the first objective function - //SASSERT(is_max.size() == 1); - ast_manager& m = objectives.get_manager(); - arith_util autil(m); - bool ismax = is_max[0]; - app_ref objective_var(m), objective_term(m), obj_eq(m); - objective_term = ismax?objectives[0].get():autil.mk_uminus(objectives[0].get()); - sort* srt = m.get_sort(objective_term); - objective_var = m.mk_fresh_const("objective", srt); - obj_eq = autil.mk_eq(objective_var, objective_term); - s.assert_expr(obj_eq); - s.set_objective(objective_var); // NSB review: I would change signature of set_objective to take is_max and decide whether to add equation. - // Otherwise, the difference logic backends will not work. - s.toggle_objective(true); + opt_solver::toggle_objective _t(s, true); + + for (unsigned i = 0; i < objectives.size(); ++i) { + s.add_objective(objectives[i]); + } + is_sat = s.check_sat(0, 0); while (is_sat == l_true) { // Extract values for objectives - inf_eps_rational val; - val = ismax ? s.get_objective_value() : -s.get_objective_value(); - - // Check whether objective is unbounded - values.reset(); - values.push_back(val); + values.append(s.get_objective_values()); + IF_VERBOSE(1, + for (unsigned i = 0; i < values.size(); ++i) { + verbose_stream() << values[i] << " "; + } + verbose_stream() << "\n";); + expr_ref_vector disj(m); + expr_ref constraint(m), num(m); + for (unsigned i = 0; i < objectives.size(); ++i) { - if (!val.get_infinity().is_zero()) { - break; + if (!values[i].get_infinity().is_zero()) { + continue; + } + num = autil.mk_numeral(values[i].get_rational(), m.get_sort(objectives[i])); + + SASSERT(values[i].get_infinitesimal().is_nonpos()); + if (values[i].get_infinitesimal().is_neg()) { + disj.push_back(autil.mk_ge(objectives[i], num)); + } + else { + disj.push_back(autil.mk_gt(objectives[i], num)); + } } - - expr_ref constraint(m); - constraint = autil.mk_gt(objective_term, autil.mk_numeral(val.get_rational(), srt)); + constraint = m.mk_or(disj.size(), disj.c_ptr()); s.assert_expr(constraint); is_sat = s.check_sat(0, 0); } @@ -86,7 +110,6 @@ namespace opt { if (is_sat == l_undef) { return is_sat; } - //SASSERT(is_sat == l_false); // NSB review: not really water-tight with cancellation and with infinitesimal solutions. return l_true; } @@ -96,9 +119,9 @@ namespace opt { */ lbool optimize_objectives(opt_solver& s, - app_ref_vector& objectives, svector const& is_max, + app_ref_vector& objectives, vector >& values) { - return mathsat_style_opt(s, objectives, is_max, values); + return mathsat_style_opt(s, objectives, values); } } diff --git a/src/opt/optimize_objectives.h b/src/opt/optimize_objectives.h index fcf388fc9..f2ce5baca 100644 --- a/src/opt/optimize_objectives.h +++ b/src/opt/optimize_objectives.h @@ -28,7 +28,7 @@ namespace opt { */ lbool optimize_objectives(opt_solver& s, - app_ref_vector& objectives, svector const& is_max, + app_ref_vector& objectives, vector >& values); };