From 780321cf54b8da33be6800ea4533d3f8176fd822 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 6 Dec 2011 17:48:31 -0800 Subject: Another attempt to make CUDD platform- and runtime-independent. --- src/bdd/cudd/cudd.h | 1 + src/bdd/cudd/cuddAPI.c | 3 +- src/bdd/cudd/cuddAndAbs.c | 2 +- src/bdd/cudd/cuddBddAbs.c | 2 +- src/bdd/cudd/cuddBddCorr.c | 4 +-- src/bdd/cudd/cuddBddIte.c | 16 ++++----- src/bdd/cudd/cuddBridge.c | 4 +-- src/bdd/cudd/cuddCache.c | 84 +++++++++++++++++++++++++++++++++------------ src/bdd/cudd/cuddCompose.c | 2 +- src/bdd/cudd/cuddInt.h | 26 ++++++++++++-- src/bdd/cudd/cuddLCache.c | 20 +++++------ src/bdd/cudd/cuddLinear.c | 6 ++-- src/bdd/cudd/cuddReorder.c | 23 ++++++++----- src/bdd/cudd/cuddSymmetry.c | 2 +- src/bdd/cudd/cuddTable.c | 43 ++++++++++++++--------- src/bdd/cudd/cuddUtil.c | 2 +- src/bdd/cudd/cuddZddLin.c | 12 +++---- src/bdd/cudd/cuddZddReord.c | 10 +++--- 18 files changed, 171 insertions(+), 91 deletions(-) (limited to 'src/bdd/cudd') diff --git a/src/bdd/cudd/cudd.h b/src/bdd/cudd/cudd.h index c72edbb0..9231b5ab 100644 --- a/src/bdd/cudd/cudd.h +++ b/src/bdd/cudd/cudd.h @@ -283,6 +283,7 @@ struct DdNode { CUDD_VALUE_TYPE value; /* for constant nodes */ DdChildren kids; /* for internal nodes */ } type; + ABC_INT64_T Id; }; #ifdef __osf__ diff --git a/src/bdd/cudd/cuddAPI.c b/src/bdd/cudd/cuddAPI.c index 233795e2..e2926ea2 100644 --- a/src/bdd/cudd/cuddAPI.c +++ b/src/bdd/cudd/cuddAPI.c @@ -3067,8 +3067,7 @@ Cudd_PrintInfo( if (retval == EOF) return(0); retval = fprintf(fp,"Number of dead ZDD nodes: %u\n", dd->deadZ); if (retval == EOF) return(0); - retval = fprintf(fp,"Total number of nodes allocated: %.0f\n", - dd->allocated); + retval = fprintf(fp,"Total number of nodes allocated: %d\n", dd->allocated); if (retval == EOF) return(0); retval = fprintf(fp,"Total number of nodes reclaimed: %.0f\n", dd->reclaimed); diff --git a/src/bdd/cudd/cuddAndAbs.c b/src/bdd/cudd/cuddAndAbs.c index b42f376d..2f38490d 100644 --- a/src/bdd/cudd/cuddAndAbs.c +++ b/src/bdd/cudd/cuddAndAbs.c @@ -259,7 +259,7 @@ cuddBddAndAbstractRecur( } } - if ( manager->TimeStop && manager->TimeStop < time(NULL) ) + if ( manager->TimeStop && manager->TimeStop < clock() ) return NULL; if (topf == top) { diff --git a/src/bdd/cudd/cuddBddAbs.c b/src/bdd/cudd/cuddBddAbs.c index 257dbbe3..9bcb32ad 100644 --- a/src/bdd/cudd/cuddBddAbs.c +++ b/src/bdd/cudd/cuddBddAbs.c @@ -500,7 +500,7 @@ cuddBddXorExistAbstractRecur( /* At this point f, g, and cube are not constant. */ - if (f > g) { /* Try to increase cache efficiency. */ + if (cuddF2L(f) > cuddF2L(g)) { /* Try to increase cache efficiency. */ DdNode *tmp = f; f = g; g = tmp; diff --git a/src/bdd/cudd/cuddBddCorr.c b/src/bdd/cudd/cuddBddCorr.c index 32d5d97c..62f48bde 100644 --- a/src/bdd/cudd/cuddBddCorr.c +++ b/src/bdd/cudd/cuddBddCorr.c @@ -258,7 +258,7 @@ bddCorrelationAux( ** (f EXNOR g) = (g EXNOR f) ** (f' EXNOR g') = (f EXNOR g). */ - if (f > g) { + if (cuddF2L(f) > cuddF2L(g)) { DdNode *tmp = f; f = g; g = tmp; } @@ -361,7 +361,7 @@ bddCorrelationWeightsAux( ** (f EXNOR g) = (g EXNOR f) ** (f' EXNOR g') = (f EXNOR g). */ - if (f > g) { + if (cuddF2L(f) > cuddF2L(g)) { DdNode *tmp = f; f = g; g = tmp; } diff --git a/src/bdd/cudd/cuddBddIte.c b/src/bdd/cudd/cuddBddIte.c index d1afdbee..df0c799f 100644 --- a/src/bdd/cudd/cuddBddIte.c +++ b/src/bdd/cudd/cuddBddIte.c @@ -556,7 +556,7 @@ Cudd_bddLeq( tmp = g; g = Cudd_Not(f); f = Cudd_Not(tmp); - } else if (Cudd_IsComplement(f) && g < f) { + } else if (Cudd_IsComplement(f) && cuddF2L(g) < cuddF2L(f)) { tmp = g; g = Cudd_Not(f); f = Cudd_Not(tmp); @@ -789,7 +789,7 @@ cuddBddIntersectRecur( if (f == one) return(g); /* At this point f and g are not constant. */ - if (f > g) { DdNode *tmp = f; f = g; g = tmp; } + if (cuddF2L(f) > cuddF2L(g)) { DdNode *tmp = f; f = g; g = tmp; } res = cuddCacheLookup2(dd,Cudd_bddIntersect,f,g); if (res != NULL) return(res); @@ -912,7 +912,7 @@ cuddBddAndRecur( } /* At this point f and g are not constant. */ - if (f > g) { /* Try to increase cache efficiency. */ + if (cuddF2L(f) > cuddF2L(g)) { /* Try to increase cache efficiency. */ DdNode *tmp = f; f = g; g = tmp; @@ -926,7 +926,7 @@ cuddBddAndRecur( if (r != NULL) return(r); } - if ( manager->TimeStop && manager->TimeStop < time(NULL) ) + if ( manager->TimeStop && manager->TimeStop < clock() ) return NULL; /* Here we can skip the use of cuddI, because the operands are known @@ -1030,7 +1030,7 @@ cuddBddXorRecur( /* Terminal cases. */ if (f == g) return(zero); if (f == Cudd_Not(g)) return(one); - if (f > g) { /* Try to increase cache efficiency and simplify tests. */ + if (cuddF2L(f) > cuddF2L(g)) { /* Try to increase cache efficiency and simplify tests. */ DdNode *tmp = f; f = g; g = tmp; @@ -1197,7 +1197,7 @@ bddVarToCanonical( change = 0; if (G == one) { /* ITE(F,c,H) */ - if ((topf > toph) || (topf == toph && f > h)) { + if ((topf > toph) || (topf == toph && cuddF2L(f) > cuddF2L(h))) { r = h; h = f; f = r; /* ITE(F,1,H) = ITE(H,1,F) */ @@ -1208,7 +1208,7 @@ bddVarToCanonical( change = 1; } } else if (H == one) { /* ITE(F,G,c) */ - if ((topf > topg) || (topf == topg && f > g)) { + if ((topf > topg) || (topf == topg && cuddF2L(f) > cuddF2L(g))) { r = g; g = f; f = r; /* ITE(F,G,0) = ITE(G,F,0) */ @@ -1219,7 +1219,7 @@ bddVarToCanonical( change = 1; } } else if (g == Cudd_Not(h)) { /* ITE(F,G,!G) = ITE(G,F,!F) */ - if ((topf > topg) || (topf == topg && f > g)) { + if ((topf > topg) || (topf == topg && cuddF2L(f) > cuddF2L(g))) { r = f; f = g; g = r; diff --git a/src/bdd/cudd/cuddBridge.c b/src/bdd/cudd/cuddBridge.c index c051666d..97a6f393 100644 --- a/src/bdd/cudd/cuddBridge.c +++ b/src/bdd/cudd/cuddBridge.c @@ -976,9 +976,9 @@ cuddBddTransferRecur( if (st_lookup(table, (const char *)f, (char **)&res)) return(Cudd_NotCond(res,comple)); - if ( ddS->TimeStop && ddS->TimeStop < time(NULL) ) + if ( ddS->TimeStop && ddS->TimeStop < clock() ) return NULL; - if ( ddD->TimeStop && ddD->TimeStop < time(NULL) ) + if ( ddD->TimeStop && ddD->TimeStop < clock() ) return NULL; /* Recursive step. */ diff --git a/src/bdd/cudd/cuddCache.c b/src/bdd/cudd/cuddCache.c index d9722ee9..b8978ab6 100644 --- a/src/bdd/cudd/cuddCache.c +++ b/src/bdd/cudd/cuddCache.c @@ -149,7 +149,8 @@ cuddInitCache( ** initial cache size. */ logSize = cuddComputeFloorLog2(ddMax(cacheSize,unique->slots/2)); cacheSize = 1 << logSize; - unique->acache = ABC_ALLOC(DdCache,cacheSize+1); +// unique->acache = ABC_ALLOC(DdCache,cacheSize+1); + unique->acache = ABC_ALLOC(DdCache,cacheSize+2); if (unique->acache == NULL) { unique->errorCode = CUDD_MEMORY_OUT; return(0); @@ -162,10 +163,13 @@ cuddInitCache( unique->memused += (cacheSize) * sizeof(DdCache); #else mem = (DdNodePtr *) unique->acache; - offset = (ptruint) mem & (sizeof(DdCache) - 1); - mem += (sizeof(DdCache) - offset) / sizeof(DdNodePtr); +// offset = (ptruint) mem & (sizeof(DdCache) - 1); +// mem += (sizeof(DdCache) - offset) / sizeof(DdNodePtr); + offset = (ptruint) mem & (32 - 1); + mem += (32 - offset) / sizeof(DdNodePtr); unique->cache = (DdCache *) mem; - assert(((ptruint) unique->cache & (sizeof(DdCache) - 1)) == 0); +// assert(((ptruint) unique->cache & (sizeof(DdCache) - 1)) == 0); + assert(((ptruint) unique->cache & (32 - 1)) == 0); unique->memused += (cacheSize+1) * sizeof(DdCache); #endif unique->cacheSlots = cacheSize; @@ -224,14 +228,22 @@ cuddCacheInsert( DdNode * data) { int posn; + unsigned hash; register DdCache *entry; ptruint uf, ug, uh; + ptruint ufc, ugc, uhc; uf = (ptruint) f | (op & 0xe); ug = (ptruint) g | (op >> 4); uh = (ptruint) h; - posn = ddCHash2(uh,uf,ug,table->cacheShift); + ufc = (ptruint) cuddF2L(f) | (op & 0xe); + ugc = (ptruint) cuddF2L(g) | (op >> 4); + uhc = (ptruint) cuddF2L(h); + + hash = ddCHash2_(uhc,ufc,ugc); +// posn = ddCHash2(uhc,ufc,ugc,table->cacheShift); + posn = hash >> table->cacheShift; entry = &table->cache[posn]; table->cachecollisions += entry->data != NULL; @@ -244,6 +256,7 @@ cuddCacheInsert( #ifdef DD_CACHE_PROFILE entry->count++; #endif + entry->hash = hash; } /* end of cuddCacheInsert */ @@ -269,9 +282,12 @@ cuddCacheInsert2( DdNode * data) { int posn; + unsigned hash; register DdCache *entry; - posn = ddCHash2(op,f,g,table->cacheShift); + hash = ddCHash2_(op,cuddF2L(f),cuddF2L(g)); +// posn = ddCHash2(op,cuddF2L(f),cuddF2L(g),table->cacheShift); + posn = hash >> table->cacheShift; entry = &table->cache[posn]; if (entry->data != NULL) { @@ -286,6 +302,7 @@ cuddCacheInsert2( #ifdef DD_CACHE_PROFILE entry->count++; #endif + entry->hash = hash; } /* end of cuddCacheInsert2 */ @@ -310,9 +327,12 @@ cuddCacheInsert1( DdNode * data) { int posn; + unsigned hash; register DdCache *entry; - posn = ddCHash2(op,f,f,table->cacheShift); + hash = ddCHash2_(op,cuddF2L(f),cuddF2L(f)); +// posn = ddCHash2(op,cuddF2L(f),cuddF2L(f),table->cacheShift); + posn = hash >> table->cacheShift; entry = &table->cache[posn]; if (entry->data != NULL) { @@ -327,6 +347,7 @@ cuddCacheInsert1( #ifdef DD_CACHE_PROFILE entry->count++; #endif + entry->hash = hash; } /* end of cuddCacheInsert1 */ @@ -356,11 +377,16 @@ cuddCacheLookup( DdCache *en,*cache; DdNode *data; ptruint uf, ug, uh; + ptruint ufc, ugc, uhc; uf = (ptruint) f | (op & 0xe); ug = (ptruint) g | (op >> 4); uh = (ptruint) h; + ufc = (ptruint) cuddF2L(f) | (op & 0xe); + ugc = (ptruint) cuddF2L(g) | (op >> 4); + uhc = (ptruint) cuddF2L(h); + cache = table->cache; #ifdef DD_DEBUG if (cache == NULL) { @@ -368,10 +394,9 @@ cuddCacheLookup( } #endif - posn = ddCHash2(uh,uf,ug,table->cacheShift); + posn = ddCHash2(uhc,ufc,ugc,table->cacheShift); en = &cache[posn]; - if (en->data != NULL && en->f==(DdNodePtr)uf && en->g==(DdNodePtr)ug && - en->h==uh) { + if (en->data != NULL && en->f==(DdNodePtr)uf && en->g==(DdNodePtr)ug && en->h==uh) { data = Cudd_Regular(en->data); table->cacheHits++; if (data->ref == 0) { @@ -418,11 +443,16 @@ cuddCacheLookupZdd( DdCache *en,*cache; DdNode *data; ptruint uf, ug, uh; + ptruint ufc, ugc, uhc; uf = (ptruint) f | (op & 0xe); ug = (ptruint) g | (op >> 4); uh = (ptruint) h; + ufc = (ptruint) cuddF2L(f) | (op & 0xe); + ugc = (ptruint) cuddF2L(g) | (op >> 4); + uhc = (ptruint) cuddF2L(h); + cache = table->cache; #ifdef DD_DEBUG if (cache == NULL) { @@ -430,7 +460,7 @@ cuddCacheLookupZdd( } #endif - posn = ddCHash2(uh,uf,ug,table->cacheShift); + posn = ddCHash2(uhc,ufc,ugc,table->cacheShift); en = &cache[posn]; if (en->data != NULL && en->f==(DdNodePtr)uf && en->g==(DdNodePtr)ug && en->h==uh) { @@ -486,7 +516,7 @@ cuddCacheLookup2( } #endif - posn = ddCHash2(op,f,g,table->cacheShift); + posn = ddCHash2(op,cuddF2L(f),cuddF2L(g),table->cacheShift); en = &cache[posn]; if (en->data != NULL && en->f==f && en->g==g && en->h==(ptruint)op) { data = Cudd_Regular(en->data); @@ -539,7 +569,7 @@ cuddCacheLookup1( } #endif - posn = ddCHash2(op,f,f,table->cacheShift); + posn = ddCHash2(op,cuddF2L(f),cuddF2L(f),table->cacheShift); en = &cache[posn]; if (en->data != NULL && en->f==f && en->h==(ptruint)op) { data = Cudd_Regular(en->data); @@ -594,7 +624,7 @@ cuddCacheLookup2Zdd( } #endif - posn = ddCHash2(op,f,g,table->cacheShift); + posn = ddCHash2(op,cuddF2L(f),cuddF2L(g),table->cacheShift); en = &cache[posn]; if (en->data != NULL && en->f==f && en->g==g && en->h==(ptruint)op) { data = Cudd_Regular(en->data); @@ -647,7 +677,7 @@ cuddCacheLookup1Zdd( } #endif - posn = ddCHash2(op,f,f,table->cacheShift); + posn = ddCHash2(op,cuddF2L(f),cuddF2L(f),table->cacheShift); en = &cache[posn]; if (en->data != NULL && en->f==f && en->h==(ptruint)op) { data = Cudd_Regular(en->data); @@ -698,18 +728,23 @@ cuddConstantLookup( int posn; DdCache *en,*cache; ptruint uf, ug, uh; + ptruint ufc, ugc, uhc; uf = (ptruint) f | (op & 0xe); ug = (ptruint) g | (op >> 4); uh = (ptruint) h; + ufc = (ptruint) cuddF2L(f) | (op & 0xe); + ugc = (ptruint) cuddF2L(g) | (op >> 4); + uhc = (ptruint) cuddF2L(h); + cache = table->cache; #ifdef DD_DEBUG if (cache == NULL) { return(NULL); } #endif - posn = ddCHash2(uh,uf,ug,table->cacheShift); + posn = ddCHash2(uhc,ufc,ugc,table->cacheShift); en = &cache[posn]; /* We do not reclaim here because the result should not be @@ -919,7 +954,8 @@ cuddCacheResize( saveHandler = MMoutOfMemory; MMoutOfMemory = Cudd_OutOfMem; - table->acache = cache = ABC_ALLOC(DdCache,slots+1); +// table->acache = cache = ABC_ALLOC(DdCache,slots+1); + table->acache = cache = ABC_ALLOC(DdCache,slots+2); MMoutOfMemory = saveHandler; /* If we fail to allocate the new table we just give up. */ if (cache == NULL) { @@ -940,10 +976,14 @@ cuddCacheResize( table->cache = cache; #else mem = (DdNodePtr *) cache; - misalignment = (ptruint) mem & (sizeof(DdCache) - 1); - mem += (sizeof(DdCache) - misalignment) / sizeof(DdNodePtr); +// misalignment = (ptruint) mem & (sizeof(DdCache) - 1); +// mem += (sizeof(DdCache) - misalignment) / sizeof(DdNodePtr); +// table->cache = cache = (DdCache *) mem; +// assert(((ptruint) table->cache & (sizeof(DdCache) - 1)) == 0); + misalignment = (ptruint) mem & (32 - 1); + mem += (32 - misalignment) / sizeof(DdNodePtr); table->cache = cache = (DdCache *) mem; - assert(((ptruint) table->cache & (sizeof(DdCache) - 1)) == 0); + assert(((ptruint) table->cache & (32 - 1)) == 0); #endif shift = --(table->cacheShift); table->memused += (slots - oldslots) * sizeof(DdCache); @@ -962,7 +1002,8 @@ cuddCacheResize( for (i = 0; (unsigned) i < oldslots; i++) { old = &oldcache[i]; if (old->data != NULL) { - posn = ddCHash2(old->h,old->f,old->g,shift); +// posn = ddCHash2(old->h,old->f,old->g,shift); + posn = old->hash >> shift; entry = &cache[posn]; entry->f = old->f; entry->g = old->g; @@ -971,6 +1012,7 @@ cuddCacheResize( #ifdef DD_CACHE_PROFILE entry->count = 1; #endif + entry->hash = old->hash; moved++; } } diff --git a/src/bdd/cudd/cuddCompose.c b/src/bdd/cudd/cuddCompose.c index 7c99ac62..8dd8f8c5 100644 --- a/src/bdd/cudd/cuddCompose.c +++ b/src/bdd/cudd/cuddCompose.c @@ -1251,7 +1251,7 @@ cuddBddVarMapRecur( return(Cudd_NotCond(res,F != f)); } - if ( manager->TimeStop && manager->TimeStop < time(NULL) ) + if ( manager->TimeStop && manager->TimeStop < clock() ) return NULL; /* Split and recur on children of this node. */ diff --git a/src/bdd/cudd/cuddInt.h b/src/bdd/cudd/cuddInt.h index 229030ca..ba8da8cf 100644 --- a/src/bdd/cudd/cuddInt.h +++ b/src/bdd/cudd/cuddInt.h @@ -315,6 +315,7 @@ typedef struct DdCache { #ifdef DD_CACHE_PROFILE ptrint count; #endif + unsigned hash; } DdCache; typedef struct DdSubtable { /* subtable for one index */ @@ -372,7 +373,8 @@ struct DdManager { /* specialized DD symbol table */ /* (measured w.r.t. slots, not keys) */ unsigned int initSlots; /* initial size of a subtable */ DdNode **stack; /* stack for iterative procedures */ - double allocated; /* number of nodes allocated */ +// double allocated; /* number of nodes allocated */ + ABC_INT64_T allocated; /* number of nodes allocated */ /* (not during reordering) */ double reclaimed; /* number of nodes brought back from the dead */ int isolated; /* isolated projection functions */ @@ -697,6 +699,20 @@ typedef struct DdLevelQueue { #define cuddIZ(dd,index) (((index)==CUDD_CONST_INDEX)?(int)(index):(dd)->permZ[(index)]) +/**Macro*********************************************************************** + + Synopsis [Converts pointer into a literal.] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +#define cuddF2L(f) ((Cudd_Regular(f)->Id << 1) | Cudd_IsComplement(f)) + + /**Macro*********************************************************************** Synopsis [Hash function for the unique table.] @@ -729,6 +745,7 @@ typedef struct DdLevelQueue { SeeAlso [ddHash ddCHash2] ******************************************************************************/ +/* #if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4 #define ddCHash(o,f,g,h,s) \ ((((((unsigned)(ptruint)(f) + (unsigned)(ptruint)(o)) * DD_P1 + \ @@ -739,7 +756,7 @@ typedef struct DdLevelQueue { ((((((unsigned)(f) + (unsigned)(o)) * DD_P1 + (unsigned)(g)) * DD_P2 + \ (unsigned)(h)) * DD_P3) >> (s)) #endif - +*/ /**Macro*********************************************************************** @@ -757,9 +774,14 @@ typedef struct DdLevelQueue { #define ddCHash2(o,f,g,s) \ (((((unsigned)(ptruint)(f) + (unsigned)(ptruint)(o)) * DD_P1 + \ (unsigned)(ptruint)(g)) * DD_P2) >> (s)) +#define ddCHash2_(o,f,g) \ +(((((unsigned)(ptruint)(f) + (unsigned)(ptruint)(o)) * DD_P1 + \ + (unsigned)(ptruint)(g)) * DD_P2)) #else #define ddCHash2(o,f,g,s) \ (((((unsigned)(f) + (unsigned)(o)) * DD_P1 + (unsigned)(g)) * DD_P2) >> (s)) +#define ddCHash2_(o,f,g) \ +(((((unsigned)(f) + (unsigned)(o)) * DD_P1 + (unsigned)(g)) * DD_P2)) #endif diff --git a/src/bdd/cudd/cuddLCache.c b/src/bdd/cudd/cuddLCache.c index 45d71a8d..2d66264e 100644 --- a/src/bdd/cudd/cuddLCache.c +++ b/src/bdd/cudd/cuddLCache.c @@ -139,7 +139,7 @@ static char rcsid[] DD_UNUSED = "$Id: cuddLCache.c,v 1.24 2009/03/08 02:49:02 fa SeeAlso [ddLCHash2 ddLCHash] ******************************************************************************/ -#define ddLCHash3(f,g,h,shift) ddCHash2(f,g,h,shift) +#define ddLCHash3(f,g,h,shift) ddCHash2(f,g,h,shift) /**AutomaticStart*************************************************************/ @@ -789,7 +789,7 @@ cuddHashTableInsert1( cuddRef(value); item->count = count; item->key[0] = f; - posn = ddLCHash2(f,f,hash->shift); + posn = ddLCHash2(cuddF2L(f),cuddF2L(f),hash->shift); item->next = hash->bucket[posn]; hash->bucket[posn] = item; @@ -827,7 +827,7 @@ cuddHashTableLookup1( assert(hash->keysize == 1); #endif - posn = ddLCHash2(f,f,hash->shift); + posn = ddLCHash2(cuddF2L(f),cuddF2L(f),hash->shift); item = hash->bucket[posn]; prev = NULL; @@ -898,7 +898,7 @@ cuddHashTableInsert2( item->count = count; item->key[0] = f; item->key[1] = g; - posn = ddLCHash2(f,g,hash->shift); + posn = ddLCHash2(cuddF2L(f),cuddF2L(g),hash->shift); item->next = hash->bucket[posn]; hash->bucket[posn] = item; @@ -937,7 +937,7 @@ cuddHashTableLookup2( assert(hash->keysize == 2); #endif - posn = ddLCHash2(f,g,hash->shift); + posn = ddLCHash2(cuddF2L(f),cuddF2L(g),hash->shift); item = hash->bucket[posn]; prev = NULL; @@ -1010,7 +1010,7 @@ cuddHashTableInsert3( item->key[0] = f; item->key[1] = g; item->key[2] = h; - posn = ddLCHash3(f,g,h,hash->shift); + posn = ddLCHash3(cuddF2L(f),cuddF2L(g),cuddF2L(h),hash->shift); item->next = hash->bucket[posn]; hash->bucket[posn] = item; @@ -1050,7 +1050,7 @@ cuddHashTableLookup3( assert(hash->keysize == 3); #endif - posn = ddLCHash3(f,g,h,hash->shift); + posn = ddLCHash3(cuddF2L(f),cuddF2L(g),cuddF2L(h),hash->shift); item = hash->bucket[posn]; prev = NULL; @@ -1326,7 +1326,7 @@ cuddHashTableResize( while (item != NULL) { next = item->next; key = item->key; - posn = ddLCHash2(key[0], key[0], shift); + posn = ddLCHash2(cuddF2L(key[0]), cuddF2L(key[0]), shift); item->next = buckets[posn]; buckets[posn] = item; item = next; @@ -1338,7 +1338,7 @@ cuddHashTableResize( while (item != NULL) { next = item->next; key = item->key; - posn = ddLCHash2(key[0], key[1], shift); + posn = ddLCHash2(cuddF2L(key[0]), cuddF2L(key[1]), shift); item->next = buckets[posn]; buckets[posn] = item; item = next; @@ -1350,7 +1350,7 @@ cuddHashTableResize( while (item != NULL) { next = item->next; key = item->key; - posn = ddLCHash3(key[0], key[1], key[2], shift); + posn = ddLCHash3(cuddF2L(key[0]), cuddF2L(key[1]), cuddF2L(key[2]), shift); item->next = buckets[posn]; buckets[posn] = item; item = next; diff --git a/src/bdd/cudd/cuddLinear.c b/src/bdd/cudd/cuddLinear.c index 19de9820..e137484c 100644 --- a/src/bdd/cudd/cuddLinear.c +++ b/src/bdd/cudd/cuddLinear.c @@ -496,7 +496,7 @@ cuddLinearInPlace( cuddSatInc(newf1->ref); } else { /* Check ylist for triple (yindex,f11,f00). */ - posn = ddHash(f11, f00, yshift); + posn = ddHash(cuddF2L(f11), cuddF2L(f00), yshift); /* For each element newf1 in collision list ylist[posn]. */ previousP = &(ylist[posn]); newf1 = *previousP; @@ -550,7 +550,7 @@ cuddLinearInPlace( f10 = Cudd_Not(f10); } /* Check ylist for triple (yindex,f01,f10). */ - posn = ddHash(f01, f10, yshift); + posn = ddHash(cuddF2L(f01), cuddF2L(f10), yshift); /* For each element newf0 in collision list ylist[posn]. */ previousP = &(ylist[posn]); newf0 = *previousP; @@ -591,7 +591,7 @@ cuddLinearInPlace( ** The modified f does not already exists in xlist. ** (Because of the uniqueness of the cofactors.) */ - posn = ddHash(newf1, newf0, xshift); + posn = ddHash(cuddF2L(newf1), cuddF2L(newf0), xshift); newxkeys++; previousP = &(xlist[posn]); tmp = *previousP; diff --git a/src/bdd/cudd/cuddReorder.c b/src/bdd/cudd/cuddReorder.c index 383be18a..f9c08772 100644 --- a/src/bdd/cudd/cuddReorder.c +++ b/src/bdd/cudd/cuddReorder.c @@ -416,7 +416,8 @@ cuddDynamicAllocNode( /* Try to allocate a new block. */ saveHandler = MMoutOfMemory; MMoutOfMemory = Cudd_OutOfMem; - mem = (DdNodePtr *) ABC_ALLOC(DdNode, DD_MEM_CHUNK + 1); +// mem = (DdNodePtr *) ABC_ALLOC(DdNode, DD_MEM_CHUNK + 1); + mem = (DdNodePtr *) ABC_ALLOC(DdNode, DD_MEM_CHUNK + 2); MMoutOfMemory = saveHandler; if (mem == NULL && table->stash != NULL) { ABC_FREE(table->stash); @@ -427,7 +428,8 @@ cuddDynamicAllocNode( for (i = 0; i < table->size; i++) { table->subtables[i].maxKeys <<= 2; } - mem = (DdNodePtr *) ABC_ALLOC(DdNode,DD_MEM_CHUNK + 1); +// mem = (DdNodePtr *) ABC_ALLOC(DdNode,DD_MEM_CHUNK + 1); + mem = (DdNodePtr *) ABC_ALLOC(DdNode,DD_MEM_CHUNK + 2); } if (mem == NULL) { /* Out of luck. Call the default handler to do @@ -453,10 +455,13 @@ cuddDynamicAllocNode( ** power of 2 and a multiple of the size of a pointer. ** If we align one node, all the others will be aligned ** as well. */ - offset = (unsigned long) mem & (sizeof(DdNode) - 1); - mem += (sizeof(DdNode) - offset) / sizeof(DdNodePtr); +// offset = (unsigned long) mem & (sizeof(DdNode) - 1); +// mem += (sizeof(DdNode) - offset) / sizeof(DdNodePtr); + offset = (unsigned long) mem & (32 - 1); + mem += (32 - offset) / sizeof(DdNodePtr); #ifdef DD_DEBUG - assert(((unsigned long) mem & (sizeof(DdNode) - 1)) == 0); +// assert(((unsigned long) mem & (sizeof(DdNode) - 1)) == 0); + assert(((unsigned long) mem & (32 - 1)) == 0); #endif list = (DdNode *) mem; @@ -927,7 +932,7 @@ cuddSwapInPlace( f1 = cuddT(f); f0 = cuddE(f); /* Check xlist for pair (f11,f01). */ - posn = ddHash(f1, f0, xshift); + posn = ddHash(cuddF2L(f1), cuddF2L(f0), xshift); /* For each element tmp in collision list xlist[posn]. */ previousP = &(xlist[posn]); tmp = *previousP; @@ -988,7 +993,7 @@ cuddSwapInPlace( cuddSatInc(newf1->ref); } else { /* Check xlist for triple (xindex,f11,f01). */ - posn = ddHash(f11, f01, xshift); + posn = ddHash(cuddF2L(f11), cuddF2L(f01), xshift); /* For each element newf1 in collision list xlist[posn]. */ previousP = &(xlist[posn]); newf1 = *previousP; @@ -1042,7 +1047,7 @@ cuddSwapInPlace( f00 = Cudd_Not(f00); } /* Check xlist for triple (xindex,f10,f00). */ - posn = ddHash(f10, f00, xshift); + posn = ddHash(cuddF2L(f10), cuddF2L(f00), xshift); /* For each element newf0 in collision list xlist[posn]. */ previousP = &(xlist[posn]); newf0 = *previousP; @@ -1083,7 +1088,7 @@ cuddSwapInPlace( ** The modified f does not already exists in ylist. ** (Because of the uniqueness of the cofactors.) */ - posn = ddHash(newf1, newf0, yshift); + posn = ddHash(cuddF2L(newf1), cuddF2L(newf0), yshift); newykeys++; previousP = &(ylist[posn]); tmp = *previousP; diff --git a/src/bdd/cudd/cuddSymmetry.c b/src/bdd/cudd/cuddSymmetry.c index 3386e798..a7ef7845 100644 --- a/src/bdd/cudd/cuddSymmetry.c +++ b/src/bdd/cudd/cuddSymmetry.c @@ -367,7 +367,7 @@ cuddSymmSifting( if (ddTotalNumberSwapping >= table->siftMaxSwap) break; // enable timeout during variable reodering - alanmi 2/13/11 - if ( table->TimeStop && table->TimeStop < time(NULL) ) + if ( table->TimeStop && table->TimeStop < clock() ) break; x = table->perm[var[i]]; #ifdef DD_STATS diff --git a/src/bdd/cudd/cuddTable.c b/src/bdd/cudd/cuddTable.c index 040e4670..c83d1073 100644 --- a/src/bdd/cudd/cuddTable.c +++ b/src/bdd/cudd/cuddTable.c @@ -260,7 +260,8 @@ cuddAllocNode( /* Try to allocate a new block. */ saveHandler = MMoutOfMemory; MMoutOfMemory = Cudd_OutOfMem; - mem = (DdNodePtr *) ABC_ALLOC(DdNode,DD_MEM_CHUNK + 1); +// mem = (DdNodePtr *) ABC_ALLOC(DdNode,DD_MEM_CHUNK + 1); + mem = (DdNodePtr *) ABC_ALLOC(DdNode,DD_MEM_CHUNK + 2); MMoutOfMemory = saveHandler; if (mem == NULL) { /* No more memory: Try collecting garbage. If this succeeds, @@ -276,7 +277,8 @@ cuddAllocNode( /* Inhibit resizing of tables. */ cuddSlowTableGrowth(unique); /* Now try again. */ - mem = (DdNodePtr *) ABC_ALLOC(DdNode,DD_MEM_CHUNK + 1); +// mem = (DdNodePtr *) ABC_ALLOC(DdNode,DD_MEM_CHUNK + 1); + mem = (DdNodePtr *) ABC_ALLOC(DdNode,DD_MEM_CHUNK + 2); } if (mem == NULL) { /* Out of luck. Call the default handler to do @@ -301,11 +303,14 @@ cuddAllocNode( mem[0] = (DdNodePtr) unique->memoryList; unique->memoryList = mem; - /* Here we rely on the fact that a DdNode is as large - ** as 4 pointers. */ - offset = (ptruint) mem & (sizeof(DdNode) - 1); - mem += (sizeof(DdNode) - offset) / sizeof(DdNodePtr); - assert(((ptruint) mem & (sizeof(DdNode) - 1)) == 0); + /* Here we rely on the fact that a DdNode is as large as 4 pointers. */ +// offset = (ptruint) mem & (sizeof(DdNode) - 1); +// mem += (sizeof(DdNode) - offset) / sizeof(DdNodePtr); +// assert(((ptruint) mem & (sizeof(DdNode) - 1)) == 0); +// list = (DdNode *) mem; + offset = (ptruint) mem & (32 - 1); + mem += (32 - offset) / sizeof(DdNodePtr); + assert(((ptruint) mem & (32 - 1)) == 0); list = (DdNode *) mem; i = 1; @@ -324,6 +329,7 @@ cuddAllocNode( unique->allocated++; node = unique->nextFree; unique->nextFree = node->next; + node->Id = (unique->allocated<<4); return(node); } /* end of cuddAllocNode */ @@ -976,8 +982,11 @@ cuddGarbageCollect( while (memListTrav != NULL) { ptruint offset; nxtNode = (DdNodePtr *)memListTrav[0]; - offset = (ptruint) memListTrav & (sizeof(DdNode) - 1); - memListTrav += (sizeof(DdNode) - offset) / sizeof(DdNodePtr); +// offset = (ptruint) memListTrav & (sizeof(DdNode) - 1); +// memListTrav += (sizeof(DdNode) - offset) / sizeof(DdNodePtr); + offset = (ptruint) memListTrav & (32 - 1); + memListTrav += (32 - offset) / sizeof(DdNodePtr); + downTrav = (DdNode *)memListTrav; k = 0; do { @@ -1147,7 +1156,7 @@ cuddUniqueInter( assert(level < (unsigned) cuddI(unique,Cudd_Regular(E)->index)); #endif - pos = ddHash(T, E, subtable->shift); + pos = ddHash(cuddF2L(T), cuddF2L(E), subtable->shift); nodelist = subtable->nodelist; previousP = &(nodelist[pos]); looking = *previousP; @@ -1205,7 +1214,7 @@ cuddUniqueInter( /* Update pointer to insertion point. In the case of rehashing, ** the slot may have changed. In the case of garbage collection, ** the predecessor may have been dead. */ - pos = ddHash(T, E, subtable->shift); + pos = ddHash(cuddF2L(T), cuddF2L(E), subtable->shift); nodelist = subtable->nodelist; previousP = &(nodelist[pos]); looking = *previousP; @@ -1236,7 +1245,7 @@ cuddUniqueInter( if (gcNumber != unique->garbageCollections) { DdNode *looking2; - pos = ddHash(T, E, subtable->shift); + pos = ddHash(cuddF2L(T), cuddF2L(E), subtable->shift); nodelist = subtable->nodelist; previousP = &(nodelist[pos]); looking2 = *previousP; @@ -1268,6 +1277,8 @@ cuddUniqueInter( cuddCheckCollisionOrdering(unique,level,pos); #endif +// assert( Cudd_Regular(T)->Id < 100000000 ); +// assert( Cudd_Regular(E)->Id < 100000000 ); return(looking); } /* end of cuddUniqueInter */ @@ -1367,7 +1378,7 @@ cuddUniqueInterZdd( } } - pos = ddHash(T, E, subtable->shift); + pos = ddHash(cuddF2L(T), cuddF2L(E), subtable->shift); nodelist = subtable->nodelist; looking = nodelist[pos]; @@ -1594,7 +1605,7 @@ cuddRehash( oddP = &(nodelist[(j<<1)+1]); while (node != sentinel) { next = node->next; - pos = ddHash(cuddT(node), cuddE(node), shift); + pos = ddHash(cuddF2L(cuddT(node)), cuddF2L(cuddE(node)), shift); if (pos & 1) { *oddP = node; oddP = &(node->next); @@ -1731,7 +1742,7 @@ cuddShrinkSubtable( DdNode *looking, *T, *E; DdNodePtr *previousP; next = node->next; - posn = ddHash(cuddT(node), cuddE(node), shift); + posn = ddHash(cuddF2L(cuddT(node)), cuddF2L(cuddE(node)), shift); previousP = &(nodelist[posn]); looking = *previousP; T = cuddT(node); @@ -2472,7 +2483,7 @@ ddRehashZdd( node = oldnodelist[j]; while (node != NULL) { next = node->next; - pos = ddHash(cuddT(node), cuddE(node), shift); + pos = ddHash(cuddF2L(cuddT(node)), cuddF2L(cuddE(node)), shift); node->next = nodelist[pos]; nodelist[pos] = node; node = next; diff --git a/src/bdd/cudd/cuddUtil.c b/src/bdd/cudd/cuddUtil.c index 80577366..ec21e928 100644 --- a/src/bdd/cudd/cuddUtil.c +++ b/src/bdd/cudd/cuddUtil.c @@ -3361,7 +3361,7 @@ cuddUniqueLookup( assert(level < (unsigned) cuddI(unique,Cudd_Regular(E)->index)); #endif - posn = ddHash(T, E, subtable->shift); + posn = ddHash(cuddF2L(T), cuddF2L(E), subtable->shift); nodelist = subtable->nodelist; looking = nodelist[posn]; diff --git a/src/bdd/cudd/cuddZddLin.c b/src/bdd/cudd/cuddZddLin.c index 0c364413..c6e11561 100644 --- a/src/bdd/cudd/cuddZddLin.c +++ b/src/bdd/cudd/cuddZddLin.c @@ -353,7 +353,7 @@ cuddZddLinearInPlace( ** eventually be moved or garbage collected. No node ** re-expression will add a pointer to it. */ - posn = ddHash(f11, f0, yshift); + posn = ddHash(cuddF2L(f11), cuddF2L(f0), yshift); f->next = ylist[posn]; ylist[posn] = f; newykeys++; @@ -388,7 +388,7 @@ cuddZddLinearInPlace( cuddSatInc(newf1->ref); } else { /* Check ylist for triple (yindex, f01, f10). */ - posn = ddHash(f01, f10, yshift); + posn = ddHash(cuddF2L(f01), cuddF2L(f10), yshift); /* For each element newf1 in collision list ylist[posn]. */ newf1 = ylist[posn]; /* Search the collision chain skipping the marked nodes. */ @@ -426,7 +426,7 @@ cuddZddLinearInPlace( cuddSatInc(newf0->ref); } else { /* Check ylist for triple (yindex, f11, f00). */ - posn = ddHash(f11, f00, yshift); + posn = ddHash(cuddF2L(f11), cuddF2L(f00), yshift); /* For each element newf0 in collision list ylist[posn]. */ newf0 = ylist[posn]; while (newf0 != NULL) { @@ -459,7 +459,7 @@ cuddZddLinearInPlace( ** The modified f does not already exists in xlist. ** (Because of the uniqueness of the cofactors.) */ - posn = ddHash(newf1, newf0, xshift); + posn = ddHash(cuddF2L(newf1), cuddF2L(newf0), xshift); newxkeys++; f->next = xlist[posn]; xlist[posn] = f; @@ -491,7 +491,7 @@ cuddZddLinearInPlace( f1 = cuddT(f); cuddSatDec(f1->ref); /* Check ylist for triple (yindex, f1, empty). */ - posn = ddHash(f1, empty, yshift); + posn = ddHash(cuddF2L(f1), cuddF2L(empty), yshift); /* For each element newf1 in collision list ylist[posn]. */ newf1 = ylist[posn]; while (newf1 != NULL) { @@ -522,7 +522,7 @@ cuddZddLinearInPlace( cuddT(f) = newf1; f0 = cuddE(f); /* Insert f in x list. */ - posn = ddHash(newf1, f0, xshift); + posn = ddHash(cuddF2L(newf1), cuddF2L(f0), xshift); newxkeys++; newykeys--; f->next = xlist[posn]; diff --git a/src/bdd/cudd/cuddZddReord.c b/src/bdd/cudd/cuddZddReord.c index 80e3601c..c5fcb9fb 100644 --- a/src/bdd/cudd/cuddZddReord.c +++ b/src/bdd/cudd/cuddZddReord.c @@ -592,7 +592,7 @@ cuddZddSwapInPlace( */ } else { /* Check xlist for triple (xindex, f11, f01). */ - posn = ddHash(f11, f01, xshift); + posn = ddHash(cuddF2L(f11), cuddF2L(f01), xshift); /* For each element newf1 in collision list xlist[posn]. */ newf1 = xlist[posn]; while (newf1 != NULL) { @@ -630,7 +630,7 @@ cuddZddSwapInPlace( cuddSatInc(newf0->ref); } else { /* Check xlist for triple (xindex, f10, f00). */ - posn = ddHash(f10, f00, xshift); + posn = ddHash(cuddF2L(f10), cuddF2L(f00), xshift); /* For each element newf0 in collision list xlist[posn]. */ newf0 = xlist[posn]; while (newf0 != NULL) { @@ -662,7 +662,7 @@ cuddZddSwapInPlace( ** The modified f does not already exists in ylist. ** (Because of the uniqueness of the cofactors.) */ - posn = ddHash(newf1, newf0, yshift); + posn = ddHash(cuddF2L(newf1), cuddF2L(newf0), yshift); newykeys++; f->next = ylist[posn]; ylist[posn] = f; @@ -1456,7 +1456,7 @@ zddReorderPostprocess( ** nodes with zero reference count; hence lower probability of finding ** a result in the cache. */ - if (table->reclaimed > table->allocated * 0.5) return(1); + if (table->reclaimed > table->allocated / 2) return(1); /* Resize subtables. */ for (i = 0; i < table->sizeZ; i++) { @@ -1491,7 +1491,7 @@ zddReorderPostprocess( node = oldnodelist[j]; while (node != NULL) { next = node->next; - posn = ddHash(cuddT(node), cuddE(node), shift); + posn = ddHash(cuddF2L(cuddT(node)), cuddF2L(cuddE(node)), shift); node->next = nodelist[posn]; nodelist[posn] = node; node = next; -- cgit v1.2.3