167 citations · 170 across the 4 of their papers we have counts for
5 papers · 1 filter
Efficient Extraction for Effectful E-Graphs
Oliver Flatt, Anjali Pal, Yihong Zhang +7
Egraphs have enabled recent advances in program optimization, synthesis, and verification, yet remain difficult to apply to effectful programs whose memory and I/O operations must…
Equality saturation theory exploration à la carte
Anjali Pal, Brett Saiki, Ryan Tjoa +6
Rewrite rules are critical in equality saturation, an increasingly popular technique in optimizing compilers, synthesizers, and verifiers. Unfortunately, developing high-quality ru…
Better Together: Unifying Datalog and Equality Saturation
Yihong Zhang, Yisu Remy Wang, Oliver Flatt +5
We present egglog, a fixpoint reasoning system that unifies Datalog and equality saturation (EqSat). Like Datalog, it supports efficient incremental execution, cooperating analyses…
Small Proofs from Congruence Closure
Oliver Flatt, Samuel Coward, Max Willsey +2
Satisfiability Modulo Theory (SMT) solvers and equality saturation engines must generate proof certificates from e-graph-based congruence closure procedures to enable verification…
egg: Fast and Extensible Equality Saturation
Max Willsey, Chandrakana Nandi, Yisu Remy Wang +3
An e-graph efficiently represents a congruence relation over many expressions. Although they were originally developed in the late 1970s for use in automated theorem provers, a mor…