# 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

Innovation. Community. Security.

##### Ecosystem
Packages Community Events OCaml Planet Jobs
##### Policies
Carbon Footprint Governance Privacy Code of Conduct