We present egglog, a fixpoint reasoning system that unifies Datalog and equality saturation (EqSat). Like Datalog, it supports efficient incremental execution, cooperating analyses, and lattice-based reasoning. Like EqSat, it supports term rewriting, efficient congruence closure, and extraction of optimized terms. We identify two recent applications--a unification-based pointer analysis in Datalog and an EqSat-based floating-point term rewriter--that have been hampered by features missing from Datalog but found in EqSat or vice-versa. We evaluate egglog by reimplementing those projects in egglog. The resulting systems in egglog are faster, simpler, and fix bugs found in the original systems.

翻译：我们提出egglog，一个统一Datalog与等式饱和（EqSat）的不动点推理系统。与Datalog类似，它支持高效的增量执行、协作分析以及基于格（lattice）的推理。与EqSat类似，它支持术语重写、高效的合闭包（congruence closure）以及优化术语的提取。我们识别出两个近期应用——基于统一（unification）的Datalog指针分析和基于EqSat的浮点术语重写器——它们分别因缺少对方系统中存在的特性而受到限制。我们通过在egglog中重新实现这些项目来评估egglog。最终在egglog中实现的系统更快、更简洁，并修复了原始系统中存在的错误。