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.@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 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
— 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
— 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.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}
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
— MethodEGraph(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
— 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.SaturationParams
— Typemutable 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, Function, 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!
— Methodanalyze!(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) -> Any
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:103
.
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:247
.
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:184
.
Metatheory.EGraphs.islazy
— Methodislazy(::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
islazy(analysis_name::Val{analysis_name}) -> Bool
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
— Methodjoin(::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
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
— Methodmake(::Val{analysis_name}, g, n)
Given an ENode n
, make
should return the corresponding analysis value.
Signatures
make(_::Val{analysis_name}, g, n)
Methods
make(_, g, n)
defined at /home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/analysis.jl:44
.
Metatheory.EGraphs.modify!
— Methodmodify!(::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:276
.
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{<: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{<: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)
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
.