## Expand description

`egg`

(**e**-**g**raphs **g**ood) 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.

### Logging

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 {
Num(i32),
"+" = Add([Id; 2]),
"*" = Mul([Id; 2]),
Symbol(Symbol),
}
}
fn make_rules() -> Vec<Rewrite<SimpleLanguage, ()>> {
vec![
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);
best.to_string()
}
#[test]
fn simple_tests() {
assert_eq!(simplify("(* 0 42)"), "0");
assert_eq!(simplify("(+ 0 (* 1 foo))"), "foo");
}
```

## Modules

- A Guide-level Explanation of
`egg`

## Macros

- A macro to easily create a
`Language`

. - A macro to easily make
`Rewrite`

s using`MultiPattern`

s. - A macro to easily make
`Rewrite`

s. - Utility to make a test proving expressions equivalent

## Structs

- A simple
`CostFunction`

that counts maximum AST depth. - A simple
`CostFunction`

that counts total AST size. - A
`RewriteScheduler`

that implements exponentional rule backoff. - A
`Condition`

that checks if two terms are equivalent. - Result of
`Analysis::merge`

indicating which of the inputs are different from the merged result. - An equivalence class of enodes.
- A data structure to keep track of equalities between expressions.
- A data structure representing an explanation that two terms are equivalent.
- A single term in an flattened explanation. After the first term in a
`FlatExplanation`

, each term will be annotated with exactly one`backward_rule`

or one`forward_rule`

. This can appear in children`FlatTerm`

s, indicating that the child is being rewritten. - A generic error for failing to parse an operator. This is the error type used by
`define_language!`

for`FromOp::Error`

, and is a sensible choice when implementing`FromOp`

manually. - Data generated by running a
`Runner`

one iteration. - A structure to perform extraction using integer linear programming. This uses the
`cbc`

solver. You must have it installed on your machine to use this feature. You can install it using: - A set of open expressions bound to variables.
- A recursive expression from a user-defined
`Language`

. - A report containing data about an entire
`Runner`

run. - A rewrite that searches for the lefthand side and applies the righthand side.
- Faciliates running rewrites over an
`EGraph`

. - The result of searching a
`Searcher`

over one eclass. - A very simple
`RewriteScheduler`

that runs every rewrite every time. - An interned string.
- A simple language used for testing.
- An explanation for a term and its equivalent children. Each child is a proof transforming the initial child into the final child term. The initial term is given by taking each first sub-term in each
`child_proofs`

recursively. The final term is given by all of the final terms in each`child_proofs`

.

## Enums

- The language of
`Pattern`

s. - A justification for a union, either via a rule or congruence. A direct union with a justification is also stored as a rule.
- An error raised when parsing a
`MultiPattern`

- An error type for failures when attempting to parse an s-expression as a
`RecExpr<L>`

. - Error returned by
`Runner`

when it stops.

## Traits

- Arbitrary data associated with an
`EClass`

. - The righthand side of a
`Rewrite`

. - A condition to check in a
`ConditionalApplier`

. - A cost function that can be used by an
`Extractor`

. - A trait for parsing e-nodes. This is implemented automatically by
`define_language!`

. - Trait that defines a Language whose terms will be in the
`EGraph`

. - A marker that defines acceptable children types for
`define_language!`

. - A cost function to be used by an
`LpExtractor`

. - The lefthand side of a
`Rewrite`

.

## Functions

- A utility for implementing
`Analysis::merge`

when the`Data`

type has a total ordering. This will take the maximum of the two values. - A utility for implementing
`Analysis::merge`

when the`Data`

type has a total ordering. This will take the minimum of the two values.

## 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. - 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.