From be82fe3ac335fff265ac3211ee7391a9a4128f5c Mon Sep 17 00:00:00 2001 From: "Documenter.jl" Date: Thu, 9 May 2024 19:56:59 +0000 Subject: [PATCH] build based on f67dd7b --- dev/api/index.html | 50 ++++++++++---------- dev/egraphs/index.html | 2 +- dev/index.html | 2 +- dev/rewrite/index.html | 2 +- dev/search/index.html | 2 +- dev/tutorials/calculational_logic/index.html | 2 +- dev/tutorials/custom_types/index.html | 4 +- dev/tutorials/fibonacci/index.html | 26 +++++----- dev/tutorials/mu/index.html | 2 +- dev/tutorials/propositional_logic/index.html | 2 +- dev/tutorials/while_interpreter/index.html | 4 +- dev/visualizing/index.html | 2 +- 12 files changed, 50 insertions(+), 50 deletions(-) diff --git a/dev/api/index.html b/dev/api/index.html index e356a662..8e0216cf 100644 --- a/dev/api/index.html +++ b/dev/api/index.html @@ -1,11 +1,11 @@ -API Documentation · Metatheory.jl
Edit on GitHub

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.

source
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;
+API Documentation · Metatheory.jl
Edit on GitHub
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.
source
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
source
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)
+x = a
See also: @rule
source
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)))
@@ -46,11 +46,11 @@
 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.@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([
+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.@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)),
-])
See also: @rule, @capture
source
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 
+])
See also: @rule, @capture
source
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)
     #...
@@ -58,26 +58,26 @@
     @rule x y z  x * (y + z) --> (x * y) + (x * z)
     @rule x y x + y == (y + x)
     #...
-];
source
Patterns
Metatheory.Patterns.PatSegment — Type
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.PatTerm — Type
Term patterns will match on terms of the same arity and with the same  function symbol operation and expression head exprhead.
source
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. 
source
Rules
Metatheory.Rules.DynamicRule — Type
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.EqualityRule — Type
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.RewriteRule — Type
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.UnequalRule — Type
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
Rules
Rewriters
Metatheory.Rewriters — Module
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.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. 
source
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
source
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}
source
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, Function, SaturationGoal}
  • stopwhen::Function
  • scheduler::Type{<:Metatheory.EGraphs.Schedulers.AbstractScheduler}
  • schedulerparams::Tuple
  • threaded::Bool
  • timer::Bool
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)
defined at /home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/analysis.jl:61.
source
Metatheory.EGraphs.egraph_reconstruct_expression — Method
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) -> Any
-
Methods
egraph_reconstruct_expression(T, op, args)
defined at /home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/egraph.jl:534.
source
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
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.
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
+];
source
Patterns
Metatheory.Patterns.PatSegment — Type
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.PatTerm — Type
Term patterns will match on terms of the same arity and with the same  function symbol operation and expression head exprhead.
source
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. 
source
Rules
Metatheory.Rules.DynamicRule — Type
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.EqualityRule — Type
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.RewriteRule — Type
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.UnequalRule — Type
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
Rules
Rewriters
Metatheory.Rewriters — Module
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.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. 
source
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
source
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}
source
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, Function, SaturationGoal}
  • stopwhen::Function
  • scheduler::Type{<:Metatheory.EGraphs.Schedulers.AbstractScheduler}
  • schedulerparams::Tuple
  • threaded::Bool
  • timer::Bool
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)
defined at /home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/analysis.jl:61.
source
Metatheory.EGraphs.egraph_reconstruct_expression — Method
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) -> Any
+
Methods
egraph_reconstruct_expression(T, op, args)
defined at /home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/egraph.jl:534.
source
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
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.
source
EGraph Schedulers
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
source
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
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)
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.
source

+saturate!(g, theory, params)

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

source

EGraph Schedulers

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

source
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

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)

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.

source
diff --git a/dev/egraphs/index.html b/dev/egraphs/index.html index b5d522f4..0003616f 100644 --- a/dev/egraphs/index.html +++ b/dev/egraphs/index.html @@ -134,4 +134,4 @@ custom_analysis(:(2*a)) # :even custom_analysis(:(3*3)) # :odd custom_analysis(:(3*(2+a)*2)) # :even -custom_analysis(:(3y * (2x*y))) # :even +custom_analysis(:(3y * (2x*y))) # :even diff --git a/dev/index.html b/dev/index.html index 7d40aebb..a8602719 100644 --- a/dev/index.html +++ b/dev/index.html @@ -5,4 +5,4 @@ -

