Struct egg::EGraph

pub struct EGraph<L: Language, N: Analysis<L>> {
    pub analysis: N,
    pub clean: bool,
    /* private fields */
}

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. EGraphs and EClasses are additionally parameterized by some Analysis, abritrary data associated with each e-class.

Many methods of EGraph deal with Ids, which represent e-classes. Because eclasses are frequently merged, many Ids 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 EGraphs 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

impl<L: Language, N: Analysis<L>> EGraph<L, N>

pub fn new(analysis: N) -> Self

Creates a new, empty EGraph with the given Analysis

pub fn classes(&self) -> impl ExactSizeIterator<Item = &EClass<L, N::Data>>

Returns an iterator over the eclasses in the egraph.

pub fn classes_mut( &mut self ) -> impl ExactSizeIterator<Item = &mut EClass<L, N::Data>>

Returns an mutating iterator over the eclasses in the egraph.

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());

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);

pub fn total_number_of_nodes(&self) -> usize

Iterates over the classes, returning the total number of nodes.

pub fn number_of_classes(&self) -> usize

Returns the number of eclasses in the egraph.

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.

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.

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.

pub fn copy_without_unions(&self, analysis: N) -> Self

Make a copy of the egraph with the same nodes, but no unions between them.

pub fn egraph_union(&mut self, other: &EGraph<L, N>)

Performs the union between two egraphs.

pub fn egraph_intersect( &self, other: &EGraph<L, N>, analysis: N ) -> EGraph<L, N>

A intersection algorithm between two egraphs. The intersection is correct for all terms that are equal in both egraphs. Be wary, though, because terms which are not represented in both egraphs are not captured in the intersection. The runtime of this algorithm is O(|E1| * |E2|), where |E1| and |E2| are the number of enodes in each egraph.

pub fn id_to_expr(&self, id: Id) -> RecExpr<L>

Pick a representative term for a given Id.

pub fn id_to_pattern( &self, id: Id, substitutions: &IndexMap<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.

pub fn get_union_equalities(&self) -> UnionEqualities

Get all the unions ever found in the egraph in terms of enode ids.

pub fn with_explanations_disabled(self) -> Self

Disable explanations for this EGraph.

pub fn are_explanations_enabled(&self) -> bool

Check if explanations are enabled.

pub fn get_num_congr(&mut self) -> usize

Get the number of congruences between nodes in the egraph. Only available when explanations are enabled.

pub fn get_explanation_num_nodes(&mut self) -> usize

Get the number of nodes in the egraph used for explanations.

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.

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.

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_expr: &RecExpr<L>, right_pattern: &PatternAst<L>, subst: &Subst ) -> Explanation<L>

Get an explanation for why an expression matches a pattern.

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));

pub fn dot(&self) -> Dot<'_, L, N>

Creates a Dot to visualize this egraph. See Dot.

impl<L: Language, N: Analysis<L>> EGraph<L, N>

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));

pub fn add_instantiation(&mut self, pat: &PatternAst<L>, subst: &Subst) -> Id

Adds a Pattern and a substitution to the EGraph, returning the eclass of the instantiated pattern.

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]));

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.

pub fn lookup_expr_ids(&self, expr: &RecExpr<L>) -> Option<Vec<Id>>

Lookup the eclasses of all the nodes in the given RecExpr.

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.

pub fn equivs(&self, expr1: &RecExpr<L>, expr2: &RecExpr<L>) -> Vec<Id>

Checks whether two RecExprs 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)

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.

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.

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.

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.

pub fn dump(&self) -> impl Debug + '_

Returns a more debug-able representation of the egraph.

EGraphs implement Debug, but it ain’t pretty. It prints a lot of stuff you probably don’t care about. This method returns a wrapper that implements Debug in a slightly nicer way, just dumping enodes in each eclass.

impl<L: Language + Display, N: Analysis<L>> EGraph<L, N>

pub fn check_goals(&self, id: Id, goals: &[Pattern<L>])

Panic if the given eclass doesn’t contain the given patterns

Useful for testing.

impl<L: Language, N: Analysis<L>> EGraph<L, N>

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

impl<L: Clone + Language, N: Clone + Analysis<L>> Clone for EGraph<L, N>where N::Data: Clone,

fn clone(&self) -> EGraph<L, N>

Returns a copy of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl<L: Language, N: Analysis<L>> Debug for EGraph<L, N>

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl<L: Language, N: Analysis<L> + Default> Default for EGraph<L, N>

fn default() -> Self

Returns the “default value” for a type.

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>,

fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error>where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl<L: Language, N: Analysis<L>> Index<Id> for EGraph<L, N>

Given an Id using the egraph[id] syntax, retrieve the e-class.

type Output = EClass<L, <N as Analysis<L>>::Data>

The returned type after indexing.

fn index(&self, id: Id) -> &Self::Output

Performs the indexing (container[index]) operation.

impl<L: Language, N: Analysis<L>> IndexMut<Id> for EGraph<L, N>

Given an Id using the &mut egraph[id] syntax, retrieve a mutable reference to the e-class.

fn index_mut(&mut self, id: Id) -> &mut Self::Output

Performs the mutable indexing (container[index]) operation.

impl<L, N> Serialize for EGraph<L, N>where N::Data: Serialize, L: Serialize + Language, N: Serialize + Analysis<L>,

fn serialize<__S>(&self, __serializer: __S) -> Result<__S::Ok, __S::Error>where __S: Serializer,

Serialize this value into the given Serde serializer.