The division operation takes place for the , and . The goal of this operation is to split the input into several graphs, such that for each one of these graphs, the node directly pointed to by points to a single node by selector . Going back to Fig. 1 (a) and (b), we can see how the is divided into graphs and .
The original graph is presented in Fig. 1(a). Note that the node directly pointed to by , , points to two different nodes by selector . Therefore, we divide this graph into two different ones in such a way that in each resulting graph, points to a single node by . We see these two graphs in Fig. 1(b), where in the node only points to node and in this node only points to node .
Basically, with the division, we try to recover the individual characteristics of memory configurations that were fused into a single RSG in a previous sentence. However, this division can generate redundant or inexistent nodes, and links which should be removed by the subsequent PRUNE operation (described next). This way, we separate several memory configurations that were represented by the same RSG, achieving a more precise representation.
Taking this into account, we define DIVIDE which divides the in the set regarding the pvar and selector . This division is carried out in the following way. If , then, , we create a such that , and . Each can contain a single node pointed to by by selector . This is subsequently pruned to obtain the definitive PRUNE for the DIVIDE function. This pruning process is described next.