extrabddmisc.c

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

	{
		bRes1 = b0;
		cuddRef( bRes1 );
	}
	else
	{
		bRes1 = extraBddTuples( dd, cuddT(bVarsK), cuddT(bVarsN) );
		if ( bRes1 == NULL ) 
		{
			Cudd_RecursiveDeref( dd, bRes0 );
			return NULL;
		}
		cuddRef( bRes1 );
	}

	/* consider the case when Res0 and Res1 are the same node */
	if ( bRes0 == bRes1 )
		bRes = bRes1;
	/* consider the case when Res1 is complemented */
	else if ( Cudd_IsComplement(bRes1) ) 
	{
		bRes = cuddUniqueInter(dd, bVarsN->index, Cudd_Not(bRes1), Cudd_Not(bRes0));
		if ( bRes == NULL ) 
		{
			Cudd_RecursiveDeref(dd,bRes0);
			Cudd_RecursiveDeref(dd,bRes1);
			return NULL;
		}
		bRes = Cudd_Not(bRes);
	} 
	else 
	{
		bRes = cuddUniqueInter( dd, bVarsN->index, bRes1, bRes0 );
		if ( bRes == NULL ) 
		{
			Cudd_RecursiveDeref(dd,bRes0);
			Cudd_RecursiveDeref(dd,bRes1);
			return NULL;
		}
	}
	cuddDeref( bRes0 );
	cuddDeref( bRes1 );

	/* insert the result into cache */
	cuddCacheInsert2(dd, extraBddTuples, bVarsK, bVarsN, bRes);
	return bRes;

} /* end of extraBddTuples */


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

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

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
DdNode* extraBddChangePolarity( 
  DdManager * dd,    /* the DD manager */
  DdNode * bFunc, 
  DdNode * bVars) 
{
	DdNode * bRes;

	if ( bVars == b1 )
		return bFunc;
	if ( Cudd_IsConstant(bFunc) )
		return bFunc;

    if ( bRes = cuddCacheLookup2(dd, extraBddChangePolarity, bFunc, bVars) )
    	return bRes;
	else
	{
		DdNode * bFR = Cudd_Regular(bFunc); 
		int LevelF   = dd->perm[bFR->index];
		int LevelV   = dd->perm[bVars->index];

		if ( LevelV < LevelF )
			bRes = extraBddChangePolarity( dd, bFunc, cuddT(bVars) );
		else // if ( LevelF <= LevelV )
		{
			DdNode * bRes0, * bRes1;             
			DdNode * bF0, * bF1;             
			DdNode * bVarsNext;

			// cofactor the functions
			if ( bFR != bFunc ) // bFunc is complemented 
			{
				bF0 = Cudd_Not( cuddE(bFR) );
				bF1 = Cudd_Not( cuddT(bFR) );
			}
			else
			{
				bF0 = cuddE(bFR);
				bF1 = cuddT(bFR);
			}

			if ( LevelF == LevelV )
				bVarsNext = cuddT(bVars);
			else
				bVarsNext = bVars;

			bRes0 = extraBddChangePolarity( dd, bF0, bVarsNext );
			if ( bRes0 == NULL ) 
				return NULL;
			cuddRef( bRes0 );

			bRes1 = extraBddChangePolarity( dd, bF1, bVarsNext );
			if ( bRes1 == NULL ) 
			{
				Cudd_RecursiveDeref( dd, bRes0 );
				return NULL;
			}
			cuddRef( bRes1 );

			if ( LevelF == LevelV )
			{ // swap the cofactors
				DdNode * bTemp;
				bTemp = bRes0;
				bRes0 = bRes1;
				bRes1 = bTemp;
			}

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

			/* consider the case when Res0 and Res1 are the same node */
			if ( bRes0 == bRes1 )
				bRes = bRes1;
			/* consider the case when Res1 is complemented */
			else if ( Cudd_IsComplement(bRes1) ) 
			{
				bRes = cuddUniqueInter(dd, bFR->index, Cudd_Not(bRes1), Cudd_Not(bRes0));
				if ( bRes == NULL ) 
				{
					Cudd_RecursiveDeref(dd,bRes0);
					Cudd_RecursiveDeref(dd,bRes1);
					return NULL;
				}
				bRes = Cudd_Not(bRes);
			} 
			else 
			{
				bRes = cuddUniqueInter( dd, bFR->index, bRes1, bRes0 );
				if ( bRes == NULL ) 
				{
					Cudd_RecursiveDeref(dd,bRes0);
					Cudd_RecursiveDeref(dd,bRes1);
					return NULL;
				}
			}
			cuddDeref( bRes0 );
			cuddDeref( bRes1 );
		}
			
		/* insert the result into cache */
		cuddCacheInsert2(dd, extraBddChangePolarity, bFunc, bVars, bRes);
		return bRes;
	}
} /* end of extraBddChangePolarity */


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

  Synopsis    [Performs the recursive steps of Extra_bddBooleanDiffCube.]

  Description [Performs the recursive steps of Extra_bddBooleanDiffCube.
  Returns the BDD obtained by XORing the cofactors of bFunc with respect to
  all the variables in bCube; NULL otherwise. Exploits the fact that dF/dx =
  dF'/dx.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
DdNode *
extraBddBooleanDiffCube( DdManager * dd, DdNode * bFunc, DdNode * bCube )
{
	DdNode * bRes;
	int LevelF;
	int LevelV;

	statLine( dd );

	assert( bCube != b1 );
	if ( cuddIsConstant(bFunc) )
		return b0;
	// from now on, bFunc and bCube are non-constants

	LevelF = dd->perm[bFunc->index];
	LevelV = dd->perm[bCube->index];
	// if bCube contains a variable not in bFunc, the EXOR of two identical cofactors is zero
	if ( LevelF > LevelV )
		return b0;

	if ( bRes = cuddCacheLookup2( dd, extraBddBooleanDiffCube, bFunc, bCube ) )
		return bRes;
	else
	{
		DdNode * bF0,   * bF1;
		DdNode * bRes0, * bRes1;

		// cofactor the function
		bF0 = cuddE(bFunc);
		bF1 = cuddT(bFunc);

		if ( LevelF == LevelV )
		{
			if ( cuddT(bCube) == b1 )
				bRes0 = bF0;
			else
				bRes0 = extraBddBooleanDiffCube( dd, Cudd_Regular(bF0), cuddT(bCube) );
			if ( bRes0 == NULL ) 
				return NULL;
			cuddRef( bRes0 );

			if ( cuddT(bCube) == b1 )
				bRes1 = bF1;
			else
				bRes1 = extraBddBooleanDiffCube( dd, bF1, cuddT(bCube) );
			if ( bRes1 == NULL ) 
			{
				Cudd_RecursiveDeref( dd, bRes0 );
				return NULL;
			}
			cuddRef( bRes1 );

			bRes = cuddBddXorRecur( dd, bRes0, bRes1 );
			if ( bRes == NULL ) 
			{
				Cudd_RecursiveDeref( dd, bRes0 );
				Cudd_RecursiveDeref( dd, bRes1 );
				return NULL;
			}
			cuddRef( bRes );
			Cudd_RecursiveDeref( dd, bRes0 );
			Cudd_RecursiveDeref( dd, bRes1 );
			cuddDeref( bRes );
		}
		else //if ( LevelF < LevelV )
		{
			bRes0 = extraBddBooleanDiffCube( dd, Cudd_Regular(bF0), bCube );
			if ( bRes0 == NULL ) 
				return NULL;
			cuddRef( bRes0 );

			bRes1 = extraBddBooleanDiffCube( dd, bF1, bCube );
			if ( bRes1 == NULL ) 
			{
				Cudd_RecursiveDeref( dd, bRes0 );
				return NULL;
			}
			cuddRef( bRes1 );

			// consider the case when bRes0 and bRes1 are the same node 
			if ( bRes0 == bRes1 )
				bRes = bRes1;
			// consider the case when Res1 is complemented 
			else if ( Cudd_IsComplement(bRes1) ) 
			{
				bRes = cuddUniqueInter(dd, bFunc->index, Cudd_Not(bRes1), Cudd_Not(bRes0));
				if ( bRes == NULL ) 
				{
					Cudd_RecursiveDeref(dd,bRes0);
					Cudd_RecursiveDeref(dd,bRes1);
					return NULL;
				}
				bRes = Cudd_Not(bRes);
			} 
			else 
			{
				bRes = cuddUniqueInter( dd, bFunc->index, bRes1, bRes0 );
				if ( bRes == NULL ) 
				{
					Cudd_RecursiveDeref(dd,bRes0);
					Cudd_RecursiveDeref(dd,bRes1);
					return NULL;
				}
			}
			cuddDeref( bRes0 );
			cuddDeref( bRes1 );
		}
	}

	cuddCacheInsert2( dd, extraBddBooleanDiffCube, bFunc, bCube, bRes );
	return bRes;

}								/* end of extraBddBooleanDiffCube */


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

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

  Synopsis    [Performs the recursive step of Extra_ProfileNode().]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
void ddProfileNode( DdManager * dd, DdNode * F, int * Profile, st_table * Visited )
// call with the regular pointer
{
	if ( F->index != CUDD_CONST_INDEX )
	{
		if ( st_lookup(Visited, (char*)F, NULL) )
		{
			// the entry already exists
			return; 
		}

		// insert the entry
		st_insert(Visited, (char*)F, NULL);

		// this node has not been visited
		Profile[dd->perm[F->index]]++;

		ddProfileNode( dd, Cudd_Regular(cuddE(F)), Profile, Visited );
		ddProfileNode( dd, cuddT(F), Profile, Visited );
	}
} /* end of ddProfileNode */


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

  Synopsis    [Performs the recursive step of Extra_ProfileEdge().]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
void ddProfileEdge( DdManager * dd, DdNode * F, int * Profile, st_table * Visited )
// call with the regular pointer
{
	if ( F->index != CUDD_CONST_INDEX )
	{
		DdNode * bF0R, * bF1R;
		int Lev, Lev0, Lev1;
		int Length0, Length1;

		if ( st_lookup(Visited, (char*)F, NULL) )
		{
			// the entry already exists
			return; 
		}

		// insert the entry
		st_insert(Visited, (char*)F, NULL);


		// compute the cofactors
		bF0R = Cudd_Regular(cuddE(F));
		bF1R = cuddT(F);
		Lev  = cuddI(dd,F->index);
		Lev0 = cuddI(dd,bF0R->index);
		Lev1 = cuddI(dd,bF1R->index);
		Length0 = ddMin( Lev0-Lev, dd->size-1 );
		Length1 = ddMin( Lev1-Lev, dd->size-1 );

		// this node has not been visited
		Profile[Length0]++;
		Profile[Length1]++;

		ddProfileEdge( dd, Cudd_Regular(cuddE(F)), Profile, Visited );
		ddProfileEdge( dd, cuddT(F), Profile, Visited );
	}
} /* end of ddProfileEdge */



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

  Synopsis    [Implements the recursive step of Cudd_bddPermute.]

  Description [ Recursively puts the BDD in the order given in the array permut.
  Checks for trivial cases to terminate recursion, then splits on the
  children of this node.  Once the solutions for the children are
  obtained, it puts into the current position the node from the rest of
  the BDD that should be here. Then returns this BDD.
  The key here is that the node being visited is NOT put in its proper
  place by this instance, but rather is switched when its proper position
  is reached in the recursion tree.<p>
  The DdNode * that is returned is the same BDD as passed in as node,
  but in the new order.]

  SideEffects [None]

  SeeAlso     [Cudd_bddPermute cuddAddPermuteRecur]

******************************************************************************/
static DdNode *
cuddBddPermuteRecur( DdManager * manager /* DD manager */ ,
					 DdHashTable * table /* computed table */ ,
					 DdNode * node /* BDD to be reordered */ ,
					 int *permut /* permutation array */  )
{
	DdNode *N, *T, *E;
	DdNode *res;
	int index;

	statLine( manager );
	N = Cudd_Regular( node );

	/* Check for terminal case of constant node. */
	if ( cuddIsConstant( N ) )
	{
		return ( node );
	}

	/* If problem already solved, look up answer and return. */
	if ( N->ref != 1 && ( res = cuddHashTableLookup1( table, N ) ) != NULL )
		return ( Cudd_NotCond( res, N != node ) );

	/* Split and recur on children of this node. */
	T = cuddBddPermuteRecur( manager, table, cuddT( N ), permut );
	if ( T == NULL )
		return ( NULL );
	cuddRef( T );
	E = cuddBddPermuteRecur( manager, table, cuddE( N ), permut );
	if ( E == NULL )
	{
		Cudd_IterDerefBdd( manager, T );
		return ( NULL );
	}
	cuddRef( E );

	/* Move variable that should be in this position to this position
	   ** by retrieving the single var BDD for that variable, and calling
	   ** cuddBddIteRecur with the T and E we just created.
	 */
	index = permut[N->index];
	res = cuddBddIteRecur( manager, manager->vars[index], T, E );
	if ( res == NULL )
	{
		Cudd_IterDerefBdd( manager, T );
		Cudd_IterDerefBdd( manager, E );
		return ( NULL );
	}
	cuddRef( res );
	Cudd_IterDerefBdd( manager, T );
	Cudd_IterDerefBdd( manager, E );

	/* Do not keep the result if the reference count is only 1, since
	   ** it will not be visited again.
	 */
	if ( N->ref != 1 )
	{
		ptrint fanout = ( ptrint ) N->ref;
		cuddSatDec( fanout );
		if ( !cuddHashTableInsert1( table, N, res, fanout ) )
		{
			Cudd_IterDerefBdd( manager, res );
			return ( NULL );
		}
	}
	cuddDeref( res );
	return ( Cudd_NotCond( res, N != node ) );

}								/* end of cuddBddPermuteRecur */


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

  Synopsis    [Performs the recursive step of Extra_bddPermuteToAdd.]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
DdNode * extraBddPermuteToAdd( DdManager * dd, DdNode * bFunc, int * Permute, st_table * Visited, DdNode ** paVars )
{
	DdNode * aRes, * aRes0, * aRes1;
	DdNode * bFuncR;

	// check for terminals
	if ( bFunc == b0 )
		return a0;
	if ( bFunc == b1 )
		return a1;

	bFuncR = Cudd_Regular( bFunc );
	if ( bFuncR->ref != 1 ) 
	{
		if ( st_lookup( Visited, (char*)bFunc, (char**)&aRes ) )
			return aRes;
	}
	// else, this BDD is pointed only once and we came here, 
	// so we did not visit it before and will not visit it again

	// solve recursively
	aRes0 = extraBddPermuteToAdd( dd, cuddE(bFuncR), Permute, Visited, paVars );
	if ( aRes0 == NULL )
		return NULL;
	cuddRef( aRes0 );
	aRes1 = extraBddPermuteToAdd( dd, cuddT(bFuncR), Permute, Visited, paVars );
	if ( aRes1 == NULL )
	{
		Cudd_RecursiveDeref( dd, aRes0 );
		return NULL;
	}
	cuddRef( aRes1 );

	// compose
	aRes = cuddAddIteRecur( dd, paVars[Permute[bFuncR->index]], aRes1, aRes0 );
	if ( aRes == NULL )
	{
		Cudd_RecursiveDeref( dd, aRes0 );
		Cudd_RecursiveDeref( dd, aRes1 );
		return ( NULL );
	}
	cuddRef( aRes );
	Cudd_RecursiveDeref( dd, aRes0 );
	Cudd_RecursiveDeref( dd, aRes1 );

	if ( bFuncR != bFunc ) 
	{
		DdNode * aTemp;
		aRes = cuddAddCmplRecur( dd, aTemp = aRes );  cuddRef( aRes );
		Cudd_RecursiveDeref( dd, aTemp );
	}

	if ( bFuncR->ref != 1 ) 
		st_insert( Visited, (char*)bFunc, (char*)aRes ); // reference the entry in cache
	else
		cuddDeref( aRes );
	return aRes;
}