src/bdd/dsd/dsdTree.c File Reference

#include "dsdInt.h"
Include dependency graph for dsdTree.c:

Go to the source code of this file.

Functions

static void Dsd_TreeUnmark_rec (Dsd_Node_t *pNode)
static void Dsd_TreeGetInfo_rec (Dsd_Node_t *pNode, int RankCur)
static int Dsd_TreeCountNonTerminalNodes_rec (Dsd_Node_t *pNode)
static int Dsd_TreeCountPrimeNodes_rec (Dsd_Node_t *pNode)
static int Dsd_TreeCollectDecomposableVars_rec (DdManager *dd, Dsd_Node_t *pNode, int *pVars, int *nVars)
static void Dsd_TreeCollectNodesDfs_rec (Dsd_Node_t *pNode, Dsd_Node_t *ppNodes[], int *pnNodes)
static void Dsd_TreePrint_rec (FILE *pFile, Dsd_Node_t *pNode, int fCcmp, char *pInputNames[], char *pOutputName, int nOffset, int *pSigCounter, int fShortNames)
static void Dsd_NodePrint_rec (FILE *pFile, Dsd_Node_t *pNode, int fComp, char *pOutputName, int nOffset, int *pSigCounter)
Dsd_Node_t * Dsd_TreeNodeCreate (int Type, int nDecs, int BlockNum)
void Dsd_TreeNodeDelete (DdManager *dd, Dsd_Node_t *pNode)
void Dsd_TreeUnmark (Dsd_Manager_t *pDsdMan)
void Dsd_TreeNodeGetInfo (Dsd_Manager_t *pDsdMan, int *DepthMax, int *GateSizeMax)
void Dsd_TreeNodeGetInfoOne (Dsd_Node_t *pNode, int *DepthMax, int *GateSizeMax)
int Dsd_TreeGetAigCost_rec (Dsd_Node_t *pNode)
int Dsd_TreeGetAigCost (Dsd_Node_t *pNode)
int Dsd_TreeCountNonTerminalNodes (Dsd_Manager_t *pDsdMan)
int Dsd_TreeCountNonTerminalNodesOne (Dsd_Node_t *pRoot)
int Dsd_TreeCountPrimeNodes (Dsd_Manager_t *pDsdMan)
int Dsd_TreeCountPrimeNodesOne (Dsd_Node_t *pRoot)
int Dsd_TreeCollectDecomposableVars (Dsd_Manager_t *pDsdMan, int *pVars)
Dsd_Node_t ** Dsd_TreeCollectNodesDfs (Dsd_Manager_t *pDsdMan, int *pnNodes)
Dsd_Node_t ** Dsd_TreeCollectNodesDfsOne (Dsd_Manager_t *pDsdMan, Dsd_Node_t *pNode, int *pnNodes)
void Dsd_TreePrint (FILE *pFile, Dsd_Manager_t *pDsdMan, char *pInputNames[], char *pOutputNames[], int fShortNames, int Output)
void Dsd_NodePrint (FILE *pFile, Dsd_Node_t *pNode)
DdNode * Dsd_TreeGetPrimeFunctionOld (DdManager *dd, Dsd_Node_t *pNode, int fRemap)

Variables

static int s_DepthMax
static int s_GateSizeMax
static int s_CounterBlocks
static int s_CounterPos
static int s_CounterNeg
static int s_CounterNo

Function Documentation

void Dsd_NodePrint ( FILE *  pFile,
Dsd_Node_t *  pNode 
)

Function*************************************************************

Synopsis [Prints the decompostion tree into file.]

Description []

SideEffects []

SeeAlso []

Definition at line 837 of file dsdTree.c.

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 }

void Dsd_NodePrint_rec ( FILE *  pFile,
Dsd_Node_t *  pNode,
int  fComp,
char *  pOutputName,
int  nOffset,
int *  pSigCounter 
) [static]

Function*************************************************************

Synopsis [Prints one node of the decomposition tree.]

Description []

SideEffects []

SeeAlso []

Definition at line 856 of file dsdTree.c.

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 }

int Dsd_TreeCollectDecomposableVars ( Dsd_Manager_t *  pDsdMan,
int *  pVars 
)

Function*************************************************************

Synopsis [Collects the decomposable vars on the PI side.]

Description []

SideEffects []

SeeAlso []

Definition at line 470 of file dsdTree.c.

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 }

