| [13] | 1 | /**CFile*********************************************************************** |
|---|
| 2 | |
|---|
| 3 | FileName [calGC.c] |
|---|
| 4 | |
|---|
| 5 | PackageName [cal] |
|---|
| 6 | |
|---|
| 7 | Synopsis [Garbage collection routines] |
|---|
| 8 | |
|---|
| 9 | Description [optional] |
|---|
| 10 | |
|---|
| 11 | SeeAlso [optional] |
|---|
| 12 | |
|---|
| 13 | Author [Jagesh Sanghavi (sanghavi@eecs.berkeley.edu) |
|---|
| 14 | Rajeev Ranjan (rajeev@eecs.berkeley.edu)] |
|---|
| 15 | |
|---|
| 16 | Copyright [Copyright (c) 1994-1996 The Regents of the Univ. of California. |
|---|
| 17 | All rights reserved. |
|---|
| 18 | |
|---|
| 19 | Permission is hereby granted, without written agreement and without license |
|---|
| 20 | or royalty fees, to use, copy, modify, and distribute this software and its |
|---|
| 21 | documentation for any purpose, provided that the above copyright notice and |
|---|
| 22 | the following two paragraphs appear in all copies of this software. |
|---|
| 23 | |
|---|
| 24 | IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR |
|---|
| 25 | DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT |
|---|
| 26 | OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF |
|---|
| 27 | CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. |
|---|
| 28 | |
|---|
| 29 | THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES, |
|---|
| 30 | INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND |
|---|
| 31 | FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS ON AN |
|---|
| 32 | "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE |
|---|
| 33 | MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.] |
|---|
| 34 | |
|---|
| 35 | Revision [$Id: calGC.c,v 1.2 1998/09/16 16:08:40 ravi Exp $] |
|---|
| 36 | |
|---|
| 37 | ******************************************************************************/ |
|---|
| 38 | |
|---|
| 39 | #include "calInt.h" |
|---|
| 40 | |
|---|
| 41 | |
|---|
| 42 | /*---------------------------------------------------------------------------*/ |
|---|
| 43 | /* Constant declarations */ |
|---|
| 44 | /*---------------------------------------------------------------------------*/ |
|---|
| 45 | |
|---|
| 46 | /*---------------------------------------------------------------------------*/ |
|---|
| 47 | /* Type declarations */ |
|---|
| 48 | /*---------------------------------------------------------------------------*/ |
|---|
| 49 | |
|---|
| 50 | /*---------------------------------------------------------------------------*/ |
|---|
| 51 | /* Stucture declarations */ |
|---|
| 52 | /*---------------------------------------------------------------------------*/ |
|---|
| 53 | |
|---|
| 54 | /*---------------------------------------------------------------------------*/ |
|---|
| 55 | /* Variable declarations */ |
|---|
| 56 | /*---------------------------------------------------------------------------*/ |
|---|
| 57 | |
|---|
| 58 | /*---------------------------------------------------------------------------*/ |
|---|
| 59 | /* Macro declarations */ |
|---|
| 60 | /*---------------------------------------------------------------------------*/ |
|---|
| 61 | |
|---|
| 62 | /**AutomaticStart*************************************************************/ |
|---|
| 63 | |
|---|
| 64 | /*---------------------------------------------------------------------------*/ |
|---|
| 65 | /* Static function prototypes */ |
|---|
| 66 | /*---------------------------------------------------------------------------*/ |
|---|
| 67 | |
|---|
| 68 | static int CeilLog2(int number); |
|---|
| 69 | |
|---|
| 70 | /**AutomaticEnd***************************************************************/ |
|---|
| 71 | |
|---|
| 72 | |
|---|
| 73 | /*---------------------------------------------------------------------------*/ |
|---|
| 74 | /* Definition of exported functions */ |
|---|
| 75 | /*---------------------------------------------------------------------------*/ |
|---|
| 76 | /**Function******************************************************************** |
|---|
| 77 | |
|---|
| 78 | Synopsis [Sets the garbage collection mode, 0 means the garbage |
|---|
| 79 | collection should be turned off, 1 means garbage collection should |
|---|
| 80 | be on.] |
|---|
| 81 | |
|---|
| 82 | Description [Sets the garbage collection mode, 0 means the garbage |
|---|
| 83 | collection should be turned off, 1 means garbage collection should |
|---|
| 84 | be on.] |
|---|
| 85 | |
|---|
| 86 | SideEffects [None.] |
|---|
| 87 | |
|---|
| 88 | ******************************************************************************/ |
|---|
| 89 | void |
|---|
| 90 | Cal_BddSetGCMode( |
|---|
| 91 | Cal_BddManager bddManager, |
|---|
| 92 | int gcMode) |
|---|
| 93 | { |
|---|
| 94 | bddManager->gcMode = gcMode; |
|---|
| 95 | } |
|---|
| 96 | |
|---|
| 97 | |
|---|
| 98 | /**Function******************************************************************** |
|---|
| 99 | |
|---|
| 100 | Synopsis [Invokes the garbage collection at the manager level.] |
|---|
| 101 | |
|---|
| 102 | Description [For each variable in the increasing id free nodes with reference |
|---|
| 103 | count equal to zero freeing a node results in decrementing reference count of |
|---|
| 104 | then and else nodes by one.] |
|---|
| 105 | |
|---|
| 106 | SideEffects [None.] |
|---|
| 107 | |
|---|
| 108 | ******************************************************************************/ |
|---|
| 109 | int |
|---|
| 110 | Cal_BddManagerGC(Cal_BddManager bddManager) |
|---|
| 111 | { |
|---|
| 112 | Cal_BddIndex_t index; |
|---|
| 113 | Cal_BddId_t id; |
|---|
| 114 | int numNodesFreed; |
|---|
| 115 | /* unsigned long origNodes = bddManager->numNodes; */ |
|---|
| 116 | |
|---|
| 117 | if (bddManager->numPeakNodes < (bddManager->numNodes + |
|---|
| 118 | bddManager->numForwardedNodes)){ |
|---|
| 119 | bddManager->numPeakNodes = bddManager->numNodes + |
|---|
| 120 | bddManager->numForwardedNodes ; |
|---|
| 121 | } |
|---|
| 122 | |
|---|
| 123 | CalHashTableGC(bddManager, bddManager->uniqueTable[0]); |
|---|
| 124 | for(index = 0; index < bddManager->numVars; index++){ |
|---|
| 125 | id = bddManager->indexToId[index]; |
|---|
| 126 | numNodesFreed = CalHashTableGC(bddManager, bddManager->uniqueTable[id]); |
|---|
| 127 | bddManager->numNodes -= numNodesFreed; |
|---|
| 128 | bddManager->numNodesFreed += numNodesFreed; |
|---|
| 129 | } |
|---|
| 130 | /* Free the cache entries related to unused BDD nodes */ |
|---|
| 131 | /* The assumption is that during CalHashTableGC, the freed BDD nodes |
|---|
| 132 | are marked. However, since they are not touched after being put |
|---|
| 133 | on the free list, the mark should be unaffected and can be used |
|---|
| 134 | for cleaning up the cache table. |
|---|
| 135 | */ |
|---|
| 136 | CalCacheTableTwoGCFlush(bddManager->cacheTable); |
|---|
| 137 | bddManager->numGC++; |
|---|
| 138 | return 0; |
|---|
| 139 | } |
|---|
| 140 | |
|---|
| 141 | /**Function******************************************************************** |
|---|
| 142 | |
|---|
| 143 | Synopsis [Sets the limit of the garbage collection.] |
|---|
| 144 | |
|---|
| 145 | Description [It tries to set the limit at twice the number of nodes |
|---|
| 146 | in the manager at the current point. However, the limit is not |
|---|
| 147 | allowed to fall below the MIN_GC_LIMIT or to exceed the value of |
|---|
| 148 | node limit (if one exists).] |
|---|
| 149 | |
|---|
| 150 | SideEffects [None.] |
|---|
| 151 | |
|---|
| 152 | ******************************************************************************/ |
|---|
| 153 | void |
|---|
| 154 | Cal_BddManagerSetGCLimit(Cal_BddManager manager) |
|---|
| 155 | { |
|---|
| 156 | manager->uniqueTableGCLimit = ((manager->numNodes) << 1); |
|---|
| 157 | if(manager->uniqueTableGCLimit < CAL_MIN_GC_LIMIT){ |
|---|
| 158 | manager->uniqueTableGCLimit = CAL_MIN_GC_LIMIT; |
|---|
| 159 | } |
|---|
| 160 | if (manager->nodeLimit && (manager->uniqueTableGCLimit > |
|---|
| 161 | manager->nodeLimit)){ |
|---|
| 162 | manager->uniqueTableGCLimit = manager->nodeLimit; |
|---|
| 163 | } |
|---|
| 164 | } |
|---|
| 165 | |
|---|
| 166 | /*---------------------------------------------------------------------------*/ |
|---|
| 167 | /* Definition of internal functions */ |
|---|
| 168 | /*---------------------------------------------------------------------------*/ |
|---|
| 169 | /**Function******************************************************************** |
|---|
| 170 | |
|---|
| 171 | Synopsis [required] |
|---|
| 172 | |
|---|
| 173 | Description [optional] |
|---|
| 174 | |
|---|
| 175 | SideEffects [required] |
|---|
| 176 | |
|---|
| 177 | SeeAlso [optional] |
|---|
| 178 | |
|---|
| 179 | ******************************************************************************/ |
|---|
| 180 | void |
|---|
| 181 | CalBddManagerGCCheck(Cal_BddManager_t * bddManager) |
|---|
| 182 | { |
|---|
| 183 | if (bddManager->gcMode == 0) return; |
|---|
| 184 | if (bddManager->gcCheck > 0) return; |
|---|
| 185 | bddManager->gcCheck = CAL_GC_CHECK; |
|---|
| 186 | if(bddManager->numNodes > bddManager->uniqueTableGCLimit){ |
|---|
| 187 | Cal_BddManagerGC(bddManager); |
|---|
| 188 | Cal_BddManagerSetGCLimit(bddManager); |
|---|
| 189 | } |
|---|
| 190 | } |
|---|
| 191 | |
|---|
| 192 | /**Function******************************************************************** |
|---|
| 193 | |
|---|
| 194 | Synopsis [This function performs the garbage collection operation |
|---|
| 195 | for a particular index.] |
|---|
| 196 | |
|---|
| 197 | Description [The input is the hash table containing the nodes |
|---|
| 198 | belonging to that level. Each bin of the hash table is traversed and |
|---|
| 199 | the Bdd nodes with 0 reference count are put at the appropriate |
|---|
| 200 | level in the processing que of the manager.] |
|---|
| 201 | |
|---|
| 202 | SideEffects [The number of nodes in the hash table can possibly decrease.] |
|---|
| 203 | |
|---|
| 204 | SeeAlso [optional] |
|---|
| 205 | |
|---|
| 206 | ******************************************************************************/ |
|---|
| 207 | int |
|---|
| 208 | CalHashTableGC(Cal_BddManager_t *bddManager, CalHashTable_t *hashTable) |
|---|
| 209 | { |
|---|
| 210 | CalBddNode_t *last, *next, *ptr, *thenBddNode, *elseBddNode; |
|---|
| 211 | int i; |
|---|
| 212 | int oldNumEntries; |
|---|
| 213 | |
|---|
| 214 | oldNumEntries = hashTable->numEntries; |
|---|
| 215 | for(i = 0; i < hashTable->numBins; i++){ |
|---|
| 216 | last = NULL; |
|---|
| 217 | ptr = hashTable->bins[i]; |
|---|
| 218 | while(ptr != Cal_Nil(CalBddNode_t)){ |
|---|
| 219 | next = CalBddNodeGetNextBddNode(ptr); |
|---|
| 220 | if(CalBddNodeIsRefCountZero(ptr)){ |
|---|
| 221 | if (last == NULL){ |
|---|
| 222 | hashTable->bins[i] = next; |
|---|
| 223 | } |
|---|
| 224 | else{ |
|---|
| 225 | CalBddNodePutNextBddNode(last,next); |
|---|
| 226 | } |
|---|
| 227 | thenBddNode = CAL_BDD_POINTER(CalBddNodeGetThenBddNode(ptr)); |
|---|
| 228 | elseBddNode = CAL_BDD_POINTER(CalBddNodeGetElseBddNode(ptr)); |
|---|
| 229 | CalBddNodeDcrRefCount(thenBddNode); |
|---|
| 230 | CalBddNodeDcrRefCount(elseBddNode); |
|---|
| 231 | CalNodeManagerFreeNode(hashTable->nodeManager, ptr); |
|---|
| 232 | /* Mark the freed node for cache table clean up */ |
|---|
| 233 | /* We have to make sure that the clean up routine is called */ |
|---|
| 234 | /* right after this function (so that the marking remains */ |
|---|
| 235 | /* valid) */ |
|---|
| 236 | CalBddNodeMark(ptr); |
|---|
| 237 | hashTable->numEntries--; |
|---|
| 238 | } |
|---|
| 239 | else { |
|---|
| 240 | last = ptr; |
|---|
| 241 | } |
|---|
| 242 | ptr = next; |
|---|
| 243 | } |
|---|
| 244 | } |
|---|
| 245 | return oldNumEntries - hashTable->numEntries; |
|---|
| 246 | } |
|---|
| 247 | |
|---|
| 248 | |
|---|
| 249 | /**Function******************************************************************** |
|---|
| 250 | |
|---|
| 251 | Synopsis [required] |
|---|
| 252 | |
|---|
| 253 | Description [optional] |
|---|
| 254 | |
|---|
| 255 | SideEffects [required] |
|---|
| 256 | |
|---|
| 257 | SeeAlso [optional] |
|---|
| 258 | |
|---|
| 259 | ******************************************************************************/ |
|---|
| 260 | void |
|---|
| 261 | CalRepackNodesAfterGC(Cal_BddManager_t *bddManager) |
|---|
| 262 | { |
|---|
| 263 | int index, id, numPagesRequired, packingFlag, pageNum, nodeNum; |
|---|
| 264 | int rehashFlag = 0; |
|---|
| 265 | int newSizeIndex, hashValue; |
|---|
| 266 | CalNodeManager_t *nodeManager; |
|---|
| 267 | CalHashTable_t *uniqueTableForId; |
|---|
| 268 | CalBddNode_t *bddNode, *thenBddNode, *elseBddNode, *freeNodeList; |
|---|
| 269 | CalBddNode_t *newNode; |
|---|
| 270 | Cal_Bdd_t thenBdd, elseBdd; |
|---|
| 271 | |
|---|
| 272 | packingFlag = 0; |
|---|
| 273 | |
|---|
| 274 | for (index = bddManager->numVars-1; index >= 0; index--){ |
|---|
| 275 | id = bddManager->indexToId[index]; |
|---|
| 276 | uniqueTableForId = bddManager->uniqueTable[id]; |
|---|
| 277 | nodeManager = uniqueTableForId->nodeManager; |
|---|
| 278 | if (CalBddIdNeedsRepacking(bddManager, id) == 0){ |
|---|
| 279 | if (packingFlag == 0) continue; /* nothing needs to be done */ |
|---|
| 280 | /* We just need to update the cofactors and continue; */ |
|---|
| 281 | for (pageNum=0; pageNum < nodeManager->numPages; pageNum++){ |
|---|
| 282 | for(nodeNum = 0, |
|---|
| 283 | bddNode = (CalBddNode_t *)nodeManager->pageList[pageNum]; |
|---|
| 284 | nodeNum < NUM_NODES_PER_PAGE; nodeNum++, bddNode += 1){ |
|---|
| 285 | if (CalBddNodeIsRefCountZero(bddNode) || |
|---|
| 286 | CalBddNodeIsForwarded(bddNode)) continue; |
|---|
| 287 | thenBddNode = CalBddNodeGetThenBddNode(bddNode); |
|---|
| 288 | elseBddNode = CalBddNodeGetElseBddNode(bddNode); |
|---|
| 289 | CalBddNodeGetThenBdd(bddNode, thenBdd); |
|---|
| 290 | CalBddNodeGetElseBdd(bddNode, elseBdd); |
|---|
| 291 | if (CalBddIsForwarded(thenBdd)){ |
|---|
| 292 | CalBddForward(thenBdd); |
|---|
| 293 | CalBddNodePutThenBdd(bddNode, thenBdd); |
|---|
| 294 | rehashFlag = 1; |
|---|
| 295 | } |
|---|
| 296 | if (CalBddIsForwarded(elseBdd)){ |
|---|
| 297 | CalBddForward(elseBdd); |
|---|
| 298 | CalBddNodePutElseBdd(bddNode, elseBdd); |
|---|
| 299 | rehashFlag = 1; |
|---|
| 300 | } |
|---|
| 301 | Cal_Assert(!CalBddIsRefCountZero(thenBdd)); |
|---|
| 302 | Cal_Assert(!CalBddIsRefCountZero(elseBdd)); |
|---|
| 303 | Cal_Assert(bddManager->idToIndex[id] < |
|---|
| 304 | bddManager->idToIndex[bddNode->thenBddId]); |
|---|
| 305 | Cal_Assert(bddManager->idToIndex[id] < |
|---|
| 306 | bddManager->idToIndex[bddNode->elseBddId]); |
|---|
| 307 | if (rehashFlag){ |
|---|
| 308 | CalUniqueTableForIdRehashNode(uniqueTableForId, bddNode, |
|---|
| 309 | thenBddNode, elseBddNode); |
|---|
| 310 | } |
|---|
| 311 | } |
|---|
| 312 | } |
|---|
| 313 | continue; /* move to next higher index */ |
|---|
| 314 | } |
|---|
| 315 | packingFlag = 1; |
|---|
| 316 | if ((uniqueTableForId->numBins > uniqueTableForId->numEntries) && |
|---|
| 317 | (uniqueTableForId->sizeIndex > HASH_TABLE_DEFAULT_SIZE_INDEX)){ |
|---|
| 318 | /* Free the old bins */ |
|---|
| 319 | Cal_MemFree(uniqueTableForId->bins); |
|---|
| 320 | /* Create the new set of bins */ |
|---|
| 321 | newSizeIndex = |
|---|
| 322 | CeilLog2(uniqueTableForId->numEntries/HASH_TABLE_DEFAULT_MAX_DENSITY); |
|---|
| 323 | if (newSizeIndex < HASH_TABLE_DEFAULT_SIZE_INDEX){ |
|---|
| 324 | newSizeIndex = HASH_TABLE_DEFAULT_SIZE_INDEX; |
|---|
| 325 | } |
|---|
| 326 | uniqueTableForId->sizeIndex = newSizeIndex; |
|---|
| 327 | uniqueTableForId->numBins = TABLE_SIZE(uniqueTableForId->sizeIndex); |
|---|
| 328 | uniqueTableForId->maxCapacity = |
|---|
| 329 | uniqueTableForId->numBins * HASH_TABLE_DEFAULT_MAX_DENSITY; |
|---|
| 330 | uniqueTableForId->bins = Cal_MemAlloc(CalBddNode_t *, |
|---|
| 331 | uniqueTableForId->numBins); |
|---|
| 332 | if(uniqueTableForId->bins == Cal_Nil(CalBddNode_t *)){ |
|---|
| 333 | CalBddFatalMessage("out of memory"); |
|---|
| 334 | } |
|---|
| 335 | } |
|---|
| 336 | /* Clear the unique table bins */ |
|---|
| 337 | memset((char *)uniqueTableForId->bins, 0, |
|---|
| 338 | uniqueTableForId->numBins*sizeof(CalBddNode_t *)); |
|---|
| 339 | numPagesRequired = |
|---|
| 340 | uniqueTableForId->numEntries/NUM_NODES_PER_PAGE+1; |
|---|
| 341 | /* Traverse the first numPagesRequired pages of this nodeManager */ |
|---|
| 342 | /* Create the new free list */ |
|---|
| 343 | nodeManager->freeNodeList = freeNodeList = Cal_Nil(CalBddNode_t); |
|---|
| 344 | for (pageNum = 0; pageNum < nodeManager->numPages; pageNum++){ |
|---|
| 345 | for(nodeNum = 0, |
|---|
| 346 | bddNode = (CalBddNode_t *)nodeManager->pageList[pageNum]; |
|---|
| 347 | nodeNum < NUM_NODES_PER_PAGE; nodeNum++, bddNode += 1){ |
|---|
| 348 | if(CalBddNodeIsRefCountZero(bddNode) || |
|---|
| 349 | CalBddNodeIsForwarded(bddNode)){ |
|---|
| 350 | if (pageNum < numPagesRequired){ |
|---|
| 351 | bddNode->nextBddNode = freeNodeList; |
|---|
| 352 | freeNodeList = bddNode; |
|---|
| 353 | } |
|---|
| 354 | continue; |
|---|
| 355 | } |
|---|
| 356 | CalBddNodeGetThenBdd(bddNode, thenBdd); |
|---|
| 357 | CalBddNodeGetElseBdd(bddNode, elseBdd); |
|---|
| 358 | if (CalBddIsForwarded(thenBdd)){ |
|---|
| 359 | CalBddForward(thenBdd); |
|---|
| 360 | CalBddNodePutThenBdd(bddNode, thenBdd); |
|---|
| 361 | } |
|---|
| 362 | if (CalBddIsForwarded(elseBdd)){ |
|---|
| 363 | CalBddForward(elseBdd); |
|---|
| 364 | CalBddNodePutElseBdd(bddNode, elseBdd); |
|---|
| 365 | } |
|---|
| 366 | if (pageNum < numPagesRequired){ |
|---|
| 367 | /* Simply insert the node in the unique table */ |
|---|
| 368 | hashValue = CalDoHash2(thenBdd.bddNode, elseBdd.bddNode, |
|---|
| 369 | uniqueTableForId); |
|---|
| 370 | CalBddNodePutNextBddNode(bddNode, uniqueTableForId->bins[hashValue]); |
|---|
| 371 | uniqueTableForId->bins[hashValue] = bddNode; |
|---|
| 372 | } |
|---|
| 373 | else { |
|---|
| 374 | /* Create a new node */ |
|---|
| 375 | newNode = freeNodeList; |
|---|
| 376 | freeNodeList = newNode->nextBddNode; |
|---|
| 377 | newNode->thenBddNode = bddNode->thenBddNode; |
|---|
| 378 | newNode->elseBddNode = bddNode->elseBddNode; |
|---|
| 379 | newNode->thenBddId = bddNode->thenBddId; |
|---|
| 380 | newNode->elseBddId = bddNode->elseBddId; |
|---|
| 381 | newNode->nextBddNode = bddNode->nextBddNode; |
|---|
| 382 | bddNode->elseBddNode = FORWARD_FLAG; |
|---|
| 383 | bddNode->thenBddId = id; |
|---|
| 384 | bddNode->thenBddNode = newNode; |
|---|
| 385 | hashValue = CalDoHash2(thenBdd.bddNode, elseBdd.bddNode, |
|---|
| 386 | uniqueTableForId); |
|---|
| 387 | CalBddNodePutNextBddNode(newNode, uniqueTableForId->bins[hashValue]); |
|---|
| 388 | uniqueTableForId->bins[hashValue] = newNode; |
|---|
| 389 | } |
|---|
| 390 | } |
|---|
| 391 | if (pageNum >= numPagesRequired){ |
|---|
| 392 | /* Free this page. I am assuming that there would not be any |
|---|
| 393 | call to PageManagerAllocPage, until this function finishes */ |
|---|
| 394 | /* Also, CalPageManagerFreePage overwrites only the first field of |
|---|
| 395 | the bdd node (the nextBddNode field), hence no relevant |
|---|
| 396 | information is lost */ |
|---|
| 397 | CalPageManagerFreePage(nodeManager->pageManager, |
|---|
| 398 | nodeManager->pageList[pageNum]); |
|---|
| 399 | nodeManager->pageList[pageNum] = 0; |
|---|
| 400 | } |
|---|
| 401 | } |
|---|
| 402 | #ifdef _CAL_VERBOSE |
|---|
| 403 | printf("Recycled %4d pages for %3d id\n", |
|---|
| 404 | nodeManager->numPages-numPagesRequired, id); |
|---|
| 405 | #endif |
|---|
| 406 | nodeManager->numPages = numPagesRequired; |
|---|
| 407 | nodeManager->freeNodeList = freeNodeList; |
|---|
| 408 | } |
|---|
| 409 | /* Need to update the handles to the nodes being moved */ |
|---|
| 410 | if (bddManager->pipelineState == CREATE){ |
|---|
| 411 | /* There are some results computed in pipeline */ |
|---|
| 412 | CalBddReorderFixProvisionalNodes(bddManager); |
|---|
| 413 | } |
|---|
| 414 | |
|---|
| 415 | CalCacheTableTwoRepackUpdate(bddManager->cacheTable); |
|---|
| 416 | |
|---|
| 417 | /* Fix the user BDDs */ |
|---|
| 418 | CalBddReorderFixUserBddPtrs(bddManager); |
|---|
| 419 | |
|---|
| 420 | /* Fix the association */ |
|---|
| 421 | CalReorderAssociationFix(bddManager); |
|---|
| 422 | |
|---|
| 423 | Cal_Assert(CalCheckAssoc(bddManager)); |
|---|
| 424 | } |
|---|
| 425 | |
|---|
| 426 | /*---------------------------------------------------------------------------*/ |
|---|
| 427 | /* Definition of static functions */ |
|---|
| 428 | /*---------------------------------------------------------------------------*/ |
|---|
| 429 | |
|---|
| 430 | /**Function******************************************************************** |
|---|
| 431 | |
|---|
| 432 | Synopsis [Returns the smallest integer greater than or equal to log2 of a |
|---|
| 433 | number] |
|---|
| 434 | |
|---|
| 435 | Description [Returns the smallest integer greater than or equal to log2 of a |
|---|
| 436 | number (The assumption is that the number is >= 1)] |
|---|
| 437 | |
|---|
| 438 | SideEffects [None] |
|---|
| 439 | |
|---|
| 440 | ******************************************************************************/ |
|---|
| 441 | static int |
|---|
| 442 | CeilLog2(int number) |
|---|
| 443 | { |
|---|
| 444 | int num, count; |
|---|
| 445 | for (num=number, count=0; num > 1; num >>= 1, count++); |
|---|
| 446 | if ((1 << count) != number) count++; |
|---|
| 447 | return count; |
|---|
| 448 | } |
|---|