[13] | 1 | /**CFile*********************************************************************** |
---|
| 2 | |
---|
| 3 | FileName [cuddZddReord.c] |
---|
| 4 | |
---|
| 5 | PackageName [cudd] |
---|
| 6 | |
---|
| 7 | Synopsis [Procedures for dynamic variable ordering of ZDDs.] |
---|
| 8 | |
---|
| 9 | Description [External procedures included in this module: |
---|
| 10 | <ul> |
---|
| 11 | <li> Cudd_zddReduceHeap() |
---|
| 12 | <li> Cudd_zddShuffleHeap() |
---|
| 13 | </ul> |
---|
| 14 | Internal procedures included in this module: |
---|
| 15 | <ul> |
---|
| 16 | <li> cuddZddAlignToBdd() |
---|
| 17 | <li> cuddZddNextHigh() |
---|
| 18 | <li> cuddZddNextLow() |
---|
| 19 | <li> cuddZddUniqueCompare() |
---|
| 20 | <li> cuddZddSwapInPlace() |
---|
| 21 | <li> cuddZddSwapping() |
---|
| 22 | <li> cuddZddSifting() |
---|
| 23 | </ul> |
---|
| 24 | Static procedures included in this module: |
---|
| 25 | <ul> |
---|
| 26 | <li> zddSwapAny() |
---|
| 27 | <li> cuddZddSiftingAux() |
---|
| 28 | <li> cuddZddSiftingUp() |
---|
| 29 | <li> cuddZddSiftingDown() |
---|
| 30 | <li> cuddZddSiftingBackward() |
---|
| 31 | <li> zddReorderPreprocess() |
---|
| 32 | <li> zddReorderPostprocess() |
---|
| 33 | <li> zddShuffle() |
---|
| 34 | <li> zddSiftUp() |
---|
| 35 | </ul> |
---|
| 36 | ] |
---|
| 37 | |
---|
| 38 | SeeAlso [] |
---|
| 39 | |
---|
| 40 | Author [Hyong-Kyoon Shin, In-Ho Moon] |
---|
| 41 | |
---|
| 42 | Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado |
---|
| 43 | |
---|
| 44 | All rights reserved. |
---|
| 45 | |
---|
| 46 | Redistribution and use in source and binary forms, with or without |
---|
| 47 | modification, are permitted provided that the following conditions |
---|
| 48 | are met: |
---|
| 49 | |
---|
| 50 | Redistributions of source code must retain the above copyright |
---|
| 51 | notice, this list of conditions and the following disclaimer. |
---|
| 52 | |
---|
| 53 | Redistributions in binary form must reproduce the above copyright |
---|
| 54 | notice, this list of conditions and the following disclaimer in the |
---|
| 55 | documentation and/or other materials provided with the distribution. |
---|
| 56 | |
---|
| 57 | Neither the name of the University of Colorado nor the names of its |
---|
| 58 | contributors may be used to endorse or promote products derived from |
---|
| 59 | this software without specific prior written permission. |
---|
| 60 | |
---|
| 61 | THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS |
---|
| 62 | "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT |
---|
| 63 | LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS |
---|
| 64 | FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE |
---|
| 65 | COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, |
---|
| 66 | INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, |
---|
| 67 | BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; |
---|
| 68 | LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER |
---|
| 69 | CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT |
---|
| 70 | LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN |
---|
| 71 | ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE |
---|
| 72 | POSSIBILITY OF SUCH DAMAGE.] |
---|
| 73 | |
---|
| 74 | ******************************************************************************/ |
---|
| 75 | |
---|
| 76 | #include "util.h" |
---|
| 77 | #include "cuddInt.h" |
---|
| 78 | |
---|
| 79 | /*---------------------------------------------------------------------------*/ |
---|
| 80 | /* Constant declarations */ |
---|
| 81 | /*---------------------------------------------------------------------------*/ |
---|
| 82 | |
---|
| 83 | #define DD_MAX_SUBTABLE_SPARSITY 8 |
---|
| 84 | #define DD_SHRINK_FACTOR 2 |
---|
| 85 | |
---|
| 86 | /*---------------------------------------------------------------------------*/ |
---|
| 87 | /* Stucture declarations */ |
---|
| 88 | /*---------------------------------------------------------------------------*/ |
---|
| 89 | |
---|
| 90 | |
---|
| 91 | /*---------------------------------------------------------------------------*/ |
---|
| 92 | /* Type declarations */ |
---|
| 93 | /*---------------------------------------------------------------------------*/ |
---|
| 94 | |
---|
| 95 | |
---|
| 96 | /*---------------------------------------------------------------------------*/ |
---|
| 97 | /* Variable declarations */ |
---|
| 98 | /*---------------------------------------------------------------------------*/ |
---|
| 99 | |
---|
| 100 | #ifndef lint |
---|
| 101 | static char rcsid[] DD_UNUSED = "$Id: cuddZddReord.c,v 1.47 2004/08/13 18:04:53 fabio Exp $"; |
---|
| 102 | #endif |
---|
| 103 | |
---|
| 104 | int *zdd_entry; |
---|
| 105 | |
---|
| 106 | int zddTotalNumberSwapping; |
---|
| 107 | |
---|
| 108 | static DdNode *empty; |
---|
| 109 | |
---|
| 110 | |
---|
| 111 | /*---------------------------------------------------------------------------*/ |
---|
| 112 | /* Macro declarations */ |
---|
| 113 | /*---------------------------------------------------------------------------*/ |
---|
| 114 | |
---|
| 115 | |
---|
| 116 | /**AutomaticStart*************************************************************/ |
---|
| 117 | |
---|
| 118 | /*---------------------------------------------------------------------------*/ |
---|
| 119 | /* Static function prototypes */ |
---|
| 120 | /*---------------------------------------------------------------------------*/ |
---|
| 121 | |
---|
| 122 | static Move * zddSwapAny (DdManager *table, int x, int y); |
---|
| 123 | static int cuddZddSiftingAux (DdManager *table, int x, int x_low, int x_high); |
---|
| 124 | static Move * cuddZddSiftingUp (DdManager *table, int x, int x_low, int initial_size); |
---|
| 125 | static Move * cuddZddSiftingDown (DdManager *table, int x, int x_high, int initial_size); |
---|
| 126 | static int cuddZddSiftingBackward (DdManager *table, Move *moves, int size); |
---|
| 127 | static void zddReorderPreprocess (DdManager *table); |
---|
| 128 | static int zddReorderPostprocess (DdManager *table); |
---|
| 129 | static int zddShuffle (DdManager *table, int *permutation); |
---|
| 130 | static int zddSiftUp (DdManager *table, int x, int xLow); |
---|
| 131 | static void zddFixTree (DdManager *table, MtrNode *treenode); |
---|
| 132 | |
---|
| 133 | /**AutomaticEnd***************************************************************/ |
---|
| 134 | |
---|
| 135 | |
---|
| 136 | /*---------------------------------------------------------------------------*/ |
---|
| 137 | /* Definition of exported functions */ |
---|
| 138 | /*---------------------------------------------------------------------------*/ |
---|
| 139 | |
---|
| 140 | |
---|
| 141 | /**Function******************************************************************** |
---|
| 142 | |
---|
| 143 | Synopsis [Main dynamic reordering routine for ZDDs.] |
---|
| 144 | |
---|
| 145 | Description [Main dynamic reordering routine for ZDDs. |
---|
| 146 | Calls one of the possible reordering procedures: |
---|
| 147 | <ul> |
---|
| 148 | <li>Swapping |
---|
| 149 | <li>Sifting |
---|
| 150 | <li>Symmetric Sifting |
---|
| 151 | </ul> |
---|
| 152 | |
---|
| 153 | For sifting and symmetric sifting it is possible to request reordering |
---|
| 154 | to convergence.<p> |
---|
| 155 | |
---|
| 156 | The core of all methods is the reordering procedure |
---|
| 157 | cuddZddSwapInPlace() which swaps two adjacent variables. |
---|
| 158 | Returns 1 in case of success; 0 otherwise. In the case of symmetric |
---|
| 159 | sifting (with and without convergence) returns 1 plus the number of |
---|
| 160 | symmetric variables, in case of success.] |
---|
| 161 | |
---|
| 162 | SideEffects [Changes the variable order for all ZDDs and clears |
---|
| 163 | the cache.] |
---|
| 164 | |
---|
| 165 | ******************************************************************************/ |
---|
| 166 | int |
---|
| 167 | Cudd_zddReduceHeap( |
---|
| 168 | DdManager * table /* DD manager */, |
---|
| 169 | Cudd_ReorderingType heuristic /* method used for reordering */, |
---|
| 170 | int minsize /* bound below which no reordering occurs */) |
---|
| 171 | { |
---|
| 172 | DdHook *hook; |
---|
| 173 | int result; |
---|
| 174 | unsigned int nextDyn; |
---|
| 175 | #ifdef DD_STATS |
---|
| 176 | unsigned int initialSize; |
---|
| 177 | unsigned int finalSize; |
---|
| 178 | #endif |
---|
| 179 | long localTime; |
---|
| 180 | |
---|
| 181 | /* Don't reorder if there are too many dead nodes. */ |
---|
| 182 | if (table->keysZ - table->deadZ < (unsigned) minsize) |
---|
| 183 | return(1); |
---|
| 184 | |
---|
| 185 | if (heuristic == CUDD_REORDER_SAME) { |
---|
| 186 | heuristic = table->autoMethodZ; |
---|
| 187 | } |
---|
| 188 | if (heuristic == CUDD_REORDER_NONE) { |
---|
| 189 | return(1); |
---|
| 190 | } |
---|
| 191 | |
---|
| 192 | /* This call to Cudd_zddReduceHeap does initiate reordering. Therefore |
---|
| 193 | ** we count it. |
---|
| 194 | */ |
---|
| 195 | table->reorderings++; |
---|
| 196 | empty = table->zero; |
---|
| 197 | |
---|
| 198 | localTime = util_cpu_time(); |
---|
| 199 | |
---|
| 200 | /* Run the hook functions. */ |
---|
| 201 | hook = table->preReorderingHook; |
---|
| 202 | while (hook != NULL) { |
---|
| 203 | int res = (hook->f)(table, "ZDD", (void *)heuristic); |
---|
| 204 | if (res == 0) return(0); |
---|
| 205 | hook = hook->next; |
---|
| 206 | } |
---|
| 207 | |
---|
| 208 | /* Clear the cache and collect garbage. */ |
---|
| 209 | zddReorderPreprocess(table); |
---|
| 210 | zddTotalNumberSwapping = 0; |
---|
| 211 | |
---|
| 212 | #ifdef DD_STATS |
---|
| 213 | initialSize = table->keysZ; |
---|
| 214 | |
---|
| 215 | switch(heuristic) { |
---|
| 216 | case CUDD_REORDER_RANDOM: |
---|
| 217 | case CUDD_REORDER_RANDOM_PIVOT: |
---|
| 218 | (void) fprintf(table->out,"#:I_RANDOM "); |
---|
| 219 | break; |
---|
| 220 | case CUDD_REORDER_SIFT: |
---|
| 221 | case CUDD_REORDER_SIFT_CONVERGE: |
---|
| 222 | case CUDD_REORDER_SYMM_SIFT: |
---|
| 223 | case CUDD_REORDER_SYMM_SIFT_CONV: |
---|
| 224 | (void) fprintf(table->out,"#:I_SIFTING "); |
---|
| 225 | break; |
---|
| 226 | case CUDD_REORDER_LINEAR: |
---|
| 227 | case CUDD_REORDER_LINEAR_CONVERGE: |
---|
| 228 | (void) fprintf(table->out,"#:I_LINSIFT "); |
---|
| 229 | break; |
---|
| 230 | default: |
---|
| 231 | (void) fprintf(table->err,"Unsupported ZDD reordering method\n"); |
---|
| 232 | return(0); |
---|
| 233 | } |
---|
| 234 | (void) fprintf(table->out,"%8d: initial size",initialSize); |
---|
| 235 | #endif |
---|
| 236 | |
---|
| 237 | result = cuddZddTreeSifting(table,heuristic); |
---|
| 238 | |
---|
| 239 | #ifdef DD_STATS |
---|
| 240 | (void) fprintf(table->out,"\n"); |
---|
| 241 | finalSize = table->keysZ; |
---|
| 242 | (void) fprintf(table->out,"#:F_REORDER %8d: final size\n",finalSize); |
---|
| 243 | (void) fprintf(table->out,"#:T_REORDER %8g: total time (sec)\n", |
---|
| 244 | ((double)(util_cpu_time() - localTime)/1000.0)); |
---|
| 245 | (void) fprintf(table->out,"#:N_REORDER %8d: total swaps\n", |
---|
| 246 | zddTotalNumberSwapping); |
---|
| 247 | #endif |
---|
| 248 | |
---|
| 249 | if (result == 0) |
---|
| 250 | return(0); |
---|
| 251 | |
---|
| 252 | if (!zddReorderPostprocess(table)) |
---|
| 253 | return(0); |
---|
| 254 | |
---|
| 255 | if (table->realignZ) { |
---|
| 256 | if (!cuddBddAlignToZdd(table)) |
---|
| 257 | return(0); |
---|
| 258 | } |
---|
| 259 | |
---|
| 260 | nextDyn = table->keysZ * DD_DYN_RATIO; |
---|
| 261 | if (table->reorderings < 20 || nextDyn > table->nextDyn) |
---|
| 262 | table->nextDyn = nextDyn; |
---|
| 263 | else |
---|
| 264 | table->nextDyn += 20; |
---|
| 265 | |
---|
| 266 | table->reordered = 1; |
---|
| 267 | |
---|
| 268 | /* Run hook functions. */ |
---|
| 269 | hook = table->postReorderingHook; |
---|
| 270 | while (hook != NULL) { |
---|
| 271 | int res = (hook->f)(table, "ZDD", (void *)localTime); |
---|
| 272 | if (res == 0) return(0); |
---|
| 273 | hook = hook->next; |
---|
| 274 | } |
---|
| 275 | /* Update cumulative reordering time. */ |
---|
| 276 | table->reordTime += util_cpu_time() - localTime; |
---|
| 277 | |
---|
| 278 | return(result); |
---|
| 279 | |
---|
| 280 | } /* end of Cudd_zddReduceHeap */ |
---|
| 281 | |
---|
| 282 | |
---|
| 283 | /**Function******************************************************************** |
---|
| 284 | |
---|
| 285 | Synopsis [Reorders ZDD variables according to given permutation.] |
---|
| 286 | |
---|
| 287 | Description [Reorders ZDD variables according to given permutation. |
---|
| 288 | The i-th entry of the permutation array contains the index of the variable |
---|
| 289 | that should be brought to the i-th level. The size of the array should be |
---|
| 290 | equal or greater to the number of variables currently in use. |
---|
| 291 | Returns 1 in case of success; 0 otherwise.] |
---|
| 292 | |
---|
| 293 | SideEffects [Changes the ZDD variable order for all diagrams and clears |
---|
| 294 | the cache.] |
---|
| 295 | |
---|
| 296 | SeeAlso [Cudd_zddReduceHeap] |
---|
| 297 | |
---|
| 298 | ******************************************************************************/ |
---|
| 299 | int |
---|
| 300 | Cudd_zddShuffleHeap( |
---|
| 301 | DdManager * table /* DD manager */, |
---|
| 302 | int * permutation /* required variable permutation */) |
---|
| 303 | { |
---|
| 304 | |
---|
| 305 | int result; |
---|
| 306 | |
---|
| 307 | empty = table->zero; |
---|
| 308 | zddReorderPreprocess(table); |
---|
| 309 | |
---|
| 310 | result = zddShuffle(table,permutation); |
---|
| 311 | |
---|
| 312 | if (!zddReorderPostprocess(table)) return(0); |
---|
| 313 | |
---|
| 314 | return(result); |
---|
| 315 | |
---|
| 316 | } /* end of Cudd_zddShuffleHeap */ |
---|
| 317 | |
---|
| 318 | |
---|
| 319 | /*---------------------------------------------------------------------------*/ |
---|
| 320 | /* Definition of internal functions */ |
---|
| 321 | /*---------------------------------------------------------------------------*/ |
---|
| 322 | |
---|
| 323 | |
---|
| 324 | /**Function******************************************************************** |
---|
| 325 | |
---|
| 326 | Synopsis [Reorders ZDD variables according to the order of the BDD |
---|
| 327 | variables.] |
---|
| 328 | |
---|
| 329 | Description [Reorders ZDD variables according to the order of the |
---|
| 330 | BDD variables. This function can be called at the end of BDD |
---|
| 331 | reordering to insure that the order of the ZDD variables is |
---|
| 332 | consistent with the order of the BDD variables. The number of ZDD |
---|
| 333 | variables must be a multiple of the number of BDD variables. Let |
---|
| 334 | <code>M</code> be the ratio of the two numbers. cuddZddAlignToBdd |
---|
| 335 | then considers the ZDD variables from <code>M*i</code> to |
---|
| 336 | <code>(M+1)*i-1</code> as corresponding to BDD variable |
---|
| 337 | <code>i</code>. This function should be normally called from |
---|
| 338 | Cudd_ReduceHeap, which clears the cache. Returns 1 in case of |
---|
| 339 | success; 0 otherwise.] |
---|
| 340 | |
---|
| 341 | SideEffects [Changes the ZDD variable order for all diagrams and performs |
---|
| 342 | garbage collection of the ZDD unique table.] |
---|
| 343 | |
---|
| 344 | SeeAlso [Cudd_zddShuffleHeap Cudd_ReduceHeap] |
---|
| 345 | |
---|
| 346 | ******************************************************************************/ |
---|
| 347 | int |
---|
| 348 | cuddZddAlignToBdd( |
---|
| 349 | DdManager * table /* DD manager */) |
---|
| 350 | { |
---|
| 351 | int *invpermZ; /* permutation array */ |
---|
| 352 | int M; /* ratio of ZDD variables to BDD variables */ |
---|
| 353 | int i,j; /* loop indices */ |
---|
| 354 | int result; /* return value */ |
---|
| 355 | |
---|
| 356 | /* We assume that a ratio of 0 is OK. */ |
---|
| 357 | if (table->sizeZ == 0) |
---|
| 358 | return(1); |
---|
| 359 | |
---|
| 360 | empty = table->zero; |
---|
| 361 | M = table->sizeZ / table->size; |
---|
| 362 | /* Check whether the number of ZDD variables is a multiple of the |
---|
| 363 | ** number of BDD variables. |
---|
| 364 | */ |
---|
| 365 | if (M * table->size != table->sizeZ) |
---|
| 366 | return(0); |
---|
| 367 | /* Create and initialize the inverse permutation array. */ |
---|
| 368 | invpermZ = ALLOC(int,table->sizeZ); |
---|
| 369 | if (invpermZ == NULL) { |
---|
| 370 | table->errorCode = CUDD_MEMORY_OUT; |
---|
| 371 | return(0); |
---|
| 372 | } |
---|
| 373 | for (i = 0; i < table->size; i++) { |
---|
| 374 | int index = table->invperm[i]; |
---|
| 375 | int indexZ = index * M; |
---|
| 376 | int levelZ = table->permZ[indexZ]; |
---|
| 377 | levelZ = (levelZ / M) * M; |
---|
| 378 | for (j = 0; j < M; j++) { |
---|
| 379 | invpermZ[M * i + j] = table->invpermZ[levelZ + j]; |
---|
| 380 | } |
---|
| 381 | } |
---|
| 382 | /* Eliminate dead nodes. Do not scan the cache again, because we |
---|
| 383 | ** assume that Cudd_ReduceHeap has already cleared it. |
---|
| 384 | */ |
---|
| 385 | cuddGarbageCollect(table,0); |
---|
| 386 | |
---|
| 387 | result = zddShuffle(table, invpermZ); |
---|
| 388 | FREE(invpermZ); |
---|
| 389 | /* Fix the ZDD variable group tree. */ |
---|
| 390 | zddFixTree(table,table->treeZ); |
---|
| 391 | return(result); |
---|
| 392 | |
---|
| 393 | } /* end of cuddZddAlignToBdd */ |
---|
| 394 | |
---|
| 395 | |
---|
| 396 | /**Function******************************************************************** |
---|
| 397 | |
---|
| 398 | Synopsis [Finds the next subtable with a larger index.] |
---|
| 399 | |
---|
| 400 | Description [Finds the next subtable with a larger index. Returns the |
---|
| 401 | index.] |
---|
| 402 | |
---|
| 403 | SideEffects [None] |
---|
| 404 | |
---|
| 405 | SeeAlso [] |
---|
| 406 | |
---|
| 407 | ******************************************************************************/ |
---|
| 408 | int |
---|
| 409 | cuddZddNextHigh( |
---|
| 410 | DdManager * table, |
---|
| 411 | int x) |
---|
| 412 | { |
---|
| 413 | return(x + 1); |
---|
| 414 | |
---|
| 415 | } /* end of cuddZddNextHigh */ |
---|
| 416 | |
---|
| 417 | |
---|
| 418 | /**Function******************************************************************** |
---|
| 419 | |
---|
| 420 | Synopsis [Finds the next subtable with a smaller index.] |
---|
| 421 | |
---|
| 422 | Description [Finds the next subtable with a smaller index. Returns the |
---|
| 423 | index.] |
---|
| 424 | |
---|
| 425 | SideEffects [None] |
---|
| 426 | |
---|
| 427 | SeeAlso [] |
---|
| 428 | |
---|
| 429 | ******************************************************************************/ |
---|
| 430 | int |
---|
| 431 | cuddZddNextLow( |
---|
| 432 | DdManager * table, |
---|
| 433 | int x) |
---|
| 434 | { |
---|
| 435 | return(x - 1); |
---|
| 436 | |
---|
| 437 | } /* end of cuddZddNextLow */ |
---|
| 438 | |
---|
| 439 | |
---|
| 440 | /**Function******************************************************************** |
---|
| 441 | |
---|
| 442 | Synopsis [Comparison function used by qsort.] |
---|
| 443 | |
---|
| 444 | Description [Comparison function used by qsort to order the |
---|
| 445 | variables according to the number of keys in the subtables. |
---|
| 446 | Returns the difference in number of keys between the two |
---|
| 447 | variables being compared.] |
---|
| 448 | |
---|
| 449 | SideEffects [None] |
---|
| 450 | |
---|
| 451 | SeeAlso [] |
---|
| 452 | |
---|
| 453 | ******************************************************************************/ |
---|
| 454 | int |
---|
| 455 | cuddZddUniqueCompare( |
---|
| 456 | int * ptr_x, |
---|
| 457 | int * ptr_y) |
---|
| 458 | { |
---|
| 459 | return(zdd_entry[*ptr_y] - zdd_entry[*ptr_x]); |
---|
| 460 | |
---|
| 461 | } /* end of cuddZddUniqueCompare */ |
---|
| 462 | |
---|
| 463 | |
---|
| 464 | /**Function******************************************************************** |
---|
| 465 | |
---|
| 466 | Synopsis [Swaps two adjacent variables.] |
---|
| 467 | |
---|
| 468 | Description [Swaps two adjacent variables. It assumes that no dead |
---|
| 469 | nodes are present on entry to this procedure. The procedure then |
---|
| 470 | guarantees that no dead nodes will be present when it terminates. |
---|
| 471 | cuddZddSwapInPlace assumes that x < y. Returns the number of keys in |
---|
| 472 | the table if successful; 0 otherwise.] |
---|
| 473 | |
---|
| 474 | SideEffects [None] |
---|
| 475 | |
---|
| 476 | SeeAlso [] |
---|
| 477 | |
---|
| 478 | ******************************************************************************/ |
---|
| 479 | int |
---|
| 480 | cuddZddSwapInPlace( |
---|
| 481 | DdManager * table, |
---|
| 482 | int x, |
---|
| 483 | int y) |
---|
| 484 | { |
---|
| 485 | DdNodePtr *xlist, *ylist; |
---|
| 486 | int xindex, yindex; |
---|
| 487 | int xslots, yslots; |
---|
| 488 | int xshift, yshift; |
---|
| 489 | int oldxkeys, oldykeys; |
---|
| 490 | int newxkeys, newykeys; |
---|
| 491 | int i; |
---|
| 492 | int posn; |
---|
| 493 | DdNode *f, *f1, *f0, *f11, *f10, *f01, *f00; |
---|
| 494 | DdNode *newf1, *newf0, *next; |
---|
| 495 | DdNodePtr g, *lastP, *previousP; |
---|
| 496 | |
---|
| 497 | #ifdef DD_DEBUG |
---|
| 498 | assert(x < y); |
---|
| 499 | assert(cuddZddNextHigh(table,x) == y); |
---|
| 500 | assert(table->subtableZ[x].keys != 0); |
---|
| 501 | assert(table->subtableZ[y].keys != 0); |
---|
| 502 | assert(table->subtableZ[x].dead == 0); |
---|
| 503 | assert(table->subtableZ[y].dead == 0); |
---|
| 504 | #endif |
---|
| 505 | |
---|
| 506 | zddTotalNumberSwapping++; |
---|
| 507 | |
---|
| 508 | /* Get parameters of x subtable. */ |
---|
| 509 | xindex = table->invpermZ[x]; |
---|
| 510 | xlist = table->subtableZ[x].nodelist; |
---|
| 511 | oldxkeys = table->subtableZ[x].keys; |
---|
| 512 | xslots = table->subtableZ[x].slots; |
---|
| 513 | xshift = table->subtableZ[x].shift; |
---|
| 514 | newxkeys = 0; |
---|
| 515 | |
---|
| 516 | yindex = table->invpermZ[y]; |
---|
| 517 | ylist = table->subtableZ[y].nodelist; |
---|
| 518 | oldykeys = table->subtableZ[y].keys; |
---|
| 519 | yslots = table->subtableZ[y].slots; |
---|
| 520 | yshift = table->subtableZ[y].shift; |
---|
| 521 | newykeys = oldykeys; |
---|
| 522 | |
---|
| 523 | /* The nodes in the x layer that don't depend on y directly |
---|
| 524 | ** will stay there; the others are put in a chain. |
---|
| 525 | ** The chain is handled as a FIFO; g points to the beginning and |
---|
| 526 | ** last points to the end. |
---|
| 527 | */ |
---|
| 528 | |
---|
| 529 | g = NULL; |
---|
| 530 | lastP = &g; |
---|
| 531 | for (i = 0; i < xslots; i++) { |
---|
| 532 | previousP = &(xlist[i]); |
---|
| 533 | f = *previousP; |
---|
| 534 | while (f != NULL) { |
---|
| 535 | next = f->next; |
---|
| 536 | f1 = cuddT(f); f0 = cuddE(f); |
---|
| 537 | if ((f1->index != (DdHalfWord) yindex) && |
---|
| 538 | (f0->index != (DdHalfWord) yindex)) { /* stays */ |
---|
| 539 | newxkeys++; |
---|
| 540 | *previousP = f; |
---|
| 541 | previousP = &(f->next); |
---|
| 542 | } else { |
---|
| 543 | f->index = yindex; |
---|
| 544 | *lastP = f; |
---|
| 545 | lastP = &(f->next); |
---|
| 546 | } |
---|
| 547 | f = next; |
---|
| 548 | } /* while there are elements in the collision chain */ |
---|
| 549 | *previousP = NULL; |
---|
| 550 | } /* for each slot of the x subtable */ |
---|
| 551 | *lastP = NULL; |
---|
| 552 | |
---|
| 553 | |
---|
| 554 | #ifdef DD_COUNT |
---|
| 555 | table->swapSteps += oldxkeys - newxkeys; |
---|
| 556 | #endif |
---|
| 557 | /* Take care of the x nodes that must be re-expressed. |
---|
| 558 | ** They form a linked list pointed by g. Their index has been |
---|
| 559 | ** changed to yindex already. |
---|
| 560 | */ |
---|
| 561 | f = g; |
---|
| 562 | while (f != NULL) { |
---|
| 563 | next = f->next; |
---|
| 564 | /* Find f1, f0, f11, f10, f01, f00. */ |
---|
| 565 | f1 = cuddT(f); |
---|
| 566 | if ((int) f1->index == yindex) { |
---|
| 567 | f11 = cuddT(f1); f10 = cuddE(f1); |
---|
| 568 | } else { |
---|
| 569 | f11 = empty; f10 = f1; |
---|
| 570 | } |
---|
| 571 | f0 = cuddE(f); |
---|
| 572 | if ((int) f0->index == yindex) { |
---|
| 573 | f01 = cuddT(f0); f00 = cuddE(f0); |
---|
| 574 | } else { |
---|
| 575 | f01 = empty; f00 = f0; |
---|
| 576 | } |
---|
| 577 | |
---|
| 578 | /* Decrease ref count of f1. */ |
---|
| 579 | cuddSatDec(f1->ref); |
---|
| 580 | /* Create the new T child. */ |
---|
| 581 | if (f11 == empty) { |
---|
| 582 | if (f01 != empty) { |
---|
| 583 | newf1 = f01; |
---|
| 584 | cuddSatInc(newf1->ref); |
---|
| 585 | } |
---|
| 586 | /* else case was already handled when finding nodes |
---|
| 587 | ** with both children below level y |
---|
| 588 | */ |
---|
| 589 | } else { |
---|
| 590 | /* Check xlist for triple (xindex, f11, f01). */ |
---|
| 591 | posn = ddHash(f11, f01, xshift); |
---|
| 592 | /* For each element newf1 in collision list xlist[posn]. */ |
---|
| 593 | newf1 = xlist[posn]; |
---|
| 594 | while (newf1 != NULL) { |
---|
| 595 | if (cuddT(newf1) == f11 && cuddE(newf1) == f01) { |
---|
| 596 | cuddSatInc(newf1->ref); |
---|
| 597 | break; /* match */ |
---|
| 598 | } |
---|
| 599 | newf1 = newf1->next; |
---|
| 600 | } /* while newf1 */ |
---|
| 601 | if (newf1 == NULL) { /* no match */ |
---|
| 602 | newf1 = cuddDynamicAllocNode(table); |
---|
| 603 | if (newf1 == NULL) |
---|
| 604 | goto zddSwapOutOfMem; |
---|
| 605 | newf1->index = xindex; newf1->ref = 1; |
---|
| 606 | cuddT(newf1) = f11; |
---|
| 607 | cuddE(newf1) = f01; |
---|
| 608 | /* Insert newf1 in the collision list xlist[pos]; |
---|
| 609 | ** increase the ref counts of f11 and f01 |
---|
| 610 | */ |
---|
| 611 | newxkeys++; |
---|
| 612 | newf1->next = xlist[posn]; |
---|
| 613 | xlist[posn] = newf1; |
---|
| 614 | cuddSatInc(f11->ref); |
---|
| 615 | cuddSatInc(f01->ref); |
---|
| 616 | } |
---|
| 617 | } |
---|
| 618 | cuddT(f) = newf1; |
---|
| 619 | |
---|
| 620 | /* Do the same for f0. */ |
---|
| 621 | /* Decrease ref count of f0. */ |
---|
| 622 | cuddSatDec(f0->ref); |
---|
| 623 | /* Create the new E child. */ |
---|
| 624 | if (f10 == empty) { |
---|
| 625 | newf0 = f00; |
---|
| 626 | cuddSatInc(newf0->ref); |
---|
| 627 | } else { |
---|
| 628 | /* Check xlist for triple (xindex, f10, f00). */ |
---|
| 629 | posn = ddHash(f10, f00, xshift); |
---|
| 630 | /* For each element newf0 in collision list xlist[posn]. */ |
---|
| 631 | newf0 = xlist[posn]; |
---|
| 632 | while (newf0 != NULL) { |
---|
| 633 | if (cuddT(newf0) == f10 && cuddE(newf0) == f00) { |
---|
| 634 | cuddSatInc(newf0->ref); |
---|
| 635 | break; /* match */ |
---|
| 636 | } |
---|
| 637 | newf0 = newf0->next; |
---|
| 638 | } /* while newf0 */ |
---|
| 639 | if (newf0 == NULL) { /* no match */ |
---|
| 640 | newf0 = cuddDynamicAllocNode(table); |
---|
| 641 | if (newf0 == NULL) |
---|
| 642 | goto zddSwapOutOfMem; |
---|
| 643 | newf0->index = xindex; newf0->ref = 1; |
---|
| 644 | cuddT(newf0) = f10; cuddE(newf0) = f00; |
---|
| 645 | /* Insert newf0 in the collision list xlist[posn]; |
---|
| 646 | ** increase the ref counts of f10 and f00. |
---|
| 647 | */ |
---|
| 648 | newxkeys++; |
---|
| 649 | newf0->next = xlist[posn]; |
---|
| 650 | xlist[posn] = newf0; |
---|
| 651 | cuddSatInc(f10->ref); |
---|
| 652 | cuddSatInc(f00->ref); |
---|
| 653 | } |
---|
| 654 | } |
---|
| 655 | cuddE(f) = newf0; |
---|
| 656 | |
---|
| 657 | /* Insert the modified f in ylist. |
---|
| 658 | ** The modified f does not already exists in ylist. |
---|
| 659 | ** (Because of the uniqueness of the cofactors.) |
---|
| 660 | */ |
---|
| 661 | posn = ddHash(newf1, newf0, yshift); |
---|
| 662 | newykeys++; |
---|
| 663 | f->next = ylist[posn]; |
---|
| 664 | ylist[posn] = f; |
---|
| 665 | f = next; |
---|
| 666 | } /* while f != NULL */ |
---|
| 667 | |
---|
| 668 | /* GC the y layer. */ |
---|
| 669 | |
---|
| 670 | /* For each node f in ylist. */ |
---|
| 671 | for (i = 0; i < yslots; i++) { |
---|
| 672 | previousP = &(ylist[i]); |
---|
| 673 | f = *previousP; |
---|
| 674 | while (f != NULL) { |
---|
| 675 | next = f->next; |
---|
| 676 | if (f->ref == 0) { |
---|
| 677 | cuddSatDec(cuddT(f)->ref); |
---|
| 678 | cuddSatDec(cuddE(f)->ref); |
---|
| 679 | cuddDeallocNode(table, f); |
---|
| 680 | newykeys--; |
---|
| 681 | } else { |
---|
| 682 | *previousP = f; |
---|
| 683 | previousP = &(f->next); |
---|
| 684 | } |
---|
| 685 | f = next; |
---|
| 686 | } /* while f */ |
---|
| 687 | *previousP = NULL; |
---|
| 688 | } /* for i */ |
---|
| 689 | |
---|
| 690 | /* Set the appropriate fields in table. */ |
---|
| 691 | table->subtableZ[x].nodelist = ylist; |
---|
| 692 | table->subtableZ[x].slots = yslots; |
---|
| 693 | table->subtableZ[x].shift = yshift; |
---|
| 694 | table->subtableZ[x].keys = newykeys; |
---|
| 695 | table->subtableZ[x].maxKeys = yslots * DD_MAX_SUBTABLE_DENSITY; |
---|
| 696 | |
---|
| 697 | table->subtableZ[y].nodelist = xlist; |
---|
| 698 | table->subtableZ[y].slots = xslots; |
---|
| 699 | table->subtableZ[y].shift = xshift; |
---|
| 700 | table->subtableZ[y].keys = newxkeys; |
---|
| 701 | table->subtableZ[y].maxKeys = xslots * DD_MAX_SUBTABLE_DENSITY; |
---|
| 702 | |
---|
| 703 | table->permZ[xindex] = y; table->permZ[yindex] = x; |
---|
| 704 | table->invpermZ[x] = yindex; table->invpermZ[y] = xindex; |
---|
| 705 | |
---|
| 706 | table->keysZ += newxkeys + newykeys - oldxkeys - oldykeys; |
---|
| 707 | |
---|
| 708 | /* Update univ section; univ[x] remains the same. */ |
---|
| 709 | table->univ[y] = cuddT(table->univ[x]); |
---|
| 710 | |
---|
| 711 | return (table->keysZ); |
---|
| 712 | |
---|
| 713 | zddSwapOutOfMem: |
---|
| 714 | (void) fprintf(table->err, "Error: cuddZddSwapInPlace out of memory\n"); |
---|
| 715 | |
---|
| 716 | return (0); |
---|
| 717 | |
---|
| 718 | } /* end of cuddZddSwapInPlace */ |
---|
| 719 | |
---|
| 720 | |
---|
| 721 | /**Function******************************************************************** |
---|
| 722 | |
---|
| 723 | Synopsis [Reorders variables by a sequence of (non-adjacent) swaps.] |
---|
| 724 | |
---|
| 725 | Description [Implementation of Plessier's algorithm that reorders |
---|
| 726 | variables by a sequence of (non-adjacent) swaps. |
---|
| 727 | <ol> |
---|
| 728 | <li> Select two variables (RANDOM or HEURISTIC). |
---|
| 729 | <li> Permute these variables. |
---|
| 730 | <li> If the nodes have decreased accept the permutation. |
---|
| 731 | <li> Otherwise reconstruct the original heap. |
---|
| 732 | <li> Loop. |
---|
| 733 | </ol> |
---|
| 734 | Returns 1 in case of success; 0 otherwise.] |
---|
| 735 | |
---|
| 736 | SideEffects [None] |
---|
| 737 | |
---|
| 738 | SeeAlso [] |
---|
| 739 | |
---|
| 740 | ******************************************************************************/ |
---|
| 741 | int |
---|
| 742 | cuddZddSwapping( |
---|
| 743 | DdManager * table, |
---|
| 744 | int lower, |
---|
| 745 | int upper, |
---|
| 746 | Cudd_ReorderingType heuristic) |
---|
| 747 | { |
---|
| 748 | int i, j; |
---|
| 749 | int max, keys; |
---|
| 750 | int nvars; |
---|
| 751 | int x, y; |
---|
| 752 | int iterate; |
---|
| 753 | int previousSize; |
---|
| 754 | Move *moves, *move; |
---|
| 755 | int pivot; |
---|
| 756 | int modulo; |
---|
| 757 | int result; |
---|
| 758 | |
---|
| 759 | #ifdef DD_DEBUG |
---|
| 760 | /* Sanity check */ |
---|
| 761 | assert(lower >= 0 && upper < table->sizeZ && lower <= upper); |
---|
| 762 | #endif |
---|
| 763 | |
---|
| 764 | nvars = upper - lower + 1; |
---|
| 765 | iterate = nvars; |
---|
| 766 | |
---|
| 767 | for (i = 0; i < iterate; i++) { |
---|
| 768 | if (heuristic == CUDD_REORDER_RANDOM_PIVOT) { |
---|
| 769 | /* Find pivot <= id with maximum keys. */ |
---|
| 770 | for (max = -1, j = lower; j <= upper; j++) { |
---|
| 771 | if ((keys = table->subtableZ[j].keys) > max) { |
---|
| 772 | max = keys; |
---|
| 773 | pivot = j; |
---|
| 774 | } |
---|
| 775 | } |
---|
| 776 | |
---|
| 777 | modulo = upper - pivot; |
---|
| 778 | if (modulo == 0) { |
---|
| 779 | y = pivot; /* y = nvars-1 */ |
---|
| 780 | } else { |
---|
| 781 | /* y = random # from {pivot+1 .. nvars-1} */ |
---|
| 782 | y = pivot + 1 + (int) (Cudd_Random() % modulo); |
---|
| 783 | } |
---|
| 784 | |
---|
| 785 | modulo = pivot - lower - 1; |
---|
| 786 | if (modulo < 1) { /* if pivot = 1 or 0 */ |
---|
| 787 | x = lower; |
---|
| 788 | } else { |
---|
| 789 | do { /* x = random # from {0 .. pivot-2} */ |
---|
| 790 | x = (int) Cudd_Random() % modulo; |
---|
| 791 | } while (x == y); |
---|
| 792 | /* Is this condition really needed, since x and y |
---|
| 793 | are in regions separated by pivot? */ |
---|
| 794 | } |
---|
| 795 | } else { |
---|
| 796 | x = (int) (Cudd_Random() % nvars) + lower; |
---|
| 797 | do { |
---|
| 798 | y = (int) (Cudd_Random() % nvars) + lower; |
---|
| 799 | } while (x == y); |
---|
| 800 | } |
---|
| 801 | |
---|
| 802 | previousSize = table->keysZ; |
---|
| 803 | moves = zddSwapAny(table, x, y); |
---|
| 804 | if (moves == NULL) |
---|
| 805 | goto cuddZddSwappingOutOfMem; |
---|
| 806 | |
---|
| 807 | result = cuddZddSiftingBackward(table, moves, previousSize); |
---|
| 808 | if (!result) |
---|
| 809 | goto cuddZddSwappingOutOfMem; |
---|
| 810 | |
---|
| 811 | while (moves != NULL) { |
---|
| 812 | move = moves->next; |
---|
| 813 | cuddDeallocMove(table, moves); |
---|
| 814 | moves = move; |
---|
| 815 | } |
---|
| 816 | #ifdef DD_STATS |
---|
| 817 | if (table->keysZ < (unsigned) previousSize) { |
---|
| 818 | (void) fprintf(table->out,"-"); |
---|
| 819 | } else if (table->keysZ > (unsigned) previousSize) { |
---|
| 820 | (void) fprintf(table->out,"+"); /* should never happen */ |
---|
| 821 | } else { |
---|
| 822 | (void) fprintf(table->out,"="); |
---|
| 823 | } |
---|
| 824 | fflush(table->out); |
---|
| 825 | #endif |
---|
| 826 | } |
---|
| 827 | |
---|
| 828 | return(1); |
---|
| 829 | |
---|
| 830 | cuddZddSwappingOutOfMem: |
---|
| 831 | while (moves != NULL) { |
---|
| 832 | move = moves->next; |
---|
| 833 | cuddDeallocMove(table, moves); |
---|
| 834 | moves = move; |
---|
| 835 | } |
---|
| 836 | return(0); |
---|
| 837 | |
---|
| 838 | } /* end of cuddZddSwapping */ |
---|
| 839 | |
---|
| 840 | |
---|
| 841 | /**Function******************************************************************** |
---|
| 842 | |
---|
| 843 | Synopsis [Implementation of Rudell's sifting algorithm.] |
---|
| 844 | |
---|
| 845 | Description [Implementation of Rudell's sifting algorithm. |
---|
| 846 | Assumes that no dead nodes are present. |
---|
| 847 | <ol> |
---|
| 848 | <li> Order all the variables according to the number of entries |
---|
| 849 | in each unique table. |
---|
| 850 | <li> Sift the variable up and down, remembering each time the |
---|
| 851 | total size of the DD heap. |
---|
| 852 | <li> Select the best permutation. |
---|
| 853 | <li> Repeat 3 and 4 for all variables. |
---|
| 854 | </ol> |
---|
| 855 | Returns 1 if successful; 0 otherwise.] |
---|
| 856 | |
---|
| 857 | SideEffects [None] |
---|
| 858 | |
---|
| 859 | SeeAlso [] |
---|
| 860 | |
---|
| 861 | ******************************************************************************/ |
---|
| 862 | int |
---|
| 863 | cuddZddSifting( |
---|
| 864 | DdManager * table, |
---|
| 865 | int lower, |
---|
| 866 | int upper) |
---|
| 867 | { |
---|
| 868 | int i; |
---|
| 869 | int *var; |
---|
| 870 | int size; |
---|
| 871 | int x; |
---|
| 872 | int result; |
---|
| 873 | #ifdef DD_STATS |
---|
| 874 | int previousSize; |
---|
| 875 | #endif |
---|
| 876 | |
---|
| 877 | size = table->sizeZ; |
---|
| 878 | |
---|
| 879 | /* Find order in which to sift variables. */ |
---|
| 880 | var = NULL; |
---|
| 881 | zdd_entry = ALLOC(int, size); |
---|
| 882 | if (zdd_entry == NULL) { |
---|
| 883 | table->errorCode = CUDD_MEMORY_OUT; |
---|
| 884 | goto cuddZddSiftingOutOfMem; |
---|
| 885 | } |
---|
| 886 | var = ALLOC(int, size); |
---|
| 887 | if (var == NULL) { |
---|
| 888 | table->errorCode = CUDD_MEMORY_OUT; |
---|
| 889 | goto cuddZddSiftingOutOfMem; |
---|
| 890 | } |
---|
| 891 | |
---|
| 892 | for (i = 0; i < size; i++) { |
---|
| 893 | x = table->permZ[i]; |
---|
| 894 | zdd_entry[i] = table->subtableZ[x].keys; |
---|
| 895 | var[i] = i; |
---|
| 896 | } |
---|
| 897 | |
---|
| 898 | qsort((void *)var, size, sizeof(int), (DD_QSFP)cuddZddUniqueCompare); |
---|
| 899 | |
---|
| 900 | /* Now sift. */ |
---|
| 901 | for (i = 0; i < ddMin(table->siftMaxVar, size); i++) { |
---|
| 902 | if (zddTotalNumberSwapping >= table->siftMaxSwap) |
---|
| 903 | break; |
---|
| 904 | x = table->permZ[var[i]]; |
---|
| 905 | if (x < lower || x > upper) continue; |
---|
| 906 | #ifdef DD_STATS |
---|
| 907 | previousSize = table->keysZ; |
---|
| 908 | #endif |
---|
| 909 | result = cuddZddSiftingAux(table, x, lower, upper); |
---|
| 910 | if (!result) |
---|
| 911 | goto cuddZddSiftingOutOfMem; |
---|
| 912 | #ifdef DD_STATS |
---|
| 913 | if (table->keysZ < (unsigned) previousSize) { |
---|
| 914 | (void) fprintf(table->out,"-"); |
---|
| 915 | } else if (table->keysZ > (unsigned) previousSize) { |
---|
| 916 | (void) fprintf(table->out,"+"); /* should never happen */ |
---|
| 917 | (void) fprintf(table->out,"\nSize increased from %d to %d while sifting variable %d\n", previousSize, table->keysZ , var[i]); |
---|
| 918 | } else { |
---|
| 919 | (void) fprintf(table->out,"="); |
---|
| 920 | } |
---|
| 921 | fflush(table->out); |
---|
| 922 | #endif |
---|
| 923 | } |
---|
| 924 | |
---|
| 925 | FREE(var); |
---|
| 926 | FREE(zdd_entry); |
---|
| 927 | |
---|
| 928 | return(1); |
---|
| 929 | |
---|
| 930 | cuddZddSiftingOutOfMem: |
---|
| 931 | |
---|
| 932 | if (zdd_entry != NULL) FREE(zdd_entry); |
---|
| 933 | if (var != NULL) FREE(var); |
---|
| 934 | |
---|
| 935 | return(0); |
---|
| 936 | |
---|
| 937 | } /* end of cuddZddSifting */ |
---|
| 938 | |
---|
| 939 | |
---|
| 940 | /*---------------------------------------------------------------------------*/ |
---|
| 941 | /* Definition of static functions */ |
---|
| 942 | /*---------------------------------------------------------------------------*/ |
---|
| 943 | |
---|
| 944 | |
---|
| 945 | /**Function******************************************************************** |
---|
| 946 | |
---|
| 947 | Synopsis [Swaps any two variables.] |
---|
| 948 | |
---|
| 949 | Description [Swaps any two variables. Returns the set of moves.] |
---|
| 950 | |
---|
| 951 | SideEffects [None] |
---|
| 952 | |
---|
| 953 | SeeAlso [] |
---|
| 954 | |
---|
| 955 | ******************************************************************************/ |
---|
| 956 | static Move * |
---|
| 957 | zddSwapAny( |
---|
| 958 | DdManager * table, |
---|
| 959 | int x, |
---|
| 960 | int y) |
---|
| 961 | { |
---|
| 962 | Move *move, *moves; |
---|
| 963 | int tmp, size; |
---|
| 964 | int x_ref, y_ref; |
---|
| 965 | int x_next, y_next; |
---|
| 966 | int limit_size; |
---|
| 967 | |
---|
| 968 | if (x > y) { /* make x precede y */ |
---|
| 969 | tmp = x; x = y; y = tmp; |
---|
| 970 | } |
---|
| 971 | |
---|
| 972 | x_ref = x; y_ref = y; |
---|
| 973 | |
---|
| 974 | x_next = cuddZddNextHigh(table, x); |
---|
| 975 | y_next = cuddZddNextLow(table, y); |
---|
| 976 | moves = NULL; |
---|
| 977 | limit_size = table->keysZ; |
---|
| 978 | |
---|
| 979 | for (;;) { |
---|
| 980 | if (x_next == y_next) { /* x < x_next = y_next < y */ |
---|
| 981 | size = cuddZddSwapInPlace(table, x, x_next); |
---|
| 982 | if (size == 0) |
---|
| 983 | goto zddSwapAnyOutOfMem; |
---|
| 984 | move = (Move *) cuddDynamicAllocNode(table); |
---|
| 985 | if (move == NULL) |
---|
| 986 | goto zddSwapAnyOutOfMem; |
---|
| 987 | move->x = x; |
---|
| 988 | move->y = x_next; |
---|
| 989 | move->size = size; |
---|
| 990 | move->next = moves; |
---|
| 991 | moves = move; |
---|
| 992 | |
---|
| 993 | size = cuddZddSwapInPlace(table, y_next, y); |
---|
| 994 | if (size == 0) |
---|
| 995 | goto zddSwapAnyOutOfMem; |
---|
| 996 | move = (Move *)cuddDynamicAllocNode(table); |
---|
| 997 | if (move == NULL) |
---|
| 998 | goto zddSwapAnyOutOfMem; |
---|
| 999 | move->x = y_next; |
---|
| 1000 | move->y = y; |
---|
| 1001 | move->size = size; |
---|
| 1002 | move->next = moves; |
---|
| 1003 | moves = move; |
---|
| 1004 | |
---|
| 1005 | size = cuddZddSwapInPlace(table, x, x_next); |
---|
| 1006 | if (size == 0) |
---|
| 1007 | goto zddSwapAnyOutOfMem; |
---|
| 1008 | move = (Move *)cuddDynamicAllocNode(table); |
---|
| 1009 | if (move == NULL) |
---|
| 1010 | goto zddSwapAnyOutOfMem; |
---|
| 1011 | move->x = x; |
---|
| 1012 | move->y = x_next; |
---|
| 1013 | move->size = size; |
---|
| 1014 | move->next = moves; |
---|
| 1015 | moves = move; |
---|
| 1016 | |
---|
| 1017 | tmp = x; x = y; y = tmp; |
---|
| 1018 | |
---|
| 1019 | } else if (x == y_next) { /* x = y_next < y = x_next */ |
---|
| 1020 | size = cuddZddSwapInPlace(table, x, x_next); |
---|
| 1021 | if (size == 0) |
---|
| 1022 | goto zddSwapAnyOutOfMem; |
---|
| 1023 | move = (Move *)cuddDynamicAllocNode(table); |
---|
| 1024 | if (move == NULL) |
---|
| 1025 | goto zddSwapAnyOutOfMem; |
---|
| 1026 | move->x = x; |
---|
| 1027 | move->y = x_next; |
---|
| 1028 | move->size = size; |
---|
| 1029 | move->next = moves; |
---|
| 1030 | moves = move; |
---|
| 1031 | |
---|
| 1032 | tmp = x; x = y; y = tmp; |
---|
| 1033 | } else { |
---|
| 1034 | size = cuddZddSwapInPlace(table, x, x_next); |
---|
| 1035 | if (size == 0) |
---|
| 1036 | goto zddSwapAnyOutOfMem; |
---|
| 1037 | move = (Move *)cuddDynamicAllocNode(table); |
---|
| 1038 | if (move == NULL) |
---|
| 1039 | goto zddSwapAnyOutOfMem; |
---|
| 1040 | move->x = x; |
---|
| 1041 | move->y = x_next; |
---|
| 1042 | move->size = size; |
---|
| 1043 | move->next = moves; |
---|
| 1044 | moves = move; |
---|
| 1045 | |
---|
| 1046 | size = cuddZddSwapInPlace(table, y_next, y); |
---|
| 1047 | if (size == 0) |
---|
| 1048 | goto zddSwapAnyOutOfMem; |
---|
| 1049 | move = (Move *)cuddDynamicAllocNode(table); |
---|
| 1050 | if (move == NULL) |
---|
| 1051 | goto zddSwapAnyOutOfMem; |
---|
| 1052 | move->x = y_next; |
---|
| 1053 | move->y = y; |
---|
| 1054 | move->size = size; |
---|
| 1055 | move->next = moves; |
---|
| 1056 | moves = move; |
---|
| 1057 | |
---|
| 1058 | x = x_next; y = y_next; |
---|
| 1059 | } |
---|
| 1060 | |
---|
| 1061 | x_next = cuddZddNextHigh(table, x); |
---|
| 1062 | y_next = cuddZddNextLow(table, y); |
---|
| 1063 | if (x_next > y_ref) |
---|
| 1064 | break; /* if x == y_ref */ |
---|
| 1065 | |
---|
| 1066 | if ((double) size > table->maxGrowth * (double) limit_size) |
---|
| 1067 | break; |
---|
| 1068 | if (size < limit_size) |
---|
| 1069 | limit_size = size; |
---|
| 1070 | } |
---|
| 1071 | if (y_next >= x_ref) { |
---|
| 1072 | size = cuddZddSwapInPlace(table, y_next, y); |
---|
| 1073 | if (size == 0) |
---|
| 1074 | goto zddSwapAnyOutOfMem; |
---|
| 1075 | move = (Move *)cuddDynamicAllocNode(table); |
---|
| 1076 | if (move == NULL) |
---|
| 1077 | goto zddSwapAnyOutOfMem; |
---|
| 1078 | move->x = y_next; |
---|
| 1079 | move->y = y; |
---|
| 1080 | move->size = size; |
---|
| 1081 | move->next = moves; |
---|
| 1082 | moves = move; |
---|
| 1083 | } |
---|
| 1084 | |
---|
| 1085 | return(moves); |
---|
| 1086 | |
---|
| 1087 | zddSwapAnyOutOfMem: |
---|
| 1088 | while (moves != NULL) { |
---|
| 1089 | move = moves->next; |
---|
| 1090 | cuddDeallocMove(table, moves); |
---|
| 1091 | moves = move; |
---|
| 1092 | } |
---|
| 1093 | return(NULL); |
---|
| 1094 | |
---|
| 1095 | } /* end of zddSwapAny */ |
---|
| 1096 | |
---|
| 1097 | |
---|
| 1098 | /**Function******************************************************************** |
---|
| 1099 | |
---|
| 1100 | Synopsis [Given xLow <= x <= xHigh moves x up and down between the |
---|
| 1101 | boundaries.] |
---|
| 1102 | |
---|
| 1103 | Description [Given xLow <= x <= xHigh moves x up and down between the |
---|
| 1104 | boundaries. Finds the best position and does the required changes. |
---|
| 1105 | Returns 1 if successful; 0 otherwise.] |
---|
| 1106 | |
---|
| 1107 | SideEffects [None] |
---|
| 1108 | |
---|
| 1109 | SeeAlso [] |
---|
| 1110 | |
---|
| 1111 | ******************************************************************************/ |
---|
| 1112 | static int |
---|
| 1113 | cuddZddSiftingAux( |
---|
| 1114 | DdManager * table, |
---|
| 1115 | int x, |
---|
| 1116 | int x_low, |
---|
| 1117 | int x_high) |
---|
| 1118 | { |
---|
| 1119 | Move *move; |
---|
| 1120 | Move *moveUp; /* list of up move */ |
---|
| 1121 | Move *moveDown; /* list of down move */ |
---|
| 1122 | |
---|
| 1123 | int initial_size; |
---|
| 1124 | int result; |
---|
| 1125 | |
---|
| 1126 | initial_size = table->keysZ; |
---|
| 1127 | |
---|
| 1128 | #ifdef DD_DEBUG |
---|
| 1129 | assert(table->subtableZ[x].keys > 0); |
---|
| 1130 | #endif |
---|
| 1131 | |
---|
| 1132 | moveDown = NULL; |
---|
| 1133 | moveUp = NULL; |
---|
| 1134 | |
---|
| 1135 | if (x == x_low) { |
---|
| 1136 | moveDown = cuddZddSiftingDown(table, x, x_high, initial_size); |
---|
| 1137 | /* after that point x --> x_high */ |
---|
| 1138 | if (moveDown == NULL) |
---|
| 1139 | goto cuddZddSiftingAuxOutOfMem; |
---|
| 1140 | result = cuddZddSiftingBackward(table, moveDown, |
---|
| 1141 | initial_size); |
---|
| 1142 | /* move backward and stop at best position */ |
---|
| 1143 | if (!result) |
---|
| 1144 | goto cuddZddSiftingAuxOutOfMem; |
---|
| 1145 | |
---|
| 1146 | } |
---|
| 1147 | else if (x == x_high) { |
---|
| 1148 | moveUp = cuddZddSiftingUp(table, x, x_low, initial_size); |
---|
| 1149 | /* after that point x --> x_low */ |
---|
| 1150 | if (moveUp == NULL) |
---|
| 1151 | goto cuddZddSiftingAuxOutOfMem; |
---|
| 1152 | result = cuddZddSiftingBackward(table, moveUp, initial_size); |
---|
| 1153 | /* move backward and stop at best position */ |
---|
| 1154 | if (!result) |
---|
| 1155 | goto cuddZddSiftingAuxOutOfMem; |
---|
| 1156 | } |
---|
| 1157 | else if ((x - x_low) > (x_high - x)) { |
---|
| 1158 | /* must go down first:shorter */ |
---|
| 1159 | moveDown = cuddZddSiftingDown(table, x, x_high, initial_size); |
---|
| 1160 | /* after that point x --> x_high */ |
---|
| 1161 | if (moveDown == NULL) |
---|
| 1162 | goto cuddZddSiftingAuxOutOfMem; |
---|
| 1163 | moveUp = cuddZddSiftingUp(table, moveDown->y, x_low, |
---|
| 1164 | initial_size); |
---|
| 1165 | if (moveUp == NULL) |
---|
| 1166 | goto cuddZddSiftingAuxOutOfMem; |
---|
| 1167 | result = cuddZddSiftingBackward(table, moveUp, initial_size); |
---|
| 1168 | /* move backward and stop at best position */ |
---|
| 1169 | if (!result) |
---|
| 1170 | goto cuddZddSiftingAuxOutOfMem; |
---|
| 1171 | } |
---|
| 1172 | else { |
---|
| 1173 | moveUp = cuddZddSiftingUp(table, x, x_low, initial_size); |
---|
| 1174 | /* after that point x --> x_high */ |
---|
| 1175 | if (moveUp == NULL) |
---|
| 1176 | goto cuddZddSiftingAuxOutOfMem; |
---|
| 1177 | moveDown = cuddZddSiftingDown(table, moveUp->x, x_high, |
---|
| 1178 | initial_size); |
---|
| 1179 | /* then move up */ |
---|
| 1180 | if (moveDown == NULL) |
---|
| 1181 | goto cuddZddSiftingAuxOutOfMem; |
---|
| 1182 | result = cuddZddSiftingBackward(table, moveDown, |
---|
| 1183 | initial_size); |
---|
| 1184 | /* move backward and stop at best position */ |
---|
| 1185 | if (!result) |
---|
| 1186 | goto cuddZddSiftingAuxOutOfMem; |
---|
| 1187 | } |
---|
| 1188 | |
---|
| 1189 | while (moveDown != NULL) { |
---|
| 1190 | move = moveDown->next; |
---|
| 1191 | cuddDeallocMove(table, moveDown); |
---|
| 1192 | moveDown = move; |
---|
| 1193 | } |
---|
| 1194 | while (moveUp != NULL) { |
---|
| 1195 | move = moveUp->next; |
---|
| 1196 | cuddDeallocMove(table, moveUp); |
---|
| 1197 | moveUp = move; |
---|
| 1198 | } |
---|
| 1199 | |
---|
| 1200 | return(1); |
---|
| 1201 | |
---|
| 1202 | cuddZddSiftingAuxOutOfMem: |
---|
| 1203 | while (moveDown != NULL) { |
---|
| 1204 | move = moveDown->next; |
---|
| 1205 | cuddDeallocMove(table, moveDown); |
---|
| 1206 | moveDown = move; |
---|
| 1207 | } |
---|
| 1208 | while (moveUp != NULL) { |
---|
| 1209 | move = moveUp->next; |
---|
| 1210 | cuddDeallocMove(table, moveUp); |
---|
| 1211 | moveUp = move; |
---|
| 1212 | } |
---|
| 1213 | |
---|
| 1214 | return(0); |
---|
| 1215 | |
---|
| 1216 | } /* end of cuddZddSiftingAux */ |
---|
| 1217 | |
---|
| 1218 | |
---|
| 1219 | /**Function******************************************************************** |
---|
| 1220 | |
---|
| 1221 | Synopsis [Sifts a variable up.] |
---|
| 1222 | |
---|
| 1223 | Description [Sifts a variable up. Moves y up until either it reaches |
---|
| 1224 | the bound (x_low) or the size of the ZDD heap increases too much. |
---|
| 1225 | Returns the set of moves in case of success; NULL if memory is full.] |
---|
| 1226 | |
---|
| 1227 | SideEffects [None] |
---|
| 1228 | |
---|
| 1229 | SeeAlso [] |
---|
| 1230 | |
---|
| 1231 | ******************************************************************************/ |
---|
| 1232 | static Move * |
---|
| 1233 | cuddZddSiftingUp( |
---|
| 1234 | DdManager * table, |
---|
| 1235 | int x, |
---|
| 1236 | int x_low, |
---|
| 1237 | int initial_size) |
---|
| 1238 | { |
---|
| 1239 | Move *moves; |
---|
| 1240 | Move *move; |
---|
| 1241 | int y; |
---|
| 1242 | int size; |
---|
| 1243 | int limit_size = initial_size; |
---|
| 1244 | |
---|
| 1245 | moves = NULL; |
---|
| 1246 | y = cuddZddNextLow(table, x); |
---|
| 1247 | while (y >= x_low) { |
---|
| 1248 | size = cuddZddSwapInPlace(table, y, x); |
---|
| 1249 | if (size == 0) |
---|
| 1250 | goto cuddZddSiftingUpOutOfMem; |
---|
| 1251 | move = (Move *)cuddDynamicAllocNode(table); |
---|
| 1252 | if (move == NULL) |
---|
| 1253 | goto cuddZddSiftingUpOutOfMem; |
---|
| 1254 | move->x = y; |
---|
| 1255 | move->y = x; |
---|
| 1256 | move->size = size; |
---|
| 1257 | move->next = moves; |
---|
| 1258 | moves = move; |
---|
| 1259 | |
---|
| 1260 | if ((double)size > (double)limit_size * table->maxGrowth) |
---|
| 1261 | break; |
---|
| 1262 | if (size < limit_size) |
---|
| 1263 | limit_size = size; |
---|
| 1264 | |
---|
| 1265 | x = y; |
---|
| 1266 | y = cuddZddNextLow(table, x); |
---|
| 1267 | } |
---|
| 1268 | return(moves); |
---|
| 1269 | |
---|
| 1270 | cuddZddSiftingUpOutOfMem: |
---|
| 1271 | while (moves != NULL) { |
---|
| 1272 | move = moves->next; |
---|
| 1273 | cuddDeallocMove(table, moves); |
---|
| 1274 | moves = move; |
---|
| 1275 | } |
---|
| 1276 | return(NULL); |
---|
| 1277 | |
---|
| 1278 | } /* end of cuddZddSiftingUp */ |
---|
| 1279 | |
---|
| 1280 | |
---|
| 1281 | /**Function******************************************************************** |
---|
| 1282 | |
---|
| 1283 | Synopsis [Sifts a variable down.] |
---|
| 1284 | |
---|
| 1285 | Description [Sifts a variable down. Moves x down until either it |
---|
| 1286 | reaches the bound (x_high) or the size of the ZDD heap increases too |
---|
| 1287 | much. Returns the set of moves in case of success; NULL if memory is |
---|
| 1288 | full.] |
---|
| 1289 | |
---|
| 1290 | SideEffects [None] |
---|
| 1291 | |
---|
| 1292 | SeeAlso [] |
---|
| 1293 | |
---|
| 1294 | ******************************************************************************/ |
---|
| 1295 | static Move * |
---|
| 1296 | cuddZddSiftingDown( |
---|
| 1297 | DdManager * table, |
---|
| 1298 | int x, |
---|
| 1299 | int x_high, |
---|
| 1300 | int initial_size) |
---|
| 1301 | { |
---|
| 1302 | Move *moves; |
---|
| 1303 | Move *move; |
---|
| 1304 | int y; |
---|
| 1305 | int size; |
---|
| 1306 | int limit_size = initial_size; |
---|
| 1307 | |
---|
| 1308 | moves = NULL; |
---|
| 1309 | y = cuddZddNextHigh(table, x); |
---|
| 1310 | while (y <= x_high) { |
---|
| 1311 | size = cuddZddSwapInPlace(table, x, y); |
---|
| 1312 | if (size == 0) |
---|
| 1313 | goto cuddZddSiftingDownOutOfMem; |
---|
| 1314 | move = (Move *)cuddDynamicAllocNode(table); |
---|
| 1315 | if (move == NULL) |
---|
| 1316 | goto cuddZddSiftingDownOutOfMem; |
---|
| 1317 | move->x = x; |
---|
| 1318 | move->y = y; |
---|
| 1319 | move->size = size; |
---|
| 1320 | move->next = moves; |
---|
| 1321 | moves = move; |
---|
| 1322 | |
---|
| 1323 | if ((double)size > (double)limit_size * table->maxGrowth) |
---|
| 1324 | break; |
---|
| 1325 | if (size < limit_size) |
---|
| 1326 | limit_size = size; |
---|
| 1327 | |
---|
| 1328 | x = y; |
---|
| 1329 | y = cuddZddNextHigh(table, x); |
---|
| 1330 | } |
---|
| 1331 | return(moves); |
---|
| 1332 | |
---|
| 1333 | cuddZddSiftingDownOutOfMem: |
---|
| 1334 | while (moves != NULL) { |
---|
| 1335 | move = moves->next; |
---|
| 1336 | cuddDeallocMove(table, moves); |
---|
| 1337 | moves = move; |
---|
| 1338 | } |
---|
| 1339 | return(NULL); |
---|
| 1340 | |
---|
| 1341 | } /* end of cuddZddSiftingDown */ |
---|
| 1342 | |
---|
| 1343 | |
---|
| 1344 | /**Function******************************************************************** |
---|
| 1345 | |
---|
| 1346 | Synopsis [Given a set of moves, returns the ZDD heap to the position |
---|
| 1347 | giving the minimum size.] |
---|
| 1348 | |
---|
| 1349 | Description [Given a set of moves, returns the ZDD heap to the |
---|
| 1350 | position giving the minimum size. In case of ties, returns to the |
---|
| 1351 | closest position giving the minimum size. Returns 1 in case of |
---|
| 1352 | success; 0 otherwise.] |
---|
| 1353 | |
---|
| 1354 | SideEffects [None] |
---|
| 1355 | |
---|
| 1356 | SeeAlso [] |
---|
| 1357 | |
---|
| 1358 | ******************************************************************************/ |
---|
| 1359 | static int |
---|
| 1360 | cuddZddSiftingBackward( |
---|
| 1361 | DdManager * table, |
---|
| 1362 | Move * moves, |
---|
| 1363 | int size) |
---|
| 1364 | { |
---|
| 1365 | int i; |
---|
| 1366 | int i_best; |
---|
| 1367 | Move *move; |
---|
| 1368 | int res; |
---|
| 1369 | |
---|
| 1370 | /* Find the minimum size among moves. */ |
---|
| 1371 | i_best = -1; |
---|
| 1372 | for (move = moves, i = 0; move != NULL; move = move->next, i++) { |
---|
| 1373 | if (move->size < size) { |
---|
| 1374 | i_best = i; |
---|
| 1375 | size = move->size; |
---|
| 1376 | } |
---|
| 1377 | } |
---|
| 1378 | |
---|
| 1379 | for (move = moves, i = 0; move != NULL; move = move->next, i++) { |
---|
| 1380 | if (i == i_best) |
---|
| 1381 | break; |
---|
| 1382 | res = cuddZddSwapInPlace(table, move->x, move->y); |
---|
| 1383 | if (!res) |
---|
| 1384 | return(0); |
---|
| 1385 | if (i_best == -1 && res == size) |
---|
| 1386 | break; |
---|
| 1387 | } |
---|
| 1388 | |
---|
| 1389 | return(1); |
---|
| 1390 | |
---|
| 1391 | } /* end of cuddZddSiftingBackward */ |
---|
| 1392 | |
---|
| 1393 | |
---|
| 1394 | /**Function******************************************************************** |
---|
| 1395 | |
---|
| 1396 | Synopsis [Prepares the ZDD heap for dynamic reordering.] |
---|
| 1397 | |
---|
| 1398 | Description [Prepares the ZDD heap for dynamic reordering. Does |
---|
| 1399 | garbage collection, to guarantee that there are no dead nodes; |
---|
| 1400 | and clears the cache, which is invalidated by dynamic reordering.] |
---|
| 1401 | |
---|
| 1402 | SideEffects [None] |
---|
| 1403 | |
---|
| 1404 | ******************************************************************************/ |
---|
| 1405 | static void |
---|
| 1406 | zddReorderPreprocess( |
---|
| 1407 | DdManager * table) |
---|
| 1408 | { |
---|
| 1409 | |
---|
| 1410 | /* Clear the cache. */ |
---|
| 1411 | cuddCacheFlush(table); |
---|
| 1412 | |
---|
| 1413 | /* Eliminate dead nodes. Do not scan the cache again. */ |
---|
| 1414 | cuddGarbageCollect(table,0); |
---|
| 1415 | |
---|
| 1416 | return; |
---|
| 1417 | |
---|
| 1418 | } /* end of ddReorderPreprocess */ |
---|
| 1419 | |
---|
| 1420 | |
---|
| 1421 | /**Function******************************************************************** |
---|
| 1422 | |
---|
| 1423 | Synopsis [Shrinks almost empty ZDD subtables at the end of reordering |
---|
| 1424 | to guarantee that they have a reasonable load factor.] |
---|
| 1425 | |
---|
| 1426 | Description [Shrinks almost empty subtables at the end of reordering to |
---|
| 1427 | guarantee that they have a reasonable load factor. However, if there many |
---|
| 1428 | nodes are being reclaimed, then no resizing occurs. Returns 1 in case of |
---|
| 1429 | success; 0 otherwise.] |
---|
| 1430 | |
---|
| 1431 | SideEffects [None] |
---|
| 1432 | |
---|
| 1433 | ******************************************************************************/ |
---|
| 1434 | static int |
---|
| 1435 | zddReorderPostprocess( |
---|
| 1436 | DdManager * table) |
---|
| 1437 | { |
---|
| 1438 | int i, j, posn; |
---|
| 1439 | DdNodePtr *nodelist, *oldnodelist; |
---|
| 1440 | DdNode *node, *next; |
---|
| 1441 | unsigned int slots, oldslots; |
---|
| 1442 | extern DD_OOMFP MMoutOfMemory; |
---|
| 1443 | DD_OOMFP saveHandler; |
---|
| 1444 | |
---|
| 1445 | #ifdef DD_VERBOSE |
---|
| 1446 | (void) fflush(table->out); |
---|
| 1447 | #endif |
---|
| 1448 | |
---|
| 1449 | /* If we have very many reclaimed nodes, we do not want to shrink |
---|
| 1450 | ** the subtables, because this will lead to more garbage |
---|
| 1451 | ** collections. More garbage collections mean shorter mean life for |
---|
| 1452 | ** nodes with zero reference count; hence lower probability of finding |
---|
| 1453 | ** a result in the cache. |
---|
| 1454 | */ |
---|
| 1455 | if (table->reclaimed > table->allocated * 0.5) return(1); |
---|
| 1456 | |
---|
| 1457 | /* Resize subtables. */ |
---|
| 1458 | for (i = 0; i < table->sizeZ; i++) { |
---|
| 1459 | int shift; |
---|
| 1460 | oldslots = table->subtableZ[i].slots; |
---|
| 1461 | if (oldslots < table->subtableZ[i].keys * DD_MAX_SUBTABLE_SPARSITY || |
---|
| 1462 | oldslots <= table->initSlots) continue; |
---|
| 1463 | oldnodelist = table->subtableZ[i].nodelist; |
---|
| 1464 | slots = oldslots >> 1; |
---|
| 1465 | saveHandler = MMoutOfMemory; |
---|
| 1466 | MMoutOfMemory = Cudd_OutOfMem; |
---|
| 1467 | nodelist = ALLOC(DdNodePtr, slots); |
---|
| 1468 | MMoutOfMemory = saveHandler; |
---|
| 1469 | if (nodelist == NULL) { |
---|
| 1470 | return(1); |
---|
| 1471 | } |
---|
| 1472 | table->subtableZ[i].nodelist = nodelist; |
---|
| 1473 | table->subtableZ[i].slots = slots; |
---|
| 1474 | table->subtableZ[i].shift++; |
---|
| 1475 | table->subtableZ[i].maxKeys = slots * DD_MAX_SUBTABLE_DENSITY; |
---|
| 1476 | #ifdef DD_VERBOSE |
---|
| 1477 | (void) fprintf(table->err, |
---|
| 1478 | "shrunk layer %d (%d keys) from %d to %d slots\n", |
---|
| 1479 | i, table->subtableZ[i].keys, oldslots, slots); |
---|
| 1480 | #endif |
---|
| 1481 | |
---|
| 1482 | for (j = 0; (unsigned) j < slots; j++) { |
---|
| 1483 | nodelist[j] = NULL; |
---|
| 1484 | } |
---|
| 1485 | shift = table->subtableZ[i].shift; |
---|
| 1486 | for (j = 0; (unsigned) j < oldslots; j++) { |
---|
| 1487 | node = oldnodelist[j]; |
---|
| 1488 | while (node != NULL) { |
---|
| 1489 | next = node->next; |
---|
| 1490 | posn = ddHash(cuddT(node), cuddE(node), shift); |
---|
| 1491 | node->next = nodelist[posn]; |
---|
| 1492 | nodelist[posn] = node; |
---|
| 1493 | node = next; |
---|
| 1494 | } |
---|
| 1495 | } |
---|
| 1496 | FREE(oldnodelist); |
---|
| 1497 | |
---|
| 1498 | table->memused += (slots - oldslots) * sizeof(DdNode *); |
---|
| 1499 | table->slots += slots - oldslots; |
---|
| 1500 | table->minDead = (unsigned) (table->gcFrac * (double) table->slots); |
---|
| 1501 | table->cacheSlack = (int) ddMin(table->maxCacheHard, |
---|
| 1502 | DD_MAX_CACHE_TO_SLOTS_RATIO*table->slots) - |
---|
| 1503 | 2 * (int) table->cacheSlots; |
---|
| 1504 | } |
---|
| 1505 | /* We don't look at the constant subtable, because it is not |
---|
| 1506 | ** affected by reordering. |
---|
| 1507 | */ |
---|
| 1508 | |
---|
| 1509 | return(1); |
---|
| 1510 | |
---|
| 1511 | } /* end of zddReorderPostprocess */ |
---|
| 1512 | |
---|
| 1513 | |
---|
| 1514 | /**Function******************************************************************** |
---|
| 1515 | |
---|
| 1516 | Synopsis [Reorders ZDD variables according to a given permutation.] |
---|
| 1517 | |
---|
| 1518 | Description [Reorders ZDD variables according to a given permutation. |
---|
| 1519 | The i-th permutation array contains the index of the variable that |
---|
| 1520 | should be brought to the i-th level. zddShuffle assumes that no |
---|
| 1521 | dead nodes are present. The reordering is achieved by a series of |
---|
| 1522 | upward sifts. Returns 1 if successful; 0 otherwise.] |
---|
| 1523 | |
---|
| 1524 | SideEffects [None] |
---|
| 1525 | |
---|
| 1526 | SeeAlso [] |
---|
| 1527 | |
---|
| 1528 | ******************************************************************************/ |
---|
| 1529 | static int |
---|
| 1530 | zddShuffle( |
---|
| 1531 | DdManager * table, |
---|
| 1532 | int * permutation) |
---|
| 1533 | { |
---|
| 1534 | int index; |
---|
| 1535 | int level; |
---|
| 1536 | int position; |
---|
| 1537 | int numvars; |
---|
| 1538 | int result; |
---|
| 1539 | #ifdef DD_STATS |
---|
| 1540 | long localTime; |
---|
| 1541 | int initialSize; |
---|
| 1542 | int finalSize; |
---|
| 1543 | int previousSize; |
---|
| 1544 | #endif |
---|
| 1545 | |
---|
| 1546 | zddTotalNumberSwapping = 0; |
---|
| 1547 | #ifdef DD_STATS |
---|
| 1548 | localTime = util_cpu_time(); |
---|
| 1549 | initialSize = table->keysZ; |
---|
| 1550 | (void) fprintf(table->out,"#:I_SHUFFLE %8d: initial size\n", |
---|
| 1551 | initialSize); |
---|
| 1552 | #endif |
---|
| 1553 | |
---|
| 1554 | numvars = table->sizeZ; |
---|
| 1555 | |
---|
| 1556 | for (level = 0; level < numvars; level++) { |
---|
| 1557 | index = permutation[level]; |
---|
| 1558 | position = table->permZ[index]; |
---|
| 1559 | #ifdef DD_STATS |
---|
| 1560 | previousSize = table->keysZ; |
---|
| 1561 | #endif |
---|
| 1562 | result = zddSiftUp(table,position,level); |
---|
| 1563 | if (!result) return(0); |
---|
| 1564 | #ifdef DD_STATS |
---|
| 1565 | if (table->keysZ < (unsigned) previousSize) { |
---|
| 1566 | (void) fprintf(table->out,"-"); |
---|
| 1567 | } else if (table->keysZ > (unsigned) previousSize) { |
---|
| 1568 | (void) fprintf(table->out,"+"); /* should never happen */ |
---|
| 1569 | } else { |
---|
| 1570 | (void) fprintf(table->out,"="); |
---|
| 1571 | } |
---|
| 1572 | fflush(table->out); |
---|
| 1573 | #endif |
---|
| 1574 | } |
---|
| 1575 | |
---|
| 1576 | #ifdef DD_STATS |
---|
| 1577 | (void) fprintf(table->out,"\n"); |
---|
| 1578 | finalSize = table->keysZ; |
---|
| 1579 | (void) fprintf(table->out,"#:F_SHUFFLE %8d: final size\n",finalSize); |
---|
| 1580 | (void) fprintf(table->out,"#:T_SHUFFLE %8g: total time (sec)\n", |
---|
| 1581 | ((double)(util_cpu_time() - localTime)/1000.0)); |
---|
| 1582 | (void) fprintf(table->out,"#:N_SHUFFLE %8d: total swaps\n", |
---|
| 1583 | zddTotalNumberSwapping); |
---|
| 1584 | #endif |
---|
| 1585 | |
---|
| 1586 | return(1); |
---|
| 1587 | |
---|
| 1588 | } /* end of zddShuffle */ |
---|
| 1589 | |
---|
| 1590 | |
---|
| 1591 | /**Function******************************************************************** |
---|
| 1592 | |
---|
| 1593 | Synopsis [Moves one ZDD variable up.] |
---|
| 1594 | |
---|
| 1595 | Description [Takes a ZDD variable from position x and sifts it up to |
---|
| 1596 | position xLow; xLow should be less than or equal to x. |
---|
| 1597 | Returns 1 if successful; 0 otherwise] |
---|
| 1598 | |
---|
| 1599 | SideEffects [None] |
---|
| 1600 | |
---|
| 1601 | SeeAlso [] |
---|
| 1602 | |
---|
| 1603 | ******************************************************************************/ |
---|
| 1604 | static int |
---|
| 1605 | zddSiftUp( |
---|
| 1606 | DdManager * table, |
---|
| 1607 | int x, |
---|
| 1608 | int xLow) |
---|
| 1609 | { |
---|
| 1610 | int y; |
---|
| 1611 | int size; |
---|
| 1612 | |
---|
| 1613 | y = cuddZddNextLow(table,x); |
---|
| 1614 | while (y >= xLow) { |
---|
| 1615 | size = cuddZddSwapInPlace(table,y,x); |
---|
| 1616 | if (size == 0) { |
---|
| 1617 | return(0); |
---|
| 1618 | } |
---|
| 1619 | x = y; |
---|
| 1620 | y = cuddZddNextLow(table,x); |
---|
| 1621 | } |
---|
| 1622 | return(1); |
---|
| 1623 | |
---|
| 1624 | } /* end of zddSiftUp */ |
---|
| 1625 | |
---|
| 1626 | |
---|
| 1627 | /**Function******************************************************************** |
---|
| 1628 | |
---|
| 1629 | Synopsis [Fixes the ZDD variable group tree after a shuffle.] |
---|
| 1630 | |
---|
| 1631 | Description [Fixes the ZDD variable group tree after a |
---|
| 1632 | shuffle. Assumes that the order of the variables in a terminal node |
---|
| 1633 | has not been changed.] |
---|
| 1634 | |
---|
| 1635 | SideEffects [Changes the ZDD variable group tree.] |
---|
| 1636 | |
---|
| 1637 | SeeAlso [] |
---|
| 1638 | |
---|
| 1639 | ******************************************************************************/ |
---|
| 1640 | static void |
---|
| 1641 | zddFixTree( |
---|
| 1642 | DdManager * table, |
---|
| 1643 | MtrNode * treenode) |
---|
| 1644 | { |
---|
| 1645 | if (treenode == NULL) return; |
---|
| 1646 | treenode->low = ((int) treenode->index < table->sizeZ) ? |
---|
| 1647 | table->permZ[treenode->index] : treenode->index; |
---|
| 1648 | if (treenode->child != NULL) { |
---|
| 1649 | zddFixTree(table, treenode->child); |
---|
| 1650 | } |
---|
| 1651 | if (treenode->younger != NULL) |
---|
| 1652 | zddFixTree(table, treenode->younger); |
---|
| 1653 | if (treenode->parent != NULL && treenode->low < treenode->parent->low) { |
---|
| 1654 | treenode->parent->low = treenode->low; |
---|
| 1655 | treenode->parent->index = treenode->index; |
---|
| 1656 | } |
---|
| 1657 | return; |
---|
| 1658 | |
---|
| 1659 | } /* end of zddFixTree */ |
---|
| 1660 | |
---|