pub struct EGraph<L: Language, N: Analysis<L>> {
pub analysis: N,
pub clean: bool,
/* private fields */
}
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
sourceimpl<L: Language, N: Analysis<L>> EGraph<L, N>
impl<L: Language, N: Analysis<L>> EGraph<L, N>
sourcepub fn classes(&self) -> impl ExactSizeIterator<Item = &EClass<L, N::Data>>
pub fn classes(&self) -> impl ExactSizeIterator<Item = &EClass<L, N::Data>>
Returns an iterator over the eclasses in the egraph.
sourcepub fn classes_mut(
&mut self
) -> impl ExactSizeIterator<Item = &mut EClass<L, N::Data>>
pub fn classes_mut(
&mut self
) -> impl ExactSizeIterator<Item = &mut EClass<L, N::Data>>
Returns an mutating iterator over the eclasses in the egraph.
sourcepub fn is_empty(&self) -> bool
pub fn is_empty(&self) -> bool
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());
sourcepub fn total_size(&self) -> usize
pub fn total_size(&self) -> usize
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);
sourcepub fn total_number_of_nodes(&self) -> usize
pub fn total_number_of_nodes(&self) -> usize
Iterates over the classes, returning the total number of nodes.
sourcepub fn number_of_classes(&self) -> usize
pub fn number_of_classes(&self) -> usize
Returns the number of eclasses in the egraph.
sourcepub fn with_explanations_enabled(self) -> Self
pub fn with_explanations_enabled(self) -> Self
Enable explanations for this EGraph
.
This allows the egraph to explain why two expressions are
equivalent with the explain_equivalence
function.
sourcepub fn with_explanations_disabled(self) -> Self
pub fn with_explanations_disabled(self) -> Self
Disable explanations for this EGraph
.
sourcepub fn are_explanations_enabled(&self) -> bool
pub fn are_explanations_enabled(&self) -> bool
Check if explanations are enabled.
sourcepub 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
.
sourcepub fn explain_existance(&mut self, expr: &RecExpr<L>) -> Explanation<L>
pub fn explain_existance(&mut self, expr: &RecExpr<L>) -> Explanation<L>
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
.
sourcepub 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.
sourcepub 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.
sourcepub fn find(&self, id: Id) -> Id
pub fn find(&self, id: Id) -> Id
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));
sourceimpl<L: Language, N: Analysis<L>> EGraph<L, N>
impl<L: Language, N: Analysis<L>> EGraph<L, N>
sourcepub fn add_expr(&mut self, expr: &RecExpr<L>) -> Id
pub fn add_expr(&mut self, expr: &RecExpr<L>) -> Id
Adds a RecExpr
to the EGraph
, returning the id of the RecExpr’s eclass.
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));
sourcepub fn add_instantiation(&mut self, pat: &PatternAst<L>, subst: &Subst) -> Id
pub fn add_instantiation(&mut self, pat: &PatternAst<L>, subst: &Subst) -> Id
sourcepub fn lookup<B>(&self, enode: B) -> Option<Id> where
B: BorrowMut<L>,
pub fn lookup<B>(&self, enode: B) -> Option<Id> where
B: BorrowMut<L>,
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]));
sourcepub fn lookup_expr(&self, expr: &RecExpr<L>) -> Option<Id>
pub fn lookup_expr(&self, expr: &RecExpr<L>) -> Option<Id>
Lookup the eclass of the given RecExpr
.
Equivalent to the last value in EGraph::lookup_expr_ids
.
sourcepub fn lookup_expr_ids(&self, expr: &RecExpr<L>) -> Option<Vec<Id>>
pub fn lookup_expr_ids(&self, expr: &RecExpr<L>) -> Option<Vec<Id>>
Lookup the eclasses of all the nodes in the given RecExpr
.
sourcepub fn add(&mut self, enode: L) -> Id
pub fn add(&mut self, enode: L) -> Id
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.
sourcepub fn equivs(&self, expr1: &RecExpr<L>, expr2: &RecExpr<L>) -> Vec<Id>
pub fn equivs(&self, expr1: &RecExpr<L>, expr2: &RecExpr<L>) -> Vec<Id>
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.
sourcepub 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 union them.
When explanations are enabled with_explanations_enabled
, use
this function instead of union
.
Returns the id of the new eclass, along with
a bool
indicating whether a union occured.
sourcepub fn union(&mut self, id1: Id, id2: Id) -> bool
pub fn union(&mut self, id1: Id, id2: Id) -> bool
Unions two eclasses given their ids.
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.
When explanations are enabled, this function is not available.
Instead, use union_instantiations
.
See explain_equivalence
for a more detailed
explanation of the feature.
sourceimpl<L: Language, N: Analysis<L>> EGraph<L, N>
impl<L: Language, N: Analysis<L>> EGraph<L, N>
sourcepub fn rebuild(&mut self) -> usize
pub fn rebuild(&mut self) -> usize
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());
// Union x and y
egraph.union(x, y);
// Classes: [x y] [ax] [ay] [a]
assert_eq!(egraph.find(x), egraph.find(y));
// Rebuilding restores the congruence invariant, 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
sourceimpl<L: Clone + Language, N: Clone + Analysis<L>> Clone for EGraph<L, N> where
N::Data: Clone,
impl<L: Clone + Language, N: Clone + Analysis<L>> Clone for EGraph<L, N> where
N::Data: Clone,
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> Send for EGraph<L, N> where
L: Send,
N: Send,
<N as Analysis<L>>::Data: Send,
impl<L, N> Sync for EGraph<L, N> where
L: Sync,
N: Sync,
<N as Analysis<L>>::Data: Sync,
impl<L, N> Unpin for EGraph<L, N> where
L: Unpin,
N: Unpin,
<N as Analysis<L>>::Data: Unpin,
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
sourceimpl<T> BorrowMut<T> for T where
T: ?Sized,
impl<T> BorrowMut<T> for T where
T: ?Sized,
const: unstable · sourcefn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more
sourceimpl<T> ToOwned for T where
T: Clone,
impl<T> ToOwned for T where
T: Clone,
type Owned = T
type Owned = T
The resulting type after obtaining ownership.
sourcefn clone_into(&self, target: &mut T)
fn clone_into(&self, target: &mut T)
toowned_clone_into
)Uses borrowed data to replace owned data, usually by cloning. Read more