package msat

  1. Overview
  2. Docs
package msat
Legend:
Library
Module
Module type
Parameter
Class
Class type

Dot backend for proofs

This module provides functions to export proofs into the dot graph format. Graphs in dot format can be used to generates images using the graphviz tool.

module type S = Backend_intf.S

Interface for exporting proofs.

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

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.

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.