EGraph (p.ego.0.0.5.doc.ego.Ego.Basic.EGraph)

Sourcetype t

Represents a syntactic-rewrite-only EGraph that operates over Sexps.

val pp : 
  ?pp_id:(Format.formatter -> Id.t -> unit) ->
  Format.formatter ->
  t ->
  unit

pp ?pp_id fmt graph prints an internal representation of the graph.

Note: This is primarily intended for debugging, and the output format is not guaranteed to remain consistent over versions.

Sourceval pp_dot : Format.formatter -> t -> unit

pp_dot fmt graph pretty prints graph in a Graphviz format.

Sourceval init : unit -> t

init () creates a new EGraph.

Sourceval add_sexp : t -> Sexplib0.Sexp.t -> Id.t

add_sexp graph sexp adds sexp to graph and returns the equivalence class associated with term.

Sourceval to_dot : t -> Odot.graph

to_dot graph converts graph into a Graphviz representation.

Sourceval merge : t -> Id.t -> Id.t -> unit

merge graph id1 id2 merges the equivalence classes associated with id1 and id2.

Note: If you call merge manually, you must call rebuild before running any queries or extraction.

Sourceval rebuild : t -> unit

rebuild graph restores the internal invariants of the EGraph graph.

Note: If you call merge manually, you must call rebuild before running any queries or extraction.

Source

val extract : 
  ((Id.t -> float) -> (Symbol.t * Id.t list) -> float) ->
  t ->
  Id.t ->
  Sexplib0.Sexp.t

extract cost_fn graph computes an extraction function Id.t -> Sexplib0.Sexp.t to extract terms (specified by Id.t) from the EGraph.

cost_fn f (sym,children) should assign costs to the node with tag sym and children children - it can use f to determine the cost of a child.

Sourceval apply_rules : t -> Rule.t list -> unit

apply_rules graph rules runs each of the rewrites in rules exactly once over the egraph graph and then returns.

Sourceval run_until_saturation : ?fuel:int -> t -> Rule.t list -> bool

run_until_saturation ?fuel graph rules repeatedly each one of the rewrites in rules until no further changes occur (i.e equality saturation), or until it runs out of fuel.

It returns a boolean indicating whether it reached equality saturation or had to terminate early.