maelvls / ocaml-qbf

OCaml bindings to QBF solver(s)

OCaml-QBF

Library to deal with Quantified Boolean Formulas in OCaml.

Linux, MacOS	Windows

Organization

• The main library, qbf, contains types and functions to deal with representing boolean literals and quantified formulas, as well as a generic interface for solvers.
• A sub-library, qbf.quantor, contains a binding to the quantor QBF solver. The solver itself and Picosat (version 535) are packaged with the library for convenience (they are rarely packaged on distributions, and require some compilation options such as -fPIC to work with OCaml).

Tested configurations

It works with any version of OCaml from 3.12.1 to 4.04.0 onwards.

1. tested on linux (Ubuntu 16.04, x86_64),
2. tested on MacOS,
3. on windows, the cross-compilation to native win32 under cygwin works fine using the mingw64-i686 cross-compiler. It does not work with the x86_64 compiler¹. Should also work under windows-bash for windows 10.

License

The library and its dependencies are licensed under the BSD license (and the MIT license for picosat), which is fairly permissive.

Installation

Please use opam (after the first release is done).

Footnotes

1. This is a bug in quantor's ./configure. When testing the size of a word, windows uses unsigned long long but this option is not checked (only unsigned long and unsigned). ↩