egg：快速可扩展的等式饱和
egg: Fast and Extensible Equality Saturation
摘要：
一个e-图有效地表示了许多表达式上的同余关系。虽然它们最初是在20世纪70年代末开发的，用于自动定理证明器，但最近的一种称为等式饱和的技术重新使用了电子图，以实现最先进的重写驱动编译器优化和程序合成器。然而，电子图对于这个较新的用例仍然是非专用的。相等饱和的工作负载表现出独特的特点，往往需要特别的电子图扩展，以纳入超越纯粹的语法重写的转换。这项工作贡献了两种技术，使e-graphs快速和可扩展的，专门用于平等饱和。一种新的摊销不变恢复技术称为重建利用等式饱和的不同工作量，在实践中提供渐近加速比目前的技术。一种称为e类分析的通用机制将特定于域的分析集成到e图中，从而减少了对特别操作的需要。我们在一个名为egg的新开源库中实现了这些技术。我们对之前发表的三个等式饱和应用的案例研究强调了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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
