Module Basic.EGraph
val pp : ?pp_id:(Stdlib.Format.formatter -> Id.t -> unit) -> Stdlib.Format.formatter -> t -> unit
pp ?pp_id fmt graph
prints an internal representation of thegraph
.Note: This is primarily intended for debugging, and the output format is not guaranteed to remain consistent over versions.
val pp_dot : Stdlib.Format.formatter -> t -> unit
pp_dot fmt graph
pretty printsgraph
in a Graphviz format.
val init : unit -> t
init ()
creates a new EGraph.
val add_sexp : t -> Sexplib0.Sexp.t -> Id.t
add_sexp graph sexp
addssexp
tograph
and returns the equivalence class associated with term.
val to_dot : t -> Odot.graph
to_dot graph
convertsgraph
into a Graphviz representation.
val merge : t -> Id.t -> Id.t -> unit
merge graph id1 id2
merges the equivalence classes associated withid1
andid2
.Note: If you call
merge
manually, you must callrebuild
before running any queries or extraction.
val rebuild : t -> unit
rebuild graph
restores the internal invariants of the EGraphgraph
.Note: If you call
merge
manually, you must callrebuild
before running any queries or extraction.
val extract : ((Id.t -> float) -> (Symbol.t * Id.t list) -> float) -> t -> Id.t -> Sexplib0.Sexp.t
extract cost_fn graph
computes an extraction functionId.t -> Sexplib0.Sexp.t
to extract terms (specified byId.t
) from the EGraph.cost_fn f (sym,children)
should assign costs to the node with tagsym
and childrenchildren
- it can usef
to determine the cost of a child.
val apply_rules : t -> Rule.t list -> unit
apply_rules graph rules
runs each of the rewrites inrules
exactly once over the egraphgraph
and then returns.
val run_until_saturation : ?fuel:int -> t -> Rule.t list -> bool
run_until_saturation ?fuel graph rules
repeatedly each one of the rewrites inrules
until no further changes occur (i.e equality saturation), or until it runs out offuel
.It returns a boolean indicating whether it reached equality saturation or had to terminate early.