Dot (u.e48875f008bd120f24d497e3f3fa21b2.msat.0.8.3.doc.msat.backend.Msat

Sourcemodule type S = Backend_intf.S

Interface for exporting proofs.

Sourcemodule type Arg = sig ... end

Term printing for DOT

module Default
  (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.

Source

module Make
  (S : Msat.S)
  (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.

Source

module Simple
  (S : Msat.S)
  (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.