+

diff --git a/dev/rewrite/index.html b/dev/rewrite/index.html index 667690b6..091fc616 100644 --- a/dev/rewrite/index.html +++ b/dev/rewrite/index.html @@ -34,4 +34,4 @@ distrib = @theory a b c begin a * (b + c) => (a * b) + (a * c) end -t = comm_monoid ∪ comm_group ∪ distrib

Composing rewriters

Rules may be chained together into more sophisticated rewriters to avoid manual application of the rules. A rewriter is any callable object 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 Rules we created above are rewriters.

The Metatheory.Rewriters module contains some types which create and transform rewriters.

Chaining rewriters

Several rules may be chained to give chain of rules. Chain is an array of rules which are subsequently applied to the expression. Important feature of Chain is that it returns the expression instead of nothing if it doesn't change the expression It is important to notice, that chain is ordered, so if rules are in different order it wouldn't work the same as in earlier example

One way to circumvent the problem of order of applying rules in chain is to use RestartedChain, it restarts the chain after each successful application of a rule, so after a rule is hit it (re)starts again and it can apply all the other rules to the resulting expression. You can also use Fixpoint to apply the rules until there are no changes.

+t = comm_monoid ∪ comm_group ∪ distrib

Composing rewriters

Rules may be chained together into more sophisticated rewriters to avoid manual application of the rules. A rewriter is any callable object 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 Rules we created above are rewriters.

The Metatheory.Rewriters module contains some types which create and transform rewriters.

Chaining rewriters

Several rules may be chained to give chain of rules. Chain is an array of rules which are subsequently applied to the expression. Important feature of Chain is that it returns the expression instead of nothing if it doesn't change the expression It is important to notice, that chain is ordered, so if rules are in different order it wouldn't work the same as in earlier example

One way to circumvent the problem of order of applying rules in chain is to use RestartedChain, it restarts the chain after each successful application of a rule, so after a rule is hit it (re)starts again and it can apply all the other rules to the resulting expression. You can also use Fixpoint to apply the rules until there are no changes.

diff --git a/dev/search/index.html b/dev/search/index.html index a0941603..004b229a 100644 --- a/dev/search/index.html +++ b/dev/search/index.html @@ -1,2 +1,2 @@ -Search · Metatheory.jl

Loading search...

    +Search · Metatheory.jl

    Loading search...

      diff --git a/dev/tutorials/calculational_logic/index.html b/dev/tutorials/calculational_logic/index.html index f9dbca5a..e981bc7d 100644 --- a/dev/tutorials/calculational_logic/index.html +++ b/dev/tutorials/calculational_logic/index.html @@ -41,4 +41,4 @@ params = SaturationParams(timeout = 12, eclasslimit = 10000, schedulerparams = (1000, 5)) @test areequal(calculational_logic_theory, true, :(((p ⟹ (p || p)) == ((!(p) && q) ⟹ q)) == true); params = params)

      Frege's theorem

        @test areequal(calculational_logic_theory, true, :((p ⟹ (q ⟹ r)) ⟹ ((p ⟹ q) ⟹ (p ⟹ r))); params = params)

      Demorgan's

        @test @areequal calculational_logic_theory true (!(p || q) == (!p && !q))

      Consensus theorem

        areequal(calculational_logic_theory, :((x && y) || (!x && z) || (y && z)), :((x && y) || (!x && z)); params = params)
-end

      This page was generated using Literate.jl.

      +end

      This page was generated using Literate.jl.

      diff --git a/dev/tutorials/custom_types/index.html b/dev/tutorials/custom_types/index.html index 68d2cdaf..b85e08e6 100644 --- a/dev/tutorials/custom_types/index.html +++ b/dev/tutorials/custom_types/index.html @@ -18,7 +18,7 @@ end
      1-element Vector{RewriteRule}:
  f(z(2), ~a) --> f(~a)

      Let's create an example expression and e-graph

      hcall = MyExpr(:h, [4], "hello")
 ex = MyExpr(:f, [MyExpr(:z, [2]), hcall])
