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

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.

pp_dot fmt graph pretty prints graph in a Graphviz format.

init () creates a new EGraph.

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

to_dot graph converts graph into a Graphviz representation.

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.

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.

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.

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

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.