package msat

You can search for identifiers within the package.

in-package search v0.2.0

Library containing a SAT solver that can be parametrized by a theory

Install

Dune Dependency

github.com Readme Changelog Edit opam file Versions (16)

Authors

Maintainers

Sources

v0.8.3.tar.gz

md5=d13411fc725e3b53343f7c389560fbdf

sha512=8ecc179e61a695c69bba5014f10e8c80b4366bec365ffe7e3274ab3d7510388f91c792ce5e7950f50f44fb556a4b66aa3cc19a745a57eac1dd09c12a0081916b

doc/msat.backend/Msat_backend/Dot/Default/index.html

Module `Dot.Default`Source

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.

Parameters

module S : Msat.S

Signature

Sourceval print_atom : Format.formatter -> S.atom -> unit

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 : 
  S.clause ->
  string * string option * (Format.formatter -> unit -> unit) list

Source

val lemma_info : 
  S.clause ->
  string * string option * (Format.formatter -> unit -> unit) list

Source

val assumption_info : 
  S.clause ->
  string * string option * (Format.formatter -> unit -> unit) list

Generate 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:

rule is a name for the proof (arbitrary, does not need to be unique, but should rather be descriptive)
color is a color name (optional) understood by DOT
l is a list of printers that will be called to print some additional information

On This Page

Parameters
Signature

package msat

Install

Dune Dependency

Authors

Maintainers

Sources

doc/msat.backend/Msat_backend/Dot/Default/index.html

Module Dot.DefaultSource

Parameters

Signature

Module `Dot.Default`Source