extrazddcovers.c

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

  positive and negative polarities are adjacent in the variable order. Is different 
  from cuddZddGetCofactors3() in that it does not compute the cofactors w.r.t. the 
  given variable but takes the cofactors with respent to the topmost variable. 
  This function is more efficient when used in recursive procedures because it does 
  not require referencing of the resulting cofactors (compare cuddZddProduct() 
  and extraZddPrimeProduct()).]

  SideEffects [None]

  SeeAlso     [cuddZddGetCofactors3]

******************************************************************************/
void 
extraDecomposeCover( 
  DdManager* dd,    /* the manager */
  DdNode*  zC,      /* the cover */
  DdNode** zC0,     /* the pointer to the negative var cofactor */ 
  DdNode** zC1,     /* the pointer to the positive var cofactor */ 
  DdNode** zC2 )    /* the pointer to the cofactor without var */ 
{
	if ( (zC->index & 1) == 0 ) 
	{ /* the top variable is present in positive polarity and maybe in negative */

		DdNode *Temp = cuddE( zC );
		*zC1  = cuddT( zC );
		if ( cuddIZ(dd,Temp->index) == cuddIZ(dd,zC->index) + 1 )
		{	/* Temp is not a terminal node 
			 * top var is present in negative polarity */
			*zC2 = cuddE( Temp );
			*zC0 = cuddT( Temp );
		}
		else
		{	/* top var is not present in negative polarity */
			*zC2 = Temp;
			*zC0 = dd->zero;
		}
	}
	else 
	{ /* the top variable is present only in negative */
		*zC1 = dd->zero;
		*zC2 = cuddE( zC );
		*zC0 = cuddT( zC );
	}
} /* extraDecomposeCover */


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

  Synopsis    [Composed three subcovers into one ZDD.]

  Description []

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
DdNode *
extraComposeCover( 
  DdManager* dd,    /* the manager */
  DdNode* zC0,     /* the pointer to the negative var cofactor */ 
  DdNode* zC1,     /* the pointer to the positive var cofactor */ 
  DdNode* zC2,     /* the pointer to the cofactor without var */ 
  int TopVar)    /* the index of the positive ZDD var */
{
	DdNode * zRes, * zTemp;
	/* compose with-neg-var and without-var using the neg ZDD var */
	zTemp = cuddZddGetNode( dd, 2*TopVar + 1, zC0, zC2 );
	if ( zTemp == NULL ) 
	{
		Cudd_RecursiveDerefZdd(dd, zC0);
		Cudd_RecursiveDerefZdd(dd, zC1);
		Cudd_RecursiveDerefZdd(dd, zC2);
		return NULL;
	}
	cuddRef( zTemp );
	cuddDeref( zC0 );
	cuddDeref( zC2 );

	/* compose with-pos-var and previous result using the pos ZDD var */
	zRes = cuddZddGetNode( dd, 2*TopVar, zC1, zTemp );
	if ( zRes == NULL ) 
	{
		Cudd_RecursiveDerefZdd(dd, zC1);
		Cudd_RecursiveDerefZdd(dd, zTemp);
		return NULL;
	}
	cuddDeref( zC1 );
	cuddDeref( zTemp );
	return zRes;
} /* extraComposeCover */


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

  Synopsis [Performs the recursive step of Extra_zddPrimeProduct.]

  Description []

  SideEffects [None]

  SeeAlso     [Extra_zddProduct]

