Conditional Rewrite Rule Synthesis Using E-Graphs and Implication Propagation

Abstract

Compilers, synthesizers, and theorem provers rely on rich rulesets for manipulating expressions via rewriting, but developing such rules remains difficult and error-prone. While prior work has automated synthesis of rewrite rules, it has focused largely on strict equalities, leaving conditional rewrites largely unsupported. Conditional rule synthesis explores a much larger search space because it must search for both the rule body and the condition. Effective pruning of the space is crucial for scaling synthesis to large grammars. The commonly used “derivability” metric for eliminating redundant rules in the strict setting does not extend directly to the conditional case. A conditional rule may be redundant not only when its body and condition are equivalent to a rule, but also when its condition implies a condition of a more general rule. We present CHOMPY, a tool for synthesizing conditional rewrite rules. CHOMPY’s core contribution is implication propagation, a technique that lifts equality saturation to the predicate level to discover logical implications between conditions, then uses those implications to obtain a new notion of conditional derivability and ruleset minimization. To evaluate CHOMPY, we compare the synthesized conditional ruleset to handwritten ones from Caviar (an equality saturation theorem prover) and Halide’s term rewriting system. CHOMPY’s rewrites derive 73.3% of Caviar’s and 57.1% of Halide’s conditional rules. CHOMPY outperforms an LLM-only baseline on both benchmarks. Unlike the LLM’s substantially variable output across runs, CHOMPY’s results are deterministic and stable.