E-graphs are a data structure for equational reasoning and optimization over ground terms. One of the benefits of e-graph rewriting is that it can declaratively handle useful but difficult to orient identities like associativity and commutativity (AC) in a generic way. However, using these generic mechanisms is more computationally expensive than using bespoke routines on terms containing sets, multi-sets, linear expressions, polynomials, and binders. A natural question arises: How can one combine the generic capabilities of e-graph rewriting with these specialized theories. This paper discusses a pragmatic approach to this e-graphs modulo theories (EMT) question using two key ideas: bottom-up e-matching and semantic e-ids.

翻译：E图是一种用于地面项等式推理与优化的数据结构。E图重写的优势之一在于能够以声明式方法通用地处理有用但难以定向的恒等式，如结合律与交换律（AC）。然而，相比在包含集合、多重集、线性表达式、多项式及绑定符的项上使用定制化程序，这些通用机制的计算成本更高。一个自然的问题随之产生：如何将E图重写的通用能力与这些专用理论相结合？本文通过两个核心思想——自底向上E-匹配与语义E标识符，探讨了解决这一“模理论E图”问题的实用方法。