ICFP 2023
Mon 4 - Sat 9 September 2023 Seattle, Washington, United States

Rewrite rules are critical in equality saturation, a technique with applications in compiler optimization, formal verification, and program synthesis. However, the process of maintaining and updating rulesets is difficult, in no small part because a valid ruleset is not necessarily a good ruleset. If a ruleset is too small, then results will be suboptimal due to missing rules; on the other hand, rules that are not useful, either because they are not used by the application or because they are redundant, will cause equality saturation to hit its resource limits prematurely. Therefore, it is important for a ruleset to contain a small, effective set of axioms. An intuitive method for comparing rulesets is needed. We propose the use of the derivability heuristic, where a rule is said to be derivable by a ruleset, 𝑅, if its left- and right-hand sides are determined to be equivalent using 𝑅’s rules. Here, we expand the notion of derivability introduced in prior work, argue that it should be defined in relation to the equality saturation application in which it is used, and evaluate different definitions of derivability on a variety of domains.