Module InvGenGraph

module InvGenGraph: sig .. end
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 
Set of terms.
type set = Term.TermSet.t 
val write_dot_to : string -> string -> string -> (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.