egg: Fast and Extensible Equality Saturation

Abstract

Abstract

E-graphs, originally developed for use in automated theorem provers, are data structures that compactly represent a large number of expressions and the equalities between them. Recently, a technique called equality saturation adapted e-graphs for program optimization. Equality saturation can ameliorate issues with traditional, destructive term rewriting since e-graph rewriting only adds information to the e-graph. After rewriting, the e-graph represents a large space of equivalent terms (including the original term), and a final extraction procedure selects the best term according to a user-provided cost function. The egg library is a fast and flexible open-source implementation of e-graphs and equality saturation. Unlike solvers, egg is a white-box library for programmatic use. Users can easily define their own languages, rewrites, and analyses, and they can inspect and manipulate the e-graph directly. It incorporates novel techniques such as e-class analysis , a mechanism for integrating program analyses modulo equality; and rebuilding , a deferred invariant restoration algorithm. egg has been used in hundreds of academic and industrial projects for program optimization, synthesis, and verification in many domains; some are briefly highlighted in this article.