# API Documentation

## Syntax

`Metatheory.Syntax.rewrite_rhs`

— Method`rewrite_rhs(expr::Expr)`

Rewrite the `expr`

by dealing with `:where`

if necessary. The `:where`

is rewritten from, for example, `~x where f(~x)`

to `f(~x) ? ~x : nothing`

.

`Metatheory.Syntax.rmlines`

— MethodRemove LineNumberNode from quoted blocks of code

`Metatheory.Syntax.@capture`

— Macro`@capture ex pattern`

Uses a `Rule`

object to capture an expression if it matches the `pattern`

. Returns `true`

and injects slot variable match results into the calling scope when the `pattern`

matches, otherwise returns false. The rule language for specifying the `pattern`

is the same in @capture as it is in `@rule`

. Contextual matching is not yet supported

```
julia> @syms a; ex = a^a;
julia> if @capture ex (~x)^(~x)
@show x
elseif @capture ex 2(~y)
@show y
end;
x = a
```

See also: `@rule`

`Metatheory.Syntax.@rule`

— Macro`@rule [SLOTS...] LHS operator RHS`

Creates an `AbstractRule`

object. A rule object is callable, and takes an expression and rewrites it if it matches the LHS pattern to the RHS pattern, returns `nothing`

otherwise. The rule language is described below.

LHS can be any possibly nested function call expression where any of the arugments can optionally be a Slot (`~x`

) or a Segment (`~x...`

) (described below).

SLOTS is an optional list of symbols to be interpeted as slots or segments directly (without using `~`

). To declare slots for several rules at once, see the `@slots`

macro.

If an expression matches LHS entirely, then it is rewritten to the pattern in the RHS , whose local scope includes the slot matches as variables. Segment (`~x`

) and slot variables (`~~x`

) on the RHS will substitute the result of the matches found for these variables in the LHS.

**Rule operators**:

`LHS => RHS`

: create a`DynamicRule`

. The RHS is*evaluated*on rewrite.`LHS --> RHS`

: create a`RewriteRule`

. The RHS is**not**evaluated but*symbolically substituted*on rewrite.`LHS == RHS`

: create a`EqualityRule`

. In e-graph rewriting, this rule behaves like`RewriteRule`

but can go in both directions. Doesn't work in classical rewriting`LHS ≠ RHS`

: create a`UnequalRule`

. Can only be used in e-graphs, and is used to eagerly stop the process of rewriting if LHS is found to be equal to RHS.

**Slot**:

A Slot variable is written as `~x`

and matches a single expression. `x`

is the name of the variable. If a slot appears more than once in an LHS expression then expression matched at every such location must be equal (as shown by `isequal`

).

*Example:*

Simple rule to turn any `sin`

into `cos`

:

```
julia> r = @rule sin(~x) --> cos(~x)
sin(~x) --> cos(~x)
julia> r(:(sin(1+a)))
:(cos((1 + a)))
```

A rule with 2 segment variables

```
julia> r = @rule sin(~x + ~y) --> sin(~x)*cos(~y) + cos(~x)*sin(~y)
sin(~x + ~y) --> sin(~x) * cos(~y) + cos(~x) * sin(~y)
julia> r(:(sin(a + b)))
:(cos(a)*sin(b) + sin(a)*cos(b))
```

A rule that matches two of the same expressions:

```
julia> r = @rule sin(~x)^2 + cos(~x)^2 --> 1
sin(~x) ^ 2 + cos(~x) ^ 2 --> 1
julia> r(:(sin(2a)^2 + cos(2a)^2))
1
julia> r(:(sin(2a)^2 + cos(a)^2))
# nothing
```

A rule without `~`

```
julia> r = @slots x y z @rule x(y + z) --> x*y + x*z
x(y + z) --> x*y + x*z
```

**Segment**: A Segment variable matches zero or more expressions in the function call. Segments may be written by splatting slot variables (`~x...`

).

*Example:*

```
julia> r = @rule f(~xs...) --> g(~xs...);
julia> r(:(f(1, 2, 3)))
:(g(1,2,3))
```

**Predicates**:

There are two kinds of predicates, namely over slot variables and over the whole rule. For the former, predicates can be used on both `~x`

and `~~x`

by using the `~x::f`

or `~~x::f`

. Here `f`

