Module InvGenGraph

Graph representing equivalence classes and ordering between some terms.

There's one graph module per domain we are interested in: bool, int and real. They're generated by a common functor using the domains from InvGenDomain.

module Lsd = LockStepDriver

LSD module.

type term = Term.t

Term.

type 'a map = 'a Term.TermHashtbl.t

Maps terms to something.

type set = Term.TermSet.t

Set of terms.

val write_dot_to : string -> string -> string -> (Stdlib.Format.formatter -> 'a -> unit) -> 'a -> unit

write_dot_to path name suff fmt graph Writes a graph in graphviz to file <path>/<name>_<suff>.dot.

module type Graph = sig ... end

Signature of the modules created by the graph functor.

module Bool : Graph

Graph of booleans with implication.

module Int : Graph

Graph of integers with less than or equal.

module BV (L : sig ... end) : Graph

Graph of signed bitvectors with less than or equal.

module UBV (L : sig ... end) : Graph

Graph of unsigned bitvectors with less than or equal.

module Real : Graph

Graph of reals with less than or equal.

module EqOnly : sig ... end

Graph modules for equivalence only.