Expression Simplification Using E-Graphs for Interval Evaluation

Abstract: Daisy is a framework for verifying and bounding the magnitudes of rounding errors introduced by floating-point arithmetic in numerical programs. As part of this, Daisy employs a rudimentary algorithm for simplifying expressions derived from the programs. We show that more advanced simplifications allow Daisy to prove tighter, and thereby more accurate error bounds. Furthermore, we design a simplification algorithm using e-graphs and equality saturation to provide these more advanced simplifications, and implement this in a tool named Oᴍᴇʟᴇᴛᴛᴇ.Expressions can be extracted from Oᴍᴇʟᴇᴛᴛᴇ using an arbitrary metric. To decide the metric optimal for use in Daisy, we define several and find that prioritizing expressions with a small range of possible values yields the lowest bound of rounding errors. We also introduce an optimization where rounding errors are computed directly from equivalences proved, and not from a simplified expression. Compared to the current algorithm, we find that Oᴍᴇʟᴇᴛᴛᴇ yields a 15% more accurate rounding error on average when using this optimization — with some benchmarks in particular showing significant improvement. This improvement comes at the cost of a longer running time as Oᴍᴇʟᴇᴛᴛᴇ is on average 3.5x slower than the current algorithm.