An Optimization Modulo Theories (OMT) tool

SMT-LIBv2 Extensions

OptiMathSAT (>= 1.6.0) accepts a modified version of SMT-LIBv2 input format, extended as follows: 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 adaptive-search 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: For maximization, the domain is dual: the lower bound is excluded, whereas the upper bound is included.
Interpretation of search bounds:

Pre-1.5.0 Compatibility.

Prior to version 1.5.0, OptiMathSAT did not support the command (get-objectives) and it had a non-standardised output format.

In order to use the previous output format with newer versions of OptiMathSAT, set the following option:
In order to make OptiMathSAT print the value of all objectives after each (check-sat), without using the new (get-objectives) command, set the following option:

Pre-1.6.0 Compatibility.

Prior to version 1.6.0, the command (load-objective-model ...) was named (set-model ...).