package mc2

  1. Overview
  2. Docs

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

Plugin providing boolean terms and the cnf service