[13] | 1 | /**CFile*********************************************************************** |
---|
| 2 | |
---|
| 3 | FileName [cuddReorder.c] |
---|
| 4 | |
---|
| 5 | PackageName [cudd] |
---|
| 6 | |
---|
| 7 | Synopsis [Functions for dynamic variable reordering.] |
---|
| 8 | |
---|
| 9 | Description [External procedures included in this file: |
---|
| 10 | <ul> |
---|
| 11 | <li> Cudd_ReduceHeap() |
---|
| 12 | <li> Cudd_ShuffleHeap() |
---|
| 13 | </ul> |
---|
| 14 | Internal procedures included in this module: |
---|
| 15 | <ul> |
---|
| 16 | <li> cuddDynamicAllocNode() |
---|
| 17 | <li> cuddSifting() |
---|
| 18 | <li> cuddSwapping() |
---|
| 19 | <li> cuddNextHigh() |
---|
| 20 | <li> cuddNextLow() |
---|
| 21 | <li> cuddSwapInPlace() |
---|
| 22 | <li> cuddBddAlignToZdd() |
---|
| 23 | </ul> |
---|
| 24 | Static procedures included in this module: |
---|
| 25 | <ul> |
---|
| 26 | <li> ddUniqueCompare() |
---|
| 27 | <li> ddSwapAny() |
---|
| 28 | <li> ddSiftingAux() |
---|
| 29 | <li> ddSiftingUp() |
---|
| 30 | <li> ddSiftingDown() |
---|
| 31 | <li> ddSiftingBackward() |
---|
| 32 | <li> ddReorderPreprocess() |
---|
| 33 | <li> ddReorderPostprocess() |
---|
| 34 | <li> ddShuffle() |
---|
| 35 | <li> ddSiftUp() |
---|
| 36 | <li> bddFixTree() |
---|
| 37 | </ul>] |
---|
| 38 | |
---|
| 39 | Author [Shipra Panda, Bernard Plessier, Fabio Somenzi] |
---|
| 40 | |
---|
| 41 | Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado |
---|
| 42 | |
---|
| 43 | All rights reserved. |
---|
| 44 | |
---|
| 45 | Redistribution and use in source and binary forms, with or without |
---|
| 46 | modification, are permitted provided that the following conditions |
---|
| 47 | are met: |
---|
| 48 | |
---|
| 49 | Redistributions of source code must retain the above copyright |
---|
| 50 | notice, this list of conditions and the following disclaimer. |
---|
| 51 | |
---|
| 52 | Redistributions in binary form must reproduce the above copyright |
---|
| 53 | notice, this list of conditions and the following disclaimer in the |
---|
| 54 | documentation and/or other materials provided with the distribution. |
---|
| 55 | |
---|
| 56 | Neither the name of the University of Colorado nor the names of its |
---|
| 57 | contributors may be used to endorse or promote products derived from |
---|
| 58 | this software without specific prior written permission. |
---|
| 59 | |
---|
| 60 | THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS |
---|
| 61 | "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT |
---|
| 62 | LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS |
---|
| 63 | FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE |
---|
| 64 | COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, |
---|
| 65 | INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, |
---|
| 66 | BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; |
---|
| 67 | LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER |
---|
| 68 | CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT |
---|
| 69 | LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN |
---|
| 70 | ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE |
---|
| 71 | POSSIBILITY OF SUCH DAMAGE.] |
---|
| 72 | |
---|
| 73 | ******************************************************************************/ |
---|
| 74 | |
---|
| 75 | #include "util.h" |
---|
| 76 | #include "cuddInt.h" |
---|
| 77 | |
---|
| 78 | /*---------------------------------------------------------------------------*/ |
---|
| 79 | /* Constant declarations */ |
---|
| 80 | /*---------------------------------------------------------------------------*/ |
---|
| 81 | |
---|
| 82 | #define DD_MAX_SUBTABLE_SPARSITY 8 |
---|
| 83 | #define DD_SHRINK_FACTOR 2 |
---|
| 84 | |
---|
| 85 | /*---------------------------------------------------------------------------*/ |
---|
| 86 | /* Stucture declarations */ |
---|
| 87 | /*---------------------------------------------------------------------------*/ |
---|
| 88 | |
---|
| 89 | /*---------------------------------------------------------------------------*/ |
---|
| 90 | /* Type declarations */ |
---|
| 91 | /*---------------------------------------------------------------------------*/ |
---|
| 92 | |
---|
| 93 | /*---------------------------------------------------------------------------*/ |
---|
| 94 | /* Variable declarations */ |
---|
| 95 | /*---------------------------------------------------------------------------*/ |
---|
| 96 | |
---|
| 97 | #ifndef lint |
---|
| 98 | static char rcsid[] DD_UNUSED = "$Id: cuddReorder.c,v 1.69 2009/02/21 18:24:10 fabio Exp $"; |
---|
| 99 | #endif |
---|
| 100 | |
---|
| 101 | static int *entry; |
---|
| 102 | |
---|
| 103 | int ddTotalNumberSwapping; |
---|
| 104 | #ifdef DD_STATS |
---|
| 105 | int ddTotalNISwaps; |
---|
| 106 | #endif |
---|
| 107 | |
---|
| 108 | /*---------------------------------------------------------------------------*/ |
---|
| 109 | /* Macro declarations */ |
---|
| 110 | /*---------------------------------------------------------------------------*/ |
---|
| 111 | |
---|
| 112 | /**AutomaticStart*************************************************************/ |
---|
| 113 | |
---|
| 114 | /*---------------------------------------------------------------------------*/ |
---|
| 115 | /* Static function prototypes */ |
---|
| 116 | /*---------------------------------------------------------------------------*/ |
---|
| 117 | |
---|
| 118 | static int ddUniqueCompare (int *ptrX, int *ptrY); |
---|
| 119 | static Move * ddSwapAny (DdManager *table, int x, int y); |
---|
| 120 | static int ddSiftingAux (DdManager *table, int x, int xLow, int xHigh); |
---|
| 121 | static Move * ddSiftingUp (DdManager *table, int y, int xLow); |
---|
| 122 | static Move * ddSiftingDown (DdManager *table, int x, int xHigh); |
---|
| 123 | static int ddSiftingBackward (DdManager *table, int size, Move *moves); |
---|
| 124 | static int ddReorderPreprocess (DdManager *table); |
---|
| 125 | static int ddReorderPostprocess (DdManager *table); |
---|
| 126 | static int ddShuffle (DdManager *table, int *permutation); |
---|
| 127 | static int ddSiftUp (DdManager *table, int x, int xLow); |
---|
| 128 | static void bddFixTree (DdManager *table, MtrNode *treenode); |
---|
| 129 | static int ddUpdateMtrTree (DdManager *table, MtrNode *treenode, int *perm, int *invperm); |
---|
| 130 | static int ddCheckPermuation (DdManager *table, MtrNode *treenode, int *perm, int *invperm); |
---|
| 131 | |
---|
| 132 | /**AutomaticEnd***************************************************************/ |
---|
| 133 | |
---|
| 134 | |
---|
| 135 | /*---------------------------------------------------------------------------*/ |
---|
| 136 | /* Definition of exported functions */ |
---|
| 137 | /*---------------------------------------------------------------------------*/ |
---|
| 138 | |
---|
| 139 | |
---|
| 140 | /**Function******************************************************************** |
---|
| 141 | |
---|
| 142 | Synopsis [Main dynamic reordering routine.] |
---|
| 143 | |
---|
| 144 | Description [Main dynamic reordering routine. |
---|
| 145 | Calls one of the possible reordering procedures: |
---|
| 146 | <ul> |
---|
| 147 | <li>Swapping |
---|
| 148 | <li>Sifting |
---|
| 149 | <li>Symmetric Sifting |
---|
| 150 | <li>Group Sifting |
---|
| 151 | <li>Window Permutation |
---|
| 152 | <li>Simulated Annealing |
---|
| 153 | <li>Genetic Algorithm |
---|
| 154 | <li>Dynamic Programming (exact) |
---|
| 155 | </ul> |
---|
| 156 | |
---|
| 157 | For sifting, symmetric sifting, group sifting, and window |
---|
| 158 | permutation it is possible to request reordering to convergence.<p> |
---|
| 159 | |
---|
| 160 | The core of all methods is the reordering procedure |
---|
| 161 | cuddSwapInPlace() which swaps two adjacent variables and is based |
---|
| 162 | on Rudell's paper. |
---|
| 163 | Returns 1 in case of success; 0 otherwise. In the case of symmetric |
---|
| 164 | sifting (with and without convergence) returns 1 plus the number of |
---|
| 165 | symmetric variables, in case of success.] |
---|
| 166 | |
---|
| 167 | SideEffects [Changes the variable order for all diagrams and clears |
---|
| 168 | the cache.] |
---|
| 169 | |
---|
| 170 | ******************************************************************************/ |
---|
| 171 | int |
---|
| 172 | Cudd_ReduceHeap( |
---|
| 173 | DdManager * table /* DD manager */, |
---|
| 174 | Cudd_ReorderingType heuristic /* method used for reordering */, |
---|
| 175 | int minsize /* bound below which no reordering occurs */) |
---|
| 176 | { |
---|
| 177 | DdHook *hook; |
---|
| 178 | int result; |
---|
| 179 | unsigned int nextDyn; |
---|
| 180 | #ifdef DD_STATS |
---|
| 181 | unsigned int initialSize; |
---|
| 182 | unsigned int finalSize; |
---|
| 183 | #endif |
---|
| 184 | long localTime; |
---|
| 185 | |
---|
| 186 | /* Don't reorder if there are too many dead nodes. */ |
---|
| 187 | if (table->keys - table->dead < (unsigned) minsize) |
---|
| 188 | return(1); |
---|
| 189 | |
---|
| 190 | if (heuristic == CUDD_REORDER_SAME) { |
---|
| 191 | heuristic = table->autoMethod; |
---|
| 192 | } |
---|
| 193 | if (heuristic == CUDD_REORDER_NONE) { |
---|
| 194 | return(1); |
---|
| 195 | } |
---|
| 196 | |
---|
| 197 | /* This call to Cudd_ReduceHeap does initiate reordering. Therefore |
---|
| 198 | ** we count it. |
---|
| 199 | */ |
---|
| 200 | table->reorderings++; |
---|
| 201 | |
---|
| 202 | localTime = util_cpu_time(); |
---|
| 203 | |
---|
| 204 | /* Run the hook functions. */ |
---|
| 205 | hook = table->preReorderingHook; |
---|
| 206 | while (hook != NULL) { |
---|
| 207 | int res = (hook->f)(table, "BDD", (void *)heuristic); |
---|
| 208 | if (res == 0) return(0); |
---|
| 209 | hook = hook->next; |
---|
| 210 | } |
---|
| 211 | |
---|
| 212 | if (!ddReorderPreprocess(table)) return(0); |
---|
| 213 | ddTotalNumberSwapping = 0; |
---|
| 214 | |
---|
| 215 | if (table->keys > table->peakLiveNodes) { |
---|
| 216 | table->peakLiveNodes = table->keys; |
---|
| 217 | } |
---|
| 218 | #ifdef DD_STATS |
---|
| 219 | initialSize = table->keys - table->isolated; |
---|
| 220 | ddTotalNISwaps = 0; |
---|
| 221 | |
---|
| 222 | switch(heuristic) { |
---|
| 223 | case CUDD_REORDER_RANDOM: |
---|
| 224 | case CUDD_REORDER_RANDOM_PIVOT: |
---|
| 225 | (void) fprintf(table->out,"#:I_RANDOM "); |
---|
| 226 | break; |
---|
| 227 | case CUDD_REORDER_SIFT: |
---|
| 228 | case CUDD_REORDER_SIFT_CONVERGE: |
---|
| 229 | case CUDD_REORDER_SYMM_SIFT: |
---|
| 230 | case CUDD_REORDER_SYMM_SIFT_CONV: |
---|
| 231 | case CUDD_REORDER_GROUP_SIFT: |
---|
| 232 | case CUDD_REORDER_GROUP_SIFT_CONV: |
---|
| 233 | (void) fprintf(table->out,"#:I_SIFTING "); |
---|
| 234 | break; |
---|
| 235 | case CUDD_REORDER_WINDOW2: |
---|
| 236 | case CUDD_REORDER_WINDOW3: |
---|
| 237 | case CUDD_REORDER_WINDOW4: |
---|
| 238 | case CUDD_REORDER_WINDOW2_CONV: |
---|
| 239 | case CUDD_REORDER_WINDOW3_CONV: |
---|
| 240 | case CUDD_REORDER_WINDOW4_CONV: |
---|
| 241 | (void) fprintf(table->out,"#:I_WINDOW "); |
---|
| 242 | break; |
---|
| 243 | case CUDD_REORDER_ANNEALING: |
---|
| 244 | (void) fprintf(table->out,"#:I_ANNEAL "); |
---|
| 245 | break; |
---|
| 246 | case CUDD_REORDER_GENETIC: |
---|
| 247 | (void) fprintf(table->out,"#:I_GENETIC "); |
---|
| 248 | break; |
---|
| 249 | case CUDD_REORDER_LINEAR: |
---|
| 250 | case CUDD_REORDER_LINEAR_CONVERGE: |
---|
| 251 | (void) fprintf(table->out,"#:I_LINSIFT "); |
---|
| 252 | break; |
---|
| 253 | case CUDD_REORDER_EXACT: |
---|
| 254 | (void) fprintf(table->out,"#:I_EXACT "); |
---|
| 255 | break; |
---|
| 256 | default: |
---|
| 257 | return(0); |
---|
| 258 | } |
---|
| 259 | (void) fprintf(table->out,"%8d: initial size",initialSize); |
---|
| 260 | #endif |
---|
| 261 | |
---|
| 262 | /* See if we should use alternate threshold for maximum growth. */ |
---|
| 263 | if (table->reordCycle && table->reorderings % table->reordCycle == 0) { |
---|
| 264 | double saveGrowth = table->maxGrowth; |
---|
| 265 | table->maxGrowth = table->maxGrowthAlt; |
---|
| 266 | result = cuddTreeSifting(table,heuristic); |
---|
| 267 | table->maxGrowth = saveGrowth; |
---|
| 268 | } else { |
---|
| 269 | result = cuddTreeSifting(table,heuristic); |
---|
| 270 | } |
---|
| 271 | |
---|
| 272 | #ifdef DD_STATS |
---|
| 273 | (void) fprintf(table->out,"\n"); |
---|
| 274 | finalSize = table->keys - table->isolated; |
---|
| 275 | (void) fprintf(table->out,"#:F_REORDER %8d: final size\n",finalSize); |
---|
| 276 | (void) fprintf(table->out,"#:T_REORDER %8g: total time (sec)\n", |
---|
| 277 | ((double)(util_cpu_time() - localTime)/1000.0)); |
---|
| 278 | (void) fprintf(table->out,"#:N_REORDER %8d: total swaps\n", |
---|
| 279 | ddTotalNumberSwapping); |
---|
| 280 | (void) fprintf(table->out,"#:M_REORDER %8d: NI swaps\n",ddTotalNISwaps); |
---|
| 281 | #endif |
---|
| 282 | |
---|
| 283 | if (result == 0) |
---|
| 284 | return(0); |
---|
| 285 | |
---|
| 286 | if (!ddReorderPostprocess(table)) |
---|
| 287 | return(0); |
---|
| 288 | |
---|
| 289 | if (table->realign) { |
---|
| 290 | if (!cuddZddAlignToBdd(table)) |
---|
| 291 | return(0); |
---|
| 292 | } |
---|
| 293 | |
---|
| 294 | nextDyn = (table->keys - table->constants.keys + 1) * |
---|
| 295 | DD_DYN_RATIO + table->constants.keys; |
---|
| 296 | if (table->reorderings < 20 || nextDyn > table->nextDyn) |
---|
| 297 | table->nextDyn = nextDyn; |
---|
| 298 | else |
---|
| 299 | table->nextDyn += 20; |
---|
| 300 | table->reordered = 1; |
---|
| 301 | |
---|
| 302 | /* Run hook functions. */ |
---|
| 303 | hook = table->postReorderingHook; |
---|
| 304 | while (hook != NULL) { |
---|
| 305 | int res = (hook->f)(table, "BDD", (void *)localTime); |
---|
| 306 | if (res == 0) return(0); |
---|
| 307 | hook = hook->next; |
---|
| 308 | } |
---|
| 309 | /* Update cumulative reordering time. */ |
---|
| 310 | table->reordTime += util_cpu_time() - localTime; |
---|
| 311 | |
---|
| 312 | return(result); |
---|
| 313 | |
---|
| 314 | } /* end of Cudd_ReduceHeap */ |
---|
| 315 | |
---|
| 316 | |
---|
| 317 | /**Function******************************************************************** |
---|
| 318 | |
---|
| 319 | Synopsis [Reorders variables according to given permutation.] |
---|
| 320 | |
---|
| 321 | Description [Reorders variables according to given permutation. |
---|
| 322 | The i-th entry of the permutation array contains the index of the variable |
---|
| 323 | that should be brought to the i-th level. The size of the array should be |
---|
| 324 | equal or greater to the number of variables currently in use. |
---|
| 325 | Returns 1 in case of success; 0 otherwise.] |
---|
| 326 | |
---|
| 327 | SideEffects [Changes the variable order for all diagrams and clears |
---|
| 328 | the cache.] |
---|
| 329 | |
---|
| 330 | SeeAlso [Cudd_ReduceHeap] |
---|
| 331 | |
---|
| 332 | ******************************************************************************/ |
---|
| 333 | int |
---|
| 334 | Cudd_ShuffleHeap( |
---|
| 335 | DdManager * table /* DD manager */, |
---|
| 336 | int * permutation /* required variable permutation */) |
---|
| 337 | { |
---|
| 338 | |
---|
| 339 | int result; |
---|
| 340 | int i; |
---|
| 341 | int identity = 1; |
---|
| 342 | int *perm; |
---|
| 343 | |
---|
| 344 | /* Don't waste time in case of identity permutation. */ |
---|
| 345 | for (i = 0; i < table->size; i++) { |
---|
| 346 | if (permutation[i] != table->invperm[i]) { |
---|
| 347 | identity = 0; |
---|
| 348 | break; |
---|
| 349 | } |
---|
| 350 | } |
---|
| 351 | if (identity == 1) { |
---|
| 352 | return(1); |
---|
| 353 | } |
---|
| 354 | if (!ddReorderPreprocess(table)) return(0); |
---|
| 355 | if (table->keys > table->peakLiveNodes) { |
---|
| 356 | table->peakLiveNodes = table->keys; |
---|
| 357 | } |
---|
| 358 | |
---|
| 359 | perm = ALLOC(int, table->size); |
---|
| 360 | for (i = 0; i < table->size; i++) |
---|
| 361 | perm[permutation[i]] = i; |
---|
| 362 | if (!ddCheckPermuation(table,table->tree,perm,permutation)) { |
---|
| 363 | FREE(perm); |
---|
| 364 | return(0); |
---|
| 365 | } |
---|
| 366 | if (!ddUpdateMtrTree(table,table->tree,perm,permutation)) { |
---|
| 367 | FREE(perm); |
---|
| 368 | return(0); |
---|
| 369 | } |
---|
| 370 | FREE(perm); |
---|
| 371 | |
---|
| 372 | result = ddShuffle(table,permutation); |
---|
| 373 | |
---|
| 374 | if (!ddReorderPostprocess(table)) return(0); |
---|
| 375 | |
---|
| 376 | return(result); |
---|
| 377 | |
---|
| 378 | } /* end of Cudd_ShuffleHeap */ |
---|
| 379 | |
---|
| 380 | |
---|
| 381 | /*---------------------------------------------------------------------------*/ |
---|
| 382 | /* Definition of internal functions */ |
---|
| 383 | /*---------------------------------------------------------------------------*/ |
---|
| 384 | |
---|
| 385 | |
---|
| 386 | /**Function******************************************************************** |
---|
| 387 | |
---|
| 388 | Synopsis [Dynamically allocates a Node.] |
---|
| 389 | |
---|
| 390 | Description [Dynamically allocates a Node. This procedure is similar |
---|
| 391 | to cuddAllocNode in Cudd_Table.c, but it does not attempt garbage |
---|
| 392 | collection, because during reordering there are no dead nodes. |
---|
| 393 | Returns a pointer to a new node if successful; NULL is memory is |
---|
| 394 | full.] |
---|
| 395 | |
---|
| 396 | SideEffects [None] |
---|
| 397 | |
---|
| 398 | SeeAlso [cuddAllocNode] |
---|
| 399 | |
---|
| 400 | ******************************************************************************/ |
---|
| 401 | DdNode * |
---|
| 402 | cuddDynamicAllocNode( |
---|
| 403 | DdManager * table) |
---|
| 404 | { |
---|
| 405 | int i; |
---|
| 406 | DdNodePtr *mem; |
---|
| 407 | DdNode *list, *node; |
---|
| 408 | extern DD_OOMFP MMoutOfMemory; |
---|
| 409 | DD_OOMFP saveHandler; |
---|
| 410 | |
---|
| 411 | if (table->nextFree == NULL) { /* free list is empty */ |
---|
| 412 | /* Try to allocate a new block. */ |
---|
| 413 | saveHandler = MMoutOfMemory; |
---|
| 414 | MMoutOfMemory = Cudd_OutOfMem; |
---|
| 415 | mem = (DdNodePtr *) ALLOC(DdNode, DD_MEM_CHUNK + 1); |
---|
| 416 | MMoutOfMemory = saveHandler; |
---|
| 417 | if (mem == NULL && table->stash != NULL) { |
---|
| 418 | FREE(table->stash); |
---|
| 419 | table->stash = NULL; |
---|
| 420 | /* Inhibit resizing of tables. */ |
---|
| 421 | table->maxCacheHard = table->cacheSlots - 1; |
---|
| 422 | table->cacheSlack = - (int) (table->cacheSlots + 1); |
---|
| 423 | for (i = 0; i < table->size; i++) { |
---|
| 424 | table->subtables[i].maxKeys <<= 2; |
---|
| 425 | } |
---|
| 426 | mem = (DdNodePtr *) ALLOC(DdNode,DD_MEM_CHUNK + 1); |
---|
| 427 | } |
---|
| 428 | if (mem == NULL) { |
---|
| 429 | /* Out of luck. Call the default handler to do |
---|
| 430 | ** whatever it specifies for a failed malloc. If this |
---|
| 431 | ** handler returns, then set error code, print |
---|
| 432 | ** warning, and return. */ |
---|
| 433 | (*MMoutOfMemory)(sizeof(DdNode)*(DD_MEM_CHUNK + 1)); |
---|
| 434 | table->errorCode = CUDD_MEMORY_OUT; |
---|
| 435 | #ifdef DD_VERBOSE |
---|
| 436 | (void) fprintf(table->err, |
---|
| 437 | "cuddDynamicAllocNode: out of memory"); |
---|
| 438 | (void) fprintf(table->err,"Memory in use = %lu\n", |
---|
| 439 | table->memused); |
---|
| 440 | #endif |
---|
| 441 | return(NULL); |
---|
| 442 | } else { /* successful allocation; slice memory */ |
---|
| 443 | unsigned long offset; |
---|
| 444 | table->memused += (DD_MEM_CHUNK + 1) * sizeof(DdNode); |
---|
| 445 | mem[0] = (DdNode *) table->memoryList; |
---|
| 446 | table->memoryList = mem; |
---|
| 447 | |
---|
| 448 | /* Here we rely on the fact that the size of a DdNode is a |
---|
| 449 | ** power of 2 and a multiple of the size of a pointer. |
---|
| 450 | ** If we align one node, all the others will be aligned |
---|
| 451 | ** as well. */ |
---|
| 452 | offset = (unsigned long) mem & (sizeof(DdNode) - 1); |
---|
| 453 | mem += (sizeof(DdNode) - offset) / sizeof(DdNodePtr); |
---|
| 454 | #ifdef DD_DEBUG |
---|
| 455 | assert(((unsigned long) mem & (sizeof(DdNode) - 1)) == 0); |
---|
| 456 | #endif |
---|
| 457 | list = (DdNode *) mem; |
---|
| 458 | |
---|
| 459 | i = 1; |
---|
| 460 | do { |
---|
| 461 | list[i - 1].ref = 0; |
---|
| 462 | list[i - 1].next = &list[i]; |
---|
| 463 | } while (++i < DD_MEM_CHUNK); |
---|
| 464 | |
---|
| 465 | list[DD_MEM_CHUNK-1].ref = 0; |
---|
| 466 | list[DD_MEM_CHUNK - 1].next = NULL; |
---|
| 467 | |
---|
| 468 | table->nextFree = &list[0]; |
---|
| 469 | } |
---|
| 470 | } /* if free list empty */ |
---|
| 471 | |
---|
| 472 | node = table->nextFree; |
---|
| 473 | table->nextFree = node->next; |
---|
| 474 | return (node); |
---|
| 475 | |
---|
| 476 | } /* end of cuddDynamicAllocNode */ |
---|
| 477 | |
---|
| 478 | |
---|
| 479 | /**Function******************************************************************** |
---|
| 480 | |
---|
| 481 | Synopsis [Implementation of Rudell's sifting algorithm.] |
---|
| 482 | |
---|
| 483 | Description [Implementation of Rudell's sifting algorithm. |
---|
| 484 | Assumes that no dead nodes are present. |
---|
| 485 | <ol> |
---|
| 486 | <li> Order all the variables according to the number of entries |
---|
| 487 | in each unique table. |
---|
| 488 | <li> Sift the variable up and down, remembering each time the |
---|
| 489 | total size of the DD heap. |
---|
| 490 | <li> Select the best permutation. |
---|
| 491 | <li> Repeat 3 and 4 for all variables. |
---|
| 492 | </ol> |
---|
| 493 | Returns 1 if successful; 0 otherwise.] |
---|
| 494 | |
---|
| 495 | SideEffects [None] |
---|
| 496 | |
---|
| 497 | ******************************************************************************/ |
---|
| 498 | int |
---|
| 499 | cuddSifting( |
---|
| 500 | DdManager * table, |
---|
| 501 | int lower, |
---|
| 502 | int upper) |
---|
| 503 | { |
---|
| 504 | int i; |
---|
| 505 | int *var; |
---|
| 506 | int size; |
---|
| 507 | int x; |
---|
| 508 | int result; |
---|
| 509 | #ifdef DD_STATS |
---|
| 510 | int previousSize; |
---|
| 511 | #endif |
---|
| 512 | |
---|
| 513 | size = table->size; |
---|
| 514 | |
---|
| 515 | /* Find order in which to sift variables. */ |
---|
| 516 | var = NULL; |
---|
| 517 | entry = ALLOC(int,size); |
---|
| 518 | if (entry == NULL) { |
---|
| 519 | table->errorCode = CUDD_MEMORY_OUT; |
---|
| 520 | goto cuddSiftingOutOfMem; |
---|
| 521 | } |
---|
| 522 | var = ALLOC(int,size); |
---|
| 523 | if (var == NULL) { |
---|
| 524 | table->errorCode = CUDD_MEMORY_OUT; |
---|
| 525 | goto cuddSiftingOutOfMem; |
---|
| 526 | } |
---|
| 527 | |
---|
| 528 | for (i = 0; i < size; i++) { |
---|
| 529 | x = table->perm[i]; |
---|
| 530 | entry[i] = table->subtables[x].keys; |
---|
| 531 | var[i] = i; |
---|
| 532 | } |
---|
| 533 | |
---|
| 534 | qsort((void *)var,size,sizeof(int),(DD_QSFP)ddUniqueCompare); |
---|
| 535 | |
---|
| 536 | /* Now sift. */ |
---|
| 537 | for (i = 0; i < ddMin(table->siftMaxVar,size); i++) { |
---|
| 538 | if (ddTotalNumberSwapping >= table->siftMaxSwap) |
---|
| 539 | break; |
---|
| 540 | x = table->perm[var[i]]; |
---|
| 541 | |
---|
| 542 | if (x < lower || x > upper || table->subtables[x].bindVar == 1) |
---|
| 543 | continue; |
---|
| 544 | #ifdef DD_STATS |
---|
| 545 | previousSize = table->keys - table->isolated; |
---|
| 546 | #endif |
---|
| 547 | result = ddSiftingAux(table, x, lower, upper); |
---|
| 548 | if (!result) goto cuddSiftingOutOfMem; |
---|
| 549 | #ifdef DD_STATS |
---|
| 550 | if (table->keys < (unsigned) previousSize + table->isolated) { |
---|
| 551 | (void) fprintf(table->out,"-"); |
---|
| 552 | } else if (table->keys > (unsigned) previousSize + table->isolated) { |
---|
| 553 | (void) fprintf(table->out,"+"); /* should never happen */ |
---|
| 554 | (void) fprintf(table->err,"\nSize increased from %d to %d while sifting variable %d\n", previousSize, table->keys - table->isolated, var[i]); |
---|
| 555 | } else { |
---|
| 556 | (void) fprintf(table->out,"="); |
---|
| 557 | } |
---|
| 558 | fflush(table->out); |
---|
| 559 | #endif |
---|
| 560 | } |
---|
| 561 | |
---|
| 562 | FREE(var); |
---|
| 563 | FREE(entry); |
---|
| 564 | |
---|
| 565 | return(1); |
---|
| 566 | |
---|
| 567 | cuddSiftingOutOfMem: |
---|
| 568 | |
---|
| 569 | if (entry != NULL) FREE(entry); |
---|
| 570 | if (var != NULL) FREE(var); |
---|
| 571 | |
---|
| 572 | return(0); |
---|
| 573 | |
---|
| 574 | } /* end of cuddSifting */ |
---|
| 575 | |
---|
| 576 | |
---|
| 577 | /**Function******************************************************************** |
---|
| 578 | |
---|
| 579 | Synopsis [Reorders variables by a sequence of (non-adjacent) swaps.] |
---|
| 580 | |
---|
| 581 | Description [Implementation of Plessier's algorithm that reorders |
---|
| 582 | variables by a sequence of (non-adjacent) swaps. |
---|
| 583 | <ol> |
---|
| 584 | <li> Select two variables (RANDOM or HEURISTIC). |
---|
| 585 | <li> Permute these variables. |
---|
| 586 | <li> If the nodes have decreased accept the permutation. |
---|
| 587 | <li> Otherwise reconstruct the original heap. |
---|
| 588 | <li> Loop. |
---|
| 589 | </ol> |
---|
| 590 | Returns 1 in case of success; 0 otherwise.] |
---|
| 591 | |
---|
| 592 | SideEffects [None] |
---|
| 593 | |
---|
| 594 | ******************************************************************************/ |
---|
| 595 | int |
---|
| 596 | cuddSwapping( |
---|
| 597 | DdManager * table, |
---|
| 598 | int lower, |
---|
| 599 | int upper, |
---|
| 600 | Cudd_ReorderingType heuristic) |
---|
| 601 | { |
---|
| 602 | int i, j; |
---|
| 603 | int max, keys; |
---|
| 604 | int nvars; |
---|
| 605 | int x, y; |
---|
| 606 | int iterate; |
---|
| 607 | int previousSize; |
---|
| 608 | Move *moves, *move; |
---|
| 609 | int pivot; |
---|
| 610 | int modulo; |
---|
| 611 | int result; |
---|
| 612 | |
---|
| 613 | #ifdef DD_DEBUG |
---|
| 614 | /* Sanity check */ |
---|
| 615 | assert(lower >= 0 && upper < table->size && lower <= upper); |
---|
| 616 | #endif |
---|
| 617 | |
---|
| 618 | nvars = upper - lower + 1; |
---|
| 619 | iterate = nvars; |
---|
| 620 | |
---|
| 621 | for (i = 0; i < iterate; i++) { |
---|
| 622 | if (ddTotalNumberSwapping >= table->siftMaxSwap) |
---|
| 623 | break; |
---|
| 624 | if (heuristic == CUDD_REORDER_RANDOM_PIVOT) { |
---|
| 625 | max = -1; |
---|
| 626 | for (j = lower; j <= upper; j++) { |
---|
| 627 | if ((keys = table->subtables[j].keys) > max) { |
---|
| 628 | max = keys; |
---|
| 629 | pivot = j; |
---|
| 630 | } |
---|
| 631 | } |
---|
| 632 | |
---|
| 633 | modulo = upper - pivot; |
---|
| 634 | if (modulo == 0) { |
---|
| 635 | y = pivot; |
---|
| 636 | } else{ |
---|
| 637 | y = pivot + 1 + ((int) Cudd_Random() % modulo); |
---|
| 638 | } |
---|
| 639 | |
---|
| 640 | modulo = pivot - lower - 1; |
---|
| 641 | if (modulo < 1) { |
---|
| 642 | x = lower; |
---|
| 643 | } else{ |
---|
| 644 | do { |
---|
| 645 | x = (int) Cudd_Random() % modulo; |
---|
| 646 | } while (x == y); |
---|
| 647 | } |
---|
| 648 | } else { |
---|
| 649 | x = ((int) Cudd_Random() % nvars) + lower; |
---|
| 650 | do { |
---|
| 651 | y = ((int) Cudd_Random() % nvars) + lower; |
---|
| 652 | } while (x == y); |
---|
| 653 | } |
---|
| 654 | previousSize = table->keys - table->isolated; |
---|
| 655 | moves = ddSwapAny(table,x,y); |
---|
| 656 | if (moves == NULL) goto cuddSwappingOutOfMem; |
---|
| 657 | result = ddSiftingBackward(table,previousSize,moves); |
---|
| 658 | if (!result) goto cuddSwappingOutOfMem; |
---|
| 659 | while (moves != NULL) { |
---|
| 660 | move = moves->next; |
---|
| 661 | cuddDeallocMove(table, moves); |
---|
| 662 | moves = move; |
---|
| 663 | } |
---|
| 664 | #ifdef DD_STATS |
---|
| 665 | if (table->keys < (unsigned) previousSize + table->isolated) { |
---|
| 666 | (void) fprintf(table->out,"-"); |
---|
| 667 | } else if (table->keys > (unsigned) previousSize + table->isolated) { |
---|
| 668 | (void) fprintf(table->out,"+"); /* should never happen */ |
---|
| 669 | } else { |
---|
| 670 | (void) fprintf(table->out,"="); |
---|
| 671 | } |
---|
| 672 | fflush(table->out); |
---|
| 673 | #endif |
---|
| 674 | #if 0 |
---|
| 675 | (void) fprintf(table->out,"#:t_SWAPPING %8d: tmp size\n", |
---|
| 676 | table->keys - table->isolated); |
---|
| 677 | #endif |
---|
| 678 | } |
---|
| 679 | |
---|
| 680 | return(1); |
---|
| 681 | |
---|
| 682 | cuddSwappingOutOfMem: |
---|
| 683 | while (moves != NULL) { |
---|
| 684 | move = moves->next; |
---|
| 685 | cuddDeallocMove(table, moves); |
---|
| 686 | moves = move; |
---|
| 687 | } |
---|
| 688 | |
---|
| 689 | return(0); |
---|
| 690 | |
---|
| 691 | } /* end of cuddSwapping */ |
---|
| 692 | |
---|
| 693 | |
---|
| 694 | /**Function******************************************************************** |
---|
| 695 | |
---|
| 696 | Synopsis [Finds the next subtable with a larger index.] |
---|
| 697 | |
---|
| 698 | Description [Finds the next subtable with a larger index. Returns the |
---|
| 699 | index.] |
---|
| 700 | |
---|
| 701 | SideEffects [None] |
---|
| 702 | |
---|
| 703 | SeeAlso [cuddNextLow] |
---|
| 704 | |
---|
| 705 | ******************************************************************************/ |
---|
| 706 | int |
---|
| 707 | cuddNextHigh( |
---|
| 708 | DdManager * table, |
---|
| 709 | int x) |
---|
| 710 | { |
---|
| 711 | return(x+1); |
---|
| 712 | |
---|
| 713 | } /* end of cuddNextHigh */ |
---|
| 714 | |
---|
| 715 | |
---|
| 716 | /**Function******************************************************************** |
---|
| 717 | |
---|
| 718 | Synopsis [Finds the next subtable with a smaller index.] |
---|
| 719 | |
---|
| 720 | Description [Finds the next subtable with a smaller index. Returns the |
---|
| 721 | index.] |
---|
| 722 | |
---|
| 723 | SideEffects [None] |
---|
| 724 | |
---|
| 725 | SeeAlso [cuddNextHigh] |
---|
| 726 | |
---|
| 727 | ******************************************************************************/ |
---|
| 728 | int |
---|
| 729 | cuddNextLow( |
---|
| 730 | DdManager * table, |
---|
| 731 | int x) |
---|
| 732 | { |
---|
| 733 | return(x-1); |
---|
| 734 | |
---|
| 735 | } /* end of cuddNextLow */ |
---|
| 736 | |
---|
| 737 | |
---|
| 738 | /**Function******************************************************************** |
---|
| 739 | |
---|
| 740 | Synopsis [Swaps two adjacent variables.] |
---|
| 741 | |
---|
| 742 | Description [Swaps two adjacent variables. It assumes that no dead |
---|
| 743 | nodes are present on entry to this procedure. The procedure then |
---|
| 744 | guarantees that no dead nodes will be present when it terminates. |
---|
| 745 | cuddSwapInPlace assumes that x < y. Returns the number of keys in |
---|
| 746 | the table if successful; 0 otherwise.] |
---|
| 747 | |
---|
| 748 | SideEffects [None] |
---|
| 749 | |
---|
| 750 | ******************************************************************************/ |
---|
| 751 | int |
---|
| 752 | cuddSwapInPlace( |
---|
| 753 | DdManager * table, |
---|
| 754 | int x, |
---|
| 755 | int y) |
---|
| 756 | { |
---|
| 757 | DdNodePtr *xlist, *ylist; |
---|
| 758 | int xindex, yindex; |
---|
| 759 | int xslots, yslots; |
---|
| 760 | int xshift, yshift; |
---|
| 761 | int oldxkeys, oldykeys; |
---|
| 762 | int newxkeys, newykeys; |
---|
| 763 | int comple, newcomplement; |
---|
| 764 | int i; |
---|
| 765 | Cudd_VariableType varType; |
---|
| 766 | Cudd_LazyGroupType groupType; |
---|
| 767 | int posn; |
---|
| 768 | int isolated; |
---|
| 769 | DdNode *f,*f0,*f1,*f01,*f00,*f11,*f10,*newf1,*newf0; |
---|
| 770 | DdNode *g,*next; |
---|
| 771 | DdNodePtr *previousP; |
---|
| 772 | DdNode *tmp; |
---|
| 773 | DdNode *sentinel = &(table->sentinel); |
---|
| 774 | extern DD_OOMFP MMoutOfMemory; |
---|
| 775 | DD_OOMFP saveHandler; |
---|
| 776 | |
---|
| 777 | #ifdef DD_DEBUG |
---|
| 778 | int count,idcheck; |
---|
| 779 | #endif |
---|
| 780 | |
---|
| 781 | #ifdef DD_DEBUG |
---|
| 782 | assert(x < y); |
---|
| 783 | assert(cuddNextHigh(table,x) == y); |
---|
| 784 | assert(table->subtables[x].keys != 0); |
---|
| 785 | assert(table->subtables[y].keys != 0); |
---|
| 786 | assert(table->subtables[x].dead == 0); |
---|
| 787 | assert(table->subtables[y].dead == 0); |
---|
| 788 | #endif |
---|
| 789 | |
---|
| 790 | ddTotalNumberSwapping++; |
---|
| 791 | |
---|
| 792 | /* Get parameters of x subtable. */ |
---|
| 793 | xindex = table->invperm[x]; |
---|
| 794 | xlist = table->subtables[x].nodelist; |
---|
| 795 | oldxkeys = table->subtables[x].keys; |
---|
| 796 | xslots = table->subtables[x].slots; |
---|
| 797 | xshift = table->subtables[x].shift; |
---|
| 798 | |
---|
| 799 | /* Get parameters of y subtable. */ |
---|
| 800 | yindex = table->invperm[y]; |
---|
| 801 | ylist = table->subtables[y].nodelist; |
---|
| 802 | oldykeys = table->subtables[y].keys; |
---|
| 803 | yslots = table->subtables[y].slots; |
---|
| 804 | yshift = table->subtables[y].shift; |
---|
| 805 | |
---|
| 806 | if (!cuddTestInteract(table,xindex,yindex)) { |
---|
| 807 | #ifdef DD_STATS |
---|
| 808 | ddTotalNISwaps++; |
---|
| 809 | #endif |
---|
| 810 | newxkeys = oldxkeys; |
---|
| 811 | newykeys = oldykeys; |
---|
| 812 | } else { |
---|
| 813 | newxkeys = 0; |
---|
| 814 | newykeys = oldykeys; |
---|
| 815 | |
---|
| 816 | /* Check whether the two projection functions involved in this |
---|
| 817 | ** swap are isolated. At the end, we'll be able to tell how many |
---|
| 818 | ** isolated projection functions are there by checking only these |
---|
| 819 | ** two functions again. This is done to eliminate the isolated |
---|
| 820 | ** projection functions from the node count. |
---|
| 821 | */ |
---|
| 822 | isolated = - ((table->vars[xindex]->ref == 1) + |
---|
| 823 | (table->vars[yindex]->ref == 1)); |
---|
| 824 | |
---|
| 825 | /* The nodes in the x layer that do not depend on |
---|
| 826 | ** y will stay there; the others are put in a chain. |
---|
| 827 | ** The chain is handled as a LIFO; g points to the beginning. |
---|
| 828 | */ |
---|
| 829 | g = NULL; |
---|
| 830 | if ((oldxkeys >= xslots || (unsigned) xslots == table->initSlots) && |
---|
| 831 | oldxkeys <= DD_MAX_SUBTABLE_DENSITY * xslots) { |
---|
| 832 | for (i = 0; i < xslots; i++) { |
---|
| 833 | previousP = &(xlist[i]); |
---|
| 834 | f = *previousP; |
---|
| 835 | while (f != sentinel) { |
---|
| 836 | next = f->next; |
---|
| 837 | f1 = cuddT(f); f0 = cuddE(f); |
---|
| 838 | if (f1->index != (DdHalfWord) yindex && |
---|
| 839 | Cudd_Regular(f0)->index != (DdHalfWord) yindex) { |
---|
| 840 | /* stays */ |
---|
| 841 | newxkeys++; |
---|
| 842 | *previousP = f; |
---|
| 843 | previousP = &(f->next); |
---|
| 844 | } else { |
---|
| 845 | f->index = yindex; |
---|
| 846 | f->next = g; |
---|
| 847 | g = f; |
---|
| 848 | } |
---|
| 849 | f = next; |
---|
| 850 | } /* while there are elements in the collision chain */ |
---|
| 851 | *previousP = sentinel; |
---|
| 852 | } /* for each slot of the x subtable */ |
---|
| 853 | } else { /* resize xlist */ |
---|
| 854 | DdNode *h = NULL; |
---|
| 855 | DdNodePtr *newxlist; |
---|
| 856 | unsigned int newxslots; |
---|
| 857 | int newxshift; |
---|
| 858 | /* Empty current xlist. Nodes that stay go to list h; |
---|
| 859 | ** nodes that move go to list g. */ |
---|
| 860 | for (i = 0; i < xslots; i++) { |
---|
| 861 | f = xlist[i]; |
---|
| 862 | while (f != sentinel) { |
---|
| 863 | next = f->next; |
---|
| 864 | f1 = cuddT(f); f0 = cuddE(f); |
---|
| 865 | if (f1->index != (DdHalfWord) yindex && |
---|
| 866 | Cudd_Regular(f0)->index != (DdHalfWord) yindex) { |
---|
| 867 | /* stays */ |
---|
| 868 | f->next = h; |
---|
| 869 | h = f; |
---|
| 870 | newxkeys++; |
---|
| 871 | } else { |
---|
| 872 | f->index = yindex; |
---|
| 873 | f->next = g; |
---|
| 874 | g = f; |
---|
| 875 | } |
---|
| 876 | f = next; |
---|
| 877 | } /* while there are elements in the collision chain */ |
---|
| 878 | } /* for each slot of the x subtable */ |
---|
| 879 | /* Decide size of new subtable. */ |
---|
| 880 | newxshift = xshift; |
---|
| 881 | newxslots = xslots; |
---|
| 882 | while ((unsigned) oldxkeys > DD_MAX_SUBTABLE_DENSITY * newxslots) { |
---|
| 883 | newxshift--; |
---|
| 884 | newxslots <<= 1; |
---|
| 885 | } |
---|
| 886 | while ((unsigned) oldxkeys < newxslots && |
---|
| 887 | newxslots > table->initSlots) { |
---|
| 888 | newxshift++; |
---|
| 889 | newxslots >>= 1; |
---|
| 890 | } |
---|
| 891 | /* Try to allocate new table. Be ready to back off. */ |
---|
| 892 | saveHandler = MMoutOfMemory; |
---|
| 893 | MMoutOfMemory = Cudd_OutOfMem; |
---|
| 894 | newxlist = ALLOC(DdNodePtr, newxslots); |
---|
| 895 | MMoutOfMemory = saveHandler; |
---|
| 896 | if (newxlist == NULL) { |
---|
| 897 | (void) fprintf(table->err, "Unable to resize subtable %d for lack of memory\n", i); |
---|
| 898 | newxlist = xlist; |
---|
| 899 | newxslots = xslots; |
---|
| 900 | newxshift = xshift; |
---|
| 901 | } else { |
---|
| 902 | table->slots += ((int) newxslots - xslots); |
---|
| 903 | table->minDead = (unsigned) |
---|
| 904 | (table->gcFrac * (double) table->slots); |
---|
| 905 | table->cacheSlack = (int) |
---|
| 906 | ddMin(table->maxCacheHard, DD_MAX_CACHE_TO_SLOTS_RATIO |
---|
| 907 | * table->slots) - 2 * (int) table->cacheSlots; |
---|
| 908 | table->memused += |
---|
| 909 | ((int) newxslots - xslots) * sizeof(DdNodePtr); |
---|
| 910 | FREE(xlist); |
---|
| 911 | xslots = newxslots; |
---|
| 912 | xshift = newxshift; |
---|
| 913 | xlist = newxlist; |
---|
| 914 | } |
---|
| 915 | /* Initialize new subtable. */ |
---|
| 916 | for (i = 0; i < xslots; i++) { |
---|
| 917 | xlist[i] = sentinel; |
---|
| 918 | } |
---|
| 919 | /* Move nodes that were parked in list h to their new home. */ |
---|
| 920 | f = h; |
---|
| 921 | while (f != NULL) { |
---|
| 922 | next = f->next; |
---|
| 923 | f1 = cuddT(f); |
---|
| 924 | f0 = cuddE(f); |
---|
| 925 | /* Check xlist for pair (f11,f01). */ |
---|
| 926 | posn = ddHash(f1, f0, xshift); |
---|
| 927 | /* For each element tmp in collision list xlist[posn]. */ |
---|
| 928 | previousP = &(xlist[posn]); |
---|
| 929 | tmp = *previousP; |
---|
| 930 | while (f1 < cuddT(tmp)) { |
---|
| 931 | previousP = &(tmp->next); |
---|
| 932 | tmp = *previousP; |
---|
| 933 | } |
---|
| 934 | while (f1 == cuddT(tmp) && f0 < cuddE(tmp)) { |
---|
| 935 | previousP = &(tmp->next); |
---|
| 936 | tmp = *previousP; |
---|
| 937 | } |
---|
| 938 | f->next = *previousP; |
---|
| 939 | *previousP = f; |
---|
| 940 | f = next; |
---|
| 941 | } |
---|
| 942 | } |
---|
| 943 | |
---|
| 944 | #ifdef DD_COUNT |
---|
| 945 | table->swapSteps += oldxkeys - newxkeys; |
---|
| 946 | #endif |
---|
| 947 | /* Take care of the x nodes that must be re-expressed. |
---|
| 948 | ** They form a linked list pointed by g. Their index has been |
---|
| 949 | ** already changed to yindex. |
---|
| 950 | */ |
---|
| 951 | f = g; |
---|
| 952 | while (f != NULL) { |
---|
| 953 | next = f->next; |
---|
| 954 | /* Find f1, f0, f11, f10, f01, f00. */ |
---|
| 955 | f1 = cuddT(f); |
---|
| 956 | #ifdef DD_DEBUG |
---|
| 957 | assert(!(Cudd_IsComplement(f1))); |
---|
| 958 | #endif |
---|
| 959 | if ((int) f1->index == yindex) { |
---|
| 960 | f11 = cuddT(f1); f10 = cuddE(f1); |
---|
| 961 | } else { |
---|
| 962 | f11 = f10 = f1; |
---|
| 963 | } |
---|
| 964 | #ifdef DD_DEBUG |
---|
| 965 | assert(!(Cudd_IsComplement(f11))); |
---|
| 966 | #endif |
---|
| 967 | f0 = cuddE(f); |
---|
| 968 | comple = Cudd_IsComplement(f0); |
---|
| 969 | f0 = Cudd_Regular(f0); |
---|
| 970 | if ((int) f0->index == yindex) { |
---|
| 971 | f01 = cuddT(f0); f00 = cuddE(f0); |
---|
| 972 | } else { |
---|
| 973 | f01 = f00 = f0; |
---|
| 974 | } |
---|
| 975 | if (comple) { |
---|
| 976 | f01 = Cudd_Not(f01); |
---|
| 977 | f00 = Cudd_Not(f00); |
---|
| 978 | } |
---|
| 979 | /* Decrease ref count of f1. */ |
---|
| 980 | cuddSatDec(f1->ref); |
---|
| 981 | /* Create the new T child. */ |
---|
| 982 | if (f11 == f01) { |
---|
| 983 | newf1 = f11; |
---|
| 984 | cuddSatInc(newf1->ref); |
---|
| 985 | } else { |
---|
| 986 | /* Check xlist for triple (xindex,f11,f01). */ |
---|
| 987 | posn = ddHash(f11, f01, xshift); |
---|
| 988 | /* For each element newf1 in collision list xlist[posn]. */ |
---|
| 989 | previousP = &(xlist[posn]); |
---|
| 990 | newf1 = *previousP; |
---|
| 991 | while (f11 < cuddT(newf1)) { |
---|
| 992 | previousP = &(newf1->next); |
---|
| 993 | newf1 = *previousP; |
---|
| 994 | } |
---|
| 995 | while (f11 == cuddT(newf1) && f01 < cuddE(newf1)) { |
---|
| 996 | previousP = &(newf1->next); |
---|
| 997 | newf1 = *previousP; |
---|
| 998 | } |
---|
| 999 | if (cuddT(newf1) == f11 && cuddE(newf1) == f01) { |
---|
| 1000 | cuddSatInc(newf1->ref); |
---|
| 1001 | } else { /* no match */ |
---|
| 1002 | newf1 = cuddDynamicAllocNode(table); |
---|
| 1003 | if (newf1 == NULL) |
---|
| 1004 | goto cuddSwapOutOfMem; |
---|
| 1005 | newf1->index = xindex; newf1->ref = 1; |
---|
| 1006 | cuddT(newf1) = f11; |
---|
| 1007 | cuddE(newf1) = f01; |
---|
| 1008 | /* Insert newf1 in the collision list xlist[posn]; |
---|
| 1009 | ** increase the ref counts of f11 and f01. |
---|
| 1010 | */ |
---|
| 1011 | newxkeys++; |
---|
| 1012 | newf1->next = *previousP; |
---|
| 1013 | *previousP = newf1; |
---|
| 1014 | cuddSatInc(f11->ref); |
---|
| 1015 | tmp = Cudd_Regular(f01); |
---|
| 1016 | cuddSatInc(tmp->ref); |
---|
| 1017 | } |
---|
| 1018 | } |
---|
| 1019 | cuddT(f) = newf1; |
---|
| 1020 | #ifdef DD_DEBUG |
---|
| 1021 | assert(!(Cudd_IsComplement(newf1))); |
---|
| 1022 | #endif |
---|
| 1023 | |
---|
| 1024 | /* Do the same for f0, keeping complement dots into account. */ |
---|
| 1025 | /* Decrease ref count of f0. */ |
---|
| 1026 | tmp = Cudd_Regular(f0); |
---|
| 1027 | cuddSatDec(tmp->ref); |
---|
| 1028 | /* Create the new E child. */ |
---|
| 1029 | if (f10 == f00) { |
---|
| 1030 | newf0 = f00; |
---|
| 1031 | tmp = Cudd_Regular(newf0); |
---|
| 1032 | cuddSatInc(tmp->ref); |
---|
| 1033 | } else { |
---|
| 1034 | /* make sure f10 is regular */ |
---|
| 1035 | newcomplement = Cudd_IsComplement(f10); |
---|
| 1036 | if (newcomplement) { |
---|
| 1037 | f10 = Cudd_Not(f10); |
---|
| 1038 | f00 = Cudd_Not(f00); |
---|
| 1039 | } |
---|
| 1040 | /* Check xlist for triple (xindex,f10,f00). */ |
---|
| 1041 | posn = ddHash(f10, f00, xshift); |
---|
| 1042 | /* For each element newf0 in collision list xlist[posn]. */ |
---|
| 1043 | previousP = &(xlist[posn]); |
---|
| 1044 | newf0 = *previousP; |
---|
| 1045 | while (f10 < cuddT(newf0)) { |
---|
| 1046 | previousP = &(newf0->next); |
---|
| 1047 | newf0 = *previousP; |
---|
| 1048 | } |
---|
| 1049 | while (f10 == cuddT(newf0) && f00 < cuddE(newf0)) { |
---|
| 1050 | previousP = &(newf0->next); |
---|
| 1051 | newf0 = *previousP; |
---|
| 1052 | } |
---|
| 1053 | if (cuddT(newf0) == f10 && cuddE(newf0) == f00) { |
---|
| 1054 | cuddSatInc(newf0->ref); |
---|
| 1055 | } else { /* no match */ |
---|
| 1056 | newf0 = cuddDynamicAllocNode(table); |
---|
| 1057 | if (newf0 == NULL) |
---|
| 1058 | goto cuddSwapOutOfMem; |
---|
| 1059 | newf0->index = xindex; newf0->ref = 1; |
---|
| 1060 | cuddT(newf0) = f10; |
---|
| 1061 | cuddE(newf0) = f00; |
---|
| 1062 | /* Insert newf0 in the collision list xlist[posn]; |
---|
| 1063 | ** increase the ref counts of f10 and f00. |
---|
| 1064 | */ |
---|
| 1065 | newxkeys++; |
---|
| 1066 | newf0->next = *previousP; |
---|
| 1067 | *previousP = newf0; |
---|
| 1068 | cuddSatInc(f10->ref); |
---|
| 1069 | tmp = Cudd_Regular(f00); |
---|
| 1070 | cuddSatInc(tmp->ref); |
---|
| 1071 | } |
---|
| 1072 | if (newcomplement) { |
---|
| 1073 | newf0 = Cudd_Not(newf0); |
---|
| 1074 | } |
---|
| 1075 | } |
---|
| 1076 | cuddE(f) = newf0; |
---|
| 1077 | |
---|
| 1078 | /* Insert the modified f in ylist. |
---|
| 1079 | ** The modified f does not already exists in ylist. |
---|
| 1080 | ** (Because of the uniqueness of the cofactors.) |
---|
| 1081 | */ |
---|
| 1082 | posn = ddHash(newf1, newf0, yshift); |
---|
| 1083 | newykeys++; |
---|
| 1084 | previousP = &(ylist[posn]); |
---|
| 1085 | tmp = *previousP; |
---|
| 1086 | while (newf1 < cuddT(tmp)) { |
---|
| 1087 | previousP = &(tmp->next); |
---|
| 1088 | tmp = *previousP; |
---|
| 1089 | } |
---|
| 1090 | while (newf1 == cuddT(tmp) && newf0 < cuddE(tmp)) { |
---|
| 1091 | previousP = &(tmp->next); |
---|
| 1092 | tmp = *previousP; |
---|
| 1093 | } |
---|
| 1094 | f->next = *previousP; |
---|
| 1095 | *previousP = f; |
---|
| 1096 | f = next; |
---|
| 1097 | } /* while f != NULL */ |
---|
| 1098 | |
---|
| 1099 | /* GC the y layer. */ |
---|
| 1100 | |
---|
| 1101 | /* For each node f in ylist. */ |
---|
| 1102 | for (i = 0; i < yslots; i++) { |
---|
| 1103 | previousP = &(ylist[i]); |
---|
| 1104 | f = *previousP; |
---|
| 1105 | while (f != sentinel) { |
---|
| 1106 | next = f->next; |
---|
| 1107 | if (f->ref == 0) { |
---|
| 1108 | tmp = cuddT(f); |
---|
| 1109 | cuddSatDec(tmp->ref); |
---|
| 1110 | tmp = Cudd_Regular(cuddE(f)); |
---|
| 1111 | cuddSatDec(tmp->ref); |
---|
| 1112 | cuddDeallocNode(table,f); |
---|
| 1113 | newykeys--; |
---|
| 1114 | } else { |
---|
| 1115 | *previousP = f; |
---|
| 1116 | previousP = &(f->next); |
---|
| 1117 | } |
---|
| 1118 | f = next; |
---|
| 1119 | } /* while f */ |
---|
| 1120 | *previousP = sentinel; |
---|
| 1121 | } /* for i */ |
---|
| 1122 | |
---|
| 1123 | #ifdef DD_DEBUG |
---|
| 1124 | #if 0 |
---|
| 1125 | (void) fprintf(table->out,"Swapping %d and %d\n",x,y); |
---|
| 1126 | #endif |
---|
| 1127 | count = 0; |
---|
| 1128 | idcheck = 0; |
---|
| 1129 | for (i = 0; i < yslots; i++) { |
---|
| 1130 | f = ylist[i]; |
---|
| 1131 | while (f != sentinel) { |
---|
| 1132 | count++; |
---|
| 1133 | if (f->index != (DdHalfWord) yindex) |
---|
| 1134 | idcheck++; |
---|
| 1135 | f = f->next; |
---|
| 1136 | } |
---|
| 1137 | } |
---|
| 1138 | if (count != newykeys) { |
---|
| 1139 | (void) fprintf(table->out, |
---|
| 1140 | "Error in finding newykeys\toldykeys = %d\tnewykeys = %d\tactual = %d\n", |
---|
| 1141 | oldykeys,newykeys,count); |
---|
| 1142 | } |
---|
| 1143 | if (idcheck != 0) |
---|
| 1144 | (void) fprintf(table->out, |
---|
| 1145 | "Error in id's of ylist\twrong id's = %d\n", |
---|
| 1146 | idcheck); |
---|
| 1147 | count = 0; |
---|
| 1148 | idcheck = 0; |
---|
| 1149 | for (i = 0; i < xslots; i++) { |
---|
| 1150 | f = xlist[i]; |
---|
| 1151 | while (f != sentinel) { |
---|
| 1152 | count++; |
---|
| 1153 | if (f->index != (DdHalfWord) xindex) |
---|
| 1154 | idcheck++; |
---|
| 1155 | f = f->next; |
---|
| 1156 | } |
---|
| 1157 | } |
---|
| 1158 | if (count != newxkeys) { |
---|
| 1159 | (void) fprintf(table->out, |
---|
| 1160 | "Error in finding newxkeys\toldxkeys = %d \tnewxkeys = %d \tactual = %d\n", |
---|
| 1161 | oldxkeys,newxkeys,count); |
---|
| 1162 | } |
---|
| 1163 | if (idcheck != 0) |
---|
| 1164 | (void) fprintf(table->out, |
---|
| 1165 | "Error in id's of xlist\twrong id's = %d\n", |
---|
| 1166 | idcheck); |
---|
| 1167 | #endif |
---|
| 1168 | |
---|
| 1169 | isolated += (table->vars[xindex]->ref == 1) + |
---|
| 1170 | (table->vars[yindex]->ref == 1); |
---|
| 1171 | table->isolated += isolated; |
---|
| 1172 | } |
---|
| 1173 | |
---|
| 1174 | /* Set the appropriate fields in table. */ |
---|
| 1175 | table->subtables[x].nodelist = ylist; |
---|
| 1176 | table->subtables[x].slots = yslots; |
---|
| 1177 | table->subtables[x].shift = yshift; |
---|
| 1178 | table->subtables[x].keys = newykeys; |
---|
| 1179 | table->subtables[x].maxKeys = yslots * DD_MAX_SUBTABLE_DENSITY; |
---|
| 1180 | i = table->subtables[x].bindVar; |
---|
| 1181 | table->subtables[x].bindVar = table->subtables[y].bindVar; |
---|
| 1182 | table->subtables[y].bindVar = i; |
---|
| 1183 | /* Adjust filds for lazy sifting. */ |
---|
| 1184 | varType = table->subtables[x].varType; |
---|
| 1185 | table->subtables[x].varType = table->subtables[y].varType; |
---|
| 1186 | table->subtables[y].varType = varType; |
---|
| 1187 | i = table->subtables[x].pairIndex; |
---|
| 1188 | table->subtables[x].pairIndex = table->subtables[y].pairIndex; |
---|
| 1189 | table->subtables[y].pairIndex = i; |
---|
| 1190 | i = table->subtables[x].varHandled; |
---|
| 1191 | table->subtables[x].varHandled = table->subtables[y].varHandled; |
---|
| 1192 | table->subtables[y].varHandled = i; |
---|
| 1193 | groupType = table->subtables[x].varToBeGrouped; |
---|
| 1194 | table->subtables[x].varToBeGrouped = table->subtables[y].varToBeGrouped; |
---|
| 1195 | table->subtables[y].varToBeGrouped = groupType; |
---|
| 1196 | |
---|
| 1197 | table->subtables[y].nodelist = xlist; |
---|
| 1198 | table->subtables[y].slots = xslots; |
---|
| 1199 | table->subtables[y].shift = xshift; |
---|
| 1200 | table->subtables[y].keys = newxkeys; |
---|
| 1201 | table->subtables[y].maxKeys = xslots * DD_MAX_SUBTABLE_DENSITY; |
---|
| 1202 | |
---|
| 1203 | table->perm[xindex] = y; table->perm[yindex] = x; |
---|
| 1204 | table->invperm[x] = yindex; table->invperm[y] = xindex; |
---|
| 1205 | |
---|
| 1206 | table->keys += newxkeys + newykeys - oldxkeys - oldykeys; |
---|
| 1207 | |
---|
| 1208 | return(table->keys - table->isolated); |
---|
| 1209 | |
---|
| 1210 | cuddSwapOutOfMem: |
---|
| 1211 | (void) fprintf(table->err,"Error: cuddSwapInPlace out of memory\n"); |
---|
| 1212 | |
---|
| 1213 | return (0); |
---|
| 1214 | |
---|
| 1215 | } /* end of cuddSwapInPlace */ |
---|
| 1216 | |
---|
| 1217 | |
---|
| 1218 | /**Function******************************************************************** |
---|
| 1219 | |
---|
| 1220 | Synopsis [Reorders BDD variables according to the order of the ZDD |
---|
| 1221 | variables.] |
---|
| 1222 | |
---|
| 1223 | Description [Reorders BDD variables according to the order of the |
---|
| 1224 | ZDD variables. This function can be called at the end of ZDD |
---|
| 1225 | reordering to insure that the order of the BDD variables is |
---|
| 1226 | consistent with the order of the ZDD variables. The number of ZDD |
---|
| 1227 | variables must be a multiple of the number of BDD variables. Let |
---|
| 1228 | <code>M</code> be the ratio of the two numbers. cuddBddAlignToZdd |
---|
| 1229 | then considers the ZDD variables from <code>M*i</code> to |
---|
| 1230 | <code>(M+1)*i-1</code> as corresponding to BDD variable |
---|
| 1231 | <code>i</code>. This function should be normally called from |
---|
| 1232 | Cudd_zddReduceHeap, which clears the cache. Returns 1 in case of |
---|
| 1233 | success; 0 otherwise.] |
---|
| 1234 | |
---|
| 1235 | SideEffects [Changes the BDD variable order for all diagrams and performs |
---|
| 1236 | garbage collection of the BDD unique table.] |
---|
| 1237 | |
---|
| 1238 | SeeAlso [Cudd_ShuffleHeap Cudd_zddReduceHeap] |
---|
| 1239 | |
---|
| 1240 | ******************************************************************************/ |
---|
| 1241 | int |
---|
| 1242 | cuddBddAlignToZdd( |
---|
| 1243 | DdManager * table /* DD manager */) |
---|
| 1244 | { |
---|
| 1245 | int *invperm; /* permutation array */ |
---|
| 1246 | int M; /* ratio of ZDD variables to BDD variables */ |
---|
| 1247 | int i; /* loop index */ |
---|
| 1248 | int result; /* return value */ |
---|
| 1249 | |
---|
| 1250 | /* We assume that a ratio of 0 is OK. */ |
---|
| 1251 | if (table->size == 0) |
---|
| 1252 | return(1); |
---|
| 1253 | |
---|
| 1254 | M = table->sizeZ / table->size; |
---|
| 1255 | /* Check whether the number of ZDD variables is a multiple of the |
---|
| 1256 | ** number of BDD variables. |
---|
| 1257 | */ |
---|
| 1258 | if (M * table->size != table->sizeZ) |
---|
| 1259 | return(0); |
---|
| 1260 | /* Create and initialize the inverse permutation array. */ |
---|
| 1261 | invperm = ALLOC(int,table->size); |
---|
| 1262 | if (invperm == NULL) { |
---|
| 1263 | table->errorCode = CUDD_MEMORY_OUT; |
---|
| 1264 | return(0); |
---|
| 1265 | } |
---|
| 1266 | for (i = 0; i < table->sizeZ; i += M) { |
---|
| 1267 | int indexZ = table->invpermZ[i]; |
---|
| 1268 | int index = indexZ / M; |
---|
| 1269 | invperm[i / M] = index; |
---|
| 1270 | } |
---|
| 1271 | /* Eliminate dead nodes. Do not scan the cache again, because we |
---|
| 1272 | ** assume that Cudd_zddReduceHeap has already cleared it. |
---|
| 1273 | */ |
---|
| 1274 | cuddGarbageCollect(table,0); |
---|
| 1275 | |
---|
| 1276 | /* Initialize number of isolated projection functions. */ |
---|
| 1277 | table->isolated = 0; |
---|
| 1278 | for (i = 0; i < table->size; i++) { |
---|
| 1279 | if (table->vars[i]->ref == 1) table->isolated++; |
---|
| 1280 | } |
---|
| 1281 | |
---|
| 1282 | /* Initialize the interaction matrix. */ |
---|
| 1283 | result = cuddInitInteract(table); |
---|
| 1284 | if (result == 0) return(0); |
---|
| 1285 | |
---|
| 1286 | result = ddShuffle(table, invperm); |
---|
| 1287 | FREE(invperm); |
---|
| 1288 | /* Free interaction matrix. */ |
---|
| 1289 | FREE(table->interact); |
---|
| 1290 | /* Fix the BDD variable group tree. */ |
---|
| 1291 | bddFixTree(table,table->tree); |
---|
| 1292 | return(result); |
---|
| 1293 | |
---|
| 1294 | } /* end of cuddBddAlignToZdd */ |
---|
| 1295 | |
---|
| 1296 | /*---------------------------------------------------------------------------*/ |
---|
| 1297 | /* Definition of static functions */ |
---|
| 1298 | /*---------------------------------------------------------------------------*/ |
---|
| 1299 | |
---|
| 1300 | |
---|
| 1301 | /**Function******************************************************************** |
---|
| 1302 | |
---|
| 1303 | Synopsis [Comparison function used by qsort.] |
---|
| 1304 | |
---|
| 1305 | Description [Comparison function used by qsort to order the |
---|
| 1306 | variables according to the number of keys in the subtables. |
---|
| 1307 | Returns the difference in number of keys between the two |
---|
| 1308 | variables being compared.] |
---|
| 1309 | |
---|
| 1310 | SideEffects [None] |
---|
| 1311 | |
---|
| 1312 | ******************************************************************************/ |
---|
| 1313 | static int |
---|
| 1314 | ddUniqueCompare( |
---|
| 1315 | int * ptrX, |
---|
| 1316 | int * ptrY) |
---|
| 1317 | { |
---|
| 1318 | #if 0 |
---|
| 1319 | if (entry[*ptrY] == entry[*ptrX]) { |
---|
| 1320 | return((*ptrX) - (*ptrY)); |
---|
| 1321 | } |
---|
| 1322 | #endif |
---|
| 1323 | return(entry[*ptrY] - entry[*ptrX]); |
---|
| 1324 | |
---|
| 1325 | } /* end of ddUniqueCompare */ |
---|
| 1326 | |
---|
| 1327 | |
---|
| 1328 | /**Function******************************************************************** |
---|
| 1329 | |
---|
| 1330 | Synopsis [Swaps any two variables.] |
---|
| 1331 | |
---|
| 1332 | Description [Swaps any two variables. Returns the set of moves.] |
---|
| 1333 | |
---|
| 1334 | SideEffects [None] |
---|
| 1335 | |
---|
| 1336 | ******************************************************************************/ |
---|
| 1337 | static Move * |
---|
| 1338 | ddSwapAny( |
---|
| 1339 | DdManager * table, |
---|
| 1340 | int x, |
---|
| 1341 | int y) |
---|
| 1342 | { |
---|
| 1343 | Move *move, *moves; |
---|
| 1344 | int xRef,yRef; |
---|
| 1345 | int xNext,yNext; |
---|
| 1346 | int size; |
---|
| 1347 | int limitSize; |
---|
| 1348 | int tmp; |
---|
| 1349 | |
---|
| 1350 | if (x >y) { |
---|
| 1351 | tmp = x; x = y; y = tmp; |
---|
| 1352 | } |
---|
| 1353 | |
---|
| 1354 | xRef = x; yRef = y; |
---|
| 1355 | |
---|
| 1356 | xNext = cuddNextHigh(table,x); |
---|
| 1357 | yNext = cuddNextLow(table,y); |
---|
| 1358 | moves = NULL; |
---|
| 1359 | limitSize = table->keys - table->isolated; |
---|
| 1360 | |
---|
| 1361 | for (;;) { |
---|
| 1362 | if ( xNext == yNext) { |
---|
| 1363 | size = cuddSwapInPlace(table,x,xNext); |
---|
| 1364 | if (size == 0) goto ddSwapAnyOutOfMem; |
---|
| 1365 | move = (Move *) cuddDynamicAllocNode(table); |
---|
| 1366 | if (move == NULL) goto ddSwapAnyOutOfMem; |
---|
| 1367 | move->x = x; |
---|
| 1368 | move->y = xNext; |
---|
| 1369 | move->size = size; |
---|
| 1370 | move->next = moves; |
---|
| 1371 | moves = move; |
---|
| 1372 | |
---|
| 1373 | size = cuddSwapInPlace(table,yNext,y); |
---|
| 1374 | if (size == 0) goto ddSwapAnyOutOfMem; |
---|
| 1375 | move = (Move *) cuddDynamicAllocNode(table); |
---|
| 1376 | if (move == NULL) goto ddSwapAnyOutOfMem; |
---|
| 1377 | move->x = yNext; |
---|
| 1378 | move->y = y; |
---|
| 1379 | move->size = size; |
---|
| 1380 | move->next = moves; |
---|
| 1381 | moves = move; |
---|
| 1382 | |
---|
| 1383 | size = cuddSwapInPlace(table,x,xNext); |
---|
| 1384 | if (size == 0) goto ddSwapAnyOutOfMem; |
---|
| 1385 | move = (Move *) cuddDynamicAllocNode(table); |
---|
| 1386 | if (move == NULL) goto ddSwapAnyOutOfMem; |
---|
| 1387 | move->x = x; |
---|
| 1388 | move->y = xNext; |
---|
| 1389 | move->size = size; |
---|
| 1390 | move->next = moves; |
---|
| 1391 | moves = move; |
---|
| 1392 | |
---|
| 1393 | tmp = x; x = y; y = tmp; |
---|
| 1394 | |
---|
| 1395 | } else if (x == yNext) { |
---|
| 1396 | |
---|
| 1397 | size = cuddSwapInPlace(table,x,xNext); |
---|
| 1398 | if (size == 0) goto ddSwapAnyOutOfMem; |
---|
| 1399 | move = (Move *) cuddDynamicAllocNode(table); |
---|
| 1400 | if (move == NULL) goto ddSwapAnyOutOfMem; |
---|
| 1401 | move->x = x; |
---|
| 1402 | move->y = xNext; |
---|
| 1403 | move->size = size; |
---|
| 1404 | move->next = moves; |
---|
| 1405 | moves = move; |
---|
| 1406 | |
---|
| 1407 | tmp = x; x = y; y = tmp; |
---|
| 1408 | |
---|
| 1409 | } else { |
---|
| 1410 | size = cuddSwapInPlace(table,x,xNext); |
---|
| 1411 | if (size == 0) goto ddSwapAnyOutOfMem; |
---|
| 1412 | move = (Move *) cuddDynamicAllocNode(table); |
---|
| 1413 | if (move == NULL) goto ddSwapAnyOutOfMem; |
---|
| 1414 | move->x = x; |
---|
| 1415 | move->y = xNext; |
---|
| 1416 | move->size = size; |
---|
| 1417 | move->next = moves; |
---|
| 1418 | moves = move; |
---|
| 1419 | |
---|
| 1420 | size = cuddSwapInPlace(table,yNext,y); |
---|
| 1421 | if (size == 0) goto ddSwapAnyOutOfMem; |
---|
| 1422 | move = (Move *) cuddDynamicAllocNode(table); |
---|
| 1423 | if (move == NULL) goto ddSwapAnyOutOfMem; |
---|
| 1424 | move->x = yNext; |
---|
| 1425 | move->y = y; |
---|
| 1426 | move->size = size; |
---|
| 1427 | move->next = moves; |
---|
| 1428 | moves = move; |
---|
| 1429 | |
---|
| 1430 | x = xNext; |
---|
| 1431 | y = yNext; |
---|
| 1432 | } |
---|
| 1433 | |
---|
| 1434 | xNext = cuddNextHigh(table,x); |
---|
| 1435 | yNext = cuddNextLow(table,y); |
---|
| 1436 | if (xNext > yRef) break; |
---|
| 1437 | |
---|
| 1438 | if ((double) size > table->maxGrowth * (double) limitSize) break; |
---|
| 1439 | if (size < limitSize) limitSize = size; |
---|
| 1440 | } |
---|
| 1441 | if (yNext>=xRef) { |
---|
| 1442 | size = cuddSwapInPlace(table,yNext,y); |
---|
| 1443 | if (size == 0) goto ddSwapAnyOutOfMem; |
---|
| 1444 | move = (Move *) cuddDynamicAllocNode(table); |
---|
| 1445 | if (move == NULL) goto ddSwapAnyOutOfMem; |
---|
| 1446 | move->x = yNext; |
---|
| 1447 | move->y = y; |
---|
| 1448 | move->size = size; |
---|
| 1449 | move->next = moves; |
---|
| 1450 | moves = move; |
---|
| 1451 | } |
---|
| 1452 | |
---|
| 1453 | return(moves); |
---|
| 1454 | |
---|
| 1455 | ddSwapAnyOutOfMem: |
---|
| 1456 | while (moves != NULL) { |
---|
| 1457 | move = moves->next; |
---|
| 1458 | cuddDeallocMove(table, moves); |
---|
| 1459 | moves = move; |
---|
| 1460 | } |
---|
| 1461 | return(NULL); |
---|
| 1462 | |
---|
| 1463 | } /* end of ddSwapAny */ |
---|
| 1464 | |
---|
| 1465 | |
---|
| 1466 | /**Function******************************************************************** |
---|
| 1467 | |
---|
| 1468 | Synopsis [Given xLow <= x <= xHigh moves x up and down between the |
---|
| 1469 | boundaries.] |
---|
| 1470 | |
---|
| 1471 | Description [Given xLow <= x <= xHigh moves x up and down between the |
---|
| 1472 | boundaries. Finds the best position and does the required changes. |
---|
| 1473 | Returns 1 if successful; 0 otherwise.] |
---|
| 1474 | |
---|
| 1475 | SideEffects [None] |
---|
| 1476 | |
---|
| 1477 | ******************************************************************************/ |
---|
| 1478 | static int |
---|
| 1479 | ddSiftingAux( |
---|
| 1480 | DdManager * table, |
---|
| 1481 | int x, |
---|
| 1482 | int xLow, |
---|
| 1483 | int xHigh) |
---|
| 1484 | { |
---|
| 1485 | |
---|
| 1486 | Move *move; |
---|
| 1487 | Move *moveUp; /* list of up moves */ |
---|
| 1488 | Move *moveDown; /* list of down moves */ |
---|
| 1489 | int initialSize; |
---|
| 1490 | int result; |
---|
| 1491 | |
---|
| 1492 | initialSize = table->keys - table->isolated; |
---|
| 1493 | |
---|
| 1494 | moveDown = NULL; |
---|
| 1495 | moveUp = NULL; |
---|
| 1496 | |
---|
| 1497 | if (x == xLow) { |
---|
| 1498 | moveDown = ddSiftingDown(table,x,xHigh); |
---|
| 1499 | /* At this point x --> xHigh unless bounding occurred. */ |
---|
| 1500 | if (moveDown == (Move *) CUDD_OUT_OF_MEM) goto ddSiftingAuxOutOfMem; |
---|
| 1501 | /* Move backward and stop at best position. */ |
---|
| 1502 | result = ddSiftingBackward(table,initialSize,moveDown); |
---|
| 1503 | if (!result) goto ddSiftingAuxOutOfMem; |
---|
| 1504 | |
---|
| 1505 | } else if (x == xHigh) { |
---|
| 1506 | moveUp = ddSiftingUp(table,x,xLow); |
---|
| 1507 | /* At this point x --> xLow unless bounding occurred. */ |
---|
| 1508 | if (moveUp == (Move *) CUDD_OUT_OF_MEM) goto ddSiftingAuxOutOfMem; |
---|
| 1509 | /* Move backward and stop at best position. */ |
---|
| 1510 | result = ddSiftingBackward(table,initialSize,moveUp); |
---|
| 1511 | if (!result) goto ddSiftingAuxOutOfMem; |
---|
| 1512 | |
---|
| 1513 | } else if ((x - xLow) > (xHigh - x)) { /* must go down first: shorter */ |
---|
| 1514 | moveDown = ddSiftingDown(table,x,xHigh); |
---|
| 1515 | /* At this point x --> xHigh unless bounding occurred. */ |
---|
| 1516 | if (moveDown == (Move *) CUDD_OUT_OF_MEM) goto ddSiftingAuxOutOfMem; |
---|
| 1517 | if (moveDown != NULL) { |
---|
| 1518 | x = moveDown->y; |
---|
| 1519 | } |
---|
| 1520 | moveUp = ddSiftingUp(table,x,xLow); |
---|
| 1521 | if (moveUp == (Move *) CUDD_OUT_OF_MEM) goto ddSiftingAuxOutOfMem; |
---|
| 1522 | /* Move backward and stop at best position */ |
---|
| 1523 | result = ddSiftingBackward(table,initialSize,moveUp); |
---|
| 1524 | if (!result) goto ddSiftingAuxOutOfMem; |
---|
| 1525 | |
---|
| 1526 | } else { /* must go up first: shorter */ |
---|
| 1527 | moveUp = ddSiftingUp(table,x,xLow); |
---|
| 1528 | /* At this point x --> xLow unless bounding occurred. */ |
---|
| 1529 | if (moveUp == (Move *) CUDD_OUT_OF_MEM) goto ddSiftingAuxOutOfMem; |
---|
| 1530 | if (moveUp != NULL) { |
---|
| 1531 | x = moveUp->x; |
---|
| 1532 | } |
---|
| 1533 | moveDown = ddSiftingDown(table,x,xHigh); |
---|
| 1534 | if (moveDown == (Move *) CUDD_OUT_OF_MEM) goto ddSiftingAuxOutOfMem; |
---|
| 1535 | /* Move backward and stop at best position. */ |
---|
| 1536 | result = ddSiftingBackward(table,initialSize,moveDown); |
---|
| 1537 | if (!result) goto ddSiftingAuxOutOfMem; |
---|
| 1538 | } |
---|
| 1539 | |
---|
| 1540 | while (moveDown != NULL) { |
---|
| 1541 | move = moveDown->next; |
---|
| 1542 | cuddDeallocMove(table, moveDown); |
---|
| 1543 | moveDown = move; |
---|
| 1544 | } |
---|
| 1545 | while (moveUp != NULL) { |
---|
| 1546 | move = moveUp->next; |
---|
| 1547 | cuddDeallocMove(table, moveUp); |
---|
| 1548 | moveUp = move; |
---|
| 1549 | } |
---|
| 1550 | |
---|
| 1551 | return(1); |
---|
| 1552 | |
---|
| 1553 | ddSiftingAuxOutOfMem: |
---|
| 1554 | if (moveDown != (Move *) CUDD_OUT_OF_MEM) { |
---|
| 1555 | while (moveDown != NULL) { |
---|
| 1556 | move = moveDown->next; |
---|
| 1557 | cuddDeallocMove(table, moveDown); |
---|
| 1558 | moveDown = move; |
---|
| 1559 | } |
---|
| 1560 | } |
---|
| 1561 | if (moveUp != (Move *) CUDD_OUT_OF_MEM) { |
---|
| 1562 | while (moveUp != NULL) { |
---|
| 1563 | move = moveUp->next; |
---|
| 1564 | cuddDeallocMove(table, moveUp); |
---|
| 1565 | moveUp = move; |
---|
| 1566 | } |
---|
| 1567 | } |
---|
| 1568 | |
---|
| 1569 | return(0); |
---|
| 1570 | |
---|
| 1571 | } /* end of ddSiftingAux */ |
---|
| 1572 | |
---|
| 1573 | |
---|
| 1574 | /**Function******************************************************************** |
---|
| 1575 | |
---|
| 1576 | Synopsis [Sifts a variable up.] |
---|
| 1577 | |
---|
| 1578 | Description [Sifts a variable up. Moves y up until either it reaches |
---|
| 1579 | the bound (xLow) or the size of the DD heap increases too much. |
---|
| 1580 | Returns the set of moves in case of success; NULL if memory is full.] |
---|
| 1581 | |
---|
| 1582 | SideEffects [None] |
---|
| 1583 | |
---|
| 1584 | ******************************************************************************/ |
---|
| 1585 | static Move * |
---|
| 1586 | ddSiftingUp( |
---|
| 1587 | DdManager * table, |
---|
| 1588 | int y, |
---|
| 1589 | int xLow) |
---|
| 1590 | { |
---|
| 1591 | Move *moves; |
---|
| 1592 | Move *move; |
---|
| 1593 | int x; |
---|
| 1594 | int size; |
---|
| 1595 | int limitSize; |
---|
| 1596 | int xindex, yindex; |
---|
| 1597 | int isolated; |
---|
| 1598 | int L; /* lower bound on DD size */ |
---|
| 1599 | #ifdef DD_DEBUG |
---|
| 1600 | int checkL; |
---|
| 1601 | int z; |
---|
| 1602 | int zindex; |
---|
| 1603 | #endif |
---|
| 1604 | |
---|
| 1605 | moves = NULL; |
---|
| 1606 | yindex = table->invperm[y]; |
---|
| 1607 | |
---|
| 1608 | /* Initialize the lower bound. |
---|
| 1609 | ** The part of the DD below y will not change. |
---|
| 1610 | ** The part of the DD above y that does not interact with y will not |
---|
| 1611 | ** change. The rest may vanish in the best case, except for |
---|
| 1612 | ** the nodes at level xLow, which will not vanish, regardless. |
---|
| 1613 | */ |
---|
| 1614 | limitSize = L = table->keys - table->isolated; |
---|
| 1615 | for (x = xLow + 1; x < y; x++) { |
---|
| 1616 | xindex = table->invperm[x]; |
---|
| 1617 | if (cuddTestInteract(table,xindex,yindex)) { |
---|
| 1618 | isolated = table->vars[xindex]->ref == 1; |
---|
| 1619 | L -= table->subtables[x].keys - isolated; |
---|
| 1620 | } |
---|
| 1621 | } |
---|
| 1622 | isolated = table->vars[yindex]->ref == 1; |
---|
| 1623 | L -= table->subtables[y].keys - isolated; |
---|
| 1624 | |
---|
| 1625 | x = cuddNextLow(table,y); |
---|
| 1626 | while (x >= xLow && L <= limitSize) { |
---|
| 1627 | xindex = table->invperm[x]; |
---|
| 1628 | #ifdef DD_DEBUG |
---|
| 1629 | checkL = table->keys - table->isolated; |
---|
| 1630 | for (z = xLow + 1; z < y; z++) { |
---|
| 1631 | zindex = table->invperm[z]; |
---|
| 1632 | if (cuddTestInteract(table,zindex,yindex)) { |
---|
| 1633 | isolated = table->vars[zindex]->ref == 1; |
---|
| 1634 | checkL -= table->subtables[z].keys - isolated; |
---|
| 1635 | } |
---|
| 1636 | } |
---|
| 1637 | isolated = table->vars[yindex]->ref == 1; |
---|
| 1638 | checkL -= table->subtables[y].keys - isolated; |
---|
| 1639 | assert(L == checkL); |
---|
| 1640 | #endif |
---|
| 1641 | size = cuddSwapInPlace(table,x,y); |
---|
| 1642 | if (size == 0) goto ddSiftingUpOutOfMem; |
---|
| 1643 | /* Update the lower bound. */ |
---|
| 1644 | if (cuddTestInteract(table,xindex,yindex)) { |
---|
| 1645 | isolated = table->vars[xindex]->ref == 1; |
---|
| 1646 | L += table->subtables[y].keys - isolated; |
---|
| 1647 | } |
---|
| 1648 | move = (Move *) cuddDynamicAllocNode(table); |
---|
| 1649 | if (move == NULL) goto ddSiftingUpOutOfMem; |
---|
| 1650 | move->x = x; |
---|
| 1651 | move->y = y; |
---|
| 1652 | move->size = size; |
---|
| 1653 | move->next = moves; |
---|
| 1654 | moves = move; |
---|
| 1655 | if ((double) size > (double) limitSize * table->maxGrowth) break; |
---|
| 1656 | if (size < limitSize) limitSize = size; |
---|
| 1657 | y = x; |
---|
| 1658 | x = cuddNextLow(table,y); |
---|
| 1659 | } |
---|
| 1660 | return(moves); |
---|
| 1661 | |
---|
| 1662 | ddSiftingUpOutOfMem: |
---|
| 1663 | while (moves != NULL) { |
---|
| 1664 | move = moves->next; |
---|
| 1665 | cuddDeallocMove(table, moves); |
---|
| 1666 | moves = move; |
---|
| 1667 | } |
---|
| 1668 | return((Move *) CUDD_OUT_OF_MEM); |
---|
| 1669 | |
---|
| 1670 | } /* end of ddSiftingUp */ |
---|
| 1671 | |
---|
| 1672 | |
---|
| 1673 | /**Function******************************************************************** |
---|
| 1674 | |
---|
| 1675 | Synopsis [Sifts a variable down.] |
---|
| 1676 | |
---|
| 1677 | Description [Sifts a variable down. Moves x down until either it |
---|
| 1678 | reaches the bound (xHigh) or the size of the DD heap increases too |
---|
| 1679 | much. Returns the set of moves in case of success; NULL if memory is |
---|
| 1680 | full.] |
---|
| 1681 | |
---|
| 1682 | SideEffects [None] |
---|
| 1683 | |
---|
| 1684 | ******************************************************************************/ |
---|
| 1685 | static Move * |
---|
| 1686 | ddSiftingDown( |
---|
| 1687 | DdManager * table, |
---|
| 1688 | int x, |
---|
| 1689 | int xHigh) |
---|
| 1690 | { |
---|
| 1691 | Move *moves; |
---|
| 1692 | Move *move; |
---|
| 1693 | int y; |
---|
| 1694 | int size; |
---|
| 1695 | int R; /* upper bound on node decrease */ |
---|
| 1696 | int limitSize; |
---|
| 1697 | int xindex, yindex; |
---|
| 1698 | int isolated; |
---|
| 1699 | #ifdef DD_DEBUG |
---|
| 1700 | int checkR; |
---|
| 1701 | int z; |
---|
| 1702 | int zindex; |
---|
| 1703 | #endif |
---|
| 1704 | |
---|
| 1705 | moves = NULL; |
---|
| 1706 | /* Initialize R */ |
---|
| 1707 | xindex = table->invperm[x]; |
---|
| 1708 | limitSize = size = table->keys - table->isolated; |
---|
| 1709 | R = 0; |
---|
| 1710 | for (y = xHigh; y > x; y--) { |
---|
| 1711 | yindex = table->invperm[y]; |
---|
| 1712 | if (cuddTestInteract(table,xindex,yindex)) { |
---|
| 1713 | isolated = table->vars[yindex]->ref == 1; |
---|
| 1714 | R += table->subtables[y].keys - isolated; |
---|
| 1715 | } |
---|
| 1716 | } |
---|
| 1717 | |
---|
| 1718 | y = cuddNextHigh(table,x); |
---|
| 1719 | while (y <= xHigh && size - R < limitSize) { |
---|
| 1720 | #ifdef DD_DEBUG |
---|
| 1721 | checkR = 0; |
---|
| 1722 | for (z = xHigh; z > x; z--) { |
---|
| 1723 | zindex = table->invperm[z]; |
---|
| 1724 | if (cuddTestInteract(table,xindex,zindex)) { |
---|
| 1725 | isolated = table->vars[zindex]->ref == 1; |
---|
| 1726 | checkR += table->subtables[z].keys - isolated; |
---|
| 1727 | } |
---|
| 1728 | } |
---|
| 1729 | assert(R == checkR); |
---|
| 1730 | #endif |
---|
| 1731 | /* Update upper bound on node decrease. */ |
---|
| 1732 | yindex = table->invperm[y]; |
---|
| 1733 | if (cuddTestInteract(table,xindex,yindex)) { |
---|
| 1734 | isolated = table->vars[yindex]->ref == 1; |
---|
| 1735 | R -= table->subtables[y].keys - isolated; |
---|
| 1736 | } |
---|
| 1737 | size = cuddSwapInPlace(table,x,y); |
---|
| 1738 | if (size == 0) goto ddSiftingDownOutOfMem; |
---|
| 1739 | move = (Move *) cuddDynamicAllocNode(table); |
---|
| 1740 | if (move == NULL) goto ddSiftingDownOutOfMem; |
---|
| 1741 | move->x = x; |
---|
| 1742 | move->y = y; |
---|
| 1743 | move->size = size; |
---|
| 1744 | move->next = moves; |
---|
| 1745 | moves = move; |
---|
| 1746 | if ((double) size > (double) limitSize * table->maxGrowth) break; |
---|
| 1747 | if (size < limitSize) limitSize = size; |
---|
| 1748 | x = y; |
---|
| 1749 | y = cuddNextHigh(table,x); |
---|
| 1750 | } |
---|
| 1751 | return(moves); |
---|
| 1752 | |
---|
| 1753 | ddSiftingDownOutOfMem: |
---|
| 1754 | while (moves != NULL) { |
---|
| 1755 | move = moves->next; |
---|
| 1756 | cuddDeallocMove(table, moves); |
---|
| 1757 | moves = move; |
---|
| 1758 | } |
---|
| 1759 | return((Move *) CUDD_OUT_OF_MEM); |
---|
| 1760 | |
---|
| 1761 | } /* end of ddSiftingDown */ |
---|
| 1762 | |
---|
| 1763 | |
---|
| 1764 | /**Function******************************************************************** |
---|
| 1765 | |
---|
| 1766 | Synopsis [Given a set of moves, returns the DD heap to the position |
---|
| 1767 | giving the minimum size.] |
---|
| 1768 | |
---|
| 1769 | Description [Given a set of moves, returns the DD heap to the |
---|
| 1770 | position giving the minimum size. In case of ties, returns to the |
---|
| 1771 | closest position giving the minimum size. Returns 1 in case of |
---|
| 1772 | success; 0 otherwise.] |
---|
| 1773 | |
---|
| 1774 | SideEffects [None] |
---|
| 1775 | |
---|
| 1776 | ******************************************************************************/ |
---|
| 1777 | static int |
---|
| 1778 | ddSiftingBackward( |
---|
| 1779 | DdManager * table, |
---|
| 1780 | int size, |
---|
| 1781 | Move * moves) |
---|
| 1782 | { |
---|
| 1783 | Move *move; |
---|
| 1784 | int res; |
---|
| 1785 | |
---|
| 1786 | for (move = moves; move != NULL; move = move->next) { |
---|
| 1787 | if (move->size < size) { |
---|
| 1788 | size = move->size; |
---|
| 1789 | } |
---|
| 1790 | } |
---|
| 1791 | |
---|
| 1792 | for (move = moves; move != NULL; move = move->next) { |
---|
| 1793 | if (move->size == size) return(1); |
---|
| 1794 | res = cuddSwapInPlace(table,(int)move->x,(int)move->y); |
---|
| 1795 | if (!res) return(0); |
---|
| 1796 | } |
---|
| 1797 | |
---|
| 1798 | return(1); |
---|
| 1799 | |
---|
| 1800 | } /* end of ddSiftingBackward */ |
---|
| 1801 | |
---|
| 1802 | |
---|
| 1803 | /**Function******************************************************************** |
---|
| 1804 | |
---|
| 1805 | Synopsis [Prepares the DD heap for dynamic reordering.] |
---|
| 1806 | |
---|
| 1807 | Description [Prepares the DD heap for dynamic reordering. Does |
---|
| 1808 | garbage collection, to guarantee that there are no dead nodes; |
---|
| 1809 | clears the cache, which is invalidated by dynamic reordering; initializes |
---|
| 1810 | the number of isolated projection functions; and initializes the |
---|
| 1811 | interaction matrix. Returns 1 in case of success; 0 otherwise.] |
---|
| 1812 | |
---|
| 1813 | SideEffects [None] |
---|
| 1814 | |
---|
| 1815 | ******************************************************************************/ |
---|
| 1816 | static int |
---|
| 1817 | ddReorderPreprocess( |
---|
| 1818 | DdManager * table) |
---|
| 1819 | { |
---|
| 1820 | int i; |
---|
| 1821 | int res; |
---|
| 1822 | |
---|
| 1823 | /* Clear the cache. */ |
---|
| 1824 | cuddCacheFlush(table); |
---|
| 1825 | cuddLocalCacheClearAll(table); |
---|
| 1826 | |
---|
| 1827 | /* Eliminate dead nodes. Do not scan the cache again. */ |
---|
| 1828 | cuddGarbageCollect(table,0); |
---|
| 1829 | |
---|
| 1830 | /* Initialize number of isolated projection functions. */ |
---|
| 1831 | table->isolated = 0; |
---|
| 1832 | for (i = 0; i < table->size; i++) { |
---|
| 1833 | if (table->vars[i]->ref == 1) table->isolated++; |
---|
| 1834 | } |
---|
| 1835 | |
---|
| 1836 | /* Initialize the interaction matrix. */ |
---|
| 1837 | res = cuddInitInteract(table); |
---|
| 1838 | if (res == 0) return(0); |
---|
| 1839 | |
---|
| 1840 | return(1); |
---|
| 1841 | |
---|
| 1842 | } /* end of ddReorderPreprocess */ |
---|
| 1843 | |
---|
| 1844 | |
---|
| 1845 | /**Function******************************************************************** |
---|
| 1846 | |
---|
| 1847 | Synopsis [Cleans up at the end of reordering.] |
---|
| 1848 | |
---|
| 1849 | Description [] |
---|
| 1850 | |
---|
| 1851 | SideEffects [None] |
---|
| 1852 | |
---|
| 1853 | ******************************************************************************/ |
---|
| 1854 | static int |
---|
| 1855 | ddReorderPostprocess( |
---|
| 1856 | DdManager * table) |
---|
| 1857 | { |
---|
| 1858 | |
---|
| 1859 | #ifdef DD_VERBOSE |
---|
| 1860 | (void) fflush(table->out); |
---|
| 1861 | #endif |
---|
| 1862 | |
---|
| 1863 | /* Free interaction matrix. */ |
---|
| 1864 | FREE(table->interact); |
---|
| 1865 | |
---|
| 1866 | return(1); |
---|
| 1867 | |
---|
| 1868 | } /* end of ddReorderPostprocess */ |
---|
| 1869 | |
---|
| 1870 | |
---|
| 1871 | /**Function******************************************************************** |
---|
| 1872 | |
---|
| 1873 | Synopsis [Reorders variables according to a given permutation.] |
---|
| 1874 | |
---|
| 1875 | Description [Reorders variables according to a given permutation. |
---|
| 1876 | The i-th permutation array contains the index of the variable that |
---|
| 1877 | should be brought to the i-th level. ddShuffle assumes that no |
---|
| 1878 | dead nodes are present and that the interaction matrix is properly |
---|
| 1879 | initialized. The reordering is achieved by a series of upward sifts. |
---|
| 1880 | Returns 1 if successful; 0 otherwise.] |
---|
| 1881 | |
---|
| 1882 | SideEffects [None] |
---|
| 1883 | |
---|
| 1884 | SeeAlso [] |
---|
| 1885 | |
---|
| 1886 | ******************************************************************************/ |
---|
| 1887 | static int |
---|
| 1888 | ddShuffle( |
---|
| 1889 | DdManager * table, |
---|
| 1890 | int * permutation) |
---|
| 1891 | { |
---|
| 1892 | int index; |
---|
| 1893 | int level; |
---|
| 1894 | int position; |
---|
| 1895 | int numvars; |
---|
| 1896 | int result; |
---|
| 1897 | #ifdef DD_STATS |
---|
| 1898 | long localTime; |
---|
| 1899 | int initialSize; |
---|
| 1900 | int finalSize; |
---|
| 1901 | int previousSize; |
---|
| 1902 | #endif |
---|
| 1903 | |
---|
| 1904 | ddTotalNumberSwapping = 0; |
---|
| 1905 | #ifdef DD_STATS |
---|
| 1906 | localTime = util_cpu_time(); |
---|
| 1907 | initialSize = table->keys - table->isolated; |
---|
| 1908 | (void) fprintf(table->out,"#:I_SHUFFLE %8d: initial size\n", |
---|
| 1909 | initialSize); |
---|
| 1910 | ddTotalNISwaps = 0; |
---|
| 1911 | #endif |
---|
| 1912 | |
---|
| 1913 | numvars = table->size; |
---|
| 1914 | |
---|
| 1915 | for (level = 0; level < numvars; level++) { |
---|
| 1916 | index = permutation[level]; |
---|
| 1917 | position = table->perm[index]; |
---|
| 1918 | #ifdef DD_STATS |
---|
| 1919 | previousSize = table->keys - table->isolated; |
---|
| 1920 | #endif |
---|
| 1921 | result = ddSiftUp(table,position,level); |
---|
| 1922 | if (!result) return(0); |
---|
| 1923 | #ifdef DD_STATS |
---|
| 1924 | if (table->keys < (unsigned) previousSize + table->isolated) { |
---|
| 1925 | (void) fprintf(table->out,"-"); |
---|
| 1926 | } else if (table->keys > (unsigned) previousSize + table->isolated) { |
---|
| 1927 | (void) fprintf(table->out,"+"); /* should never happen */ |
---|
| 1928 | } else { |
---|
| 1929 | (void) fprintf(table->out,"="); |
---|
| 1930 | } |
---|
| 1931 | fflush(table->out); |
---|
| 1932 | #endif |
---|
| 1933 | } |
---|
| 1934 | |
---|
| 1935 | #ifdef DD_STATS |
---|
| 1936 | (void) fprintf(table->out,"\n"); |
---|
| 1937 | finalSize = table->keys - table->isolated; |
---|
| 1938 | (void) fprintf(table->out,"#:F_SHUFFLE %8d: final size\n",finalSize); |
---|
| 1939 | (void) fprintf(table->out,"#:T_SHUFFLE %8g: total time (sec)\n", |
---|
| 1940 | ((double)(util_cpu_time() - localTime)/1000.0)); |
---|
| 1941 | (void) fprintf(table->out,"#:N_SHUFFLE %8d: total swaps\n", |
---|
| 1942 | ddTotalNumberSwapping); |
---|
| 1943 | (void) fprintf(table->out,"#:M_SHUFFLE %8d: NI swaps\n",ddTotalNISwaps); |
---|
| 1944 | #endif |
---|
| 1945 | |
---|
| 1946 | return(1); |
---|
| 1947 | |
---|
| 1948 | } /* end of ddShuffle */ |
---|
| 1949 | |
---|
| 1950 | |
---|
| 1951 | /**Function******************************************************************** |
---|
| 1952 | |
---|
| 1953 | Synopsis [Moves one variable up.] |
---|
| 1954 | |
---|
| 1955 | Description [Takes a variable from position x and sifts it up to |
---|
| 1956 | position xLow; xLow should be less than or equal to x. |
---|
| 1957 | Returns 1 if successful; 0 otherwise] |
---|
| 1958 | |
---|
| 1959 | SideEffects [None] |
---|
| 1960 | |
---|
| 1961 | SeeAlso [] |
---|
| 1962 | |
---|
| 1963 | ******************************************************************************/ |
---|
| 1964 | static int |
---|
| 1965 | ddSiftUp( |
---|
| 1966 | DdManager * table, |
---|
| 1967 | int x, |
---|
| 1968 | int xLow) |
---|
| 1969 | { |
---|
| 1970 | int y; |
---|
| 1971 | int size; |
---|
| 1972 | |
---|
| 1973 | y = cuddNextLow(table,x); |
---|
| 1974 | while (y >= xLow) { |
---|
| 1975 | size = cuddSwapInPlace(table,y,x); |
---|
| 1976 | if (size == 0) { |
---|
| 1977 | return(0); |
---|
| 1978 | } |
---|
| 1979 | x = y; |
---|
| 1980 | y = cuddNextLow(table,x); |
---|
| 1981 | } |
---|
| 1982 | return(1); |
---|
| 1983 | |
---|
| 1984 | } /* end of ddSiftUp */ |
---|
| 1985 | |
---|
| 1986 | |
---|
| 1987 | /**Function******************************************************************** |
---|
| 1988 | |
---|
| 1989 | Synopsis [Fixes the BDD variable group tree after a shuffle.] |
---|
| 1990 | |
---|
| 1991 | Description [Fixes the BDD variable group tree after a |
---|
| 1992 | shuffle. Assumes that the order of the variables in a terminal node |
---|
| 1993 | has not been changed.] |
---|
| 1994 | |
---|
| 1995 | SideEffects [Changes the BDD variable group tree.] |
---|
| 1996 | |
---|
| 1997 | SeeAlso [] |
---|
| 1998 | |
---|
| 1999 | ******************************************************************************/ |
---|
| 2000 | static void |
---|
| 2001 | bddFixTree( |
---|
| 2002 | DdManager * table, |
---|
| 2003 | MtrNode * treenode) |
---|
| 2004 | { |
---|
| 2005 | if (treenode == NULL) return; |
---|
| 2006 | treenode->low = ((int) treenode->index < table->size) ? |
---|
| 2007 | table->perm[treenode->index] : treenode->index; |
---|
| 2008 | if (treenode->child != NULL) { |
---|
| 2009 | bddFixTree(table, treenode->child); |
---|
| 2010 | } |
---|
| 2011 | if (treenode->younger != NULL) |
---|
| 2012 | bddFixTree(table, treenode->younger); |
---|
| 2013 | if (treenode->parent != NULL && treenode->low < treenode->parent->low) { |
---|
| 2014 | treenode->parent->low = treenode->low; |
---|
| 2015 | treenode->parent->index = treenode->index; |
---|
| 2016 | } |
---|
| 2017 | return; |
---|
| 2018 | |
---|
| 2019 | } /* end of bddFixTree */ |
---|
| 2020 | |
---|
| 2021 | |
---|
| 2022 | /**Function******************************************************************** |
---|
| 2023 | |
---|
| 2024 | Synopsis [Updates the BDD variable group tree before a shuffle.] |
---|
| 2025 | |
---|
| 2026 | Description [Updates the BDD variable group tree before a shuffle. |
---|
| 2027 | Returns 1 if successful; 0 otherwise.] |
---|
| 2028 | |
---|
| 2029 | SideEffects [Changes the BDD variable group tree.] |
---|
| 2030 | |
---|
| 2031 | SeeAlso [] |
---|
| 2032 | |
---|
| 2033 | ******************************************************************************/ |
---|
| 2034 | static int |
---|
| 2035 | ddUpdateMtrTree( |
---|
| 2036 | DdManager * table, |
---|
| 2037 | MtrNode * treenode, |
---|
| 2038 | int * perm, |
---|
| 2039 | int * invperm) |
---|
| 2040 | { |
---|
| 2041 | unsigned int i, size; |
---|
| 2042 | int index, level, minLevel, maxLevel, minIndex; |
---|
| 2043 | |
---|
| 2044 | if (treenode == NULL) return(1); |
---|
| 2045 | |
---|
| 2046 | minLevel = CUDD_MAXINDEX; |
---|
| 2047 | maxLevel = 0; |
---|
| 2048 | minIndex = -1; |
---|
| 2049 | /* i : level */ |
---|
| 2050 | for (i = treenode->low; i < treenode->low + treenode->size; i++) { |
---|
| 2051 | index = table->invperm[i]; |
---|
| 2052 | level = perm[index]; |
---|
| 2053 | if (level < minLevel) { |
---|
| 2054 | minLevel = level; |
---|
| 2055 | minIndex = index; |
---|
| 2056 | } |
---|
| 2057 | if (level > maxLevel) |
---|
| 2058 | maxLevel = level; |
---|
| 2059 | } |
---|
| 2060 | size = maxLevel - minLevel + 1; |
---|
| 2061 | if (minIndex == -1) return(0); |
---|
| 2062 | if (size == treenode->size) { |
---|
| 2063 | treenode->low = minLevel; |
---|
| 2064 | treenode->index = minIndex; |
---|
| 2065 | } else { |
---|
| 2066 | return(0); |
---|
| 2067 | } |
---|
| 2068 | |
---|
| 2069 | if (treenode->child != NULL) { |
---|
| 2070 | if (!ddUpdateMtrTree(table, treenode->child, perm, invperm)) |
---|
| 2071 | return(0); |
---|
| 2072 | } |
---|
| 2073 | if (treenode->younger != NULL) { |
---|
| 2074 | if (!ddUpdateMtrTree(table, treenode->younger, perm, invperm)) |
---|
| 2075 | return(0); |
---|
| 2076 | } |
---|
| 2077 | return(1); |
---|
| 2078 | } |
---|
| 2079 | |
---|
| 2080 | |
---|
| 2081 | /**Function******************************************************************** |
---|
| 2082 | |
---|
| 2083 | Synopsis [Checks the BDD variable group tree before a shuffle.] |
---|
| 2084 | |
---|
| 2085 | Description [Checks the BDD variable group tree before a shuffle. |
---|
| 2086 | Returns 1 if successful; 0 otherwise.] |
---|
| 2087 | |
---|
| 2088 | SideEffects [Changes the BDD variable group tree.] |
---|
| 2089 | |
---|
| 2090 | SeeAlso [] |
---|
| 2091 | |
---|
| 2092 | ******************************************************************************/ |
---|
| 2093 | static int |
---|
| 2094 | ddCheckPermuation( |
---|
| 2095 | DdManager * table, |
---|
| 2096 | MtrNode * treenode, |
---|
| 2097 | int * perm, |
---|
| 2098 | int * invperm) |
---|
| 2099 | { |
---|
| 2100 | unsigned int i, size; |
---|
| 2101 | int index, level, minLevel, maxLevel; |
---|
| 2102 | |
---|
| 2103 | if (treenode == NULL) return(1); |
---|
| 2104 | |
---|
| 2105 | minLevel = table->size; |
---|
| 2106 | maxLevel = 0; |
---|
| 2107 | /* i : level */ |
---|
| 2108 | for (i = treenode->low; i < treenode->low + treenode->size; i++) { |
---|
| 2109 | index = table->invperm[i]; |
---|
| 2110 | level = perm[index]; |
---|
| 2111 | if (level < minLevel) |
---|
| 2112 | minLevel = level; |
---|
| 2113 | if (level > maxLevel) |
---|
| 2114 | maxLevel = level; |
---|
| 2115 | } |
---|
| 2116 | size = maxLevel - minLevel + 1; |
---|
| 2117 | if (size != treenode->size) |
---|
| 2118 | return(0); |
---|
| 2119 | |
---|
| 2120 | if (treenode->child != NULL) { |
---|
| 2121 | if (!ddCheckPermuation(table, treenode->child, perm, invperm)) |
---|
| 2122 | return(0); |
---|
| 2123 | } |
---|
| 2124 | if (treenode->younger != NULL) { |
---|
| 2125 | if (!ddCheckPermuation(table, treenode->younger, perm, invperm)) |
---|
| 2126 | return(0); |
---|
| 2127 | } |
---|
| 2128 | return(1); |
---|
| 2129 | } |
---|