src/misc/extra/extraBddUnate.c File Reference

#include "extra.h"
Include dependency graph for extraBddUnate.c:

Go to the source code of this file.

Functions

Extra_UnateInfo_t * Extra_UnateComputeFast (DdManager *dd, DdNode *bFunc)
DdNode * Extra_zddUnateInfoCompute (DdManager *dd, DdNode *bF, DdNode *bVars)
DdNode * Extra_zddGetSingletonsBoth (DdManager *dd, DdNode *bVars)
Extra_UnateInfo_t * Extra_UnateInfoAllocate (int nVars)
void Extra_UnateInfoDissolve (Extra_UnateInfo_t *p)
void Extra_UnateInfoPrint (Extra_UnateInfo_t *p)
Extra_UnateInfo_t * Extra_UnateInfoCreateFromZdd (DdManager *dd, DdNode *zPairs, DdNode *bSupp)
Extra_UnateInfo_t * Extra_UnateComputeSlow (DdManager *dd, DdNode *bFunc)
int Extra_bddCheckUnateNaive (DdManager *dd, DdNode *bF, int iVar)
DdNode * extraZddUnateInfoCompute (DdManager *dd, DdNode *bFunc, DdNode *bVars)
DdNode * extraZddGetSingletonsBoth (DdManager *dd, DdNode *bVars)

Function Documentation

int Extra_bddCheckUnateNaive ( DdManager *  dd,
DdNode *  bF,
int  iVar 
)

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 []

Definition at line 335 of file extraBddUnate.c.

00339 {
00340     DdNode * bCof0, * bCof1;
00341     int Res;
00342 
00343     assert( iVar < dd->size );
00344 
00345     bCof0 = Cudd_Cofactor( dd, bF, Cudd_Not(Cudd_bddIthVar(dd,iVar)) );  Cudd_Ref( bCof0 );
00346     bCof1 = Cudd_Cofactor( dd, bF, Cudd_bddIthVar(dd,iVar) );            Cudd_Ref( bCof1 );
00347 
00348     if ( Cudd_bddLeq( dd, bCof0, bCof1 ) )
00349         Res = 1;
00350     else if ( Cudd_bddLeq( dd, bCof1, bCof0 ) )
00351         Res =-1;
00352     else
00353         Res = 0;
00354 
00355     Cudd_RecursiveDeref( dd, bCof0 );
00356     Cudd_RecursiveDeref( dd, bCof1 );
00357     return Res;
00358 } /* end of Extra_bddCheckUnateNaive */

Extra_UnateInfo_t* Extra_UnateComputeFast ( DdManager *  dd,
DdNode *  bFunc 
)

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

]AutomaticStart AutomaticEnd 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 []

Definition at line 70 of file extraBddUnate.c.

00073 {
00074     DdNode * bSupp;
00075     DdNode * zRes;
00076     Extra_UnateInfo_t * p;
00077 
00078     bSupp = Cudd_Support( dd, bFunc );                      Cudd_Ref( bSupp );
00079     zRes  = Extra_zddUnateInfoCompute( dd, bFunc, bSupp );  Cudd_Ref( zRes );
00080 
00081     p = Extra_UnateInfoCreateFromZdd( dd, zRes, bSupp );
00082 
00083     Cudd_RecursiveDeref( dd, bSupp );
00084     Cudd_RecursiveDerefZdd( dd, zRes );
00085 
00086     return p;
00087 
00088 } /* end of Extra_UnateInfoCompute */

Extra_UnateInfo_t* Extra_UnateComputeSlow ( DdManager *  dd,
DdNode *  bFunc 
)

Function********************************************************************

Synopsis [Computes the classical unateness information for the function.]

Description [Uses the naive way of comparing cofactors.]

SideEffects []

SeeAlso []

Definition at line 290 of file extraBddUnate.c.

