extraaddspectra.c

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

		{
			/* solve subproblems */
			aInvH0 = extraBddHaarInverse( dd, aFunc0, aSteps, cuddT(bVars), bVarsAll, nVarsAll, InverseMap );
			if ( aInvH0 == NULL )
				return NULL;
			cuddRef( aInvH0 );

			aStepNext = cuddUniqueConst( dd, 1.0 );
			if ( aStepNext == NULL )
			{
				Cudd_RecursiveDeref( dd, aInvH0 );
				return NULL;
			}
			cuddRef( aStepNext );

			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 );


			/* compute  aRes0 = aWalsh0 + aWalsh1 */
			aRes0 = cuddAddApplyRecur( dd, Cudd_addPlus, aInvH0, aInvH1 );
			if ( aRes0 == NULL )
			{
				Cudd_RecursiveDeref( dd, aInvH0 );
				Cudd_RecursiveDeref( dd, aInvH1 );
				return NULL;
			}
			cuddRef( aRes0 );

			/* compute  aRes1 = aWalsh0 - aWalsh1 */
			aRes1 = cuddAddApplyRecur( dd, Cudd_addMinus, aInvH0, aInvH1 );
			if ( aRes1 == NULL )
			{
				Cudd_RecursiveDeref( dd, aInvH0 );
				Cudd_RecursiveDeref( dd, aInvH1 );
				Cudd_RecursiveDeref( dd, aRes0 );
				return NULL;
			}
			cuddRef( aRes1 );

			Cudd_RecursiveDeref(dd, aInvH0);
			Cudd_RecursiveDeref(dd, aInvH1);
		}

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

		/* consider the case when Res0 and Res1 are the same node */
		aRes = extraAddIteRecurGeneral( dd, dd->vars[ InverseMap[bVars->index] ], aRes1, aRes0 );
		if (aRes == NULL) 
		{
			Cudd_RecursiveDeref(dd, aRes1);
			Cudd_RecursiveDeref(dd, aRes0);
			return NULL;
		}
		cuddRef( aRes );
		Cudd_RecursiveDeref(dd, aRes1);
		Cudd_RecursiveDeref(dd, aRes0);
		cuddDeref( aRes );

		/* insert the result into cache */
		cuddCacheInsert(dd, DD_ADD_HAAR_INVERSE_TAG, aFunc, aSteps, bCacheCube, aRes);
		Cudd_RecursiveDeref( dd, bCacheCube );
		return aRes;
	}
} /* end of extraBddHaarInverse */


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

  Synopsis    [Replaces the negative variable assignment node in the ADD by the given value.]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
DdNode * extraAddUpdateZeroCubeValue(
  DdManager * dd, 
  DdNode * aFunc,    /* the ADD to be updated */
  DdNode * bVars,
  DdNode * aNode )  /* the terminal node representing the required value */
{
	DdNode * aRes;
    statLine(dd); 

	/* terminal cases */
	if ( bVars == b1 )
	{
		assert( Cudd_IsConstant(aFunc) );
		return aNode;
	}

    /* check cache */
    if ( aRes = cuddCacheLookup(dd, DD_ADD_UPDATE_ZERO_CUBE_TAG, aFunc, bVars, aNode) )
	{ 
		s_CacheHit++;
   		return aRes;
	}
	else
	{
		DdNode * aFunc0, * aFunc1;    /* cofactors */
		DdNode * aRes0,  * aRes1;     /* partial results to be composed by ITE */

		s_CacheMiss++;

		if ( aFunc->index == bVars->index )
		{
			aFunc0 = cuddE( aFunc );
			aFunc1 = cuddT( aFunc );
		}
		else
			aFunc0 = aFunc1 = aFunc;


		aRes0  = extraAddUpdateZeroCubeValue( dd, aFunc0, cuddT(bVars), aNode );
		if ( aRes0 == NULL )
			return NULL;
		cuddRef( aRes0 );

		aRes1 = aFunc1;
//		cuddRef( aRes1 );

		/* 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 */
		cuddCacheInsert(dd, DD_ADD_UPDATE_ZERO_CUBE_TAG, aFunc, bVars, aNode, aRes);
		return aRes;
	}
} /* end of extraAddUpdateZeroCubeValue */


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

  Synopsis    [Implements the recursive step of Cudd_addIteGeneral(f,g,h).]

  Description [Implements the recursive step of Cudd_addIteGeneral(f,g,h),
  meaning that g and h are not supposed to be 0-1 ADDs but may have more terminals.
  Applying arithmetic addition in the terminal case. Returns a pointer to the 
  resulting ADD if successful; NULL otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_addIte]

