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.

Maps terms to something.

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

Maps terms to something.

Set of terms.

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 Real : Graph: Graph of reals with less than or equal.

module EqOnly : sig ... end: Graph modules for equivalence only.