Struct egg::EGraph

source · []
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. 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

Creates a new, empty EGraph with the given Analysis

Returns an iterator over the eclasses in the egraph.

Returns an mutating iterator over the eclasses in the egraph.

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

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

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

Returns the number of eclasses in the egraph.

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

Disable explanations for this EGraph.

Check if explanations are enabled.

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.

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.

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

Get an explanation for why an expression matches a pattern.

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

Creates a Dot to visualize this egraph. See Dot.

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

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

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

Lookup the eclass of the given RecExpr.

Equivalent to the last value in EGraph::lookup_expr_ids.

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

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.

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.

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.

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.

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.

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

Useful for testing.

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

Returns a copy of the value. Read more

Performs copy-assignment from source. Read more

Formats the value using the given formatter. Read more

Returns the “default value” for a type. Read more

Deserialize this value from the given Serde deserializer. Read more

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

The returned type after indexing.

Performs the indexing (container[index]) operation. Read more

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

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

Serialize this value into the given Serde serializer. Read more

Auto Trait Implementations

Blanket Implementations

Gets the TypeId of self. Read more

Immutably borrows from an owned value. Read more

Mutably borrows from an owned value. Read more

Returns the argument unchanged.

Calls U::from(self).

That is, this conversion is whatever the implementation of From<T> for U chooses to do.

The resulting type after obtaining ownership.

Creates owned data from borrowed data, usually by cloning. Read more

🔬 This is a nightly-only experimental API. (toowned_clone_into)

Uses borrowed data to replace owned data, usually by cloning. Read more

The type returned in the event of a conversion error.

Performs the conversion.

The type returned in the event of a conversion error.

Performs the conversion.