package ego

  1. Overview
  2. Docs

The module type ANALYSIS_OPS defines the main operations for an EClass analysis over an EGraph.

type 'a t

Represents the EGraph over which the analysis operates.

type analysis

Represents the persistent state of the analysis.

type node

Represents expressions of the language over which the analysis operates.

type data

Represents the additional analysis information that we will be attached to each EClass.

val make : ro t -> node -> data

make graph node returns the analysis data for node.

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 of d1 and d2 and a tuple indicating whether the result differs from d1 and or d2.

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.