Rewrite Rule Inference Using Equality Saturation
09/11/2021, 10:30am
Speaker
Abstract
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 can slow down rule-based search and frustrate debugging.
This talk explores how equality saturation, a promising technique that uses e-graphs to apply rewrite rules, can also be used to infer rewrite rules. E-graphs can compactly represent the exponentially large sets of enumerated terms and potential rewrite rules. We will see how equality saturation efficiently shrinks both sets, leading to faster synthesis of smaller, moregeneral rulesets.
Compared to a similar tool built on CVC4, our tool, dubbed Ruler, synthesizes 5.8X smaller rulesets 25X faster without compromising on proving power. We will also see how Ruler-synthesized rules perform as well as those crafted by domain experts by using a numerical program synthesis tool as a case study.
Speaker Bio
Chandra is a Senior Researcher at Certora Inc. Her current research interest lies in program optimization and program synthesis. She recently graduated with a PhD in Programming Languages and Software Engineering from University of Washington. During her PhD, she focused on developing DSLs, compilers, and program synthesizers for computational geometry. Much of her work is on using a term-rewriting technique called equality saturation to optimize and synthesize programs which has since been used in a wide range of domains. Her work has won several awards including an Adobe Fellowship and a POPL Best Paper Award. Outside of work, she enjoys long distance running with friends.