From bd640142e0fe2260e3d28e187f21a36d3cc8e08f Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 7 Aug 2005 08:01:00 -0700 Subject: Version abc50807 --- src/bdd/dsd/dsd.h | 3 +++ src/bdd/dsd/dsdApi.c | 1 + src/bdd/dsd/dsdInt.h | 2 ++ src/bdd/dsd/dsdProc.c | 32 +++++++++++++++++++++----------- src/bdd/dsd/dsdTree.c | 36 ++++++++++++++++++++++++++++++------ 5 files changed, 57 insertions(+), 17 deletions(-) (limited to 'src/bdd') diff --git a/src/bdd/dsd/dsd.h b/src/bdd/dsd/dsd.h index 60cf4a4e..5396bacd 100644 --- a/src/bdd/dsd/dsd.h +++ b/src/bdd/dsd/dsd.h @@ -88,6 +88,7 @@ extern Dsd_Node_t * Dsd_NodeReadDec ( Dsd_Node_t * p, int i ); extern int Dsd_NodeReadDecsNum( Dsd_Node_t * p ); extern int Dsd_NodeReadMark( Dsd_Node_t * p ); extern void Dsd_NodeSetMark( Dsd_Node_t * p, int Mark ); +extern DdManager * Dsd_ManagerReadDd( Dsd_Manager_t * pMan ); extern Dsd_Node_t * Dsd_ManagerReadRoot( Dsd_Manager_t * pMan, int i ); extern Dsd_Node_t * Dsd_ManagerReadInput( Dsd_Manager_t * pMan, int i ); /*=== dsdMan.c =======================================================*/ @@ -95,6 +96,7 @@ extern Dsd_Manager_t * Dsd_ManagerStart( DdManager * dd, int nSuppMax, int fVerb extern void Dsd_ManagerStop( Dsd_Manager_t * dMan ); /*=== dsdProc.c =======================================================*/ extern void Dsd_Decompose( Dsd_Manager_t * dMan, DdNode ** pbFuncs, int nFuncs ); +extern Dsd_Node_t * Dsd_DecomposeOne( Dsd_Manager_t * pDsdMan, DdNode * bFunc ); /*=== dsdTree.c =======================================================*/ extern void Dsd_TreeNodeGetInfo( Dsd_Manager_t * dMan, int * DepthMax, int * GateSizeMax ); extern void Dsd_TreeNodeGetInfoOne( Dsd_Node_t * pNode, int * DepthMax, int * GateSizeMax ); @@ -104,6 +106,7 @@ extern int Dsd_TreeCountPrimeNodes( Dsd_Manager_t * pDsdMan ); extern int Dsd_TreeCountPrimeNodesOne( Dsd_Node_t * pRoot ); extern int Dsd_TreeCollectDecomposableVars( Dsd_Manager_t * dMan, int * pVars ); extern Dsd_Node_t ** Dsd_TreeCollectNodesDfs( Dsd_Manager_t * dMan, int * pnNodes ); +extern Dsd_Node_t ** Dsd_TreeCollectNodesDfsOne( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pNode, int * pnNodes ); extern void Dsd_TreePrint( FILE * pFile, Dsd_Manager_t * dMan, char * pInputNames[], char * pOutputNames[], int fShortNames, int Output ); /*=== dsdLocal.c =======================================================*/ extern DdNode * Dsd_TreeGetPrimeFunction( DdManager * dd, Dsd_Node_t * pNode ); diff --git a/src/bdd/dsd/dsdApi.c b/src/bdd/dsd/dsdApi.c index f2269092..daf3080f 100644 --- a/src/bdd/dsd/dsdApi.c +++ b/src/bdd/dsd/dsdApi.c @@ -89,6 +89,7 @@ void Dsd_NodeSetMark( Dsd_Node_t * p, int Mark ){ p->Mark = Mark; } ***********************************************************************/ Dsd_Node_t * Dsd_ManagerReadRoot( Dsd_Manager_t * pMan, int i ) { return pMan->pRoots[i]; } Dsd_Node_t * Dsd_ManagerReadInput( Dsd_Manager_t * pMan, int i ) { return pMan->pInputs[i]; } +DdManager * Dsd_ManagerReadDd( Dsd_Manager_t * pMan ) { return pMan->dd; } //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/bdd/dsd/dsdInt.h b/src/bdd/dsd/dsdInt.h index 81440460..5008c24e 100644 --- a/src/bdd/dsd/dsdInt.h +++ b/src/bdd/dsd/dsdInt.h @@ -61,6 +61,8 @@ struct Dsd_Node_t_ /// MACRO DEFITIONS /// //////////////////////////////////////////////////////////////////////// +#define MAXINPUTS 1000 + //////////////////////////////////////////////////////////////////////// /// PARAMETERS /// //////////////////////////////////////////////////////////////////////// diff --git a/src/bdd/dsd/dsdProc.c b/src/bdd/dsd/dsdProc.c index 38cdc2b8..08c029e1 100644 --- a/src/bdd/dsd/dsdProc.c +++ b/src/bdd/dsd/dsdProc.c @@ -223,6 +223,22 @@ s_Loops2Useless = 0; */ } +/**Function************************************************************* + + Synopsis [Performs decomposition for one function.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Dsd_Node_t * Dsd_DecomposeOne( Dsd_Manager_t * pDsdMan, DdNode * bFunc ) +{ + return dsdKernelDecompose_rec( pDsdMan, bFunc ); +} + /**Function************************************************************* Synopsis [The main function of this module. Recursive implementation of DSD.] @@ -1053,7 +1069,7 @@ if ( s_Show ) // go through the decomposition list of pPrev and find components // whose support does not overlap with supp(Lower) - Dsd_Node_t ** pNonOverlap = ALLOC( Dsd_Node_t *, dd->size ); + static Dsd_Node_t * pNonOverlap[MAXINPUTS]; int i, nNonOverlap = 0; for ( i = 0; i < pPrev->nDecs; i++ ) { @@ -1089,7 +1105,6 @@ if ( s_Show ) // assign the support to be subtracted from both components bSuppSubract = pDENew->S; } - free( pNonOverlap ); } // subtract its support from the support of upper component @@ -1106,8 +1121,8 @@ if ( s_Show ) } // end of if ( !fEqualLevel ) else // if ( fEqualLevel ) -- they have the same top level var { - Dsd_Node_t ** pMarkedLeft = ALLOC( Dsd_Node_t *, dd->size ); // the pointers to the marked blocks - char * pMarkedPols = ALLOC( char, dd->size ); // polarities of the marked blocks + static Dsd_Node_t * pMarkedLeft[MAXINPUTS]; // the pointers to the marked blocks + static char pMarkedPols[MAXINPUTS]; // polarities of the marked blocks int nMarkedLeft = 0; int fPolarity = 0; @@ -1198,9 +1213,6 @@ if ( s_Show ) SuppH = Cudd_bddExistAbstract( dd, bTemp = SuppH, bSuppSubract ), Cudd_Ref( SuppH ); Cudd_RecursiveDeref(dd, bTemp); - free( pMarkedLeft ); - free( pMarkedPols ); - } // end of if ( fEqualLevel ) } // end of decomposition list comparison @@ -1333,7 +1345,7 @@ Dsd_Node_t * dsdKernelFindContainingComponent( Dsd_Manager_t * pDsdMan, Dsd_Node ***********************************************************************/ int dsdKernelFindCommonComponents( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pL, Dsd_Node_t * pH, Dsd_Node_t *** pCommon, Dsd_Node_t ** pLastDiffL, Dsd_Node_t ** pLastDiffH ) { - Dsd_Node_t ** Common = ALLOC( Dsd_Node_t *, pDsdMan->dd->size ); + static Dsd_Node_t * Common[MAXINPUTS]; int nCommon = 0; // pointers to the current decomposition entries @@ -1402,7 +1414,6 @@ int dsdKernelFindCommonComponents( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pL, Dsd // return the pointer to the array *pCommon = Common; // return the number of common components - free( Common ); return nCommon; } @@ -1567,7 +1578,7 @@ int dsdKernelVerifyDecomposition( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pDE ) else if ( pR->Type == DSD_NODE_PRIME ) { int i; - DdNode ** bGVars = ALLOC( DdNode *, dd->size ); + static DdNode * bGVars[MAXINPUTS]; // transform the function of this block, so that it depended on inputs // corresponding to the formal inputs DdNode * bNewFunc = Dsd_TreeGetPrimeFunctionOld( dd, pR, 1 ); Cudd_Ref( bNewFunc ); @@ -1589,7 +1600,6 @@ int dsdKernelVerifyDecomposition( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pDE ) RetValue = (int)( bRes == pR->G );//|| bRes == Cudd_Not(pR->G) ); ///////////////////////////////////////////////////////// Cudd_Deref( bRes ); - free( bGVars ); } else { diff --git a/src/bdd/dsd/dsdTree.c b/src/bdd/dsd/dsdTree.c index b1532715..7905cbdd 100644 --- a/src/bdd/dsd/dsdTree.c +++ b/src/bdd/dsd/dsdTree.c @@ -517,6 +517,33 @@ Dsd_Node_t ** Dsd_TreeCollectNodesDfs( Dsd_Manager_t * pDsdMan, int * pnNodes ) return ppNodes; } +/**Function************************************************************* + + Synopsis [Creates the DFS ordered array of DSD nodes in the tree.] + + Description [The collected nodes do not include the terminal nodes + and the constant 1 node. The array of nodes is returned. The number + of entries in the array is returned in the variale pnNodes.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Dsd_Node_t ** Dsd_TreeCollectNodesDfsOne( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pNode, int * pnNodes ) +{ + Dsd_Node_t ** ppNodes; + int nNodes, nNodesAlloc; + nNodesAlloc = Dsd_TreeCountNonTerminalNodesOne(pNode); + nNodes = 0; + ppNodes = ALLOC( Dsd_Node_t *, nNodesAlloc ); + Dsd_TreeCollectNodesDfs_rec( Dsd_Regular(pNode), ppNodes, &nNodes ); + Dsd_TreeUnmark_rec(Dsd_Regular(pNode)); + assert( nNodesAlloc == nNodes ); + *pnNodes = nNodes; + return ppNodes; +} + /**Function************************************************************* @@ -777,9 +804,7 @@ DdNode * Dsd_TreeGetPrimeFunctionOld( DdManager * dd, Dsd_Node_t * pNode, int fR DdNode * bCof0, * bCof1, * bCube0, * bCube1, * bNewFunc, * bTemp; int i; int fAllBuffs = 1; - int * pPermute; - - pPermute = ALLOC( int, dd->size ); + static int Permute[MAXINPUTS]; assert( pNode ); assert( !Dsd_IsComplement( pNode ) ); @@ -821,14 +846,13 @@ DdNode * Dsd_TreeGetPrimeFunctionOld( DdManager * dd, Dsd_Node_t * pNode, int fR // remap the function to the first variables of the manager for ( i = 0; i < pNode->nDecs; i++ ) // Permute[ pNode->pDecs[i]->S->index ] = dd->invperm[i]; - pPermute[ pNode->pDecs[i]->S->index ] = i; + Permute[ pNode->pDecs[i]->S->index ] = i; - bNewFunc = Cudd_bddPermute( dd, bTemp = bNewFunc, pPermute ); Cudd_Ref( bNewFunc ); + bNewFunc = Cudd_bddPermute( dd, bTemp = bNewFunc, Permute ); Cudd_Ref( bNewFunc ); Cudd_RecursiveDeref( dd, bTemp ); } Cudd_Deref( bNewFunc ); - free( pPermute ); return bNewFunc; } -- cgit v1.2.3