Module Mc2_core.Tseitin
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.
module type Arg = Mc2_core__.Tseitin_intf.Arg
The implementation of formulas required to implement Tseitin's CNF conversion.
module type S = Mc2_core__.Tseitin_intf.S
The exposed interface of Tseitin's CNF conversion.