******************************************************************************/
DdNode	*
extraZddPrimeProduct(
  DdManager * dd,
  DdNode * f,
  DdNode * g)
{
    DdNode	*zRes;
    int		LevelF, LevelG;
    statLine(dd); 

    /* terminal cases */
    if (f == dd->zero || g == dd->zero)
        return dd->zero;
    if (f == dd->one)
        return g;
    if (g == dd->one)
        return f;
    if (f == g)
        return f;

	/* level in terms of original variables, not ZDD variables */
    LevelF = dd->permZ[f->index] >> 1;
    LevelG = dd->permZ[g->index] >> 1;

    /* normalize */
    if (LevelF > LevelG)
		return extraZddPrimeProduct(dd, g, f);

    /* check cache */
    zRes = cuddCacheLookup2Zdd(dd, extraZddPrimeProduct, f, g);
    if (zRes)
		return zRes;
	else
	{
		DdNode *zRes0, *zRes1, *zRes2, *zTemp;
		int TopZddVar;

		if ( LevelF < LevelG )
		{
			DdNode *zF0, *zF1, *zF2;
			extraDecomposeCover(dd, f, &zF0, &zF1, &zF2);

			/* (zF0 + zF1 + zF2) * g = // the expanded product
			 *
			 *  zF0 * g +              // cofactors with negative var
			 *  zF1 * g +              // cofactors with positive var
			 *  zF2 * g =              // cofactors without var
			 */
			
			/* ------  cofactor with negative variable ------ */
			/* compute (zF0 * g) */
			zRes0 = extraZddPrimeProduct( dd, zF0, g );
			if ( zRes0 == NULL )
				return NULL;
			cuddRef( zRes0 );

			/* ------- cofactor with positive variable ------ */
			/* compute (zF1 * g) */
			zRes1 = extraZddPrimeProduct( dd, zF1, g );
			if ( zRes1 == NULL )
			{
				Cudd_RecursiveDerefZdd( dd, zRes0 );
				return NULL;
			}
			cuddRef( zRes1 );

			/* --------- cofactor without variable ------------ */
			/* compute (zF2 + g) */
			zRes2 = extraZddPrimeProduct( dd, zF2, g );
			if ( zRes2 == NULL )
			{
				Cudd_RecursiveDerefZdd( dd, zRes0 );
				Cudd_RecursiveDerefZdd( dd, zRes1 );
				return NULL;
			}
			cuddRef( zRes2 );
			/* at this point, only zRes0, zRes2, and zRes2 are referenced */
		}
		else /* if ( LevelF == LevelG ) */
		{
			DdNode *zF0, *zF1, *zF2;
			DdNode *zG0, *zG1, *zG2, *zG20, *zG21;
			DdNode *zTerm1, *zTerm2;

			extraDecomposeCover(dd, f, &zF0, &zF1, &zF2);
			extraDecomposeCover(dd, g, &zG0, &zG1, &zG2);

			/* (zF0 + zF1 + zF2) * (zG0 + zG1 + zG2) = // the expanded product
			 *
			 * (zF2 * zG0 + zF0 * zG2 + zF0 * zG0) +   // cofactors with negative var
			 * (zF2 * zG1 + zF1 * zG2 + zF1 * zG1) +   // cofactors with positive var
			 *  zF2 * zG2 =                            // cofactors without var
			 *
			 * (zF2 * zG0 + zF0 * (zG2 + zG0)) +       // cofactors with negative var
			 * (zF2 * zG1 + zF1 * (zG2 + zG1)) +       // cofactors with positive var
			 *  zF2 * zG2                              // cofactors without var
			 */

			/* ------  cofactors with negative variable ------ */
			/* compute (zG2 + zG0) */
			zG20 = extraZddMinUnion( dd, zG2, zG0 );
			if ( zG20 == NULL )
				return NULL;
			cuddRef( zG20 );

			/* compute zF0 * (zG2 + zG0) */
			zTerm1 = extraZddPrimeProduct( dd, zF0, zG20 );
			if ( zTerm1 == NULL )
			{
				Cudd_RecursiveDerefZdd( dd, zG20 );
				return NULL;
			}
			cuddRef( zTerm1 );
			Cudd_RecursiveDerefZdd( dd, zG20 );

			/* compute (zF2 * zG0) */
			zTerm2 = extraZddPrimeProduct( dd, zF2, zG0 );
			if ( zTerm2 == NULL )
			{
				Cudd_RecursiveDerefZdd( dd, zTerm1 );
				return NULL;
			}
			cuddRef( zTerm2 );

			/* compute the sum of these two parts */
			zRes0 = extraZddMinUnion( dd, zTerm1, zTerm2 );
			if ( zRes0 == NULL )
			{
				Cudd_RecursiveDerefZdd( dd, zTerm1 );
				Cudd_RecursiveDerefZdd( dd, zTerm2 );
				return NULL;
			}
			cuddRef( zRes0 );
			Cudd_RecursiveDerefZdd( dd, zTerm1 );
			Cudd_RecursiveDerefZdd( dd, zTerm2 );


			/* ------- cofactors with positive variable ------ */
			/* compute (zG2 + zG1) */
			zG21 = extraZddMinUnion( dd, zG2, zG1 );
			if ( zG21 == NULL )
			{
				Cudd_RecursiveDerefZdd( dd, zRes0 );
				return NULL;
			}
			cuddRef( zG21 );

			/* compute zF0 * (zG2 + zG0) */
			zTerm1 = extraZddPrimeProduct( dd, zF1, zG21 );
			if ( zTerm1 == NULL )
			{
				Cudd_RecursiveDerefZdd( dd, zRes0 );
				Cudd_RecursiveDerefZdd( dd, zG21 );
				return NULL;
			}
			cuddRef( zTerm1 );
			Cudd_RecursiveDerefZdd( dd, zG21 );

			/* compute (zF2 * zG0) */
			zTerm2 = extraZddPrimeProduct( dd, zF2, zG1 );
			if ( zTerm2 == NULL )
			{
				Cudd_RecursiveDerefZdd( dd, zRes0 );
				Cudd_RecursiveDerefZdd( dd, zTerm1 );
				return NULL;
			}
			cuddRef( zTerm2 );

			/* compute the sum of these two parts */
			zRes1 = extraZddMinUnion( dd, zTerm1, zTerm2 );
			if ( zRes1 == NULL )
			{
				Cudd_RecursiveDerefZdd( dd, zRes0 );
				Cudd_RecursiveDerefZdd( dd, zTerm1 );
				Cudd_RecursiveDerefZdd( dd, zTerm2 );
				return NULL;
			}
			cuddRef( zRes1 );
			Cudd_RecursiveDerefZdd( dd, zTerm1 );
			Cudd_RecursiveDerefZdd( dd, zTerm2 );

			/* --------- cofactor without variable ------------ */
			/* compute (zF2 + zG2) */
			zRes2 = extraZddPrimeProduct( dd, zF2, zG2 );
			if ( zRes2 == NULL )
			{
				Cudd_RecursiveDerefZdd( dd, zRes0 );
				Cudd_RecursiveDerefZdd( dd, zRes1 );
				return NULL;
			}
			cuddRef( zRes2 );
			/* at this point, only zRes0, zRes2, and zRes2 are referenced */
		}

		/* ---- filtering cofactors with/without variable --- */
		/* remove negative var cubes contained in cubes without var */
		zRes0 = extraZddNotSupSet(dd, zTemp = zRes0, zRes2);
		if ( zRes0 == NULL )
		{
			Cudd_RecursiveDerefZdd(dd, zTemp);
			Cudd_RecursiveDerefZdd(dd, zRes1);
			Cudd_RecursiveDerefZdd(dd, zRes2);
			return NULL;
		}
		cuddRef( zRes0 );
		Cudd_RecursiveDerefZdd(dd, zTemp);

		/* remove positive var cubes contained in cubes without var */
		zRes1 = extraZddNotSupSet(dd, zTemp = zRes1, zRes2);
		if ( zRes1 == NULL )
		{
			Cudd_RecursiveDerefZdd(dd, zRes0);
			Cudd_RecursiveDerefZdd(dd, zTemp);
			Cudd_RecursiveDerefZdd(dd, zRes2);
			return NULL;
		}
		cuddRef( zRes1 );
		Cudd_RecursiveDerefZdd(dd, zTemp);

		/* --------------- composing the result ------------------ */
		/* the index of the positive ZDD variable in F */
		TopZddVar = (f->index >> 1) << 1;

		/* compose with-neg-var and without-var using the neg ZDD var */
		zTemp = cuddZddGetNode(dd, TopZddVar + 1, zRes0, zRes2 );
		if ( zTemp == NULL ) 
		{
			Cudd_RecursiveDerefZdd(dd, zRes0);
			Cudd_RecursiveDerefZdd(dd, zRes1);
			Cudd_RecursiveDerefZdd(dd, zRes2);
			return NULL;
		}
		cuddRef( zTemp );
		cuddDeref( zRes0 );
		cuddDeref( zRes2 );

		/* compose with-pos-var and previous result using the pos ZDD var */
		zRes = cuddZddGetNode(dd, TopZddVar, zRes1, zTemp );
		if ( zRes == NULL ) 
		{
			Cudd_RecursiveDerefZdd(dd, zRes1);
			Cudd_RecursiveDerefZdd(dd, zTemp);
			return NULL;
		}
		cuddDeref( zRes1 );
		cuddDeref( zTemp );

		/* insert the result into cache */
		cuddCacheInsert2(dd, extraZddPrimeProduct, f, g, zRes);
		return zRes;
	}
} /* end of extraZddPrimeProduct */


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

  Synopsis [Performs the recursive step of Extra_zddProductAlt.]

  Description [Alternative implementation of Extra_zddProduct]

  SideEffects [None]

  SeeAlso     [Extra_zddProduct]

