diff --git a/src/opt/fu_malik.cpp b/src/opt/fu_malik.cpp index 977174681..92b26ad0b 100644 --- a/src/opt/fu_malik.cpp +++ b/src/opt/fu_malik.cpp @@ -38,26 +38,24 @@ namespace opt { class fu_malik { ast_manager& m; solver& s; - expr_ref_vector& m_soft; + expr_ref_vector m_soft; expr_ref_vector m_aux; public: - fu_malik(ast_manager& m, solver& s, expr_ref_vector& soft): + fu_malik(ast_manager& m, solver& s, expr_ref_vector const& soft): m(m), s(s), m_soft(soft), - m_aux_vars(m) + m_aux(m) { - m_aux.reset(); for (unsigned i = 0; i < m_soft.size(); i++) { - m_aux.push_back(m.mk_fresh_const("p",m.mk_bool())); - s.assert_expr(m.mk_or(m_soft[i].get(), m_aux[i].get())); + m_aux.push_back(m.mk_fresh_const("p", m.mk_bool_sort())); + s.assert_expr(m.mk_or(soft[i], m_aux[i].get())); } } /** - \brief Implement one step of the Fu&Malik algorithm. - See fu_malik_maxsat function for more details. + \brief One step of the Fu&Malik algorithm. Input: soft constraints + aux-vars (aka answer literals) Output: done/not-done when not done return updated set of soft-constraints and aux-vars. @@ -85,7 +83,7 @@ namespace opt { s.get_unsat_core(core); // update soft-constraints and aux_vars - for (i = 0; i < m_soft.size(); i++) { + for (unsigned i = 0; i < m_soft.size(); i++) { bool found = false; for (unsigned j = 0; !found && j < core.size(); ++j) { @@ -108,36 +106,49 @@ namespace opt { private: void assert_at_most_one(expr_ref_vector const& block_vars) { - + expr_ref has_one(m), no_one(m), at_most_one(m); + mk_at_most_one(block_vars.size(), block_vars.c_ptr(), has_one, no_one); + at_most_one = m.mk_or(has_one, no_one); + s.assert_expr(at_most_one); } -#if 0 - expr_ref mk_at_most_one(unsigned n, expr* const * vars) { - if (n <= 1) { - return expr_ref(m.mk_true(), m); + void mk_at_most_one(unsigned n, expr* const * vars, expr_ref& has_one, expr_ref& no_one) { + if (n == 1) { + has_one = vars[0]; + no_one = m.mk_not(vars[0]); + } + else { + unsigned mid = n/2; + expr_ref has_one1(m), has_one2(m), no_one1(m), no_one2(m); + mk_at_most_one(mid, vars, has_one1, no_one1); + mk_at_most_one(n-mid, vars+mid, has_one2, no_one2); + has_one = m.mk_or(m.mk_and(has_one1, no_one2), m.mk_and(has_one2, no_one1)); + no_one = m.mk_and(no_one1, no_one2); } - unsigned mid = n/2; - } -#endif }; + // TBD: the vector of soft constraints gets updated + // but we really want to return the maximal set of + // original soft constraints that are satisfied. + // so we need to read out of the model what soft constraints + // were satisfied. + lbool fu_malik_maxsat(solver& s, expr_ref_vector& soft_constraints) { ast_manager m = soft_constraints.get_manager(); - lbool is_sat = s.check(); - if (is_sat != l_true) { - return is_sat; + lbool is_sat = s.check_sat(0,0); + if (!soft_constraints.empty() && is_sat == l_true) { + s.push(); + fu_malik fm(m, s, soft_constraints); + while (!fm.step()); + s.pop(1); } - if (soft_constraints.empty()) { - return is_sat; - } - s.push(); - fu_malik fm(m, s, soft_constraints); - while (!fm.step()); - s.pop(); - // we are done and soft_constraints has been updated with the max-sat assignment. + // we are done and soft_constraints has + // been updated with the max-sat assignment. + + return is_sat; } }; diff --git a/src/opt/opt_cmds.cpp b/src/opt/opt_cmds.cpp index b5b7d1ddd..8c0a458d5 100644 --- a/src/opt/opt_cmds.cpp +++ b/src/opt/opt_cmds.cpp @@ -18,6 +18,8 @@ Notes: #include "opt_cmds.h" #include "cmd_context.h" #include "ast_pp.h" +#include "smt_solver.h" +#include "fu_malik.h" class opt_context { ast_manager& m; @@ -35,7 +37,7 @@ public: m_weights.push_back(w); } - expr_ref_vector const& formulas() const { return m_formulas; } + expr_ref_vector const & formulas() const { return m_formulas; } vector const& weights() const { return m_weights; } }; @@ -93,7 +95,6 @@ public: } virtual void execute(cmd_context & ctx) { - std::cout << "TODO: " << mk_pp(m_formula, ctx.m()) << " " << m_weight << "\n"; m_opt_ctx->add_formula(m_formula, m_weight); reset(ctx); } @@ -141,22 +142,51 @@ public: } virtual void execute(cmd_context & ctx) { + ast_manager& m = m_term.get_manager(); std::cout << "TODO: " << mk_pp(m_term, ctx.m()) << "\n"; // Here is how to retrieve the soft constraints - m_opt_ctx->formulas(); - m_opt_ctx->weights(); - get_background(ctx); - // reset m_opt_ctx? - } + expr_ref_vector const& fmls = m_opt_ctx->formulas(); + vector const& ws = m_opt_ctx->weights(); + + // TODO: move most functionaltiy to separate module, because it is going to grow.. + ref s; + symbol logic; + params_ref p; + p.set_bool("model", true); + p.set_bool("unsat_core", true); + s = mk_smt_solver(m, p, logic); -private: - void get_background(cmd_context& ctx) { ptr_vector::const_iterator it = ctx.begin_assertions(); ptr_vector::const_iterator end = ctx.end_assertions(); for (; it != end; ++it) { - // Need a solver object that supports soft constraints - // m_solver.assert_expr(*it); + s->assert_expr(*it); } + expr_ref_vector fmls_copy(fmls); + if (is_maxsat_problem(ws)) { + lbool is_sat = opt::fu_malik_maxsat(*s, fmls_copy); + std::cout << "is-sat: " << is_sat << "\n"; + if (is_sat == l_true) { + for (unsigned i = 0; i < fmls_copy.size(); ++i) { + std::cout << mk_pp(fmls_copy[i].get(), m) << "\n"; + } + } + } + else { + NOT_IMPLEMENTED_YET(); + } + + // handle optimization criterion. + } + +private: + + bool is_maxsat_problem(vector const& ws) const { + for (unsigned i = 0; i < ws.size(); ++i) { + if (!ws[i].is_one()) { + return false; + } + } + return true; } };