package msat

  1. Overview
  2. Docs

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 pp : Format.formatter -> t -> unit

Print the given formula.