Scheduling for E-Graph rewriting

abstract type AbstractScheduler

Represents a rule scheduler for the equality saturation process

Fields

mutable struct BackoffScheduler <: Metatheory.EGraphs.Schedulers.AbstractScheduler

A Rewrite Scheduler that implements exponential rule backoff. For each rewrite, there exists a configurable initial match limit. If a rewrite search yield more than this limit, then we ban this rule for number of iterations, double its limit, and double the time it will be banned next time.

This seems effective at preventing explosive rules like associativity from taking an unfair amount of resources.

Fields

• data::IdDict{AbstractRule, Metatheory.EGraphs.Schedulers.BackoffSchedulerEntry}

• G::EGraph

• theory::Vector{var"#s618"} where var"#s618"<:AbstractRule

• curr_iter::Int64

mutable struct ScoredScheduler <: Metatheory.EGraphs.Schedulers.AbstractScheduler

A Rewrite Scheduler that implements exponential rule backoff. For each rewrite, there exists a configurable initial match limit. If a rewrite search yield more than this limit, then we ban this rule for number of iterations, double its limit, and double the time it will be banned next time.

This seems effective at preventing explosive rules like associativity from taking an unfair amount of resources.

Fields

• data::IdDict{AbstractRule, Metatheory.EGraphs.Schedulers.ScoredSchedulerEntry}

• G::EGraph

• theory::Vector{var"#s618"} where var"#s618"<:AbstractRule

• curr_iter::Int64

struct SimpleScheduler <: Metatheory.EGraphs.Schedulers.AbstractScheduler

A simple Rewrite Scheduler that applies every rule every time

Fields

Should return true if the e-graph can be said to be saturated

cansaturate(s::AbstractScheduler)

Signatures

Methods

cansaturate(s)

cansaturate(s)

cansaturate(s)

Should return false if the rule r should be skipped

cansearch(s::AbstractScheduler, r::Rule)

Signatures

Methods

cansearch(s, r)

cansearch(s, r)

cansearch(s, r)

This function is called after pattern matching on the e-graph, informs the scheduler about the yielded matches. Returns false if the matches should not be yielded and ignored.

inform!(s::AbstractScheduler, r::AbstractRule, n_matches)

Signatures

Methods

inform!(s, rule, n_matches)

inform!(s, rule, n_matches)

inform!(s, r, n_matches)