diff --git a/src/opt/objective_ast.cpp b/src/opt/objective_ast.cpp new file mode 100644 index 000000000..79d2516d6 --- /dev/null +++ b/src/opt/objective_ast.cpp @@ -0,0 +1,54 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + objective_ast.h + +Abstract: + Abstract data-type for compound objectives. + +Author: + + Anh-Dung Phan (t-anphan) 2013-11-26 + +Notes: + +--*/ + +#include"objective_ast.h" + +namespace opt { + + objective* objective::mk_max(expr_ref& e) { return alloc(min_max_objective, MAXIMIZE, e); }; + objective* objective::mk_min(expr_ref& e) { return alloc(min_max_objective, MINIMIZE, e); }; + objective* objective::mk_maxsat(symbol id) { return alloc(maxsat_objective, id); }; + + objective* objective::mk_lex(unsigned sz, objective * const* children) { + return alloc(compound_objective, LEX, sz, children); + }; + + objective* objective::mk_box(unsigned sz, objective * const* children) { + return alloc(compound_objective, BOX, sz, children); + }; + + objective* objective::mk_pareto(unsigned sz, objective * const* children) { + return alloc(compound_objective, PARETO, sz, children); + }; + + compound_objective& objective::get_compound() { + SASSERT(m_type == LEX || m_type == BOX || m_type == PARETO); + return dynamic_cast(*this); + } + + min_max_objective& objective::get_min_max() { + SASSERT(m_type == MAXIMIZE || m_type == MINIMIZE); + return dynamic_cast(*this); + } + + maxsat_objective& objective::get_maxsat() { + SASSERT(m_type == MAXSAT); + return dynamic_cast(*this); + } + +}; diff --git a/src/opt/objective_ast.h b/src/opt/objective_ast.h index b1005b40d..31a2bf543 100644 --- a/src/opt/objective_ast.h +++ b/src/opt/objective_ast.h @@ -18,6 +18,8 @@ Notes: #ifndef __OBJECTIVE_AST_H_ #define __OBJECTIVE_AST_H_ +#include"ast.h" + namespace opt { enum objective_t { @@ -46,35 +48,45 @@ namespace opt { // constructors; static objective* mk_max(expr_ref& e); static objective* mk_min(expr_ref& e); + static objective* mk_maxsat(symbol id); + static objective* mk_lex(unsigned sz, objective * const* children); static objective* mk_box(unsigned sz, objective * const* children); static objective* mk_pareto(unsigned sz, objective * const* children); - static objective* mk_maxsat(symbol id); // accessors (implicit cast operations) - compound_objective& get_compound(); // eg. SASSERT(m_type == LEX/BOX/PARETO); return dynamic_cast(*this); - min_max_objective& get_min_max(); - maxsat_objective& get_maxsat(); + compound_objective& get_compound(); + min_max_objective& get_min_max(); + maxsat_objective& get_maxsat(); }; class compound_objective : public objective { ptr_vector m_children; public: - compound_objective(objective_t t): objective(t) {} + compound_objective(objective_t t, unsigned sz, objective * const* children): + objective(t), + m_children(sz, children) {} + virtual ~compound_objective() { - // dealloc vector m_children; + ptr_vector::iterator it = m_children.begin(), end = m_children.end(); + for (; it != end; ++it) { + dealloc(*it); + } } objective *const* children() const { return m_children.c_ptr(); } unsigned num_children() const { return m_children.size(); } - } + }; class min_max_objective : public objective { bool m_is_max; expr_ref m_expr; public: - min_max_objective(bool is_max, expr_ref& e): m_is_max(is_max), m_expr(e) {} + min_max_objective(bool is_max, expr_ref& e): + objective(is_max ? MAXIMIZE : MINIMIZE), + m_is_max(is_max), + m_expr(e) {} virtual ~min_max_objective() {} @@ -85,7 +97,7 @@ namespace opt { class maxsat_objective : public objective { symbol m_id; public: - maxsat_objective(symbol const& id): m_id(id) {} + maxsat_objective(symbol const& id): objective(MAXSAT), m_id(id) {} virtual ~maxsat_objective() {} symbol const& get_id() const { return m_id; } diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 6afc7779e..17d829ab9 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -27,7 +27,8 @@ namespace opt { context::context(ast_manager& m): m(m), m_hard_constraints(m), - m_optsmt(m) + m_optsmt(m), + m_objs(m) { m_params.set_bool("model", true); m_params.set_bool("unsat_core", true); @@ -50,57 +51,98 @@ namespace opt { ms->add(f, w); } - lbool context::optimize() { - if (m_params.get_bool("pareto", false)) { - return optimize_pareto(); - } - else { - return optimize_box(); + lbool context::execute(objective & obj, bool committed) { + switch (obj.type()) { + case MINIMIZE: + case MAXIMIZE: + return execute_min_max(obj.get_min_max(), committed); + case MAXSAT: + return execute_maxsat(obj.get_maxsat(), committed); + case LEX: + return execute_lex(obj.get_compound()); + case BOX: + return execute_box(obj.get_compound()); + case PARETO: + return execute_pareto(obj.get_compound()); + default: + UNREACHABLE(); + return l_undef; } } - lbool context::optimize_box() { + lbool context::execute_min_max(min_max_objective & obj, bool committed) { + // HACK: reuse m_optsmt but add only a single objective each round + m_optsmt.add(to_app(obj.term()), obj.is_max()); + opt_solver& s = *m_solver.get(); + lbool result = m_optsmt(s); + if (committed) m_optsmt.commit_assignment(0); + return result; + } + + lbool context::execute_maxsat(maxsat_objective & obj, bool committed) { + maxsmt* ms; + SASSERT(m_maxsmts.find(obj.get_id(), ms)); + opt_solver& s = *m_solver.get(); + lbool result = (*ms)(s); + if (committed) ms->commit_assignment(); + return result; + } + + lbool context::execute_lex(compound_objective & obj) { + ptr_vector children(obj.num_children(), obj.children()); + for (unsigned i = 0; i < children.size(); ++i) { + lbool result = execute(*children[i], true); + if (result != l_true) return result; + } + return l_true; + } + + lbool context::execute_box(compound_objective & obj) { + ptr_vector children(obj.num_children(), obj.children()); + for (unsigned i = 0; i < children.size(); ++i) { + lbool result = execute(*children[i], false); + if (result != l_true) return result; + } + return l_true; + } + + lbool context::execute_pareto(compound_objective & obj) { + // TODO: record a stream of results from pareto front + return execute_lex(obj); + } + + lbool context::optimize() { + // Construct objectives + ptr_vector objectives; + map_t::iterator it = m_maxsmts.begin(), end = m_maxsmts.end(); + for (; it != end; ++it) { + objectives.push_back(objective::mk_maxsat(it->m_key)); + } + + for (unsigned i = 0; i < m_objs.size(); ++i) { + expr_ref e(m_objs[i].get(), m); + objective * o = m_ismaxs[i] ? objective::mk_max(e) : objective::mk_min(e); + objectives.push_back(o); + } + + objective * objective; + if (m_params.get_bool("pareto", false)) { + objective = objective::mk_pareto(objectives.size(), objectives.c_ptr()); + } + else { + objective = objective::mk_box(objectives.size(), objectives.c_ptr()); + } + opt_solver& s = *m_solver.get(); solver::scoped_push _sp(s); for (unsigned i = 0; i < m_hard_constraints.size(); ++i) { s.assert_expr(m_hard_constraints[i].get()); } - - lbool is_sat = l_true; - map_t::iterator it = m_maxsmts.begin(), end = m_maxsmts.end(); - for (; is_sat == l_true && it != end; ++it) { - maxsmt& ms = *it->m_value; - is_sat = ms(s); - } - if (is_sat == l_true) { - is_sat = m_optsmt(s); - } - return is_sat; - } - // finds a random pareto front. - // enumerating more is TBD, e.g., - lbool context::optimize_pareto() { - opt_solver& s = *m_solver.get(); - opt_solver::scoped_push _sp(s); - - for (unsigned i = 0; i < m_hard_constraints.size(); ++i) { - s.assert_expr(m_hard_constraints[i].get()); - } - - lbool is_sat = l_true; - map_t::iterator it = m_maxsmts.begin(), end = m_maxsmts.end(); - for (; is_sat == l_true && it != end; ++it) { - maxsmt* ms = it->m_value; - is_sat = (*ms)(s); - ms->commit_assignment(); - } - for (unsigned i = 0; is_sat == l_true && i < m_optsmt.get_num_objectives(); ++i) { - is_sat = m_optsmt(s); - m_optsmt.commit_assignment(i); - } - return is_sat; + lbool result = execute(*objective, false); + dealloc(objective); + return result; } void context::display_assignment(std::ostream& out) { diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h index 081bf7c1d..14ef2df0b 100644 --- a/src/opt/opt_context.h +++ b/src/opt/opt_context.h @@ -29,6 +29,7 @@ Notes: #include "opt_solver.h" #include "optsmt.h" #include "maxsmt.h" +#include "objective_ast.h" namespace opt { @@ -42,12 +43,22 @@ namespace opt { params_ref m_params; optsmt m_optsmt; map_t m_maxsmts; + expr_ref_vector m_objs; + svector m_ismaxs; public: context(ast_manager& m); ~context(); void add_soft_constraint(expr* f, rational const& w, symbol const& id); - void add_objective(app* t, bool is_max) { m_optsmt.add(t, is_max); } + void add_objective(app* t, bool is_max) { m_objs.push_back(t); m_ismaxs.push_back(is_max); } void add_hard_constraint(expr* f) { m_hard_constraints.push_back(f); } + + lbool execute(objective & obj, bool committed); + lbool execute_min_max(min_max_objective & obj, bool committed); + lbool execute_maxsat(maxsat_objective & obj, bool committed); + lbool execute_lex(compound_objective & obj); + lbool execute_box(compound_objective & obj); + lbool execute_pareto(compound_objective & obj); + lbool optimize(); void set_cancel(bool f); void reset_cancel() { set_cancel(false); } @@ -58,9 +69,6 @@ namespace opt { static void collect_param_descrs(param_descrs & r); void updt_params(params_ref& p); private: - lbool optimize_pareto(); - lbool optimize_box(); - void validate_feasibility(maxsmt& ms); }; diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp index b6a39a949..091adb9b0 100644 --- a/src/opt/opt_solver.cpp +++ b/src/opt/opt_solver.cpp @@ -56,7 +56,7 @@ namespace opt { } void opt_solver::collect_statistics(statistics & st) const { - // Hack to display fu_malik statistics + // HACK: display fu_malik statistics if (m_stats.size() > 0) { st.copy(m_stats); }