From 4d30a1e4f1edecff86d5066ce4653a370e59e5e1 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 30 Jan 2008 08:01:00 -0800 Subject: Version abc80130 --- src/misc/extra/extraBddAuto.c | 1558 ----------------------------------------- 1 file changed, 1558 deletions(-) delete mode 100644 src/misc/extra/extraBddAuto.c (limited to 'src/misc/extra/extraBddAuto.c') diff --git a/src/misc/extra/extraBddAuto.c b/src/misc/extra/extraBddAuto.c deleted file mode 100644 index 21a969ba..00000000 --- a/src/misc/extra/extraBddAuto.c +++ /dev/null @@ -1,1558 +0,0 @@ -/**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 */ -/*---------------------------------------------------------------------------*/ - -- cgit v1.2.3