Scheduling for E-Graph rewriting

abstract type AbstractScheduler

Represents a rule scheduler for the equality saturation process

Fields

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::Dict{Rule,Metatheory.EGraphs.Schedulers.BackoffSchedulerEntry}

• G::EGraph

• theory::Array{var"#s309",1} where var"#s309"<:Rule

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::Dict{Rule,Metatheory.EGraphs.Schedulers.ScoredSchedulerEntry}

• G::EGraph

• theory::Array{var"#s309",1} where var"#s309"<:Rule

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

Signatures

cansaturate(s::Metatheory.EGraphs.Schedulers.AbstractScheduler) -> Bool

Methods

cansaturate(s)

cansaturate(s)

cansaturate(s)

cansaturate(s)

This function is called before pattern matching on the e-graph

Signatures

readstep!(s::Metatheory.EGraphs.Schedulers.AbstractScheduler)

Methods

readstep!(s)

readstep!(s)

readstep!(s)

readstep!(s)

Should return true if the rule r should be skipped

Signatures

shouldskip(s::Metatheory.EGraphs.Schedulers.AbstractScheduler, r::Rule) -> Bool

Methods

shouldskip(s, r)

shouldskip(s, r)

shouldskip(s, r)

shouldskip(s, r)

This function is called after pattern matching on the e-graph

Signatures

writestep!(s::Metatheory.EGraphs.Schedulers.AbstractScheduler, r::Rule) -> Union{Nothing, Int64}

Methods

writestep!(s, r)

writestep!(s, rule)

writestep!(s, rule)

writestep!(s, r)