/**CFile**************************************************************** FileName [extraBddAuto.c] PackageName [extra] Synopsis [Computation of autosymmetries.] Author [Alan Mishchenko] Affiliation [UC Berkeley] Date [Ver. 2.0. Started - September 1, 2003.] Revision [$Id: extraBddAuto.c,v 1.0 2003/05/21 18:03:50 alanmi Exp $] ***********************************************************************/ #include "extraBdd.h" ABC_NAMESPACE_IMPL_START /*---------------------------------------------------------------------------*/ /* Constant declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Stucture declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Type declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Variable declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Macro declarations */ /*---------------------------------------------------------------------------*/ /**AutomaticStart*************************************************************/ /*---------------------------------------------------------------------------*/ /* Static function prototypes */ /*---------------------------------------------------------------------------*/ /**AutomaticEnd***************************************************************/ /* LinearSpace(f) = Space(f,f) Space(f,g) { if ( f = const ) { if ( f = g ) return 1; else return 0; } if ( g = const ) return 0; return x' * Space(fx',gx') * Space(fx,gx) + x * Space(fx',gx) * Space(fx,gx'); } Equations(s) = Pos(s) + Neg(s); Pos(s) { if ( s = 0 ) return 1; if ( s = 1 ) return 0; if ( sx'= 0 ) return Pos(sx) + x; if ( sx = 0 ) return Pos(sx'); return 1 * [Pos(sx') & Pos(sx)] + x * [Pos(sx') & Neg(sx)]; } Neg(s) { if ( s = 0 ) return 1; if ( s = 1 ) return 0; if ( sx'= 0 ) return Neg(sx); if ( sx = 0 ) return Neg(sx') + x; return 1 * [Neg(sx') & Neg(sx)] + x * [Neg(sx') & Pos(sx)]; } SpaceP(A) { if ( A = 0 ) return 1; if ( A = 1 ) return 1; return x' * SpaceP(Ax') * SpaceP(Ax) + x * SpaceP(Ax') * SpaceN(Ax); } SpaceN(A) { if ( A = 0 ) return 1; if ( A = 1 ) return 0; return x' * SpaceN(Ax') * SpaceN(Ax) + x * SpaceN(Ax') * SpaceP(Ax); } LinInd(A) { if ( A = const ) return 1; if ( !LinInd(Ax') ) return 0; if ( !LinInd(Ax) ) return 0; if ( LinSumOdd(Ax') & LinSumEven(Ax) != 0 ) return 0; if ( LinSumEven(Ax') & LinSumEven(Ax) != 0 ) return 0; return 1; } LinSumOdd(A) { if ( A = 0 ) return 0; // Odd0 ---e-- Odd1 if ( A = 1 ) return 1; // \ o Odd0 = LinSumOdd(Ax'); // x is absent // \ Even0 = LinSumEven(Ax'); // x is absent // / o Odd1 = LinSumOdd(Ax); // x is present // Even0 ---e-- Even1 Even1 = LinSumEven(Ax); // x is absent return 1 * [Odd0 + ExorP(Odd0, Even1)] + x * [Odd1 + ExorP(Odd1, Even0)]; } LinSumEven(A) { if ( A = 0 ) return 0; if ( A = 1 ) return 0; Odd0 = LinSumOdd(Ax'); // x is absent Even0 = LinSumEven(Ax'); // x is absent Odd1 = LinSumOdd(Ax); // x is present Even1 = LinSumEven(Ax); // x is absent return 1 * [Even0 + Even1 + ExorP(Even0, Even1)] + x * [ExorP(Odd0, Odd1)]; } */ /*---------------------------------------------------------------------------*/ /* Definition of exported functions */ /*---------------------------------------------------------------------------*/ /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ DdNode * Extra_bddSpaceFromFunctionFast( DdManager * dd, DdNode * bFunc ) { int * pSupport; int * pPermute; int * pPermuteBack; DdNode ** pCompose; DdNode * bCube, * bTemp; DdNode * bSpace, * bFunc1, * bFunc2, * bSpaceShift; int nSupp, Counter; int i, lev; // get the support pSupport = ABC_ALLOC( int, ddMax(dd->size,dd->sizeZ) ); Extra_SupportArray( dd, bFunc, pSupport ); nSupp = 0; for ( i = 0; i < dd->size; i++ ) if ( pSupport[i] ) nSupp++; // make sure the manager has enough variables if ( 2*nSupp > dd->size ) { printf( "Cannot derive linear space, because DD manager does not have enough variables.\n" ); fflush( stdout ); ABC_FREE( pSupport ); return NULL; } // create the permutation arrays pPermute = ABC_ALLOC( int, dd->size ); pPermuteBack = ABC_ALLOC( int, dd->size ); pCompose = ABC_ALLOC( DdNode *, dd->size ); for ( i = 0; i < dd->size; i++ ) { pPermute[i] = i; pPermuteBack[i] = i; pCompose[i] = dd->vars[i]; Cudd_Ref( pCompose[i] ); } // remap the function in such a way that the variables are interleaved Counter = 0; bCube = b1; Cudd_Ref( bCube ); for ( lev = 0; lev < dd->size; lev++ ) if ( pSupport[ dd->invperm[lev] ] ) { // var "dd->invperm[lev]" on level "lev" should go to level 2*Counter; pPermute[ dd->invperm[lev] ] = dd->invperm[2*Counter]; // var from level 2*Counter+1 should go back to the place of this var pPermuteBack[ dd->invperm[2*Counter+1] ] = dd->invperm[lev]; // the permutation should be defined in such a way that variable // on level 2*Counter is replaced by an EXOR of itself and var on the next level Cudd_Deref( pCompose[ dd->invperm[2*Counter] ] ); pCompose[ dd->invperm[2*Counter] ] = Cudd_bddXor( dd, dd->vars[ dd->invperm[2*Counter] ], dd->vars[ dd->invperm[2*Counter+1] ] ); Cudd_Ref( pCompose[ dd->invperm[2*Counter] ] ); // add this variable to the cube bCube = Cudd_bddAnd( dd, bTemp = bCube, dd->vars[ dd->invperm[2*Counter] ] ); Cudd_Ref( bCube ); Cudd_RecursiveDeref( dd, bTemp ); // increment the counter Counter ++; } // permute the functions bFunc1 = Cudd_bddPermute( dd, bFunc, pPermute ); Cudd_Ref( bFunc1 ); // compose to gate the function depending on both vars bFunc2 = Cudd_bddVectorCompose( dd, bFunc1, pCompose ); Cudd_Ref( bFunc2 ); // gate the vector space // L(a) = ForAll x [ F(x) = F(x+a) ] = Not( Exist x [ F(x) (+) F(x+a) ] ) bSpaceShift = Cudd_bddXorExistAbstract( dd, bFunc1, bFunc2, bCube ); Cudd_Ref( bSpaceShift ); bSpaceShift = Cudd_Not( bSpaceShift ); // permute the space back into the original mapping bSpace = Cudd_bddPermute( dd, bSpaceShift, pPermuteBack ); Cudd_Ref( bSpace ); Cudd_RecursiveDeref( dd, bFunc1 ); Cudd_RecursiveDeref( dd, bFunc2 ); Cudd_RecursiveDeref( dd, bSpaceShift ); Cudd_RecursiveDeref( dd, bCube ); for ( i = 0; i < dd->size; i++ ) Cudd_RecursiveDeref( dd, pCompose[i] ); ABC_FREE( pPermute ); ABC_FREE( pPermuteBack ); ABC_FREE( pCompose ); ABC_FREE( pSupport ); Cudd_Deref( bSpace ); return bSpace; } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ DdNode * Extra_bddSpaceFromFunction( DdManager * dd, DdNode * bF, DdNode * bG ) { DdNode * bRes; do { dd->reordered = 0; bRes = extraBddSpaceFromFunction( dd, bF, bG ); } while (dd->reordered == 1); return bRes; } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ DdNode * Extra_bddSpaceFromFunctionPos( DdManager * dd, DdNode * bFunc ) { DdNode * bRes; do { dd->reordered = 0; bRes = extraBddSpaceFromFunctionPos( dd, bFunc ); } while (dd->reordered == 1); return bRes; } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ DdNode * Extra_bddSpaceFromFunctionNeg( DdManager * dd, DdNode * bFunc ) { DdNode * bRes; do { dd->reordered = 0; bRes = extraBddSpaceFromFunctionNeg( dd, bFunc ); } while (dd->reordered == 1); return bRes; } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ DdNode * Extra_bddSpaceCanonVars( DdManager * dd, DdNode * bSpace ) { DdNode * bRes; do { dd->reordered = 0; bRes = extraBddSpaceCanonVars( dd, bSpace ); } while (dd->reordered == 1); return bRes; } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ DdNode * Extra_bddSpaceReduce( DdManager * dd, DdNode * bFunc, DdNode * bCanonVars ) { DdNode * bNegCube; DdNode * bResult; bNegCube = Extra_bddSupportNegativeCube( dd, bCanonVars ); Cudd_Ref( bNegCube ); bResult = Cudd_Cofactor( dd, bFunc, bNegCube ); Cudd_Ref( bResult ); Cudd_RecursiveDeref( dd, bNegCube ); Cudd_Deref( bResult ); return bResult; } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ DdNode * Extra_bddSpaceEquations( DdManager * dd, DdNode * bSpace ) { DdNode * zRes; DdNode * zEquPos; DdNode * zEquNeg; zEquPos = Extra_bddSpaceEquationsPos( dd, bSpace ); Cudd_Ref( zEquPos ); zEquNeg = Extra_bddSpaceEquationsNeg( dd, bSpace ); Cudd_Ref( zEquNeg ); zRes = Cudd_zddUnion( dd, zEquPos, zEquNeg ); Cudd_Ref( zRes ); Cudd_RecursiveDerefZdd( dd, zEquPos ); Cudd_RecursiveDerefZdd( dd, zEquNeg ); Cudd_Deref( zRes ); return zRes; } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ DdNode * Extra_bddSpaceEquationsPos( DdManager * dd, DdNode * bSpace ) { DdNode * zRes; do { dd->reordered = 0; zRes = extraBddSpaceEquationsPos( dd, bSpace ); } while (dd->reordered == 1); return zRes; } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ DdNode * Extra_bddSpaceEquationsNeg( DdManager * dd, DdNode * bSpace ) { DdNode * zRes; do { dd->reordered = 0; zRes = extraBddSpaceEquationsNeg( dd, bSpace ); } while (dd->reordered == 1); return zRes; } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ DdNode * Extra_bddSpaceFromMatrixPos( DdManager * dd, DdNode * zA ) { DdNode * bRes; do { dd->reordered = 0; bRes = extraBddSpaceFromMatrixPos( dd, zA ); } while (dd->reordered == 1); return bRes; } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ DdNode * Extra_bddSpaceFromMatrixNeg( DdManager * dd, DdNode * zA ) { DdNode * bRes; do { dd->reordered = 0; bRes = extraBddSpaceFromMatrixNeg( dd, zA ); } while (dd->reordered == 1); return bRes; } /**Function************************************************************* Synopsis [Counts the number of literals in one combination.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Extra_zddLitCountComb( DdManager * dd, DdNode * zComb ) { int Counter; if ( zComb == z0 ) return 0; Counter = 0; for ( ; zComb != z1; zComb = cuddT(zComb) ) Counter++; return Counter; } /**Function************************************************************* Synopsis [] Description [Returns the array of ZDDs with the number equal to the number of vars in the DD manager. If the given var is non-canonical, this array contains the referenced ZDD representing literals in the corresponding EXOR equation.] SideEffects [] SeeAlso [] ***********************************************************************/ DdNode ** Extra_bddSpaceExorGates( DdManager * dd, DdNode * bFuncRed, DdNode * zEquations ) { DdNode ** pzRes; int * pVarsNonCan; DdNode * zEquRem; int iVarNonCan; DdNode * zExor, * zTemp; // get the set of non-canonical variables pVarsNonCan = ABC_ALLOC( int, ddMax(dd->size,dd->sizeZ) ); Extra_SupportArray( dd, bFuncRed, pVarsNonCan ); // allocate storage for the EXOR sets pzRes = ABC_ALLOC( DdNode *, dd->size ); memset( pzRes, 0, sizeof(DdNode *) * dd->size ); // go through all the equations zEquRem = zEquations; Cudd_Ref( zEquRem ); while ( zEquRem != z0 ) { // extract one product zExor = Extra_zddSelectOneSubset( dd, zEquRem ); Cudd_Ref( zExor ); // remove it from the set zEquRem = Cudd_zddDiff( dd, zTemp = zEquRem, zExor ); Cudd_Ref( zEquRem ); Cudd_RecursiveDerefZdd( dd, zTemp ); // locate the non-canonical variable iVarNonCan = -1; for ( zTemp = zExor; zTemp != z1; zTemp = cuddT(zTemp) ) { if ( pVarsNonCan[zTemp->index/2] == 1 ) { assert( iVarNonCan == -1 ); iVarNonCan = zTemp->index/2; } } assert( iVarNonCan != -1 ); if ( Extra_zddLitCountComb( dd, zExor ) > 1 ) pzRes[ iVarNonCan ] = zExor; // takes ref else Cudd_RecursiveDerefZdd( dd, zExor ); } Cudd_RecursiveDerefZdd( dd, zEquRem ); ABC_FREE( pVarsNonCan ); return pzRes; } /*---------------------------------------------------------------------------*/ /* Definition of internal functions */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [Performs the recursive steps of Extra_bddSpaceFromFunction.] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ DdNode * extraBddSpaceFromFunction( DdManager * dd, DdNode * bF, DdNode * bG ) { DdNode * bRes; DdNode * bFR, * bGR; bFR = Cudd_Regular( bF ); bGR = Cudd_Regular( bG ); if ( cuddIsConstant(bFR) ) { if ( bF == bG ) return b1; else return b0; } if ( cuddIsConstant(bGR) ) return b0; // both bFunc and bCore are not constants // the operation is commutative - normalize the problem if ( (unsigned)(ABC_PTRUINT_T)bF > (unsigned)(ABC_PTRUINT_T)bG ) return extraBddSpaceFromFunction(dd, bG, bF); if ( (bRes = cuddCacheLookup2(dd, extraBddSpaceFromFunction, bF, bG)) ) return bRes; else { DdNode * bF0, * bF1; DdNode * bG0, * bG1; DdNode * bTemp1, * bTemp2; DdNode * bRes0, * bRes1; int LevelF, LevelG; int index; LevelF = dd->perm[bFR->index]; LevelG = dd->perm[bGR->index]; if ( LevelF <= LevelG ) { index = dd->invperm[LevelF]; if ( bFR != bF ) { bF0 = Cudd_Not( cuddE(bFR) ); bF1 = Cudd_Not( cuddT(bFR) ); } else { bF0 = cuddE(bFR); bF1 = cuddT(bFR); } } else { index = dd->invperm[LevelG]; bF0 = bF1 = bF; } if ( LevelG <= LevelF ) { if ( bGR != bG ) { bG0 = Cudd_Not( cuddE(bGR) ); bG1 = Cudd_Not( cuddT(bGR) ); } else { bG0 = cuddE(bGR); bG1 = cuddT(bGR); } } else bG0 = bG1 = bG; bTemp1 = extraBddSpaceFromFunction( dd, bF0, bG0 ); if ( bTemp1 == NULL ) return NULL; cuddRef( bTemp1 ); bTemp2 = extraBddSpaceFromFunction( dd, bF1, bG1 ); if ( bTemp2 == NULL ) { Cudd_RecursiveDeref( dd, bTemp1 ); return NULL; } cuddRef( bTemp2 ); bRes0 = cuddBddAndRecur( dd, bTemp1, bTemp2 ); if ( bRes0 == NULL ) { Cudd_RecursiveDeref( dd, bTemp1 ); Cudd_RecursiveDeref( dd, bTemp2 ); return NULL; } cuddRef( bRes0 ); Cudd_RecursiveDeref( dd, bTemp1 ); Cudd_RecursiveDeref( dd, bTemp2 ); bTemp1 = extraBddSpaceFromFunction( dd, bF0, bG1 ); if ( bTemp1 == NULL ) { Cudd_RecursiveDeref( dd, bRes0 ); return NULL; } cuddRef( bTemp1 ); bTemp2 = extraBddSpaceFromFunction( dd, bF1, bG0 ); if ( bTemp2 == NULL ) { Cudd_RecursiveDeref( dd, bRes0 ); Cudd_RecursiveDeref( dd, bTemp1 ); return NULL; } cuddRef( bTemp2 ); bRes1 = cuddBddAndRecur( dd, bTemp1, bTemp2 ); if ( bRes1 == NULL ) { Cudd_RecursiveDeref( dd, bRes0 ); Cudd_RecursiveDeref( dd, bTemp1 ); Cudd_RecursiveDeref( dd, bTemp2 ); return NULL; } cuddRef( bRes1 ); Cudd_RecursiveDeref( dd, bTemp1 ); Cudd_RecursiveDeref( dd, bTemp2 ); // consider the case when Res0 and Res1 are the same node if ( bRes0 == bRes1 ) bRes = bRes1; // consider the case when Res1 is complemented else if ( Cudd_IsComplement(bRes1) ) { bRes = cuddUniqueInter(dd, index, Cudd_Not(bRes1), Cudd_Not(bRes0)); if ( bRes == NULL ) { Cudd_RecursiveDeref(dd,bRes0); Cudd_RecursiveDeref(dd,bRes1); return NULL; } bRes = Cudd_Not(bRes); } else { bRes = cuddUniqueInter( dd, index, bRes1, bRes0 ); if ( bRes == NULL ) { Cudd_RecursiveDeref(dd,bRes0); Cudd_RecursiveDeref(dd,bRes1); return NULL; } } cuddDeref( bRes0 ); cuddDeref( bRes1 ); // insert the result into cache cuddCacheInsert2(dd, extraBddSpaceFromFunction, bF, bG, bRes); return bRes; } } /* end of extraBddSpaceFromFunction */ /**Function************************************************************* Synopsis [Performs the recursive step of Extra_bddSpaceFromFunctionPos().] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ DdNode * extraBddSpaceFromFunctionPos( DdManager * dd, DdNode * bF ) { DdNode * bRes, * bFR; statLine( dd ); bFR = Cudd_Regular(bF); if ( cuddIsConstant(bFR) ) return b1; if ( (bRes = cuddCacheLookup1(dd, extraBddSpaceFromFunctionPos, bF)) ) return bRes; else { DdNode * bF0, * bF1; DdNode * bPos0, * bPos1; DdNode * bNeg0, * bNeg1; DdNode * bRes0, * bRes1; if ( bFR != bF ) // bF is complemented { bF0 = Cudd_Not( cuddE(bFR) ); bF1 = Cudd_Not( cuddT(bFR) ); } else { bF0 = cuddE(bFR); bF1 = cuddT(bFR); } bPos0 = extraBddSpaceFromFunctionPos( dd, bF0 ); if ( bPos0 == NULL ) return NULL; cuddRef( bPos0 ); bPos1 = extraBddSpaceFromFunctionPos( dd, bF1 ); if ( bPos1 == NULL ) { Cudd_RecursiveDeref( dd, bPos0 ); return NULL; } cuddRef( bPos1 ); bRes0 = cuddBddAndRecur( dd, bPos0, bPos1 ); if ( bRes0 == NULL ) { Cudd_RecursiveDeref( dd, bPos0 ); Cudd_RecursiveDeref( dd, bPos1 ); return NULL; } cuddRef( bRes0 ); Cudd_RecursiveDeref( dd, bPos0 ); Cudd_RecursiveDeref( dd, bPos1 ); bNeg0 = extraBddSpaceFromFunctionNeg( dd, bF0 ); if ( bNeg0 == NULL ) { Cudd_RecursiveDeref( dd, bRes0 ); return NULL; } cuddRef( bNeg0 ); bNeg1 = extraBddSpaceFromFunctionNeg( dd, bF1 ); if ( bNeg1 == NULL ) { Cudd_RecursiveDeref( dd, bRes0 ); Cudd_RecursiveDeref( dd, bNeg0 ); return NULL; } cuddRef( bNeg1 ); bRes1 = cuddBddAndRecur( dd, bNeg0, bNeg1 ); if ( bRes1 == NULL ) { Cudd_RecursiveDeref( dd, bRes0 ); Cudd_RecursiveDeref( dd, bNeg0 ); Cudd_RecursiveDeref( dd, bNeg1 ); return NULL; } cuddRef( bRes1 ); Cudd_RecursiveDeref( dd, bNeg0 ); Cudd_RecursiveDeref( dd, bNeg1 ); // consider the case when Res0 and Res1 are the same node if ( bRes0 == bRes1 ) bRes = bRes1; // consider the case when Res1 is complemented else if ( Cudd_IsComplement(bRes1) ) { bRes = cuddUniqueInter( dd, bFR->index, Cudd_Not(bRes1), Cudd_Not(bRes0) ); if ( bRes == NULL ) { Cudd_RecursiveDeref(dd,bRes0); Cudd_RecursiveDeref(dd,bRes1); return NULL; } bRes = Cudd_Not(bRes); } else { bRes = cuddUniqueInter( dd, bFR->index, bRes1, bRes0 ); if ( bRes == NULL ) { Cudd_RecursiveDeref(dd,bRes0); Cudd_RecursiveDeref(dd,bRes1); return NULL; } } cuddDeref( bRes0 ); cuddDeref( bRes1 ); cuddCacheInsert1( dd, extraBddSpaceFromFunctionPos, bF, bRes ); return bRes; } } /**Function************************************************************* Synopsis [Performs the recursive step of Extra_bddSpaceFromFunctionPos().] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ DdNode * extraBddSpaceFromFunctionNeg( DdManager * dd, DdNode * bF ) { DdNode * bRes, * bFR; statLine( dd ); bFR = Cudd_Regular(bF); if ( cuddIsConstant(bFR) ) return b0; if ( (bRes = cuddCacheLookup1(dd, extraBddSpaceFromFunctionNeg, bF)) ) return bRes; else { DdNode * bF0, * bF1; DdNode * bPos0, * bPos1; DdNode * bNeg0, * bNeg1; DdNode * bRes0, * bRes1; if ( bFR != bF ) // bF is complemented { bF0 = Cudd_Not( cuddE(bFR) ); bF1 = Cudd_Not( cuddT(bFR) ); } else { bF0 = cuddE(bFR); bF1 = cuddT(bFR); } bPos0 = extraBddSpaceFromFunctionNeg( dd, bF0 ); if ( bPos0 == NULL ) return NULL; cuddRef( bPos0 ); bPos1 = extraBddSpaceFromFunctionNeg( dd, bF1 ); if ( bPos1 == NULL ) { Cudd_RecursiveDeref( dd, bPos0 ); return NULL; } cuddRef( bPos1 ); bRes0 = cuddBddAndRecur( dd, bPos0, bPos1 ); if ( bRes0 == NULL ) { Cudd_RecursiveDeref( dd, bPos0 ); Cudd_RecursiveDeref( dd, bPos1 ); return NULL; } cuddRef( bRes0 ); Cudd_RecursiveDeref( dd, bPos0 ); Cudd_RecursiveDeref( dd, bPos1 ); bNeg0 = extraBddSpaceFromFunctionPos( dd, bF0 ); if ( bNeg0 == NULL ) { Cudd_RecursiveDeref( dd, bRes0 ); return NULL; } cuddRef( bNeg0 ); bNeg1 = extraBddSpaceFromFunctionPos( dd, bF1 ); if ( bNeg1 == NULL ) { Cudd_RecursiveDeref( dd, bRes0 ); Cudd_RecursiveDeref( dd, bNeg0 ); return NULL; } cuddRef( bNeg1 ); bRes1 = cuddBddAndRecur( dd, bNeg0, bNeg1 ); if ( bRes1 == NULL ) { Cudd_RecursiveDeref( dd, bRes0 ); Cudd_RecursiveDeref( dd, bNeg0 ); Cudd_RecursiveDeref( dd, bNeg1 ); return NULL; } cuddRef( bRes1 ); Cudd_RecursiveDeref( dd, bNeg0 ); Cudd_RecursiveDeref( dd, bNeg1 ); // consider the case when Res0 and Res1 are the same node if ( bRes0 == bRes1 ) bRes = bRes1; // consider the case when Res1 is complemented else if ( Cudd_IsComplement(bRes1) ) { bRes = cuddUniqueInter( dd, bFR->index, Cudd_Not(bRes1), Cudd_Not(bRes0) ); if ( bRes == NULL ) { Cudd_RecursiveDeref(dd,bRes0); Cudd_RecursiveDeref(dd,bRes1); return NULL; } bRes = Cudd_Not(bRes); } else { bRes = cuddUniqueInter( dd, bFR->index, bRes1, bRes0 ); if ( bRes == NULL ) { Cudd_RecursiveDeref(dd,bRes0); Cudd_RecursiveDeref(dd,bRes1); return NULL; } } cuddDeref( bRes0 ); cuddDeref( bRes1 ); cuddCacheInsert1( dd, extraBddSpaceFromFunctionNeg, bF, bRes ); return bRes; } } /**Function************************************************************* Synopsis [Performs the recursive step of Extra_bddSpaceCanonVars().] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ DdNode * extraBddSpaceCanonVars( DdManager * dd, DdNode * bF ) { DdNode * bRes, * bFR; statLine( dd ); bFR = Cudd_Regular(bF); if ( cuddIsConstant(bFR) ) return bF; if ( (bRes = cuddCacheLookup1(dd, extraBddSpaceCanonVars, bF)) ) return bRes; else { DdNode * bF0, * bF1; DdNode * bRes, * bRes0; if ( bFR != bF ) // bF is complemented { bF0 = Cudd_Not( cuddE(bFR) ); bF1 = Cudd_Not( cuddT(bFR) ); } else { bF0 = cuddE(bFR); bF1 = cuddT(bFR); } if ( bF0 == b0 ) { bRes = extraBddSpaceCanonVars( dd, bF1 ); if ( bRes == NULL ) return NULL; } else if ( bF1 == b0 ) { bRes = extraBddSpaceCanonVars( dd, bF0 ); if ( bRes == NULL ) return NULL; } else { bRes0 = extraBddSpaceCanonVars( dd, bF0 ); if ( bRes0 == NULL ) return NULL; cuddRef( bRes0 ); bRes = cuddUniqueInter( dd, bFR->index, bRes0, b0 ); if ( bRes == NULL ) { Cudd_RecursiveDeref( dd,bRes0 ); return NULL; } cuddDeref( bRes0 ); } cuddCacheInsert1( dd, extraBddSpaceCanonVars, bF, bRes ); return bRes; } } /**Function************************************************************* Synopsis [Performs the recursive step of Extra_bddSpaceEquationsPos().] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ DdNode * extraBddSpaceEquationsPos( DdManager * dd, DdNode * bF ) { DdNode * zRes; statLine( dd ); if ( bF == b0 ) return z1; if ( bF == b1 ) return z0; if ( (zRes = cuddCacheLookup1Zdd(dd, extraBddSpaceEquationsPos, bF)) ) return zRes; else { DdNode * bFR, * bF0, * bF1; DdNode * zPos0, * zPos1, * zNeg1; DdNode * zRes, * zRes0, * zRes1; bFR = Cudd_Regular(bF); if ( bFR != bF ) // bF is complemented { bF0 = Cudd_Not( cuddE(bFR) ); bF1 = Cudd_Not( cuddT(bFR) ); } else { bF0 = cuddE(bFR); bF1 = cuddT(bFR); } if ( bF0 == b0 ) { zRes1 = extraBddSpaceEquationsPos( dd, bF1 ); if ( zRes1 == NULL ) return NULL; cuddRef( zRes1 ); // add the current element to the set zRes = cuddZddGetNode( dd, 2*bFR->index, z1, zRes1 ); if ( zRes == NULL ) { Cudd_RecursiveDerefZdd(dd, zRes1); return NULL; } cuddDeref( zRes1 ); } else if ( bF1 == b0 ) { zRes = extraBddSpaceEquationsPos( dd, bF0 ); if ( zRes == NULL ) return NULL; } else { zPos0 = extraBddSpaceEquationsPos( dd, bF0 ); if ( zPos0 == NULL ) return NULL; cuddRef( zPos0 ); zPos1 = extraBddSpaceEquationsPos( dd, bF1 ); if ( zPos1 == NULL ) { Cudd_RecursiveDerefZdd(dd, zPos0); return NULL; } cuddRef( zPos1 ); zNeg1 = extraBddSpaceEquationsNeg( dd, bF1 ); if ( zNeg1 == NULL ) { Cudd_RecursiveDerefZdd(dd, zPos0); Cudd_RecursiveDerefZdd(dd, zPos1); return NULL; } cuddRef( zNeg1 ); zRes0 = cuddZddIntersect( dd, zPos0, zPos1 ); if ( zRes0 == NULL ) { Cudd_RecursiveDerefZdd(dd, zNeg1); Cudd_RecursiveDerefZdd(dd, zPos0); Cudd_RecursiveDerefZdd(dd, zPos1); return NULL; } cuddRef( zRes0 ); zRes1 = cuddZddIntersect( dd, zPos0, zNeg1 ); if ( zRes1 == NULL ) { Cudd_RecursiveDerefZdd(dd, zRes0); Cudd_RecursiveDerefZdd(dd, zNeg1); Cudd_RecursiveDerefZdd(dd, zPos0); Cudd_RecursiveDerefZdd(dd, zPos1); return NULL; } cuddRef( zRes1 ); Cudd_RecursiveDerefZdd(dd, zNeg1); Cudd_RecursiveDerefZdd(dd, zPos0); Cudd_RecursiveDerefZdd(dd, zPos1); // only zRes0 and zRes1 are refed at this point zRes = cuddZddGetNode( dd, 2*bFR->index, zRes1, zRes0 ); if ( zRes == NULL ) { Cudd_RecursiveDerefZdd(dd, zRes0); Cudd_RecursiveDerefZdd(dd, zRes1); return NULL; } cuddDeref( zRes0 ); cuddDeref( zRes1 ); } cuddCacheInsert1( dd, extraBddSpaceEquationsPos, bF, zRes ); return zRes; } } /**Function************************************************************* Synopsis [Performs the recursive step of Extra_bddSpaceEquationsNev().] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ DdNode * extraBddSpaceEquationsNeg( DdManager * dd, DdNode * bF ) { DdNode * zRes; statLine( dd ); if ( bF == b0 ) return z1; if ( bF == b1 ) return z0; if ( (zRes = cuddCacheLookup1Zdd(dd, extraBddSpaceEquationsNeg, bF)) ) return zRes; else { DdNode * bFR, * bF0, * bF1; DdNode * zPos0, * zPos1, * zNeg1; DdNode * zRes, * zRes0, * zRes1; bFR = Cudd_Regular(bF); if ( bFR != bF ) // bF is complemented { bF0 = Cudd_Not( cuddE(bFR) ); bF1 = Cudd_Not( cuddT(bFR) ); } else { bF0 = cuddE(bFR); bF1 = cuddT(bFR); } if ( bF0 == b0 ) { zRes = extraBddSpaceEquationsNeg( dd, bF1 ); if ( zRes == NULL ) return NULL; } else if ( bF1 == b0 ) { zRes0 = extraBddSpaceEquationsNeg( dd, bF0 ); if ( zRes0 == NULL ) return NULL; cuddRef( zRes0 ); // add the current element to the set zRes = cuddZddGetNode( dd, 2*bFR->index, z1, zRes0 ); if ( zRes == NULL ) { Cudd_RecursiveDerefZdd(dd, zRes0); return NULL; } cuddDeref( zRes0 ); } else { zPos0 = extraBddSpaceEquationsNeg( dd, bF0 ); if ( zPos0 == NULL ) return NULL; cuddRef( zPos0 ); zPos1 = extraBddSpaceEquationsNeg( dd, bF1 ); if ( zPos1 == NULL ) { Cudd_RecursiveDerefZdd(dd, zPos0); return NULL; } cuddRef( zPos1 ); zNeg1 = extraBddSpaceEquationsPos( dd, bF1 ); if ( zNeg1 == NULL ) { Cudd_RecursiveDerefZdd(dd, zPos0); Cudd_RecursiveDerefZdd(dd, zPos1); return NULL; } cuddRef( zNeg1 ); zRes0 = cuddZddIntersect( dd, zPos0, zPos1 ); if ( zRes0 == NULL ) { Cudd_RecursiveDerefZdd(dd, zNeg1); Cudd_RecursiveDerefZdd(dd, zPos0); Cudd_RecursiveDerefZdd(dd, zPos1); return NULL; } cuddRef( zRes0 ); zRes1 = cuddZddIntersect( dd, zPos0, zNeg1 ); if ( zRes1 == NULL ) { Cudd_RecursiveDerefZdd(dd, zRes0); Cudd_RecursiveDerefZdd(dd, zNeg1); Cudd_RecursiveDerefZdd(dd, zPos0); Cudd_RecursiveDerefZdd(dd, zPos1); return NULL; } cuddRef( zRes1 ); Cudd_RecursiveDerefZdd(dd, zNeg1); Cudd_RecursiveDerefZdd(dd, zPos0); Cudd_RecursiveDerefZdd(dd, zPos1); // only zRes0 and zRes1 are refed at this point zRes = cuddZddGetNode( dd, 2*bFR->index, zRes1, zRes0 ); if ( zRes == NULL ) { Cudd_RecursiveDerefZdd(dd, zRes0); Cudd_RecursiveDerefZdd(dd, zRes1); return NULL; } cuddDeref( zRes0 ); cuddDeref( zRes1 ); } cuddCacheInsert1( dd, extraBddSpaceEquationsNeg, bF, zRes ); return zRes; } } /**Function************************************************************* Synopsis [Performs the recursive step of Extra_bddSpaceFromFunctionPos().] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ DdNode * extraBddSpaceFromMatrixPos( DdManager * dd, DdNode * zA ) { DdNode * bRes; statLine( dd ); if ( zA == z0 ) return b1; if ( zA == z1 ) return b1; if ( (bRes = cuddCacheLookup1(dd, extraBddSpaceFromMatrixPos, zA)) ) return bRes; else { DdNode * bP0, * bP1; DdNode * bN0, * bN1; DdNode * bRes0, * bRes1; bP0 = extraBddSpaceFromMatrixPos( dd, cuddE(zA) ); if ( bP0 == NULL ) return NULL; cuddRef( bP0 ); bP1 = extraBddSpaceFromMatrixPos( dd, cuddT(zA) ); if ( bP1 == NULL ) { Cudd_RecursiveDeref( dd, bP0 ); return NULL; } cuddRef( bP1 ); bRes0 = cuddBddAndRecur( dd, bP0, bP1 ); if ( bRes0 == NULL ) { Cudd_RecursiveDeref( dd, bP0 ); Cudd_RecursiveDeref( dd, bP1 ); return NULL; } cuddRef( bRes0 ); Cudd_RecursiveDeref( dd, bP0 ); Cudd_RecursiveDeref( dd, bP1 ); bN0 = extraBddSpaceFromMatrixPos( dd, cuddE(zA) ); if ( bN0 == NULL ) { Cudd_RecursiveDeref( dd, bRes0 ); return NULL; } cuddRef( bN0 ); bN1 = extraBddSpaceFromMatrixNeg( dd, cuddT(zA) ); if ( bN1 == NULL ) { Cudd_RecursiveDeref( dd, bRes0 ); Cudd_RecursiveDeref( dd, bN0 ); return NULL; } cuddRef( bN1 ); bRes1 = cuddBddAndRecur( dd, bN0, bN1 ); if ( bRes1 == NULL ) { Cudd_RecursiveDeref( dd, bRes0 ); Cudd_RecursiveDeref( dd, bN0 ); Cudd_RecursiveDeref( dd, bN1 ); return NULL; } cuddRef( bRes1 ); Cudd_RecursiveDeref( dd, bN0 ); Cudd_RecursiveDeref( dd, bN1 ); // consider the case when Res0 and Res1 are the same node if ( bRes0 == bRes1 ) bRes = bRes1; // consider the case when Res1 is complemented else if ( Cudd_IsComplement(bRes1) ) { bRes = cuddUniqueInter( dd, zA->index/2, Cudd_Not(bRes1), Cudd_Not(bRes0) ); if ( bRes == NULL ) { Cudd_RecursiveDeref(dd,bRes0); Cudd_RecursiveDeref(dd,bRes1); return NULL; } bRes = Cudd_Not(bRes); } else { bRes = cuddUniqueInter( dd, zA->index/2, bRes1, bRes0 ); if ( bRes == NULL ) { Cudd_RecursiveDeref(dd,bRes0); Cudd_RecursiveDeref(dd,bRes1); return NULL; } } cuddDeref( bRes0 ); cuddDeref( bRes1 ); cuddCacheInsert1( dd, extraBddSpaceFromMatrixPos, zA, bRes ); return bRes; } } /**Function************************************************************* Synopsis [Performs the recursive step of Extra_bddSpaceFromFunctionPos().] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ DdNode * extraBddSpaceFromMatrixNeg( DdManager * dd, DdNode * zA ) { DdNode * bRes; statLine( dd ); if ( zA == z0 ) return b1; if ( zA == z1 ) return b0; if ( (bRes = cuddCacheLookup1(dd, extraBddSpaceFromMatrixNeg, zA)) ) return bRes; else { DdNode * bP0, * bP1; DdNode * bN0, * bN1; DdNode * bRes0, * bRes1; bP0 = extraBddSpaceFromMatrixNeg( dd, cuddE(zA) ); if ( bP0 == NULL ) return NULL; cuddRef( bP0 ); bP1 = extraBddSpaceFromMatrixNeg( dd, cuddT(zA) ); if ( bP1 == NULL ) { Cudd_RecursiveDeref( dd, bP0 ); return NULL; } cuddRef( bP1 ); bRes0 = cuddBddAndRecur( dd, bP0, bP1 ); if ( bRes0 == NULL ) { Cudd_RecursiveDeref( dd, bP0 ); Cudd_RecursiveDeref( dd, bP1 ); return NULL; } cuddRef( bRes0 ); Cudd_RecursiveDeref( dd, bP0 ); Cudd_RecursiveDeref( dd, bP1 ); bN0 = extraBddSpaceFromMatrixNeg( dd, cuddE(zA) ); if ( bN0 == NULL ) { Cudd_RecursiveDeref( dd, bRes0 ); return NULL; } cuddRef( bN0 ); bN1 = extraBddSpaceFromMatrixPos( dd, cuddT(zA) ); if ( bN1 == NULL ) { Cudd_RecursiveDeref( dd, bRes0 ); Cudd_RecursiveDeref( dd, bN0 ); return NULL; } cuddRef( bN1 ); bRes1 = cuddBddAndRecur( dd, bN0, bN1 ); if ( bRes1 == NULL ) { Cudd_RecursiveDeref( dd, bRes0 ); Cudd_RecursiveDeref( dd, bN0 ); Cudd_RecursiveDeref( dd, bN1 ); return NULL; } cuddRef( bRes1 ); Cudd_RecursiveDeref( dd, bN0 ); Cudd_RecursiveDeref( dd, bN1 ); // consider the case when Res0 and Res1 are the same node if ( bRes0 == bRes1 ) bRes = bRes1; // consider the case when Res1 is complemented else if ( Cudd_IsComplement(bRes1) ) { bRes = cuddUniqueInter( dd, zA->index/2, Cudd_Not(bRes1), Cudd_Not(bRes0) ); if ( bRes == NULL ) { Cudd_RecursiveDeref(dd,bRes0); Cudd_RecursiveDeref(dd,bRes1); return NULL; } bRes = Cudd_Not(bRes); } else { bRes = cuddUniqueInter( dd, zA->index/2, bRes1, bRes0 ); if ( bRes == NULL ) { Cudd_RecursiveDeref(dd,bRes0); Cudd_RecursiveDeref(dd,bRes1); return NULL; } } cuddDeref( bRes0 ); cuddDeref( bRes1 ); cuddCacheInsert1( dd, extraBddSpaceFromMatrixNeg, zA, bRes ); return bRes; } } /*---------------------------------------------------------------------------*/ /* Definition of static functions */ /*---------------------------------------------------------------------------*/ ABC_NAMESPACE_IMPL_END