Abstract Interpretation on E-Graphs

TL;DR

This paper explores applying abstract interpretation to e-graphs, demonstrating how using interval arithmetic can improve the precision of equivalence over-approximations within e-graphs.

Contribution

It introduces a novel approach of integrating abstract interpretation with e-graphs, enhancing the precision of equivalence classes through lattice meet operations.

Findings

Using interval arithmetic improves over-approximation precision.

Lattice meet operation has a natural interpretation in e-graphs.

Abstract interpretation can be effectively applied to e-graph analysis.

Abstract

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.