Egg, from hack to a framework

At the heart of equality saturation lies a clever data structure called an e-graph. If you know how an abstract syntax tree—or expression tree—represents a single program, an e-graph does the same for many equivalent variants of that program, compactly folding them into a single structure (so compact, in fact, that a finite e-graph can represent infinitely many variants!). Equality saturation uses e-graphs for program optimization: It keeps adding new equivalent program variants to the graph and eventually extracts the “best” one according to some metric. The catch is that adding each new variant can break the e-graph’s compactness property, and an expensive compaction step is required to restore it. The first version of egg was fast because it skipped this compaction step—producing incorrect results. But while restoring it, Max had an epiphany: Why compact after every addition? — Nadia Polikarpova, in Technical Perspective: egg: ‘Ridiculously’ Fast and Extensible Equality Saturation…