EGraphs and Equality Saturation

An EGraph is an efficient data structure for representing congruence relations. EGraphs are data structures originating from theorem provers. Several projects have very recently repurposed EGraphs to implement state-of-the-art, rewrite-driven compiler optimizations and program synthesizers using a technique known as equality saturation. Metatheory.jl provides a general purpose, customizable implementation of EGraphs and equality saturation, inspired from the egg library for Rust. You can read more about the design of the EGraph data structure and equality saturation algorithm in the egg paper.

What can I do with EGraphs in Metatheory.jl?

Most importantly, the EGraph backend for Metatheory.jl allows you to create an EGraph from a starting expression, to add more expressions to the EGraph with addexpr!, and then to effectively fill the EGraph with all possible equivalent expressions resulting from applying rewrite rules from a theory, by using the saturate! function. You can then easily extract expressions with a cost function and an ExtractionAnalysis.

A killer feature of egg and Metatheory.jl are EGraph Analyses. They allow you to annotate expressions and equivalence classes in an EGraph with values from a semilattice domain, and then to:

• Extract expressions from an EGraph basing from analysis data.
• Have conditional rules that are executed if some criteria is met on analysis data
• Have dynamic rules that compute the right hand side based on analysis data.

Theories and Algebraic Structures

The e-graphs backend can directly handle associativity, commutativity and distributivity, rules that are otherwise known of causing loops in symbolic computations.

comm_monoid = @theory begin
    a * b => b * a
    a * 1 => a
    a * (b * c) => (a * b) * c
end

The Metatheory Library

The Metatheory.Library module contains utility functions and macros for creating rules and theories from commonly used algebraic structures and properties.

using Metatheory.Library

comm_monoid = commutative_monoid(:(*), 1)
# alternatively
comm_monoid = @commutative_monoid (*) 1

Equality Saturation

We can programmatically build and saturate an EGraph. The function saturate! takes an EGraph and a theory, and executes equality saturation. Returns a report of the equality saturation process. saturate! is configurable, customizable parameters include a timeout on the number of iterations, a eclasslimit on the number of e-classes in the EGraph, a stopwhen functions that stops saturation when it evaluates to true.

G = EGraph(:((a * b) * (1 * (b + c))));
report = saturate!(G, t);
# access the saturated EGraph
report.egraph

# show some fancy stats
println(report);

With the EGraph equality saturation backend, Metatheory.jl can prove simple equalities very efficiently. The @areequal macro takes a theory and some expressions and returns true iff the expressions are equal according to the theory. The following example returns true.

@areequal t (x+y)*(a+b) ((a*(x+y))+b*(x+y)) ((x*(a+b))+y*(a+b))

Configurable Parameters

EGraphs.saturate! can accept an additional parameter of type EGraphs.SaturationParams to configure the equality saturation algorithm. The documentation for the configurable parameters is available in the EGraphs.SaturationParams API docstring.

# create the saturation params
params = SaturationParams(timeout=10, eclasslimit=4000)
saturate!(egraph, theory, params)

API Docs

eqsat_step!(g::EGraph, theory::Vector{var"#s617"} where var"#s617"<:AbstractRule, curr_iter, scheduler::Metatheory.EGraphs.Schedulers.AbstractScheduler, match_hist::Vector{Metatheory.EGraphs.Match}, params::SaturationParams, report) -> Tuple{Any, EGraph}

eqsat_step!(g, theory, curr_iter, scheduler, match_hist, params, report)

saturate!(g::EGraph, theory::Vector{var"#s493"} where var"#s493"<:AbstractRule) -> Metatheory.EGraphs.Report
saturate!(g::EGraph, theory::Vector{var"#s492"} where var"#s492"<:AbstractRule, params) -> Metatheory.EGraphs.Report

saturate!(g, theory)
saturate!(g, theory, params)