abc70930: src/bdd/dsd/dsdTree.c Source File

00001 
00019 #include "dsdInt.h"
00020 
00024 
00025 static void Dsd_TreeUnmark_rec( Dsd_Node_t * pNode );
00026 static void Dsd_TreeGetInfo_rec( Dsd_Node_t * pNode, int RankCur );
00027 static int  Dsd_TreeCountNonTerminalNodes_rec( Dsd_Node_t * pNode );
00028 static int  Dsd_TreeCountPrimeNodes_rec( Dsd_Node_t * pNode );
00029 static int  Dsd_TreeCollectDecomposableVars_rec( DdManager * dd, Dsd_Node_t * pNode, int * pVars, int * nVars );
00030 static void Dsd_TreeCollectNodesDfs_rec( Dsd_Node_t * pNode, Dsd_Node_t * ppNodes[], int * pnNodes );
00031 static void Dsd_TreePrint_rec( FILE * pFile, Dsd_Node_t * pNode, int fCcmp, char * pInputNames[], char * pOutputName, int nOffset, int * pSigCounter, int fShortNames );
00032 static void Dsd_NodePrint_rec( FILE * pFile, Dsd_Node_t * pNode, int fComp, char * pOutputName, int nOffset, int * pSigCounter );
00033 
00037 
00038 static int s_DepthMax;
00039 static int s_GateSizeMax;
00040 
00041 static int s_CounterBlocks;
00042 static int s_CounterPos;
00043 static int s_CounterNeg;
00044 static int s_CounterNo;
00045 
00049 
00061 Dsd_Node_t * Dsd_TreeNodeCreate( int Type, int nDecs, int BlockNum )
00062 {
00063         // allocate memory for this node 
00064         Dsd_Node_t * p = (Dsd_Node_t *) malloc( sizeof(Dsd_Node_t) );
00065         memset( p, 0, sizeof(Dsd_Node_t) );
00066         p->Type       = Type;       // the type of this block
00067         p->nDecs      = nDecs;      // the number of decompositions
00068         if ( p->nDecs )
00069         {
00070                 p->pDecs      = (Dsd_Node_t **) malloc( p->nDecs * sizeof(Dsd_Node_t *) );
00071                 p->pDecs[0]   = NULL;
00072         }
00073         return p;
00074 }
00075 
00087 void Dsd_TreeNodeDelete( DdManager * dd, Dsd_Node_t * pNode )
00088 {
00089         if ( pNode->G )  Cudd_RecursiveDeref( dd, pNode->G );
00090         if ( pNode->S )  Cudd_RecursiveDeref( dd, pNode->S );
00091         FREE( pNode->pDecs );
00092         FREE( pNode );
00093 }
00094 
00107 void Dsd_TreeUnmark( Dsd_Manager_t * pDsdMan )
00108 {
00109         int i;
00110         for ( i = 0; i < pDsdMan->nRoots; i++ )
00111                 Dsd_TreeUnmark_rec( Dsd_Regular( pDsdMan->pRoots[i] ) );
00112 }
00113 
00114 
00127 void Dsd_TreeUnmark_rec( Dsd_Node_t * pNode )
00128 {
00129         int i;
00130 
00131         assert( pNode );
00132         assert( !Dsd_IsComplement( pNode ) );
00133         assert( pNode->nVisits > 0 );
00134 
00135         if ( --pNode->nVisits ) // if this is not the last visit, return
00136                 return;
00137 
00138         // upon the last visit, go through the list of successors and call recursively 
00139         if ( pNode->Type != DSD_NODE_BUF && pNode->Type != DSD_NODE_CONST1 )
00140         for ( i = 0; i < pNode->nDecs; i++ )
00141                 Dsd_TreeUnmark_rec( Dsd_Regular(pNode->pDecs[i]) );
00142 }
00143 
00156 void Dsd_TreeNodeGetInfo( Dsd_Manager_t * pDsdMan, int * DepthMax, int * GateSizeMax )
00157 {
00158         int i;
00159         s_DepthMax    = 0;
00160         s_GateSizeMax = 0;
00161 
00162         for ( i = 0; i < pDsdMan->nRoots; i++ )
00163         Dsd_TreeGetInfo_rec( Dsd_Regular( pDsdMan->pRoots[i] ), 0 );
00164 
00165         if ( DepthMax ) 
00166                 *DepthMax     = s_DepthMax;
00167         if ( GateSizeMax ) 
00168                 *GateSizeMax  = s_GateSizeMax;
00169 }
00170 
00183 void Dsd_TreeNodeGetInfoOne( Dsd_Node_t * pNode, int * DepthMax, int * GateSizeMax )
00184 {
00185         s_DepthMax    = 0;
00186         s_GateSizeMax = 0;
00187 
00188         Dsd_TreeGetInfo_rec( Dsd_Regular(pNode), 0 );
00189 
00190         if ( DepthMax ) 
00191                 *DepthMax     = s_DepthMax;
00192         if ( GateSizeMax ) 
00193                 *GateSizeMax  = s_GateSizeMax;
00194 }
00195 
00196 
00212 void Dsd_TreeGetInfo_rec( Dsd_Node_t * pNode, int RankCur )
00213 {
00214         int i;
00215         int GateSize;
00216 
00217         assert( pNode );
00218         assert( !Dsd_IsComplement( pNode ) );
00219         assert( pNode->nVisits >= 0 );
00220 
00221         // we don't want the two-input gates to count for non-decomposable blocks
00222         if ( pNode->Type == DSD_NODE_OR  || 
00223                  pNode->Type == DSD_NODE_EXOR )
00224                 GateSize = 2;
00225         else
00226                 GateSize = pNode->nDecs;
00227 
00228         // update the max size of the node
00229         if ( s_GateSizeMax < GateSize )
00230                  s_GateSizeMax = GateSize;
00231 
00232         if ( pNode->nDecs < 2 )
00233                 return;
00234 
00235         // update the max rank
00236         if ( s_DepthMax < RankCur+1 )
00237                  s_DepthMax = RankCur+1;
00238 
00239         // call recursively
00240         for ( i = 0; i < pNode->nDecs; i++ )
00241                 Dsd_TreeGetInfo_rec( Dsd_Regular(pNode->pDecs[i]), RankCur+1 );
00242 }
00243 
00255 int Dsd_TreeGetAigCost_rec( Dsd_Node_t * pNode )
00256 {
00257         int i, Counter = 0;
00258 
00259         assert( pNode );
00260         assert( !Dsd_IsComplement( pNode ) );
00261         assert( pNode->nVisits >= 0 );
00262 
00263         if ( pNode->nDecs < 2 )
00264                 return 0;
00265 
00266         // we don't want the two-input gates to count for non-decomposable blocks
00267         if ( pNode->Type == DSD_NODE_OR )
00268         Counter += pNode->nDecs - 1;
00269         else if ( pNode->Type == DSD_NODE_EXOR )
00270                 Counter += 3*(pNode->nDecs - 1);
00271     else if ( pNode->Type == DSD_NODE_PRIME && pNode->nDecs == 3 )
00272                 Counter += 3;
00273 
00274         // call recursively
00275         for ( i = 0; i < pNode->nDecs; i++ )
00276                 Counter += Dsd_TreeGetAigCost_rec( Dsd_Regular(pNode->pDecs[i]) );
00277     return Counter;
00278 }
00279 
00291 int Dsd_TreeGetAigCost( Dsd_Node_t * pNode )
00292 {
00293     return Dsd_TreeGetAigCost_rec( Dsd_Regular(pNode) );
00294 }
00295 
00310 int Dsd_TreeCountNonTerminalNodes( Dsd_Manager_t * pDsdMan )
00311 {
00312         int Counter, i;
00313     Counter = 0;
00314         for ( i = 0; i < pDsdMan->nRoots; i++ )
00315                 Counter += Dsd_TreeCountNonTerminalNodes_rec( Dsd_Regular( pDsdMan->pRoots[i] ) );
00316         Dsd_TreeUnmark( pDsdMan );
00317     return Counter;
00318 }
00319 
00331 int Dsd_TreeCountNonTerminalNodesOne( Dsd_Node_t * pRoot )
00332 {
00333         int Counter = 0;
00334 
00335         // go through the list of successors and call recursively 
00336         Counter = Dsd_TreeCountNonTerminalNodes_rec( Dsd_Regular(pRoot) );
00337 
00338         Dsd_TreeUnmark_rec( Dsd_Regular(pRoot) );
00339         return Counter;
00340 }
00341 
00342 
00354 int Dsd_TreeCountNonTerminalNodes_rec( Dsd_Node_t * pNode )
00355 {
00356         int i;
00357         int Counter = 0;
00358 
00359         assert( pNode );
00360         assert( !Dsd_IsComplement( pNode ) );
00361         assert( pNode->nVisits >= 0 );
00362 
00363         if ( pNode->nVisits++ ) // if this is not the first visit, return zero
00364                 return 0;
00365 
00366         if ( pNode->nDecs <= 1 )
00367                 return 0;
00368 
00369         // upon the first visit, go through the list of successors and call recursively 
00370         for ( i = 0; i < pNode->nDecs; i++ )
00371                 Counter += Dsd_TreeCountNonTerminalNodes_rec( Dsd_Regular(pNode->pDecs[i]) );
00372 
00373         return Counter + 1;
00374 }
00375 
00376 
00389 int Dsd_TreeCountPrimeNodes( Dsd_Manager_t * pDsdMan )
00390 {
00391         int Counter, i;
00392     Counter = 0;
00393         for ( i = 0; i < pDsdMan->nRoots; i++ )
00394                 Counter += Dsd_TreeCountPrimeNodes_rec( Dsd_Regular( pDsdMan->pRoots[i] ) );
00395         Dsd_TreeUnmark( pDsdMan );
00396     return Counter;
00397 }
00398 
00410 int Dsd_TreeCountPrimeNodesOne( Dsd_Node_t * pRoot )
00411 {
00412         int Counter = 0;
00413 
00414         // go through the list of successors and call recursively 
00415         Counter = Dsd_TreeCountPrimeNodes_rec( Dsd_Regular(pRoot) );
00416 
00417         Dsd_TreeUnmark_rec( Dsd_Regular(pRoot) );
00418         return Counter;
00419 }
00420 
00421 
00433 int Dsd_TreeCountPrimeNodes_rec( Dsd_Node_t * pNode )
00434 {
00435         int i;
00436         int Counter = 0;
00437 
00438         assert( pNode );
00439         assert( !Dsd_IsComplement( pNode ) );
00440         assert( pNode->nVisits >= 0 );
00441 
00442         if ( pNode->nVisits++ ) // if this is not the first visit, return zero
00443                 return 0;
00444 
00445         if ( pNode->nDecs <= 1 )
00446                 return 0;
00447 
00448         // upon the first visit, go through the list of successors and call recursively 
00449         for ( i = 0; i < pNode->nDecs; i++ )
00450                 Counter += Dsd_TreeCountPrimeNodes_rec( Dsd_Regular(pNode->pDecs[i]) );
00451 
00452         if ( pNode->Type == DSD_NODE_PRIME )
00453                 Counter++;
00454 
00455         return Counter;
00456 }
00457 
00458 
00470 int Dsd_TreeCollectDecomposableVars( Dsd_Manager_t * pDsdMan, int * pVars )
00471 {
00472         int nVars;
00473 
00474         // set the vars collected to 0
00475         nVars = 0;
00476         Dsd_TreeCollectDecomposableVars_rec( pDsdMan->dd, Dsd_Regular(pDsdMan->pRoots[0]), pVars, &nVars );
00477         // return the number of collected vars
00478         return nVars;
00479 }
00480 
00494 int Dsd_TreeCollectDecomposableVars_rec( DdManager * dd, Dsd_Node_t * pNode, int * pVars, int * nVars )
00495 {
00496         int fSkipThisNode, i;
00497         Dsd_Node_t * pTemp;
00498         int fVerbose = 0;
00499 
00500         assert( pNode );
00501         assert( !Dsd_IsComplement( pNode ) );
00502 
00503         if ( pNode->nDecs <= 1 )
00504                 return 0;
00505 
00506         // go through the list of successors and call recursively 
00507         fSkipThisNode = 0;
00508         for ( i = 0; i < pNode->nDecs; i++ )
00509                 if ( Dsd_TreeCollectDecomposableVars_rec(dd, Dsd_Regular(pNode->pDecs[i]), pVars, nVars) )
00510                         fSkipThisNode = 1;
00511 
00512         if ( !fSkipThisNode && (pNode->Type == DSD_NODE_OR || pNode->Type == DSD_NODE_EXOR || pNode->nDecs <= 4) )
00513         {
00514 if ( fVerbose )
00515 printf( "Node of type <%d> (OR=6,EXOR=8,RAND=1): ", pNode->Type );
00516 
00517                 for ( i = 0; i < pNode->nDecs; i++ )
00518                 {
00519                         pTemp = Dsd_Regular(pNode->pDecs[i]);
00520                         if ( pTemp->Type == DSD_NODE_BUF )
00521                         {
00522                                 if ( pVars )
00523                                         pVars[ (*nVars)++ ] = pTemp->S->index;
00524                                 else
00525                                         (*nVars)++;
00526                                         
00527 if ( fVerbose )
00528 printf( "%d ", pTemp->S->index );
00529                         }
00530                 }
00531 if ( fVerbose )
00532 printf( "\n" );
00533         }
00534         else
00535                 fSkipThisNode = 1;
00536 
00537 
00538         return fSkipThisNode;
00539 }
00540 
00541 
00555 Dsd_Node_t ** Dsd_TreeCollectNodesDfs( Dsd_Manager_t * pDsdMan, int * pnNodes )
00556 {
00557         Dsd_Node_t ** ppNodes;
00558         int nNodes, nNodesAlloc;
00559         int i;
00560 
00561     nNodesAlloc = Dsd_TreeCountNonTerminalNodes(pDsdMan);
00562         nNodes  = 0;
00563         ppNodes = ALLOC( Dsd_Node_t *, nNodesAlloc );
00564         for ( i = 0; i < pDsdMan->nRoots; i++ )
00565                 Dsd_TreeCollectNodesDfs_rec( Dsd_Regular(pDsdMan->pRoots[i]), ppNodes, &nNodes );
00566         Dsd_TreeUnmark( pDsdMan );
00567     assert( nNodesAlloc == nNodes );
00568         *pnNodes = nNodes;
00569         return ppNodes;
00570 }
00571 
00585 Dsd_Node_t ** Dsd_TreeCollectNodesDfsOne( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pNode, int * pnNodes )
00586 {
00587         Dsd_Node_t ** ppNodes;
00588         int nNodes, nNodesAlloc;
00589     nNodesAlloc = Dsd_TreeCountNonTerminalNodesOne(pNode);
00590         nNodes  = 0;
00591         ppNodes = ALLOC( Dsd_Node_t *, nNodesAlloc );
00592     Dsd_TreeCollectNodesDfs_rec( Dsd_Regular(pNode), ppNodes, &nNodes );
00593         Dsd_TreeUnmark_rec(Dsd_Regular(pNode));
00594     assert( nNodesAlloc == nNodes );
00595         *pnNodes = nNodes;
00596         return ppNodes;
00597 }
00598 
00599 
00611 void Dsd_TreeCollectNodesDfs_rec( Dsd_Node_t * pNode, Dsd_Node_t * ppNodes[], int * pnNodes )
00612 {
00613         int i;
00614         assert( pNode );
00615         assert( !Dsd_IsComplement(pNode) );
00616         assert( pNode->nVisits >= 0 );
00617 
00618         if ( pNode->nVisits++ ) // if this is not the first visit, return zero
00619                 return;
00620         if ( pNode->nDecs <= 1 )
00621                 return;
00622 
00623         // upon the first visit, go through the list of successors and call recursively 
00624         for ( i = 0; i < pNode->nDecs; i++ )
00625                 Dsd_TreeCollectNodesDfs_rec( Dsd_Regular(pNode->pDecs[i]), ppNodes, pnNodes );
00626 
00627         ppNodes[ (*pnNodes)++ ] = pNode;
00628 }
00629 
00641 void Dsd_TreePrint( FILE * pFile, Dsd_Manager_t * pDsdMan, char * pInputNames[], char * pOutputNames[], int fShortNames, int Output )
00642 {
00643         Dsd_Node_t * pNode;
00644         int SigCounter;
00645         int i;
00646         SigCounter = 1;
00647 
00648         if ( Output == -1 )
00649         {
00650                 for ( i = 0; i < pDsdMan->nRoots; i++ )
00651                 {
00652                         pNode = Dsd_Regular( pDsdMan->pRoots[i] );
00653                         Dsd_TreePrint_rec( pFile, pNode, (pNode != pDsdMan->pRoots[i]), pInputNames, pOutputNames[i], 0, &SigCounter, fShortNames );
00654                 }
00655         }
00656         else
00657         {
00658                 assert( Output >= 0 && Output < pDsdMan->nRoots );
00659                 pNode = Dsd_Regular( pDsdMan->pRoots[Output] );
00660                 Dsd_TreePrint_rec( pFile, pNode, (pNode != pDsdMan->pRoots[Output]), pInputNames, pOutputNames[Output], 0, &SigCounter, fShortNames );
00661         }
00662 }
00663 
00675 void Dsd_TreePrint_rec( FILE * pFile, Dsd_Node_t * pNode, int fComp, char * pInputNames[], char * pOutputName, int nOffset, int * pSigCounter, int fShortNames )
00676 {
00677         char Buffer[100];
00678         Dsd_Node_t * pInput;
00679         int * pInputNums;
00680         int fCompNew, i;
00681 
00682         assert( pNode->Type == DSD_NODE_BUF || pNode->Type == DSD_NODE_CONST1 || 
00683         pNode->Type == DSD_NODE_PRIME || pNode->Type == DSD_NODE_OR || pNode->Type == DSD_NODE_EXOR ); 
00684 
00685         Extra_PrintSymbols( pFile, ' ', nOffset, 0 );
00686     if ( !fComp )
00687             fprintf( pFile, "%s = ", pOutputName );
00688     else
00689             fprintf( pFile, "NOT(%s) = ", pOutputName );
00690         pInputNums = ALLOC( int, pNode->nDecs );
00691         if ( pNode->Type == DSD_NODE_CONST1 )
00692         {
00693             fprintf( pFile, " Constant 1.\n" );
00694         }
00695         else if ( pNode->Type == DSD_NODE_BUF )
00696         {
00697                 if ( fShortNames )
00698                         fprintf( pFile, "%d", 'a' + pNode->S->index );
00699                 else
00700                         fprintf( pFile, "%s", pInputNames[pNode->S->index] );
00701                 fprintf( pFile, "\n" );
00702         }
00703         else if ( pNode->Type == DSD_NODE_PRIME )
00704         {
00705                 // print the line
00706                 fprintf( pFile, "PRIME(" );
00707                 for ( i = 0; i < pNode->nDecs; i++ )
00708                 {
00709                         pInput   = Dsd_Regular( pNode->pDecs[i] );
00710                         fCompNew = (int)( pInput != pNode->pDecs[i] );
00711                         if ( i )
00712                                 fprintf( pFile, "," );
00713                         if ( fCompNew )
00714                                 fprintf( pFile, " NOT(" );
00715                         else
00716                                 fprintf( pFile, " " );
00717                         if ( pInput->Type == DSD_NODE_BUF )
00718                         {
00719                                 pInputNums[i] = 0;
00720                                 if ( fShortNames )
00721                                         fprintf( pFile, "%d", pInput->S->index );
00722                                 else
00723                                         fprintf( pFile, "%s", pInputNames[pInput->S->index] );
00724                         }
00725                         else
00726                         {
00727                                 pInputNums[i] = (*pSigCounter)++;
00728                                 fprintf( pFile, "<%d>", pInputNums[i] );
00729                         }
00730                         if ( fCompNew )
00731                                 fprintf( pFile, ")" );
00732                 }
00733                 fprintf( pFile, " )\n" );
00734                 // call recursively for the following blocks
00735                 for ( i = 0; i < pNode->nDecs; i++ )
00736                         if ( pInputNums[i] )
00737                         {
00738                                 pInput   = Dsd_Regular( pNode->pDecs[i] );
00739                                 sprintf( Buffer, "<%d>", pInputNums[i] );
00740                                 Dsd_TreePrint_rec( pFile, Dsd_Regular( pNode->pDecs[i] ), 0, pInputNames, Buffer, nOffset + 6, pSigCounter, fShortNames );
00741                         }
00742         }
00743         else if ( pNode->Type == DSD_NODE_OR )
00744         {
00745                 // print the line
00746         fprintf( pFile, "OR(" );
00747                 for ( i = 0; i < pNode->nDecs; i++ )
00748                 {
00749                         pInput = Dsd_Regular( pNode->pDecs[i] );
00750                         fCompNew  = (int)( pInput != pNode->pDecs[i] );
00751                         if ( i )
00752                                 fprintf( pFile, "," );
00753                         if ( fCompNew )
00754                                 fprintf( pFile, " NOT(" );
00755                         else
00756                                 fprintf( pFile, " " );
00757                         if ( pInput->Type == DSD_NODE_BUF )
00758                         {
00759                                 pInputNums[i] = 0;
00760                                 if ( fShortNames )
00761                                         fprintf( pFile, "%c", 'a' + pInput->S->index );
00762                                 else
00763                                         fprintf( pFile, "%s", pInputNames[pInput->S->index] );
00764                         }
00765                         else
00766                         {
00767                                 pInputNums[i] = (*pSigCounter)++;
00768                                 fprintf( pFile, "<%d>", pInputNums[i] );
00769                         }
00770                         if ( fCompNew )
00771                                 fprintf( pFile, ")" );
00772                 }
00773                 fprintf( pFile, " )\n" );
00774                 // call recursively for the following blocks
00775                 for ( i = 0; i < pNode->nDecs; i++ )
00776                         if ( pInputNums[i] )
00777                         {
00778                                 pInput = Dsd_Regular( pNode->pDecs[i] );
00779                                 sprintf( Buffer, "<%d>", pInputNums[i] );
00780                                 Dsd_TreePrint_rec( pFile, Dsd_Regular( pNode->pDecs[i] ), 0, pInputNames, Buffer, nOffset + 6, pSigCounter, fShortNames );
00781                         }
00782         }
00783         else if ( pNode->Type == DSD_NODE_EXOR )
00784         {
00785                 // print the line
00786         fprintf( pFile, "EXOR(" );
00787                 for ( i = 0; i < pNode->nDecs; i++ )
00788                 {
00789                         pInput = Dsd_Regular( pNode->pDecs[i] );
00790                         fCompNew  = (int)( pInput != pNode->pDecs[i] );
00791                         if ( i )
00792                                 fprintf( pFile, "," );
00793                         if ( fCompNew )
00794                                 fprintf( pFile, " NOT(" );
00795                         else
00796                                 fprintf( pFile, " " );
00797                         if ( pInput->Type == DSD_NODE_BUF )
00798                         {
00799                                 pInputNums[i] = 0;
00800                                 if ( fShortNames )
00801                                         fprintf( pFile, "%c", 'a' + pInput->S->index );
00802                                 else
00803                                         fprintf( pFile, "%s", pInputNames[pInput->S->index] );
00804                         }
00805                         else
00806                         {
00807                                 pInputNums[i] = (*pSigCounter)++;
00808                                 fprintf( pFile, "<%d>", pInputNums[i] );
00809                         }
00810                         if ( fCompNew )
00811                                 fprintf( pFile, ")" );
00812                 }
00813                 fprintf( pFile, " )\n" );
00814                 // call recursively for the following blocks
00815                 for ( i = 0; i < pNode->nDecs; i++ )
00816                         if ( pInputNums[i] )
00817                         {
00818                                 pInput = Dsd_Regular( pNode->pDecs[i] );
00819                                 sprintf( Buffer, "<%d>", pInputNums[i] );
00820                                 Dsd_TreePrint_rec( pFile, Dsd_Regular( pNode->pDecs[i] ), 0, pInputNames, Buffer, nOffset + 6, pSigCounter, fShortNames );
00821                         }
00822         }
00823         free( pInputNums );
00824 }
00825 
00837 void Dsd_NodePrint( FILE * pFile, Dsd_Node_t * pNode )
00838 {
00839     Dsd_Node_t * pNodeR;
00840         int SigCounter = 1;
00841         pNodeR = Dsd_Regular(pNode);
00842         Dsd_NodePrint_rec( pFile, pNodeR, pNodeR != pNode, "F", 0, &SigCounter );
00843 }
00844 
00856 void Dsd_NodePrint_rec( FILE * pFile, Dsd_Node_t * pNode, int fComp, char * pOutputName, int nOffset, int * pSigCounter )
00857 {
00858         char Buffer[100];
00859         Dsd_Node_t * pInput;
00860         int * pInputNums;
00861         int fCompNew, i;
00862 
00863         assert( pNode->Type == DSD_NODE_BUF || pNode->Type == DSD_NODE_CONST1 || 
00864         pNode->Type == DSD_NODE_PRIME || pNode->Type == DSD_NODE_OR || pNode->Type == DSD_NODE_EXOR ); 
00865 
00866         Extra_PrintSymbols( pFile, ' ', nOffset, 0 );
00867     if ( !fComp )
00868             fprintf( pFile, "%s = ", pOutputName );
00869     else
00870             fprintf( pFile, "NOT(%s) = ", pOutputName );
00871         pInputNums = ALLOC( int, pNode->nDecs );
00872         if ( pNode->Type == DSD_NODE_CONST1 )
00873         {
00874                 fprintf( pFile, " Constant 1.\n" );
00875         }
00876         else if ( pNode->Type == DSD_NODE_BUF )
00877         {
00878                 fprintf( pFile, " " );
00879         fprintf( pFile, "%c", 'a' + pNode->S->index );
00880                 fprintf( pFile, "\n" );
00881         }
00882         else if ( pNode->Type == DSD_NODE_PRIME )
00883         {
00884                 // print the line
00885                 fprintf( pFile, "PRIME(" );
00886                 for ( i = 0; i < pNode->nDecs; i++ )
00887                 {
00888                         pInput   = Dsd_Regular( pNode->pDecs[i] );
00889                         fCompNew = (int)( pInput != pNode->pDecs[i] );
00890             assert( fCompNew == 0 );
00891                         if ( i )
00892                                 fprintf( pFile, "," );
00893                         if ( pInput->Type == DSD_NODE_BUF )
00894             {
00895                                 pInputNums[i] = 0;
00896                                 fprintf( pFile, " %c", 'a' + pInput->S->index );
00897             }
00898                         else
00899                         {
00900                                 pInputNums[i] = (*pSigCounter)++;
00901                                 fprintf( pFile, " <%d>", pInputNums[i] );
00902                         }
00903                         if ( fCompNew )
00904                                 fprintf( pFile, "\'" );
00905                 }
00906                 fprintf( pFile, " )\n" );
00907 /*
00908                 fprintf( pFile, " )  " );  
00909         {
00910             DdNode * bLocal;
00911             bLocal = Dsd_TreeGetPrimeFunction( dd, pNodeDsd );  Cudd_Ref( bLocal );
00912             Extra_bddPrint( dd, bLocal );
00913             Cudd_RecursiveDeref( dd, bLocal );
00914         }
00915 */
00916                 // call recursively for the following blocks
00917                 for ( i = 0; i < pNode->nDecs; i++ )
00918                         if ( pInputNums[i] )
00919                         {
00920                                 pInput   = Dsd_Regular( pNode->pDecs[i] );
00921                                 sprintf( Buffer, "<%d>", pInputNums[i] );
00922                                 Dsd_NodePrint_rec( pFile, Dsd_Regular( pNode->pDecs[i] ), 0, Buffer, nOffset + 6, pSigCounter );
00923                         }
00924         }
00925         else if ( pNode->Type == DSD_NODE_OR )
00926         {
00927                 // print the line
00928                 fprintf( pFile, "OR(" );
00929                 for ( i = 0; i < pNode->nDecs; i++ )
00930                 {
00931                         pInput = Dsd_Regular( pNode->pDecs[i] );
00932                         fCompNew  = (int)( pInput != pNode->pDecs[i] );
00933                         if ( i )
00934                                 fprintf( pFile, "," );
00935                         if ( pInput->Type == DSD_NODE_BUF )
00936             {
00937                                 pInputNums[i] = 0;
00938                                 fprintf( pFile, " %c", 'a' + pInput->S->index );
00939             }
00940                         else
00941                         {
00942                                 pInputNums[i] = (*pSigCounter)++;
00943                                 fprintf( pFile, " <%d>", pInputNums[i] );
00944                         }
00945                         if ( fCompNew )
00946                                 fprintf( pFile, "\'" );
00947                 }
00948                 fprintf( pFile, " )\n" );
00949                 // call recursively for the following blocks
00950                 for ( i = 0; i < pNode->nDecs; i++ )
00951                         if ( pInputNums[i] )
00952                         {
00953                                 pInput = Dsd_Regular( pNode->pDecs[i] );
00954                                 sprintf( Buffer, "<%d>", pInputNums[i] );
00955                                 Dsd_NodePrint_rec( pFile, Dsd_Regular( pNode->pDecs[i] ), 0, Buffer, nOffset + 6, pSigCounter );
00956                         }
00957         }
00958         else if ( pNode->Type == DSD_NODE_EXOR )
00959         {
00960                 // print the line
00961                 fprintf( pFile, "EXOR(" );
00962                 for ( i = 0; i < pNode->nDecs; i++ )
00963                 {
00964                         pInput = Dsd_Regular( pNode->pDecs[i] );
00965                         fCompNew  = (int)( pInput != pNode->pDecs[i] );
00966             assert( fCompNew == 0 );
00967                         if ( i )
00968                                 fprintf( pFile, "," );
00969                         if ( pInput->Type == DSD_NODE_BUF )
00970             {
00971                                 pInputNums[i] = 0;
00972                                 fprintf( pFile, " %c", 'a' + pInput->S->index );
00973             }
00974                         else
00975                         {
00976                                 pInputNums[i] = (*pSigCounter)++;
00977                                 fprintf( pFile, " <%d>", pInputNums[i] );
00978                         }
00979                         if ( fCompNew )
00980                                 fprintf( pFile, "\'" );
00981                 }
00982                 fprintf( pFile, " )\n" );
00983                 // call recursively for the following blocks
00984                 for ( i = 0; i < pNode->nDecs; i++ )
00985                         if ( pInputNums[i] )
00986                         {
00987                                 pInput = Dsd_Regular( pNode->pDecs[i] );
00988                                 sprintf( Buffer, "<%d>", pInputNums[i] );
00989                                 Dsd_NodePrint_rec( pFile, Dsd_Regular( pNode->pDecs[i] ), 0, Buffer, nOffset + 6, pSigCounter );
00990                         }
00991         }
00992         free( pInputNums );
00993 }
00994 
00995 
01008 DdNode * Dsd_TreeGetPrimeFunctionOld( DdManager * dd, Dsd_Node_t * pNode, int fRemap ) 
01009 {
01010         DdNode * bCof0,  * bCof1, * bCube0, * bCube1, * bNewFunc, * bTemp;
01011         int i;
01012         int fAllBuffs = 1;
01013         static int Permute[MAXINPUTS];
01014 
01015         assert( pNode );
01016         assert( !Dsd_IsComplement( pNode ) );
01017         assert( pNode->Type == DSD_NODE_PRIME );
01018 
01019         // transform the function of this block to depend on inputs
01020         // corresponding to the formal inputs
01021 
01022         // first, substitute those inputs that have some blocks associated with them
01023         // second, remap the inputs to the top of the manager (then, it is easy to output them)
01024 
01025         // start the function
01026         bNewFunc = pNode->G;  Cudd_Ref( bNewFunc );
01027         // go over all primary inputs
01028         for ( i = 0; i < pNode->nDecs; i++ )
01029         if ( pNode->pDecs[i]->Type != DSD_NODE_BUF ) // remap only if it is not the buffer
01030         {
01031                 bCube0 = Extra_bddFindOneCube( dd, Cudd_Not(pNode->pDecs[i]->G) );  Cudd_Ref( bCube0 );
01032                 bCof0 = Cudd_Cofactor( dd, bNewFunc, bCube0 );                     Cudd_Ref( bCof0 );
01033                 Cudd_RecursiveDeref( dd, bCube0 );
01034 
01035                 bCube1 = Extra_bddFindOneCube( dd,          pNode->pDecs[i]->G  );  Cudd_Ref( bCube1 );
01036                 bCof1 = Cudd_Cofactor( dd, bNewFunc, bCube1 );                     Cudd_Ref( bCof1 );
01037                 Cudd_RecursiveDeref( dd, bCube1 );
01038 
01039                 Cudd_RecursiveDeref( dd, bNewFunc );
01040 
01041                 // use the variable in the i-th level of the manager
01042 //              bNewFunc = Cudd_bddIte( dd, dd->vars[dd->invperm[i]],bCof1,bCof0 );     Cudd_Ref( bNewFunc );
01043                 // use the first variale in the support of the component
01044                 bNewFunc = Cudd_bddIte( dd, dd->vars[pNode->pDecs[i]->S->index],bCof1,bCof0 );     Cudd_Ref( bNewFunc );
01045                 Cudd_RecursiveDeref( dd, bCof0 );
01046                 Cudd_RecursiveDeref( dd, bCof1 );
01047         }
01048 
01049         if ( fRemap )
01050         {
01051                 // remap the function to the top of the manager
01052                 // remap the function to the first variables of the manager
01053                 for ( i = 0; i < pNode->nDecs; i++ )
01054         //              Permute[ pNode->pDecs[i]->S->index ] = dd->invperm[i];
01055                         Permute[ pNode->pDecs[i]->S->index ] = i;
01056 
01057                 bNewFunc = Cudd_bddPermute( dd, bTemp = bNewFunc, Permute );   Cudd_Ref( bNewFunc );
01058                 Cudd_RecursiveDeref( dd, bTemp );
01059         }
01060 
01061         Cudd_Deref( bNewFunc );
01062         return bNewFunc;
01063 }
01064 
01065