Better Together: Unifying Datalog and Equality Saturation
summary
egglog claims a single system that combines Datalog-style declarative analyses with equality-saturation rewriting by introducing functional dependency repair and a union‑find backed, database-style representation. It implements relational imaging and semi‑naive incremental evaluation to get incremental equality saturation, yielding a 9.27× speedup versus egg on microbenchmarks and almost 5× on a points‑to case study. The team reimplements Herbie and a unification‑based pointer analysis, restores soundness for Herbie, fixes bugs, and matches or improves performance.
AI-written summary · about
chapters (14)
- 0:00EOG introduction and goals
- 1:02Equality saturation background
- 3:54E-class analysis limits
- 4:59Datalog for e-matching
- 6:43EOG core mechanism
- 8:05Functional dependency repair
- 9:08Composable program analysis
- 10:12Performance evaluation
- 11:16Herby floating-point case
- 12:39Datalog analysis case
- 13:44EOG unified benefits
- 14:05EOG language demo
- 14:28Q&A: Dependency repair
- 15:35Q&A: Extraction problem
related talks
01h 01mDatalog and Equality Saturation
30megg: Fast and Extensible Equality Saturation
20mEquality Saturation and Joins
19mTowards Relational Contextual Equality Saturation
19meqsat: An Equality Saturation Dialect for Non-destructive Rewriting
28mBridging Syntax and Semantics of Lean Expressions in E-Graphs
26mEquality Saturation Guided by Large Language Models
22mOatlog: A performant ahead-of-time compiled e-graph engine