-g = EGraph(ex; keepmeta = true)
      EGraph(IntDisjointSet([-1, -1, -1, -1, -1], Base.RefValue{Bool}(true)), Dict{Int64, EClass}(5 => EClass 5 ([ENode(call, f, Main.var"ex-custom_types".MyExpr, [2, 4])], ), 4 => EClass 4 ([ENode(call, h, Main.var"ex-custom_types".MyExpr, [3])], ), 2 => EClass 2 ([ENode(call, z, Main.var"ex-custom_types".MyExpr, [1])], ), 3 => EClass 3 ([4], ), 1 => EClass 1 ([2], )), Dict{AbstractENode, Int64}(4 => 3, 2 => 1, ENode(call, f, Main.var"ex-custom_types".MyExpr, [2, 4]) => 5, ENode(call, z, Main.var"ex-custom_types".MyExpr, [1]) => 2, ENode(call, h, Main.var"ex-custom_types".MyExpr, [3]) => 4), Int64[], 5, Dict{Union{Function, Symbol}, Union{Function, Symbol}}(:metadata_analysis => :metadata_analysis), Dict{Any, Vector{Int64}}(:f => [5], 4 => [3], 2 => [1], :h => [4], :z => [2]), Expr, Dict{Tuple{Any, Int64}, Type}(), 5, 0, false, Base.ImmutableDict{Int64, Tuple{Int64, Int64}}[], Tuple{Int64, Int64}[], ReentrantLock(nothing, 0x00000000, 0x00, Base.GenericCondition{Base.Threads.SpinLock}(Base.IntrusiveLinkedList{Task}(nothing, nothing), Base.Threads.SpinLock(0)), (2, 139686195244896, 139686195252336)))

      We use settermtype! on an existing e-graph to inform the system about the default type of expressions that we want newly added expressions to have.

      settermtype!(g, MyExpr)
      Main.var"ex-custom_types".MyExpr

      Now let's test that it works.

      saturate!(g, t)
+g = EGraph(ex; keepmeta = true)
      EGraph(IntDisjointSet([-1, -1, -1, -1, -1], Base.RefValue{Bool}(true)), Dict{Int64, EClass}(5 => EClass 5 ([ENode(call, f, Main.var"ex-custom_types".MyExpr, [2, 4])], ), 4 => EClass 4 ([ENode(call, h, Main.var"ex-custom_types".MyExpr, [3])], ), 2 => EClass 2 ([ENode(call, z, Main.var"ex-custom_types".MyExpr, [1])], ), 3 => EClass 3 ([4], ), 1 => EClass 1 ([2], )), Dict{AbstractENode, Int64}(4 => 3, 2 => 1, ENode(call, f, Main.var"ex-custom_types".MyExpr, [2, 4]) => 5, ENode(call, z, Main.var"ex-custom_types".MyExpr, [1]) => 2, ENode(call, h, Main.var"ex-custom_types".MyExpr, [3]) => 4), Int64[], 5, Dict{Union{Function, Symbol}, Union{Function, Symbol}}(:metadata_analysis => :metadata_analysis), Dict{Any, Vector{Int64}}(:f => [5], 4 => [3], 2 => [1], :h => [4], :z => [2]), Expr, Dict{Tuple{Any, Int64}, Type}(), 5, 0, false, Base.ImmutableDict{Int64, Tuple{Int64, Int64}}[], Tuple{Int64, Int64}[], ReentrantLock(nothing, 0x00000000, 0x00, Base.GenericCondition{Base.Threads.SpinLock}(Base.IntrusiveLinkedList{Task}(nothing, nothing), Base.Threads.SpinLock(0)), (0, 0, 0)))

      We use settermtype! on an existing e-graph to inform the system about the default type of expressions that we want newly added expressions to have.

      settermtype!(g, MyExpr)
      Main.var"ex-custom_types".MyExpr

      Now let's test that it works.

      saturate!(g, t)
 expected = MyExpr(:f, [MyExpr(:h, [4], "HELLO")], "")
 extracted = extract!(g, astsize)
