Crate egg[−][src]
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.
!
Modules
A Guide-level Explanation of egg
Macros
A macro to easily create a Language.
Make a test function
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 rewrite that searches for the lefthand side and applies the righthand side.
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 recursivly.
The final term is given by all of the final terms in each child_proofs.
Enums
The language of Patterns.
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!.
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.