Module type Tseitin_intf.Arg

module type Arg = sig .. end

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.