extrabddmisc.c

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

******************************************************************************/
void Extra_addShowFromBdd( DdManager * dd, DdNode * bFunc )
{ 
	DdNode * aFunc;
    FILE * pFileDot = fopen( "bdd.dot", "w" );
	aFunc = Cudd_BddToAdd( dd, bFunc );  Cudd_Ref( aFunc );
    Cudd_DumpDot( dd, 1, &aFunc, NULL, NULL, pFileDot );
	Cudd_RecursiveDeref( dd, aFunc );
    fclose( pFileDot );
}


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

  Synopsis    [Finds the smallest integer larger of equal than the logarithm.]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
int Extra_Base2Log( unsigned Num )
// returns [Log2(Num)]
{
	int Res;
	assert( Num >= 0 );
	if ( Num == 0 ) return 0;
	if ( Num == 1 ) return 1;
	for ( Res = 0, Num--; Num; Num >>= 1, Res++ );
	return Res;
} /* end of Extra_Base2Log */

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

  Synopsis    [Finds the smallest integer larger of equal than the logarithm.]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
int Extra_Base2LogDouble( double Num )
{
	double Res;
	int ResInt;

	Res    = log(Num)/log(2.0);
	ResInt = (int)Res;
	if ( ResInt == Res )
		return ResInt;
	else 
		return ResInt+1;
}


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

  Synopsis    [Returns the power of two as a double.]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
