OptiMathSAT

An Optimization Modulo Theories (OMT) tool

SMT-LIBv2 Extensions

OptiMathSAT (>= 1.3.1) 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 

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 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 local bound: For maximization, the domain is dual: the lower bound is excluded, whereas the upper bound is included.
Interpretation of local bounds: