package ego

  1. Overview
  2. Docs

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.