{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,28]],"date-time":"2026-02-28T22:36:52Z","timestamp":1772318212702,"version":"3.50.1"},"reference-count":71,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2021,10,15]],"date-time":"2021-10-15T00:00:00Z","timestamp":1634256000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1813166, 1749570"],"award-info":[{"award-number":["1813166, 1749570"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2021,10,20]]},"abstract":"<jats:p>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.<\/jats:p>\n          <jats:p>\n            This paper explores how equality saturation, a promising technique that uses e-graphs to\n            <jats:italic>apply<\/jats:italic>\n            rewrite rules, can also be used to\n            <jats:italic>infer<\/jats:italic>\n            rewrite 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.\n          <\/jats:p>\n          <jats:p>We prototyped these strategies in a tool dubbed Ruler. Compared to a similar tool built on CVC4, Ruler synthesizes 5.8\u00d7 smaller rulesets 25\u00d7 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.<\/jats:p>","DOI":"10.1145\/3485496","type":"journal-article","created":{"date-parts":[[2021,10,15]],"date-time":"2021-10-15T19:18:28Z","timestamp":1634325508000},"page":"1-28","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":31,"title":["Rewrite rule inference using equality saturation"],"prefix":"10.1145","volume":"5","author":[{"given":"Chandrakana","family":"Nandi","sequence":"first","affiliation":[{"name":"University of Washington, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8066-4218","authenticated-orcid":false,"given":"Max","family":"Willsey","sequence":"additional","affiliation":[{"name":"University of Washington, USA"}]},{"given":"Amy","family":"Zhu","sequence":"additional","affiliation":[{"name":"University of Washington, USA"}]},{"given":"Yisu Remy","family":"Wang","sequence":"additional","affiliation":[{"name":"University of Washington, USA"}]},{"given":"Brett","family":"Saiki","sequence":"additional","affiliation":[{"name":"University of Washington, USA"}]},{"given":"Adam","family":"Anderson","sequence":"additional","affiliation":[{"name":"University of Washington, USA"}]},{"given":"Adriana","family":"Schulz","sequence":"additional","affiliation":[{"name":"University of Washington, USA"}]},{"given":"Dan","family":"Grossman","sequence":"additional","affiliation":[{"name":"University of Washington, USA"}]},{"given":"Zachary","family":"Tatlock","sequence":"additional","affiliation":[{"name":"University of Washington, USA"}]}],"member":"320","published-online":{"date-parts":[[2021,10,15]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139172752"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/10720084_16"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1168857.1168906"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-17945-3_8"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.5555\/2032305.2032319"},{"key":"e_1_2_2_6_1","unstructured":"Clark Barrett Pascal Fontaine and Cesare Tinelli. 2016. The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org.  Clark Barrett Pascal Fontaine and Cesare Tinelli. 2016. The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org."},{"key":"e_1_2_2_7_1","volume-title":"Interactive Theorem Proving and Program Development: Coq\u2019Art The Calculus of Inductive Constructions","author":"Bertot Yves","year":"2058","edition":"1"},{"key":"e_1_2_2_8_1","volume-title":"Term Rewriting Systems","author":"Bezem M.","year":"2002"},{"key":"e_1_2_2_9_1","volume-title":"Survey on Instruction Selection: An Extensive and Modern Literature Review. CoRR, abs\/1306.4898","author":"Blindell Gabriel Hjort","year":"2013"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)82552-6"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3168821"},{"key":"e_1_2_2_12_1","volume-title":"Proceedings of the 13th USENIX Conference on Operating Systems Design and Implementation (OSDI\u201918)","author":"Chen Tianqi","year":"2018"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38574-2_27"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-13977-2_3"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71999-1"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/989393.989407"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(82)90026-3"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(87)80022-6"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1066100.1066102"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706346"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44881-0_3"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/368892.368907"},{"key":"e_1_2_2_25_1","unstructured":"Herbie. 2021. Herbie can generate more-complex expressions that aren\u2019t more precise. https:\/\/github.com\/uwplse\/herbie\/issues\/261#issuecomment-680896733  Herbie. 2021. Herbie can generate more-complex expressions that aren\u2019t more precise. https:\/\/github.com\/uwplse\/herbie\/issues\/261#issuecomment-680896733"},{"key":"e_1_2_2_26_1","unstructured":"Herbie. 2021. Optimize floating-point expressions for accuracy. https:\/\/github.com\/uwplse\/herbie\/issues  Herbie. 2021. Optimize floating-point expressions for accuracy. https:\/\/github.com\/uwplse\/herbie\/issues"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-35498-9_52"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359630"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-010-9193-y"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08434-3_9"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/543552.512566"},{"key":"e_1_2_2_32_1","volume-title":"Logic, Rewriting, and Concurrency","author":"Kirchner H\u00e9l\u00e8ne"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-81955-1_23"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/CGO51591.2021.9370308"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2644805"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454030"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45653-8_46"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/36177.36194"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/364995.365000"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062372"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-53413-7_16"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_44"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386012"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428234"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-020-00359-9"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-24258-9_20"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/2813885.2737959"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0028727"},{"key":"e_1_2_2_51_1","volume-title":"2001 Haskell Workshop (2001 haskell workshop ed.). https:\/\/www.microsoft.com\/en-us\/research\/publication\/playing-by-the-rules-rewriting-as-a-practical-optimisation-technique-in-ghc\/","author":"Jones Simon Peyton","year":"2001"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386001"},{"key":"e_1_2_2_53_1","unstructured":"Racket. 2021. Racket the Programming Language. https:\/\/racket-lang.org\/  Racket. 2021. Racket the Programming Language. https:\/\/racket-lang.org\/"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462176"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39176-7_19"},{"key":"e_1_2_2_56_1","unstructured":"Rust. 2021. Rust BigInt Library. https:\/\/docs.rs\/num-bigint\/0.4.0\/num_bigint\/struct.BigInt.html  Rust. 2021. Rust BigInt Library. https:\/\/docs.rs\/num-bigint\/0.4.0\/num_bigint\/struct.BigInt.html"},{"key":"e_1_2_2_57_1","unstructured":"Rust. 2021. Rust Rational Library. https:\/\/docs.rs\/num-rational\/0.4.0\/num_rational\/struct.Ratio.html  Rust. 2021. Rust Rational Library. https:\/\/docs.rs\/num-rational\/0.4.0\/num_rational\/struct.Ratio.html"},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594302"},{"key":"e_1_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/2858965.2814278"},{"key":"e_1_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2016.7886678"},{"key":"e_1_2_2_61_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81688-9_6"},{"key":"e_1_2_2_63_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_59"},{"key":"e_1_2_2_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/321879.321884"},{"key":"e_1_2_2_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480915"},{"key":"e_1_2_2_66_1","doi-asserted-by":"publisher","DOI":"10.1145\/3445814.3446707"},{"key":"e_1_2_2_67_1","volume-title":"Stratego: A Language for Program Transformation Based on Rewriting Strategies System Description of Stratego 0.5","author":"Visser Eelco","year":"2001"},{"key":"e_1_2_2_68_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)00270-1"},{"key":"e_1_2_2_69_1","doi-asserted-by":"publisher","DOI":"10.14778\/3407790.3407799"},{"key":"e_1_2_2_70_1","doi-asserted-by":"publisher","DOI":"10.1145\/267959.267960"},{"key":"e_1_2_2_71_1","unstructured":"Max Willsey. 2021. egg Documentation. https:\/\/docs.rs\/egg\/0.6.0\/egg\/struct.BackoffScheduler.html  Max Willsey. 2021. egg Documentation. https:\/\/docs.rs\/egg\/0.6.0\/egg\/struct.BackoffScheduler.html"},{"key":"e_1_2_2_72_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434304"},{"key":"e_1_2_2_73_1","doi-asserted-by":"publisher","DOI":"10.1145\/3355089.3356518"},{"key":"e_1_2_2_74_1","volume-title":"Proceedings of Machine Learning and Systems, A. Smola, A. Dimakis, and I. Stoica (Eds.). 3, 255\u2013268","author":"Yang Yichen","year":"2021"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3485496","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3485496","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3485496","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:18:40Z","timestamp":1750191520000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3485496"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,10,15]]},"references-count":71,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2021,10,20]]}},"alternative-id":["10.1145\/3485496"],"URL":"https:\/\/doi.org\/10.1145\/3485496","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,10,15]]},"assertion":[{"value":"2021-10-15","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}