论文标题
鸡蛋：快速且可扩展的平等饱和
egg: Fast and Extensible Equality Saturation
论文作者
论文摘要
电子图表有效地代表了许多表达式的一致关系。尽管它们最初是在1970年代后期开发的，用于自动定理掠夺，但一种较新的技术称为“等效饱和度”重新利用电子图形，以实现最新的，重写的编译器优化和程序合成器。但是，对于此较新的用例，电子图表仍然没有专业化。平等性饱和工作负载具有不同的特征，通常需要临时的电子图形扩展，以结合纯粹的句法重写以外的转换。 这项工作贡献了两种使电子支柱快速且可扩展的技术，将它们专门用于平等饱和。一种称为重建的新摊销不变的恢复技术利用了平等饱和的独特工作量，在实践中提供了比当前技术的渐近加速。一种称为E级分析的一般机制将特定于域的分析集成到电子图表中，从而减少了对临时操作的需求。 我们在一个名为Egg的新开源库中实施了这些技术。我们对以前发表的相等性饱和应用的三个以前发表的应用的案例研究突出了鸡蛋的性能和灵活性如何使各种领域的最先进结果。
An e-graph efficiently represents a congruence relation over many expressions. Although they were originally developed in the late 1970s for use in automated theorem provers, a more recent technique known as equality saturation repurposes e-graphs to implement state-of-the-art, rewrite-driven compiler optimizations and program synthesizers. However, e-graphs remain unspecialized for this newer use case. Equality saturation workloads exhibit distinct characteristics and often require ad-hoc e-graph extensions to incorporate transformations beyond purely syntactic rewrites. This work contributes two techniques that make e-graphs fast and extensible, specializing them to equality saturation. A new amortized invariant restoration technique called rebuilding takes advantage of equality saturation's distinct workload, providing asymptotic speedups over current techniques in practice. A general mechanism called e-class analyses integrates domain-specific analyses into the e-graph, reducing the need for ad hoc manipulation. We implemented these techniques in a new open-source library called egg. Our case studies on three previously published applications of equality saturation highlight how egg's performance and flexibility enable state-of-the-art results across diverse domains.
