case CUDD_REORDER_RANDOM:	case CUDD_REORDER_RANDOM_PIVOT:	    result = cuddSwapping(table,lower,upper,method);	    break;	case CUDD_REORDER_SIFT:	    result = cuddSifting(table,lower,upper);	    break;	case CUDD_REORDER_SIFT_CONVERGE:	    do {		initialSize = table->keys - table->isolated;		result = cuddSifting(table,lower,upper);		if (initialSize <= table->keys - table->isolated)		    break;#ifdef DD_STATS		else		    (void) fprintf(table->out,"\n");#endif	    } while (result != 0);	    break;	case CUDD_REORDER_SYMM_SIFT:	    result = cuddSymmSifting(table,lower,upper);	    break;	case CUDD_REORDER_SYMM_SIFT_CONV:	    result = cuddSymmSiftingConv(table,lower,upper);	    break;	case CUDD_REORDER_GROUP_SIFT:	    if (table->groupcheck == CUDD_NO_CHECK) {		result = ddGroupSifting(table,lower,upper,ddNoCheck,					DD_NORMAL_SIFT);	    } else if (table->groupcheck == CUDD_GROUP_CHECK5) {		result = ddGroupSifting(table,lower,upper,ddExtSymmCheck,					DD_NORMAL_SIFT);	    } else if (table->groupcheck == CUDD_GROUP_CHECK7) {		result = ddGroupSifting(table,lower,upper,ddExtSymmCheck,					DD_NORMAL_SIFT);	    } else {		(void) fprintf(table->err,			       "Unknown group ckecking method\n");		result = 0;	    }	    break;	case CUDD_REORDER_GROUP_SIFT_CONV:	    do {		initialSize = table->keys - table->isolated;		if (table->groupcheck == CUDD_NO_CHECK) {		    result = ddGroupSifting(table,lower,upper,ddNoCheck,					    DD_NORMAL_SIFT);		} else if (table->groupcheck == CUDD_GROUP_CHECK5) {		    result = ddGroupSifting(table,lower,upper,ddExtSymmCheck,					    DD_NORMAL_SIFT);		} else if (table->groupcheck == CUDD_GROUP_CHECK7) {		    result = ddGroupSifting(table,lower,upper,ddExtSymmCheck,					    DD_NORMAL_SIFT);		} else {		    (void) fprintf(table->err,				   "Unknown group ckecking method\n");		    result = 0;		}#ifdef DD_STATS		(void) fprintf(table->out,"\n");#endif		result = cuddWindowReorder(table,lower,upper,					   CUDD_REORDER_WINDOW4);		if (initialSize <= table->keys - table->isolated)		    break;#ifdef DD_STATS		else		    (void) fprintf(table->out,"\n");#endif	    } while (result != 0);	    break;	case CUDD_REORDER_WINDOW2:	case CUDD_REORDER_WINDOW3:	case CUDD_REORDER_WINDOW4:	case CUDD_REORDER_WINDOW2_CONV:	case CUDD_REORDER_WINDOW3_CONV:	case CUDD_REORDER_WINDOW4_CONV:	    result = cuddWindowReorder(table,lower,upper,method);	    break;	case CUDD_REORDER_ANNEALING:	    result = cuddAnnealing(table,lower,upper);	    break;	case CUDD_REORDER_GENETIC:	    result = cuddGa(table,lower,upper);	    break;	case CUDD_REORDER_LINEAR:	    result = cuddLinearAndSifting(table,lower,upper);	    break;	case CUDD_REORDER_LINEAR_CONVERGE:	    do {		initialSize = table->keys - table->isolated;		result = cuddLinearAndSifting(table,lower,upper);		if (initialSize <= table->keys - table->isolated)		    break;#ifdef DD_STATS		else		    (void) fprintf(table->out,"\n");#endif	    } while (result != 0);	    break;	case CUDD_REORDER_EXACT:	    result = cuddExact(table,lower,upper);	    break;	case CUDD_REORDER_LAZY_SIFT:	    result = ddGroupSifting(table,lower,upper,ddVarGroupCheck,				    DD_LAZY_SIFT);	    break;	default:	    return(0);	}    }    /* Create a single group for all the variables that were sifted,    ** so that they will be treated as a single block by successive    ** invocations of ddGroupSifting.    */    ddMergeGroups(table,treenode,lower,upper);#ifdef DD_DEBUG    if (pr > 0) (void) fprintf(table->out,"ddReorderChildren:");#endif    return(result);} /* end of ddReorderChildren *//**Function********************************************************************  Synopsis    [Finds the lower and upper bounds of the group represented  by treenode.]  Description [Finds the lower and upper bounds of the group  represented by treenode.  From the index and size fields we need to  derive the current positions, and find maximum and minimum.]  SideEffects [The bounds are returned as side effects.]  SeeAlso     []******************************************************************************/static voidddFindNodeHiLo(  DdManager * table,  MtrNode * treenode,  int * lower,  int * upper){    int low;    int high;    /* Check whether no variables in this group already exist.    ** If so, return immediately. The calling procedure will know from    ** the values of upper that no reordering is needed.    */    if ((int) treenode->low >= table->size) {	*lower = table->size;	*upper = -1;	return;    }    *lower = low = (unsigned int) table->perm[treenode->index];    high = (int) (low + treenode->size - 1);    if (high >= table->size) {	/* This is the case of a partially existing group. The aim is to	** reorder as many variables as safely possible.  If the tree	** node is terminal, we just reorder the subset of the group	** that is currently in existence.  If the group has	** subgroups, then we only reorder those subgroups that are	** fully instantiated.  This way we avoid breaking up a group.	*/	MtrNode *auxnode = treenode->child;	if (auxnode == NULL) {	    *upper = (unsigned int) table->size - 1;	} else {	    /* Search the subgroup that strands the table->size line.	    ** If the first group starts at 0 and goes past table->size	    ** upper will get -1, thus correctly signaling that no reordering	    ** should take place.	    */	    while (auxnode != NULL) {		int thisLower = table->perm[auxnode->low];		int thisUpper = thisLower + auxnode->size - 1;		if (thisUpper >= table->size && thisLower < table->size)		    *upper = (unsigned int) thisLower - 1;		auxnode = auxnode->younger;	    }	}    } else {	/* Normal case: All the variables of the group exist. */	*upper = (unsigned int) high;    }#ifdef DD_DEBUG    /* Make sure that all variables in group are contiguous. */    assert(treenode->size >= *upper - *lower + 1);#endif    return;} /* end of ddFindNodeHiLo *//**Function********************************************************************  Synopsis    [Comparison function used by qsort.]  Description [Comparison function used by qsort to order the variables  according to the number of keys in the subtables.  Returns the  difference in number of keys between the two variables being  compared.]  SideEffects [None]******************************************************************************/static intddUniqueCompareGroup(  int * ptrX,  int * ptrY){#if 0    if (entry[*ptrY] == entry[*ptrX]) {	return((*ptrX) - (*ptrY));    }#endif    return(entry[*ptrY] - entry[*ptrX]);} /* end of ddUniqueCompareGroup *//**Function********************************************************************  Synopsis    [Sifts from treenode->low to treenode->high.]  Description [Sifts from treenode->low to treenode->high. If  croupcheck == CUDD_GROUP_CHECK7, it checks for group creation at the  end of the initial sifting. If a group is created, it is then sifted  again. After sifting one variable, the group that contains it is  dissolved.  Returns 1 in case of success; 0 otherwise.]  SideEffects [None]******************************************************************************/static intddGroupSifting(  DdManager * table,  int  lower,  int  upper,  int (*checkFunction)(DdManager *, int, int),  int lazyFlag){    int		*var;    int		i,j,x,xInit;    int		nvars;    int		classes;    int		result;    int		*sifted;    int		merged;    int		dissolve;#ifdef DD_STATS    unsigned	previousSize;#endif    int		xindex;    nvars = table->size;    /* Order variables to sift. */    entry = NULL;    sifted = NULL;    var = ALLOC(int,nvars);    if (var == NULL) {	table->errorCode = CUDD_MEMORY_OUT;	goto ddGroupSiftingOutOfMem;    }    entry = ALLOC(int,nvars);    if (entry == NULL) {	table->errorCode = CUDD_MEMORY_OUT;	goto ddGroupSiftingOutOfMem;    }    sifted = ALLOC(int,nvars);    if (sifted == NULL) {	table->errorCode = CUDD_MEMORY_OUT;	goto ddGroupSiftingOutOfMem;    }    /* Here we consider only one representative for each group. */    for (i = 0, classes = 0; i < nvars; i++) {	sifted[i] = 0;	x = table->perm[i];	if ((unsigned) x >= table->subtables[x].next) {	    entry[i] = table->subtables[x].keys;	    var[classes] = i;	    classes++;	}    }    qsort((void *)var,classes,sizeof(int),	  (int (*)(const void *, const void *)) ddUniqueCompareGroup);    if (lazyFlag) {	for (i = 0; i < nvars; i ++) {	    ddResetVarHandled(table, i);	}    }    /* Now sift. */    for (i = 0; i < ddMin(table->siftMaxVar,classes); i++) {	if (ddTotalNumberSwapping >= table->siftMaxSwap)	    break;	xindex = var[i];	if (sifted[xindex] == 1) /* variable already sifted as part of group */	    continue;        x = table->perm[xindex]; /* find current level of this variable */	if (x < lower || x > upper || table->subtables[x].bindVar == 1)	    continue;#ifdef DD_STATS	previousSize = table->keys - table->isolated;#endif#ifdef DD_DEBUG	/* x is bottom of group */        assert((unsigned) x >= table->subtables[x].next);#endif	if ((unsigned) x == table->subtables[x].next) {	    dissolve = 1;	    result = ddGroupSiftingAux(table,x,lower,upper,checkFunction,	    				lazyFlag);	} else {	    dissolve = 0;	    result = ddGroupSiftingAux(table,x,lower,upper,ddNoCheck,lazyFlag);	}	if (!result) goto ddGroupSiftingOutOfMem;	/* check for aggregation */	merged = 0;	if (lazyFlag == 0 && table->groupcheck == CUDD_GROUP_CHECK7) {	    x = table->perm[xindex]; /* find current level */	    if ((unsigned) x == table->subtables[x].next) { /* not part of a group */		if (x != upper && sifted[table->invperm[x+1]] == 0 &&		(unsigned) x+1 == table->subtables[x+1].next) {		    if (ddSecDiffCheck(table,x,x+1)) {			merged =1;			ddCreateGroup(table,x,x+1);		    }		}		if (x != lower && sifted[table->invperm[x-1]] == 0 &&		(unsigned) x-1 == table->subtables[x-1].next) {		    if (ddSecDiffCheck(table,x-1,x)) {			merged =1;			ddCreateGroup(table,x-1,x);		    }		}	    }	}	if (merged) { /* a group was created */	    /* move x to bottom of group */	    while ((unsigned) x < table->subtables[x].next)		x = table->subtables[x].next;	    /* sift */	    result = ddGroupSiftingAux(table,x,lower,upper,ddNoCheck,lazyFlag);	    if (!result) goto ddGroupSiftingOutOfMem;#ifdef DD_STATS	    if (table->keys < previousSize + table->isolated) {		(void) fprintf(table->out,"_");	    } else if (table->keys > previousSize + table->isolated) {		(void) fprintf(table->out,"^");	    } else {		(void) fprintf(table->out,"*");	    }	    fflush(table->out);	} else {	    if (table->keys < previousSize + table->isolated) {		(void) fprintf(table->out,"-");	    } else if (table->keys > previousSize + table->isolated) {		(void) fprintf(table->out,"+");	    } else {		(void) fprintf(table->out,"=");	    }	    fflush(table->out);#endif	}	/* Mark variables in the group just sifted. */	x = table->perm[xindex];	if ((unsigned) x != table->subtables[x].next) {	    xInit = x;	    do {		j = table->invperm[x];		sifted[j] = 1;		x = table->subtables[x].next;	    } while (x != xInit);	    /* Dissolve the group if it was created. */	    if (lazyFlag == 0 && dissolve) {		do {		    j = table->subtables[x].next;		    table->subtables[x].next = x;		    x = j;		} while (x != xInit);	    }	}#ifdef DD_DEBUG	if (pr > 0) (void) fprintf(table->out,"ddGroupSifting:");#endif      if (lazyFlag) ddSetVarHandled(table, xindex);    } /* for */    FREE(sifted);    FREE(var);    FREE(entry);    return(1);ddGroupSiftingOutOfMem:    if (entry != NULL)	FREE(entry);    if (var != NULL)	FREE(var);    if (sifted != NULL)	FREE(sifted);    return(0);} /* end of ddGroupSifting *//**Function********************************************************************