extraaddspectra.c

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

		/* insert the result into cache */
//		if ( bFunc->ref != 1 )
		cuddCacheInsert2(dd, extraBddWalsh, bFunc, bVars, aRes);
		return aRes;
	}
} /* end of extraBddWalsh */

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

  Synopsis    [Performs the reordering-sensitive step of Extra_bddReedMuller().]

  Description [Generates in a bottom-up fashion an ADD for all spectral
               coefficients of the functions represented by a BDD.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
DdNode* extraBddReedMuller( 
  DdManager * dd,    /* the manager */
  DdNode * bFunc,    /* the function whose spectrum is being computed */
  DdNode * bVars)    /* the variables on which the function depends */
{
	DdNode * aRes;
    statLine(dd); 

	/* terminal cases */
	if ( bVars == b1 )
	{
		assert( Cudd_IsConstant(bFunc) );
		if ( bFunc == b0 )
			return a0;
		else
			return a1;
	}

    /* check cache */
    if ( aRes = cuddCacheLookup2(dd, extraBddReedMuller, bFunc, bVars) )
    	return aRes;
	else
	{
		DdNode * bFunc0, * bFunc1;   /* cofactors of the function */
		DdNode * aRes0,  * aRes1;    /* partial results to be composed by ITE */
		DdNode * bFuncR = Cudd_Regular(bFunc); /* the regular pointer to the function */
		DdNode * aTemp;

		/* bFunc cannot depend on a variable that is not in bVars */
		assert( cuddI(dd,bFuncR->index) >= cuddI(dd,bVars->index) );


		/* cofactor the BDD */
		if ( bFuncR->index == bVars->index )
		{
			if ( bFuncR != bFunc ) /* bFunc is complemented */
			{
				bFunc0 = Cudd_Not( cuddE(bFuncR) );
				bFunc1 = Cudd_Not( cuddT(bFuncR) );
			}
			else
			{
				bFunc0 = cuddE(bFuncR);
				bFunc1 = cuddT(bFuncR);
			}
		}
		else /* bVars is higher in the variable order */
			bFunc0 = bFunc1 = bFunc;


		/* solve subproblems */
		aRes0 = extraBddReedMuller( dd, bFunc0, cuddT(bVars) );
		if ( aRes0 == NULL )
			return NULL;
		cuddRef( aRes0 );

		aRes1 = extraBddReedMuller( dd, bFunc1, cuddT(bVars) );
		if ( aRes1 == NULL )
		{
			Cudd_RecursiveDeref( dd, aRes0 );
			return NULL;
		}
		cuddRef( aRes1 );

		/* compute  aRes1 = aRes1 (+) aRes0 */
		aRes1 = cuddAddApplyRecur( dd, Cudd_addXor, aTemp = aRes1, aRes0 );
		if ( aRes1 == NULL )
		{
			Cudd_RecursiveDeref( dd, aRes0 );
			Cudd_RecursiveDeref( dd, aTemp );
			return NULL;
		}
		cuddRef( aRes1 );
		Cudd_RecursiveDeref(dd, aTemp);


		/* only aRes0 and aRes1 are referenced at this point */

		/* consider the case when Res0 and Res1 are the same node */
		aRes = (aRes1 == aRes0) ? aRes1 : cuddUniqueInter( dd, bVars->index, aRes1, aRes0 );
		if (aRes == NULL) 
		{
			Cudd_RecursiveDeref(dd, aRes1);
			Cudd_RecursiveDeref(dd, aRes0);
			return NULL;
		}
		cuddDeref(aRes1);
		cuddDeref(aRes0);

		/* insert the result into cache */
		cuddCacheInsert2(dd, extraBddReedMuller, bFunc, bVars, aRes);
		return aRes;
	}
} /* end of extraBddReedMuller */

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

  Synopsis    [Performs the reordering-sensitive step of Extra_bddHaar().]

  Description [Generates in a bottom-up fashion an ADD for all spectral
               coefficients of the functions represented by a BDD.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
DdNode* extraBddHaar( 
  DdManager * dd,    /* the manager */
  DdNode * bFunc,    /* the function whose spectrum is being computed */
  DdNode * bVars)    /* the variables on which the function depends */
{
	DdNode * aRes;
    statLine(dd); 

	/* terminal cases */
	if ( bVars == b1 )
	{
		assert( Cudd_IsConstant(bFunc) );
		if ( bFunc == b0 )
			return a0;
		else
			return a1;
	}

    /* check cache */
//	if ( bFunc->ref != 1 )
    if ( aRes = cuddCacheLookup2(dd, extraBddHaar, bFunc, bVars) )
    	return aRes;
	else
	{
		DdNode * bFunc0, * bFunc1;   /* cofactors of the function */
		DdNode * aHaar0, * aHaar1;   /* partial solutions of the problem */
		DdNode * aNode0, * aNode1;   /* the special terminal nodes */
		DdNode * aRes0,  * aRes1;    /* partial results to be composed by ITE */
		DdNode * bFuncR = Cudd_Regular(bFunc); /* the regular pointer to the function */
		DdNode * aTemp;
		double   dValue0, dValue1;

		/* bFunc cannot depend on a variable that is not in bVars */
		assert( cuddI(dd,bFuncR->index) >= cuddI(dd,bVars->index) );


		/* cofactor the BDD */
		if ( bFuncR->index == bVars->index )
		{
			if ( bFuncR != bFunc ) /* bFunc is complemented */
			{
				bFunc0 = Cudd_Not( cuddE(bFuncR) );
				bFunc1 = Cudd_Not( cuddT(bFuncR) );
			}
			else
			{
				bFunc0 = cuddE(bFuncR);
				bFunc1 = cuddT(bFuncR);
			}
		}
		else /* bVars is higher in the variable order */
			bFunc0 = bFunc1 = bFunc;


		/* solve subproblems */
		aHaar0 = extraBddHaar( dd, bFunc0, cuddT(bVars) );
		if ( aHaar0 == NULL )
			return NULL;
		cuddRef( aHaar0 );

		aHaar1 = extraBddHaar( dd, bFunc1, cuddT(bVars) );
		if ( aHaar1 == NULL )
		{
			Cudd_RecursiveDeref( dd, aHaar0 );
			return NULL;
		}
		cuddRef( aHaar1 );

		/* retrieve the terminal values in aHaar0 and aHaar1 */
		for ( aTemp = aHaar0; aTemp->index != CUDD_CONST_INDEX; aTemp = cuddE(aTemp) );
		dValue0 = cuddV( aTemp );
		for ( aTemp = aHaar1; aTemp->index != CUDD_CONST_INDEX; aTemp = cuddE(aTemp) );
		dValue1 = cuddV( aTemp );

		/* get the new terminal nodes */
		aNode0 = cuddUniqueConst( dd, dValue0 + dValue1 );
		if ( aNode0 == NULL )
		{
			Cudd_RecursiveDeref( dd, aHaar0 );
			Cudd_RecursiveDeref( dd, aHaar1 );
			return NULL;
		}
		cuddRef( aNode0 );

		aNode1 = cuddUniqueConst( dd, dValue0 - dValue1 );
		if ( aNode1 == NULL )
		{
			Cudd_RecursiveDeref( dd, aHaar0 );
			Cudd_RecursiveDeref( dd, aHaar1 );
			Cudd_RecursiveDeref( dd, aNode0 );
			return NULL;
		}
		cuddRef( aNode1 );


		/* replace the terminal nodes in the cofactor ADDs */
		aRes0 = extraAddUpdateZeroCubeValue( dd, aHaar0, cuddT(bVars), aNode0  );
		if ( aRes0 == NULL )
		{
			Cudd_RecursiveDeref( dd, aHaar0 );
			Cudd_RecursiveDeref( dd, aHaar1 );
			Cudd_RecursiveDeref( dd, aNode0 );
			Cudd_RecursiveDeref( dd, aNode1 );
			return NULL;
		}
		cuddRef( aRes0 );

		aRes1 = extraAddUpdateZeroCubeValue( dd, aHaar1, cuddT(bVars), aNode1  );
		if ( aRes1 == NULL )
		{
			Cudd_RecursiveDeref( dd, aHaar0 );
			Cudd_RecursiveDeref( dd, aHaar1 );
			Cudd_RecursiveDeref( dd, aNode0 );
			Cudd_RecursiveDeref( dd, aNode1 );
			Cudd_RecursiveDeref( dd, aRes0 );
			return NULL;
		}
		cuddRef( aRes1 );

		Cudd_RecursiveDeref(dd, aHaar0);
		Cudd_RecursiveDeref(dd, aHaar1);

		Cudd_RecursiveDeref(dd, aNode0);
		Cudd_RecursiveDeref(dd, aNode1);


		/* only aRes0 and aRes1 are referenced at this point */

		/* consider the case when Res0 and Res1 are the same node */
		aRes = (aRes1 == aRes0) ? aRes1 : cuddUniqueInter( dd, bVars->index, aRes1, aRes0 );
		if (aRes == NULL) 
		{
			Cudd_RecursiveDeref(dd, aRes1);
			Cudd_RecursiveDeref(dd, aRes0);
			return NULL;
		}
		cuddDeref(aRes1);
		cuddDeref(aRes0);

		/* insert the result into cache */
//		if ( bFunc->ref != 1 )
		cuddCacheInsert2(dd, extraBddHaar, bFunc, bVars, aRes);
		return aRes;
	}
} /* end of extraBddHaar */

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

  Synopsis    [Performs the reordering-sensitive step of Extra_bddHaarInverse().]

  Description [Generates in a bottom-up fashion an ADD for the inverse Haar.]

  SideEffects [The third cached argument (bSteps) is the BDD of the elementary variable
  whose index equal to the number of lazy steps made thus far plus one. On the top-most
  level it is 0, next it is 1, etc.]

  SeeAlso     []

******************************************************************************/
DdNode * extraBddHaarInverse( 
  DdManager * dd,    /* the manager */
  DdNode * aFunc,    /* the function whose spectrum is being computed */
  DdNode * aSteps,   /* the index of this variable indicates the number of previous lazy recursive calls */
  DdNode * bVars,    /* the variables, on which the function depends */
  DdNode * bVarsAll, /* the set of all variables, which will never change through the calls */
  int      nVarsAll, /* the number of vars in the set */
  int    * InverseMap ) /* the variable map mapping the var index into its inverse var index */
{
	DdNode * aRes;
	DdNode * bCacheCube;
    statLine(dd); 

	/* terminal cases */
	if ( bVars == b1 )
	{ // return a terminal node with a value equal to cuddV(aFunc) * 2^(nSteps-1)
		if ( cuddV(aSteps) == 0.0 )
			return cuddUniqueConst( dd, cuddV(aFunc) ); 
		else
			return cuddUniqueConst( dd, cuddV(aFunc) * Extra_Power2( (int)(cuddV(aSteps)-1) ) ); 
	}

    /* check cache */
    /* the last two arguments are derivitives, therefore there are useless for caching */
	/* the other two arguments (bVars and bVarsAll) can be combined into one argument */
	bCacheCube = extraCachingCube( dd, bVarsAll, bVars );  Cudd_Ref( bCacheCube );
    if ( aRes = cuddCacheLookup(dd, DD_ADD_HAAR_INVERSE_TAG, aFunc, aSteps, bCacheCube) )
	{
		Cudd_RecursiveDeref( dd, bCacheCube );
   		return aRes;
	}
	else
	{
		DdNode * aFunc0, * aFunc1;   /* cofactors of the function */
		DdNode * aInvH0, * aInvH1;   /* partial solutions of the problem */
		DdNode * aRes0,  * aRes1;    /* partial results to be composed by ITE */
		DdNode * aStepNext;

		/* aFunc cannot depend on a variable that is not in bVars */
		assert( cuddI(dd,aFunc->index) >= cuddI(dd,bVars->index) );

		/* cofactor the ADD */
		if ( aFunc->index == bVars->index )
		{
			aFunc0 = cuddE(aFunc);
			aFunc1 = cuddT(aFunc);
		}
		else /* bVars is higher in the variable order */
			aFunc0 = aFunc1 = aFunc;


		if ( cuddV(aSteps) > 0.0 ) /* meaning that it is a lazy call */
		{
			/* solve subproblems */
			aStepNext = cuddUniqueConst( dd, cuddV(aSteps)+1 );
			if ( aStepNext == NULL )
				return NULL;
			cuddRef( aStepNext );

			aInvH0 = extraBddHaarInverse( dd, aFunc0, aStepNext, cuddT(bVars), bVarsAll, nVarsAll, InverseMap );
			if ( aInvH0 == NULL )
			{
				Cudd_RecursiveDeref( dd, aStepNext );
				return NULL;
			}
			cuddRef( aInvH0 );

			aInvH1 = extraBddHaarInverse( dd, aFunc1, aStepNext, cuddT(bVars), bVarsAll, nVarsAll, InverseMap );
			if ( aInvH1 == NULL )
			{
				Cudd_RecursiveDeref( dd, aStepNext );
				Cudd_RecursiveDeref( dd, aInvH0 );
				return NULL;
			}
			cuddRef( aInvH1 );
			Cudd_RecursiveDeref( dd, aStepNext );

			aRes0 = aInvH0;
			aRes1 = aInvH1;
		}
		else // if ( cuddV(aSteps) == 0.0 )