Dis/Equality Graphs
summary
The paper develops an abstract, extensible framework that proves e-graphs encode the smallest reflexive, symmetric, transitive, congruent closure and adds direct disequality support, implements it as an egg Rust extension, and evaluates it in an SMT core and an automated prover. Analytic and empirical results show direct disequality support outperforms embeddings: profiling on 7,600 SMT-LIB benchmarks and prover traces finds significant time and memory savings; they proved equivalence to RSTC closure and show the structural (Nelson) disequality edges wins in practice.
AI-written summary · about