To focus the search input from anywhere on the page, press the 'S' key.
in-package search v0.1.0
package msat
-
msat
-
-
msat.backend
-
-
msat.backtrack
-
msat.tseitin
Legend:
Library
Module
Module type
Parameter
Class
Class type
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.SInterface for exporting proofs.
module type Arg = sig ... endTerm 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.clauseProvides 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.proofFunctor 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.proofFunctor 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.