luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Another attempt to make CUDD platform- and runtime-independent.

This commit is contained in:
Alan Mishchenko 2011-12-06 17:48:31 -08:00
parent 7cce97b4b3
commit 780321cf54
18 changed files with 171 additions and 91 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
src/bdd/cudd/cudd.h
View File

@ -283,6 +283,7 @@ struct DdNode {
CUDD_VALUE_TYPE value; /* for constant nodes */ CUDD_VALUE_TYPE value; /* for constant nodes */
DdChildren kids; /* for internal nodes */ DdChildren kids; /* for internal nodes */
} type; } type;
ABC_INT64_T Id;
}; };
#ifdef __osf__ #ifdef __osf__

3
src/bdd/cudd/cuddAPI.c
View File

@ -3067,8 +3067,7 @@ Cudd_PrintInfo(
if (retval == EOF) return(0); if (retval == EOF) return(0);
retval = fprintf(fp,"Number of dead ZDD nodes: %u\n", dd->deadZ); retval = fprintf(fp,"Number of dead ZDD nodes: %u\n", dd->deadZ);
if (retval == EOF) return(0); if (retval == EOF) return(0);
retval = fprintf(fp,"Total number of nodes allocated: %.0f\n", retval = fprintf(fp,"Total number of nodes allocated: %d\n", dd->allocated);
dd->allocated);
if (retval == EOF) return(0); if (retval == EOF) return(0);
retval = fprintf(fp,"Total number of nodes reclaimed: %.0f\n", retval = fprintf(fp,"Total number of nodes reclaimed: %.0f\n",
dd->reclaimed); dd->reclaimed);

2
src/bdd/cudd/cuddAndAbs.c
View File

@ -259,7 +259,7 @@ cuddBddAndAbstractRecur(
} }
} }
if ( manager->TimeStop && manager->TimeStop < time(NULL) ) if ( manager->TimeStop && manager->TimeStop < clock() )
return NULL; return NULL;
if (topf == top) { if (topf == top) {

2
src/bdd/cudd/cuddBddAbs.c
View File

@ -500,7 +500,7 @@ cuddBddXorExistAbstractRecur(
/* At this point f, g, and cube are not constant. */ /* 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; DdNode *tmp = f;
f = g; f = g;
g = tmp; g = tmp;

4
src/bdd/cudd/cuddBddCorr.c
View File

@ -258,7 +258,7 @@ bddCorrelationAux(
** (f EXNOR g) = (g EXNOR f) ** (f EXNOR g) = (g EXNOR f)
** (f' EXNOR g') = (f EXNOR g). ** (f' EXNOR g') = (f EXNOR g).
*/ */
if (f > g) { if (cuddF2L(f) > cuddF2L(g)) {
DdNode *tmp = f; DdNode *tmp = f;
f = g; g = tmp; f = g; g = tmp;
} }
@ -361,7 +361,7 @@ bddCorrelationWeightsAux(
** (f EXNOR g) = (g EXNOR f) ** (f EXNOR g) = (g EXNOR f)
** (f' EXNOR g') = (f EXNOR g). ** (f' EXNOR g') = (f EXNOR g).
*/ */
if (f > g) { if (cuddF2L(f) > cuddF2L(g)) {
DdNode *tmp = f; DdNode *tmp = f;
f = g; g = tmp; f = g; g = tmp;
} }

16
src/bdd/cudd/cuddBddIte.c
View File

@ -556,7 +556,7 @@ Cudd_bddLeq(
tmp = g; tmp = g;
g = Cudd_Not(f); g = Cudd_Not(f);
f = Cudd_Not(tmp); f = Cudd_Not(tmp);
} else if (Cudd_IsComplement(f) && g < f) { } else if (Cudd_IsComplement(f) && cuddF2L(g) < cuddF2L(f)) {
tmp = g; tmp = g;
g = Cudd_Not(f); g = Cudd_Not(f);
f = Cudd_Not(tmp); f = Cudd_Not(tmp);
@ -789,7 +789,7 @@ cuddBddIntersectRecur(
if (f == one) return(g); if (f == one) return(g);
/* At this point f and g are not constant. */ /* 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); res = cuddCacheLookup2(dd,Cudd_bddIntersect,f,g);
if (res != NULL) return(res); if (res != NULL) return(res);
@ -912,7 +912,7 @@ cuddBddAndRecur(
} }
/* At this point f and g are not constant. */ /* 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; DdNode *tmp = f;
f = g; f = g;
g = tmp; g = tmp;
@ -926,7 +926,7 @@ cuddBddAndRecur(
if (r != NULL) return(r); if (r != NULL) return(r);
} }
if ( manager->TimeStop && manager->TimeStop < time(NULL) ) if ( manager->TimeStop && manager->TimeStop < clock() )
return NULL; return NULL;
/* Here we can skip the use of cuddI, because the operands are known /* Here we can skip the use of cuddI, because the operands are known
@ -1030,7 +1030,7 @@ cuddBddXorRecur(
/* Terminal cases. */ /* Terminal cases. */
if (f == g) return(zero); if (f == g) return(zero);
if (f == Cudd_Not(g)) return(one); 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; DdNode *tmp = f;
f = g; f = g;
g = tmp; g = tmp;
@ -1197,7 +1197,7 @@ bddVarToCanonical(
change = 0; change = 0;
if (G == one) { /* ITE(F,c,H) */ 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; r = h;
h = f; h = f;
f = r; /* ITE(F,1,H) = ITE(H,1,F) */ f = r; /* ITE(F,1,H) = ITE(H,1,F) */
@ -1208,7 +1208,7 @@ bddVarToCanonical(
change = 1; change = 1;
} }
} else if (H == one) { /* ITE(F,G,c) */ } 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; r = g;
g = f; g = f;
f = r; /* ITE(F,G,0) = ITE(G,F,0) */ f = r; /* ITE(F,G,0) = ITE(G,F,0) */
@ -1219,7 +1219,7 @@ bddVarToCanonical(
change = 1; change = 1;
} }
} else if (g == Cudd_Not(h)) { /* ITE(F,G,!G) = ITE(G,F,!F) */ } 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; r = f;
f = g; f = g;
g = r; g = r;

4
src/bdd/cudd/cuddBridge.c
View File

@ -976,9 +976,9 @@ cuddBddTransferRecur(
if (st_lookup(table, (const char *)f, (char **)&res)) if (st_lookup(table, (const char *)f, (char **)&res))
return(Cudd_NotCond(res,comple)); return(Cudd_NotCond(res,comple));
if ( ddS->TimeStop && ddS->TimeStop < time(NULL) ) if ( ddS->TimeStop && ddS->TimeStop < clock() )
return NULL; return NULL;
if ( ddD->TimeStop && ddD->TimeStop < time(NULL) ) if ( ddD->TimeStop && ddD->TimeStop < clock() )
return NULL; return NULL;
/* Recursive step. */ /* Recursive step. */

84
src/bdd/cudd/cuddCache.c
View File

@ -149,7 +149,8 @@ cuddInitCache(
** initial cache size. */ ** initial cache size. */
logSize = cuddComputeFloorLog2(ddMax(cacheSize,unique->slots/2)); logSize = cuddComputeFloorLog2(ddMax(cacheSize,unique->slots/2));
cacheSize = 1 << logSize; 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) { if (unique->acache == NULL) {
unique->errorCode = CUDD_MEMORY_OUT; unique->errorCode = CUDD_MEMORY_OUT;
return(0); return(0);
@ -162,10 +163,13 @@ cuddInitCache(
unique->memused += (cacheSize) * sizeof(DdCache); unique->memused += (cacheSize) * sizeof(DdCache);
#else #else
mem = (DdNodePtr *) unique->acache; mem = (DdNodePtr *) unique->acache;
offset = (ptruint) mem & (sizeof(DdCache) - 1); // offset = (ptruint) mem & (sizeof(DdCache) - 1);
mem += (sizeof(DdCache) - offset) / sizeof(DdNodePtr); // mem += (sizeof(DdCache) - offset) / sizeof(DdNodePtr);
offset = (ptruint) mem & (32 - 1);
mem += (32 - offset) / sizeof(DdNodePtr);
unique->cache = (DdCache *) mem; 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); unique->memused += (cacheSize+1) * sizeof(DdCache);
#endif #endif
unique->cacheSlots = cacheSize; unique->cacheSlots = cacheSize;
@ -224,14 +228,22 @@ cuddCacheInsert(
DdNode * data) DdNode * data)
{ {
int posn; int posn;
unsigned hash;
register DdCache *entry; register DdCache *entry;
ptruint uf, ug, uh; ptruint uf, ug, uh;
ptruint ufc, ugc, uhc;
uf = (ptruint) f | (op & 0xe); uf = (ptruint) f | (op & 0xe);
ug = (ptruint) g | (op >> 4); ug = (ptruint) g | (op >> 4);
uh = (ptruint) h; 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]; entry = &table->cache[posn];
table->cachecollisions += entry->data != NULL; table->cachecollisions += entry->data != NULL;
@ -244,6 +256,7 @@ cuddCacheInsert(
#ifdef DD_CACHE_PROFILE #ifdef DD_CACHE_PROFILE
entry->count++; entry->count++;
#endif #endif
entry->hash = hash;
} /* end of cuddCacheInsert */ } /* end of cuddCacheInsert */
@ -269,9 +282,12 @@ cuddCacheInsert2(
DdNode * data) DdNode * data)
{ {
int posn; int posn;
unsigned hash;
register DdCache *entry; 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]; entry = &table->cache[posn];
if (entry->data != NULL) { if (entry->data != NULL) {
@ -286,6 +302,7 @@ cuddCacheInsert2(
#ifdef DD_CACHE_PROFILE #ifdef DD_CACHE_PROFILE
entry->count++; entry->count++;
#endif #endif
entry->hash = hash;
} /* end of cuddCacheInsert2 */ } /* end of cuddCacheInsert2 */
@ -310,9 +327,12 @@ cuddCacheInsert1(
DdNode * data) DdNode * data)
{ {
int posn; int posn;
unsigned hash;
register DdCache *entry; 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]; entry = &table->cache[posn];
if (entry->data != NULL) { if (entry->data != NULL) {
@ -327,6 +347,7 @@ cuddCacheInsert1(
#ifdef DD_CACHE_PROFILE #ifdef DD_CACHE_PROFILE
entry->count++; entry->count++;
#endif #endif
entry->hash = hash;
} /* end of cuddCacheInsert1 */ } /* end of cuddCacheInsert1 */
@ -356,11 +377,16 @@ cuddCacheLookup(
DdCache *en,*cache; DdCache *en,*cache;
DdNode *data; DdNode *data;
ptruint uf, ug, uh; ptruint uf, ug, uh;
ptruint ufc, ugc, uhc;
uf = (ptruint) f | (op & 0xe); uf = (ptruint) f | (op & 0xe);
ug = (ptruint) g | (op >> 4); ug = (ptruint) g | (op >> 4);
uh = (ptruint) h; uh = (ptruint) h;
ufc = (ptruint) cuddF2L(f) | (op & 0xe);
ugc = (ptruint) cuddF2L(g) | (op >> 4);
uhc = (ptruint) cuddF2L(h);
cache = table->cache; cache = table->cache;
#ifdef DD_DEBUG #ifdef DD_DEBUG
if (cache == NULL) { if (cache == NULL) {
@ -368,10 +394,9 @@ cuddCacheLookup(
} }
#endif #endif
posn = ddCHash2(uh,uf,ug,table->cacheShift); posn = ddCHash2(uhc,ufc,ugc,table->cacheShift);
en = &cache[posn]; en = &cache[posn];
if (en->data != NULL && en->f==(DdNodePtr)uf && en->g==(DdNodePtr)ug && if (en->data != NULL && en->f==(DdNodePtr)uf && en->g==(DdNodePtr)ug && en->h==uh) {
en->h==uh) {
data = Cudd_Regular(en->data); data = Cudd_Regular(en->data);
table->cacheHits++; table->cacheHits++;
if (data->ref == 0) { if (data->ref == 0) {
@ -418,11 +443,16 @@ cuddCacheLookupZdd(
DdCache *en,*cache; DdCache *en,*cache;
DdNode *data; DdNode *data;
ptruint uf, ug, uh; ptruint uf, ug, uh;
ptruint ufc, ugc, uhc;
uf = (ptruint) f | (op & 0xe); uf = (ptruint) f | (op & 0xe);
ug = (ptruint) g | (op >> 4); ug = (ptruint) g | (op >> 4);
uh = (ptruint) h; uh = (ptruint) h;
ufc = (ptruint) cuddF2L(f) | (op & 0xe);
ugc = (ptruint) cuddF2L(g) | (op >> 4);
uhc = (ptruint) cuddF2L(h);
cache = table->cache; cache = table->cache;
#ifdef DD_DEBUG #ifdef DD_DEBUG
if (cache == NULL) { if (cache == NULL) {
@ -430,7 +460,7 @@ cuddCacheLookupZdd(
} }
#endif #endif
posn = ddCHash2(uh,uf,ug,table->cacheShift); posn = ddCHash2(uhc,ufc,ugc,table->cacheShift);
en = &cache[posn]; en = &cache[posn];
if (en->data != NULL && en->f==(DdNodePtr)uf && en->g==(DdNodePtr)ug && if (en->data != NULL && en->f==(DdNodePtr)uf && en->g==(DdNodePtr)ug &&
en->h==uh) { en->h==uh) {
@ -486,7 +516,7 @@ cuddCacheLookup2(
} }
#endif #endif
posn = ddCHash2(op,f,g,table->cacheShift); posn = ddCHash2(op,cuddF2L(f),cuddF2L(g),table->cacheShift);
en = &cache[posn]; en = &cache[posn];
if (en->data != NULL && en->f==f && en->g==g && en->h==(ptruint)op) { if (en->data != NULL && en->f==f && en->g==g && en->h==(ptruint)op) {
data = Cudd_Regular(en->data); data = Cudd_Regular(en->data);
@ -539,7 +569,7 @@ cuddCacheLookup1(
} }
#endif #endif
posn = ddCHash2(op,f,f,table->cacheShift); posn = ddCHash2(op,cuddF2L(f),cuddF2L(f),table->cacheShift);
en = &cache[posn]; en = &cache[posn];
if (en->data != NULL && en->f==f && en->h==(ptruint)op) { if (en->data != NULL && en->f==f && en->h==(ptruint)op) {
data = Cudd_Regular(en->data); data = Cudd_Regular(en->data);
@ -594,7 +624,7 @@ cuddCacheLookup2Zdd(
} }
#endif #endif
posn = ddCHash2(op,f,g,table->cacheShift); posn = ddCHash2(op,cuddF2L(f),cuddF2L(g),table->cacheShift);
en = &cache[posn]; en = &cache[posn];
if (en->data != NULL && en->f==f && en->g==g && en->h==(ptruint)op) { if (en->data != NULL && en->f==f && en->g==g && en->h==(ptruint)op) {
data = Cudd_Regular(en->data); data = Cudd_Regular(en->data);
@ -647,7 +677,7 @@ cuddCacheLookup1Zdd(
} }
#endif #endif
posn = ddCHash2(op,f,f,table->cacheShift); posn = ddCHash2(op,cuddF2L(f),cuddF2L(f),table->cacheShift);
en = &cache[posn]; en = &cache[posn];
if (en->data != NULL && en->f==f && en->h==(ptruint)op) { if (en->data != NULL && en->f==f && en->h==(ptruint)op) {
data = Cudd_Regular(en->data); data = Cudd_Regular(en->data);
@ -698,18 +728,23 @@ cuddConstantLookup(
int posn; int posn;
DdCache *en,*cache; DdCache *en,*cache;
ptruint uf, ug, uh; ptruint uf, ug, uh;
ptruint ufc, ugc, uhc;
uf = (ptruint) f | (op & 0xe); uf = (ptruint) f | (op & 0xe);
ug = (ptruint) g | (op >> 4); ug = (ptruint) g | (op >> 4);
uh = (ptruint) h; uh = (ptruint) h;
ufc = (ptruint) cuddF2L(f) | (op & 0xe);
ugc = (ptruint) cuddF2L(g) | (op >> 4);
uhc = (ptruint) cuddF2L(h);
cache = table->cache; cache = table->cache;
#ifdef DD_DEBUG #ifdef DD_DEBUG
if (cache == NULL) { if (cache == NULL) {
return(NULL); return(NULL);
} }
#endif #endif
posn = ddCHash2(uh,uf,ug,table->cacheShift); posn = ddCHash2(uhc,ufc,ugc,table->cacheShift);
en = &cache[posn]; en = &cache[posn];
/* We do not reclaim here because the result should not be /* We do not reclaim here because the result should not be
@ -919,7 +954,8 @@ cuddCacheResize(
saveHandler = MMoutOfMemory; saveHandler = MMoutOfMemory;
MMoutOfMemory = Cudd_OutOfMem; 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; MMoutOfMemory = saveHandler;
/* If we fail to allocate the new table we just give up. */ /* If we fail to allocate the new table we just give up. */
if (cache == NULL) { if (cache == NULL) {
@ -940,10 +976,14 @@ cuddCacheResize(
table->cache = cache; table->cache = cache;
#else #else
mem = (DdNodePtr *) cache; mem = (DdNodePtr *) cache;
misalignment = (ptruint) mem & (sizeof(DdCache) - 1); // misalignment = (ptruint) mem & (sizeof(DdCache) - 1);
mem += (sizeof(DdCache) - misalignment) / sizeof(DdNodePtr); // 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; table->cache = cache = (DdCache *) mem;
assert(((ptruint) table->cache & (sizeof(DdCache) - 1)) == 0); assert(((ptruint) table->cache & (32 - 1)) == 0);
#endif #endif
shift = --(table->cacheShift); shift = --(table->cacheShift);
table->memused += (slots - oldslots) * sizeof(DdCache); table->memused += (slots - oldslots) * sizeof(DdCache);
@ -962,7 +1002,8 @@ cuddCacheResize(
for (i = 0; (unsigned) i < oldslots; i++) { for (i = 0; (unsigned) i < oldslots; i++) {
old = &oldcache[i]; old = &oldcache[i];
if (old->data != NULL) { 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 = &cache[posn];
entry->f = old->f; entry->f = old->f;
entry->g = old->g; entry->g = old->g;
@ -971,6 +1012,7 @@ cuddCacheResize(
#ifdef DD_CACHE_PROFILE #ifdef DD_CACHE_PROFILE
entry->count = 1; entry->count = 1;
#endif #endif
entry->hash = old->hash;
moved++; moved++;
} }
} }

2
src/bdd/cudd/cuddCompose.c
View File

@ -1251,7 +1251,7 @@ cuddBddVarMapRecur(
return(Cudd_NotCond(res,F != f)); return(Cudd_NotCond(res,F != f));
} }
if ( manager->TimeStop && manager->TimeStop < time(NULL) ) if ( manager->TimeStop && manager->TimeStop < clock() )
return NULL; return NULL;
/* Split and recur on children of this node. */ /* Split and recur on children of this node. */

26
src/bdd/cudd/cuddInt.h
View File

@ -315,6 +315,7 @@ typedef struct DdCache {
#ifdef DD_CACHE_PROFILE #ifdef DD_CACHE_PROFILE
ptrint count; ptrint count;
#endif #endif
unsigned hash;
} DdCache; } DdCache;
typedef struct DdSubtable { /* subtable for one index */ typedef struct DdSubtable { /* subtable for one index */
@ -372,7 +373,8 @@ struct DdManager { /* specialized DD symbol table */
/* (measured w.r.t. slots, not keys) */ /* (measured w.r.t. slots, not keys) */
unsigned int initSlots; /* initial size of a subtable */ unsigned int initSlots; /* initial size of a subtable */
DdNode **stack; /* stack for iterative procedures */ 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) */ /* (not during reordering) */
double reclaimed; /* number of nodes brought back from the dead */ double reclaimed; /* number of nodes brought back from the dead */
int isolated; /* isolated projection functions */ 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)]) #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*********************************************************************** /**Macro***********************************************************************
Synopsis [Hash function for the unique table.] Synopsis [Hash function for the unique table.]
@ -729,6 +745,7 @@ typedef struct DdLevelQueue {
SeeAlso [ddHash ddCHash2] SeeAlso [ddHash ddCHash2]
******************************************************************************/ ******************************************************************************/
/*
#if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4 #if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4
#define ddCHash(o,f,g,h,s) \ #define ddCHash(o,f,g,h,s) \
((((((unsigned)(ptruint)(f) + (unsigned)(ptruint)(o)) * DD_P1 + \ ((((((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)(f) + (unsigned)(o)) * DD_P1 + (unsigned)(g)) * DD_P2 + \
(unsigned)(h)) * DD_P3) >> (s)) (unsigned)(h)) * DD_P3) >> (s))
#endif #endif
*/
/**Macro*********************************************************************** /**Macro***********************************************************************
@ -757,9 +774,14 @@ typedef struct DdLevelQueue {
#define ddCHash2(o,f,g,s) \ #define ddCHash2(o,f,g,s) \
(((((unsigned)(ptruint)(f) + (unsigned)(ptruint)(o)) * DD_P1 + \ (((((unsigned)(ptruint)(f) + (unsigned)(ptruint)(o)) * DD_P1 + \
(unsigned)(ptruint)(g)) * DD_P2) >> (s)) (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 #else
#define ddCHash2(o,f,g,s) \ #define ddCHash2(o,f,g,s) \
(((((unsigned)(f) + (unsigned)(o)) * DD_P1 + (unsigned)(g)) * DD_P2) >> (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 #endif

18
src/bdd/cudd/cuddLCache.c
View File

@ -789,7 +789,7 @@ cuddHashTableInsert1(
cuddRef(value); cuddRef(value);
item->count = count; item->count = count;
item->key[0] = f; item->key[0] = f;
posn = ddLCHash2(f,f,hash->shift); posn = ddLCHash2(cuddF2L(f),cuddF2L(f),hash->shift);
item->next = hash->bucket[posn]; item->next = hash->bucket[posn];
hash->bucket[posn] = item; hash->bucket[posn] = item;
@ -827,7 +827,7 @@ cuddHashTableLookup1(
assert(hash->keysize == 1); assert(hash->keysize == 1);
#endif #endif
posn = ddLCHash2(f,f,hash->shift); posn = ddLCHash2(cuddF2L(f),cuddF2L(f),hash->shift);
item = hash->bucket[posn]; item = hash->bucket[posn];
prev = NULL; prev = NULL;
@ -898,7 +898,7 @@ cuddHashTableInsert2(
item->count = count; item->count = count;
item->key[0] = f; item->key[0] = f;
item->key[1] = g; item->key[1] = g;
posn = ddLCHash2(f,g,hash->shift); posn = ddLCHash2(cuddF2L(f),cuddF2L(g),hash->shift);
item->next = hash->bucket[posn]; item->next = hash->bucket[posn];
hash->bucket[posn] = item; hash->bucket[posn] = item;
@ -937,7 +937,7 @@ cuddHashTableLookup2(
assert(hash->keysize == 2); assert(hash->keysize == 2);
#endif #endif
posn = ddLCHash2(f,g,hash->shift); posn = ddLCHash2(cuddF2L(f),cuddF2L(g),hash->shift);
item = hash->bucket[posn]; item = hash->bucket[posn];
prev = NULL; prev = NULL;
@ -1010,7 +1010,7 @@ cuddHashTableInsert3(
item->key[0] = f; item->key[0] = f;
item->key[1] = g; item->key[1] = g;
item->key[2] = h; 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]; item->next = hash->bucket[posn];
hash->bucket[posn] = item; hash->bucket[posn] = item;
@ -1050,7 +1050,7 @@ cuddHashTableLookup3(
assert(hash->keysize == 3); assert(hash->keysize == 3);
#endif #endif
posn = ddLCHash3(f,g,h,hash->shift); posn = ddLCHash3(cuddF2L(f),cuddF2L(g),cuddF2L(h),hash->shift);
item = hash->bucket[posn]; item = hash->bucket[posn];
prev = NULL; prev = NULL;
@ -1326,7 +1326,7 @@ cuddHashTableResize(
while (item != NULL) { while (item != NULL) {
next = item->next; next = item->next;
key = item->key; key = item->key;
posn = ddLCHash2(key[0], key[0], shift); posn = ddLCHash2(cuddF2L(key[0]), cuddF2L(key[0]), shift);
item->next = buckets[posn]; item->next = buckets[posn];
buckets[posn] = item; buckets[posn] = item;
item = next; item = next;
@ -1338,7 +1338,7 @@ cuddHashTableResize(
while (item != NULL) { while (item != NULL) {
next = item->next; next = item->next;
key = item->key; key = item->key;
posn = ddLCHash2(key[0], key[1], shift); posn = ddLCHash2(cuddF2L(key[0]), cuddF2L(key[1]), shift);
item->next = buckets[posn]; item->next = buckets[posn];
buckets[posn] = item; buckets[posn] = item;
item = next; item = next;
@ -1350,7 +1350,7 @@ cuddHashTableResize(
while (item != NULL) { while (item != NULL) {
next = item->next; next = item->next;
key = item->key; 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]; item->next = buckets[posn];
buckets[posn] = item; buckets[posn] = item;
item = next; item = next;

6
src/bdd/cudd/cuddLinear.c
View File

@ -496,7 +496,7 @@ cuddLinearInPlace(
cuddSatInc(newf1->ref); cuddSatInc(newf1->ref);
} else { } else {
/* Check ylist for triple (yindex,f11,f00). */ /* 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]. */ /* For each element newf1 in collision list ylist[posn]. */
previousP = &(ylist[posn]); previousP = &(ylist[posn]);
newf1 = *previousP; newf1 = *previousP;
@ -550,7 +550,7 @@ cuddLinearInPlace(
f10 = Cudd_Not(f10); f10 = Cudd_Not(f10);
} }
/* Check ylist for triple (yindex,f01,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]. */ /* For each element newf0 in collision list ylist[posn]. */
previousP = &(ylist[posn]); previousP = &(ylist[posn]);
newf0 = *previousP; newf0 = *previousP;
@ -591,7 +591,7 @@ cuddLinearInPlace(
** The modified f does not already exists in xlist. ** The modified f does not already exists in xlist.
** (Because of the uniqueness of the cofactors.) ** (Because of the uniqueness of the cofactors.)
*/ */
posn = ddHash(newf1, newf0, xshift); posn = ddHash(cuddF2L(newf1), cuddF2L(newf0), xshift);
newxkeys++; newxkeys++;
previousP = &(xlist[posn]); previousP = &(xlist[posn]);
tmp = *previousP; tmp = *previousP;

23
src/bdd/cudd/cuddReorder.c
View File

@ -416,7 +416,8 @@ cuddDynamicAllocNode(
/* Try to allocate a new block. */ /* Try to allocate a new block. */
saveHandler = MMoutOfMemory; saveHandler = MMoutOfMemory;
MMoutOfMemory = Cudd_OutOfMem; 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; MMoutOfMemory = saveHandler;
if (mem == NULL && table->stash != NULL) { if (mem == NULL && table->stash != NULL) {
ABC_FREE(table->stash); ABC_FREE(table->stash);
@ -427,7 +428,8 @@ cuddDynamicAllocNode(
for (i = 0; i < table->size; i++) { for (i = 0; i < table->size; i++) {
table->subtables[i].maxKeys <<= 2; 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) { if (mem == NULL) {
/* Out of luck. Call the default handler to do /* 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. ** power of 2 and a multiple of the size of a pointer.
** If we align one node, all the others will be aligned ** If we align one node, all the others will be aligned
** as well. */ ** as well. */
offset = (unsigned long) mem & (sizeof(DdNode) - 1); // offset = (unsigned long) mem & (sizeof(DdNode) - 1);
mem += (sizeof(DdNode) - offset) / sizeof(DdNodePtr); // mem += (sizeof(DdNode) - offset) / sizeof(DdNodePtr);
offset = (unsigned long) mem & (32 - 1);
mem += (32 - offset) / sizeof(DdNodePtr);
#ifdef DD_DEBUG #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 #endif
list = (DdNode *) mem; list = (DdNode *) mem;
@ -927,7 +932,7 @@ cuddSwapInPlace(
f1 = cuddT(f); f1 = cuddT(f);
f0 = cuddE(f); f0 = cuddE(f);
/* Check xlist for pair (f11,f01). */ /* 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]. */ /* For each element tmp in collision list xlist[posn]. */
previousP = &(xlist[posn]); previousP = &(xlist[posn]);
tmp = *previousP; tmp = *previousP;
@ -988,7 +993,7 @@ cuddSwapInPlace(
cuddSatInc(newf1->ref); cuddSatInc(newf1->ref);
} else { } else {
/* Check xlist for triple (xindex,f11,f01). */ /* 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]. */ /* For each element newf1 in collision list xlist[posn]. */
previousP = &(xlist[posn]); previousP = &(xlist[posn]);
newf1 = *previousP; newf1 = *previousP;
@ -1042,7 +1047,7 @@ cuddSwapInPlace(
f00 = Cudd_Not(f00); f00 = Cudd_Not(f00);
} }
/* Check xlist for triple (xindex,f10,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]. */ /* For each element newf0 in collision list xlist[posn]. */
previousP = &(xlist[posn]); previousP = &(xlist[posn]);
newf0 = *previousP; newf0 = *previousP;
@ -1083,7 +1088,7 @@ cuddSwapInPlace(
** The modified f does not already exists in ylist. ** The modified f does not already exists in ylist.
** (Because of the uniqueness of the cofactors.) ** (Because of the uniqueness of the cofactors.)
*/ */
posn = ddHash(newf1, newf0, yshift); posn = ddHash(cuddF2L(newf1), cuddF2L(newf0), yshift);
newykeys++; newykeys++;
previousP = &(ylist[posn]); previousP = &(ylist[posn]);
tmp = *previousP; tmp = *previousP;

2
src/bdd/cudd/cuddSymmetry.c
View File

@ -367,7 +367,7 @@ cuddSymmSifting(
if (ddTotalNumberSwapping >= table->siftMaxSwap) if (ddTotalNumberSwapping >= table->siftMaxSwap)
break; break;
// enable timeout during variable reodering - alanmi 2/13/11 // enable timeout during variable reodering - alanmi 2/13/11
if ( table->TimeStop && table->TimeStop < time(NULL) ) if ( table->TimeStop && table->TimeStop < clock() )
break; break;
x = table->perm[var[i]]; x = table->perm[var[i]];
#ifdef DD_STATS #ifdef DD_STATS

43
src/bdd/cudd/cuddTable.c
View File

@ -260,7 +260,8 @@ cuddAllocNode(
/* Try to allocate a new block. */ /* Try to allocate a new block. */
saveHandler = MMoutOfMemory; saveHandler = MMoutOfMemory;
MMoutOfMemory = Cudd_OutOfMem; 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; MMoutOfMemory = saveHandler;
if (mem == NULL) { if (mem == NULL) {
/* No more memory: Try collecting garbage. If this succeeds, /* No more memory: Try collecting garbage. If this succeeds,
@ -276,7 +277,8 @@ cuddAllocNode(
/* Inhibit resizing of tables. */ /* Inhibit resizing of tables. */
cuddSlowTableGrowth(unique); cuddSlowTableGrowth(unique);
/* Now try again. */ /* 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) { if (mem == NULL) {
/* Out of luck. Call the default handler to do /* Out of luck. Call the default handler to do
@ -301,11 +303,14 @@ cuddAllocNode(
mem[0] = (DdNodePtr) unique->memoryList; mem[0] = (DdNodePtr) unique->memoryList;
unique->memoryList = mem; unique->memoryList = mem;
/* Here we rely on the fact that a DdNode is as large /* Here we rely on the fact that a DdNode is as large as 4 pointers. */
** as 4 pointers. */ // offset = (ptruint) mem & (sizeof(DdNode) - 1);
offset = (ptruint) mem & (sizeof(DdNode) - 1); // mem += (sizeof(DdNode) - offset) / sizeof(DdNodePtr);
mem += (sizeof(DdNode) - offset) / sizeof(DdNodePtr); // assert(((ptruint) mem & (sizeof(DdNode) - 1)) == 0);
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; list = (DdNode *) mem;
i = 1; i = 1;
@ -324,6 +329,7 @@ cuddAllocNode(
unique->allocated++; unique->allocated++;
node = unique->nextFree; node = unique->nextFree;
unique->nextFree = node->next; unique->nextFree = node->next;
node->Id = (unique->allocated<<4);
return(node); return(node);
} /* end of cuddAllocNode */ } /* end of cuddAllocNode */
@ -976,8 +982,11 @@ cuddGarbageCollect(
while (memListTrav != NULL) { while (memListTrav != NULL) {
ptruint offset; ptruint offset;
nxtNode = (DdNodePtr *)memListTrav[0]; nxtNode = (DdNodePtr *)memListTrav[0];
offset = (ptruint) memListTrav & (sizeof(DdNode) - 1); // offset = (ptruint) memListTrav & (sizeof(DdNode) - 1);
memListTrav += (sizeof(DdNode) - offset) / sizeof(DdNodePtr); // memListTrav += (sizeof(DdNode) - offset) / sizeof(DdNodePtr);
offset = (ptruint) memListTrav & (32 - 1);
memListTrav += (32 - offset) / sizeof(DdNodePtr);
downTrav = (DdNode *)memListTrav; downTrav = (DdNode *)memListTrav;
k = 0; k = 0;
do { do {
@ -1147,7 +1156,7 @@ cuddUniqueInter(
assert(level < (unsigned) cuddI(unique,Cudd_Regular(E)->index)); assert(level < (unsigned) cuddI(unique,Cudd_Regular(E)->index));
#endif #endif
pos = ddHash(T, E, subtable->shift); pos = ddHash(cuddF2L(T), cuddF2L(E), subtable->shift);
nodelist = subtable->nodelist; nodelist = subtable->nodelist;
previousP = &(nodelist[pos]); previousP = &(nodelist[pos]);
looking = *previousP; looking = *previousP;
@ -1205,7 +1214,7 @@ cuddUniqueInter(
/* Update pointer to insertion point. In the case of rehashing, /* Update pointer to insertion point. In the case of rehashing,
** the slot may have changed. In the case of garbage collection, ** the slot may have changed. In the case of garbage collection,
** the predecessor may have been dead. */ ** the predecessor may have been dead. */
pos = ddHash(T, E, subtable->shift); pos = ddHash(cuddF2L(T), cuddF2L(E), subtable->shift);
nodelist = subtable->nodelist; nodelist = subtable->nodelist;
previousP = &(nodelist[pos]); previousP = &(nodelist[pos]);
looking = *previousP; looking = *previousP;
@ -1236,7 +1245,7 @@ cuddUniqueInter(
if (gcNumber != unique->garbageCollections) { if (gcNumber != unique->garbageCollections) {
DdNode *looking2; DdNode *looking2;
pos = ddHash(T, E, subtable->shift); pos = ddHash(cuddF2L(T), cuddF2L(E), subtable->shift);
nodelist = subtable->nodelist; nodelist = subtable->nodelist;
previousP = &(nodelist[pos]); previousP = &(nodelist[pos]);
looking2 = *previousP; looking2 = *previousP;
@ -1268,6 +1277,8 @@ cuddUniqueInter(
cuddCheckCollisionOrdering(unique,level,pos); cuddCheckCollisionOrdering(unique,level,pos);
#endif #endif
// assert( Cudd_Regular(T)->Id < 100000000 );
// assert( Cudd_Regular(E)->Id < 100000000 );
return(looking); return(looking);
} /* end of cuddUniqueInter */ } /* 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; nodelist = subtable->nodelist;
looking = nodelist[pos]; looking = nodelist[pos];
@ -1594,7 +1605,7 @@ cuddRehash(
oddP = &(nodelist[(j<<1)+1]); oddP = &(nodelist[(j<<1)+1]);
while (node != sentinel) { while (node != sentinel) {
next = node->next; next = node->next;
pos = ddHash(cuddT(node), cuddE(node), shift); pos = ddHash(cuddF2L(cuddT(node)), cuddF2L(cuddE(node)), shift);
if (pos & 1) { if (pos & 1) {
*oddP = node; *oddP = node;
oddP = &(node->next); oddP = &(node->next);
@ -1731,7 +1742,7 @@ cuddShrinkSubtable(
DdNode *looking, *T, *E; DdNode *looking, *T, *E;
DdNodePtr *previousP; DdNodePtr *previousP;
next = node->next; next = node->next;
posn = ddHash(cuddT(node), cuddE(node), shift); posn = ddHash(cuddF2L(cuddT(node)), cuddF2L(cuddE(node)), shift);
previousP = &(nodelist[posn]); previousP = &(nodelist[posn]);
looking = *previousP; looking = *previousP;
T = cuddT(node); T = cuddT(node);
@ -2472,7 +2483,7 @@ ddRehashZdd(
node = oldnodelist[j]; node = oldnodelist[j];
while (node != NULL) { while (node != NULL) {
next = node->next; next = node->next;
pos = ddHash(cuddT(node), cuddE(node), shift); pos = ddHash(cuddF2L(cuddT(node)), cuddF2L(cuddE(node)), shift);
node->next = nodelist[pos]; node->next = nodelist[pos];
nodelist[pos] = node; nodelist[pos] = node;
node = next; node = next;

2
src/bdd/cudd/cuddUtil.c
View File

@ -3361,7 +3361,7 @@ cuddUniqueLookup(
assert(level < (unsigned) cuddI(unique,Cudd_Regular(E)->index)); assert(level < (unsigned) cuddI(unique,Cudd_Regular(E)->index));
#endif #endif
posn = ddHash(T, E, subtable->shift); posn = ddHash(cuddF2L(T), cuddF2L(E), subtable->shift);
nodelist = subtable->nodelist; nodelist = subtable->nodelist;
looking = nodelist[posn]; looking = nodelist[posn];

12
src/bdd/cudd/cuddZddLin.c
View File

@ -353,7 +353,7 @@ cuddZddLinearInPlace(
** eventually be moved or garbage collected. No node ** eventually be moved or garbage collected. No node
** re-expression will add a pointer to it. ** re-expression will add a pointer to it.
*/ */
posn = ddHash(f11, f0, yshift); posn = ddHash(cuddF2L(f11), cuddF2L(f0), yshift);
f->next = ylist[posn]; f->next = ylist[posn];
ylist[posn] = f; ylist[posn] = f;
newykeys++; newykeys++;
@ -388,7 +388,7 @@ cuddZddLinearInPlace(
cuddSatInc(newf1->ref); cuddSatInc(newf1->ref);
} else { } else {
/* Check ylist for triple (yindex, f01, f10). */ /* 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]. */ /* For each element newf1 in collision list ylist[posn]. */
newf1 = ylist[posn]; newf1 = ylist[posn];
/* Search the collision chain skipping the marked nodes. */ /* Search the collision chain skipping the marked nodes. */
@ -426,7 +426,7 @@ cuddZddLinearInPlace(
cuddSatInc(newf0->ref); cuddSatInc(newf0->ref);
} else { } else {
/* Check ylist for triple (yindex, f11, f00). */ /* 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]. */ /* For each element newf0 in collision list ylist[posn]. */
newf0 = ylist[posn]; newf0 = ylist[posn];
while (newf0 != NULL) { while (newf0 != NULL) {
@ -459,7 +459,7 @@ cuddZddLinearInPlace(
** The modified f does not already exists in xlist. ** The modified f does not already exists in xlist.
** (Because of the uniqueness of the cofactors.) ** (Because of the uniqueness of the cofactors.)
*/ */
posn = ddHash(newf1, newf0, xshift); posn = ddHash(cuddF2L(newf1), cuddF2L(newf0), xshift);
newxkeys++; newxkeys++;
f->next = xlist[posn]; f->next = xlist[posn];
xlist[posn] = f; xlist[posn] = f;
@ -491,7 +491,7 @@ cuddZddLinearInPlace(
f1 = cuddT(f); f1 = cuddT(f);
cuddSatDec(f1->ref); cuddSatDec(f1->ref);
/* Check ylist for triple (yindex, f1, empty). */ /* 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]. */ /* For each element newf1 in collision list ylist[posn]. */
newf1 = ylist[posn]; newf1 = ylist[posn];
while (newf1 != NULL) { while (newf1 != NULL) {
@ -522,7 +522,7 @@ cuddZddLinearInPlace(
cuddT(f) = newf1; cuddT(f) = newf1;
f0 = cuddE(f); f0 = cuddE(f);
/* Insert f in x list. */ /* Insert f in x list. */
posn = ddHash(newf1, f0, xshift); posn = ddHash(cuddF2L(newf1), cuddF2L(f0), xshift);
newxkeys++; newxkeys++;
newykeys--; newykeys--;
f->next = xlist[posn]; f->next = xlist[posn];

10
src/bdd/cudd/cuddZddReord.c
View File

@ -592,7 +592,7 @@ cuddZddSwapInPlace(
*/ */
} else { } else {
/* Check xlist for triple (xindex, f11, f01). */ /* 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]. */ /* For each element newf1 in collision list xlist[posn]. */
newf1 = xlist[posn]; newf1 = xlist[posn];
while (newf1 != NULL) { while (newf1 != NULL) {
@ -630,7 +630,7 @@ cuddZddSwapInPlace(
cuddSatInc(newf0->ref); cuddSatInc(newf0->ref);
} else { } else {
/* Check xlist for triple (xindex, f10, 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]. */ /* For each element newf0 in collision list xlist[posn]. */
newf0 = xlist[posn]; newf0 = xlist[posn];
while (newf0 != NULL) { while (newf0 != NULL) {
@ -662,7 +662,7 @@ cuddZddSwapInPlace(
** The modified f does not already exists in ylist. ** The modified f does not already exists in ylist.
** (Because of the uniqueness of the cofactors.) ** (Because of the uniqueness of the cofactors.)
*/ */
posn = ddHash(newf1, newf0, yshift); posn = ddHash(cuddF2L(newf1), cuddF2L(newf0), yshift);
newykeys++; newykeys++;
f->next = ylist[posn]; f->next = ylist[posn];
ylist[posn] = f; ylist[posn] = f;
@ -1456,7 +1456,7 @@ zddReorderPostprocess(
** nodes with zero reference count; hence lower probability of finding ** nodes with zero reference count; hence lower probability of finding
** a result in the cache. ** a result in the cache.
*/ */
if (table->reclaimed > table->allocated * 0.5) return(1); if (table->reclaimed > table->allocated / 2) return(1);
/* Resize subtables. */ /* Resize subtables. */
for (i = 0; i < table->sizeZ; i++) { for (i = 0; i < table->sizeZ; i++) {
@ -1491,7 +1491,7 @@ zddReorderPostprocess(
node = oldnodelist[j]; node = oldnodelist[j];
while (node != NULL) { while (node != NULL) {
next = node->next; next = node->next;
posn = ddHash(cuddT(node), cuddE(node), shift); posn = ddHash(cuddF2L(cuddT(node)), cuddF2L(cuddE(node)), shift);
node->next = nodelist[posn]; node->next = nodelist[posn];
nodelist[posn] = node; nodelist[posn] = node;
node = next; node = next;