Synopsis    [Creates a group encompassing variables from x to y in the  DD table.]  Description [Creates a group encompassing variables from x to y in the  DD table. In the current implementation it must be y == x+1.  Returns 1 in case of success; 0 otherwise.]  SideEffects [None]******************************************************************************/static voidddCreateGroup(  DdManager * table,  int  x,  int  y){    int  gybot;#ifdef DD_DEBUG    assert(y == x+1);#endif    /* Find bottom of second group. */    gybot = y;    while ((unsigned) gybot < table->subtables[gybot].next)	gybot = table->subtables[gybot].next;    /* Link groups. */    table->subtables[x].next = y;    table->subtables[gybot].next = x;    return;} /* ddCreateGroup *//**Function********************************************************************  Synopsis    [Sifts one variable up and down until it has taken all  positions. Checks for aggregation.]  Description [Sifts one variable up and down until it has taken all  positions. Checks for aggregation. There may be at most two sweeps,  even if the group grows.  Assumes that x is either an isolated  variable, or it is the bottom of a group. All groups may not have  been found. The variable being moved is returned to the best position  seen during sifting.  Returns 1 in case of success; 0 otherwise.]  SideEffects [None]******************************************************************************/static intddGroupSiftingAux(  DdManager * table,  int  x,  int  xLow,  int  xHigh,  int (*checkFunction)(DdManager *, int, int),  int lazyFlag){    Move *move;    Move *moves;	/* list of moves */    int  initialSize;    int  result;    int  y;    int  topbot;#ifdef DD_DEBUG    if (pr > 0) (void) fprintf(table->out,			       "ddGroupSiftingAux from %d to %d\n",xLow,xHigh);    assert((unsigned) x >= table->subtables[x].next); /* x is bottom of group */#endif    initialSize = table->keys - table->isolated;    moves = NULL;    originalSize = initialSize;		/* for lazy sifting */    /* If we have a singleton, we check for aggregation in both    ** directions before we sift.    */    if ((unsigned) x == table->subtables[x].next) {	/* Will go down first, unless x == xHigh:	** Look for aggregation above x.	*/	for (y = x; y > xLow; y--) {	    if (!checkFunction(table,y-1,y))		break;	    topbot = table->subtables[y-1].next; /* find top of y-1's group */	    table->subtables[y-1].next = y;	    table->subtables[x].next = topbot; /* x is bottom of group so its */					       /* next is top of y-1's group */	    y = topbot + 1; /* add 1 for y--; new y is top of group */	}	/* Will go up first unless x == xlow:	** Look for aggregation below x.	*/	for (y = x; y < xHigh; y++) {	    if (!checkFunction(table,y,y+1))		break;	    /* find bottom of y+1's group */	    topbot = y + 1;	    while ((unsigned) topbot < table->subtables[topbot].next) {		topbot = table->subtables[topbot].next;	    }	    table->subtables[topbot].next = table->subtables[y].next;	    table->subtables[y].next = y + 1;	    y = topbot - 1; /* subtract 1 for y++; new y is bottom of group */	}    }    /* Now x may be in the middle of a group.    ** Find bottom of x's group.    */    while ((unsigned) x < table->subtables[x].next)	x = table->subtables[x].next;    originalLevel = x;			/* for lazy sifting */    if (x == xLow) { /* Sift down */#ifdef DD_DEBUG	/* x must be a singleton */	assert((unsigned) x == table->subtables[x].next);#endif	if (x == xHigh) return(1);	/* just one variable */        if (!ddGroupSiftingDown(table,x,xHigh,checkFunction,&moves))            goto ddGroupSiftingAuxOutOfMem;	/* at this point x == xHigh, unless early term */	/* move backward and stop at best position */	result = ddGroupSiftingBackward(table,moves,initialSize,					DD_SIFT_DOWN,lazyFlag);#ifdef DD_DEBUG	assert(table->keys - table->isolated <= (unsigned) initialSize);#endif        if (!result) goto ddGroupSiftingAuxOutOfMem;    } else if (cuddNextHigh(table,x) > xHigh) { /* Sift up */#ifdef DD_DEBUG	/* x is bottom of group */        assert((unsigned) x >= table->subtables[x].next);#endif        /* Find top of x's group */        x = table->subtables[x].next;        if (!ddGroupSiftingUp(table,x,xLow,checkFunction,&moves))            goto ddGroupSiftingAuxOutOfMem;	/* at this point x == xLow, unless early term */	/* move backward and stop at best position */	result = ddGroupSiftingBackward(table,moves,initialSize,					DD_SIFT_UP,lazyFlag);#ifdef DD_DEBUG	assert(table->keys - table->isolated <= (unsigned) initialSize);#endif        if (!result) goto ddGroupSiftingAuxOutOfMem;    } else if (x - xLow > xHigh - x) { /* must go down first: shorter */        if (!ddGroupSiftingDown(table,x,xHigh,checkFunction,&moves))            goto ddGroupSiftingAuxOutOfMem;	/* at this point x == xHigh, unless early term */        /* Find top of group */	if (moves) {	    x = moves->y;	}	while ((unsigned) x < table->subtables[x].next)	    x = table->subtables[x].next;	x = table->subtables[x].next;#ifdef DD_DEBUG        /* x should be the top of a group */        assert((unsigned) x <= table->subtables[x].next);#endif        if (!ddGroupSiftingUp(table,x,xLow,checkFunction,&moves))            goto ddGroupSiftingAuxOutOfMem;	/* move backward and stop at best position */	result = ddGroupSiftingBackward(table,moves,initialSize,					DD_SIFT_UP,lazyFlag);#ifdef DD_DEBUG	assert(table->keys - table->isolated <= (unsigned) initialSize);#endif        if (!result) goto ddGroupSiftingAuxOutOfMem;    } else { /* moving up first: shorter */        /* Find top of x's group */        x = table->subtables[x].next;        if (!ddGroupSiftingUp(table,x,xLow,checkFunction,&moves))            goto ddGroupSiftingAuxOutOfMem;	/* at this point x == xHigh, unless early term */        if (moves) {	    x = moves->x;	}	while ((unsigned) x < table->subtables[x].next)	    x = table->subtables[x].next;#ifdef DD_DEBUG        /* x is bottom of a group */        assert((unsigned) x >= table->subtables[x].next);#endif        if (!ddGroupSiftingDown(table,x,xHigh,checkFunction,&moves))            goto ddGroupSiftingAuxOutOfMem;	/* move backward and stop at best position */	result = ddGroupSiftingBackward(table,moves,initialSize,					DD_SIFT_DOWN,lazyFlag);#ifdef DD_DEBUG	assert(table->keys - table->isolated <= (unsigned) initialSize);#endif        if (!result) goto ddGroupSiftingAuxOutOfMem;    }    while (moves != NULL) {        move = moves->next;        cuddDeallocNode(table, (DdNode *) moves);        moves = move;    }    return(1);ddGroupSiftingAuxOutOfMem:    while (moves != NULL) {        move = moves->next;        cuddDeallocNode(table, (DdNode *) moves);        moves = move;    }    return(0);} /* end of ddGroupSiftingAux *//**Function********************************************************************  Synopsis    [Sifts up a variable until either it reaches position xLow  or the size of the DD heap increases too much.]  Description [Sifts up a variable until either it reaches position  xLow or the size of the DD heap increases too much. Assumes that y is  the top of a group (or a singleton).  Checks y for aggregation to the  adjacent variables. Records all the moves that are appended to the  list of moves received as input and returned as a side effect.  Returns 1 in case of success; 0 otherwise.]  SideEffects [None]******************************************************************************/static intddGroupSiftingUp(  DdManager * table,  int  y,  int  xLow,  int (*checkFunction)(DdManager *, int, int),  Move ** moves){    Move *move;    int  x;    int  size;    int  i;    int  gxtop,gybot;    int  limitSize;    int  xindex, yindex;    int  zindex;    int  z;    int  isolated;    int  L;	/* lower bound on DD size */#ifdef DD_DEBUG    int  checkL;#endif    yindex = table->invperm[y];    /* Initialize the lower bound.    ** The part of the DD below the bottom of y's group will not change.    ** The part of the DD above y that does not interact with any    ** variable of y's group will not change.    ** The rest may vanish in the best case, except for    ** the nodes at level xLow, which will not vanish, regardless.    ** What we use here is not really a lower bound, because we ignore    ** the interactions with all variables except y.    */    limitSize = L = table->keys - table->isolated;    gybot = y;    while ((unsigned) gybot < table->subtables[gybot].next)	gybot = table->subtables[gybot].next;    for (z = xLow + 1; z <= gybot; z++) {	zindex = table->invperm[z];	if (zindex == yindex || cuddTestInteract(table,zindex,yindex)) {	    isolated = table->vars[zindex]->ref == 1;	    L -= table->subtables[z].keys - isolated;	}    }    originalLevel = y;			/* for lazy sifting */    x = cuddNextLow(table,y);    while (x >= xLow && L <= limitSize) {#ifdef DD_DEBUG	gybot = y;	while ((unsigned) gybot < table->subtables[gybot].next)	    gybot = table->subtables[gybot].next;	checkL = table->keys - table->isolated;	for (z = xLow + 1; z <= gybot; z++) {	    zindex = table->invperm[z];	    if (zindex == yindex || cuddTestInteract(table,zindex,yindex)) {		isolated = table->vars[zindex]->ref == 1;		checkL -= table->subtables[z].keys - isolated;	    }	}	if (pr > 0 && L != checkL) {	    (void) fprintf(table->out,			   "Inaccurate lower bound: L = %d checkL = %d\n",			   L, checkL);	}#endif        gxtop = table->subtables[x].next;        if (checkFunction(table,x,y)) {	    /* Group found, attach groups */	    table->subtables[x].next = y;	    i = table->subtables[y].next;	    while (table->subtables[i].next != (unsigned) y)		i = table->subtables[i].next;	    table->subtables[i].next = gxtop;	    move = (Move *)cuddDynamicAllocNode(table);	    if (move == NULL) goto ddGroupSiftingUpOutOfMem;	    move->x = x;	    move->y = y;	    move->flags = MTR_NEWNODE;	    move->size = table->keys - table->isolated;	    move->next = *moves;	    *moves = move;        } else if (table->subtables[x].next == (unsigned) x &&		   table->subtables[y].next == (unsigned) y) {            /* x and y are self groups */	    xindex = table->invperm[x];            size = cuddSwapInPlace(table,x,y);#ifdef DD_DEBUG            assert(table->subtables[x].next == (unsigned) x);            assert(table->subtables[y].next == (unsigned) y);#endif            if (size == 0) goto ddGroupSiftingUpOutOfMem;	    /* Update the lower bound. */	    if (cuddTestInteract(table,xindex,yindex)) {		isolated = table->vars[xindex]->ref == 1;		L += table->subtables[y].keys - isolated;	    }            move = (Move *)cuddDynamicAllocNode(table);            if (move == NULL) goto ddGroupSiftingUpOutOfMem;            move->x = x;            move->y = y;	    move->flags = MTR_DEFAULT;            move->size = size;            move->next = *moves;            *moves = move;#ifdef DD_DEBUG	    if (pr > 0) (void) fprintf(table->out,				       "ddGroupSiftingUp (2 single groups):\n");#endif            if ((double) size > (double) limitSize * table->maxGrowth)		return(1);            if (size < limitSize) limitSize = size;        } else { /* Group move */            size = ddGroupMove(table,x,y,moves);	    if (size == 0) goto ddGroupSiftingUpOutOfMem;	    /* Update the lower bound. */	    z = (*moves)->y;	    do {		zindex = table->invperm[z];		if (cuddTestInteract(table,zindex,yindex)) {		    isolated = table->vars[zindex]->ref == 1;		    L += table->subtables[z].keys - isolated;		}		z = table->subtables[z].next;	    } while (z != (int) (*moves)->y);            if ((double) size > (double) limitSize * table->maxGrowth)		return(1);            if (size < limitSize) limitSize = size;        }        y = gxtop;        x = cuddNextLow(table,y);    }    return(1);ddGroupSiftingUpOutOfMem:    while (*moves != NULL) {        move = (*moves)->next;        cuddDeallocNode(table, (DdNode *) *moves);        *moves = move;    }    return(0);} /* end of ddGroupSiftingUp *//**Function********************************************************************  Synopsis    [Sifts down a variable until it reaches position xHigh.]  Description [Sifts down a variable until it reaches position xHigh.  Assumes that x is the bottom of a group (or a singleton).  Records  all the moves.  Returns 1 in case of success; 0 otherwise.]  SideEffects [None]******************************************************************************/static intddGroupSiftingDown(  DdManager * table,  int  x,  int  xHigh,  int (*checkFunction)(DdManager *, int, int),  Move ** moves){    Move *move;    int  y;    int  size;    int  limitSize;    int  gxtop,gybot;    int  R;	/* upper bound on node decrease */    int  xindex, yindex;    int  isolated, allVars;    int  z;    int  zindex;