extrazddsubsup.c

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

			cuddDeref( zRes0 );
			cuddDeref( zRes1 );
		}
		else if ( TopLevelX == TopLevelY )
		{
			/* combs of X without var that are supersets of combs of Y without var */
			zRes0 = extraZddSupSet( dd, cuddE( X ), cuddE( Y ) );
			if ( zRes0 == NULL )  return NULL;
			cuddRef( zRes0 );

			/* merge combs of Y with and without var */
			zTemp = cuddZddUnion( dd, cuddE( Y ), cuddT( Y ) );
			if ( zTemp == NULL )  
			{
				Cudd_RecursiveDerefZdd( dd, zRes0 );
				return NULL;
			}
			cuddRef( zTemp );

			/* combs of X with label that are supersets of combs in Temp */
			zRes1 = extraZddSupSet( dd, cuddT( X ), zTemp );
			if ( zRes1 == NULL )  
			{
				Cudd_RecursiveDerefZdd( dd, zRes0 );
				Cudd_RecursiveDerefZdd( dd, zTemp );
				return NULL;
			}
			cuddRef( zRes1 );
			Cudd_RecursiveDerefZdd( dd, zTemp );

			/* compose Res0 and Res1 with the given ZDD variable */
			zRes = cuddZddGetNode( dd, X->index, zRes1, zRes0 );
			if ( zRes == NULL ) 
			{
				Cudd_RecursiveDerefZdd( dd, zRes0 );
				Cudd_RecursiveDerefZdd( dd, zRes1 );
				return NULL;
			}
			cuddDeref( zRes0 );
			cuddDeref( zRes1 );
		}
		else /* if ( TopLevelX > TopLevelY ) */
		{
			/* combs of X that are supersets of combs of Y without label */
			zRes = extraZddSupSet( dd, X, cuddE( Y ) );
			if ( zRes == NULL )  return NULL;
		}

		/* insert the result into cache */
	    cuddCacheInsert2(dd, extraZddSupSet, X, Y, zRes);
		return zRes;
	}
} /* end of extraZddSupSet */


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

  Synopsis [Performs the recursive step of Extra_zddNotSubSet.]

  Description []

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
DdNode* extraZddNotSubSet( DdManager *dd, DdNode *X, DdNode *Y )
{	
	DdNode *zRes;
    statLine(dd); 
	/* any comb is a subset of itself */
	if ( X == Y ) 
		return z0;
	/* combs in X are notsubsets of non-existant combs in Y */
	if ( Y == z0 ) 
		return X;	
	/* only {()} is the subset of {()} */
	if ( Y == z1 ) /* remove empty combination from X */
		return cuddZddDiff( dd, X, z1 );
	/* if X is empty, the result is empty */
	if ( X == z0 ) 
		return z0;
	/* the empty comb is contained in all combs of Y */
	if ( X == z1 ) 
		return z0;

    /* check cache */
    zRes = cuddCacheLookup2Zdd(dd, extraZddNotSubSet, X, Y);
    if (zRes)
    	return(zRes);
	else
	{
		DdNode *zRes0, *zRes1, *zTemp;
		int TopLevelX = dd->permZ[ X->index ];
		int TopLevelY = dd->permZ[ Y->index ];

		if ( TopLevelX < TopLevelY )
		{
			/* compute combs of X without var that are notsubsets of combs with Y */
			zRes0 = extraZddNotSubSet( dd, cuddE( X ), Y );
			if ( zRes0 == NULL )  
				return NULL;
			cuddRef( zRes0 );

			/* combs of X with var cannot be subsets of combs without var in Y */
			zRes1 = cuddT( X );

			/* compose Res0 and Res1 with the given ZDD variable */
			zRes = cuddZddGetNode( dd, X->index, zRes1, zRes0 );
			if ( zRes == NULL ) 
			{
				Cudd_RecursiveDerefZdd( dd, zRes0 );
				return NULL;
			}
			cuddDeref( zRes0 );
		}
		else if ( TopLevelX == TopLevelY )
		{
			/* merge combs of Y with and without var */
			zTemp = cuddZddUnion( dd, cuddE( Y ), cuddT( Y ) );
			if ( zTemp == NULL )  
				return NULL;
			cuddRef( zTemp );

			/* compute combs of X without var that are notsubsets of combs is Temp */
			zRes0 = extraZddNotSubSet( dd, cuddE( X ), zTemp );
			if ( zRes0 == NULL )  
			{
				Cudd_RecursiveDerefZdd( dd, zTemp );
				return NULL;
			}
			cuddRef( zRes0 );
			Cudd_RecursiveDerefZdd( dd, zTemp );

			/* combs of X with var that are notsubsets of combs in Y with var */
			zRes1 = extraZddNotSubSet( dd, cuddT( X ), cuddT( Y ) );
			if ( zRes1 == NULL )  
			{
				Cudd_RecursiveDerefZdd( dd, zRes0 );
				return NULL;
			}
			cuddRef( zRes1 );

			/* compose Res0 and Res1 with the given ZDD variable */
			zRes = cuddZddGetNode( dd, X->index, zRes1, zRes0 );
			if ( zRes == NULL ) 
			{
				Cudd_RecursiveDerefZdd( dd, zRes0 );
				Cudd_RecursiveDerefZdd( dd, zRes1 );
				return NULL;
			}
			cuddDeref( zRes0 );
			cuddDeref( zRes1 );
		}
		else /* if ( TopLevelX > TopLevelY ) */
		{
			/* merge combs of Y with and without var */
			zTemp = cuddZddUnion( dd, cuddE( Y ), cuddT( Y ) );
			if ( zTemp == NULL )  
				return NULL;
			cuddRef( zTemp );

			/* compute combs that are notsubsets of Temp */
			zRes = extraZddNotSubSet( dd, X, zTemp );
			if ( zRes == NULL ) 
			{
				Cudd_RecursiveDerefZdd( dd, zTemp );
				return NULL;
			}
			cuddRef( zRes );
			Cudd_RecursiveDerefZdd( dd, zTemp );
			cuddDeref( zRes );
		}

		/* insert the result into cache */
	    cuddCacheInsert2(dd, extraZddNotSubSet, X, Y, zRes);
		return zRes;
	}
} /* end of extraZddNotSubSet */


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

  Synopsis [Performs the recursive step of Extra_zddNotSupSet.]

  Description []

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
DdNode* extraZddNotSupSet( DdManager *dd, DdNode *X, DdNode *Y )
{	
	DdNode *zRes;
    statLine(dd); 
	/* any comb is a superset of itself */
	if ( X == Y ) 
		return z0;
	/* no comb in X is superset of non-existing combs */
	if ( Y == z0 ) 
		return X;	
	/* any comb in X is the superset of the empty comb */
	if ( Extra_zddEmptyBelongs( dd, Y ) ) 
		return z0;
	/* if X is empty, the result is empty */
	if ( X == z0 ) 
		return z0;
	/* if X is the empty comb (and Y does not contain it!), return it */
	if ( X == z1 ) 
		return z1;

    /* check cache */
    zRes = cuddCacheLookup2Zdd(dd, extraZddNotSupSet, X, Y);
    if (zRes)
    	return(zRes);
	else
	{
		DdNode *zRes0, *zRes1, *zTemp;
		int TopLevelX = dd->permZ[ X->index ];
		int TopLevelY = dd->permZ[ Y->index ];

		if ( TopLevelX < TopLevelY )
		{
			/* combinations of X without label that are supersets of combinations of Y */
			zRes0 = extraZddNotSupSet( dd, cuddE( X ), Y );
			if ( zRes0 == NULL )  
				return NULL;
			cuddRef( zRes0 );

			/* combinations of X with label that are supersets of combinations of Y */
			zRes1 = extraZddNotSupSet( dd, cuddT( X ), Y );
			if ( zRes1 == NULL )  
			{
				Cudd_RecursiveDerefZdd( dd, zRes0 );
				return NULL;
			}
			cuddRef( zRes1 );

			/* compose Res0 and Res1 with the given ZDD variable */
			zRes = cuddZddGetNode( dd, X->index, zRes1, zRes0 );
			if ( zRes == NULL )
			{
				Cudd_RecursiveDerefZdd( dd, zRes0 );
				Cudd_RecursiveDerefZdd( dd, zRes1 );
				return NULL;
			}
			cuddDeref( zRes0 );
			cuddDeref( zRes1 );
		}
		else if ( TopLevelX == TopLevelY )
		{
			/* combs of X without var that are not supersets of combs of Y without var */
			zRes0 = extraZddNotSupSet( dd, cuddE( X ), cuddE( Y ) );
			if ( zRes0 == NULL )  
				return NULL;
			cuddRef( zRes0 );

			/* merge combs of Y with and without var */
			zTemp = cuddZddUnion( dd, cuddE( Y ), cuddT( Y ) );
			if ( zTemp == NULL )
			{
				Cudd_RecursiveDerefZdd( dd, zRes0 );
				return NULL;
			}
			cuddRef( zTemp );

			/* combs of X with label that are supersets of combs in Temp */
			zRes1 = extraZddNotSupSet( dd, cuddT( X ), zTemp );
			if ( zRes1 == NULL )
			{
				Cudd_RecursiveDerefZdd( dd, zRes0 );
				Cudd_RecursiveDerefZdd( dd, zTemp );
				return NULL;
			}
			cuddRef( zRes1 );
			Cudd_RecursiveDerefZdd( dd, zTemp );

			/* compose Res0 and Res1 with the given ZDD variable */
			zRes = cuddZddGetNode( dd, X->index, zRes1, zRes0 );
			if ( zRes == NULL ) 
			{
				Cudd_RecursiveDerefZdd( dd, zRes0 );
				Cudd_RecursiveDerefZdd( dd, zRes1 );
				return NULL;
			}
			cuddDeref( zRes0 );
			cuddDeref( zRes1 );
		}
		else /* if ( TopLevelX > TopLevelY ) */
		{
			/* combs of X that are supersets of combs of Y without label */
			zRes = extraZddNotSupSet( dd, X, cuddE( Y ) );
			if ( zRes == NULL )  return NULL;
		}

		/* insert the result into cache */
	    cuddCacheInsert2(dd, extraZddNotSupSet, X, Y, zRes);
		return zRes;
	}
} /* end of extraZddNotSupSet */



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

  Synopsis [Performs the recursive step of Extra_zddMaxNotSupSet.]

  Description []

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
DdNode* extraZddMaxNotSupSet( DdManager *dd, DdNode *X, DdNode *Y )
{	
	DdNode *zRes;
    statLine(dd); 
	/* any comb is a superset of itself */
	if ( X == Y ) 
		return z0;
	/* no comb in X is superset of non-existing combs */
	if ( Y == z0 ) 
		return extraZddMaximal( dd, X );	
	/* any comb in X is the superset of the empty comb */
	if ( Extra_zddEmptyBelongs( dd, Y ) ) 
		return z0;
	/* if X is empty, the result is empty */
	if ( X == z0 ) 
		return z0;
	/* if X is the empty comb (and Y does not contain it!), return it */
	if ( X == z1 ) 
		return z1;

    /* check cache */
    zRes = cuddCacheLookup2Zdd(dd, extraZddMaxNotSupSet, X, Y);
    if (zRes)
    	return(zRes);
	else
	{
		DdNode *zRes0, *zRes1, *zTemp;
		int TopLevelX = dd->permZ[ X->index ];
		int TopLevelY = dd->permZ[ Y->index ];

		if ( TopLevelX < TopLevelY )
		{
			/* combinations of X without label that are supersets of combinations with Y */
			zRes0 = extraZddMaxNotSupSet( dd, cuddE( X ), Y );
			if ( zRes0 == NULL )  
				return NULL;
			cuddRef( zRes0 );

			/* combinations of X with label that are supersets of combinations with Y */
			zRes1 = extraZddMaxNotSupSet( dd, cuddT( X ), Y );
			if ( zRes1 == NULL )  
			{
				Cudd_RecursiveDerefZdd( dd, zRes0 );
				return NULL;
			}
			cuddRef( zRes1 );

			/* ---------------------------------------------------- */
			/* remove subsets without this element covered by subsets with this element */
			zRes0 = extraZddNotSubSet(dd, zTemp = zRes0, zRes1);
			if ( zRes0 == NULL )
			{
				Cudd_RecursiveDerefZdd(dd, zTemp);
				Cudd_RecursiveDerefZdd(dd, zRes1);
				return NULL;
			}
			cuddRef( zRes0 );
			Cudd_RecursiveDerefZdd(dd, zTemp);
			/* ---------------------------------------------------- */

			/* compose Res0 and Res1 with the given ZDD variable */
			zRes = cuddZddGetNode( dd, X->index, zRes1, zRes0 );
			if ( zRes == NULL )
			{
				Cudd_RecursiveDerefZdd( dd, zRes0 );
				Cudd_RecursiveDerefZdd( dd, zRes1 );
				return NULL;
			}
			cuddDeref( zRes0 );
			cuddDeref( zRes1 );
		}
		else if ( TopLevelX == TopLevelY )
		{
			/* combs of X without var that are supersets of combs of Y without var */
			zRes0 = extraZddMaxNotSupSet( dd, cuddE( X ), cuddE( Y ) );
			if ( zRes0 == NULL )  
				return NULL;
			cuddRef( zRes0 );

			/* merge combs of Y with and without var */
			zTemp = cuddZddUnion( dd, cuddE( Y ), cuddT( Y ) );
			if ( zTemp == NULL )
			{
				Cudd_RecursiveDerefZdd( dd, zRes0 );
				return NULL;
			}
			cuddRef( zTemp );

			/* combs of X with label that are supersets of combs in Temp */
			zRes1 = extraZddMaxNotSupSet( dd, cuddT( X ), zTemp );
			if ( zRes1 == NULL )
			{
				Cudd_RecursiveDerefZdd( dd, zRes0 );
				Cudd_RecursiveDerefZdd( dd, zTemp );
				return NULL;
			}
			cuddRef( zRes1 );
			Cudd_RecursiveDerefZdd( dd, zTemp );

			/* ---------------------------------------------------- */
			/* remove subsets without this element covered by subsets with this element */
			zRes0 = extraZddNotSubSet(dd, zTemp = zRes0, zRes1);
			if ( zRes0 == NULL )
			{
				Cudd_RecursiveDerefZdd(dd, zTemp);
				Cudd_RecursiveDerefZdd(dd, zRes1);
				return NULL;
			}
			cuddRef( zRes0 );
			Cudd_RecursiveDerefZdd(dd, zTemp);
			/* ---------------------------------------------------- */

			/* compose Res0 and Res1 with the given ZDD variable */
			zRes = cuddZddGetNode( dd, X->index, zRes1, zRes0 );
			if ( zRes == NULL ) 
			{
				Cudd_RecursiveDerefZdd( dd, zRes0 );
				Cudd_RecursiveDerefZdd( dd, zRes1 );
				return NULL;
			}
			cuddDeref( zRes0 );
			cuddDeref( zRes1 );
		}
		else /* if ( TopLevelX > TopLevelY ) */
		{
			/* combs of X that are supersets of combs of Y without label */
			zRes = extraZddMaxNotSupSet( dd, X, cuddE( Y ) );
			if ( zRes == NULL )  return NULL;
		}

		/* insert the result into cache */
	    cuddCacheInsert2(dd, extraZddMaxNotSupSet, X, Y, zRes);
		return zRes;
	}
} /* end of extraZddMaxNotSupSet */


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