OptiMathSAT

Input Format

OptiMathSAT accepts two input formats:

• (v. >= 1.3.0) - the SMT-LIB v2 enriched with language extensions for dealing with optimization capabilities.
  Usage examples and a detailed documentation are made available.


• (v. >= 1.4.0) - a subset of the FlatZinc 1.6 language format.
  A usage reference is made available.

Configurations and command-line options

OptiMathSAT supports several options for controlling its behaviour and features in various ways.
The complete list of options can be obtained with the -help command-line switch.

References and Examples

OptiMathSAT shares with MathSAT 5 a great chunk of his API, which documentation is available at MathSAT 5 API, MathSAT 5 C API and MathSAT 5 Examples.

Here, we restrict our focus on OptiMathSAT specific API:

• OptiMathSAT C API Reference
• OptiMathSAT C API Examples


• OptiMathSAT Python API Examples [github]


• SMT-LIBv2 Extensions
• SMT-LIBv2 Examples


• FlatZinc 1.6 Reference

Linking the OptiMathSAT binary against different GMP and/or libc versions

The OptiMathSAT binary is linked with the Gnu Multiprecision Library (GMP) and (on Linux) the GNU C library (glibc), both covered by the GNU LGPL license. The executable provided in the distribution is linked statically, so as to avoid potential issues with library versions. However, a OptiMathSAT executable linked against a different version of GMP and/or libc can be obtained easily, by creating a main.c C file with the following content:

extern int msat_main(int argc, const char **argv);
int main(int argc, const char **argv) { return msat_main(argc, argv); }

and linking it against liboptimathsat.a, GMP and glibc. For example, using GCC this can be done as follows:

gcc main.c -o optimathsat lib/liboptimathsat.a -lgmpxx -lgmp