E-graphs are a prominent data structure that has been increasing in popularity in recent years due to their expanding range of applications in various formal reasoning tasks. Often, they are used for equality saturation, a process of deriving consequences through repeatedly applying universally quantified equality formulas via term rewriting. They handle equality reasoning over a large spaces of terms, but are severely limited in their handling of case splitting and other types of logical cuts, especially when compared to other reasoning techniques such as sequent calculi and resolution. The main difficulty is when equality reasoning requires multiple inconsistent assumptions to reach a single conclusion. Ad-hoc solutions, such as duplicating the e-graph for each assumption, are available, but they are notably resource-intensive. We introduce a key observation is that each duplicate e-graph (with an added assumption) corresponds to coarsened congruence relation. Based on that, we present an extension to e-graphs, called Colored E-Graphs, as a way to represent all of the coarsened congruence relations in a single structure. A colored e-graph is a memory-efficient equivalent of multiple copies of an e-graph, with a much lower overhead. This is attained by sharing as much as possible between different cases, while carefully tracking which conclusion is true under which assumption. Support for multiple relations can be thought of as adding multiple "color-coded" layers on top of the original e-graph structure, leading to a large degree of sharing. In our implementation, we introduce optimizations to rebuilding and e-matching. We run experiments and demonstrate that our colored e-graphs can support hundreds of assumptions and millions of terms with space requirements that are an order of magnitude lower, and with similar time requirements.

翻译：E-graph是一种重要的数据结构，近年来因其在各种形式化推理任务中不断扩大的应用范围而日益受到关注。通常，它们被用于等式饱和——通过反复应用全称量化的等式公式进行项重写来推导结论的过程。虽然E-graph能够在庞大的项空间中进行等式推理，但在处理情况分裂和其他类型的逻辑切割时存在严重局限，尤其是与相继式演算和归结等其他推理技术相比。主要困难在于当等式推理需要多个不一致的假设才能得出单一结论时。虽然存在一些临时解决方案（如为每个假设复制E-graph），但这些方法资源消耗显著。我们提出一个关键观察：每个复制的E-graph（包含一个额外假设）都对应一个粗化的同余关系。基于此，我们提出E-graph的扩展——彩色E-graph，作为在单一结构中表示所有粗化同余关系的方法。彩色E-graph在内存效率上相当于多个E-graph副本，且开销显著降低。这是通过在不同情况之间尽可能共享，同时仔细追踪每个结论在何种假设下成立来实现的。对多重关系的支持可视为在原始E-graph结构之上添加多个"颜色编码"层，从而实现高度共享。在我们的实现中，我们引入了针对重建和e-matching的优化。实验证明，我们的彩色E-graph能够支持数百个假设和数百万个项，空间需求降低一个数量级，时间需求与原始方法相当。