package msat
Library containing a SAT solver that can be parametrized by a theory
Install
Dune Dependency
Authors
Maintainers
Sources
v0.8.tar.gz
md5=fe2f507bff99166ad2004786ca1ae59b
sha512=4cd653218e1767152c1d66700ccfc421d6d2da6ddffc8af4ee9151a3b5d25920f9d735a416f962227ffe458bb56e1f1977d180dd91415d37af9e1ea41dbb1045
doc/msat.backend/Msat_backend/Dot/index.html
Module Msat_backend.Dot
Source
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.clause
Provides 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.proof
Functor 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.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.
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>