can be any julia function. In the case of a slot the function gets a single matched subexpression, in the case of segment, it gets an array of matched expressions.

The predicate should return `true`

if the current match is acceptable, and `false`

otherwise.

```
julia> two_πs(x::Number) = abs(round(x/(2π)) - x/(2π)) < 10^-9
two_πs (generic function with 1 method)
julia> two_πs(x) = false
two_πs (generic function with 2 methods)
julia> r = @rule sin(~~x + ~y::two_πs + ~~z) => :(sin($(Expr(:call, :+, ~~x..., ~~z...))))
sin(~(~x) + ~(y::two_πs) + ~(~z)) --> sin(+(~(~x)..., ~(~z)...))
julia> r(:(sin(a+$(3π))))
julia> r(:(sin(a+$(6π))))
:(sin(+a))
julia> r(sin(a+6π+c))
:(sin(a + c))
```

Predicate function gets an array of values if attached to a segment variable (`~x...`

).

For the predicate over the whole rule, use `@rule <LHS> => <RHS> where <predicate>`

:

```
julia> predicate(x) = x === a;
julia> r = @rule ~x => ~x where f(~x);
julia> r(a)
a
julia> r(b) === nothing
true
```

Note that this is syntactic sugar and that it is the same as `@rule ~x => f(~x) ? ~x : nothing`

.

**Compatibility**: Segment variables may still be written as (`~~x`

), and slot (`~x`

) and segment (`~x...`

or `~~x`

) syntaxes on the RHS will still substitute the result of the matches. See also: `@capture`

, `@slots`

`Metatheory.Syntax.@slots`

— Macro`@slots [SLOTS...] ex`

Declare SLOTS as slot variables for all `@rule`

or `@capture`

invocations in the expression `ex`

. *Example:*

```
julia> @slots x y z a b c Chain([
(@rule x^2 + 2x*y + y^2 => (x + y)^2),
(@rule x^a * y^b => (x*y)^a * y^(b-a)),
(@rule +(x...) => sum(x)),
])
```

`Metatheory.Syntax.@theory`

— Macro`@theory [SLOTS...] begin (LHS operator RHS)... end`

Syntax sugar to define a vector of rules in a nice and readable way. Can use `@slots`

or have the slots as the first arguments:

```
julia> t = @theory x y z begin
x * (y + z) --> (x * y) + (x * z)
x + y == (y + x)
#...
end;
```

Is the same thing as writing

```
julia> v = [
@rule x y z x * (y + z) --> (x * y) + (x * z)
@rule x y x + y == (y + x)
#...
];
```

## Patterns

`Metatheory.Patterns.AbstractPat`

— TypeAbstract type representing a pattern used in all the various pattern matching backends.

`Metatheory.Patterns.PatSegment`

— TypeIf you want to match a variable number of subexpressions at once, you will need a **segment pattern**. A segment pattern represents a vector of subexpressions matched. You can attach a predicate `g`

to a segment variable. In the case of segment variables `g`

gets a vector of 0 or more expressions and must return a boolean value.

`Metatheory.Patterns.PatTerm`

— TypeTerm patterns will match on terms of the same `arity`

and with the same function symbol `operation`

and expression head `exprhead`

.

`Metatheory.Patterns.PatVar`

— Type`PatVar{P}(name, debrujin_index, predicate::P)`

Pattern variables will first match on one subterm and instantiate the substitution to that subterm.

Matcher pattern may contain pattern variables with attached predicates, where `predicate`

is a function that takes a matched expression and returns a boolean value. Such a slot will be considered a match only if `f`

returns true.

`predicate`

can also be a `Type{<:t}`

, this predicate is called a type assertion. Type assertions on a `PatVar`

, will match if and only if the type of the matched term for the pattern variable is a subtype of `T`

.

`Metatheory.Patterns.isground`

— MethodA ground pattern contains no pattern variables and only literal values to match.

`Metatheory.Patterns.patvars`

— MethodCollects pattern variables appearing in a pattern into a vector of symbols

## Rules

`Metatheory.Rules.DynamicRule`

— TypeRules defined as `left_hand => right_hand`

are called `dynamic`

rules. Dynamic rules behave like anonymous functions. Instead of a symbolic substitution, the right hand of a dynamic `=>`

