extraddutils.c

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

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

  Synopsis [Performs the recursive step of Cudd_zddNotCoveredByCover.]

  Description []

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
DdNode	*
extraZddNotCoveredByCover(
  DdManager * dd,
  DdNode * zC,   /* the ZDD for the cover */
  DdNode * zD)   /* the ZDD for the second cover */
{
    DdNode	*zRes;
    statLine(dd); 

	/* if the second cover is empty, the first cover is not covered */
	if ( zD == z0 )  return zC;
	/* if the second cover is full, not a part of the first cover is not covered */
	if ( zD == z1 )  return z0;
	/* if there is nothing in the cover, nothing is not covered */
	if ( zC == z0 )  return z0;
	/* if the first cover is full (and the second cover is not empty), 
	   the universe is partially covered, so the result is empty */
	if ( zC == z1 )  return z1;

    /* check cache */
    zRes = cuddCacheLookup2Zdd(dd, extraZddNotCoveredByCover, zC, zD);
    if (zRes)
		return zRes;
	else
	{
		/* find the level in terms of the original variable levels, not ZDD variable levels */
		int levC = dd->permZ[zC->index] >> 1;
		int levD = dd->permZ[zD->index] >> 1;

		if ( levC > levD )
		{
			DdNode *zD0, *zD1, *zD2;
			extraDecomposeCover(dd, zD, &zD0, &zD1, &zD2);

			/* C cannot be covered by zD0 and zD1 - only zD2 left to consider */
			zRes = extraZddNotCoveredByCover( dd, zC, zD2 );
			if ( zRes == NULL ) return NULL;
		}
		else /* if ( levC <= levD ) */
		{
			DdNode *zRes0, *zRes1, *zRes2;
			DdNode *zC0, *zC1, *zC2;
			DdNode *zD0, *zD1, *zD2, *zTemp;
			int TopZddVar;

			/* decompose covers */
			extraDecomposeCover(dd, zC, &zC0, &zC1, &zC2);
			if ( levC == levD )
				extraDecomposeCover(dd, zD, &zD0, &zD1, &zD2);
			else /* if ( levC < levD ) */
				zD0 = zD1 = z0, zD2 = zD;

			/* solve subproblems */

			/* cover with negative literal can only be contained in zD0 + zD2 */
			zTemp = cuddZddUnion( dd, zD0, zD2 );
			if ( zTemp == NULL )
				return NULL;
			cuddRef( zTemp );

			zRes0 = extraZddNotCoveredByCover( dd, zC0, zTemp );
			if ( zRes0 == NULL )
			{
				Cudd_RecursiveDerefZdd(dd, zTemp);
				return NULL;
			}
			cuddRef( zRes0 );
			Cudd_RecursiveDerefZdd(dd, zTemp);

			/* cover with positive literal can only be contained in zD1 + zD2 */
			zTemp = cuddZddUnion( dd, zD1, zD2 );
			if ( zTemp == NULL )
			{
				Cudd_RecursiveDerefZdd(dd, zRes0);
				return NULL;
			}
			cuddRef( zTemp );

			zRes1 = extraZddNotCoveredByCover( dd, zC1, zTemp );
			if ( zRes1 == NULL )
			{
				Cudd_RecursiveDerefZdd(dd, zTemp);
				Cudd_RecursiveDerefZdd(dd, zRes0);
				return NULL;
			}
			cuddRef( zRes1 );
			Cudd_RecursiveDerefZdd(dd, zTemp);


			/* cover without literal can only be contained in zD2 */
			zRes2 = extraZddNotCoveredByCover( dd, zC2, zD2 );
			if ( zRes2 == NULL )
			{
				Cudd_RecursiveDerefZdd(dd, zRes0);
				Cudd_RecursiveDerefZdd(dd, zRes1);
				return NULL;
			}
			cuddRef( zRes2 );

			/* --------------- compose the result ------------------ */
			/* the index of the positive ZDD variable in zC */
			TopZddVar = (zC->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 and return */
		cuddCacheInsert2(dd, extraZddNotCoveredByCover, zC, zD, zRes);
		return zRes;
	}
} /* end of extraZddNotCoveredByCover */



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

  Synopsis [Performs the recursive step of Cudd_zddOverlappingWithArea.]

  Description []

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
DdNode	*
extraZddOverlappingWithArea(
  DdManager * dd,
  DdNode * zC,   /* the ZDD for the cover */
  DdNode * bA)   /* the BDD for the area */
{
    DdNode	*zRes;
    statLine(dd); 

	/* if there is no area, there are no overlapping cubes */
	if ( bA == b0 )  return z0;
	/* if the area is the total boolean space, all cubes of the cover overlap with area */
	if ( bA == b1 )  return zC;
	/* if there is nothing in the cover, nothing to overlap */
	if ( zC == z0 )  return z0;
	/* if the cover is the universe (and the area is something), the universe overlaps */
	if ( zC == z1 )  return zC;

    /* check cache */
    zRes = cuddCacheLookup2Zdd(dd, extraZddOverlappingWithArea, zC, bA);
    if (zRes)
		return zRes;
	else
	{
		DdNode *bA0, *bA1, *bA01;

		/* 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 )
		{
			/* find the parts(cofactors) of the area */
			bA0 = Cudd_NotCond( Cudd_E( bA ), fIsComp );
			bA1 = Cudd_NotCond( Cudd_T( bA ), fIsComp );

			/* find the union of cofactors */
			bA01 = cuddBddAndRecur( dd, Cudd_Not(bA0), Cudd_Not(bA1) );
			if ( bA01 == NULL ) return NULL;
			cuddRef( bA01 );
			bA01 = Cudd_Not(bA01);

			/* those cubes overlap, which overlap with the union of cofactors */
			zRes = extraZddOverlappingWithArea( dd, zC, bA01 );
			if ( zRes == NULL ) 
			{
				Cudd_RecursiveDeref( dd, bA01 );
				return NULL;
			}
			cuddRef( zRes );
			Cudd_RecursiveDeref( dd, bA01 );
			cuddDeref( zRes );
		}
		else /* if ( levCover <= levArea ) */
		{
			DdNode *zRes0, *zRes1, *zRes2, *zTemp;
			int TopZddVar;

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

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

				/* find the union of cofactors */
				bA01 = cuddBddAndRecur( dd, Cudd_Not(bA0), Cudd_Not(bA1) );
				if ( bA01 == NULL ) return NULL;
				cuddRef( bA01 );
				bA01 = Cudd_Not(bA01);
			}
			else /* if ( levCover < levArea ) */
			{
				/* assign the cofactors and their union */
				bA0 = bA1 = bA01 = bA;
				/* reference the union for uniformity with the above case */
				cuddRef( bA01 );
			}

			/* solve subproblems */

			/* cover without literal overlaps with the union */
			zRes2 = extraZddOverlappingWithArea( dd, zC2, bA01 );
			if ( zRes2 == NULL )
			{
				Cudd_RecursiveDeref( dd, bA01 );
				return NULL;
			}
			cuddRef( zRes2 );
			Cudd_RecursiveDeref( dd, bA01 );

			/* cover with negative literal overlaps with bA0 */
			zRes0 = extraZddOverlappingWithArea( dd, zC0, bA0 );
			if ( zRes0 == NULL )
			{
				Cudd_RecursiveDerefZdd(dd, zRes2);
				return NULL;
			}
			cuddRef( zRes0 );

			/* cover with positive literal overlaps with bA1 */
			zRes1 = extraZddOverlappingWithArea( dd, zC1, bA1 );
			if ( zRes1 == NULL )
			{
				Cudd_RecursiveDerefZdd(dd, zRes0);
				Cudd_RecursiveDerefZdd(dd, zRes2);
				return NULL;
			}
			cuddRef( zRes1 );

			/* --------------- compose the result ------------------ */
			/* the index of the positive ZDD variable in zC */
			TopZddVar = (zC->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 and return */
		cuddCacheInsert2(dd, extraZddOverlappingWithArea, zC, bA, zRes);
		return zRes;
	}
} /* end of extraZddOverlappingWithArea */


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

  Synopsis [Performs the recursive step of Cudd_zddConvertToBdd.]

  Description []

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
DdNode	*
extraZddConvertToBdd(
  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, extraZddConvertToBdd, 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 = extraZddConvertToBdd(dd, zC0);
		if ( bRes0 == NULL )
			return NULL;
		cuddRef( bRes0 );

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

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

		/* compute  bdd(zC0)+bdd(zC2) */
		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);

		/* compute  bdd(zC1)+bdd(zC2) */
		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 */
		cuddCacheInsert1(dd, extraZddConvertToBdd, zC, bRes);
		return bRes;
	}
} /* end of extraZddConvertToBdd */


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

  Synopsis [Performs the recursive step of Extra_zddConvertToBddUnate.]

  Description []

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
DdNode	*
extraZddConvertToBddUnate(
  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, extraZddConvertToBddUnate, zC);
    if (bRes)
		return(bRes);
	else
	{
		DdNode * bRes0, * bRes1, * bTemp;
//		DdNode * zUnion;
/*
		bRes0 = extraZddConvertToBddUnate(dd, cuddE(zC));
		if ( bRes0 == NULL )
			return NULL;
		cuddRef( bRes0 );

		zUnion = cuddZddUnion( dd, cuddE(zC), cuddT(zC) );
		if ( zUnion == NULL )
		{
			Cudd_RecursiveDeref(dd, bRes0);
			return NULL;
		}
		cuddRef( zUnion );

		bRes1 = extraZddConvertToBddUnate(dd, zUnion);
		if ( bRes1 == NULL )
		{
			Cudd_RecursiveDeref(dd, bRes0);
			Cudd_RecursiveDerefZdd(dd, zUnion);
			return NULL;
		}
		cuddRef( bRes1 );
		Cudd_RecursiveDerefZdd(dd, zUnion);
*/



		bRes0 = extraZddConvertToBddUnate(dd, cuddE(zC));
		if ( bRes0 == NULL )
			return NULL;
		cuddRef( bRes0 );

		bRes1 = extraZddConvertToBddUnate(dd, cuddT(zC));
		if ( bRes1 == NULL )
		{
			Cudd_RecursiveDeref(dd, bRes0);
			return NULL;
		}
		cuddRef( bRes1 );

		bRes1 = cuddBddAndRecur(dd, bTemp = Cudd_Not(bRes1), Cudd_Not(bRes0));
		if ( bRes1 == NULL )
		{
			Cudd_RecursiveDeref(dd, bRes0);
			Cudd_RecursiveDeref(dd, bRes1);
			return NULL;
		}
		cuddRef( bRes1 );
		Cudd_RecursiveDeref(dd, bTemp);
		bRes1 = Cudd_Not(bRes1);


		/* 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, zC->index/2, 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, zC->index/2, bRes1, bRes0 );
			if ( bRes == NULL ) 
			{
				Cudd_RecursiveDeref(dd,bRes0);