package ego

  1. Overview
  2. Docs
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.

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.t -> data

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

val guard_rule_usage : (Id.t L.shape, A.t, A.data, 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.