Racket E-graph Library
Equivalence graphs are a data structure for compactly storing many equivalent expressions. The Denali paper is a good introduction to the general idea and one of its uses. Regraph is a battle-tested, production-ready implementation of this data structure in pure Racket, originally developed for the Herbie project, which has since migrated to the Rust-based E-Graphs Good library.
Regraph can be installed directly from package servers:
raco pkg install regraph
You can then include Regraph with
Creating Equivalence Graphs
Regraph considers two types of expressions: atomic expressions, which
can be anything except a list, and function applications, which are a
list where the first element is the function and later elements are
arguments. It is convenient if
#f is not a valid expression.
The Regraph API is fairly simple:
(make-regraph exprs #:limit N)creates an equivalence graph, initially seeded with the expressions from
exprs, and limited to
Nnodes, which in practice should be around 10 000.
(regraph-cost rg)measure the physical and logical size of the equivalence graph.
(regraph-extract rg)returns expressions equivalent to those in
exprs, but optimized to have lower cost.
rg above represents the equivalence graph returned by
make-regraph. In Regraph, cost is just the total size of the
expression, counting atomic expressions as 1 and function applications
as 1 plus the size of the arguments.
Adding to Equivalence Graphs
However, if you just apply these methods, you won't get interesting results. To do that, you'll need to add expressions and expression equivalences to the equivalence graph using "phases". Regraph provides four:
(rule-phase ipats opats)applies rewrite rules, given by patterns, wherever they match in the equivalence graph. The rules are given by two parallel lists, which contain the input and output patterns of each rule.
A pattern is like an expression, but symbols represent pattern variables. For example, the pattern
(+ a b)matches all expressions with
+applied to any two arguments, while
(* a (/ 1 a))matches all products of one thing and
/applied to the atomic expression
1and that thing.
(fn op args ...)for each function application expression whose arguments are equivalent to atomic expressinos.
fnshould return either
#f(meaning that no answer can be computed) or an expression, in which case that expression will me made equivalent to the original. This is particularly useful for implementing various forms of constant-folding.
prune-phasedeletes all expressions from the equivalence graph that are equivalent to an atomic expression, since atomic expressions are lower-cost than any non-atomic expressions. Calling this often may prevent Regraph from finding the lowest-cost equivalent to an expression, but will speed up rule application. It does not affect
extractor-phaseupdates the lowest-cost versions of each expression. Run this before calling
(regraph-cost)to get accurate results.
Each phase can be applied to an equivalence graph with
Phases will not do anything once the equivalence graph hits the node
limit it was defined with.
The best way to use Regraph is to create the equivalence graph with
make-regraph, then apply whatever phases you'd like in a loop until
regraph-count either ceases to change or hits the defined limit, and
regraph-extract to get the best versions of the original
For simplifying algebraic expressions, define a set of rewrite rules from algebraic identities. Then create an equivalence graph, apply the rules repeatedly, and extract the results.
For solving congruence closure problems, create an equivalence graph with the two sides of the equality being tested, add each given equality as a rewrite rule, and test the extracted results for exact equality.