Struct egg::EGraph

pub struct EGraph<L: Language, N: Analysis<L>> {
    pub analysis: N,
    // some fields omitted
}

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:

1. 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 by union and rebuild.

2. 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 and a + y are represented in eclasses 1 and 2, respectively. At some later point, x and y become equivalent (perhaps the user called union 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.

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

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

pub fn new(analysis: N) -> Self

Creates a new, empty EGraph with the given Analysis

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

Returns an iterator over the eclasses in the egraph.

pub fn classes_mut(&mut self) -> impl Iterator<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 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);
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.

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 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"));
let c = egraph.add(SymbolLang::leaf("c"));

// lookup will find this node if its in the egraph
let mut node_f_ac = SymbolLang::new("f", vec![a, c]);
assert_eq!(egraph.lookup(node_f_ac.clone()), None);
let id = egraph.add(node_f_ac.clone());
assert_eq!(egraph.lookup(node_f_ac.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(b, c);
egraph.rebuild();
assert_eq!(egraph.lookup(&mut node_f_ac), Some(id));
assert_eq!(node_f_ac, SymbolLang::new("f", vec![a, b]));

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. Otherwise

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 check_goals(&self, id: Id, goals: &[Pattern<L>])

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

Useful for testing.

pub fn union(&mut self, id1: Id, id2: Id) -> (Id, bool)

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

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, N: Analysis<L>> EGraph<L, N>

pub fn rebuild(&mut self) -> usize

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::{*, 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; 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, 

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<L: Language, N: Analysis<L>> Index<Id> for EGraph<L, N>

type Output = EClass<L, N::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>

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

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