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 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.
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 Pattern
s.
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.