package ego

  1. Overview
  2. Docs

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


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


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,, rw) egraph -> bool) -> (Id.t L.shape, A.t,, 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.


Innovation. Community. Security.