rule is evaluated during rewriting: matched values are bound to pattern variables as in a regular function call. This allows for dynamic computation of right hand sides.

Dynamic rule

`@rule ~a::Number * ~b::Number => ~a*~b`

`Metatheory.Rules.EqualityRule`

— TypeAn `EqualityRule`

can is a symbolic substitution rule that can be rewritten bidirectional. Therefore, it should only be used with the EGraphs backend.

`@rule ~a * ~b == ~b * ~a`

`Metatheory.Rules.RewriteRule`

— TypeRules defined as `left_hand --> right_hand`

are called *symbolic rewrite* rules. Application of a *rewrite* Rule is a replacement of the `left_hand`

pattern with the `right_hand`

substitution, with the correct instantiation of pattern variables. Function call symbols are not treated as pattern variables, all other identifiers are treated as pattern variables. Literals such as `5, :e, "hello"`

are not treated as pattern variables.

`@rule ~a * ~b --> ~b * ~a`

`Metatheory.Rules.UnequalRule`

— TypeThis type of *anti*-rules is used for checking contradictions in the EGraph backend. If two terms, corresponding to the left and right hand side of an *anti-rule* are found in an [`EGraph`

], saturation is halted immediately.

`!a ≠ a`

## Rules

## Rewriters

`Metatheory.Rewriters`

— ModuleA rewriter is any function which takes an expression and returns an expression or `nothing`

. If `nothing`

is returned that means there was no changes applicable to the input expression.

The `Rewriters`

module contains some types which create and transform rewriters.

`Empty()`

is a rewriter which always returns`nothing`

`Chain(itr)`

chain an iterator of rewriters into a single rewriter which applies each chained rewriter in the given order. If a rewriter returns`nothing`

this is treated as a no-change.`RestartedChain(itr)`

like`Chain(itr)`

but restarts from the first rewriter once on the first successful application of one of the chained rewriters.`IfElse(cond, rw1, rw2)`

runs the`cond`

function on the input, applies`rw1`

if cond returns true,`rw2`

if it retuns false`If(cond, rw)`

is the same as`IfElse(cond, rw, Empty())`

`Prewalk(rw; threaded=false, thread_cutoff=100)`

returns a rewriter which does a pre-order traversal of a given expression and applies the rewriter`rw`

. Note that if`rw`

returns`nothing`

when a match is not found, then`Prewalk(rw)`

will also return nothing unless a match is found at every level of the walk.`threaded=true`

will use multi threading for traversal.`thread_cutoff`

is the minimum number of nodes in a subtree which should be walked in a threaded spawn.`Postwalk(rw; threaded=false, thread_cutoff=100)`

similarly does post-order traversal.`Fixpoint(rw)`

returns a rewriter which applies`rw`

repeatedly until there are no changes to be made.`FixpointNoCycle`

behaves like`Fixpoint`

but instead it applies`rw`

repeatedly only while it is returning new results.`PassThrough(rw)`

returns a rewriter which if`rw(x)`

returns`nothing`

will instead return`x`

otherwise will return`rw(x)`

.

**Imports**

`Base`

`Base.Threads`

`Core`

`TermInterface`

`Metatheory.Rewriters.FixpointNoCycle`

— Type`FixpointNoCycle(rw)`

`FixpointNoCycle`

behaves like `Fixpoint`

, but returns a rewriter which applies `rw`

repeatedly until it produces a result that was already produced before, for example, if the repeated application of `rw`

produces results `a, b, c, d, b`

in order, `FixpointNoCycle`

stops because `b`

has been already produced.

## EGraphs

`Metatheory.EGraphs.EGraph`

— Type`mutable struct EGraph`

A concrete type representing an [`EGraph`

]. See the egg paper for implementation details.

**Fields**

`uf::IntDisjointSet`

stores the equality relations over e-class ids

`classes::Dict{Int64, EClass}`

map from eclass id to eclasses

`memo::Dict{AbstractENode, Int64}`

hashcons

`dirty::Vector{Int64}`

worklist for ammortized upwards merging

`root::Int64`

`analyses::Dict{Union{Function, Symbol}, Union{Function, Symbol}}`

A vector of analyses associated to the EGraph

`symcache::Dict{Any, Vector{Int64}}`