******************************************************************************/
DdNode * extraAddIteRecurGeneral( DdManager * dd, DdNode * bX, DdNode * aF, DdNode * aG )
{
	DdNode * aRes;
	statLine( dd );

	assert( !Cudd_IsConstant(bX) );
	assert(  cuddE(bX) == b0 && cuddT(bX) == b1 ); /* the elementary variable */

    /* check cache */
    if ( aRes = cuddCacheLookup(dd, DD_ADD_ITE_GENERAL_TAG, bX, aF, aG) )
    	return aRes;
	else
	{
		DdNode * aF0, * aF1, * aG0, * aG1;
		int LevelF, LevelG, LevelX, LevelTop;

		LevelF = cuddI(dd,aF->index);
		LevelG = cuddI(dd,aG->index);
		LevelX = dd->perm[bX->index];
		LevelTop = ddMin(LevelF, LevelG);
		LevelTop = ddMin(LevelX, LevelTop);

		if ( LevelF == LevelTop )
		{
			aF0 = cuddE(aF);
			aF1 = cuddT(aF);
		}
		else
			aF0 = aF1 = aF;

		if ( LevelG == LevelTop )
		{
			aG0 = cuddE(aG);
			aG1 = cuddT(aG);
		}
		else
			aG0 = aG1 = aG;

		if ( LevelX == LevelTop )
		{
			assert( LevelX < LevelF );
			assert( LevelX < LevelG );

			/* consider the case when Res0 and Res1 are the same node */
			aRes = (aF == aG) ? aF : cuddUniqueInter( dd, bX->index, aF, aG );
			if (aRes == NULL) 
				return NULL;
		}
		else
		{
			DdNode * aRes0,  * aRes1;     /* partial results to be composed by ITE */

			aRes0  = extraAddIteRecurGeneral( dd, bX, aF0, aG0 );
			if ( aRes0 == NULL )
				return NULL;
			cuddRef( aRes0 );

			aRes1  = extraAddIteRecurGeneral( dd, bX, aF1, aG1 );
			if ( aRes1 == NULL )
			{
				Cudd_RecursiveDeref(dd, aRes0);
				return NULL;
			}
			cuddRef( aRes1 );

			/* 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, dd->invperm[LevelTop], aRes1, aRes0 );
			if (aRes == NULL) 
			{
				Cudd_RecursiveDeref(dd, aRes1);
				Cudd_RecursiveDeref(dd, aRes0);
				return NULL;
			}
			cuddDeref(aRes1);
			cuddDeref(aRes0);
		}

		cuddCacheInsert( dd, DD_ADD_ITE_GENERAL_TAG, bX, aF, aG, aRes );
		return aRes;
	}
}	/* end of extraAddIteRecurGeneral */



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

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

  Synopsis    [Computes a caching cube.]

  Description [It is known that bVars is a cube representing a subset of bVarsAll
  this function computes the canonical representation of the pair (bVarsAll, bVars) 
  by one DD node the convention is the following: if ( bVars == bVarsAll), return bVarsAll,
  otherwise return ITE(x, cuddT(bVarsAll), bVars), where x is the topmost var in bVarsAll.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
DdNode * extraCachingCube( DdManager * dd, DdNode * bVarsAll, DdNode * bVars )
{
	if ( bVars == bVarsAll)  
		return bVarsAll;
	else
		return cuddUniqueInter( dd, bVarsAll->index, cuddT(bVarsAll), bVars );
	// because bVarsAll is positive cube, cuddT(bVarsAll) is never complemented
}



/*

void Experiment( BFunc * pFunc )
{
	int i;
	int nVars = pFunc->nInputs;
	int nOuts = pFunc->nOutputs;
	DdManager * dd = pFunc->dd;
	long clk;

	DdNode * aSpectrum[MAXOUTPUTS];
	DdNode * aModified[MAXOUTPUTS];
	DdNode * aInverse[MAXOUTPUTS];
	DdNode * bTest;
	DdNode * bSupp;
//	DdNode * bTemp;
	// introduce an additional variable
	DdNode * bVarTemp = Cudd_bddNewVar(dd);

//	if ( nVars < 5 )
//	{
//		PRK(pFunc->pOutputs[0],nVars);
//	}


	clk = clock();
	for ( i = 0; i < nOuts; i++ )
	{
		bSupp = Cudd_Support( dd, pFunc->pOutputs[i] );  Cudd_Ref( bSupp ); 


		aSpectrum[i] = Extra_bddHaar( dd, pFunc->pOutputs[i], bSupp );   Cudd_Ref( aSpectrum[i] );
		aModified[i] = Extra_addRemapNatural2Sequential( dd, aSpectrum[i], bSupp ); Cudd_Ref( aModified[i] );
		aInverse[i]  = Extra_bddHaarInverse( dd, aModified[i], bSupp );   Cudd_Ref( aInverse[i] );

		bTest = Cudd_addBddPattern( dd, aInverse[i] );  Cudd_Ref( bTest );
		if ( bTest != pFunc->pOutputs[i] )
			printf( "Output #%d: Verification FAILED!\n", i );
		else
			printf( "Output #%d: Verification okay!\n", i );
		Cudd_RecursiveDeref( dd, bTest );


		Cudd_RecursiveDeref( dd, bSupp );
		fprintf( stderr, "." );
		fflush( stderr );
	}


	{ // visualize the ADD 
//		FILE* pFileDot = fopen( "FuncADD.dot", "w" );
//		Cudd_DumpDot( dd, 1, &aSpectrum2[0], NULL, NULL, pFileDot );
//		fclose( pFileDot );
	}


//	printf( "\n" ) << "s_CacheHit = %d", s_CacheHit );
//	printf( "s_CacheMiss = %d", s_CacheMiss );
	printf( "\n" );
//	printf( "\n" );
	printf( "Spectrum generation time = %.2f sec\n", (float)(clock() - clk)/(float)(CLOCKS_PER_SEC) );
	printf( "Shared BDD node count = %d\n", Cudd_SharingSize(pFunc->pOutputs,nOuts) );
	printf( "Shared ADD node count = %d\n", Cudd_SharingSize(aSpectrum,nOuts) );
	printf( "\n" );
	printf( "Statistics for the all outputs:\n" );
	printf( "The number of different coefficients = %d\n", Extra_addCountConstArray(dd,aSpectrum,nOuts) );
	printf( "The smallest coefficient = %.1f\n", cuddV(Extra_addFindMinArray(dd,aSpectrum,nOuts)) );
	printf( "The largest coefficient = %.1f\n", cuddV(Extra_addFindMaxArray(dd,aSpectrum,nOuts)) );
	printf( "\n" );


	for ( i = 0; i < nOuts; i++ )
	{
		Cudd_RecursiveDeref( dd, aSpectrum[i] );
		Cudd_RecursiveDeref( dd, aModified[i] );
		Cudd_RecursiveDeref( dd, aInverse[i] );
	}

	return;
}
*/

////////////////////////////////////////////////////////////////////////
///                           END OF FILE                            ///
////////////////////////////////////////////////////////////////////////