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§
source§impl<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 without_explanation_length_optimization(self) -> Self
pub fn without_explanation_length_optimization(self) -> Self
By default, egg runs a greedy algorithm to reduce the size of resulting explanations (without complexity overhead). Use this function to turn this algorithm off.
sourcepub fn with_explanation_length_optimization(self) -> Self
pub fn with_explanation_length_optimization(self) -> Self
By default, egg runs a greedy algorithm to reduce the size of resulting explanations (without complexity overhead). Use this function to turn this algorithm on again if you have turned it off.
sourcepub fn copy_without_unions(&self, analysis: N) -> Self
pub fn copy_without_unions(&self, analysis: N) -> Self
Make a copy of the egraph with the same nodes, but no unions between them.
sourcepub fn egraph_union(&mut self, other: &EGraph<L, N>)
pub fn egraph_union(&mut self, other: &EGraph<L, N>)
Performs the union between two egraphs.
sourcepub fn egraph_intersect_incomplete(
&mut self,
other: &mut EGraph<L, N>,
resulting: &mut EGraph<L, N>
)
pub fn egraph_intersect_incomplete(
&mut self,
other: &mut EGraph<L, N>,
resulting: &mut EGraph<L, N>
)
A best-effort intersection algorithm between two egraphs. The intersection is guaranteed to be correct for all direct equalities found in the original two egraphs. Implied equalities due to congruence, however, may not be preserved. The two input egraphs are mutable because some terms may be added for equality checks (but no new unions will be added).
sourcepub fn id_to_expr(&self, id: Id) -> RecExpr<L>
pub fn id_to_expr(&self, id: Id) -> RecExpr<L>
Pick a representative term for a given Id.
sourcepub fn id_to_pattern(
&self,
id: Id,
substitutions: &HashMap<Id, Id, FxBuildHasher>
) -> (Pattern<L>, Subst)
pub fn id_to_pattern(
&self,
id: Id,
substitutions: &HashMap<Id, Id, FxBuildHasher>
) -> (Pattern<L>, Subst)
Like id_to_expr
, but creates a pattern instead of a term.
When an eclass listed in the given substitutions is found, it creates a variable.
It also adds this variable and the corresponding Id value to the resulting Subst
Otherwise it behaves like id_to_expr
.
sourcepub fn get_union_equalities(&self) -> UnionEqualities
pub fn get_union_equalities(&self) -> UnionEqualities
Get all the unions ever found in the egraph in terms of enode ids.
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 get_num_congr(&mut self) -> usize
pub fn get_num_congr(&mut self) -> usize
Get the number of congruences between nodes in the egraph. Only available when explanations are enabled.
sourcepub fn get_explanation_num_nodes(&mut self) -> usize
pub fn get_explanation_num_nodes(&mut self) -> usize
Get the number of nodes in the egraph used for explanations.
sourcepub fn explain_equivalence(
&mut self,
left_expr: &RecExpr<L>,
right_expr: &RecExpr<L>
) -> Explanation<L>
pub fn explain_equivalence(
&mut self,
left_expr: &RecExpr<L>,
right_expr: &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_expr: &RecExpr<L>,
right_pattern: &PatternAst<L>,
subst: &Subst
) -> Explanation<L>
pub fn explain_matches(
&mut self,
left_expr: &RecExpr<L>,
right_pattern: &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));
source§impl<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_trusted(
&mut self,
from: Id,
to: Id,
reason: impl Into<Symbol>
) -> bool
pub fn union_trusted(
&mut self,
from: Id,
to: Id,
reason: impl Into<Symbol>
) -> bool
Unions two e-classes, using a given reason to justify it.
Unlike union_instantiations
, this function picks arbitrary representatives
from either e-class.
When possible, use union_instantiations
,
since that ensures that the proof rewrites between the terms you are
actually proving equivalent.
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 behaves like EGraph::union_trusted
,
and it lists the call site as the proof reason.
You should prefer union_instantiations
when
you want the proofs to always be meaningful.
See explain_equivalence
for a more detailed
explanation of the feature.
sourcepub fn set_analysis_data(&mut self, id: Id, new_data: N::Data)
pub fn set_analysis_data(&mut self, id: Id, new_data: N::Data)
Update the analysis data of an e-class.
This also propagates the changes through the e-graph,
so Analysis::make
and Analysis::merge
will get
called for other parts of the e-graph on rebuild.
source§impl<L: Language + Display, N: Analysis<L>> EGraph<L, N>
impl<L: Language + Display, N: Analysis<L>> EGraph<L, N>
sourcepub fn check_goals(&self, id: Id, goals: &[Pattern<L>])
pub fn check_goals(&self, id: Id, goals: &[Pattern<L>])
Panic if the given eclass doesn’t contain the given patterns
Useful for testing.
source§impl<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§
source§impl<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,
source§impl<'de, L, N> Deserialize<'de> for EGraph<L, N>where
N::Data: for<'a> Deserialize<'a>,
L: Deserialize<'de> + Language,
N: Deserialize<'de> + Analysis<L>,
impl<'de, L, N> Deserialize<'de> for EGraph<L, N>where
N::Data: for<'a> Deserialize<'a>,
L: Deserialize<'de> + Language,
N: Deserialize<'de> + Analysis<L>,
source§fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error>where
__D: Deserializer<'de>,
fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error>where
__D: Deserializer<'de>,
source§impl<L: Language, N: Analysis<L>> Index<Id> for EGraph<L, N>
impl<L: Language, N: Analysis<L>> Index<Id> for EGraph<L, N>
Given an Id
using the egraph[id]
syntax, retrieve the e-class.