package qbf

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

a QBF formula

package qbf

qbf
- Qbf
  - CNF
  - Formula
  - Lit
  - QCNF
  - QFormula
qbf.quantor
- Quantor
  - Raw

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

| And of t list
| Or of t list
| Imply of t * t
| XOr of t list
(*
exactly one element in the list is true
*)
| Equiv of t list
(*
all the elements are true, or all of them are false
*)
| True
| False
| Not of t
| 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.