/**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