extraddtimed.c

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

{
	DdNode *T, *E, *res, *res1, *res2;

	// quit because of timeout or spaceout
	if ( s_Timeout && clock() > s_TimeLimit )
	{
//		printf( "t" );
		return NULL;
	}
	if ( s_KeysAllowedIncrease && (int)manager->keys > s_KeysLimit )
	{
//		printf( "s" );
		return NULL;
	}

	statLine( manager );
	if ( cuddI( manager, f->index ) > manager->perm[var->index] )
	{
		/* f does not depend on var. */
		return ( Cudd_Not( DD_ONE( manager ) ) );
	}

	/* From now on, f is non-constant. */

	/* If the two indices are the same, so are their levels. */
	if ( f->index == var->index )
	{
		res = cuddBddXorRecur( manager, cuddT( f ), cuddE( f ) );
		return ( res );
	}

	/* From now on, cuddI(manager,f->index) < cuddI(manager,cube->index). */

	/* Check the cache. */
	res = cuddCacheLookup2( manager, extraBddBooleanDiffRecur, f, var );
	if ( res != NULL )
	{
		return ( res );
	}

	/* Compute the cofactors of f. */
	T = cuddT( f );
	E = cuddE( f );

	res1 = extraBddBooleanDiffRecur( manager, T, var );
	if ( res1 == NULL )
		return ( NULL );
	cuddRef( res1 );
	res2 = extraBddBooleanDiffRecur( manager, Cudd_Regular( E ), var );
	if ( res2 == NULL )
	{
		Cudd_IterDerefBdd( manager, res1 );
		return ( NULL );
	}
	cuddRef( res2 );
	/* ITE takes care of possible complementation of res1 and of the
	   ** case in which res1 == res2. */
	res = cuddBddIteRecur( manager, manager->vars[f->index], res1, res2 );
	if ( res == NULL )
	{
		Cudd_IterDerefBdd( manager, res1 );
		Cudd_IterDerefBdd( manager, res2 );
		return ( NULL );
	}
	cuddDeref( res1 );
	cuddDeref( res2 );
	cuddCacheInsert2( manager, extraBddBooleanDiffRecur, f, var, res );
	return ( res );

}								/* end of extraBddBooleanDiffRecur */

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

  Synopsis    [Performs the recursive step of the alternative ISOP computation.]

  Description []

  SideEffects []

  SeeAlso     [Extra_zddIsopCover]

