extrabddsupp.c

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

******************************************************************************/
int *
Extra_VectorSupportArray( 
  DdManager * dd, /* manager */ 
  DdNode ** F, /* array of DDs whose support is sought */ 
  int n, /* size of the array */  
  int * support ) /* array allocated by the user */
{
	int i, size;

	/* Allocate and initialize support array for ddSupportStep. */
	size = ddMax( dd->size, dd->sizeZ );
	for ( i = 0; i < size; i++ )
		support[i] = 0;

	/* Compute support and clean up markers. */
	for ( i = 0; i < n; i++ )
		ddSupportStep( Cudd_Regular(F[i]), support );
	for ( i = 0; i < n; i++ )
		ddClearFlag( Cudd_Regular(F[i]) );

    return support;
}


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

  Synopsis    [This procedure computes the node count and support size at the same time]

  Description []

  SideEffects [Uses static variables defined on top of the file.]

  SeeAlso     [Cudd_DagSize Cudd_Support Cudd_SupportSize]

******************************************************************************/
int Extra_DagSizeSuppSize( DdNode * node, int * pnSuppSize )
{
	int nNodeCount;
	int nSuppSize;

	// set a new signature to distinquish this call from other calls
	s_UniqueCounter++;
	nSuppSize = 0;
	nNodeCount = ddDagSizeSuppSizeStep( Cudd_Regular(node), &nSuppSize );
	ddClearFlag( Cudd_Regular(node) );

	*pnSuppSize = nSuppSize;
	return nNodeCount;
}								/* end of Extra_DagSizeSuppSize */


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

  Synopsis    [Finds the support and writes it in cache.]

  Description [Finds the variables on which a DD depends.
  Returns an ADD consisting of the product of the variables in the positive polarity if
  successful; NULL otherwise.]

  SideEffects [Should not be used with ZDD.]

  SeeAlso     [Cudd_VectorSupport Cudd_Support]

******************************************************************************/
DdNode * Extra_SupportCache( DdManager * dd, DdNode * f )
{
	DdNode * bRes;
    if ( bRes = cuddCacheLookup1(dd, Extra_SupportCache, f) )
		return bRes;
	bRes = Cudd_Support( dd, f );
    cuddCacheInsert1(dd, Extra_SupportCache, f, bRes);
	return bRes;
}

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

  Synopsis    [Finds variables on which the DD depends and returns them as a ZDD.]

  Description [Finds the variables on which the DD depends.
  Returns a ZDD consisting of the combination of the variables if
  successful; NULL otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_Support Cudd_VectorSupport Cudd_ClassifySupport]

******************************************************************************/
DdNode *
Extra_zddSupport(
  DdManager * dd /* manager */,
  DdNode * f     /* DD whose support is sought */)
{
    int	*support;
    DdNode *res;
    int	i, size;

    /* Allocate and initialize support array for ddSupportStep. */
    size = ddMax(dd->size, dd->sizeZ);
    support = ALLOC(int,size);
    if (support == NULL) {
		dd->errorCode = CUDD_MEMORY_OUT;
		return(NULL);
    }
    for (i = 0; i < size; i++) 
		support[i] = 0;
    

    /* Compute support and clean up markers. */
    ddSupportStep(Cudd_Regular(f),support);
    ddClearFlag(Cudd_Regular(f));

    /* Transform support from array to cube. */
	res = Extra_zddCombination( dd, support, size );

    FREE(support);
    return(res);

} /* end of Extra_zddSupport */


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

  Synopsis    [Finds the support as a negative polarity cube.]

  Description [Finds the variables on which a DD depends. Returns a BDD 
  consisting of the product of the variables in the negative polarity 
  if successful; NULL otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_VectorSupport Cudd_Support]

