package msat
Library containing a SAT solver that can be parametrized by a theory
Install
Dune Dependency
Authors
Maintainers
Sources
v0.9.tar.gz
md5=8ee967a889188d8d937e3c1ca2c50deb
sha512=5185e02f2f41a3672afaf64b47ddf6efd787811a73f0286a670a64783a86a9c422c4a874c48884622961354105283b60223562025f1fa21edba67f0eb8cb172b
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.