src/bdd/dsd/dsdCheck.c File Reference

#include "dsdInt.h"
Include dependency graph for dsdCheck.c:

Go to the source code of this file.

Data Structures

struct  Dsd_Cache_t_
struct  Dsd_Entry_t_

Typedefs

typedef struct Dsd_Cache_t_ Dds_Cache_t
typedef struct Dsd_Entry_t_ Dsd_Entry_t

Functions

static int Dsd_CheckRootFunctionIdentity_rec (DdManager *dd, DdNode *bF1, DdNode *bF2, DdNode *bC1, DdNode *bC2)
void Dsd_CheckCacheAllocate (int nEntries)
void Dsd_CheckCacheDeallocate ()
void Dsd_CheckCacheClear ()
int Dsd_CheckRootFunctionIdentity (DdManager *dd, DdNode *bF1, DdNode *bF2, DdNode *bC1, DdNode *bC2)

Variables

static Dds_Cache_t * pCache

Typedef Documentation

typedef struct Dsd_Cache_t_ Dds_Cache_t

CFile****************************************************************

FileName [dsdCheck.c]

PackageName [DSD: Disjoint-support decomposition package.]

Synopsis [Procedures to check the identity of root functions.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 8.0. Started - September 22, 2003.]

Revision [

Id
dsdCheck.c,v 1.0 2002/22/09 00:00:00 alanmi Exp

] DECLARATIONS ///

Definition at line 25 of file dsdCheck.c.

typedef struct Dsd_Entry_t_ Dsd_Entry_t

Definition at line 26 of file dsdCheck.c.

Function Documentation

void Dsd_CheckCacheAllocate ( int  nEntries  ) 

FUNCTION DEFINITIONS ///Function********************************************************************

Synopsis [(Re)allocates the local cache.]

Description []

SideEffects []

SeeAlso []

Definition at line 60 of file dsdCheck.c.

00061 {
00062         int nRequested;
00063 
00064     pCache = ALLOC( Dds_Cache_t, 1 );
00065     memset( pCache, 0, sizeof(Dds_Cache_t) );
00066 
00067         // check what is the size of the current cache
00068     nRequested = Cudd_Prime( nEntries );
00069         if ( pCache->nTableSize != nRequested )
00070         { // the current size is different
00071                 // deallocate the old, allocate the new
00072                 if ( pCache->nTableSize )
00073                         Dsd_CheckCacheDeallocate();
00074                 // allocate memory for the hash table
00075                 pCache->nTableSize = nRequested;
00076                 pCache->pTable = ALLOC( Dsd_Entry_t, nRequested );
00077         }
00078         // otherwise, there is no need to allocate, just clean
00079         Dsd_CheckCacheClear();
00080 //      printf( "\nThe number of allocated cache entries = %d.\n\n", pCache->nTableSize );
00081 }

void Dsd_CheckCacheClear (  ) 

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

Synopsis [Clears the local cache.]

Description []

SideEffects []

SeeAlso []

Definition at line 111 of file dsdCheck.c.

00112 {
00113         int i;
00114         for ( i = 0; i < pCache->nTableSize; i++ )
00115                 pCache->pTable[0].bX[0] = NULL;
00116 }

void Dsd_CheckCacheDeallocate (  ) 

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

Synopsis [Deallocates the local cache.]

Description []

SideEffects []

SeeAlso []

Definition at line 94 of file dsdCheck.c.

00095 {
00096         free( pCache->pTable );
00097     free( pCache );
00098 }

int Dsd_CheckRootFunctionIdentity ( DdManager *  dd,
DdNode *  bF1,
DdNode *  bF2,
DdNode *  bC1,
DdNode *  bC2 
)

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

Synopsis [Checks whether it is true that bF1(bC1=0) == bF2(bC2=0).]

Description []

SideEffects []

SeeAlso []

Definition at line 130 of file dsdCheck.c.

00131 {
00132         int RetValue;
00133 //      pCache->nSuccess = 0;
00134 //      pCache->nFailure = 0;
00135         RetValue = Dsd_CheckRootFunctionIdentity_rec(dd, bF1, bF2, bC1, bC2);
00136 //      printf( "Cache success = %d. Cache failure = %d.\n", pCache->nSuccess, pCache->nFailure );
00137         return RetValue;
00138 }

