Graph matching function accepting two lists of arcs and returning a node map if successful

A label lookup table specialized to LabelIndex indices.

Type for label->index lookup table

A label associated with a LabelIndex

A Mapping between a label and a value (e.g. an index value).

This instance of class label adds a graph identifier to each variable label, so that variable labels from different graphs are always seen as distinct values.

The essential logic added by this class instance is embodied in the eq and hash functions. Note that variable label hashes depend only on the graph in which they appear, and non-variable label hashes depend only on the variable. Label hash values are used when initializing a label equivalence-class map (and, for non-variable labels, also for resolving hash collisions).

Create a scoped label given an identifier and label.

Create an arc containining a scoped label with the given identifier.

LabelIndex is a unique value assigned to each label, such that labels with different values are definitely different values in the graph; e.g. do not map to each other in the graph bijection. The first member is a generation counter that ensures new values are distinct from earlier passes.

Type for equivalence class description (An equivalence class is a collection of labels with the same LabelIndex value.)

The null, or empty, index value.

The empty label map table.

Does this node have a variable binding?

Calculate the hash of the label using the supplied seed.

Map a label to its corresponding label index value in the supplied LabelMap.

Replace a label and its associated value in a label map with a new value using the supplied hash value and the current LabelMap generation number. If the key is not found, then no change is made to the label map.

Replace selected values in a label map with new values from the supplied list of labels and new label index values. The generation number is supplied from the current label map. The generation number in the resulting label map is incremented.

Return the set of distinct labels used in the graph.

Scan label list, assigning initial label map values, adding new values to the label map supplied.

Label map values are assigned on the basis of the label alone, without regard for it's connectivity in the graph. (cf. reclassify).

All variable node labels are assigned the same initial value, as they may be matched with each other.

Increment the generation of the label map.

Returns a new label map identical to the supplied value but with an incremented generation number.

Recursive graph matching function

This function assumes that no variable label appears in both graphs. (Function graphMatch, which calls this, ensures that all variable labels are distinct.)

Auxiliary graph matching function

This function is called when deterministic decomposition of node mapping equivalence classes has run its course.

It picks a pair of equivalence classes in ecpairs, and arbitrarily matches pairs of nodes in those equivalence classes, recursively calling the graph matching function until a suitable node mapping is discovered (success), or until all such pairs have been tried (failure).

This function represents a point to which arbitrary choices are backtracked. The list comprehension glp represents the alternative choices at the point of backtracking

The selected pair of nodes are placed in a new equivalence class based on their original equivalence class value, but with a new NodeVal generation number.

Return the equivalence classes of the supplied nodes using the label map.

Reclassify labels

Examines the supplied label equivalence classes (based on the supplied label map), and evaluates new equivalence subclasses based on node values and adjacency (for variable nodes) and rehashing (for non-variable nodes).

Note, assumes that all all equivalence classes supplied are non-singletons; i.e. contain more than one label.