Parameter BuildRunner.1-S
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 -> data
create_rule_metadata scheduler rule
returns the initial metadata for a rulerule
.
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 callbackgen_matches
), and should return a filtered set of matches according to the scheduling of the rule.