package ego

  1. Overview
  2. Docs

Parameters

module S : GRAPH_API with type 'p t = (Id.t L.shape, A.t, A.data, 'p) egraph and type analysis := A.t and type data := A.data and type 'a shape := 'a L.shape and type node := L.t

Signature

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

Represents the EGraph over which the analysis operates.

val make : ro t -> Id.t L.shape -> A.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 : A.t -> A.data -> A.data -> A.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.

OCaml

Innovation. Community. Security.