extrazddcovers.c

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

		/* --------------- 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, extraZddProductAlt, f, g, zRes);
		return zRes;
	}
} /* end of extraZddProductAlt */


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

  Synopsis [Performs the recursive step of Extra_zddCompatible.]

  Description []

  SideEffects [None]

  SeeAlso     [Extra_zddCompatibleCount]

******************************************************************************/
DdNode	*
extraZddCompatible(
  DdManager * dd,     /* the DD manager */
  DdNode * zCover,    /* the cover */
  DdNode * zCube)     /* the cube */
{
    DdNode	*zRes;
    statLine(dd); 

    /* terminal cases */
	assert( zCube != dd->zero );
    if ( zCube == dd->one || zCover == dd->zero || zCover == dd->one )
        return zCover;

    /* check cache */
    zRes = cuddCacheLookup2Zdd(dd, extraZddCompatible, zCover, zCube);
    if (zRes)
		return zRes;
	else
	{
		DdNode *zRes0, *zRes1, *zRes2, *zTemp;
		int TopZddVar;

		/* level in terms of original variables, not ZDD variables */
		int LevelCover = dd->permZ[zCover->index] >> 1;
		int LevelCube  = dd->permZ[zCube->index]  >> 1;

		if ( LevelCover > LevelCube )
			return extraZddCompatible( dd, zCover, cuddT(zCube) );
		else if ( LevelCover < LevelCube )
		{
			/* decompose the cover */
			DdNode *zCover0, *zCover1, *zCover2;
			extraDecomposeCover(dd, zCover, &zCover0, &zCover1, &zCover2);

			/* cover with negative literal */
			zRes0 = extraZddCompatible( dd, zCover0, zCube );
			if ( zRes0 == NULL )
				return NULL;
			cuddRef( zRes0 );

			/* cover with positive literal */
			zRes1 = extraZddCompatible( dd, zCover1, zCube );
			if ( zRes1 == NULL )
			{
				Cudd_RecursiveDerefZdd(dd, zRes0);
				return NULL;
			}
			cuddRef( zRes1 );
		
			/* cover without literal */
			zRes2 = extraZddCompatible( dd, zCover2, zCube );
			if ( zRes2 == NULL )
			{
				Cudd_RecursiveDerefZdd(dd, zRes0);
				Cudd_RecursiveDerefZdd(dd, zRes1);
				return NULL;
			}
			cuddRef( zRes2 );
		}
		else /* if ( LevelCover == LevelCube ) */
		{
			/* decompose the cover */
			DdNode *zCover0, *zCover1, *zCover2;
			extraDecomposeCover(dd, zCover, &zCover0, &zCover1, &zCover2);

			if ( 2 * LevelCube == dd->permZ[zCube->index] )
			{ /* cube has positive literal */

				/* cover with positive literal */
				zRes1 = extraZddCompatible( dd, zCover1, cuddT(zCube) );
				if ( zRes1 == NULL )
					return NULL;
				cuddRef( zRes1 );

				/* cover with negative literal */
				zRes0 = dd->zero;
				cuddRef( zRes0 );
			}
			else if ( 2 * LevelCube + 1 == dd->permZ[zCube->index] )
			{ /* cube has negative literal */

				/* cover with negative literal */
				zRes0 = extraZddCompatible( dd, zCover0, cuddT(zCube) );
				if ( zRes0 == NULL )
					return NULL;
				cuddRef( zRes0 );

				/* cover with positive literal */
				zRes1 = dd->zero;
				cuddRef( zRes1 );
			}
			else
				assert(0);
		
			/* cover without literal */
			zRes2 = extraZddCompatible( dd, zCover2, cuddT(zCube) );
			if ( zRes2 == NULL )
			{
				Cudd_RecursiveDerefZdd(dd, zRes0);
				Cudd_RecursiveDerefZdd(dd, zRes1);
				return NULL;
			}
			cuddRef( zRes2 );
		}

		/* --------------- composing the result ------------------ */
		/* the index of the positive ZDD variable in zCover */
		TopZddVar = (zCover->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, extraZddCompatible, zCover, zCube, zRes);
		return zRes;
	}
} /* end of extraZddCompatible */



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

  Synopsis    [Performs the recursive step of the alternative ISOP computation.]

  Description []

  SideEffects []

  SeeAlso     [Extra_zddIsopCover]

