diff options
Diffstat (limited to 'src/bdd/cudd/cuddReorder.c')
| -rw-r--r-- | src/bdd/cudd/cuddReorder.c | 1859 |
1 files changed, 950 insertions, 909 deletions
diff --git a/src/bdd/cudd/cuddReorder.c b/src/bdd/cudd/cuddReorder.c index 020a1b5e..383be18a 100644 --- a/src/bdd/cudd/cuddReorder.c +++ b/src/bdd/cudd/cuddReorder.c @@ -7,41 +7,68 @@ Synopsis [Functions for dynamic variable reordering.] Description [External procedures included in this file: - <ul> - <li> Cudd_ReduceHeap() - <li> Cudd_ShuffleHeap() - </ul> - Internal procedures included in this module: - <ul> - <li> cuddDynamicAllocNode() - <li> cuddSifting() - <li> cuddSwapping() - <li> cuddNextHigh() - <li> cuddNextLow() - <li> cuddSwapInPlace() - <li> cuddBddAlignToZdd() - </ul> - Static procedures included in this module: - <ul> - <li> ddUniqueCompare() - <li> ddSwapAny() - <li> ddSiftingAux() - <li> ddSiftingUp() - <li> ddSiftingDown() - <li> ddSiftingBackward() - <li> ddReorderPreprocess() - <li> ddReorderPostprocess() - <li> ddShuffle() - <li> ddSiftUp() - <li> bddFixTree() - </ul>] + <ul> + <li> Cudd_ReduceHeap() + <li> Cudd_ShuffleHeap() + </ul> + Internal procedures included in this module: + <ul> + <li> cuddDynamicAllocNode() + <li> cuddSifting() + <li> cuddSwapping() + <li> cuddNextHigh() + <li> cuddNextLow() + <li> cuddSwapInPlace() + <li> cuddBddAlignToZdd() + </ul> + Static procedures included in this module: + <ul> + <li> ddUniqueCompare() + <li> ddSwapAny() + <li> ddSiftingAux() + <li> ddSiftingUp() + <li> ddSiftingDown() + <li> ddSiftingBackward() + <li> ddReorderPreprocess() + <li> ddReorderPostprocess() + <li> ddShuffle() + <li> ddSiftUp() + <li> bddFixTree() + </ul>] Author [Shipra Panda, Bernard Plessier, Fabio Somenzi] - Copyright [This file was created at the University of Colorado at - Boulder. The University of Colorado at Boulder makes no warranty - about the suitability of this software for any purpose. It is - presented on an AS IS basis.] + Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado + + All rights reserved. + + Redistribution and use in source and binary forms, with or without + modification, are permitted provided that the following conditions + are met: + + Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + + Redistributions in binary form must reproduce the above copyright + notice, this list of conditions and the following disclaimer in the + documentation and/or other materials provided with the distribution. + + Neither the name of the University of Colorado nor the names of its + contributors may be used to endorse or promote products derived from + this software without specific prior written permission. + + THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS + "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT + LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS + FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE + COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, + INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, + BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; + LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER + CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT + LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN + ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE + POSSIBILITY OF SUCH DAMAGE.] ******************************************************************************/ @@ -51,6 +78,7 @@ ABC_NAMESPACE_IMPL_START + /*---------------------------------------------------------------------------*/ /* Constant declarations */ /*---------------------------------------------------------------------------*/ @@ -71,14 +99,14 @@ ABC_NAMESPACE_IMPL_START /*---------------------------------------------------------------------------*/ #ifndef lint -static char rcsid[] DD_UNUSED = "$Id: cuddReorder.c,v 1.1.1.1 2003/02/24 22:23:53 wjiang Exp $"; +static char rcsid[] DD_UNUSED = "$Id: cuddReorder.c,v 1.69 2009/02/21 18:24:10 fabio Exp $"; #endif -static int *entry; +static int *entry; -int ddTotalNumberSwapping; +int ddTotalNumberSwapping; #ifdef DD_STATS -int ddTotalNISwaps; +int ddTotalNISwaps; #endif /*---------------------------------------------------------------------------*/ @@ -91,19 +119,19 @@ int ddTotalNISwaps; /* Static function prototypes */ /*---------------------------------------------------------------------------*/ -static int ddUniqueCompare ARGS((int *ptrX, int *ptrY)); -static Move * ddSwapAny ARGS((DdManager *table, int x, int y)); -static int ddSiftingAux ARGS((DdManager *table, int x, int xLow, int xHigh)); -static Move * ddSiftingUp ARGS((DdManager *table, int y, int xLow)); -static Move * ddSiftingDown ARGS((DdManager *table, int x, int xHigh)); -static int ddSiftingBackward ARGS((DdManager *table, int size, Move *moves)); -static int ddReorderPreprocess ARGS((DdManager *table)); -static int ddReorderPostprocess ARGS((DdManager *table)); -static int ddShuffle ARGS((DdManager *table, int *permutation)); -static int ddSiftUp ARGS((DdManager *table, int x, int xLow)); -static void bddFixTree ARGS((DdManager *table, MtrNode *treenode)); -static int ddUpdateMtrTree ARGS((DdManager *table, MtrNode *treenode, int *perm, int *invperm)); -static int ddCheckPermuation ARGS((DdManager *table, MtrNode *treenode, int *perm, int *invperm)); +static int ddUniqueCompare (int *ptrX, int *ptrY); +static Move * ddSwapAny (DdManager *table, int x, int y); +static int ddSiftingAux (DdManager *table, int x, int xLow, int xHigh); +static Move * ddSiftingUp (DdManager *table, int y, int xLow); +static Move * ddSiftingDown (DdManager *table, int x, int xHigh); +static int ddSiftingBackward (DdManager *table, int size, Move *moves); +static int ddReorderPreprocess (DdManager *table); +static int ddReorderPostprocess (DdManager *table); +static int ddShuffle (DdManager *table, int *permutation); +static int ddSiftUp (DdManager *table, int x, int xLow); +static void bddFixTree (DdManager *table, MtrNode *treenode); +static int ddUpdateMtrTree (DdManager *table, MtrNode *treenode, int *perm, int *invperm); +static int ddCheckPermuation (DdManager *table, MtrNode *treenode, int *perm, int *invperm); /**AutomaticEnd***************************************************************/ @@ -151,24 +179,23 @@ Cudd_ReduceHeap( int minsize /* bound below which no reordering occurs */) { DdHook *hook; - int result; + int result; unsigned int nextDyn; #ifdef DD_STATS unsigned int initialSize; unsigned int finalSize; #endif long localTime; - int TimeStop = table->TimeStop; /* Don't reorder if there are too many dead nodes. */ if (table->keys - table->dead < (unsigned) minsize) - return(1); + return(1); if (heuristic == CUDD_REORDER_SAME) { - heuristic = table->autoMethod; + heuristic = table->autoMethod; } if (heuristic == CUDD_REORDER_NONE) { - return(1); + return(1); } /* This call to Cudd_ReduceHeap does initiate reordering. Therefore @@ -181,16 +208,16 @@ Cudd_ReduceHeap( /* Run the hook functions. */ hook = table->preReorderingHook; while (hook != NULL) { - int res = (hook->f)(table, "BDD", (void *)heuristic); - if (res == 0) return(0); - hook = hook->next; + int res = (hook->f)(table, "BDD", (void *)heuristic); + if (res == 0) return(0); + hook = hook->next; } if (!ddReorderPreprocess(table)) return(0); ddTotalNumberSwapping = 0; - + if (table->keys > table->peakLiveNodes) { - table->peakLiveNodes = table->keys; + table->peakLiveNodes = table->keys; } #ifdef DD_STATS initialSize = table->keys - table->isolated; @@ -199,89 +226,89 @@ Cudd_ReduceHeap( switch(heuristic) { case CUDD_REORDER_RANDOM: case CUDD_REORDER_RANDOM_PIVOT: - (void) fprintf(table->out,"#:I_RANDOM "); - break; + (void) fprintf(table->out,"#:I_RANDOM "); + break; case CUDD_REORDER_SIFT: case CUDD_REORDER_SIFT_CONVERGE: case CUDD_REORDER_SYMM_SIFT: case CUDD_REORDER_SYMM_SIFT_CONV: case CUDD_REORDER_GROUP_SIFT: case CUDD_REORDER_GROUP_SIFT_CONV: - (void) fprintf(table->out,"#:I_SIFTING "); - break; + (void) fprintf(table->out,"#:I_SIFTING "); + break; case CUDD_REORDER_WINDOW2: case CUDD_REORDER_WINDOW3: case CUDD_REORDER_WINDOW4: case CUDD_REORDER_WINDOW2_CONV: case CUDD_REORDER_WINDOW3_CONV: case CUDD_REORDER_WINDOW4_CONV: - (void) fprintf(table->out,"#:I_WINDOW "); - break; + (void) fprintf(table->out,"#:I_WINDOW "); + break; case CUDD_REORDER_ANNEALING: - (void) fprintf(table->out,"#:I_ANNEAL "); - break; + (void) fprintf(table->out,"#:I_ANNEAL "); + break; case CUDD_REORDER_GENETIC: - (void) fprintf(table->out,"#:I_GENETIC "); - break; + (void) fprintf(table->out,"#:I_GENETIC "); + break; case CUDD_REORDER_LINEAR: case CUDD_REORDER_LINEAR_CONVERGE: - (void) fprintf(table->out,"#:I_LINSIFT "); - break; + (void) fprintf(table->out,"#:I_LINSIFT "); + break; case CUDD_REORDER_EXACT: - (void) fprintf(table->out,"#:I_EXACT "); - break; + (void) fprintf(table->out,"#:I_EXACT "); + break; default: - return(0); + return(0); } - (void) fprintf(table->out,"%8d: initial size",initialSize); + (void) fprintf(table->out,"%8d: initial size",initialSize); #endif /* See if we should use alternate threshold for maximum growth. */ if (table->reordCycle && table->reorderings % table->reordCycle == 0) { - double saveGrowth = table->maxGrowth; - table->maxGrowth = table->maxGrowthAlt; - result = cuddTreeSifting(table,heuristic,TimeStop); - table->maxGrowth = saveGrowth; + double saveGrowth = table->maxGrowth; + table->maxGrowth = table->maxGrowthAlt; + result = cuddTreeSifting(table,heuristic); + table->maxGrowth = saveGrowth; } else { - result = cuddTreeSifting(table,heuristic,TimeStop); + result = cuddTreeSifting(table,heuristic); } #ifdef DD_STATS (void) fprintf(table->out,"\n"); finalSize = table->keys - table->isolated; - (void) fprintf(table->out,"#:F_REORDER %8d: final size\n",finalSize); + (void) fprintf(table->out,"#:F_REORDER %8d: final size\n",finalSize); (void) fprintf(table->out,"#:T_REORDER %8g: total time (sec)\n", - ((double)(util_cpu_time() - localTime)/1000.0)); + ((double)(util_cpu_time() - localTime)/1000.0)); (void) fprintf(table->out,"#:N_REORDER %8d: total swaps\n", - ddTotalNumberSwapping); + ddTotalNumberSwapping); (void) fprintf(table->out,"#:M_REORDER %8d: NI swaps\n",ddTotalNISwaps); #endif if (result == 0) - return(0); + return(0); if (!ddReorderPostprocess(table)) - return(0); + return(0); if (table->realign) { - if (!cuddZddAlignToBdd(table)) - return(0); + if (!cuddZddAlignToBdd(table)) + return(0); } nextDyn = (table->keys - table->constants.keys + 1) * - DD_DYN_RATIO + table->constants.keys; + DD_DYN_RATIO + table->constants.keys; if (table->reorderings < 20 || nextDyn > table->nextDyn) - table->nextDyn = nextDyn; + table->nextDyn = nextDyn; else - table->nextDyn += 20; + table->nextDyn += 20; table->reordered = 1; /* Run hook functions. */ hook = table->postReorderingHook; while (hook != NULL) { - int res = (hook->f)(table, "BDD", (void *)localTime); - if (res == 0) return(0); - hook = hook->next; + int res = (hook->f)(table, "BDD", (void *)localTime); + if (res == 0) return(0); + hook = hook->next; } /* Update cumulative reordering time. */ table->reordTime += util_cpu_time() - localTime; @@ -313,36 +340,36 @@ Cudd_ShuffleHeap( int * permutation /* required variable permutation */) { - int result; + int result; int i; int identity = 1; int *perm; /* Don't waste time in case of identity permutation. */ for (i = 0; i < table->size; i++) { - if (permutation[i] != table->invperm[i]) { - identity = 0; - break; - } + if (permutation[i] != table->invperm[i]) { + identity = 0; + break; + } } if (identity == 1) { - return(1); + return(1); } if (!ddReorderPreprocess(table)) return(0); if (table->keys > table->peakLiveNodes) { - table->peakLiveNodes = table->keys; + table->peakLiveNodes = table->keys; } perm = ABC_ALLOC(int, table->size); for (i = 0; i < table->size; i++) - perm[permutation[i]] = i; + perm[permutation[i]] = i; if (!ddCheckPermuation(table,table->tree,perm,permutation)) { - ABC_FREE(perm); - return(0); + ABC_FREE(perm); + return(0); } if (!ddUpdateMtrTree(table,table->tree,perm,permutation)) { - ABC_FREE(perm); - return(0); + ABC_FREE(perm); + return(0); } ABC_FREE(perm); @@ -382,66 +409,68 @@ cuddDynamicAllocNode( int i; DdNodePtr *mem; DdNode *list, *node; -// extern void (*MMoutOfMemory)(long); - void (*saveHandler)(long); + extern DD_OOMFP MMoutOfMemory; + DD_OOMFP saveHandler; if (table->nextFree == NULL) { /* free list is empty */ - /* Try to allocate a new block. */ - saveHandler = MMoutOfMemory; - MMoutOfMemory = Cudd_OutOfMem; - mem = (DdNodePtr *) ABC_ALLOC(DdNode, DD_MEM_CHUNK + 1); - MMoutOfMemory = saveHandler; - if (mem == NULL && table->stash != NULL) { - ABC_FREE(table->stash); - table->stash = NULL; - /* Inhibit resizing of tables. */ - table->maxCacheHard = table->cacheSlots - 1; - table->cacheSlack = -(int)(table->cacheSlots + 1); - for (i = 0; i < table->size; i++) { - table->subtables[i].maxKeys <<= 2; + /* Try to allocate a new block. */ + saveHandler = MMoutOfMemory; + MMoutOfMemory = Cudd_OutOfMem; + mem = (DdNodePtr *) ABC_ALLOC(DdNode, DD_MEM_CHUNK + 1); + MMoutOfMemory = saveHandler; + if (mem == NULL && table->stash != NULL) { + ABC_FREE(table->stash); + table->stash = NULL; + /* Inhibit resizing of tables. */ + table->maxCacheHard = table->cacheSlots - 1; + table->cacheSlack = - (int) (table->cacheSlots + 1); + 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); - } - if (mem == NULL) { - /* Out of luck. Call the default handler to do - ** whatever it specifies for a failed malloc. If this - ** handler returns, then set error code, print - ** warning, and return. */ - (*MMoutOfMemory)(sizeof(DdNode)*(DD_MEM_CHUNK + 1)); - table->errorCode = CUDD_MEMORY_OUT; + if (mem == NULL) { + /* Out of luck. Call the default handler to do + ** whatever it specifies for a failed malloc. If this + ** handler returns, then set error code, print + ** warning, and return. */ + (*MMoutOfMemory)(sizeof(DdNode)*(DD_MEM_CHUNK + 1)); + table->errorCode = CUDD_MEMORY_OUT; #ifdef DD_VERBOSE - (void) fprintf(table->err, - "cuddDynamicAllocNode: out of memory"); - (void) fprintf(table->err,"Memory in use = %ld\n", - table->memused); + (void) fprintf(table->err, + "cuddDynamicAllocNode: out of memory"); + (void) fprintf(table->err,"Memory in use = %lu\n", + table->memused); #endif - return(NULL); - } else { /* successful allocation; slice memory */ - unsigned long offset; - table->memused += (DD_MEM_CHUNK + 1) * sizeof(DdNode); - mem[0] = (DdNode *) table->memoryList; - table->memoryList = mem; - - /* Here we rely on the fact that the size of a DdNode is a - ** 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); + return(NULL); + } else { /* successful allocation; slice memory */ + unsigned long offset; + table->memused += (DD_MEM_CHUNK + 1) * sizeof(DdNode); + mem[0] = (DdNode *) table->memoryList; + table->memoryList = mem; + + /* Here we rely on the fact that the size of a DdNode is a + ** 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); #ifdef DD_DEBUG - assert(((unsigned long) mem & (sizeof(DdNode) - 1)) == 0); + assert(((unsigned long) mem & (sizeof(DdNode) - 1)) == 0); #endif - list = (DdNode *) mem; + list = (DdNode *) mem; - i = 1; - do { - list[i - 1].next = &list[i]; - } while (++i < DD_MEM_CHUNK); + i = 1; + do { + list[i - 1].ref = 0; + list[i - 1].next = &list[i]; + } while (++i < DD_MEM_CHUNK); - list[DD_MEM_CHUNK - 1].next = NULL; + list[DD_MEM_CHUNK-1].ref = 0; + list[DD_MEM_CHUNK - 1].next = NULL; - table->nextFree = &list[0]; - } + table->nextFree = &list[0]; + } } /* if free list empty */ node = table->nextFree; @@ -476,13 +505,13 @@ cuddSifting( int lower, int upper) { - int i; - int *var; - int size; - int x; - int result; + int i; + int *var; + int size; + int x; + int result; #ifdef DD_STATS - int previousSize; + int previousSize; #endif size = table->size; @@ -491,46 +520,46 @@ cuddSifting( var = NULL; entry = ABC_ALLOC(int,size); if (entry == NULL) { - table->errorCode = CUDD_MEMORY_OUT; - goto cuddSiftingOutOfMem; + table->errorCode = CUDD_MEMORY_OUT; + goto cuddSiftingOutOfMem; } var = ABC_ALLOC(int,size); if (var == NULL) { - table->errorCode = CUDD_MEMORY_OUT; - goto cuddSiftingOutOfMem; + table->errorCode = CUDD_MEMORY_OUT; + goto cuddSiftingOutOfMem; } for (i = 0; i < size; i++) { - x = table->perm[i]; - entry[i] = table->subtables[x].keys; - var[i] = i; + x = table->perm[i]; + entry[i] = table->subtables[x].keys; + var[i] = i; } - qsort((void *)var,size,sizeof(int),(int (*)(const void *, const void *))ddUniqueCompare); + qsort((void *)var,size,sizeof(int),(DD_QSFP)ddUniqueCompare); /* Now sift. */ for (i = 0; i < ddMin(table->siftMaxVar,size); i++) { - if (ddTotalNumberSwapping >= table->siftMaxSwap) - break; - x = table->perm[var[i]]; - - if (x < lower || x > upper || table->subtables[x].bindVar == 1) - continue; + if (ddTotalNumberSwapping >= table->siftMaxSwap) + break; + x = table->perm[var[i]]; + + if (x < lower || x > upper || table->subtables[x].bindVar == 1) + continue; #ifdef DD_STATS - previousSize = table->keys - table->isolated; + previousSize = table->keys - table->isolated; #endif - result = ddSiftingAux(table, x, lower, upper); - if (!result) goto cuddSiftingOutOfMem; + result = ddSiftingAux(table, x, lower, upper); + if (!result) goto cuddSiftingOutOfMem; #ifdef DD_STATS - if (table->keys < (unsigned) previousSize + table->isolated) { - (void) fprintf(table->out,"-"); - } else if (table->keys > (unsigned) previousSize + table->isolated) { - (void) fprintf(table->out,"+"); /* should never happen */ - (void) fprintf(table->err,"\nSize increased from %d to %d while sifting variable %d\n", previousSize, table->keys - table->isolated, var[i]); - } else { - (void) fprintf(table->out,"="); - } - fflush(table->out); + if (table->keys < (unsigned) previousSize + table->isolated) { + (void) fprintf(table->out,"-"); + } else if (table->keys > (unsigned) previousSize + table->isolated) { + (void) fprintf(table->out,"+"); /* should never happen */ + (void) fprintf(table->err,"\nSize increased from %d to %d while sifting variable %d\n", previousSize, table->keys - table->isolated, var[i]); + } else { + (void) fprintf(table->out,"="); + } + fflush(table->out); #endif } @@ -544,7 +573,7 @@ cuddSiftingOutOfMem: if (entry != NULL) ABC_FREE(entry); if (var != NULL) ABC_FREE(var); - return(0); + return(0); } /* end of cuddSifting */ @@ -574,15 +603,15 @@ cuddSwapping( int upper, Cudd_ReorderingType heuristic) { - int i, j; - int max, keys; - int nvars; - int x, y; - int iterate; + int i, j; + int max, keys; + int nvars; + int x, y; + int iterate; int previousSize; Move *moves, *move; - int pivot = 0; // Suppress "might be used uninitialized" - int modulo; + int pivot; + int modulo; int result; #ifdef DD_DEBUG @@ -594,61 +623,61 @@ cuddSwapping( iterate = nvars; for (i = 0; i < iterate; i++) { - if (ddTotalNumberSwapping >= table->siftMaxSwap) - break; - if (heuristic == CUDD_REORDER_RANDOM_PIVOT) { - max = -1; - for (j = lower; j <= upper; j++) { - if ((keys = table->subtables[j].keys) > max) { - max = keys; - pivot = j; - } - } + if (ddTotalNumberSwapping >= table->siftMaxSwap) + break; + if (heuristic == CUDD_REORDER_RANDOM_PIVOT) { + max = -1; + for (j = lower; j <= upper; j++) { + if ((keys = table->subtables[j].keys) > max) { + max = keys; + pivot = j; + } + } - modulo = upper - pivot; - if (modulo == 0) { - y = pivot; - } else{ - y = pivot + 1 + ((int) Cudd_Random() % modulo); - } + modulo = upper - pivot; + if (modulo == 0) { + y = pivot; + } else{ + y = pivot + 1 + ((int) Cudd_Random() % modulo); + } - modulo = pivot - lower - 1; - if (modulo < 1) { - x = lower; - } else{ - do { - x = (int) Cudd_Random() % modulo; - } while (x == y); + modulo = pivot - lower - 1; + if (modulo < 1) { + x = lower; + } else{ + do { + x = (int) Cudd_Random() % modulo; + } while (x == y); + } + } else { + x = ((int) Cudd_Random() % nvars) + lower; + do { + y = ((int) Cudd_Random() % nvars) + lower; + } while (x == y); + } + previousSize = table->keys - table->isolated; + moves = ddSwapAny(table,x,y); + if (moves == NULL) goto cuddSwappingOutOfMem; + result = ddSiftingBackward(table,previousSize,moves); + if (!result) goto cuddSwappingOutOfMem; + while (moves != NULL) { + move = moves->next; + cuddDeallocMove(table, moves); + moves = move; } - } else { - x = ((int) Cudd_Random() % nvars) + lower; - do { - y = ((int) Cudd_Random() % nvars) + lower; - } while (x == y); - } - previousSize = table->keys - table->isolated; - moves = ddSwapAny(table,x,y); - if (moves == NULL) goto cuddSwappingOutOfMem; - result = ddSiftingBackward(table,previousSize,moves); - if (!result) goto cuddSwappingOutOfMem; - while (moves != NULL) { - move = moves->next; - cuddDeallocNode(table, (DdNode *) moves); - moves = move; - } #ifdef DD_STATS - if (table->keys < (unsigned) previousSize + table->isolated) { - (void) fprintf(table->out,"-"); - } else if (table->keys > (unsigned) previousSize + table->isolated) { - (void) fprintf(table->out,"+"); /* should never happen */ - } else { - (void) fprintf(table->out,"="); - } - fflush(table->out); + if (table->keys < (unsigned) previousSize + table->isolated) { + (void) fprintf(table->out,"-"); + } else if (table->keys > (unsigned) previousSize + table->isolated) { + (void) fprintf(table->out,"+"); /* should never happen */ + } else { + (void) fprintf(table->out,"="); + } + fflush(table->out); #endif #if 0 - (void) fprintf(table->out,"#:t_SWAPPING %8d: tmp size\n", - table->keys - table->isolated); + (void) fprintf(table->out,"#:t_SWAPPING %8d: tmp size\n", + table->keys - table->isolated); #endif } @@ -656,9 +685,9 @@ cuddSwapping( cuddSwappingOutOfMem: while (moves != NULL) { - move = moves->next; - cuddDeallocNode(table, (DdNode *) moves); - moves = move; + move = moves->next; + cuddDeallocMove(table, moves); + moves = move; } return(0); @@ -686,7 +715,7 @@ cuddNextHigh( return(x+1); } /* end of cuddNextHigh */ - + /**Function******************************************************************** @@ -746,10 +775,10 @@ cuddSwapInPlace( DdNodePtr *previousP; DdNode *tmp; DdNode *sentinel = &(table->sentinel); -// extern void (*MMoutOfMemory)(long); - void (*saveHandler)(long); + extern DD_OOMFP MMoutOfMemory; + DD_OOMFP saveHandler; -#if DD_DEBUG +#ifdef DD_DEBUG int count,idcheck; #endif @@ -766,7 +795,7 @@ cuddSwapInPlace( /* Get parameters of x subtable. */ xindex = table->invperm[x]; - xlist = table->subtables[x].nodelist; + xlist = table->subtables[x].nodelist; oldxkeys = table->subtables[x].keys; xslots = table->subtables[x].slots; xshift = table->subtables[x].shift; @@ -780,365 +809,370 @@ cuddSwapInPlace( if (!cuddTestInteract(table,xindex,yindex)) { #ifdef DD_STATS - ddTotalNISwaps++; + ddTotalNISwaps++; #endif - newxkeys = oldxkeys; - newykeys = oldykeys; + newxkeys = oldxkeys; + newykeys = oldykeys; } else { - newxkeys = 0; - newykeys = oldykeys; - - /* Check whether the two projection functions involved in this - ** swap are isolated. At the end, we'll be able to tell how many - ** isolated projection functions are there by checking only these - ** two functions again. This is done to eliminate the isolated - ** projection functions from the node count. - */ - isolated = - ((table->vars[xindex]->ref == 1) + - (table->vars[yindex]->ref == 1)); + newxkeys = 0; + newykeys = oldykeys; + + /* Check whether the two projection functions involved in this + ** swap are isolated. At the end, we'll be able to tell how many + ** isolated projection functions are there by checking only these + ** two functions again. This is done to eliminate the isolated + ** projection functions from the node count. + */ + isolated = - ((table->vars[xindex]->ref == 1) + + (table->vars[yindex]->ref == 1)); - /* The nodes in the x layer that do not depend on - ** y will stay there; the others are put in a chain. - ** The chain is handled as a LIFO; g points to the beginning. - */ - g = NULL; - if ((oldxkeys >= xslots || (unsigned) xslots == table->initSlots) && - oldxkeys <= DD_MAX_SUBTABLE_DENSITY * xslots) { - for (i = 0; i < xslots; i++) { - previousP = &(xlist[i]); - f = *previousP; - while (f != sentinel) { - next = f->next; - f1 = cuddT(f); f0 = cuddE(f); - if (f1->index != (DdHalfWord) yindex && - Cudd_Regular(f0)->index != (DdHalfWord) yindex) { - /* stays */ - newxkeys++; - *previousP = f; - previousP = &(f->next); - } else { - f->index = yindex; - f->next = g; - g = f; + /* The nodes in the x layer that do not depend on + ** y will stay there; the others are put in a chain. + ** The chain is handled as a LIFO; g points to the beginning. + */ + g = NULL; + if ((oldxkeys >= xslots || (unsigned) xslots == table->initSlots) && + oldxkeys <= DD_MAX_SUBTABLE_DENSITY * xslots) { + for (i = 0; i < xslots; i++) { + previousP = &(xlist[i]); + f = *previousP; + while (f != sentinel) { + next = f->next; + f1 = cuddT(f); f0 = cuddE(f); + if (f1->index != (DdHalfWord) yindex && + Cudd_Regular(f0)->index != (DdHalfWord) yindex) { + /* stays */ + newxkeys++; + *previousP = f; + previousP = &(f->next); + } else { + f->index = yindex; + f->next = g; + g = f; + } + f = next; + } /* while there are elements in the collision chain */ + *previousP = sentinel; + } /* for each slot of the x subtable */ + } else { /* resize xlist */ + DdNode *h = NULL; + DdNodePtr *newxlist; + unsigned int newxslots; + int newxshift; + /* Empty current xlist. Nodes that stay go to list h; + ** nodes that move go to list g. */ + for (i = 0; i < xslots; i++) { + f = xlist[i]; + while (f != sentinel) { + next = f->next; + f1 = cuddT(f); f0 = cuddE(f); + if (f1->index != (DdHalfWord) yindex && + Cudd_Regular(f0)->index != (DdHalfWord) yindex) { + /* stays */ + f->next = h; + h = f; + newxkeys++; + } else { + f->index = yindex; + f->next = g; + g = f; + } + f = next; + } /* while there are elements in the collision chain */ + } /* for each slot of the x subtable */ + /* Decide size of new subtable. */ + newxshift = xshift; + newxslots = xslots; + while ((unsigned) oldxkeys > DD_MAX_SUBTABLE_DENSITY * newxslots) { + newxshift--; + newxslots <<= 1; } - f = next; - } /* while there are elements in the collision chain */ - *previousP = sentinel; - } /* for each slot of the x subtable */ - } else { /* resize xlist */ - DdNode *h = NULL; - DdNodePtr *newxlist; - unsigned int newxslots; - int newxshift; - /* Empty current xlist. Nodes that stay go to list h; - ** nodes that move go to list g. */ - for (i = 0; i < xslots; i++) { - f = xlist[i]; - while (f != sentinel) { - next = f->next; - f1 = cuddT(f); f0 = cuddE(f); - if (f1->index != (DdHalfWord) yindex && - Cudd_Regular(f0)->index != (DdHalfWord) yindex) { - /* stays */ - f->next = h; - h = f; - newxkeys++; + while ((unsigned) oldxkeys < newxslots && + newxslots > table->initSlots) { + newxshift++; + newxslots >>= 1; + } + /* Try to allocate new table. Be ready to back off. */ + saveHandler = MMoutOfMemory; + MMoutOfMemory = Cudd_OutOfMem; + newxlist = ABC_ALLOC(DdNodePtr, newxslots); + MMoutOfMemory = saveHandler; + if (newxlist == NULL) { + (void) fprintf(table->err, "Unable to resize subtable %d for lack of memory\n", i); + newxlist = xlist; + newxslots = xslots; + newxshift = xshift; } else { - f->index = yindex; - f->next = g; - g = f; + table->slots += ((int) newxslots - xslots); + table->minDead = (unsigned) + (table->gcFrac * (double) table->slots); + table->cacheSlack = (int) + ddMin(table->maxCacheHard, DD_MAX_CACHE_TO_SLOTS_RATIO + * table->slots) - 2 * (int) table->cacheSlots; + table->memused += + ((int) newxslots - xslots) * sizeof(DdNodePtr); + ABC_FREE(xlist); + xslots = newxslots; + xshift = newxshift; + xlist = newxlist; + } + /* Initialize new subtable. */ + for (i = 0; i < xslots; i++) { + xlist[i] = sentinel; + } + /* Move nodes that were parked in list h to their new home. */ + f = h; + while (f != NULL) { + next = f->next; + f1 = cuddT(f); + f0 = cuddE(f); + /* Check xlist for pair (f11,f01). */ + posn = ddHash(f1, f0, xshift); + /* For each element tmp in collision list xlist[posn]. */ + previousP = &(xlist[posn]); + tmp = *previousP; + while (f1 < cuddT(tmp)) { + previousP = &(tmp->next); + tmp = *previousP; + } + while (f1 == cuddT(tmp) && f0 < cuddE(tmp)) { + previousP = &(tmp->next); + tmp = *previousP; + } + f->next = *previousP; + *previousP = f; + f = next; } - f = next; - } /* while there are elements in the collision chain */ - } /* for each slot of the x subtable */ - /* Decide size of new subtable. */ - if (oldxkeys > DD_MAX_SUBTABLE_DENSITY * xslots) { - newxshift = xshift - 1; - newxslots = xslots << 1; - } else { - newxshift = xshift + 1; - newxslots = xslots >> 1; - } - /* Try to allocate new table. Be ready to back off. */ - saveHandler = MMoutOfMemory; - MMoutOfMemory = Cudd_OutOfMem; - newxlist = ABC_ALLOC(DdNodePtr, newxslots); - MMoutOfMemory = saveHandler; - if (newxlist == NULL) { - (void) fprintf(table->err, "Unable to resize subtable %d for lack of memory\n", i); - newxlist = xlist; - newxslots = xslots; - newxshift = xshift; - } else { - table->slots += (newxslots - xslots); - table->minDead = (unsigned) - (table->gcFrac * (double) table->slots); - table->cacheSlack = (int) - ddMin(table->maxCacheHard, DD_MAX_CACHE_TO_SLOTS_RATIO - * table->slots) - 2 * (int) table->cacheSlots; - table->memused += (newxslots - xslots) * sizeof(DdNodePtr); - ABC_FREE(xlist); - xslots = newxslots; - xshift = newxshift; - xlist = newxlist; - } - /* Initialize new subtable. */ - for (i = 0; i < xslots; i++) { - xlist[i] = sentinel; - } - /* Move nodes that were parked in list h to their new home. */ - f = h; - while (f != NULL) { - next = f->next; - f1 = cuddT(f); - f0 = cuddE(f); - /* Check xlist for pair (f11,f01). */ - posn = ddHash(f1, f0, xshift); - /* For each element tmp in collision list xlist[posn]. */ - previousP = &(xlist[posn]); - tmp = *previousP; - while (f1 < cuddT(tmp)) { - previousP = &(tmp->next); - tmp = *previousP; - } - while (f1 == cuddT(tmp) && f0 < cuddE(tmp)) { - previousP = &(tmp->next); - tmp = *previousP; - } - f->next = *previousP; - *previousP = f; - f = next; } - } #ifdef DD_COUNT - table->swapSteps += oldxkeys - newxkeys; + table->swapSteps += oldxkeys - newxkeys; #endif - /* Take care of the x nodes that must be re-expressed. - ** They form a linked list pointed by g. Their index has been - ** already changed to yindex. - */ - f = g; - while (f != NULL) { - next = f->next; - /* Find f1, f0, f11, f10, f01, f00. */ - f1 = cuddT(f); + /* Take care of the x nodes that must be re-expressed. + ** They form a linked list pointed by g. Their index has been + ** already changed to yindex. + */ + f = g; + while (f != NULL) { + next = f->next; + /* Find f1, f0, f11, f10, f01, f00. */ + f1 = cuddT(f); #ifdef DD_DEBUG - assert(!(Cudd_IsComplement(f1))); + assert(!(Cudd_IsComplement(f1))); #endif - if ((int) f1->index == yindex) { - f11 = cuddT(f1); f10 = cuddE(f1); - } else { - f11 = f10 = f1; - } + if ((int) f1->index == yindex) { + f11 = cuddT(f1); f10 = cuddE(f1); + } else { + f11 = f10 = f1; + } #ifdef DD_DEBUG - assert(!(Cudd_IsComplement(f11))); + assert(!(Cudd_IsComplement(f11))); #endif - f0 = cuddE(f); - comple = Cudd_IsComplement(f0); - f0 = Cudd_Regular(f0); - if ((int) f0->index == yindex) { - f01 = cuddT(f0); f00 = cuddE(f0); - } else { - f01 = f00 = f0; - } - if (comple) { - f01 = Cudd_Not(f01); - f00 = Cudd_Not(f00); - } - /* Decrease ref count of f1. */ - cuddSatDec(f1->ref); - /* Create the new T child. */ - if (f11 == f01) { - newf1 = f11; - cuddSatInc(newf1->ref); - } else { - /* Check xlist for triple (xindex,f11,f01). */ - posn = ddHash(f11, f01, xshift); - /* For each element newf1 in collision list xlist[posn]. */ - previousP = &(xlist[posn]); - newf1 = *previousP; - while (f11 < cuddT(newf1)) { - previousP = &(newf1->next); - newf1 = *previousP; - } - while (f11 == cuddT(newf1) && f01 < cuddE(newf1)) { - previousP = &(newf1->next); - newf1 = *previousP; - } - if (cuddT(newf1) == f11 && cuddE(newf1) == f01) { - cuddSatInc(newf1->ref); - } else { /* no match */ - newf1 = cuddDynamicAllocNode(table); - if (newf1 == NULL) - goto cuddSwapOutOfMem; - newf1->index = xindex; newf1->ref = 1; - cuddT(newf1) = f11; - cuddE(newf1) = f01; - /* Insert newf1 in the collision list xlist[posn]; - ** increase the ref counts of f11 and f01. - */ - newxkeys++; - newf1->next = *previousP; - *previousP = newf1; - cuddSatInc(f11->ref); - tmp = Cudd_Regular(f01); - cuddSatInc(tmp->ref); - } - } - cuddT(f) = newf1; + f0 = cuddE(f); + comple = Cudd_IsComplement(f0); + f0 = Cudd_Regular(f0); + if ((int) f0->index == yindex) { + f01 = cuddT(f0); f00 = cuddE(f0); + } else { + f01 = f00 = f0; + } + if (comple) { + f01 = Cudd_Not(f01); + f00 = Cudd_Not(f00); + } + /* Decrease ref count of f1. */ + cuddSatDec(f1->ref); + /* Create the new T child. */ + if (f11 == f01) { + newf1 = f11; + cuddSatInc(newf1->ref); + } else { + /* Check xlist for triple (xindex,f11,f01). */ + posn = ddHash(f11, f01, xshift); + /* For each element newf1 in collision list xlist[posn]. */ + previousP = &(xlist[posn]); + newf1 = *previousP; + while (f11 < cuddT(newf1)) { + previousP = &(newf1->next); + newf1 = *previousP; + } + while (f11 == cuddT(newf1) && f01 < cuddE(newf1)) { + previousP = &(newf1->next); + newf1 = *previousP; + } + if (cuddT(newf1) == f11 && cuddE(newf1) == f01) { + cuddSatInc(newf1->ref); + } else { /* no match */ + newf1 = cuddDynamicAllocNode(table); + if (newf1 == NULL) + goto cuddSwapOutOfMem; + newf1->index = xindex; newf1->ref = 1; + cuddT(newf1) = f11; + cuddE(newf1) = f01; + /* Insert newf1 in the collision list xlist[posn]; + ** increase the ref counts of f11 and f01. + */ + newxkeys++; + newf1->next = *previousP; + *previousP = newf1; + cuddSatInc(f11->ref); + tmp = Cudd_Regular(f01); + cuddSatInc(tmp->ref); + } + } + cuddT(f) = newf1; #ifdef DD_DEBUG - assert(!(Cudd_IsComplement(newf1))); + assert(!(Cudd_IsComplement(newf1))); #endif - /* Do the same for f0, keeping complement dots into account. */ - /* Decrease ref count of f0. */ - tmp = Cudd_Regular(f0); - cuddSatDec(tmp->ref); - /* Create the new E child. */ - if (f10 == f00) { - newf0 = f00; - tmp = Cudd_Regular(newf0); - cuddSatInc(tmp->ref); - } else { - /* make sure f10 is regular */ - newcomplement = Cudd_IsComplement(f10); - if (newcomplement) { - f10 = Cudd_Not(f10); - f00 = Cudd_Not(f00); - } - /* Check xlist for triple (xindex,f10,f00). */ - posn = ddHash(f10, f00, xshift); - /* For each element newf0 in collision list xlist[posn]. */ - previousP = &(xlist[posn]); - newf0 = *previousP; - while (f10 < cuddT(newf0)) { - previousP = &(newf0->next); - newf0 = *previousP; - } - while (f10 == cuddT(newf0) && f00 < cuddE(newf0)) { - previousP = &(newf0->next); - newf0 = *previousP; - } - if (cuddT(newf0) == f10 && cuddE(newf0) == f00) { - cuddSatInc(newf0->ref); - } else { /* no match */ - newf0 = cuddDynamicAllocNode(table); - if (newf0 == NULL) - goto cuddSwapOutOfMem; - newf0->index = xindex; newf0->ref = 1; - cuddT(newf0) = f10; - cuddE(newf0) = f00; - /* Insert newf0 in the collision list xlist[posn]; - ** increase the ref counts of f10 and f00. - */ - newxkeys++; - newf0->next = *previousP; - *previousP = newf0; - cuddSatInc(f10->ref); - tmp = Cudd_Regular(f00); - cuddSatInc(tmp->ref); - } - if (newcomplement) { - newf0 = Cudd_Not(newf0); - } - } - cuddE(f) = newf0; - - /* Insert the modified f in ylist. - ** The modified f does not already exists in ylist. - ** (Because of the uniqueness of the cofactors.) - */ - posn = ddHash(newf1, newf0, yshift); - newykeys++; - previousP = &(ylist[posn]); - tmp = *previousP; - while (newf1 < cuddT(tmp)) { - previousP = &(tmp->next); - tmp = *previousP; - } - while (newf1 == cuddT(tmp) && newf0 < cuddE(tmp)) { - previousP = &(tmp->next); - tmp = *previousP; - } - f->next = *previousP; - *previousP = f; - f = next; - } /* while f != NULL */ - - /* GC the y layer. */ - - /* For each node f in ylist. */ - for (i = 0; i < yslots; i++) { - previousP = &(ylist[i]); - f = *previousP; - while (f != sentinel) { - next = f->next; - if (f->ref == 0) { - tmp = cuddT(f); - cuddSatDec(tmp->ref); - tmp = Cudd_Regular(cuddE(f)); + /* Do the same for f0, keeping complement dots into account. */ + /* Decrease ref count of f0. */ + tmp = Cudd_Regular(f0); cuddSatDec(tmp->ref); - cuddDeallocNode(table,f); - newykeys--; - } else { + /* Create the new E child. */ + if (f10 == f00) { + newf0 = f00; + tmp = Cudd_Regular(newf0); + cuddSatInc(tmp->ref); + } else { + /* make sure f10 is regular */ + newcomplement = Cudd_IsComplement(f10); + if (newcomplement) { + f10 = Cudd_Not(f10); + f00 = Cudd_Not(f00); + } + /* Check xlist for triple (xindex,f10,f00). */ + posn = ddHash(f10, f00, xshift); + /* For each element newf0 in collision list xlist[posn]. */ + previousP = &(xlist[posn]); + newf0 = *previousP; + while (f10 < cuddT(newf0)) { + previousP = &(newf0->next); + newf0 = *previousP; + } + while (f10 == cuddT(newf0) && f00 < cuddE(newf0)) { + previousP = &(newf0->next); + newf0 = *previousP; + } + if (cuddT(newf0) == f10 && cuddE(newf0) == f00) { + cuddSatInc(newf0->ref); + } else { /* no match */ + newf0 = cuddDynamicAllocNode(table); + if (newf0 == NULL) + goto cuddSwapOutOfMem; + newf0->index = xindex; newf0->ref = 1; + cuddT(newf0) = f10; + cuddE(newf0) = f00; + /* Insert newf0 in the collision list xlist[posn]; + ** increase the ref counts of f10 and f00. + */ + newxkeys++; + newf0->next = *previousP; + *previousP = newf0; + cuddSatInc(f10->ref); + tmp = Cudd_Regular(f00); + cuddSatInc(tmp->ref); + } + if (newcomplement) { + newf0 = Cudd_Not(newf0); + } + } + cuddE(f) = newf0; + + /* Insert the modified f in ylist. + ** The modified f does not already exists in ylist. + ** (Because of the uniqueness of the cofactors.) + */ + posn = ddHash(newf1, newf0, yshift); + newykeys++; + previousP = &(ylist[posn]); + tmp = *previousP; + while (newf1 < cuddT(tmp)) { + previousP = &(tmp->next); + tmp = *previousP; + } + while (newf1 == cuddT(tmp) && newf0 < cuddE(tmp)) { + previousP = &(tmp->next); + tmp = *previousP; + } + f->next = *previousP; *previousP = f; - previousP = &(f->next); - } - f = next; - } /* while f */ - *previousP = sentinel; - } /* for i */ + f = next; + } /* while f != NULL */ + + /* GC the y layer. */ + + /* For each node f in ylist. */ + for (i = 0; i < yslots; i++) { + previousP = &(ylist[i]); + f = *previousP; + while (f != sentinel) { + next = f->next; + if (f->ref == 0) { + tmp = cuddT(f); + cuddSatDec(tmp->ref); + tmp = Cudd_Regular(cuddE(f)); + cuddSatDec(tmp->ref); + cuddDeallocNode(table,f); + newykeys--; + } else { + *previousP = f; + previousP = &(f->next); + } + f = next; + } /* while f */ + *previousP = sentinel; + } /* for i */ -#if DD_DEBUG +#ifdef DD_DEBUG #if 0 - (void) fprintf(table->out,"Swapping %d and %d\n",x,y); + (void) fprintf(table->out,"Swapping %d and %d\n",x,y); #endif - count = 0; - idcheck = 0; - for (i = 0; i < yslots; i++) { - f = ylist[i]; - while (f != sentinel) { - count++; - if (f->index != (DdHalfWord) yindex) - idcheck++; - f = f->next; + count = 0; + idcheck = 0; + for (i = 0; i < yslots; i++) { + f = ylist[i]; + while (f != sentinel) { + count++; + if (f->index != (DdHalfWord) yindex) + idcheck++; + f = f->next; + } } - } - if (count != newykeys) { - (void) fprintf(table->out, - "Error in finding newykeys\toldykeys = %d\tnewykeys = %d\tactual = %d\n", - oldykeys,newykeys,count); - } - if (idcheck != 0) - (void) fprintf(table->out, - "Error in id's of ylist\twrong id's = %d\n", - idcheck); - count = 0; - idcheck = 0; - for (i = 0; i < xslots; i++) { - f = xlist[i]; - while (f != sentinel) { - count++; - if (f->index != (DdHalfWord) xindex) - idcheck++; - f = f->next; + if (count != newykeys) { + (void) fprintf(table->out, + "Error in finding newykeys\toldykeys = %d\tnewykeys = %d\tactual = %d\n", + oldykeys,newykeys,count); } - } - if (count != newxkeys) { - (void) fprintf(table->out, - "Error in finding newxkeys\toldxkeys = %d \tnewxkeys = %d \tactual = %d\n", - oldxkeys,newxkeys,count); - } - if (idcheck != 0) - (void) fprintf(table->out, - "Error in id's of xlist\twrong id's = %d\n", - idcheck); + if (idcheck != 0) + (void) fprintf(table->out, + "Error in id's of ylist\twrong id's = %d\n", + idcheck); + count = 0; + idcheck = 0; + for (i = 0; i < xslots; i++) { + f = xlist[i]; + while (f != sentinel) { + count++; + if (f->index != (DdHalfWord) xindex) + idcheck++; + f = f->next; + } + } + if (count != newxkeys) { + (void) fprintf(table->out, + "Error in finding newxkeys\toldxkeys = %d \tnewxkeys = %d \tactual = %d\n", + oldxkeys,newxkeys,count); + } + if (idcheck != 0) + (void) fprintf(table->out, + "Error in id's of xlist\twrong id's = %d\n", + idcheck); #endif - isolated += (table->vars[xindex]->ref == 1) + - (table->vars[yindex]->ref == 1); - table->isolated += isolated; + isolated += (table->vars[xindex]->ref == 1) + + (table->vars[yindex]->ref == 1); + table->isolated += isolated; } /* Set the appropriate fields in table. */ @@ -1212,31 +1246,31 @@ int cuddBddAlignToZdd( DdManager * table /* DD manager */) { - int *invperm; /* permutation array */ - int M; /* ratio of ZDD variables to BDD variables */ - int i; /* loop index */ - int result; /* return value */ + int *invperm; /* permutation array */ + int M; /* ratio of ZDD variables to BDD variables */ + int i; /* loop index */ + int result; /* return value */ /* We assume that a ratio of 0 is OK. */ if (table->size == 0) - return(1); + return(1); M = table->sizeZ / table->size; /* Check whether the number of ZDD variables is a multiple of the ** number of BDD variables. */ if (M * table->size != table->sizeZ) - return(0); + return(0); /* Create and initialize the inverse permutation array. */ invperm = ABC_ALLOC(int,table->size); if (invperm == NULL) { - table->errorCode = CUDD_MEMORY_OUT; - return(0); + table->errorCode = CUDD_MEMORY_OUT; + return(0); } for (i = 0; i < table->sizeZ; i += M) { - int indexZ = table->invpermZ[i]; - int index = indexZ / M; - invperm[i / M] = index; + int indexZ = table->invpermZ[i]; + int index = indexZ / M; + invperm[i / M] = index; } /* Eliminate dead nodes. Do not scan the cache again, because we ** assume that Cudd_zddReduceHeap has already cleared it. @@ -1246,7 +1280,7 @@ cuddBddAlignToZdd( /* Initialize number of isolated projection functions. */ table->isolated = 0; for (i = 0; i < table->size; i++) { - if (table->vars[i]->ref == 1) table->isolated++; + if (table->vars[i]->ref == 1) table->isolated++; } /* Initialize the interaction matrix. */ @@ -1287,7 +1321,7 @@ ddUniqueCompare( { #if 0 if (entry[*ptrY] == entry[*ptrX]) { - return((*ptrX) - (*ptrY)); + return((*ptrX) - (*ptrY)); } #endif return(entry[*ptrY] - entry[*ptrX]); @@ -1310,15 +1344,15 @@ ddSwapAny( int x, int y) { - Move *move, *moves; - int xRef,yRef; - int xNext,yNext; - int size; - int limitSize; - int tmp; + Move *move, *moves; + int xRef,yRef; + int xNext,yNext; + int size; + int limitSize; + int tmp; if (x >y) { - tmp = x; x = y; y = tmp; + tmp = x; x = y; y = tmp; } xRef = x; yRef = y; @@ -1329,64 +1363,86 @@ ddSwapAny( limitSize = table->keys - table->isolated; for (;;) { - if ( xNext == yNext) { - size = cuddSwapInPlace(table,x,xNext); - if (size == 0) goto ddSwapAnyOutOfMem; - move = (Move *) cuddDynamicAllocNode(table); - if (move == NULL) goto ddSwapAnyOutOfMem; - move->x = x; - move->y = xNext; - move->size = size; - move->next = moves; - moves = move; - - size = cuddSwapInPlace(table,yNext,y); - if (size == 0) goto ddSwapAnyOutOfMem; - move = (Move *) cuddDynamicAllocNode(table); - if (move == NULL) goto ddSwapAnyOutOfMem; - move->x = yNext; - move->y = y; - move->size = size; - move->next = moves; - moves = move; - - size = cuddSwapInPlace(table,x,xNext); - if (size == 0) goto ddSwapAnyOutOfMem; - move = (Move *) cuddDynamicAllocNode(table); - if (move == NULL) goto ddSwapAnyOutOfMem; - move->x = x; - move->y = xNext; - move->size = size; - move->next = moves; - moves = move; + if ( xNext == yNext) { + size = cuddSwapInPlace(table,x,xNext); + if (size == 0) goto ddSwapAnyOutOfMem; + move = (Move *) cuddDynamicAllocNode(table); + if (move == NULL) goto ddSwapAnyOutOfMem; + move->x = x; + move->y = xNext; + move->size = size; + move->next = moves; + moves = move; + + size = cuddSwapInPlace(table,yNext,y); + if (size == 0) goto ddSwapAnyOutOfMem; + move = (Move *) cuddDynamicAllocNode(table); + if (move == NULL) goto ddSwapAnyOutOfMem; + move->x = yNext; + move->y = y; + move->size = size; + move->next = moves; + moves = move; + + size = cuddSwapInPlace(table,x,xNext); + if (size == 0) goto ddSwapAnyOutOfMem; + move = (Move *) cuddDynamicAllocNode(table); + if (move == NULL) goto ddSwapAnyOutOfMem; + move->x = x; + move->y = xNext; + move->size = size; + move->next = moves; + moves = move; + + tmp = x; x = y; y = tmp; + + } else if (x == yNext) { + + size = cuddSwapInPlace(table,x,xNext); + if (size == 0) goto ddSwapAnyOutOfMem; + move = (Move *) cuddDynamicAllocNode(table); + if (move == NULL) goto ddSwapAnyOutOfMem; + move->x = x; + move->y = xNext; + move->size = size; + move->next = moves; + moves = move; + + tmp = x; x = y; y = tmp; - tmp = x; x = y; y = tmp; - - } else if (x == yNext) { - - size = cuddSwapInPlace(table,x,xNext); - if (size == 0) goto ddSwapAnyOutOfMem; - move = (Move *) cuddDynamicAllocNode(table); - if (move == NULL) goto ddSwapAnyOutOfMem; - move->x = x; - move->y = xNext; - move->size = size; - move->next = moves; - moves = move; - - tmp = x; x = y; y = tmp; + } else { + size = cuddSwapInPlace(table,x,xNext); + if (size == 0) goto ddSwapAnyOutOfMem; + move = (Move *) cuddDynamicAllocNode(table); + if (move == NULL) goto ddSwapAnyOutOfMem; + move->x = x; + move->y = xNext; + move->size = size; + move->next = moves; + moves = move; + + size = cuddSwapInPlace(table,yNext,y); + if (size == 0) goto ddSwapAnyOutOfMem; + move = (Move *) cuddDynamicAllocNode(table); + if (move == NULL) goto ddSwapAnyOutOfMem; + move->x = yNext; + move->y = y; + move->size = size; + move->next = moves; + moves = move; + + x = xNext; + y = yNext; + } - } else { - size = cuddSwapInPlace(table,x,xNext); - if (size == 0) goto ddSwapAnyOutOfMem; - move = (Move *) cuddDynamicAllocNode(table); - if (move == NULL) goto ddSwapAnyOutOfMem; - move->x = x; - move->y = xNext; - move->size = size; - move->next = moves; - moves = move; + xNext = cuddNextHigh(table,x); + yNext = cuddNextLow(table,y); + if (xNext > yRef) break; + if ((double) size > table->maxGrowth * (double) limitSize) break; + if (size < limitSize) limitSize = size; + } + if (yNext>=xRef) { size = cuddSwapInPlace(table,yNext,y); if (size == 0) goto ddSwapAnyOutOfMem; move = (Move *) cuddDynamicAllocNode(table); @@ -1396,37 +1452,15 @@ ddSwapAny( move->size = size; move->next = moves; moves = move; - - x = xNext; - y = yNext; - } - - xNext = cuddNextHigh(table,x); - yNext = cuddNextLow(table,y); - if (xNext > yRef) break; - - if ((double) size > table->maxGrowth * (double) limitSize) break; - if (size < limitSize) limitSize = size; - } - if (yNext>=xRef) { - size = cuddSwapInPlace(table,yNext,y); - if (size == 0) goto ddSwapAnyOutOfMem; - move = (Move *) cuddDynamicAllocNode(table); - if (move == NULL) goto ddSwapAnyOutOfMem; - move->x = yNext; - move->y = y; - move->size = size; - move->next = moves; - moves = move; } return(moves); - + ddSwapAnyOutOfMem: while (moves != NULL) { - move = moves->next; - cuddDeallocNode(table, (DdNode *) moves); - moves = move; + move = moves->next; + cuddDeallocMove(table, moves); + moves = move; } return(NULL); @@ -1453,11 +1487,11 @@ ddSiftingAux( int xHigh) { - Move *move; - Move *moveUp; /* list of up moves */ - Move *moveDown; /* list of down moves */ - int initialSize; - int result; + Move *move; + Move *moveUp; /* list of up moves */ + Move *moveDown; /* list of down moves */ + int initialSize; + int result; initialSize = table->keys - table->isolated; @@ -1465,75 +1499,75 @@ ddSiftingAux( moveUp = NULL; if (x == xLow) { - moveDown = ddSiftingDown(table,x,xHigh); - /* At this point x --> xHigh unless bounding occurred. */ - if (moveDown == (Move *) CUDD_OUT_OF_MEM) goto ddSiftingAuxOutOfMem; - /* Move backward and stop at best position. */ - result = ddSiftingBackward(table,initialSize,moveDown); - if (!result) goto ddSiftingAuxOutOfMem; + moveDown = ddSiftingDown(table,x,xHigh); + /* At this point x --> xHigh unless bounding occurred. */ + if (moveDown == (Move *) CUDD_OUT_OF_MEM) goto ddSiftingAuxOutOfMem; + /* Move backward and stop at best position. */ + result = ddSiftingBackward(table,initialSize,moveDown); + if (!result) goto ddSiftingAuxOutOfMem; } else if (x == xHigh) { - moveUp = ddSiftingUp(table,x,xLow); - /* At this point x --> xLow unless bounding occurred. */ - if (moveUp == (Move *) CUDD_OUT_OF_MEM) goto ddSiftingAuxOutOfMem; - /* Move backward and stop at best position. */ - result = ddSiftingBackward(table,initialSize,moveUp); - if (!result) goto ddSiftingAuxOutOfMem; + moveUp = ddSiftingUp(table,x,xLow); + /* At this point x --> xLow unless bounding occurred. */ + if (moveUp == (Move *) CUDD_OUT_OF_MEM) goto ddSiftingAuxOutOfMem; + /* Move backward and stop at best position. */ + result = ddSiftingBackward(table,initialSize,moveUp); + if (!result) goto ddSiftingAuxOutOfMem; } else if ((x - xLow) > (xHigh - x)) { /* must go down first: shorter */ - moveDown = ddSiftingDown(table,x,xHigh); - /* At this point x --> xHigh unless bounding occurred. */ - if (moveDown == (Move *) CUDD_OUT_OF_MEM) goto ddSiftingAuxOutOfMem; - if (moveDown != NULL) { - x = moveDown->y; - } - moveUp = ddSiftingUp(table,x,xLow); - if (moveUp == (Move *) CUDD_OUT_OF_MEM) goto ddSiftingAuxOutOfMem; - /* Move backward and stop at best position */ - result = ddSiftingBackward(table,initialSize,moveUp); - if (!result) goto ddSiftingAuxOutOfMem; + moveDown = ddSiftingDown(table,x,xHigh); + /* At this point x --> xHigh unless bounding occurred. */ + if (moveDown == (Move *) CUDD_OUT_OF_MEM) goto ddSiftingAuxOutOfMem; + if (moveDown != NULL) { + x = moveDown->y; + } + moveUp = ddSiftingUp(table,x,xLow); + if (moveUp == (Move *) CUDD_OUT_OF_MEM) goto ddSiftingAuxOutOfMem; + /* Move backward and stop at best position */ + result = ddSiftingBackward(table,initialSize,moveUp); + if (!result) goto ddSiftingAuxOutOfMem; } else { /* must go up first: shorter */ - moveUp = ddSiftingUp(table,x,xLow); - /* At this point x --> xLow unless bounding occurred. */ - if (moveUp == (Move *) CUDD_OUT_OF_MEM) goto ddSiftingAuxOutOfMem; - if (moveUp != NULL) { - x = moveUp->x; - } - moveDown = ddSiftingDown(table,x,xHigh); - if (moveDown == (Move *) CUDD_OUT_OF_MEM) goto ddSiftingAuxOutOfMem; - /* Move backward and stop at best position. */ - result = ddSiftingBackward(table,initialSize,moveDown); - if (!result) goto ddSiftingAuxOutOfMem; + moveUp = ddSiftingUp(table,x,xLow); + /* At this point x --> xLow unless bounding occurred. */ + if (moveUp == (Move *) CUDD_OUT_OF_MEM) goto ddSiftingAuxOutOfMem; + if (moveUp != NULL) { + x = moveUp->x; + } + moveDown = ddSiftingDown(table,x,xHigh); + if (moveDown == (Move *) CUDD_OUT_OF_MEM) goto ddSiftingAuxOutOfMem; + /* Move backward and stop at best position. */ + result = ddSiftingBackward(table,initialSize,moveDown); + if (!result) goto ddSiftingAuxOutOfMem; } while (moveDown != NULL) { - move = moveDown->next; - cuddDeallocNode(table, (DdNode *) moveDown); - moveDown = move; + move = moveDown->next; + cuddDeallocMove(table, moveDown); + moveDown = move; } while (moveUp != NULL) { - move = moveUp->next; - cuddDeallocNode(table, (DdNode *) moveUp); - moveUp = move; + move = moveUp->next; + cuddDeallocMove(table, moveUp); + moveUp = move; } return(1); ddSiftingAuxOutOfMem: if (moveDown != (Move *) CUDD_OUT_OF_MEM) { - while (moveDown != NULL) { - move = moveDown->next; - cuddDeallocNode(table, (DdNode *) moveDown); - moveDown = move; - } + while (moveDown != NULL) { + move = moveDown->next; + cuddDeallocMove(table, moveDown); + moveDown = move; + } } if (moveUp != (Move *) CUDD_OUT_OF_MEM) { - while (moveUp != NULL) { - move = moveUp->next; - cuddDeallocNode(table, (DdNode *) moveUp); - moveUp = move; - } + while (moveUp != NULL) { + move = moveUp->next; + cuddDeallocMove(table, moveUp); + moveUp = move; + } } return(0); @@ -1558,14 +1592,14 @@ ddSiftingUp( int y, int xLow) { - Move *moves; - Move *move; - int x; - int size; - int limitSize; - int xindex, yindex; - int isolated; - int L; /* lower bound on DD size */ + Move *moves; + Move *move; + int x; + int size; + int limitSize; + int xindex, yindex; + int isolated; + int L; /* lower bound on DD size */ #ifdef DD_DEBUG int checkL; int z; @@ -1583,62 +1617,62 @@ ddSiftingUp( */ limitSize = L = table->keys - table->isolated; for (x = xLow + 1; x < y; x++) { - xindex = table->invperm[x]; - if (cuddTestInteract(table,xindex,yindex)) { - isolated = table->vars[xindex]->ref == 1; - L -= table->subtables[x].keys - isolated; - } + xindex = table->invperm[x]; + if (cuddTestInteract(table,xindex,yindex)) { + isolated = table->vars[xindex]->ref == 1; + L -= table->subtables[x].keys - isolated; + } } isolated = table->vars[yindex]->ref == 1; L -= table->subtables[y].keys - isolated; x = cuddNextLow(table,y); while (x >= xLow && L <= limitSize) { - xindex = table->invperm[x]; + xindex = table->invperm[x]; #ifdef DD_DEBUG - checkL = table->keys - table->isolated; - for (z = xLow + 1; z < y; z++) { - zindex = table->invperm[z]; - if (cuddTestInteract(table,zindex,yindex)) { - isolated = table->vars[zindex]->ref == 1; - checkL -= table->subtables[z].keys - isolated; + checkL = table->keys - table->isolated; + for (z = xLow + 1; z < y; z++) { + zindex = table->invperm[z]; + if (cuddTestInteract(table,zindex,yindex)) { + isolated = table->vars[zindex]->ref == 1; + checkL -= table->subtables[z].keys - isolated; + } } - } - isolated = table->vars[yindex]->ref == 1; - checkL -= table->subtables[y].keys - isolated; - assert(L == checkL); + isolated = table->vars[yindex]->ref == 1; + checkL -= table->subtables[y].keys - isolated; + assert(L == checkL); #endif - size = cuddSwapInPlace(table,x,y); - if (size == 0) goto ddSiftingUpOutOfMem; - /* Update the lower bound. */ - if (cuddTestInteract(table,xindex,yindex)) { - isolated = table->vars[xindex]->ref == 1; - L += table->subtables[y].keys - isolated; - } - move = (Move *) cuddDynamicAllocNode(table); - if (move == NULL) goto ddSiftingUpOutOfMem; - move->x = x; - move->y = y; - move->size = size; - move->next = moves; - moves = move; - if ((double) size > (double) limitSize * table->maxGrowth) break; - if (size < limitSize) limitSize = size; - y = x; - x = cuddNextLow(table,y); + size = cuddSwapInPlace(table,x,y); + if (size == 0) goto ddSiftingUpOutOfMem; + /* Update the lower bound. */ + if (cuddTestInteract(table,xindex,yindex)) { + isolated = table->vars[xindex]->ref == 1; + L += table->subtables[y].keys - isolated; + } + move = (Move *) cuddDynamicAllocNode(table); + if (move == NULL) goto ddSiftingUpOutOfMem; + move->x = x; + move->y = y; + move->size = size; + move->next = moves; + moves = move; + if ((double) size > (double) limitSize * table->maxGrowth) break; + if (size < limitSize) limitSize = size; + y = x; + x = cuddNextLow(table,y); } return(moves); ddSiftingUpOutOfMem: while (moves != NULL) { - move = moves->next; - cuddDeallocNode(table, (DdNode *) moves); - moves = move; + move = moves->next; + cuddDeallocMove(table, moves); + moves = move; } return((Move *) CUDD_OUT_OF_MEM); } /* end of ddSiftingUp */ - + /**Function******************************************************************** @@ -1658,18 +1692,18 @@ ddSiftingDown( int x, int xHigh) { - Move *moves; - Move *move; - int y; - int size; - int R; /* upper bound on node decrease */ - int limitSize; - int xindex, yindex; - int isolated; + Move *moves; + Move *move; + int y; + int size; + int R; /* upper bound on node decrease */ + int limitSize; + int xindex, yindex; + int isolated; #ifdef DD_DEBUG - int checkR; - int z; - int zindex; + int checkR; + int z; + int zindex; #endif moves = NULL; @@ -1678,53 +1712,53 @@ ddSiftingDown( limitSize = size = table->keys - table->isolated; R = 0; for (y = xHigh; y > x; y--) { - yindex = table->invperm[y]; - if (cuddTestInteract(table,xindex,yindex)) { - isolated = table->vars[yindex]->ref == 1; - R += table->subtables[y].keys - isolated; - } + yindex = table->invperm[y]; + if (cuddTestInteract(table,xindex,yindex)) { + isolated = table->vars[yindex]->ref == 1; + R += table->subtables[y].keys - isolated; + } } y = cuddNextHigh(table,x); while (y <= xHigh && size - R < limitSize) { #ifdef DD_DEBUG - checkR = 0; - for (z = xHigh; z > x; z--) { - zindex = table->invperm[z]; - if (cuddTestInteract(table,xindex,zindex)) { - isolated = table->vars[zindex]->ref == 1; - checkR += table->subtables[z].keys - isolated; + checkR = 0; + for (z = xHigh; z > x; z--) { + zindex = table->invperm[z]; + if (cuddTestInteract(table,xindex,zindex)) { + isolated = table->vars[zindex]->ref == 1; + checkR += table->subtables[z].keys - isolated; + } } - } - assert(R == checkR); + assert(R == checkR); #endif - /* Update upper bound on node decrease. */ - yindex = table->invperm[y]; - if (cuddTestInteract(table,xindex,yindex)) { - isolated = table->vars[yindex]->ref == 1; - R -= table->subtables[y].keys - isolated; - } - size = cuddSwapInPlace(table,x,y); - if (size == 0) goto ddSiftingDownOutOfMem; - move = (Move *) cuddDynamicAllocNode(table); - if (move == NULL) goto ddSiftingDownOutOfMem; - move->x = x; - move->y = y; - move->size = size; - move->next = moves; - moves = move; - if ((double) size > (double) limitSize * table->maxGrowth) break; - if (size < limitSize) limitSize = size; - x = y; - y = cuddNextHigh(table,x); + /* Update upper bound on node decrease. */ + yindex = table->invperm[y]; + if (cuddTestInteract(table,xindex,yindex)) { + isolated = table->vars[yindex]->ref == 1; + R -= table->subtables[y].keys - isolated; + } + size = cuddSwapInPlace(table,x,y); + if (size == 0) goto ddSiftingDownOutOfMem; + move = (Move *) cuddDynamicAllocNode(table); + if (move == NULL) goto ddSiftingDownOutOfMem; + move->x = x; + move->y = y; + move->size = size; + move->next = moves; + moves = move; + if ((double) size > (double) limitSize * table->maxGrowth) break; + if (size < limitSize) limitSize = size; + x = y; + y = cuddNextHigh(table,x); } return(moves); ddSiftingDownOutOfMem: while (moves != NULL) { - move = moves->next; - cuddDeallocNode(table, (DdNode *) moves); - moves = move; + move = moves->next; + cuddDeallocMove(table, moves); + moves = move; } return((Move *) CUDD_OUT_OF_MEM); @@ -1751,18 +1785,18 @@ ddSiftingBackward( Move * moves) { Move *move; - int res; + int res; for (move = moves; move != NULL; move = move->next) { - if (move->size < size) { - size = move->size; - } + if (move->size < size) { + size = move->size; + } } for (move = moves; move != NULL; move = move->next) { - if (move->size == size) return(1); - res = cuddSwapInPlace(table,(int)move->x,(int)move->y); - if (!res) return(0); + if (move->size == size) return(1); + res = cuddSwapInPlace(table,(int)move->x,(int)move->y); + if (!res) return(0); } return(1); @@ -1800,7 +1834,7 @@ ddReorderPreprocess( /* Initialize number of isolated projection functions. */ table->isolated = 0; for (i = 0; i < table->size; i++) { - if (table->vars[i]->ref == 1) table->isolated++; + if (table->vars[i]->ref == 1) table->isolated++; } /* Initialize the interaction matrix. */ @@ -1859,16 +1893,16 @@ ddShuffle( DdManager * table, int * permutation) { - int index; - int level; - int position; - int numvars; - int result; + int index; + int level; + int position; + int numvars; + int result; #ifdef DD_STATS - long localTime; - int initialSize; - int finalSize; - int previousSize; + long localTime; + int initialSize; + int finalSize; + int previousSize; #endif ddTotalNumberSwapping = 0; @@ -1876,40 +1910,40 @@ ddShuffle( localTime = util_cpu_time(); initialSize = table->keys - table->isolated; (void) fprintf(table->out,"#:I_SHUFFLE %8d: initial size\n", - initialSize); + initialSize); ddTotalNISwaps = 0; #endif numvars = table->size; for (level = 0; level < numvars; level++) { - index = permutation[level]; - position = table->perm[index]; + index = permutation[level]; + position = table->perm[index]; #ifdef DD_STATS - previousSize = table->keys - table->isolated; + previousSize = table->keys - table->isolated; #endif - result = ddSiftUp(table,position,level); - if (!result) return(0); + result = ddSiftUp(table,position,level); + if (!result) return(0); #ifdef DD_STATS - if (table->keys < (unsigned) previousSize + table->isolated) { - (void) fprintf(table->out,"-"); - } else if (table->keys > (unsigned) previousSize + table->isolated) { - (void) fprintf(table->out,"+"); /* should never happen */ - } else { - (void) fprintf(table->out,"="); - } - fflush(table->out); + if (table->keys < (unsigned) previousSize + table->isolated) { + (void) fprintf(table->out,"-"); + } else if (table->keys > (unsigned) previousSize + table->isolated) { + (void) fprintf(table->out,"+"); /* should never happen */ + } else { + (void) fprintf(table->out,"="); + } + fflush(table->out); #endif } #ifdef DD_STATS (void) fprintf(table->out,"\n"); finalSize = table->keys - table->isolated; - (void) fprintf(table->out,"#:F_SHUFFLE %8d: final size\n",finalSize); + (void) fprintf(table->out,"#:F_SHUFFLE %8d: final size\n",finalSize); (void) fprintf(table->out,"#:T_SHUFFLE %8g: total time (sec)\n", - ((double)(util_cpu_time() - localTime)/1000.0)); + ((double)(util_cpu_time() - localTime)/1000.0)); (void) fprintf(table->out,"#:N_SHUFFLE %8d: total swaps\n", - ddTotalNumberSwapping); + ddTotalNumberSwapping); (void) fprintf(table->out,"#:M_SHUFFLE %8d: NI swaps\n",ddTotalNISwaps); #endif @@ -1942,12 +1976,12 @@ ddSiftUp( y = cuddNextLow(table,x); while (y >= xLow) { - size = cuddSwapInPlace(table,y,x); - if (size == 0) { - return(0); - } - x = y; - y = cuddNextLow(table,x); + size = cuddSwapInPlace(table,y,x); + if (size == 0) { + return(0); + } + x = y; + y = cuddNextLow(table,x); } return(1); @@ -1974,15 +2008,15 @@ bddFixTree( { if (treenode == NULL) return; treenode->low = ((int) treenode->index < table->size) ? - table->perm[treenode->index] : treenode->index; + table->perm[treenode->index] : treenode->index; if (treenode->child != NULL) { - bddFixTree(table, treenode->child); + bddFixTree(table, treenode->child); } if (treenode->younger != NULL) - bddFixTree(table, treenode->younger); + bddFixTree(table, treenode->younger); if (treenode->parent != NULL && treenode->low < treenode->parent->low) { - treenode->parent->low = treenode->low; - treenode->parent->index = treenode->index; + treenode->parent->low = treenode->low; + treenode->parent->index = treenode->index; } return; @@ -2008,36 +2042,41 @@ ddUpdateMtrTree( int * perm, int * invperm) { - int i, size, index, level; - int minLevel = table->size, maxLevel = 0, minIndex = 0; // Suppress "might be used uninitialized" + int i, size; + int index, level, minLevel, maxLevel, minIndex; if (treenode == NULL) return(1); + minLevel = CUDD_MAXINDEX; + maxLevel = 0; + minIndex = -1; /* i : level */ for (i = treenode->low; i < treenode->low + treenode->size; i++) { - index = table->invperm[i]; - level = perm[index]; - if (level < minLevel) { - minLevel = level; - minIndex = index; - } - if (level > maxLevel) - maxLevel = level; + index = table->invperm[i]; + level = perm[index]; + if (level < minLevel) { + minLevel = level; + minIndex = index; + } + if (level > maxLevel) + maxLevel = level; } size = maxLevel - minLevel + 1; + if (minIndex == -1) return(0); if (size == treenode->size) { - treenode->low = minLevel; - treenode->index = minIndex; - } else - return(0); + treenode->low = minLevel; + treenode->index = minIndex; + } else { + return(0); + } if (treenode->child != NULL) { - if (!ddUpdateMtrTree(table, treenode->child, perm, invperm)) - return(0); + if (!ddUpdateMtrTree(table, treenode->child, perm, invperm)) + return(0); } if (treenode->younger != NULL) { - if (!ddUpdateMtrTree(table, treenode->younger, perm, invperm)) - return(0); + if (!ddUpdateMtrTree(table, treenode->younger, perm, invperm)) + return(0); } return(1); } @@ -2062,8 +2101,8 @@ ddCheckPermuation( int * perm, int * invperm) { - int i, size, index, level; - int minLevel, maxLevel; + int i, size; + int index, level, minLevel, maxLevel; if (treenode == NULL) return(1); @@ -2071,26 +2110,28 @@ ddCheckPermuation( maxLevel = 0; /* i : level */ for (i = treenode->low; i < treenode->low + treenode->size; i++) { - index = table->invperm[i]; - level = perm[index]; - if (level < minLevel) - minLevel = level; - if (level > maxLevel) - maxLevel = level; + index = table->invperm[i]; + level = perm[index]; + if (level < minLevel) + minLevel = level; + if (level > maxLevel) + maxLevel = level; } size = maxLevel - minLevel + 1; if (size != treenode->size) - return(0); + return(0); if (treenode->child != NULL) { - if (!ddCheckPermuation(table, treenode->child, perm, invperm)) - return(0); + if (!ddCheckPermuation(table, treenode->child, perm, invperm)) + return(0); } if (treenode->younger != NULL) { - if (!ddCheckPermuation(table, treenode->younger, perm, invperm)) - return(0); + if (!ddCheckPermuation(table, treenode->younger, perm, invperm)) + return(0); } return(1); } + + ABC_NAMESPACE_IMPL_END |