Abstract Interpretation on E-Graphs
This work addresses a domain-specific issue for researchers in program analysis and verification, presenting an incremental improvement.
The paper tackles the problem of equivalences in e-graphs not holding across different interpretations by applying abstract interpretation to e-graphs, showing that the lattice meet operation improves precision in over-approximation, as illustrated with Interval Arithmetic.
Recent e-graph applications have typically considered concrete semantics of expressions, where the notion of equivalence stems from concrete interpretation of expressions. However, equivalences that hold over one interpretation may not hold in an alternative interpretation. Such an observation can be exploited. We consider the application of abstract interpretation to e-graphs, and show that within an e-graph, the lattice meet operation associated with the abstract domain has a natural interpretation for an e-class, leading to improved precision in over-approximation. In this extended abstract, we use Interval Arithmetic (IA) to illustrate this point.