-@test expected == extracted
      Test Passed

      This page was generated using Literate.jl.

      +@test expected == extracted
      Test Passed

      This page was generated using Literate.jl.

      diff --git a/dev/tutorials/fibonacci/index.html b/dev/tutorials/fibonacci/index.html index fe9830dd..9b4d8bff 100644 --- a/dev/tutorials/fibonacci/index.html +++ b/dev/tutorials/fibonacci/index.html @@ -18,15 +18,15 @@ ──────────────────────────────────────────────────────────────────── Time Allocations ─────────────────────── ──────────────────────── - Tot / % measured: 458ms / 10.1% 21.6MiB / 8.8% + Tot / % measured: 376ms / 12.3% 21.6MiB / 8.8% Section ncalls time %tot avg alloc %tot avg ──────────────────────────────────────────────────────────────────── - Search 16 30.7ms 66.2% 1.92ms 1.34MiB 70.2% 85.5KiB - 2 16 30.6ms 65.9% 1.91ms 1.29MiB 67.8% 82.6KiB - 1 16 120μs 0.3% 7.48μs 43.4KiB 2.2% 2.71KiB - Apply 16 15.4ms 33.2% 962μs 511KiB 26.2% 32.0KiB - Rebuild 16 252μs 0.5% 15.8μs 69.4KiB 3.6% 4.34KiB + Search 16 30.3ms 65.4% 1.89ms 1.34MiB 70.2% 85.5KiB + 2 16 30.1ms 65.1% 1.88ms 1.29MiB 67.8% 82.6KiB + 1 16 115μs 0.2% 7.20μs 43.4KiB 2.2% 2.71KiB + Apply 16 15.8ms 34.0% 986μs 511KiB 26.2% 32.0KiB + Rebuild 16 256μs 0.6% 16.0μs 69.4KiB 3.6% 4.34KiB ────────────────────────────────────────────────────────────────────

      That's fast!

      z = EGraph(:(fib(10)))
 saturate!(z, fibo, params)
      SaturationReport
@@ -37,16 +37,16 @@
  ────────────────────────────────────────────────────────────────────
                             Time                    Allocations      
                    ───────────────────────   ────────────────────────
- Tot / % measured:     1.43ms /  81.3%            575KiB /  87.3%    
+ Tot / % measured:     1.49ms /  81.1%            575KiB /  87.3%    
 
  Section   ncalls     time    %tot     avg     alloc    %tot      avg
  ────────────────────────────────────────────────────────────────────
- Apply         16    815μs   69.9%  51.0μs    332KiB   66.1%  20.7KiB
- Rebuild       16    208μs   17.8%  13.0μs   69.4KiB   13.8%  4.34KiB
- Search        16    143μs   12.2%  8.92μs    101KiB   20.1%  6.30KiB
-   1           16   67.5μs    5.8%  4.22μs   43.4KiB    8.6%  2.71KiB
-   2           16   63.8μs    5.5%  3.99μs   53.2KiB   10.6%  3.33KiB
+ Apply         16    845μs   70.0%  52.8μs    332KiB   66.1%  20.7KiB
+ Rebuild       16    218μs   18.0%  13.6μs   69.4KiB   13.8%  4.34KiB
+ Search        16    145μs   12.0%  9.07μs    101KiB   20.1%  6.30KiB
+   1           16   67.0μs    5.5%  4.19μs   43.4KiB    8.6%  2.71KiB
+   2           16   66.3μs    5.5%  4.14μs   53.2KiB   10.6%  3.33KiB
  ────────────────────────────────────────────────────────────────────

      We can test that the result is correct.

      @testset "Fibonacci" begin
   @test 55 == extract!(g, astsize)
