1 /**
2 @file
3
4 @ingroup cudd
5
6 @brief Functions for exact variable reordering.
7
8 @author Cheng Hua, Fabio Somenzi
9
10 @copyright@parblock
11 Copyright (c) 1995-2015, Regents of the University of Colorado
12
13 All rights reserved.
14
15 Redistribution and use in source and binary forms, with or without
16 modification, are permitted provided that the following conditions
17 are met:
18
19 Redistributions of source code must retain the above copyright
20 notice, this list of conditions and the following disclaimer.
21
22 Redistributions in binary form must reproduce the above copyright
23 notice, this list of conditions and the following disclaimer in the
24 documentation and/or other materials provided with the distribution.
25
26 Neither the name of the University of Colorado nor the names of its
27 contributors may be used to endorse or promote products derived from
28 this software without specific prior written permission.
29
30 THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
31 "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
32 LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
33 FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
34 COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
35 INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
36 BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
37 LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
38 CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
39 LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
40 ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
41 POSSIBILITY OF SUCH DAMAGE.
42 @endparblock
43
44 */
45
46 #include "util.h"
47 #include "cuddInt.h"
48
49 /*---------------------------------------------------------------------------*/
50 /* Constant declarations */
51 /*---------------------------------------------------------------------------*/
52
53 /*---------------------------------------------------------------------------*/
54 /* Stucture declarations */
55 /*---------------------------------------------------------------------------*/
56
57 /*---------------------------------------------------------------------------*/
58 /* Type declarations */
59 /*---------------------------------------------------------------------------*/
60
61 /*---------------------------------------------------------------------------*/
62 /* Variable declarations */
63 /*---------------------------------------------------------------------------*/
64
65 /*---------------------------------------------------------------------------*/
66 /* Macro declarations */
67 /*---------------------------------------------------------------------------*/
68
69 /** \cond */
70
71 /*---------------------------------------------------------------------------*/
72 /* Static function prototypes */
73 /*---------------------------------------------------------------------------*/
74
75 static int getMaxBinomial (int n);
76 static DdHalfWord ** getMatrix (int rows, int cols);
77 static void freeMatrix (DdHalfWord **matrix);
78 static int getLevelKeys (DdManager *table, int l);
79 static int ddShuffle (DdManager *table, DdHalfWord *permutation, int lower, int upper);
80 static int ddSiftUp (DdManager *table, int x, int xLow);
81 static int updateUB (DdManager *table, int oldBound, DdHalfWord *bestOrder, int lower, int upper);
82 static int ddCountRoots (DdManager *table, int lower, int upper);
83 static void ddClearGlobal (DdManager *table, int lower, int maxlevel);
84 static int computeLB (DdManager *table, DdHalfWord *order, int roots, int cost, int lower, int upper, int level);
85 static int updateEntry (DdManager *table, DdHalfWord *order, int level, int cost, DdHalfWord **orders, int *costs, int subsets, char *mask, int lower, int upper);
86 static void pushDown (DdHalfWord *order, int j, int level);
87 static DdHalfWord * initSymmInfo (DdManager *table, int lower, int upper);
88 static int checkSymmInfo (DdManager *table, DdHalfWord *symmInfo, int index, int level);
89
90 /** \endcond */
91
92
93 /*---------------------------------------------------------------------------*/
94 /* Definition of exported functions */
95 /*---------------------------------------------------------------------------*/
96
97 /*---------------------------------------------------------------------------*/
98 /* Definition of internal functions */
99 /*---------------------------------------------------------------------------*/
100
101
102 /**
103 @brief Exact variable ordering algorithm.
104
105 @details Finds an optimum order for the variables between lower and
106 upper.
107
108 @return 1 if successful; 0 otherwise.
109
110 @sideeffect None
111
112 */
113 int
cuddExact(DdManager * table,int lower,int upper)114 cuddExact(
115 DdManager * table,
116 int lower,
117 int upper)
118 {
119 int k, i, j;
120 int maxBinomial, oldSubsets, newSubsets;
121 int subsetCost;
122 int size; /* number of variables to be reordered */
123 int unused, nvars, level, result;
124 int upperBound, lowerBound, cost;
125 int roots;
126 char *mask = NULL;
127 DdHalfWord *symmInfo = NULL;
128 DdHalfWord **newOrder = NULL;
129 DdHalfWord **oldOrder = NULL;
130 int *newCost = NULL;
131 int *oldCost = NULL;
132 DdHalfWord **tmpOrder;
133 int *tmpCost;
134 DdHalfWord *bestOrder = NULL;
135 DdHalfWord *order;
136 #ifdef DD_STATS
137 int ddTotalSubsets;
138 #endif
139
140 /* Restrict the range to be reordered by excluding unused variables
141 ** at the two ends. */
142 while (table->subtables[lower].keys == 1 &&
143 table->vars[table->invperm[lower]]->ref == 1 &&
144 lower < upper)
145 lower++;
146 while (table->subtables[upper].keys == 1 &&
147 table->vars[table->invperm[upper]]->ref == 1 &&
148 lower < upper)
149 upper--;
150 if (lower == upper) return(1); /* trivial problem */
151
152 /* Apply symmetric sifting to get a good upper bound and to extract
153 ** symmetry information. */
154 result = cuddSymmSiftingConv(table,lower,upper);
155 if (result == 0) goto cuddExactOutOfMem;
156
157 #ifdef DD_STATS
158 (void) fprintf(table->out,"\n");
159 table->totalShuffles = 0;
160 ddTotalSubsets = 0;
161 #endif
162
163 /* Initialization. */
164 nvars = table->size;
165 size = upper - lower + 1;
166 /* Count unused variable among those to be reordered. This is only
167 ** used to compute maxBinomial. */
168 unused = 0;
169 for (i = lower + 1; i < upper; i++) {
170 if (table->subtables[i].keys == 1 &&
171 table->vars[table->invperm[i]]->ref == 1)
172 unused++;
173 }
174
175 /* Find the maximum number of subsets we may have to store. */
176 maxBinomial = getMaxBinomial(size - unused);
177 if (maxBinomial == -1) goto cuddExactOutOfMem;
178
179 newOrder = getMatrix(maxBinomial, size);
180 if (newOrder == NULL) goto cuddExactOutOfMem;
181
182 newCost = ALLOC(int, maxBinomial);
183 if (newCost == NULL) goto cuddExactOutOfMem;
184
185 oldOrder = getMatrix(maxBinomial, size);
186 if (oldOrder == NULL) goto cuddExactOutOfMem;
187
188 oldCost = ALLOC(int, maxBinomial);
189 if (oldCost == NULL) goto cuddExactOutOfMem;
190
191 bestOrder = ALLOC(DdHalfWord, size);
192 if (bestOrder == NULL) goto cuddExactOutOfMem;
193
194 mask = ALLOC(char, nvars);
195 if (mask == NULL) goto cuddExactOutOfMem;
196
197 symmInfo = initSymmInfo(table, lower, upper);
198 if (symmInfo == NULL) goto cuddExactOutOfMem;
199
200 roots = ddCountRoots(table, lower, upper);
201
202 /* Initialize the old order matrix for the empty subset and the best
203 ** order to the current order. The cost for the empty subset includes
204 ** the cost of the levels between upper and the constants. These levels
205 ** are not going to change. Hence, we count them only once.
206 */
207 oldSubsets = 1;
208 for (i = 0; i < size; i++) {
209 oldOrder[0][i] = bestOrder[i] = (DdHalfWord) table->invperm[i+lower];
210 }
211 subsetCost = (int) table->constants.keys;
212 for (i = upper + 1; i < nvars; i++)
213 subsetCost += getLevelKeys(table,i);
214 oldCost[0] = subsetCost;
215 /* The upper bound is initialized to the current size of the BDDs. */
216 upperBound = (int) (table->keys - table->isolated);
217
218 /* Now consider subsets of increasing size. */
219 for (k = 1; k <= size; k++) {
220 #ifdef DD_STATS
221 (void) fprintf(table->out,"Processing subsets of size %d\n", k);
222 fflush(table->out);
223 #endif
224 newSubsets = 0;
225 level = size - k; /* offset of first bottom variable */
226
227 for (i = 0; i < oldSubsets; i++) { /* for each subset of size k-1 */
228 order = oldOrder[i];
229 cost = oldCost[i];
230 lowerBound = computeLB(table, order, roots, cost, lower, upper,
231 level);
232 if (lowerBound >= upperBound)
233 continue;
234 /* Impose new order. */
235 result = ddShuffle(table, order, lower, upper);
236 if (result == 0) goto cuddExactOutOfMem;
237 upperBound = updateUB(table,upperBound,bestOrder,lower,upper);
238 /* For each top bottom variable. */
239 for (j = level; j >= 0; j--) {
240 /* Skip unused variables. */
241 if (table->subtables[j+lower-1].keys == 1 &&
242 table->vars[table->invperm[j+lower-1]]->ref == 1) continue;
243 /* Find cost under this order. */
244 subsetCost = cost + getLevelKeys(table, lower + level);
245 newSubsets = updateEntry(table, order, level, subsetCost,
246 newOrder, newCost, newSubsets, mask,
247 lower, upper);
248 if (j == 0)
249 break;
250 if (checkSymmInfo(table, symmInfo, (int) order[j-1], level) == 0)
251 continue;
252 pushDown(order,j-1,level);
253 /* Impose new order. */
254 result = ddShuffle(table, order, lower, upper);
255 if (result == 0) goto cuddExactOutOfMem;
256 upperBound = updateUB(table,upperBound,bestOrder,lower,upper);
257 } /* for each bottom variable */
258 } /* for each subset of size k */
259
260 /* New orders become old orders in preparation for next iteration. */
261 tmpOrder = oldOrder; tmpCost = oldCost;
262 oldOrder = newOrder; oldCost = newCost;
263 newOrder = tmpOrder; newCost = tmpCost;
264 #ifdef DD_STATS
265 ddTotalSubsets += newSubsets;
266 #endif
267 oldSubsets = newSubsets;
268 }
269 result = ddShuffle(table, bestOrder, lower, upper);
270 if (result == 0) goto cuddExactOutOfMem;
271 #ifdef DD_STATS
272 #ifdef DD_VERBOSE
273 (void) fprintf(table->out,"\n");
274 #endif
275 (void) fprintf(table->out,"#:S_EXACT %8d: total subsets\n",
276 ddTotalSubsets);
277 (void) fprintf(table->out,"#:H_EXACT %8d: total shuffles",
278 table->totalShuffles);
279 #endif
280
281 freeMatrix(newOrder);
282 freeMatrix(oldOrder);
283 FREE(bestOrder);
284 FREE(oldCost);
285 FREE(newCost);
286 FREE(symmInfo);
287 FREE(mask);
288 return(1);
289
290 cuddExactOutOfMem:
291
292 if (newOrder != NULL) freeMatrix(newOrder);
293 if (oldOrder != NULL) freeMatrix(oldOrder);
294 if (bestOrder != NULL) FREE(bestOrder);
295 if (oldCost != NULL) FREE(oldCost);
296 if (newCost != NULL) FREE(newCost);
297 if (symmInfo != NULL) FREE(symmInfo);
298 if (mask != NULL) FREE(mask);
299 table->errorCode = CUDD_MEMORY_OUT;
300 return(0);
301
302 } /* end of cuddExact */
303
304
305 /**
306 @brief Returns the maximum value of `(n choose k)` for a given `n`.
307
308 @details Computes the maximum value of `(n choose k)` for a given
309 `n`. The maximum value occurs for `k = n/2` when `n` is even, or `k =
310 (n-1)/2` when `n` is odd. The algorithm used in this procedure avoids
311 intermediate overflow problems. It is based on the identity
312
313 binomial(n,k) = n/k * binomial(n-1,k-1).
314
315 @return the computed value if successful; -1 if out of range.
316
317 @sideeffect None
318
319 */
320 static int
getMaxBinomial(int n)321 getMaxBinomial(
322 int n)
323 {
324 double i, j, result;
325
326 if (n < 0 || n > 33) return(-1); /* error */
327 if (n < 2) return(1);
328
329 for (result = (double)((n+3)/2), i = result+1, j=2; i <= n; i++, j++) {
330 result *= i;
331 result /= j;
332 }
333
334 return((int)result);
335
336 } /* end of getMaxBinomial */
337
338
339 #if 0
340 /**
341 @brief Returns the gcd of two integers.
342
343 @details Uses the binary GCD algorithm described in Cormen,
344 Leiserson, and Rivest.
345
346 @sideeffect None
347
348 */
349 static int
350 gcd(
351 int x,
352 int y)
353 {
354 int a;
355 int b;
356 int lsbMask;
357
358 /* GCD(n,0) = n. */
359 if (x == 0) return(y);
360 if (y == 0) return(x);
361
362 a = x; b = y; lsbMask = 1;
363
364 /* Here both a and b are != 0. The iteration maintains this invariant.
365 ** Hence, we only need to check for when they become equal.
366 */
367 while (a != b) {
368 if (a & lsbMask) {
369 if (b & lsbMask) { /* both odd */
370 if (a < b) {
371 b = (b - a) >> 1;
372 } else {
373 a = (a - b) >> 1;
374 }
375 } else { /* a odd, b even */
376 b >>= 1;
377 }
378 } else {
379 if (b & lsbMask) { /* a even, b odd */
380 a >>= 1;
381 } else { /* both even */
382 lsbMask <<= 1;
383 }
384 }
385 }
386
387 return(a);
388
389 } /* end of gcd */
390 #endif
391
392
393 /**
394 @brief Allocates a two-dimensional matrix of ints.
395
396 @return the pointer to the matrix if successful; NULL otherwise.
397
398 @sideeffect None
399
400 @see freeMatrix
401
402 */
403 static DdHalfWord **
getMatrix(int rows,int cols)404 getMatrix(
405 int rows /* number of rows */,
406 int cols /* number of columns */)
407 {
408 DdHalfWord **matrix;
409 int i;
410
411 if (cols*rows == 0) return(NULL);
412 matrix = ALLOC(DdHalfWord *, rows);
413 if (matrix == NULL) return(NULL);
414 matrix[0] = ALLOC(DdHalfWord, cols*rows);
415 if (matrix[0] == NULL) {
416 FREE(matrix);
417 return(NULL);
418 }
419 for (i = 1; i < rows; i++) {
420 matrix[i] = matrix[i-1] + cols;
421 }
422 return(matrix);
423
424 } /* end of getMatrix */
425
426
427 /**
428 @brief Frees a two-dimensional matrix allocated by getMatrix.
429
430 @sideeffect None
431
432 @see getMatrix
433
434 */
435 static void
freeMatrix(DdHalfWord ** matrix)436 freeMatrix(
437 DdHalfWord ** matrix)
438 {
439 FREE(matrix[0]);
440 FREE(matrix);
441 return;
442
443 } /* end of freeMatrix */
444
445
446 /**
447 @brief Returns the number of nodes at one level of a unique table.
448
449 @details The projection function, if isolated, is not counted.
450
451 @sideeffect None
452
453 */
454 static int
getLevelKeys(DdManager * table,int l)455 getLevelKeys(
456 DdManager * table,
457 int l)
458 {
459 int isolated;
460 int x; /* x is an index */
461
462 x = table->invperm[l];
463 isolated = table->vars[x]->ref == 1;
464
465 return((int) table->subtables[l].keys - isolated);
466
467 } /* end of getLevelKeys */
468
469
470 /**
471 @brief Reorders variables according to a given permutation.
472
473 @details The i-th permutation array contains the index of the
474 variable that should be brought to the i-th level. ddShuffle assumes
475 that no dead nodes are present and that the interaction matrix is
476 properly initialized. The reordering is achieved by a series of
477 upward sifts.
478
479 @return 1 if successful; 0 otherwise.
480
481 @sideeffect None
482
483 */
484 static int
ddShuffle(DdManager * table,DdHalfWord * permutation,int lower,int upper)485 ddShuffle(
486 DdManager * table,
487 DdHalfWord * permutation,
488 int lower,
489 int upper)
490 {
491 DdHalfWord index;
492 int level;
493 int position;
494 #if 0
495 int numvars;
496 #endif
497 int result;
498 #if defined(DD_STATS) && defined(DD_VERBOSE)
499 int initialSize;
500 int finalSize;
501 #endif
502
503 #if defined(DD_STATS) && defined(DD_VERBOSE)
504 initialSize = (int) (table->keys - table->isolated);
505 #endif
506
507 #if 0
508 numvars = table->size;
509
510 (void) fprintf(table->out,"%d:", table->totalShuffles);
511 for (level = 0; level < numvars; level++) {
512 (void) fprintf(table->out," %d", table->invperm[level]);
513 }
514 (void) fprintf(table->out,"\n");
515 #endif
516
517 for (level = 0; level <= upper - lower; level++) {
518 index = permutation[level];
519 position = table->perm[index];
520 result = ddSiftUp(table,position,level+lower);
521 if (!result) return(0);
522 }
523
524 #ifdef DD_STATS
525 table->totalShuffles++;
526 #ifdef DD_VERBOSE
527 finalSize = (int) (table->keys - table->isolated);
528 if (finalSize < initialSize) {
529 (void) fprintf(table->out,"-");
530 } else if (finalSize > initialSize) {
531 (void) fprintf(table->out,"+");
532 } else {
533 (void) fprintf(table->out,"=");
534 }
535 if ((table->totalShuffles & 63) == 0) (void) fprintf(table->out,"\n");
536 fflush(table->out);
537 #endif
538 #endif
539
540 return(1);
541
542 } /* end of ddShuffle */
543
544
545 /**
546 @brief Moves one variable up.
547
548 @details Takes a variable from position x and sifts it up to
549 position xLow; xLow should be less than or equal to x.
550
551 @return 1 if successful; 0 otherwise
552
553 @sideeffect None
554
555 */
556 static int
ddSiftUp(DdManager * table,int x,int xLow)557 ddSiftUp(
558 DdManager * table,
559 int x,
560 int xLow)
561 {
562 int y;
563 int size;
564
565 y = cuddNextLow(table,x);
566 while (y >= xLow) {
567 size = cuddSwapInPlace(table,y,x);
568 if (size == 0) {
569 return(0);
570 }
571 x = y;
572 y = cuddNextLow(table,x);
573 }
574 return(1);
575
576 } /* end of ddSiftUp */
577
578
579 /**
580 @brief Updates the upper bound and saves the best order seen so far.
581
582 @return the current value of the upper bound.
583
584 @sideeffect None
585
586 */
587 static int
updateUB(DdManager * table,int oldBound,DdHalfWord * bestOrder,int lower,int upper)588 updateUB(
589 DdManager * table,
590 int oldBound,
591 DdHalfWord * bestOrder,
592 int lower,
593 int upper)
594 {
595 int i;
596 int newBound = (int) (table->keys - table->isolated);
597
598 if (newBound < oldBound) {
599 #ifdef DD_STATS
600 (void) fprintf(table->out,"New upper bound = %d\n", newBound);
601 fflush(table->out);
602 #endif
603 for (i = lower; i <= upper; i++)
604 bestOrder[i-lower] = (DdHalfWord) table->invperm[i];
605 return(newBound);
606 } else {
607 return(oldBound);
608 }
609
610 } /* end of updateUB */
611
612
613 /**
614 @brief Counts the number of roots.
615
616 @details Counts the number of roots at the levels between lower and
617 upper. The computation is based on breadth-first search. A node is
618 a root if it is not reachable from any previously visited node.
619 (All the nodes at level lower are therefore considered roots.) The
620 roots that are constant nodes are always ignored. The visited flag
621 uses the LSB of the next pointer.
622
623 @return the root count.
624
625 @sideeffect None
626
627 @see ddClearGlobal
628
629 */
630 static int
ddCountRoots(DdManager * table,int lower,int upper)631 ddCountRoots(
632 DdManager * table,
633 int lower,
634 int upper)
635 {
636 int i,j;
637 DdNode *f;
638 DdNodePtr *nodelist;
639 DdNode *sentinel = &(table->sentinel);
640 int slots;
641 int roots = 0;
642 int maxlevel = lower;
643
644 for (i = lower; i <= upper; i++) {
645 nodelist = table->subtables[i].nodelist;
646 slots = (int) table->subtables[i].slots;
647 for (j = 0; j < slots; j++) {
648 f = nodelist[j];
649 while (f != sentinel) {
650 /* A node is a root of the DAG if it cannot be
651 ** reached by nodes above it. If a node was never
652 ** reached during the previous depth-first searches,
653 ** then it is a root, and we start a new depth-first
654 ** search from it.
655 */
656 if (!Cudd_IsComplement(f->next)) {
657 if (f != table->vars[f->index]) {
658 roots++;
659 }
660 }
661 if (!cuddIsConstant(cuddT(f))) {
662 cuddT(f)->next = Cudd_Complement(cuddT(f)->next);
663 if (table->perm[cuddT(f)->index] > maxlevel)
664 maxlevel = table->perm[cuddT(f)->index];
665 }
666 if (!Cudd_IsConstantInt(cuddE(f))) {
667 Cudd_Regular(cuddE(f))->next =
668 Cudd_Complement(Cudd_Regular(cuddE(f))->next);
669 if (table->perm[Cudd_Regular(cuddE(f))->index] > maxlevel)
670 maxlevel = table->perm[Cudd_Regular(cuddE(f))->index];
671 }
672 f = Cudd_Regular(f->next);
673 }
674 }
675 }
676 ddClearGlobal(table, lower, maxlevel);
677
678 return(roots);
679
680 } /* end of ddCountRoots */
681
682
683 /**
684 @brief Scans the %DD and clears the LSB of the next pointers.
685
686 @details The LSB of the next pointers are used as markers to tell
687 whether a node was reached. Once the roots are counted, these flags
688 are reset.
689
690 @sideeffect None
691
692 @see ddCountRoots
693
694 */
695 static void
ddClearGlobal(DdManager * table,int lower,int maxlevel)696 ddClearGlobal(
697 DdManager * table,
698 int lower,
699 int maxlevel)
700 {
701 int i,j;
702 DdNode *f;
703 DdNodePtr *nodelist;
704 DdNode *sentinel = &(table->sentinel);
705 int slots;
706
707 for (i = lower; i <= maxlevel; i++) {
708 nodelist = table->subtables[i].nodelist;
709 slots = (int) table->subtables[i].slots;
710 for (j = 0; j < slots; j++) {
711 f = nodelist[j];
712 while (f != sentinel) {
713 f->next = Cudd_Regular(f->next);
714 f = f->next;
715 }
716 }
717 }
718
719 } /* end of ddClearGlobal */
720
721
722 /**
723 @brief Computes a lower bound on the size of a %BDD.
724
725 @details The lower bound depends on the following factors:
726 <ul>
727 <li> size of the lower part of it;
728 <li> size of the part of the upper part not subjected to reordering;
729 <li> number of roots in the part of the %BDD subjected to reordering;
730 <li> variable in the support of the roots in the upper part of the
731 %BDD subjected to reordering.
732 </ul>
733
734 @sideeffect None
735
736 */
737 static int
computeLB(DdManager * table,DdHalfWord * order,int roots,int cost,int lower,int upper,int level)738 computeLB(
739 DdManager * table /**< manager */,
740 DdHalfWord * order /**< optimal order for the subset */,
741 int roots /**< roots between lower and upper */,
742 int cost /**< minimum cost for the subset */,
743 int lower /**< lower level to be reordered */,
744 int upper /**< upper level to be reordered */,
745 int level /**< offset for the current top bottom var */
746 )
747 {
748 int i;
749 int lb = cost;
750 int lb1 = 0;
751 int lb2;
752 int support;
753 DdHalfWord ref;
754
755 /* The levels not involved in reordering are not going to change.
756 ** Add their sizes to the lower bound.
757 */
758 for (i = 0; i < lower; i++) {
759 lb += getLevelKeys(table,i);
760 }
761 /* If a variable is in the support, then there is going
762 ** to be at least one node labeled by that variable.
763 */
764 for (i = lower; i <= lower+level; i++) {
765 support = table->subtables[i].keys > 1 ||
766 table->vars[order[i-lower]]->ref > 1;
767 lb1 += support;
768 }
769
770 /* Estimate the number of nodes required to connect the roots to
771 ** the nodes in the bottom part. */
772 if (lower+level+1 < table->size) {
773 if (lower+level < upper)
774 ref = table->vars[order[level+1]]->ref;
775 else
776 ref = table->vars[table->invperm[upper+1]]->ref;
777 lb2 = (int) table->subtables[lower+level+1].keys -
778 (ref > (DdHalfWord) 1) - roots;
779 } else {
780 lb2 = 0;
781 }
782
783 lb += lb1 > lb2 ? lb1 : lb2;
784
785 return(lb);
786
787 } /* end of computeLB */
788
789
790 /**
791 @brief Updates entry for a subset.
792
793 @details Finds the subset, if it exists. If the new order for the
794 subset has lower cost, or if the subset did not exist, it stores the
795 new order and cost.
796
797 @return the number of subsets currently in the table.
798
799 @sideeffect None
800
801 */
802 static int
updateEntry(DdManager * table,DdHalfWord * order,int level,int cost,DdHalfWord ** orders,int * costs,int subsets,char * mask,int lower,int upper)803 updateEntry(
804 DdManager * table,
805 DdHalfWord * order,
806 int level,
807 int cost,
808 DdHalfWord ** orders,
809 int * costs,
810 int subsets,
811 char * mask,
812 int lower,
813 int upper)
814 {
815 int i, j;
816 int size = upper - lower + 1;
817
818 /* Build a mask that says what variables are in this subset. */
819 for (i = lower; i <= upper; i++)
820 mask[table->invperm[i]] = 0;
821 for (i = level; i < size; i++)
822 mask[order[i]] = 1;
823
824 /* Check each subset until a match is found or all subsets are examined. */
825 for (i = 0; i < subsets; i++) {
826 DdHalfWord *subset = orders[i];
827 for (j = level; j < size; j++) {
828 if (mask[subset[j]] == 0)
829 break;
830 }
831 if (j == size) /* no mismatches: success */
832 break;
833 }
834 if (i == subsets || cost < costs[i]) { /* add or replace */
835 for (j = 0; j < size; j++)
836 orders[i][j] = order[j];
837 costs[i] = cost;
838 subsets += (i == subsets);
839 }
840 return(subsets);
841
842 } /* end of updateEntry */
843
844
845 /**
846 @brief Pushes a variable in the order down to position "level."
847
848 @sideeffect None
849
850 */
851 static void
pushDown(DdHalfWord * order,int j,int level)852 pushDown(
853 DdHalfWord * order,
854 int j,
855 int level)
856 {
857 int i;
858 DdHalfWord tmp;
859
860 tmp = order[j];
861 for (i = j; i < level; i++) {
862 order[i] = order[i+1];
863 }
864 order[level] = tmp;
865 return;
866
867 } /* end of pushDown */
868
869
870 /**
871 @brief Gathers symmetry information.
872
873 @details Translates the symmetry information stored in the next
874 field of each subtable from level to indices. This procedure is called
875 immediately after symmetric sifting, so that the next fields are correct.
876 By translating this informaton in terms of indices, we make it independent
877 of subsequent reorderings. The format used is that of the next fields:
878 a circular list where each variable points to the next variable in the
879 same symmetry group. Only the entries between lower and upper are
880 considered. The procedure returns a pointer to an array
881 holding the symmetry information if successful; NULL otherwise.
882
883 @sideeffect None
884
885 @see checkSymmInfo
886
887 */
888 static DdHalfWord *
initSymmInfo(DdManager * table,int lower,int upper)889 initSymmInfo(
890 DdManager * table,
891 int lower,
892 int upper)
893 {
894 int level, index, next, nextindex;
895 DdHalfWord *symmInfo;
896
897 symmInfo = ALLOC(DdHalfWord, table->size);
898 if (symmInfo == NULL) return(NULL);
899
900 for (level = lower; level <= upper; level++) {
901 index = table->invperm[level];
902 next = (int) table->subtables[level].next;
903 nextindex = table->invperm[next];
904 symmInfo[index] = (DdHalfWord) nextindex;
905 }
906 return(symmInfo);
907
908 } /* end of initSymmInfo */
909
910
911 /**
912 @brief Check symmetry condition.
913
914 @details Returns 1 if a variable is the one with the highest index
915 among those belonging to a symmetry group that are in the top part of
916 the %BDD. The top part is given by level.
917
918 @sideeffect None
919
920 @see initSymmInfo
921
922 */
923 static int
checkSymmInfo(DdManager * table,DdHalfWord * symmInfo,int index,int level)924 checkSymmInfo(
925 DdManager * table,
926 DdHalfWord * symmInfo,
927 int index,
928 int level)
929 {
930 int i;
931
932 i = (int) symmInfo[index];
933 while (i != index) {
934 if (index < i && table->perm[i] <= level)
935 return(0);
936 i = (int) symmInfo[i];
937 }
938 return(1);
939
940 } /* end of checkSymmInfo */
941