From b5335bc34be690c722e94192d4471c3894ab67da Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 13 Jan 2018 20:08:23 -0800 Subject: [PATCH] change behavior of single-objective pareto to use Pareto GIA algorithm (so not a good idea with MaxSAT solving, but then uniform behavior #1439 Signed-off-by: Nikolaj Bjorner --- src/opt/opt_context.cpp | 35 ++++++++++++++++------------------- 1 file changed, 16 insertions(+), 19 deletions(-) diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 0daf98320..f5f3f06fd 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -287,27 +287,24 @@ namespace opt { TRACE("opt", model_smt2_pp(tout, m, *m_model, 0);); m_optsmt.setup(*m_opt_solver.get()); update_lower(); + + opt_params optp(m_params); + symbol pri = optp.priority(); - switch (m_objectives.size()) { - case 0: - break; - case 1: - is_sat = execute(m_objectives[0], true, false); - break; - default: { - opt_params optp(m_params); - symbol pri = optp.priority(); - if (pri == symbol("pareto")) { - is_sat = execute_pareto(); - } - else if (pri == symbol("box")) { - is_sat = execute_box(); - } - else { - is_sat = execute_lex(); - } - break; + if (0 == m_objectives.size()) { + // no op } + else if (pri == symbol("pareto")) { + is_sat = execute_pareto(); + } + else if (1 == m_objectives.size()) { + is_sat = execute(m_objectives[0], true, false); + } + else if (pri == symbol("box")) { + is_sat = execute_box(); + } + else { + is_sat = execute_lex(); } return adjust_unknown(is_sat); }