extraaddmisc.c

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

/**CFile****************************************************************

  FileName    [extraAddMisc.c]

  PackageName [extra]

  Synopsis    [Various ADD manipulating procedures.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - February 1, 2003.]

  Revision    [$Id: extraAddMisc.c,v 1.2 2003/05/27 23:14:37 alanmi Exp $]

***********************************************************************/

#include "util.h"
#include "cuddInt.h"
#include "time.h"
#include "extra.h"

/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Stucture declarations                                                     */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Macro declarations                                                        */
/*---------------------------------------------------------------------------*/


/**AutomaticStart*************************************************************/

/*---------------------------------------------------------------------------*/
/* Static function prototypes                                                */
/*---------------------------------------------------------------------------*/

/**AutomaticEnd***************************************************************/


/*---------------------------------------------------------------------------*/
/* Definition of exported functions                                          */
/*---------------------------------------------------------------------------*/

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

  Synopsis    [Remaps the function to depend on the topmost variables on the manager.]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
DdNode * Extra_addRemapUp(
  DdManager * dd,
  DdNode * aF )
{
	static int Permute[MAXINPUTS];
	DdNode * bSupp, * bTemp, * aRes;
	int Counter;

	// get support
	bSupp = Cudd_Support( dd, aF );    Cudd_Ref( bSupp );

	// create the variable map
	// to remap the DD into the upper part of the manager
	Counter = 0;
	for ( bTemp = bSupp; bTemp != b1; bTemp = cuddT(bTemp) )
		Permute[bTemp->index] = dd->invperm[Counter++];

	// transfer the BDD and remap it
	aRes = Cudd_addPermute( dd, aF, Permute );  Cudd_Ref( aRes );

	// remove support
	Cudd_RecursiveDeref( dd, bSupp );

	// return
	Cudd_Deref( aRes );
	return aRes;
}

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

  Synopsis    [Counts the number of different constant nodes of the ADD.]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
int Extra_addCountConst(
  DdManager * dd,
  DdNode * aFunc )
{
	DdGen * genDD;
	DdNode * node;
	int Count = 0;

	/* iterate through the nodes */
	Cudd_ForeachNode( dd, aFunc, genDD, node )
	{
		if ( Cudd_IsConstant(node) )
			Count++;
	}
	return Count;
}


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

  Synopsis    [Counts the number of different constant nodes of the array of ADDs.]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
int Extra_addCountConstArray(
  DdManager * dd,
  DdNode ** paFuncs,
  int nFuncs )
{
	st_table * Visited;
	st_generator * gen;
	DdNode * aNode;
	int i, Count = 0;
	assert( nFuncs > 0 );

	// start the table
	Visited = st_init_table( st_ptrcmp, st_ptrhash );

	// collect the unique nodes in the shared ADD
	for ( i = 0; i < nFuncs; i++ )
		cuddCollectNodes( Cudd_Regular( paFuncs[i] ), Visited );

	// count the unique terminals
	st_foreach_item( Visited, gen, (char**)&aNode, NULL) 
	{
		if ( Cudd_IsConstant(aNode) )
			Count++;
	}

	// deref the visited table
	st_free_table( Visited );
	return Count;
}

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

  Synopsis    [Return the encoded set of absolute values of the constant nodes of an ADD.]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
DdNode * Extra_bddAddConstants(
  DdManager * dd,
  DdNode * aFunc )
{
	st_table * Visited;
	st_generator * gen;
	DdNode * aNode, * bRes, * bTemp, * bCube;
	int nVars;

	// start the table
	Visited = st_init_table( st_ptrcmp, st_ptrhash );

	// collect the unique nodes in the ADD
	cuddCollectNodes( Cudd_Regular(aFunc), Visited );

	nVars = Cudd_SupportSize( dd, aFunc );

	// start the set of encoded constants
	bRes = b0;  Cudd_Ref( bRes );
	st_foreach_item( Visited, gen, (char**)&aNode, NULL) 
	{
		if ( Cudd_IsConstant(aNode) )
		{
			bCube = Extra_bddBitsToCube( dd, (int)ddAbs(cuddV(aNode)), nVars, NULL );  Cudd_Ref( bCube );
			bRes  = Cudd_bddOr( dd, bCube, bTemp = bRes );                            Cudd_Ref( bRes );
			Cudd_RecursiveDeref( dd, bTemp );
			Cudd_RecursiveDeref( dd, bCube );
		}
	}

	// deref the visited table
	st_free_table( Visited );

	Cudd_Deref( bRes );
	return bRes;
} /* end of Extra_bddAddConstants */


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

  Synopsis    [Restructure the ADD by replacing negative terminals with their abs value.]

  Description []

  SideEffects []

  SeeAlso     [Cudd_addMonadicApply]

