Module type Generic.ANALYSIS_OPS
The module type ANALYSIS_OPS
defines the main operations for an EClass analysis over an EGraph.
val make : ro t -> node -> data
make graph node
returns the analysis data fornode
.This function is called whenever a new node is added and should generate a new abstract value for the node, usually using the abstract values of its children.
Note: In terms of abstract interpretation, this function can be thought of the "abstraction" function, mapping concrete terms to their corresponding values in the abstract domain.
val merge : analysis -> data -> data -> data * (bool * bool)
merge st d1 d2
returns the analysis data that represents the combination ofd1
andd2
and a tuple indicating whether the result differs fromd1
and ord2
.This function is called whenever two equivalance classes are merged and should produce a new abstract value that represents the merge of their corresponding abstract values.
Note: In terms of abstract interpretation, this function can be thought of the least upper bound (lub), exposing the semi-lattice structure of the abstract domain.
val modify : rw t -> Id.t -> unit
modify graph class
is used to introduce new children of an equivalence class whenever new information about its elements is found by the analysis.This function is called whenever the children or abstract values of an eclass are modified and may use the abstract value of its to modify the egraph.
Note: In terms of abstract interpretation, this function can be thought of the "abstraction" function, mapping concrete terms to their corresponding values in the abstract domain.