int Dsd_TreeCollectDecomposableVars_rec ( DdManager *  dd,
Dsd_Node_t *  pNode,
int *  pVars,
int *  nVars 
) [static]

Function*************************************************************

Synopsis [Implements the recursive part of Dsd_TreeCollectDecomposableVars().]

Description [Adds decomposable variables as they are found to pVars and increments nVars. Returns 1 if a non-dec node with more than 4 inputs was encountered in the processed subtree. Returns 0, otherwise. ]

SideEffects []

SeeAlso []

Definition at line 494 of file dsdTree.c.

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 }

Dsd_Node_t** Dsd_TreeCollectNodesDfs ( Dsd_Manager_t *  pDsdMan,
int *  pnNodes 
)

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 []

Definition at line 555 of file dsdTree.c.

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 }

void Dsd_TreeCollectNodesDfs_rec ( Dsd_Node_t *  pNode,
Dsd_Node_t *  ppNodes[],
int *  pnNodes 
) [static]

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 611 of file dsdTree.c.

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 }

Dsd_Node_t** Dsd_TreeCollectNodesDfsOne ( Dsd_Manager_t *  pDsdMan,
Dsd_Node_t *  pNode,
int *  pnNodes 
)

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 []

Definition at line 585 of file dsdTree.c.

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 }

int Dsd_TreeCountNonTerminalNodes ( Dsd_Manager_t *  pDsdMan  ) 

Function*************************************************************

Synopsis [Counts non-terminal nodes of the DSD tree.]

Description [Nonterminal nodes include all the nodes with the support more than 1. These are OR, EXOR, and PRIME nodes. They do not include the elementary variable nodes and the constant 1 node.]

SideEffects []

SeeAlso []

Definition at line 310 of file dsdTree.c.

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 }

int Dsd_TreeCountNonTerminalNodes_rec ( Dsd_Node_t *  pNode  )  [static]

Function*************************************************************

Synopsis [Counts non-terminal nodes for one root.]

Description []

SideEffects []

SeeAlso []

Definition at line 354 of file dsdTree.c.

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 }

int Dsd_TreeCountNonTerminalNodesOne ( Dsd_Node_t *  pRoot  ) 

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 331 of file dsdTree.c.

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 }

int Dsd_TreeCountPrimeNodes ( Dsd_Manager_t *  pDsdMan  ) 

Function*************************************************************

Synopsis [Counts prime nodes of the DSD tree.]

Description [Prime nodes are nodes with the support more than 2, that is not an OR or EXOR gate.]

SideEffects []

SeeAlso []

Definition at line 389 of file dsdTree.c.

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 }

int Dsd_TreeCountPrimeNodes_rec ( Dsd_Node_t *  pNode  )  [static]

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 433 of file dsdTree.c.

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 }

int Dsd_TreeCountPrimeNodesOne ( Dsd_Node_t *  pRoot  ) 

Function*************************************************************

Synopsis [Counts prime nodes for one root.]

Description []

SideEffects []

SeeAlso []

Definition at line 410 of file dsdTree.c.

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 }

int Dsd_TreeGetAigCost ( Dsd_Node_t *  pNode  ) 

Function*************************************************************

Synopsis [Counts AIG nodes needed to implement this node.]

Description [Assumes that the only primes of the DSD tree are MUXes.]

SideEffects []

SeeAlso []

Definition at line 291 of file dsdTree.c.

00292 {
00293     return Dsd_TreeGetAigCost_rec( Dsd_Regular(pNode) );
00294 }

int Dsd_TreeGetAigCost_rec ( Dsd_Node_t *  pNode  ) 

Function*************************************************************

Synopsis [Counts AIG nodes needed to implement this node.]

Description []

SideEffects []

SeeAlso []

Definition at line 255 of file dsdTree.c.

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 }

void Dsd_TreeGetInfo_rec ( Dsd_Node_t *  pNode,
int  RankCur 
) [static]

Function*************************************************************

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

Description [pNode is the node, for the tree rooted in which we are determining info. RankCur is the current rank to assign to the node. fSetRank is the flag saying whether the rank will be written in the node. s_DepthMax is the maximum depths of the tree. s_GateSizeMax is the maximum gate size.]

SideEffects []

SeeAlso []

Definition at line 212 of file dsdTree.c.

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 }

DdNode* Dsd_TreeGetPrimeFunctionOld ( DdManager *  dd,
Dsd_Node_t *  pNode,
int  fRemap 
)

