Crate egg

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§

tutorials: A Guide-level Explanation of egg

Macros§

define_language: A macro to easily create a Language.
multi_rewrite: A macro to easily make Rewrites using MultiPatterns.
rewrite: A macro to easily make Rewrites.
test_fn: Utility to make a test proving expressions equivalent

Structs§

AstDepth: A simple CostFunction that counts maximum AST depth.
AstSize: A simple CostFunction that counts total AST size.
BackoffScheduler: A RewriteScheduler that implements exponentional rule backoff.
ConditionEqual: A Condition that checks if two terms are equivalent.
ConditionalApplier: An Applier that checks a Condition before applying.
DidMerge: Result of Analysis::merge indicating which of the inputs are different from the merged result.
Dot: A wrapper for an EGraph that can output GraphViz for visualization.
EClass: An equivalence class of enodes.
EGraph: A data structure to keep track of equalities between expressions.
Explanation: A data structure representing an explanation that two terms are equivalent.
Extractor: Extracting a single RecExpr from an EGraph.
FlatTerm: 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.
FromOpError: 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.
Id: A key to identify EClasses within an EGraph.
Iteration: Data generated by running a Runner one iteration.
LpExtractorlp: 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:
MultiPattern: A set of open expressions bound to variables.
Pattern: A pattern that can function as either a Searcher or Applier.
RecExpr: A recursive expression from a user-defined Language.
Report: A report containing data about an entire Runner run.
Rewrite: A rewrite that searches for the lefthand side and applies the righthand side.
Runner: Faciliates running rewrites over an EGraph.
RunnerLimits: Describes the limits that would stop a Runner.
SearchMatches: The result of searching a Searcher over one eclass.
SimpleLanguageMapper: An implementation of LanguageMapper that can convert an EGraph over one language into an EGraph over a different language in common cases.
SimpleScheduler: A very simple RewriteScheduler that runs every rewrite every time.
Subst: A substitution mapping Vars to eclass Ids.
Symbol: An interned string.
SymbolLang: A simple language used for testing.
TreeTerm: 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.
Var: A variable for use in Patterns or Substs.

Enums§

ENodeOrVar: The language of Patterns.
Justification: A justification for a union, either via a rule or congruence. A direct union with a justification is also stored as a rule.
MultiPatternParseError: An error raised when parsing a MultiPattern
RecExprParseError: An error type for failures when attempting to parse an s-expression as a RecExpr<L>.
StopReason: Error returned by Runner when it stops.

Traits§

Analysis: Arbitrary data associated with an EClass.
Applier: The righthand side of a Rewrite.
Condition: A condition to check in a ConditionalApplier.
CostFunction: A cost function that can be used by an Extractor.
FromOp: A trait for parsing e-nodes. This is implemented automatically by define_language!.
IterationData: Custom data to inject into the Iterations recorded by a Runner
Language: Trait that defines a Language whose terms will be in the EGraph.
LanguageChildren: A marker that defines acceptable children types for define_language!.
LanguageMapper: Translates EGraph<L, A> into EGraph<L2, A2>. For common cases, you don’t need to implement this manually. See the provided SimpleLanguageMapper.
LpCostFunctionlp: A cost function to be used by an LpExtractor.
RewriteScheduler: A way to customize how a Runner runs Rewrites.
Searcher: The lefthand side of a Rewrite.

Functions§

merge_max: A utility for implementing Analysis::merge when the Data type has a total ordering. This will take the maximum of the two values.
merge_min: A utility for implementing Analysis::merge when the Data type has a total ordering. This will take the minimum of the two values.
merge_option: A utility for implementing Analysis::merge when the Data type is an Option.

Type Aliases§

FlatExplanation: 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.
PatternAst: A RecExpr that represents a Pattern.
RunnerResult: Type alias for the result of a Runner.
TreeExplanation: Explanation trees are the compact representation showing how one term can be rewritten to another.
UnionEqualities: A vector of equalities based on enode ids. Each entry represents two enode ids that are equal and why.

Crate eggCopy item path