École Nationale Supérieure de
Techniques Avancées

Résumé

When dealing with automatically generated formulas, the need for simplification arises quickly. Because this problem is not specific to the program generating these formulas, a more general tool is needed. Furthermore, having a tool that automatically generates the code that applies simplification makes adding simplification rules a lot easier, and allows for easier experimentation on the technique used to apply these simplifications. Here we focus on rewriting terms by following a bottom-up strategy, using a simplified version of e-graphs ([Nel80], [Wil+21]). This allows us to represent a term and its rewrite at the same time, to enable the use of equality saturation ([Tat+09]).