package qbf

  1. Overview
  2. Docs

Module QbfSource

Bindings to Quantor

Sourcetype 'a printer = Format.formatter -> 'a -> unit
Sourcetype 'a sequence = ('a -> unit) -> unit
Sourcetype assignment =
  1. | True
  2. | False
  3. | Undef
Sourceval pp_assignment : assignment printer
Sourcetype quantifier =
  1. | Forall
  2. | Exists
Sourceval pp_quantifier : quantifier printer
Sourcemodule Lit : sig ... end
Sourcemodule CNF : sig ... end
Sourcemodule QCNF : sig ... end
Sourcemodule Formula : sig ... end
Sourcemodule QFormula : sig ... end

Solvers

Sourcetype result =
  1. | Unknown
  2. | Sat of Lit.t -> assignment
  3. | Unsat
  4. | Timeout
  5. | Spaceout
Sourceval pp_result : result printer
Sourcetype solver = {
  1. name : string;
  2. solve : QCNF.t -> result;
}
Sourceval solve : solver:solver -> QCNF.t -> result

Check whether the CNF formula is true (satisfiable) or false using the given solver