发表机构
Saarland University（萨尔兰州立大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文评估了 Knuth-Bendix 完备化方法，用于自动生成和扩充等式饱和中的重写规则，实验表明其能加快优化并发现先前遗漏的优化机会。
AI 中文摘要
等式饱和（EqSat）是一种强大的程序优化技术，它系统地探索候选程序的搜索空间，以克服阶段排序问题。然而，EqSat 的可行性和性能在很大程度上依赖于用于推导等价程序的特定重写规则。这些规则集通常是手工制作的，需要广泛的领域专业知识，并且存在遗漏有价值变换的风险。在本工作中，我们评估了 Knuth-Bendix 完备化（KBC）作为一种自动生成和扩充 EqSat 重写规则的方法。我们的实验表明，该方法能实现更快的优化，并且能够达到更好的项，实现先前遗漏的优化。
英文摘要
Equality Saturation (EqSat) is a powerful technique for program optimization, systematically exploring the search space of candidate programs to overcome the phase ordering problem. However, the feasibility and performance of EqSat rely heavily on the specific rewrite rules used to derive equivalent programs. These rule sets are typically handcrafted, requiring extensive domain expertise and carrying the risk of missing valuable transformations. In this work, we evaluate Knuth-Bendix Completion (KBC) as a method for automatically generating and augmenting rewrite rules for EqSat. Our experiments show faster optimization as well as reaching better terms with previously missed optimizations.
