Add support for get-objectives

[Halbaroth]

No description provided.

[bclement-ocp]

We should use the (get-objectives) command supported by Z3 and OptiMathSAT and hence de-facto standard rather than a custom get-info flag.

[Gbury]

Does that mean that (get-objectives) is a statement that is commonly used along (minimize ...) and (maximize ...) ? If so I'll add it to the maxsmt extension in Dolmen. Also, if there are other statements commonly used for maxsmt, it'd be useful to know.

[bclement-ocp]

Does that mean that (get-objectives) is a statement that is commonly used along (minimize ...) and (maximize ...) ? If so I'll add it to the maxsmt extension in Dolmen.

ahem 😅

Also, if there are other statements commonly used for maxsmt, it'd be useful to know.

For Z3: Optmization and soft constraints

For OptiMathSAT: https://optimathsat.disi.unitn.it/pages/smt2reference.html

Those two are the solvers I know that implement MaxSMT extensions in the SMT-LIB format; the common ones are minimize, maximize, get-objectives and assert-soft which are those currently in Dolmen's MaxSMT extension.

[Gbury]

Does that mean that (get-objectives) is a statement that is commonly used along (minimize ...) and (maximize ...) ? If so I'll add it to the maxsmt extension in Dolmen.

ahem 😅

Point taken, I should sleep a bit more, :p