1 /**CFile*********************************************************************** 2 3 FileName [cuddZddLin.c] 4 5 PackageName [cudd] 6 7 Synopsis [Procedures for dynamic variable ordering of ZDDs.] 8 9 Description [Internal procedures included in this module: 10 <ul> 11 <li> cuddZddLinearSifting() 12 </ul> 13 Static procedures included in this module: 14 <ul> 15 <li> cuddZddLinearInPlace() 16 <li> cuddZddLinerAux() 17 <li> cuddZddLinearUp() 18 <li> cuddZddLinearDown() 19 <li> cuddZddLinearBackward() 20 <li> cuddZddUndoMoves() 21 </ul> 22 ] 23 24 SeeAlso [cuddLinear.c cuddZddReord.c] 25 26 Author [Fabio Somenzi] 27 28 Copyright [Copyright (c) 1995-2012, Regents of the University of Colorado 29 30 All rights reserved. 31 32 Redistribution and use in source and binary forms, with or without 33 modification, are permitted provided that the following conditions 34 are met: 35 36 Redistributions of source code must retain the above copyright 37 notice, this list of conditions and the following disclaimer. 38 39 Redistributions in binary form must reproduce the above copyright 40 notice, this list of conditions and the following disclaimer in the 41 documentation and/or other materials provided with the distribution. 42 43 Neither the name of the University of Colorado nor the names of its 44 contributors may be used to endorse or promote products derived from 45 this software without specific prior written permission. 46 47 THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS 48 "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT 49 LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS 50 FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE 51 COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, 52 INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, 53 BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; 54 LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER 55 CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT 56 LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN 57 ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE 58 POSSIBILITY OF SUCH DAMAGE.] 59 60 ******************************************************************************/ 61 62 #include "util.h" 63 #include "cuddInt.h" 64 65 /*---------------------------------------------------------------------------*/ 66 /* Constant declarations */ 67 /*---------------------------------------------------------------------------*/ 68 69 #define CUDD_SWAP_MOVE 0 70 #define CUDD_LINEAR_TRANSFORM_MOVE 1 71 #define CUDD_INVERSE_TRANSFORM_MOVE 2 72 73 /*---------------------------------------------------------------------------*/ 74 /* Stucture declarations */ 75 /*---------------------------------------------------------------------------*/ 76 77 78 /*---------------------------------------------------------------------------*/ 79 /* Type declarations */ 80 /*---------------------------------------------------------------------------*/ 81 82 83 /*---------------------------------------------------------------------------*/ 84 /* Variable declarations */ 85 /*---------------------------------------------------------------------------*/ 86 87 #ifndef lint 88 static char rcsid[] DD_UNUSED = "$Id: cuddZddLin.c,v 1.16 2012/02/05 01:07:19 fabio Exp $"; 89 #endif 90 91 extern int *zdd_entry; 92 extern int zddTotalNumberSwapping; 93 static int zddTotalNumberLinearTr; 94 static DdNode *empty; 95 96 97 /*---------------------------------------------------------------------------*/ 98 /* Macro declarations */ 99 /*---------------------------------------------------------------------------*/ 100 101 102 /**AutomaticStart*************************************************************/ 103 104 /*---------------------------------------------------------------------------*/ 105 /* Static function prototypes */ 106 /*---------------------------------------------------------------------------*/ 107 108 static int cuddZddLinearInPlace (DdManager * table, int x, int y); 109 static int cuddZddLinearAux (DdManager *table, int x, int xLow, int xHigh); 110 static Move * cuddZddLinearUp (DdManager *table, int y, int xLow, Move *prevMoves); 111 static Move * cuddZddLinearDown (DdManager *table, int x, int xHigh, Move *prevMoves); 112 static int cuddZddLinearBackward (DdManager *table, int size, Move *moves); 113 static Move* cuddZddUndoMoves (DdManager *table, Move *moves); 114 115 /**AutomaticEnd***************************************************************/ 116 117 118 /*---------------------------------------------------------------------------*/ 119 /* Definition of exported functions */ 120 /*---------------------------------------------------------------------------*/ 121 122 123 /*---------------------------------------------------------------------------*/ 124 /* Definition of internal functions */ 125 /*---------------------------------------------------------------------------*/ 126 127 128 129 130 /**Function******************************************************************** 131 Cudd_zddIsop(DdManager * dd,DdNode * L,DdNode * U,DdNode ** zdd_I)132 Synopsis [Implementation of the linear sifting algorithm for ZDDs.] 133 134 Description [Implementation of the linear sifting algorithm for ZDDs. 135 Assumes that no dead nodes are present. 136 <ol> 137 <li> Order all the variables according to the number of entries 138 in each unique table. 139 <li> Sift the variable up and down and applies the XOR transformation, 140 remembering each time the total size of the DD heap. 141 <li> Select the best permutation. 142 <li> Repeat 3 and 4 for all variables. 143 </ol> 144 Returns 1 if successful; 0 otherwise.] 145 146 SideEffects [None] 147 148 SeeAlso [] 149 150 ******************************************************************************/ 151 int 152 cuddZddLinearSifting( 153 DdManager * table, 154 int lower, 155 int upper) 156 { 157 int i; 158 int *var; 159 int size; 160 int x; 161 int result; 162 #ifdef DD_STATS 163 int previousSize; 164 #endif 165 166 size = table->sizeZ; 167 empty = table->zero; 168 169 /* Find order in which to sift variables. */ 170 var = NULL; 171 zdd_entry = ALLOC(int, size); 172 if (zdd_entry == NULL) { 173 table->errorCode = CUDD_MEMORY_OUT; 174 goto cuddZddSiftingOutOfMem; 175 } 176 var = ALLOC(int, size); 177 if (var == NULL) { 178 table->errorCode = CUDD_MEMORY_OUT; 179 goto cuddZddSiftingOutOfMem; 180 } 181 182 for (i = 0; i < size; i++) { 183 x = table->permZ[i]; 184 zdd_entry[i] = table->subtableZ[x].keys; 185 var[i] = i; 186 } 187 188 qsort((void *)var, size, sizeof(int), (DD_QSFP)cuddZddUniqueCompare); 189 190 /* Now sift. */ 191 for (i = 0; i < ddMin(table->siftMaxVar, size); i++) { 192 if (zddTotalNumberSwapping >= table->siftMaxSwap) 193 break; 194 if (util_cpu_time() - table->startTime > table->timeLimit) { 195 table->autoDynZ = 0; /* prevent further reordering */ 196 break; 197 } 198 x = table->permZ[var[i]]; 199 if (x < lower || x > upper) continue; 200 #ifdef DD_STATS 201 previousSize = table->keysZ; 202 #endif 203 result = cuddZddLinearAux(table, x, lower, upper); 204 if (!result) 205 goto cuddZddSiftingOutOfMem; 206 #ifdef DD_STATS 207 if (table->keysZ < (unsigned) previousSize) { 208 (void) fprintf(table->out,"-"); 209 } else if (table->keysZ > (unsigned) previousSize) { 210 (void) fprintf(table->out,"+"); /* should never happen */ 211 (void) fprintf(table->out,"\nSize increased from %d to %d while sifting variable %d\n", previousSize, table->keysZ , var[i]); 212 } else { 213 (void) fprintf(table->out,"="); 214 } 215 fflush(table->out); 216 #endif 217 } 218 219 FREE(var); 220 FREE(zdd_entry); 221 222 return(1); 223 224 cuddZddSiftingOutOfMem: 225 226 if (zdd_entry != NULL) FREE(zdd_entry); 227 if (var != NULL) FREE(var); 228 229 return(0); 230 231 } /* end of cuddZddLinearSifting */ 232 233 234 /*---------------------------------------------------------------------------*/ 235 /* Definition of static functions */ 236 /*---------------------------------------------------------------------------*/ 237 238 239 /**Function******************************************************************** 240 241 Synopsis [Linearly combines two adjacent variables.] 242 243 Description [Linearly combines two adjacent variables. It assumes 244 that no dead nodes are present on entry to this procedure. The 245 procedure then guarantees that no dead nodes will be present when it 246 terminates. cuddZddLinearInPlace assumes that x < y. Returns the 247 number of keys in the table if successful; 0 otherwise.] 248 249 SideEffects [None] 250 251 SeeAlso [cuddZddSwapInPlace cuddLinearInPlace] 252 253 ******************************************************************************/ 254 static int 255 cuddZddLinearInPlace( 256 DdManager * table, 257 int x, 258 int y) 259 { 260 DdNodePtr *xlist, *ylist; 261 int xindex, yindex; 262 int xslots, yslots; 263 int xshift, yshift; 264 int oldxkeys, oldykeys; 265 int newxkeys, newykeys; 266 int i; 267 int posn; 268 DdNode *f, *f1, *f0, *f11, *f10, *f01, *f00; 269 DdNode *newf1, *newf0, *g, *next, *previous; 270 DdNode *special; 271 272 #ifdef DD_DEBUG 273 assert(x < y); 274 assert(cuddZddNextHigh(table,x) == y); 275 assert(table->subtableZ[x].keys != 0); 276 assert(table->subtableZ[y].keys != 0); 277 assert(table->subtableZ[x].dead == 0); 278 assert(table->subtableZ[y].dead == 0); 279 #endif 280 281 zddTotalNumberLinearTr++; 282 283 /* Get parameters of x subtable. */ 284 xindex = table->invpermZ[x]; 285 xlist = table->subtableZ[x].nodelist; 286 oldxkeys = table->subtableZ[x].keys; 287 xslots = table->subtableZ[x].slots; 288 xshift = table->subtableZ[x].shift; 289 newxkeys = 0; 290 291 /* Get parameters of y subtable. */ 292 yindex = table->invpermZ[y]; 293 ylist = table->subtableZ[y].nodelist; 294 oldykeys = table->subtableZ[y].keys; 295 yslots = table->subtableZ[y].slots; 296 yshift = table->subtableZ[y].shift; 297 newykeys = oldykeys; 298 299 /* The nodes in the x layer are put in two chains. The chain 300 ** pointed by g holds the normal nodes. When re-expressed they stay 301 ** in the x list. The chain pointed by special holds the elements 302 ** that will move to the y list. 303 */ 304 g = special = NULL; 305 for (i = 0; i < xslots; i++) { 306 f = xlist[i]; 307 if (f == NULL) continue; 308 xlist[i] = NULL; 309 while (f != NULL) { 310 next = f->next; 311 f1 = cuddT(f); 312 /* if (f1->index == yindex) */ cuddSatDec(f1->ref); 313 f0 = cuddE(f); 314 /* if (f0->index == yindex) */ cuddSatDec(f0->ref); 315 if ((int) f1->index == yindex && cuddE(f1) == empty && 316 (int) f0->index != yindex) { 317 f->next = special; 318 special = f; 319 } else { 320 f->next = g; 321 g = f; 322 } 323 f = next; 324 } /* while there are elements in the collision chain */ 325 } /* for each slot of the x subtable */ 326 327 /* Mark y nodes with pointers from above x. We mark them by 328 ** changing their index to x. 329 */ 330 for (i = 0; i < yslots; i++) { 331 f = ylist[i]; 332 while (f != NULL) { 333 if (f->ref != 0) { 334 f->index = xindex; 335 } 336 f = f->next; 337 } /* while there are elements in the collision chain */ 338 } /* for each slot of the y subtable */ 339 340 /* Move special nodes to the y list. */ 341 f = special; 342 while (f != NULL) { 343 next = f->next; 344 f1 = cuddT(f); 345 f11 = cuddT(f1); 346 cuddT(f) = f11; 347 cuddSatInc(f11->ref); 348 f0 = cuddE(f); 349 cuddSatInc(f0->ref); 350 f->index = yindex; 351 /* Insert at the beginning of the list so that it will be 352 ** found first if there is a duplicate. The duplicate will 353 ** eventually be moved or garbage collected. No node 354 ** re-expression will add a pointer to it. 355 */ 356 posn = ddHash(f11, f0, yshift); 357 f->next = ylist[posn]; 358 ylist[posn] = f; 359 newykeys++; 360 f = next; 361 } 362 363 /* Take care of the remaining x nodes that must be re-expressed. 364 ** They form a linked list pointed by g. 365 */ 366 f = g; 367 while (f != NULL) { 368 #ifdef DD_COUNT 369 table->swapSteps++; 370 #endif 371 next = f->next; 372 /* Find f1, f0, f11, f10, f01, f00. */ 373 f1 = cuddT(f); 374 if ((int) f1->index == yindex || (int) f1->index == xindex) { 375 f11 = cuddT(f1); f10 = cuddE(f1); 376 } else { 377 f11 = empty; f10 = f1; 378 } 379 f0 = cuddE(f); 380 if ((int) f0->index == yindex || (int) f0->index == xindex) { 381 f01 = cuddT(f0); f00 = cuddE(f0); 382 } else { 383 f01 = empty; f00 = f0; 384 } 385 /* Create the new T child. */ 386 if (f01 == empty) { 387 newf1 = f10; 388 cuddSatInc(newf1->ref); 389 } else { 390 /* Check ylist for triple (yindex, f01, f10). */ 391 posn = ddHash(f01, f10, yshift); 392 /* For each element newf1 in collision list ylist[posn]. */ 393 newf1 = ylist[posn]; 394 /* Search the collision chain skipping the marked nodes. */ 395 while (newf1 != NULL) { 396 if (cuddT(newf1) == f01 && cuddE(newf1) == f10 && 397 (int) newf1->index == yindex) { 398 cuddSatInc(newf1->ref); 399 break; /* match */ 400 } 401 newf1 = newf1->next; 402 } /* while newf1 */ 403 if (newf1 == NULL) { /* no match */ 404 newf1 = cuddDynamicAllocNode(table); 405 if (newf1 == NULL) 406 goto zddSwapOutOfMem; 407 newf1->index = yindex; newf1->ref = 1; 408 cuddT(newf1) = f01; 409 cuddE(newf1) = f10; 410 /* Insert newf1 in the collision list ylist[pos]; 411 ** increase the ref counts of f01 and f10 412 */ 413 newykeys++; 414 newf1->next = ylist[posn]; 415 ylist[posn] = newf1; 416 cuddSatInc(f01->ref); 417 cuddSatInc(f10->ref); 418 } 419 } 420 cuddT(f) = newf1; 421 422 /* Do the same for f0. */ 423 /* Create the new E child. */ 424 if (f11 == empty) { 425 newf0 = f00; 426 cuddSatInc(newf0->ref); 427 } else { 428 /* Check ylist for triple (yindex, f11, f00). */ 429 posn = ddHash(f11, f00, yshift); 430 /* For each element newf0 in collision list ylist[posn]. */ 431 newf0 = ylist[posn]; 432 while (newf0 != NULL) { 433 if (cuddT(newf0) == f11 && cuddE(newf0) == f00 && 434 (int) newf0->index == yindex) { 435 cuddSatInc(newf0->ref); 436 break; /* match */ 437 } 438 newf0 = newf0->next; 439 } /* while newf0 */ 440 if (newf0 == NULL) { /* no match */ 441 newf0 = cuddDynamicAllocNode(table); 442 if (newf0 == NULL) 443 goto zddSwapOutOfMem; 444 newf0->index = yindex; newf0->ref = 1; 445 cuddT(newf0) = f11; cuddE(newf0) = f00; 446 /* Insert newf0 in the collision list ylist[posn]; 447 ** increase the ref counts of f11 and f00. 448 */ 449 newykeys++; 450 newf0->next = ylist[posn]; 451 ylist[posn] = newf0; 452 cuddSatInc(f11->ref); 453 cuddSatInc(f00->ref); 454 } 455 } 456 cuddE(f) = newf0; 457 458 /* Re-insert the modified f in xlist. 459 ** The modified f does not already exists in xlist. 460 ** (Because of the uniqueness of the cofactors.) 461 */ 462 posn = ddHash(newf1, newf0, xshift); 463 newxkeys++; 464 f->next = xlist[posn]; 465 xlist[posn] = f; 466 f = next; 467 } /* while f != NULL */ 468 469 /* GC the y layer and move the marked nodes to the x list. */ 470 471 /* For each node f in ylist. */ 472 for (i = 0; i < yslots; i++) { 473 previous = NULL; 474 f = ylist[i]; 475 while (f != NULL) { 476 next = f->next; 477 if (f->ref == 0) { 478 cuddSatDec(cuddT(f)->ref); 479 cuddSatDec(cuddE(f)->ref); 480 cuddDeallocNode(table, f); 481 newykeys--; 482 if (previous == NULL) 483 ylist[i] = next; 484 else 485 previous->next = next; 486 } else if ((int) f->index == xindex) { /* move marked node */ 487 if (previous == NULL) 488 ylist[i] = next; 489 else 490 previous->next = next; 491 f1 = cuddT(f); 492 cuddSatDec(f1->ref); 493 /* Check ylist for triple (yindex, f1, empty). */ 494 posn = ddHash(f1, empty, yshift); 495 /* For each element newf1 in collision list ylist[posn]. */ 496 newf1 = ylist[posn]; 497 while (newf1 != NULL) { 498 if (cuddT(newf1) == f1 && cuddE(newf1) == empty && 499 (int) newf1->index == yindex) { 500 cuddSatInc(newf1->ref); 501 break; /* match */ 502 } 503 newf1 = newf1->next; 504 } /* while newf1 */ 505 if (newf1 == NULL) { /* no match */ 506 newf1 = cuddDynamicAllocNode(table); 507 if (newf1 == NULL) 508 goto zddSwapOutOfMem; 509 newf1->index = yindex; newf1->ref = 1; 510 cuddT(newf1) = f1; cuddE(newf1) = empty; 511 /* Insert newf1 in the collision list ylist[posn]; 512 ** increase the ref counts of f1 and empty. 513 */ 514 newykeys++; 515 newf1->next = ylist[posn]; 516 ylist[posn] = newf1; 517 if (posn == i && previous == NULL) 518 previous = newf1; 519 cuddSatInc(f1->ref); 520 cuddSatInc(empty->ref); 521 } 522 cuddT(f) = newf1; 523 f0 = cuddE(f); 524 /* Insert f in x list. */ 525 posn = ddHash(newf1, f0, xshift); 526 newxkeys++; 527 newykeys--; 528 f->next = xlist[posn]; 529 xlist[posn] = f; 530 } else { 531 previous = f; 532 } 533 f = next; 534 } /* while f */ 535 } /* for i */ 536 537 /* Set the appropriate fields in table. */ 538 table->subtableZ[x].keys = newxkeys; 539 table->subtableZ[y].keys = newykeys; 540 541 table->keysZ += newxkeys + newykeys - oldxkeys - oldykeys; 542 543 /* Update univ section; univ[x] remains the same. */ 544 table->univ[y] = cuddT(table->univ[x]); 545 546 #if 0 547 (void) fprintf(table->out,"x = %d y = %d\n", x, y); 548 (void) Cudd_DebugCheck(table); 549 (void) Cudd_CheckKeys(table); 550 #endif 551 552 return (table->keysZ); 553 554 zddSwapOutOfMem: 555 (void) fprintf(table->err, "Error: cuddZddSwapInPlace out of memory\n"); 556 557 return (0); 558 559 } /* end of cuddZddLinearInPlace */ 560 561 562 /**Function******************************************************************** 563 564 Synopsis [Given xLow <= x <= xHigh moves x up and down between the 565 boundaries.] 566 567 Description [Given xLow <= x <= xHigh moves x up and down between the 568 boundaries. Finds the best position and does the required changes. 569 Returns 1 if successful; 0 otherwise.] 570 571 SideEffects [None] cuddBddIsop(DdManager * dd,DdNode * L,DdNode * U)572 573 SeeAlso [] 574 575 ******************************************************************************/ 576 static int 577 cuddZddLinearAux( 578 DdManager * table, 579 int x, 580 int xLow, 581 int xHigh) 582 { 583 Move *move; 584 Move *moveUp; /* list of up move */ 585 Move *moveDown; /* list of down move */ 586 587 int initial_size; 588 int result; 589 590 initial_size = table->keysZ; 591 592 #ifdef DD_DEBUG 593 assert(table->subtableZ[x].keys > 0); 594 #endif 595 596 moveDown = NULL; 597 moveUp = NULL; 598 599 if (x == xLow) { 600 moveDown = cuddZddLinearDown(table, x, xHigh, NULL); 601 /* At this point x --> xHigh. */ 602 if (moveDown == (Move *) CUDD_OUT_OF_MEM) 603 goto cuddZddLinearAuxOutOfMem; 604 /* Move backward and stop at best position. */ 605 result = cuddZddLinearBackward(table, initial_size, moveDown); 606 if (!result) 607 goto cuddZddLinearAuxOutOfMem; 608 609 } else if (x == xHigh) { 610 moveUp = cuddZddLinearUp(table, x, xLow, NULL); 611 /* At this point x --> xLow. */ 612 if (moveUp == (Move *) CUDD_OUT_OF_MEM) 613 goto cuddZddLinearAuxOutOfMem; 614 /* Move backward and stop at best position. */ 615 result = cuddZddLinearBackward(table, initial_size, moveUp); 616 if (!result) 617 goto cuddZddLinearAuxOutOfMem; 618 619 } else if ((x - xLow) > (xHigh - x)) { /* must go down first: shorter */ 620 moveDown = cuddZddLinearDown(table, x, xHigh, NULL); 621 /* At this point x --> xHigh. */ 622 if (moveDown == (Move *) CUDD_OUT_OF_MEM) 623 goto cuddZddLinearAuxOutOfMem; 624 moveUp = cuddZddUndoMoves(table,moveDown); 625 #ifdef DD_DEBUG 626 assert(moveUp == NULL || moveUp->x == x); 627 #endif 628 moveUp = cuddZddLinearUp(table, x, xLow, moveUp); 629 if (moveUp == (Move *) CUDD_OUT_OF_MEM) 630 goto cuddZddLinearAuxOutOfMem; 631 /* Move backward and stop at best position. */ 632 result = cuddZddLinearBackward(table, initial_size, moveUp); 633 if (!result) 634 goto cuddZddLinearAuxOutOfMem; 635 636 } else { 637 moveUp = cuddZddLinearUp(table, x, xLow, NULL); 638 /* At this point x --> xHigh. */ 639 if (moveUp == (Move *) CUDD_OUT_OF_MEM) 640 goto cuddZddLinearAuxOutOfMem; 641 /* Then move up. */ 642 moveDown = cuddZddUndoMoves(table,moveUp); 643 #ifdef DD_DEBUG 644 assert(moveDown == NULL || moveDown->y == x); 645 #endif 646 moveDown = cuddZddLinearDown(table, x, xHigh, moveDown); 647 if (moveDown == (Move *) CUDD_OUT_OF_MEM) 648 goto cuddZddLinearAuxOutOfMem; 649 /* Move backward and stop at best position. */ 650 result = cuddZddLinearBackward(table, initial_size, moveDown); 651 if (!result) 652 goto cuddZddLinearAuxOutOfMem; 653 } 654 655 while (moveDown != NULL) { 656 move = moveDown->next; 657 cuddDeallocMove(table, moveDown); 658 moveDown = move; 659 } 660 while (moveUp != NULL) { 661 move = moveUp->next; 662 cuddDeallocMove(table, moveUp); 663 moveUp = move; 664 } 665 666 return(1); 667 668 cuddZddLinearAuxOutOfMem: 669 if (moveDown != (Move *) CUDD_OUT_OF_MEM) { 670 while (moveDown != NULL) { 671 move = moveDown->next; 672 cuddDeallocMove(table, moveDown); 673 moveDown = move; 674 } 675 } 676 if (moveUp != (Move *) CUDD_OUT_OF_MEM) { 677 while (moveUp != NULL) { 678 move = moveUp->next; 679 cuddDeallocMove(table, moveUp); 680 moveUp = move; 681 } 682 } 683 684 return(0); 685 686 } /* end of cuddZddLinearAux */ 687 688 689 /**Function******************************************************************** 690 691 Synopsis [Sifts a variable up applying the XOR transformation.] 692 693 Description [Sifts a variable up applying the XOR 694 transformation. Moves y up until either it reaches the bound (xLow) 695 or the size of the ZDD heap increases too much. Returns the set of 696 moves in case of success; NULL if memory is full.] 697 698 SideEffects [None] 699 700 SeeAlso [] 701 702 ******************************************************************************/ 703 static Move * 704 cuddZddLinearUp( 705 DdManager * table, 706 int y, 707 int xLow, 708 Move * prevMoves) 709 { 710 Move *moves; 711 Move *move; 712 int x; 713 int size, newsize; 714 int limitSize; 715 716 moves = prevMoves; 717 limitSize = table->keysZ; 718 719 x = cuddZddNextLow(table, y); 720 while (x >= xLow) { 721 size = cuddZddSwapInPlace(table, x, y); 722 if (size == 0) 723 goto cuddZddLinearUpOutOfMem; 724 newsize = cuddZddLinearInPlace(table, x, y); 725 if (newsize == 0) 726 goto cuddZddLinearUpOutOfMem; 727 move = (Move *) cuddDynamicAllocNode(table); 728 if (move == NULL) 729 goto cuddZddLinearUpOutOfMem; 730 move->x = x; 731 move->y = y; 732 move->next = moves; 733 moves = move; 734 move->flags = CUDD_SWAP_MOVE; 735 if (newsize > size) { 736 /* Undo transformation. The transformation we apply is 737 ** its own inverse. Hence, we just apply the transformation 738 ** again. 739 */ 740 newsize = cuddZddLinearInPlace(table,x,y); 741 if (newsize == 0) goto cuddZddLinearUpOutOfMem; 742 #ifdef DD_DEBUG 743 if (newsize != size) { 744 (void) fprintf(table->err,"Change in size after identity transformation! From %d to %d\n",size,newsize); 745 } 746 #endif 747 } else { 748 size = newsize; 749 move->flags = CUDD_LINEAR_TRANSFORM_MOVE; 750 } 751 move->size = size; 752 753 if ((double)size > (double)limitSize * table->maxGrowth) 754 break; 755 if (size < limitSize) 756 limitSize = size; 757 758 y = x; 759 x = cuddZddNextLow(table, y); 760 } 761 return(moves); 762 763 cuddZddLinearUpOutOfMem: 764 while (moves != NULL) { 765 move = moves->next; 766 cuddDeallocMove(table, moves); 767 moves = move; 768 } 769 return((Move *) CUDD_OUT_OF_MEM); 770 771 } /* end of cuddZddLinearUp */ 772 773 774 /**Function******************************************************************** 775 776 Synopsis [Sifts a variable down and applies the XOR transformation.] 777 778 Description [Sifts a variable down. Moves x down until either it 779 reaches the bound (xHigh) or the size of the ZDD heap increases too 780 much. Returns the set of moves in case of success; NULL if memory is 781 full.] 782 783 SideEffects [None] 784 785 SeeAlso [] 786 787 ******************************************************************************/ 788 static Move * 789 cuddZddLinearDown( 790 DdManager * table, 791 int x, 792 int xHigh, 793 Move * prevMoves) 794 { 795 Move *moves; 796 Move *move; cuddMakeBddFromZddCover(DdManager * dd,DdNode * node)797 int y; 798 int size, newsize; 799 int limitSize; 800 801 moves = prevMoves; 802 limitSize = table->keysZ; 803 804 y = cuddZddNextHigh(table, x); 805 while (y <= xHigh) { 806 size = cuddZddSwapInPlace(table, x, y); 807 if (size == 0) 808 goto cuddZddLinearDownOutOfMem; 809 newsize = cuddZddLinearInPlace(table, x, y); 810 if (newsize == 0) 811 goto cuddZddLinearDownOutOfMem; 812 move = (Move *) cuddDynamicAllocNode(table); 813 if (move == NULL) 814 goto cuddZddLinearDownOutOfMem; 815 move->x = x; 816 move->y = y; 817 move->next = moves; 818 moves = move; 819 move->flags = CUDD_SWAP_MOVE; 820 if (newsize > size) { 821 /* Undo transformation. The transformation we apply is 822 ** its own inverse. Hence, we just apply the transformation 823 ** again. 824 */ 825 newsize = cuddZddLinearInPlace(table,x,y); 826 if (newsize == 0) goto cuddZddLinearDownOutOfMem; 827 if (newsize != size) { 828 (void) fprintf(table->err,"Change in size after identity transformation! From %d to %d\n",size,newsize); 829 } 830 } else { 831 size = newsize; 832 move->flags = CUDD_LINEAR_TRANSFORM_MOVE; 833 } 834 move->size = size; 835 836 if ((double)size > (double)limitSize * table->maxGrowth) 837 break; 838 if (size < limitSize) 839 limitSize = size; 840 841 x = y; 842 y = cuddZddNextHigh(table, x); 843 } 844 return(moves); 845 846 cuddZddLinearDownOutOfMem: 847 while (moves != NULL) { 848 move = moves->next; 849 cuddDeallocMove(table, moves); 850 moves = move; 851 } 852 return((Move *) CUDD_OUT_OF_MEM); 853 854 } /* end of cuddZddLinearDown */ 855 856 857 /**Function******************************************************************** 858 859 Synopsis [Given a set of moves, returns the ZDD heap to the position 860 giving the minimum size.] 861 862 Description [Given a set of moves, returns the ZDD heap to the 863 position giving the minimum size. In case of ties, returns to the 864 closest position giving the minimum size. Returns 1 in case of 865 success; 0 otherwise.] 866 867 SideEffects [None] 868 869 SeeAlso [] 870 871 ******************************************************************************/ 872 static int 873 cuddZddLinearBackward( 874 DdManager * table, 875 int size, 876 Move * moves) 877 { 878 Move *move; 879 int res; 880 881 /* Find the minimum size among moves. */ 882 for (move = moves; move != NULL; move = move->next) { 883 if (move->size < size) { 884 size = move->size; 885 } 886 } 887 888 for (move = moves; move != NULL; move = move->next) { 889 if (move->size == size) return(1); 890 if (move->flags == CUDD_LINEAR_TRANSFORM_MOVE) { 891 res = cuddZddLinearInPlace(table,(int)move->x,(int)move->y); 892 if (!res) return(0); 893 } 894 res = cuddZddSwapInPlace(table, move->x, move->y); 895 if (!res) 896 return(0); 897 if (move->flags == CUDD_INVERSE_TRANSFORM_MOVE) { 898 res = cuddZddLinearInPlace(table,(int)move->x,(int)move->y); 899 if (!res) return(0); 900 } 901 } 902 903 return(1); 904 905 } /* end of cuddZddLinearBackward */ 906 907 908 /**Function******************************************************************** 909 910 Synopsis [Given a set of moves, returns the ZDD heap to the order 911 in effect before the moves.] 912 913 Description [Given a set of moves, returns the ZDD heap to the 914 order in effect before the moves. Returns 1 in case of success; 915 0 otherwise.] 916 917 SideEffects [None] 918 919 ******************************************************************************/ 920 static Move* 921 cuddZddUndoMoves( 922 DdManager * table, 923 Move * moves) 924 { 925 Move *invmoves = NULL; 926 Move *move; 927 Move *invmove; 928 int size; 929 930 for (move = moves; move != NULL; move = move->next) { 931 invmove = (Move *) cuddDynamicAllocNode(table); 932 if (invmove == NULL) goto cuddZddUndoMovesOutOfMem; 933 invmove->x = move->x; 934 invmove->y = move->y; 935 invmove->next = invmoves; 936 invmoves = invmove; 937 if (move->flags == CUDD_SWAP_MOVE) { 938 invmove->flags = CUDD_SWAP_MOVE; 939 size = cuddZddSwapInPlace(table,(int)move->x,(int)move->y); 940 if (!size) goto cuddZddUndoMovesOutOfMem; 941 } else if (move->flags == CUDD_LINEAR_TRANSFORM_MOVE) { 942 invmove->flags = CUDD_INVERSE_TRANSFORM_MOVE; 943 size = cuddZddLinearInPlace(table,(int)move->x,(int)move->y); 944 if (!size) goto cuddZddUndoMovesOutOfMem; 945 size = cuddZddSwapInPlace(table,(int)move->x,(int)move->y); 946 if (!size) goto cuddZddUndoMovesOutOfMem; 947 } else { /* must be CUDD_INVERSE_TRANSFORM_MOVE */ 948 #ifdef DD_DEBUG 949 (void) fprintf(table->err,"Unforseen event in ddUndoMoves!\n"); 950 #endif 951 invmove->flags = CUDD_LINEAR_TRANSFORM_MOVE; 952 size = cuddZddSwapInPlace(table,(int)move->x,(int)move->y); 953 if (!size) goto cuddZddUndoMovesOutOfMem; 954 size = cuddZddLinearInPlace(table,(int)move->x,(int)move->y); 955 if (!size) goto cuddZddUndoMovesOutOfMem; 956 } 957 invmove->size = size; 958 } 959 960 return(invmoves); 961 962 cuddZddUndoMovesOutOfMem: 963 while (invmoves != NULL) { 964 move = invmoves->next; 965 cuddDeallocMove(table, invmoves); 966 invmoves = move; 967 } 968 return((Move *) CUDD_OUT_OF_MEM); 969 970 } /* end of cuddZddUndoMoves */ 971 972