# API Documentation

## Syntax

Metatheory.Syntax.rewrite_rhsMethod
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.

source
Metatheory.Syntax.@captureMacro
@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

source
Metatheory.Syntax.@ruleMacro
@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

source
Metatheory.Syntax.@slotsMacro
@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)),
])

See also: @rule, @capture

source
Metatheory.Syntax.@theoryMacro
@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)
#...
];
source

## Patterns

Metatheory.Patterns.PatSegmentType

If 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.

source
Metatheory.Patterns.PatVarType
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.

source

## Rules

Metatheory.Rules.DynamicRuleType

Rules 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
source
Metatheory.Rules.EqualityRuleType

An 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
source
Metatheory.Rules.RewriteRuleType

Rules 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
source
Metatheory.Rules.UnequalRuleType

This 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
source

## Rewriters

Metatheory.RewritersModule

A 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
source
Metatheory.Rewriters.FixpointNoCycleType
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.

source

## EGraphs

Metatheory.EGraphs.EGraphType
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

source
Metatheory.EGraphs.EGraphMethod
EGraph(expr)

Construct an EGraph from a starting symbolic expression expr.

Signatures

EGraph() -> EGraph


Methods

EGraph()
source
Metatheory.EGraphs.EqualityGoalType
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}

source
Metatheory.EGraphs.SaturationParamsType
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

• printiter::Bool

source
Base.merge!Method

Given 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)
source
Metatheory.EGraphs.addexpr!Method

Recursively 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; keepmeta) -> Int64


Methods

addexpr!(g, se; keepmeta)
addexpr!(g, ec; keepmeta)
source
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)
source
Metatheory.EGraphs.astsizeMethod

A 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)
source
Metatheory.EGraphs.astsize_invMethod

A 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)
source
Metatheory.EGraphs.egraph_reconstruct_expressionMethod

When 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; metadata, exprhead) -> Expr


Methods

egraph_reconstruct_expression(T, op, args; metadata, exprhead)
source
Metatheory.EGraphs.eqsat_search!Method

Returns an iterator of Matches.

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)
source
Metatheory.EGraphs.eqsat_step!Method

Core 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)
source
Metatheory.EGraphs.findMethod

Returns the canonical e-class id for a given e-class.

Signatures

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


Methods

find(g, a)
source
Metatheory.EGraphs.instantiate_actual_param!Method

Instantiate 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)
source
Metatheory.EGraphs.islazyMethod
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(_)
islazy(analysis_name)
islazy(_)
source
Metatheory.EGraphs.joinMethod
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)
source
Metatheory.EGraphs.makeMethod

When 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)
source
Metatheory.EGraphs.makeMethod
make(::Val{analysis_name}, g, n)

Given an ENode n, make should return the corresponding analysis value.

Signatures

Methods

make(_, g, n)
source
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)
source
Metatheory.EGraphs.preprocessMethod

Extend 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)
source
Metatheory.EGraphs.saturate!Function

Given 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)
source

## EGraph Schedulers

Metatheory.EGraphs.Schedulers.BackoffSchedulerType
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

source
Metatheory.EGraphs.Schedulers.ScoredSchedulerType
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

source
Metatheory.EGraphs.Schedulers.cansaturateFunction

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

cansaturate(s::AbstractScheduler)

Signatures

Methods

cansaturate(s)
cansaturate(s)
cansaturate(s)
source
Metatheory.EGraphs.Schedulers.cansearchFunction

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)
source
Metatheory.EGraphs.Schedulers.inform!Function

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, r, n_matches)
inform!(s, rule, n_matches)
inform!(s, rule, n_matches)
source