Refinement E-Graphs
Summary
The article introduces Refinement E-Graphs, an extension of traditional e-graphs that bakes in a monotone <= relation, enabling inequality-based reasoning alongside standard equality. It explains the theory, demonstrates a toy Python implementation (LE_EGraph), presents examples and experiments, and discusses Don’t Care semantics, e-matching, and extraction. It also surveys potential applications and related work, suggesting refinement closure as a practical area for further exploration.