package qbf

  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

doc/qbf.quantor/Quantor/Raw/index.html

Module Quantor.RawSource

Sourcetype t

Encapsulated solver

Sourceval create : unit -> t

Allocate a new QBF solver

Sourceval sat : t -> Qbf.result

Current status of the solver

Sourceval scope : t -> Qbf.quantifier -> unit

Open a new scope with the given kind of quantifier

Sourceval add : t -> lit -> unit

Add a literal, or end the current clause/scope with 0

Sourceval deref : t -> lit -> Qbf.assignment

Obtain the value of this literal in the current model