Struct egg::EGraph [−][src]
pub struct EGraph<L: Language, N: Analysis<L>> {
pub analysis: N,
pub clean: bool,
// some fields omitted
}
Expand description
A data structure to keep track of equalities between expressions.
Check out the background tutorial for more information on e-graphs in general.
E-graphs in egg
In egg
, the main types associated with e-graphs are
EGraph
, EClass
, Language
, and Id
.
EGraph
and EClass
are all generic over a
Language
, meaning that types actually floating around in the
egraph are all user-defined.
In particular, the e-nodes are elements of your Language
.
EGraph
s and EClass
es are additionally parameterized by some
Analysis
, abritrary data associated with each e-class.
Many methods of EGraph
deal with Id
s, which represent e-classes.
Because eclasses are frequently merged, many Id
s will refer to the
same e-class.
You can use the egraph[id]
syntax to get an EClass
from an Id
, because
EGraph
implements
Index
and
IndexMut
.
Enabling the serde-1
feature on this crate will allow you to
de/serialize EGraph
s using serde
.
You must call EGraph::rebuild
after deserializing an e-graph!
Fields
analysis: N
The Analysis
given when creating this EGraph
.
clean: bool
Whether or not reading operation are allowed on this e-graph.
Mutating operations will set this to false
, and
EGraph::rebuild
will set it to true.
Reading operations require this to be true
.
Only manually set it if you know what you’re doing.
Implementations
Returns an iterator over the eclasses in the egraph.
Returns an mutating iterator over the eclasses in the egraph.
Returns true
if the egraph is empty
Example
use egg::{*, SymbolLang as S};
let mut egraph = EGraph::<S, ()>::default();
assert!(egraph.is_empty());
egraph.add(S::leaf("foo"));
assert!(!egraph.is_empty());
Returns the number of enodes in the EGraph
.
Actually returns the size of the hashcons index.
Example
use egg::{*, SymbolLang as S};
let mut egraph = EGraph::<S, ()>::default();
let x = egraph.add(S::leaf("x"));
let y = egraph.add(S::leaf("y"));
// only one eclass
egraph.union(x, y);
egraph.rebuild();
assert_eq!(egraph.total_size(), 2);
assert_eq!(egraph.number_of_classes(), 1);
Iterates over the classes, returning the total number of nodes.
Returns the number of eclasses in the egraph.
Enable explanations for this EGraph
.
This allows the egraph to explain why two expressions are
equivalent with the explain_equivalence
function.
Disable explanations for this EGraph
.
Check if explanations are enabled.
pub fn explain_equivalence(
&mut self,
left: &RecExpr<L>,
right: &RecExpr<L>
) -> Explanation<L>
pub fn explain_equivalence(
&mut self,
left: &RecExpr<L>,
right: &RecExpr<L>
) -> Explanation<L>
When explanations are enabled, this function
produces an Explanation
describing why two expressions are equivalent.
The Explanation
can be used in it’s default tree form or in a less compact
flattened form. Each of these also has a s-expression string representation,
given by get_flat_string
and get_string
.
When explanations are enabled, this function
produces an Explanation
describing how the given expression came
to be in the egraph.
The Explanation
begins with some expression that was added directly
into the egraph and ends with the given expr
.
Note that this function can be called again to explain any intermediate terms
used in the output Explanation
.
pub fn explain_existance_pattern(
&mut self,
pattern: &PatternAst<L>,
subst: &Subst
) -> Explanation<L>
pub fn explain_existance_pattern(
&mut self,
pattern: &PatternAst<L>,
subst: &Subst
) -> Explanation<L>
Return an Explanation
for why a pattern appears in the egraph.
pub fn explain_matches(
&mut self,
left: &RecExpr<L>,
right: &PatternAst<L>,
subst: &Subst
) -> Explanation<L>
pub fn explain_matches(
&mut self,
left: &RecExpr<L>,
right: &PatternAst<L>,
subst: &Subst
) -> Explanation<L>
Get an explanation for why an expression matches a pattern.
Canonicalizes an eclass id.
This corresponds to the find
operation on the egraph’s
underlying unionfind data structure.
Example
use egg::{*, SymbolLang as S};
let mut egraph = EGraph::<S, ()>::default();
let x = egraph.add(S::leaf("x"));
let y = egraph.add(S::leaf("y"));
assert_ne!(egraph.find(x), egraph.find(y));
egraph.union(x, y);
egraph.rebuild();
assert_eq!(egraph.find(x), egraph.find(y));
Example
use egg::{*, SymbolLang as S};
let mut egraph = EGraph::<S, ()>::default();
let x = egraph.add(S::leaf("x"));
let y = egraph.add(S::leaf("y"));
let plus = egraph.add(S::new("+", vec![x, y]));
let plus_recexpr = "(+ x y)".parse().unwrap();
assert_eq!(plus, egraph.add_expr(&plus_recexpr));
Lookup the eclass of the given enode.
You can pass in either an owned enode or a &mut
enode,
in which case the enode’s children will be canonicalized.
Example
let mut egraph: EGraph<SymbolLang, ()> = Default::default();
let a = egraph.add(SymbolLang::leaf("a"));
let b = egraph.add(SymbolLang::leaf("b"));
// lookup will find this node if its in the egraph
let mut node_f_ab = SymbolLang::new("f", vec![a, b]);
assert_eq!(egraph.lookup(node_f_ab.clone()), None);
let id = egraph.add(node_f_ab.clone());
assert_eq!(egraph.lookup(node_f_ab.clone()), Some(id));
// if the query node isn't canonical, and its passed in by &mut instead of owned,
// its children will be canonicalized
egraph.union(a, b);
egraph.rebuild();
assert_eq!(egraph.lookup(&mut node_f_ab), Some(id));
assert_eq!(node_f_ab, SymbolLang::new("f", vec![a, a]));
Lookup the eclass of the given RecExpr
.
Equivalent to the last value in EGraph::lookup_expr_ids
.
Lookup the eclasses of all the nodes in the given RecExpr
.
Adds an enode to the EGraph
.
When adding an enode, to the egraph, add
it performs
hashconsing (sometimes called interning in other contexts).
Hashconsing ensures that only one copy of that enode is in the egraph.
If a copy is in the egraph, then add
simply returns the id of the
eclass in which the enode was found.
Like union
, this modifies the e-graph,
so you must call rebuild
any query operations.
Checks whether two RecExpr
s are equivalent.
Returns a list of id where both expression are represented.
In most cases, there will none or exactly one id.
pub fn union_instantiations(
&mut self,
from_pat: &PatternAst<L>,
to_pat: &PatternAst<L>,
subst: &Subst,
rule_name: impl Into<Symbol>
) -> (Id, bool)
pub fn union_instantiations(
&mut self,
from_pat: &PatternAst<L>,
to_pat: &PatternAst<L>,
subst: &Subst,
rule_name: impl Into<Symbol>
) -> (Id, bool)
Given two patterns and a substitution, add the patterns
and mark them for unioning.
The unions are performed when rebuild
is called.
When explanations are enabled with_explanations_enabled
, use
this function instead of union
.
The returned bool
indicates whether a union is necessary,
and returned Id represents the eclass of the left pattern.
Marks two eclasses to be unioned given their ids.
At the end of each iteration, these classes are unioned during
rebuild
.
The given ids need not be canonical.
The returned bool
indicates whether a union is necessary,
so it’s false
if they were already equivalent.
Both results are canonical.
When explanations are enabled, this function is not available.
Instead, use union_instantiations
.
See explain_equivalence
for a more detailed
explanation of the feature.
You must call rebuild
to observe any effect.
Restores the egraph invariants of congruence and enode uniqueness.
As mentioned
in the tutorial,
egg
takes a lazy approach to maintaining the egraph invariants.
The rebuild
method allows the user to manually restore those
invariants at a time of their choosing. It’s a reasonably
fast, linear-ish traversal through the egraph.
After modifying an e-graph with add
or
union
, you must call rebuild
to restore
invariants before any query operations, otherwise the results
may be stale or incorrect.
This will set EGraph::clean
to true
.
Example
use egg::{*, SymbolLang as S};
let mut egraph = EGraph::<S, ()>::default();
let x = egraph.add(S::leaf("x"));
let y = egraph.add(S::leaf("y"));
let ax = egraph.add_expr(&"(+ a x)".parse().unwrap());
let ay = egraph.add_expr(&"(+ a y)".parse().unwrap());
// The effects of this union aren't yet visible;
// The union has not taken effect.
egraph.union(x, y);
// Classes: [x] [y] [ax] [ay] [a]
assert_eq!(egraph.number_of_classes(), 5);
assert_ne!(egraph.find(ax), egraph.find(ay));
// Rebuilding applies the union and restores the invariants, finding
// that ax and ay are equivalent.
egraph.rebuild();
// Classes: [x y] [ax ay] [a]
assert_eq!(egraph.number_of_classes(), 3);
assert_eq!(egraph.find(ax), egraph.find(ay));
Trait Implementations
Given an Id
using the egraph[id]
syntax, retrieve the e-class.
Auto Trait Implementations
impl<L, N> RefUnwindSafe for EGraph<L, N> where
L: RefUnwindSafe,
N: RefUnwindSafe,
<N as Analysis<L>>::Data: RefUnwindSafe,
<L as DiscriminantKind>::Discriminant: RefUnwindSafe,
impl<L, N> UnwindSafe for EGraph<L, N> where
L: UnwindSafe,
N: UnwindSafe,
<N as Analysis<L>>::Data: UnwindSafe,
<L as DiscriminantKind>::Discriminant: UnwindSafe,
Blanket Implementations
Mutably borrows from an owned value. Read more