abc70930: src/misc/extra/extraBddAuto.c Source File

00001 
00019 #include "extra.h"
00020 
00021 /*---------------------------------------------------------------------------*/
00022 /* Constant declarations                                                     */
00023 /*---------------------------------------------------------------------------*/
00024 
00025 /*---------------------------------------------------------------------------*/
00026 /* Stucture declarations                                                     */
00027 /*---------------------------------------------------------------------------*/
00028 
00029 /*---------------------------------------------------------------------------*/
00030 /* Type declarations                                                         */
00031 /*---------------------------------------------------------------------------*/
00032 
00033 /*---------------------------------------------------------------------------*/
00034 /* Variable declarations                                                     */
00035 /*---------------------------------------------------------------------------*/
00036 
00037 /*---------------------------------------------------------------------------*/
00038 /* Macro declarations                                                        */
00039 /*---------------------------------------------------------------------------*/
00040 
00041 
00044 /*---------------------------------------------------------------------------*/
00045 /* Static function prototypes                                                */
00046 /*---------------------------------------------------------------------------*/
00047 
00051 /*
00052     LinearSpace(f) = Space(f,f)
00053 
00054     Space(f,g)
00055         {
00056                 if ( f = const )
00057                 { 
00058                     if ( f = g )  return 1;
00059                         else          return 0;
00060                 }
00061                 if ( g = const )  return 0;
00062                 return x' * Space(fx',gx') * Space(fx,gx) + x * Space(fx',gx) * Space(fx,gx');
00063         }
00064 
00065         Equations(s) = Pos(s) + Neg(s);
00066 
00067         Pos(s)
00068         {
00069                 if ( s  = 0 )   return 1;
00070                 if ( s  = 1 )   return 0;
00071                 if ( sx'= 0 )   return Pos(sx) + x;
00072                 if ( sx = 0 )   return Pos(sx');
00073                 return 1 * [Pos(sx') & Pos(sx)] + x * [Pos(sx') & Neg(sx)];
00074         }
00075 
00076         Neg(s)
00077         {
00078                 if ( s  = 0 )   return 1;
00079                 if ( s  = 1 )   return 0;
00080                 if ( sx'= 0 )   return Neg(sx);
00081                 if ( sx = 0 )   return Neg(sx') + x;
00082                 return 1 * [Neg(sx') & Neg(sx)] + x * [Neg(sx') & Pos(sx)];
00083         }
00084 
00085 
00086     SpaceP(A)
00087         {
00088                 if ( A = 0 )    return 1;
00089                 if ( A = 1 )    return 1;
00090                 return x' * SpaceP(Ax') * SpaceP(Ax) + x * SpaceP(Ax') * SpaceN(Ax);
00091         }
00092 
00093     SpaceN(A)
00094         {
00095                 if ( A = 0 )    return 1;
00096                 if ( A = 1 )    return 0;
00097                 return x' * SpaceN(Ax') * SpaceN(Ax) + x * SpaceN(Ax') * SpaceP(Ax);
00098         }
00099 
00100 
00101     LinInd(A)
00102         {
00103                 if ( A = const )     return 1;
00104                 if ( !LinInd(Ax') )  return 0;
00105                 if ( !LinInd(Ax)  )  return 0;
00106                 if (  LinSumOdd(Ax')  & LinSumEven(Ax) != 0 )  return 0;
00107                 if (  LinSumEven(Ax') & LinSumEven(Ax) != 0 )  return 0;
00108                 return 1;
00109         }
00110 
00111         LinSumOdd(A)
00112         {
00113                 if ( A = 0 )    return 0;                 // Odd0  ---e-- Odd1
00114                 if ( A = 1 )    return 1;                 //       \   o
00115                 Odd0  = LinSumOdd(Ax');  // x is absent   //         \ 
00116                 Even0 = LinSumEven(Ax'); // x is absent   //       /   o  
00117                 Odd1  = LinSumOdd(Ax);   // x is present  // Even0 ---e-- Even1 
00118                 Even1 = LinSumEven(Ax);  // x is absent
00119                 return 1 * [Odd0 + ExorP(Odd0, Even1)] + x * [Odd1 + ExorP(Odd1, Even0)];
00120         }
00121 
00122         LinSumEven(A)
00123         {
00124                 if ( A = 0 )    return 0;
00125                 if ( A = 1 )    return 0;
00126                 Odd0  = LinSumOdd(Ax');  // x is absent
00127                 Even0 = LinSumEven(Ax'); // x is absent
00128                 Odd1  = LinSumOdd(Ax);   // x is present
00129                 Even1 = LinSumEven(Ax);  // x is absent
00130                 return 1 * [Even0 + Even1 + ExorP(Even0, Even1)] + x * [ExorP(Odd0, Odd1)];
00131         }
00132         
00133 */
00134 
00135 /*---------------------------------------------------------------------------*/
00136 /* Definition of exported functions                                          */
00137 /*---------------------------------------------------------------------------*/
00138 
00150 DdNode * Extra_bddSpaceFromFunctionFast( DdManager * dd, DdNode * bFunc )
00151 {
00152         int * pSupport;
00153         int * pPermute;
00154         int * pPermuteBack;
00155         DdNode ** pCompose;
00156         DdNode * bCube, * bTemp;
00157         DdNode * bSpace, * bFunc1, * bFunc2, * bSpaceShift;
00158         int nSupp, Counter;
00159         int i, lev;
00160 
00161         // get the support
00162         pSupport = ALLOC( int, ddMax(dd->size,dd->sizeZ) );
00163         Extra_SupportArray( dd, bFunc, pSupport );
00164         nSupp = 0;
00165         for ( i = 0; i < dd->size; i++ )
00166                 if ( pSupport[i] )
00167                         nSupp++;
00168 
00169         // make sure the manager has enough variables
00170         if ( 2*nSupp > dd->size )
00171         {
00172                 printf( "Cannot derive linear space, because DD manager does not have enough variables.\n" );
00173                 fflush( stdout );
00174                 free( pSupport );
00175                 return NULL;
00176         }
00177 
00178         // create the permutation arrays
00179         pPermute     = ALLOC( int, dd->size );
00180         pPermuteBack = ALLOC( int, dd->size );
00181         pCompose     = ALLOC( DdNode *, dd->size );
00182         for ( i = 0; i < dd->size; i++ )
00183         {
00184                 pPermute[i]     = i;
00185                 pPermuteBack[i] = i;
00186                 pCompose[i]     = dd->vars[i];   Cudd_Ref( pCompose[i] );
00187         }
00188 
00189         // remap the function in such a way that the variables are interleaved
00190         Counter = 0;
00191         bCube = b1;  Cudd_Ref( bCube );
00192         for ( lev = 0; lev < dd->size; lev++ )
00193                 if ( pSupport[ dd->invperm[lev] ] )
00194                 {   // var "dd->invperm[lev]" on level "lev" should go to level 2*Counter;
00195                         pPermute[ dd->invperm[lev] ] = dd->invperm[2*Counter];
00196                         // var from level 2*Counter+1 should go back to the place of this var
00197                         pPermuteBack[ dd->invperm[2*Counter+1] ] = dd->invperm[lev];
00198                         // the permutation should be defined in such a way that variable
00199                         // on level 2*Counter is replaced by an EXOR of itself and var on the next level
00200                         Cudd_Deref( pCompose[ dd->invperm[2*Counter] ] );
00201                         pCompose[ dd->invperm[2*Counter] ] = 
00202                                 Cudd_bddXor( dd, dd->vars[ dd->invperm[2*Counter] ], dd->vars[ dd->invperm[2*Counter+1] ] );  
00203                         Cudd_Ref( pCompose[ dd->invperm[2*Counter] ] );
00204                         // add this variable to the cube
00205                         bCube = Cudd_bddAnd( dd, bTemp = bCube, dd->vars[ dd->invperm[2*Counter] ] );  Cudd_Ref( bCube );
00206                         Cudd_RecursiveDeref( dd, bTemp );
00207                         // increment the counter
00208                         Counter ++;
00209                 }
00210 
00211         // permute the functions
00212         bFunc1 = Cudd_bddPermute( dd, bFunc, pPermute );         Cudd_Ref( bFunc1 );
00213         // compose to gate the function depending on both vars
00214         bFunc2 = Cudd_bddVectorCompose( dd, bFunc1, pCompose );  Cudd_Ref( bFunc2 );
00215         // gate the vector space
00216         // L(a) = ForAll x [ F(x) = F(x+a) ] = Not( Exist x [ F(x) (+) F(x+a) ] )
00217         bSpaceShift = Cudd_bddXorExistAbstract( dd, bFunc1, bFunc2, bCube );  Cudd_Ref( bSpaceShift );
00218         bSpaceShift = Cudd_Not( bSpaceShift );
00219         // permute the space back into the original mapping
00220         bSpace = Cudd_bddPermute( dd, bSpaceShift, pPermuteBack ); Cudd_Ref( bSpace );
00221         Cudd_RecursiveDeref( dd, bFunc1 );
00222         Cudd_RecursiveDeref( dd, bFunc2 );
00223         Cudd_RecursiveDeref( dd, bSpaceShift );
00224         Cudd_RecursiveDeref( dd, bCube );
00225 
00226         for ( i = 0; i < dd->size; i++ )
00227                 Cudd_RecursiveDeref( dd, pCompose[i] );
00228         free( pPermute );
00229         free( pPermuteBack );
00230         free( pCompose );
00231     free( pSupport );
00232 
00233         Cudd_Deref( bSpace );
00234         return bSpace;
00235 }
00236 
00237 
00238 
00250 DdNode * Extra_bddSpaceFromFunction( DdManager * dd, DdNode * bF, DdNode * bG )
00251 {
00252     DdNode * bRes;
00253     do {
00254                 dd->reordered = 0;
00255                 bRes = extraBddSpaceFromFunction( dd, bF, bG );
00256     } while (dd->reordered == 1);
00257     return bRes;
00258 }
00259 
00271 DdNode * Extra_bddSpaceFromFunctionPos( DdManager * dd, DdNode * bFunc )
00272 {
00273     DdNode * bRes;
00274     do {
00275                 dd->reordered = 0;
00276                 bRes = extraBddSpaceFromFunctionPos( dd, bFunc );
00277     } while (dd->reordered == 1);
00278     return bRes;
00279 }
00280 
00292 DdNode * Extra_bddSpaceFromFunctionNeg( DdManager * dd, DdNode * bFunc )
00293 {
00294     DdNode * bRes;
00295     do {
00296                 dd->reordered = 0;
00297                 bRes = extraBddSpaceFromFunctionNeg( dd, bFunc );
00298     } while (dd->reordered == 1);
00299     return bRes;
00300 }
00301 
00313 DdNode * Extra_bddSpaceCanonVars( DdManager * dd, DdNode * bSpace )
00314 {
00315     DdNode * bRes;
00316     do {
00317                 dd->reordered = 0;
00318                 bRes = extraBddSpaceCanonVars( dd, bSpace );
00319     } while (dd->reordered == 1);
00320     return bRes;
00321 }
00322 
00334 DdNode * Extra_bddSpaceReduce( DdManager * dd, DdNode * bFunc, DdNode * bCanonVars )
00335 {
00336         DdNode * bNegCube;
00337         DdNode * bResult;
00338         bNegCube = Extra_bddSupportNegativeCube( dd, bCanonVars );  Cudd_Ref( bNegCube );
00339         bResult  = Cudd_Cofactor( dd, bFunc, bNegCube );            Cudd_Ref( bResult );
00340         Cudd_RecursiveDeref( dd, bNegCube );
00341         Cudd_Deref( bResult );
00342         return bResult;
00343 }
00344 
00345 
00346 
00358 DdNode * Extra_bddSpaceEquations( DdManager * dd, DdNode * bSpace )
00359 {
00360     DdNode * zRes;
00361         DdNode * zEquPos;
00362         DdNode * zEquNeg;
00363         zEquPos = Extra_bddSpaceEquationsPos( dd, bSpace );  Cudd_Ref( zEquPos );
00364         zEquNeg = Extra_bddSpaceEquationsNeg( dd, bSpace );  Cudd_Ref( zEquNeg );
00365         zRes    = Cudd_zddUnion( dd, zEquPos, zEquNeg );     Cudd_Ref( zRes );
00366         Cudd_RecursiveDerefZdd( dd, zEquPos );
00367         Cudd_RecursiveDerefZdd( dd, zEquNeg );
00368         Cudd_Deref( zRes );
00369     return zRes;
00370 }
00371 
00372 
00384 DdNode * Extra_bddSpaceEquationsPos( DdManager * dd, DdNode * bSpace )
00385 {
00386     DdNode * zRes;
00387     do {
00388                 dd->reordered = 0;
00389                 zRes = extraBddSpaceEquationsPos( dd, bSpace );
00390     } while (dd->reordered == 1);
00391     return zRes;
00392 }
00393 
00394 
00406 DdNode * Extra_bddSpaceEquationsNeg( DdManager * dd, DdNode * bSpace )
00407 {
00408     DdNode * zRes;
00409     do {
00410                 dd->reordered = 0;
00411                 zRes = extraBddSpaceEquationsNeg( dd, bSpace );
00412     } while (dd->reordered == 1);
00413     return zRes;
00414 }
00415 
00416 
00428 DdNode * Extra_bddSpaceFromMatrixPos( DdManager * dd, DdNode * zA )
00429 {
00430     DdNode * bRes;
00431     do {
00432                 dd->reordered = 0;
00433                 bRes = extraBddSpaceFromMatrixPos( dd, zA );
00434     } while (dd->reordered == 1);
00435     return bRes;
00436 }
00437 
00449 DdNode * Extra_bddSpaceFromMatrixNeg( DdManager * dd, DdNode * zA )
00450 {
00451     DdNode * bRes;
00452     do {
00453                 dd->reordered = 0;
00454                 bRes = extraBddSpaceFromMatrixNeg( dd, zA );
00455     } while (dd->reordered == 1);
00456     return bRes;
00457 }
00458 
00470 int Extra_zddLitCountComb( DdManager * dd, DdNode * zComb )
00471 {
00472         int Counter;
00473         if ( zComb == z0 )
00474                 return 0;
00475         Counter = 0;
00476         for ( ; zComb != z1; zComb = cuddT(zComb) )
00477                 Counter++;
00478         return Counter;
00479 }
00480 
00494 DdNode ** Extra_bddSpaceExorGates( DdManager * dd, DdNode * bFuncRed, DdNode * zEquations )
00495 {
00496         DdNode ** pzRes;
00497         int * pVarsNonCan;
00498         DdNode * zEquRem;
00499         int iVarNonCan;
00500         DdNode * zExor, * zTemp;
00501 
00502         // get the set of non-canonical variables
00503         pVarsNonCan = ALLOC( int, ddMax(dd->size,dd->sizeZ) );
00504         Extra_SupportArray( dd, bFuncRed, pVarsNonCan );
00505 
00506         // allocate storage for the EXOR sets
00507         pzRes = ALLOC( DdNode *, dd->size );
00508         memset( pzRes, 0, sizeof(DdNode *) * dd->size );
00509 
00510         // go through all the equations
00511         zEquRem = zEquations;  Cudd_Ref( zEquRem );
00512         while ( zEquRem != z0 )
00513         {
00514                 // extract one product
00515                 zExor = Extra_zddSelectOneSubset( dd, zEquRem );   Cudd_Ref( zExor );
00516                 // remove it from the set
00517                 zEquRem = Cudd_zddDiff( dd, zTemp = zEquRem, zExor );  Cudd_Ref( zEquRem );
00518                 Cudd_RecursiveDerefZdd( dd, zTemp );
00519 
00520                 // locate the non-canonical variable
00521                 iVarNonCan = -1;
00522                 for ( zTemp = zExor; zTemp != z1; zTemp = cuddT(zTemp) )
00523                 {
00524                         if ( pVarsNonCan[zTemp->index/2] == 1 )
00525                         {
00526                                 assert( iVarNonCan == -1 );
00527                                 iVarNonCan = zTemp->index/2;
00528                         }
00529                 }
00530                 assert( iVarNonCan != -1 );
00531 
00532                 if ( Extra_zddLitCountComb( dd, zExor ) > 1 )
00533                         pzRes[ iVarNonCan ] = zExor; // takes ref
00534                 else
00535                         Cudd_RecursiveDerefZdd( dd, zExor );
00536         }
00537         Cudd_RecursiveDerefZdd( dd, zEquRem );
00538 
00539         free( pVarsNonCan );
00540         return pzRes;
00541 }
00542 
00543 
00544 /*---------------------------------------------------------------------------*/
00545 /* Definition of internal functions                                          */
00546 /*---------------------------------------------------------------------------*/
00547 
00559 DdNode * extraBddSpaceFromFunction( DdManager * dd, DdNode * bF, DdNode * bG )
00560 {
00561         DdNode * bRes;
00562         DdNode * bFR, * bGR;
00563 
00564         bFR = Cudd_Regular( bF ); 
00565         bGR = Cudd_Regular( bG ); 
00566         if ( cuddIsConstant(bFR) )
00567         {
00568                 if ( bF == bG )
00569                         return b1;
00570                 else 
00571                         return b0;
00572         }
00573         if ( cuddIsConstant(bGR) )
00574                 return b0;
00575         // both bFunc and bCore are not constants
00576 
00577         // the operation is commutative - normalize the problem
00578         if ( (unsigned)bF > (unsigned)bG )
00579                 return extraBddSpaceFromFunction(dd, bG, bF);
00580 
00581 
00582     if ( bRes = cuddCacheLookup2(dd, extraBddSpaceFromFunction, bF, bG) )
00583         return bRes;
00584         else
00585         {
00586                 DdNode * bF0, * bF1;
00587                 DdNode * bG0, * bG1;
00588                 DdNode * bTemp1, * bTemp2;
00589                 DdNode * bRes0, * bRes1;
00590                 int LevelF, LevelG;
00591                 int index;
00592 
00593                 LevelF = dd->perm[bFR->index];
00594                 LevelG = dd->perm[bGR->index];
00595                 if ( LevelF <= LevelG )
00596                 {
00597                         index = dd->invperm[LevelF];
00598                         if ( bFR != bF )
00599                         {
00600                                 bF0 = Cudd_Not( cuddE(bFR) );
00601                                 bF1 = Cudd_Not( cuddT(bFR) );
00602                         }
00603                         else
00604                         {
00605                                 bF0 = cuddE(bFR);
00606                                 bF1 = cuddT(bFR);
00607                         }
00608                 }
00609                 else
00610                 {
00611                         index = dd->invperm[LevelG];
00612                         bF0 = bF1 = bF;
00613                 }
00614 
00615                 if ( LevelG <= LevelF )
00616                 {
00617                         if ( bGR != bG )
00618                         {
00619                                 bG0 = Cudd_Not( cuddE(bGR) );
00620                                 bG1 = Cudd_Not( cuddT(bGR) );
00621                         }
00622                         else
00623                         {
00624                                 bG0 = cuddE(bGR);
00625                                 bG1 = cuddT(bGR);
00626                         }
00627                 }
00628                 else
00629                         bG0 = bG1 = bG;
00630 
00631                 bTemp1 = extraBddSpaceFromFunction( dd, bF0, bG0 );
00632                 if ( bTemp1 == NULL ) 
00633                         return NULL;
00634                 cuddRef( bTemp1 );
00635 
00636                 bTemp2 = extraBddSpaceFromFunction( dd, bF1, bG1 );
00637                 if ( bTemp2 == NULL ) 
00638                 {
00639                         Cudd_RecursiveDeref( dd, bTemp1 );
00640                         return NULL;
00641                 }
00642                 cuddRef( bTemp2 );
00643 
00644 
00645                 bRes0  = cuddBddAndRecur( dd, bTemp1, bTemp2 );
00646                 if ( bRes0 == NULL )
00647                 {
00648                         Cudd_RecursiveDeref( dd, bTemp1 );
00649                         Cudd_RecursiveDeref( dd, bTemp2 );
00650                         return NULL;
00651                 }
00652                 cuddRef( bRes0 );
00653                 Cudd_RecursiveDeref( dd, bTemp1 );
00654                 Cudd_RecursiveDeref( dd, bTemp2 );
00655 
00656 
00657                 bTemp1  = extraBddSpaceFromFunction( dd, bF0, bG1 );
00658                 if ( bTemp1 == NULL )
00659                 {
00660                         Cudd_RecursiveDeref( dd, bRes0 );
00661                         return NULL;
00662                 }
00663                 cuddRef( bTemp1 );
00664 
00665                 bTemp2  = extraBddSpaceFromFunction( dd, bF1, bG0 );
00666                 if ( bTemp2 == NULL )
00667                 {
00668                         Cudd_RecursiveDeref( dd, bRes0 );
00669                         Cudd_RecursiveDeref( dd, bTemp1 );
00670                         return NULL;
00671                 }
00672                 cuddRef( bTemp2 );
00673 
00674                 bRes1  = cuddBddAndRecur( dd, bTemp1, bTemp2 );
00675                 if ( bRes1 == NULL )
00676                 {
00677                         Cudd_RecursiveDeref( dd, bRes0 );
00678                         Cudd_RecursiveDeref( dd, bTemp1 );
00679                         Cudd_RecursiveDeref( dd, bTemp2 );
00680                         return NULL;
00681                 }
00682                 cuddRef( bRes1 );
00683                 Cudd_RecursiveDeref( dd, bTemp1 );
00684                 Cudd_RecursiveDeref( dd, bTemp2 );
00685 
00686 
00687 
00688                 // consider the case when Res0 and Res1 are the same node 
00689                 if ( bRes0 == bRes1 )
00690                         bRes = bRes1;
00691                 // consider the case when Res1 is complemented 
00692                 else if ( Cudd_IsComplement(bRes1) ) 
00693                 {
00694                         bRes = cuddUniqueInter(dd, index, Cudd_Not(bRes1), Cudd_Not(bRes0));
00695                         if ( bRes == NULL ) 
00696                         {
00697                                 Cudd_RecursiveDeref(dd,bRes0);
00698                                 Cudd_RecursiveDeref(dd,bRes1);
00699                                 return NULL;
00700                         }
00701                         bRes = Cudd_Not(bRes);
00702                 } 
00703                 else 
00704                 {
00705                         bRes = cuddUniqueInter( dd, index, bRes1, bRes0 );
00706                         if ( bRes == NULL ) 
00707                         {
00708                                 Cudd_RecursiveDeref(dd,bRes0);
00709                                 Cudd_RecursiveDeref(dd,bRes1);
00710                                 return NULL;
00711                         }
00712                 }
00713                 cuddDeref( bRes0 );
00714                 cuddDeref( bRes1 );
00715                         
00716                 // insert the result into cache 
00717                 cuddCacheInsert2(dd, extraBddSpaceFromFunction, bF, bG, bRes);
00718                 return bRes;
00719         }
00720 }  /* end of extraBddSpaceFromFunction */
00721 
00722 
00723 
00735 DdNode * extraBddSpaceFromFunctionPos( DdManager * dd, DdNode * bF )
00736 {
00737         DdNode * bRes, * bFR;
00738         statLine( dd );
00739 
00740         bFR = Cudd_Regular(bF);
00741         if ( cuddIsConstant(bFR) )
00742                 return b1;
00743 
00744     if ( bRes = cuddCacheLookup1(dd, extraBddSpaceFromFunctionPos, bF) )
00745         return bRes;
00746         else
00747         {
00748                 DdNode * bF0,   * bF1;
00749                 DdNode * bPos0, * bPos1;
00750                 DdNode * bNeg0, * bNeg1;
00751                 DdNode * bRes0, * bRes1; 
00752 
00753                 if ( bFR != bF ) // bF is complemented 
00754                 {
00755                         bF0 = Cudd_Not( cuddE(bFR) );
00756                         bF1 = Cudd_Not( cuddT(bFR) );
00757                 }
00758                 else
00759                 {
00760                         bF0 = cuddE(bFR);
00761                         bF1 = cuddT(bFR);
00762                 }
00763 
00764 
00765                 bPos0  = extraBddSpaceFromFunctionPos( dd, bF0 );
00766                 if ( bPos0 == NULL )
00767                         return NULL;
00768                 cuddRef( bPos0 );
00769 
00770                 bPos1  = extraBddSpaceFromFunctionPos( dd, bF1 );
00771                 if ( bPos1 == NULL )
00772                 {
00773                         Cudd_RecursiveDeref( dd, bPos0 );
00774                         return NULL;
00775                 }
00776                 cuddRef( bPos1 );
00777 
00778                 bRes0  = cuddBddAndRecur( dd, bPos0, bPos1 );
00779                 if ( bRes0 == NULL )
00780                 {
00781                         Cudd_RecursiveDeref( dd, bPos0 );
00782                         Cudd_RecursiveDeref( dd, bPos1 );
00783                         return NULL;
00784                 }
00785                 cuddRef( bRes0 );
00786                 Cudd_RecursiveDeref( dd, bPos0 );
00787                 Cudd_RecursiveDeref( dd, bPos1 );
00788 
00789 
00790                 bNeg0  = extraBddSpaceFromFunctionNeg( dd, bF0 );
00791                 if ( bNeg0 == NULL )
00792                 {
00793                         Cudd_RecursiveDeref( dd, bRes0 );
00794                         return NULL;
00795                 }
00796                 cuddRef( bNeg0 );
00797 
00798                 bNeg1  = extraBddSpaceFromFunctionNeg( dd, bF1 );
00799                 if ( bNeg1 == NULL )
00800                 {
00801                         Cudd_RecursiveDeref( dd, bRes0 );
00802                         Cudd_RecursiveDeref( dd, bNeg0 );
00803                         return NULL;
00804                 }
00805                 cuddRef( bNeg1 );
00806 
00807                 bRes1  = cuddBddAndRecur( dd, bNeg0, bNeg1 );
00808                 if ( bRes1 == NULL )
00809                 {
00810                         Cudd_RecursiveDeref( dd, bRes0 );
00811                         Cudd_RecursiveDeref( dd, bNeg0 );
00812                         Cudd_RecursiveDeref( dd, bNeg1 );
00813                         return NULL;
00814                 }
00815                 cuddRef( bRes1 );
00816                 Cudd_RecursiveDeref( dd, bNeg0 );
00817                 Cudd_RecursiveDeref( dd, bNeg1 );
00818 
00819 
00820                 // consider the case when Res0 and Res1 are the same node 
00821                 if ( bRes0 == bRes1 )
00822                         bRes = bRes1;
00823                 // consider the case when Res1 is complemented 
00824                 else if ( Cudd_IsComplement(bRes1) ) 
00825                 {
00826                         bRes = cuddUniqueInter( dd, bFR->index, Cudd_Not(bRes1), Cudd_Not(bRes0) );
00827                         if ( bRes == NULL ) 
00828                         {
00829                                 Cudd_RecursiveDeref(dd,bRes0);
00830                                 Cudd_RecursiveDeref(dd,bRes1);
00831                                 return NULL;
00832                         }
00833                         bRes = Cudd_Not(bRes);
00834                 } 
00835                 else 
00836                 {
00837                         bRes = cuddUniqueInter( dd, bFR->index, bRes1, bRes0 );
00838                         if ( bRes == NULL ) 
00839                         {
00840                                 Cudd_RecursiveDeref(dd,bRes0);
00841                                 Cudd_RecursiveDeref(dd,bRes1);
00842                                 return NULL;
00843                         }
00844                 }
00845                 cuddDeref( bRes0 );
00846                 cuddDeref( bRes1 );
00847 
00848                 cuddCacheInsert1( dd, extraBddSpaceFromFunctionPos, bF, bRes );
00849                 return bRes;
00850         }
00851 }
00852 
00853 
00854 
00866 DdNode * extraBddSpaceFromFunctionNeg( DdManager * dd, DdNode * bF )
00867 {
00868         DdNode * bRes, * bFR;
00869         statLine( dd );
00870 
00871         bFR = Cudd_Regular(bF);
00872         if ( cuddIsConstant(bFR) )
00873                 return b0;
00874 
00875     if ( bRes = cuddCacheLookup1(dd, extraBddSpaceFromFunctionNeg, bF) )
00876         return bRes;
00877         else
00878         {
00879                 DdNode * bF0,   * bF1;
00880                 DdNode * bPos0, * bPos1;
00881                 DdNode * bNeg0, * bNeg1;
00882                 DdNode * bRes0, * bRes1; 
00883 
00884                 if ( bFR != bF ) // bF is complemented 
00885                 {
00886                         bF0 = Cudd_Not( cuddE(bFR) );
00887                         bF1 = Cudd_Not( cuddT(bFR) );
00888                 }
00889                 else
00890                 {
00891                         bF0 = cuddE(bFR);
00892                         bF1 = cuddT(bFR);
00893                 }
00894 
00895 
00896                 bPos0  = extraBddSpaceFromFunctionNeg( dd, bF0 );
00897                 if ( bPos0 == NULL )
00898                         return NULL;
00899                 cuddRef( bPos0 );
00900 
00901                 bPos1  = extraBddSpaceFromFunctionNeg( dd, bF1 );
00902                 if ( bPos1 == NULL )
00903                 {
00904                         Cudd_RecursiveDeref( dd, bPos0 );
00905                         return NULL;
00906                 }
00907                 cuddRef( bPos1 );
00908 
00909                 bRes0  = cuddBddAndRecur( dd, bPos0, bPos1 );
00910                 if ( bRes0 == NULL )
00911                 {
00912                         Cudd_RecursiveDeref( dd, bPos0 );
00913                         Cudd_RecursiveDeref( dd, bPos1 );
00914                         return NULL;
00915                 }
00916                 cuddRef( bRes0 );
00917                 Cudd_RecursiveDeref( dd, bPos0 );
00918                 Cudd_RecursiveDeref( dd, bPos1 );
00919 
00920 
00921                 bNeg0  = extraBddSpaceFromFunctionPos( dd, bF0 );
00922                 if ( bNeg0 == NULL )
00923                 {
00924                         Cudd_RecursiveDeref( dd, bRes0 );
00925                         return NULL;
00926                 }
00927                 cuddRef( bNeg0 );
00928 
00929                 bNeg1  = extraBddSpaceFromFunctionPos( dd, bF1 );
00930                 if ( bNeg1 == NULL )
00931                 {
00932                         Cudd_RecursiveDeref( dd, bRes0 );
00933                         Cudd_RecursiveDeref( dd, bNeg0 );
00934                         return NULL;
00935                 }
00936                 cuddRef( bNeg1 );
00937 
00938                 bRes1  = cuddBddAndRecur( dd, bNeg0, bNeg1 );
00939                 if ( bRes1 == NULL )
00940                 {
00941                         Cudd_RecursiveDeref( dd, bRes0 );
00942                         Cudd_RecursiveDeref( dd, bNeg0 );
00943                         Cudd_RecursiveDeref( dd, bNeg1 );
00944                         return NULL;
00945                 }
00946                 cuddRef( bRes1 );
00947                 Cudd_RecursiveDeref( dd, bNeg0 );
00948                 Cudd_RecursiveDeref( dd, bNeg1 );
00949 
00950 
00951                 // consider the case when Res0 and Res1 are the same node 
00952                 if ( bRes0 == bRes1 )
00953                         bRes = bRes1;
00954                 // consider the case when Res1 is complemented 
00955                 else if ( Cudd_IsComplement(bRes1) ) 
00956                 {
00957                         bRes = cuddUniqueInter( dd, bFR->index, Cudd_Not(bRes1), Cudd_Not(bRes0) );
00958                         if ( bRes == NULL ) 
00959                         {
00960                                 Cudd_RecursiveDeref(dd,bRes0);
00961                                 Cudd_RecursiveDeref(dd,bRes1);
00962                                 return NULL;
00963                         }
00964                         bRes = Cudd_Not(bRes);
00965                 } 
00966                 else 
00967                 {
00968                         bRes = cuddUniqueInter( dd, bFR->index, bRes1, bRes0 );
00969                         if ( bRes == NULL ) 
00970                         {
00971                                 Cudd_RecursiveDeref(dd,bRes0);
00972                                 Cudd_RecursiveDeref(dd,bRes1);
00973                                 return NULL;
00974                         }
00975                 }
00976                 cuddDeref( bRes0 );
00977                 cuddDeref( bRes1 );
00978 
00979                 cuddCacheInsert1( dd, extraBddSpaceFromFunctionNeg, bF, bRes );
00980                 return bRes;
00981         }
00982 }
00983 
00984 
00985 
00997 DdNode * extraBddSpaceCanonVars( DdManager * dd, DdNode * bF )
00998 {
00999         DdNode * bRes, * bFR;
01000         statLine( dd );
01001 
01002         bFR = Cudd_Regular(bF);
01003         if ( cuddIsConstant(bFR) )
01004                 return bF;
01005 
01006     if ( bRes = cuddCacheLookup1(dd, extraBddSpaceCanonVars, bF) )
01007         return bRes;
01008         else
01009         {
01010                 DdNode * bF0,  * bF1;
01011                 DdNode * bRes, * bRes0; 
01012 
01013                 if ( bFR != bF ) // bF is complemented 
01014                 {
01015                         bF0 = Cudd_Not( cuddE(bFR) );
01016                         bF1 = Cudd_Not( cuddT(bFR) );
01017                 }
01018                 else
01019                 {
01020                         bF0 = cuddE(bFR);
01021                         bF1 = cuddT(bFR);
01022                 }
01023 
01024                 if ( bF0 == b0 )
01025                 {
01026                         bRes = extraBddSpaceCanonVars( dd, bF1 );
01027                         if ( bRes == NULL )
01028                                 return NULL;
01029                 }
01030                 else if ( bF1 == b0 )
01031                 {
01032                         bRes = extraBddSpaceCanonVars( dd, bF0 );
01033                         if ( bRes == NULL )
01034                                 return NULL;
01035                 }
01036                 else
01037                 {
01038                         bRes0 = extraBddSpaceCanonVars( dd, bF0 );
01039                         if ( bRes0 == NULL )
01040                                 return NULL;
01041                         cuddRef( bRes0 );
01042 
01043                         bRes = cuddUniqueInter( dd, bFR->index, bRes0, b0 );
01044                         if ( bRes == NULL ) 
01045                         {
01046                                 Cudd_RecursiveDeref( dd,bRes0 );
01047                                 return NULL;
01048                         }
01049                         cuddDeref( bRes0 );
01050                 }
01051 
01052                 cuddCacheInsert1( dd, extraBddSpaceCanonVars, bF, bRes );
01053                 return bRes;
01054         }
01055 }
01056 
01068 DdNode * extraBddSpaceEquationsPos( DdManager * dd, DdNode * bF )
01069 {
01070         DdNode * zRes;
01071         statLine( dd );
01072 
01073         if ( bF == b0 )
01074                 return z1;
01075         if ( bF == b1 )
01076                 return z0;
01077         
01078     if ( zRes = cuddCacheLookup1Zdd(dd, extraBddSpaceEquationsPos, bF) )
01079         return zRes;
01080         else
01081         {
01082                 DdNode * bFR, * bF0,  * bF1;
01083                 DdNode * zPos0, * zPos1, * zNeg1; 
01084                 DdNode * zRes, * zRes0, * zRes1;
01085 
01086                 bFR = Cudd_Regular(bF);
01087                 if ( bFR != bF ) // bF is complemented 
01088                 {
01089                         bF0 = Cudd_Not( cuddE(bFR) );
01090                         bF1 = Cudd_Not( cuddT(bFR) );
01091                 }
01092                 else
01093                 {
01094                         bF0 = cuddE(bFR);
01095                         bF1 = cuddT(bFR);
01096                 }
01097 
01098                 if ( bF0 == b0 )
01099                 {
01100                         zRes1 = extraBddSpaceEquationsPos( dd, bF1 );
01101                         if ( zRes1 == NULL )
01102                                 return NULL;
01103                         cuddRef( zRes1 );
01104 
01105                         // add the current element to the set
01106                         zRes = cuddZddGetNode( dd, 2*bFR->index, z1, zRes1 );
01107                         if ( zRes == NULL ) 
01108                         {
01109                                 Cudd_RecursiveDerefZdd(dd, zRes1);
01110                                 return NULL;
01111                         }
01112                         cuddDeref( zRes1 );
01113                 }
01114                 else if ( bF1 == b0 )
01115                 {
01116                         zRes = extraBddSpaceEquationsPos( dd, bF0 );
01117                         if ( zRes == NULL )
01118                                 return NULL;
01119                 }
01120                 else
01121                 {
01122                         zPos0 = extraBddSpaceEquationsPos( dd, bF0 );
01123                         if ( zPos0 == NULL )
01124                                 return NULL;
01125                         cuddRef( zPos0 );
01126 
01127                         zPos1 = extraBddSpaceEquationsPos( dd, bF1 );
01128                         if ( zPos1 == NULL )
01129                         {
01130                                 Cudd_RecursiveDerefZdd(dd, zPos0);
01131                                 return NULL;
01132                         }
01133                         cuddRef( zPos1 );
01134 
01135                         zNeg1 = extraBddSpaceEquationsNeg( dd, bF1 );
01136                         if ( zNeg1 == NULL )
01137                         {
01138                                 Cudd_RecursiveDerefZdd(dd, zPos0);
01139                                 Cudd_RecursiveDerefZdd(dd, zPos1);
01140                                 return NULL;
01141                         }
01142                         cuddRef( zNeg1 );
01143 
01144 
01145                         zRes0 = cuddZddIntersect( dd, zPos0, zPos1 );
01146                         if ( zRes0 == NULL )
01147                         {
01148                                 Cudd_RecursiveDerefZdd(dd, zNeg1);
01149                                 Cudd_RecursiveDerefZdd(dd, zPos0);
01150                                 Cudd_RecursiveDerefZdd(dd, zPos1);
01151                                 return NULL;
01152                         }
01153                         cuddRef( zRes0 );
01154 
01155                         zRes1 = cuddZddIntersect( dd, zPos0, zNeg1 );
01156                         if ( zRes1 == NULL )
01157                         {
01158                                 Cudd_RecursiveDerefZdd(dd, zRes0);
01159                                 Cudd_RecursiveDerefZdd(dd, zNeg1);
01160                                 Cudd_RecursiveDerefZdd(dd, zPos0);
01161                                 Cudd_RecursiveDerefZdd(dd, zPos1);
01162                                 return NULL;
01163                         }
01164                         cuddRef( zRes1 );
01165                         Cudd_RecursiveDerefZdd(dd, zNeg1);
01166                         Cudd_RecursiveDerefZdd(dd, zPos0);
01167                         Cudd_RecursiveDerefZdd(dd, zPos1);
01168                         // only zRes0 and zRes1 are refed at this point
01169 
01170                         zRes = cuddZddGetNode( dd, 2*bFR->index, zRes1, zRes0 );
01171                         if ( zRes == NULL ) 
01172                         {
01173                                 Cudd_RecursiveDerefZdd(dd, zRes0);
01174                                 Cudd_RecursiveDerefZdd(dd, zRes1);
01175                                 return NULL;
01176                         }
01177                         cuddDeref( zRes0 );
01178                         cuddDeref( zRes1 );
01179                 }
01180 
01181                 cuddCacheInsert1( dd, extraBddSpaceEquationsPos, bF, zRes );
01182                 return zRes;
01183         }
01184 }
01185 
01186 
01198 DdNode * extraBddSpaceEquationsNeg( DdManager * dd, DdNode * bF )
01199 {
01200         DdNode * zRes;
01201         statLine( dd );
01202 
01203         if ( bF == b0 )
01204                 return z1;
01205         if ( bF == b1 )
01206                 return z0;
01207         
01208     if ( zRes = cuddCacheLookup1Zdd(dd, extraBddSpaceEquationsNeg, bF) )
01209         return zRes;
01210         else
01211         {
01212                 DdNode * bFR, * bF0,  * bF1;
01213                 DdNode * zPos0, * zPos1, * zNeg1; 
01214                 DdNode * zRes, * zRes0, * zRes1;
01215 
01216                 bFR = Cudd_Regular(bF);
01217                 if ( bFR != bF ) // bF is complemented 
01218                 {
01219                         bF0 = Cudd_Not( cuddE(bFR) );
01220                         bF1 = Cudd_Not( cuddT(bFR) );
01221                 }
01222                 else
01223                 {
01224                         bF0 = cuddE(bFR);
01225                         bF1 = cuddT(bFR);
01226                 }
01227 
01228                 if ( bF0 == b0 )
01229                 {
01230                         zRes = extraBddSpaceEquationsNeg( dd, bF1 );
01231                         if ( zRes == NULL )
01232                                 return NULL;
01233                 }
01234                 else if ( bF1 == b0 )
01235                 {
01236                         zRes0 = extraBddSpaceEquationsNeg( dd, bF0 );
01237                         if ( zRes0 == NULL )
01238                                 return NULL;
01239                         cuddRef( zRes0 );
01240 
01241                         // add the current element to the set
01242                         zRes = cuddZddGetNode( dd, 2*bFR->index, z1, zRes0 );
01243                         if ( zRes == NULL ) 
01244                         {
01245                                 Cudd_RecursiveDerefZdd(dd, zRes0);
01246                                 return NULL;
01247                         }
01248                         cuddDeref( zRes0 );
01249                 }
01250                 else
01251                 {
01252                         zPos0 = extraBddSpaceEquationsNeg( dd, bF0 );
01253                         if ( zPos0 == NULL )
01254                                 return NULL;
01255                         cuddRef( zPos0 );
01256 
01257                         zPos1 = extraBddSpaceEquationsNeg( dd, bF1 );
01258                         if ( zPos1 == NULL )
01259                         {
01260                                 Cudd_RecursiveDerefZdd(dd, zPos0);
01261                                 return NULL;
01262                         }
01263                         cuddRef( zPos1 );
01264 
01265                         zNeg1 = extraBddSpaceEquationsPos( dd, bF1 );
01266                         if ( zNeg1 == NULL )
01267                         {
01268                                 Cudd_RecursiveDerefZdd(dd, zPos0);
01269                                 Cudd_RecursiveDerefZdd(dd, zPos1);
01270                                 return NULL;
01271                         }
01272                         cuddRef( zNeg1 );
01273 
01274 
01275                         zRes0 = cuddZddIntersect( dd, zPos0, zPos1 );
01276                         if ( zRes0 == NULL )
01277                         {
01278                                 Cudd_RecursiveDerefZdd(dd, zNeg1);
01279                                 Cudd_RecursiveDerefZdd(dd, zPos0);
01280                                 Cudd_RecursiveDerefZdd(dd, zPos1);
01281                                 return NULL;
01282                         }
01283                         cuddRef( zRes0 );
01284 
01285                         zRes1 = cuddZddIntersect( dd, zPos0, zNeg1 );
01286                         if ( zRes1 == NULL )
01287                         {
01288                                 Cudd_RecursiveDerefZdd(dd, zRes0);
01289                                 Cudd_RecursiveDerefZdd(dd, zNeg1);
01290                                 Cudd_RecursiveDerefZdd(dd, zPos0);
01291                                 Cudd_RecursiveDerefZdd(dd, zPos1);
01292                                 return NULL;
01293                         }
01294                         cuddRef( zRes1 );
01295                         Cudd_RecursiveDerefZdd(dd, zNeg1);
01296                         Cudd_RecursiveDerefZdd(dd, zPos0);
01297                         Cudd_RecursiveDerefZdd(dd, zPos1);
01298                         // only zRes0 and zRes1 are refed at this point
01299 
01300                         zRes = cuddZddGetNode( dd, 2*bFR->index, zRes1, zRes0 );
01301                         if ( zRes == NULL ) 
01302                         {
01303                                 Cudd_RecursiveDerefZdd(dd, zRes0);
01304                                 Cudd_RecursiveDerefZdd(dd, zRes1);
01305                                 return NULL;
01306                         }
01307                         cuddDeref( zRes0 );
01308                         cuddDeref( zRes1 );
01309                 }
01310 
01311                 cuddCacheInsert1( dd, extraBddSpaceEquationsNeg, bF, zRes );
01312                 return zRes;
01313         }
01314 }
01315 
01316 
01317 
01318 
01330 DdNode * extraBddSpaceFromMatrixPos( DdManager * dd, DdNode * zA )
01331 {
01332         DdNode * bRes;
01333         statLine( dd );
01334 
01335         if ( zA == z0 )
01336                 return b1;
01337         if ( zA == z1 )
01338                 return b1;
01339 
01340     if ( bRes = cuddCacheLookup1(dd, extraBddSpaceFromMatrixPos, zA) )
01341         return bRes;
01342         else
01343         {
01344                 DdNode * bP0, * bP1;
01345                 DdNode * bN0, * bN1;
01346                 DdNode * bRes0, * bRes1; 
01347 
01348                 bP0  = extraBddSpaceFromMatrixPos( dd, cuddE(zA) );
01349                 if ( bP0 == NULL )
01350                         return NULL;
01351                 cuddRef( bP0 );
01352 
01353                 bP1  = extraBddSpaceFromMatrixPos( dd, cuddT(zA) );
01354                 if ( bP1 == NULL )
01355                 {
01356                         Cudd_RecursiveDeref( dd, bP0 );
01357                         return NULL;
01358                 }
01359                 cuddRef( bP1 );
01360 
01361                 bRes0  = cuddBddAndRecur( dd, bP0, bP1 );
01362                 if ( bRes0 == NULL )
01363                 {
01364                         Cudd_RecursiveDeref( dd, bP0 );
01365                         Cudd_RecursiveDeref( dd, bP1 );
01366                         return NULL;
01367                 }
01368                 cuddRef( bRes0 );
01369                 Cudd_RecursiveDeref( dd, bP0 );
01370                 Cudd_RecursiveDeref( dd, bP1 );
01371 
01372 
01373                 bN0  = extraBddSpaceFromMatrixPos( dd, cuddE(zA) );
01374                 if ( bN0 == NULL )
01375                 {
01376                         Cudd_RecursiveDeref( dd, bRes0 );
01377                         return NULL;
01378                 }
01379                 cuddRef( bN0 );
01380 
01381                 bN1  = extraBddSpaceFromMatrixNeg( dd, cuddT(zA) );
01382                 if ( bN1 == NULL )
01383                 {
01384                         Cudd_RecursiveDeref( dd, bRes0 );
01385                         Cudd_RecursiveDeref( dd, bN0 );
01386                         return NULL;
01387                 }
01388                 cuddRef( bN1 );
01389 
01390                 bRes1  = cuddBddAndRecur( dd, bN0, bN1 );
01391                 if ( bRes1 == NULL )
01392                 {
01393                         Cudd_RecursiveDeref( dd, bRes0 );
01394                         Cudd_RecursiveDeref( dd, bN0 );
01395                         Cudd_RecursiveDeref( dd, bN1 );
01396                         return NULL;
01397                 }
01398                 cuddRef( bRes1 );
01399                 Cudd_RecursiveDeref( dd, bN0 );
01400                 Cudd_RecursiveDeref( dd, bN1 );
01401 
01402 
01403                 // consider the case when Res0 and Res1 are the same node 
01404                 if ( bRes0 == bRes1 )
01405                         bRes = bRes1;
01406                 // consider the case when Res1 is complemented 
01407                 else if ( Cudd_IsComplement(bRes1) ) 
01408                 {
01409                         bRes = cuddUniqueInter( dd, zA->index/2, Cudd_Not(bRes1), Cudd_Not(bRes0) );
01410                         if ( bRes == NULL ) 
01411                         {
01412                                 Cudd_RecursiveDeref(dd,bRes0);
01413                                 Cudd_RecursiveDeref(dd,bRes1);
01414                                 return NULL;
01415                         }
01416                         bRes = Cudd_Not(bRes);
01417                 } 
01418                 else 
01419                 {
01420                         bRes = cuddUniqueInter( dd, zA->index/2, bRes1, bRes0 );
01421                         if ( bRes == NULL ) 
01422                         {
01423                                 Cudd_RecursiveDeref(dd,bRes0);
01424                                 Cudd_RecursiveDeref(dd,bRes1);
01425                                 return NULL;
01426                         }
01427                 }
01428                 cuddDeref( bRes0 );
01429                 cuddDeref( bRes1 );
01430 
01431                 cuddCacheInsert1( dd, extraBddSpaceFromMatrixPos, zA, bRes );
01432                 return bRes;
01433         }
01434 }
01435 
01436 
01448 DdNode * extraBddSpaceFromMatrixNeg( DdManager * dd, DdNode * zA )
01449 {
01450         DdNode * bRes;
01451         statLine( dd );
01452 
01453         if ( zA == z0 )
01454                 return b1;
01455         if ( zA == z1 )
01456                 return b0;
01457 
01458     if ( bRes = cuddCacheLookup1(dd, extraBddSpaceFromMatrixNeg, zA) )
01459         return bRes;
01460         else
01461         {
01462                 DdNode * bP0, * bP1;
01463                 DdNode * bN0, * bN1;
01464                 DdNode * bRes0, * bRes1; 
01465 
01466                 bP0  = extraBddSpaceFromMatrixNeg( dd, cuddE(zA) );
01467                 if ( bP0 == NULL )
01468                         return NULL;
01469                 cuddRef( bP0 );
01470 
01471                 bP1  = extraBddSpaceFromMatrixNeg( dd, cuddT(zA) );
01472                 if ( bP1 == NULL )
01473                 {
01474                         Cudd_RecursiveDeref( dd, bP0 );
01475                         return NULL;
01476                 }
01477                 cuddRef( bP1 );
01478 
01479                 bRes0  = cuddBddAndRecur( dd, bP0, bP1 );
01480                 if ( bRes0 == NULL )
01481                 {
01482                         Cudd_RecursiveDeref( dd, bP0 );
01483                         Cudd_RecursiveDeref( dd, bP1 );
01484                         return NULL;
01485                 }
01486                 cuddRef( bRes0 );
01487                 Cudd_RecursiveDeref( dd, bP0 );
01488                 Cudd_RecursiveDeref( dd, bP1 );
01489 
01490 
01491                 bN0  = extraBddSpaceFromMatrixNeg( dd, cuddE(zA) );
01492                 if ( bN0 == NULL )
01493                 {
01494                         Cudd_RecursiveDeref( dd, bRes0 );
01495                         return NULL;
01496                 }
01497                 cuddRef( bN0 );
01498 
01499                 bN1  = extraBddSpaceFromMatrixPos( dd, cuddT(zA) );
01500                 if ( bN1 == NULL )
01501                 {
01502                         Cudd_RecursiveDeref( dd, bRes0 );
01503                         Cudd_RecursiveDeref( dd, bN0 );
01504                         return NULL;
01505                 }
01506                 cuddRef( bN1 );
01507 
01508                 bRes1  = cuddBddAndRecur( dd, bN0, bN1 );
01509                 if ( bRes1 == NULL )
01510                 {
01511                         Cudd_RecursiveDeref( dd, bRes0 );
01512                         Cudd_RecursiveDeref( dd, bN0 );
01513                         Cudd_RecursiveDeref( dd, bN1 );
01514                         return NULL;
01515                 }
01516                 cuddRef( bRes1 );
01517                 Cudd_RecursiveDeref( dd, bN0 );
01518                 Cudd_RecursiveDeref( dd, bN1 );
01519 
01520 
01521                 // consider the case when Res0 and Res1 are the same node 
01522                 if ( bRes0 == bRes1 )
01523                         bRes = bRes1;
01524                 // consider the case when Res1 is complemented 
01525                 else if ( Cudd_IsComplement(bRes1) ) 
01526                 {
01527                         bRes = cuddUniqueInter( dd, zA->index/2, Cudd_Not(bRes1), Cudd_Not(bRes0) );
01528                         if ( bRes == NULL ) 
01529                         {
01530                                 Cudd_RecursiveDeref(dd,bRes0);
01531                                 Cudd_RecursiveDeref(dd,bRes1);
01532                                 return NULL;
01533                         }
01534                         bRes = Cudd_Not(bRes);
01535                 } 
01536                 else 
01537                 {
01538                         bRes = cuddUniqueInter( dd, zA->index/2, bRes1, bRes0 );
01539                         if ( bRes == NULL ) 
01540                         {
01541                                 Cudd_RecursiveDeref(dd,bRes0);
01542                                 Cudd_RecursiveDeref(dd,bRes1);
01543                                 return NULL;
01544                         }
01545                 }
01546                 cuddDeref( bRes0 );
01547                 cuddDeref( bRes1 );
01548 
01549                 cuddCacheInsert1( dd, extraBddSpaceFromMatrixNeg, zA, bRes );
01550                 return bRes;
01551         }
01552 }
01553 
01554 
01555 /*---------------------------------------------------------------------------*/
01556 /* Definition of static functions                                            */
01557 /*---------------------------------------------------------------------------*/
01558