Equality saturation is an increasingly popular term rewriting technique that uses equivalence graphs (e-graphs). Modern equality saturation engines are fast and extensible, leading to the development of several e-graph applications across multiple domains, including compiler optimization and program synthesis. However, equality saturation engines are not memory scalable, forcing application designers to choose between practicality and expression quality.

In this paper, we present CERES, a new rewrite scheduler to improve the memory scalability of equality saturation. The core of CERES is a novel algorithm to approximate the subset of important rewrites to apply at each iteration. We evaluate CERES on Herbie, a widely used application that utilizes equality saturation for improving the accuracy of floating-point expressions. We show that CERES achieves similar expression quality for e-graphs in Herbie’s Hamming benchmark within an 8–12× lower memory budget, and, for the same memory budget, CERES achieves a 40–62% reduction in expression cost over the default Backoff Scheduler.

At the EGRAPHS workshop, we’ll present CERES and its benefits across multiple e-graph applications. We hope to work with the e-graph community to integrate CERES with upstream repositories of egg and egglog for wider adoption.