egg: egraphs good
egg is a library for e-graphs and equality saturation. It can be used to build program optimizers, synthesizers, verifiers, and more. For more information, see these resources:
Also check out the egglog system that provides an alternative approach to equality saturation based on Datalog. It features a language-based design, incremental execution, and composable analyses. See also the paper and the egglog web demo.
Are you using egg? Please cite using the BibTeX below and add your project to the "Awesome E-graphs" page!
Using egg
Add egg to your Cargo.toml like this:
[]
= "0.11.0"
Make sure to compile with --release if you are measuring performance!
Developing
It's written in Rust.
Typically, you install Rust using rustup.
Run cargo doc --open to build and open the documentation in a browser.
Before committing/pushing, make sure to run make,
which runs all the tests and lints that CI will (including those under feature flags).
This requires the cbc solver
due to the lp feature.
Tests
Running cargo test will run the tests.
Some tests may time out; try cargo test --release if that happens.
There are a couple interesting tests in the tests directory:
prop.rsimplements propositional logic and proves some simple theorems.math.rsimplements real arithmetic, with a little bit of symbolic differentiation.lambda.rsimplements a small lambda calculus, usingeggas a partial evaluator.
Benchmarking
To get a simple csv of the runtime of each test, you set the environment variable
EGG_BENCH_CSV to something to append a row per test to a csv.
Example:
EGG_BENCH_CSV=math.csv