EggMT
June 10, 2025 ยท View on GitHub
Egraphs Modulo Theories
Curently more activity is happening here https://github.com/philzook58/knuckledragger/blob/main/kdrag/solvers/egraph.py
Simple egraph and knuth bendix prototypes to add theory specific capabilities to equality saturation.
python3 -m pip install -e .
- Bottom Up Egraph Ematching Plays Nicer with Theories (AC, etc) https://www.philipzucker.com/bottom_up/
- An External Z3 Egraph for Egraphs Modulo Theories https://www.philipzucker.com/ext_z3_egraph/
- Gauss and Groebner Egraphs: Intrinsic Linear and Polynomial Equations https://www.philipzucker.com/linear_grobner_egraph/
- String Knuth Bendix https://www.philipzucker.com/string_knuth/
- Co-Egraphs: Streams, Unification, PEGs, Rational Lambdas https://www.philipzucker.com/coegraph/
- Acyclic Egraphs and Smart Constructors https://www.philipzucker.com/smart_constructor_aegraph/
- Towards an AC Egraph: Groebner, Graver and Ground Multiset Rewriting https://www.philipzucker.com/multiset_rw/
- Brute Force E-Graphs Modulo Theories via SMT https://www.philipzucker.com/brute_eggmt/
- Brute E-Graphs Modulo Theories 2: Extraction, Proofs, and Context https://www.philipzucker.com/egraph-mt2/