a cache mapping function symbols to e-classes that contain e-nodes with that function symbol.

`default_termtype::Type`

`termtypes::Dict{Tuple{Any, Int64}, Type}`

`numclasses::Int64`

`numnodes::Int64`

`needslock::Bool`

If we use global buffers we may need to lock. Defaults to true.

`buffer::Vector{Base.ImmutableDict{Int64, Tuple{Int64, Int64}}}`

Buffer for e-matching which defaults to a global. Use a local buffer for generated functions.

`merges_buffer::Vector{Tuple{Int64, Int64}}`

Buffer for rule application which defaults to a global. Use a local buffer for generated functions.

`lock::ReentrantLock`

`Metatheory.EGraphs.EGraph`

— Method`EGraph(expr)`

Construct an EGraph from a starting symbolic expression `expr`

.

**Signatures**

```
EGraph() -> EGraph
```

**Methods**

`EGraph()`

defined at `/home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/egraph.jl:212`

.

`Metatheory.EGraphs.EqualityGoal`

— Type`struct EqualityGoal <: SaturationGoal`

This goal is reached when the `exprs`

list of expressions are in the same equivalence class.

**Fields**

`exprs::Vector{Any}`

`ids::Vector{Int64}`

`Metatheory.EGraphs.FunctionGoal`

— Type`struct FunctionGoal <: SaturationGoal`

Boolean valued function as an arbitrary saturation goal. User supplied function must take an `EGraph`

as the only parameter.

**Fields**

`fun::Function`

`Metatheory.EGraphs.SaturationParams`

— Type`mutable struct SaturationParams`

Configurable Parameters for the equality saturation process.

**Fields**

`timeout::Int64`

`timelimit::UInt64`

Timeout in nanoseconds

`eclasslimit::Int64`

Maximum number of eclasses allowed

`enodelimit::Int64`

`goal::Union{Nothing, SaturationGoal}`

`stopwhen::Function`

`scheduler::Type{<:Metatheory.EGraphs.Schedulers.AbstractScheduler}`

`schedulerparams::Tuple`

`threaded::Bool`

`timer::Bool`

`Base.merge!`

— MethodGiven an `EGraph`

and two e-class ids, set the two e-classes as equal.

**Signatures**

```
merge!(g::EGraph, a::Int64, b::Int64) -> Int64
```

**Methods**

`merge!(g, a, b)`

defined at `/home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/egraph.jl:391`

.

`Metatheory.EGraphs.add!`

— MethodInserts an e-node in an `EGraph`

**Signatures**

```
add!(g::EGraph, n::AbstractENode) -> Int64
```

**Methods**

`add!(g, n)`

defined at `/home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/egraph.jl:315`

.

`Metatheory.EGraphs.addexpr!`

— MethodRecursively traverse an type satisfying the `TermInterface`

and insert terms into an `EGraph`

. If `e`

has no children (has an arity of 0) then directly insert the literal into the `EGraph`

.

**Signatures**

```
addexpr!(g::EGraph, se) -> Int64
```

**Methods**

`addexpr!(g, se)`

defined at `/home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/egraph.jl:365`

.

`addexpr!(g, ec)`

defined at `/home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/egraph.jl:382`

.

`Metatheory.EGraphs.analyze!`

— Method`analyze!(egraph, analysis_name, [ECLASS_IDS])`

Given an EGraph and an `analysis`

identified by name `analysis_name`

, do an automated bottom up trasversal of the EGraph, associating a value from the domain of analysis to each ENode in the egraph by the make function. Then, for each EClass, compute the join of the children ENodes analyses values. After `analyze!`

is called, an analysis value will be associated to each EClass in the EGraph. One can inspect and retrieve analysis values by using hasdata and getdata.

**Signatures**

```
analyze!(g::EGraph, analysis_ref, ids::Vector{Int64}) -> Bool
```

**Methods**

`analyze!(g, analysis_ref, ids)`

defined at `/home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/analysis.jl:61`

.

`Metatheory.EGraphs.astsize`

— MethodA basic cost function, where the computed cost is the size (number of children) of the current expression.

**Signatures**

```
astsize(n::ENodeTerm, g::EGraph) -> Any
```

**Methods**

`astsize(n, g)`

defined at `/home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/analysis.jl:98`

.

