Module `Msat_backend.Dot`

module type S = Backend_intf.S: Interface for exporting proofs.

module type Arg = sig ... end

module Default : functor (S : Msat.S) -> Arg with type atom := S.atom and type hyp := S.clause and type lemma := S.clause and type assumption := S.clause: Provides a reasonnable default to instantiate the Make functor, assuming the original printing functions are compatible with DOT html labels.

module Make : functor (S : Msat.S) -> functor (A : Arg with type atom := S.atom and type hyp := S.clause and type lemma := S.clause and type assumption := S.clause) -> S with type t := S.proof: Functor for making a module to export proofs to the DOT format.

module Simple : functor (S : Msat.S) -> functor (A : Arg with type atom := S.formula and type hyp = S.formula list and type lemma := S.lemma and type assumption = S.formula) -> S with type t := S.proof: Functor for making a module to export proofs to the DOT format. The substitution of the hyp type is non-destructive due to a restriction of destructive substitutions on earlier versions of ocaml.