Better Together: Unifying Datalog and Equality Saturation

[Submitted on 10 Apr 2023 (v1), last revised 11 Apr 2023 (this version, v2)]

Title:Better Together: Unifying Datalog and Equality Saturation

Download a PDF of the paper titled Better Together: Unifying Datalog and Equality Saturation, by Yihong Zhang and 7 other authors

Download PDF

Abstract: 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.

Submission history

From: Yihong Zhang [view email]

[v1] Mon, 10 Apr 2023 00:04:56 UTC (12,929 KB)

[v2] Tue, 11 Apr 2023 17:38:35 UTC (12,783 KB)

from Hacker News https://ift.tt/t9jhaKQ