******************************************************************************/
DdNode* extraZddIsopCoverAltTimed( 
  DdManager * dd,     /* the DD manager */
  DdNode * bA,        /* the on-set */
  DdNode * bB)        /* the on-set + dc-set */
{
    DdNode	*zRes;
    statLine(dd); 

	// quit because of timeout or spaceout
	if ( s_Timeout && clock() > s_TimeLimit )
	{
//		printf( "t" );
		return NULL;
	}
	if ( s_KeysAllowedIncrease && (int)dd->keys > s_KeysLimit )
	{
//		printf( "s" );
		return NULL;
	}

	/* if there is no area (the cover should be empty), there is nowhere to expand */
	if ( bA == b0 )    return z0;
	/* if the area is the total boolean space, the cover is expanded into a single large cube */
	if ( bB == b1 )    return z1;

    /* check cache */
    zRes = cuddCacheLookup2Zdd(dd, extraZddIsopCoverAltTimed, bA, bB);
    if (zRes)
		return zRes;
	else
	{
		DdNode *bA0, *bA1, *bB0, *bB1, *bG0, *bG1, *bHA, *bHB;
		DdNode *zRes0, *zRes1, *zRes2;

		DdNode *bAA = Cudd_Regular(bA);
		DdNode *bBB = Cudd_Regular(bB);

		int LevA = dd->perm[bAA->index];
		int LevB = dd->perm[bBB->index];

		/* the index of the positive ZDD variable in the result */
		int TopVar;

		if ( LevA <= LevB )
		{
			int fIsComp = (int)(bA != bAA);
			bA0 = Cudd_NotCond( cuddE(bAA), fIsComp );
			bA1 = Cudd_NotCond( cuddT(bAA), fIsComp );
			TopVar = bAA->index;
		}
		else
			bA0 = bA1 = bA;

		if ( LevB <= LevA )
		{
			int fIsComp = (int)(bB != bBB);
			bB0 = Cudd_NotCond( cuddE(bBB), fIsComp );
			bB1 = Cudd_NotCond( cuddT(bBB), fIsComp );
			TopVar = bBB->index;
		}
		else
			bB0 = bB1 = bB;

		/* g0 = F1(x=0) & !F12(x=1) */
		bG0 = cuddBddAndRecur( dd, bA0, Cudd_Not(bB1) );
		if ( bG0 == NULL ) return NULL;
		cuddRef( bG0 );

		/* P0 = IrrCover( g0, F12(x=0) ) */
		zRes0 = extraZddIsopCoverAltTimed( dd, bG0, bB0 );
		if ( zRes0 == NULL )
		{
			Cudd_IterDerefBdd(dd, bG0);
			return NULL;
		}
		cuddRef( zRes0 );
		Cudd_IterDerefBdd(dd, bG0);


		/* g0 = F1(x=1) & !F12(x=0) */
		bG1 = cuddBddAndRecur( dd, bA1, Cudd_Not(bB0) );
		if ( bG1 == NULL )
		{
			Cudd_RecursiveDerefZdd(dd, zRes0);
			return NULL;
		}
		cuddRef( bG1 );

		/* P1 = IrrCover( g1, F12(x=1) ) */
		zRes1 = extraZddIsopCoverAltTimed( dd, bG1, bB1 );
		if ( zRes1 == NULL )
		{
			Cudd_IterDerefBdd(dd, bG1);
			Cudd_RecursiveDerefZdd(dd, zRes0);
			return NULL;
		}
		cuddRef( zRes1 );
		Cudd_IterDerefBdd(dd, bG1);

		/* h1 = F1(x=0) & !bdd(P0)  +   F1(x=1) & !bdd(P1) */
		bG0 = extraZddConvertToBddAndAdd( dd, zRes0, Cudd_Not(bA0) );
		if ( bG0 == NULL )
		{
			Cudd_RecursiveDerefZdd(dd, zRes0);
			Cudd_RecursiveDerefZdd(dd, zRes1);
			return NULL;
		}
		cuddRef( bG0 );

		bG1 = extraZddConvertToBddAndAdd( dd, zRes1, Cudd_Not(bA1) );
		if ( bG1 == NULL )
		{
			Cudd_IterDerefBdd(dd, bG0);
			Cudd_RecursiveDerefZdd(dd, zRes0);
			Cudd_RecursiveDerefZdd(dd, zRes1);
			return NULL;
		}
		cuddRef( bG1 );

		bHA = cuddBddAndRecur( dd, bG0, bG1 );
		if ( bHA == NULL )
		{
			Cudd_IterDerefBdd(dd, bG0);
			Cudd_IterDerefBdd(dd, bG1);
			Cudd_RecursiveDerefZdd(dd, zRes0);
			Cudd_RecursiveDerefZdd(dd, zRes1);
			return NULL;
		}
		cuddRef( bHA );
		bHA = Cudd_Not(bHA);
		Cudd_IterDerefBdd(dd, bG0);
		Cudd_IterDerefBdd(dd, bG1);

		/* h12 = F12(x=0) & F12(x=1) */
		bHB = cuddBddAndRecur( dd, bB0, bB1 );
		if ( bHB == NULL )
		{
			Cudd_IterDerefBdd(dd, bHA);
			Cudd_RecursiveDerefZdd(dd, zRes0);
			Cudd_RecursiveDerefZdd(dd, zRes1);
			return NULL;
		}
		cuddRef( bHB );

		/* P1 = IrrCover( h1, h12 ) */
		zRes2 = extraZddIsopCoverAltTimed( dd, bHA, bHB );
		if ( zRes2 == NULL )
		{
			Cudd_IterDerefBdd(dd, bHA);
			Cudd_IterDerefBdd(dd, bHB);
			Cudd_RecursiveDerefZdd(dd, zRes0);
			Cudd_RecursiveDerefZdd(dd, zRes1);
			return NULL;
		}
		cuddRef( zRes2 );
		Cudd_IterDerefBdd(dd, bHA);
		Cudd_IterDerefBdd(dd, bHB);

		/* --------------- compose the result ------------------ */
		zRes = extraComposeCover( dd, zRes0, zRes1, zRes2, TopVar );
		if ( zRes == NULL ) return NULL;

		/* insert the result into cache and return */
		cuddCacheInsert2(dd, extraZddIsopCoverAltTimed, bA, bB, zRes);
		return zRes;
	}
} /* end of extraZddIsopCoverAltTimed */


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

  Synopsis    [Performs the recursive step of the alternative ISOP computation.]

  Description []

  SideEffects []

  SeeAlso     [Extra_zddIsopCover]

