From 02f74f102826ab1f529e48e2f144b8a240eb296b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 17 Dec 2013 05:03:20 +0200 Subject: [PATCH] trying Cezary's example Signed-off-by: Nikolaj Bjorner --- src/opt/maxsmt.cpp | 3 +++ src/opt/weighted_maxsat.cpp | 1 + 2 files changed, 4 insertions(+) diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp index 3b0f684e8..8f77cdf85 100644 --- a/src/opt/maxsmt.cpp +++ b/src/opt/maxsmt.cpp @@ -39,6 +39,9 @@ namespace opt { if (m_maxsat_engine == symbol("core_maxsat")) { m_msolver = alloc(core_maxsat, m, s, m_soft_constraints); } + else if (m_maxsat_engine == symbol("weighted_maxsat")) { + m_msolver = alloc(wmaxsmt, m, opt_solver::to_opt(s), m_soft_constraints, m_weights); + } else { m_msolver = alloc(fu_malik, m, s, m_soft_constraints); } diff --git a/src/opt/weighted_maxsat.cpp b/src/opt/weighted_maxsat.cpp index 6c4e99d7e..1d2aa22a6 100644 --- a/src/opt/weighted_maxsat.cpp +++ b/src/opt/weighted_maxsat.cpp @@ -253,6 +253,7 @@ namespace smt { disj.push_back(m.mk_not(m_min_cost_atom)); } if (is_optimal()) { + IF_VERBOSE(1, verbose_stream() << "(wmaxsat with lower bound: " << weight << "\n";); m_min_cost = weight; m_cost_save.reset(); m_cost_save.append(m_costs);