一句话：提出可编程理论探索 DSL Enumo，以可组合算子引导等价饱和的重写规则推断，并支持免求值的 fast-forwarding 策略。
重写规则对等价饱和至关重要，但高质量规则集难以开发和维护。现有自动规则推断难以扩展到大型项或文法，且工具单体、不透明，用户难以引导推断并增量构建规则集。本文提出 Enumo，一种用于可编程理论探索的 DSL，提供一组核心算子，使用户能策略性地引导规则推断并逐步构建规则集。其算子可组合，便于开发新的规则集推断策略。作者还提出 fast-forwarding 策略，无需在目标语言中求值项，从而支持先前工作无法覆盖的领域。评估在多个领域进行，与最先进技术相比，Enumo 能合成更好的规则集，在某些情况下可匹配等价饱和系统中手工开发规则集的效果。
Rewrite rules are critical in equality saturation, an increasingly popular technique in optimizing compilers, synthesizers, and verifiers. Unfortunately, developing high-quality rulesets is difficult and error-prone. Recent work on automatically inferring rewrite rules does not scale to large terms or grammars, and existing rule inference tools are monolithic and opaque. Equality saturation users therefore struggle to guide inference and incrementally construct rulesets. As a result, most users still manually develop and maintain rulesets. This paper proposes Enumo, a new domain-specific language for programmable theory exploration. Enumo provides a small set of core operators that enable users to strategically guide rule inference and incrementally build rulesets. Short Enumo programs easily replicate results from state-of-the-art tools, but Enumo programs can also scale to infer deeper rules from larger grammars than prior approaches. Its composable operators even facilitate developing new strategies for ruleset inference. We introduce a new fast-forwarding strategy that does not require evaluating terms in the target language, and can thus support domains that were out of scope for prior work. We evaluate Enumo and fast-forwarding across a variety of domains. Compared to state-of-the-art techniques, enumo can synthesize better rulesets over a diverse set of domains, in some cases matching the effects of manually-developed rulesets in systems driven by equality saturation.
@article{paperbot1868,
title = {Equality Saturation Theory Exploration à la Carte},
author = {Anjali Pal and Brett Saiki and Ryan Tjoa and Cynthia Richey and Amy Zhu and Oliver Flatt and Max Willsey and Zachary Tatlock and Chandrakana Nandi},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {OOPSLA2},
year = {2023},
doi = {10.1145/3622834}
}