package qbf

  1. Overview
  2. Docs
On This Page
  1. a QBF formula
package qbf
Legend:
Library
Module
Module type
Parameter
Class
Class type

a QBF formula

The formula must already be prenex, i.e. it should be nested quantifiers with a quantifier-free formula inside.

type t = private
  1. | And of t list
  2. | Or of t list
  3. | Imply of t * t
  4. | XOr of t list
    (*

    exactly one element in the list is true

    *)
  5. | Equiv of t list
    (*

    all the elements are true, or all of them are false

    *)
  6. | True
  7. | False
  8. | Not of t
  9. | Atom of Lit.t
val true_ : t
val false_ : t
val and_l : t list -> t
val and_seq : t sequence -> t
val or_l : t list -> t
val or_seq : t sequence -> t
val xor_l : t list -> t
val equiv_l : t list -> t
val imply : t -> t -> t
val atom : Lit.t -> t
val neg : t -> t
val and_map : f:('a -> t) -> 'a sequence -> t

and_map f seq computes f x for each x in seq, and joins the resulting formulas with "and"

val or_map : f:('a -> t) -> 'a sequence -> t
val equal : t -> t -> bool
val compare : t -> t -> int
val hash : t -> int
val print : t printer
val print_with : pp_lit:Lit.t printer -> t printer
val simplify : t -> t

Simplifications

val cnf : ?gensym:(unit -> Lit.t) -> t -> CNF.t * Lit.t list

Convert the formula into a prenex-clausal normal form. This can use some Tseitin conversion, introducing new literals, to avoid the exponential blowup that can sometimes occur.

  • returns

    a pair of the CNF, and the list of newly created literals

  • parameter gensym

    a way to generate new literals to avoid exponential blowup. Default is Lit.fresh.