发表机构
University of Washington; University of Pennsylvania; University of California, Berkeley; Certora Inc.（华盛顿大学; 宾夕法尼亚大学; 加利福尼亚大学伯克利分校; Certora公司）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文提出Enumo，一种可编程领域特定语言，通过核心操作符和快进策略，实现可扩展、可组合的等式饱和规则推断，在多个领域超越现有方法，甚至匹配手动规则集效果。
AI 中文摘要
重写规则在等式饱和中至关重要，等式饱和是一种在优化编译器、合成器和验证器中日益流行的技术。不幸的是，开发高质量的规则集既困难又容易出错。最近自动推断重写规则的工作无法扩展到大型项或文法。用户难以引导推断并增量构建规则集，因为现有的规则推断工具是整体式且不透明的。因此，大多数等式饱和用户仍然手动开发和维护规则集。本文提出了Enumo，一种用于可编程理论探索的新型领域特定语言。Enumo提供了一小组核心操作符，使用户能够战略性地引导规则推断并增量构建规则集。简短的Enumo程序可以轻松复现Ruler等最先进工具的结果，但Enumo程序也能扩展到从比先前方法更大的文法中推断更深的规则。Enumo的可组合操作符甚至有助于开发新的规则集推断策略。我们引入了一种新的快进策略，该策略不需要在目标语言中评估项，因此支持先前工作范围之外的领域。Enumo还易于扩展：两个新操作符就足以将大型语言模型纳入规则推断，其中它们补充了引导搜索。我们在各种领域评估了Enumo和快进策略。与最先进的技术相比，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 to automatically infer rewrite rules does not scale to large terms or grammars. Users struggle to guide inference and incrementally construct rulesets because existing rule inference tools are monolithic and opaque. As a result, most equality saturation 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 like Ruler, but Enumo programs can also scale to infer deeper rules from larger grammars than prior approaches. Enumo's composable operators even facilitate developing new strategies for ruleset inference. We introduce a new fast-forwarding strategy which does not require evaluating terms in the target language, and thus supports domains that were out of scope for prior work. Enumo is also easy to extend: two new operators suffice to incorporate large language models into rule inference, where they complement guided search. 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.
Comments43 pages, 9 figures, Extended version of the OOPSLA 2023 paper, submitted to the Journal of Functional Programming. v2: corrected the accent in the title metadata; paper unchanged
