Optimization Output

[PatrickTrentin88]

z3 version: 5bc4c9809e232d63f46018b200cb930bca993ce5

issue: z3 does not print the value of objective functions.

steps to reproduce:

The following formula:

(declare-fun x () Real)
(declare-fun y () Real)
(assert (<= (- 5) x))
(assert (<= x 5))
(assert (<= y 10))
(assert (<= (- 10) y))
(minimize x)
(maximize y)
(maximize (- x y))
(set-option:opt.priority box)
(check-sat)
(get-model)

produces the following output:

sat
(model 
  (define-fun y () Real
    (- 4.0))
  (define-fun x () Real
    (- 5.0))
)

whereas I would have expected something similar:

(objectives
  (x (- 5))
  (y 10)
  ((- x y) 15)
)
sat
(model 
  (define-fun y () Real
    (- 4.0))
  (define-fun x () Real
    (- 5.0))
)

Which is the output I was used to see when running z3.

Has anything changed in the source code? Am I doing something wrong?

[PatrickTrentin88]

I just found out that for some reasons z3 has changed output format and it now requires

(get-objectives)

to appear in the formula.

I am unsure why this change was introduced, but I think the issue can be closed.

note: if the command (get-objectives) is issued before any (check-sat), the error that is printed is somewhat confusing, perhaps it can be adjusted.

[NikolajBjorner]

It was changed because Levent Erkok pointed out that all other SMT-LIB2 commands print a single S-expression in response to a command. Printing both "sat" and the objectives would break this.

[PatrickTrentin88]

@NikolajBjorner so did you change the 'pareto-optimization' output as well?

[NikolajBjorner]

I believe it is addressed. Levent also pointed out that the output for Pareto fronts was not conformant, or you did. You have to call check-sat multiple times to get the different fronts.

[PatrickTrentin88]

Thanks for your explanation, I was not aware of these changes until now.

I assume that any assert/assert-soft/reset/push/pop/minimize/maximize command 'resets' the pareto search, is that correct? Are there any other actions that may cause the pareto search to start from scratch at the next 'check-sat'?