00291 {
00292     int nSuppSize;
00293     DdNode * bSupp, * bTemp;
00294     Extra_UnateInfo_t * p;
00295     int i, Res;
00296 
00297     // compute the support
00298     bSupp = Cudd_Support( dd, bFunc );   Cudd_Ref( bSupp );
00299     nSuppSize = Extra_bddSuppSize( dd, bSupp );
00300 //printf( "Support = %d. ", nSuppSize );
00301 //Extra_bddPrint( dd, bSupp );
00302 //printf( "%d ", nSuppSize );
00303 
00304     // allocate the storage for symmetry info
00305     p = Extra_UnateInfoAllocate( nSuppSize );
00306 
00307     // assign the variables
00308     p->nVarsMax = dd->size;
00309     for ( i = 0, bTemp = bSupp; bTemp != b1; bTemp = cuddT(bTemp), i++ )
00310     {
00311         Res = Extra_bddCheckUnateNaive( dd, bFunc, bTemp->index );
00312         p->pVars[i].iVar = bTemp->index;
00313         if ( Res == -1 )
00314             p->pVars[i].Neg = 1;
00315         else if ( Res == 1 )
00316             p->pVars[i].Pos = 1;
00317         p->nUnate += (Res != 0);
00318     }
00319     Cudd_RecursiveDeref( dd, bSupp );
00320     return p;
00321 
00322 } /* end of Extra_UnateComputeSlow */

Extra_UnateInfo_t* Extra_UnateInfoAllocate ( int  nVars  ) 

Function********************************************************************

Synopsis [Allocates unateness information structure.]

Description []

SideEffects []

SeeAlso []

Definition at line 152 of file extraBddUnate.c.

00153 {
00154     Extra_UnateInfo_t * p;
00155     // allocate and clean the storage for unateness info
00156     p = ALLOC( Extra_UnateInfo_t, 1 );
00157     memset( p, 0, sizeof(Extra_UnateInfo_t) );
00158     p->nVars     = nVars;
00159     p->pVars     = ALLOC( Extra_UnateVar_t, nVars );  
00160     memset( p->pVars, 0, nVars * sizeof(Extra_UnateVar_t) );
00161     return p;
00162 } /* end of Extra_UnateInfoAllocate */

Extra_UnateInfo_t* Extra_UnateInfoCreateFromZdd ( DdManager *  dd,
DdNode *  zPairs,
DdNode *  bSupp 
)

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 []

Definition at line 224 of file extraBddUnate.c.

00225 {
00226     Extra_UnateInfo_t * p;
00227     DdNode * bTemp, * zSet, * zCube, * zTemp;
00228     int * pMapVars2Nums;
00229     int i, nSuppSize;
00230 
00231     nSuppSize = Extra_bddSuppSize( dd, bSupp );
00232 
00233     // allocate and clean the storage for symmetry info
00234     p = Extra_UnateInfoAllocate( nSuppSize );
00235 
00236     // allocate the storage for the temporary map
00237     pMapVars2Nums = ALLOC( int, dd->size );
00238     memset( pMapVars2Nums, 0, dd->size * sizeof(int) );
00239 
00240     // assign the variables
00241     p->nVarsMax = dd->size;
00242     for ( i = 0, bTemp = bSupp; bTemp != b1; bTemp = cuddT(bTemp), i++ )
00243     {
00244         p->pVars[i].iVar = bTemp->index;
00245         pMapVars2Nums[bTemp->index] = i;
00246     }
00247 
00248     // write the symmetry info into the structure
00249     zSet = zPairs;   Cudd_Ref( zSet );
00250 //    Cudd_zddPrintCover( dd, zPairs );    printf( "\n" );
00251     while ( zSet != z0 )
00252     {
00253         // get the next cube
00254         zCube  = Extra_zddSelectOneSubset( dd, zSet );    Cudd_Ref( zCube );
00255 
00256         // add this var to the data structure
00257         assert( cuddT(zCube) == z1 && cuddE(zCube) == z0 );
00258         if ( zCube->index & 1 ) // neg
00259             p->pVars[ pMapVars2Nums[zCube->index/2] ].Neg = 1;
00260         else
00261             p->pVars[ pMapVars2Nums[zCube->index/2] ].Pos = 1;
00262         // count the unate vars
00263         p->nUnate++;
00264 
00265         // update the cuver and deref the cube
00266         zSet = Cudd_zddDiff( dd, zTemp = zSet, zCube );     Cudd_Ref( zSet );
00267         Cudd_RecursiveDerefZdd( dd, zTemp );
00268         Cudd_RecursiveDerefZdd( dd, zCube );
00269 
00270     } // for each cube 
00271     Cudd_RecursiveDerefZdd( dd, zSet );
00272     FREE( pMapVars2Nums );
00273     return p;
00274 
00275 } /* end of Extra_UnateInfoCreateFromZdd */

