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

00001 
00019 #include "dsdInt.h"
00020 
00021 
00025 
00026 // the most important procedures
00027 void dsdKernelDecompose( Dsd_Manager_t * pDsdMan, DdNode ** pbFuncs, int nFuncs );
00028 static Dsd_Node_t * dsdKernelDecompose_rec( Dsd_Manager_t * pDsdMan, DdNode * F );
00029 
00030 // additional procedures
00031 static Dsd_Node_t * dsdKernelFindContainingComponent( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pWhere, DdNode * Var, int * fPolarity );
00032 static int dsdKernelFindCommonComponents( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pL, Dsd_Node_t * pH, Dsd_Node_t *** pCommon, Dsd_Node_t ** pLastDiffL, Dsd_Node_t ** pLastDiffH );
00033 static void dsdKernelComputeSumOfComponents( Dsd_Manager_t * pDsdMan, Dsd_Node_t ** pCommon, int nCommon, DdNode ** pCompF, DdNode ** pCompS, int fExor );
00034 static int dsdKernelCheckContainment( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pL, Dsd_Node_t * pH, Dsd_Node_t ** pLarge, Dsd_Node_t ** pSmall );
00035 
00036 // list copying
00037 static void dsdKernelCopyListPlusOne( Dsd_Node_t * p, Dsd_Node_t * First, Dsd_Node_t ** ppList, int nListSize );
00038 static void dsdKernelCopyListPlusOneMinusOne( Dsd_Node_t * p, Dsd_Node_t * First, Dsd_Node_t ** ppList, int nListSize, int Skipped );
00039 
00040 // debugging procedures
00041 static int dsdKernelVerifyDecomposition( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pDE );
00042 
00046 
00047 // the counter of marks
00048 static int s_Mark;
00049 
00050 // debugging flag
00051 static int s_Show = 0;
00052 // temporary var used for debugging
00053 static int Depth = 0;
00054 
00055 static int s_Loops1;
00056 static int s_Loops2;
00057 static int s_Loops3;
00058 static int s_Pivot;
00059 static int s_PivotNo;
00060 static int s_Common;
00061 static int s_CommonNo;
00062 
00063 static int s_Case4Calls;
00064 static int s_Case4CallsSpecial;
00065 
00066 static int s_Case5;
00067 static int s_Loops2Useless;
00068 
00069 
00070 static int s_DecNodesTotal;
00071 static int s_DecNodesUsed;
00072 
00073 // statistical variables
00074 static int   s_nDecBlocks;
00075 static int   s_nLiterals;
00076 static int   s_nExorGates; 
00077 static int   s_nReusedBlocks;
00078 static int   s_nCascades;
00079 static float s_nArea;    
00080 static float s_MaxDelay;
00081 static long  s_Time;
00082 static int   s_nInvertors;
00083 static int   s_nPrimeBlocks;
00084 
00085 static int HashSuccess = 0;
00086 static int HashFailure = 0;
00087 
00088 static int s_CacheEntries;
00089 
00090 
00094 
00120 void Dsd_Decompose( Dsd_Manager_t * pDsdMan, DdNode ** pbFuncs, int nFuncs )
00121 {
00122         DdManager * dd = pDsdMan->dd;
00123         int i;
00124         long clk;
00125         Dsd_Node_t * pTemp;
00126         int SumMaxGateSize = 0;
00127         int nDecOutputs = 0;
00128         int nCBFOutputs = 0;
00129 /*
00130 s_Loops1 = 0;
00131 s_Loops2 = 0;
00132 s_Loops3 = 0;
00133 s_Case4Calls = 0;
00134 s_Case4CallsSpecial = 0;
00135 s_Case5 = 0;
00136 s_Loops2Useless = 0;
00137 */
00138         // resize the number of roots in the manager
00139         if ( pDsdMan->nRootsAlloc < nFuncs )
00140         {
00141                 if ( pDsdMan->nRootsAlloc > 0 )
00142                         free( pDsdMan->pRoots );
00143                 pDsdMan->nRootsAlloc = nFuncs;
00144                 pDsdMan->pRoots = (Dsd_Node_t **) malloc( pDsdMan->nRootsAlloc * sizeof(Dsd_Node_t *) );
00145         }
00146 
00147         if ( pDsdMan->fVerbose )
00148                 printf( "\nDecomposability statistics for individual outputs:\n" );
00149 
00150         // set the counter of decomposition nodes
00151         s_nDecBlocks = 0;
00152 
00153         // perform decomposition for all outputs
00154         clk = clock();
00155         pDsdMan->nRoots = 0;
00156         s_nCascades = 0;
00157         for ( i = 0; i < nFuncs; i++ )
00158         {
00159                 int nLiteralsPrev;
00160                 int nDecBlocksPrev;
00161                 int nExorGatesPrev;
00162                 int nReusedBlocksPres;
00163                 int nCascades;
00164                 int MaxBlock;
00165                 int nPrimeBlocks;
00166                 long clk;
00167 
00168                 clk = clock();
00169                 nLiteralsPrev     = s_nLiterals;
00170                 nDecBlocksPrev    = s_nDecBlocks;
00171                 nExorGatesPrev    = s_nExorGates;
00172                 nReusedBlocksPres = s_nReusedBlocks;
00173                 nPrimeBlocks      = s_nPrimeBlocks;
00174 
00175                 pDsdMan->pRoots[ pDsdMan->nRoots++ ] = dsdKernelDecompose_rec( pDsdMan, pbFuncs[i] );
00176 
00177                 Dsd_TreeNodeGetInfoOne( pDsdMan->pRoots[i], &nCascades, &MaxBlock );
00178                 s_nCascades = ddMax( s_nCascades, nCascades );
00179                 pTemp = Dsd_Regular(pDsdMan->pRoots[i]);
00180                 if ( pTemp->Type != DSD_NODE_PRIME || pTemp->nDecs != Extra_bddSuppSize(dd,pTemp->S) )
00181                         nDecOutputs++;
00182                 if ( MaxBlock < 3 )
00183                         nCBFOutputs++;
00184                 SumMaxGateSize += MaxBlock;
00185 
00186                 if ( pDsdMan->fVerbose )
00187                 {
00188                         printf("#%02d: ", i );                              
00189                         printf("Ins=%2d. ", Cudd_SupportSize(dd,pbFuncs[i]) );                  
00190                         printf("Gts=%3d. ", Dsd_TreeCountNonTerminalNodesOne( pDsdMan->pRoots[i] ) ); 
00191                         printf("Pri=%3d. ", Dsd_TreeCountPrimeNodesOne( pDsdMan->pRoots[i] ) ); 
00192                         printf("Max=%3d. ", MaxBlock ); 
00193                         printf("Reuse=%2d. ", s_nReusedBlocks-nReusedBlocksPres ); 
00194                         printf("Csc=%2d. ", nCascades ); 
00195                         printf("T= %.2f s. ", (float)(clock()-clk)/(float)(CLOCKS_PER_SEC) ) ;
00196                         printf("Bdd=%2d. ", Cudd_DagSize(pbFuncs[i]) ); 
00197                         printf("\n");
00198                         fflush( stdout );
00199                 }
00200         }
00201         assert( pDsdMan->nRoots == nFuncs );
00202 
00203         if ( pDsdMan->fVerbose )
00204         {
00205                 printf( "\n" );
00206                 printf( "The cumulative decomposability statistics:\n" );
00207                 printf( "  Total outputs                             = %5d\n", nFuncs );
00208                 printf( "  Decomposable outputs                      = %5d\n", nDecOutputs );
00209                 printf( "  Completely decomposable outputs           = %5d\n", nCBFOutputs );
00210                 printf( "  The sum of max gate sizes                 = %5d\n", SumMaxGateSize );
00211                 printf( "  Shared BDD size                           = %5d\n", Cudd_SharingSize( pbFuncs, nFuncs ) );
00212                 printf( "  Decomposition entries                     = %5d\n", st_count( pDsdMan->Table ) );
00213                 printf( "  Pure decomposition time                   =  %.2f sec\n", (float)(clock() - clk)/(float)(CLOCKS_PER_SEC) );
00214         }
00215 /*
00216     printf( "s_Loops1 = %d.\n", s_Loops1 );
00217     printf( "s_Loops2 = %d.\n", s_Loops2 );
00218     printf( "s_Loops3 = %d.\n", s_Loops3 );
00219     printf( "s_Case4Calls = %d.\n", s_Case4Calls );
00220     printf( "s_Case4CallsSpecial = %d.\n", s_Case4CallsSpecial );
00221     printf( "s_Case5 = %d.\n", s_Case5 );
00222     printf( "s_Loops2Useless = %d.\n", s_Loops2Useless );
00223 */
00224 }
00225 
00237 Dsd_Node_t * Dsd_DecomposeOne( Dsd_Manager_t * pDsdMan, DdNode * bFunc )
00238 {
00239     return dsdKernelDecompose_rec( pDsdMan, bFunc );
00240 }
00241 
00253 Dsd_Node_t * dsdKernelDecompose_rec( Dsd_Manager_t * pDsdMan, DdNode * bFunc0 )
00254 {
00255         DdManager * dd = pDsdMan->dd;
00256         DdNode * bLow;
00257         DdNode * bLowR;
00258         DdNode * bHigh;
00259 
00260         int      VarInt;
00261         DdNode * bVarCur;
00262         Dsd_Node_t *     pVarCurDE; 
00263         // works only if var indices start from 0!!!
00264         DdNode * bSuppNew = NULL, * bTemp;
00265 
00266         int fContained;
00267         int nSuppLH;
00268         int nSuppL;
00269         int nSuppH;
00270 
00271 
00272 
00273         // various decomposition nodes
00274         Dsd_Node_t * pThis, * pL, * pH, * pLR, * pHR;
00275 
00276         Dsd_Node_t * pSmallR, * pLargeR;
00277         Dsd_Node_t * pTableEntry;
00278 
00279 
00280         // treat the complemented case
00281         DdNode * bF = Cudd_Regular(bFunc0);
00282         int  fCompF = (int)(bF != bFunc0);
00283 
00284         // check cache
00285         if ( st_lookup( pDsdMan->Table, (char*)bF, (char**)&pTableEntry ) )
00286         { // the entry is present 
00287         HashSuccess++;
00288         return Dsd_NotCond( pTableEntry, fCompF );
00289     }
00290     HashFailure++;
00291         Depth++;
00292 
00293         // proceed to consider "four cases"
00295         // TERMINAL CASES - CASES 1 and 2
00297         bLow    = cuddE(bF);
00298         bLowR   = Cudd_Regular(bLow);
00299         bHigh   = cuddT(bF);
00300         VarInt    = bF->index;
00301         bVarCur   = dd->vars[VarInt];
00302         pVarCurDE = pDsdMan->pInputs[VarInt]; 
00303         // works only if var indices start from 0!!!
00304         bSuppNew = NULL;
00305 
00306         if ( bLowR->index == CUDD_CONST_INDEX || bHigh->index == CUDD_CONST_INDEX )
00307         { // one of the cofactors in the constant
00308                 if ( bHigh == b1 )  // bHigh cannot be equal to b0, because then it will be complemented
00309                   if ( bLow == b0 ) // bLow cannot be equal to b1, because then the node will have bLow == bHigh
00311                   // bLow == 0, bHigh == 1, F = x'&0 + x&1 = x
00313                   { // create the elementary variable node
00314                         assert(0); // should be already in the hash table
00315                         pThis = Dsd_TreeNodeCreate( DSD_NODE_BUF, 1, s_nDecBlocks++ );
00316                         pThis->pDecs[0] = NULL;
00317                   }
00318                   else // if ( bLow != constant )
00320                   // bLow != const, bHigh == 1, F = x'&bLow + x&1 = bLow + x  --- DSD_NODE_OR(x,bLow)
00322                   {
00323                         pL  = dsdKernelDecompose_rec( pDsdMan, bLow );
00324                         pLR = Dsd_Regular( pL );
00325                         bSuppNew = Cudd_bddAnd( dd, bVarCur, pLR->S ); Cudd_Ref(bSuppNew);
00326                         if ( pLR->Type == DSD_NODE_OR && pL == pLR ) // OR and no complement
00327                         { // add to the components
00328                                 pThis = Dsd_TreeNodeCreate( DSD_NODE_OR, pL->nDecs+1, s_nDecBlocks++ );
00329                                 dsdKernelCopyListPlusOne( pThis, pVarCurDE, pL->pDecs, pL->nDecs );
00330                         }
00331                         else // all other cases
00332                         { // create a new 2-input OR-gate
00333                                 pThis = Dsd_TreeNodeCreate( DSD_NODE_OR, 2, s_nDecBlocks++ );
00334                                 dsdKernelCopyListPlusOne( pThis, pVarCurDE, &pL, 1 );
00335                         }
00336                   }
00337                 else // if ( bHigh != const ) // meaning that bLow should be a constant
00338                 {
00339                   pH = dsdKernelDecompose_rec( pDsdMan, bHigh );
00340                   pHR = Dsd_Regular( pH );
00341                   bSuppNew = Cudd_bddAnd( dd, bVarCur, pHR->S ); Cudd_Ref(bSuppNew);
00342                   if ( bLow == b0 )
00344                   // Low == 0, High != 1, F = x'&0+x&High = (x'+High')'--- NOR(x',High')
00346                     if ( pHR->Type == DSD_NODE_OR && pH != pHR ) // DSD_NODE_OR and complement
00347                         { // add to the components
00348                           pThis = Dsd_TreeNodeCreate( DSD_NODE_OR, pHR->nDecs+1, s_nDecBlocks++ );
00349                           dsdKernelCopyListPlusOne( pThis, Dsd_Not(pVarCurDE), pHR->pDecs, pHR->nDecs );
00350                           pThis = Dsd_Not(pThis);
00351                         }
00352                     else // all other cases
00353                         { // create a new 2-input NOR gate
00354                           pThis = Dsd_TreeNodeCreate( DSD_NODE_OR, 2, s_nDecBlocks++ );
00355                           pH = Dsd_Not(pH);
00356                           dsdKernelCopyListPlusOne( pThis, Dsd_Not(pVarCurDE), &pH, 1 );
00357                           pThis = Dsd_Not(pThis);
00358                         }
00359                   else // if ( bLow == b1 )
00361                   // Low == 1, High != 1, F = x'&1 + x&High = x' + High --- DSD_NODE_OR(x',High)
00363                         if ( pHR->Type == DSD_NODE_OR && pH == pHR ) // OR and no complement
00364                         { // add to the components
00365                                 pThis = Dsd_TreeNodeCreate( DSD_NODE_OR, pH->nDecs+1, s_nDecBlocks++ );
00366                                 dsdKernelCopyListPlusOne( pThis, Dsd_Not(pVarCurDE), pH->pDecs, pH->nDecs );
00367                         }
00368                         else // all other cases
00369                         { // create a new 2-input OR-gate
00370                                 pThis = Dsd_TreeNodeCreate( DSD_NODE_OR, 2, s_nDecBlocks++ );
00371                                 dsdKernelCopyListPlusOne( pThis, Dsd_Not(pVarCurDE), &pH, 1 );
00372                         }
00373                 }
00374                 goto EXIT;
00375         }
00376         // else if ( bLow != const && bHigh != const )
00377 
00378         // the case of equal cofactors (up to complementation)
00379         if ( bLowR == bHigh )
00381         // Low == G, High == G', F = x'&G + x&G' = (x(+)G) --- EXOR(x,Low)
00383         {
00384                 pL  = dsdKernelDecompose_rec( pDsdMan, bLow );
00385                 pLR = Dsd_Regular( pL );
00386                 bSuppNew = Cudd_bddAnd( dd, bVarCur, pLR->S ); Cudd_Ref(bSuppNew);
00387                 if ( pLR->Type == DSD_NODE_EXOR ) // complemented or not - does not matter!
00388                 { // add to the components
00389                         pThis = Dsd_TreeNodeCreate( DSD_NODE_EXOR, pLR->nDecs+1, s_nDecBlocks++ );
00390                         dsdKernelCopyListPlusOne( pThis, pVarCurDE, pLR->pDecs, pLR->nDecs );
00391                         if ( pL != pLR )
00392                                 pThis = Dsd_Not( pThis );
00393                 }
00394                 else // all other cases
00395                 { // create a new 2-input EXOR-gate
00396                         pThis = Dsd_TreeNodeCreate( DSD_NODE_EXOR, 2, s_nDecBlocks++ );
00397                         if ( pL != pLR ) // complemented
00398                         {
00399                                 dsdKernelCopyListPlusOne( pThis, pVarCurDE, &pLR, 1 );
00400                                 pThis = Dsd_Not( pThis );
00401                         }
00402                         else // non-complemented
00403                                 dsdKernelCopyListPlusOne( pThis, pVarCurDE, &pL, 1 );
00404                 }
00405                 goto EXIT;
00406         }
00407 
00409         // solve subproblems
00411         pL   = dsdKernelDecompose_rec( pDsdMan, bLow );
00412         pH   = dsdKernelDecompose_rec( pDsdMan, bHigh );
00413         pLR  = Dsd_Regular( pL );
00414         pHR  = Dsd_Regular( pH );
00415 
00416         assert( pLR->Type == DSD_NODE_BUF || pLR->Type == DSD_NODE_OR || pLR->Type == DSD_NODE_EXOR || pLR->Type == DSD_NODE_PRIME );
00417         assert( pHR->Type == DSD_NODE_BUF || pHR->Type == DSD_NODE_OR || pHR->Type == DSD_NODE_EXOR || pHR->Type == DSD_NODE_PRIME );
00418 
00419 /*
00420 if ( Depth == 1 )
00421 {
00422 //      PRK(bLow,pDecTreeTotal->nInputs);
00423 //      PRK(bHigh,pDecTreeTotal->nInputs);
00424 if ( s_Show )
00425 {
00426         PRD( pL );
00427         PRD( pH );
00428 }
00429 }
00430 */
00431         // compute the new support
00432         bTemp    = Cudd_bddAnd( dd, pLR->S, pHR->S );   Cudd_Ref( bTemp );
00433         nSuppL   = Extra_bddSuppSize( dd, pLR->S );
00434         nSuppH   = Extra_bddSuppSize( dd, pHR->S );
00435         nSuppLH  = Extra_bddSuppSize( dd, bTemp );
00436         bSuppNew = Cudd_bddAnd( dd, bTemp, bVarCur );   Cudd_Ref( bSuppNew );
00437         Cudd_RecursiveDeref( dd, bTemp );
00438 
00439 
00440         // several possibilities are possible
00441         // (1) support of one component contains another
00442         // (2) none of the supports is contained in another
00443         fContained = dsdKernelCheckContainment( pDsdMan, pLR, pHR, &pLargeR, &pSmallR );
00444 
00446         // CASE 3.b One of the cofactors in a constant (OR and EXOR)
00448         // the support of the larger component should contain the support of the smaller
00449         // it is possible to have PRIME function in this role
00450         // for example: F = ITE( a+b, c(+)d, e+f ), F0 = ITE( b, c(+)d, e+f ), F1 = c(+)d
00451         if ( fContained )
00452         {
00453                 Dsd_Node_t * pSmall, * pLarge;
00454                 int c, iCompLarge; // the number of the component is Large is equal to the whole of Small
00455                 int fLowIsLarge;
00456 
00457                 DdNode * bFTemp;     // the changed input function
00458                 Dsd_Node_t * pDETemp, * pDENew;
00459 
00460                 Dsd_Node_t * pComp = NULL;
00461                 int  nComp;
00462 
00463                 if ( pSmallR == pLR )
00464                 { // Low is Small => High is Large
00465                         pSmall = pL;
00466                         pLarge = pH;
00467                         fLowIsLarge = 0;
00468                 }
00469                 else
00470                 { // vice versa
00471                         pSmall = pH;
00472                         pLarge = pL;
00473                         fLowIsLarge = 1;
00474                 }
00475 
00476                 // treat the situation when the larger is PRIME
00477                 if ( pLargeR->Type == DSD_NODE_PRIME ) //&& pLargeR->nDecs != pSmallR->nDecs )
00478                 {
00479                         // QUESTION: Is it possible for pLargeR->nDecs > 3 
00480                         // and pSmall contained as one of input in pLarge?
00481                         // Yes, for example F = a'c + a & MUX(b,c',d) = a'c + abc' + ab'd is non-decomposable
00482                         // Consider the function H(a->xy) = F( xy, b, c, d )
00483                         // H0 = H(x=0) = F(0,b,c,d) = c
00484                         // H1 = F(x=1) = F(y,b,c,d) - non-decomposable
00485                         //
00486                         // QUESTION: Is it possible that pLarge is PRIME(3) and pSmall is OR(2),
00487                         // which is not contained in PRIME as one input?
00488                         // Yes, for example F = abcd + b'c'd' + a'c'd' = PRIME(ab, c, d)
00489                         // F(a=0) = c'd' = NOT(OR(a,d))  F(a=1) = bcd + b'c'd' = PRIME(b,c,d)
00490                         // To find decomposition, we have to prove that F(a=1)|b=0 = F(a=0)
00491 
00492                         // Is it possible that (pLargeR->nDecs == pSmallR->nDecs) and yet this case holds?
00493                         // Yes, consider the function such that F(a=0) = PRIME(a,b+c,d,e) and F(a=1) = OR(b,c,d,e)
00494                         // They have the same number of inputs and it is possible that they will be the cofactors
00495                         // as discribed in the previous example.
00496 
00497                         // find the component, which when substituted for 0 or 1, produces the desired result
00498                         int g, fFoundComp; // {0,1} depending on whether setting cofactor to 0 or 1 worked out
00499 
00500                         DdNode * bLarge, * bSmall;
00501                         if ( fLowIsLarge )
00502                         {
00503                                 bLarge = bLow;
00504                                 bSmall = bHigh;
00505                         }
00506                         else
00507                         {
00508                                 bLarge = bHigh;
00509                                 bSmall = bLow;
00510                         }
00511 
00512                         for ( g = 0; g < pLargeR->nDecs; g++ )
00513 //                      if ( g != c )
00514                         {
00515                                 pDETemp = pLargeR->pDecs[g]; // cannot be complemented
00516                                 if ( Dsd_CheckRootFunctionIdentity( dd, bLarge, bSmall, pDETemp->G, b1 ) )
00517                                 {
00518                                         fFoundComp = 1;
00519                                         break;
00520                                 }
00521 
00522                                 s_Loops1++;
00523 
00524                                 if ( Dsd_CheckRootFunctionIdentity( dd, bLarge, bSmall, Cudd_Not(pDETemp->G), b1 ) )
00525                                 {
00526                                         fFoundComp = 0;
00527                                         break;
00528                                 }
00529 
00530                                 s_Loops1++;
00531                         }
00532 
00533                         if ( g != pLargeR->nDecs ) 
00534                         { // decomposition is found
00535                                 if ( fFoundComp )
00536                                         if ( fLowIsLarge )
00537                                                 bFTemp = Cudd_bddOr( dd, bVarCur, pLargeR->pDecs[g]->G );
00538                                         else
00539                                                 bFTemp = Cudd_bddOr( dd, Cudd_Not(bVarCur), pLargeR->pDecs[g]->G );
00540                                 else
00541                                         if ( fLowIsLarge )
00542                                                 bFTemp = Cudd_bddAnd( dd, Cudd_Not(bVarCur), pLargeR->pDecs[g]->G );
00543                                         else
00544                                                 bFTemp = Cudd_bddAnd( dd, bVarCur, pLargeR->pDecs[g]->G );
00545                                 Cudd_Ref( bFTemp );
00546 
00547                                 pDENew = dsdKernelDecompose_rec( pDsdMan, bFTemp );
00548                                 pDENew = Dsd_Regular( pDENew );
00549                                 Cudd_RecursiveDeref( dd, bFTemp );
00550 
00551                                 // get the new gate
00552                                 pThis = Dsd_TreeNodeCreate( DSD_NODE_PRIME, pLargeR->nDecs, s_nDecBlocks++ );
00553                                 dsdKernelCopyListPlusOneMinusOne( pThis, pDENew, pLargeR->pDecs, pLargeR->nDecs, g );
00554                                 goto EXIT;
00555                         }
00556                 }
00557 
00558                 // try to find one component in the pLarger that is equal to the whole of pSmaller
00559                 for ( c = 0; c < pLargeR->nDecs; c++ )
00560                         if ( pLargeR->pDecs[c] == pSmall || pLargeR->pDecs[c] == Dsd_Not(pSmall) )
00561                         {
00562                                 iCompLarge = c;
00563                                 break;
00564                         }
00565 
00566                 // assign the equal component
00567                 if ( c != pLargeR->nDecs )  // the decomposition is possible!
00568                 { 
00569                         pComp  = pLargeR->pDecs[iCompLarge];
00570                         nComp  = 1;
00571                 }
00572                 else // the decomposition is still possible
00573                 { // for example F = OR(ab,c,d), F(a=0) = OR(c,d), F(a=1) = OR(b,c,d)
00574                         // supp(F0) is contained in supp(F1), Polarity(F(a=0)) == Polarity(F(a=1))
00575 
00576                         // try to find a group of common components
00577                         if ( pLargeR->Type == pSmallR->Type &&
00578                                 (pLargeR->Type == DSD_NODE_EXOR || pSmallR->Type == DSD_NODE_OR&& ((pLarge==pLargeR) == (pSmall==pSmallR))) )
00579                         {
00580                                 Dsd_Node_t ** pCommon, * pLastDiffL = NULL, * pLastDiffH = NULL; 
00581                                 int nCommon = dsdKernelFindCommonComponents( pDsdMan, pLargeR, pSmallR, &pCommon, &pLastDiffL, &pLastDiffH );
00582                                 // if all the components of pSmall are contained in pLarge,
00583                                 // then the decomposition exists
00584                                 if ( nCommon == pSmallR->nDecs )
00585                                 {
00586                                         pComp = pSmallR;
00587                                         nComp = pSmallR->nDecs;
00588                                 }
00589                         }
00590                 }
00591 
00592                 if ( pComp ) // the decomposition is possible!
00593                 {
00594 //                      Dsd_Node_t * pComp  = pLargeR->pDecs[iCompLarge];
00595                         Dsd_Node_t * pCompR = Dsd_Regular( pComp );
00596                         int fComp1 = (int)( pLarge != pLargeR );
00597                         int fComp2 = (int)( pComp  != pCompR );
00598                         int fComp3 = (int)( pSmall != pSmallR );
00599 
00600                         DdNode * bFuncComp;  // the function of the given component
00601                         DdNode * bFuncNew;   // the function of the input component
00602 
00603                         if ( pLargeR->Type == DSD_NODE_OR ) // Figure 4 of Matsunaga's paper
00604                         { 
00605                                 // the decomposition exists only if the polarity assignment 
00606                                 // along the paths is the same
00607                                 if ( (fComp1 ^ fComp2) == fComp3 )
00608                                 { // decomposition exists = consider 4 cases
00609                                         // consideration of cases leads to the following conclusion
00610                                         // fComp1 gives the polarity of the resulting DSD_NODE_OR gate
00611                                         // fComp2 gives the polarity of the common component feeding into the DSD_NODE_OR gate
00612                                         //
00613                                         //                  |  fComp1              pL/  |pS
00614                                         //                  <> .........<=>....... <>   |
00615                                         //                  |                     /     |
00616                                         //                [OR]                  [OR]    | fComp3
00617                                         //                /  \  fComp2          / | \   |
00618                                         //              <>    <> .......<=>... /..|..<> | 
00619                                         //             /        \             /   |    \|
00620                                         //          [OR]        [C]          S1   S2    C 
00621                                         //          /  \
00622                                         //        <>    \
00623                                         //       /       \
00624                                         //     [OR]      [x]
00625                                         //     /  \
00626                                         //    S1   S2
00627                                         //
00628 
00629 
00630                                         // at this point we have the function F (bFTemp) and the common component C (bFuncComp)
00631                                     // to get the remainder, R, in the relationship F = R + C, supp(R) & supp(C) = 0
00632                                     // we compute the following R = Exist( F - C, supp(C) )
00633                                         bFTemp = (fComp1)? Cudd_Not( bF ): bF;
00634                                         bFuncComp = (fComp2)? Cudd_Not( pCompR->G ): pCompR->G;
00635                                         bFuncNew  = Cudd_bddAndAbstract( dd, bFTemp, Cudd_Not(bFuncComp), pCompR->S ); Cudd_Ref( bFuncNew );
00636 
00637                                         // there is no need to copy the dec entry list first, because pComp is a component
00638                                         // which will not be destroyed by the recursive call to decomposition
00639                                         pDENew = dsdKernelDecompose_rec( pDsdMan, bFuncNew );
00640                                         assert( Dsd_IsComplement(pDENew) ); // follows from the consideration of cases
00641                                         Cudd_RecursiveDeref( dd, bFuncNew );
00642 
00643                                         // get the new gate
00644                                         if ( nComp == 1 )
00645                                         {
00646                                                 pThis = Dsd_TreeNodeCreate( DSD_NODE_OR, 2, s_nDecBlocks++ );
00647                                                 pThis->pDecs[0] = pDENew;
00648                                                 pThis->pDecs[1] = pComp; // takes the complement
00649                                         }
00650                                         else
00651                                         {  // pComp is not complemented
00652                                                 pThis = Dsd_TreeNodeCreate( DSD_NODE_OR, nComp+1, s_nDecBlocks++ );
00653                                                 dsdKernelCopyListPlusOne( pThis, pDENew, pComp->pDecs, nComp );
00654                                         }
00655                                         
00656                                         if ( fComp1 )
00657                                                 pThis = Dsd_Not( pThis );
00658                                         goto EXIT;
00659                                 }
00660                         }
00661                         else if ( pLargeR->Type == DSD_NODE_EXOR ) // Figure 5 of Matsunaga's paper (with correction)
00662                         { // decomposition always exists = consider 4 cases
00663 
00664                                 // consideration of cases leads to the following conclusion
00665                                 // fComp3 gives the COMPLEMENT of the polarity of the resulting EXOR gate
00666                                 // (if fComp3 is 0, the EXOR gate is complemented, and vice versa)
00667                                 //
00668                                 //                  |  fComp1              pL/  |pS
00669                                 //                  <> .........<=>....... /....|  fComp3
00670                                 //                  |                     /     |
00671                                 //                [XOR]                [XOR]    |
00672                                 //                /  \  fComp2==0       / | \   |
00673                                 //              /     \                /  |  \  | 
00674                                 //             /        \             /   |    \|
00675                                 //          [OR]        [C]          S1   S2    C 
00676                                 //          /  \
00677                                 //        <>    \
00678                                 //       /       \
00679                                 //    [XOR]      [x]
00680                                 //     /  \
00681                                 //    S1   S2
00682                                 //
00683 
00684                                 assert( fComp2 == 0 );
00685                                 // find the functionality of the lower gates
00686                                 bFTemp = (fComp3)? bF: Cudd_Not( bF );
00687                                 bFuncNew = Cudd_bddXor( dd, bFTemp, pComp->G );   Cudd_Ref( bFuncNew );
00688 
00689                                 pDENew = dsdKernelDecompose_rec( pDsdMan, bFuncNew );
00690                                 assert( !Dsd_IsComplement(pDENew) ); // follows from the consideration of cases
00691                                 Cudd_RecursiveDeref( dd, bFuncNew ); 
00692 
00693                                 // get the new gate
00694                                 if ( nComp == 1 )
00695                                 {
00696                                         pThis = Dsd_TreeNodeCreate( DSD_NODE_EXOR, 2, s_nDecBlocks++ );
00697                                         pThis->pDecs[0] = pDENew;
00698                                         pThis->pDecs[1] = pComp; 
00699                                 }
00700                                 else
00701                                 {  // pComp is not complemented
00702                                         pThis = Dsd_TreeNodeCreate( DSD_NODE_EXOR, nComp+1, s_nDecBlocks++ );
00703                                         dsdKernelCopyListPlusOne( pThis, pDENew, pComp->pDecs, nComp );
00704                                 }
00705 
00706                                 if ( !fComp3 )
00707                                         pThis = Dsd_Not( pThis );
00708                                 goto EXIT;
00709                         }
00710                 }
00711         }
00712 
00713         // this case was added to fix the trivial bug found November 4, 2002 in Japan
00714         // by running the example provided by T. Sasao
00715         if ( nSuppLH == nSuppL + nSuppH ) // the supports of the components are disjoint
00716         {
00717                 // create a new component of the type ITE( a, pH, pL )
00718                 pThis = Dsd_TreeNodeCreate( DSD_NODE_PRIME, 3, s_nDecBlocks++ );
00719                 if ( dd->perm[pLR->S->index] < dd->perm[pHR->S->index] ) // pLR is higher in the varible order
00720                 {
00721                         pThis->pDecs[1] = pLR;
00722                         pThis->pDecs[2] = pHR;
00723                 }
00724                 else  // pHR is higher in the varible order
00725                 {
00726                         pThis->pDecs[1] = pHR;
00727                         pThis->pDecs[2] = pLR;
00728                 }
00729                 // add the first component
00730                 pThis->pDecs[0] = pVarCurDE;
00731                 goto EXIT;
00732         }
00733 
00734 
00736         // CASE 3.a Neither of the cofactors is a constant (OR, EXOR, PRIME)
00738         // the component types are identical 
00739         // and if they are OR, they are either both complemented or both not complemented
00740         // and if they are PRIME, their dec numbers should be the same
00741         if ( pLR->Type == pHR->Type && 
00742                  pLR->Type != DSD_NODE_BUF &&           
00743                 (pLR->Type != DSD_NODE_OR    || ( pL == pLR && pH == pHR || pL != pLR && pH != pHR ) ) &&
00744                 (pLR->Type != DSD_NODE_PRIME || pLR->nDecs == pHR->nDecs)  )
00745         {
00746                 // array to store common comps in pL and pH
00747                 Dsd_Node_t ** pCommon, * pLastDiffL = NULL, * pLastDiffH = NULL; 
00748                 int nCommon = dsdKernelFindCommonComponents( pDsdMan, pLR, pHR, &pCommon, &pLastDiffL, &pLastDiffH );
00749                 if ( nCommon )
00750                 {
00751                         if ( pLR->Type == DSD_NODE_OR ) // Figure 2 of Matsunaga's paper
00752                         { // at this point we have the function F and the group of common components C
00753                                 // to get the remainder, R, in the relationship F = R + C, supp(R) & supp(C) = 0
00754                                 // we compute the following R = Exist( F - C, supp(C) )
00755 
00756                                 // compute the sum total of the common components and the union of their supports
00757                                 DdNode * bCommF, * bCommS, * bFTemp, * bFuncNew;
00758                                 Dsd_Node_t * pDENew;
00759 
00760                                 dsdKernelComputeSumOfComponents( pDsdMan, pCommon, nCommon, &bCommF, &bCommS, 0 );
00761                                 Cudd_Ref( bCommF );
00762                                 Cudd_Ref( bCommS );
00763                                 bFTemp = ( pL != pLR )? Cudd_Not(bF): bF;
00764 
00765                                 bFuncNew = Cudd_bddAndAbstract( dd, bFTemp, Cudd_Not(bCommF), bCommS ); Cudd_Ref( bFuncNew );
00766                                 Cudd_RecursiveDeref( dd, bCommF );
00767                                 Cudd_RecursiveDeref( dd, bCommS );
00768 
00769                                 // get the new gate
00770 
00771                                 // copy the components first, then call the decomposition
00772                                 // because decomposition will distroy the list used for copying
00773                                 pThis = Dsd_TreeNodeCreate( DSD_NODE_OR, nCommon + 1, s_nDecBlocks++ );
00774                                 dsdKernelCopyListPlusOne( pThis, NULL, pCommon, nCommon );
00775 
00776                                 // call the decomposition recursively
00777                                 pDENew = dsdKernelDecompose_rec( pDsdMan, bFuncNew );
00778 //                              assert( !Dsd_IsComplement(pDENew) ); // follows from the consideration of cases
00779                                 Cudd_RecursiveDeref( dd, bFuncNew );
00780 
00781                                 // add the first component
00782                                 pThis->pDecs[0] = pDENew;
00783                                 
00784                                 if ( pL != pLR )
00785                                         pThis = Dsd_Not( pThis );
00786                                 goto EXIT;
00787                         }
00788                         else
00789                         if ( pLR->Type == DSD_NODE_EXOR ) // Figure 3 of Matsunaga's paper
00790                         {
00791                                 // compute the sum total of the common components and the union of their supports
00792                                 DdNode * bCommF, * bFuncNew;
00793                                 Dsd_Node_t * pDENew;
00794                                 int fCompExor;
00795 
00796                                 dsdKernelComputeSumOfComponents( pDsdMan, pCommon, nCommon, &bCommF, NULL, 1 );
00797                                 Cudd_Ref( bCommF );
00798 
00799                                 bFuncNew = Cudd_bddXor( dd, bF, bCommF ); Cudd_Ref( bFuncNew );
00800                                 Cudd_RecursiveDeref( dd, bCommF );
00801 
00802                                 // get the new gate
00803 
00804                                 // copy the components first, then call the decomposition
00805                                 // because decomposition will distroy the list used for copying
00806                                 pThis = Dsd_TreeNodeCreate( DSD_NODE_EXOR, nCommon + 1, s_nDecBlocks++ );
00807                                 dsdKernelCopyListPlusOne( pThis, NULL, pCommon, nCommon );
00808 
00809                                 // call the decomposition recursively
00810                                 pDENew = dsdKernelDecompose_rec( pDsdMan, bFuncNew );
00811                                 Cudd_RecursiveDeref( dd, bFuncNew );
00812 
00813                                 // remember the fact that it was complemented
00814                                 fCompExor = Dsd_IsComplement(pDENew);
00815                                 pDENew = Dsd_Regular(pDENew);
00816 
00817                                 // add the first component
00818                                 pThis->pDecs[0] = pDENew;
00819 
00820         
00821                                 if ( fCompExor )
00822                                         pThis = Dsd_Not( pThis );
00823                                 goto EXIT;
00824                         }
00825                         else 
00826                         if ( pLR->Type == DSD_NODE_PRIME && (nCommon == pLR->nDecs-1 || nCommon == pLR->nDecs) )
00827                         {
00828                                 // for example the function F(a,b,c,d) = ITE(b,c,a(+)d) produces
00829                                 // two cofactors F(a=0) = PRIME(b,c,d) and F(a=1) = PRIME(b,c,d)
00830                                 // with exactly the same list of common components
00831 
00832                                 Dsd_Node_t * pDENew;
00833                                 DdNode * bFuncNew;
00834                                 int fCompComp = 0;      // this flag can be {0,1,2}
00835                                 // if it is 0 there is no identity
00836                                 // if it is 1/2, the cofactored functions are equal in the direct/complemented polarity
00837 
00838                                 if ( nCommon == pLR->nDecs )
00839                                 {       // all the components are the same
00840                                         // find the formal input, in which pLow and pHigh differ (if such input exists)
00841                                         int m;
00842                                         Dsd_Node_t * pTempL, * pTempH;
00843 
00844                                         s_Common++;
00845                                         for ( m = 0; m < pLR->nDecs; m++ )
00846                                         {
00847                                                 pTempL = pLR->pDecs[m]; // cannot be complemented
00848                                                 pTempH = pHR->pDecs[m]; // cannot be complemented
00849 
00850                                                 if ( Dsd_CheckRootFunctionIdentity( dd, bLow, bHigh,          pTempL->G, Cudd_Not(pTempH->G) ) &&
00851                                                          Dsd_CheckRootFunctionIdentity( dd, bLow, bHigh, Cudd_Not(pTempL->G),         pTempH->G ) )
00852                                                 {
00853                                                          pLastDiffL = pTempL;
00854                                                          pLastDiffH = pTempH;
00855                                                          assert( pLastDiffL == pLastDiffH );
00856                                                          fCompComp = 2;
00857                                                          break;
00858                                                 }
00859 
00860                                                 s_Loops2++;
00861                                                 s_Loops2++;
00862 /* 
00863                         if ( s_Loops2 % 10000  == 0 )
00864                         {
00865                             int i;
00866                             for ( i = 0; i < pLR->nDecs; i++ )
00867                                 printf( " %d(s=%d)", pLR->pDecs[i]->Type,
00868                                     Extra_bddSuppSize(dd, pLR->pDecs[i]->S) );
00869                             printf( "\n" );
00870                         }
00871 */
00872 
00873                                         }
00874 //                    if ( pLR->nDecs == Extra_bddSuppSize(dd, pLR->S) )
00875 //                        s_Loops2Useless += pLR->nDecs * 2;
00876 
00877                                         if ( fCompComp )
00878                                         { // put the equal components into pCommon, so that they could be copied into the new dec entry
00879                                                 nCommon = 0;
00880                                                 for ( m = 0; m < pLR->nDecs; m++ )
00881                                                         if ( pLR->pDecs[m] != pLastDiffL )
00882                                                                  pCommon[nCommon++] = pLR->pDecs[m];
00883                                                 assert( nCommon = pLR->nDecs-1 );
00884                                         }
00885                                 }
00886                                 else
00887                                 {  // the differing components are known - check that they have compatible PRIME function
00888 
00889                                         s_CommonNo++;
00890 
00891                                         // find the numbers of different components
00892                                         assert( pLastDiffL );
00893                                         assert( pLastDiffH );
00894                                         // also, they cannot be complemented, because the decomposition type is PRIME
00895 
00896                                         if ( Dsd_CheckRootFunctionIdentity( dd, bLow, bHigh, Cudd_Not(pLastDiffL->G), Cudd_Not(pLastDiffH->G) ) &&
00897                                                  Dsd_CheckRootFunctionIdentity( dd, bLow, bHigh,          pLastDiffL->G,           pLastDiffH->G ) )
00898                                                 fCompComp = 1;
00899                                         else if ( Dsd_CheckRootFunctionIdentity( dd, bLow, bHigh,          pLastDiffL->G, Cudd_Not(pLastDiffH->G) ) &&
00900                                                           Dsd_CheckRootFunctionIdentity( dd, bLow, bHigh, Cudd_Not(pLastDiffL->G),         pLastDiffH->G ) )
00901                                                 fCompComp = 2;
00902 
00903                                         s_Loops3 += 4;
00904                                 }
00905 
00906                                 if ( fCompComp )
00907                                 {
00908                                         if ( fCompComp == 1 ) // it is true that bLow(G=0) == bHigh(H=0) && bLow(G=1) == bHigh(H=1)
00909                                                 bFuncNew = Cudd_bddIte( dd, bVarCur, pLastDiffH->G, pLastDiffL->G ); 
00910                                         else // it is true that bLow(G=0) == bHigh(H=1) && bLow(G=1) == bHigh(H=0)
00911                                                 bFuncNew = Cudd_bddIte( dd, bVarCur, Cudd_Not(pLastDiffH->G), pLastDiffL->G ); 
00912                                         Cudd_Ref( bFuncNew );
00913 
00914                                         // get the new gate
00915 
00916                                         // copy the components first, then call the decomposition
00917                                         // because decomposition will distroy the list used for copying
00918                                         pThis = Dsd_TreeNodeCreate( DSD_NODE_PRIME, pLR->nDecs, s_nDecBlocks++ );
00919                                         dsdKernelCopyListPlusOne( pThis, NULL, pCommon, nCommon );
00920 
00921                                         // create a new component
00922                                         pDENew = dsdKernelDecompose_rec( pDsdMan, bFuncNew );
00923                                         Cudd_RecursiveDeref( dd, bFuncNew );
00924                                         // the BDD of the argument function in PRIME decomposition, should be regular
00925                                         pDENew = Dsd_Regular(pDENew);
00926 
00927                                         // add the first component
00928                                         pThis->pDecs[0] = pDENew;
00929                                         goto EXIT;
00930                                 }
00931                         } // end of PRIME type
00932                 } // end of existing common components
00933         } // end of CASE 3.a
00934 
00935 // if ( Depth != 1) 
00936 // {
00937 
00938 //CASE4:
00940         // CASE 4
00942         {
00943         // estimate the number of entries in the list
00944         int nEntriesMax = pDsdMan->nInputs - dd->perm[VarInt];
00945 
00946         // create the new decomposition entry
00947         int nEntries = 0;
00948 
00949         DdNode * SuppL, * SuppH, * SuppL_init, * SuppH_init;
00950         Dsd_Node_t *pHigher, *pLower, * pTemp, * pDENew;
00951 
00952 
00953         int levTopSuppL;
00954         int levTopSuppH;
00955         int levTop;
00956 
00957         pThis = Dsd_TreeNodeCreate( DSD_NODE_PRIME, nEntriesMax, s_nDecBlocks++ );
00958         pThis->pDecs[ nEntries++ ] = pVarCurDE;
00959         // other entries will be added to this list one-by-one during analysis
00960 
00961         // count how many times does it happen that the decomposition entries are
00962     s_Case4Calls++;
00963  
00964         // consider the simplest case: when the supports are equal 
00965     // and at least one of the components
00966         // is the PRIME without decompositions, or 
00967     // when both of them are without decomposition
00968         if ( (((pLR->Type == DSD_NODE_PRIME && nSuppL == pLR->nDecs) || (pHR->Type == DSD_NODE_PRIME && nSuppH == pHR->nDecs)) && pLR->S == pHR->S)  ||
00969                   ((pLR->Type == DSD_NODE_PRIME && nSuppL == pLR->nDecs) && (pHR->Type == DSD_NODE_PRIME && nSuppH == pHR->nDecs)) )
00970         {
00971 
00972                  s_Case4CallsSpecial++;
00973                  // walk through both supports and create the decomposition list composed of simple entries
00974                  SuppL = pLR->S;
00975                  SuppH = pHR->S;
00976                  do
00977                  {
00978                          // determine levels
00979                          levTopSuppL = cuddI(dd,SuppL->index);
00980                          levTopSuppH = cuddI(dd,SuppH->index);
00981 
00982                          // skip the topmost variable in both supports
00983                          if ( levTopSuppL <= levTopSuppH )
00984                          {
00985                                  levTop = levTopSuppL;
00986                                  SuppL  = cuddT(SuppL);
00987                          }
00988                          else
00989                                  levTop = levTopSuppH;
00990 
00991                          if ( levTopSuppH <= levTopSuppL )
00992                                  SuppH = cuddT(SuppH);
00993 
00994                          // set the new decomposition entry
00995                          pThis->pDecs[ nEntries++ ] = pDsdMan->pInputs[ dd->invperm[levTop] ];
00996                  }
00997                  while ( SuppL != b1 || SuppH != b1 );
00998         }
00999         else
01000         {
01001 
01002                 // compare two different decomposition lists
01003                 SuppL_init = pLR->S;
01004                 SuppH_init = pHR->S;
01005                 // start references (because these supports will change)
01006                 SuppL = pLR->S;  Cudd_Ref( SuppL );
01007                 SuppH = pHR->S;  Cudd_Ref( SuppH );
01008                 while ( SuppL != b1 || SuppH != b1 )
01009                 {
01010                         // determine the top level in cofactors and
01011                         // whether they have the same top level
01012                         int TopLevL  = cuddI(dd,SuppL->index);
01013                         int TopLevH  = cuddI(dd,SuppH->index);
01014                         int TopLevel = TopLevH;
01015                         int fEqualLevel = 0;
01016 
01017                         DdNode * bVarTop;
01018                         DdNode * bSuppSubract;
01019 
01020 
01021                         if ( TopLevL < TopLevH )
01022                         {
01023                                 pHigher = pLR;
01024                                 pLower  = pHR;
01025                                 TopLevel = TopLevL;
01026                         }
01027                         else if ( TopLevL > TopLevH )
01028                         {
01029                                 pHigher = pHR;
01030                                 pLower  = pLR;
01031                         }
01032                         else
01033                                 fEqualLevel = 1;
01034                         assert( TopLevel != CUDD_CONST_INDEX );
01035 
01036 
01037                         // find the currently top variable in the decomposition lists
01038                         bVarTop = dd->vars[dd->invperm[TopLevel]];
01039 
01040                         if ( !fEqualLevel )
01041                         {
01042                                 // find the lower support
01043                                 DdNode * bSuppLower = (TopLevL < TopLevH)? SuppH_init: SuppL_init; 
01044 
01045                                 // find the first component in pHigher 
01046                                 // whose support does not overlap with supp(Lower) 
01047                                 // and remember the previous component
01048                                 int fPolarity;                  
01049                                 Dsd_Node_t * pPrev = NULL;       // the pointer to the component proceeding pCur
01050                                 Dsd_Node_t * pCur  = pHigher;    // the first component not contained in supp(Lower)
01051                                 while ( Extra_bddSuppOverlapping( dd, pCur->S, bSuppLower ) )
01052                                 {       // get the next component
01053                                         pPrev = pCur;
01054                                         pCur  = dsdKernelFindContainingComponent( pDsdMan, pCur, bVarTop, &fPolarity );
01055                                 };
01056 
01057                                 // look for the possibility to subtract more than one component
01058                                 if ( pPrev == NULL || pPrev->Type == DSD_NODE_PRIME )
01059                                 { // if there is no previous component, or if the previous component is PRIME
01060                                   // there is no way to subtract more than one component
01061 
01062                                         // add the new decomposition entry (it is already regular)
01063                                         pThis->pDecs[ nEntries++ ] = pCur;
01064                                         // assign the support to be subtracted from both components
01065                                         bSuppSubract = pCur->S;
01066                                 }
01067                                 else // all other types
01068                                 {
01069                                         // go through the decomposition list of pPrev and find components 
01070                                         // whose support does not overlap with supp(Lower) 
01071 
01072                                         static Dsd_Node_t * pNonOverlap[MAXINPUTS];
01073                                         int i, nNonOverlap = 0;
01074                                         for ( i = 0; i < pPrev->nDecs; i++ )
01075                                         {
01076                                                 pTemp = Dsd_Regular( pPrev->pDecs[i] );
01077                                                 if ( !Extra_bddSuppOverlapping( dd, pTemp->S, bSuppLower ) )
01078                                                         pNonOverlap[ nNonOverlap++ ] = pPrev->pDecs[i];
01079                                         }
01080                                         assert( nNonOverlap > 0 );
01081 
01082                                         if ( nNonOverlap == 1 )
01083                                         { // one one component was found, which is the original one
01084                                                 assert( Dsd_Regular(pNonOverlap[0]) == pCur);
01085                                                 // add the new decomposition entry
01086                                                 pThis->pDecs[ nEntries++ ] = pCur;
01087                                                 // assign the support to be subtracted from both components
01088                                                 bSuppSubract = pCur->S;
01089                                         }
01090                                         else // more than one components was found
01091                                         {
01092                                                 // find the OR (EXOR) of the non-overlapping components
01093                                                 DdNode * bCommF;
01094                                                 dsdKernelComputeSumOfComponents( pDsdMan, pNonOverlap, nNonOverlap, &bCommF, NULL, (int)(pPrev->Type==DSD_NODE_EXOR) );
01095                                                 Cudd_Ref( bCommF );
01096 
01097                                                 // create a new gated 
01098                                                 pDENew = dsdKernelDecompose_rec( pDsdMan, bCommF );
01099                                                 Cudd_RecursiveDeref(dd, bCommF);
01100                                                 // make it regular... it must be regular already
01101                                                 assert( !Dsd_IsComplement(pDENew) );
01102 
01103                                                 // add the new decomposition entry
01104                                                 pThis->pDecs[ nEntries++ ] = pDENew;
01105                                                 // assign the support to be subtracted from both components
01106                                                 bSuppSubract = pDENew->S;
01107                                         }
01108                                 }
01109                                 
01110                                 // subtract its support from the support of upper component
01111                                 if ( TopLevL < TopLevH )
01112                                 {
01113                                         SuppL = Cudd_bddExistAbstract( dd, bTemp = SuppL, bSuppSubract ); Cudd_Ref( SuppL );
01114                                         Cudd_RecursiveDeref(dd, bTemp);
01115                                 }
01116                                 else
01117                                 {
01118                                         SuppH = Cudd_bddExistAbstract( dd, bTemp = SuppH, bSuppSubract ); Cudd_Ref( SuppH );
01119                                         Cudd_RecursiveDeref(dd, bTemp);
01120                                 }
01121                         } // end of if ( !fEqualLevel )
01122                         else // if ( fEqualLevel ) -- they have the same top level var
01123                         {
01124                                 static Dsd_Node_t * pMarkedLeft[MAXINPUTS]; // the pointers to the marked blocks
01125                                 static char pMarkedPols[MAXINPUTS]; // polarities of the marked blocks
01126                                 int nMarkedLeft = 0;
01127 
01128                                 int fPolarity = 0;
01129                                 Dsd_Node_t * pTempL = pLR;
01130 
01131                                 int fPolarityCurH = 0;
01132                                 Dsd_Node_t * pPrevH = NULL, * pCurH = pHR;
01133 
01134                                 int fPolarityCurL = 0;
01135                                 Dsd_Node_t * pPrevL = NULL, * pCurL = pLR; // = pMarkedLeft[0];
01136                                 int index = 1;
01137 
01138                                 // set the new mark
01139                                 s_Mark++;
01140 
01141                                 // go over the dec list of pL, mark all components that contain the given variable
01142                                 assert( Extra_bddSuppContainVar( dd, pLR->S, bVarTop ) );
01143                                 assert( Extra_bddSuppContainVar( dd, pHR->S, bVarTop ) );
01144                                 do {
01145                                         pTempL->Mark = s_Mark;
01146                                         pMarkedLeft[ nMarkedLeft ] = pTempL;
01147                                         pMarkedPols[ nMarkedLeft ] = fPolarity;
01148                                         nMarkedLeft++;
01149                                 } while ( pTempL = dsdKernelFindContainingComponent( pDsdMan, pTempL, bVarTop, &fPolarity ) );
01150 
01151                                 // go over the dec list of pH, and find the component that is marked and the previos one
01152                                 // (such component always exists, because they have common variables)
01153                                 while ( pCurH->Mark != s_Mark )
01154                                 {
01155                                         pPrevH = pCurH;
01156                                         pCurH  = dsdKernelFindContainingComponent( pDsdMan, pCurH, bVarTop, &fPolarityCurH );
01157                                         assert( pCurH );
01158                                 }
01159 
01160                                 // go through the first list once again and find 
01161                                 // the component proceeding the one marked found in the second list
01162                                 while ( pCurL != pCurH )
01163                                 {
01164                                         pPrevL = pCurL;
01165                                         pCurL  = pMarkedLeft[index];
01166                                         fPolarityCurL = pMarkedPols[index];
01167                                         index++;
01168                                 }
01169 
01170                                 // look for the possibility to subtract more than one component
01171                                 if ( !pPrevL || !pPrevH || pPrevL->Type != pPrevH->Type || pPrevL->Type == DSD_NODE_PRIME || fPolarityCurL != fPolarityCurH )
01172                                 { // there is no way to extract more than one
01173                                         pThis->pDecs[ nEntries++ ] = pCurH;
01174                                         // assign the support to be subtracted from both components
01175                                         bSuppSubract = pCurH->S;
01176                                 }
01177                                 else 
01178                                 {
01179                                         // find the equal components in two decomposition lists
01180                                         Dsd_Node_t ** pCommon, * pLastDiffL = NULL, * pLastDiffH = NULL; 
01181                                         int nCommon = dsdKernelFindCommonComponents( pDsdMan, pPrevL, pPrevH, &pCommon, &pLastDiffL, &pLastDiffH );
01182                 
01183                                         if ( nCommon == 0 || nCommon == 1 )
01184                                         { // one one component was found, which is the original one
01185         //                                      assert( Dsd_Regular(pCommon[0]) == pCurL);
01186                                                 // add the new decomposition entry
01187                                                 pThis->pDecs[ nEntries++ ] = pCurL;
01188                                                 // assign the support to be subtracted from both components
01189                                                 bSuppSubract = pCurL->S;
01190                                         }
01191                                         else // more than one components was found
01192                                         {
01193                                                 // find the OR (EXOR) of the non-overlapping components
01194                                                 DdNode * bCommF;
01195                                                 dsdKernelComputeSumOfComponents( pDsdMan, pCommon, nCommon, &bCommF, NULL, (int)(pPrevL->Type==DSD_NODE_EXOR) );
01196                                                 Cudd_Ref( bCommF );
01197 
01198                                                 pDENew = dsdKernelDecompose_rec( pDsdMan, bCommF );
01199                                                 assert( !Dsd_IsComplement(pDENew) ); // cannot be complemented because of construction
01200                                                 Cudd_RecursiveDeref( dd, bCommF );
01201 
01202                                                 // add the new decomposition entry
01203                                                 pThis->pDecs[ nEntries++ ] = pDENew;
01204 
01205                                                 // assign the support to be subtracted from both components
01206                                                 bSuppSubract = pDENew->S;
01207                                         }
01208                                 }
01209 
01210                                 SuppL = Cudd_bddExistAbstract( dd, bTemp = SuppL, bSuppSubract ), Cudd_Ref( SuppL );
01211                                 Cudd_RecursiveDeref(dd, bTemp);
01212 
01213                                 SuppH = Cudd_bddExistAbstract( dd, bTemp = SuppH, bSuppSubract ), Cudd_Ref( SuppH );
01214                                 Cudd_RecursiveDeref(dd, bTemp);
01215 
01216                         } // end of if ( fEqualLevel ) 
01217 
01218                 } // end of decomposition list comparison
01219                 Cudd_RecursiveDeref( dd, SuppL );
01220                 Cudd_RecursiveDeref( dd, SuppH );
01221 
01222         }
01223 
01224         // check that the estimation of the number of entries was okay
01225         assert( nEntries <= nEntriesMax );
01226 
01227 //    if ( nEntries != Extra_bddSuppSize(dd, bSuppNew) )
01228 //        s_Case5++;
01229 
01230         // update the number of entries in the new decomposition list
01231         pThis->nDecs = nEntries;
01232         }
01233 //}
01234 EXIT:
01235 
01236         {
01237         // if the component created is complemented, it represents a function without complement
01238         // therefore, as it is, without complement, it should recieve the complemented function
01239         Dsd_Node_t * pThisR = Dsd_Regular( pThis );
01240         assert( pThisR->G == NULL );
01241         assert( pThisR->S == NULL );
01242 
01243         if ( pThisR == pThis ) // set regular function
01244                 pThisR->G = bF; 
01245         else // set complemented function
01246                 pThisR->G = Cudd_Not(bF);    
01247         Cudd_Ref(bF);           // reference the function in the component
01248 
01249         assert( bSuppNew );
01250         pThisR->S = bSuppNew;   // takes the reference from the new support
01251         if ( st_insert( pDsdMan->Table, (char*)bF, (char*)pThis ) )
01252         {
01253                 assert( 0 );
01254         }
01255         s_CacheEntries++;
01256 
01257 
01258 /*
01259         if ( dsdKernelVerifyDecomposition(dd, pThis) == 0 )
01260         {
01261                 // write the function, for which verification does not work
01262                 cout << endl << "Internal verification failed!"" );
01263 
01264                 // create the variable mask
01265                 static int s_pVarMask[MAXINPUTS];
01266                 int nInputCounter = 0;
01267 
01268                 Cudd_SupportArray( dd, bF, s_pVarMask );
01269                 int k; 
01270                 for ( k = 0; k < dd->size; k++ )
01271                         if ( s_pVarMask[k] )
01272                                 nInputCounter++;
01273 
01274                 cout << endl << "The problem function is "" );
01275 
01276                 DdNode * zNewFunc = Cudd_zddIsopCover( dd, bF, bF ); Cudd_Ref( zNewFunc );
01277                 cuddWriteFunctionSop( stdout, dd, zNewFunc, -1, dd->size, "1", s_pVarMask );
01278                 Cudd_RecursiveDerefZdd( dd, zNewFunc );
01279         }
01280 */
01281 
01282         }
01283 
01284         Depth--;
01285     return Dsd_NotCond( pThis, fCompF );
01286 }
01287 
01288 
01292 
01306 Dsd_Node_t * dsdKernelFindContainingComponent( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pWhere, DdNode * Var, int * fPolarity )
01307 
01308 {
01309         Dsd_Node_t * pTemp;
01310         int i;
01311 
01312 //      assert( !Dsd_IsComplement( pWhere ) );
01313 //      assert( Extra_bddSuppContainVar( pDsdMan->dd, pWhere->S, Var ) );
01314 
01315         if ( pWhere->nDecs == 1 )
01316                 return NULL;
01317 
01318         for( i = 0; i < pWhere->nDecs; i++ )
01319         {
01320                 pTemp = Dsd_Regular( pWhere->pDecs[i] );
01321                 if ( Extra_bddSuppContainVar( pDsdMan->dd, pTemp->S, Var ) )
01322                 {
01323                         *fPolarity = (int)( pTemp != pWhere->pDecs[i] );
01324                         return pTemp;
01325                 }
01326         }
01327         assert( 0 );
01328         return NULL;
01329 }
01330 
01346 int dsdKernelFindCommonComponents( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pL, Dsd_Node_t * pH, Dsd_Node_t *** pCommon, Dsd_Node_t ** pLastDiffL, Dsd_Node_t ** pLastDiffH )
01347 {
01348         static Dsd_Node_t * Common[MAXINPUTS];
01349         int nCommon = 0;
01350 
01351         // pointers to the current decomposition entries
01352         Dsd_Node_t * pLcur;
01353         Dsd_Node_t * pHcur;
01354 
01355         // the pointers to their supports
01356         DdNode * bSLcur;
01357         DdNode * bSHcur;
01358 
01359         // the top variable in the supports
01360         int TopVar;
01361 
01362         // the indices running through the components
01363         int iCurL = 0;
01364         int iCurH = 0;
01365         while ( iCurL < pL->nDecs && iCurH < pH->nDecs )
01366         { // both did not run out
01367 
01368                 pLcur = Dsd_Regular(pL->pDecs[iCurL]);
01369                 pHcur = Dsd_Regular(pH->pDecs[iCurH]);
01370 
01371                 bSLcur = pLcur->S;
01372                 bSHcur = pHcur->S;
01373 
01374                 // find out what component is higher in the BDD
01375                 if ( pDsdMan->dd->perm[bSLcur->index] < pDsdMan->dd->perm[bSHcur->index] )
01376                         TopVar = bSLcur->index;
01377                 else
01378                         TopVar = bSHcur->index;
01379 
01380                 if ( TopVar == bSLcur->index && TopVar == bSHcur->index ) 
01381                 {
01382                         // the components may be equal - should match exactly!
01383                         if ( pL->pDecs[iCurL] == pH->pDecs[iCurH] )
01384                                 Common[nCommon++] = pL->pDecs[iCurL];
01385                         else
01386                         {
01387                                 *pLastDiffL = pL->pDecs[iCurL];
01388                                 *pLastDiffH = pH->pDecs[iCurH];
01389                         }
01390 
01391                         // skip both
01392                         iCurL++;
01393                         iCurH++;
01394                 }
01395                 else if ( TopVar == bSLcur->index )
01396                 {  // the components cannot be equal
01397                         // skip the top-most one
01398                         *pLastDiffL = pL->pDecs[iCurL++];
01399                 }
01400                 else // if ( TopVar == bSHcur->index )
01401                 {  // the components cannot be equal
01402                         // skip the top-most one
01403                         *pLastDiffH = pH->pDecs[iCurH++];
01404                 }
01405         }
01406 
01407         // if one of the lists still has components, write the first one down
01408         if ( iCurL < pL->nDecs )
01409                 *pLastDiffL = pL->pDecs[iCurL];
01410 
01411         if ( iCurH < pH->nDecs )
01412                 *pLastDiffH = pH->pDecs[iCurH];
01413 
01414         // return the pointer to the array
01415         *pCommon = Common;
01416         // return the number of common components
01417         return nCommon;                 
01418 }
01419 
01431 void dsdKernelComputeSumOfComponents( Dsd_Manager_t * pDsdMan, Dsd_Node_t ** pCommon, int nCommon, DdNode ** pCompF, DdNode ** pCompS, int fExor )
01432 {
01433         DdManager * dd = pDsdMan->dd;
01434         DdNode * bF, * bS, * bFadd, * bTemp;
01435         Dsd_Node_t * pDE, * pDER;
01436         int i;
01437 
01438         // start the function
01439         bF = b0; Cudd_Ref( bF );
01440         // start the support
01441         if ( pCompS )
01442                 bS = b1, Cudd_Ref( bS );
01443 
01444         assert( nCommon > 0 );
01445         for ( i = 0; i < nCommon; i++ )
01446         {
01447                 pDE  = pCommon[i];
01448                 pDER = Dsd_Regular( pDE );
01449                 bFadd = (pDE != pDER)? Cudd_Not(pDER->G): pDER->G;
01450                 // add to the function
01451                 if ( fExor )
01452                         bF = Cudd_bddXor( dd, bTemp = bF, bFadd );
01453                 else
01454                         bF = Cudd_bddOr( dd, bTemp = bF, bFadd );
01455                 Cudd_Ref( bF );
01456                 Cudd_RecursiveDeref( dd, bTemp );
01457                 if ( pCompS )
01458                 {
01459                         // add to the support
01460                         bS = Cudd_bddAnd( dd, bTemp = bS, pDER->S );  Cudd_Ref( bS );
01461                         Cudd_RecursiveDeref( dd, bTemp );
01462                 }
01463         }
01464         // return the function
01465         Cudd_Deref( bF );
01466         *pCompF = bF;
01467 
01468         // return the support
01469         if ( pCompS )
01470                 Cudd_Deref( bS ), *pCompS = bS;
01471 }
01472 
01488 int dsdKernelCheckContainment( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pL, Dsd_Node_t * pH, Dsd_Node_t ** pLarge, Dsd_Node_t ** pSmall )
01489 {
01490         DdManager * dd = pDsdMan->dd;
01491         DdNode * bSuppLarge, * bSuppSmall;
01492         int RetValue;
01493         
01494         RetValue = Extra_bddSuppCheckContainment( dd, pL->S, pH->S, &bSuppLarge, &bSuppSmall );
01495 
01496         if ( RetValue == 0 ) 
01497                 return 0;
01498 
01499         if ( pH->S == bSuppLarge )
01500         {
01501                 *pLarge = pH;
01502                 *pSmall = pL;
01503         }
01504         else // if ( pL->S == bSuppLarge )
01505         {
01506                 *pLarge = pL;
01507                 *pSmall = pH;
01508         }
01509         return 1;
01510 }
01511 
01523 void dsdKernelCopyListPlusOne( Dsd_Node_t * p, Dsd_Node_t * First, Dsd_Node_t ** ppList, int nListSize )
01524 {
01525         int i;
01526         assert( nListSize+1 == p->nDecs );
01527         p->pDecs[0] = First;
01528         for( i = 0; i < nListSize; i++ )
01529                 p->pDecs[i+1] = ppList[i];
01530 }
01531 
01543 void dsdKernelCopyListPlusOneMinusOne( Dsd_Node_t * p, Dsd_Node_t * First, Dsd_Node_t ** ppList, int nListSize, int iSkipped )
01544 {
01545         int i, Counter;
01546         assert( nListSize == p->nDecs );
01547         p->pDecs[0] = First;
01548         for( i = 0, Counter = 1; i < nListSize; i++ )
01549                 if ( i != iSkipped )
01550                         p->pDecs[Counter++] = ppList[i];
01551 }
01552 
01564 int dsdKernelVerifyDecomposition( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pDE )
01565 {
01566         DdManager * dd = pDsdMan->dd;
01567         Dsd_Node_t * pR    = Dsd_Regular(pDE);
01568         int fCompP = (int)( pDE != pR );
01569         int RetValue;
01570 
01571         DdNode * bRes;
01572         if ( pR->Type == DSD_NODE_CONST1 )
01573                 bRes = b1;
01574         else if ( pR->Type == DSD_NODE_BUF )
01575                 bRes = pR->G;
01576         else if ( pR->Type == DSD_NODE_OR || pR->Type == DSD_NODE_EXOR )
01577                 dsdKernelComputeSumOfComponents( pDsdMan, pR->pDecs, pR->nDecs, &bRes, NULL, (int)(pR->Type == DSD_NODE_EXOR) );
01578         else if ( pR->Type == DSD_NODE_PRIME )
01579         {
01580                 int i;
01581                 static DdNode * bGVars[MAXINPUTS];
01582                 // transform the function of this block, so that it depended on inputs
01583                 // corresponding to the formal inputs
01584                 DdNode * bNewFunc = Dsd_TreeGetPrimeFunctionOld( dd, pR, 1 );  Cudd_Ref( bNewFunc );
01585 
01586                 // compose this function with the inputs
01587                 // create the elementary permutation
01588                 for ( i = 0; i < dd->size; i++ )
01589                         bGVars[i] = dd->vars[i];
01590 
01591                 // assign functions to be composed
01592                 for ( i = 0; i < pR->nDecs; i++ )
01593                         bGVars[dd->invperm[i]] = pR->pDecs[i]->G;
01594 
01595                 // perform the composition
01596                 bRes = Cudd_bddVectorCompose( dd, bNewFunc, bGVars );      Cudd_Ref( bRes );
01597                 Cudd_RecursiveDeref( dd, bNewFunc );
01598 
01600                 RetValue = (int)( bRes == pR->G );//|| bRes == Cudd_Not(pR->G) );
01602                 Cudd_Deref( bRes );
01603         }
01604         else
01605         {
01606                 assert(0);
01607         }
01608 
01609         Cudd_Ref( bRes );
01610         RetValue = (int)( bRes == pR->G );//|| bRes == Cudd_Not(pR->G) );
01611         Cudd_RecursiveDeref( dd, bRes );
01612         return RetValue;
01613 }
01614