int Dsd_CheckRootFunctionIdentity_rec ( DdManager *  dd,
DdNode *  bF1,
DdNode *  bF2,
DdNode *  bC1,
DdNode *  bC2 
) [static]

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

Synopsis [Performs the recursive step of Dsd_CheckRootFunctionIdentity().]

Description []

SideEffects []

SeeAlso []

Definition at line 151 of file dsdCheck.c.

00152 {
00153         unsigned HKey;
00154 
00155         // if either bC1 or bC2 is zero, the test is true
00156 //      if ( bC1 == b0 || bC2 == b0 )  return 1;
00157         assert( bC1 != b0 );
00158         assert( bC2 != b0 );
00159 
00160         // if both bC1 and bC2 are one - perform comparison
00161         if ( bC1 == b1 && bC2 == b1 )  return (int)( bF1 == bF2 );
00162 
00163         if ( bF1 == b0 )
00164                 return Cudd_bddLeq( dd, bC2, Cudd_Not(bF2) );
00165 
00166         if ( bF1 == b1 )
00167                 return Cudd_bddLeq( dd, bC2, bF2 );
00168 
00169         if ( bF2 == b0 )
00170                 return Cudd_bddLeq( dd, bC1, Cudd_Not(bF1) );
00171 
00172         if ( bF2 == b1 )
00173                 return Cudd_bddLeq( dd, bC1, bF1 );
00174 
00175         // otherwise, keep expanding
00176 
00177         // check cache
00178 //      HKey = _Hash( ((unsigned)bF1), ((unsigned)bF2), ((unsigned)bC1), ((unsigned)bC2) );
00179         HKey = hashKey4( bF1, bF2, bC1, bC2, pCache->nTableSize );
00180         if ( pCache->pTable[HKey].bX[0] == bF1 && 
00181                  pCache->pTable[HKey].bX[1] == bF2 && 
00182                  pCache->pTable[HKey].bX[2] == bC1 && 
00183                  pCache->pTable[HKey].bX[3] == bC2 )
00184         {
00185                 pCache->nSuccess++;
00186                 return (int)pCache->pTable[HKey].bX[4]; // the last bit records the result (yes/no)
00187         }
00188         else
00189         {
00190 
00191                 // determine the top variables
00192                 int RetValue;
00193                 DdNode * bA[4]  = { bF1, bF2, bC1, bC2 }; // arguments
00194                 DdNode * bAR[4] = { Cudd_Regular(bF1), Cudd_Regular(bF2), Cudd_Regular(bC1), Cudd_Regular(bC2) }; // regular arguments
00195                 int CurLevel[4] = { cuddI(dd,bAR[0]->index), cuddI(dd,bAR[1]->index), cuddI(dd,bAR[2]->index), cuddI(dd,bAR[3]->index) };
00196                 int TopLevel = CUDD_CONST_INDEX;
00197                 int i;
00198                 DdNode * bE[4], * bT[4];
00199                 DdNode * bF1next, * bF2next, * bC1next, * bC2next;
00200 
00201                 pCache->nFailure++;
00202 
00203                 // determine the top level
00204                 for ( i = 0; i < 4; i++ )
00205                         if ( TopLevel > CurLevel[i] )
00206                                  TopLevel = CurLevel[i];
00207 
00208                 // compute the cofactors
00209                 for ( i = 0; i < 4; i++ )
00210                 if ( TopLevel == CurLevel[i] )
00211                 {
00212                         if ( bA[i] != bAR[i] ) // complemented
00213                         {
00214                                 bE[i] = Cudd_Not(cuddE(bAR[i]));
00215                                 bT[i] = Cudd_Not(cuddT(bAR[i]));
00216                         }
00217                         else
00218                         {
00219                                 bE[i] = cuddE(bAR[i]);
00220                                 bT[i] = cuddT(bAR[i]);
00221                         }
00222                 }
00223                 else
00224                         bE[i] = bT[i] = bA[i];
00225 
00226                 // solve subproblems
00227                 // three cases are possible
00228 
00229                 // (1) the top var belongs to both C1 and C2
00230                 //     in this case, any cofactor of F1 and F2 will do, 
00231                 //     as long as the corresponding cofactor of C1 and C2 is not equal to 0
00232                 if ( TopLevel == CurLevel[2] && TopLevel == CurLevel[3] ) 
00233                 {
00234                         if ( bE[2] != b0 ) // C1
00235                         {
00236                                 bF1next = bE[0];
00237                                 bC1next = bE[2];
00238                         }
00239                         else
00240                         {
00241                                 bF1next = bT[0];
00242                                 bC1next = bT[2];
00243                         }
00244                         if ( bE[3] != b0 ) // C2
00245                         {
00246                                 bF2next = bE[1];
00247                                 bC2next = bE[3];
00248                         }
00249                         else
00250                         {
00251                                 bF2next = bT[1];
00252                                 bC2next = bT[3];
00253                         }
00254                         RetValue = Dsd_CheckRootFunctionIdentity_rec( dd, bF1next, bF2next, bC1next, bC2next );
00255                 }
00256                 // (2) the top var belongs to either C1 or C2
00257                 //     in this case normal splitting of cofactors
00258                 else if ( TopLevel == CurLevel[2] && TopLevel != CurLevel[3] ) 
00259                 {
00260                         if ( bE[2] != b0 ) // C1
00261                         {
00262                                 bF1next = bE[0];
00263                                 bC1next = bE[2];
00264                         }
00265                         else
00266                         {
00267                                 bF1next = bT[0];
00268                                 bC1next = bT[2];
00269                         }
00270                         // split around this variable
00271                         RetValue = Dsd_CheckRootFunctionIdentity_rec( dd, bF1next, bE[1], bC1next, bE[3] );
00272                         if ( RetValue == 1 ) // test another branch; otherwise, there is no need to test
00273                                 RetValue = Dsd_CheckRootFunctionIdentity_rec( dd, bF1next, bT[1], bC1next, bT[3] );
00274                 }
00275                 else if ( TopLevel != CurLevel[2] && TopLevel == CurLevel[3] ) 
00276                 {
00277                         if ( bE[3] != b0 ) // C2
00278                         {
00279                                 bF2next = bE[1];
00280                                 bC2next = bE[3];
00281                         }
00282                         else
00283                         {
00284                                 bF2next = bT[1];
00285                                 bC2next = bT[3];
00286                         }
00287                         // split around this variable
00288                         RetValue = Dsd_CheckRootFunctionIdentity_rec( dd, bE[0], bF2next, bE[2], bC2next );
00289                         if ( RetValue == 1 ) // test another branch; otherwise, there is no need to test
00290                                 RetValue = Dsd_CheckRootFunctionIdentity_rec( dd, bT[0], bF2next, bT[2], bC2next );
00291                 }
00292                 // (3) the top var does not belong to C1 and C2
00293                 //     in this case normal splitting of cofactors
00294                 else // if ( TopLevel != CurLevel[2] && TopLevel != CurLevel[3] )
00295                 {
00296                         // split around this variable
00297                         RetValue = Dsd_CheckRootFunctionIdentity_rec( dd, bE[0], bE[1], bE[2], bE[3] );
00298                         if ( RetValue == 1 ) // test another branch; otherwise, there is no need to test
00299                                 RetValue = Dsd_CheckRootFunctionIdentity_rec( dd, bT[0], bT[1], bT[2], bT[3] );
00300                 }
00301 
00302                 // set cache
00303                 for ( i = 0; i < 4; i++ )
00304                         pCache->pTable[HKey].bX[i] = bA[i];
00305                 pCache->pTable[HKey].bX[4] = (DdNode*)RetValue;
00306 
00307                 return RetValue;
00308         }
00309 }

Variable Documentation

Dds_Cache_t* pCache [static]

Definition at line 41 of file dsdCheck.c.

Generated on Tue Jan 5 12:18:58 2010 for abc70930 by  doxygen 1.6.1