`Metatheory.EGraphs.astsize_inv`

— MethodA basic cost function, where the computed cost is the size (number of children) of the current expression, times -1. Strives to get the largest expression

**Signatures**

```
astsize_inv(n::ENodeTerm, g::EGraph) -> Any
```

**Methods**

`astsize_inv(n, g)`

defined at `/home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/analysis.jl:115`

.

`Metatheory.EGraphs.egraph_reconstruct_expression`

— MethodWhen extracting symbolic expressions from an e-graph, we need to instruct the e-graph how to rebuild expressions of a certain type. This function must be extended by the user to add new types of expressions that can be manipulated by e-graphs.

**Signatures**

```
egraph_reconstruct_expression(T::Type{Expr}, op, args) -> Expr
```

**Methods**

`egraph_reconstruct_expression(T, op, args)`

defined at `/home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/egraph.jl:534`

.

`Metatheory.EGraphs.eqsat_search!`

— MethodReturns an iterator of `Match`

es.

**Signatures**

```
eqsat_search!(g::EGraph, theory::Vector{<:AbstractRule}, scheduler::Metatheory.EGraphs.Schedulers.AbstractScheduler, report::Metatheory.EGraphs.SaturationReport) -> Int64
```

**Methods**

`eqsat_search!(g, theory, scheduler, report)`

defined at `/home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/saturation.jl:114`

.

`Metatheory.EGraphs.eqsat_step!`

— MethodCore algorithm of the library: the equality saturation step.

**Signatures**

```
eqsat_step!(g::EGraph, theory::Vector{<:AbstractRule}, curr_iter, scheduler::Metatheory.EGraphs.Schedulers.AbstractScheduler, params::SaturationParams, report) -> Any
```

**Methods**

`eqsat_step!(g, theory, curr_iter, scheduler, params, report)`

defined at `/home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/saturation.jl:257`

.

`Metatheory.EGraphs.extract!`

— MethodGiven a cost function, extract the expression with the smallest computed cost from an `EGraph`

**Signatures**

```
extract!(g::EGraph, costfun::Function) -> Any
```

**Methods**

`extract!(g, costfun)`

defined at `/home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/analysis.jl:163`

.

`Metatheory.EGraphs.find`

— MethodReturns the canonical e-class id for a given e-class.

**Signatures**

```
find(g::EGraph, a::Int64) -> Int64
```

**Methods**

`find(g, a)`

defined at `/home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/egraph.jl:272`

.

`Metatheory.EGraphs.instantiate_actual_param!`

— MethodInstantiate argument for dynamic rule application in e-graph

**Signatures**

```
instantiate_actual_param!(bindings::Base.ImmutableDict{Int64, Tuple{Int64, Int64}}, g::EGraph, i) -> Any
```

**Methods**

`instantiate_actual_param!(bindings, g, i)`

defined at `/home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/saturation.jl:194`

.

`Metatheory.EGraphs.islazy`

— Method`islazy(::Val{analysis_name})`

Should return `true`

if the EGraph Analysis `an`

is lazy and false otherwise. A *lazy* EGraph Analysis is computed only when analyze! is called. *Non-lazy* analyses are instead computed on-the-fly every time ENodes are added to the EGraph or EClasses are merged.

**Signatures**

**Methods**

`islazy(_)`

defined at `/home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/analysis.jl:14`

.

`islazy(analysis_name)`

defined at `/home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/analysis.jl:15`

.

`islazy(_)`

defined at `/home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/analysis.jl:135`

.

`Metatheory.EGraphs.join`

— Method`join(::Val{analysis_name}, a, b)`

Joins two analyses values into a single one, used by analyze! when two eclasses are being merged or the analysis is being constructed.

**Signatures**

```
join(analysis::Val{analysis_name}, a, b)
```

**Methods**

`join(analysis, a, b)`

defined at `/home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/analysis.jl:35`

.

`Metatheory.EGraphs.make`

— MethodWhen passing a function to analysis functions it is considered as a cost function

**Signatures**

```
make(f::Function, g::EGraph, n::AbstractENode) -> Tuple{AbstractENode, Any}
```

**Methods**

`make(f, g, n)`

defined at `/home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/analysis.jl:131`

.

`Metatheory.EGraphs.make`

— Method`make(::Val{analysis_name}, g, n)`

