summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/bdd/cudd/cudd.h1
-rw-r--r--src/bdd/cudd/cuddAPI.c3
-rw-r--r--src/bdd/cudd/cuddAndAbs.c2
-rw-r--r--src/bdd/cudd/cuddBddAbs.c2
-rw-r--r--src/bdd/cudd/cuddBddCorr.c4
-rw-r--r--src/bdd/cudd/cuddBddIte.c16
-rw-r--r--src/bdd/cudd/cuddBridge.c4
-rw-r--r--src/bdd/cudd/cuddCache.c84
-rw-r--r--src/bdd/cudd/cuddCompose.c2
-rw-r--r--src/bdd/cudd/cuddInt.h26
-rw-r--r--src/bdd/cudd/cuddLCache.c20
-rw-r--r--src/bdd/cudd/cuddLinear.c6
-rw-r--r--src/bdd/cudd/cuddReorder.c23
-rw-r--r--src/bdd/cudd/cuddSymmetry.c2
-rw-r--r--src/bdd/cudd/cuddTable.c43
-rw-r--r--src/bdd/cudd/cuddUtil.c2
-rw-r--r--src/bdd/cudd/cuddZddLin.c12
-rw-r--r--src/bdd/cudd/cuddZddReord.c10
18 files changed, 171 insertions, 91 deletions
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 */
@@ -699,6 +701,20 @@ typedef struct DdLevelQueue {
/**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.]
Description []
@@ -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;
generated by cgit v1.2.3 (git 2.25.1) at 2025-11-04 05:07:55 +0000