MathSAT 5

Input Formats

The default input format for MathSAT is SMT-LIB v2. The solver accepts also SMT-LIBv1.2 and DIMACS. The input format can be selected with the -input command-line argument. In all cases, the input problem must be given on standard input.

Configurations and command-line options

MathSAT 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

• API Reference
• Low-level API Reference
• C API Example
• Examples for interacting with the solver via SMT-LIBv2 files
• Using a 3rd-party SAT solver with MathSAT
• NEW: PySMT, a high-level, solver-agnostic Python API for SMT
• For optimization examples, check out OptiMathSAT.

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

The MathSAT 5 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 MathSAT 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 libmathsat.a, GMP and glibc. For example, using GCC this can be done as follows:

gcc main.c -o mathsat lib/libmathsat.a -lgmpxx -lgmp