******************************************************************************/
DdNode * Cudd_addAbs( DdManager * dd, DdNode * f )
{
	if ( cuddIsConstant( f ) )
	{
		CUDD_VALUE_TYPE value = cuddV( f );
		if ( value < 0 )	value = -value;
		return cuddUniqueConst( dd, value );
	}
	return ( NULL );

}								/* end of Cudd_addAbs */


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

  Synopsis    [Finds the minimum discriminant of the array of ADDs.]

  Description [Returns a pointer to a constant ADD.]

  SideEffects [None]

******************************************************************************/
DdNode * Extra_addFindMinArray( DdManager * dd, DdNode ** paFuncs, int nFuncs )
{
	DdNode * aRes, * aCur;
	int i;
	assert( nFuncs > 0 );

	aRes = Cudd_addFindMin( dd, paFuncs[0] );
	for ( i = 1; i < nFuncs; i++ )
	{
		aCur = Cudd_addFindMin( dd, paFuncs[i] );
		aRes = ( cuddV(aRes) <= cuddV(aCur) ) ? aRes: aCur;
	}

	return aRes;
}  /* end of Extra_addFindMinArray */


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

  Synopsis    [Finds the maximum discriminant of the array of ADDs.]

  Description [Returns a pointer to a constant ADD.]

  SideEffects [None]

******************************************************************************/
DdNode * Extra_addFindMaxArray( DdManager * dd, DdNode ** paFuncs, int nFuncs )
{
	DdNode * aRes, * aCur;
	int i;
	assert( nFuncs > 0 );

	aRes = Cudd_addFindMax( dd, paFuncs[0] );
	for ( i = 1; i < nFuncs; i++ )
	{
		aCur = Cudd_addFindMax( dd, paFuncs[i] );
		aRes = ( cuddV(aRes) >= cuddV(aCur) ) ? aRes: aCur;
	}

	return aRes;
}  /* end of Extra_addFindMinArray */


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

  Synopsis    [Absolute value of an ADD.]

  Description [Absolute value of an ADD. Returns NULL if not a terminal case; 
  abs(f) otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_addMonadicApply]

******************************************************************************/
DdNode * Extra_addAbs( DdManager * dd, DdNode * f )
{
	if ( cuddIsConstant( f ) )
	{
		CUDD_VALUE_TYPE value = ( cuddV( f ) > 0 )? cuddV( f ): -cuddV( f );
		DdNode *res = cuddUniqueConst( dd, value );
		return ( res );
	}
	return ( NULL );

} /* end of Extra_addAbs */


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

  Synopsis    [Determines whether this is an ADD or a BDD.]

  Description [Returns 1, if the function is an ADD; 0, if the function is a BDD; -1, if unknown.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
int Extra_addDetectAdd( DdManager * dd, DdNode * Func )
{
	int RetValue;

	if ( Cudd_IsComplement(Func) )
		return 0;
	if ( Func == dd->one )
		return -1;
	if ( Func == dd->zero )
		return 1;

	// treat the case of MTBDD (it may have some strange terminal nodes)
	if ( Cudd_IsConstant(Func) )
		return 1;

	RetValue = Extra_addDetectAdd( dd, cuddE(Func) );
	if ( RetValue == 1 )
		return 1;
	if ( RetValue == 0 )
		return 0;
	return Extra_addDetectAdd( dd, cuddT(Func) );
}