More Like this

1. Database Theory in Action: Search-Based Program Optimization

   https://doi.org/10.4230/LIPICS.ICDT.2025.34  

   Zhang, Yihong; Suciu, Dan; Wang, Yisu Remy; Willsey, Max (January 2025, Schloss Dagstuhl – Leibniz-Zentrum für Informatik)

   Roy, Sudeepa; Kara, Ahmet (Ed.)

   Recent work in programming languages developed an approach to term rewritings based on equality saturation (EqSat), which, instead of applying destructively the rewrite rules, maintains all equivalent expressions in a structure called an E-graph. This paper describes two surprising connections between EqSat and databases, going both ways. On one hand equality saturation can be viewed as a query evaluation problem, with great benefits. On the other hand, most sophisticated SQL query optimizers are based on the Volcano/Cascades framework which, we explain, is a variant of EqSat. 

   more » « less
2. egg: Fast and extensible equality saturation

   https://doi.org/10.1145/3434304  

   Willsey, Max; Nandi, Chandrakana; Wang, Yisu_Remy; Flatt, Oliver; Tatlock, Zachary; Panchekha, Pavel (January 2021, Proceedings of the ACM on Programming Languages)

   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 more recent technique known as equality saturation repurposes e-graphs to implement state-of-the-art, rewrite-driven compiler optimizations and program synthesizers. However, e-graphs remain unspecialized for this newer use case. Equality saturation workloads exhibit distinct characteristics and often require ad-hoc e-graph extensions to incorporate transformations beyond purely syntactic rewrites. This work contributes two techniques that make e-graphs fast and extensible, specializing them to equality saturation. A new amortized invariant restoration technique called rebuilding takes advantage of equality saturation's distinct workload, providing asymptotic speedups over current techniques in practice. A general mechanism called e-class analyses integrates domain-specific analyses into the e-graph, reducing the need for ad hoc manipulation. We implemented these techniques in a new open-source library called egg. Our case studies on three previously published applications of equality saturation highlight how egg's performance and flexibility enable state-of-the-art results across diverse domains. 

   more » « less
3. CCLemma: E-Graph Guided Lemma Discovery for Inductive Equational Proofs

   https://doi.org/10.1145/3674653  

   Kurashige, Cole; Ji, Ruyi; Giridharan, Aditya; Barbone, Mark; Noor, Daniel; Itzhaky, Shachar; Jhala, Ranjit; Polikarpova, Nadia (August 2024, Proceedings of the ACM on Programming Languages)

   The problem of automatically proving the equality of terms over recursive functions and inductive data types is challenging, as such proofs often require auxiliary lemmas which must themselves be proven. Previous attempts at lemma discovery compromise on either efficiency or efficacy.Goal-directedapproaches are fast but limited in expressiveness, as they can only discover auxiliary lemmas which entail their goals.Theory explorationapproaches are expressive but inefficient, as they exhaustively enumerate candidate lemmas. We introducee-graph guided lemma discovery, a new approach to finding equational proofs that makes theory exploration goal-directed. We accomplish this by using e-graphs and equality saturation to efficiently construct and compactly represent the space ofallgoal-oriented proofs. This allows us to explore only those auxiliary lemmasguaranteedto help make progress on some of these proofs. We implemented our method in a new prover called CCLemma and compared it with three state-of-the-art provers across a variety of benchmarks. CCLemma performs consistently well on two standard benchmarks and additionally solves 50% more problems than the next best tool on a new challenging set. 

   more » « less
4. Rewrite rule inference using equality saturation

   https://doi.org/10.1145/3485496  

   Nandi, Chandrakana; Willsey, Max; Zhu, Amy; Wang, Yisu_Remy; Saiki, Brett; Anderson, Adam; Schulz, Adriana; Grossman, Dan; Tatlock, Zachary (October 2021, Proceedings of the ACM on Programming Languages)

   Many compilers, synthesizers, and theorem provers rely on rewrite rules to simplify expressions or prove equivalences. Developing rewrite rules can be difficult: rules may be subtly incorrect, profitable rules are easy to miss, and rulesets must be rechecked or extended whenever semantics are tweaked. Large rulesets can also be challenging to apply: redundant rules slow down rule-based search and frustrate debugging. This paper explores how equality saturation, a promising technique that uses e-graphs toapplyrewrite rules, can also be used toinferrewrite rules. E-graphs can compactly represent the exponentially large sets of enumerated terms and potential rewrite rules. We show that equality saturation efficiently shrinks both sets, leading to faster synthesis of smaller, more general rulesets. We prototyped these strategies in a tool dubbed Ruler. Compared to a similar tool built on CVC4, Ruler synthesizes 5.8× smaller rulesets 25× faster without compromising on proving power. In an end-to-end case study, we show Ruler-synthesized rules which perform as well as those crafted by domain experts, and addressed a longstanding issue in a popular open source tool. 

   more » « less
5. Co-Optimization of Design and Fabrication Plans for Carpentry

   https://doi.org/10.1145/3508499  

   Zhao, Haisen; Willsey, Max; Zhu, Amy; Nandi, Chandrakana; Tatlock, Zachary; Solomon, Justin; Schulz, Adriana (June 2022, ACM Transactions on Graphics)

   Past work on optimizing fabrication plans given a carpentry design can provide Pareto-optimal plans trading off between material waste, fabrication time, precision, and other considerations. However, when developing fabrication plans, experts rarely restrict to a single design , instead considering families of design variations , sometimes adjusting designs to simplify fabrication. Jointly exploring the design and fabrication plan spaces for each design is intractable using current techniques. We present a new approach to jointly optimize design and fabrication plans for carpentered objects. To make this bi-level optimization tractable, we adapt recent work from program synthesis based on equality graphs (e-graphs), which encode sets of equivalent programs. Our insight is that subproblems within our bi-level problem share significant substructures. By representing both designs and fabrication plans in a new bag of parts (BOP) e-graph, we amortize the cost of optimizing design components shared among multiple candidates. Even using BOP e-graphs, the optimization space grows quickly in practice. Hence, we also show how a feedback-guided search strategy dubbed Iterative Contraction and Expansion on E-graphs (ICEE) can keep the size of the e-graph manageable and direct the search towards promising candidates. We illustrate the advantages of our pipeline through examples from the carpentry domain. 

   more » « less