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. 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.