package msat
Library containing a SAT solver that can be parametrized by a theory
Install
Dune Dependency
Authors
Maintainers
Sources
v0.8.3.tar.gz
md5=d13411fc725e3b53343f7c389560fbdf
sha512=8ecc179e61a695c69bba5014f10e8c80b4366bec365ffe7e3274ab3d7510388f91c792ce5e7950f50f44fb556a4b66aa3cc19a745a57eac1dd09c12a0081916b
doc/msat.backend/Msat_backend/Dot/index.html
Module Msat_backend.DotSource
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.
Interface for exporting proofs.
Source
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.
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.proofFunctor 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.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.