From 6e1c18601746227da98ed102ccf700c3a268a52c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 8 Nov 2013 20:55:01 -0800 Subject: [PATCH] enable answer generation Signed-off-by: Nikolaj Bjorner --- src/opt/fu_malik.cpp | 18 ++++++----- src/opt/maxsmt.cpp | 12 ++++---- src/opt/maxsmt.h | 1 - src/opt/opt_cmds.cpp | 16 +++++++++- src/opt/opt_context.cpp | 64 ++++++++++++++++++++++++++++++++++----- src/opt/opt_context.h | 8 +++-- src/opt/optsmt.cpp | 39 ++++++++++++++++-------- src/opt/optsmt.h | 9 ++++-- src/opt/weighted_maxsat.h | 12 ++++---- 9 files changed, 131 insertions(+), 48 deletions(-) diff --git a/src/opt/fu_malik.cpp b/src/opt/fu_malik.cpp index fe4cdb1f7..6bfe1d5cc 100644 --- a/src/opt/fu_malik.cpp +++ b/src/opt/fu_malik.cpp @@ -39,14 +39,17 @@ namespace opt { ast_manager& m; solver& s; expr_ref_vector m_soft; + expr_ref_vector m_orig_soft; expr_ref_vector m_aux; expr_ref_vector m_assignment; + unsigned m_upper_size; imp(ast_manager& m, solver& s, expr_ref_vector const& soft): m(m), s(s), m_soft(soft), + m_orig_soft(soft), m_aux(m), m_assignment(m) { @@ -54,6 +57,7 @@ namespace opt { m_aux.push_back(m.mk_fresh_const("p", m.mk_bool_sort())); s.assert_expr(m.mk_or(m_soft[i].get(), m_aux[i].get())); } + m_upper_size = m_soft.size() + 1; } @@ -136,9 +140,10 @@ namespace opt { if (!m_soft.empty() && is_sat == l_true) { opt_solver::scoped_push _sp(s); - lbool is_sat = l_true; + lbool is_sat = l_true; do { is_sat = step(); + --m_upper_size; } while (is_sat == l_false); @@ -148,11 +153,11 @@ namespace opt { s.get_model(model); m_assignment.reset(); - for (unsigned i = 0; i < m_soft.size(); ++i) { + for (unsigned i = 0; i < m_orig_soft.size(); ++i) { expr_ref val(m); - VERIFY(model->eval(m_soft[i].get(), val)); + VERIFY(model->eval(m_orig_soft[i].get(), val)); if (m.is_true(val)) { - m_assignment.push_back(m_soft[i].get()); + m_assignment.push_back(m_orig_soft[i].get()); } } } @@ -175,15 +180,12 @@ namespace opt { return (*m_imp)(); } rational fu_malik::get_lower() const { - NOT_IMPLEMENTED_YET(); return rational(0); } rational fu_malik::get_upper() const { - NOT_IMPLEMENTED_YET(); - return rational(m_imp->m_soft.size()); + return rational(m_imp->m_upper_size); } rational fu_malik::get_value() const { - NOT_IMPLEMENTED_YET(); return rational(m_imp->m_assignment.size()); } expr_ref_vector fu_malik::get_assignment() const { diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp index f68e4a50b..1625b6440 100644 --- a/src/opt/maxsmt.cpp +++ b/src/opt/maxsmt.cpp @@ -28,7 +28,7 @@ namespace opt { lbool is_sat; m_answer.reset(); m_msolver = 0; - if (m_answer.empty()) { + if (m_soft_constraints.empty()) { m_msolver = 0; is_sat = s.check_sat(0, 0); m_answer.append(m_soft_constraints); @@ -46,11 +46,11 @@ namespace opt { } // Infrastructure for displaying and storing solution is TBD. - std::cout << "is-sat: " << is_sat << "\n"; - if (is_sat == l_true) { - std::cout << "Satisfying soft constraints\n"; - display_answer(std::cout); - } + IF_VERBOSE(1, verbose_stream() << "is-sat: " << is_sat << "\n"; + if (is_sat == l_true) { + verbose_stream() << "Satisfying soft constraints\n"; + display_answer(verbose_stream()); + }); return is_sat; } diff --git a/src/opt/maxsmt.h b/src/opt/maxsmt.h index b23d8811e..3d67ee7eb 100644 --- a/src/opt/maxsmt.h +++ b/src/opt/maxsmt.h @@ -62,7 +62,6 @@ namespace opt { } void commit_assignment(); - inf_eps get_value() const; inf_eps get_lower() const; inf_eps get_upper() const; diff --git a/src/opt/opt_cmds.cpp b/src/opt/opt_cmds.cpp index ad5985d1c..35652918b 100644 --- a/src/opt/opt_cmds.cpp +++ b/src/opt/opt_cmds.cpp @@ -201,13 +201,14 @@ public: for (; it != end; ++it) { opt.add_hard_constraint(*it); } + lbool r = l_undef; cancel_eh eh(opt); { scoped_ctrl_c ctrlc(eh); scoped_timer timer(timeout, &eh); cmd_context::scoped_watch sw(ctx); try { - opt.optimize(); + r = opt.optimize(); } catch (z3_error& ex) { ctx.regular_stream() << "(error: " << ex.msg() << "\")" << std::endl; @@ -216,6 +217,19 @@ public: ctx.regular_stream() << "(error: " << ex.msg() << "\")" << std::endl; } } + switch(r) { + case l_true: + ctx.regular_stream() << "sat\n"; + opt.display_assignment(ctx.regular_stream()); + break; + case l_false: + ctx.regular_stream() << "unsat\n"; + break; + case l_undef: + ctx.regular_stream() << "unknown\n"; + opt.display_range_assignment(ctx.regular_stream()); + break; + } if (p.get_bool("print_statistics", false)) { display_statistics(ctx); } diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index ede93b34a..7808a3d0c 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -6,6 +6,7 @@ Module Name: opt_context.cpp Abstract: + Facility for running optimization problem. Author: @@ -14,17 +15,11 @@ Author: Notes: - TODO: - - - there are race conditions for cancelation. - --*/ #include "opt_context.h" #include "ast_pp.h" #include "opt_solver.h" -#include "arith_decl_plugin.h" -#include "th_rewriter.h" #include "opt_params.hpp" namespace opt { @@ -55,8 +50,12 @@ namespace opt { ms->add(f, w); } - void context::optimize() { + lbool context::optimize() { + // TBD: add configurtion parameter + return optimize_box(); + } + lbool context::optimize_box() { opt_solver& s = *m_solver.get(); opt_solver::scoped_push _sp(s); @@ -73,6 +72,55 @@ namespace opt { 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; + } + + void context::display_assignment(std::ostream& out) { + map_t::iterator it = m_maxsmts.begin(), end = m_maxsmts.end(); + for (; it != end; ++it) { + maxsmt* ms = it->m_value; + if (it->m_key != symbol::null) { + out << it->m_key << " : "; + } + out << ms->get_value() << "\n"; + } + m_optsmt.display_assignment(out); + } + + void context::display_range_assignment(std::ostream& out) { + map_t::iterator it = m_maxsmts.begin(), end = m_maxsmts.end(); + for (; it != end; ++it) { + maxsmt* ms = it->m_value; + if (it->m_key != symbol::null) { + out << it->m_key << " : "; + } + out << "[" << ms->get_lower() << ":" << ms->get_upper() << "]\n"; + } + m_optsmt.display_range_assignment(out); } void context::set_cancel(bool f) { @@ -86,7 +134,7 @@ namespace opt { } } - void context::collect_statistics(statistics& stats) { + void context::collect_statistics(statistics& stats) const { if (m_solver) { m_solver->collect_statistics(stats); } diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h index c9388a56a..15f59efc8 100644 --- a/src/opt/opt_context.h +++ b/src/opt/opt_context.h @@ -48,11 +48,15 @@ namespace opt { 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_hard_constraint(expr* f) { m_hard_constraints.push_back(f); } - void optimize(); + lbool optimize(); + lbool optimize_pareto(); + lbool optimize_box(); void set_cancel(bool f); void reset_cancel() { set_cancel(false); } void cancel() { set_cancel(true); } - void collect_statistics(statistics& stats); + void collect_statistics(statistics& stats) const; + void display_assignment(std::ostream& out); + void display_range_assignment(std::ostream& out); static void collect_param_descrs(param_descrs & r); void updt_params(params_ref& p); }; diff --git a/src/opt/optsmt.cpp b/src/opt/optsmt.cpp index 28dd95f67..1d3aa1f77 100644 --- a/src/opt/optsmt.cpp +++ b/src/opt/optsmt.cpp @@ -238,8 +238,8 @@ namespace opt { } } - std::cout << "is-sat: " << is_sat << std::endl; - display(std::cout); + IF_VERBOSE(1, verbose_stream() << "is-sat: " << is_sat << std::endl; + display_assignment(verbose_stream());); return is_sat; } @@ -262,22 +262,35 @@ namespace opt { s->assert_expr(s->block_upper_bound(i, get_lower(i))); } - void optsmt::display(std::ostream& out) const { + std::ostream& optsmt::display_objective(std::ostream& out, unsigned i) const { + bool is_max = m_is_max[i]; + inf_eps val = get_value(i); + expr_ref obj(m_objs[i], m); + if (!is_max) { + arith_util a(m); + th_rewriter rw(m); + obj = a.mk_uminus(obj); + rw(obj, obj); + } + return out << obj; + } + + void optsmt::display_assignment(std::ostream& out) const { unsigned sz = m_objs.size(); for (unsigned i = 0; i < sz; ++i) { - bool is_max = m_is_max[i]; - inf_eps val = get_value(i); - expr_ref obj(m_objs[i], m); - if (!is_max) { - arith_util a(m); - th_rewriter rw(m); - obj = a.mk_uminus(obj); - rw(obj, obj); - } - out << "objective value: " << obj << " |-> " << val << std::endl; + display_objective(out, i) << " |-> " << get_value(i) << std::endl; } } + void optsmt::display_range_assignment(std::ostream& out) const { + unsigned sz = m_objs.size(); + for (unsigned i = 0; i < sz; ++i) { + display_objective(out, i) << " |-> [" << get_lower(i) << ":" << get_upper(i) << "]" << std::endl; + } + } + + + void optsmt::add(app* t, bool is_max) { expr_ref t1(t, m), t2(m); th_rewriter rw(m); diff --git a/src/opt/optsmt.h b/src/opt/optsmt.h index b892ef38f..2dae59a4f 100644 --- a/src/opt/optsmt.h +++ b/src/opt/optsmt.h @@ -44,20 +44,23 @@ namespace opt { void add(app* t, bool is_max); - void commit_assignment(unsigned i); - void set_cancel(bool f); void updt_params(params_ref& p); - void display(std::ostream& out) const; + void display_assignment(std::ostream& out) const; + void display_range_assignment(std::ostream& out) const; + unsigned get_num_objectives() const { return m_vars.size(); } + void commit_assignment(unsigned i); inf_eps get_value(unsigned index) const; inf_eps get_lower(unsigned index) const; inf_eps get_upper(unsigned index) const; private: + std::ostream& display_objective(std::ostream& out, unsigned i) const; + lbool basic_opt(); lbool farkas_opt(); diff --git a/src/opt/weighted_maxsat.h b/src/opt/weighted_maxsat.h index 3e1cd8529..8621ff9e1 100644 --- a/src/opt/weighted_maxsat.h +++ b/src/opt/weighted_maxsat.h @@ -6,7 +6,8 @@ Module Name: weighted_maxsat.h Abstract: - Weighted MAXSAT module + + Weighted MAXSAT module Author: @@ -14,6 +15,10 @@ Author: Notes: + Takes solver with hard constraints added. + Returns a maximal satisfying subset of weighted soft_constraints + that are still consistent with the solver state. + --*/ #ifndef _OPT_WEIGHTED_MAX_SAT_H_ #define _OPT_WEIGHTED_MAX_SAT_H_ @@ -22,11 +27,6 @@ Notes: #include "maxsmt.h" namespace opt { - /** - Takes solver with hard constraints added. - Returns a maximal satisfying subset of weighted soft_constraints - that are still consistent with the solver state. - */ class wmaxsmt : public maxsmt_solver { struct imp; imp* m_imp;