mc2.propositional
Mc2_propositional
mc2.backend
mc2.core
mc2.dimacs
mc2.lra
mc2.smtlib
mc2.uf
mc2.unin_sort
module F : Mc2_core.Tseitin.S with type atom := Mc2_core.atom
Formulas
val k_cnf : (?simplify:bool -> F.t -> Mc2_core.atom list list) Mc2_core.Service.Key.t
Service for computing CNF
val k_fresh : (unit -> Mc2_core.atom) Mc2_core.Service.Key.t
Service for making fresh terms
val plugin : Mc2_core.Plugin.Factory.t
Plugin providing boolean terms and the cnf service
cnf