******************************************************************************/
DdNode* extraZddIsopCoverAltLimited( 
  DdManager * dd,     /* the DD manager */
  DdNode * bA,        /* the on-set */
  DdNode * bB,        /* the on-set + dc-set */
  int * pnBTracks)
{
    DdNode	*zRes;
    statLine(dd); 

	/* if there is no area (the cover should be empty), there is nowhere to expand */
	if ( bA == b0 )    return z0;
	/* if the area is the total boolean space, the cover is expanded into a single large cube */
	if ( bB == b1 )    return z1;

	// quit because of the limit on the number of backtracks
	if ( --(*pnBTracks) < 0 )
		return NULL;

    /* check cache */
    zRes = cuddCacheLookup2Zdd(dd, extraZddIsopCoverAlt, bA, bB);
    if (zRes)
		return zRes;
	else
	{
		DdNode *bA0, *bA1, *bB0, *bB1, *bG0, *bG1, *bHA, *bHB;
		DdNode *zRes0, *zRes1, *zRes2;

		DdNode *bAA = Cudd_Regular(bA);
		DdNode *bBB = Cudd_Regular(bB);

		int LevA = dd->perm[bAA->index];
		int LevB = dd->perm[bBB->index];

		/* the index of the positive ZDD variable in the result */
		int TopVar;

		if ( LevA <= LevB )
		{
			int fIsComp = (int)(bA != bAA);
			bA0 = Cudd_NotCond( cuddE(bAA), fIsComp );
			bA1 = Cudd_NotCond( cuddT(bAA), fIsComp );
			TopVar = bAA->index;
		}
		else
			bA0 = bA1 = bA;

		if ( LevB <= LevA )
		{
			int fIsComp = (int)(bB != bBB);
			bB0 = Cudd_NotCond( cuddE(bBB), fIsComp );
			bB1 = Cudd_NotCond( cuddT(bBB), fIsComp );
			TopVar = bBB->index;
		}
		else
			bB0 = bB1 = bB;

		/* g0 = F1(x=0) & !F12(x=1) */
		bG0 = cuddBddAndRecur( dd, bA0, Cudd_Not(bB1) );
		if ( bG0 == NULL ) return NULL;
		cuddRef( bG0 );

		/* P0 = IrrCover( g0, F12(x=0) ) */
		zRes0 = extraZddIsopCoverAltLimited( dd, bG0, bB0, pnBTracks );
		if ( zRes0 == NULL )
		{
			Cudd_IterDerefBdd(dd, bG0);
			return NULL;
		}
		cuddRef( zRes0 );
		Cudd_IterDerefBdd(dd, bG0);


		/* g0 = F1(x=1) & !F12(x=0) */
		bG1 = cuddBddAndRecur( dd, bA1, Cudd_Not(bB0) );
		if ( bG1 == NULL )
		{
			Cudd_RecursiveDerefZdd(dd, zRes0);
			return NULL;
		}
		cuddRef( bG1 );

		/* P1 = IrrCover( g1, F12(x=1) ) */
		zRes1 = extraZddIsopCoverAltLimited( dd, bG1, bB1, pnBTracks );
		if ( zRes1 == NULL )
		{
			Cudd_IterDerefBdd(dd, bG1);
			Cudd_RecursiveDerefZdd(dd, zRes0);
			return NULL;
		}
		cuddRef( zRes1 );
		Cudd_IterDerefBdd(dd, bG1);

		/* h1 = F1(x=0) & !bdd(P0)  +   F1(x=1) & !bdd(P1) */
		bG0 = extraZddConvertToBddAndAdd( dd, zRes0, Cudd_Not(bA0) );
		if ( bG0 == NULL )
		{
			Cudd_RecursiveDerefZdd(dd, zRes0);
			Cudd_RecursiveDerefZdd(dd, zRes1);
			return NULL;
		}
		cuddRef( bG0 );

		bG1 = extraZddConvertToBddAndAdd( dd, zRes1, Cudd_Not(bA1) );
		if ( bG1 == NULL )
		{
			Cudd_IterDerefBdd(dd, bG0);
			Cudd_RecursiveDerefZdd(dd, zRes0);
			Cudd_RecursiveDerefZdd(dd, zRes1);
			return NULL;
		}
		cuddRef( bG1 );

		bHA = cuddBddAndRecur( dd, bG0, bG1 );
		if ( bHA == NULL )
		{
			Cudd_IterDerefBdd(dd, bG0);
			Cudd_IterDerefBdd(dd, bG1);
			Cudd_RecursiveDerefZdd(dd, zRes0);
			Cudd_RecursiveDerefZdd(dd, zRes1);
			return NULL;
		}
		cuddRef( bHA );
		bHA = Cudd_Not(bHA);
		Cudd_IterDerefBdd(dd, bG0);
		Cudd_IterDerefBdd(dd, bG1);

		/* h12 = F12(x=0) & F12(x=1) */
		bHB = cuddBddAndRecur( dd, bB0, bB1 );
		if ( bHB == NULL )
		{
			Cudd_IterDerefBdd(dd, bHA);
			Cudd_RecursiveDerefZdd(dd, zRes0);
			Cudd_RecursiveDerefZdd(dd, zRes1);
			return NULL;
		}
		cuddRef( bHB );

		/* P1 = IrrCover( h1, h12 ) */
		zRes2 = extraZddIsopCoverAltLimited( dd, bHA, bHB, pnBTracks );
		if ( zRes2 == NULL )
		{
			Cudd_IterDerefBdd(dd, bHA);
			Cudd_IterDerefBdd(dd, bHB);
			Cudd_RecursiveDerefZdd(dd, zRes0);
			Cudd_RecursiveDerefZdd(dd, zRes1);
			return NULL;
		}
		cuddRef( zRes2 );
		Cudd_IterDerefBdd(dd, bHA);
		Cudd_IterDerefBdd(dd, bHB);

		/* --------------- compose the result ------------------ */
		zRes = extraComposeCover( dd, zRes0, zRes1, zRes2, TopVar );
		if ( zRes == NULL ) return NULL;

		/* insert the result into cache and return */
		cuddCacheInsert2(dd, extraZddIsopCoverAlt, bA, bB, zRes);
		return zRes;
	}
} /* end of extraZddIsopCoverAltLimited */




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

  Synopsis    [Computes the vector compose with the timeout.]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
