Library to deal with Quantified Boolean Formulas
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.
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
-fPICto work with OCaml).
It works with any version of OCaml from 4.08.x to 4.10.x onwards.
tested on linux (Ubuntu 16.04, x86_64),
tested on MacOS,
tested on Windows using Cygwin32 and Cygwin64 by cross-compilating to
native win32 under using the
Should also work under WSL and WSL2 on Windows 10.
The library and its dependencies are licensed under the BSD license
(and the MIT license for picosat), which is fairly permissive.
opam install qbf
opam install . --working-dir --deps-only dune build
process killed by signal -5is due to a dlopen problem: the binary has been
linked against the shared library
dllqbf-quantor_stubs.sobut this shared
lib isn't installed yet.
process killed by signal -10is still unknown. It was happening in
travis-ci. My workaround was to remove the travis-ci cache (~/.opam was
cached between two builds).