Struct EGraph 

pub struct EGraph<L, N>
where
    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, N> EGraph<L, N>

where L: Language, N: Analysis<L>,

pub fn new(analysis: N) -> EGraph<L, N>

Creates a new, empty EGraph with the given Analysis

pub fn classes(&self) -> impl ExactSizeIterator

Returns an iterator over the eclasses in the egraph.

pub fn classes_mut(&mut self) -> impl ExactSizeIterator

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

Enable explanations for this EGraph. This allows the egraph to explain why two expressions are equivalent with the explain_equivalence function.

pub fn with_explanations_disabled(self) -> EGraph<L, N>

Disable explanations for this EGraph.

pub fn are_explanations_enabled(&self) -> bool

Check if explanations are enabled.

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.

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

Return an Explanation for why a pattern appears in the egraph.

pub fn explain_matches( &mut self, left: &RecExpr<L>, right: &RecExpr<ENodeOrVar<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, N> EGraph<L, N>

where L: Language, N: Analysis<L>,

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 add_instantiation( &mut self, pat: &RecExpr<ENodeOrVar<L>>, subst: &Subst, ) -> Id

Adds a Pattern and a substitution to the EGraph.

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, so you must call rebuild any query operations.

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: &RecExpr<ENodeOrVar<L>>, to_pat: &RecExpr<ENodeOrVar<L>>, subst: &Subst, rule_name: impl Into<Symbol>, ) -> (Id, bool)

Given two patterns and a substitution, add the patterns and mark them for unioning. The unions are performed when rebuild is called. When explanations are enabled with_explanations_enabled, use this function instead of union.

The returned bool indicates whether a union is necessary, and returned Id represents the eclass of the left pattern.

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

Marks two eclasses to be unioned given their ids.

At the end of each iteration, these classes are unioned during rebuild.

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. Both results are canonical.

When explanations are enabled, this function is not available. Instead, use union_instantiations. See explain_equivalence for a more detailed explanation of the feature.

You must call rebuild to observe any effect.

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

where L: Language + Display, N: Analysis<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.

impl<L, N> EGraph<L, N>

where L: Language, N: Analysis<L>,

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());
// The effects of this union aren't yet visible;
// The union has not taken effect.
egraph.union(x, y);
// Classes: [x] [y] [ax] [ay] [a]
assert_eq!(egraph.number_of_classes(), 5);
assert_ne!(egraph.find(ax), egraph.find(ay));

// Rebuilding applies the union and restores the invariants, 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, N> Clone for EGraph<L, N>

where L: Clone + Language, N: Clone + Analysis<L>, <N as Analysis<L>>::Data: Clone,

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

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl<L, N> Debug for EGraph<L, N>

where L: Language, N: Analysis<L>,

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

Formats the value using the given formatter.

impl<L, N> Default for EGraph<L, N>

where L: Language, N: Analysis<L> + Default,

fn default() -> EGraph<L, N>

Returns the “default value” for a type.

impl<'de, L, N> Deserialize<'de> for EGraph<L, N>

where L: Language + Deserialize<'de>, N: Analysis<L> + Deserialize<'de>, <N as Analysis<L>>::Data: for<'a> Deserialize<'a>,

fn deserialize<__D>( __deserializer: __D, ) -> Result<EGraph<L, N>, <__D as Deserializer<'de>>::Error>

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl<L, N> Index<Id> for EGraph<L, N>

where L: Language, N: Analysis<L>,

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) -> &<EGraph<L, N> as Index<Id>>::Output

Performs the indexing (container[index]) operation.

impl<L, N> IndexMut<Id> for EGraph<L, N>

where L: Language, N: Analysis<L>,

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 <EGraph<L, N> as Index<Id>>::Output

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

impl<L, N> Serialize for EGraph<L, N>

where L: Language + Serialize, N: Analysis<L> + Serialize, <N as Analysis<L>>::Data: Serialize,

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

where __S: Serializer,

Serialize this value into the given Serde serializer.