一句话：提出版本化 E-Graph，同时编码多个等价集合与共享信息，并证明其正确性，显著提升条件等价场景性能。
E-Graph 能高效表示并维护一组等式，但其一次只能编码单个等价集合，因此条件等式（如自动证明中不同分支下的等式）通常需要为每个分支维护多个 E-Graph，导致共享等式被大量复制。本文提出版本化 E-Graph，在单一结构中同时编码多个等价集合，并最大化版本间的信息共享；作者给出形式化定义并证明正确性。与维护多个 E-Graph 的常用方案相比，版本化 E-Graph 在多个案例中内存效率提升 5–30%，最高加速 4 倍，当被探索的程序项和分支数量很大时优势尤其明显。
E-Graphs are an efficient encoding for discovering and maintaining sets of equalities, commonly adopted in the context of formal proofs, program analysis, and optimization. In several scenarios, equalities may hold only conditionally, i.e., under certain assumptions. For example, in automated provers the proof is often split into multiple branches, such that each branch considers a different set of equalities. A limitation of traditional e-graphs is that they can only encode a single set of equalities at a time. Conditional equalities are then handled by maintaining multiple e-graphs, e.g., one for each branch in the proof, which is inefficient as equalities shared among branches are simply replicated many times. In this paper, we introduce versioned e-graphs, which efficiently encode multiple equivalence sets at the same time, maximizing shared information among them. We formalize for versioned e-graphs and prove their correctness. We evaluate our solution against widely-adopted solutions which maintain multiple e-graphs and show that versioned e-graphs are up to 5–30 % more memory efficient and up to 4× faster depending on the case study, especially when solution spaces are large both in explored program terms and number of branches.
@article{CesarioZWS26,
title = {Versioned E-Graphs},
author = {Jahrim Gabriele Cesario and George Zakhour and Pascal Weisenburger and Guido Salvaneschi},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {PLDI},
year = {2026},
doi = {10.1145/3808249}
}