******************************************************************************/
DdNode * Extra_bddSupportNegativeCube( DdManager * dd, DdNode * f )
{
	int *support;
	DdNode *res, *tmp, *var;
	int i, j;
	int size;

	/* Allocate and initialize support array for ddSupportStep. */
	size = ddMax( dd->size, dd->sizeZ );
	support = ALLOC( int, size );
	if ( support == NULL )
	{
		dd->errorCode = CUDD_MEMORY_OUT;
		return ( NULL );
	}
	for ( i = 0; i < size; i++ )
	{
		support[i] = 0;
	}

	/* Compute support and clean up markers. */
	ddSupportStep( Cudd_Regular( f ), support );
	ddClearFlag( Cudd_Regular( f ) );

	/* Transform support from array to cube. */
	do
	{
		dd->reordered = 0;
		res = DD_ONE( dd );
		cuddRef( res );
		for ( j = size - 1; j >= 0; j-- )
		{						/* for each level bottom-up */
			i = ( j >= dd->size ) ? j : dd->invperm[j];
			if ( support[i] == 1 )
			{
				var = cuddUniqueInter( dd, i, dd->one, Cudd_Not( dd->one ) );
				//////////////////////////////////////////////////////////////////
				var = Cudd_Not(var);
				//////////////////////////////////////////////////////////////////
				cuddRef( var );
				tmp = cuddBddAndRecur( dd, res, var );
				if ( tmp == NULL )
				{
					Cudd_RecursiveDeref( dd, res );
					Cudd_RecursiveDeref( dd, var );
					res = NULL;
					break;
				}
				cuddRef( tmp );
				Cudd_RecursiveDeref( dd, res );
				Cudd_RecursiveDeref( dd, var );
				res = tmp;
			}
		}
	}
	while ( dd->reordered == 1 );

	FREE( support );
	if ( res != NULL )
		cuddDeref( res );
	return ( res );

}								/* end of Extra_SupportNeg */


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

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


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

  Synopsis    [Performs the recursive step of Extra_zddSupport.]

  Description [Performs the recursive step of Extra_Support. Performs a
  DFS from f. The support is accumulated in supp as a side effect. Uses
  the LSB of the then pointer as visited flag.]

  SideEffects [None]

  SeeAlso     [ddClearFlag]

******************************************************************************/
static int ddDagSizeSuppSizeStep( DdNode * n, int * pnSuppSize )
{
	int tval, eval;

	// check if this node has already been visited
	if ( Cudd_IsComplement( n->next ) )
		return 0;

	// mark this node as visited
	n->next = Cudd_Not( n->next );

	// check if this node is a constant (no support changes in this case)
	if ( cuddIsConstant( n ) )
		return 1;

	tval = ddDagSizeSuppSizeStep( cuddT(n), pnSuppSize );
	eval = ddDagSizeSuppSizeStep( Cudd_Regular( cuddE(n) ), pnSuppSize );

	// add to the support storage if necessary
	if ( s_nArrayAlloc <= n->index )
	{ // reallocate the array
		s_pArray      = REALLOC(unsigned, s_pArray, sizeof(unsigned) * (2 * n->index + 1000) );
		// clean the new part
		memset( s_pArray + s_nArrayAlloc, 0, sizeof(unsigned) * (2 * n->index + 1000 - s_nArrayAlloc) );
		// update the pointer to the new block
		s_nArrayAlloc = 2 * n->index + 1000;
	}
	// check if the given variable has been visited
	if ( s_pArray[n->index] != s_UniqueCounter )
	{
		// the variable is new - mark it as visited
		s_pArray[n->index] = s_UniqueCounter;
		// update the support counter
		(*pnSuppSize)++;
	}
	return ( 1 + tval + eval );
}								/* end of ddDagSizeSuppSizeStep */


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

  Synopsis    [Performs the recursive step of Extra_zddSupport.]

  Description [Performs the recursive step of Extra_Support. Performs a
  DFS from f. The support is accumulated in supp as a side effect. Uses
  the LSB of the then pointer as visited flag.]

  SideEffects [None]

  SeeAlso     [ddClearFlag]

******************************************************************************/
static void
ddSupportStep(
  DdNode * f,
  int * support)
{
    if (cuddIsConstant(f) || Cudd_IsComplement(f->next)) {
	return;
    }

    support[f->index] = 1;
    ddSupportStep(cuddT(f),support);
    ddSupportStep(Cudd_Regular(cuddE(f)),support);
    /* Mark as visited. */
    f->next = Cudd_Not(f->next);
    return;

} /* end of ddSupportStep */


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

  Synopsis    [Performs a DFS from f, clearing the LSB of the next
  pointers.]

  Description []

  SideEffects [None]

  SeeAlso     [ddSupportStep ddDagInt]

******************************************************************************/
static void
ddClearFlag(
  DdNode * f)
{
    if (!Cudd_IsComplement(f->next)) {
	return;
    }
    /* Clear visited flag. */
    f->next = Cudd_Regular(f->next);
    if (cuddIsConstant(f)) {
	return;
    }
    ddClearFlag(cuddT(f));
    ddClearFlag(Cudd_Regular(cuddE(f)));
    return;

} /* end of ddClearFlag */