******************************************************************************/
DdNode	*
extraZddProductAlt(
  DdManager * dd,
  DdNode * f,
  DdNode * g)
{
    DdNode	*zRes;
    int		LevelF, LevelG;
    statLine(dd); 

    /* terminal cases */
    if (f == dd->zero || g == dd->zero)
        return dd->zero;
    if (f == dd->one)
        return g;
    if (g == dd->one)
        return f;
    if (f == g)
        return f;

	/* level in terms of original variables, not ZDD variables */
    LevelF = dd->permZ[f->index] >> 1;
    LevelG = dd->permZ[g->index] >> 1;

    /* normalize */
    if (LevelF > LevelG)
		return extraZddProductAlt(dd, g, f);

    /* check cache */
    zRes = cuddCacheLookup2Zdd(dd, extraZddProductAlt, f, g);
    if (zRes)
		return zRes;
	else
	{
		DdNode *zRes0, *zRes1, *zRes2, *zTemp;
		int TopZddVar;

		if ( LevelF < LevelG )
		{
			DdNode *zF0, *zF1, *zF2;
			extraDecomposeCover(dd, f, &zF0, &zF1, &zF2);

			/* (zF0 + zF1 + zF2) * g = // the expanded product
			 *
			 *  zF0 * g +              // cofactors with negative var
			 *  zF1 * g +              // cofactors with positive var
			 *  zF2 * g =              // cofactors without var
			 */
			
			/* ------  cofactor with negative variable ------ */
			/* compute (zF0 * g) */
			zRes0 = extraZddProductAlt( dd, zF0, g );
			if ( zRes0 == NULL )
				return NULL;
			cuddRef( zRes0 );

			/* ------- cofactor with positive variable ------ */
			/* compute (zF1 * g) */
			zRes1 = extraZddProductAlt( dd, zF1, g );
			if ( zRes1 == NULL )
			{
				Cudd_RecursiveDerefZdd( dd, zRes0 );
				return NULL;
			}
			cuddRef( zRes1 );

			/* --------- cofactor without variable ------------ */
			/* compute (zF2 + g) */
			zRes2 = extraZddProductAlt( dd, zF2, g );
			if ( zRes2 == NULL )
			{
				Cudd_RecursiveDerefZdd( dd, zRes0 );
				Cudd_RecursiveDerefZdd( dd, zRes1 );
				return NULL;
			}
			cuddRef( zRes2 );
			/* at this point, only zRes0, zRes2, and zRes2 are referenced */
		}
		else /* if ( LevelF == LevelG ) */
		{
			DdNode *zF0, *zF1, *zF2;
			DdNode *zG0, *zG1, *zG2, *zG20, *zG21;
			DdNode *zTerm1, *zTerm2;

			extraDecomposeCover(dd, f, &zF0, &zF1, &zF2);
			extraDecomposeCover(dd, g, &zG0, &zG1, &zG2);

			/* (zF0 + zF1 + zF2) * (zG0 + zG1 + zG2) = // the expanded product
			 *
			 * (zF2 * zG0 + zF0 * zG2 + zF0 * zG0) +   // cofactors with negative var
			 * (zF2 * zG1 + zF1 * zG2 + zF1 * zG1) +   // cofactors with positive var
			 *  zF2 * zG2 =                            // cofactors without var
			 *
			 * (zF2 * zG0 + zF0 * (zG2 + zG0)) +       // cofactors with negative var
			 * (zF2 * zG1 + zF1 * (zG2 + zG1)) +       // cofactors with positive var
			 *  zF2 * zG2                              // cofactors without var
			 */

			/* ------  cofactors with negative variable ------ */
			/* compute (zG2 + zG0) */
			zG20 = cuddZddUnion( dd, zG2, zG0 );
			if ( zG20 == NULL )
				return NULL;
			cuddRef( zG20 );

			/* compute zF0 * (zG2 + zG0) */
			zTerm1 = extraZddProductAlt( dd, zF0, zG20 );
			if ( zTerm1 == NULL )
			{
				Cudd_RecursiveDerefZdd( dd, zG20 );
				return NULL;
			}
			cuddRef( zTerm1 );
			Cudd_RecursiveDerefZdd( dd, zG20 );

			/* compute (zF2 * zG0) */
			zTerm2 = extraZddProductAlt( dd, zF2, zG0 );
			if ( zTerm2 == NULL )
			{
				Cudd_RecursiveDerefZdd( dd, zTerm1 );
				return NULL;
			}
			cuddRef( zTerm2 );

			/* compute the sum of these two parts */
			zRes0 = cuddZddUnion( dd, zTerm1, zTerm2 );
			if ( zRes0 == NULL )
			{
				Cudd_RecursiveDerefZdd( dd, zTerm1 );
				Cudd_RecursiveDerefZdd( dd, zTerm2 );
				return NULL;
			}
			cuddRef( zRes0 );
			Cudd_RecursiveDerefZdd( dd, zTerm1 );
			Cudd_RecursiveDerefZdd( dd, zTerm2 );


			/* ------- cofactors with positive variable ------ */
			/* compute (zG2 + zG1) */
			zG21 = cuddZddUnion( dd, zG2, zG1 );
			if ( zG21 == NULL )
			{
				Cudd_RecursiveDerefZdd( dd, zRes0 );
				return NULL;
			}
			cuddRef( zG21 );

			/* compute zF0 * (zG2 + zG0) */
			zTerm1 = extraZddProductAlt( dd, zF1, zG21 );
			if ( zTerm1 == NULL )
			{
				Cudd_RecursiveDerefZdd( dd, zRes0 );
				Cudd_RecursiveDerefZdd( dd, zG21 );
				return NULL;
			}
			cuddRef( zTerm1 );
			Cudd_RecursiveDerefZdd( dd, zG21 );

			/* compute (zF2 * zG0) */
			zTerm2 = extraZddProductAlt( dd, zF2, zG1 );
			if ( zTerm2 == NULL )
			{
				Cudd_RecursiveDerefZdd( dd, zRes0 );
				Cudd_RecursiveDerefZdd( dd, zTerm1 );
				return NULL;
			}
			cuddRef( zTerm2 );

			/* compute the sum of these two parts */
			zRes1 = cuddZddUnion( dd, zTerm1, zTerm2 );
			if ( zRes1 == NULL )
			{
				Cudd_RecursiveDerefZdd( dd, zRes0 );
				Cudd_RecursiveDerefZdd( dd, zTerm1 );
				Cudd_RecursiveDerefZdd( dd, zTerm2 );
				return NULL;
			}
			cuddRef( zRes1 );
			Cudd_RecursiveDerefZdd( dd, zTerm1 );
			Cudd_RecursiveDerefZdd( dd, zTerm2 );

			/* --------- cofactor without variable ------------ */
			/* compute (zF2 + zG2) */
			zRes2 = extraZddProductAlt( dd, zF2, zG2 );
			if ( zRes2 == NULL )
			{
				Cudd_RecursiveDerefZdd( dd, zRes0 );
				Cudd_RecursiveDerefZdd( dd, zRes1 );
				return NULL;
			}
			cuddRef( zRes2 );
			/* at this point, only zRes0, zRes2, and zRes2 are referenced */
		}