OCaml bindings for MathSAT 5
Most of MathSAT's functionality required for checking satisfiability and computing interpolants for linear rational/integer arithmetic is implemented.
Requires MathSAT 5 to be installed in a place where gcc and ld can find it (e.g., libmathsat.a in /usr/lib, and mathsat.h in /usr/include). Also requires MLGMPIDL and OUnit to be installed through ocamlfind.
makebuilds the library and runs unit testsmake docsbuilds documentationmake installinstalls the library though ocamlfind
- MathSAT 5 API reference
- MathSAT-ML Another set of OCaml bindings for MathSAT 5 (via Ctypes). Currently doesn't support static linking.