diff options
Diffstat (limited to 'src/misc/extra/extraBddMisc.c')
| -rw-r--r-- | src/misc/extra/extraBddMisc.c | 2342 |
1 files changed, 0 insertions, 2342 deletions
diff --git a/src/misc/extra/extraBddMisc.c b/src/misc/extra/extraBddMisc.c deleted file mode 100644 index a2ba4036..00000000 --- a/src/misc/extra/extraBddMisc.c +++ /dev/null @@ -1,2342 +0,0 @@ -/**CFile**************************************************************** - - FileName [extraBddMisc.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [extra] - - Synopsis [DD-based utilities.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: extraBddMisc.c,v 1.4 2005/10/04 00:19:54 alanmi Exp $] - -***********************************************************************/ - -#include "extraBdd.h" - -ABC_NAMESPACE_IMPL_START - - -/*---------------------------------------------------------------------------*/ -/* Constant declarations */ -/*---------------------------------------------------------------------------*/ - -/*---------------------------------------------------------------------------*/ -/* Stucture declarations */ -/*---------------------------------------------------------------------------*/ - -/*---------------------------------------------------------------------------*/ -/* Type declarations */ -/*---------------------------------------------------------------------------*/ - -/*---------------------------------------------------------------------------*/ -/* Variable declarations */ -/*---------------------------------------------------------------------------*/ - -/*---------------------------------------------------------------------------*/ -/* Macro declarations */ -/*---------------------------------------------------------------------------*/ - - -/**AutomaticStart*************************************************************/ - -/*---------------------------------------------------------------------------*/ -/* Static function prototypes */ -/*---------------------------------------------------------------------------*/ - -// file "extraDdTransfer.c" -static DdNode * extraTransferPermuteRecur( DdManager * ddS, DdManager * ddD, DdNode * f, st__table * table, int * Permute ); -static DdNode * extraTransferPermute( DdManager * ddS, DdManager * ddD, DdNode * f, int * Permute ); -static DdNode * cuddBddPermuteRecur ARGS( ( DdManager * manager, DdHashTable * table, DdNode * node, int *permut ) ); - -static DdNode * extraBddAndPermute( DdHashTable * table, DdManager * ddF, DdNode * bF, DdManager * ddG, DdNode * bG, int * pPermute ); - -// file "cuddUtils.c" -static void ddSupportStep(DdNode *f, int *support); -static void ddClearFlag(DdNode *f); - -static DdNode* extraZddPrimes( DdManager *dd, DdNode* F ); - -/**AutomaticEnd***************************************************************/ - -/*---------------------------------------------------------------------------*/ -/* Definition of exported functions */ -/*---------------------------------------------------------------------------*/ - -/**Function******************************************************************** - - Synopsis [Convert a {A,B}DD from a manager to another with variable remapping.] - - Description [Convert a {A,B}DD from a manager to another one. The orders of the - variables in the two managers may be different. Returns a - pointer to the {A,B}DD in the destination manager if successful; NULL - otherwise. The i-th entry in the array Permute tells what is the index - of the i-th variable from the old manager in the new manager.] - - SideEffects [None] - - SeeAlso [] - -******************************************************************************/ -DdNode * Extra_TransferPermute( DdManager * ddSource, DdManager * ddDestination, DdNode * f, int * Permute ) -{ - DdNode * bRes; - do - { - ddDestination->reordered = 0; - bRes = extraTransferPermute( ddSource, ddDestination, f, Permute ); - } - while ( ddDestination->reordered == 1 ); - return ( bRes ); - -} /* end of Extra_TransferPermute */ - -/**Function******************************************************************** - - Synopsis [Transfers the BDD from one manager into another level by level.] - - Description [Transfers the BDD from one manager into another while - preserving the correspondence between variables level by level.] - - SideEffects [None] - - SeeAlso [] - -******************************************************************************/ -DdNode * Extra_TransferLevelByLevel( DdManager * ddSource, DdManager * ddDestination, DdNode * f ) -{ - DdNode * bRes; - int * pPermute; - int nMin, nMax, i; - - nMin = ddMin(ddSource->size, ddDestination->size); - nMax = ddMax(ddSource->size, ddDestination->size); - pPermute = ABC_ALLOC( int, nMax ); - // set up the variable permutation - for ( i = 0; i < nMin; i++ ) - pPermute[ ddSource->invperm[i] ] = ddDestination->invperm[i]; - if ( ddSource->size > ddDestination->size ) - { - for ( ; i < nMax; i++ ) - pPermute[ ddSource->invperm[i] ] = -1; - } - bRes = Extra_TransferPermute( ddSource, ddDestination, f, pPermute ); - ABC_FREE( pPermute ); - return bRes; -} - -/**Function******************************************************************** - - Synopsis [Remaps the function to depend on the topmost variables on the manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -******************************************************************************/ -DdNode * Extra_bddRemapUp( - DdManager * dd, - DdNode * bF ) -{ - int * pPermute; - DdNode * bSupp, * bTemp, * bRes; - int Counter; - - pPermute = ABC_ALLOC( int, dd->size ); - - // get support - bSupp = Cudd_Support( dd, bF ); Cudd_Ref( bSupp ); - - // create the variable map - // to remap the DD into the upper part of the manager - Counter = 0; - for ( bTemp = bSupp; bTemp != dd->one; bTemp = cuddT(bTemp) ) - pPermute[bTemp->index] = dd->invperm[Counter++]; - - // transfer the BDD and remap it - bRes = Cudd_bddPermute( dd, bF, pPermute ); Cudd_Ref( bRes ); - - // remove support - Cudd_RecursiveDeref( dd, bSupp ); - - // return - Cudd_Deref( bRes ); - ABC_FREE( pPermute ); - return bRes; -} - -/**Function******************************************************************** - - Synopsis [Moves the BDD by the given number of variables up or down.] - - Description [] - - SideEffects [] - - SeeAlso [Extra_bddShift] - -******************************************************************************/ -DdNode * Extra_bddMove( - DdManager * dd, /* the DD manager */ - DdNode * bF, - int nVars) -{ - DdNode * res; - DdNode * bVars; - if ( nVars == 0 ) - return bF; - if ( Cudd_IsConstant(bF) ) - return bF; - assert( nVars <= dd->size ); - if ( nVars > 0 ) - bVars = dd->vars[nVars]; - else - bVars = Cudd_Not(dd->vars[-nVars]); - - do { - dd->reordered = 0; - res = extraBddMove( dd, bF, bVars ); - } while (dd->reordered == 1); - return(res); - -} /* end of Extra_bddMove */ - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Extra_StopManager( DdManager * dd ) -{ - int RetValue; - // check for remaining references in the package - RetValue = Cudd_CheckZeroRef( dd ); - if ( RetValue > 10 ) -// if ( RetValue ) - printf( "\nThe number of referenced nodes = %d\n\n", RetValue ); -// Cudd_PrintInfo( dd, stdout ); - Cudd_Quit( dd ); -} - -/**Function******************************************************************** - - Synopsis [Outputs the BDD in a readable format.] - - Description [] - - SideEffects [None] - - SeeAlso [] - -******************************************************************************/ -void Extra_bddPrint( DdManager * dd, DdNode * F ) -{ - DdGen * Gen; - int * Cube; - CUDD_VALUE_TYPE Value; - int nVars = dd->size; - int fFirstCube = 1; - int i; - - if ( F == NULL ) - { - printf("NULL"); - return; - } - if ( F == b0 ) - { - printf("Constant 0"); - return; - } - if ( F == b1 ) - { - printf("Constant 1"); - return; - } - - Cudd_ForeachCube( dd, F, Gen, Cube, Value ) - { - if ( fFirstCube ) - fFirstCube = 0; - else -// Output << " + "; - printf( " + " ); - - for ( i = 0; i < nVars; i++ ) - if ( Cube[i] == 0 ) - printf( "[%d]'", i ); -// printf( "%c'", (char)('a'+i) ); - else if ( Cube[i] == 1 ) - printf( "[%d]", i ); -// printf( "%c", (char)('a'+i) ); - } - -// printf("\n"); -} - -/**Function******************************************************************** - - Synopsis [Outputs the BDD in a readable format.] - - Description [] - - SideEffects [None] - - SeeAlso [] - -******************************************************************************/ -void Extra_bddPrintSupport( DdManager * dd, DdNode * F ) -{ - DdNode * bSupp; - bSupp = Cudd_Support( dd, F ); Cudd_Ref( bSupp ); - Extra_bddPrint( dd, bSupp ); - Cudd_RecursiveDeref( dd, bSupp ); -} - -/**Function******************************************************************** - - Synopsis [Returns the size of the support.] - - Description [] - - SideEffects [] - - SeeAlso [] - -******************************************************************************/ -int Extra_bddSuppSize( DdManager * dd, DdNode * bSupp ) -{ - int Counter = 0; - while ( bSupp != b1 ) - { - assert( !Cudd_IsComplement(bSupp) ); - assert( cuddE(bSupp) == b0 ); - - bSupp = cuddT(bSupp); - Counter++; - } - return Counter; -} - -/**Function******************************************************************** - - Synopsis [Returns 1 if the support contains the given BDD variable.] - - Description [] - - SideEffects [] - - SeeAlso [] - -******************************************************************************/ -int Extra_bddSuppContainVar( DdManager * dd, DdNode * bS, DdNode * bVar ) -{ - for( ; bS != b1; bS = cuddT(bS) ) - if ( bS->index == bVar->index ) - return 1; - return 0; -} - -/**Function******************************************************************** - - Synopsis [Returns 1 if two supports represented as BDD cubes are overlapping.] - - Description [] - - SideEffects [] - - SeeAlso [] - -******************************************************************************/ -int Extra_bddSuppOverlapping( DdManager * dd, DdNode * S1, DdNode * S2 ) -{ - while ( S1->index != CUDD_CONST_INDEX && S2->index != CUDD_CONST_INDEX ) - { - // if the top vars are the same, they intersect - if ( S1->index == S2->index ) - return 1; - // if the top vars are different, skip the one, which is higher - if ( dd->perm[S1->index] < dd->perm[S2->index] ) - S1 = cuddT(S1); - else - S2 = cuddT(S2); - } - return 0; -} - -/**Function******************************************************************** - - Synopsis [Returns the number of different vars in two supports.] - - Description [Counts the number of variables that appear in one support and - does not appear in other support. If the number exceeds DiffMax, returns DiffMax.] - - SideEffects [] - - SeeAlso [] - -******************************************************************************/ -int Extra_bddSuppDifferentVars( DdManager * dd, DdNode * S1, DdNode * S2, int DiffMax ) -{ - int Result = 0; - while ( S1->index != CUDD_CONST_INDEX && S2->index != CUDD_CONST_INDEX ) - { - // if the top vars are the same, this var is the same - if ( S1->index == S2->index ) - { - S1 = cuddT(S1); - S2 = cuddT(S2); - continue; - } - // the top var is different - Result++; - - if ( Result >= DiffMax ) - return DiffMax; - - // if the top vars are different, skip the one, which is higher - if ( dd->perm[S1->index] < dd->perm[S2->index] ) - S1 = cuddT(S1); - else - S2 = cuddT(S2); - } - - // consider the remaining variables - if ( S1->index != CUDD_CONST_INDEX ) - Result += Extra_bddSuppSize(dd,S1); - else if ( S2->index != CUDD_CONST_INDEX ) - Result += Extra_bddSuppSize(dd,S2); - - if ( Result >= DiffMax ) - return DiffMax; - return Result; -} - - -/**Function******************************************************************** - - Synopsis [Checks the support containment.] - - Description [This function returns 1 if one support is contained in another. - In this case, bLarge (bSmall) is assigned to point to the larger (smaller) support. - If the supports are identical, return 0 and does not assign the supports!] - - SideEffects [] - - SeeAlso [] - -******************************************************************************/ -int Extra_bddSuppCheckContainment( DdManager * dd, DdNode * bL, DdNode * bH, DdNode ** bLarge, DdNode ** bSmall ) -{ - DdNode * bSL = bL; - DdNode * bSH = bH; - int fLcontainsH = 1; - int fHcontainsL = 1; - int TopVar; - - if ( bSL == bSH ) - return 0; - - while ( bSL != b1 || bSH != b1 ) - { - if ( bSL == b1 ) - { // Low component has no vars; High components has some vars - fLcontainsH = 0; - if ( fHcontainsL == 0 ) - return 0; - else - break; - } - - if ( bSH == b1 ) - { // similarly - fHcontainsL = 0; - if ( fLcontainsH == 0 ) - return 0; - else - break; - } - - // determine the topmost var of the supports by comparing their levels - if ( dd->perm[bSL->index] < dd->perm[bSH->index] ) - TopVar = bSL->index; - else - TopVar = bSH->index; - - if ( TopVar == bSL->index && TopVar == bSH->index ) - { // they are on the same level - // it does not tell us anything about their containment - // skip this var - bSL = cuddT(bSL); - bSH = cuddT(bSH); - } - else if ( TopVar == bSL->index ) // and TopVar != bSH->index - { // Low components is higher and contains more vars - // it is not possible that High component contains Low - fHcontainsL = 0; - // skip this var - bSL = cuddT(bSL); - } - else // if ( TopVar == bSH->index ) // and TopVar != bSL->index - { // similarly - fLcontainsH = 0; - // skip this var - bSH = cuddT(bSH); - } - - // check the stopping condition - if ( !fHcontainsL && !fLcontainsH ) - return 0; - } - // only one of them can be true at the same time - assert( !fHcontainsL || !fLcontainsH ); - if ( fHcontainsL ) - { - *bLarge = bH; - *bSmall = bL; - } - else // fLcontainsH - { - *bLarge = bL; - *bSmall = bH; - } - return 1; -} - - -/**Function******************************************************************** - - Synopsis [Finds variables on which the DD depends and returns them as am array.] - - Description [Finds the variables on which the DD depends. Returns an array - with entries set to 1 for those variables that belong to the support; - NULL otherwise. The array is allocated by the user and should have at least - as many entries as the maximum number of variables in BDD and ZDD parts of - the manager.] - - SideEffects [None] - - SeeAlso [Cudd_Support Cudd_VectorSupport Cudd_ClassifySupport] - -******************************************************************************/ -int * -Extra_SupportArray( - DdManager * dd, /* manager */ - DdNode * f, /* DD whose support is sought */ - int * support ) /* array allocated by the user */ -{ - int i, size; - - /* Initialize support array for ddSupportStep. */ - size = ddMax(dd->size, dd->sizeZ); - for (i = 0; i < size; i++) - support[i] = 0; - - /* Compute support and clean up markers. */ - ddSupportStep(Cudd_Regular(f),support); - ddClearFlag(Cudd_Regular(f)); - - return(support); - -} /* end of Extra_SupportArray */ - -/**Function******************************************************************** - - Synopsis [Finds the variables on which a set of DDs depends.] - - Description [Finds the variables on which a set of DDs depends. - The set must contain either BDDs and ADDs, or ZDDs. - Returns a BDD consisting of the product of the variables if - successful; NULL otherwise.] - - SideEffects [None] - - SeeAlso [Cudd_Support Cudd_ClassifySupport] - -******************************************************************************/ -int * -Extra_VectorSupportArray( - DdManager * dd, /* manager */ - DdNode ** F, /* array of DDs whose support is sought */ - int n, /* size of the array */ - int * support ) /* array allocated by the user */ -{ - int i, size; - - /* Allocate and initialize support array for ddSupportStep. */ - size = ddMax( dd->size, dd->sizeZ ); - for ( i = 0; i < size; i++ ) - support[i] = 0; - - /* Compute support and clean up markers. */ - for ( i = 0; i < n; i++ ) - ddSupportStep( Cudd_Regular(F[i]), support ); - for ( i = 0; i < n; i++ ) - ddClearFlag( Cudd_Regular(F[i]) ); - - return support; -} - -/**Function******************************************************************** - - Synopsis [Find any cube belonging to the on-set of the function.] - - Description [] - - SideEffects [] - - SeeAlso [] - -******************************************************************************/ -DdNode * Extra_bddFindOneCube( DdManager * dd, DdNode * bF ) -{ - char * s_Temp; - DdNode * bCube, * bTemp; - int v; - - // get the vector of variables in the cube - s_Temp = ABC_ALLOC( char, dd->size ); - Cudd_bddPickOneCube( dd, bF, s_Temp ); - - // start the cube - bCube = b1; Cudd_Ref( bCube ); - for ( v = 0; v < dd->size; v++ ) - if ( s_Temp[v] == 0 ) - { -// Cube &= !s_XVars[v]; - bCube = Cudd_bddAnd( dd, bTemp = bCube, Cudd_Not(dd->vars[v]) ); Cudd_Ref( bCube ); - Cudd_RecursiveDeref( dd, bTemp ); - } - else if ( s_Temp[v] == 1 ) - { -// Cube &= s_XVars[v]; - bCube = Cudd_bddAnd( dd, bTemp = bCube, dd->vars[v] ); Cudd_Ref( bCube ); - Cudd_RecursiveDeref( dd, bTemp ); - } - Cudd_Deref(bCube); - ABC_FREE( s_Temp ); - return bCube; -} - -/**Function******************************************************************** - - Synopsis [Returns one cube contained in the given BDD.] - - Description [This function returns the cube with the smallest - bits-to-integer value.] - - SideEffects [] - -******************************************************************************/ -DdNode * Extra_bddGetOneCube( DdManager * dd, DdNode * bFunc ) -{ - DdNode * bFuncR, * bFunc0, * bFunc1; - DdNode * bRes0, * bRes1, * bRes; - - bFuncR = Cudd_Regular(bFunc); - if ( cuddIsConstant(bFuncR) ) - return bFunc; - - // cofactor - if ( Cudd_IsComplement(bFunc) ) - { - bFunc0 = Cudd_Not( cuddE(bFuncR) ); - bFunc1 = Cudd_Not( cuddT(bFuncR) ); - } - else - { - bFunc0 = cuddE(bFuncR); - bFunc1 = cuddT(bFuncR); - } - - // try to find the cube with the negative literal - bRes0 = Extra_bddGetOneCube( dd, bFunc0 ); Cudd_Ref( bRes0 ); - - if ( bRes0 != b0 ) - { - bRes = Cudd_bddAnd( dd, bRes0, Cudd_Not(dd->vars[bFuncR->index]) ); Cudd_Ref( bRes ); - Cudd_RecursiveDeref( dd, bRes0 ); - } - else - { - Cudd_RecursiveDeref( dd, bRes0 ); - // try to find the cube with the positive literal - bRes1 = Extra_bddGetOneCube( dd, bFunc1 ); Cudd_Ref( bRes1 ); - assert( bRes1 != b0 ); - bRes = Cudd_bddAnd( dd, bRes1, dd->vars[bFuncR->index] ); Cudd_Ref( bRes ); - Cudd_RecursiveDeref( dd, bRes1 ); - } - - Cudd_Deref( bRes ); - return bRes; -} - -/**Function******************************************************************** - - Synopsis [Performs the reordering-sensitive step of Extra_bddMove().] - - Description [] - - SideEffects [] - - SeeAlso [] - -******************************************************************************/ -DdNode * Extra_bddComputeRangeCube( DdManager * dd, int iStart, int iStop ) -{ - DdNode * bTemp, * bProd; - int i; - assert( iStart <= iStop ); - assert( iStart >= 0 && iStart <= dd->size ); - assert( iStop >= 0 && iStop <= dd->size ); - bProd = b1; Cudd_Ref( bProd ); - for ( i = iStart; i < iStop; i++ ) - { - bProd = Cudd_bddAnd( dd, bTemp = bProd, dd->vars[i] ); Cudd_Ref( bProd ); - Cudd_RecursiveDeref( dd, bTemp ); - } - Cudd_Deref( bProd ); - return bProd; -} - -/**Function******************************************************************** - - Synopsis [Computes the cube of BDD variables corresponding to bits it the bit-code] - - Description [Returns a bdd composed of elementary bdds found in array BddVars[] such - that the bdd vars encode the number Value of bit length CodeWidth (if fMsbFirst is 1, - the most significant bit is encoded with the first bdd variable). If the variables - BddVars are not specified, takes the first CodeWidth variables of the manager] - - SideEffects [] - - SeeAlso [] - -******************************************************************************/ -DdNode * Extra_bddBitsToCube( DdManager * dd, int Code, int CodeWidth, DdNode ** pbVars, int fMsbFirst ) -{ - int z; - DdNode * bTemp, * bVar, * bVarBdd, * bResult; - - bResult = b1; Cudd_Ref( bResult ); - for ( z = 0; z < CodeWidth; z++ ) - { - bVarBdd = (pbVars)? pbVars[z]: dd->vars[z]; - if ( fMsbFirst ) - bVar = Cudd_NotCond( bVarBdd, (Code & (1 << (CodeWidth-1-z)))==0 ); - else - bVar = Cudd_NotCond( bVarBdd, (Code & (1 << (z)))==0 ); - bResult = Cudd_bddAnd( dd, bTemp = bResult, bVar ); Cudd_Ref( bResult ); - Cudd_RecursiveDeref( dd, bTemp ); - } - Cudd_Deref( bResult ); - - return bResult; -} /* end of Extra_bddBitsToCube */ - -/**Function******************************************************************** - - Synopsis [Finds the support as a negative polarity cube.] - - Description [Finds the variables on which a DD depends. Returns a BDD - consisting of the product of the variables in the negative polarity - if successful; NULL otherwise.] - - SideEffects [None] - - SeeAlso [Cudd_VectorSupport Cudd_Support] - -******************************************************************************/ -DdNode * Extra_bddSupportNegativeCube( DdManager * dd, DdNode * f ) -{ - int *support; - DdNode *res, *tmp, *var; - int i, j; - int size; - - /* Allocate and initialize support array for ddSupportStep. */ - size = ddMax( dd->size, dd->sizeZ ); - support = ABC_ALLOC( int, size ); - if ( support == NULL ) - { - dd->errorCode = CUDD_MEMORY_OUT; - return ( NULL ); - } - for ( i = 0; i < size; i++ ) - { - support[i] = 0; - } - - /* Compute support and clean up markers. */ - ddSupportStep( Cudd_Regular( f ), support ); - ddClearFlag( Cudd_Regular( f ) ); - - /* Transform support from array to cube. */ - do - { - dd->reordered = 0; - res = DD_ONE( dd ); - cuddRef( res ); - for ( j = size - 1; j >= 0; j-- ) - { /* for each level bottom-up */ - i = ( j >= dd->size ) ? j : dd->invperm[j]; - if ( support[i] == 1 ) - { - var = cuddUniqueInter( dd, i, dd->one, Cudd_Not( dd->one ) ); - ////////////////////////////////////////////////////////////////// - var = Cudd_Not(var); - ////////////////////////////////////////////////////////////////// - cuddRef( var ); - tmp = cuddBddAndRecur( dd, res, var ); - if ( tmp == NULL ) - { - Cudd_RecursiveDeref( dd, res ); - Cudd_RecursiveDeref( dd, var ); - res = NULL; - break; - } - cuddRef( tmp ); - Cudd_RecursiveDeref( dd, res ); - Cudd_RecursiveDeref( dd, var ); - res = tmp; - } - } - } - while ( dd->reordered == 1 ); - - ABC_FREE( support ); - if ( res != NULL ) - cuddDeref( res ); - return ( res ); - -} /* end of Extra_SupportNeg */ - -/**Function******************************************************************** - - Synopsis [Returns 1 if the BDD is the BDD of elementary variable.] - - Description [] - - SideEffects [] - - SeeAlso [] - -******************************************************************************/ -int Extra_bddIsVar( DdNode * bFunc ) -{ - bFunc = Cudd_Regular( bFunc ); - if ( cuddIsConstant(bFunc) ) - return 0; - return cuddIsConstant( cuddT(bFunc) ) && cuddIsConstant( Cudd_Regular(cuddE(bFunc)) ); -} - -/**Function******************************************************************** - - Synopsis [Creates AND composed of the first nVars of the manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -******************************************************************************/ -DdNode * Extra_bddCreateAnd( DdManager * dd, int nVars ) -{ - DdNode * bFunc, * bTemp; - int i; - bFunc = Cudd_ReadOne(dd); Cudd_Ref( bFunc ); - for ( i = 0; i < nVars; i++ ) - { - bFunc = Cudd_bddAnd( dd, bTemp = bFunc, Cudd_bddIthVar(dd,i) ); Cudd_Ref( bFunc ); - Cudd_RecursiveDeref( dd, bTemp ); - } - Cudd_Deref( bFunc ); - return bFunc; -} - -/**Function******************************************************************** - - Synopsis [Creates OR composed of the first nVars of the manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -******************************************************************************/ -DdNode * Extra_bddCreateOr( DdManager * dd, int nVars ) -{ - DdNode * bFunc, * bTemp; - int i; - bFunc = Cudd_ReadLogicZero(dd); Cudd_Ref( bFunc ); - for ( i = 0; i < nVars; i++ ) - { - bFunc = Cudd_bddOr( dd, bTemp = bFunc, Cudd_bddIthVar(dd,i) ); Cudd_Ref( bFunc ); - Cudd_RecursiveDeref( dd, bTemp ); - } - Cudd_Deref( bFunc ); - return bFunc; -} - -/**Function******************************************************************** - - Synopsis [Creates EXOR composed of the first nVars of the manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -******************************************************************************/ -DdNode * Extra_bddCreateExor( DdManager * dd, int nVars ) -{ - DdNode * bFunc, * bTemp; - int i; - bFunc = Cudd_ReadLogicZero(dd); Cudd_Ref( bFunc ); - for ( i = 0; i < nVars; i++ ) - { - bFunc = Cudd_bddXor( dd, bTemp = bFunc, Cudd_bddIthVar(dd,i) ); Cudd_Ref( bFunc ); - Cudd_RecursiveDeref( dd, bTemp ); - } - Cudd_Deref( bFunc ); - return bFunc; -} - -/**Function******************************************************************** - - Synopsis [Computes the set of primes as a ZDD.] - - Description [] - - SideEffects [] - - SeeAlso [] - -******************************************************************************/ -DdNode * Extra_zddPrimes( DdManager * dd, DdNode * F ) -{ - DdNode *res; - do { - dd->reordered = 0; - res = extraZddPrimes(dd, F); - if ( dd->reordered == 1 ) - printf("\nReordering in Extra_zddPrimes()\n"); - } while (dd->reordered == 1); - return(res); - -} /* end of Extra_zddPrimes */ - -/**Function******************************************************************** - - Synopsis [Permutes the variables of the array of BDDs.] - - Description [Given a permutation in array permut, creates a new BDD - with permuted variables. There should be an entry in array permut - for each variable in the manager. The i-th entry of permut holds the - index of the variable that is to substitute the i-th variable. - The DDs in the resulting array are already referenced.] - - SideEffects [None] - - SeeAlso [Cudd_addPermute Cudd_bddSwapVariables] - -******************************************************************************/ -void Extra_bddPermuteArray( DdManager * manager, DdNode ** bNodesIn, DdNode ** bNodesOut, int nNodes, int *permut ) -{ - DdHashTable *table; - int i, k; - do - { - manager->reordered = 0; - table = cuddHashTableInit( manager, 1, 2 ); - - /* permute the output functions one-by-one */ - for ( i = 0; i < nNodes; i++ ) - { - bNodesOut[i] = cuddBddPermuteRecur( manager, table, bNodesIn[i], permut ); - if ( bNodesOut[i] == NULL ) - { - /* deref the array of the already computed outputs */ - for ( k = 0; k < i; k++ ) - Cudd_RecursiveDeref( manager, bNodesOut[k] ); - break; - } - cuddRef( bNodesOut[i] ); - } - /* Dispose of local cache. */ - cuddHashTableQuit( table ); - } - while ( manager->reordered == 1 ); -} /* end of Extra_bddPermuteArray */ - - -/**Function******************************************************************** - - Synopsis [Computes the positive polarty cube composed of the first vars in the array.] - - Description [] - - SideEffects [] - - SeeAlso [] - -******************************************************************************/ -DdNode * Extra_bddComputeCube( DdManager * dd, DdNode ** bXVars, int nVars ) -{ - DdNode * bRes; - DdNode * bTemp; - int i; - - bRes = b1; Cudd_Ref( bRes ); - for ( i = 0; i < nVars; i++ ) - { - bRes = Cudd_bddAnd( dd, bTemp = bRes, bXVars[i] ); Cudd_Ref( bRes ); - Cudd_RecursiveDeref( dd, bTemp ); - } - - Cudd_Deref( bRes ); - return bRes; -} - -/**Function******************************************************************** - - Synopsis [Changes the polarity of vars listed in the cube.] - - Description [] - - SideEffects [] - - SeeAlso [] - -******************************************************************************/ -DdNode * Extra_bddChangePolarity( - DdManager * dd, /* the DD manager */ - DdNode * bFunc, - DdNode * bVars) -{ - DdNode *res; - do { - dd->reordered = 0; - res = extraBddChangePolarity( dd, bFunc, bVars ); - } while (dd->reordered == 1); - return(res); - -} /* end of Extra_bddChangePolarity */ - - -/**Function************************************************************* - - Synopsis [Checks if the given variable belongs to the cube.] - - Description [Return -1 if the var does not appear in the cube. - Otherwise, returns polarity (0 or 1) of the var in the cube.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Extra_bddVarIsInCube( DdNode * bCube, int iVar ) -{ - DdNode * bCube0, * bCube1; - while ( Cudd_Regular(bCube)->index != CUDD_CONST_INDEX ) - { - bCube0 = Cudd_NotCond( cuddE(Cudd_Regular(bCube)), Cudd_IsComplement(bCube) ); - bCube1 = Cudd_NotCond( cuddT(Cudd_Regular(bCube)), Cudd_IsComplement(bCube) ); - // make sure it is a cube - assert( (Cudd_IsComplement(bCube0) && Cudd_Regular(bCube0)->index == CUDD_CONST_INDEX) || // bCube0 == 0 - (Cudd_IsComplement(bCube1) && Cudd_Regular(bCube1)->index == CUDD_CONST_INDEX) ); // bCube1 == 0 - // quit if it is the last one - if ( Cudd_Regular(bCube)->index == iVar ) - return (int)(Cudd_IsComplement(bCube0) && Cudd_Regular(bCube0)->index == CUDD_CONST_INDEX); - // get the next cube - if ( (Cudd_IsComplement(bCube0) && Cudd_Regular(bCube0)->index == CUDD_CONST_INDEX) ) - bCube = bCube1; - else - bCube = bCube0; - } - return -1; -} - -/**Function************************************************************* - - Synopsis [Computes the AND of two BDD with different orders.] - - Description [Derives the result of Boolean AND of bF and bG in ddF. - The array pPermute gives the mapping of variables of ddG into that of ddF.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -DdNode * Extra_bddAndPermute( DdManager * ddF, DdNode * bF, DdManager * ddG, DdNode * bG, int * pPermute ) -{ - DdHashTable * table; - DdNode * bRes; - do - { - ddF->reordered = 0; - table = cuddHashTableInit( ddF, 2, 256 ); - if (table == NULL) return NULL; - bRes = extraBddAndPermute( table, ddF, bF, ddG, bG, pPermute ); - if ( bRes ) cuddRef( bRes ); - cuddHashTableQuit( table ); - if ( bRes ) cuddDeref( bRes ); -//if ( ddF->reordered == 1 ) -//printf( "Reordering happened\n" ); - } - while ( ddF->reordered == 1 ); -//printf( "|F| =%6d |G| =%6d |H| =%6d |F|*|G| =%9d\n", -// Cudd_DagSize(bF), Cudd_DagSize(bG), Cudd_DagSize(bRes), -// Cudd_DagSize(bF) * Cudd_DagSize(bG) ); - return ( bRes ); -} - -/*---------------------------------------------------------------------------*/ -/* Definition of internal functions */ -/*---------------------------------------------------------------------------*/ - -/**Function******************************************************************** - - Synopsis [Performs the reordering-sensitive step of Extra_bddMove().] - - Description [] - - SideEffects [] - - SeeAlso [] - -******************************************************************************/ -DdNode * extraBddMove( - DdManager * dd, /* the DD manager */ - DdNode * bF, - DdNode * bDist) -{ - DdNode * bRes; - - if ( Cudd_IsConstant(bF) ) - return bF; - - if ( (bRes = cuddCacheLookup2(dd, extraBddMove, bF, bDist)) ) - return bRes; - else - { - DdNode * bRes0, * bRes1; - DdNode * bF0, * bF1; - DdNode * bFR = Cudd_Regular(bF); - int VarNew; - - if ( Cudd_IsComplement(bDist) ) - VarNew = bFR->index - Cudd_Not(bDist)->index; - else - VarNew = bFR->index + bDist->index; - assert( VarNew < dd->size ); - - // cofactor the functions - if ( bFR != bF ) // bFunc is complemented - { - bF0 = Cudd_Not( cuddE(bFR) ); - bF1 = Cudd_Not( cuddT(bFR) ); - } - else - { - bF0 = cuddE(bFR); - bF1 = cuddT(bFR); - } - - bRes0 = extraBddMove( dd, bF0, bDist ); - if ( bRes0 == NULL ) - return NULL; - cuddRef( bRes0 ); - - bRes1 = extraBddMove( dd, bF1, bDist ); - if ( bRes1 == NULL ) - { - Cudd_RecursiveDeref( dd, bRes0 ); - return NULL; - } - cuddRef( bRes1 ); - - /* only bRes0 and bRes1 are referenced at this point */ - bRes = cuddBddIteRecur( dd, dd->vars[VarNew], bRes1, bRes0 ); - if ( bRes == NULL ) - { - Cudd_RecursiveDeref( dd, bRes0 ); - Cudd_RecursiveDeref( dd, bRes1 ); - return NULL; - } - cuddRef( bRes ); - Cudd_RecursiveDeref( dd, bRes0 ); - Cudd_RecursiveDeref( dd, bRes1 ); - - /* insert the result into cache */ - cuddCacheInsert2( dd, extraBddMove, bF, bDist, bRes ); - cuddDeref( bRes ); - return bRes; - } -} /* end of extraBddMove */ - - -/**Function******************************************************************** - - Synopsis [Finds three cofactors of the cover w.r.t. to the topmost variable.] - - Description [Finds three cofactors of the cover w.r.t. to the topmost variable. - Does not check the cover for being a constant. Assumes that ZDD variables encoding - positive and negative polarities are adjacent in the variable order. Is different - from cuddZddGetCofactors3() in that it does not compute the cofactors w.r.t. the - given variable but takes the cofactors with respent to the topmost variable. - This function is more efficient when used in recursive procedures because it does - not require referencing of the resulting cofactors (compare cuddZddProduct() - and extraZddPrimeProduct()).] - - SideEffects [None] - - SeeAlso [cuddZddGetCofactors3] - -******************************************************************************/ -void -extraDecomposeCover( - DdManager* dd, /* the manager */ - DdNode* zC, /* the cover */ - DdNode** zC0, /* the pointer to the negative var cofactor */ - DdNode** zC1, /* the pointer to the positive var cofactor */ - DdNode** zC2 ) /* the pointer to the cofactor without var */ -{ - if ( (zC->index & 1) == 0 ) - { /* the top variable is present in positive polarity and maybe in negative */ - - DdNode *Temp = cuddE( zC ); - *zC1 = cuddT( zC ); - if ( cuddIZ(dd,Temp->index) == cuddIZ(dd,zC->index) + 1 ) - { /* Temp is not a terminal node - * top var is present in negative polarity */ - *zC2 = cuddE( Temp ); - *zC0 = cuddT( Temp ); - } - else - { /* top var is not present in negative polarity */ - *zC2 = Temp; - *zC0 = dd->zero; - } - } - else - { /* the top variable is present only in negative */ - *zC1 = dd->zero; - *zC2 = cuddE( zC ); - *zC0 = cuddT( zC ); - } -} /* extraDecomposeCover */ - - - -/**Function******************************************************************** - - Synopsis [Counts the total number of cubes in the ISOPs of the functions.] - - Description [Returns -1 if the number of cubes exceeds the limit.] - - SideEffects [None] - - SeeAlso [Extra_TransferPermute] - -******************************************************************************/ -static DdNode * extraBddCountCubes( DdManager * dd, DdNode * L, DdNode * U, st__table *table, int * pnCubes, int Limit ) -{ - DdNode *one = DD_ONE(dd); - DdNode *zero = Cudd_Not(one); - int v, top_l, top_u; - DdNode *Lsub0, *Usub0, *Lsub1, *Usub1, *Ld, *Ud; - DdNode *Lsuper0, *Usuper0, *Lsuper1, *Usuper1; - DdNode *Isub0, *Isub1, *Id; - DdNode *x; - DdNode *term0, *term1, *sum; - DdNode *Lv, *Uv, *Lnv, *Unv; - DdNode *r; - int index; - int Count0 = 0, Count1 = 0, Count2 = 0; - - statLine(dd); - if (L == zero) - { - *pnCubes = 0; - return(zero); - } - if (U == one) - { - *pnCubes = 1; - return(one); - } - - /* Check cache */ - r = cuddCacheLookup2(dd, cuddBddIsop, L, U); - if (r) - { - int nCubes = 0; - if ( st__lookup( table, (char *)r, (char **)&nCubes ) ) - *pnCubes = nCubes; - else assert( 0 ); - return r; - } - - top_l = dd->perm[Cudd_Regular(L)->index]; - top_u = dd->perm[Cudd_Regular(U)->index]; - v = ddMin(top_l, top_u); - - /* Compute cofactors */ - if (top_l == v) { - index = Cudd_Regular(L)->index; - Lv = Cudd_T(L); - Lnv = Cudd_E(L); - if (Cudd_IsComplement(L)) { - Lv = Cudd_Not(Lv); - Lnv = Cudd_Not(Lnv); - } - } - else { - index = Cudd_Regular(U)->index; - Lv = Lnv = L; - } - - if (top_u == v) { - Uv = Cudd_T(U); - Unv = Cudd_E(U); - if (Cudd_IsComplement(U)) { - Uv = Cudd_Not(Uv); - Unv = Cudd_Not(Unv); - } - } - else { - Uv = Unv = U; - } - - Lsub0 = cuddBddAndRecur(dd, Lnv, Cudd_Not(Uv)); - if (Lsub0 == NULL) - return(NULL); - Cudd_Ref(Lsub0); - Usub0 = Unv; - Lsub1 = cuddBddAndRecur(dd, Lv, Cudd_Not(Unv)); - if (Lsub1 == NULL) { - Cudd_RecursiveDeref(dd, Lsub0); - return(NULL); - } - Cudd_Ref(Lsub1); - Usub1 = Uv; - - Isub0 = extraBddCountCubes(dd, Lsub0, Usub0, table, &Count0, Limit); - if (Isub0 == NULL) { - Cudd_RecursiveDeref(dd, Lsub0); - Cudd_RecursiveDeref(dd, Lsub1); - return(NULL); - } - Cudd_Ref(Isub0); - Isub1 = extraBddCountCubes(dd, Lsub1, Usub1, table, &Count1, Limit); - if (Isub1 == NULL) { - Cudd_RecursiveDeref(dd, Lsub0); - Cudd_RecursiveDeref(dd, Lsub1); - Cudd_RecursiveDeref(dd, Isub0); - return(NULL); - } - Cudd_Ref(Isub1); - Cudd_RecursiveDeref(dd, Lsub0); - Cudd_RecursiveDeref(dd, Lsub1); - - Lsuper0 = cuddBddAndRecur(dd, Lnv, Cudd_Not(Isub0)); - if (Lsuper0 == NULL) { - Cudd_RecursiveDeref(dd, Isub0); - Cudd_RecursiveDeref(dd, Isub1); - return(NULL); - } - Cudd_Ref(Lsuper0); - Lsuper1 = cuddBddAndRecur(dd, Lv, Cudd_Not(Isub1)); - if (Lsuper1 == NULL) { - Cudd_RecursiveDeref(dd, Isub0); - Cudd_RecursiveDeref(dd, Isub1); - Cudd_RecursiveDeref(dd, Lsuper0); - return(NULL); - } - Cudd_Ref(Lsuper1); - Usuper0 = Unv; - Usuper1 = Uv; - - /* Ld = Lsuper0 + Lsuper1 */ - Ld = cuddBddAndRecur(dd, Cudd_Not(Lsuper0), Cudd_Not(Lsuper1)); - Ld = Cudd_NotCond(Ld, Ld != NULL); - if (Ld == NULL) { - Cudd_RecursiveDeref(dd, Isub0); - Cudd_RecursiveDeref(dd, Isub1); - Cudd_RecursiveDeref(dd, Lsuper0); - Cudd_RecursiveDeref(dd, Lsuper1); - return(NULL); - } - Cudd_Ref(Ld); - Ud = cuddBddAndRecur(dd, Usuper0, Usuper1); - if (Ud == NULL) { - Cudd_RecursiveDeref(dd, Isub0); - Cudd_RecursiveDeref(dd, Isub1); - Cudd_RecursiveDeref(dd, Lsuper0); - Cudd_RecursiveDeref(dd, Lsuper1); - Cudd_RecursiveDeref(dd, Ld); - return(NULL); - } - Cudd_Ref(Ud); - Cudd_RecursiveDeref(dd, Lsuper0); - Cudd_RecursiveDeref(dd, Lsuper1); - - Id = extraBddCountCubes(dd, Ld, Ud, table, &Count2, Limit); - if (Id == NULL) { - Cudd_RecursiveDeref(dd, Isub0); - Cudd_RecursiveDeref(dd, Isub1); - Cudd_RecursiveDeref(dd, Ld); - Cudd_RecursiveDeref(dd, Ud); - return(NULL); - } - Cudd_Ref(Id); - Cudd_RecursiveDeref(dd, Ld); - Cudd_RecursiveDeref(dd, Ud); - - x = cuddUniqueInter(dd, index, one, zero); - if (x == NULL) { - Cudd_RecursiveDeref(dd, Isub0); - Cudd_RecursiveDeref(dd, Isub1); - Cudd_RecursiveDeref(dd, Id); - return(NULL); - } - Cudd_Ref(x); - term0 = cuddBddAndRecur(dd, Cudd_Not(x), Isub0); - if (term0 == NULL) { - Cudd_RecursiveDeref(dd, Isub0); - Cudd_RecursiveDeref(dd, Isub1); - Cudd_RecursiveDeref(dd, Id); - Cudd_RecursiveDeref(dd, x); - return(NULL); - } - Cudd_Ref(term0); - Cudd_RecursiveDeref(dd, Isub0); - term1 = cuddBddAndRecur(dd, x, Isub1); - if (term1 == NULL) { - Cudd_RecursiveDeref(dd, Isub1); - Cudd_RecursiveDeref(dd, Id); - Cudd_RecursiveDeref(dd, x); - Cudd_RecursiveDeref(dd, term0); - return(NULL); - } - Cudd_Ref(term1); - Cudd_RecursiveDeref(dd, x); - Cudd_RecursiveDeref(dd, Isub1); - /* sum = term0 + term1 */ - sum = cuddBddAndRecur(dd, Cudd_Not(term0), Cudd_Not(term1)); - sum = Cudd_NotCond(sum, sum != NULL); - if (sum == NULL) { - Cudd_RecursiveDeref(dd, Id); - Cudd_RecursiveDeref(dd, term0); - Cudd_RecursiveDeref(dd, term1); - return(NULL); - } - Cudd_Ref(sum); - Cudd_RecursiveDeref(dd, term0); - Cudd_RecursiveDeref(dd, term1); - /* r = sum + Id */ - r = cuddBddAndRecur(dd, Cudd_Not(sum), Cudd_Not(Id)); - r = Cudd_NotCond(r, r != NULL); - if (r == NULL) { - Cudd_RecursiveDeref(dd, Id); - Cudd_RecursiveDeref(dd, sum); - return(NULL); - } - Cudd_Ref(r); - Cudd_RecursiveDeref(dd, sum); - Cudd_RecursiveDeref(dd, Id); - - cuddCacheInsert2(dd, cuddBddIsop, L, U, r); - *pnCubes = Count0 + Count1 + Count2; - if ( st__add_direct( table, (char *)r, (char *)(ABC_PTRINT_T)*pnCubes ) == st__OUT_OF_MEM ) - { - Cudd_RecursiveDeref( dd, r ); - return NULL; - } - if ( *pnCubes > Limit ) - { - Cudd_RecursiveDeref( dd, r ); - return NULL; - } - //printf( "%d ", *pnCubes ); - Cudd_Deref(r); - return r; -} -int Extra_bddCountCubes( DdManager * dd, DdNode ** pFuncs, int nFuncs, int fMode, int nLimit, int * pGuide ) -{ - DdNode * pF0, * pF1; - int i, Count, Count0, Count1, CounterAll = 0; - st__table *table = st__init_table( st__ptrcmp, st__ptrhash ); - unsigned int saveLimit = dd->maxLive; - dd->maxLive = dd->keys - dd->dead + 1000000; // limit on intermediate BDD nodes - for ( i = 0; i < nFuncs; i++ ) - { - if ( !pFuncs[i] ) - continue; - pF1 = pF0 = NULL; - Count0 = Count1 = nLimit; - if ( fMode == -1 || fMode == 1 ) // both or pos - pF1 = extraBddCountCubes( dd, pFuncs[i], pFuncs[i], table, &Count1, nLimit ); - pFuncs[i] = Cudd_Not( pFuncs[i] ); - if ( fMode == -1 || fMode == 0 ) // both or neg - pF0 = extraBddCountCubes( dd, pFuncs[i], pFuncs[i], table, &Count0, Count1 ); - pFuncs[i] = Cudd_Not( pFuncs[i] ); - if ( !pF1 && !pF0 ) - break; - if ( !pF0 ) pGuide[i] = 1, Count = Count1; // use pos - else if ( !pF1 ) pGuide[i] = 0, Count = Count0; // use neg - else if ( Count1 <= Count0 ) pGuide[i] = 1, Count = Count1; // use pos - else pGuide[i] = 0, Count = Count0; // use neg - CounterAll += Count; - //printf( "Output %5d has %5d cubes (%d) (%5d and %5d)\n", nOuts++, Count, pGuide[i], Count1, Count0 ); - } - dd->maxLive = saveLimit; - st__free_table( table ); - return i == nFuncs ? CounterAll : -1; -} /* end of Extra_bddCountCubes */ - -/*---------------------------------------------------------------------------*/ -/* Definition of static Functions */ -/*---------------------------------------------------------------------------*/ - -/**Function******************************************************************** - - Synopsis [Convert a BDD from a manager to another one.] - - Description [Convert a BDD from a manager to another one. Returns a - pointer to the BDD in the destination manager if successful; NULL - otherwise.] - - SideEffects [None] - - SeeAlso [Extra_TransferPermute] - -******************************************************************************/ -DdNode * extraTransferPermute( DdManager * ddS, DdManager * ddD, DdNode * f, int * Permute ) -{ - DdNode *res; - st__table *table = NULL; - st__generator *gen = NULL; - DdNode *key, *value; - - table = st__init_table( st__ptrcmp, st__ptrhash ); - if ( table == NULL ) - goto failure; - res = extraTransferPermuteRecur( ddS, ddD, f, table, Permute ); - if ( res != NULL ) - cuddRef( res ); - - /* Dereference all elements in the table and dispose of the table. - ** This must be done also if res is NULL to avoid leaks in case of - ** reordering. */ - gen = st__init_gen( table ); - if ( gen == NULL ) - goto failure; - while ( st__gen( gen, ( const char ** ) &key, ( char ** ) &value ) ) - { - Cudd_RecursiveDeref( ddD, value ); - } - st__free_gen( gen ); - gen = NULL; - st__free_table( table ); - table = NULL; - - if ( res != NULL ) - cuddDeref( res ); - return ( res ); - - failure: - if ( table != NULL ) - st__free_table( table ); - if ( gen != NULL ) - st__free_gen( gen ); - return ( NULL ); - -} /* end of extraTransferPermute */ - - -/**Function******************************************************************** - - Synopsis [Performs the recursive step of Extra_TransferPermute.] - - Description [Performs the recursive step of Extra_TransferPermute. - Returns a pointer to the result if successful; NULL otherwise.] - - SideEffects [None] - - SeeAlso [extraTransferPermute] - -******************************************************************************/ -static DdNode * -extraTransferPermuteRecur( - DdManager * ddS, - DdManager * ddD, - DdNode * f, - st__table * table, - int * Permute ) -{ - DdNode *ft, *fe, *t, *e, *var, *res; - DdNode *one, *zero; - int index; - int comple = 0; - - statLine( ddD ); - one = DD_ONE( ddD ); - comple = Cudd_IsComplement( f ); - - /* Trivial cases. */ - if ( Cudd_IsConstant( f ) ) - return ( Cudd_NotCond( one, comple ) ); - - - /* Make canonical to increase the utilization of the cache. */ - f = Cudd_NotCond( f, comple ); - /* Now f is a regular pointer to a non-constant node. */ - - /* Check the cache. */ - if ( st__lookup( table, ( char * ) f, ( char ** ) &res ) ) - return ( Cudd_NotCond( res, comple ) ); - - if ( ddS->TimeStop && Abc_Clock() > ddS->TimeStop ) - return NULL; - if ( ddD->TimeStop && Abc_Clock() > ddD->TimeStop ) - return NULL; - - /* Recursive step. */ - if ( Permute ) - index = Permute[f->index]; - else - index = f->index; - - ft = cuddT( f ); - fe = cuddE( f ); - - t = extraTransferPermuteRecur( ddS, ddD, ft, table, Permute ); - if ( t == NULL ) - { - return ( NULL ); - } - cuddRef( t ); - - e = extraTransferPermuteRecur( ddS, ddD, fe, table, Permute ); - if ( e == NULL ) - { - Cudd_RecursiveDeref( ddD, t ); - return ( NULL ); - } - cuddRef( e ); - - zero = Cudd_Not(ddD->one); - var = cuddUniqueInter( ddD, index, one, zero ); - if ( var == NULL ) - { - Cudd_RecursiveDeref( ddD, t ); - Cudd_RecursiveDeref( ddD, e ); - return ( NULL ); - } - res = cuddBddIteRecur( ddD, var, t, e ); - - if ( res == NULL ) - { - Cudd_RecursiveDeref( ddD, t ); - Cudd_RecursiveDeref( ddD, e ); - return ( NULL ); - } - cuddRef( res ); - Cudd_RecursiveDeref( ddD, t ); - Cudd_RecursiveDeref( ddD, e ); - - if ( st__add_direct( table, ( char * ) f, ( char * ) res ) == - st__OUT_OF_MEM ) - { - Cudd_RecursiveDeref( ddD, res ); - return ( NULL ); - } - return ( Cudd_NotCond( res, comple ) ); - -} /* end of extraTransferPermuteRecur */ - -/**Function******************************************************************** - - Synopsis [Performs the recursive step of Cudd_Support.] - - Description [Performs the recursive step of Cudd_Support. Performs a - DFS from f. The support is accumulated in supp as a side effect. Uses - the LSB of the then pointer as visited flag.] - - SideEffects [None] - - SeeAlso [ddClearFlag] - -******************************************************************************/ -static void -ddSupportStep( - DdNode * f, - int * support) -{ - if (cuddIsConstant(f) || Cudd_IsComplement(f->next)) { - return; - } - - support[f->index] = 1; - ddSupportStep(cuddT(f),support); - ddSupportStep(Cudd_Regular(cuddE(f)),support); - /* Mark as visited. */ - f->next = Cudd_Not(f->next); - return; - -} /* end of ddSupportStep */ - - -/**Function******************************************************************** - - Synopsis [Performs a DFS from f, clearing the LSB of the next - pointers.] - - Description [] - - SideEffects [None] - - SeeAlso [ddSupportStep ddDagInt] - -******************************************************************************/ -static void -ddClearFlag( - DdNode * f) -{ - if (!Cudd_IsComplement(f->next)) { - return; - } - /* Clear visited flag. */ - f->next = Cudd_Regular(f->next); - if (cuddIsConstant(f)) { - return; - } - ddClearFlag(cuddT(f)); - ddClearFlag(Cudd_Regular(cuddE(f))); - return; - -} /* end of ddClearFlag */ - - -/**Function******************************************************************** - - Synopsis [Composed three subcovers into one ZDD.] - - Description [] - - SideEffects [None] - - SeeAlso [] - -******************************************************************************/ -DdNode * -extraComposeCover( - DdManager* dd, /* the manager */ - DdNode* zC0, /* the pointer to the negative var cofactor */ - DdNode* zC1, /* the pointer to the positive var cofactor */ - DdNode* zC2, /* the pointer to the cofactor without var */ - int TopVar) /* the index of the positive ZDD var */ -{ - DdNode * zRes, * zTemp; - /* compose with-neg-var and without-var using the neg ZDD var */ - zTemp = cuddZddGetNode( dd, 2*TopVar + 1, zC0, zC2 ); - if ( zTemp == NULL ) - { - Cudd_RecursiveDerefZdd(dd, zC0); - Cudd_RecursiveDerefZdd(dd, zC1); - Cudd_RecursiveDerefZdd(dd, zC2); - return NULL; - } - cuddRef( zTemp ); - cuddDeref( zC0 ); - cuddDeref( zC2 ); - - /* compose with-pos-var and previous result using the pos ZDD var */ - zRes = cuddZddGetNode( dd, 2*TopVar, zC1, zTemp ); - if ( zRes == NULL ) - { - Cudd_RecursiveDerefZdd(dd, zC1); - Cudd_RecursiveDerefZdd(dd, zTemp); - return NULL; - } - cuddDeref( zC1 ); - cuddDeref( zTemp ); - return zRes; -} /* extraComposeCover */ - -/**Function******************************************************************** - - Synopsis [Performs the recursive step of prime computation.] - - Description [] - - SideEffects [] - - SeeAlso [] - -******************************************************************************/ -DdNode* extraZddPrimes( DdManager *dd, DdNode* F ) -{ - DdNode *zRes; - - if ( F == Cudd_Not( dd->one ) ) - return dd->zero; - if ( F == dd->one ) - return dd->one; - - /* check cache */ - zRes = cuddCacheLookup1Zdd(dd, extraZddPrimes, F); - if (zRes) - return(zRes); - { - /* temporary variables */ - DdNode *bF01, *zP0, *zP1; - /* three components of the prime set */ - DdNode *zResE, *zResP, *zResN; - int fIsComp = Cudd_IsComplement( F ); - - /* find cofactors of F */ - DdNode * bF0 = Cudd_NotCond( Cudd_E( F ), fIsComp ); - DdNode * bF1 = Cudd_NotCond( Cudd_T( F ), fIsComp ); - - /* find the intersection of cofactors */ - bF01 = cuddBddAndRecur( dd, bF0, bF1 ); - if ( bF01 == NULL ) return NULL; - cuddRef( bF01 ); - - /* solve the problems for cofactors */ - zP0 = extraZddPrimes( dd, bF0 ); - if ( zP0 == NULL ) - { - Cudd_RecursiveDeref( dd, bF01 ); - return NULL; - } - cuddRef( zP0 ); - - zP1 = extraZddPrimes( dd, bF1 ); - if ( zP1 == NULL ) - { - Cudd_RecursiveDeref( dd, bF01 ); - Cudd_RecursiveDerefZdd( dd, zP0 ); - return NULL; - } - cuddRef( zP1 ); - - /* check for local unateness */ - if ( bF01 == bF0 ) /* unate increasing */ - { - /* intersection is useless */ - cuddDeref( bF01 ); - /* the primes of intersection are the primes of F0 */ - zResE = zP0; - /* there are no primes with negative var */ - zResN = dd->zero; - cuddRef( zResN ); - /* primes with positive var are primes of F1 that are not primes of F01 */ - zResP = cuddZddDiff( dd, zP1, zP0 ); - if ( zResP == NULL ) - { - Cudd_RecursiveDerefZdd( dd, zResE ); - Cudd_RecursiveDerefZdd( dd, zResN ); - Cudd_RecursiveDerefZdd( dd, zP1 ); - return NULL; - } - cuddRef( zResP ); - Cudd_RecursiveDerefZdd( dd, zP1 ); - } - else if ( bF01 == bF1 ) /* unate decreasing */ - { - /* intersection is useless */ - cuddDeref( bF01 ); - /* the primes of intersection are the primes of F1 */ - zResE = zP1; - /* there are no primes with positive var */ - zResP = dd->zero; - cuddRef( zResP ); - /* primes with negative var are primes of F0 that are not primes of F01 */ - zResN = cuddZddDiff( dd, zP0, zP1 ); - if ( zResN == NULL ) - { - Cudd_RecursiveDerefZdd( dd, zResE ); - Cudd_RecursiveDerefZdd( dd, zResP ); - Cudd_RecursiveDerefZdd( dd, zP0 ); - return NULL; - } - cuddRef( zResN ); - Cudd_RecursiveDerefZdd( dd, zP0 ); - } - else /* not unate */ - { - /* primes without the top var are primes of F10 */ - zResE = extraZddPrimes( dd, bF01 ); - if ( zResE == NULL ) - { - Cudd_RecursiveDerefZdd( dd, bF01 ); - Cudd_RecursiveDerefZdd( dd, zP0 ); - Cudd_RecursiveDerefZdd( dd, zP1 ); - return NULL; - } - cuddRef( zResE ); - Cudd_RecursiveDeref( dd, bF01 ); - - /* primes with the negative top var are those of P0 that are not in F10 */ - zResN = cuddZddDiff( dd, zP0, zResE ); - if ( zResN == NULL ) - { - Cudd_RecursiveDerefZdd( dd, zResE ); - Cudd_RecursiveDerefZdd( dd, zP0 ); - Cudd_RecursiveDerefZdd( dd, zP1 ); - return NULL; - } - cuddRef( zResN ); - Cudd_RecursiveDerefZdd( dd, zP0 ); - - /* primes with the positive top var are those of P1 that are not in F10 */ - zResP = cuddZddDiff( dd, zP1, zResE ); - if ( zResP == NULL ) - { - Cudd_RecursiveDerefZdd( dd, zResE ); - Cudd_RecursiveDerefZdd( dd, zResN ); - Cudd_RecursiveDerefZdd( dd, zP1 ); - return NULL; - } - cuddRef( zResP ); - Cudd_RecursiveDerefZdd( dd, zP1 ); - } - - zRes = extraComposeCover( dd, zResN, zResP, zResE, Cudd_Regular(F)->index ); - if ( zRes == NULL ) return NULL; - - /* insert the result into cache */ - cuddCacheInsert1(dd, extraZddPrimes, F, zRes); - return zRes; - } -} /* end of extraZddPrimes */ - -/**Function******************************************************************** - - Synopsis [Implements the recursive step of Cudd_bddPermute.] - - Description [ Recursively puts the BDD in the order given in the array permut. - Checks for trivial cases to terminate recursion, then splits on the - children of this node. Once the solutions for the children are - obtained, it puts into the current position the node from the rest of - the BDD that should be here. Then returns this BDD. - The key here is that the node being visited is NOT put in its proper - place by this instance, but rather is switched when its proper position - is reached in the recursion tree.<p> - The DdNode * that is returned is the same BDD as passed in as node, - but in the new order.] - - SideEffects [None] - - SeeAlso [Cudd_bddPermute cuddAddPermuteRecur] - -******************************************************************************/ -static DdNode * -cuddBddPermuteRecur( DdManager * manager /* DD manager */ , - DdHashTable * table /* computed table */ , - DdNode * node /* BDD to be reordered */ , - int *permut /* permutation array */ ) -{ - DdNode *N, *T, *E; - DdNode *res; - int index; - - statLine( manager ); - N = Cudd_Regular( node ); - - /* Check for terminal case of constant node. */ - if ( cuddIsConstant( N ) ) - { - return ( node ); - } - - /* If problem already solved, look up answer and return. */ - if ( N->ref != 1 && ( res = cuddHashTableLookup1( table, N ) ) != NULL ) - { - return ( Cudd_NotCond( res, N != node ) ); - } - - /* Split and recur on children of this node. */ - T = cuddBddPermuteRecur( manager, table, cuddT( N ), permut ); - if ( T == NULL ) - return ( NULL ); - cuddRef( T ); - E = cuddBddPermuteRecur( manager, table, cuddE( N ), permut ); - if ( E == NULL ) - { - Cudd_IterDerefBdd( manager, T ); - return ( NULL ); - } - cuddRef( E ); - - /* Move variable that should be in this position to this position - ** by retrieving the single var BDD for that variable, and calling - ** cuddBddIteRecur with the T and E we just created. - */ - index = permut[N->index]; - res = cuddBddIteRecur( manager, manager->vars[index], T, E ); - if ( res == NULL ) - { - Cudd_IterDerefBdd( manager, T ); - Cudd_IterDerefBdd( manager, E ); - return ( NULL ); - } - cuddRef( res ); - Cudd_IterDerefBdd( manager, T ); - Cudd_IterDerefBdd( manager, E ); - - /* Do not keep the result if the reference count is only 1, since - ** it will not be visited again. - */ - if ( N->ref != 1 ) - { - ptrint fanout = ( ptrint ) N->ref; - cuddSatDec( fanout ); - if ( !cuddHashTableInsert1( table, N, res, fanout ) ) - { - Cudd_IterDerefBdd( manager, res ); - return ( NULL ); - } - } - cuddDeref( res ); - return ( Cudd_NotCond( res, N != node ) ); - -} /* end of cuddBddPermuteRecur */ - - -/**Function******************************************************************** - - Synopsis [Performs the reordering-sensitive step of Extra_bddChangePolarity().] - - Description [] - - SideEffects [] - - SeeAlso [] - -******************************************************************************/ -DdNode * extraBddChangePolarity( - DdManager * dd, /* the DD manager */ - DdNode * bFunc, - DdNode * bVars) -{ - DdNode * bRes; - - if ( bVars == b1 ) - return bFunc; - if ( Cudd_IsConstant(bFunc) ) - return bFunc; - - if ( (bRes = cuddCacheLookup2(dd, extraBddChangePolarity, bFunc, bVars)) ) - return bRes; - else - { - DdNode * bFR = Cudd_Regular(bFunc); - int LevelF = dd->perm[bFR->index]; - int LevelV = dd->perm[bVars->index]; - - if ( LevelV < LevelF ) - bRes = extraBddChangePolarity( dd, bFunc, cuddT(bVars) ); - else // if ( LevelF <= LevelV ) - { - DdNode * bRes0, * bRes1; - DdNode * bF0, * bF1; - DdNode * bVarsNext; - - // cofactor the functions - if ( bFR != bFunc ) // bFunc is complemented - { - bF0 = Cudd_Not( cuddE(bFR) ); - bF1 = Cudd_Not( cuddT(bFR) ); - } - else - { - bF0 = cuddE(bFR); - bF1 = cuddT(bFR); - } - - if ( LevelF == LevelV ) - bVarsNext = cuddT(bVars); - else - bVarsNext = bVars; - - bRes0 = extraBddChangePolarity( dd, bF0, bVarsNext ); - if ( bRes0 == NULL ) - return NULL; - cuddRef( bRes0 ); - - bRes1 = extraBddChangePolarity( dd, bF1, bVarsNext ); - if ( bRes1 == NULL ) - { - Cudd_RecursiveDeref( dd, bRes0 ); - return NULL; - } - cuddRef( bRes1 ); - - if ( LevelF == LevelV ) - { // swap the cofactors - DdNode * bTemp; - bTemp = bRes0; - bRes0 = bRes1; - bRes1 = bTemp; - } - - /* only aRes0 and aRes1 are referenced at this point */ - - /* 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 ); - } - - /* insert the result into cache */ - cuddCacheInsert2(dd, extraBddChangePolarity, bFunc, bVars, bRes); - return bRes; - } -} /* end of extraBddChangePolarity */ - - - -static int Counter = 0; - -/**Function************************************************************* - - Synopsis [Computes the AND of two BDD with different orders.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -DdNode * extraBddAndPermute( DdHashTable * table, DdManager * ddF, DdNode * bF, DdManager * ddG, DdNode * bG, int * pPermute ) -{ - DdNode * bF0, * bF1, * bG0, * bG1, * bRes0, * bRes1, * bRes, * bVar; - int LevF, LevG, Lev; - - // if F == 0, return 0 - if ( bF == Cudd_Not(ddF->one) ) - return Cudd_Not(ddF->one); - // if G == 0, return 0 - if ( bG == Cudd_Not(ddG->one) ) - return Cudd_Not(ddF->one); - // if G == 1, return F - if ( bG == ddG->one ) - return bF; - // cannot use F == 1, because the var order of G has to be changed - - // check cache - if ( //(Cudd_Regular(bF)->ref != 1 || Cudd_Regular(bG)->ref != 1) && - (bRes = cuddHashTableLookup2(table, bF, bG)) ) - return bRes; - Counter++; - - if ( ddF->TimeStop && Abc_Clock() > ddF->TimeStop ) - return NULL; - if ( ddG->TimeStop && Abc_Clock() > ddG->TimeStop ) - return NULL; - - // find the topmost variable in F and G using var order of F - LevF = cuddI( ddF, Cudd_Regular(bF)->index ); - LevG = cuddI( ddF, pPermute ? pPermute[Cudd_Regular(bG)->index] : Cudd_Regular(bG)->index ); - Lev = Abc_MinInt( LevF, LevG ); - assert( Lev < ddF->size ); - bVar = ddF->vars[ddF->invperm[Lev]]; - - // cofactor - bF0 = (Lev < LevF) ? bF : Cudd_NotCond( cuddE(Cudd_Regular(bF)), Cudd_IsComplement(bF) ); - bF1 = (Lev < LevF) ? bF : Cudd_NotCond( cuddT(Cudd_Regular(bF)), Cudd_IsComplement(bF) ); - bG0 = (Lev < LevG) ? bG : Cudd_NotCond( cuddE(Cudd_Regular(bG)), Cudd_IsComplement(bG) ); - bG1 = (Lev < LevG) ? bG : Cudd_NotCond( cuddT(Cudd_Regular(bG)), Cudd_IsComplement(bG) ); - - // call for cofactors - bRes0 = extraBddAndPermute( table, ddF, bF0, ddG, bG0, pPermute ); - if ( bRes0 == NULL ) - return NULL; - cuddRef( bRes0 ); - // call for cofactors - bRes1 = extraBddAndPermute( table, ddF, bF1, ddG, bG1, pPermute ); - if ( bRes1 == NULL ) - { - Cudd_IterDerefBdd( ddF, bRes0 ); - return NULL; - } - cuddRef( bRes1 ); - - // compose the result - bRes = cuddBddIteRecur( ddF, bVar, bRes1, bRes0 ); - if ( bRes == NULL ) - { - Cudd_IterDerefBdd( ddF, bRes0 ); - Cudd_IterDerefBdd( ddF, bRes1 ); - return NULL; - } - cuddRef( bRes ); - Cudd_IterDerefBdd( ddF, bRes0 ); - Cudd_IterDerefBdd( ddF, bRes1 ); - - // cache the result -// if ( Cudd_Regular(bF)->ref != 1 || Cudd_Regular(bG)->ref != 1 ) - { - ptrint fanout = (ptrint)Cudd_Regular(bF)->ref * Cudd_Regular(bG)->ref; - cuddSatDec(fanout); - cuddHashTableInsert2( table, bF, bG, bRes, fanout ); - } - cuddDeref( bRes ); - return bRes; -} - -/**Function************************************************************* - - Synopsis [Testbench.] - - Description [This procedure takes BDD manager ddF and two BDDs - in this manager (bF and bG). It creates a new manager ddG, - transfers bG into it and then reorders it, resulting in bG2. - Then it tries to compute the product of bF and bG2 in ddF.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Extra_TestAndPerm( DdManager * ddF, DdNode * bF, DdNode * bG ) -{ - DdManager * ddG; - DdNode * bG2, * bRes1, * bRes2; - abctime clk; - // disable variable ordering in ddF - Cudd_AutodynDisable( ddF ); - - // create new BDD manager - ddG = Cudd_Init( ddF->size, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); - // transfer BDD into it - Cudd_ShuffleHeap( ddG, ddF->invperm ); - bG2 = Extra_TransferLevelByLevel( ddF, ddG, bG ); Cudd_Ref( bG2 ); - // reorder the new manager - Cudd_ReduceHeap( ddG, CUDD_REORDER_SYMM_SIFT, 1 ); - - // compute the result -clk = Abc_Clock(); - bRes1 = Cudd_bddAnd( ddF, bF, bG ); Cudd_Ref( bRes1 ); -Abc_PrintTime( 1, "Runtime of Cudd_bddAnd ", Abc_Clock() - clk ); - - // compute the result -Counter = 0; -clk = Abc_Clock(); - bRes2 = Extra_bddAndPermute( ddF, bF, ddG, bG2, NULL ); Cudd_Ref( bRes2 ); -Abc_PrintTime( 1, "Runtime of new procedure", Abc_Clock() - clk ); -printf( "Recursive calls = %d\n", Counter ); -printf( "|F| =%6d |G| =%6d |H| =%6d |F|*|G| =%9d ", - Cudd_DagSize(bF), Cudd_DagSize(bG), Cudd_DagSize(bRes2), - Cudd_DagSize(bF) * Cudd_DagSize(bG) ); - - if ( bRes1 == bRes2 ) - printf( "Result verified.\n\n" ); - else - printf( "Result is incorrect.\n\n" ); - - Cudd_RecursiveDeref( ddF, bRes1 ); - Cudd_RecursiveDeref( ddF, bRes2 ); - // quit the new manager - Cudd_RecursiveDeref( ddG, bG2 ); - Extra_StopManager( ddG ); - - // re-enable variable ordering in ddF - Cudd_AutodynEnable( ddF, CUDD_REORDER_SYMM_SIFT ); -} - -/**Function************************************************************* - - Synopsis [Writes ZDD into a PLA file.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Extra_zddDumpPla( DdManager * dd, DdNode * F, int nVars, char * pFileName ) -{ - DdGen *gen; - char * pCube; - int * pPath, i; - FILE * pFile = fopen( pFileName, "wb" ); - if ( pFile == NULL ) - { - printf( "Cannot open file \"%s\" for writing.\n", pFileName ); - return; - } - fprintf( pFile, "# PLA file dumped by Extra_zddDumpPla() in ABC\n" ); - fprintf( pFile, ".i %d\n", nVars ); - fprintf( pFile, ".o 1\n" ); - pCube = ABC_CALLOC( char, dd->sizeZ ); - Cudd_zddForeachPath( dd, F, gen, pPath ) - { - for ( i = 0; i < nVars; i++ ) - pCube[i] = '-'; - for ( i = 0; i < nVars; i++ ) - if ( pPath[2*i] == 1 || pPath[2*i+1] == 1 ) - pCube[i] = '0' + (pPath[2*i] == 1); - fprintf( pFile, "%s 1\n", pCube ); - } - fprintf( pFile, ".e\n\n" ); - fclose( pFile ); - ABC_FREE( pCube ); -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - -ABC_NAMESPACE_IMPL_END - |