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.
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 Rewrites using MultiPatterns.
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 FlatTerms,
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.
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 rewrite that searches for the lefthand side and applies the righthand side.
The result of searching a Searcher over one eclass.
An implementation of LanguageMapper that can convert an EGraph over one
language into an EGraph over a different language in common cases.
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 Patterns.
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
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!.
A marker that defines acceptable children types for define_language!.
Translates EGraph<L, A> into EGraph<L2, A2>. For common cases, you don’t
need to implement this manually. See the provided SimpleLanguageMapper.
A cost function to be used by an LpExtractor.
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.
A utility for implementing Analysis::merge
when the Data type is an Option.
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.