DdNode * extraBddVectorCompose_rec( DdManager * dd, DdNode * f, DdNode ** vector, int deepest )
{
	DdNode * F, * T, * E;
	DdNode * res;
	unsigned HKey;
	statLine( dd );

	// quit because of timeout or spaceout
	if ( s_Timeout && clock() > s_TimeLimit )
	{
//		printf( "t" );
		return NULL;
	}
	if ( s_KeysAllowedIncrease && (int)dd->keys > s_KeysLimit )
	{
//		printf( "s" );
		return NULL;
	}


	F = Cudd_Regular( f );

	/* If we are past the deepest substitution, return f. */
	if ( cuddI( dd, F->index ) > deepest )
		return ( f );

	/* If problem already solved, look up answer and return. */
//	if ( ( res = cuddHashTableLookup1( table, F ) ) != NULL )
//		return ( Cudd_NotCond( res, F != f ) );
	HKey = hashKey2(s_Signature,F,g_TABLESIZE);
	if ( HTable[HKey].Sign == s_Signature && HTable[HKey].Arg1 == (unsigned)F )
	{
		res = (DdNode*) HTable[HKey].Arg2;  
		assert( res );
		return Cudd_NotCond( res, (int)(F!=f) );
	}


	/* Split and recur on children of this node. */
	T = extraBddVectorCompose_rec( dd, cuddT( F ), vector, deepest );
	if ( T == NULL )
		return ( NULL );
	cuddRef( T );
	E = extraBddVectorCompose_rec( dd, cuddE( F ), vector, deepest );
	if ( E == NULL )
	{
		Cudd_IterDerefBdd( dd, T );
		return ( NULL );
	}
	cuddRef( E );

	/* Call cuddBddIteRecur with the BDD that replaces the current top
	   ** variable and the T and E we just created.
	 */
	res = cuddBddIteRecur( dd, vector[F->index], T, E );
	if ( res == NULL )
	{
		Cudd_IterDerefBdd( dd, T );
		Cudd_IterDerefBdd( dd, E );
		return ( NULL );
	}
	cuddRef( res );
	Cudd_IterDerefBdd( dd, T );
	Cudd_IterDerefBdd( dd, E );

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

	HTable[HKey].Sign = s_Signature;
	HTable[HKey].Arg1 = (unsigned)F;
	HTable[HKey].Arg2 = (unsigned)res;  
	// add the BDD to the referenced DD list
	Extra_RefListAdd( res );

	cuddDeref( res );
	return ( Cudd_NotCond( res, F != f ) );
}


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

