E-graphs are a data structure that compactly represents equivalent expressions. They are constructed via the repeated application of rewrite rules. Often in practical applications, conditional rewrite rules are crucial, but their application requires the detection - at the time the e-graph is being built - that a condition is valid in the domain of application. Detecting condition validity amounts to proving a property of the program. Abstract interpretation is a general method to learn such properties, traditionally used in static analysis tools. We demonstrate that abstract interpretation and e-graph analysis naturally reinforce each other through a tight integration because (i) the e-graph clustering of equivalent expressions induces natural precision refinement of abstractions and (ii) precise abstractions allow the application of deeper rewrite rules (and hence potentially even greater precision). We develop the theory behind this intuition and present an exemplar interval arithmetic implementation, which we apply to the FPBench suite.

翻译：E-graphs是一种紧凑表示等价表达式的数据结构，通过重复应用重写规则构建。在实际应用中，条件重写规则至关重要，但其应用需要在构建e-graph时检测条件在应用域中的有效性。检测条件有效性相当于证明程序的某个属性。抽象解释是一种学习此类属性的通用方法，传统上用于静态分析工具中。我们证明，通过紧密集成，抽象解释和e-graph分析能够自然相互强化，原因在于：(i) e-graph对等价表达式的聚类能自然地提升抽象精度；(ii) 精确的抽象允许应用更深层的重写规则（从而可能实现更高的精度）。我们为该直觉建立了理论框架，并实现了一个区间算术示例，将其应用于FPBench测试套件。