Module Mc2_core.TseitinSource

Tseitin CNF conversion

This modules implements Tseitin's Conjunctive Normal Form conversion, i.e. the ability to transform an arbitrary boolean formula into an equi-satisfiable CNF, that can then be fed to a SAT/SMT/McSat solver.

Sourcemodule type Arg = sig ... end

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

Sourcemodule type S = sig ... end

The exposed interface of Tseitin's CNF conversion.

Sourcemodule Make (F : Arg) : S with type atom = F.t

Tseitin's CNF conversion.