This module implements an E-graph (Equivalence Graph) data structure, commonly used for efficient term rewriting, congruence closure, and e-matching. The E-graph state is typically threaded through operations using DCG notation.

Rewrite rules are automatically compiled into efficient DCG predicates via term expansion. See the egraph_compile module for full details. The supported rule declarations are:

• egraph:rewrite(Name, Lhs, Rhs)
• egraph:rewrite(Name, Lhs, Rhs, RhsOptions)
• egraph:rewrite(Name, Lhs, LhsOptions, Rhs, RhsOptions)
• egraph:rewrite(Name, Lhs, LhsOptions, Rhs, RhsOptions) :- Body

Main predicates:

• add_term//2: Adds a term to the E-graph, returning its e-class ID.
• union//2: Merges two e-classes.
• saturate//1, saturate//2: Applies compiled rewrite rules to the E-graph until saturation or an iteration limit is reached.
• extract/1, extract//0: Extracts the optimal term(s) from the E-graph based on term costs.
• lookup/2: Retrieves an e-class node from a sorted list of E-graph nodes.

 lookup(+Pair, +SortedPairs) is semidet

Retrieves a value from a sorted list of pairs using standard term comparison. The search is unrolled for performance. Adapted from ord_memberchk/2.

Arguments:

Pair	- A Key-Value pair where Key is the target key to find, and Value is unified with the associated value.
SortedPairs	- A list of Key-Value pairs sorted by Key.

 add_term(+Term, -Id)// is det

Adds a term to the E-graph, returning its e-class ID. Compound terms are recursively traversed and their arguments are added to the E-graph first. Variables are represented using '$VAR'/1 wrappers.

Arguments:

Term	- The term to be added.
Id	- The e-class ID representing the added term.

 union(+Id1, +Id2)// is det

Merges two e-classes by unifying their IDs and merging their underlying nodes.

Arguments:

Id1	- The first e-class ID.
Id2	- The second e-class ID.

 saturate(+Rules)// is det

Applies a list of compiled rewrite rules to the E-graph until saturation is reached.

Arguments:

Rules

- A list of compiled rewrite rule names to apply.

 saturate(+Rules, +N)// is det

Applies a list of compiled rewrite rules to the E-graph up to N times or until saturation is reached.

Arguments:

Rules	- A list of compiled rewrite rule names to apply.
N	- The maximum number of iterations (or inf for no limit).

 extract(+Nodes) is det

 extract// is det

Extracts the optimal term(s) from the E-graph based on term costs.

Arguments:

Nodes

- A list of E-graph nodes representing the state.

Undocumented predicates

The following predicates are exported, but not or incorrectly documented.

 extract(Arg1, Arg2)