| /**CFile**************************************************************** |
| |
| FileName [extraBddUnate.c] |
| |
| PackageName [extra] |
| |
| Synopsis [Efficient methods to compute the information about |
| unate variables using an algorithm that is conceptually similar to |
| the algorithm for two-variable symmetry computation presented in: |
| A. Mishchenko. Fast Computation of Symmetries in Boolean Functions. |
| Transactions on CAD, Nov. 2003.] |
| |
| Author [Alan Mishchenko] |
| |
| Affiliation [UC Berkeley] |
| |
| Date [Ver. 2.0. Started - September 1, 2003.] |
| |
| Revision [$Id: extraBddUnate.c,v 1.0 2003/09/01 00:00:00 alanmi Exp $] |
| |
| ***********************************************************************/ |
| |
| #include "extraBdd.h" |
| |
| ABC_NAMESPACE_IMPL_START |
| |
| |
| /*---------------------------------------------------------------------------*/ |
| /* Constant declarations */ |
| /*---------------------------------------------------------------------------*/ |
| |
| /*---------------------------------------------------------------------------*/ |
| /* Stucture declarations */ |
| /*---------------------------------------------------------------------------*/ |
| |
| /*---------------------------------------------------------------------------*/ |
| /* Type declarations */ |
| /*---------------------------------------------------------------------------*/ |
| |
| /*---------------------------------------------------------------------------*/ |
| /* Variable declarations */ |
| /*---------------------------------------------------------------------------*/ |
| |
| /*---------------------------------------------------------------------------*/ |
| /* Macro declarations */ |
| /*---------------------------------------------------------------------------*/ |
| |
| /**AutomaticStart*************************************************************/ |
| |
| /*---------------------------------------------------------------------------*/ |
| /* Static function prototypes */ |
| /*---------------------------------------------------------------------------*/ |
| |
| /**AutomaticEnd***************************************************************/ |
| |
| /*---------------------------------------------------------------------------*/ |
| /* Definition of exported functions */ |
| /*---------------------------------------------------------------------------*/ |
| |
| |
| /**Function******************************************************************** |
| |
| Synopsis [Computes the classical symmetry information for the function.] |
| |
| Description [Returns the symmetry information in the form of Extra_UnateInfo_t structure.] |
| |
| SideEffects [If the ZDD variables are not derived from BDD variables with |
| multiplicity 2, this function may derive them in a wrong way.] |
| |
| SeeAlso [] |
| |
| ******************************************************************************/ |
| Extra_UnateInfo_t * Extra_UnateComputeFast( |
| DdManager * dd, /* the manager */ |
| DdNode * bFunc) /* the function whose symmetries are computed */ |
| { |
| DdNode * bSupp; |
| DdNode * zRes; |
| Extra_UnateInfo_t * p; |
| |
| bSupp = Cudd_Support( dd, bFunc ); Cudd_Ref( bSupp ); |
| zRes = Extra_zddUnateInfoCompute( dd, bFunc, bSupp ); Cudd_Ref( zRes ); |
| |
| p = Extra_UnateInfoCreateFromZdd( dd, zRes, bSupp ); |
| |
| Cudd_RecursiveDeref( dd, bSupp ); |
| Cudd_RecursiveDerefZdd( dd, zRes ); |
| |
| return p; |
| |
| } /* end of Extra_UnateInfoCompute */ |
| |
| |
| /**Function******************************************************************** |
| |
| Synopsis [Computes the classical symmetry information as a ZDD.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ******************************************************************************/ |
| DdNode * Extra_zddUnateInfoCompute( |
| DdManager * dd, /* the DD manager */ |
| DdNode * bF, |
| DdNode * bVars) |
| { |
| DdNode * res; |
| do { |
| dd->reordered = 0; |
| res = extraZddUnateInfoCompute( dd, bF, bVars ); |
| } while (dd->reordered == 1); |
| return(res); |
| |
| } /* end of Extra_zddUnateInfoCompute */ |
| |
| |
| /**Function******************************************************************** |
| |
| Synopsis [Converts a set of variables into a set of singleton subsets.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ******************************************************************************/ |
| DdNode * Extra_zddGetSingletonsBoth( |
| DdManager * dd, /* the DD manager */ |
| DdNode * bVars) /* the set of variables */ |
| { |
| DdNode * res; |
| do { |
| dd->reordered = 0; |
| res = extraZddGetSingletonsBoth( dd, bVars ); |
| } while (dd->reordered == 1); |
| return(res); |
| |
| } /* end of Extra_zddGetSingletonsBoth */ |
| |
| /**Function******************************************************************** |
| |
| Synopsis [Allocates unateness information structure.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ******************************************************************************/ |
| Extra_UnateInfo_t * Extra_UnateInfoAllocate( int nVars ) |
| { |
| Extra_UnateInfo_t * p; |
| // allocate and clean the storage for unateness info |
| p = ABC_ALLOC( Extra_UnateInfo_t, 1 ); |
| memset( p, 0, sizeof(Extra_UnateInfo_t) ); |
| p->nVars = nVars; |
| p->pVars = ABC_ALLOC( Extra_UnateVar_t, nVars ); |
| memset( p->pVars, 0, nVars * sizeof(Extra_UnateVar_t) ); |
| return p; |
| } /* end of Extra_UnateInfoAllocate */ |
| |
| /**Function******************************************************************** |
| |
| Synopsis [Deallocates symmetry information structure.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ******************************************************************************/ |
| void Extra_UnateInfoDissolve( Extra_UnateInfo_t * p ) |
| { |
| ABC_FREE( p->pVars ); |
| ABC_FREE( p ); |
| } /* end of Extra_UnateInfoDissolve */ |
| |
| /**Function******************************************************************** |
| |
| Synopsis [Allocates symmetry information structure.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ******************************************************************************/ |
| void Extra_UnateInfoPrint( Extra_UnateInfo_t * p ) |
| { |
| char * pBuffer; |
| int i; |
| pBuffer = ABC_ALLOC( char, p->nVarsMax+1 ); |
| memset( pBuffer, ' ', p->nVarsMax ); |
| pBuffer[p->nVarsMax] = 0; |
| for ( i = 0; i < p->nVars; i++ ) |
| if ( p->pVars[i].Neg ) |
| pBuffer[ p->pVars[i].iVar ] = 'n'; |
| else if ( p->pVars[i].Pos ) |
| pBuffer[ p->pVars[i].iVar ] = 'p'; |
| else |
| pBuffer[ p->pVars[i].iVar ] = '.'; |
| printf( "%s\n", pBuffer ); |
| ABC_FREE( pBuffer ); |
| } /* end of Extra_UnateInfoPrint */ |
| |
| |
| /**Function******************************************************************** |
| |
| Synopsis [Creates the symmetry information structure from ZDD.] |
| |
| Description [ZDD representation of symmetries is the set of cubes, each |
| of which has two variables in the positive polarity. These variables correspond |
| to the symmetric variable pair.] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ******************************************************************************/ |
| Extra_UnateInfo_t * Extra_UnateInfoCreateFromZdd( DdManager * dd, DdNode * zPairs, DdNode * bSupp ) |
| { |
| Extra_UnateInfo_t * p; |
| DdNode * bTemp, * zSet, * zCube, * zTemp; |
| int * pMapVars2Nums; |
| int i, nSuppSize; |
| |
| nSuppSize = Extra_bddSuppSize( dd, bSupp ); |
| |
| // allocate and clean the storage for symmetry info |
| p = Extra_UnateInfoAllocate( nSuppSize ); |
| |
| // allocate the storage for the temporary map |
| pMapVars2Nums = ABC_ALLOC( int, dd->size ); |
| memset( pMapVars2Nums, 0, dd->size * sizeof(int) ); |
| |
| // assign the variables |
| p->nVarsMax = dd->size; |
| for ( i = 0, bTemp = bSupp; bTemp != b1; bTemp = cuddT(bTemp), i++ ) |
| { |
| p->pVars[i].iVar = bTemp->index; |
| pMapVars2Nums[bTemp->index] = i; |
| } |
| |
| // write the symmetry info into the structure |
| zSet = zPairs; Cudd_Ref( zSet ); |
| // Cudd_zddPrintCover( dd, zPairs ); printf( "\n" ); |
| while ( zSet != z0 ) |
| { |
| // get the next cube |
| zCube = Extra_zddSelectOneSubset( dd, zSet ); Cudd_Ref( zCube ); |
| |
| // add this var to the data structure |
| assert( cuddT(zCube) == z1 && cuddE(zCube) == z0 ); |
| if ( zCube->index & 1 ) // neg |
| p->pVars[ pMapVars2Nums[zCube->index/2] ].Neg = 1; |
| else |
| p->pVars[ pMapVars2Nums[zCube->index/2] ].Pos = 1; |
| // count the unate vars |
| p->nUnate++; |
| |
| // update the cuver and deref the cube |
| zSet = Cudd_zddDiff( dd, zTemp = zSet, zCube ); Cudd_Ref( zSet ); |
| Cudd_RecursiveDerefZdd( dd, zTemp ); |
| Cudd_RecursiveDerefZdd( dd, zCube ); |
| |
| } // for each cube |
| Cudd_RecursiveDerefZdd( dd, zSet ); |
| ABC_FREE( pMapVars2Nums ); |
| return p; |
| |
| } /* end of Extra_UnateInfoCreateFromZdd */ |
| |
| |
| |
| /**Function******************************************************************** |
| |
| Synopsis [Computes the classical unateness information for the function.] |
| |
| Description [Uses the naive way of comparing cofactors.] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ******************************************************************************/ |
| Extra_UnateInfo_t * Extra_UnateComputeSlow( DdManager * dd, DdNode * bFunc ) |
| { |
| int nSuppSize; |
| DdNode * bSupp, * bTemp; |
| Extra_UnateInfo_t * p; |
| int i, Res; |
| |
| // compute the support |
| bSupp = Cudd_Support( dd, bFunc ); Cudd_Ref( bSupp ); |
| nSuppSize = Extra_bddSuppSize( dd, bSupp ); |
| //printf( "Support = %d. ", nSuppSize ); |
| //Extra_bddPrint( dd, bSupp ); |
| //printf( "%d ", nSuppSize ); |
| |
| // allocate the storage for symmetry info |
| p = Extra_UnateInfoAllocate( nSuppSize ); |
| |
| // assign the variables |
| p->nVarsMax = dd->size; |
| for ( i = 0, bTemp = bSupp; bTemp != b1; bTemp = cuddT(bTemp), i++ ) |
| { |
| Res = Extra_bddCheckUnateNaive( dd, bFunc, bTemp->index ); |
| p->pVars[i].iVar = bTemp->index; |
| if ( Res == -1 ) |
| p->pVars[i].Neg = 1; |
| else if ( Res == 1 ) |
| p->pVars[i].Pos = 1; |
| p->nUnate += (Res != 0); |
| } |
| Cudd_RecursiveDeref( dd, bSupp ); |
| return p; |
| |
| } /* end of Extra_UnateComputeSlow */ |
| |
| /**Function******************************************************************** |
| |
| Synopsis [Checks if the two variables are symmetric.] |
| |
| Description [Returns 0 if vars are not unate. Return -1/+1 if the var is neg/pos unate.] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ******************************************************************************/ |
| int Extra_bddCheckUnateNaive( |
| DdManager * dd, /* the DD manager */ |
| DdNode * bF, |
| int iVar) |
| { |
| DdNode * bCof0, * bCof1; |
| int Res; |
| |
| assert( iVar < dd->size ); |
| |
| bCof0 = Cudd_Cofactor( dd, bF, Cudd_Not(Cudd_bddIthVar(dd,iVar)) ); Cudd_Ref( bCof0 ); |
| bCof1 = Cudd_Cofactor( dd, bF, Cudd_bddIthVar(dd,iVar) ); Cudd_Ref( bCof1 ); |
| |
| if ( Cudd_bddLeq( dd, bCof0, bCof1 ) ) |
| Res = 1; |
| else if ( Cudd_bddLeq( dd, bCof1, bCof0 ) ) |
| Res =-1; |
| else |
| Res = 0; |
| |
| Cudd_RecursiveDeref( dd, bCof0 ); |
| Cudd_RecursiveDeref( dd, bCof1 ); |
| return Res; |
| } /* end of Extra_bddCheckUnateNaive */ |
| |
| |
| |
| /*---------------------------------------------------------------------------*/ |
| /* Definition of internal functions */ |
| /*---------------------------------------------------------------------------*/ |
| |
| /**Function******************************************************************** |
| |
| Synopsis [Performs a recursive step of Extra_UnateInfoCompute.] |
| |
| Description [Returns the set of symmetric variable pairs represented as a set |
| of two-literal ZDD cubes. Both variables always appear in the positive polarity |
| in the cubes. This function works without building new BDD nodes. Some relatively |
| small number of ZDD nodes may be built to ensure proper bookkeeping of the |
| symmetry information.] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ******************************************************************************/ |
| DdNode * |
| extraZddUnateInfoCompute( |
| DdManager * dd, /* the manager */ |
| DdNode * bFunc, /* the function whose symmetries are computed */ |
| DdNode * bVars ) /* the set of variables on which this function depends */ |
| { |
| DdNode * zRes; |
| DdNode * bFR = Cudd_Regular(bFunc); |
| |
| if ( cuddIsConstant(bFR) ) |
| { |
| if ( cuddIsConstant(bVars) ) |
| return z0; |
| return extraZddGetSingletonsBoth( dd, bVars ); |
| } |
| assert( bVars != b1 ); |
| |
| if ( (zRes = cuddCacheLookup2Zdd(dd, extraZddUnateInfoCompute, bFunc, bVars)) ) |
| return zRes; |
| else |
| { |
| DdNode * zRes0, * zRes1; |
| DdNode * zTemp, * zPlus; |
| DdNode * bF0, * bF1; |
| DdNode * bVarsNew; |
| int nVarsExtra; |
| int LevelF; |
| int AddVar; |
| |
| // every variable in bF should be also in bVars, therefore LevelF cannot be above LevelV |
| // if LevelF is below LevelV, scroll through the vars in bVars to the same level as F |
| // count how many extra vars are there in bVars |
| nVarsExtra = 0; |
| LevelF = dd->perm[bFR->index]; |
| for ( bVarsNew = bVars; LevelF > dd->perm[bVarsNew->index]; bVarsNew = cuddT(bVarsNew) ) |
| nVarsExtra++; |
| // the indexes (level) of variables should be synchronized now |
| assert( bFR->index == bVarsNew->index ); |
| |
| // cofactor the function |
| if ( bFR != bFunc ) // bFunc is complemented |
| { |
| bF0 = Cudd_Not( cuddE(bFR) ); |
| bF1 = Cudd_Not( cuddT(bFR) ); |
| } |
| else |
| { |
| bF0 = cuddE(bFR); |
| bF1 = cuddT(bFR); |
| } |
| |
| // solve subproblems |
| zRes0 = extraZddUnateInfoCompute( dd, bF0, cuddT(bVarsNew) ); |
| if ( zRes0 == NULL ) |
| return NULL; |
| cuddRef( zRes0 ); |
| |
| // if there is no symmetries in the negative cofactor |
| // there is no need to test the positive cofactor |
| if ( zRes0 == z0 ) |
| zRes = zRes0; // zRes takes reference |
| else |
| { |
| zRes1 = extraZddUnateInfoCompute( dd, bF1, cuddT(bVarsNew) ); |
| if ( zRes1 == NULL ) |
| { |
| Cudd_RecursiveDerefZdd( dd, zRes0 ); |
| return NULL; |
| } |
| cuddRef( zRes1 ); |
| |
| // only those variables are pair-wise symmetric |
| // that are pair-wise symmetric in both cofactors |
| // therefore, intersect the solutions |
| zRes = cuddZddIntersect( dd, zRes0, zRes1 ); |
| if ( zRes == NULL ) |
| { |
| Cudd_RecursiveDerefZdd( dd, zRes0 ); |
| Cudd_RecursiveDerefZdd( dd, zRes1 ); |
| return NULL; |
| } |
| cuddRef( zRes ); |
| Cudd_RecursiveDerefZdd( dd, zRes0 ); |
| Cudd_RecursiveDerefZdd( dd, zRes1 ); |
| } |
| |
| // consider the current top-most variable |
| AddVar = -1; |
| if ( Cudd_bddLeq( dd, bF0, bF1 ) ) // pos |
| AddVar = 0; |
| else if ( Cudd_bddLeq( dd, bF1, bF0 ) ) // neg |
| AddVar = 1; |
| if ( AddVar >= 0 ) |
| { |
| // create the singleton |
| zPlus = cuddZddGetNode( dd, 2*bFR->index + AddVar, z1, z0 ); |
| if ( zPlus == NULL ) |
| { |
| Cudd_RecursiveDerefZdd( dd, zRes ); |
| return NULL; |
| } |
| cuddRef( zPlus ); |
| |
| // add these to the result |
| zRes = cuddZddUnion( dd, zTemp = zRes, zPlus ); |
| if ( zRes == NULL ) |
| { |
| Cudd_RecursiveDerefZdd( dd, zTemp ); |
| Cudd_RecursiveDerefZdd( dd, zPlus ); |
| return NULL; |
| } |
| cuddRef( zRes ); |
| Cudd_RecursiveDerefZdd( dd, zTemp ); |
| Cudd_RecursiveDerefZdd( dd, zPlus ); |
| } |
| // only zRes is referenced at this point |
| |
| // if we skipped some variables, these variables cannot be symmetric with |
| // any variables that are currently in the support of bF, but they can be |
| // symmetric with the variables that are in bVars but not in the support of bF |
| for ( bVarsNew = bVars; LevelF > dd->perm[bVarsNew->index]; bVarsNew = cuddT(bVarsNew) ) |
| { |
| // create the negative singleton |
| zPlus = cuddZddGetNode( dd, 2*bVarsNew->index+1, z1, z0 ); |
| if ( zPlus == NULL ) |
| { |
| Cudd_RecursiveDerefZdd( dd, zRes ); |
| return NULL; |
| } |
| cuddRef( zPlus ); |
| |
| // add these to the result |
| zRes = cuddZddUnion( dd, zTemp = zRes, zPlus ); |
| if ( zRes == NULL ) |
| { |
| Cudd_RecursiveDerefZdd( dd, zTemp ); |
| Cudd_RecursiveDerefZdd( dd, zPlus ); |
| return NULL; |
| } |
| cuddRef( zRes ); |
| Cudd_RecursiveDerefZdd( dd, zTemp ); |
| Cudd_RecursiveDerefZdd( dd, zPlus ); |
| |
| |
| // create the positive singleton |
| zPlus = cuddZddGetNode( dd, 2*bVarsNew->index, z1, z0 ); |
| if ( zPlus == NULL ) |
| { |
| Cudd_RecursiveDerefZdd( dd, zRes ); |
| return NULL; |
| } |
| cuddRef( zPlus ); |
| |
| // add these to the result |
| zRes = cuddZddUnion( dd, zTemp = zRes, zPlus ); |
| if ( zRes == NULL ) |
| { |
| Cudd_RecursiveDerefZdd( dd, zTemp ); |
| Cudd_RecursiveDerefZdd( dd, zPlus ); |
| return NULL; |
| } |
| cuddRef( zRes ); |
| Cudd_RecursiveDerefZdd( dd, zTemp ); |
| Cudd_RecursiveDerefZdd( dd, zPlus ); |
| } |
| cuddDeref( zRes ); |
| |
| /* insert the result into cache */ |
| cuddCacheInsert2(dd, extraZddUnateInfoCompute, bFunc, bVars, zRes); |
| return zRes; |
| } |
| } /* end of extraZddUnateInfoCompute */ |
| |
| |
| /**Function******************************************************************** |
| |
| Synopsis [Performs a recursive step of Extra_zddGetSingletons.] |
| |
| Description [Returns the set of ZDD singletons, containing those pos/neg |
| polarity ZDD variables that correspond to the BDD variables in bVars.] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ******************************************************************************/ |
| DdNode * extraZddGetSingletonsBoth( |
| DdManager * dd, /* the DD manager */ |
| DdNode * bVars) /* the set of variables */ |
| { |
| DdNode * zRes; |
| |
| if ( bVars == b1 ) |
| return z1; |
| |
| if ( (zRes = cuddCacheLookup1Zdd(dd, extraZddGetSingletonsBoth, bVars)) ) |
| return zRes; |
| else |
| { |
| DdNode * zTemp, * zPlus; |
| |
| // solve subproblem |
| zRes = extraZddGetSingletonsBoth( dd, cuddT(bVars) ); |
| if ( zRes == NULL ) |
| return NULL; |
| cuddRef( zRes ); |
| |
| |
| // create the negative singleton |
| zPlus = cuddZddGetNode( dd, 2*bVars->index+1, z1, z0 ); |
| if ( zPlus == NULL ) |
| { |
| Cudd_RecursiveDerefZdd( dd, zRes ); |
| return NULL; |
| } |
| cuddRef( zPlus ); |
| |
| // add these to the result |
| zRes = cuddZddUnion( dd, zTemp = zRes, zPlus ); |
| if ( zRes == NULL ) |
| { |
| Cudd_RecursiveDerefZdd( dd, zTemp ); |
| Cudd_RecursiveDerefZdd( dd, zPlus ); |
| return NULL; |
| } |
| cuddRef( zRes ); |
| Cudd_RecursiveDerefZdd( dd, zTemp ); |
| Cudd_RecursiveDerefZdd( dd, zPlus ); |
| |
| |
| // create the positive singleton |
| zPlus = cuddZddGetNode( dd, 2*bVars->index, z1, z0 ); |
| if ( zPlus == NULL ) |
| { |
| Cudd_RecursiveDerefZdd( dd, zRes ); |
| return NULL; |
| } |
| cuddRef( zPlus ); |
| |
| // add these to the result |
| zRes = cuddZddUnion( dd, zTemp = zRes, zPlus ); |
| if ( zRes == NULL ) |
| { |
| Cudd_RecursiveDerefZdd( dd, zTemp ); |
| Cudd_RecursiveDerefZdd( dd, zPlus ); |
| return NULL; |
| } |
| cuddRef( zRes ); |
| Cudd_RecursiveDerefZdd( dd, zTemp ); |
| Cudd_RecursiveDerefZdd( dd, zPlus ); |
| |
| cuddDeref( zRes ); |
| cuddCacheInsert1( dd, extraZddGetSingletonsBoth, bVars, zRes ); |
| return zRes; |
| } |
| } /* end of extraZddGetSingletonsBoth */ |
| |
| |
| /*---------------------------------------------------------------------------*/ |
| /* Definition of static Functions */ |
| /*---------------------------------------------------------------------------*/ |
| ABC_NAMESPACE_IMPL_END |
| |
