cuddgroup.c

主要进行大规模的电路综合

	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 void
ddFindNodeHiLo(
  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 int
ddUniqueCompareGroup(
  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 int
ddGroupSifting(
  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********************************************************************