******************************************************************************/
DdNode* extraZddSimplify( 
  DdManager * dd,     /* the DD manager */
  DdNode * bA,        /* the on-set */
  DdNode * bB)        /* the on-set + dc-set */
{
    DdNode	*zRes;
    statLine(dd); 

	/* if there is no area (the cover should be empty), there is nowhere to expand */
	if ( bA == b0 )    return z0;
	/* if the area is the total boolean space, the cover is expanded into a single large cube */
	if ( bB == b1 )    return z1;

    /* check cache */
    zRes = cuddCacheLookup2Zdd(dd, extraZddSimplify, bA, bB);
    if (zRes)
		return zRes;
	else
	{
		DdNode *bA0, *bA1, *bB0, *bB1;
		DdNode *zRes0, *zRes1, *zRes2, *zTemp;

		DdNode *bAA = Cudd_Regular(bA);
		DdNode *bBB = Cudd_Regular(bB);

		int LevA = dd->perm[bAA->index];
		int LevB = dd->perm[bBB->index];

		/* the index of the positive ZDD variable in the result */
		int TopVar;

		if ( LevA <= LevB )
		{
			int fIsComp = (int)(bA != bAA);
			bA0 = Cudd_NotCond( cuddE(bAA), fIsComp );
			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;


		/* zRes0 = extraZddSimplify( bA0, bB0 ) */
		zRes0 = extraZddSimplify( dd, bA0, bB0 );
		if ( zRes0 == NULL )
			return NULL;
		cuddRef( zRes0 );

		/* zRes1 = extraZddSimplify( bA1, bB1 ) */
		zRes1 = extraZddSimplify( dd, bA1, bB1 );
		if ( zRes1 == NULL )
		{
			Cudd_RecursiveDerefZdd(dd, zRes0);
			return NULL;
		}
		cuddRef( zRes1 );

		/* zRes2 = cuddZddIntersect( zRes0, zRes1 ) */
		zRes2 = cuddZddIntersect( dd, zRes0, zRes1 );
		if ( zRes2 == NULL )
		{
			Cudd_RecursiveDerefZdd(dd, zRes0);
			Cudd_RecursiveDerefZdd(dd, zRes1);
			return NULL;
		}
		cuddRef( zRes2 );

		/* zRes0 = cuddZddDiff( zRes0, zRes2 ) */
		zRes0 = cuddZddDiff( 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);

		/* zRes1 = cuddZddDiff( zRes1, zRes2 ) */
		zRes1 = cuddZddDiff( 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);

		/* --------------- compose the result ------------------ */
		zRes = extraComposeCover( dd, zRes0, zRes1, zRes2, TopVar );
		if ( zRes == NULL ) return NULL;

		/* insert the result into cache and return */
		cuddCacheInsert2(dd, extraZddSimplify, bA, bB, zRes);
		return zRes;
	}
} /* end of extraZddSimplify */



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

  Synopsis    [Performs the recursive step of the alternative ISOP computation.]

  Description []

  SideEffects []

  SeeAlso     [Extra_zddIsopCover]

******************************************************************************/
DdNode* extraZddIsopCoverAlt( 
  DdManager * dd,     /* the DD manager */
  DdNode * bA,        /* the on-set */
  DdNode * bB)        /* the on-set + dc-set */
{
    DdNode	*zRes;
    statLine(dd); 

	/* if there is no area (the cover should be empty), there is nowhere to expand */
	if ( bA == b0 )    return z0;
	/* if the area is the total boolean space, the cover is expanded into a single large cube */
	if ( bB == b1 )    return z1;

    /* check cache */
    zRes = cuddCacheLookup2Zdd(dd, extraZddIsopCoverAlt, bA, bB);
    if (zRes)
		return zRes;
	else
	{
		DdNode *bA0, *bA1, *bB0, *bB1, *bG0, *bG1, *bHA, *bHB;
		DdNode *zRes0, *zRes1, *zRes2;

		DdNode *bAA = Cudd_Regular(bA);
		DdNode *bBB = Cudd_Regular(bB);

		int LevA = dd->perm[bAA->index];
		int LevB = dd->perm[bBB->index];

		/* the index of the positive ZDD variable in the result */
		int TopVar;

		if ( LevA <= LevB )
		{
			int fIsComp = (int)(bA != bAA);
			bA0 = Cudd_NotCond( cuddE(bAA), fIsComp );
			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) ) */
		zRes0 = extraZddIsopCoverAlt( dd, bG0, bB0 );
		if ( zRes0 == NULL )
		{
			Cudd_IterDerefBdd(dd, bG0);
			return NULL;
		}
		cuddRef( zRes0 );
		Cudd_IterDerefBdd(dd, bG0);


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

		/* P1 = IrrCover( g1, F12(x=1) ) */
		zRes1 = extraZddIsopCoverAlt( dd, bG1, bB1 );
		if ( zRes1 == NULL )
		{
			Cudd_IterDerefBdd(dd, bG1);
			Cudd_RecursiveDerefZdd(dd, zRes0);
			return NULL;
		}
		cuddRef( zRes1 );
		Cudd_IterDerefBdd(dd, bG1);

		/* h1 = F1(x=0) & !bdd(P0)  +   F1(x=1) & !bdd(P1) */
		bG0 = extraZddConvertToBddAndAdd( dd, zRes0, Cudd_Not(bA0) );
		if ( bG0 == NULL )
		{
			Cudd_RecursiveDerefZdd(dd, zRes0);
			Cudd_RecursiveDerefZdd(dd, zRes1);
			return NULL;
		}
		cuddRef( bG0 );

		bG1 = extraZddConvertToBddAndAdd( dd, zRes1, Cudd_Not(bA1) );
		if ( bG1 == NULL )
		{
			Cudd_IterDerefBdd(dd, bG0);
			Cudd_RecursiveDerefZdd(dd, zRes0);
			Cudd_RecursiveDerefZdd(dd, zRes1);
			return NULL;
		}
		cuddRef( bG1 );

		bHA = cuddBddAndRecur( dd, bG0, bG1 );
		if ( bHA == NULL )
		{
			Cudd_IterDerefBdd(dd, bG0);
			Cudd_IterDerefBdd(dd, bG1);
			Cudd_RecursiveDerefZdd(dd, zRes0);
			Cudd_RecursiveDerefZdd(dd, zRes1);
			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_RecursiveDerefZdd(dd, zRes0);
			Cudd_RecursiveDerefZdd(dd, zRes1);
			return NULL;
		}
		cuddRef( bHB );

		/* P1 = IrrCover( h1, h12 ) */
		zRes2 = extraZddIsopCoverAlt( dd, bHA, bHB );
		if ( zRes2 == NULL )
		{
			Cudd_IterDerefBdd(dd, bHA);
			Cudd_IterDerefBdd(dd, bHB);
			Cudd_RecursiveDerefZdd(dd, zRes0);
			Cudd_RecursiveDerefZdd(dd, zRes1);
			return NULL;
		}
		cuddRef( zRes2 );
		Cudd_IterDerefBdd(dd, bHA);
		Cudd_IterDerefBdd(dd, bHB);

		/* --------------- compose the result ------------------ */
		zRes = extraComposeCover( dd, zRes0, zRes1, zRes2, TopVar );
		if ( zRes == NULL ) return NULL;

		/* insert the result into cache and return */
		cuddCacheInsert2(dd, extraZddIsopCoverAlt, bA, bB, zRes);
		return zRes;
	}
} /* end of extraZddIsopCoverAlt */




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

  Synopsis    [Performs the recursive step of the alternative ISOP computation.]

  Description []

  SideEffects []

  SeeAlso     [Extra_zddIsopCover]

