extrazddmisc.c

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

  SeeAlso     []

******************************************************************************/
DdNode * extraZddUniverse(
  DdManager * dd, 
  DdNode * VarSet)
{
	DdNode *zRes, *zPart;
    statLine(dd); 

	if ( VarSet == dd->zero )
	{
		printf("\nextraZddUniverse(): Singles is not a ZDD!\n");
		return NULL;
	}
	if ( VarSet == dd->one )
		return dd->one;

    /* check cache */
    zRes = cuddCacheLookup1Zdd(dd, extraZddUniverse, VarSet);
    if (zRes)
		return(zRes);

	/* make sure that VarSet is a single combination */
	if ( cuddE( VarSet ) != dd->zero )
	{
		printf("\nextraZddUniverse(): VarSet is not a single combination!\n");
		return NULL;
	}

	/* solve the problem recursively */
	zPart = extraZddUniverse( dd, cuddT( VarSet ) );
	if ( zPart == NULL ) 
		return NULL;
	cuddRef( zPart );

	/* create new node with this variable */
	zRes = cuddZddGetNode( dd, VarSet->index, zPart, zPart );
	if ( zRes == NULL ) 
	{
		Cudd_RecursiveDerefZdd( dd, zPart );
		return NULL;
	}
	cuddDeref( zPart );

    cuddCacheInsert1(dd, extraZddUniverse, VarSet, zRes);
	return zRes;

} /* end of extraZddUniverse */


/**Function********************************************************************

  Synopsis    [Performs the reordering-sensitive step of Extra_zddTuples().]

  Description [Generates in a bottom-up fashion ZDD for all combinations
               composed of k variables out of variables belonging to Support.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
DdNode* extraZddTuples( 
  DdManager * dd,   /* the DD manager */
  DdNode * zVarsK,   /* the number of variables in tuples */
  DdNode * zVarsN)   /* the set of all variables */
{
	DdNode *zRes, *zRes0, *zRes1;
    statLine(dd); 

	/* terminal cases */
/*	if ( k < 0 || k > n )
 *		return dd->zero;
 *	if ( n == 0 )
 *		return dd->one; 
 */
	if ( cuddIZ( dd, zVarsK->index ) < cuddIZ( dd, zVarsN->index ) )
		return z0;
	if ( zVarsN == z1 )
		return z1;

    /* check cache */
    zRes = cuddCacheLookup2Zdd(dd, extraZddTuples, zVarsK, zVarsN);
    if (zRes)
    	return(zRes);

	/* ZDD in which this variable is 0 */
/*	zRes0 = extraZddTuples( dd, k,     n-1 ); */
	zRes0 = extraZddTuples( dd, zVarsK, cuddT(zVarsN) );
	if ( zRes0 == NULL ) 
		return NULL;
	cuddRef( zRes0 );

	/* ZDD in which this variable is 1 */
/*	zRes1 = extraZddTuples( dd, k-1,          n-1 ); */
	if ( zVarsK == z1 )
	{
		zRes1 = z0;
		cuddRef( zRes1 );
	}
	else
	{
		zRes1 = extraZddTuples( dd, cuddT(zVarsK), cuddT(zVarsN) );
		if ( zRes1 == NULL ) 
		{
			Cudd_RecursiveDerefZdd( dd, zRes0 );
			return NULL;
		}
		cuddRef( zRes1 );
	}

	/* compose Res0 and Res1 with the given ZDD variable */
	zRes = cuddZddGetNode( dd, zVarsN->index, zRes1, zRes0 );
	if ( zRes == NULL ) 
	{
		Cudd_RecursiveDerefZdd( dd, zRes0 );
		Cudd_RecursiveDerefZdd( dd, zRes1 );
		return NULL;
	}
	cuddDeref( zRes0 );
	cuddDeref( zRes1 );

	/* insert the result into cache */
	cuddCacheInsert2(dd, extraZddTuples, zVarsK, zVarsN, zRes);
	return zRes;

} /* end of extraZddTuples */


