  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 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
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.8X smaller rulesets 25X 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.

Programming Languages