void Extra_UnateInfoDissolve ( Extra_UnateInfo_t *  p  ) 

Function********************************************************************

Synopsis [Deallocates symmetry information structure.]

Description []

SideEffects []

SeeAlso []

Definition at line 175 of file extraBddUnate.c.

00176 {
00177     free( p->pVars );
00178     free( p );
00179 } /* end of Extra_UnateInfoDissolve */

void Extra_UnateInfoPrint ( Extra_UnateInfo_t *  p  ) 

Function********************************************************************

Synopsis [Allocates symmetry information structure.]

Description []

SideEffects []

SeeAlso []

Definition at line 192 of file extraBddUnate.c.

00193 {
00194     char * pBuffer;
00195     int i;
00196     pBuffer = ALLOC( char, p->nVarsMax+1 );
00197     memset( pBuffer, ' ', p->nVarsMax );
00198     pBuffer[p->nVarsMax] = 0;
00199     for ( i = 0; i < p->nVars; i++ )
00200         if ( p->pVars[i].Neg )
00201             pBuffer[ p->pVars[i].iVar ] = 'n';
00202         else if ( p->pVars[i].Pos )
00203             pBuffer[ p->pVars[i].iVar ] = 'p';
00204         else
00205             pBuffer[ p->pVars[i].iVar ] = '.';
00206     printf( "%s\n", pBuffer );
00207     free( pBuffer );
00208 } /* end of Extra_UnateInfoPrint */

DdNode* Extra_zddGetSingletonsBoth ( DdManager *  dd,
DdNode *  bVars 
)

Function********************************************************************

Synopsis [Converts a set of variables into a set of singleton subsets.]

Description []

SideEffects []

SeeAlso []

Definition at line 128 of file extraBddUnate.c.

00131 {
00132     DdNode * res;
00133     do {
00134         dd->reordered = 0;
00135         res = extraZddGetSingletonsBoth( dd, bVars );
00136     } while (dd->reordered == 1);
00137     return(res);
00138 
00139 } /* end of Extra_zddGetSingletonsBoth */

DdNode* Extra_zddUnateInfoCompute ( DdManager *  dd,
DdNode *  bF,
DdNode *  bVars 
)

Function********************************************************************

Synopsis [Computes the classical symmetry information as a ZDD.]

Description []

SideEffects []

SeeAlso []

Definition at line 102 of file extraBddUnate.c.

00106 {
00107     DdNode * res;
00108     do {
00109         dd->reordered = 0;
00110         res = extraZddUnateInfoCompute( dd, bF, bVars );
00111     } while (dd->reordered == 1);
00112     return(res);
00113 
00114 } /* end of Extra_zddUnateInfoCompute */

DdNode* extraZddGetSingletonsBoth ( DdManager *  dd,
DdNode *  bVars 
)

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 []

Definition at line 567 of file extraBddUnate.c.

00570 {
00571     DdNode * zRes;
00572 
00573     if ( bVars == b1 )
00574         return z1;
00575 
00576     if ( zRes = cuddCacheLookup1Zdd(dd, extraZddGetSingletonsBoth, bVars) )
00577         return zRes;
00578     else
00579     {
00580         DdNode * zTemp, * zPlus;          
00581 
00582         // solve subproblem
00583         zRes = extraZddGetSingletonsBoth( dd, cuddT(bVars) );
00584         if ( zRes == NULL ) 
00585             return NULL;
00586         cuddRef( zRes );
00587 
00588         
00589         // create the negative singleton
00590         zPlus = cuddZddGetNode( dd, 2*bVars->index+1, z1, z0 );
00591         if ( zPlus == NULL ) 
00592         {
00593             Cudd_RecursiveDerefZdd( dd, zRes );
00594             return NULL;
00595         }
00596         cuddRef( zPlus );
00597 
00598         // add these to the result
00599         zRes = cuddZddUnion( dd, zTemp = zRes, zPlus );
00600         if ( zRes == NULL )
00601         {
00602             Cudd_RecursiveDerefZdd( dd, zTemp );
00603             Cudd_RecursiveDerefZdd( dd, zPlus );
00604             return NULL;
00605         }
00606         cuddRef( zRes );
00607         Cudd_RecursiveDerefZdd( dd, zTemp );
00608         Cudd_RecursiveDerefZdd( dd, zPlus );
00609         
00610 
00611         // create the positive singleton
00612         zPlus = cuddZddGetNode( dd, 2*bVars->index, z1, z0 );
00613         if ( zPlus == NULL ) 
00614         {
00615             Cudd_RecursiveDerefZdd( dd, zRes );
00616             return NULL;
00617         }
00618         cuddRef( zPlus );
00619 
00620         // add these to the result
00621         zRes = cuddZddUnion( dd, zTemp = zRes, zPlus );
00622         if ( zRes == NULL )
00623         {
00624             Cudd_RecursiveDerefZdd( dd, zTemp );
00625             Cudd_RecursiveDerefZdd( dd, zPlus );
00626             return NULL;
00627         }
00628         cuddRef( zRes );
00629         Cudd_RecursiveDerefZdd( dd, zTemp );
00630         Cudd_RecursiveDerefZdd( dd, zPlus );
00631 
00632         cuddDeref( zRes );
00633         cuddCacheInsert1( dd, extraZddGetSingletonsBoth, bVars, zRes );
00634         return zRes;
00635     }
00636 }   /* end of extraZddGetSingletonsBoth */