/**Function********************************************************************

  Synopsis    [Performs the reordering-sensitive step of Extra_zddTupleFromBdd().]

  Description [Generates in a bottom-up fashion ZDD for all combinations
               composed of k variables out of variables belonging to Support.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
DdNode* extraZddTuplesFromBdd( 
  DdManager * dd,   /* the DD manager */
  DdNode * bVarsK,   /* the number of variables in tuples */
  DdNode * bVarsN)   /* the set of all variables */
{
	DdNode *zRes, *zRes0, *zRes1;
    statLine(dd); 

	/* terminal cases */
/*	if ( k < 0 || k > n )
 *		return dd->zero;
 *	if ( n == 0 )
 *		return dd->one; 
 */
	if ( cuddI( dd, bVarsK->index ) < cuddI( dd, bVarsN->index ) )
		return z0;
	if ( bVarsN == b1 )
		return z1;

    /* check cache */
    zRes = cuddCacheLookup2Zdd(dd, extraZddTuplesFromBdd, bVarsK, bVarsN);
    if (zRes)
    	return(zRes);

	/* ZDD in which this variable is 0 */
/*	zRes0 = extraZddTuplesFromBdd( dd, k,     n-1 ); */
	zRes0 = extraZddTuplesFromBdd( dd, bVarsK, cuddT(bVarsN) );
	if ( zRes0 == NULL ) 
		return NULL;
	cuddRef( zRes0 );

	/* ZDD in which this variable is 1 */
/*	zRes1 = extraZddTuplesFromBdd( dd, k-1,          n-1 ); */
	if ( bVarsK == b1 )
	{
		zRes1 = z0;
		cuddRef( zRes1 );
	}
	else
	{
		zRes1 = extraZddTuplesFromBdd( dd, cuddT(bVarsK), cuddT(bVarsN) );
		if ( zRes1 == NULL ) 
		{
			Cudd_RecursiveDerefZdd( dd, zRes0 );
			return NULL;
		}
		cuddRef( zRes1 );
	}

	/* compose Res0 and Res1 with the given ZDD variable */
	zRes = cuddZddGetNode( dd, 2*bVarsN->index, zRes1, zRes0 );
	if ( zRes == NULL ) 
	{
		Cudd_RecursiveDerefZdd( dd, zRes0 );
		Cudd_RecursiveDerefZdd( dd, zRes1 );
		return NULL;
	}
	cuddDeref( zRes0 );
	cuddDeref( zRes1 );

	/* insert the result into cache */
	cuddCacheInsert2(dd, extraZddTuplesFromBdd, bVarsK, bVarsN, zRes);
	return zRes;

} /* end of extraZddTuplesFromBdd */

/**Function********************************************************************

  Synopsis    [Performs the reordering-sensitive step of Extra_zddSinglesToComb().]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
DdNode * extraZddSinglesToComb(
  DdManager * dd,   /* the DD manager */
  DdNode * Singles) /* the set of singleton combinations */
{
	DdNode *zRes, *zPart;
    statLine(dd); 

	if ( Singles == dd->one )
	{
		printf("\nextraZddSinglesToComb(): Singles is not a ZDD!\n");
		return NULL;
	}
	if ( Singles == dd->zero )
		return dd->one;

    /* check cache */
    zRes = cuddCacheLookup1Zdd(dd, extraZddSinglesToComb, Singles);
    if (zRes)
		return(zRes);

	/* make sure that this is the set of singletons */
	if ( cuddT( Singles ) != dd->one )
	{
		printf("\nextraZddSinglesToComb(): Singles is not a set of singletons!\n");
		return NULL;
	}

	/* solve the problem recursively */
	zPart = extraZddSinglesToComb( dd, cuddE( Singles ) );
	if ( zPart == NULL )
		return NULL;
	cuddRef( zPart );

	/* create new node with this variable */
	/* compose Res0 and Res1 with the given ZDD variable */
	zRes = cuddZddGetNode( dd, Singles->index, zPart, dd->zero );
	if ( zRes == NULL ) 
	{
		Cudd_RecursiveDerefZdd( dd, zPart );
		return NULL;
	}
	cuddDeref( zPart );

    cuddCacheInsert1(dd, extraZddSinglesToComb, Singles, zRes);
	return zRes;

} /* end of extraZddSinglesToComb */


/**Function********************************************************************

  Synopsis    [Performs the reordering-sensitive step of Extra_zddMaximum().]

  Description [Generates in a bottom-up fashion ZDD for all combinations
  that have maximum cardinality in the cover.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
DdNode * extraZddMaximum(
  DdManager * dd,   /* the DD manager */
  DdNode * S,       /* the set of combinations */
  int * nVars)      /* the pointer where cardinality goes */ 
{
	DdNode *zRes;
	DdNode*(*cacheOp)(DdManager*,DdNode*);
    statLine(dd); 

	/* terminal cases */
	if ( S == dd->zero || S == dd->one )
	{
		*nVars = 0;
		return S;
	}

    /* check cache */
	cacheOp = (DdNode*(*)(DdManager*,DdNode*))extraZddMaximum;

    zRes = cuddCacheLookup1Zdd(dd, cacheOp, S);
    if (zRes)
	{
		*nVars = zddCountVars( dd, zRes );
		return(zRes);
	}
	else
	{
		DdNode *zSet0, *zSet1;
		int     Card0,  Card1;

		/* solve the else problem recursively */
		zSet0 = extraZddMaximum( dd, cuddE( S ), &Card0 );
		if ( zSet0 == NULL )
			return NULL;
		cuddRef( zSet0 );

		/* solve the then problem recursively */
		zSet1 = extraZddMaximum( dd, cuddT( S ), &Card1 );
		if ( zSet1 == NULL )
		{
			Cudd_RecursiveDerefZdd( dd, zSet0 );
			return NULL;
		}
		cuddRef( zSet1 );

		/* compare the solutions */
		if ( Card0 == Card1 + 1 ) 
		{  /* both sets are good */

			/* create new node with this variable */
			zRes = cuddZddGetNode( dd, S->index, zSet1, zSet0 );
			if ( zRes == NULL ) 
			{
				Cudd_RecursiveDerefZdd( dd, zSet0 );
				Cudd_RecursiveDerefZdd( dd, zSet1 );
				return NULL;
			}
			cuddDeref( zSet0 );
			cuddDeref( zSet1 );

			*nVars = Card0;
		}
		else if ( Card0 > Card1 + 1 )
		{  /* take only zSet0 */

			Cudd_RecursiveDerefZdd( dd, zSet1 );
			zRes = zSet0;
			cuddDeref( zRes );

			*nVars = Card0;
		}
		else /* if ( Card0 < Card1 + 1 ) */
		{  /* take only zSet1 */

			Cudd_RecursiveDerefZdd( dd, zSet0 );

			/* create new node with this variable and empty else child */
			zRes = cuddZddGetNode( dd, S->index, zSet1, dd->zero );
			if ( zRes == NULL ) 
			{
				Cudd_RecursiveDerefZdd( dd, zSet1 );
				return NULL;
			}
			cuddDeref( zSet1 );

			*nVars = Card1 + 1;
		}

		cuddCacheInsert1(dd, cacheOp, S, zRes);
		return zRes;
	}
} /* end of extraZddMaximum */


