{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,24]],"date-time":"2026-08-24T08:40:01Z","timestamp":1787560801190,"version":"build-2736575974"},"reference-count":41,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2025,1,7]],"date-time":"2025-01-07T00:00:00Z","timestamp":1736208000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100001711","name":"Schweizerischer Nationalfonds zur F\u00f6rderung der Wissenschaftlichen Forschung","doi-asserted-by":"crossref","award":["200429"],"award-info":[{"award-number":["200429"]}],"id":[{"id":"10.13039\/501100001711","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,1,7]]},"abstract":"<jats:p>E-graphs are a data structure to compactly represent a program space and reason about equality of program terms. E-graphs have been successfully applied to a number of domains, including program optimization and automated theorem proving. In many applications, however, it is necessary to reason about disequality of terms as well as equality. While disequality reasoning can be encoded, direct support for disequalities increases performance and simplifies the metatheory.<\/jats:p>\n                  <jats:p>In this paper, we develop a framework independent of a specific implementation to formally reason about e-graphs. For the first time, we prove the equivalence of e-graphs to the reflexive, symmetric, transitive, and congruent closure of the equivalence relation they are expected to encode. We use these results to present the first formalization of an extension of e-graphs that directly supports disequalities and prove an analytical result about their superior efficiency compared to embedding techniques that are commonly used in SMT solvers and automated verifiers. We further profile an SMT solver and find that it spends a measurable amount of time handling disequalities.<\/jats:p>\n                  <jats:p>We implement our approach in an extension to egg, a popular e-graph Rust library. We evaluate our solution in an SMT solver and an automated theorem prover using standard benchmarks. The results indicate that direct support for disequalities outperforms other encodings based on equality embedding, confirming the results obtained analytically.<\/jats:p>","DOI":"10.1145\/3704913","type":"journal-article","created":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T05:48:42Z","timestamp":1736401722000},"page":"2282-2305","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Dis\/Equality Graphs"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0009-0000-5042-1207","authenticated-orcid":false,"given":"George","family":"Zakhour","sequence":"first","affiliation":[{"name":"University of St. Gallen, St Gallen, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1288-1485","authenticated-orcid":false,"given":"Pascal","family":"Weisenburger","sequence":"additional","affiliation":[{"name":"University of St. Gallen, St Gallen, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-1448-5676","authenticated-orcid":false,"given":"Jahrim Gabriele","family":"Cesario","sequence":"additional","affiliation":[{"name":"University of St. Gallen, St Gallen, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9324-8894","authenticated-orcid":false,"given":"Guido","family":"Salvaneschi","sequence":"additional","affiliation":[{"name":"University of St. Gallen, St Gallen, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,1,9]]},"reference":[{"key":"e_1_3_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133906"},{"key":"e_1_3_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"e_1_3_2_4_1","unstructured":"Clark Barrett Pascal Fontaine and Cesare Tinelli. 2015. The Satisfiability Modulo Theories Library (SMT-LIB). Retrieved November 20 2024 from https:\/\/smt-lib.org\/."},{"key":"e_1_3_2_5_1","doi-asserted-by":"publisher","unstructured":"Ian Briggs and Pavel Panchekha. 2022. Synthesizing Mathematical Identities with E-Graphs. In Proceedings of the 1st ACM SIGPLAN International Symposium on E-Graph Research Applications Practices and Human-Factors (San Diego CA USA) (EGRAPHS \u201922). ACM New York NY USA 1\u20136. https:\/\/doi.org\/10.1145\/3520308.3534506 10.1145\/3520308.3534506","DOI":"10.1145\/3520308.3534506"},{"key":"e_1_3_2_6_1","doi-asserted-by":"publisher","unstructured":"Roberto Bruttomesso Edgar Pek Natasha Sharygina and Aliaksei Tsitovich. 2010. The OpenSMT Solver. In Proceedings of the 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (Paphos Cyprus) (TACAS \u201910) Javier Esparza and Rupak Majumdar (Eds.). Springer-Verlag Berlin Heidelberg 150\u2013153. https:\/\/doi.org\/10.1007\/978-3-642-12002-2_12 10.1007\/978-3-642-12002-2_12","DOI":"10.1007\/978-3-642-12002-2_12"},{"key":"e_1_3_2_7_1","unstructured":"Bytecode Alliance. 2016. Cranelift. Retrieved November 20 2024 from https:\/\/cranelift.dev\/. Optimizing compiler backend."},{"key":"e_1_3_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571207"},{"key":"e_1_3_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-20615-8_23"},{"key":"e_1_3_2_10_1","unstructured":"Leonardo de Moura. 2008. SMT Solvers: Theory and Implementation. Retrieved November 20 2024 from https:\/\/leodemoura.github.io\/files\/oregon08.pdf. Presentation at the Summer School on Logic and Theorem Proving in Programming Languages Oregon."},{"key":"e_1_3_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73595-3_13"},{"key":"e_1_3_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1066100.1066102"},{"key":"e_1_3_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-019-09519-x"},{"key":"e_1_3_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24605-3_37"},{"key":"e_1_3_2_16_1","doi-asserted-by":"publisher","DOI":"10.34727\/2022\/isbn.978-3-85448-053-2_13"},{"key":"e_1_3_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/364099.364331"},{"key":"e_1_3_2_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICST57152.2023.00035"},{"key":"e_1_3_2_19_1","doi-asserted-by":"publisher","DOI":"10.1137\/0202024"},{"key":"e_1_3_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512566"},{"key":"e_1_3_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547622"},{"key":"e_1_3_2_22_1","first-page":"527","volume-title":"Proceedings of the 17th International Conference on Machine Learning (ICML \u201900)","author":"Lau Tessa","year":"2000","unstructured":"Tessa Lau, Pedro Domingos, and Daniel S. Weld. 2000. Version Space Algebra and its Application to Programming by Demonstration. In Proceedings of the 17th International Conference on Machine Learning (ICML \u201900). Morgan Kaufmann Publishers Inc., San Francisco, CA, USA, 527\u2013534."},{"key":"e_1_3_2_23_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1025671410623"},{"key":"e_1_3_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386012"},{"key":"e_1_3_2_25_1","volume-title":"Techniques for Program Verification","author":"Nelson Charles Gregory","year":"1980","unstructured":"Charles Gregory Nelson. 1980. Techniques for Program Verification. Ph. D. Dissertation. Stanford, CA, USA. AAI8011683."},{"key":"e_1_3_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72013-1_8"},{"key":"e_1_3_2_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-32033-3_33"},{"key":"e_1_3_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3622834"},{"key":"e_1_3_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737959"},{"key":"e_1_3_2_30_1","doi-asserted-by":"publisher","unstructured":"Gordon D. Plotkin. 2004. A Structural Approach to Operational Semantics. The Journal of Logic and Algebraic Programming 60\u201361 (2004) 17\u2013139. https:\/\/doi.org\/10.1016\/j.jlap.2004.05.001 10.1016\/j.jlap.2004.05.001","DOI":"10.1016\/j.jlap.2004.05.001"},{"key":"e_1_3_2_31_1","doi-asserted-by":"publisher","DOI":"10.34727\/2024\/isbn.978-3-85448-065-5_13"},{"key":"e_1_3_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/321879.321884"},{"key":"e_1_3_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480915"},{"key":"e_1_3_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3445814.3446707"},{"key":"e_1_3_2_35_1","doi-asserted-by":"publisher","DOI":"10.14778\/3407790.3407799"},{"key":"e_1_3_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434304"},{"key":"e_1_3_2_37_1","unstructured":"Yichen Yang Phitchaya Mangpo Phothilimthana Yisu Remy Wang Max Willsey Sudip Roy and Jacques Pienaar. 2021. Equality Saturation for Tensor Graph Superoptimization. In Proceedings of the 4th Conference on Machine Learning and Systems (MLSys \u201921) Alex Smola Alex Dimakis and Ion Stoica (Eds.). MLSys."},{"key":"e_1_3_2_38_1","doi-asserted-by":"publisher","unstructured":"George Zakhour Pascal Weisenburger Jahrim Gabriele Cesario and Guido Salvaneschi. 2024b. Dis\/Equality Graphs. https:\/\/doi.org\/10.5281\/zenodo.13938878 10.5281\/zenodo.13938878","DOI":"10.5281\/zenodo.13938878"},{"key":"e_1_3_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591276"},{"key":"e_1_3_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3656408"},{"key":"e_1_3_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591239"},{"key":"e_1_3_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498696"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704913","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3704913","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T10:18:55Z","timestamp":1770200335000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704913"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,7]]},"references-count":41,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2025,1,7]]}},"alternative-id":["10.1145\/3704913"],"URL":"https:\/\/doi.org\/10.1145\/3704913","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,1,7]]},"assertion":[{"value":"2024-07-11","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-11-07","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-01-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}