package ego

  1. Overview
  2. Docs

Parameter MakeAnalysisOps.S

type 'p t = (Id.t L.shape, A.t, A.data, 'p) egraph

Represents an EGraph with read permissions 'p.

val freeze : rw t -> ro t

freeze graph returns a read-only reference to the EGraph.

Note: it is safe to modify graph after passing it to freeze, this method is mainly intended to allow using the read-only APIs of the EGraph when you have a RW instance of the EGraph.

val class_equal : ro t -> Id.t -> Id.t -> bool

class_equal graph cls1 cls2 returns true if and only if cls1 and cls2 are congruent in the EGraph graph.

val iter_children : ro t -> Id.t -> Id.t L.shape Iter.t

iter_children graph cls returns an iterator over the children of the current EClass.

val set_data : rw t -> Id.t -> A.data -> unit

set_data graph cls data sets the analysis data for EClass cls in EGraph graph to be data.

val get_data : ro t -> Id.t -> A.data

get_data graph cls returns the analysis data for EClass cls in EGraph graph.

val get_analysis : rw t -> A.t

get_analysis graph returns the persistent analysis sate for an EGraph.

val add_node : rw t -> L.t -> Id.t

add_node graph term adds the term term into the EGraph graph and returns the corresponding equivalence class.

val merge : rw t -> Id.t -> Id.t -> unit

merge graph cls1 cls2 merges the two equivalence classes cls1 and cls2.