DdNode* extraZddUnateInfoCompute ( DdManager *  dd,
DdNode *  bFunc,
DdNode *  bVars 
)

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 []

Definition at line 382 of file extraBddUnate.c.

00386 {
00387     DdNode * zRes;
00388     DdNode * bFR = Cudd_Regular(bFunc); 
00389 
00390     if ( cuddIsConstant(bFR) )
00391     {
00392         if ( cuddIsConstant(bVars) )
00393             return z0;
00394         return extraZddGetSingletonsBoth( dd, bVars );
00395     }
00396     assert( bVars != b1 );
00397 
00398     if ( zRes = cuddCacheLookup2Zdd(dd, extraZddUnateInfoCompute, bFunc, bVars) )
00399         return zRes;
00400     else
00401     {
00402         DdNode * zRes0, * zRes1;
00403         DdNode * zTemp, * zPlus;             
00404         DdNode * bF0, * bF1;             
00405         DdNode * bVarsNew;
00406         int nVarsExtra;
00407         int LevelF;
00408         int AddVar;
00409 
00410         // every variable in bF should be also in bVars, therefore LevelF cannot be above LevelV
00411         // if LevelF is below LevelV, scroll through the vars in bVars to the same level as F
00412         // count how many extra vars are there in bVars
00413         nVarsExtra = 0;
00414         LevelF = dd->perm[bFR->index];
00415         for ( bVarsNew = bVars; LevelF > dd->perm[bVarsNew->index]; bVarsNew = cuddT(bVarsNew) )
00416             nVarsExtra++; 
00417         // the indexes (level) of variables should be synchronized now
00418         assert( bFR->index == bVarsNew->index );
00419 
00420         // cofactor the function
00421         if ( bFR != bFunc ) // bFunc is complemented 
00422         {
00423             bF0 = Cudd_Not( cuddE(bFR) );
00424             bF1 = Cudd_Not( cuddT(bFR) );
00425         }
00426         else
00427         {
00428             bF0 = cuddE(bFR);
00429             bF1 = cuddT(bFR);
00430         }
00431 
00432         // solve subproblems
00433         zRes0 = extraZddUnateInfoCompute( dd, bF0, cuddT(bVarsNew) );
00434         if ( zRes0 == NULL )
00435             return NULL;
00436         cuddRef( zRes0 );
00437 
00438         // if there is no symmetries in the negative cofactor
00439         // there is no need to test the positive cofactor
00440         if ( zRes0 == z0 )
00441             zRes = zRes0;  // zRes takes reference
00442         else
00443         {
00444             zRes1 = extraZddUnateInfoCompute( dd, bF1, cuddT(bVarsNew) );
00445             if ( zRes1 == NULL )
00446             {
00447                 Cudd_RecursiveDerefZdd( dd, zRes0 );
00448                 return NULL;
00449             }
00450             cuddRef( zRes1 );
00451 
00452             // only those variables are pair-wise symmetric 
00453             // that are pair-wise symmetric in both cofactors
00454             // therefore, intersect the solutions
00455             zRes = cuddZddIntersect( dd, zRes0, zRes1 );
00456             if ( zRes == NULL )
00457             {
00458                 Cudd_RecursiveDerefZdd( dd, zRes0 );
00459                 Cudd_RecursiveDerefZdd( dd, zRes1 );
00460                 return NULL;
00461             }
00462             cuddRef( zRes );
00463             Cudd_RecursiveDerefZdd( dd, zRes0 );
00464             Cudd_RecursiveDerefZdd( dd, zRes1 );
00465         }
00466 
00467         // consider the current top-most variable
00468         AddVar = -1;
00469         if ( Cudd_bddLeq( dd, bF0, bF1 ) ) // pos
00470             AddVar = 0;
00471         else if ( Cudd_bddLeq( dd, bF1, bF0 ) ) // neg
00472             AddVar = 1;
00473         if ( AddVar >= 0 )
00474         {
00475             // create the singleton
00476             zPlus = cuddZddGetNode( dd, 2*bFR->index + AddVar, z1, z0 );
00477             if ( zPlus == NULL ) 
00478             {
00479                 Cudd_RecursiveDerefZdd( dd, zRes );
00480                 return NULL;
00481             }
00482             cuddRef( zPlus );
00483 
00484             // add these to the result
00485             zRes = cuddZddUnion( dd, zTemp = zRes, zPlus );
00486             if ( zRes == NULL )
00487             {
00488                 Cudd_RecursiveDerefZdd( dd, zTemp );
00489                 Cudd_RecursiveDerefZdd( dd, zPlus );
00490                 return NULL;
00491             }
00492             cuddRef( zRes );
00493             Cudd_RecursiveDerefZdd( dd, zTemp );
00494             Cudd_RecursiveDerefZdd( dd, zPlus );
00495         }
00496         // only zRes is referenced at this point
00497 
00498         // if we skipped some variables, these variables cannot be symmetric with
00499         // any variables that are currently in the support of bF, but they can be 
00500         // symmetric with the variables that are in bVars but not in the support of bF
00501         for ( bVarsNew = bVars; LevelF > dd->perm[bVarsNew->index]; bVarsNew = cuddT(bVarsNew) )
00502         {
00503             // create the negative singleton
00504             zPlus = cuddZddGetNode( dd, 2*bVarsNew->index+1, z1, z0 );
00505             if ( zPlus == NULL ) 
00506             {
00507                 Cudd_RecursiveDerefZdd( dd, zRes );
00508                 return NULL;
00509             }
00510             cuddRef( zPlus );
00511 
00512             // add these to the result
00513             zRes = cuddZddUnion( dd, zTemp = zRes, zPlus );
00514             if ( zRes == NULL )
00515             {
00516                 Cudd_RecursiveDerefZdd( dd, zTemp );
00517                 Cudd_RecursiveDerefZdd( dd, zPlus );
00518                 return NULL;
00519             }
00520             cuddRef( zRes );
00521             Cudd_RecursiveDerefZdd( dd, zTemp );
00522             Cudd_RecursiveDerefZdd( dd, zPlus );
00523         
00524 
00525             // create the positive singleton
00526             zPlus = cuddZddGetNode( dd, 2*bVarsNew->index, z1, z0 );
00527             if ( zPlus == NULL ) 
00528             {
00529                 Cudd_RecursiveDerefZdd( dd, zRes );
00530                 return NULL;
00531             }
00532             cuddRef( zPlus );
00533 
00534             // add these to the result
00535             zRes = cuddZddUnion( dd, zTemp = zRes, zPlus );
00536             if ( zRes == NULL )
00537             {
00538                 Cudd_RecursiveDerefZdd( dd, zTemp );
00539                 Cudd_RecursiveDerefZdd( dd, zPlus );
00540                 return NULL;
00541             }
00542             cuddRef( zRes );
00543             Cudd_RecursiveDerefZdd( dd, zTemp );
00544             Cudd_RecursiveDerefZdd( dd, zPlus );
00545         }
00546         cuddDeref( zRes );
00547 
00548         /* insert the result into cache */
00549         cuddCacheInsert2(dd, extraZddUnateInfoCompute, bFunc, bVars, zRes);
00550         return zRes;
00551     }
00552 } /* end of extraZddUnateInfoCompute */

Generated on Tue Jan 5 12:19:14 2010 for abc70930 by  doxygen 1.6.1