/**Function********************************************************************

  Synopsis    [Performs the reordering-sensitive step of Extra_zddMinimum().]

  Description [Generates in a bottom-up fashion ZDD for all combinations
  that have minimum cardinality in the cover.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
DdNode * extraZddMinimum(
  DdManager * dd,   /* the DD manager */
  DdNode * S,       /* the set of combinations */
  int * nVars)      /* the pointer where cardinality goes */ 
{
	DdNode *zRes;
	DdNode*(*cacheOp)(DdManager*,DdNode*);
    statLine(dd); 

	/* terminal cases */
	if ( S == dd->zero )
	{
		*nVars = s_LargeNum;
		return S;
	}
	if ( S == dd->one )
	{
		*nVars = 0;
		return S;
	}

    /* check cache */
	cacheOp = (DdNode*(*)(DdManager*,DdNode*))extraZddMinimum;

    zRes = cuddCacheLookup1Zdd(dd, cacheOp, S);
    if (zRes)
	{
		*nVars = zddCountVars( dd, zRes );
		return(zRes);
	}
	else
	{
		DdNode *zSet0, *zSet1;
		int     Card0,  Card1;

		/* solve the else problem recursively */
		zSet0 = extraZddMinimum( dd, cuddE( S ), &Card0 );
		if ( zSet0 == NULL )
			return NULL;
		cuddRef( zSet0 );

		/* solve the then problem recursively */
		zSet1 = extraZddMinimum( dd, cuddT( S ), &Card1 );
		if ( zSet1 == NULL )
		{
			Cudd_RecursiveDerefZdd( dd, zSet0 );
			return NULL;
		}
		cuddRef( zSet1 );

		/* compare the solutions */
		if ( Card0 == Card1 + 1 ) 
		{  /* both sets are good */

			/* create new node with this variable */
			zRes = cuddZddGetNode( dd, S->index, zSet1, zSet0 );
			if ( zRes == NULL ) 
			{
				Cudd_RecursiveDerefZdd( dd, zSet0 );
				Cudd_RecursiveDerefZdd( dd, zSet1 );
				return NULL;
			}
			cuddDeref( zSet0 );
			cuddDeref( zSet1 );

			*nVars = Card0;
		}
		else if ( Card0 < Card1 + 1 )
		{  /* take only zSet0 */

			Cudd_RecursiveDerefZdd( dd, zSet1 );
			zRes = zSet0;
			cuddDeref( zRes );

			*nVars = Card0;
		}
		else /* if ( Card0 > Card1 + 1 ) */
		{  /* take only zSet1 */

			Cudd_RecursiveDerefZdd( dd, zSet0 );

			/* create new node with this variable and empty else child */
			zRes = cuddZddGetNode( dd, S->index, zSet1, dd->zero );
			if ( zRes == NULL ) 
			{
				Cudd_RecursiveDerefZdd( dd, zSet1 );
				return NULL;
			}
			cuddDeref( zSet1 );

			*nVars = Card1 + 1;
		}

		cuddCacheInsert1(dd, cacheOp, S, zRes);
		return zRes;
	}
} /* end of extraZddMinimum */




/*---------------------------------------------------------------------------*/
/* Definition of static functions                                            */
/*---------------------------------------------------------------------------*/


/**Function********************************************************************

  Synopsis    [Returns the number of elements in a randomly selected combination.]

  Description [Returns the number of elements in a randomly selected combination.
               This number may be useful if the set contains combinations of 
			   the same cardinality.]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
static int 
zddCountVars( 
  DdManager *dd, /* the manager */
  DdNode* S)     /* the set */
{
	/* in a ZDD, positive edge never points to dd->zero */
	int Counter;
	assert( S != dd->zero );
	for ( Counter = 0; S != dd->one; Counter++, S = cuddT(S) );
	return Counter;
}