1 /*========================================================================
2 Copyright (C) 1996-2002 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: /cvsroot/buddy/buddy/src/reorder.c,v 1.1.1.1 2004/06/25 13:22:59 haimcohen Exp $
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 */
66 static int bddreordermethod;
67 static int bddreordertimes;
68
69 /* Flag for disabling reordering temporarily */
70 static int reorderdisabled;
71
72 /* Store for the variable relationships */
73 static BddTree *vartree;
74 static int blockid;
75
76 /* Store for the ref.cou. of the external roots */
77 static int *extroots;
78 static int extrootsize;
79
80 /* Level data */
81 typedef 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
89 static levelData *levels; /* Indexed by variable! */
90
91 /* Interaction matrix */
92 static imatrix *iactmtx;
93
94 /* Reordering information for the user */
95 static int verbose;
96 static bddinthandler reorder_handler;
97 static bddfilehandler reorder_filehandler;
98 static bddsizehandler reorder_nodenum;
99
100 /* Number of live nodes before and after a reordering session */
101 static int usednum_before;
102 static int usednum_after;
103
104 /* Kernel variables needed for reordering */
105 extern int bddfreepos;
106 extern int bddfreenum;
107 extern int bddproduced;
108
109 /* Flag telling us when a node table resize is done */
110 static 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 */
116 static void blockdown(BddTree *);
117 static void addref_rec(int, char *);
118 static void reorder_gbc();
119 static void reorder_setLevellookup(void);
120 static int reorder_makenode(int, int, int);
121 static int reorder_varup(int);
122 static int reorder_vardown(int);
123 static int reorder_init(void);
124 static void reorder_done(void);
125
126 #define random(a) (rand() % (a))
127
128 /* For sorting the blocks according to some specific size value */
129 typedef struct s_sizePair
130 {
131 int val;
132 BddTree *block;
133 } sizePair;
134
135
136 /*************************************************************************
137 Initialize and shutdown
138 *************************************************************************/
139
bdd_reorder_init(void)140 void 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
bdd_reorder_done(void)155 void 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
reorder_win2(BddTree * t)169 static 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
reorder_win2ite(BddTree * t)209 static 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
reorder_swapwin3(BddTree * this,BddTree ** first)260 static 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
reorder_win3(BddTree * t)394 static 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
reorder_win3ite(BddTree * t)424 static 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 */
reorder_sift_bestpos(BddTree * blk,int middlePos)468 static 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 */
reorder_sift_seq(BddTree * t,BddTree ** seq,int num)573 static 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 */
siftTestCmp(const void * aa,const void * bb)615 static 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 */
reorder_sift(BddTree * t)630 static 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 */
reorder_siftite(BddTree * t)678 static 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
reorder_random(BddTree * t)703 static 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
blockdown(BddTree * left)741 static 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 */
addref_rec(int r,char * dep)810 static 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
addDependencies(char * dep)842 static 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 */
mark_roots(void)864 static 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 */
reorder_gbc(void)923 static 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
reorder_setLevellookup(void)956 static 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
reorder_rehashAll(void)983 static 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 */
reorder_makenode(int var,int low,int high)1019 static 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 */
reorder_downSimple(int var0)1117 static 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 */
reorder_swap(int toBeProcessed,int var0)1170 static 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 */
reorder_localGbc(int var0)1234 static 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
reorder_swapResize(int toBeProcessed,int var0)1279 static 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
reorder_localGbcResize(int toBeProcessed,int var0)1336 static 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
reorder_varup(int var)1401 static 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
1412 static 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
reorder_vardown(int var)1451 static 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 /*
1506 NAME {* bdd\_swapvar *}
1507 SECTION {* reorder *}
1508 SHORT {* Swap two BDD variables *}
1509 PROTO {* int bdd_swapvar(int v1, int v2) *}
1510 DESCR {* 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. *}
1519 RETURN {* Zero on succes and a negative error code otherwise. *}
1520 ALSO {* bdd\_reorder, bdd\_addvarblock *}
1521 */
bdd_swapvar(int v1,int v2)1522 int 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
bdd_default_reohandler(int prestate)1567 void 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 /*
1589 NAME {* bdd\_disable\_reorder *}
1590 SECTION {* reorder *}
1591 SHORT {* Disable automatic reordering *}
1592 PROTO {* void bdd_disable_reorder(void) *}
1593 DESCR {* 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. *}
1596 ALSO {* bdd\_enable\_reorder *}
1597 */
bdd_disable_reorder(void)1598 void bdd_disable_reorder(void)
1599 {
1600 reorderdisabled = 1;
1601 }
1602
1603
1604 /*
1605 NAME {* bdd\_enable\_reorder *}
1606 SECTION {* reorder *}
1607 SHORT {* Enables automatic reordering *}
1608 PROTO {* void bdd_enable_reorder(void) *}
1609 DESCR {* Re-enables reordering after a call to {\tt bdd\_disable\_reorder}. *}
1610 ALSO {* bdd\_disable\_reorder *}
1611 */
bdd_enable_reorder(void)1612 void bdd_enable_reorder(void)
1613 {
1614 reorderdisabled = 0;
1615 }
1616
1617
bdd_reorder_ready(void)1618 int 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
bdd_reorder_auto(void)1627 void 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
reorder_init(void)1643 static 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
reorder_done(void)1672 static 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
varseqCmp(const void * aa,const void * bb)1708 static 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
reorder_block(BddTree * t,int method)1721 static 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 /*
1767 NAME {* bdd\_reorder *}
1768 SECTION {* reorder *}
1769 SHORT {* start dynamic reordering *}
1770 PROTO {* void bdd_reorder(int method) *}
1771 DESCR {* 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 *}
1799 ALSO {* bdd\_autoreorder, bdd\_reorder\_verbose, bdd\_addvarblock, bdd\_clrvarblocks *}
1800 */
bdd_reorder(int method)1801 void 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 /*
1836 NAME {* bdd\_reorder\_gain *}
1837 SECTION {* reorder *}
1838 SHORT {* Calculate the gain in size after a reordering *}
1839 PROTO {* int bdd_reorder_gain(void) *}
1840 DESCR {* 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 */
bdd_reorder_gain(void)1847 int 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 /*
1857 NAME {* bdd\_reorder\_hook *}
1858 SECTION {* reorder *}
1859 SHORT {* sets a handler for automatic reorderings *}
1860 PROTO {* bddinthandler bdd_reorder_hook(bddinthandler handler) *}
1861 DESCR {* 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}
1872 void reorderhandler(int prestate)
1873 {
1874 if (prestate)
1875 printf("Start reordering");
1876 else
1877 printf("End reordering");
1878 }
1879 \end{verbatim} *}
1880 RETURN {* The previous handler *}
1881 ALSO {* bdd\_reorder, bdd\_autoreorder, bdd\_resize\_hook *}
1882 */
bdd_reorder_hook(bddinthandler handler)1883 bddinthandler bdd_reorder_hook(bddinthandler handler)
1884 {
1885 bddinthandler tmp = reorder_handler;
1886 reorder_handler = handler;
1887 return tmp;
1888 }
1889
1890
1891 /*
1892 NAME {* bdd\_blockfile\_hook *}
1893 SECTION {* reorder *}
1894 SHORT {* Specifies a printing callback handler *}
1895 PROTO {* bddfilehandler bdd_blockfile_hook(bddfilehandler handler) *}
1896 DESCR {* 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}
1901 void 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. *}
1913 RETURN {* The old handler *}
1914 ALSO {* bdd\_printorder *}
1915 */
bdd_blockfile_hook(bddfilehandler handler)1916 bddfilehandler bdd_blockfile_hook(bddfilehandler handler)
1917 {
1918 bddfilehandler tmp = reorder_filehandler;
1919 reorder_filehandler = handler;
1920 return tmp;
1921 }
1922
1923
1924 /*
1925 NAME {* bdd\_autoreorder *}
1926 EXTRA {* bdd\_autoreorder\_times *}
1927 SECTION {* reorder *}
1928 SHORT {* enables automatic reordering *}
1929 PROTO {* int bdd_autoreorder(int method)
1930 int bdd_autoreorder_times(int method, int num) *}
1931 DESCR {* 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 *}
1944 RETURN {* Returns the old value of {\tt method} *}
1945 ALSO {* bdd\_reorder *}
1946 */
bdd_autoreorder(int method)1947 int bdd_autoreorder(int method)
1948 {
1949 int tmp = bddreordermethod;
1950 bddreordermethod = method;
1951 bddreordertimes = -1;
1952 return tmp;
1953 }
1954
1955
bdd_autoreorder_times(int method,int num)1956 int 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 /*
1966 NAME {* bdd\_var2level *}
1967 SECTION {* reorder *}
1968 SHORT {* Fetch the level of a specific BDD variable *}
1969 PROTO {* int bdd_var2level(int var) *}
1970 DESCR {* Returns the position of the variable {\tt var} in the current
1971 variable order. *}
1972 ALSO {* bdd\_reorder, bdd\_level2var *}
1973 */
bdd_var2level(int var)1974 int 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 /*
1984 NAME {* bdd\_level2var *}
1985 SECTION {* reorder *}
1986 SHORT {* Fetch the variable number of a specific level *}
1987 PROTO {* int bdd_level2var(int level) *}
1988 DESCR {* Returns the variable placed at position {\tt level} in the
1989 current variable order. *}
1990 ALSO {* bdd\_reorder, bdd\_var2level *}
1991 */
bdd_level2var(int level)1992 int 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 /*
2002 NAME {* bdd\_getreorder\_times *}
2003 SECTION {* reorder *}
2004 SHORT {* Fetch the current number of allowed reorderings *}
2005 PROTO {* int bdd_getreorder_times(void) *}
2006 DESCR {* Returns the current number of allowed reorderings left. This
2007 value can be defined by {\tt bdd\_autoreorder\_times}. *}
2008 ALSO {* bdd\_reorder\_times, bdd\_getreorder\_method *}
2009 */
bdd_getreorder_times(void)2010 int bdd_getreorder_times(void)
2011 {
2012 return bddreordertimes;
2013 }
2014
2015
2016 /*
2017 NAME {* bdd\_getreorder\_method *}
2018 SECTION {* reorder *}
2019 SHORT {* Fetch the current reorder method *}
2020 PROTO {* int bdd_getreorder_method(void) *}
2021 DESCR {* Returns the current reorder method as defined by
2022 {\tt bdd\_autoreorder}. *}
2023 ALSO {* bdd\_reorder, bdd\_getreorder\_times *}
2024 */
bdd_getreorder_method(void)2025 int bdd_getreorder_method(void)
2026 {
2027 return bddreordermethod;
2028 }
2029
2030
2031 /*
2032 NAME {* bdd\_reorder\_verbose *}
2033 SECTION {* reorder *}
2034 SHORT {* enables verbose information about reorderings *}
2035 PROTO {* int bdd_reorder_verbose(int v) *}
2036 DESCR {* 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. *}
2041 RETURN {* The old verbose level *}
2042 ALSO {* bdd\_reorder *}
2043 */
bdd_reorder_verbose(int v)2044 int bdd_reorder_verbose(int v)
2045 {
2046 int tmp = verbose;
2047 verbose = v;
2048 return tmp;
2049 }
2050
2051
2052 /*
2053 NAME {* bdd\_reorder\_probe *}
2054 SECTION {* reorder *}
2055 SHORT {* Define a handler for minimization of BDDs *}
2056 PROTO {* bddsizehandler bdd_reorder_probe(bddsizehandler handler) *}
2057 DESCR {* 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}
2065 int 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 *}
2074 RETURN {* The old handler *}
2075 ALSO {* bdd\_reorder *}
2076 */
bdd_reorder_probe(bddsizehandler handler)2077 bddsizehandler 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 /*
2088 NAME {* bdd\_clrvarblocks *}
2089 SECTION {* reorder *}
2090 SHORT {* clears all variable blocks *}
2091 PROTO {* void bdd_clrvarblocks(void) *}
2092 DESCR {* Clears all the variable blocks that has been defined by calls
2093 to bdd\_addvarblock. *}
2094 ALSO {* bdd\_addvarblock *}
2095 */
bdd_clrvarblocks(void)2096 void bdd_clrvarblocks(void)
2097 {
2098 bddtree_del(vartree);
2099 vartree = NULL;
2100 blockid = 0;
2101 }
2102
2103
2104 /*
2105 NAME {* bdd\_addvarblock *}
2106 EXTRA {* bdd\_intaddvarblock *}
2107 SECTION {* reorder *}
2108 SHORT {* adds a new variable block for reordering *}
2109 PROTO {* int bdd_addvarblock(BDD var, int fixed)
2110 int bdd_intaddvarblock(int first, int last, int fixed) *}
2111 DESCR {* 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 *}
2137 RETURN {* A non-negative identifier on success, otherwise a negative error code. *}
2138 ALSO {* bdd\_varblockall, fdd\_intaddvarblock, bdd\_clrvarblocks *} */
bdd_addvarblock(BDD b,int fixed)2139 int 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
bdd_intaddvarblock(int first,int last,int fixed)2168 int 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 /*
2184 NAME {* bdd\_varblockall *}
2185 SECTION {* reorder *}
2186 SHORT {* add a variable block for all variables *}
2187 PROTO {* void bdd_varblockall(void) *}
2188 DESCR {* 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. *}
2193 ALSO {* bdd\_addvarblock, bdd\_intaddvarblock *}
2194 */
bdd_varblockall(void)2195 void 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 /*
2205 NAME {* bdd\_printorder *}
2206 SECTION {* reorder *}
2207 SHORT {* prints the current order *}
2208 PROTO {* void bdd_printorder(void)
2209 bdd_fprint_order(FILE *f)*}
2210 DESCR {* 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 *}
2228 ALSO {* bdd\_reorder, bdd\_addvarblock *}
2229 */
bdd_printorder(void)2230 void bdd_printorder(void)
2231 {
2232 bdd_fprintorder(stdout);
2233 }
2234
2235
2236 /*
2237 NAME {* bdd\_setvarorder *}
2238 SECTION {* reorder *}
2239 SHORT {* set a specific variable order *}
2240 PROTO {* void bdd_setvarorder(int *neworder) *}
2241 DESCR {* 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$. *}
2248 ALSO {* bdd\_reorder, bdd\_printorder *}
2249 */
bdd_setvarorder(int * neworder)2250 void 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
print_order_rec(FILE * o,BddTree * t,int level)2275 static 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
bdd_fprintorder(FILE * ofile)2315 void bdd_fprintorder(FILE *ofile)
2316 {
2317 print_order_rec(ofile, vartree, 0);
2318 }
2319
2320
2321
2322 /* EOF */
2323