[−][src]Struct egg::EGraph
A data structure to keep track of equalities between expressions.
What's an egraph?
An egraph (/'igraf/) is a data structure to maintain equivalence
classes of expressions. An egraph conceptually is a set of eclasses, each of which contains equivalent enodes. An enode is conceptually and operator with children, but instead of children being other operators or values, the children are eclasses.
In egg
, these are respresented by the EGraph
, EClass
, and
Language
(enodes) types.
Here's an egraph created and rendered by this example. As described in the documentation for egraph visualization and in the academic literature, we picture eclasses as dotted boxes surrounding the equivalent enodes:
We say a term t is represented in an eclass e if you can pick a
single enode from each eclass such that t is in e.
A term is represented in the egraph if it's represented in any eclass.
In the image above, the terms 2 * a
, a * 2
, and a << 1
are all
represented in the same eclass and thus are equivalent.
The terms 1
, (a * 2) / 2
, and (a << 1) / 2
are represented in
the egraph, but not in the same eclass as the prior three terms, so
these three are not equivalent to those three.
Egraphs are useful when you have a bunch of very similar expressions,
some of which are equivalent, and you'd like a compactly store them.
This compactness allows rewrite systems based on egraphs to
efficiently "remember" the expression before and after rewriting, so
you can essentially apply all rewrites at once.
See Rewrite
and Runner
for more details about rewrites and
running rewrite systems, respectively.
Invariants and Rebuilding
An egraph has two core operations that modify the egraph:
add
which adds enodes to the egraph, and
union
which merges two eclasses.
These operations maintains two key (related) invariants:
-
Uniqueness of enodes
There do not exist two distinct enodes with equal operators and equal children in the eclass, either in the same eclass or different eclasses. This is maintained in part by the hashconsing performed by
add
, and by deduplication performed byunion
andrebuild
. -
Congruence closure
An egraph maintains not just an equivalence relation over expressions, but a congruence relation. So as the user calls
union
, many eclasses other than the given two may need to merge to maintain congruence.For example, suppose terms
a + x
anda + y
are represented in eclasses 1 and 2, respectively. At some later point,x
andy
become equivalent (perhaps the user calledunion
on their containing eclasses). Eclasses 1 and 2 must merge, because now the two+
operators have equivalent arguments, making them equivalent.
egg
takes a delayed approach to maintaining these invariants.
Specifically, the effects of calling union
(or applying a rewrite,
which calls union
) may not be reflected immediately.
To restore the egraph invariants and make these effects visible, the
user must call the rebuild
method.
egg
s choice here allows for a higher performance implementation.
Maintaining the congruence relation complicates the core egraph data
structure and requires an expensive traversal through the egraph on
every union
.
egg
chooses to relax these invariants for better performance, only
restoring the invariants on a call to rebuild
.
See the rebuild
documentation for more information.
Note also that Runner
s take care of this for you, calling
rebuild
between rewrite iterations.
egraphs in egg
In egg
, the main types associated with egraphs 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 enodes are elements of your Language
.
EGraph
s and EClass
es are additionally parameterized by some
Analysis
, abritrary data associated with each eclass.
Many methods of EGraph
deal with Id
s, which represent eclasses.
Because eclasses are frequently merged, many Id
s will refer to the
same eclass.
Fields
analysis: N
The Analysis
given when creating this EGraph
.
Implementations
impl<L: Language, N: Analysis<L>> EGraph<L, N>
[src]
pub fn new(analysis: N) -> Self
[src]
Creates a new, empty EGraph
with the given Analysis
pub fn classes(&self) -> impl Iterator<Item = &EClass<L, N::Data>>
[src]
Returns an iterator over the eclasses in the egraph.
pub fn classes_mut(&mut self) -> impl Iterator<Item = &mut EClass<L, N::Data>>
[src]
Returns an mutating iterator over the eclasses in the egraph.
pub fn is_empty(&self) -> bool
[src]
Returns true
if the egraph is empty
Example
use egg::{*, StringLang as S}; let mut egraph = EGraph::<S, ()>::default(); assert!(egraph.is_empty()); egraph.add(S::leaf("foo")); assert!(!egraph.is_empty());
pub fn total_size(&self) -> usize
[src]
Returns the number of enodes in the EGraph
.
Actually returns the size of the hashcons index.
Example
use egg::{*, StringLang 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);
pub fn total_number_of_nodes(&self) -> usize
[src]
Iterates over the classes, returning the total number of nodes.
pub fn number_of_classes(&self) -> usize
[src]
Returns the number of eclasses in the egraph.
pub fn find(&self, id: Id) -> Id
[src]
Canonicalizes an eclass id.
This corresponds to the find
operation on the egraph's
underlying unionfind data structure.
Example
use egg::{*, StringLang 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); assert_eq!(egraph.find(x), egraph.find(y));
pub fn dot(&self) -> Dot<L, N>
[src]
impl<L: Language, N: Analysis<L>> EGraph<L, N>
[src]
pub fn add_expr(&mut self, expr: &RecExpr<L>) -> Id
[src]
Example
use egg::{*, StringLang 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));
pub fn add(&mut self, enode: L) -> Id
[src]
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.
Otherwise
pub fn equivs(&self, expr1: &RecExpr<L>, expr2: &RecExpr<L>) -> Vec<Id>
[src]
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(&mut self, id1: Id, id2: Id) -> (Id, bool)
[src]
Unions two eclasses given their ids.
The given ids need not be canonical.
The returned bool
indicates whether a union was done,
so it's false
if they were already equivalent.
Both results are canonical.
pub fn dump<'a>(&'a self) -> impl Debug + 'a
[src]
impl<L: Language, N: Analysis<L>> EGraph<L, N>
[src]
pub fn rebuild(&mut self) -> usize
[src]
Restores the egraph invariants of congruence and enode uniqueness.
As mentioned above,
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.
Example
use egg::{*, StringLang 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; ax and ay // should be equivalent by congruence since x = y. egraph.union(x, y); // Classes: [x y] [ax] [ay] [a] assert_eq!(egraph.number_of_classes(), 4); assert_ne!(egraph.find(ax), egraph.find(ay)); // Rebuilding restores the invariants, finding the "missing" equivalence 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
impl<L: Clone + Language, N: Clone + Analysis<L>> Clone for EGraph<L, N> where
N::Data: Clone,
[src]
N::Data: Clone,
impl<L: Language, N: Analysis<L>> Debug for EGraph<L, N>
[src]
impl<L: Language, N: Analysis<L> + Default> Default for EGraph<L, N>
[src]
impl<L: Language, N: Analysis<L>> Index<u32> for EGraph<L, N>
[src]
type Output = EClass<L, N::Data>
The returned type after indexing.
fn index(&self, id: Id) -> &Self::Output
[src]
impl<L: Language, N: Analysis<L>> IndexMut<u32> for EGraph<L, N>
[src]
Auto Trait Implementations
impl<L, N> !RefUnwindSafe for EGraph<L, N>
impl<L, N> Send for EGraph<L, N> where
L: Send,
N: Send,
<N as Analysis<L>>::Data: Send,
L: Send,
N: Send,
<N as Analysis<L>>::Data: Send,
impl<L, N> !Sync for EGraph<L, N>
impl<L, N> Unpin for EGraph<L, N> where
L: Unpin,
N: Unpin,
L: Unpin,
N: Unpin,
impl<L, N> UnwindSafe for EGraph<L, N> where
L: UnwindSafe,
N: UnwindSafe,
<N as Analysis<L>>::Data: UnwindSafe,
L: UnwindSafe,
N: UnwindSafe,
<N as Analysis<L>>::Data: UnwindSafe,
Blanket Implementations
impl<T> Any for T where
T: 'static + ?Sized,
[src]
T: 'static + ?Sized,
impl<T> Borrow<T> for T where
T: ?Sized,
[src]
T: ?Sized,
impl<T> BorrowMut<T> for T where
T: ?Sized,
[src]
T: ?Sized,
fn borrow_mut(&mut self) -> &mut T
[src]
impl<T> From<T> for T
[src]
impl<T, U> Into<U> for T where
U: From<T>,
[src]
U: From<T>,
impl<T> ToOwned for T where
T: Clone,
[src]
T: Clone,
type Owned = T
The resulting type after obtaining ownership.
fn to_owned(&self) -> T
[src]
fn clone_into(&self, target: &mut T)
[src]
impl<T, U> TryFrom<U> for T where
U: Into<T>,
[src]
U: Into<T>,
type Error = Infallible
The type returned in the event of a conversion error.
fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>
[src]
impl<T, U> TryInto<U> for T where
U: TryFrom<T>,
[src]
U: TryFrom<T>,