ego 0.0.6 (latest) · OCaml Package

This module defines the main interface to the EGraph provided by Ego.Basic.

type t

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

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 the graph.

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 prints graph 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 adds sexp to graph and returns the equivalence class associated with term.

val to_dot : t -> Odot.graph

to_dot graph converts graph into a Graphviz representation.

val 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.

val 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.

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.

val 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.

val 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.

package ego