diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2008-01-30 08:01:00 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2008-01-30 08:01:00 -0800 |
commit | 4d30a1e4f1edecff86d5066ce4653a370e59e5e1 (patch) | |
tree | 366355938a4af0a92f848841ac65374f338d691b /src/bdd/dsd | |
parent | 6537f941887b06e588d3acfc97b5fdf48875cc4e (diff) | |
download | abc-4d30a1e4f1edecff86d5066ce4653a370e59e5e1.tar.gz abc-4d30a1e4f1edecff86d5066ce4653a370e59e5e1.tar.bz2 abc-4d30a1e4f1edecff86d5066ce4653a370e59e5e1.zip |
Version abc80130
Diffstat (limited to 'src/bdd/dsd')
-rw-r--r-- | src/bdd/dsd/dsd.h | 29 | ||||
-rw-r--r-- | src/bdd/dsd/dsdApi.c | 3 | ||||
-rw-r--r-- | src/bdd/dsd/dsdCheck.c | 4 | ||||
-rw-r--r-- | src/bdd/dsd/dsdInt.h | 9 | ||||
-rw-r--r-- | src/bdd/dsd/dsdMan.c | 1 | ||||
-rw-r--r-- | src/bdd/dsd/dsdProc.c | 4 | ||||
-rw-r--r-- | src/bdd/dsd/dsdTree.c | 304 |
7 files changed, 67 insertions, 287 deletions
diff --git a/src/bdd/dsd/dsd.h b/src/bdd/dsd/dsd.h index b73b81ab..5396bacd 100644 --- a/src/bdd/dsd/dsd.h +++ b/src/bdd/dsd/dsd.h @@ -28,12 +28,8 @@ #ifndef __DSD_H__ #define __DSD_H__ -#ifdef __cplusplus -extern "C" { -#endif - //////////////////////////////////////////////////////////////////////// -/// TYPEDEF DEFINITIONS /// +/// TYPEDEF DEFITIONS /// //////////////////////////////////////////////////////////////////////// typedef struct Dsd_Manager_t_ Dsd_Manager_t; @@ -59,14 +55,14 @@ enum Dsd_Type_t_ { }; //////////////////////////////////////////////////////////////////////// -/// MACRO DEFINITIONS /// +/// MACRO DEFITIONS /// //////////////////////////////////////////////////////////////////////// // complementation and testing for pointers for decomposition entries -#define Dsd_IsComplement(p) (((int)((unsigned long) (p) & 01))) -#define Dsd_Regular(p) ((Dsd_Node_t *)((unsigned long)(p) & ~01)) -#define Dsd_Not(p) ((Dsd_Node_t *)((unsigned long)(p) ^ 01)) -#define Dsd_NotCond(p,c) ((Dsd_Node_t *)((unsigned long)(p) ^ (c))) +#define Dsd_IsComplement(p) (((int)((long) (p) & 01))) +#define Dsd_Regular(p) ((Dsd_Node_t *)((unsigned)(p) & ~01)) +#define Dsd_Not(p) ((Dsd_Node_t *)((long)(p) ^ 01)) +#define Dsd_NotCond(p,c) ((Dsd_Node_t *)((long)(p) ^ (c))) //////////////////////////////////////////////////////////////////////// /// ITERATORS /// @@ -80,7 +76,7 @@ enum Dsd_Type_t_ { Index++ ) //////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// +/// FUNCTION DEFITIONS /// //////////////////////////////////////////////////////////////////////// /*=== dsdApi.c =======================================================*/ @@ -95,7 +91,6 @@ 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 ); -extern Dsd_Node_t * Dsd_ManagerReadConst1( Dsd_Manager_t * pMan ); /*=== dsdMan.c =======================================================*/ extern Dsd_Manager_t * Dsd_ManagerStart( DdManager * dd, int nSuppMax, int fVerbose ); extern void Dsd_ManagerStop( Dsd_Manager_t * dMan ); @@ -105,7 +100,6 @@ 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 ); -extern int Dsd_TreeGetAigCost( Dsd_Node_t * pNode ); extern int Dsd_TreeCountNonTerminalNodes( Dsd_Manager_t * dMan ); extern int Dsd_TreeCountNonTerminalNodesOne( Dsd_Node_t * pRoot ); extern int Dsd_TreeCountPrimeNodes( Dsd_Manager_t * pDsdMan ); @@ -114,16 +108,11 @@ extern int Dsd_TreeCollectDecomposableVars( Dsd_Manager_t * dMan, in 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 ); -extern void Dsd_NodePrint( FILE * pFile, Dsd_Node_t * pNode ); /*=== dsdLocal.c =======================================================*/ extern DdNode * Dsd_TreeGetPrimeFunction( DdManager * dd, Dsd_Node_t * pNode ); -#ifdef __cplusplus -} -#endif - -#endif - //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// + +#endif
\ No newline at end of file diff --git a/src/bdd/dsd/dsdApi.c b/src/bdd/dsd/dsdApi.c index d1c90e23..daf3080f 100644 --- a/src/bdd/dsd/dsdApi.c +++ b/src/bdd/dsd/dsdApi.c @@ -23,7 +23,7 @@ //////////////////////////////////////////////////////////////////////// //////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// +/// FUNCTION DEFITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* @@ -89,7 +89,6 @@ 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]; } -Dsd_Node_t * Dsd_ManagerReadConst1( Dsd_Manager_t * pMan ) { return pMan->pConst1; } DdManager * Dsd_ManagerReadDd( Dsd_Manager_t * pMan ) { return pMan->dd; } //////////////////////////////////////////////////////////////////////// diff --git a/src/bdd/dsd/dsdCheck.c b/src/bdd/dsd/dsdCheck.c index 58b824d2..608aa2e3 100644 --- a/src/bdd/dsd/dsdCheck.c +++ b/src/bdd/dsd/dsdCheck.c @@ -43,7 +43,7 @@ static Dds_Cache_t * pCache; static int Dsd_CheckRootFunctionIdentity_rec( DdManager * dd, DdNode * bF1, DdNode * bF2, DdNode * bC1, DdNode * bC2 ); //////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// +/// FUNCTION DEFITIONS /// //////////////////////////////////////////////////////////////////////// /**Function******************************************************************** @@ -82,7 +82,7 @@ void Dsd_CheckCacheAllocate( int nEntries ) /**Function******************************************************************** - Synopsis [Deallocates the local cache.] + Synopsis [Delocates the local cache.] Description [] diff --git a/src/bdd/dsd/dsdInt.h b/src/bdd/dsd/dsdInt.h index 62ce7e99..5008c24e 100644 --- a/src/bdd/dsd/dsdInt.h +++ b/src/bdd/dsd/dsdInt.h @@ -23,7 +23,7 @@ #include "dsd.h" //////////////////////////////////////////////////////////////////////// -/// TYPEDEF DEFINITIONS /// +/// TYPEDEF DEFITIONS /// //////////////////////////////////////////////////////////////////////// typedef unsigned char byte; @@ -42,7 +42,6 @@ struct Dsd_Manager_t_ int nRootsAlloc;// the number of primary outputs Dsd_Node_t ** pInputs; // the primary input nodes Dsd_Node_t ** pRoots; // the primary output nodes - Dsd_Node_t * pConst1; // the constant node int fVerbose; // the verbosity level }; @@ -59,7 +58,7 @@ struct Dsd_Node_t_ }; //////////////////////////////////////////////////////////////////////// -/// MACRO DEFINITIONS /// +/// MACRO DEFITIONS /// //////////////////////////////////////////////////////////////////////// #define MAXINPUTS 1000 @@ -83,9 +82,9 @@ extern void Dsd_TreeNodeDelete( DdManager * dd, Dsd_Node_t * pNode ); extern void Dsd_TreeUnmark( Dsd_Manager_t * dMan ); extern DdNode * Dsd_TreeGetPrimeFunctionOld( DdManager * dd, Dsd_Node_t * pNode, int fRemap ); -#endif - //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// + +#endif
\ No newline at end of file diff --git a/src/bdd/dsd/dsdMan.c b/src/bdd/dsd/dsdMan.c index 6e43f0f4..4529e75a 100644 --- a/src/bdd/dsd/dsdMan.c +++ b/src/bdd/dsd/dsdMan.c @@ -73,7 +73,6 @@ Dsd_Manager_t * Dsd_ManagerStart( DdManager * dd, int nSuppMax, int fVerbose ) pNode->G = b1; Cudd_Ref( pNode->G ); pNode->S = b1; Cudd_Ref( pNode->S ); st_insert( dMan->Table, (char*)b1, (char*)pNode ); - dMan->pConst1 = pNode; Dsd_CheckCacheAllocate( 5000 ); return dMan; diff --git a/src/bdd/dsd/dsdProc.c b/src/bdd/dsd/dsdProc.c index 543ad387..08c029e1 100644 --- a/src/bdd/dsd/dsdProc.c +++ b/src/bdd/dsd/dsdProc.c @@ -1255,7 +1255,7 @@ EXIT: s_CacheEntries++; -/* +#if 0 if ( dsdKernelVerifyDecomposition(dd, pThis) == 0 ) { // write the function, for which verification does not work @@ -1277,7 +1277,7 @@ EXIT: cuddWriteFunctionSop( stdout, dd, zNewFunc, -1, dd->size, "1", s_pVarMask ); Cudd_RecursiveDerefZdd( dd, zNewFunc ); } -*/ +#endif } diff --git a/src/bdd/dsd/dsdTree.c b/src/bdd/dsd/dsdTree.c index 2855d68d..7905cbdd 100644 --- a/src/bdd/dsd/dsdTree.c +++ b/src/bdd/dsd/dsdTree.c @@ -29,7 +29,7 @@ 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 ); + //////////////////////////////////////////////////////////////////////// /// STATIC VARIABLES /// @@ -243,58 +243,6 @@ void Dsd_TreeGetInfo_rec( Dsd_Node_t * pNode, int RankCur ) /**Function************************************************************* - Synopsis [Counts AIG nodes needed to implement this node.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Dsd_TreeGetAigCost_rec( Dsd_Node_t * pNode ) -{ - int i, Counter = 0; - - assert( pNode ); - assert( !Dsd_IsComplement( pNode ) ); - assert( pNode->nVisits >= 0 ); - - if ( pNode->nDecs < 2 ) - return 0; - - // we don't want the two-input gates to count for non-decomposable blocks - if ( pNode->Type == DSD_NODE_OR ) - Counter += pNode->nDecs - 1; - else if ( pNode->Type == DSD_NODE_EXOR ) - Counter += 3*(pNode->nDecs - 1); - else if ( pNode->Type == DSD_NODE_PRIME && pNode->nDecs == 3 ) - Counter += 3; - - // call recursively - for ( i = 0; i < pNode->nDecs; i++ ) - Counter += Dsd_TreeGetAigCost_rec( Dsd_Regular(pNode->pDecs[i]) ); - return Counter; -} - -/**Function************************************************************* - - Synopsis [Counts AIG nodes needed to implement this node.] - - Description [Assumes that the only primes of the DSD tree are MUXes.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Dsd_TreeGetAigCost( Dsd_Node_t * pNode ) -{ - return Dsd_TreeGetAigCost_rec( Dsd_Regular(pNode) ); -} - -/**Function************************************************************* - Synopsis [Counts non-terminal nodes of the DSD tree.] Description [Nonterminal nodes include all the nodes with the @@ -683,21 +631,27 @@ void Dsd_TreePrint_rec( FILE * pFile, Dsd_Node_t * pNode, int fComp, char * pInp pNode->Type == DSD_NODE_PRIME || pNode->Type == DSD_NODE_OR || pNode->Type == DSD_NODE_EXOR ); Extra_PrintSymbols( pFile, ' ', nOffset, 0 ); - if ( !fComp ) - fprintf( pFile, "%s = ", pOutputName ); - else - fprintf( pFile, "NOT(%s) = ", pOutputName ); + fprintf( pFile, "%s: ", pOutputName ); pInputNums = ALLOC( int, pNode->nDecs ); if ( pNode->Type == DSD_NODE_CONST1 ) { - fprintf( pFile, " Constant 1.\n" ); + if ( fComp ) + fprintf( pFile, " Constant 0.\n" ); + else + fprintf( pFile, " Constant 1.\n" ); } else if ( pNode->Type == DSD_NODE_BUF ) { + if ( fComp ) + fprintf( pFile, " NOT(" ); + else + fprintf( pFile, " " ); if ( fShortNames ) - fprintf( pFile, "%d", 'a' + pNode->S->index ); + fprintf( pFile, "%d", pNode->S->index ); else fprintf( pFile, "%s", pInputNames[pNode->S->index] ); + if ( fComp ) + fprintf( pFile, ")" ); fprintf( pFile, "\n" ); } else if ( pNode->Type == DSD_NODE_PRIME ) @@ -710,25 +664,25 @@ void Dsd_TreePrint_rec( FILE * pFile, Dsd_Node_t * pNode, int fComp, char * pInp fCompNew = (int)( pInput != pNode->pDecs[i] ); if ( i ) fprintf( pFile, "," ); - if ( fCompNew ) - fprintf( pFile, " NOT(" ); - else - fprintf( pFile, " " ); if ( pInput->Type == DSD_NODE_BUF ) { pInputNums[i] = 0; + if ( fCompNew ) + fprintf( pFile, " NOT(" ); + else + fprintf( pFile, " " ); if ( fShortNames ) fprintf( pFile, "%d", pInput->S->index ); else fprintf( pFile, "%s", pInputNames[pInput->S->index] ); + if ( fCompNew ) + fprintf( pFile, ")" ); } else { pInputNums[i] = (*pSigCounter)++; - fprintf( pFile, "<%d>", pInputNums[i] ); + fprintf( pFile, " <%d>", pInputNums[i] ); } - if ( fCompNew ) - fprintf( pFile, ")" ); } fprintf( pFile, " )\n" ); // call recursively for the following blocks @@ -736,39 +690,43 @@ void Dsd_TreePrint_rec( FILE * pFile, Dsd_Node_t * pNode, int fComp, char * pInp if ( pInputNums[i] ) { pInput = Dsd_Regular( pNode->pDecs[i] ); + fCompNew = (int)( pInput != pNode->pDecs[i] ); sprintf( Buffer, "<%d>", pInputNums[i] ); - Dsd_TreePrint_rec( pFile, Dsd_Regular( pNode->pDecs[i] ), 0, pInputNames, Buffer, nOffset + 6, pSigCounter, fShortNames ); + Dsd_TreePrint_rec( pFile, Dsd_Regular( pNode->pDecs[i] ), fCompNew, pInputNames, Buffer, nOffset + 6, pSigCounter, fShortNames ); } } else if ( pNode->Type == DSD_NODE_OR ) { // print the line - fprintf( pFile, "OR(" ); + if ( fComp ) + fprintf( pFile, "AND(" ); + else + fprintf( pFile, "OR(" ); for ( i = 0; i < pNode->nDecs; i++ ) { pInput = Dsd_Regular( pNode->pDecs[i] ); fCompNew = (int)( pInput != pNode->pDecs[i] ); if ( i ) fprintf( pFile, "," ); - if ( fCompNew ) - fprintf( pFile, " NOT(" ); - else - fprintf( pFile, " " ); if ( pInput->Type == DSD_NODE_BUF ) { pInputNums[i] = 0; + if ( fCompNew ) + fprintf( pFile, " NOT(" ); + else + fprintf( pFile, " " ); if ( fShortNames ) - fprintf( pFile, "%c", 'a' + pInput->S->index ); + fprintf( pFile, "%d", pInput->S->index ); else fprintf( pFile, "%s", pInputNames[pInput->S->index] ); + if ( fCompNew ) + fprintf( pFile, ")" ); } else { pInputNums[i] = (*pSigCounter)++; - fprintf( pFile, "<%d>", pInputNums[i] ); + fprintf( pFile, " <%d>", pInputNums[i] ); } - if ( fCompNew ) - fprintf( pFile, ")" ); } fprintf( pFile, " )\n" ); // call recursively for the following blocks @@ -776,208 +734,43 @@ void Dsd_TreePrint_rec( FILE * pFile, Dsd_Node_t * pNode, int fComp, char * pInp if ( pInputNums[i] ) { pInput = Dsd_Regular( pNode->pDecs[i] ); + fCompNew = (int)( pInput != pNode->pDecs[i] ); sprintf( Buffer, "<%d>", pInputNums[i] ); - Dsd_TreePrint_rec( pFile, Dsd_Regular( pNode->pDecs[i] ), 0, pInputNames, Buffer, nOffset + 6, pSigCounter, fShortNames ); + Dsd_TreePrint_rec( pFile, Dsd_Regular( pNode->pDecs[i] ), fComp ^ fCompNew, pInputNames, Buffer, nOffset + 6, pSigCounter, fShortNames ); } } else if ( pNode->Type == DSD_NODE_EXOR ) { // print the line - fprintf( pFile, "EXOR(" ); + if ( fComp ) + fprintf( pFile, "NEXOR(" ); + else + fprintf( pFile, "EXOR(" ); for ( i = 0; i < pNode->nDecs; i++ ) { pInput = Dsd_Regular( pNode->pDecs[i] ); fCompNew = (int)( pInput != pNode->pDecs[i] ); if ( i ) fprintf( pFile, "," ); - if ( fCompNew ) - fprintf( pFile, " NOT(" ); - else - fprintf( pFile, " " ); if ( pInput->Type == DSD_NODE_BUF ) { pInputNums[i] = 0; + if ( fCompNew ) + fprintf( pFile, " NOT(" ); + else + fprintf( pFile, " " ); if ( fShortNames ) - fprintf( pFile, "%c", 'a' + pInput->S->index ); + fprintf( pFile, "%d", pInput->S->index ); else fprintf( pFile, "%s", pInputNames[pInput->S->index] ); - } - else - { - pInputNums[i] = (*pSigCounter)++; - fprintf( pFile, "<%d>", pInputNums[i] ); - } - if ( fCompNew ) - fprintf( pFile, ")" ); - } - fprintf( pFile, " )\n" ); - // call recursively for the following blocks - for ( i = 0; i < pNode->nDecs; i++ ) - if ( pInputNums[i] ) - { - pInput = Dsd_Regular( pNode->pDecs[i] ); - sprintf( Buffer, "<%d>", pInputNums[i] ); - Dsd_TreePrint_rec( pFile, Dsd_Regular( pNode->pDecs[i] ), 0, pInputNames, Buffer, nOffset + 6, pSigCounter, fShortNames ); - } - } - free( pInputNums ); -} - -/**Function************************************************************* - - Synopsis [Prints the decompostion tree into file.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Dsd_NodePrint( FILE * pFile, Dsd_Node_t * pNode ) -{ - Dsd_Node_t * pNodeR; - int SigCounter = 1; - pNodeR = Dsd_Regular(pNode); - Dsd_NodePrint_rec( pFile, pNodeR, pNodeR != pNode, "F", 0, &SigCounter ); -} - -/**Function************************************************************* - - Synopsis [Prints one node of the decomposition tree.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Dsd_NodePrint_rec( FILE * pFile, Dsd_Node_t * pNode, int fComp, char * pOutputName, int nOffset, int * pSigCounter ) -{ - char Buffer[100]; - Dsd_Node_t * pInput; - int * pInputNums; - int fCompNew, i; - - assert( pNode->Type == DSD_NODE_BUF || pNode->Type == DSD_NODE_CONST1 || - pNode->Type == DSD_NODE_PRIME || pNode->Type == DSD_NODE_OR || pNode->Type == DSD_NODE_EXOR ); - - Extra_PrintSymbols( pFile, ' ', nOffset, 0 ); - if ( !fComp ) - fprintf( pFile, "%s = ", pOutputName ); - else - fprintf( pFile, "NOT(%s) = ", pOutputName ); - pInputNums = ALLOC( int, pNode->nDecs ); - if ( pNode->Type == DSD_NODE_CONST1 ) - { - fprintf( pFile, " Constant 1.\n" ); - } - else if ( pNode->Type == DSD_NODE_BUF ) - { - fprintf( pFile, " " ); - fprintf( pFile, "%c", 'a' + pNode->S->index ); - fprintf( pFile, "\n" ); - } - else if ( pNode->Type == DSD_NODE_PRIME ) - { - // print the line - fprintf( pFile, "PRIME(" ); - for ( i = 0; i < pNode->nDecs; i++ ) - { - pInput = Dsd_Regular( pNode->pDecs[i] ); - fCompNew = (int)( pInput != pNode->pDecs[i] ); - assert( fCompNew == 0 ); - if ( i ) - fprintf( pFile, "," ); - if ( pInput->Type == DSD_NODE_BUF ) - { - pInputNums[i] = 0; - fprintf( pFile, " %c", 'a' + pInput->S->index ); - } - else - { - pInputNums[i] = (*pSigCounter)++; - fprintf( pFile, " <%d>", pInputNums[i] ); - } - if ( fCompNew ) - fprintf( pFile, "\'" ); - } - fprintf( pFile, " )\n" ); -/* - fprintf( pFile, " ) " ); - { - DdNode * bLocal; - bLocal = Dsd_TreeGetPrimeFunction( dd, pNodeDsd ); Cudd_Ref( bLocal ); - Extra_bddPrint( dd, bLocal ); - Cudd_RecursiveDeref( dd, bLocal ); - } -*/ - // call recursively for the following blocks - for ( i = 0; i < pNode->nDecs; i++ ) - if ( pInputNums[i] ) - { - pInput = Dsd_Regular( pNode->pDecs[i] ); - sprintf( Buffer, "<%d>", pInputNums[i] ); - Dsd_NodePrint_rec( pFile, Dsd_Regular( pNode->pDecs[i] ), 0, Buffer, nOffset + 6, pSigCounter ); - } - } - else if ( pNode->Type == DSD_NODE_OR ) - { - // print the line - fprintf( pFile, "OR(" ); - for ( i = 0; i < pNode->nDecs; i++ ) - { - pInput = Dsd_Regular( pNode->pDecs[i] ); - fCompNew = (int)( pInput != pNode->pDecs[i] ); - if ( i ) - fprintf( pFile, "," ); - if ( pInput->Type == DSD_NODE_BUF ) - { - pInputNums[i] = 0; - fprintf( pFile, " %c", 'a' + pInput->S->index ); - } - else - { - pInputNums[i] = (*pSigCounter)++; - fprintf( pFile, " <%d>", pInputNums[i] ); - } - if ( fCompNew ) - fprintf( pFile, "\'" ); - } - fprintf( pFile, " )\n" ); - // call recursively for the following blocks - for ( i = 0; i < pNode->nDecs; i++ ) - if ( pInputNums[i] ) - { - pInput = Dsd_Regular( pNode->pDecs[i] ); - sprintf( Buffer, "<%d>", pInputNums[i] ); - Dsd_NodePrint_rec( pFile, Dsd_Regular( pNode->pDecs[i] ), 0, Buffer, nOffset + 6, pSigCounter ); - } - } - else if ( pNode->Type == DSD_NODE_EXOR ) - { - // print the line - fprintf( pFile, "EXOR(" ); - for ( i = 0; i < pNode->nDecs; i++ ) - { - pInput = Dsd_Regular( pNode->pDecs[i] ); - fCompNew = (int)( pInput != pNode->pDecs[i] ); - assert( fCompNew == 0 ); - if ( i ) - fprintf( pFile, "," ); - if ( pInput->Type == DSD_NODE_BUF ) - { - pInputNums[i] = 0; - fprintf( pFile, " %c", 'a' + pInput->S->index ); + if ( fCompNew ) + fprintf( pFile, ")" ); } else { pInputNums[i] = (*pSigCounter)++; fprintf( pFile, " <%d>", pInputNums[i] ); } - if ( fCompNew ) - fprintf( pFile, "\'" ); } fprintf( pFile, " )\n" ); // call recursively for the following blocks @@ -985,8 +778,9 @@ void Dsd_NodePrint_rec( FILE * pFile, Dsd_Node_t * pNode, int fComp, char * pOut if ( pInputNums[i] ) { pInput = Dsd_Regular( pNode->pDecs[i] ); + fCompNew = (int)( pInput != pNode->pDecs[i] ); sprintf( Buffer, "<%d>", pInputNums[i] ); - Dsd_NodePrint_rec( pFile, Dsd_Regular( pNode->pDecs[i] ), 0, Buffer, nOffset + 6, pSigCounter ); + Dsd_TreePrint_rec( pFile, Dsd_Regular( pNode->pDecs[i] ), fCompNew, pInputNames, Buffer, nOffset + 6, pSigCounter, fShortNames ); } } free( pInputNums ); |