Crate egg

source ·
Expand description

egg (e-graphs good) is a e-graph library optimized for equality saturation.

This is the API documentation.

The tutorial is a good starting point if you’re new to e-graphs, equality saturation, or Rust.

The tests on Github provide some more elaborate examples.

There is also a paper describing egg and some of its technical novelties.


Many parts of egg dump useful logging info using the log crate. The easiest way to see this info is to use the env_logger crate in your binary or test. The simplest way to enable env_logger is to put the following line near the top of your main: env_logger::init();. Then, set the environment variable RUST_LOG=egg=info, or use warn or debug instead of info for less or more logging.

Simple Example

use egg::*;

define_language! {
    enum SimpleLanguage {
        "+" = Add([Id; 2]),
        "*" = Mul([Id; 2]),

fn make_rules() -> Vec<Rewrite<SimpleLanguage, ()>> {
        rewrite!("commute-add"; "(+ ?a ?b)" => "(+ ?b ?a)"),
        rewrite!("commute-mul"; "(* ?a ?b)" => "(* ?b ?a)"),
        rewrite!("add-0"; "(+ ?a 0)" => "?a"),
        rewrite!("mul-0"; "(* ?a 0)" => "0"),
        rewrite!("mul-1"; "(* ?a 1)" => "?a"),

/// parse an expression, simplify it using egg, and pretty print it back out
fn simplify(s: &str) -> String {
    // parse the expression, the type annotation tells it which Language to use
    let expr: RecExpr<SimpleLanguage> = s.parse().unwrap();

    // simplify the expression using a Runner, which creates an e-graph with
    // the given expression and runs the given rules over it
    let runner = Runner::default().with_expr(&expr).run(&make_rules());

    // the Runner knows which e-class the expression given with `with_expr` is in
    let root = runner.roots[0];

    // use an Extractor to pick the best element of the root eclass
    let extractor = Extractor::new(&runner.egraph, AstSize);
    let (best_cost, best) = extractor.find_best(root);
    println!("Simplified {} to {} with cost {}", expr, best, best_cost);

fn simple_tests() {
    assert_eq!(simplify("(* 0 42)"), "0");
    assert_eq!(simplify("(+ 0 (* 1 foo))"), "foo");







Type Definitions

  • FlatExplanation are the simpler, expanded representation showing one term being rewritten to another. Each step contains a full FlatTerm. Each flat term is connected to the previous by exactly one rewrite.
  • A RecExpr that represents a Pattern.
  • Explanation trees are the compact representation showing how one term can be rewritten to another.
  • A vector of equalities based on enode ids. Each entry represents two enode ids that are equal and why.