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