-end
      Test.DefaultTestSet("Fibonacci", Any[], 1, false, false, true, 1.715283203253726e9, 1.715283203269987e9, false, "none")

      This page was generated using Literate.jl.

      +end
      Test.DefaultTestSet("Fibonacci", Any[], 1, false, false, true, 1.715284592972322e9, 1.715284592988204e9, false, "none")

      This page was generated using Literate.jl.

      diff --git a/dev/tutorials/mu/index.html b/dev/tutorials/mu/index.html index 741697bb..cf3b95cb 100644 --- a/dev/tutorials/mu/index.html +++ b/dev/tutorials/mu/index.html @@ -15,4 +15,4 @@ start = :(M ⋅ I ⋅ END) g = EGraph(start) saturate!(g, miu) -@test false == areequal(g, miu, start, :(M ⋅ U ⋅ END); params = params)
      Test Passed

      This page was generated using Literate.jl.

      +@test false == areequal(g, miu, start, :(M ⋅ U ⋅ END); params = params)
      Test Passed

      This page was generated using Literate.jl.

      diff --git a/dev/tutorials/propositional_logic/index.html b/dev/tutorials/propositional_logic/index.html index 7de803cb..431c5887 100644 --- a/dev/tutorials/propositional_logic/index.html +++ b/dev/tutorials/propositional_logic/index.html @@ -92,4 +92,4 @@ @test @areequal propositional_logic_theory true ((!p || !p) == !p) (!p || p) !(!p && p) @test @areequal propositional_logic_theory p (p || p) @test @areequal propositional_logic_theory true ((p ⟹ (p || p))) - @test @areequal propositional_logic_theory true ((p ⟹ (p || p)) == ((!(p) && q) ⟹ q)) == true

      Frege's theorem

        @test @areequal propositional_logic_theory true (p ⟹ (q ⟹ r)) ⟹ ((p ⟹ q) ⟹ (p ⟹ r))

      Demorgan's

        @test @areequal propositional_logic_theory true (!(p || q) == (!p && !q))

      Consensus theorem @testbroken @areequal propositionallogic_theory true ((x && y) || (!x && z) || (y && z)) ((x && y) || (!x && z))

      end

      This page was generated using Literate.jl.

      + @test @areequal propositional_logic_theory true ((p ⟹ (p || p)) == ((!(p) && q) ⟹ q)) == true

      Frege's theorem

        @test @areequal propositional_logic_theory true (p ⟹ (q ⟹ r)) ⟹ ((p ⟹ q) ⟹ (p ⟹ r))

      Demorgan's

        @test @areequal propositional_logic_theory true (!(p || q) == (!p && !q))

      Consensus theorem @testbroken @areequal propositionallogic_theory true ((x && y) || (!x && z) || (y && z)) ((x && y) || (!x && z))

      end

      This page was generated using Literate.jl.

      diff --git a/dev/tutorials/while_interpreter/index.html b/dev/tutorials/while_interpreter/index.html index 9921ebb5..cb632be1 100644 --- a/dev/tutorials/while_interpreter/index.html +++ b/dev/tutorials/while_interpreter/index.html @@ -58,7 +58,7 @@ @test 0 == eval_if(:(cond(false, x, 0)), Mem(:x => 2)) @test 2 == eval_if(:(cond(!(false), x, 0)), Mem(:x => 2)) @test 0 == eval_if(:(cond(!(2 < x), x, 0)), Mem(:x => 3)) -end
      Test.DefaultTestSet("If Semantics", Any[], 4, false, false, true, 1.715283211519213e9, 1.715283211907445e9, false, "none")

      Writing memory

      Our language then needs a mechanism to write in memory. We define the behavior of the store construct, which behaves like the = assignment operator in other programming languages. store(a, 5) will store the value 5 in the a variable inside the program's memory.

      write_mem = @theory sym val σ begin
+end
      Test.DefaultTestSet("If Semantics", Any[], 4, false, false, true, 1.715284602268126e9, 1.715284602664992e9, false, "none")

      Writing memory

      Our language then needs a mechanism to write in memory. We define the behavior of the store construct, which behaves like the = assignment operator in other programming languages. store(a, 5) will store the value 5 in the a variable inside the program's memory.

      write_mem = @theory sym val σ begin
   (store(sym::Symbol, val), σ) => (σ[sym] = eval_if(val, σ);
   σ)
 end
      1-element Vector{DynamicRule}:
@@ -90,4 +90,4 @@
   @test Mem(:x => 4) == eval_while(:(cond(x < 10, store(x, x + 1))), Mem(:x => 3))
   @test 10 == eval_while(:(seq(loop(x < 10, store(x, x + 1)), x)), Mem(:x => 3))
   @test 50 == eval_while(:(seq(loop(x < y, seq(store(x, x + 1), store(y, y - 1))), x)), Mem(:x => 0, :y => 100))
-end
      Test.DefaultTestSet("While Semantics", Any[], 5, false, false, true, 1.715283213209895e9, 1.71528321409595e9, false, "none")

      This page was generated using Literate.jl.

      +end
      Test.DefaultTestSet("While Semantics", Any[], 5, false, false, true, 1.715284604005169e9, 1.715284604901068e9, false, "none")

      This page was generated using Literate.jl.

      diff --git a/dev/visualizing/index.html b/dev/visualizing/index.html index 8de0fb08..ed0992e6 100644 --- a/dev/visualizing/index.html +++ b/dev/visualizing/index.html @@ -27,4 +27,4 @@ g = EGraph(ex) params = SaturationParams(; timeout = 2) saturate!(g, algebra_rules, params) -g

      And you will see a nice e-graph drawing in the Julia Plots VSCode panel:

      E-Graph Drawing

      +g

      And you will see a nice e-graph drawing in the Julia Plots VSCode panel:

      E-Graph Drawing