一句话：提出可在等价饱和过程中进行乐观抽象解释的统一算法，避免不健全性并提升SSA程序分析精度。
等价饱和是一种基于非破坏性重写和e-class分析的优化技术，但现有e-class分析过于悲观，分析SSA等循环程序时通常不精确。作者发现，直接采用乐观e-class分析会因e-graph表示程序的微妙之处而导致不健全。为此，论文提出一种抽象解释算法来规避该问题，并可在等价饱和过程中乐观地分析e-graph，从而将乐观分析与非破坏性重写统一在一个算法中。作者为SSA程序实现了原型抽象解释器与等价饱和工具。实验表明，该工具在示例程序上比纯抽象解释和悲观e-class分析更精确，同时性能与现有抽象解释及e-class分析技术相当。
Equality saturation is a program optimization technique based on non-destructive rewriting and a form of abstract interpretation called e-class analysis. Existing e-class analyses are pessimistic and therefore typically imprecise when analyzing cyclic programs, such as those in SSA form. We show that a straightforward optimistic variant of e-class analysis can result in unsoundness, due to a subtlety in how e-graphs represent programs. We propose an abstract interpretation algorithm that circumvents this issue and can optimistically analyze e-graphs during equality saturation. This results in a unified algorithm for optimistic analysis and non-destructive rewriting. We implement a prototype abstract interpreter and equality saturation tool for SSA programs. Our tool exhibits precision improvements over pure abstract interpretation (without rewriting) and pessimistic e-class analysis on example programs. Additionally, its performance is comparable to existing abstract interpretation and e-class analysis techniques.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{ArboreCW26,
title = {Optimism in Equality Saturation},
author = {Russel Arbore and Alvin Cheung and Max Willsey},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {PLDI},
year = {2026},
doi = {10.1145/3808302}
}