Function*************************************************************

Synopsis [Retuns the function of one node of the decomposition tree.]

Description [This is the old procedure. It is now superceded by the procedure Dsd_TreeGetPrimeFunction() found in "dsdLocal.c".]

SideEffects []

SeeAlso []

Definition at line 1008 of file dsdTree.c.

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 }

Dsd_Node_t* Dsd_TreeNodeCreate ( int  Type,
int  nDecs,
int  BlockNum 
)

FUNCTION DEFINITIONS ///Function*************************************************************

Synopsis [Create the DSD node.]

Description []

SideEffects []

SeeAlso []

Definition at line 61 of file dsdTree.c.

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 }

void Dsd_TreeNodeDelete ( DdManager *  dd,
Dsd_Node_t *  pNode 
)

Function*************************************************************

Synopsis [Frees the DSD node.]

Description []

SideEffects []

SeeAlso []

Definition at line 87 of file dsdTree.c.

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 }

void Dsd_TreeNodeGetInfo ( Dsd_Manager_t *  pDsdMan,
int *  DepthMax,
int *  GateSizeMax 
)

Function*************************************************************

Synopsis [Getting information about the node.]

Description [This function computes the max depth and the max gate size of the tree rooted at the node.]

SideEffects []

SeeAlso []

Definition at line 156 of file dsdTree.c.

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 }

void Dsd_TreeNodeGetInfoOne ( Dsd_Node_t *  pNode,
int *  DepthMax,
int *  GateSizeMax 
)

Function*************************************************************

Synopsis [Getting information about the node.]

Description [This function computes the max depth and the max gate size of the tree rooted at the node.]

SideEffects []

SeeAlso []

Definition at line 183 of file dsdTree.c.

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 }

void Dsd_TreePrint ( FILE *  pFile,
Dsd_Manager_t *  pDsdMan,
char *  pInputNames[],
char *  pOutputNames[],
int  fShortNames,
int  Output 
)

Function*************************************************************

Synopsis [Prints the decompostion tree into file.]

Description []

SideEffects []

SeeAlso []

Definition at line 641 of file dsdTree.c.

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 }

void Dsd_TreePrint_rec ( FILE *  pFile,
Dsd_Node_t *  pNode,
int  fComp,
char *  pInputNames[],
char *  pOutputName,
int  nOffset,
int *  pSigCounter,
int  fShortNames 
) [static]

Function*************************************************************

Synopsis [Prints the decompostion tree into file.]

Description []

SideEffects []

SeeAlso []

Definition at line 675 of file dsdTree.c.

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 }

void Dsd_TreeUnmark ( Dsd_Manager_t *  pDsdMan  ) 

Function*************************************************************

Synopsis [Unmarks the decomposition tree.]

Description [This function assumes that originally pNode->nVisits are set to zero!]

SideEffects []

SeeAlso []

Definition at line 107 of file dsdTree.c.

00108 {
00109         int i;
00110         for ( i = 0; i < pDsdMan->nRoots; i++ )
00111                 Dsd_TreeUnmark_rec( Dsd_Regular( pDsdMan->pRoots[i] ) );
00112 }

void Dsd_TreeUnmark_rec ( Dsd_Node_t *  pNode  )  [static]

CFile****************************************************************

FileName [dsdTree.c]

PackageName [DSD: Disjoint-support decomposition package.]

Synopsis [Managing the decomposition tree.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 8.0. Started - September 22, 2003.]

Revision [

Id
dsdTree.c,v 1.0 2002/22/09 00:00:00 alanmi Exp

] FUNCTION DECLARATIONS ///

Function*************************************************************

Synopsis [Recursive unmarking.]

Description [This function should be called with a non-complemented pointer.]

SideEffects []

SeeAlso []

Definition at line 127 of file dsdTree.c.

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 }

Variable Documentation

int s_CounterBlocks [static]

Definition at line 41 of file dsdTree.c.

int s_CounterNeg [static]

Definition at line 43 of file dsdTree.c.

int s_CounterNo [static]

Definition at line 44 of file dsdTree.c.

int s_CounterPos [static]

Definition at line 42 of file dsdTree.c.

int s_DepthMax [static]

STATIC VARIABLES ///

Definition at line 38 of file dsdTree.c.

int s_GateSizeMax [static]

Definition at line 39 of file dsdTree.c.

Generated on Tue Jan 5 12:18:59 2010 for abc70930 by  doxygen 1.6.1