diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2006-02-11 08:01:00 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2006-02-11 08:01:00 -0800 |
commit | 77d7377442c28fd5c65144d7ea23938600967b2b (patch) | |
tree | dad44cc2d4bad07bf91c47c889c8c8c46ef13006 /src/misc/extra/extraBddAuto.c | |
parent | c0ef1f469a3204adbd26edec0b9d3af56532d794 (diff) | |
download | abc-77d7377442c28fd5c65144d7ea23938600967b2b.tar.gz abc-77d7377442c28fd5c65144d7ea23938600967b2b.tar.bz2 abc-77d7377442c28fd5c65144d7ea23938600967b2b.zip |
Version abc60211
Diffstat (limited to 'src/misc/extra/extraBddAuto.c')
-rw-r--r-- | src/misc/extra/extraBddAuto.c | 1558 |
1 files changed, 1558 insertions, 0 deletions
diff --git a/src/misc/extra/extraBddAuto.c b/src/misc/extra/extraBddAuto.c new file mode 100644 index 00000000..21a969ba --- /dev/null +++ b/src/misc/extra/extraBddAuto.c @@ -0,0 +1,1558 @@ +/**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 "extra.h" + +/*---------------------------------------------------------------------------*/ +/* 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 = 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 ); + free( pSupport ); + return NULL; + } + + // create the permutation arrays + pPermute = ALLOC( int, dd->size ); + pPermuteBack = ALLOC( int, dd->size ); + pCompose = 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] ); + free( pPermute ); + free( pPermuteBack ); + free( pCompose ); + 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 = ALLOC( int, ddMax(dd->size,dd->sizeZ) ); + Extra_SupportArray( dd, bFuncRed, pVarsNonCan ); + + // allocate storage for the EXOR sets + pzRes = 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 ); + + 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)bF > (unsigned)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 */ +/*---------------------------------------------------------------------------*/ + |