package qbf

  1. Overview
  2. Docs
package qbf
Legend:
Library
Module
Module type
Parameter
Class
Class type

Bindings to Quantor

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

Solvers

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

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