package mc2
A mcsat-based SMT solver in pure OCaml
Install
Dune Dependency
Authors
Maintainers
Sources
v0.1.tar.gz
md5=92de696251ec76fbf3eba6ee917fd80f
sha512=e88ba0cfc23186570a52172a0bd7c56053273941eaf3cda0b80fb6752e05d1b75986b01a4e4d46d9711124318e57cba1cd92d302e81d34f9f1ae8b49f39114f0
doc/mc2.backend/Mc2_backend/Dot/index.html
Module Mc2_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 :
Arg
with type atom := Mc2_core.Atom.t
and type hyp := Mc2_core.Clause.t
and type lemma := Mc2_core.Clause.t
and type assumption := Mc2_core.Clause.tProvides a reasonnable default to instantiate the Make functor, assuming the original printing functions are compatible with DOT html labels.
Source
module Make
(A :
Arg
with type atom := Mc2_core.Atom.t
and type hyp := Mc2_core.Clause.t
and type lemma := Mc2_core.Clause.t
and type assumption := Mc2_core.Clause.t) :
S with type t := Mc2_core.Proof.tFunctor for making a module to export proofs to the DOT format.