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
• egraph:analyze(Name, Lhs, RhsOptions)
• egraph:analyze(Name, Lhs, LhsOptions, RhsOptions)
• egraph:analyze(Name, Lhs, LhsOptions, RhsOptions) :- Body
• egraph:merge_property(Name, V1, V2, Merged)
• egraph:merge_property(Name, V1, V2, Merged) :- Body
• egraph:rule(Name, Lhs, Rhs)
• egraph:rule(Name, Lhs, Rhs) :- Body
• egraph:rule(Name, Lhs, Rhs, RhsOptions)
• egraph:rule(Name, Lhs, Rhs, RhsOptions) :- Body
• egraph:rule(Name, Lhs, LhsOptions, Rhs, RhsOptions)
• egraph:rule(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//2: Extracts the optimal term from the E-graph based on term costs.
• extract_all//2: Extracts all optimal terms from the E-graph based on term costs.
• lookup/2: Retrieves an e-class node from a sorted list of E-graph nodes.
• query//1: Queries the E-graph and dynamically binds pattern variables.

 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.

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

 query(?Pattern)// is multi

Queries the E-graph and dynamically binds pattern variables. Upon success, the variables in the query are bound and the Pattern is unified with the complete extracted matching term from the E-graph. On backtracking, Pattern will be bound to all possible representations of the matched equivalence class in increasing order of cost.

Arguments:

Pattern

- The term pattern to search for, which is unified with the fully extracted match.

 extract(Id, Extracted)// is det

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

Arguments:

Id	- The eclass Id to be extracted as returned by add_term
Extracted	- the extracted term

Undocumented predicates

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

 add_terms(Arg1, Arg2, Arg3, Arg4)

 extract_all(Arg1, Arg2, Arg3, Arg4)