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

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

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> :locallb LOWER
:localub UPPER
:id label)
; push max(TERM) with interval ]LOWER, UPPER]
; on the stack of objectives
(maximize <TERM> :locallb LOWER
:localub UPPER
:id label)
Notes:
 Local bounds are optional;
 In minimization, the lower bound is considered not strict whereas the upper bound is considered strict. Dual in maximization;
 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>
:locallb LOWER
:localub UPPER
:id label)
; push max(min(TERM_0), ..., min(TERM_N))
; with interval [LOWER, UPPER[ on the stack of objectives
(maxmin <TERM_0> ... <TERM_N>
:locallb LOWER
:localub UPPER
:id label)
Notes:
 Local bounds are optional;
 In minmax, the lower bound is considered strict whereas the upper bound is considered not strict. Dual in maxmin;
 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 POSITIVE_INTEGER
:dweight POSITIVE_FLOAT
:id MAXSMT_GROUP)
Notes:
 :weight and :dweight are mutually exclusive, if both are omitted the weight is assumed to be 1
 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.
(setmodel <INT>)
Notes:
 it can not be used after push/pop/assert instructions or when there are no objectives
The input problem must be given to OptiMathSAT on standard input:
~$ ./optimathsat < FILENAME.smt2
Local Bounds: an explanation.
Local 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 local 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 local 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 local bounds:
 In singleobjective and lexicographic optimization modes, the local bounds are equivalent to setting a global bound.
 In boxed multiobjective mode, each objective is considered as an independent problem. Therefore, the local bounds of
an objective do not affect the domain of other objectives in the same problem.