package msat
Library containing a SAT solver that can be parametrized by a theory
Install
Dune Dependency
Authors
Maintainers
Sources
v0.8.1.tar.gz
md5=70159e4db67c5b3118fd765c478ffac8
sha512=dc92ad406270bac92caf9451bfeef6e396f0fed3af7cab102c6d2d2e09cc256cbbf728c2025e1cf6d9662a3eb0425aad75fe7f41d9413dccf1d520b38f964ef1
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.