Module Make.BuildRunner
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
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 inrules
according to the schedulerscheduler
until no further changes occur (i.e equality saturation), or until it runs out offuel
(defaults to 30) or reaches somenode_limit
(defaults to 10_000) or some predicateuntil
is satisfied.It returns a boolean indicating whether it reached equality saturation or had to terminate early.