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/Default/index.html
Module Dot.DefaultSource
Provides a reasonnable default to instantiate the Make functor, assuming the original printing functions are compatible with DOT html labels.
Term printing for DOT
This module defines what functions are required in order to export a proof to the DOT format.
Print the contents of the given atomic formulas. WARNING: this function should take care to escape and/or not output special reserved characters for the dot format (such as quotes and so on).
Source
val hyp_info :
Mc2_core.Clause.t ->
string * string option * (Format.formatter -> unit -> unit) listSource
val lemma_info :
Mc2_core.Clause.t ->
string * string option * (Format.formatter -> unit -> unit) listSource
val assumption_info :
Mc2_core.Clause.t ->
string * string option * (Format.formatter -> unit -> unit) listGenerate some information about the leafs of the proof tree. Currently this backend print each lemma/assumption/hypothesis as a single leaf of the proof tree. These function should return a triplet (rule, color, l), such that:
ruleis a name for the proof (arbitrary, does not need to be unique, but should rather be descriptive)coloris a color name (optional) understood by DOTlis a list of printers that will be called to print some additional information