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 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 themingw64-i686
(respectivelymingw64-x86_64
)
cross-compiler.Should also work under WSL and WSL2 on 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
Using opam:
opam install qbf
From source:
opam install . --working-dir --deps-only
dune build
Known issues
process killed by signal -5
is due to a dlopen problem: the binary has been
linked against the shared librarydllqbf-quantor_stubs.so
but this shared
lib isn't installed yet.process killed by signal -10
is still unknown. It was happening in
travis-ci. My workaround was to remove the travis-ci cache (~/.opam was
cached between two builds).
sha256=2f6c085db501511cf34a76d763409b58cb05ea88bf77cc75fd486ddb83f51f0a
sha512=89fe7271671ea9c72ae87505a54d101f0b95c3374161305ac26177146559fcb7f61ad2f6d8ae9944f92185d5b85b19673cb4f8bfed43dbc2c772f9962717f73e