package ego

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Parameters
Signature

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 BuildRunner allows users to supply their own custom domain-specific scheduling strategies for equality saturation by supplying a corresponding Scheduling module satisfying SCHEDULER

Parameters

module S : 
  SCHEDULER
    with type 'a egraph := (Id.t L.shape, A.t, A.data, rw) egraph
     and type rule := Rule.t

Signature

val run_until_saturation : 
  ?scheduler:S.t ->
  ?node_limit:[ `Bounded of int | `Unbounded ] ->
  ?fuel:[ `Bounded of int | `Unbounded ] ->
  ?until:((Id.t L.shape, A.t, A.data, rw) egraph -> bool) ->
  (Id.t L.shape, A.t, A.data, rw) egraph ->
  Rule.t list ->
  bool

run_until_saturation ?scheduler ?node_limit ?fuel ?until graph rules repeatedly each one of the rewrites in rules according to the scheduler scheduler until no further changes occur (i.e equality saturation), or until it runs out of fuel (defaults to 30) or reaches some node_limit (defaults to 10_000) or some predicate until is satisfied.

It returns a boolean indicating whether it reached equality saturation or had to terminate early.