double Extra_Power2( unsigned Degree )
{
	double Res;
	assert( Degree >= 0 );
	if ( Degree < 32 )
		return (double)(01<<Degree); 
	for ( Res = 1.0; Degree; Res *= 2.0, Degree-- );
	return Res;
}


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

  Synopsis    [Outputs the BDD in a readable format.]

  Description []

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
void Extra_bddPrint( DdManager * dd, DdNode * F )
// utility to convert an ADD or a BDD into a string containing set of cubes
{
    DdGen * Gen;
    int * Cube;
    CUDD_VALUE_TYPE Value;
    int nVars = dd->size;
    int fFirstCube = 1;
	int i;

    if ( F == b0 || F == a0 )
	{
		printf("Constant 0");
		return;
	}
    if ( F == b1 || F == a1 )
	{
		printf("Constant 1");
		return;
	}

    Cudd_ForeachCube( dd, F, Gen, Cube, Value )
    {
        if ( fFirstCube )
			fFirstCube = 0;
		else
//			Output << " + ";
			printf( " + " );

        for ( i = 0; i < nVars; i++ )
            if ( Cube[i] == 0 )
				printf( "[%d]'", i );
//				printf( "%c'", (char)('a'+i) );
            else if ( Cube[i] == 1 )
				printf( "[%d]", i );
//				printf( "%c", (char)('a'+i) );
    }

//	printf("\n");
}

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

  Synopsis    [Builds BDD representing the set of fixed-size variable tuples.]

  Description [Creates BDD of all combinations of variables in Support that have k vars in them.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
DdNode* Extra_bddTuples( 
  DdManager * dd,   /* the DD manager */
  int K,            /* the number of variables in tuples */
  DdNode * VarsN)   /* the set of all variables represented as a BDD */
{
    DdNode	*res;
    int		autoDyn;

	/* it is important that reordering does not happen, 
	   otherwise, this methods will not work */

    autoDyn = dd->autoDyn;
    dd->autoDyn = 0;

    do {
		/* transform the numeric arguments (K) into a DdNode* argument;
		 * this allows us to use the standard internal CUDD cache */
		DdNode *VarSet = VarsN, *VarsK = VarsN;
		int     nVars = 0, i;

		/* determine the number of variables in VarSet */
		while ( VarSet != b1 )
		{
			nVars++;
			/* make sure that the VarSet is a cube */
			if ( cuddE( VarSet ) != b0 )
				return NULL;
			VarSet = cuddT( VarSet );
		}
		/* make sure that the number of variables in VarSet is less or equal 
		   that the number of variables that should be present in the tuples
		*/
		if ( K > nVars )
			return NULL;

		/* the second argument in the recursive call stannds for <n>;
		/* reate the first argument, which stands for <k> 
		 * as when we are talking about the tuple of <k> out of <n> */
		for ( i = 0; i < nVars-K; i++ )
			VarsK = cuddT( VarsK );

		dd->reordered = 0;
		res = extraBddTuples(dd, VarsK, VarsN );

    } while (dd->reordered == 1);
    dd->autoDyn = autoDyn;
    return(res);

} /* end of Extra_bddTuples */


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

  Synopsis    [Changes the polarity of vars listed in the cube.]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
DdNode* Extra_bddChangePolarity( 
  DdManager * dd,   /* the DD manager */
  DdNode * bFunc,
  DdNode * bVars) 
{
    DdNode	*res;
    do {
		dd->reordered = 0;
		res = extraBddChangePolarity( dd, bFunc, bVars );
    } while (dd->reordered == 1);
    return(res);

} /* end of Extra_bddChangePolarity */



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

  Synopsis    [Finds the node profile of the DD.]

  Description [Finds the number of nodes on each level. The array is allocated 
  by the user and should have at least   as many entries as the maximum number 
  of variables in the BDD and ZDD parts of the manager.]

  SideEffects [None]

  SeeAlso     [Cudd_Support]

******************************************************************************/
int * 
Extra_ProfileNode(
  DdManager * dd, /* manager */
  DdNode * F,     /* DD whose profile is sought */
  int * Profile ) /* array allocated by the user */
{
    int	i, size;
	st_table * Visited;

    // Initialize support array for ddSupportStep. 
    size = ddMax(dd->size, dd->sizeZ);
    for (i = 0; i < size; i++) 
		Profile[i] = 0;
  
	// start the visited table
	Visited  = st_init_table(st_ptrcmp,st_ptrhash);
  
    // get the profile
    ddProfileNode(dd, Cudd_Regular(F), Profile, Visited);

	st_free_table( Visited );
    return(Profile);

} /* end of Extra_ProfileNode */

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

  Synopsis    [Finds the node profile of the shared DD.]

  Description [Finds the number of nodes on each level. The array is allocated 
  by the user and should have at least as many entries as the maximum number 
  of variables in the BDD and ZDD parts of the manager.]

  SideEffects [None]

  SeeAlso     [Cudd_Support]

******************************************************************************/
int * 
Extra_ProfileNodeSharing(
  DdManager * dd,    /* manager */
  DdNode ** pFuncs,  /* the DDs whose profile is sought */
  int nFuncs,        /* the number of DDs */
  int * Profile )    /* array allocated by the user */
{
    int	i, size;
	st_table * Visited;

    // Initialize support array for ddSupportStep. 
    size = ddMax(dd->size, dd->sizeZ);
    for (i = 0; i < size; i++) 
		Profile[i] = 0;
  
	// start the visited table
	Visited  = st_init_table(st_ptrcmp,st_ptrhash);
  
    // get the profile
	for ( i = 0; i < nFuncs; i++ )
		ddProfileNode(dd, Cudd_Regular(pFuncs[i]), Profile, Visited);

	st_free_table( Visited );
    return(Profile);

} /* end of Extra_ProfileNodeSharing */


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

  Synopsis    [Finds the edge profile of the DD.]

  Description [Finds how many edges of each length exists. The array is allocated 
  by the user and should have at least   as many entries as the maximum number 
  of variables in the BDD and ZDD parts of the manager.]

  SideEffects [None]

  SeeAlso     [Cudd_Support]

******************************************************************************/
int * 
Extra_ProfileEdge(
  DdManager * dd, /* manager */
  DdNode * F,     /* DD whose profile is sought */
  int * Profile ) /* array allocated by the user */
{
    int	i, size;
	st_table * Visited;

    // Initialize support array for ddSupportStep. 
    size = ddMax(dd->size, dd->sizeZ);
    for (i = 0; i < size; i++) 
		Profile[i] = 0;
  
	// start the visited table
	Visited  = st_init_table(st_ptrcmp,st_ptrhash);
  
    // get the profile
    ddProfileEdge(dd, Cudd_Regular(F), Profile, Visited);

	st_free_table( Visited );
    return(Profile);

} /* end of Extra_ProfileEdge */

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

  Synopsis    [Finds the edge profile of the shared DD.]

  Description [Finds how many edges of each length exists. The array is allocated 
  by the user and should have at least as many entries as the maximum number 
  of variables in the BDD and ZDD parts of the manager.]

  SideEffects [None]

  SeeAlso     [Cudd_Support]

******************************************************************************/
int * 
Extra_ProfileEdgeSharing(
  DdManager * dd,    /* manager */
  DdNode ** pFuncs,  /* the DDs whose profile is sought */
  int nFuncs,        /* the number of DDs */
  int * Profile )    /* array allocated by the user */
{
    int	i, size;
	st_table * Visited;

    // Initialize support array for ddSupportStep. 
    size = ddMax(dd->size, dd->sizeZ);
    for (i = 0; i < size; i++) 
		Profile[i] = 0;
  
	// start the visited table
	Visited  = st_init_table(st_ptrcmp,st_ptrhash);
  
    // get the profile
	for ( i = 0; i < nFuncs; i++ )
		ddProfileEdge(dd, Cudd_Regular(pFuncs[i]), Profile, Visited);

	st_free_table( Visited );
    return(Profile);

} /* end of Extra_ProfileEdgeSharing */


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

  Synopsis    [Permutes the variables of the array of BDDs.]

  Description [Given a permutation in array permut, creates a new BDD
  with permuted variables. There should be an entry in array permut
  for each variable in the manager. The i-th entry of permut holds the
  index of the variable that is to substitute the i-th variable.
  The DDs in the resulting array are already referenced.]

  SideEffects [None]

  SeeAlso     [Cudd_addPermute Cudd_bddSwapVariables]

******************************************************************************/
void Extra_bddPermuteArray( DdManager * manager, DdNode ** bNodesIn, DdNode ** bNodesOut, int nNodes, int *permut )
{
	DdHashTable *table;
	int i, k;
	do
	{
		manager->reordered = 0;
		table = cuddHashTableInit( manager, 1, 2 );

		/* permute the output functions one-by-one */
		for ( i = 0; i < nNodes; i++ )
		{
			bNodesOut[i] = cuddBddPermuteRecur( manager, table, bNodesIn[i], permut );
			if ( bNodesOut[i] == NULL )
			{
				/* deref the array of the already computed outputs */
				for ( k = 0; k < i; k++ )
					Cudd_RecursiveDeref( manager, bNodesOut[k] );
				break;
			}
			cuddRef( bNodesOut[i] );
		}
		/* Dispose of local cache. */
		cuddHashTableQuit( table );
	}
	while ( manager->reordered == 1 );
}	/* end of Extra_bddPermuteArray */


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

  Synopsis    [Performs the boolean difference w.r.t to a cube (AKA unique quontifier).]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
DdNode *
Extra_bddBooleanDiffCube( DdManager * dd, DdNode * bFunc, DdNode * bCube )
{
	DdNode * bRes;
	if ( bCube == b1 )
		return bFunc;
	do
	{
		dd->reordered = 0;
		bRes = extraBddBooleanDiffCube( dd, Cudd_Regular(bFunc), bCube );
	}
	while ( dd->reordered == 1 );
	return bRes;
}								/* end of Extra_bddBooleanDiffCube */


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

  Synopsis    [Takes the BDD and the permutation array. Returns the ADD.]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
DdNode * 
Extra_bddPermuteToAdd( DdManager * dd, DdNode * bFunc, int * Permute )
{
	DdNode * aRes;
	st_generator * gen;
	DdNode * bNode, * aNode;
	st_table *  Visited;
	DdNode ** paVars;
	int i;

	// start the visited table
	Visited = st_init_table(st_ptrcmp,st_ptrhash);
	// prepare the array of ADD vars
	paVars = ALLOC( DdNode *, dd->size );
	for ( i = 0; i < dd->size; i++ )
	{
		paVars[i] =	cuddUniqueInter( dd, i, a1, a0 ); cuddRef( paVars[i] );
	}

	aRes = extraBddPermuteToAdd( dd, bFunc, Permute, Visited, paVars ); cuddRef( aRes );

//printf( "The number of cache entries = %d\n", st_count(Visited) );
	// remove the ADDs in cache
	st_foreach_item( Visited, gen, (char**)&bNode, (char**)&aNode) 
		Cudd_RecursiveDeref( dd, aNode );
	st_free_table(Visited);
	for ( i = 0; i < dd->size; i++ )
		Cudd_RecursiveDeref( dd, paVars[i] );
	free( paVars );

	cuddDeref( aRes );
	return aRes;
}

/*---------------------------------------------------------------------------*/
/* Definition of internal functions                                          */
/*---------------------------------------------------------------------------*/

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

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

  Description [Generates in a bottom-up fashion BDD for all combinations
               composed of k variables out of variables belonging to bVarsN.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
DdNode* extraBddTuples( 
  DdManager * dd,    /* the DD manager */
  DdNode * bVarsK,   /* the number of variables in tuples */
  DdNode * bVarsN)   /* the set of all variables */
{
	DdNode *bRes, *bRes0, *bRes1;
    statLine(dd); 

	/* terminal cases */
/*	if ( k < 0 || k > n )
 *		return dd->zero;
 *	if ( n == 0 )
 *		return dd->one; 
 */
	if ( cuddI( dd, bVarsK->index ) < cuddI( dd, bVarsN->index ) )
		return b0;
	if ( bVarsN == b1 )
		return b1;

    /* check cache */
    bRes = cuddCacheLookup2(dd, extraBddTuples, bVarsK, bVarsN);
    if (bRes)
    	return(bRes);

	/* ZDD in which is variable is 0 */
/*	bRes0 = extraBddTuples( dd, k,     n-1 ); */
	bRes0 = extraBddTuples( dd, bVarsK, cuddT(bVarsN) );
	if ( bRes0 == NULL ) 
		return NULL;
	cuddRef( bRes0 );

	/* ZDD in which is variable is 1 */
/*	bRes1 = extraBddTuples( dd, k-1,          n-1 ); */
	if ( bVarsK == b1 )