SMTLIBv2 Extensions
OptiMathSAT (>= 1.6.0) accepts a modified version of
SMTLIBv2
input format, extended as follows:

An option to configure optimathsat to optimize in lexicographic, pareto or boxed mode when dealing with multiple
objectives:
; set boxed or lexicographic optimization
(setoption :opt.priority boxlexpareto)

A pair of commands to set a linear arithmetic term as a new objective:
; push min(TERM) with interval [LOWER, UPPER[
; on the stack of objectives
(minimize <TERM> :lower LOWER
:upper UPPER
:signed
:id label)
; push max(TERM) with interval ]LOWER, UPPER]
; on the stack of objectives
(maximize <TERM> :lower LOWER
:upper UPPER
:signed
:id label)
Notes:
 Bounds are optional;
 LOWER and UPPER are expected to be constantvalued terms of the same type of the objective function
 In minimization, the lower bound is considered not strict whereas the upper bound is considered strict. Dual in maximization;
 The signed flag is only used to mark a BV objective as signed
 Id is optional; useful for combining objectives or retrieving the model value

A pair of commands to define MinMax or MaxMin objectives over a list of linear arithmetic terms:
; push min(max(TERM_0), ..., max(TERM_N))
; with interval ]LOWER, UPPER] on the stack of objectives
(minmax <TERM_0> ... <TERM_N>
:lower LOWER
:upper UPPER
:signed
:id label)
; push max(min(TERM_0), ..., min(TERM_N))
; with interval [LOWER, UPPER[ on the stack of objectives
(maxmin <TERM_0> ... <TERM_N>
:lower LOWER
:upper UPPER
:signed
:id label)
Notes:
 Local bounds are optional;
 LOWER and UPPER are expected to be constantvalued terms of the same type of the objective function
 In minmax, the lower bound is considered strict whereas the upper bound is considered not strict. Dual in maxmin;
 The signed flag is only used to mark a BV objective as signed
 Id is optional; useful for combining objectives or retrieving the model value

A command to specify soft clauses for MaxSMT:
; Associate a cost weight to not satisfying TERM
; the equation of cost MAXSMT_GROUP
(assertsoft <TERM> :weight WEIGHT
:id MAXSMT_GROUP)
Notes:
 if :weight is omitted, it is assumed to be 1
 WEIGHT must be a constantvalued TERM of Real or Integer type
 if MAXSMT_GROUP is omitted, the cost is puhed inthe default group "I"
 In order to activate the MaxSMT group, the user should explicitly use the MAXSMT_GROUP label
within an objective to be minimized.

A command to load into OptiMathSAT environment the optimum model of a cost function:
; load into memory the optimum model of the
; objective at position N%size(objective_stack)
; N can be positive, negative or zero.
(loadobjectivemodel <INT>)
Notes:
 it can not be used when there are no objectives

A command to print the value of all objectives on the stack of objectives:
(getobjectives)
The input problem must be given to OptiMathSAT on standard input:
~$ ./optimathsat < FILENAME.smt2
Search bounds: an explanation.
Search bounds constitute optional supplementary information that the user can add to the input formula
to restrict the domain of satisfiable values for an objective.
OptiMathSAT can use search bounds to perform the optimization search in either binary or adaptivesearch modes.
For minimization, the user must provide at least the lower bound to use one of those search modes. Dual for maximization.
Domain effect of a bound:
 When a lower bound lb is set on a minimization objective, the bound lb is not excluded from the objective domain.
 When an upper bound ub is set on a minimization objective, the bound ub is excluded from the objective domain.
For maximization, the domain is dual: the lower bound is excluded, whereas the upper bound is included.
Interpretation of search bounds:
 In singleobjective, lexicographic and Pareto optimization modes, search bounds are equivalent to setting a global bound.
 In boxed multiobjective mode, each objective is considered as an independent problem. Therefore, the search bounds of
an objective do not affect the domain of other objectives in the same problem.
Pre1.5.0 Compatibility.
Prior to version 1.5.0, OptiMathSAT did not support the command
(getobjectives) and it had a nonstandardised
output format.
In order to use the previous output format with newer versions of OptiMathSAT, set the following option:
opt.output_format=old
In order to make OptiMathSAT print the value of all objectives after each
(checksat), without using the new
(getobjectives) command, set the following option:
opt.print_objectives=True
Pre1.6.0 Compatibility.
Prior to version 1.6.0, the command
(loadobjectivemodel ...) was named
(setmodel ...).