SMTLIBv2 Extensions
Note: OptiMathSAT now requires
optimization=true to be set in order to use the
optimization interface. If that option is not set, OptiMathSAT
behaves as MathSAT.
OptiMathSAT (>= 1.7.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)
; on the stack of objectives
(minimize <TERM>
:signed
:id label)
; push max(TERM)
; on the stack of objectives
(maximize <TERM>
:signed
:id label)
Notes:
 The (optional) signed flag is only used to mark a BV objective as signed
 The (optional) id is 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))
; on the stack of objectives
(minmax <TERM_0> ... <TERM_N>
:signed
:id label)
; push max(min(TERM_0), ..., min(TERM_N))
; on the stack of objectives
(maxmin <TERM_0> ... <TERM_N>
:signed
:id label)
Notes:
 The (optional) signed flag is only used to mark a BV objective as signed
 The (optional) id is 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