An Optimization Modulo Theories (OMT) tool


Input Format

OptiMathSAT accepts two input formats:

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:

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