Module `Mc2_propositional`

Propositional Literal

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