Egraphs Modulo Theories
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/