extrazddcovers.c

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

			bA1 = Cudd_NotCond( cuddT(bAA), fIsComp );
			TopVar = bAA->index;
		}
		else
			bA0 = bA1 = bA;

		if ( LevB <= LevA )
		{
			int fIsComp = (int)(bB != bBB);
			bB0 = Cudd_NotCond( cuddE(bBB), fIsComp );
			bB1 = Cudd_NotCond( cuddT(bBB), fIsComp );
			TopVar = bBB->index;
		}
		else
			bB0 = bB1 = bB;

		/* g0 = F1(x=0) & !F12(x=1) */
		bG0 = cuddBddAndRecur( dd, bA0, Cudd_Not(bB1) );
		if ( bG0 == NULL ) return NULL;
		cuddRef( bG0 );

		/* P0 = IrrCover( g0, F12(x=0) ) */
		bRes0 = extraZddIsopCubeNum( dd, bG0, bB0, &nCubes0 );
		if ( bRes0 == NULL )
		{
			Cudd_IterDerefBdd(dd, bG0);
			return NULL;
		}
		cuddRef( bRes0 );
		Cudd_IterDerefBdd(dd, bG0);


		/* g0 = F1(x=1) & !F12(x=0) */
		bG1 = cuddBddAndRecur( dd, bA1, Cudd_Not(bB0) );
		if ( bG1 == NULL )
		{
			Cudd_IterDerefBdd(dd, bRes0);
			return NULL;
		}
		cuddRef( bG1 );

		/* P1 = IrrCover( g1, F12(x=1) ) */
		bRes1 = extraZddIsopCubeNum( dd, bG1, bB1, &nCubes1 );
		if ( bRes1 == NULL )
		{
			Cudd_IterDerefBdd(dd, bG1);
			Cudd_IterDerefBdd(dd, bRes0);
			return NULL;
		}
		cuddRef( bRes1 );
		Cudd_IterDerefBdd(dd, bG1);

		/* h1 = F1(x=0) & !bdd(P0)  +   F1(x=1) & !bdd(P1) */
		bG0 = cuddBddAndRecur( dd, bA0, Cudd_Not(bRes0) );
		if ( bG0 == NULL )
		{
			Cudd_IterDerefBdd(dd, bRes0);
			Cudd_IterDerefBdd(dd, bRes1);
			return NULL;
		}
		cuddRef( bG0 );

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

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

		/* h12 = F12(x=0) & F12(x=1) */
		bHB = cuddBddAndRecur( dd, bB0, bB1 );
		if ( bHB == NULL )
		{
			Cudd_IterDerefBdd(dd, bHA);
			Cudd_IterDerefBdd(dd, bRes0);
			Cudd_IterDerefBdd(dd, bRes1);
			return NULL;
		}
		cuddRef( bHB );

		/* P1 = IrrCover( h1, h12 ) */
		bRes2 = extraZddIsopCubeNum( dd, bHA, bHB, &nCubes2 );
		if ( bRes2 == NULL )
		{
			Cudd_IterDerefBdd(dd, bHA);
			Cudd_IterDerefBdd(dd, bHB);
			Cudd_IterDerefBdd(dd, bRes0);
			Cudd_IterDerefBdd(dd, bRes1);
			return NULL;
		}
		cuddRef( bRes2 );
		Cudd_IterDerefBdd(dd, bHA);
		Cudd_IterDerefBdd(dd, bHB);

        // add 2 to 0 and 1
   		bRes0 = cuddBddAndRecur( dd, bTemp = Cudd_Not(bRes0), Cudd_Not(bRes2) );
		if ( bRes0 == NULL )
		{
			Cudd_IterDerefBdd(dd, bRes0);
			Cudd_IterDerefBdd(dd, bRes1);
			Cudd_IterDerefBdd(dd, bRes2);
			return NULL;
		}
		cuddRef( bRes0 );
        bRes0 = Cudd_Not( bRes0 );
		Cudd_IterDerefBdd(dd, bTemp);

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


		/* --------------- compose the result ------------------ */
        *pnCubes = nCubes0 + nCubes1 + nCubes2;

	    /* 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, TopVar, 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, TopVar, bRes1, bRes0 );
		    if ( bRes == NULL ) 
		    {
			    Cudd_RecursiveDeref(dd,bRes0);
			    Cudd_RecursiveDeref(dd,bRes1);
			    return NULL;
		    }
	    }
	    cuddDeref( bRes0 );
	    cuddDeref( bRes1 );
        cuddRef( bRes );

	    // insert the BDD of the ISOP into cache
	    cuddCacheInsert2(dd, cacheOp2, bA, bB, bRes);

        // get the ADD node, which represents the number of cubes in the ISOP
        aNum = cuddUniqueConst( dd, (CUDD_VALUE_TYPE)(*pnCubes) );
		if ( aNum == NULL ) 
		{
			Cudd_RecursiveDeref(dd,bRes);
			return NULL;
		}

        // insert the ADD node into cache
	    cuddCacheInsert1(dd, cacheOp1, bRes, aNum);

        // return the BDD of the ISOP
	    cuddDeref( bRes );
	    return bRes;
	}
} /* end of extraZddIsopCubeNum */



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

  Synopsis    [Performs the recursive step of Extra_zddNotContainedCubesOverArea().]

  Description [Given two covers, C and D, and an area of boolean space, A, 
  this procedure returns the set of all such cubes c in C, for which there 
  DOES NOT EXIST a cube d in D, such that the overlap of c and A 
  (c intersection A) is completely contained.]

  SideEffects []

  SeeAlso     [Extra_zddIsopCover]

