From 3dd72f8f16adbea0b23cebb8779985cbc4b05b1d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 19 Oct 2013 17:43:59 -0700 Subject: [PATCH] more updates Signed-off-by: Nikolaj Bjorner --- src/opt/opt_cmds.cpp | 5 ++- src/opt/opt_context.h | 11 +++-- src/opt/optimize_objectives.cpp | 76 +++++++++++++++++++-------------- src/opt/optimize_objectives.h | 4 +- 4 files changed, 54 insertions(+), 42 deletions(-) diff --git a/src/opt/opt_cmds.cpp b/src/opt/opt_cmds.cpp index 58a404328..aa02eae4f 100644 --- a/src/opt/opt_cmds.cpp +++ b/src/opt/opt_cmds.cpp @@ -138,7 +138,10 @@ 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) { - m_opt_ctx().add_objective(t, m_is_max); + if (!is_app(t)) { + throw cmd_exception("malformed objective term: it cannot be a quantifier or bound variable"); + } + m_opt_ctx().add_objective(to_app(t), m_is_max); } virtual void failure_cleanup(cmd_context & ctx) { diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h index 914ee3edb..a08260cb1 100644 --- a/src/opt/opt_context.h +++ b/src/opt/opt_context.h @@ -32,13 +32,12 @@ namespace opt { class context { ast_manager& m; - expr_ref_vector m_hard_constraints; + expr_ref_vector m_hard_constraints; expr_ref_vector m_soft_constraints; vector m_weights; - - expr_ref_vector m_objectives; - svector m_is_max; - ref m_solver; + app_ref_vector m_objectives; + svector m_is_max; + ref m_solver; public: context(ast_manager& m): @@ -53,7 +52,7 @@ namespace opt { m_weights.push_back(w); } - void add_objective(expr* t, bool is_max) { + void add_objective(app* t, bool is_max) { m_objectives.push_back(t); m_is_max.push_back(is_max); } diff --git a/src/opt/optimize_objectives.cpp b/src/opt/optimize_objectives.cpp index 8dc942c32..f7bcb362c 100644 --- a/src/opt/optimize_objectives.cpp +++ b/src/opt/optimize_objectives.cpp @@ -29,58 +29,68 @@ namespace opt { /* Enumerate locally optimal assignments until fixedpoint. */ - lbool mathsat_style_opt(opt_solver& s, - expr_ref_vector& objectives, svector const& is_max, - vector >& values) { - enable_trace("maximize"); + lbool mathsat_style_opt( + opt_solver& s, + app_ref_vector& objectives, + svector const& is_max, + vector >& values) + { + SASSERT(is_max.size() == objectives.size()); + + enable_trace("maximize"); // NSB review: OK for now for debugging. Otherwise, use command-line /tr:maximize + // First check_sat call for initialize theories lbool is_sat = s.check_sat(0, 0); - if (is_sat == l_false) { - return l_false; + if (is_sat != l_false) { + return is_sat; } s.push(); + // Assume there is only one objective function + SASSERT(is_max.size() == 1); ast_manager& m = objectives.get_manager(); arith_util autil(m); - app* objective = m.mk_fresh_const("objective", autil.mk_real()); - if (is_max[0]) { - s.assert_expr(autil.mk_eq(objective, objectives[0].get())); - } else { - s.assert_expr(autil.mk_eq(objective, autil.mk_uminus(objectives[0].get()))); - }; - s.set_objective(objective); + 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); is_sat = s.check_sat(0, 0); - - while (is_sat != l_false) { + + while (is_sat == l_true) { // Extract values for objectives inf_eps_rational val; - val = is_max[0] ? s.get_objective_value() : -s.get_objective_value(); + val = is_max[0] ? s.get_objective_value() : -s.get_objective_value(); // Check whether objective is unbounded - if (!val.is_rational()) { - values.reset(); - values.push_back(val); - break; - } - - // If values have initial data, they will be dropped + // NSB: review: what if optimal is 1-epsilon. Then the check also fails. + values.reset(); values.push_back(val); - - // 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(val.get_rational(), 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()); + + if (!val.is_rational()) { + break; + } + + expr_ref constraint(m); + constraint = autil.mk_gt(objective_term, autil.mk_numeral(val.get_rational(), srt)); + s.assert_expr(constraint); + is_sat = s.check_sat(0, 0); } s.pop(1); - + + 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; } @@ -90,7 +100,7 @@ namespace opt { */ lbool optimize_objectives(opt_solver& s, - expr_ref_vector& objectives, svector const& is_max, + app_ref_vector& objectives, svector const& is_max, vector >& values) { return mathsat_style_opt(s, objectives, is_max, values); } diff --git a/src/opt/optimize_objectives.h b/src/opt/optimize_objectives.h index aa02a992e..94a6f591a 100644 --- a/src/opt/optimize_objectives.h +++ b/src/opt/optimize_objectives.h @@ -28,8 +28,8 @@ namespace opt { */ lbool optimize_objectives(opt_solver& s, - expr_ref_vector& objectives, svector const& is_max, - vector >& values); + app_ref_vector& objectives, svector const& is_max, + vector >& values); }; #endif