package qbf

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

Module Qbf.FormulaSource

a QBF formula

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

Sourcetype 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
Sourceval true_ : t
Sourceval false_ : t
Sourceval and_l : t list -> t
Sourceval and_seq : t sequence -> t
Sourceval or_l : t list -> t
Sourceval or_seq : t sequence -> t
Sourceval xor_l : t list -> t
Sourceval equiv_l : t list -> t
Sourceval imply : t -> t -> t
Sourceval atom : Lit.t -> t
Sourceval neg : t -> t
Sourceval 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"

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

Simplifications

Sourceval 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.