From 9f1b2ccfc4f8545406b2411b32e66cd8386af67c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 23 Jul 2014 23:53:03 +0200 Subject: [PATCH] restructure maxsmt solvers, flatten weighted/non-weighted versions, fix bugs and simplify mus/max-res Signed-off-by: Nikolaj Bjorner --- src/opt/hitting_sets.cpp | 2 +- src/opt/maxres.cpp | 174 +++++++--------- src/opt/maxres.h | 42 ++-- src/opt/maxsmt.cpp | 173 ++++++++++++++-- src/opt/maxsmt.h | 62 ++++++ src/opt/mus.cpp | 86 ++++++-- src/opt/mus.h | 24 ++- src/opt/opt_params.pyg | 3 +- src/opt/weighted_maxsat.cpp | 387 ++++++------------------------------ src/opt/weighted_maxsat.h | 37 ++-- 10 files changed, 492 insertions(+), 498 deletions(-) diff --git a/src/opt/hitting_sets.cpp b/src/opt/hitting_sets.cpp index fb9d2d009..c3436f61d 100644 --- a/src/opt/hitting_sets.cpp +++ b/src/opt/hitting_sets.cpp @@ -228,7 +228,7 @@ namespace opt { inc_score(clause_id); } TRACE("opt", display(tout, j);); - IF_VERBOSE(1, if (!sign) display(verbose_stream(), j);); + IF_VERBOSE(2, if (!sign) display(verbose_stream(), j);); if (!sign && m_enable_simplex) { add_simplex_row(!sign, sz, S); } diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp index 11d87a98e..2ec73bab4 100644 --- a/src/opt/maxres.cpp +++ b/src/opt/maxres.cpp @@ -1,7 +1,21 @@ -/** - MaxRes (weighted) max-sat algorithm by Nina and Bacchus, AAAI 2014. +/*++ +Copyright (c) 2014 Microsoft Corporation + +Module Name: + + maxsres.cpp + +Abstract: -*/ + MaxRes (weighted) max-sat algorithm by Nina and Bacchus, AAAI 2014. + +Author: + + Nikolaj Bjorner (nbjorner) 2014-20-7 + +Notes: + +--*/ #include "solver.h" #include "maxsmt.h" @@ -11,7 +25,8 @@ using namespace opt; -struct maxres::imp { + +class maxres : public maxsmt_solver_base { struct info { app* m_cls; rational m_weight; @@ -19,31 +34,25 @@ struct maxres::imp { m_cls(cls), m_weight(w) {} info(): m_cls(0) {} }; - ast_manager& m; - solver& s; expr_ref_vector m_B; - expr_ref_vector m_D; expr_ref_vector m_asms; - model_ref m_model; - expr_ref_vector m_soft_constraints; - volatile bool m_cancel; - rational m_lower; - rational m_upper; obj_map m_asm2info; ptr_vector m_new_core; mus m_mus; expr_ref_vector m_trail; - imp(ast_manager& m, solver& s, expr_ref_vector& soft_constraints, vector const& weights): - m(m), s(s), m_B(m), m_D(m), m_asms(m), m_soft_constraints(m), - m_cancel(false), - m_mus(s, m), +public: + maxres(ast_manager& m, opt_solver* s, params_ref& p, + vector const& ws, expr_ref_vector const& soft): + maxsmt_solver_base(s, m, p, ws, soft), + m_B(m), m_asms(m), + m_mus(m_s, m), m_trail(m) { - // TBD: this introduces an assertion to solver. - init_soft(weights, soft_constraints); } + virtual ~maxres() {} + bool is_literal(expr* l) { return is_uninterp_const(l) || @@ -60,9 +69,9 @@ struct maxres::imp { asum = e; } else { - asum = m.mk_fresh_const("soft", m.mk_bool_sort()); + asum = mk_fresh_bool("soft"); fml = m.mk_iff(asum, e); - s.assert_expr(fml); + m_s->assert_expr(fml); } new_assumption(asum, cls, w); m_upper += w; @@ -78,28 +87,35 @@ struct maxres::imp { lbool operator()() { expr_ref fml(m); ptr_vector core; - solver::scoped_push _sc(s); + solver::scoped_push _sc(*m_s.get()); + init(); + init_local(); while (true) { TRACE("opt", display_vec(tout, m_asms.size(), m_asms.c_ptr()); - s.display(tout); + m_s->display(tout); tout << "\n"; display(tout); ); - lbool is_sat = s.check_sat(m_asms.size(), m_asms.c_ptr()); + lbool is_sat = m_s->check_sat(m_asms.size(), m_asms.c_ptr()); if (m_cancel) { return l_undef; } switch (is_sat) { case l_true: - s.get_model(m_model); + m_s->get_model(m_model); + for (unsigned i = 0; i < m_soft.size(); ++i) { + expr_ref tmp(m); + VERIFY(m_model->eval(m_soft[i].get(), tmp)); + m_assignment[i] = m.is_true(tmp); + } m_upper = m_lower; return l_true; case l_undef: return l_undef; default: core.reset(); - s.get_unsat_core(core); + m_s->get_unsat_core(core); TRACE("opt", display_vec(tout << "core: ", core.size(), core.c_ptr());); SASSERT(!core.empty()); is_sat = minimize_core(core); @@ -115,7 +131,7 @@ struct maxres::imp { TRACE("opt", display_vec(tout << "minimized core: ", core.size(), core.c_ptr());); max_resolve(core, w); fml = m.mk_not(m.mk_and(m_B.size(), m_B.c_ptr())); - s.assert_expr(fml); + m_s->assert_expr(fml); m_lower += w; break; } @@ -192,31 +208,33 @@ struct maxres::imp { void max_resolve(ptr_vector& core, rational const& w) { SASSERT(!core.empty()); expr_ref fml(m), asum(m); - app_ref cls(m); + app_ref cls(m), d(m); m_B.reset(); - m_D.reset(); - m_D.resize(core.size()); m_B.append(core.size(), core.c_ptr()); - m_D[core.size()-1] = m.mk_false(); + d = m.mk_true(); // - // d_{sz-1} := false - // d_i := (!core_{i+1} or d_{i+1}) for i = 0...sz-2 - // soft (!d_i or core_i) - // - for (unsigned i = core.size()-1; i > 0; ) { - --i; - expr* d_i1 = m_D[i+1].get(); - expr* b_i = m_B[i].get(); - expr* b_i1 = m_B[i+1].get(); - m_D[i] = m.mk_implies(b_i1, d_i1); - expr* d_i = m_D[i].get(); - asum = m.mk_fresh_const("a", m.mk_bool_sort()); - cls = m.mk_implies(d_i, b_i); + // d_0 := true + // d_i := b_{i-1} and d_{i-1} for i = 1...sz-1 + // soft (b_i or !d_i) + // == (b_i or !(!b_{i-1} or d_{i-1})) + // == (b_i or b_0 & b_1 & ... & b_{i-1}) + // + // Soft constraint is satisfied if previous soft constraint + // holds or if it is the first soft constraint to fail. + // + // Soundness of this rule can be established using MaxRes + // + for (unsigned i = 1; i < core.size(); ++i) { + expr* b_i = m_B[i-1].get(); + expr* b_i1 = m_B[i].get(); + d = m.mk_and(b_i, d); + asum = mk_fresh_bool("a"); + cls = m.mk_or(b_i1, d); fml = m.mk_iff(asum, cls); cls = mk_cls(cls); m_trail.push_back(cls); new_assumption(asum, cls, w); - s.assert_expr(fml); + m_s->assert_expr(fml); } } @@ -262,77 +280,25 @@ struct maxres::imp { } } - rational get_lower() const { - return m_lower; - } - - rational get_upper() const { - return m_upper; - } - - bool get_assignment(unsigned index) const { - expr_ref tmp(m); - VERIFY(m_model->eval(m_soft_constraints[index], tmp)); - return m.is_true(tmp); - } - void set_cancel(bool f) { - m_cancel = f; + virtual void set_cancel(bool f) { + maxsmt_solver_base::set_cancel(f); m_mus.set_cancel(f); } - void collect_statistics(statistics& st) const { - } - void get_model(model_ref& mdl) { - mdl = m_model; - } - void updt_params(params_ref& p) { - ; - } - void init_soft(vector const& weights, expr_ref_vector const& soft) { - m_soft_constraints.reset(); + void init_local() { m_upper.reset(); m_lower.reset(); m_asm2info.reset(); m_trail.reset(); - m_soft_constraints.append(soft); - for (unsigned i = 0; i < m_soft_constraints.size(); ++i) { - add_soft(m_soft_constraints[i].get(), weights[i]); + for (unsigned i = 0; i < m_soft.size(); ++i) { + add_soft(m_soft[i].get(), m_weights[i]); } } }; -maxres::maxres(ast_manager& m, solver& s, expr_ref_vector& soft_constraints, vector const& weights) { - m_imp = alloc(imp, m, s, soft_constraints, weights); +opt::maxsmt_solver_base* opt::mk_maxres(ast_manager& m, opt_solver* s, params_ref& p, + vector const& ws, expr_ref_vector const& soft) { + return alloc(maxres, m, s, p, ws, soft); } -maxres::~maxres() { - dealloc(m_imp); -} - - -lbool maxres::operator()() { - return (*m_imp)(); -} - -rational maxres::get_lower() const { - return m_imp->get_lower(); -} -rational maxres::get_upper() const { - return m_imp->get_upper(); -} -bool maxres::get_assignment(unsigned index) const { - return m_imp->get_assignment(index); -} -void maxres::set_cancel(bool f) { - m_imp->set_cancel(f); -} -void maxres::collect_statistics(statistics& st) const { - m_imp->collect_statistics(st); -} -void maxres::get_model(model_ref& mdl) { - m_imp->get_model(mdl); -} -void maxres::updt_params(params_ref& p) { - m_imp->updt_params(p); -} diff --git a/src/opt/maxres.h b/src/opt/maxres.h index 41b57456f..8058a0376 100644 --- a/src/opt/maxres.h +++ b/src/opt/maxres.h @@ -1,18 +1,30 @@ +/*++ +Copyright (c) 2014 Microsoft Corporation + +Module Name: + + maxsres.h + +Abstract: + + MaxRes (weighted) max-sat algorithm by Nina and Bacchus, AAAI 2014. + +Author: + + Nikolaj Bjorner (nbjorner) 2014-20-7 + +Notes: + +--*/ + +#ifndef _MAXRES_H_ +#define _MAXRES_H_ namespace opt { - class maxres : public maxsmt_solver { - struct imp; - imp* m_imp; - public: - maxres(ast_manager& m, solver& s, expr_ref_vector& soft_constraints, vectorconst& weights); - ~maxres(); - virtual lbool operator()(); - virtual rational get_lower() const; - virtual rational get_upper() const; - virtual bool get_assignment(unsigned index) const; - virtual void set_cancel(bool f); - virtual void collect_statistics(statistics& st) const; - virtual void get_model(model_ref& mdl); - virtual void updt_params(params_ref& p); - }; + maxsmt_solver_base* mk_maxres(ast_manager& m, opt_solver* s, params_ref& p, + vector const& ws, expr_ref_vector const& soft); + + }; + +#endif diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp index 1cc98d328..2b20ccbd0 100644 --- a/src/opt/maxsmt.cpp +++ b/src/opt/maxsmt.cpp @@ -25,9 +25,140 @@ Notes: #include "weighted_maxsat.h" #include "ast_pp.h" #include "opt_params.hpp" +#include "pb_decl_plugin.h" +#include "pb_sls.h" +#include "tactical.h" +#include "tactic.h" +#include "tactic2solver.h" +#include "qfbv_tactic.h" +#include "card2bv_tactic.h" +#include "uint_set.h" +#include "opt_sls_solver.h" +#include "pb_preprocess_tactic.h" + + namespace opt { + void maxsmt_solver_base::updt_params(params_ref& p) { + m_params.copy(p); + s().updt_params(p); + opt_params _p(p); + m_enable_sat = _p.enable_sat(); + m_enable_sls = _p.enable_sls(); + } + + void maxsmt_solver_base::init_soft(vector const& weights, expr_ref_vector const& soft) { + m_weights.reset(); + m_soft.reset(); + m_weights.append(weights); + m_soft.append(soft); + } + + void maxsmt_solver_base::init() { + m_lower.reset(); + m_upper.reset(); + m_assignment.reset(); + for (unsigned i = 0; i < m_weights.size(); ++i) { + expr_ref val(m); + VERIFY(m_model->eval(m_soft[i].get(), val)); + m_assignment.push_back(m.is_true(val)); + if (!m_assignment.back()) { + m_upper += m_weights[i]; + } + } + + TRACE("opt", + tout << m_upper << ": "; + for (unsigned i = 0; i < m_weights.size(); ++i) { + tout << (m_assignment[i]?"1":"0"); + } + tout << "\n";); + } + + expr* maxsmt_solver_base::mk_not(expr* e) { + if (m.is_not(e, e)) { + return e; + } + else { + return m.mk_not(e); + } + } + + struct maxsmt_solver_base::is_bv { + struct found {}; + ast_manager& m; + pb_util pb; + bv_util bv; + is_bv(ast_manager& m): m(m), pb(m), bv(m) {} + void operator()(var *) { throw found(); } + void operator()(quantifier *) { throw found(); } + void operator()(app *n) { + family_id fid = n->get_family_id(); + if (fid != m.get_basic_family_id() && + fid != pb.get_family_id() && + fid != bv.get_family_id() && + !is_uninterp_const(n)) { + throw found(); + } + } + }; + + bool maxsmt_solver_base::probe_bv() { + expr_fast_mark1 visited; + is_bv proc(m); + try { + unsigned sz = s().get_num_assertions(); + for (unsigned i = 0; i < sz; i++) { + quick_for_each_expr(proc, visited, s().get_assertion(i)); + } + sz = m_soft.size(); + for (unsigned i = 0; i < sz; ++i) { + quick_for_each_expr(proc, visited, m_soft[i].get()); + } + } + catch (is_bv::found) { + return false; + } + return true; + } + + void maxsmt_solver_base::enable_bvsat() { + if (m_enable_sat && !m_sat_enabled && probe_bv()) { + tactic_ref pb2bv = mk_card2bv_tactic(m, m_params); + tactic_ref bv2sat = mk_qfbv_tactic(m, m_params); + tactic_ref tac = and_then(pb2bv.get(), bv2sat.get()); + solver* sat_solver = mk_tactic2solver(m, tac.get(), m_params); + unsigned sz = s().get_num_assertions(); + for (unsigned i = 0; i < sz; ++i) { + sat_solver->assert_expr(s().get_assertion(i)); + } + unsigned lvl = m_s->get_scope_level(); + while (lvl > 0) { sat_solver->push(); --lvl; } + m_s = sat_solver; + m_sat_enabled = true; + } + } + + void maxsmt_solver_base::enable_sls() { + if (m_enable_sls && !m_sls_enabled && probe_bv()) { + m_params.set_uint("restarts", 20); + unsigned lvl = m_s->get_scope_level(); + sls_solver* sls = alloc(sls_solver, m, m_s.get(), m_soft, m_weights, m_params); + m_s = sls; + while (lvl > 0) { m_s->push(); --lvl; } + m_sls_enabled = true; + sls->opt(m_model); + } + } + + app* maxsmt_solver_base::mk_fresh_bool(char const* name) { + app* result = m.mk_fresh_const(name, m.mk_bool_sort()); + m_mc->insert(result->get_decl()); + return result; + } + + lbool maxsmt::operator()(opt_solver* s) { lbool is_sat; m_msolver = 0; @@ -39,26 +170,40 @@ namespace opt { m_msolver = 0; is_sat = m_s->check_sat(0, 0); } - else if (m_maxsat_engine == symbol("maxres")) { - m_msolver = alloc(maxres, m, *m_s, m_soft_constraints, m_weights); + else if (m_maxsat_engine == symbol("maxres")) { + m_msolver = mk_maxres(m, s, m_params, m_weights, m_soft_constraints); } - else if (is_maxsat_problem(m_weights)) { - if (m_maxsat_engine == symbol("core_maxsat")) { - m_msolver = alloc(core_maxsat, m, *m_s, m_soft_constraints); - } - else if (m_maxsat_engine == symbol("weighted_maxsat")) { - m_msolver = alloc(wmaxsmt, m, m_s.get(), m_soft_constraints, m_weights); - } - else { - m_msolver = alloc(fu_malik, m, *m_s, m_soft_constraints); - } + else if (m_maxsat_engine == symbol("pbmax")) { + m_msolver = mk_pbmax(m, s, m_params, m_weights, m_soft_constraints); + } + else if (m_maxsat_engine == symbol("wpm2")) { + m_msolver = mk_wpm2(m, s, m_params, m_weights, m_soft_constraints); + } + else if (m_maxsat_engine == symbol("bcd2")) { + m_msolver = mk_bcd2(m, s, m_params, m_weights, m_soft_constraints); + } + else if (m_maxsat_engine == symbol("hsmax")) { + m_msolver = mk_hsmax(m, s, m_params, m_weights, m_soft_constraints); + } + else if (m_maxsat_engine == symbol("sls")) { + // NB: this is experimental one-round version of SLS + m_msolver = mk_sls(m, s, m_params, m_weights, m_soft_constraints); + } + else if (is_maxsat_problem(m_weights) && m_maxsat_engine == symbol("core_maxsat")) { + m_msolver = alloc(core_maxsat, m, *m_s, m_soft_constraints); + } + else if (is_maxsat_problem(m_weights) && m_maxsat_engine == symbol("fu_malik")) { + m_msolver = alloc(fu_malik, m, *m_s, m_soft_constraints); } else { - m_msolver = alloc(wmaxsmt, m, m_s.get(), m_soft_constraints, m_weights); + if (m_maxsat_engine != symbol::null) { + warning_msg("solver %s is not recognized, using default 'wmax'", + m_maxsat_engine.str().c_str()); + } + m_msolver = mk_wmax(m, m_s.get(), m_params, m_weights, m_soft_constraints); } if (m_msolver) { - m_msolver->updt_params(m_params); is_sat = (*m_msolver)(); if (is_sat != l_false) { m_msolver->get_model(m_model); diff --git a/src/opt/maxsmt.h b/src/opt/maxsmt.h index cd26c40e5..0cc833cba 100644 --- a/src/opt/maxsmt.h +++ b/src/opt/maxsmt.h @@ -37,6 +37,68 @@ namespace opt { virtual void updt_params(params_ref& p) = 0; }; + + // --------------------------------------------- + // base class with common utilities used + // by maxsmt solvers + // + class maxsmt_solver_base : public maxsmt_solver { + protected: + ref m_s; + ast_manager& m; + volatile bool m_cancel; + expr_ref_vector m_soft; + vector m_weights; + rational m_lower; + rational m_upper; + model_ref m_model; + ref m_mc; // model converter to remove fresh variables + svector m_assignment; // truth assignment to soft constraints + params_ref m_params; // config + bool m_enable_sls; // config + bool m_enable_sat; // config + bool m_sls_enabled; + bool m_sat_enabled; + struct is_bv; + + public: + maxsmt_solver_base(opt_solver* s, ast_manager& m, params_ref& p, + vector const& ws, expr_ref_vector const& soft): + m_s(s), m(m), m_cancel(false), m_soft(m), + m_enable_sls(false), m_enable_sat(false), + m_sls_enabled(false), m_sat_enabled(false) { + m_s->get_model(m_model); + SASSERT(m_model); + updt_params(p); + set_converter(s->mc_ref().get()); + init_soft(ws, soft); + } + + virtual ~maxsmt_solver_base() {} + virtual rational get_lower() const { return m_lower; } + virtual rational get_upper() const { return m_upper; } + virtual bool get_assignment(unsigned index) const { return m_assignment[index]; } + virtual void set_cancel(bool f) { m_cancel = f; m_s->set_cancel(f); } + virtual void collect_statistics(statistics& st) const { + if (m_sls_enabled || m_sat_enabled) { + m_s->collect_statistics(st); + } + } + virtual void get_model(model_ref& mdl) { mdl = m_model.get(); } + void set_model() { s().get_model(m_model); } + virtual void updt_params(params_ref& p); + virtual void init_soft(vector const& weights, expr_ref_vector const& soft); + void add_hard(expr* e){ s().assert_expr(e); } + solver& s() { return *m_s; } + void set_converter(filter_model_converter* mc) { m_mc = mc; } + void init(); + expr* mk_not(expr* e); + bool probe_bv(); + void enable_bvsat(); + void enable_sls(); + app* mk_fresh_bool(char const* name); + }; + /** Takes solver with hard constraints added. Returns modified soft constraints that are maximal assignments. diff --git a/src/opt/mus.cpp b/src/opt/mus.cpp index 9d9278a27..2e71f1bb8 100644 --- a/src/opt/mus.cpp +++ b/src/opt/mus.cpp @@ -1,15 +1,37 @@ +/*++ +Copyright (c) 2014 Microsoft Corporation + +Module Name: + + mus.cpp + +Abstract: + + Faster MUS extraction based on Belov et.al. HYB (Algorithm 3, 4) + +Author: + + Nikolaj Bjorner (nbjorner) 2014-20-7 + +Notes: + + Model rotation needs fixes to ensure that hard constraints are satisfied + under pertubed model. Model rotation also has o be consistent with theories. + +--*/ + #include "solver.h" #include "smt_literal.h" #include "mus.h" #include "ast_pp.h" +#include "model_smt2_pp.h" using namespace opt; -// Faster MUS extraction based on Belov et.al. HYB (Algorithm 3, 4) - +// struct mus::imp { - solver& s; + ref& m_s; ast_manager& m; expr_ref_vector m_cls2expr; obj_map m_expr2cls; @@ -18,7 +40,7 @@ struct mus::imp { obj_map m_var2idx; volatile bool m_cancel; - imp(solver& s, ast_manager& m): s(s), m(m), m_cls2expr(m), m_vars(m), m_cancel(false) {} + imp(ref& s, ast_manager& m): m_s(s), m(m), m_cls2expr(m), m_vars(m), m_cancel(false) {} void reset() { m_cls2expr.reset(); @@ -26,6 +48,7 @@ struct mus::imp { m_cls2lits.reset(); m_vars.reset(); m_var2idx.reset(); + m_vars.push_back(m.mk_true()); } void set_cancel(bool f) { @@ -42,7 +65,7 @@ struct mus::imp { } unsigned add_soft(expr* cls, unsigned sz, expr* const* args) { - TRACE("opt", tout << sz << ": " << mk_pp(cls, m) << "\n";); + SASSERT(is_uninterp_const(cls) || m.is_not(cls) && is_uninterp_const(to_app(cls)->get_arg(0))); smt::literal_vector lits; expr* arg; for (unsigned i = 0; i < sz; ++i) { @@ -57,6 +80,10 @@ struct mus::imp { m_expr2cls.insert(cls, idx); m_cls2expr.push_back(cls); m_cls2lits.push_back(lits); + TRACE("opt", + tout << idx << ": " << mk_pp(cls, m) << "\n"; + display_vec(tout, lits); + ); return idx; } @@ -68,7 +95,11 @@ struct mus::imp { } lbool get_mus(unsigned_vector& mus) { - TRACE("opt", tout << "\n";); + TRACE("opt", + for (unsigned i = 0; i < m_cls2lits.size(); ++i) { + display_vec(tout, m_cls2lits[i]); + } + ); unsigned_vector core; for (unsigned i = 0; i < m_cls2expr.size(); ++i) { core.push_back(i); @@ -79,13 +110,13 @@ struct mus::imp { ptr_vector core_exprs; model.resize(m_vars.size()); while (!core.empty()) { + IF_VERBOSE(1, verbose_stream() << "(opt.mus reducing core: " << core.size() << " new core: " << mus.size() << ")\n";); + unsigned cls_id = core.back(); TRACE("opt", display_vec(tout << "core: ", core); display_vec(tout << "mus: ", mus); display_vec(tout << "model: ", model); ); - IF_VERBOSE(1, verbose_stream() << "(opt.mus reducing core: " << core.size() << " new core: " << mus.size() << ")\n";); - unsigned cls_id = core.back(); core.pop_back(); expr* cls = m_cls2expr[cls_id].get(); expr_ref not_cls(m); @@ -93,7 +124,7 @@ struct mus::imp { unsigned sz = assumptions.size(); assumptions.push_back(not_cls); add_core(core, assumptions); - lbool is_sat = s.check_sat(assumptions.size(), assumptions.c_ptr()); + lbool is_sat = m_s->check_sat(assumptions.size(), assumptions.c_ptr()); assumptions.resize(sz); switch(is_sat) { case l_undef: @@ -101,7 +132,7 @@ struct mus::imp { case l_true: assumptions.push_back(cls); mus.push_back(cls_id); - extract_model(s, model); + extract_model(model); sz = core.size(); core.append(mus); rmr(core, mus, model); @@ -109,7 +140,7 @@ struct mus::imp { break; default: core_exprs.reset(); - s.get_unsat_core(core_exprs); + m_s->get_unsat_core(core_exprs); if (!core_exprs.contains(not_cls)) { // core := core_exprs \ mus core.reset(); @@ -141,14 +172,19 @@ struct mus::imp { out << "\n"; } - void extract_model(solver& s, svector& model) { + void extract_model(svector& model) { model_ref mdl; - s.get_model(mdl); + m_s->get_model(mdl); for (unsigned i = 0; i < m_vars.size(); ++i) { expr_ref tmp(m); mdl->eval(m_vars[i].get(), tmp); model[i] = m.is_true(tmp); } + TRACE("opt", + display_vec(tout << "model: ", model); + model_smt2_pp(tout, m, *mdl, 0); + ); + } /** @@ -166,7 +202,9 @@ struct mus::imp { smt::literal lit = cls[i]; SASSERT(model[lit.var()] == lit.sign()); // literal evaluates to false. model[lit.var()] = !model[lit.var()]; // swap assignment - if (!mus.contains(cls_id) && has_single_unsat(model, cls_id)) { + if (has_single_unsat(model, cls_id) && + !mus.contains(cls_id) && + model_check(model, cls_id)) { mus.push_back(cls_id); rmr(M, mus, model); } @@ -174,6 +212,11 @@ struct mus::imp { } } + bool model_check(svector const& model, unsigned cls_id) { + // model has to work for hard constraints. + return false; + } + bool has_single_unsat(svector const& model, unsigned& cls_id) const { cls_id = UINT_MAX; for (unsigned i = 0; i < m_cls2lits.size(); ++i) { @@ -186,21 +229,24 @@ struct mus::imp { } } } + TRACE("opt", display_vec(tout << "clause: " << cls_id << " model: ", model);); return cls_id != UINT_MAX; } bool eval(svector const& model, smt::literal_vector const& cls) const { - for (unsigned i = 0; i < cls.size(); ++i) { - if (model[cls[i].var()] != cls[i].sign()) { - return true; - } + bool result = false; + for (unsigned i = 0; !result && i < cls.size(); ++i) { + result = (model[cls[i].var()] != cls[i].sign()); } - return false; + TRACE("opt", display_vec(tout << "model: ", model); + display_vec(tout << "clause: ", cls); + tout << "result: " << result << "\n";); + return result; } }; -mus::mus(solver& s, ast_manager& m) { +mus::mus(ref& s, ast_manager& m) { m_imp = alloc(imp, s, m); } diff --git a/src/opt/mus.h b/src/opt/mus.h index e3cb4c963..064ab3b0e 100644 --- a/src/opt/mus.h +++ b/src/opt/mus.h @@ -1,10 +1,30 @@ +/*++ +Copyright (c) 2014 Microsoft Corporation + +Module Name: + + mus.h + +Abstract: + + Faster MUS extraction based on Belov et.al. HYB (Algorithm 3, 4) + +Author: + + Nikolaj Bjorner (nbjorner) 2014-20-7 + +Notes: + +--*/ +#ifndef _MUS_H_ +#define _MUS_H_ namespace opt { class mus { struct imp; imp * m_imp; public: - mus(solver& s, ast_manager& m); + mus(ref& s, ast_manager& m); ~mus(); /** Add soft constraint. @@ -23,3 +43,5 @@ namespace opt { }; }; + +#endif diff --git a/src/opt/opt_params.pyg b/src/opt/opt_params.pyg index 2e6f67219..fbc2a8796 100644 --- a/src/opt/opt_params.pyg +++ b/src/opt/opt_params.pyg @@ -3,13 +3,12 @@ def_module_params('opt', export=True, params=(('timeout', UINT, UINT_MAX, 'set timeout'), ('engine', SYMBOL, 'basic', "select optimization engine: 'basic', 'farkas', 'symba'"), - ('maxsat_engine', SYMBOL, 'fu_malik', "select engine for non-weighted maxsat: 'fu_malik', 'core_maxsat'"), + ('maxsat_engine', SYMBOL, 'wmax', "select engine for maxsat: 'fu_malik', 'core_maxsat', 'wmax', 'pbmax', 'maxres', 'bcd2', 'wpm2', 'sls', 'hsmax'"), ('priority', SYMBOL, 'lex', "select how to priortize objectives: 'lex' (lexicographic), 'pareto', or 'box'"), ('dump_benchmarks', BOOL, False, 'dump benchmarks for profiling'), ('print_model', BOOL, False, 'display model for satisfiable constraints'), ('print_all_models', BOOL, False, 'display all intermediary models for satisfiable constraints'), ('debug_conflict', BOOL, False, 'debug conflict resolution'), - ('wmaxsat_engine', SYMBOL, 'wmax', "weighted maxsat engine: 'wmax', 'pbmax', 'bcd2', 'wpm2', 'bvsls', 'sls'"), ('enable_sls', BOOL, False, 'enable SLS tuning during weighted maxsast'), ('enable_sat', BOOL, False, 'enable the new SAT core for propositional constraints'), ('sls_engine', SYMBOL, 'pb', "SLS engine. Either 'bv' or 'pb'"), diff --git a/src/opt/weighted_maxsat.cpp b/src/opt/weighted_maxsat.cpp index 8d405196c..dbd5a060f 100644 --- a/src/opt/weighted_maxsat.cpp +++ b/src/opt/weighted_maxsat.cpp @@ -26,19 +26,12 @@ Notes: #include "opt_params.hpp" #include "pb_decl_plugin.h" #include "uint_set.h" -#include "tactical.h" -#include "tactic.h" #include "model_smt2_pp.h" -#include "pb_sls.h" -#include "tactic2solver.h" -#include "pb_preprocess_tactic.h" -#include "qfbv_tactic.h" -#include "card2bv_tactic.h" -#include "opt_sls_solver.h" #include "cancel_eh.h" #include "scoped_timer.h" #include "optsmt.h" #include "hitting_sets.h" +#include "stopwatch.h" namespace opt { @@ -56,162 +49,6 @@ namespace opt { } }; - // --------------------------------------------- - // base class with common utilities used - // by maxsmt solvers - // - class maxsmt_solver_base : public maxsmt_solver { - protected: - ref m_s; - ast_manager& m; - volatile bool m_cancel; - expr_ref_vector m_soft; - vector m_weights; - rational m_lower; - rational m_upper; - model_ref m_model; - ref m_mc; // model converter to remove fresh variables - svector m_assignment; // truth assignment to soft constraints - params_ref m_params; // config - bool m_enable_sls; // config - bool m_enable_sat; // config - bool m_sls_enabled; - bool m_sat_enabled; - public: - maxsmt_solver_base(solver* s, ast_manager& m): - m_s(s), m(m), m_cancel(false), m_soft(m), - m_enable_sls(false), m_enable_sat(false), - m_sls_enabled(false), m_sat_enabled(false) { - m_s->get_model(m_model); - SASSERT(m_model); - } - - virtual ~maxsmt_solver_base() {} - virtual rational get_lower() const { return m_lower; } - virtual rational get_upper() const { return m_upper; } - virtual bool get_assignment(unsigned index) const { return m_assignment[index]; } - virtual void set_cancel(bool f) { m_cancel = f; m_s->set_cancel(f); } - virtual void collect_statistics(statistics& st) const { - if (m_sls_enabled || m_sat_enabled) { - m_s->collect_statistics(st); - } - } - virtual void get_model(model_ref& mdl) { mdl = m_model.get(); } - void set_model() { s().get_model(m_model); } - virtual void updt_params(params_ref& p) { - m_params.copy(p); - s().updt_params(p); - opt_params _p(p); - m_enable_sat = _p.enable_sat(); - m_enable_sls = _p.enable_sls(); - } - virtual void init_soft(vector const& weights, expr_ref_vector const& soft) { - m_weights.reset(); - m_soft.reset(); - m_weights.append(weights); - m_soft.append(soft); - } - void add_hard(expr* e){ s().assert_expr(e); } - solver& s() { return *m_s; } - void set_converter(filter_model_converter* mc) { m_mc = mc; } - - void init() { - m_lower.reset(); - m_upper.reset(); - m_assignment.reset(); - for (unsigned i = 0; i < m_weights.size(); ++i) { - expr_ref val(m); - VERIFY(m_model->eval(m_soft[i].get(), val)); - m_assignment.push_back(m.is_true(val)); - if (!m_assignment.back()) { - m_upper += m_weights[i]; - } - } - - TRACE("opt", - tout << m_upper << ": "; - for (unsigned i = 0; i < m_weights.size(); ++i) { - tout << (m_assignment[i]?"1":"0"); - } - tout << "\n";); - } - - expr* mk_not(expr* e) { - if (m.is_not(e, e)) { - return e; - } - else { - return m.mk_not(e); - } - } - - struct is_bv { - struct found {}; - ast_manager& m; - pb_util pb; - bv_util bv; - is_bv(ast_manager& m): m(m), pb(m), bv(m) {} - void operator()(var *) { throw found(); } - void operator()(quantifier *) { throw found(); } - void operator()(app *n) { - family_id fid = n->get_family_id(); - if (fid != m.get_basic_family_id() && - fid != pb.get_family_id() && - fid != bv.get_family_id() && - !is_uninterp_const(n)) { - throw found(); - } - } - }; - - bool probe_bv() { - expr_fast_mark1 visited; - is_bv proc(m); - try { - unsigned sz = s().get_num_assertions(); - for (unsigned i = 0; i < sz; i++) { - quick_for_each_expr(proc, visited, s().get_assertion(i)); - } - sz = m_soft.size(); - for (unsigned i = 0; i < sz; ++i) { - quick_for_each_expr(proc, visited, m_soft[i].get()); - } - } - catch (is_bv::found) { - return false; - } - return true; - } - - void enable_bvsat() { - if (m_enable_sat && !m_sat_enabled && probe_bv()) { - tactic_ref pb2bv = mk_card2bv_tactic(m, m_params); - tactic_ref bv2sat = mk_qfbv_tactic(m, m_params); - tactic_ref tac = and_then(pb2bv.get(), bv2sat.get()); - solver* sat_solver = mk_tactic2solver(m, tac.get(), m_params); - unsigned sz = s().get_num_assertions(); - for (unsigned i = 0; i < sz; ++i) { - sat_solver->assert_expr(s().get_assertion(i)); - } - unsigned lvl = m_s->get_scope_level(); - while (lvl > 0) { sat_solver->push(); --lvl; } - m_s = sat_solver; - m_sat_enabled = true; - } - } - - void enable_sls() { - if (m_enable_sls && !m_sls_enabled && probe_bv()) { - m_params.set_uint("restarts", 20); - unsigned lvl = m_s->get_scope_level(); - sls_solver* sls = alloc(sls_solver, m, m_s.get(), m_soft, m_weights, m_params); - m_s = sls; - while (lvl > 0) { m_s->push(); --lvl; } - m_sls_enabled = true; - sls->opt(m_model); - } - } - }; // ------------------------------------------------------ // Morgado, Heras, Marques-Silva 2013 @@ -247,8 +84,7 @@ namespace opt { es.push_back(m.mk_not(*it)); } } - virtual void init_soft(vector const& weights, expr_ref_vector const& soft) { - maxsmt_solver_base::init_soft(weights, soft); + void bcd2_init_soft(vector const& weights, expr_ref_vector const& soft) { // normalize weights to be integral: m_den = rational::one(); @@ -290,13 +126,15 @@ namespace opt { } public: - bcd2(solver* s, ast_manager& m): - maxsmt_solver_base(s, m), + bcd2(opt_solver* s, ast_manager& m, params_ref& p, + vector const& ws, expr_ref_vector const& soft): + maxsmt_solver_base(s, m, p, ws, soft), pb(m), m_soft_aux(m), m_trail(m), m_soft_constraints(m), m_enable_lazy(true) { + bcd2_init_soft(ws, soft); } virtual ~bcd2() {} @@ -315,7 +153,7 @@ namespace opt { } process_sat(); while (m_lower < m_upper) { - IF_VERBOSE(1, verbose_stream() << "(wmaxsat.bcd2 [" << m_lower << ":" << m_upper << "])\n";); + IF_VERBOSE(1, verbose_stream() << "(bcd2 [" << m_lower << ":" << m_upper << "])\n";); assert_soft(); solver::scoped_push _scope2(s()); TRACE("opt", display(tout);); @@ -412,10 +250,8 @@ namespace opt { } expr* mk_fresh() { - app_ref r(m); - r = m.mk_fresh_const("r", m.mk_bool_sort()); + expr* r = mk_fresh_bool("r"); m_trail.push_back(r); - m_mc->insert(r->get_decl()); return r; } @@ -627,8 +463,8 @@ namespace opt { public: - hsmax(solver* s, ast_manager& m): - maxsmt_solver_base(s, m), + hsmax(opt_solver* s, ast_manager& m, params_ref& p, vector const& ws, expr_ref_vector const& soft): + maxsmt_solver_base(s, m, p, ws, soft), m_aux(m), pb(m), a(m), @@ -641,10 +477,6 @@ namespace opt { m_hs.set_cancel(f); } - virtual void updt_params(params_ref& p) { - maxsmt_solver_base::updt_params(p); - } - virtual void collect_statistics(statistics& st) const { maxsmt_solver_base::collect_statistics(st); m_hs.collect_statistics(st); @@ -670,8 +502,8 @@ namespace opt { while (m_lower < m_upper) { ++m_stats.m_num_iterations; IF_VERBOSE(1, verbose_stream() << - "(wmaxsat.hsmax [" << m_lower << ":" << m_upper << "])\n";); - TRACE("opt", tout << "(wmaxsat.hsmax [" << m_lower << ":" << m_upper << "])\n";); + "(hsmax [" << m_lower << ":" << m_upper << "])\n";); + TRACE("opt", tout << "(hsmax [" << m_lower << ":" << m_upper << "])\n";); if (m_cancel) { return l_undef; } @@ -688,7 +520,7 @@ namespace opt { break; case l_false: TRACE("opt", tout << "no more seeds\n";); - IF_VERBOSE(1, verbose_stream() << "(wmaxsat.maxhs.no-more-seeds)\n";); + IF_VERBOSE(1, verbose_stream() << "(maxhs.no-more-seeds)\n";); m_lower = m_upper; return l_true; case l_undef: @@ -697,7 +529,7 @@ namespace opt { break; } case l_false: - IF_VERBOSE(1, verbose_stream() << "(wmaxsat.maxhs.no-more-cores)\n";); + IF_VERBOSE(1, verbose_stream() << "(maxhs.no-more-cores)\n";); TRACE("opt", tout << "no more cores\n";); m_lower = m_upper; return l_true; @@ -1119,8 +951,9 @@ namespace opt { class pbmax : public maxsmt_solver_base { public: - pbmax(solver* s, ast_manager& m): - maxsmt_solver_base(s, m) { + pbmax(opt_solver* s, ast_manager& m, params_ref& p, + vector const& ws, expr_ref_vector const& soft): + maxsmt_solver_base(s, m, p, ws, soft) { } virtual ~pbmax() {} @@ -1154,7 +987,7 @@ namespace opt { m_upper += m_weights[i]; } } - IF_VERBOSE(1, verbose_stream() << "(wmaxsat.pb solve with upper bound: " << m_upper << ")\n";); + IF_VERBOSE(1, verbose_stream() << "(pb solve with upper bound: " << m_upper << ")\n";); TRACE("opt", tout << "new upper: " << m_upper << "\n";); fml = u.mk_lt(nsoft.size(), m_weights.c_ptr(), nsoft.c_ptr(), m_upper); @@ -1182,15 +1015,16 @@ namespace opt { class wpm2 : public maxsmt_solver_base { scoped_ptr maxs; public: - wpm2(solver* s, ast_manager& m, maxsmt_solver_base* _maxs): - maxsmt_solver_base(s, m), maxs(_maxs) { + wpm2(opt_solver* s, ast_manager& m, maxsmt_solver_base* _maxs, params_ref& p, + vector const& ws, expr_ref_vector const& soft): + maxsmt_solver_base(s, m, p, ws, soft), maxs(_maxs) { } virtual ~wpm2() {} lbool operator()() { enable_sls(); - IF_VERBOSE(1, verbose_stream() << "(wmaxsat.wpm2 solve)\n";); + IF_VERBOSE(1, verbose_stream() << "(wpm2 solve)\n";); solver::scoped_push _s(s()); pb_util u(m); app_ref fml(m), a(m), b(m), c(m); @@ -1203,20 +1037,17 @@ namespace opt { for (unsigned i = 0; i < m_soft.size(); ++i) { rational w = m_weights[i]; - b = m.mk_fresh_const("b", m.mk_bool_sort()); - m_mc->insert(b->get_decl()); + b = mk_fresh_bool("b"); block.push_back(b); expr* bb = b; - a = m.mk_fresh_const("a", m.mk_bool_sort()); - m_mc->insert(a->get_decl()); + a = mk_fresh_bool("a"); ans.push_back(a); ans_index.insert(a, i); fml = m.mk_or(m_soft[i].get(), b, m.mk_not(a)); s().assert_expr(fml); - c = m.mk_fresh_const("c", m.mk_bool_sort()); - m_mc->insert(c->get_decl()); + c = mk_fresh_bool("c"); fml = m.mk_implies(c, u.mk_le(1,&w,&bb,rational(0))); s().assert_expr(fml); @@ -1321,11 +1152,10 @@ namespace opt { B_ge_k = u.mk_ge(ws.size(), ws.c_ptr(), bs.c_ptr(), k); s().assert_expr(B_ge_k); al.push_back(B_ge_k); - IF_VERBOSE(1, verbose_stream() << "(wmaxsat.wpm2 lower bound: " << m_lower << ")\n";); + IF_VERBOSE(1, verbose_stream() << "(wpm2 lower bound: " << m_lower << ")\n";); IF_VERBOSE(2, verbose_stream() << "New lower bound: " << B_ge_k << "\n";); - c = m.mk_fresh_const("c", m.mk_bool_sort()); - m_mc->insert(c->get_decl()); + c = mk_fresh_bool("c"); fml = m.mk_implies(c, B_le_k); s().assert_expr(fml); sc.push_back(B); @@ -1394,8 +1224,9 @@ namespace opt { class sls : public maxsmt_solver_base { public: - sls(solver* s, ast_manager& m): - maxsmt_solver_base(s, m) { + sls(opt_solver* s, ast_manager& m, params_ref& p, + vector const& ws, expr_ref_vector const& soft): + maxsmt_solver_base(s, m, p, ws, soft) { } virtual ~sls() {} lbool operator()() { @@ -1425,8 +1256,9 @@ namespace opt { class maxsmt_solver_wbase : public maxsmt_solver_base { smt::context& ctx; public: - maxsmt_solver_wbase(solver* s, ast_manager& m, smt::context& ctx): - maxsmt_solver_base(s, m), ctx(ctx) {} + maxsmt_solver_wbase(opt_solver* s, ast_manager& m, smt::context& ctx, params_ref& p, + vector const& ws, expr_ref_vector const& soft): + maxsmt_solver_base(s, m, p, ws, soft), ctx(ctx) {} ~maxsmt_solver_wbase() {} class scoped_ensure_theory { @@ -1471,7 +1303,9 @@ namespace opt { class wmax : public maxsmt_solver_wbase { public: - wmax(solver* s, ast_manager& m, smt::context& ctx): maxsmt_solver_wbase(s, m, ctx) {} + wmax(opt_solver* s, ast_manager& m, smt::context& ctx, params_ref& p, + vector const& ws, expr_ref_vector const& soft): + maxsmt_solver_wbase(s, m, ctx, p, ws, soft) {} virtual ~wmax() {} lbool operator()() { @@ -1515,129 +1349,36 @@ namespace opt { } }; - struct wmaxsmt::imp { - ast_manager& m; - ref s; // solver state that contains hard constraints - expr_ref_vector m_soft; // set of soft constraints - vector m_weights; // their weights - symbol m_engine; // config - mutable params_ref m_params; // config - mutable scoped_ptr m_maxsmt; // underlying maxsmt solver - imp(ast_manager& m, - opt_solver* s, - expr_ref_vector const& soft_constraints, - vector const& weights): - m(m), - s(s), - m_soft(soft_constraints), - m_weights(weights) - { - } + maxsmt_solver_base* opt::mk_bcd2(ast_manager& m, opt_solver* s, params_ref& p, + vector const& ws, expr_ref_vector const& soft) { + return alloc(bcd2, s, m, p, ws, soft); + } + maxsmt_solver_base* opt::mk_pbmax(ast_manager& m, opt_solver* s, params_ref& p, + vector const& ws, expr_ref_vector const& soft) { + return alloc(pbmax, s, m, p, ws, soft); + } + maxsmt_solver_base* opt::mk_hsmax(ast_manager& m, opt_solver* s, params_ref& p, + vector const& ws, expr_ref_vector const& soft) { + return alloc(hsmax, s, m, p, ws, soft); + } + maxsmt_solver_base* opt::mk_sls(ast_manager& m, opt_solver* s, params_ref& p, + vector const& ws, expr_ref_vector const& soft) { + return alloc(hsmax, s, m, p, ws, soft); + } + maxsmt_solver_base* opt::mk_wmax(ast_manager& m, opt_solver* s, params_ref& p, + vector const& ws, expr_ref_vector const& soft) { + return alloc(wmax, s, m, s->get_context(), p, ws, soft); + } + maxsmt_solver_base* opt::mk_wpm2(ast_manager& m, opt_solver* s, params_ref& p, + vector const& ws, expr_ref_vector const& soft) { - maxsmt_solver_base& maxsmt() const { - if (m_maxsmt) { - return *m_maxsmt; - } - if (m_engine == symbol("pbmax")) { - m_maxsmt = alloc(pbmax, s.get(), m); - } - else if (m_engine == symbol("wpm2")) { - ref s0 = alloc(opt_solver, m, m_params, symbol()); - // initialize model. - s0->check_sat(0,0); - maxsmt_solver_base* s2 = alloc(pbmax, s0.get(), m); - m_maxsmt = alloc(wpm2, s.get(), m, s2); - } - else if (m_engine == symbol("bcd2")) { - m_maxsmt = alloc(bcd2, s.get(), m); - } - else if (m_engine == symbol("hsmax")) { - m_maxsmt = alloc(hsmax, s.get(), m); - } - // NB: this is experimental one-round version of SLS - else if (m_engine == symbol("sls")) { - m_maxsmt = alloc(sls, s.get(), m); - } - else if (m_engine == symbol::null || m_engine == symbol("wmax")) { - m_maxsmt = alloc(wmax, s.get(), m, s->get_context()); - } - else { - IF_VERBOSE(0, verbose_stream() << "(unknown engine " << m_engine << " using default 'wmax')\n";); - m_maxsmt = alloc(wmax, s.get(), m, s->get_context()); - } - m_maxsmt->updt_params(m_params); - m_maxsmt->init_soft(m_weights, m_soft); - m_maxsmt->set_converter(s->mc_ref().get()); - return *m_maxsmt; - } + ref s0 = alloc(opt_solver, m, p, symbol()); + // initialize model. + s0->check_sat(0,0); + maxsmt_solver_base* s2 = alloc(pbmax, s0.get(), m, p, ws, soft); + return alloc(wpm2, s, m, s2, p, ws, soft); + } - ~imp() {} - /** - Takes solver with hard constraints added. - Returns a maximal satisfying subset of weighted soft_constraints - that are still consistent with the solver state. - */ - lbool operator()() { - return maxsmt()(); - } - rational get_lower() const { - return maxsmt().get_lower(); - } - rational get_upper() const { - return maxsmt().get_upper(); - } - void get_model(model_ref& mdl) { - if (m_maxsmt) m_maxsmt->get_model(mdl); - } - void set_cancel(bool f) { - if (m_maxsmt) m_maxsmt->set_cancel(f); - } - bool get_assignment(unsigned index) const { - return maxsmt().get_assignment(index); - } - void collect_statistics(statistics& st) const { - if (m_maxsmt) m_maxsmt->collect_statistics(st); - } - void updt_params(params_ref& p) { - opt_params _p(p); - m_engine = _p.wmaxsat_engine(); - m_maxsmt = 0; - } - }; - - wmaxsmt::wmaxsmt(ast_manager& m, - opt_solver* s, - expr_ref_vector& soft_constraints, - vector const& weights) { - m_imp = alloc(imp, m, s, soft_constraints, weights); - } - wmaxsmt::~wmaxsmt() { - dealloc(m_imp); - } - lbool wmaxsmt::operator()() { - return (*m_imp)(); - } - rational wmaxsmt::get_lower() const { - return m_imp->get_lower(); - } - rational wmaxsmt::get_upper() const { - return m_imp->get_upper(); - } - bool wmaxsmt::get_assignment(unsigned idx) const { - return m_imp->get_assignment(idx); - } - void wmaxsmt::set_cancel(bool f) { - m_imp->set_cancel(f); - } - void wmaxsmt::collect_statistics(statistics& st) const { - m_imp->collect_statistics(st); - } - void wmaxsmt::get_model(model_ref& mdl) { - m_imp->get_model(mdl); - } - void wmaxsmt::updt_params(params_ref& p) { - m_imp->updt_params(p); - } }; diff --git a/src/opt/weighted_maxsat.h b/src/opt/weighted_maxsat.h index d84f96f0a..5343a3b97 100644 --- a/src/opt/weighted_maxsat.h +++ b/src/opt/weighted_maxsat.h @@ -27,24 +27,25 @@ Notes: #include "maxsmt.h" namespace opt { - class wmaxsmt : public maxsmt_solver { - struct imp; - imp* m_imp; - public: - wmaxsmt(ast_manager& m, - opt_solver* s, - expr_ref_vector& soft_constraints, - vector const& weights); - ~wmaxsmt(); - virtual lbool operator()(); - virtual rational get_lower() const; - virtual rational get_upper() const; - virtual bool get_assignment(unsigned idx) const; - virtual void set_cancel(bool f); - virtual void collect_statistics(statistics& st) const; - virtual void get_model(model_ref& mdl); - virtual void updt_params(params_ref& p); - }; + + maxsmt_solver_base* mk_bcd2(ast_manager& m, opt_solver* s, params_ref& p, + vector const& ws, expr_ref_vector const& soft); + + maxsmt_solver_base* mk_hsmax(ast_manager& m, opt_solver* s, params_ref& p, + vector const& ws, expr_ref_vector const& soft); + + maxsmt_solver_base* mk_pbmax(ast_manager& m, opt_solver* s, params_ref& p, + vector const& ws, expr_ref_vector const& soft); + + maxsmt_solver_base* mk_wpm2(ast_manager& m, opt_solver* s, params_ref& p, + vector const& ws, expr_ref_vector const& soft); + + maxsmt_solver_base* mk_sls(ast_manager& m, opt_solver* s, params_ref& p, + vector const& ws, expr_ref_vector const& soft); + + maxsmt_solver_base* mk_wmax(ast_manager& m, opt_solver* s, params_ref& p, + vector const& ws, expr_ref_vector const& soft); + }; #endif