package ego

You can search for identifiers within the package.

in-package search v0.2.0

package ego

ego
- Ego
  - Basic
    
    EGraph
    
    Query
    
    Rule
    
    Symbol
  - Generic
    
    ANALYSIS
    
    ANALYSIS_OPS
    
    COST
    
    GRAPH_API
    
    LANGUAGE
    
    Make
    
    A
    
    BuildRunner
    
    S
    
    L
    
    MakeAnalysisOps
    
    S
    
    Rule
    
    MakeExtractor
    
    E
    
    L
    
    MakePrinter
    
    A
    
    L
    
    Query
    
    RULE
    
    SCHEDULER
    
    Scheduler
    
    Backoff
    
    Simple
  - Id

Legend:
Library
Module
Module type
Parameter
Class
Class type

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.