Given an ENode `n`

, `make`

should return the corresponding analysis value.

**Signatures**

**Methods**

`make(_, g, n)`

defined at `/home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/analysis.jl:44`

.

`Metatheory.EGraphs.modify!`

— Method`modify!(::Val{analysis_name}, g, id)`

The `modify!`

function for EGraph Analysis can optionally modify the eclass `g[id]`

after it has been analyzed, typically by adding an ENode. It should be **idempotent** if no other changes occur to the EClass. (See the egg paper).

**Signatures**

**Methods**

`modify!(_, g, id)`

defined at `/home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/analysis.jl:25`

.

`Metatheory.EGraphs.preprocess`

— MethodExtend this function on your types to do preliminary preprocessing of a symbolic term before adding it to an EGraph. Most common preprocessing techniques are binarization of n-ary terms and metadata stripping.

**Signatures**

```
preprocess(e::Expr) -> Any
```

**Methods**

`preprocess(e)`

defined at `/home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/egraph.jl:355`

.

`Metatheory.EGraphs.reachable`

— MethodRecursive function that traverses an `EGraph`

and returns a vector of all reachable e-classes from a given e-class id.

**Signatures**

```
reachable(g::EGraph, id::Int64) -> Vector{Int64}
```

**Methods**

`reachable(g, id)`

defined at `/home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/egraph.jl:501`

.

`Metatheory.EGraphs.rebuild!`

— MethodThis function restores invariants and executes upwards merging in an `EGraph`

. See the egg paper for more details.

**Signatures**

```
rebuild!(g::EGraph) -> Bool
```

**Methods**

`rebuild!(g)`

defined at `/home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/egraph.jl:426`

.

`Metatheory.EGraphs.saturate!`

— FunctionGiven an `EGraph`

and a collection of rewrite rules, execute the equality saturation algorithm.

**Signatures**

```
saturate!(g::EGraph, theory::Vector{<:AbstractRule}) -> Metatheory.EGraphs.SaturationReport
saturate!(g::EGraph, theory::Vector{<:AbstractRule}, params) -> Metatheory.EGraphs.SaturationReport
```

**Methods**

```
saturate!(g, theory)
saturate!(g, theory, params)
```

defined at `/home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/saturation.jl:286`

.

## EGraph Schedulers

`Metatheory.EGraphs.Schedulers.AbstractScheduler`

— Type`abstract type AbstractScheduler`

Represents a rule scheduler for the equality saturation process

**Fields**

`Metatheory.EGraphs.Schedulers.BackoffScheduler`

— Type`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{<:AbstractRule}`

`curr_iter::Int64`

`Metatheory.EGraphs.Schedulers.ScoredScheduler`

— Type`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{<:AbstractRule}`

`curr_iter::Int64`

`Metatheory.EGraphs.Schedulers.SimpleScheduler`

— Type`struct SimpleScheduler <: Metatheory.EGraphs.Schedulers.AbstractScheduler`

A simple Rewrite Scheduler that applies every rule every time

**Fields**

`Metatheory.EGraphs.Schedulers.cansaturate`

— FunctionShould return `true`

if the e-graph can be said to be saturated

`cansaturate(s::AbstractScheduler)`

**Signatures**

**Methods**

`cansaturate(s)`

defined at `/home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/Schedulers.jl:63`

.

`cansaturate(s)`

defined at `/home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/Schedulers.jl:120`

.

`cansaturate(s)`

defined at `/home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/Schedulers.jl:231`

.

`Metatheory.EGraphs.Schedulers.cansearch`

— FunctionShould return `false`

if the rule `r`

should be skipped

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

**Signatures**

**Methods**

`cansearch(s, r)`

defined at `/home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/Schedulers.jl:64`

.

`cansearch(s, r)`

defined at `/home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/Schedulers.jl:100`

.

`cansearch(s, r)`

defined at `/home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/Schedulers.jl:169`

.

`Metatheory.EGraphs.Schedulers.inform!`

— FunctionThis 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, r, n_matches)`

defined at `/home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/Schedulers.jl:68`

.

`inform!(s, rule, n_matches)`

defined at `/home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/Schedulers.jl:123`

.

`inform!(s, rule, n_matches)`

defined at `/home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/Schedulers.jl:234`

.