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

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;