package msat

  1. Overview
  2. Docs


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

Print the given formula.


Innovation. Community. Security.