Caviar：用于自动代码优化的基于电子图谱的TRS

术语重写系统（TRS）在编译器中被用来简化和证明表达式。编译器中最先进的TRS使用一种贪婪的算法，按照预定的顺序应用一组重写规则（其中一些规则不是公理的）。这导致了简化某些表达式的能力的损失。电子图谱和等价饱和避开了这个问题，它以一种紧凑的方式表示不同的等价表达，从中可以提取出最佳表达。虽然基于电子图谱的TRS比使用贪婪算法的TRS更强大，但它的速度较慢，因为表达式可能有大量或有时无限多的等价表达式。加快电子图谱的构建对于使电子图谱在编译器中的使用实用化至关重要。在本文中，我们提出了Caviar，一个基于电子图谱的TRS，用于证明编译器中的表达式。Caviar是一个快速（比基本电子图谱TRS快20倍）和灵活（完全参数化）的TRS，它依赖于三种新技术。1）一种在达到目标时停止电子图谱增长的技术，称为迭代水平检查；2）一种在平等饱和算法中平衡探索和利用的机制，称为脉冲式鱼子酱；3）一种在检测到不可证明的模式时在达到饱和之前停止电子图谱构建的技术，称为不可证明模式检测（NPPD）。我们在Halide上对Caviar进行了评估，Halide是一个优化的编译器，依靠基于贪婪算法的TRS来简化和证明其表达式。所提出的技术使Caviar在证明表达式的任务中加快了20倍的e-graph扩展。它们还允许Caviar证明Halide的TRS无法证明的51%的表达式，而速度只慢0.68倍。

原文题目：Caviar: An E-graph Based TRS for Automatic Code Optimization

原文：Term Rewriting Systems (TRS) are used in compilers to simplify and prove expressions. State-of-the-art TRSs in compilers use a greedy algorithm that applies a set of rewriting rules in a predefined order (where some of the rules are not axiomatic). This leads to a loss in the ability to simplify certain expressions. E-graphs and equality saturation sidestep this issue by representing the different equivalent expressions in a compact manner from which the optimal expression can be extracted. While an e-graph-based TRS can be more powerful than a TRS that uses a greedy algorithm, it is slower because expressions may have a large or sometimes infinite number of equivalent expressions. Accelerating e-graph construction is crucial for making the use of e-graphs practical in compilers. In this paper, we present Caviar, an e-graph-based TRS for proving expressions within compilers. Caviar is a fast (20x faster than base e-graph TRS) and flexible (completely parameterized) TRS that that relies on three novel techniques: 1) a technique that stops e-graphs from growing when the goal is reached, called Iteration Level Check; 2) a mechanism that balances exploration and exploitation in the equality saturation algorithm, called Pulsing Caviar; 3) a technique to stop e-graph construction before reaching saturation when a non-provable pattern is detected, called Non-Provable Patterns Detection (NPPD). We evaluate caviar on Halide, an optimizing compiler that relies on a greedy-algorithm-based TRS to simplify and prove its expressions. The proposed techniques allow Caviar to accelerate e-graph expansion by 20x for the task of proving expressions. They also allow Caviar to prove 51% of the expressions that Halide's TRS cannot prove while being only 0.68x slower.