Extracting from an E-Graph

Extraction can be formulated as an EGraph analysis, or after saturation. A cost function can be provided. Metatheory.jl already provides some simple cost functions, such as astsize, which expresses preference for the smallest expressions.

Given the theory:

using Metatheory
using Metatheory.Library
using Metatheory.EGraphs

@metatheory_init ()

comm_monoid = commutative_monoid(:(*), 1);
comm_group = @theory begin
    a + 0 => a
    a + b => b + a
    a + inv(a) => 0 # inverse
    a + (b + c) => (a + b) + c
end
distrib = @theory begin
	a * (b + c) => (a * b) + (a * c)
	(a * b) + (a * c) => a * (b + c)
end
powers = @theory begin
	a * a => a^2
	a => a^1
	a^n * a^m => a^(n+m)
end
logids = @theory begin
	log(a^n) => n * log(a)
	log(x * y) => log(x) + log(y)
	log(1) => 0
	log(:e) => 1
	:e^(log(x)) => x
end
fold = @theory begin
	a::Number + b::Number |> a + b
	a::Number * b::Number |> a * b
end
t = comm_monoid ∪ comm_group ∪ distrib ∪ powers ∪ logids ∪ fold ;

We can extract an expression by using

G = EGraph(:((log(e) * log(e)) * (log(a^3 * a^2))))
saturate!(G, t)
ex = extract!(G, astsize)
:(log(a ^ 5))

The second argument to extract! is a cost function. astsize is a cost function provided by default, which computes the size of expressions.

Defining custom cost functions

TODO

API Docs

Metatheory.EGraphs.astsize — Method

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

Signatures

astsize(n::ENode, g::EGraph, an::Type{var"#s489"} where var"#s489"<:AbstractAnalysis) -> Any

Methods

astsize(n, g, an)
Metatheory.EGraphs.astsize_inv — Method

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::ENode, g::EGraph, an::Type{var"#s490"} where var"#s490"<:AbstractAnalysis) -> Any

Methods

astsize_inv(n, g, an)
Metatheory.EGraphs.extract! — Method

Given a cost function, extract the expression with the smallest computed cost from an EGraph

Signatures

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

Methods

extract!(g, costfun; root)