******************************************************************************/
DdNode * extraZddIsopCubeNum( 
  DdManager * dd,     /* the DD manager */
  DdNode * bA,        /* the on-set */
  DdNode * bB,        /* the on-set + dc-set */
  int * pnCubes)      /* the number of cubes (return value) */
{
    DdNode	* bRes;
    DdNode	* aNum;
  	DdNode * (*cacheOp1)(DdManager*,DdNode*);
  	DdNode * (*cacheOp2)(DdManager*,DdNode*,DdNode*);

    statLine(dd); 

	/* if there is no area (the cover should be empty), there is nowhere to expand */
	if ( bA == b0 )    
    {
        *pnCubes = 0;
        return b0;
    }
	/* if the area is the total boolean space, the cover is expanded into a single large cube */
	if ( bB == b1 )    
    {
        *pnCubes = 1;
        return b1;
    }

    assert( Cudd_bddLeq( dd, bA, bB ) );

    /* check cache */
    cacheOp1 = (DdNode*(*)(DdManager*,DdNode*))extraZddIsopCubeNum;
    cacheOp2 = (DdNode*(*)(DdManager*,DdNode*,DdNode*))Extra_zddIsopCubeNum;

    bRes = cuddCacheLookup2(dd, cacheOp2, bA, bB);
    if ( bRes )
    {
        // get the number of cubes in this ISOP
        aNum = cuddCacheLookup1( dd, cacheOp1, bRes );
        if ( aNum )
        {
            cuddRef( aNum );
            *pnCubes = (int)(cuddV(aNum));
            Cudd_RecursiveDeref( dd, aNum );
		    return bRes;
        }
        cuddRef( bRes );
        Cudd_IterDerefBdd( dd, bRes );
    }
    // if the ISOP as a BDD or the number of cubes cannot be found, 
    // perform the regular expansion
	{
		DdNode *bA0, *bA1, *bB0, *bB1, *bG0, *bG1, *bHA, *bHB;
		DdNode *bRes0, *bRes1, *bRes2, *bTemp;

		DdNode *bAA = Cudd_Regular(bA);
		DdNode *bBB = Cudd_Regular(bB);

		int LevA = dd->perm[bAA->index];
		int LevB = dd->perm[bBB->index];

        int nCubes0, nCubes1, nCubes2;

		/* the index of the positive ZDD variable in the result */
		int TopVar;

		if ( LevA <= LevB )
		{
			int fIsComp = (int)(bA != bAA);
			bA0 = Cudd_NotCond( cuddE(bAA), fIsComp );