Graph rewriting with one-to-many pattern matching? In the single-pushout approach to graph rewriting, many nodes in a pattern graph can be matched to a single node of a target graph.

My question is if there is a notion of graph rewriting where the inverse is true: that a single node in the pattern graph can match to many nodes of the target graph. For example, the pattern graph $A \rightarrow B$ should be able to match a subgraph isomorphic to $X \rightarrow Y \leftarrow Z$, with the mapping $A \mapsto \{ X, Z \}, B \mapsto \{Y$}.  I'm especially interested in a definition where $A \mapsto \{X\}, B \mapsto \{ Y\}$ would not be a valid match for any graph that contains $X \rightarrow Y \leftarrow Z$ as a subgraph.

As an example application, consider the problem of for-loop desugaring. This for-loop:

for (int i = 0; i &lt; n; i++) {
  if ( i % 3 == 0) {
    printf("Divisible by 3\n");
    continue;
  }
  printf("%d\n", i);
}


desugars to:

int i = 0;
while (i &lt; n) {
  if (i % 3 == 0) {
    printf("Divisible by 3\n");
    i++;
    continue;
  }
  printf("%d\n", i);
  i++;
}


A key part of this desugaring -- that the "step" part of the for loop be inserted at the end of the loop and before every "continue" statement -- is most easily expressed as a rewrite on the control-flow graph, where that statement is inserted before every predecessor of the condition (except for before the loop runs).
Belatedly posting this answer:

This is called set node or multi-object matching. This is implemented in tools like Henshin https://www.eclipse.org/henshin/publications.php and described informally in http://www.cs.le.ac.uk/people/rh122/papers/2006/Hec06Nutshell.pdf, see 3.2. 

A more formal account is in "Formal foundation of consistent EMF model transformations by algebraic graph transformation."

Thanks to Reiko Heckel for providing me this answer 1 year ago.