Data.Equality.Saturation.Scheduler

Definition of Scheduler as a way to control application of rewrite rules.

The BackoffScheduler is a scheduler which implements exponential rule backoff and is used by default in equalitySaturation

Documentation

class Scheduler s where

A Scheduler determines whether a certain rewrite rule is banned from being used based on statistics it defines and collects on applied rewrite rules.

Associated Types

data Stat s

Methods

updateStats

Arguments

:: s

The scheduler itself

-> Int

Iteration we're in

-> Int

Index of rewrite rule we're updating

-> Maybe (Stat s)

Current stat for this rewrite rule (we already got it so no point in doing a lookup again)

-> IntMap (Stat s)

The current stats map

-> [Match]

The list of matches resulting from matching this rewrite rule

-> IntMap (Stat s)

The updated map with new stats

Scheduler: update stats

isBanned

Arguments

:: Int

Iteration we're in

-> Stat s

Stats for the rewrite rule

-> Bool

Whether the rule should be applied or not

Instances

Scheduler BackoffScheduler

Defined in Data.Equality.Saturation.Scheduler

Associated Types

data Stat BackoffScheduler

Methods

updateStats :: BackoffScheduler -> Int -> Int -> Maybe (Stat BackoffScheduler) -> IntMap (Stat BackoffScheduler) -> [Match] -> IntMap (Stat BackoffScheduler)

isBanned :: Int -> Stat BackoffScheduler -> Bool

data BackoffScheduler

A Scheduler that implements exponentional 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.

Originaly in egg

Constructors

BackoffScheduler

Fields

• matchLimit :: !Int
• banLength :: !Int

Instances

Scheduler BackoffScheduler

Defined in Data.Equality.Saturation.Scheduler

Associated Types

data Stat BackoffScheduler

Methods

updateStats :: BackoffScheduler -> Int -> Int -> Maybe (Stat BackoffScheduler) -> IntMap (Stat BackoffScheduler) -> [Match] -> IntMap (Stat BackoffScheduler)

isBanned :: Int -> Stat BackoffScheduler -> Bool

Show (Stat BackoffScheduler)

Defined in Data.Equality.Saturation.Scheduler

Methods

showsPrec :: Int -> Stat BackoffScheduler -> ShowS

show :: Stat BackoffScheduler -> String

showList :: [Stat BackoffScheduler] -> ShowS

data Stat BackoffScheduler

Defined in Data.Equality.Saturation.Scheduler

data Stat BackoffScheduler = BSS {

• bannedUntil :: !Int
• timesBanned :: !Int

}

defaultBackoffScheduler :: BackoffScheduler

The default BackoffScheduler.

The match limit is set to 1000 and the ban length is set to 10.