package qbf

All checked builds pass
  1. Overview
  2. Docs
QBF solving in OCaml, including bindings to solvers

Install 

dune-project
 Dependency

github.com Readme Changelog Edit opam file Versions (2)

Authors

  1. S
    Simon Cruanes

Maintainers

  1. S
    Simon Cruanes <simon.cruanes@inria.fr>

Sources

qbf-0.3.tbz
sha256=2f6c085db501511cf34a76d763409b58cb05ea88bf77cc75fd486ddb83f51f0a
sha512=89fe7271671ea9c72ae87505a54d101f0b95c3374161305ac26177146559fcb7f61ad2f6d8ae9944f92185d5b85b19673cb4f8bfed43dbc2c772f9962717f73e

Description

Ocaml-qbf provides a unified API to several QBF solvers, along with common types for formulas, QCNF and literals and operations such as simplifications and reduction to CNF.

It packs:

  • a binding to quantor, which is shipped with the library
  • a binding to Depqbf

Tags

clib:quantor clib:qdpll clib:picosat

Added to opam-repository:

README

OCaml-QBF

Library to deal with Quantified Boolean Formulas in OCaml.

Linux, MacOS, Windows

ci

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.

  1. tested on linux (Ubuntu 16.04, x86_64),
  2. tested on MacOS,
  3. tested on Windows using Cygwin32 and Cygwin64 by cross-compilating to native win32 under using the mingw64-i686 (respectively mingw64-x86_64) cross-compiler.
  4. 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 library dllqbf-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).

Dependencies (2)

  1. dune >= "2.0"
  2. ocaml >= "4.08"

Dev Dependencies (2)

  1. odoc with-doc
  2. ounit with-test

Used by

None

Conflicts

None

Build status

Results of building qbf with each compiler on check.ci.ocaml.org, run of against opam-repository 7cdc698. All results for this package.

Each result links to its build log. To keep crawlers from overloading the site, build logs require a GitHub sign-in (see ocurrent/opam-health-check). On your first log, GitHub asks you to “Authorize opam-health-check”, the OCurrent app that runs these checks; it sees only your public profile, not your repositories. The sign-in lasts 30 days.

Version OCaml 4.11 OCaml 4.14 OCaml 5.2 OCaml 5.4 OCaml 5.5
0.3 (this version) good good good good good
  • good Package successfully built
  • partial One of the dependencies failed to build
  • bad Package failed to build
  • n/a Package is not available in this environment
  • internal Internal failure