package msat

  1. Overview
  2. Docs
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.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.

Sourcemodule type S = Backend_intf.S

Interface for exporting proofs.

Sourcemodule type Arg = sig ... end

Term printing for DOT

Sourcemodule 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.

Sourcemodule 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.

Sourcemodule 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.

OCaml

Innovation. Community. Security.