API Documentation
Syntax
Metatheory.Syntax.rewrite_rhs
— Methodrewrite_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.@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 aDynamicRule
. The RHS is evaluated on rewrite.LHS --> RHS
: create aRewriteRule
. The RHS is not evaluated but symbolically substituted on rewrite.LHS == RHS
: create aEqualityRule
. In e-graph rewriting, this rule behaves likeRewriteRule
but can go in both directions. Doesn't work in classical rewritingLHS ≠ RHS
: create aUnequalRule
. 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
— MacroMetatheory.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
— TypePatVar{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 returnsnothing
Chain(itr)
chain an iterator of rewriters into a single rewriter which applies each chained rewriter in the given order. If a rewriter returnsnothing
this is treated as a no-change.RestartedChain(itr)
likeChain(itr)
but restarts from the first rewriter once on the first successful application of one of the chained rewriters.IfElse(cond, rw1, rw2)
runs thecond
function on the input, appliesrw1
if cond returns true,rw2
if it retuns falseIf(cond, rw)
is the same asIfElse(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 rewriterrw
. Note that ifrw
returnsnothing
when a match is not found, thenPrewalk(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 appliesrw
repeatedly until there are no changes to be made.FixpointNoCycle
behaves likeFixpoint
but instead it appliesrw
repeatedly only while it is returning new results.PassThrough(rw)
returns a rewriter which ifrw(x)
returnsnothing
will instead returnx
otherwise will returnrw(x)
.
Imports
Base
Base.Threads
Core
TermInterface
Metatheory.Rewriters.FixpointNoCycle
— TypeFixpointNoCycle(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.AbstractAnalysis
— Typeabstract type AbstractAnalysis
Abstract type representing an EGraph
analysis, attaching values from a join semi-lattice domain to an EGraph
Fields
Metatheory.EGraphs.EGraph
— Typemutable 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}
dirty::Vector{Int64}
worklist for ammortized upwards merging
root::Int64
analyses::Set{Type{var"#s631"} where var"#s631"<:AbstractAnalysis}
A vector of analyses associated to the EGraph
default_termtype::Type
termtypes::Dict{Tuple{Any, Int64}, Type}
numclasses::Int64
numnodes::Int64
Metatheory.EGraphs.EGraph
— MethodEGraph(expr)
Construct an EGraph from a starting symbolic expression expr
.
Signatures
EGraph() -> EGraph
Methods
EGraph()
Metatheory.EGraphs.EqualityGoal
— Typestruct 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.ExtractionAnalysis
— TypeAn AbstractAnalysis
that computes the cost of expression nodes and chooses the node with the smallest cost for each E-Class. This abstract type is parametrised by a function F. This is useful for the analysis storage in EClass
Metatheory.EGraphs.FunctionGoal
— Typestruct 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
— Typemutable struct SaturationParams
Configurable Parameters for the equality saturation process.
Fields
timeout::Int64
Default: 8
timelimit::Dates.Period
Default: Second(-1)
matchlimit::Int64
Default: 5000
eclasslimit::Int64
Default: 5000
enodelimit::Int64
Default: 15000
goal::Union{Nothing, SaturationGoal}
Default: nothing
stopwhen::Function
Default: ()->begin #= /juliateam/.julia/packages/Metatheory/CTXnY/src/EGraphs/saturation.jl:71 =# false end
scheduler::Type{var"#s631"} where var"#s631"<:Metatheory.EGraphs.Schedulers.AbstractScheduler
Default: BackoffScheduler
schedulerparams::Tuple
Default: ()
threaded::Bool
Default: false
timer::Bool
Default: true
printiter::Bool
Default: false
simterm::Function
Default: similarterm
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)
Metatheory.EGraphs.add!
— MethodInserts an e-node in an EGraph
Signatures
add!(g::EGraph, n::AbstractENode) -> EClass
Methods
add!(g, n)
Metatheory.EGraphs.addexpr!
— MethodMetatheory.EGraphs.analyze!
— Methodanalyze!(egraph, analysis, [ECLASS_IDS])
Given an EGraph and an analysis
of type <:AbstractAnalysis
, 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. Note that an EGraph can only contain one analysis of type an
.
Signatures
analyze!(g::EGraph, an::Type{var"#s505"} where var"#s505"<:AbstractAnalysis, ids::Vector{Int64}) -> Bool
Methods
analyze!(g, an, ids)
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, an::Type{var"#s506"} where var"#s506"<:AbstractAnalysis) -> Any
Methods
astsize(n, g, an)
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, an::Type{var"#s506"} where var"#s506"<:AbstractAnalysis) -> Any
Methods
astsize_inv(n, g, an)
Metatheory.EGraphs.eqsat_search!
— MethodReturns an iterator of Match
es.
Signatures
eqsat_search!(egraph::EGraph, theory::Vector{var"#s502"} where var"#s502"<:AbstractRule, scheduler::Metatheory.EGraphs.Schedulers.AbstractScheduler, report; threaded) -> Base.Iterators.Flatten{Vector{Vector{Metatheory.EGraphs.Match}}}
Methods
eqsat_search!(egraph, theory, scheduler, report; threaded)
Metatheory.EGraphs.eqsat_step!
— MethodCore algorithm of the library: the equality saturation step.
Signatures
eqsat_step!(g::EGraph, theory::Vector{var"#s630"} where var"#s630"<:AbstractRule, curr_iter, scheduler::Metatheory.EGraphs.Schedulers.AbstractScheduler, match_hist::Vector{Metatheory.EGraphs.Match}, params::SaturationParams, report) -> Tuple{Any, EGraph}
Methods
eqsat_step!(g, theory, curr_iter, scheduler, match_hist, params, report)
Metatheory.EGraphs.extract!
— MethodGiven a cost function, extract the expression with the smallest computed cost from an EGraph
Signatures
extract!(g::EGraph, costfun::Function; root, simterm) -> Any
Methods
extract!(g, costfun; root, simterm)
Metatheory.EGraphs.extract!
— MethodGiven an ExtractionAnalysis
, extract the expression with the smallest computed cost from an EGraph
Signatures
extract!(g::EGraph, a::Type{ExtractionAnalysis{F}} where F; root, simterm) -> Any
Methods
extract!(g, a; root, simterm)
Metatheory.EGraphs.islazy
— Methodislazy(an::Type{<:AbstractAnalysis})
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
islazy(an::Type{var"#s630"} where var"#s630"<:AbstractAnalysis) -> Bool
Methods
islazy(an)
islazy(a)
Metatheory.EGraphs.join
— Methodjoin(an::Type{<:AbstractAnalysis}, 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::Type{var"#s630"} where var"#s630"<:AbstractAnalysis, a, b) -> Any
Methods
join(analysis, a, b)
join(a, from, to)
Metatheory.EGraphs.make
— Methodmake(an::Type{<:AbstractAnalysis}, g, n)
Given an ENode n
, make
should return the corresponding analysis value.
Signatures
make(analysis::Type{var"#s630"} where var"#s630"<:AbstractAnalysis, g, n) -> Tuple{AbstractENode, Any}
Methods
make(analysis, g, n)
make(a, g, n)
Metatheory.EGraphs.modify!
— Methodmodify!(an::Type{<:AbstractAnalysis}, 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
modify!(analysis::Type{var"#s630"} where var"#s630"<:AbstractAnalysis, g, id)
Methods
modify!(analysis, g, id)
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)
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)
Metatheory.EGraphs.rebuild!
— MethodMetatheory.EGraphs.saturate!
— FunctionGiven an EGraph
and a collection of rewrite rules, execute the equality saturation algorithm.
Signatures
saturate!(g::EGraph, theory::Vector{var"#s505"} where var"#s505"<:AbstractRule) -> Metatheory.EGraphs.Report
saturate!(g::EGraph, theory::Vector{var"#s504"} where var"#s504"<:AbstractRule, params) -> Metatheory.EGraphs.Report
Methods
saturate!(g, theory)
saturate!(g, theory, params)
EGraph Schedulers
Metatheory.EGraphs.Schedulers.AbstractScheduler
— Typeabstract type AbstractScheduler
Represents a rule scheduler for the equality saturation process
Fields
Metatheory.EGraphs.Schedulers.BackoffScheduler
— Typemutable 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"#s631"} where var"#s631"<:AbstractRule
curr_iter::Int64
Metatheory.EGraphs.Schedulers.ScoredScheduler
— Typemutable 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"#s631"} where var"#s631"<:AbstractRule
curr_iter::Int64
Metatheory.EGraphs.Schedulers.SimpleScheduler
— Typestruct 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)
cansaturate(s)
cansaturate(s)
Metatheory.EGraphs.Schedulers.cansearch
— FunctionShould 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)
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)
inform!(s, rule, n_matches)
inform!(s, rule, n_matches)