Authors: Anjali Pal, Brett Saiki, Ryan Tjoa, Cynthia Richey, Amy Zhu, Oliver Flatt, Max Willsey, Zachary Tatlock, Chandrakana Nandi

Venue: Object-Oriented Programming, Systems, Languages and Applications (OOPSLA) 2023

Links: Paper

Abstract

Rewrite rules are critical in equality saturation, an increasingly popular technique in optimizing compilers, synthesizers, and verifiers. Unfortunately, developing high-quality rulesets is difficult and error-prone. Recent work on automatically inferring rewrite rules does not scale to large terms or grammars, and existing rule inference tools are monolithic and opaque. Equality saturation users therefore struggle to guide inference and incrementally construct rulesets. As a result, most users still manually develop and maintain rulesets. This paper proposes Enumo, a new domain-specific language for programmable theory exploration. Enumo provides a small set of core operators that enable users to strategically guide rule inference and incrementally build rulesets. Short Enumo programs easily replicate results from state-of-the-art tools, but Enumo programs can also scale to infer deeper rules from larger grammars than prior approaches. Its composable operators even facilitate developing new strategies for ruleset inference. We introduce a new fast-forwarding strategy that does not require evaluating terms in the target language, and can thus support domains that were out of scope for prior work.

We evaluate Enumo and fast-forwarding across a variety of domains. Compared to state-of-the-art techniques, Enumo can synthesize better rulesets over a diverse set of domains, in some cases matching the effects of manually-developed rulesets in systems driven by equality saturation

@article{10.1145/3622834,
author = {Pal, Anjali and Saiki, Brett and Tjoa, Ryan and Richey, Cynthia and Zhu, Amy and Flatt, Oliver and Willsey, Max and Tatlock, Zachary and Nandi, Chandrakana},
title = {Equality Saturation Theory Exploration \`{a} la Carte},
year = {2023},
issue_date = {October 2023},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {7},
number = {OOPSLA2},
url = {https://doi.org/10.1145/3622834},
doi = {10.1145/3622834},
abstract = {Rewrite rules are critical in equality saturation, an increasingly popular technique  in optimizing compilers, synthesizers, and verifiers. Unfortunately,   developing high-quality rulesets is difficult and error-prone. Recent   work on automatically inferring rewrite rules does not scale to large   terms or grammars, and existing rule inference tools are monolithic and   opaque. Equality saturation users therefore struggle to guide inference and   incrementally construct rulesets. As a result, most users still   manually develop and maintain rulesets.    This paper proposes Enumo, a new domain-specific language for   programmable theory exploration. Enumo provides a small set of core   operators that enable users to strategically guide rule inference and   incrementally build rulesets. Short Enumo programs easily replicate   results from state-of-the-art tools, but Enumo programs can also scale   to infer deeper rules from larger grammars than prior approaches. Its   composable operators even facilitate developing new strategies for   ruleset inference. We introduce a new fast-forwarding strategy that does not require  evaluating terms in the target language, and can thus support domains   that were out of scope for prior work.    We evaluate Enumo and fast-forwarding across a variety of domains. Compared to   state-of-the-art techniques, enumo can synthesize better rulesets over a   diverse set of domains, in some cases matching the effects of   manually-developed rulesets in systems driven by equality saturation.},
journal = {Proc. ACM Program. Lang.},
month = oct,
articleno = {258},
numpages = {29},
keywords = {Rewrite rules, equality saturation, program synthesis}
}