package ego

You can search for identifiers within the package.

in-package search v0.2.0

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

The module type SCHEDULER represents the definition of some scheduling system for ranking rule applications during equality saturation.

See Scheduler for some generic schedulers.

type 'p egraph

Represents an EGraph with read/write permissions 'p.

type t

Represents any persistent state of the scheduler that must be maintained separately to its rules.

type data

Represents metadata about a rule that the scheduler keeps track of in order to schedule rules.

type rule

Represents the type of rules over which this scheduler operates

val default : unit -> t

Create a default instance of the scheduler.

val should_stop : t -> int -> data Iter.t -> bool

should_stop scheduler iteration data is called whenever the EGraph reaches saturation (with the rules that have been scheduled), and should return whether further iterations should be run (i.e we will be trying a different schedule) or whether we have actually truly reached saturation.

val create_rule_metadata : t -> rule -> data

create_rule_metadata scheduler rule returns the initial metadata for a rule rule.

val guard_rule_usage : 
  rw egraph ->
  t ->
  data ->
  int ->
  (unit -> (Id.t * Id.t StringMap.t) Iter.t) ->
  (Id.t * Id.t StringMap.t) Iter.t

guard_rule_usage graph scheduler data iteration gen_matches is called before the execution of a particular rule (represented by the callback gen_matches), and should return a filtered set of matches according to the scheduling of the rule.