extraddutils.c

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

				Cudd_RecursiveDeref(dd,bRes1);
				return NULL;
			}
		}
		cuddDeref( bRes0 );
		cuddDeref( bRes1 );

		/* insert the result into cache */
		cuddCacheInsert1(dd, extraZddConvertToBddUnate, zC, bRes);
		return bRes;
	}
} /* end of extraZddConvertToBddUnate */



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

  Synopsis [Performs the recursive step of Cudd_zddConvertEsopToBdd.]

  Description []

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
DdNode	*
extraZddConvertEsopToBdd(
  DdManager * dd,
  DdNode * zC)
{
    DdNode	*bRes;
    statLine(dd); 

	/* if there is no cover, there is no BDD */
	if ( zC == z0 )  return b0;
	/* if the cover is the universe, the BDD is constant 1 */
	if ( zC == z1 )  return b1;

    /* check cache */
    bRes = cuddCacheLookup1(dd, extraZddConvertEsopToBdd, zC);
    if (bRes)
		return(bRes);
	else
	{
		DdNode * bRes0, * bRes1, * bRes2, * bTemp;
		DdNode * zC0, * zC1, * zC2;
		int TopBddVar = (zC->index >> 1);

		/* cofactor the cover */
		extraDecomposeCover(dd, zC, &zC0, &zC1, &zC2);

		/* compute bdds for the three cofactors of the cover */
		bRes0 = extraZddConvertEsopToBdd(dd, zC0);
		if ( bRes0 == NULL )
			return NULL;
		cuddRef( bRes0 );

		bRes1 = extraZddConvertEsopToBdd(dd, zC1);
		if ( bRes1 == NULL )
		{
			Cudd_RecursiveDeref(dd, bRes0);
			return NULL;
		}
		cuddRef( bRes1 );

		bRes2 = extraZddConvertEsopToBdd(dd, zC2);
		if ( bRes2 == NULL )
		{
			Cudd_RecursiveDeref(dd, bRes0);
			Cudd_RecursiveDeref(dd, bRes1);
			return NULL;
		}
		cuddRef( bRes2 );

		/* compute  bdd(zC0) (+) bdd(zC2) */
		bRes0 = cuddBddXorRecur(dd, bTemp = bRes0, bRes2);
		if ( bRes0 == NULL )
		{
			Cudd_RecursiveDeref(dd, bTemp);
			Cudd_RecursiveDeref(dd, bRes1);
			Cudd_RecursiveDeref(dd, bRes2);
			return NULL;
		}
		cuddRef( bRes0 );
		Cudd_RecursiveDeref(dd, bTemp);

		/* compute  bdd(zC1) (+) bdd(zC2) */
		bRes1 = cuddBddXorRecur(dd, bTemp = bRes1, bRes2);
		if ( bRes1 == NULL )
		{
			Cudd_RecursiveDeref(dd, bRes0);
			Cudd_RecursiveDeref(dd, bTemp);
			Cudd_RecursiveDeref(dd, bRes2);
			return NULL;
		}
		cuddRef( bRes1 );
		Cudd_RecursiveDeref(dd, bTemp);
		Cudd_RecursiveDeref(dd, bRes2);
		/* only bRes0 and bRes1 are referenced at this point */

		/* consider the case when Res0 and Res1 are the same node */
		if ( bRes0 == bRes1 )
			bRes = bRes1;
		/* consider the case when Res1 is complemented */
		else if ( Cudd_IsComplement(bRes1) ) 
		{
			bRes = cuddUniqueInter(dd, TopBddVar, Cudd_Not(bRes1), Cudd_Not(bRes0));
			if ( bRes == NULL ) 
			{
				Cudd_RecursiveDeref(dd,bRes0);
				Cudd_RecursiveDeref(dd,bRes1);
				return NULL;
			}
			bRes = Cudd_Not(bRes);
		} 
		else 
		{
			bRes = cuddUniqueInter( dd, TopBddVar, bRes1, bRes0 );
			if ( bRes == NULL ) 
			{
				Cudd_RecursiveDeref(dd,bRes0);
				Cudd_RecursiveDeref(dd,bRes1);
				return NULL;
			}
		}
		cuddDeref( bRes0 );
		cuddDeref( bRes1 );

		/* insert the result into cache */
		cuddCacheInsert1(dd, extraZddConvertEsopToBdd, zC, bRes);
		return bRes;
	}
} /* end of extraZddConvertEsopToBdd */



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

  Synopsis [Performs the recursive step of Cudd_zddConvertToBddAndAdd.]

  Description []

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
DdNode	*
extraZddConvertToBddAndAdd(
  DdManager * dd,
  DdNode * zC,     /* the cover */
  DdNode * bA)     /* the area */
{
    DdNode	*bRes;
    statLine(dd); 

	/* if there is no cover, return the BDD */
	if ( zC == z0 )  return bA;
	/* if the cover is the universe, the sum is constant 1 */
	if ( zC == z1 )  return b1;
	/* if the area is absent, convert cover to BDD */
	if ( bA == b0 )  return extraZddConvertToBdd(dd,zC);
	/* if the area is constant 1, the BDD is also constant 1 */
	if ( bA == b1 )  return b1;

    /* check cache */
    bRes = cuddCacheLookup2(dd, extraZddConvertToBddAndAdd, zC, bA);
    if (bRes)
		return(bRes);
	else
	{
		DdNode * bRes0, * bRes1, * bRes2;
		DdNode * bA0, * bA1, * bTemp;
		int TopBddVar;
		/* find the level in terms of the original variable levels, not ZDD variable levels */
		int levCover = dd->permZ[zC->index] >> 1;
		int levArea  = dd->perm[Cudd_Regular(bA)->index];
		/* determine whether the area is a complemented BDD */
		int fIsComp  = Cudd_IsComplement(bA);

		if ( levCover > levArea )
		{
			TopBddVar = Cudd_Regular(bA)->index;

			/* find the parts(cofactors) of the area */
			bA0 = Cudd_NotCond( Cudd_E(bA), fIsComp );
			bA1 = Cudd_NotCond( Cudd_T(bA), fIsComp );

			/* solve for the Else part */
			bRes0 = extraZddConvertToBddAndAdd( dd, zC, bA0 );
			if ( bRes0 == NULL ) return NULL;
			cuddRef( bRes0 );

			/* solve for the Then part */
			bRes1 = extraZddConvertToBddAndAdd( dd, zC, bA1 );
			if ( bRes1 == NULL ) 
			{
				Cudd_RecursiveDeref( dd, bRes0 );
				return NULL;
			}
			cuddRef( bRes1 );
			/* only bRes0 and bRes1 are referenced at this point */
		}
		else /* if ( levCover <= levArea ) */
		{
			/* decompose the cover */
			DdNode *zC0, *zC1, *zC2;
			extraDecomposeCover(dd, zC, &zC0, &zC1, &zC2);

			/* assign the top-most BDD variable */
			TopBddVar = (zC->index >> 1);

			/* find the parts(cofactors) of the area */
			if ( levCover == levArea )
			{ /* find the parts(cofactors) of the area */
				bA0 = Cudd_NotCond( Cudd_E( bA ), fIsComp );
				bA1 = Cudd_NotCond( Cudd_T( bA ), fIsComp );
			}
			else /* if ( levCover < levArea ) */
			{ /* assign the cofactors */
				bA0 = bA1 = bA;
			}

			/* start the Else part of the solution */
			bRes0 = extraZddConvertToBddAndAdd(dd, zC0, bA0);
			if ( bRes0 == NULL )
				return NULL;
			cuddRef( bRes0 );

			/* start the Then part of the solution */
			bRes1 = extraZddConvertToBddAndAdd(dd, zC1, bA1);
			if ( bRes1 == NULL )
			{
				Cudd_RecursiveDeref(dd, bRes0);
				return NULL;
			}
			cuddRef( bRes1 );

			/* cover without literals converted into BDD */
			bRes2 = extraZddConvertToBdd(dd, zC2);
			if ( bRes2 == NULL ) 
			{
				Cudd_RecursiveDeref(dd, bRes0);
				Cudd_RecursiveDeref(dd, bRes1);
				return NULL;
			}
			cuddRef( bRes2 );

			/* add this BDD to the Else part */
			bTemp = bRes0;
			bRes0 = cuddBddAndRecur(dd, Cudd_Not(bRes0), Cudd_Not(bRes2));
			if ( bRes0 == NULL )
			{
				Cudd_RecursiveDeref(dd, bTemp);
				Cudd_RecursiveDeref(dd, bRes1);
				Cudd_RecursiveDeref(dd, bRes2);
				return NULL;
			}
			cuddRef( bRes0 );
			bRes0 = Cudd_Not(bRes0);
			Cudd_RecursiveDeref(dd, bTemp);

			/* add this BDD to the Then part */
			bTemp = bRes1;
			bRes1 = cuddBddAndRecur(dd, Cudd_Not(bRes1), Cudd_Not(bRes2));
			if ( bRes1 == NULL )
			{
				Cudd_RecursiveDeref(dd, bRes0);
				Cudd_RecursiveDeref(dd, bTemp);
				Cudd_RecursiveDeref(dd, bRes2);
				return NULL;
			}
			cuddRef( bRes1 );
			bRes1 = Cudd_Not(bRes1);
			Cudd_RecursiveDeref(dd, bTemp);
			Cudd_RecursiveDeref(dd, bRes2);
			/* only bRes0 and bRes1 are referenced at this point */
		}

		/* consider the case when Res0 and Res1 are the same node */
		if ( bRes0 == bRes1 )
			bRes = bRes1;
		/* consider the case when Res1 is complemented */
		else if ( Cudd_IsComplement(bRes1) ) 
		{
			bRes = cuddUniqueInter(dd, TopBddVar, Cudd_Not(bRes1), Cudd_Not(bRes0));
			if ( bRes == NULL ) 
			{
				Cudd_RecursiveDeref(dd,bRes0);
				Cudd_RecursiveDeref(dd,bRes1);
				return NULL;
			}
			bRes = Cudd_Not(bRes);
		} 
		else 
		{
			bRes = cuddUniqueInter( dd, TopBddVar, bRes1, bRes0 );
			if ( bRes == NULL ) 
			{
				Cudd_RecursiveDeref(dd,bRes0);
				Cudd_RecursiveDeref(dd,bRes1);
				return NULL;
			}
		}
		cuddDeref( bRes0 );
		cuddDeref( bRes1 );

		/* insert the result into cache */
		cuddCacheInsert2(dd, extraZddConvertToBddAndAdd, zC, bA, bRes);
		return bRes;
	}
} /* end of extraZddConvertToBddAndAdd */


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

  Synopsis [Performs the recursive step of Cudd_zddSingleCoveredArea.]

  Description []

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
DdNode	*
extraZddSingleCoveredArea(
  DdManager * dd,
  DdNode * zC)
{
    DdNode	*bRes;
    statLine(dd); 

	/* if there is no cover, there is no BDD */
	if ( zC == z0 )  return b0;
	/* if the cover is the universe, the BDD is constant 1 */
	if ( zC == z1 )  return b1;

    /* check cache */
    bRes = cuddCacheLookup1(dd, extraZddSingleCoveredArea, zC);
    if (bRes)
		return(bRes);
	else
	{
		DdNode * bRes0, * bRes1, * bRes2, * bG0, * bG1;
		DdNode * zC0, * zC1, * zC2;
		int TopBddVar = (zC->index >> 1);

		/* cofactor the cover */
		extraDecomposeCover(dd, zC, &zC0, &zC1, &zC2);

		/* compute bdds for the three cofactors of the cover */
		bRes0 = extraZddSingleCoveredArea(dd, zC0);
		if ( bRes0 == NULL )
			return NULL;
		cuddRef( bRes0 );

		bRes1 = extraZddSingleCoveredArea(dd, zC1);
		if ( bRes1 == NULL )
		{
			Cudd_RecursiveDeref(dd, bRes0);
			return NULL;
		}
		cuddRef( bRes1 );

		bRes2 = extraZddSingleCoveredArea(dd, zC2);
		if ( bRes2 == NULL )
		{
			Cudd_RecursiveDeref(dd, bRes0);
			Cudd_RecursiveDeref(dd, bRes1);
			return NULL;
		}
		cuddRef( bRes2 );
		/* only bRes0, bRes1 and bRes2 are referenced at this point */

		/* bRes0 = bRes0 & !bdd(zC2) + bRes2 & !bdd(zC0) */
		bG0 = extraZddConvertToBddAndAdd( dd, zC2, Cudd_Not(bRes0) );
		if ( bG0 == NULL )
		{
			Cudd_IterDerefBdd(dd, bRes0);
			Cudd_IterDerefBdd(dd, bRes1);
			Cudd_IterDerefBdd(dd, bRes2);
			return NULL;
		}
		cuddRef( bG0 );
		Cudd_IterDerefBdd(dd, bRes0);

		bG1 = extraZddConvertToBddAndAdd( dd, zC0, Cudd_Not(bRes2) );
		if ( bG1 == NULL )
		{
			Cudd_IterDerefBdd(dd, bG0);
			Cudd_IterDerefBdd(dd, bRes1);
			Cudd_IterDerefBdd(dd, bRes2);
			return NULL;
		}
		cuddRef( bG1 );

		bRes0 = cuddBddAndRecur( dd, bG0, bG1 );
		if ( bRes0 == NULL )
		{
			Cudd_IterDerefBdd(dd, bG0);
			Cudd_IterDerefBdd(dd, bG1);
			Cudd_IterDerefBdd(dd, bRes1);
			Cudd_IterDerefBdd(dd, bRes2);
			return NULL;
		}
		cuddRef( bRes0 );
		bRes0 = Cudd_Not(bRes0);
		Cudd_IterDerefBdd(dd, bG0);
		Cudd_IterDerefBdd(dd, bG1);

		/* bRes1 = bRes1 & !bdd(zC2) + bRes2 & !bdd(zC1) */
		bG0 = extraZddConvertToBddAndAdd( dd, zC2, Cudd_Not(bRes1) );
		if ( bG0 == NULL )
		{
			Cudd_IterDerefBdd(dd, bRes0);
			Cudd_IterDerefBdd(dd, bRes1);
			Cudd_IterDerefBdd(dd, bRes2);
			return NULL;
		}
		cuddRef( bG0 );
		Cudd_IterDerefBdd(dd, bRes1);

		bG1 = extraZddConvertToBddAndAdd( dd, zC1, Cudd_Not(bRes2) );
		if ( bG1 == NULL )
		{
			Cudd_IterDerefBdd(dd, bG0);
			Cudd_IterDerefBdd(dd, bRes0);
			Cudd_IterDerefBdd(dd, bRes2);
			return NULL;
		}
		cuddRef( bG1 );
		Cudd_IterDerefBdd(dd, bRes2);

		bRes1 = cuddBddAndRecur( dd, bG0, bG1 );
		if ( bRes1 == NULL )
		{
			Cudd_IterDerefBdd(dd, bG0);
			Cudd_IterDerefBdd(dd, bG1);
			Cudd_IterDerefBdd(dd, bRes0);
			return NULL;
		}
		cuddRef( bRes1 );
		bRes1 = Cudd_Not(bRes1);
		Cudd_IterDerefBdd(dd, bG0);
		Cudd_IterDerefBdd(dd, bG1);

		/* only bRes0 and bRes1 are referenced at this point */

		/* consider the case when Res0 and Res1 are the same node */
		if ( bRes0 == bRes1 )
			bRes = bRes1;
		/* consider the case when Res1 is complemented */
		else if ( Cudd_IsComplement(bRes1) ) 
		{
			bRes = cuddUniqueInter(dd, TopBddVar, Cudd_Not(bRes1), Cudd_Not(bRes0));
			if ( bRes == NULL ) 
			{
				Cudd_RecursiveDeref(dd,bRes0);
				Cudd_RecursiveDeref(dd,bRes1);
				return NULL;
			}
			bRes = Cudd_Not(bRes);
		} 
		else 
		{
			bRes = cuddUniqueInter( dd, TopBddVar, bRes1, bRes0 );
			if ( bRes == NULL ) 
			{
				Cudd_RecursiveDeref(dd,bRes0);
				Cudd_RecursiveDeref(dd,bRes1);
				return NULL;
			}
		}
		cuddDeref( bRes0 );
		cuddDeref( bRes1 );

		/* insert the result into cache */
		cuddCacheInsert1(dd, extraZddSingleCoveredArea, zC, bRes);
		return bRes;
	}
} /* end of extraZddSingleCoveredArea */


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

  Synopsis    [Finds three cofactors of the cover w.r.t. to the topmost variable.]

  Description [Finds three cofactors of the cover w.r.t. to the topmost variable.
  Does not check the cover for being a constant. Assumes that ZDD variables encoding 
  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 cuddZddPrimeProduct()).]

  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 */

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