16.3.2 Encoding Nodes as Records

In our implementation, we associate with each node a unique index which is an integer number I and a record with features

eq down up side eqdown  
equp daughters

The entries of the record are set variables N.eq, N.down, N.up and N.side whose meaning was explained above. Furthermore, there are auxiliary sets variables N.eqDown and N.eqUp which satisfy

Finally, the value of N.daughters is the list of records for the daughter nodes. We require the following membership constraint in order to relate the index I with the record N of a node:

The functional procedure MakeNode below inputs the index I of a node and a tuple VDom=[1#N] where N is the number of all nodes in the constraint graph. It returns the record for the node and imposes the above given constraints on its set variables.

<DC: make node>=

fun {MakeNode I VDom}
   Eq     = {FS.var.upperBound VDom}
   Down   = {FS.var.upperBound VDom}
   Up     = {FS.var.upperBound VDom}
   Side   = {FS.var.upperBound VDom}
   EqDown = {FS.union Eq Down}
   EqUp   = {FS.union Eq Up}
in 
   {FS.partition [Eq Down Up Side] {FS.value.make VDom}}
   {FS.include I Eq}
   node(
      eq        : Eq
      down      : Down
      up        : Up
      side      : Side
      eqdown    : EqDown
      equp      : EqUp
      daughters : _)
end

If two nodes are forced to denote the same node then the corresponding records are unified (but not the corresponding indices). Thus all features of the unified records are unified as well. Hence, the corresponding records for the daughtors of both nodes are also unified. This shows how record unification is used in the dominance constraint solver.