mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
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 <nbjorner@microsoft.com>
This commit is contained in:
parent
450f3c9b45
commit
b5335bc34b
|
@ -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);
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue