return(1);} /* end of ddGroupSiftingBackward *//**Function********************************************************************  Synopsis    [Merges groups in the DD table.]  Description [Creates a single group from low to high and adjusts the  index field of the tree node.]  SideEffects [None]******************************************************************************/static voidddMergeGroups(  DdManager * table,  MtrNode * treenode,  int  low,  int  high){    int i;    MtrNode *auxnode;    int saveindex;    int newindex;    /* Merge all variables from low to high in one group, unless    ** this is the topmost group. In such a case we do not merge lest    ** we lose the symmetry information. */    if (treenode != table->tree) {	for (i = low; i < high; i++)	    table->subtables[i].next = i+1;	table->subtables[high].next = low;    }    /* Adjust the index fields of the tree nodes. If a node is the    ** first child of its parent, then the parent may also need adjustment. */    saveindex = treenode->index;    newindex = table->invperm[low];    auxnode = treenode;    do {	auxnode->index = newindex;	if (auxnode->parent == NULL ||		(int) auxnode->parent->index != saveindex)	    break;	auxnode = auxnode->parent;    } while (1);    return;} /* end of ddMergeGroups *//**Function********************************************************************  Synopsis    [Dissolves a group in the DD table.]  Description [x and y are variables in a group to be cut in two. The cut  is to pass between x and y.]  SideEffects [None]******************************************************************************/static voidddDissolveGroup(  DdManager * table,  int  x,  int  y){    int topx;    int boty;    /* find top and bottom of the two groups */    boty = y;    while ((unsigned) boty < table->subtables[boty].next)	boty = table->subtables[boty].next;        topx = table->subtables[boty].next;    table->subtables[boty].next = y;    table->subtables[x].next = topx;    return;} /* end of ddDissolveGroup *//**Function********************************************************************  Synopsis    [Pretends to check two variables for aggregation.]  Description [Pretends to check two variables for aggregation. Always  returns 0.]  SideEffects [None]******************************************************************************/static intddNoCheck(  DdManager * table,  int  x,  int  y){    return(0);} /* end of ddNoCheck *//**Function********************************************************************  Synopsis    [Checks two variables for aggregation.]  Description [Checks two variables for aggregation. The check is based  on the second difference of the number of nodes as a function of the  layer. If the second difference is lower than a given threshold  (typically negative) then the two variables should be aggregated.  Returns 1 if the two variables pass the test; 0 otherwise.]  SideEffects [None]******************************************************************************/static intddSecDiffCheck(  DdManager * table,  int  x,  int  y){    double Nx,Nx_1;    double Sx;    double threshold;    int    xindex,yindex;    if (x==0) return(0);#ifdef DD_STATS    secdiffcalls++;#endif    Nx = (double) table->subtables[x].keys;    Nx_1 = (double) table->subtables[x-1].keys;    Sx = (table->subtables[y].keys/Nx) - (Nx/Nx_1);    threshold = table->recomb / 100.0;    if (Sx < threshold) {	xindex = table->invperm[x];	yindex = table->invperm[y];	if (cuddTestInteract(table,xindex,yindex)) {#if defined(DD_DEBUG) && defined(DD_VERBOSE)	    (void) fprintf(table->out,			   "Second difference for %d = %g Pos(%d)\n",			   table->invperm[x],Sx,x);#endif#ifdef DD_STATS	    secdiff++;#endif	    return(1);	} else {#ifdef DD_STATS	    secdiffmisfire++;#endif	    return(0);	}    }    return(0);} /* end of ddSecDiffCheck *//**Function********************************************************************  Synopsis    [Checks for extended symmetry of x and y.]  Description [Checks for extended symmetry of x and y. Returns 1 in  case of extended symmetry; 0 otherwise.]  SideEffects [None]******************************************************************************/static intddExtSymmCheck(  DdManager * table,  int  x,  int  y){    DdNode *f,*f0,*f1,*f01,*f00,*f11,*f10;    DdNode *one;    int comple;		/* f0 is complemented */    int notproj;	/* f is not a projection function */    int arccount;	/* number of arcs from layer x to layer y */    int TotalRefCount;	/* total reference count of layer y minus 1 */    int counter;	/* number of nodes of layer x that are allowed */    			/* to violate extended symmetry conditions */    int arccounter;	/* number of arcs into layer y that are allowed */			/* to come from layers other than x */    int i;    int xindex;    int yindex;    int res;    int slots;    DdNodePtr *list;    DdNode *sentinel = &(table->sentinel);    xindex = table->invperm[x];    yindex = table->invperm[y];    /* If the two variables do not interact, we do not want to merge them. */    if (!cuddTestInteract(table,xindex,yindex))	return(0);#ifdef DD_DEBUG    /* Checks that x and y do not contain just the projection functions.    ** With the test on interaction, these test become redundant,    ** because an isolated projection function does not interact with    ** any other variable.    */    if (table->subtables[x].keys == 1) {	assert(table->vars[xindex]->ref != 1);    }    if (table->subtables[y].keys == 1) {	assert(table->vars[yindex]->ref != 1);    }#endif#ifdef DD_STATS    extsymmcalls++;#endif    arccount = 0;    counter = (int) (table->subtables[x].keys *	      (table->symmviolation/100.0) + 0.5);    one = DD_ONE(table);    slots = table->subtables[x].slots;    list = table->subtables[x].nodelist;    for (i = 0; i < slots; i++) {	f = list[i];	while (f != sentinel) {	    /* Find f1, f0, f11, f10, f01, f00. */	    f1 = cuddT(f);	    f0 = Cudd_Regular(cuddE(f));	    comple = Cudd_IsComplement(cuddE(f));	    notproj = f1 != one || f0 != one || f->ref != (DdHalfWord) 1;	    if (f1->index == yindex) {		arccount++;		f11 = cuddT(f1); f10 = cuddE(f1);	    } else {		if ((int) f0->index != yindex) {		    /* If f is an isolated projection function it is		    ** allowed to bypass layer y.		    */		    if (notproj) {			if (counter == 0)			    return(0);			counter--; /* f bypasses layer y */		    }		}		f11 = f10 = f1;	    }	    if ((int) f0->index == yindex) {		arccount++;		f01 = cuddT(f0); f00 = cuddE(f0);	    } else {		f01 = f00 = f0;	    }	    if (comple) {		f01 = Cudd_Not(f01);		f00 = Cudd_Not(f00);	    }	    /* Unless we are looking at a projection function	    ** without external references except the one from the	    ** table, we insist that f01 == f10 or f11 == f00	    */	    if (notproj) {		if (f01 != f10 && f11 != f00) {		    if (counter == 0)			return(0);		    counter--;		}	    }	    f = f->next;	} /* while */    } /* for */    /* Calculate the total reference counts of y */    TotalRefCount = -1;	/* -1 for projection function */    slots = table->subtables[y].slots;    list = table->subtables[y].nodelist;    for (i = 0; i < slots; i++) {	f = list[i];	while (f != sentinel) {	    TotalRefCount += f->ref;	    f = f->next;	}    }    arccounter = (int) (table->subtables[y].keys *		 (table->arcviolation/100.0) + 0.5);    res = arccount >= TotalRefCount - arccounter;#if defined(DD_DEBUG) && defined(DD_VERBOSE)    if (res) {	(void) fprintf(table->out,		       "Found extended symmetry! x = %d\ty = %d\tPos(%d,%d)\n",		       xindex,yindex,x,y);    }#endif#ifdef DD_STATS    if (res)	extsymm++;#endif    return(res);} /* end ddExtSymmCheck *//**Function********************************************************************  Synopsis    [Checks for grouping of x and y.]  Description [Checks for grouping of x and y. Returns 1 in  case of grouping; 0 otherwise. This function is used for lazy sifting.]  SideEffects [None]******************************************************************************/static intddVarGroupCheck(  DdManager * table,  int x,  int y){    int xindex = table->invperm[x];    int yindex = table->invperm[y];    if (Cudd_bddIsVarToBeUngrouped(table, xindex)) return(0);    if (Cudd_bddReadPairIndex(table, xindex) == yindex) {	if (ddIsVarHandled(table, xindex) ||	    ddIsVarHandled(table, yindex)) {	    if (Cudd_bddIsVarToBeGrouped(table, xindex) ||		Cudd_bddIsVarToBeGrouped(table, yindex) ) {		if (table->keys - table->isolated <= originalSize) {		    return(1);		}	    }	}    }    return(0);} /* end of ddVarGroupCheck *//**Function********************************************************************  Synopsis    [Sets a variable to already handled.]  Description [Sets a variable to already handled. This function is used  for lazy sifting.]  SideEffects [none]  SeeAlso     []******************************************************************************/static intddSetVarHandled(  DdManager *dd,  int index){    if (index >= dd->size || index < 0) return(0);    dd->subtables[dd->perm[index]].varHandled = 1;    return(1);} /* end of ddSetVarHandled *//**Function********************************************************************  Synopsis    [Resets a variable to be processed.]  Description [Resets a variable to be processed. This function is used  for lazy sifting.]  SideEffects [none]  SeeAlso     []******************************************************************************/static intddResetVarHandled(  DdManager *dd,  int index){    if (index >= dd->size || index < 0) return(0);    dd->subtables[dd->perm[index]].varHandled = 0;    return(1);} /* end of ddResetVarHandled *//**Function********************************************************************  Synopsis    [Checks whether a variables is already handled.]  Description [Checks whether a variables is already handled. This  function is used for lazy sifting.]  SideEffects [none]  SeeAlso     []******************************************************************************/static intddIsVarHandled(  DdManager *dd,  int index){    if (index >= dd->size || index < 0) return(-1);    return dd->subtables[dd->perm[index]].varHandled;} /* end of ddIsVarHandled */