1/*======================================================================== 2 Copyright (C) 1996-2001 by Jorn Lind-Nielsen 3 All rights reserved 4 5 Permission is hereby granted, without written agreement and without 6 license or royalty fees, to use, reproduce, prepare derivative 7 works, distribute, and display this software and its documentation 8 for any purpose, provided that (1) the above copyright notice and 9 the following two paragraphs appear in all copies of the source code 10 and (2) redistributions, including without limitation binaries, 11 reproduce these notices in the supporting documentation. Substantial 12 modifications to this software may be copyrighted by their authors 13 and need not follow the licensing terms described here, provided 14 that the new terms are clearly indicated in all files where they apply. 15 16 IN NO EVENT SHALL JORN LIND-NIELSEN, OR DISTRIBUTORS OF THIS 17 SOFTWARE BE LIABLE TO ANY PARTY FOR DIRECT, INDIRECT, SPECIAL, 18 INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OF THIS 19 SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE AUTHORS OR ANY OF THE 20 ABOVE PARTIES HAVE BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. 21 22 JORN LIND-NIELSEN SPECIFICALLY DISCLAIM ANY WARRANTIES, INCLUDING, 23 BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND 24 FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS 25 ON AN "AS IS" BASIS, AND THE AUTHORS AND DISTRIBUTORS HAVE NO 26 OBLIGATION TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR 27 MODIFICATIONS. 28========================================================================*/ 29 30/************************************************************************* 31 $Header$ 32 FILE: reorder.c 33 DESCR: BDD reordering functions 34 AUTH: Jorn Lind 35 DATE: (C) january 1998 36*************************************************************************/ 37#include <stdlib.h> 38#include <string.h> 39#include <time.h> 40#include <math.h> 41#include <assert.h> 42#include "kernel.h" 43#include "bddtree.h" 44#include "imatrix.h" 45#include "prime.h" 46 47/* IMPORTANT: 48 * The semantics of the "level" field in the BddNode struct changes during 49 * variable reordering in order to make a fast variable swap possible when 50 * two variables are independent. Instead of refering to the level of the node 51 * it refers to the *variable* !!! 52 */ 53 54 /* Change macros to reflect the above idea */ 55#define VAR(n) (bddnodes[n].level) 56#define VARp(p) (p->level) 57 58 /* Avoid these - they are misleading! */ 59#undef LEVEL 60#undef LEVELp 61 62 63#define __USERESIZE /* FIXME */ 64 65 /* Current auto reord. method and number of automatic reorderings left */ 66static int bddreordermethod; 67static int bddreordertimes; 68 69 /* Flag for disabling reordering temporarily */ 70static int reorderdisabled; 71 72 /* Store for the variable relationships */ 73static BddTree *vartree; 74static int blockid; 75 76 /* Store for the ref.cou. of the external roots */ 77static int *extroots; 78static int extrootsize; 79 80/* Level data */ 81typedef struct _levelData 82{ 83 int start; /* Start of this sub-table (entry in "bddnodes") */ 84 int size; /* Size of this sub-table */ 85 int maxsize; /* Max. allowed size of sub-table */ 86 int nodenum; /* Number of nodes in this level */ 87} levelData; 88 89static levelData *levels; /* Indexed by variable! */ 90 91 /* Interaction matrix */ 92static imatrix *iactmtx; 93 94 /* Reordering information for the user */ 95static int verbose; 96static bddinthandler reorder_handler; 97static bddfilehandler reorder_filehandler; 98static bddsizehandler reorder_nodenum; 99 100 /* Number of live nodes before and after a reordering session */ 101static int usednum_before; 102static int usednum_after; 103 104 /* Kernel variables needed for reordering */ 105extern int bddfreepos; 106extern int bddfreenum; 107extern int bddproduced; 108 109 /* Flag telling us when a node table resize is done */ 110static int resizedInMakenode; 111 112 /* New node hashing function for use with reordering */ 113#define NODEHASH(var,l,h) ((PAIR((l),(h))%levels[var].size)+levels[var].start) 114 115 /* Reordering prototypes */ 116static void blockdown(BddTree *); 117static void addref_rec(int, char *); 118static void reorder_gbc(); 119static void reorder_setLevellookup(void); 120static int reorder_makenode(int, int, int); 121static int reorder_varup(int); 122static int reorder_vardown(int); 123static int reorder_init(void); 124static void reorder_done(void); 125 126#define random(a) (rand() % (a)) 127 128 /* For sorting the blocks according to some specific size value */ 129typedef struct s_sizePair 130{ 131 int val; 132 BddTree *block; 133} sizePair; 134 135 136/************************************************************************* 137 Initialize and shutdown 138*************************************************************************/ 139 140void bdd_reorder_init(void) 141{ 142 reorderdisabled = 0; 143 vartree = NULL; 144 145 bdd_clrvarblocks(); 146 bdd_reorder_hook(bdd_default_reohandler); 147 bdd_reorder_verbose(0); 148 bdd_autoreorder_times(BDD_REORDER_NONE, 0); 149 reorder_nodenum = bdd_getnodenum; 150 usednum_before = usednum_after = 0; 151 blockid = 0; 152} 153 154 155void bdd_reorder_done(void) 156{ 157 bddtree_del(vartree); 158 bdd_operator_reset(); 159 vartree = NULL; 160} 161 162 163/************************************************************************* 164 Reordering heuristics 165*************************************************************************/ 166 167/*=== Reorder using a sliding window of size 2 =========================*/ 168 169static BddTree *reorder_win2(BddTree *t) 170{ 171 BddTree *this=t, *first=t; 172 173 if (t == NULL) 174 return t; 175 176 if (verbose > 1) 177 printf("Win2 start: %d nodes\n", reorder_nodenum()); 178 fflush(stdout); 179 180 while (this->next != NULL) 181 { 182 int best = reorder_nodenum(); 183 blockdown(this); 184 185 if (best < reorder_nodenum()) 186 { 187 blockdown(this->prev); 188 this = this->next; 189 } 190 else 191 if (first == this) 192 first = this->prev; 193 194 if (verbose > 1) 195 { 196 printf("."); 197 fflush(stdout); 198 } 199 } 200 201 if (verbose > 1) 202 printf("\nWin2 end: %d nodes\n", reorder_nodenum()); 203 fflush(stdout); 204 205 return first; 206} 207 208 209static BddTree *reorder_win2ite(BddTree *t) 210{ 211 BddTree *this, *first=t; 212 int lastsize; 213 int c=1; 214 215 if (t == NULL) 216 return t; 217 218 if (verbose > 1) 219 printf("Win2ite start: %d nodes\n", reorder_nodenum()); 220 221 do 222 { 223 lastsize = reorder_nodenum(); 224 225 this = t; 226 while (this->next != NULL) 227 { 228 int best = reorder_nodenum(); 229 230 blockdown(this); 231 232 if (best < reorder_nodenum()) 233 { 234 blockdown(this->prev); 235 this = this->next; 236 } 237 else 238 if (first == this) 239 first = this->prev; 240 if (verbose > 1) 241 { 242 printf("."); 243 fflush(stdout); 244 } 245 } 246 247 if (verbose > 1) 248 printf(" %d nodes\n", reorder_nodenum()); 249 c++; 250 } 251 while (reorder_nodenum() != lastsize); 252 253 return first; 254} 255 256 257/*=== Reorder using a sliding window of size 3 =========================*/ 258#define X(a) 259 260static BddTree *reorder_swapwin3(BddTree *this, BddTree **first) 261{ 262 int setfirst = (this->prev == NULL ? 1 : 0); 263 BddTree *next = this; 264 int best = reorder_nodenum(); 265 266 if (this->next->next == NULL) /* Only two blocks left -> win2 swap */ 267 { 268 blockdown(this); 269 270 if (best < reorder_nodenum()) 271 { 272 blockdown(this->prev); 273 next = this->next; 274 } 275 else 276 { 277 next = this; 278 if (setfirst) 279 *first = this->prev; 280 } 281 } 282 else /* Real win3 swap */ 283 { 284 int pos = 0; 285 X(printf("%d: ", reorder_nodenum())); 286 blockdown(this); /* B A* C (4) */ 287 X(printf("A")); 288 pos++; 289 if (best > reorder_nodenum()) 290 { 291 X(printf("(%d)", reorder_nodenum())); 292 pos = 0; 293 best = reorder_nodenum(); 294 } 295 296 blockdown(this); /* B C A* (3) */ 297 X(printf("B")); 298 pos++; 299 if (best > reorder_nodenum()) 300 { 301 X(printf("(%d)", reorder_nodenum())); 302 pos = 0; 303 best = reorder_nodenum(); 304 } 305 306 this = this->prev->prev; 307 blockdown(this); /* C B* A (2) */ 308 X(printf("C")); 309 pos++; 310 if (best > reorder_nodenum()) 311 { 312 X(printf("(%d)", reorder_nodenum())); 313 pos = 0; 314 best = reorder_nodenum(); 315 } 316 317 blockdown(this); /* C A B* (1) */ 318 X(printf("D")); 319 pos++; 320 if (best > reorder_nodenum()) 321 { 322 X(printf("(%d)", reorder_nodenum())); 323 pos = 0; 324 best = reorder_nodenum(); 325 } 326 327 this = this->prev->prev; 328 blockdown(this); /* A C* B (0)*/ 329 X(printf("E")); 330 pos++; 331 if (best > reorder_nodenum()) 332 { 333 X(printf("(%d)", reorder_nodenum())); 334 pos = 0; 335 best = reorder_nodenum(); 336 } 337 338 X(printf(" -> ")); 339 340 if (pos >= 1) /* A C B -> C A* B */ 341 { 342 this = this->prev; 343 blockdown(this); 344 next = this; 345 if (setfirst) 346 *first = this->prev; 347 X(printf("a(%d)", reorder_nodenum())); 348 } 349 350 if (pos >= 2) /* C A B -> C B A* */ 351 { 352 blockdown(this); 353 next = this->prev; 354 if (setfirst) 355 *first = this->prev->prev; 356 X(printf("b(%d)", reorder_nodenum())); 357 } 358 359 if (pos >= 3) /* C B A -> B C* A */ 360 { 361 this = this->prev->prev; 362 blockdown(this); 363 next = this; 364 if (setfirst) 365 *first = this->prev; 366 X(printf("c(%d)", reorder_nodenum())); 367 } 368 369 if (pos >= 4) /* B C A -> B A C* */ 370 { 371 blockdown(this); 372 next = this->prev; 373 if (setfirst) 374 *first = this->prev->prev; 375 X(printf("d(%d)", reorder_nodenum())); 376 } 377 378 if (pos >= 5) /* B A C -> A B* C */ 379 { 380 this = this->prev->prev; 381 blockdown(this); 382 next = this; 383 if (setfirst) 384 *first = this->prev; 385 X(printf("e(%d)", reorder_nodenum())); 386 } 387 X(printf("\n")); 388 } 389 390 return next; 391} 392 393 394static BddTree *reorder_win3(BddTree *t) 395{ 396 BddTree *this=t, *first=t; 397 398 if (t == NULL) 399 return t; 400 401 if (verbose > 1) 402 printf("Win3 start: %d nodes\n", reorder_nodenum()); 403 fflush(stdout); 404 405 while (this->next != NULL) 406 { 407 this = reorder_swapwin3(this, &first); 408 409 if (verbose > 1) 410 { 411 printf("."); 412 fflush(stdout); 413 } 414 } 415 416 if (verbose > 1) 417 printf("\nWin3 end: %d nodes\n", reorder_nodenum()); 418 fflush(stdout); 419 420 return first; 421} 422 423 424static BddTree *reorder_win3ite(BddTree *t) 425{ 426 BddTree *this=t, *first=t; 427 int lastsize; 428 429 if (t == NULL) 430 return t; 431 432 if (verbose > 1) 433 printf("Win3ite start: %d nodes\n", reorder_nodenum()); 434 435 do 436 { 437 lastsize = reorder_nodenum(); 438 this = first; 439 440 while (this->next != NULL && this->next->next != NULL) 441 { 442 this = reorder_swapwin3(this, &first); 443 444 if (verbose > 1) 445 { 446 printf("."); 447 fflush(stdout); 448 } 449 } 450 451 if (verbose > 1) 452 printf(" %d nodes\n", reorder_nodenum()); 453 } 454 while (reorder_nodenum() != lastsize); 455 456 if (verbose > 1) 457 printf("Win3ite end: %d nodes\n", reorder_nodenum()); 458 459 return first; 460} 461 462 463/*=== Reorder by sifting =============================================*/ 464 465/* Move a specific block up and down in the order and place at last in 466 the best position 467*/ 468static void reorder_sift_bestpos(BddTree *blk, int middlePos) 469{ 470 int best = reorder_nodenum(); 471 int maxAllowed; 472 int bestpos = 0; 473 int dirIsUp = 1; 474 int n; 475 476 if (bddmaxnodesize > 0) 477 maxAllowed = MIN(best/5+best, bddmaxnodesize-bddmaxnodeincrease-2); 478 else 479 maxAllowed = best/5+best; 480 481 /* Determine initial direction */ 482 if (blk->pos > middlePos) 483 dirIsUp = 0; 484 485 /* Move block back and forth */ 486 for (n=0 ; n<2 ; n++) 487 { 488 int first = 1; 489 490 if (dirIsUp) 491 { 492 while (blk->prev != NULL && 493 (reorder_nodenum() <= maxAllowed || first)) 494 { 495 first = 0; 496 blockdown(blk->prev); 497 bestpos--; 498 499 if (verbose > 1) 500 { 501 printf("-"); 502 fflush(stdout); 503 } 504 505 if (reorder_nodenum() < best) 506 { 507 best = reorder_nodenum(); 508 bestpos = 0; 509 510 if (bddmaxnodesize > 0) 511 maxAllowed = MIN(best/5+best, 512 bddmaxnodesize-bddmaxnodeincrease-2); 513 else 514 maxAllowed = best/5+best; 515 } 516 } 517 } 518 else 519 { 520 while (blk->next != NULL && 521 (reorder_nodenum() <= maxAllowed || first)) 522 { 523 first = 0; 524 blockdown(blk); 525 bestpos++; 526 527 if (verbose > 1) 528 { 529 printf("+"); 530 fflush(stdout); 531 } 532 533 if (reorder_nodenum() < best) 534 { 535 best = reorder_nodenum(); 536 bestpos = 0; 537 538 if (bddmaxnodesize > 0) 539 maxAllowed = MIN(best/5+best, 540 bddmaxnodesize-bddmaxnodeincrease-2); 541 else 542 maxAllowed = best/5+best; 543 } 544 } 545 } 546 547 if (reorder_nodenum() > maxAllowed && verbose > 1) 548 { 549 printf("!"); 550 fflush(stdout); 551 } 552 553 dirIsUp = !dirIsUp; 554 } 555 556 /* Move to best pos */ 557 while (bestpos < 0) 558 { 559 blockdown(blk); 560 bestpos++; 561 } 562 while (bestpos > 0) 563 { 564 blockdown(blk->prev); 565 bestpos--; 566 } 567} 568 569 570/* Go through all blocks in a specific sequence and find best 571 position for each of them 572*/ 573static BddTree *reorder_sift_seq(BddTree *t, BddTree **seq, int num) 574{ 575 BddTree *this; 576 int n; 577 578 if (t == NULL) 579 return t; 580 581 for (n=0 ; n<num ; n++) 582 { 583 long c2, c1 = clock(); 584 585 if (verbose > 1) 586 { 587 printf("Sift "); 588 if (reorder_filehandler) 589 reorder_filehandler(stdout, seq[n]->id); 590 else 591 printf("%d", seq[n]->id); 592 printf(": "); 593 } 594 595 reorder_sift_bestpos(seq[n], num/2); 596 597 if (verbose > 1) 598 printf("\n> %d nodes", reorder_nodenum()); 599 600 c2 = clock(); 601 if (verbose > 1) 602 printf(" (%.1f sec)\n", (float)(c2-c1)/CLOCKS_PER_SEC); 603 } 604 605 /* Find first block */ 606 for (this=t ; this->prev != NULL ; this=this->prev) 607 /* nil */; 608 609 return this; 610} 611 612 613/* Compare function for sorting sifting sequence 614 */ 615static int siftTestCmp(const void *aa, const void *bb) 616{ 617 const sizePair *a = (sizePair*)aa; 618 const sizePair *b = (sizePair*)bb; 619 620 if (a->val < b->val) 621 return -1; 622 if (a->val > b->val) 623 return 1; 624 return 0; 625} 626 627 628/* Find sifting sequence based on the number of nodes at each level 629 */ 630static BddTree *reorder_sift(BddTree *t) 631{ 632 BddTree *this, **seq; 633 sizePair *p; 634 int n, num; 635 636 for (this=t,num=0 ; this!=NULL ; this=this->next) 637 this->pos = num++; 638 639 if ((p=NEW(sizePair,num)) == NULL) 640 return t; 641 if ((seq=NEW(BddTree*,num)) == NULL) 642 { 643 free(p); 644 return t; 645 } 646 647 for (this=t,n=0 ; this!=NULL ; this=this->next,n++) 648 { 649 int v; 650 651 /* Accumulate number of nodes for each block */ 652 p[n].val = 0; 653 for (v=this->first ; v<=this->last ; v++) 654 p[n].val -= levels[v].nodenum; 655 656 p[n].block = this; 657 } 658 659 /* Sort according to the number of nodes at each level */ 660 qsort(p, num, sizeof(sizePair), siftTestCmp); 661 662 /* Create sequence */ 663 for (n=0 ; n<num ; n++) 664 seq[n] = p[n].block; 665 666 /* Do the sifting on this sequence */ 667 t = reorder_sift_seq(t, seq, num); 668 669 free(seq); 670 free(p); 671 672 return t; 673} 674 675 676/* Do sifting iteratively until no more improvement can be found 677 */ 678static BddTree *reorder_siftite(BddTree *t) 679{ 680 BddTree *first=t; 681 int lastsize; 682 int c=1; 683 684 if (t == NULL) 685 return t; 686 687 do 688 { 689 if (verbose > 1) 690 printf("Reorder %d\n", c++); 691 692 lastsize = reorder_nodenum(); 693 first = reorder_sift(first); 694 } 695 while (reorder_nodenum() != lastsize); 696 697 return first; 698} 699 700 701/*=== Random reordering (mostly for debugging and test ) =============*/ 702 703static BddTree *reorder_random(BddTree *t) 704{ 705 BddTree *this; 706 BddTree **seq; 707 int n, num=0; 708 709 if (t == NULL) 710 return t; 711 712 for (this=t ; this!=NULL ; this=this->next) 713 num++; 714 seq = NEW(BddTree*,num); 715 for (this=t,num=0 ; this!=NULL ; this=this->next) 716 seq[num++] = this; 717 718 for (n=0 ; n<4*num ; n++) 719 { 720 int blk = random(num); 721 if (seq[blk]->next != NULL) 722 blockdown(seq[blk]); 723 } 724 725 /* Find first block */ 726 for (this=t ; this->prev != NULL ; this=this->prev) 727 /* nil */; 728 729 free(seq); 730 731 if (verbose) 732 printf("Random order: %d nodes\n", reorder_nodenum()); 733 return this; 734} 735 736 737/************************************************************************* 738 Swapping adjacent blocks 739*************************************************************************/ 740 741static void blockdown(BddTree *left) 742{ 743 BddTree *right = left->next; 744 int n; 745 int leftsize = left->last - left->first; 746 int rightsize = right->last - right->first; 747 int leftstart = bddvar2level[left->seq[0]]; 748 int *lseq = left->seq; 749 int *rseq = right->seq; 750 751 /* Move left past right */ 752 while (bddvar2level[lseq[0]] < bddvar2level[rseq[rightsize]]) 753 { 754 for (n=0 ; n<leftsize ; n++) 755 { 756 if (bddvar2level[lseq[n]]+1 != bddvar2level[lseq[n+1]] 757 && bddvar2level[lseq[n]] < bddvar2level[rseq[rightsize]]) 758 { 759 reorder_vardown(lseq[n]); 760 } 761 } 762 763 if (bddvar2level[lseq[leftsize]] < bddvar2level[rseq[rightsize]]) 764 { 765 reorder_vardown(lseq[leftsize]); 766 } 767 } 768 769 /* Move right to where left started */ 770 while (bddvar2level[rseq[0]] > leftstart) 771 { 772 for (n=rightsize ; n>0 ; n--) 773 { 774 if (bddvar2level[rseq[n]]-1 != bddvar2level[rseq[n-1]] 775 && bddvar2level[rseq[n]] > leftstart) 776 { 777 reorder_varup(rseq[n]); 778 } 779 } 780 781 if (bddvar2level[rseq[0]] > leftstart) 782 reorder_varup(rseq[0]); 783 } 784 785 /* Swap left and right data in the order */ 786 left->next = right->next; 787 right->prev = left->prev; 788 left->prev = right; 789 right->next = left; 790 791 if (right->prev != NULL) 792 right->prev->next = right; 793 if (left->next != NULL) 794 left->next->prev = left; 795 796 n = left->pos; 797 left->pos = right->pos; 798 right->pos = n; 799} 800 801 802/************************************************************************* 803 Kernel reordering routines 804*************************************************************************/ 805 806/*=== Garbage collection for reordering ================================*/ 807 808/* Note: Node may be marked 809 */ 810static void addref_rec(int r, char *dep) 811{ 812 if (r < 2) 813 return; 814 815 if (bddnodes[r].refcou == 0) 816 { 817 bddfreenum--; 818 819 /* Detect variable dependencies for the interaction matrix */ 820 dep[VAR(r) & MARKHIDE] = 1; 821 822 /* Make sure the nodenum field is updated. Used in the initial GBC */ 823 levels[VAR(r) & MARKHIDE].nodenum++; 824 825 addref_rec(LOW(r), dep); 826 addref_rec(HIGH(r), dep); 827 } 828 else 829 { 830 int n; 831 832 /* Update (from previously found) variable dependencies 833 * for the interaction matrix */ 834 for (n=0 ; n<bddvarnum ; n++) 835 dep[n] |= imatrixDepends(iactmtx, VAR(r) & MARKHIDE, n); 836 } 837 838 INCREF(r); 839} 840 841 842static void addDependencies(char *dep) 843{ 844 int n,m; 845 846 for (n=0 ; n<bddvarnum ; n++) 847 { 848 for (m=n ; m<bddvarnum ; m++) 849 { 850 if (dep[n] && dep[m]) 851 { 852 imatrixSet(iactmtx, n,m); 853 imatrixSet(iactmtx, m,n); 854 } 855 } 856 } 857} 858 859 860/* Make sure all nodes are recursively reference counted and store info about 861 nodes that are refcou. externally. This info is used at last to revert 862 to the standard GBC mode. 863 */ 864static int mark_roots(void) 865{ 866 char *dep = NEW(char,bddvarnum); 867 int n; 868 869 for (n=2,extrootsize=0 ; n<bddnodesize ; n++) 870 { 871 /* This is where we go from .level to .var! 872 * - Do NOT use the LEVEL macro here. */ 873 bddnodes[n].level = bddlevel2var[bddnodes[n].level]; 874 875 if (bddnodes[n].refcou > 0) 876 { 877 SETMARK(n); 878 extrootsize++; 879 } 880 } 881 882 if ((extroots=(int*)(malloc(sizeof(int)*extrootsize))) == NULL) 883 return bdd_error(BDD_MEMORY); 884 885 iactmtx = imatrixNew(bddvarnum); 886 887 for (n=2,extrootsize=0 ; n<bddnodesize ; n++) 888 { 889 BddNode *node = &bddnodes[n]; 890 891 if (MARKEDp(node)) 892 { 893 UNMARKp(node); 894 extroots[extrootsize++] = n; 895 896 memset(dep,0,bddvarnum); 897 dep[VARp(node)] = 1; 898 levels[VARp(node)].nodenum++; 899 900 addref_rec(LOWp(node), dep); 901 addref_rec(HIGHp(node), dep); 902 903 addDependencies(dep); 904 } 905 906 /* Make sure the hash field is empty. This saves a loop in the 907 initial GBC */ 908 node->hash = 0; 909 } 910 911 bddnodes[0].hash = 0; 912 bddnodes[1].hash = 0; 913 914 free(dep); 915 return 0; 916} 917 918 919/* Now that all nodes are recursively reference counted we must make sure 920 that the new hashing scheme is used AND that dead nodes are removed. 921 This is also a good time to create the interaction matrix. 922*/ 923static void reorder_gbc(void) 924{ 925 int n; 926 927 bddfreepos = 0; 928 bddfreenum = 0; 929 930 /* No need to zero all hash fields - this is done in mark_roots */ 931 932 for (n=bddnodesize-1 ; n>=2 ; n--) 933 { 934 register BddNode *node = &bddnodes[n]; 935 936 if (node->refcou > 0) 937 { 938 register unsigned int hash; 939 940 hash = NODEHASH(VARp(node), LOWp(node), HIGHp(node)); 941 node->next = bddnodes[hash].hash; 942 bddnodes[hash].hash = n; 943 944 } 945 else 946 { 947 LOWp(node) = -1; 948 node->next = bddfreepos; 949 bddfreepos = n; 950 bddfreenum++; 951 } 952 } 953} 954 955 956static void reorder_setLevellookup(void) 957{ 958 int n; 959 960 for (n=0 ; n<bddvarnum ; n++) 961 { 962#ifdef USERESIZE 963 levels[n].maxsize = bddnodesize / bddvarnum; 964 levels[n].start = n * levels[n].maxsize; 965 levels[n].size = MIN(levels[n].maxsize, (levels[n].nodenum*5)/4); 966#else 967 levels[n].maxsize = bddnodesize / bddvarnum; 968 levels[n].start = n * levels[n].maxsize; 969 levels[n].size = levels[n].maxsize; 970#endif 971 972 if (levels[n].size >= 4) 973 levels[n].size = bdd_prime_lte(levels[n].size); 974 975#if 0 976 printf("L%3d: start %d, size %d, nodes %d\n", n, levels[n].start, 977 levels[n].size, levels[n].nodenum); 978#endif 979 } 980} 981 982 983static void reorder_rehashAll(void) 984{ 985 int n; 986 987 reorder_setLevellookup(); 988 bddfreepos = 0; 989 990 for (n=bddnodesize-1 ; n>=0 ; n--) 991 bddnodes[n].hash = 0; 992 993 for (n=bddnodesize-1 ; n>=2 ; n--) 994 { 995 register BddNode *node = &bddnodes[n]; 996 997 if (node->refcou > 0) 998 { 999 register unsigned int hash; 1000 1001 hash = NODEHASH(VARp(node), LOWp(node), HIGHp(node)); 1002 node->next = bddnodes[hash].hash; 1003 bddnodes[hash].hash = n; 1004 } 1005 else 1006 { 1007 node->next = bddfreepos; 1008 bddfreepos = n; 1009 } 1010 } 1011} 1012 1013 1014/*=== Unique table handling for reordering =============================*/ 1015 1016/* Note: rehashing must not take place during a makenode call. It is okay 1017 to resize the table, but *not* to rehash it. 1018 */ 1019static int reorder_makenode(int var, int low, int high) 1020{ 1021 register BddNode *node; 1022 register unsigned int hash; 1023 register int res; 1024 1025#ifdef CACHESTATS 1026 bddcachestats.uniqueAccess++; 1027#endif 1028 1029 /* Note: We know that low,high has a refcou greater than zero, so 1030 there is no need to add reference *recursively* */ 1031 1032 /* check whether childs are equal */ 1033 if (low == high) 1034 { 1035 INCREF(low); 1036 return low; 1037 } 1038 1039 /* Try to find an existing node of this kind */ 1040 hash = NODEHASH(var, low, high); 1041 res = bddnodes[hash].hash; 1042 1043 while(res != 0) 1044 { 1045 if (LOW(res) == low && HIGH(res) == high) 1046 { 1047#ifdef CACHESTATS 1048 bddcachestats.uniqueHit++; 1049#endif 1050 INCREF(res); 1051 return res; 1052 } 1053 res = bddnodes[res].next; 1054 1055#ifdef CACHESTATS 1056 bddcachestats.uniqueChain++; 1057#endif 1058 } 1059 1060 /* No existing node -> build one */ 1061#ifdef CACHESTATS 1062 bddcachestats.uniqueMiss++; 1063#endif 1064 1065 /* Any free nodes to use ? */ 1066 if (bddfreepos == 0) 1067 { 1068 if (bdderrorcond) 1069 return 0; 1070 1071 /* Try to allocate more nodes - call noderesize without 1072 * enabling rehashing. 1073 * Note: if ever rehashing is allowed here, then remember to 1074 * update local variable "hash" */ 1075 bdd_noderesize(0); 1076 resizedInMakenode = 1; 1077 1078 /* Panic if that is not possible */ 1079 if (bddfreepos == 0) 1080 { 1081 bdd_error(BDD_NODENUM); 1082 bdderrorcond = abs(BDD_NODENUM); 1083 return 0; 1084 } 1085 } 1086 1087 /* Build new node */ 1088 res = bddfreepos; 1089 bddfreepos = bddnodes[bddfreepos].next; 1090 levels[var].nodenum++; 1091 bddproduced++; 1092 bddfreenum--; 1093 1094 node = &bddnodes[res]; 1095 VARp(node) = var; 1096 LOWp(node) = low; 1097 HIGHp(node) = high; 1098 1099 /* Insert node in hash chain */ 1100 node->next = bddnodes[hash].hash; 1101 bddnodes[hash].hash = res; 1102 1103 /* Make sure it is reference counted */ 1104 node->refcou = 1; 1105 INCREF(LOWp(node)); 1106 INCREF(HIGHp(node)); 1107 1108 return res; 1109} 1110 1111 1112/*=== Swapping two adjacent variables ==================================*/ 1113 1114/* Go through var 0 nodes. Move nodes that depends on var 1 to a separate 1115 * chain (toBeProcessed) and let the rest stay in the table. 1116 */ 1117static int reorder_downSimple(int var0) 1118{ 1119 int toBeProcessed = 0; 1120 int var1 = bddlevel2var[bddvar2level[var0]+1]; 1121 int vl0 = levels[var0].start; 1122 int size0 = levels[var0].size; 1123 int n; 1124 1125 levels[var0].nodenum = 0; 1126 1127 for (n=0 ; n<size0 ; n++) 1128 { 1129 int r; 1130 1131 r = bddnodes[n + vl0].hash; 1132 bddnodes[n + vl0].hash = 0; 1133 1134 while (r != 0) 1135 { 1136 BddNode *node = &bddnodes[r]; 1137 int next = node->next; 1138 1139 if (VAR(LOWp(node)) != var1 && VAR(HIGHp(node)) != var1) 1140 { 1141 /* Node does not depend on next var, let it stay in the chain */ 1142 node->next = bddnodes[n+vl0].hash; 1143 bddnodes[n+vl0].hash = r; 1144 levels[var0].nodenum++; 1145 } 1146 else 1147 { 1148 /* Node depends on next var - save it for later procesing */ 1149 node->next = toBeProcessed; 1150 toBeProcessed = r; 1151#ifdef SWAPCOUNT 1152 bddcachestats.swapCount++; 1153#endif 1154 1155 } 1156 1157 r = next; 1158 } 1159 } 1160 1161 return toBeProcessed; 1162} 1163 1164 1165/* Now process all the var 0 nodes that depends on var 1. 1166 * 1167 * It is extremely important that no rehashing is done inside the makenode 1168 * calls, since this would destroy the toBeProcessed chain. 1169 */ 1170static void reorder_swap(int toBeProcessed, int var0) 1171{ 1172 int var1 = bddlevel2var[bddvar2level[var0]+1]; 1173 1174 while (toBeProcessed) 1175 { 1176 BddNode *node = &bddnodes[toBeProcessed]; 1177 int next = node->next; 1178 int f0 = LOWp(node); 1179 int f1 = HIGHp(node); 1180 int f00, f01, f10, f11, hash; 1181 1182 /* Find the cofactors for the new nodes */ 1183 if (VAR(f0) == var1) 1184 { 1185 f00 = LOW(f0); 1186 f01 = HIGH(f0); 1187 } 1188 else 1189 f00 = f01 = f0; 1190 1191 if (VAR(f1) == var1) 1192 { 1193 f10 = LOW(f1); 1194 f11 = HIGH(f1); 1195 } 1196 else 1197 f10 = f11 = f1; 1198 1199 /* Note: makenode does refcou. */ 1200 f0 = reorder_makenode(var0, f00, f10); 1201 f1 = reorder_makenode(var0, f01, f11); 1202 node = &bddnodes[toBeProcessed]; /* Might change in makenode */ 1203 1204 /* We know that the refcou of the grandchilds of this node 1205 * is greater than one (these are f00...f11), so there is 1206 * no need to do a recursive refcou decrease. It is also 1207 * possible for the LOWp(node)/high nodes to come alive again, 1208 * so deref. of the childs is delayed until the local GBC. */ 1209 1210 DECREF(LOWp(node)); 1211 DECREF(HIGHp(node)); 1212 1213 /* Update in-place */ 1214 VARp(node) = var1; 1215 LOWp(node) = f0; 1216 HIGHp(node) = f1; 1217 1218 levels[var1].nodenum++; 1219 1220 /* Rehash the node since it got new childs */ 1221 hash = NODEHASH(VARp(node), LOWp(node), HIGHp(node)); 1222 node->next = bddnodes[hash].hash; 1223 bddnodes[hash].hash = toBeProcessed; 1224 1225 toBeProcessed = next; 1226 } 1227} 1228 1229 1230/* Now go through the var 1 chains. The nodes live here have survived 1231 * the call to reorder_swap() and may stay in the chain. 1232 * The dead nodes are reclaimed. 1233 */ 1234static void reorder_localGbc(int var0) 1235{ 1236 int var1 = bddlevel2var[bddvar2level[var0]+1]; 1237 int vl1 = levels[var1].start; 1238 int size1 = levels[var1].size; 1239 int n; 1240 1241 for (n=0 ; n<size1 ; n++) 1242 { 1243 int hash = n+vl1; 1244 int r = bddnodes[hash].hash; 1245 bddnodes[hash].hash = 0; 1246 1247 while (r) 1248 { 1249 BddNode *node = &bddnodes[r]; 1250 int next = node->next; 1251 1252 if (node->refcou > 0) 1253 { 1254 node->next = bddnodes[hash].hash; 1255 bddnodes[hash].hash = r; 1256 } 1257 else 1258 { 1259 DECREF(LOWp(node)); 1260 DECREF(HIGHp(node)); 1261 1262 LOWp(node) = -1; 1263 node->next = bddfreepos; 1264 bddfreepos = r; 1265 levels[var1].nodenum--; 1266 bddfreenum++; 1267 } 1268 1269 r = next; 1270 } 1271 } 1272} 1273 1274 1275 1276 1277#ifdef USERESIZE 1278 1279static void reorder_swapResize(int toBeProcessed, int var0) 1280{ 1281 int var1 = bddlevel2var[bddvar2level[var0]+1]; 1282 1283 while (toBeProcessed) 1284 { 1285 BddNode *node = &bddnodes[toBeProcessed]; 1286 int next = node->next; 1287 int f0 = LOWp(node); 1288 int f1 = HIGHp(node); 1289 int f00, f01, f10, f11; 1290 1291 /* Find the cofactors for the new nodes */ 1292 if (VAR(f0) == var1) 1293 { 1294 f00 = LOW(f0); 1295 f01 = HIGH(f0); 1296 } 1297 else 1298 f00 = f01 = f0; 1299 1300 if (VAR(f1) == var1) 1301 { 1302 f10 = LOW(f1); 1303 f11 = HIGH(f1); 1304 } 1305 else 1306 f10 = f11 = f1; 1307 1308 /* Note: makenode does refcou. */ 1309 f0 = reorder_makenode(var0, f00, f10); 1310 f1 = reorder_makenode(var0, f01, f11); 1311 node = &bddnodes[toBeProcessed]; /* Might change in makenode */ 1312 1313 /* We know that the refcou of the grandchilds of this node 1314 * is greater than one (these are f00...f11), so there is 1315 * no need to do a recursive refcou decrease. It is also 1316 * possible for the LOWp(node)/high nodes to come alive again, 1317 * so deref. of the childs is delayed until the local GBC. */ 1318 1319 DECREF(LOWp(node)); 1320 DECREF(HIGHp(node)); 1321 1322 /* Update in-place */ 1323 VARp(node) = var1; 1324 LOWp(node) = f0; 1325 HIGHp(node) = f1; 1326 1327 levels[var1].nodenum++; 1328 1329 /* Do not rehash yet since we are going to resize the hash table */ 1330 1331 toBeProcessed = next; 1332 } 1333} 1334 1335 1336static void reorder_localGbcResize(int toBeProcessed, int var0) 1337{ 1338 int var1 = bddlevel2var[bddvar2level[var0]+1]; 1339 int vl1 = levels[var1].start; 1340 int size1 = levels[var1].size; 1341 int n; 1342 1343 for (n=0 ; n<size1 ; n++) 1344 { 1345 int hash = n+vl1; 1346 int r = bddnodes[hash].hash; 1347 bddnodes[hash].hash = 0; 1348 1349 while (r) 1350 { 1351 BddNode *node = &bddnodes[r]; 1352 int next = node->next; 1353 1354 if (node->refcou > 0) 1355 { 1356 node->next = toBeProcessed; 1357 toBeProcessed = r; 1358 } 1359 else 1360 { 1361 DECREF(LOWp(node)); 1362 DECREF(HIGHp(node)); 1363 1364 LOWp(node) = -1; 1365 node->next = bddfreepos; 1366 bddfreepos = r; 1367 levels[var1].nodenum--; 1368 bddfreenum++; 1369 } 1370 1371 r = next; 1372 } 1373 } 1374 1375 /* Resize */ 1376 if (levels[var1].nodenum < levels[var1].size) 1377 levels[var1].size = MIN(levels[var1].maxsize, levels[var1].size/2); 1378 else 1379 levels[var1].size = MIN(levels[var1].maxsize, levels[var1].size*2); 1380 1381 if (levels[var1].size >= 4) 1382 levels[var1].size = bdd_prime_lte(levels[var1].size); 1383 1384 /* Rehash the remaining live nodes */ 1385 while (toBeProcessed) 1386 { 1387 BddNode *node = &bddnodes[toBeProcessed]; 1388 int next = node->next; 1389 int hash = NODEHASH(VARp(node), LOWp(node), HIGHp(node)); 1390 1391 node->next = bddnodes[hash].hash; 1392 bddnodes[hash].hash = toBeProcessed; 1393 1394 toBeProcessed = next; 1395 } 1396} 1397 1398#endif /* USERESIZE */ 1399 1400 1401static int reorder_varup(int var) 1402{ 1403 if (var < 0 || var >= bddvarnum) 1404 return bdd_error(BDD_VAR); 1405 if (bddvar2level[var] == 0) 1406 return 0; 1407 return reorder_vardown( bddlevel2var[bddvar2level[var]-1]); 1408} 1409 1410 1411#if 0 1412static void sanitycheck(void) 1413{ 1414 int n,v,r; 1415 int cou=0; 1416 1417 for (v=0 ; v<bddvarnum ; v++) 1418 { 1419 int vcou=0; 1420 1421 for (n=0 ; n<levels[v].size ; n++) 1422 { 1423 r = bddnodes[n+levels[v].start].hash; 1424 1425 while (r) 1426 { 1427 assert(VAR(r) == v); 1428 r = bddnodes[r].next; 1429 cou++; 1430 vcou++; 1431 } 1432 } 1433 1434 assert(vcou == levels[v].nodenum); 1435 } 1436 1437 for (n=2 ; n<bddnodesize ; n++) 1438 { 1439 if (bddnodes[n].refcou > 0) 1440 { 1441 assert(LEVEL(n) < LEVEL(LOW(n))); 1442 assert(LEVEL(n) < LEVEL(HIGH(n))); 1443 cou--; 1444 } 1445 } 1446 1447 assert(cou == 0); 1448} 1449#endif 1450 1451static int reorder_vardown(int var) 1452{ 1453 int n, level; 1454 1455 if (var < 0 || var >= bddvarnum) 1456 return bdd_error(BDD_VAR); 1457 if ((level=bddvar2level[var]) >= bddvarnum-1) 1458 return 0; 1459 1460 resizedInMakenode = 0; 1461 1462 if (imatrixDepends(iactmtx, var, bddlevel2var[level+1])) 1463 { 1464 int toBeProcessed = reorder_downSimple(var); 1465#ifdef USERESIZE 1466 levelData *l = &levels[var]; 1467 1468 if (l->nodenum < (l->size)/3 || 1469 l->nodenum >= (l->size*3)/2 && l->size < l->maxsize) 1470 { 1471 reorder_swapResize(toBeProcessed, var); 1472 reorder_localGbcResize(toBeProcessed, var); 1473 } 1474 else 1475#endif 1476 { 1477 reorder_swap(toBeProcessed, var); 1478 reorder_localGbc(var); 1479 } 1480 } 1481 1482 /* Swap the var<->level tables */ 1483 n = bddlevel2var[level]; 1484 bddlevel2var[level] = bddlevel2var[level+1]; 1485 bddlevel2var[level+1] = n; 1486 1487 n = bddvar2level[var]; 1488 bddvar2level[var] = bddvar2level[ bddlevel2var[level] ]; 1489 bddvar2level[ bddlevel2var[level] ] = n; 1490 1491 /* Update all rename pairs */ 1492 bdd_pairs_vardown(level); 1493 1494 if (resizedInMakenode) 1495 reorder_rehashAll(); 1496 1497 return 0; 1498} 1499 1500 1501/************************************************************************* 1502 User reordering interface 1503*************************************************************************/ 1504 1505/* 1506NAME {* bdd\_swapvar *} 1507SECTION {* reorder *} 1508SHORT {* Swap two BDD variables *} 1509PROTO {* int bdd_swapvar(int v1, int v2) *} 1510DESCR {* Use {\tt bdd\_swapvar} to swap the position (in the current 1511 variable order) of the two BDD 1512 variables {\tt v1} and {\tt v2}. There are no constraints on the 1513 position of the two variables before the call. This function may 1514 {\em not} be used together with user defined variable blocks. 1515 The swap is done by a series of adjacent variable swaps and 1516 requires the whole node table to be rehashed twice for each call 1517 to {\tt bdd\_swapvar}. It should therefore not be used were 1518 efficiency is a major concern. *} 1519RETURN {* Zero on succes and a negative error code otherwise. *} 1520ALSO {* bdd\_reorder, bdd\_addvarblock *} 1521*/ 1522int bdd_swapvar(int v1, int v2) 1523{ 1524 int l1, l2; 1525 1526 /* Do not swap when variable-blocks are used */ 1527 if (vartree != NULL) 1528 return bdd_error(BDD_VARBLK); 1529 1530 /* Don't bother swapping x with x */ 1531 if (v1 == v2) 1532 return 0; 1533 1534 /* Make sure the variable exists */ 1535 if (v1 < 0 || v1 >= bddvarnum || v2 < 0 || v2 >= bddvarnum) 1536 return bdd_error(BDD_VAR); 1537 1538 l1 = bddvar2level[v1]; 1539 l2 = bddvar2level[v2]; 1540 1541 /* Make sure v1 is before v2 */ 1542 if (l1 > l2) 1543 { 1544 int tmp = v1; 1545 v1 = v2; 1546 v2 = tmp; 1547 l1 = bddvar2level[v1]; 1548 l2 = bddvar2level[v2]; 1549 } 1550 1551 reorder_init(); 1552 1553 /* Move v1 to v2's position */ 1554 while (bddvar2level[v1] < l2) 1555 reorder_vardown(v1); 1556 1557 /* Move v2 to v1's position */ 1558 while (bddvar2level[v2] > l1) 1559 reorder_varup(v2); 1560 1561 reorder_done(); 1562 1563 return 0; 1564} 1565 1566 1567void bdd_default_reohandler(int prestate) 1568{ 1569 static long c1; 1570 1571 if (verbose > 0) 1572 { 1573 if (prestate) 1574 { 1575 printf("Start reordering\n"); 1576 c1 = clock(); 1577 } 1578 else 1579 { 1580 long c2 = clock(); 1581 printf("End reordering. Went from %d to %d nodes (%.1f sec)\n", 1582 usednum_before, usednum_after, (float)(c2-c1)/CLOCKS_PER_SEC); 1583 } 1584 } 1585} 1586 1587 1588/* 1589NAME {* bdd\_disable\_reorder *} 1590SECTION {* reorder *} 1591SHORT {* Disable automatic reordering *} 1592PROTO {* void bdd_disable_reorder(void) *} 1593DESCR {* Disables automatic reordering until {\tt bdd\_enable\_reorder} 1594 is called. Reordering is enabled by default as soon as any variable 1595 blocks have been defined. *} 1596ALSO {* bdd\_enable\_reorder *} 1597*/ 1598void bdd_disable_reorder(void) 1599{ 1600 reorderdisabled = 1; 1601} 1602 1603 1604/* 1605NAME {* bdd\_enable\_reorder *} 1606SECTION {* reorder *} 1607SHORT {* Enables automatic reordering *} 1608PROTO {* void bdd_enable_reorder(void) *} 1609DESCR {* Re-enables reordering after a call to {\tt bdd\_disable\_reorder}. *} 1610ALSO {* bdd\_disable\_reorder *} 1611*/ 1612void bdd_enable_reorder(void) 1613{ 1614 reorderdisabled = 0; 1615} 1616 1617 1618int bdd_reorder_ready(void) 1619{ 1620 if (bddreordermethod == BDD_REORDER_NONE || vartree == NULL || 1621 bddreordertimes == 0 || reorderdisabled) 1622 return 0; 1623 return 1; 1624} 1625 1626 1627void bdd_reorder_auto(void) 1628{ 1629 if (!bdd_reorder_ready) 1630 return; 1631 1632 if (reorder_handler != NULL) 1633 reorder_handler(1); 1634 1635 bdd_reorder(bddreordermethod); 1636 bddreordertimes--; 1637 1638 if (reorder_handler != NULL) 1639 reorder_handler(0); 1640} 1641 1642 1643static int reorder_init(void) 1644{ 1645 int n; 1646 1647 if ((levels=NEW(levelData,bddvarnum)) == NULL) 1648 return -1; 1649 1650 for (n=0 ; n<bddvarnum ; n++) 1651 { 1652 levels[n].start = -1; 1653 levels[n].size = 0; 1654 levels[n].nodenum = 0; 1655 } 1656 1657 /* First mark and recursive refcou. all roots and childs. Also do some 1658 * setup here for both setLevellookup and reorder_gbc */ 1659 if (mark_roots() < 0) 1660 return -1; 1661 1662 /* Initialize the hash tables */ 1663 reorder_setLevellookup(); 1664 1665 /* Garbage collect and rehash to new scheme */ 1666 reorder_gbc(); 1667 1668 return 0; 1669} 1670 1671 1672static void reorder_done(void) 1673{ 1674 int n; 1675 1676 for (n=0 ; n<extrootsize ; n++) 1677 SETMARK(extroots[n]); 1678 for (n=2 ; n<bddnodesize ; n++) 1679 { 1680 if (MARKED(n)) 1681 UNMARK(n); 1682 else 1683 bddnodes[n].refcou = 0; 1684 1685 /* This is where we go from .var to .level again! 1686 * - Do NOT use the LEVEL macro here. */ 1687 bddnodes[n].level = bddvar2level[bddnodes[n].level]; 1688 } 1689 1690#if 0 1691 for (n=0 ; n<bddvarnum ; n++) 1692 printf("%3d\n", bddlevel2var[n]); 1693 printf("\n"); 1694#endif 1695 1696#if 0 1697 for (n=0 ; n<bddvarnum ; n++) 1698 printf("%3d: %4d nodes , %4d entries\n", n, levels[n].nodenum, 1699 levels[n].size); 1700#endif 1701 free(extroots); 1702 free(levels); 1703 imatrixDelete(iactmtx); 1704 bdd_gbc(); 1705} 1706 1707 1708static int varseqCmp(const void *aa, const void *bb) 1709{ 1710 int a = bddvar2level[*((const int*)aa)]; 1711 int b = bddvar2level[*((const int*)bb)]; 1712 1713 if (a < b) 1714 return -1; 1715 if (a > b) 1716 return 1; 1717 return 0; 1718} 1719 1720 1721static BddTree *reorder_block(BddTree *t, int method) 1722{ 1723 BddTree *this; 1724 1725 if (t == NULL) 1726 return NULL; 1727 1728 if (t->fixed == BDD_REORDER_FREE && t->nextlevel!=NULL) 1729 { 1730 switch(method) 1731 { 1732 case BDD_REORDER_WIN2: 1733 t->nextlevel = reorder_win2(t->nextlevel); 1734 break; 1735 case BDD_REORDER_WIN2ITE: 1736 t->nextlevel = reorder_win2ite(t->nextlevel); 1737 break; 1738 case BDD_REORDER_SIFT: 1739 t->nextlevel = reorder_sift(t->nextlevel); 1740 break; 1741 case BDD_REORDER_SIFTITE: 1742 t->nextlevel = reorder_siftite(t->nextlevel); 1743 break; 1744 case BDD_REORDER_WIN3: 1745 t->nextlevel = reorder_win3(t->nextlevel); 1746 break; 1747 case BDD_REORDER_WIN3ITE: 1748 t->nextlevel = reorder_win3ite(t->nextlevel); 1749 break; 1750 case BDD_REORDER_RANDOM: 1751 t->nextlevel = reorder_random(t->nextlevel); 1752 break; 1753 } 1754 } 1755 1756 for (this=t->nextlevel ; this ; this=this->next) 1757 reorder_block(this, method); 1758 1759 if (t->seq != NULL) 1760 qsort(t->seq, t->last-t->first+1, sizeof(int), varseqCmp); 1761 1762 return t; 1763} 1764 1765 1766/* 1767NAME {* bdd\_reorder *} 1768SECTION {* reorder *} 1769SHORT {* start dynamic reordering *} 1770PROTO {* void bdd_reorder(int method) *} 1771DESCR {* This function initiates dynamic reordering using the heuristic 1772 defined by {\tt method}, which may be one of the following 1773 \begin{description} 1774 \item {\tt BDD\_REORDER\_WIN2}\\ 1775 Reordering using a sliding window of size 2. This algorithm 1776 swaps two adjacent variable blocks and if this results in 1777 more nodes then the two blocks are swapped back again. 1778 Otherwise the result is kept in the variable order. This is 1779 then repeated for all variable blocks. 1780 \item {\tt BDD\_REORDER\_WIN2ITE}\\ 1781 The same as above but the process is repeated until no further 1782 progress is done. Usually a fast and efficient method. 1783 \item {\tt BDD\_REORDER\_WIN3}\\ 1784 The same as above but with a window size of 3. 1785 \item {\tt BDD\_REORDER\_WIN2ITE}\\ 1786 The same as above but with a window size of 3. 1787 \item {\tt BDD\_REORDER\_SIFT}\\ 1788 Reordering where each block is moved through all possible 1789 positions. The best of these is then used as the new position. 1790 Potentially a very slow but good method. 1791 \item {\tt BDD\_REORDER\_SIFTITE}\\ 1792 The same as above but the process is repeated until no further 1793 progress is done. Can be extremely slow. 1794 \item {\tt BDD\_REORDER\_RANDOM}\\ 1795 Mostly used for debugging purpose, but may be usefull for 1796 others. Selects a random position for each variable. 1797 \end{description} 1798 *} 1799ALSO {* bdd\_autoreorder, bdd\_reorder\_verbose, bdd\_addvarblock, bdd\_clrvarblocks *} 1800*/ 1801void bdd_reorder(int method) 1802{ 1803 BddTree *top; 1804 int savemethod = bddreordermethod; 1805 int savetimes = bddreordertimes; 1806 1807 bddreordermethod = method; 1808 bddreordertimes = 1; 1809 1810 if ((top=bddtree_new(-1)) == NULL) 1811 return; 1812 if (reorder_init() < 0) 1813 return; 1814 1815 usednum_before = bddnodesize - bddfreenum; 1816 1817 top->first = 0; 1818 top->last = bdd_varnum()-1; 1819 top->fixed = 0; 1820 top->next = NULL; 1821 top->nextlevel = vartree; 1822 1823 reorder_block(top, method); 1824 vartree = top->nextlevel; 1825 free(top); 1826 1827 usednum_after = bddnodesize - bddfreenum; 1828 1829 reorder_done(); 1830 bddreordermethod = savemethod; 1831 bddreordertimes = savetimes; 1832} 1833 1834 1835/* 1836NAME {* bdd\_reorder\_gain *} 1837SECTION {* reorder *} 1838SHORT {* Calculate the gain in size after a reordering *} 1839PROTO {* int bdd_reorder_gain(void) *} 1840DESCR {* Returns the gain in percent of the previous number of used 1841 nodes. The value returned is 1842 \[ (100 * (A - B)) / A \] 1843 Where $A$ is previous number of used nodes and $B$ is current 1844 number of used nodes. 1845 *} 1846*/ 1847int bdd_reorder_gain(void) 1848{ 1849 if (usednum_before == 0) 1850 return 0; 1851 1852 return (100*(usednum_before - usednum_after)) / usednum_before; 1853} 1854 1855 1856/* 1857NAME {* bdd\_reorder\_hook *} 1858SECTION {* reorder *} 1859SHORT {* sets a handler for automatic reorderings *} 1860PROTO {* bddinthandler bdd_reorder_hook(bddinthandler handler) *} 1861DESCR {* Whenever automatic reordering is done, a check is done to see 1862 if the user has supplied a handler for that event. If so then 1863 it is called with the argument {\tt prestate} being 1 if the 1864 handler is called immediately {\em before} reordering and 1865 {\tt prestate} being 0 if it is called immediately after. 1866 The default handler is 1867 {\tt bdd\_default\_reohandler} which will print information 1868 about the reordering. 1869 1870 A typical handler could look like this: 1871 \begin{verbatim} 1872void reorderhandler(int prestate) 1873{ 1874 if (prestate) 1875 printf("Start reordering"); 1876 else 1877 printf("End reordering"); 1878} 1879\end{verbatim} *} 1880RETURN {* The previous handler *} 1881ALSO {* bdd\_reorder, bdd\_autoreorder, bdd\_resize\_hook *} 1882*/ 1883bddinthandler bdd_reorder_hook(bddinthandler handler) 1884{ 1885 bddinthandler tmp = reorder_handler; 1886 reorder_handler = handler; 1887 return tmp; 1888} 1889 1890 1891/* 1892NAME {* bdd\_blockfile\_hook *} 1893SECTION {* reorder *} 1894SHORT {* Specifies a printing callback handler *} 1895PROTO {* bddfilehandler bdd_blockfile_hook(bddfilehandler handler) *} 1896DESCR {* A printing callback handler is used to convert the variable 1897 block identifiers into something readable by the end user. Use 1898 {\tt bdd\_blockfile\_hook} to pass a handler to BuDDy. A typical 1899 handler could look like this: 1900\begin{verbatim} 1901void printhandler(FILE *o, int block) 1902{ 1903 extern char **blocknames; 1904 fprintf(o, "%s", blocknames[block]); 1905} 1906\end{verbatim} 1907 \noindent 1908 The handler is then called from {\tt bdd\_printorder} and 1909 {\tt bdd\_reorder} (depending on the verbose level) with 1910 the block numbers returned by {\tt bdd\_addvarblock} as arguments. 1911 No default handler is supplied. The argument {\tt handler} may be 1912 NULL if no handler is needed. *} 1913RETURN {* The old handler *} 1914ALSO {* bdd\_printorder *} 1915*/ 1916bddfilehandler bdd_blockfile_hook(bddfilehandler handler) 1917{ 1918 bddfilehandler tmp = reorder_filehandler; 1919 reorder_filehandler = handler; 1920 return tmp; 1921} 1922 1923 1924/* 1925NAME {* bdd\_autoreorder *} 1926EXTRA {* bdd\_autoreorder\_times *} 1927SECTION {* reorder *} 1928SHORT {* enables automatic reordering *} 1929PROTO {* int bdd_autoreorder(int method) 1930int bdd_autoreorder_times(int method, int num) *} 1931DESCR {* Enables automatic reordering using {\tt method} as the reordering 1932 method. If {\tt method} is {\tt BDD\_REORDER\_NONE} then 1933 automatic reordering is disabled. Automatic 1934 reordering is done every time the number of active nodes in the 1935 node table has been doubled and works by interrupting the current 1936 BDD operation, doing the reordering and the retrying the operation. 1937 1938 In the second form the argument {\tt num} specifies the allowed 1939 number of reorderings. So if for example a "one shot" reordering 1940 is needed, then the {\tt num} argument would be set to one. 1941 1942 Values for {\tt method} can be found under {\tt bdd\_reorder}. 1943 *} 1944RETURN {* Returns the old value of {\tt method} *} 1945ALSO {* bdd\_reorder *} 1946*/ 1947int bdd_autoreorder(int method) 1948{ 1949 int tmp = bddreordermethod; 1950 bddreordermethod = method; 1951 bddreordertimes = -1; 1952 return tmp; 1953} 1954 1955 1956int bdd_autoreorder_times(int method, int num) 1957{ 1958 int tmp = bddreordermethod; 1959 bddreordermethod = method; 1960 bddreordertimes = num; 1961 return tmp; 1962} 1963 1964 1965/* 1966NAME {* bdd\_var2level *} 1967SECTION {* reorder *} 1968SHORT {* Fetch the level of a specific BDD variable *} 1969PROTO {* int bdd_var2level(int var) *} 1970DESCR {* Returns the position of the variable {\tt var} in the current 1971 variable order. *} 1972ALSO {* bdd\_reorder, bdd\_level2var *} 1973*/ 1974int bdd_var2level(int var) 1975{ 1976 if (var < 0 || var >= bddvarnum) 1977 return bdd_error(BDD_VAR); 1978 1979 return bddvar2level[var]; 1980} 1981 1982 1983/* 1984NAME {* bdd\_level2var *} 1985SECTION {* reorder *} 1986SHORT {* Fetch the variable number of a specific level *} 1987PROTO {* int bdd_level2var(int level) *} 1988DESCR {* Returns the variable placed at position {\tt level} in the 1989 current variable order. *} 1990ALSO {* bdd\_reorder, bdd\_var2level *} 1991*/ 1992int bdd_level2var(int level) 1993{ 1994 if (level < 0 || level >= bddvarnum) 1995 return bdd_error(BDD_VAR); 1996 1997 return bddlevel2var[level]; 1998} 1999 2000 2001/* 2002NAME {* bdd\_getreorder\_times *} 2003SECTION {* reorder *} 2004SHORT {* Fetch the current number of allowed reorderings *} 2005PROTO {* int bdd_getreorder_times(void) *} 2006DESCR {* Returns the current number of allowed reorderings left. This 2007 value can be defined by {\tt bdd\_autoreorder\_times}. *} 2008ALSO {* bdd\_reorder\_times, bdd\_getreorder\_method *} 2009*/ 2010int bdd_getreorder_times(void) 2011{ 2012 return bddreordertimes; 2013} 2014 2015 2016/* 2017NAME {* bdd\_getreorder\_method *} 2018SECTION {* reorder *} 2019SHORT {* Fetch the current reorder method *} 2020PROTO {* int bdd_getreorder_method(void) *} 2021DESCR {* Returns the current reorder method as defined by 2022 {\tt bdd\_autoreorder}. *} 2023ALSO {* bdd\_reorder, bdd\_getreorder\_times *} 2024*/ 2025int bdd_getreorder_method(void) 2026{ 2027 return bddreordermethod; 2028} 2029 2030 2031/* 2032NAME {* bdd\_reorder\_verbose *} 2033SECTION {* reorder *} 2034SHORT {* enables verbose information about reorderings *} 2035PROTO {* int bdd_reorder_verbose(int v) *} 2036DESCR {* With {\tt bdd\_reorder\_verbose} it is possible to set the level 2037 of information which should be printed during reordering. A value 2038 of zero means no information, a value of one means some information 2039 and any greater value will result in a lot of reordering 2040 information. The default value is zero. *} 2041RETURN {* The old verbose level *} 2042ALSO {* bdd\_reorder *} 2043*/ 2044int bdd_reorder_verbose(int v) 2045{ 2046 int tmp = verbose; 2047 verbose = v; 2048 return tmp; 2049} 2050 2051 2052/* 2053NAME {* bdd\_reorder\_probe *} 2054SECTION {* reorder *} 2055SHORT {* Define a handler for minimization of BDDs *} 2056PROTO {* bddsizehandler bdd_reorder_probe(bddsizehandler handler) *} 2057DESCR {* Reordering is typically done to minimize the global number of 2058 BDD nodes in use, but it may in some cases be usefull to minimize 2059 with respect to a specific BDD. With {\tt bdd\_reorder\_probe} it 2060 is possible to define a callback function that calculates the 2061 size of a specific BDD (or anything else in fact). This handler 2062 will then be called by the reordering functions to get the current 2063 size information. A typical handle could look like this: 2064\begin{verbatim} 2065int sizehandler(void) 2066{ 2067 extern BDD mybdd; 2068 return bdd_nodecount(mybdd); 2069} 2070\end{verbatim} 2071 No default handler is supplied. The argument {\tt handler} may be 2072 NULL if no handler is needed. *} 2073 *} 2074RETURN {* The old handler *} 2075ALSO {* bdd\_reorder *} 2076*/ 2077bddsizehandler bdd_reorder_probe(bddsizehandler handler) 2078{ 2079 bddsizehandler old = reorder_nodenum; 2080 if (handler == NULL) 2081 return reorder_nodenum; 2082 reorder_nodenum = handler; 2083 return old; 2084} 2085 2086 2087/* 2088NAME {* bdd\_clrvarblocks *} 2089SECTION {* reorder *} 2090SHORT {* clears all variable blocks *} 2091PROTO {* void bdd_clrvarblocks(void) *} 2092DESCR {* Clears all the variable blocks that has been defined by calls 2093 to bdd\_addvarblock. *} 2094ALSO {* bdd\_addvarblock *} 2095*/ 2096void bdd_clrvarblocks(void) 2097{ 2098 bddtree_del(vartree); 2099 vartree = NULL; 2100 blockid = 0; 2101} 2102 2103 2104/* 2105NAME {* bdd\_addvarblock *} 2106EXTRA {* bdd\_intaddvarblock *} 2107SECTION {* reorder *} 2108SHORT {* adds a new variable block for reordering *} 2109PROTO {* int bdd_addvarblock(BDD var, int fixed) 2110int bdd_intaddvarblock(int first, int last, int fixed) *} 2111DESCR {* Creates a new variable block with the variables in the variable 2112 set {\tt var}. The variables in {\tt var} must be contiguous. 2113 In the second form the argument {\tt first} is the first variable 2114 included in the block and {\tt last} is the last variable included 2115 in the block. This order does not depend on current variable 2116 order. 2117 2118 The variable blocks are ordered as a tree, with the largest 2119 ranges at top and the smallest at the bottom. Example: Assume 2120 the block 0-9 is added as the first block and then the block 0-6. 2121 This yields the 0-9 block at the top, with the 0-6 block as a 2122 child. If now the block 2-4 was added, it would become a child 2123 of the 0-6 block. A block of 0-8 would be a child of the 0-9 2124 block and have the 0-6 block as a child. Partially overlapping 2125 blocks are not allowed. 2126 2127 The {\tt fixed} parameter sets the block to be fixed (no 2128 reordering of its child blocks is allowed) or free, using 2129 the constants {\tt BDD\_REORDER\_FIXED} and {\tt 2130 BDD\_REORDER\_FREE}. Reordering is always done on the top 2131 most blocks first and then recursively downwards. 2132 2133 The return value is an integer that can be used to identify 2134 the block later on - with for example {\tt bdd\_blockfile\_hook}. 2135 The values returned will be in the sequence $0,1,2,3,\ldots$. 2136 *} 2137RETURN {* A non-negative identifier on success, otherwise a negative error code. *} 2138ALSO {* bdd\_varblockall, fdd\_intaddvarblock, bdd\_clrvarblocks *} */ 2139int bdd_addvarblock(BDD b, int fixed) 2140{ 2141 BddTree *t; 2142 int n, *v, size; 2143 int first, last; 2144 2145 if ((n=bdd_scanset(b, &v, &size)) < 0) 2146 return n; 2147 if (size < 1) 2148 return bdd_error(BDD_VARBLK); 2149 2150 first = last = v[0]; 2151 2152 for (n=0 ; n<size ; n++) 2153 { 2154 if (v[n] < first) 2155 first = v[n]; 2156 if (v[n] > last) 2157 last = v[n]; 2158 } 2159 2160 if ((t=bddtree_addrange(vartree, first,last, fixed,blockid)) == NULL) 2161 return bdd_error(BDD_VARBLK); 2162 2163 vartree = t; 2164 return blockid++; 2165} 2166 2167 2168int bdd_intaddvarblock(int first, int last, int fixed) 2169{ 2170 BddTree *t; 2171 2172 if (first < 0 || first >= bddvarnum || last < 0 || last >= bddvarnum) 2173 return bdd_error(BDD_VAR); 2174 2175 if ((t=bddtree_addrange(vartree, first,last, fixed,blockid)) == NULL) 2176 return bdd_error(BDD_VARBLK); 2177 2178 vartree = t; 2179 return blockid++; 2180} 2181 2182 2183/* 2184NAME {* bdd\_varblockall *} 2185SECTION {* reorder *} 2186SHORT {* add a variable block for all variables *} 2187PROTO {* void bdd_varblockall(void) *} 2188DESCR {* Adds a variable block for all BDD variables declared so far. 2189 Each block contains one variable only. More variable blocks 2190 can be added later with the use of {\tt bdd\_addvarblock} -- 2191 in this case the tree of variable blocks will have the blocks 2192 of single variables as the leafs. *} 2193ALSO {* bdd\_addvarblock, bdd\_intaddvarblock *} 2194*/ 2195void bdd_varblockall(void) 2196{ 2197 int n; 2198 2199 for (n=0 ; n<bddvarnum ; n++) 2200 bdd_intaddvarblock(n,n,1); 2201} 2202 2203 2204/* 2205NAME {* bdd\_printorder *} 2206SECTION {* reorder *} 2207SHORT {* prints the current order *} 2208PROTO {* void bdd_printorder(void) 2209bdd_fprint_order(FILE *f)*} 2210DESCR {* Prints an indented list of the variable blocks, showing the top 2211 most blocks to the left and the lower blocks to the right. 2212 Example:\\ 2213 \begin{verbatim} 2214 2{ 2215 0 2216 1 2217 2} 2218 3 2219 4 2220\end{verbatim} 2221 This shows 5 variable blocks. The first one added is block zero, 2222 which is on the same level as block one. These two blocks are then 2223 sub-blocks of block two and block two is on the same level as 2224 block three and four. The numbers are the identifiers returned 2225 from {\tt bdd\_addvarblock}. The block levels depends on the 2226 variables included in the blocks. 2227 *} 2228ALSO {* bdd\_reorder, bdd\_addvarblock *} 2229*/ 2230void bdd_printorder(void) 2231{ 2232 bdd_fprintorder(stdout); 2233} 2234 2235 2236/* 2237NAME {* bdd\_setvarorder *} 2238SECTION {* reorder *} 2239SHORT {* set a specific variable order *} 2240PROTO {* void bdd_setvarorder(int *neworder) *} 2241DESCR {* This function sets the current variable order to be the one 2242 defined by {\tt neworder}. The parameter {\tt neworder} is 2243 interpreted as a sequence of variable indecies and the new 2244 variable order is exactly this sequence. The array {\em must} 2245 contain all the variables defined so far. If for instance the 2246 current number of variables is 3 and {\tt neworder} contains 2247 $[1,0,2]$ then the new variable order is $v_1 < v_0 < v_2$. *} 2248ALSO {* bdd\_reorder, bdd\_printorder *} 2249*/ 2250void bdd_setvarorder(int *neworder) 2251{ 2252 int level; 2253 2254 /* Do not set order when variable-blocks are used */ 2255 if (vartree != NULL) 2256 { 2257 bdd_error(BDD_VARBLK); 2258 return; 2259 } 2260 2261 reorder_init(); 2262 2263 for (level=0 ; level<bddvarnum ; level++) 2264 { 2265 int lowvar = neworder[level]; 2266 2267 while (bddvar2level[lowvar] > level) 2268 reorder_varup(lowvar); 2269 } 2270 2271 reorder_done(); 2272} 2273 2274 2275static void print_order_rec(FILE *o, BddTree *t, int level) 2276{ 2277 if (t == NULL) 2278 return; 2279 2280 if (t->nextlevel) 2281 { 2282 fprintf(o, "%*s", level*3, ""); 2283 if (reorder_filehandler) 2284 reorder_filehandler(o,t->id); 2285 else 2286 fprintf(o, "%3d", t->id); 2287 fprintf(o, "{\n"); 2288 2289 print_order_rec(o, t->nextlevel, level+1); 2290 2291 fprintf(o, "%*s", level*3, ""); 2292 if (reorder_filehandler) 2293 reorder_filehandler(o,t->id); 2294 else 2295 fprintf(o, "%3d", t->id); 2296 fprintf(o, "}\n"); 2297 2298 print_order_rec(o, t->next, level); 2299 } 2300 else 2301 { 2302 fprintf(o, "%*s", level*3, ""); 2303 if (reorder_filehandler) 2304 reorder_filehandler(o,t->id); 2305 else 2306 fprintf(o, "%3d", t->id); 2307 fprintf(o, "\n"); 2308 2309 print_order_rec(o, t->next, level); 2310 } 2311} 2312 2313 2314 2315void bdd_fprintorder(FILE *ofile) 2316{ 2317 print_order_rec(ofile, vartree, 0); 2318} 2319 2320 2321 2322/* EOF */ 2323