A lightweight wrapper around an e-graph that defers the application of union operations.
Normally, applying a union in an e-graph requires invoking EClassCall)], ParallelMap), which merges the e-classes and triggers a rebuild. When many unions are expected—such as during a rewrite pass—it is more efficient to defer them and apply them all at once.
EGraphWithPendingUnions collects such deferred unions and lets you apply them in a batch by calling rebuilt or rebuild. Internally, these methods delegate to EClassCall)], ParallelMap), ensuring that all unions are applied and the e-graph is fully rebuilt.
You rarely need to construct this wrapper directly. Instead, you can call EGraph.union, which returns an EGraphWithPendingUnions, allowing fluent chaining:
val updated = egraph
.union(a, b) // returns EGraphWithPendingUnions
.union(c, d) // chains further unions
.rebuilt // applies all pending unions and returns a rebuilt EGraph
This is particularly useful in rewrite systems and equality saturation loops, where batching union operations avoids excessive intermediate rebuilds and improves performance.
Type parameters
NodeT
The type of e-nodes stored in the e-graph.
Repr
The concrete type of the underlying e-graph, which must support union and rebuild.
Value parameters
egraph
The underlying e-graph.
pending
A list of deferred unions (pairs of e-class references).
The union is not applied immediately but instead recorded in the list of pending unions. Use rebuild or rebuilt to apply all deferred unions and obtain a fully updated e-graph.
If the two e-classes already belong to the same class, this method is a no-op.