******************************************************************************/
DdNode* extraZddNotContainedCubesOverArea( 
  DdManager * dd,     /* the DD manager */
  DdNode * zC,        /* the cover whose cubes are filtered */
  DdNode * zD,        /* the cover whose cubes are used to determine filterning */
  DdNode * bA)        /* the area */
{
    DdNode	*zRes;
    statLine(dd); 

	/* if there is no area, the intersection of any cube with it 
	   is empty and therefore is always contained in D (D is not empty!) */
	if ( bA == b0 )    return z0;
	/* if there are no containing cubes, any cover is not contained */
	if ( zD == z0 )    return zC;
	/* if the area is the b-space, only those cubes are not contained
	   whose literals are not supersets of cubes in D */
	if ( bA == b1 )    return extraZddNotSupSet( dd, zC, zD );
	/* if D is the tautology cube (and area is not empty), 
	   the intersection of cubes in C with area is always contained in D */
	if ( zD == z1 )    return z0;
	/* if there are no cubes in C, none of them are contained or not contained */
	if ( zC == z0 )    return z0;
	/* if C is the tautology cube, it is contained only if
	   there is at least one cube in D that completely contains A */
	/* this case is treated by further expansion */
//	if ( zC == z1 )    return ???

    /* check cache */
    zRes = cuddCacheLookup(dd, DD_ZDD_BDD_SUBSET_TAG, zC, zD, bA);
    if (zRes)
		return zRes;
	else
	{
		DdNode *bA0, *bA1, *bA01;
		DdNode *zC0, *zC1, *zC2, *zD0, *zD1, *zD2, *zUnion;
		DdNode *zRes0, *zRes1, *zRes2;

		int LevC = cuddIZ( dd, zC->index ) >> 1;
		int LevD = cuddIZ( dd, zD->index ) >> 1;
		int LevA = cuddI(  dd, Cudd_Regular(bA)->index );

		/* consider the easy case, when the area splits higher */
		if ( LevA < LevC && LevA < LevD ) 
		{
			/* determine whether the area is a complemented BDD */
			int fIsComp  = Cudd_IsComplement( bA );
			/* 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 = extraZddNotContainedCubesOverArea( dd, zC, zD, bA01 );
			if ( zRes == NULL ) 
			{
				Cudd_RecursiveDeref( dd, bA01 );
				return NULL;
			}
			cuddRef( zRes );
			Cudd_RecursiveDeref( dd, bA01 );
			cuddDeref( zRes );
		}
		else
		{ /* now, either zC or zD (or both) have the top-most variable */

			int TopVar = -1;
			/* cofactor covers and area */
			if ( LevC <= LevD )
			{
				TopVar = zC->index >> 1;
				extraDecomposeCover(dd, zC, &zC0, &zC1, &zC2);
			}
			else
				zC0 = zC1 = z0, zC2 = zC;

			if ( LevD <= LevC )
			{
				TopVar = zD->index >> 1;
				extraDecomposeCover(dd, zD, &zD0, &zD1, &zD2);
			}
			else
				zD0 = zD1 = z0, zD2 = zD;
			assert( TopVar != -1 );

			if ( Cudd_Regular(bA)->index == TopVar )
			{
				/* determine whether the area is a complemented BDD */
				int fIsComp  = Cudd_IsComplement( bA );
				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
			{
				bA0 = bA1 = bA01 = bA;
				cuddRef( bA01 );
			}

			/* cubes without this literal can be covered by cubes without this literal
			   as well as by cubes with positive literal if bA0 = 0
			   or by cubes with negative literals if bA1 = 0 */
			if ( bA0 == b0 )
			{
				zUnion = cuddZddUnion( dd, zD2, zD1 );
				if ( zUnion == NULL )
				{
					Cudd_RecursiveDeref( dd, bA01 );
					return NULL;
				}
				cuddRef( zUnion );
			}
			else if ( bA1 == b0 )
			{
				zUnion = cuddZddUnion( dd, zD2, zD0 );
				if ( zUnion == NULL )
				{
					Cudd_RecursiveDeref( dd, bA01 );
					return NULL;
				}
				cuddRef( zUnion );
			}
			else
			{
				zUnion = zD2;
				cuddRef( zUnion );
			}


			/* solve the problem for cubes without literal */
			zRes2 = extraZddNotContainedCubesOverArea( dd, zC2, zUnion, bA01 );
			if ( zRes2 == NULL )
			{
				Cudd_RecursiveDeref( dd, bA01 );
				Cudd_RecursiveDerefZdd( dd, zUnion );
				return NULL;
			}
			cuddRef( zRes2 );
			Cudd_RecursiveDeref( dd, bA01 );
			Cudd_RecursiveDerefZdd( dd, zUnion );


			/* compute the union of those cubes in D 
			   that can potentially contain cubes in C0 */
			zUnion = cuddZddUnion( dd, zD0, zD2 );
			if ( zUnion == NULL )
			{
				Cudd_RecursiveDerefZdd( dd, zRes2 );
				return NULL;
			}
			cuddRef( zUnion );

			/* solve the problem for cubes with negative literals */
			zRes0 = extraZddNotContainedCubesOverArea( dd, zC0, zUnion, bA0 );
			if ( zRes0 == NULL )
			{
				Cudd_RecursiveDerefZdd( dd, zUnion );
				Cudd_RecursiveDerefZdd( dd, zRes2 );
				return NULL;
			}
			cuddRef( zRes0 );
			Cudd_RecursiveDerefZdd( dd, zUnion );


			/* compute the union of those cubes in D 
			   that can potentially contain cubes in C1 */
			zUnion = cuddZddUnion( dd, zD1, zD2 );
			if ( zUnion == NULL )
			{
				Cudd_RecursiveDerefZdd( dd, zRes0 );
				Cudd_RecursiveDerefZdd( dd, zRes2 );
				return NULL;
			}
			cuddRef( zUnion );

			/* solve the problem for cubes with negative literals */
			zRes1 = extraZddNotContainedCubesOverArea( dd, zC1, zUnion, bA1 );
			if ( zRes1 == NULL )
			{
				Cudd_RecursiveDerefZdd( dd, zUnion );
				Cudd_RecursiveDerefZdd( dd, zRes0 );
				Cudd_RecursiveDerefZdd( dd, zRes2 );
				return NULL;
			}
			cuddRef( zRes1 );
			Cudd_RecursiveDerefZdd( dd, zUnion );

			/* --------------- compose the result ------------------ */
			zRes = extraComposeCover( dd, zRes0, zRes1, zRes2, TopVar );
			if ( zRes == NULL ) return NULL;
		}			
		/* insert the result into cache and return */
		cuddCacheInsert(dd, DD_ZDD_BDD_SUBSET_TAG, zC, zD, bA, zRes);
		return zRes;
	}
} /* end of extraZddNotContainedCubesOverArea */


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

  Synopsis    [Performs the recursive step of Extra_zddSelectOneCube.]

  Description []

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
DdNode * extraZddSelectOneCube( 
  DdManager * dd, 
  DdNode * zS )
// selects one cube from the ZDD zS
// returns z0 if and only if zS is an empty set of cubes
{
	DdNode * zRes;

	if ( zS == z0 )    return z0;
	if ( zS == z1 )    return z1;
	
	// check cache
	if ( zRes = cuddCacheLookup1Zdd( dd, extraZddSelectOneCube, zS ) )
		return zRes;
	else
	{
		DdNode * zS0, * zS1, * zS2, * zTemp; 
		int topVar = zS->index/2;

		extraDecomposeCover( dd, zS, &zS0, &zS1, &zS2 );

		if ( zS2 != z0 )
		{
			zRes = extraZddSelectOneCube( dd, zS2 );
			if ( zRes == NULL )
				return NULL;
		}
		else if ( zS0 != z0 )
		{
			zTemp = extraZddSelectOneCube( dd, zS0 );
			if ( zTemp == NULL )
				return NULL;
			cuddRef( zTemp );

			zRes = cuddZddGetNode( dd, 2*topVar+1, zTemp, dd->zero );
			if ( zRes == NULL ) 
			{
				Cudd_RecursiveDerefZdd( dd, zTemp );
				return NULL;
			}
			cuddDeref( zTemp );
		}
		else if ( zS1 != z0 )
		{
			zTemp = extraZddSelectOneCube( dd, zS1 );
			if ( zTemp == NULL )
				return NULL;
			cuddRef( zTemp );

			zRes = cuddZddGetNode( dd, 2*topVar, zTemp, dd->zero );
			if ( zRes == NULL ) 
			{
				Cudd_RecursiveDerefZdd( dd, zTemp );
				return NULL;
			}
			cuddDeref( zTemp );
		}
		else
			assert( 0 );

		// insert the result into cache
		cuddCacheInsert1( dd, extraZddSelectOneCube, zS, zRes );
		return zRes;
	}		
} /* end of extraZddSelectOneCube */


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

  Synopsis    [Performs the recursive step of Extra_zddSelectOneSubset.]

  Description []

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
DdNode * extraZddSelectOneSubset( 
  DdManager * dd, 
  DdNode * zS )
// selects one subset from the ZDD zS
// returns z0 if and only if zS is an empty set of cubes
{
	DdNode * zRes;

	if ( zS == z0 )    return z0;
	if ( zS == z1 )    return z1;
	
	// check cache
	if ( zRes = cuddCacheLookup1Zdd( dd, extraZddSelectOneSubset, zS ) )
		return zRes;
	else
	{
		DdNode * zS0, * zS1, * zTemp; 

		zS0 = cuddE(zS);
		zS1 = cuddT(zS);

		if ( zS0 != z0 )
		{
			zRes = extraZddSelectOneSubset( dd, zS0 );
			if ( zRes == NULL )
				return NULL;
		}
		else // if ( zS0 == z0 )
		{
			assert( zS1 != z0 );
			zRes = extraZddSelectOneSubset( dd, zS1 );
			if ( zRes == NULL )
				return NULL;
			cuddRef( zRes );

			zRes = cuddZddGetNode( dd, zS->index, zTemp = zRes, z0 );
			if ( zRes == NULL ) 
			{
				Cudd_RecursiveDerefZdd( dd, zTemp );
				return NULL;
			}
			cuddDeref( zTemp );
		}

		// insert the result into cache
		cuddCacheInsert1( dd, extraZddSelectOneSubset, zS, zRes );
		return zRes;
	}		
} /* end of extraZddSelectOneSubset */


/*---------------------------------------------------------------------------*/
/* Definition of static Functions                                            */
/*---------------------------------------------------------------------------*/