msat

Library containing a SAT solver that can be parametrized by a theory
package msat
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library msat.backend
Module Msat_backend . Dot
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.