From e307c5fddabe9813c84d4d5086e819cd9ed3655a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 7 Dec 2013 14:47:47 -0800 Subject: [PATCH] fix minimize->maxsat Signed-off-by: Nikolaj Bjorner --- src/opt/opt_context.cpp | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 52ae1e38e..2d1b9c268 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -221,7 +221,18 @@ namespace opt { if (is_minimize(fml, term, index)) { TRACE("opt", tout << "try to convert minimization" << mk_pp(term, m) << "\n";); rational coeff(0); - return get_pb_sum(term, terms, weights, coeff); + // minimize 2*x + 3*y + // <=> + // (assret-soft (not x) 2) + // (assert-soft (not y) 3) + // + if (get_pb_sum(term, terms, weights, coeff) && coeff.is_zero()) { + // TBD: and weights are positive? + for (unsigned i = 0; i < terms.size(); ++i) { + terms[i] = m.mk_not(terms[i].get()); + } + return true; + } } return false; }