Module type Tseitin.Arg

module type Arg = Tseitin_intf.Arg

The implementation of formulas required to implement Tseitin's CNF conversion.

Formulas

This defines what is needed of formulas in order to implement Tseitin's CNF conversion.

type t

Type of atomic formulas.

val neg : t -> t

Negation of atomic formulas.

val fresh : unit -> t

Generate fresh formulas (that are different from any other).

val print : Format.formatter -> t -> unit

Print the given formula.