diff --git a/src/bdd/cudd/cuddAddApply.c b/src/bdd/cudd/cuddAddApply.c index 86737f423..6009e6d78 100644 --- a/src/bdd/cudd/cuddAddApply.c +++ b/src/bdd/cudd/cuddAddApply.c @@ -182,7 +182,7 @@ Cudd_addPlus( res = cuddUniqueConst(dd,value); return(res); } - if (F > G) { /* swap f and g */ + if (cuddF2L(F) > cuddF2L(G)) { /* swap f and g */ *f = G; *g = F; } @@ -223,7 +223,7 @@ Cudd_addTimes( res = cuddUniqueConst(dd,value); return(res); } - if (F > G) { /* swap f and g */ + if (cuddF2L(F) > cuddF2L(G)) { /* swap f and g */ *f = G; *g = F; } @@ -405,7 +405,7 @@ Cudd_addMinimum( return(G); } } - if (F > G) { /* swap f and g */ + if (cuddF2L(F) > cuddF2L(G)) { /* swap f and g */ *f = G; *g = F; } @@ -450,7 +450,7 @@ Cudd_addMaximum( return(G); } } - if (F > G) { /* swap f and g */ + if (cuddF2L(F) > cuddF2L(G)) { /* swap f and g */ *f = G; *g = F; } @@ -590,7 +590,7 @@ Cudd_addOr( if (cuddIsConstant(F)) return(G); if (cuddIsConstant(G)) return(F); if (F == G) return(F); - if (F > G) { /* swap f and g */ + if (cuddF2L(F) > cuddF2L(G)) { /* swap f and g */ *f = G; *g = F; } @@ -622,7 +622,7 @@ Cudd_addNand( F = *f; G = *g; if (F == DD_ZERO(dd) || G == DD_ZERO(dd)) return(DD_ONE(dd)); if (cuddIsConstant(F) && cuddIsConstant(G)) return(DD_ZERO(dd)); - if (F > G) { /* swap f and g */ + if (cuddF2L(F) > cuddF2L(G)) { /* swap f and g */ *f = G; *g = F; } @@ -654,7 +654,7 @@ Cudd_addNor( F = *f; G = *g; if (F == DD_ONE(dd) || G == DD_ONE(dd)) return(DD_ZERO(dd)); if (cuddIsConstant(F) && cuddIsConstant(G)) return(DD_ONE(dd)); - if (F > G) { /* swap f and g */ + if (cuddF2L(F) > cuddF2L(G)) { /* swap f and g */ *f = G; *g = F; } @@ -688,7 +688,7 @@ Cudd_addXor( if (F == DD_ONE(dd) && G == DD_ZERO(dd)) return(DD_ONE(dd)); if (G == DD_ONE(dd) && F == DD_ZERO(dd)) return(DD_ONE(dd)); if (cuddIsConstant(F) && cuddIsConstant(G)) return(DD_ZERO(dd)); - if (F > G) { /* swap f and g */ + if (cuddF2L(F) > cuddF2L(G)) { /* swap f and g */ *f = G; *g = F; } @@ -722,7 +722,7 @@ Cudd_addXnor( if (F == DD_ONE(dd) && G == DD_ONE(dd)) return(DD_ONE(dd)); if (G == DD_ZERO(dd) && F == DD_ZERO(dd)) return(DD_ONE(dd)); if (cuddIsConstant(F) && cuddIsConstant(G)) return(DD_ZERO(dd)); - if (F > G) { /* swap f and g */ + if (cuddF2L(F) > cuddF2L(G)) { /* swap f and g */ *f = G; *g = F; } diff --git a/src/bdd/cudd/cuddAndAbs.c b/src/bdd/cudd/cuddAndAbs.c index d9ad1d236..a321afdc2 100644 --- a/src/bdd/cudd/cuddAndAbs.c +++ b/src/bdd/cudd/cuddAndAbs.c @@ -226,7 +226,7 @@ cuddBddAndAbstractRecur( } /* 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/cuddClip.c b/src/bdd/cudd/cuddClip.c index 32ee7f6ee..9d3261326 100644 --- a/src/bdd/cudd/cuddClip.c +++ b/src/bdd/cudd/cuddClip.c @@ -331,7 +331,7 @@ cuddBddClippingAndRecur( /* Check cache. Try to increase cache efficiency by sorting the ** pointers. */ - if (f > g) { + if (cuddF2L(f) > cuddF2L(g)) { DdNode *tmp = f; f = g; g = tmp; } @@ -469,7 +469,7 @@ cuddBddClipAndAbsRecur( distance--; /* Check cache. */ - 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/cuddInt.h b/src/bdd/cudd/cuddInt.h index c8e49a4ed..15b0a1d76 100644 --- a/src/bdd/cudd/cuddInt.h +++ b/src/bdd/cudd/cuddInt.h @@ -716,7 +716,7 @@ typedef struct DdLevelQueue { SeeAlso [] ******************************************************************************/ -#define cuddF2L(f) ((Cudd_Regular(f)->Id << 1) | Cudd_IsComplement(f)) +#define cuddF2L(f) ((Cudd_Regular(f)) ? ((Cudd_Regular(f)->Id << 1) | Cudd_IsComplement(f)) : 0) /**Macro*********************************************************************** diff --git a/src/bdd/cudd/cuddLinear.c b/src/bdd/cudd/cuddLinear.c index 7a0bf8db5..b38ea7294 100644 --- a/src/bdd/cudd/cuddLinear.c +++ b/src/bdd/cudd/cuddLinear.c @@ -500,11 +500,11 @@ cuddLinearInPlace( /* For each element newf1 in collision list ylist[posn]. */ previousP = &(ylist[posn]); newf1 = *previousP; - while (f11 < cuddT(newf1)) { + while (cuddF2L(f11) < cuddF2L(cuddT(newf1))) { previousP = &(newf1->next); newf1 = *previousP; } - while (f11 == cuddT(newf1) && f00 < cuddE(newf1)) { + while (f11 == cuddT(newf1) && cuddF2L(f00) < cuddF2L(cuddE(newf1))) { previousP = &(newf1->next); newf1 = *previousP; } @@ -554,11 +554,11 @@ cuddLinearInPlace( /* For each element newf0 in collision list ylist[posn]. */ previousP = &(ylist[posn]); newf0 = *previousP; - while (f01 < cuddT(newf0)) { + while (cuddF2L(f01) < cuddF2L(cuddT(newf0))) { previousP = &(newf0->next); newf0 = *previousP; } - while (f01 == cuddT(newf0) && f10 < cuddE(newf0)) { + while (f01 == cuddT(newf0) && cuddF2L(f10) < cuddF2L(cuddE(newf0))) { previousP = &(newf0->next); newf0 = *previousP; } @@ -595,11 +595,11 @@ cuddLinearInPlace( newxkeys++; previousP = &(xlist[posn]); tmp = *previousP; - while (newf1 < cuddT(tmp)) { + while (cuddF2L(newf1) < cuddF2L(cuddT(tmp))) { previousP = &(tmp->next); tmp = *previousP; } - while (newf1 == cuddT(tmp) && newf0 < cuddE(tmp)) { + while (newf1 == cuddT(tmp) && cuddF2L(newf0) < cuddF2L(cuddE(tmp))) { previousP = &(tmp->next); tmp = *previousP; } diff --git a/src/bdd/cudd/cuddMatMult.c b/src/bdd/cudd/cuddMatMult.c index 3dafa226e..63e9cd484 100644 --- a/src/bdd/cudd/cuddMatMult.c +++ b/src/bdd/cudd/cuddMatMult.c @@ -583,7 +583,7 @@ addTriangleRecur( res = cuddUniqueConst(dd, value); return(res); } - if (f < g) { + if (cuddF2L(f) < cuddF2L(g)) { DdNode *tmp = f; f = g; g = tmp; diff --git a/src/bdd/cudd/cuddReorder.c b/src/bdd/cudd/cuddReorder.c index 105cc12a3..e5aa86716 100644 --- a/src/bdd/cudd/cuddReorder.c +++ b/src/bdd/cudd/cuddReorder.c @@ -937,11 +937,11 @@ cuddSwapInPlace( /* For each element tmp in collision list xlist[posn]. */ previousP = &(xlist[posn]); tmp = *previousP; - while (cuddF2L(f1) < (cuddT(tmp) ? cuddF2L(cuddT(tmp)) : 0)) { + while (cuddF2L(f1) < cuddF2L(cuddT(tmp))) { previousP = &(tmp->next); tmp = *previousP; } - while (f1 == cuddT(tmp) && cuddF2L(f0) < (cuddE(tmp) ? cuddF2L(cuddE(tmp)) : 0)) { + while (f1 == cuddT(tmp) && cuddF2L(f0) < cuddF2L(cuddE(tmp))) { previousP = &(tmp->next); tmp = *previousP; } @@ -998,11 +998,11 @@ cuddSwapInPlace( /* For each element newf1 in collision list xlist[posn]. */ previousP = &(xlist[posn]); newf1 = *previousP; - while (cuddF2L(f11) < (cuddT(newf1) ? cuddF2L(cuddT(newf1)) : 0)) { + while (cuddF2L(f11) < cuddF2L(cuddT(newf1))) { previousP = &(newf1->next); newf1 = *previousP; } - while (f11 == cuddT(newf1) && cuddF2L(f01) < (cuddE(newf1) ? cuddF2L(cuddE(newf1)) : 0)) { + while (f11 == cuddT(newf1) && cuddF2L(f01) < cuddF2L(cuddE(newf1))) { previousP = &(newf1->next); newf1 = *previousP; } @@ -1052,11 +1052,11 @@ cuddSwapInPlace( /* For each element newf0 in collision list xlist[posn]. */ previousP = &(xlist[posn]); newf0 = *previousP; - while (cuddF2L(f10) < (cuddT(newf0) ? cuddF2L(cuddT(newf0)) : 0)) { + while (cuddF2L(f10) < cuddF2L(cuddT(newf0))) { previousP = &(newf0->next); newf0 = *previousP; } - while (f10 == cuddT(newf0) && cuddF2L(f00) < (cuddE(newf0) ? cuddF2L(cuddE(newf0)) : 0)) { + while (f10 == cuddT(newf0) && cuddF2L(f00) < cuddF2L(cuddE(newf0))) { previousP = &(newf0->next); newf0 = *previousP; } @@ -1093,11 +1093,11 @@ cuddSwapInPlace( newykeys++; previousP = &(ylist[posn]); tmp = *previousP; - while (cuddF2L(newf1) < (cuddT(tmp) ? cuddF2L(cuddT(tmp)) : 0)) { + while (cuddF2L(newf1) < cuddF2L(cuddT(tmp))) { previousP = &(tmp->next); tmp = *previousP; } - while (newf1 == cuddT(tmp) && cuddF2L(newf0) < (cuddE(tmp) ? cuddF2L(cuddE(tmp)) : 0)) { + while (newf1 == cuddT(tmp) && cuddF2L(newf0) < cuddF2L(cuddE(tmp))) { previousP = &(tmp->next); tmp = *previousP; } diff --git a/src/bdd/cudd/cuddSat.c b/src/bdd/cudd/cuddSat.c index 0f5f1056b..0c8cbb257 100644 --- a/src/bdd/cudd/cuddSat.c +++ b/src/bdd/cudd/cuddSat.c @@ -552,7 +552,7 @@ Cudd_EquivDC( /* From now on, D is non-constant. */ /* Normalize call to increase cache efficiency. */ - if (F > G) { + if (cuddF2L(F) > cuddF2L(G)) { tmp = F; F = G; G = tmp; @@ -674,7 +674,7 @@ Cudd_bddLeqUnless( /* !g <= D unless !f or !D <= g unless !f */ tmp = D; D = Cudd_Not(f); - if (g < tmp) { + if (cuddF2L(g) < cuddF2L(tmp)) { f = Cudd_Not(g); g = tmp; } else { @@ -717,7 +717,7 @@ Cudd_bddLeqUnless( } } else { /* f <= g unless D or !g <= !f unless D */ - if (g < f) { + if (cuddF2L(g) < cuddF2L(f)) { tmp = g; g = Cudd_Not(f); f = Cudd_Not(tmp); @@ -725,7 +725,7 @@ Cudd_bddLeqUnless( } } else { /* f <= g unless D or f <= D unless g */ - if (D < g) { + if (cuddF2L(D) < cuddF2L(g)) { tmp = D; D = g; g = tmp; diff --git a/src/bdd/cudd/cuddTable.c b/src/bdd/cudd/cuddTable.c index 6020f94c4..03d6ab831 100644 --- a/src/bdd/cudd/cuddTable.c +++ b/src/bdd/cudd/cuddTable.c @@ -1162,14 +1162,14 @@ cuddUniqueInter( previousP = &(nodelist[pos]); looking = *previousP; - while (T < cuddT(looking)) { + while (cuddF2L(T) < cuddF2L(cuddT(looking))) { previousP = &(looking->next); looking = *previousP; #ifdef DD_UNIQUE_PROFILE unique->uniqueLinks++; #endif } - while (T == cuddT(looking) && E < cuddE(looking)) { + while (T == cuddT(looking) && cuddF2L(E) < cuddF2L(cuddE(looking))) { previousP = &(looking->next); looking = *previousP; #ifdef DD_UNIQUE_PROFILE @@ -1220,14 +1220,14 @@ cuddUniqueInter( previousP = &(nodelist[pos]); looking = *previousP; - while (T < cuddT(looking)) { + while (cuddF2L(T) < cuddF2L(cuddT(looking))) { previousP = &(looking->next); looking = *previousP; #ifdef DD_UNIQUE_PROFILE unique->uniqueLinks++; #endif } - while (T == cuddT(looking) && E < cuddE(looking)) { + while (T == cuddT(looking) && cuddF2L(E) < cuddF2L(cuddE(looking))) { previousP = &(looking->next); looking = *previousP; #ifdef DD_UNIQUE_PROFILE @@ -1251,14 +1251,14 @@ cuddUniqueInter( previousP = &(nodelist[pos]); looking2 = *previousP; - while (T < cuddT(looking2)) { + while (cuddF2L(T) < cuddF2L(cuddT(looking2))) { previousP = &(looking2->next); looking2 = *previousP; #ifdef DD_UNIQUE_PROFILE unique->uniqueLinks++; #endif } - while (T == cuddT(looking2) && E < cuddE(looking2)) { + while (T == cuddT(looking2) && cuddF2L(E) < cuddF2L(cuddE(looking2))) { previousP = &(looking2->next); looking2 = *previousP; #ifdef DD_UNIQUE_PROFILE @@ -1664,7 +1664,7 @@ cuddRehash( while (node != NULL) { next = node->next; split.value = cuddV(node); - pos = ddHash(split.bits[0], split.bits[1], shift); + pos = ddHash(cuddF2L(split.bits[0]), cuddF2L(split.bits[1]), shift); node->next = nodelist[pos]; nodelist[pos] = node; node = next; @@ -1748,14 +1748,14 @@ cuddShrinkSubtable( looking = *previousP; T = cuddT(node); E = cuddE(node); - while (T < cuddT(looking)) { + while (cuddF2L(T) < cuddF2L(cuddT(looking))) { previousP = &(looking->next); looking = *previousP; #ifdef DD_UNIQUE_PROFILE unique->uniqueLinks++; #endif } - while (T == cuddT(looking) && E < cuddE(looking)) { + while (T == cuddT(looking) && cuddF2L(E) < cuddF2L(cuddE(looking))) { previousP = &(looking->next); looking = *previousP; #ifdef DD_UNIQUE_PROFILE @@ -2771,10 +2771,10 @@ cuddFindParent( for (j = 0; j < slots; j++) { f = nodelist[j]; - while (cuddT(f) > node) { + while (cuddF2L(cuddT(f)) > cuddF2L(node)) { f = f->next; } - while (cuddT(f) == node && Cudd_Regular(cuddE(f)) > node) { + while (cuddT(f) == node && cuddF2L(Cudd_Regular(cuddE(f))) > cuddF2L(node)) { f = f->next; } if (cuddT(f) == node && Cudd_Regular(cuddE(f)) == node) { @@ -3126,8 +3126,8 @@ cuddCheckCollisionOrdering( if (node == sentinel) return(1); next = node->next; while (next != sentinel) { - if (cuddT(node) < cuddT(next) || - (cuddT(node) == cuddT(next) && cuddE(node) < cuddE(next))) { + if (cuddF2L(cuddT(node)) < cuddF2L(cuddT(next)) || + (cuddT(node) == cuddT(next) && cuddF2L(cuddE(node)) < cuddF2L(cuddE(next)))) { (void) fprintf(unique->err, "Unordered list: index %u, position %d\n", i, j); return(0); diff --git a/src/bdd/cudd/cuddUtil.c b/src/bdd/cudd/cuddUtil.c index fe913fee3..c76709ef8 100644 --- a/src/bdd/cudd/cuddUtil.c +++ b/src/bdd/cudd/cuddUtil.c @@ -3357,10 +3357,10 @@ cuddUniqueLookup( nodelist = subtable->nodelist; looking = nodelist[posn]; - while (T < cuddT(looking)) { + while (cuddF2L(T) < cuddF2L(cuddT(looking))) { looking = Cudd_Regular(looking->next); } - while (T == cuddT(looking) && E < cuddE(looking)) { + while (T == cuddT(looking) && cuddF2L(E) < cuddF2L(cuddE(looking))) { looking = Cudd_Regular(looking->next); } if (cuddT(looking) == T && cuddE(looking) == E) {