diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2008-01-30 20:01:00 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2008-01-30 20:01:00 -0800 |
commit | 0c6505a26a537dc911b6566f82d759521e527c08 (patch) | |
tree | f2687995efd4943fe3b1307fce7ef5942d0a57b3 /src/misc/extra/extraBddMisc.c | |
parent | 4d30a1e4f1edecff86d5066ce4653a370e59e5e1 (diff) | |
download | abc-0c6505a26a537dc911b6566f82d759521e527c08.tar.gz abc-0c6505a26a537dc911b6566f82d759521e527c08.tar.bz2 abc-0c6505a26a537dc911b6566f82d759521e527c08.zip |
Version abc80130_2
Diffstat (limited to 'src/misc/extra/extraBddMisc.c')
-rw-r--r-- | src/misc/extra/extraBddMisc.c | 574 |
1 files changed, 571 insertions, 3 deletions
diff --git a/src/misc/extra/extraBddMisc.c b/src/misc/extra/extraBddMisc.c index 373ce5c5..a3320ad3 100644 --- a/src/misc/extra/extraBddMisc.c +++ b/src/misc/extra/extraBddMisc.c @@ -14,7 +14,7 @@ Date [Ver. 1.0. Started - June 20, 2005.] - Revision [$Id: extraBddMisc.c,v 1.0 2003/09/01 00:00:00 alanmi Exp $] + Revision [$Id: extraBddMisc.c,v 1.4 2005/10/04 00:19:54 alanmi Exp $] ***********************************************************************/ @@ -50,10 +50,13 @@ // 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 ) ); // file "cuddUtils.c" -static void ddSupportStep ARGS((DdNode *f, int *support)); -static void ddClearFlag ARGS((DdNode *f)); +static void ddSupportStep(DdNode *f, int *support); +static void ddClearFlag(DdNode *f); + +static DdNode* extraZddPrimes( DdManager *dd, DdNode* F ); /**AutomaticEnd***************************************************************/ @@ -684,6 +687,280 @@ DdNode * Extra_bddComputeRangeCube( DdManager * dd, int iStart, int iStop ) 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 = 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 ); + + 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 */ + + /*---------------------------------------------------------------------------*/ /* Definition of internal functions */ /*---------------------------------------------------------------------------*/ @@ -1039,6 +1316,297 @@ ddClearFlag( } /* 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 ) + { +#ifdef DD_DEBUG + bddPermuteRecurHits++; +#endif + 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 */ + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// |