////////////////////////////////////////////////////////////////////////
///          implementation of the referenced BDD lists              ///
////////////////////////////////////////////////////////////////////////

void Extra_RefListAdd( DdNode * bF )
 // creates new reference to be stored in cache
{
	 // add the BDD to the referenced DD list
	 if ( s_nRefDDs >= s_nRefDDsAlloc )
	 { // resize the list of referenced DDs
		DdNode ** s_pRefDDsNew;
		int nSizeNew, i;

		// get the new size
		if ( s_nRefDDsAlloc > 1000 )
			nSizeNew = s_nRefDDsAlloc * 2;
		else
			nSizeNew = s_nRefDDsAlloc + 1000;

		// allocate the new units
		s_pRefDDsNew = (DdNode**) malloc( nSizeNew * sizeof(DdNode*) );

		// copy the previous units if any
		for ( i = 0; i < s_nRefDDs; i++ )
			s_pRefDDsNew[i] = s_pRefDDs[i];

		// free the previous entries if they were allocated
		if ( s_pRefDDs )
			free( s_pRefDDs );
		s_pRefDDs      = s_pRefDDsNew;
		s_nRefDDsAlloc = nSizeNew;
	 }
	 s_pRefDDs[s_nRefDDs++] = bF;  Cudd_Ref( bF ); 
}

void Extra_RefListRecursiveDeref( DdManager * dd )
{
	// dereference the referenced DDs
	int i;
	for ( i = 0; i < s_nRefDDs; i++ )
		Cudd_IterDerefBdd( dd, s_pRefDDs[i] );
	s_nRefDDs = 0;
}