1 /**
2 @file
3
4 @ingroup cudd
5
6 @brief Functions for symmetry-based variable reordering.
7
8 @author Shipra Panda, 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 #define MV_OOM (Move *)1
54
55 /*---------------------------------------------------------------------------*/
56 /* Stucture declarations */
57 /*---------------------------------------------------------------------------*/
58
59 /*---------------------------------------------------------------------------*/
60 /* Type declarations */
61 /*---------------------------------------------------------------------------*/
62
63 /*---------------------------------------------------------------------------*/
64 /* Variable declarations */
65 /*---------------------------------------------------------------------------*/
66
67 /*---------------------------------------------------------------------------*/
68 /* Macro declarations */
69 /*---------------------------------------------------------------------------*/
70
71 /** \cond */
72
73 /*---------------------------------------------------------------------------*/
74 /* Static function prototypes */
75 /*---------------------------------------------------------------------------*/
76
77 static int ddSymmUniqueCompare (void const *ptrX, void const *ptrY);
78 static int ddSymmSiftingAux (DdManager *table, int x, int xLow, int xHigh);
79 static int ddSymmSiftingConvAux (DdManager *table, int x, int xLow, int xHigh);
80 static Move * ddSymmSiftingUp (DdManager *table, int y, int xLow);
81 static Move * ddSymmSiftingDown (DdManager *table, int x, int xHigh);
82 static int ddSymmGroupMove (DdManager *table, int x, int y, Move **moves);
83 static int ddSymmGroupMoveBackward (DdManager *table, int x, int y);
84 static int ddSymmSiftingBackward (DdManager *table, Move *moves, int size);
85 static void ddSymmSummary (DdManager *table, int lower, int upper, int *symvars, int *symgroups);
86
87 /** \endcond */
88
89
90 /*---------------------------------------------------------------------------*/
91 /* Definition of exported functions */
92 /*---------------------------------------------------------------------------*/
93
94
95 /**
96 @brief Prints statistics on symmetric variables.
97
98 @details The information is accurate only if this function is called
99 right after reordering with methods CUDD_REORDER_SYMM_SIFT or
100 CUDD_REORDER_SYMM_SIFT_CONV.
101
102 @sideeffect None
103
104 */
105 void
Cudd_SymmProfile(DdManager * table,int lower,int upper)106 Cudd_SymmProfile(
107 DdManager * table,
108 int lower,
109 int upper)
110 {
111 int i,x,gbot;
112 int TotalSymm = 0;
113 int TotalSymmGroups = 0;
114
115 for (i = lower; i <= upper; i++) {
116 if (table->subtables[i].next != (unsigned) i) {
117 x = i;
118 (void) fprintf(table->out,"Group:");
119 do {
120 (void) fprintf(table->out," %d",table->invperm[x]);
121 TotalSymm++;
122 gbot = x;
123 x = table->subtables[x].next;
124 } while (x != i);
125 TotalSymmGroups++;
126 #ifdef DD_DEBUG
127 assert(table->subtables[gbot].next == (unsigned) i);
128 #endif
129 i = gbot;
130 (void) fprintf(table->out,"\n");
131 }
132 }
133 (void) fprintf(table->out,"Total Symmetric = %d\n",TotalSymm);
134 (void) fprintf(table->out,"Total Groups = %d\n",TotalSymmGroups);
135
136 } /* end of Cudd_SymmProfile */
137
138
139 /*---------------------------------------------------------------------------*/
140 /* Definition of internal functions */
141 /*---------------------------------------------------------------------------*/
142
143
144 /**
145 @brief Checks for symmetry of x and y.
146
147 @details Ignores projection functions, unless they are isolated.
148
149 @return 1 in case of symmetry; 0 otherwise.
150
151 @sideeffect None
152
153 */
154 int
cuddSymmCheck(DdManager * table,int x,int y)155 cuddSymmCheck(
156 DdManager * table,
157 int x,
158 int y)
159 {
160 DdNode *f,*f0,*f1,*f01,*f00,*f11,*f10;
161 int comple; /* f0 is complemented */
162 int xsymmy; /* x and y may be positively symmetric */
163 int xsymmyp; /* x and y may be negatively symmetric */
164 int arccount; /* number of arcs from layer x to layer y */
165 int TotalRefCount; /* total reference count of layer y minus 1 */
166 int yindex;
167 int i;
168 DdNodePtr *list;
169 int slots;
170 DdNode *sentinel = &(table->sentinel);
171 #ifdef DD_DEBUG
172 int xindex;
173 #endif
174
175 /* Checks that x and y are not the projection functions.
176 ** For x it is sufficient to check whether there is only one
177 ** node; indeed, if there is one node, it is the projection function
178 ** and it cannot point to y. Hence, if y isn't just the projection
179 ** function, it has one arc coming from a layer different from x.
180 */
181 if (table->subtables[x].keys == 1) {
182 return(0);
183 }
184 yindex = table->invperm[y];
185 if (table->subtables[y].keys == 1) {
186 if (table->vars[yindex]->ref == 1)
187 return(0);
188 }
189
190 xsymmy = xsymmyp = 1;
191 arccount = 0;
192 slots = table->subtables[x].slots;
193 list = table->subtables[x].nodelist;
194 for (i = 0; i < slots; i++) {
195 f = list[i];
196 while (f != sentinel) {
197 /* Find f1, f0, f11, f10, f01, f00. */
198 f1 = cuddT(f);
199 f0 = Cudd_Regular(cuddE(f));
200 comple = Cudd_IsComplement(cuddE(f));
201 if ((int) f1->index == yindex) {
202 arccount++;
203 f11 = cuddT(f1); f10 = cuddE(f1);
204 } else {
205 if ((int) f0->index != yindex) {
206 /* If f is an isolated projection function it is
207 ** allowed to bypass layer y.
208 */
209 if (f1 != DD_ONE(table) || f0 != DD_ONE(table) || f->ref != 1)
210 return(0); /* f bypasses layer y */
211 }
212 f11 = f10 = f1;
213 }
214 if ((int) f0->index == yindex) {
215 arccount++;
216 f01 = cuddT(f0); f00 = cuddE(f0);
217 } else {
218 f01 = f00 = f0;
219 }
220 if (comple) {
221 f01 = Cudd_Not(f01);
222 f00 = Cudd_Not(f00);
223 }
224
225 if (f1 != DD_ONE(table) || f0 != DD_ONE(table) || f->ref != 1) {
226 xsymmy &= f01 == f10;
227 xsymmyp &= f11 == f00;
228 if ((xsymmy == 0) && (xsymmyp == 0))
229 return(0);
230 }
231
232 f = f->next;
233 } /* while */
234 } /* for */
235
236 /* Calculate the total reference counts of y */
237 TotalRefCount = -1; /* -1 for projection function */
238 slots = table->subtables[y].slots;
239 list = table->subtables[y].nodelist;
240 for (i = 0; i < slots; i++) {
241 f = list[i];
242 while (f != sentinel) {
243 TotalRefCount += f->ref;
244 f = f->next;
245 }
246 }
247
248 #if defined(DD_DEBUG) && defined(DD_VERBOSE)
249 if (arccount == TotalRefCount) {
250 xindex = table->invperm[x];
251 (void) fprintf(table->out,
252 "Found symmetry! x =%d\ty = %d\tPos(%d,%d)\n",
253 xindex,yindex,x,y);
254 }
255 #endif
256
257 return(arccount == TotalRefCount);
258
259 } /* end of cuddSymmCheck */
260
261
262 /**
263 @brief Symmetric sifting algorithm.
264
265 @details Assumes that no dead nodes are present.
266 <ol>
267 <li> Order all the variables according to the number of entries in
268 each unique subtable.
269 <li> Sift the variable up and down, remembering each time the total
270 size of the DD heap and grouping variables that are symmetric.
271 <li> Select the best permutation.
272 <li> Repeat 3 and 4 for all variables.
273 </ol>
274
275 @return 1 plus the number of symmetric variables if successful; 0
276 otherwise.
277
278 @sideeffect None
279
280 @see cuddSymmSiftingConv
281
282 */
283 int
cuddSymmSifting(DdManager * table,int lower,int upper)284 cuddSymmSifting(
285 DdManager * table,
286 int lower,
287 int upper)
288 {
289 int i;
290 IndexKey *var;
291 int size;
292 int x;
293 int result;
294 int symvars;
295 int symgroups;
296 #ifdef DD_STATS
297 int previousSize;
298 #endif
299
300 size = table->size;
301
302 /* Find order in which to sift variables. */
303 var = ALLOC(IndexKey,size);
304 if (var == NULL) {
305 table->errorCode = CUDD_MEMORY_OUT;
306 goto ddSymmSiftingOutOfMem;
307 }
308
309 for (i = 0; i < size; i++) {
310 x = table->perm[i];
311 var[i].index = i;
312 var[i].keys = table->subtables[x].keys;
313 }
314
315 util_qsort(var,size,sizeof(IndexKey),ddSymmUniqueCompare);
316
317 /* Initialize the symmetry of each subtable to itself. */
318 for (i = lower; i <= upper; i++) {
319 table->subtables[i].next = i;
320 }
321
322 for (i = 0; i < ddMin(table->siftMaxVar,size); i++) {
323 if (table->ddTotalNumberSwapping >= table->siftMaxSwap)
324 break;
325 if (util_cpu_time() - table->startTime > table->timeLimit) {
326 table->autoDyn = 0; /* prevent further reordering */
327 break;
328 }
329 if (table->terminationCallback != NULL &&
330 table->terminationCallback(table->tcbArg)) {
331 table->autoDyn = 0; /* prevent further reordering */
332 break;
333 }
334 x = table->perm[var[i].index];
335 #ifdef DD_STATS
336 previousSize = (int) (table->keys - table->isolated);
337 #endif
338 if (x < lower || x > upper) continue;
339 if (table->subtables[x].next == (unsigned) x) {
340 result = ddSymmSiftingAux(table,x,lower,upper);
341 if (!result) goto ddSymmSiftingOutOfMem;
342 #ifdef DD_STATS
343 if (table->keys < (unsigned) previousSize + table->isolated) {
344 (void) fprintf(table->out,"-");
345 } else if (table->keys > (unsigned) previousSize +
346 table->isolated) {
347 (void) fprintf(table->out,"+"); /* should never happen */
348 } else {
349 (void) fprintf(table->out,"=");
350 }
351 fflush(table->out);
352 #endif
353 }
354 }
355
356 FREE(var);
357
358 ddSymmSummary(table, lower, upper, &symvars, &symgroups);
359
360 #ifdef DD_STATS
361 (void) fprintf(table->out, "\n#:S_SIFTING %8d: symmetric variables\n",
362 symvars);
363 (void) fprintf(table->out, "#:G_SIFTING %8d: symmetric groups",
364 symgroups);
365 #endif
366
367 return(1+symvars);
368
369 ddSymmSiftingOutOfMem:
370
371 if (var != NULL) FREE(var);
372
373 return(0);
374
375 } /* end of cuddSymmSifting */
376
377
378 /**
379 @brief Symmetric sifting to convergence algorithm.
380
381 @details Assumes that no dead nodes are present.
382 <ol>
383 <li> Order all the variables according to the number of entries in
384 each unique subtable.
385 <li> Sift the variable up and down, remembering each time the total
386 size of the %DD heap and grouping variables that are symmetric.
387 <li> Select the best permutation.
388 <li> Repeat 3 and 4 for all variables.
389 <li> Repeat 1-4 until no further improvement.
390 </ol>
391
392 @return 1 plus the number of symmetric variables if successful; 0
393 otherwise.
394
395 @sideeffect None
396
397 @see cuddSymmSifting
398
399 */
400 int
cuddSymmSiftingConv(DdManager * table,int lower,int upper)401 cuddSymmSiftingConv(
402 DdManager * table,
403 int lower,
404 int upper)
405 {
406 int i;
407 IndexKey *var;
408 int size;
409 int x;
410 int result;
411 int symvars;
412 int symgroups;
413 int classes;
414 int initialSize;
415 #ifdef DD_STATS
416 int previousSize;
417 #endif
418
419 initialSize = (int) (table->keys - table->isolated);
420
421 size = table->size;
422
423 /* Find order in which to sift variables. */
424 var = ALLOC(IndexKey,size);
425 if (var == NULL) {
426 table->errorCode = CUDD_MEMORY_OUT;
427 goto ddSymmSiftingConvOutOfMem;
428 }
429
430 for (i = 0; i < size; i++) {
431 x = table->perm[i];
432 var[i].index = i;
433 var[i].keys = table->subtables[x].keys;
434 }
435
436 util_qsort(var,size,sizeof(IndexKey),ddSymmUniqueCompare);
437
438 /* Initialize the symmetry of each subtable to itself
439 ** for first pass of converging symmetric sifting.
440 */
441 for (i = lower; i <= upper; i++) {
442 table->subtables[i].next = i;
443 }
444
445 for (i = 0; i < ddMin(table->siftMaxVar, table->size); i++) {
446 if (table->ddTotalNumberSwapping >= table->siftMaxSwap)
447 break;
448 if (util_cpu_time() - table->startTime > table->timeLimit) {
449 table->autoDyn = 0; /* prevent further reordering */
450 break;
451 }
452 if (table->terminationCallback != NULL &&
453 table->terminationCallback(table->tcbArg)) {
454 table->autoDyn = 0; /* prevent further reordering */
455 break;
456 }
457 x = table->perm[var[i].index];
458 if (x < lower || x > upper) continue;
459 /* Only sift if not in symmetry group already. */
460 if (table->subtables[x].next == (unsigned) x) {
461 #ifdef DD_STATS
462 previousSize = (int) (table->keys - table->isolated);
463 #endif
464 result = ddSymmSiftingAux(table,x,lower,upper);
465 if (!result) goto ddSymmSiftingConvOutOfMem;
466 #ifdef DD_STATS
467 if (table->keys < (unsigned) previousSize + table->isolated) {
468 (void) fprintf(table->out,"-");
469 } else if (table->keys > (unsigned) previousSize +
470 table->isolated) {
471 (void) fprintf(table->out,"+");
472 } else {
473 (void) fprintf(table->out,"=");
474 }
475 fflush(table->out);
476 #endif
477 }
478 }
479
480 /* Sifting now until convergence. */
481 while ((unsigned) initialSize > table->keys - table->isolated) {
482 initialSize = (int) (table->keys - table->isolated);
483 #ifdef DD_STATS
484 (void) fprintf(table->out,"\n");
485 #endif
486 /* Here we consider only one representative for each symmetry class. */
487 for (x = lower, classes = 0; x <= upper; x++, classes++) {
488 while ((unsigned) x < table->subtables[x].next) {
489 x = table->subtables[x].next;
490 }
491 /* Here x is the largest index in a group.
492 ** Groups consist of adjacent variables.
493 ** Hence, the next increment of x will move it to a new group.
494 */
495 i = table->invperm[x];
496 var[classes].keys = table->subtables[x].keys;
497 var[classes].index = i;
498 }
499
500 util_qsort(var,classes,sizeof(IndexKey),ddSymmUniqueCompare);
501
502 /* Now sift. */
503 for (i = 0; i < ddMin(table->siftMaxVar,classes); i++) {
504 if (table->ddTotalNumberSwapping >= table->siftMaxSwap)
505 break;
506 if (util_cpu_time() - table->startTime > table->timeLimit) {
507 table->autoDyn = 0; /* prevent further reordering */
508 break;
509 }
510 if (table->terminationCallback != NULL &&
511 table->terminationCallback(table->tcbArg)) {
512 table->autoDyn = 0; /* prevent further reordering */
513 break;
514 }
515 x = table->perm[var[i].index];
516 if ((unsigned) x >= table->subtables[x].next) {
517 #ifdef DD_STATS
518 previousSize = (int) (table->keys - table->isolated);
519 #endif
520 result = ddSymmSiftingConvAux(table,x,lower,upper);
521 if (!result ) goto ddSymmSiftingConvOutOfMem;
522 #ifdef DD_STATS
523 if (table->keys < (unsigned) previousSize + table->isolated) {
524 (void) fprintf(table->out,"-");
525 } else if (table->keys > (unsigned) previousSize +
526 table->isolated) {
527 (void) fprintf(table->out,"+");
528 } else {
529 (void) fprintf(table->out,"=");
530 }
531 fflush(table->out);
532 #endif
533 }
534 } /* for */
535 }
536
537 ddSymmSummary(table, lower, upper, &symvars, &symgroups);
538
539 #ifdef DD_STATS
540 (void) fprintf(table->out, "\n#:S_SIFTING %8d: symmetric variables\n",
541 symvars);
542 (void) fprintf(table->out, "#:G_SIFTING %8d: symmetric groups",
543 symgroups);
544 #endif
545
546 FREE(var);
547
548 return(1+symvars);
549
550 ddSymmSiftingConvOutOfMem:
551
552 if (var != NULL) FREE(var);
553
554 return(0);
555
556 } /* end of cuddSymmSiftingConv */
557
558
559 /*---------------------------------------------------------------------------*/
560 /* Definition of static functions */
561 /*---------------------------------------------------------------------------*/
562
563
564 /**
565 @brief Comparison function used by qsort.
566
567 @details Used to order the variables according to the number of keys
568 in the subtables.
569
570 @return the difference in number of keys between the two variables
571 being compared.
572
573 @sideeffect None
574
575 */
576 static int
ddSymmUniqueCompare(void const * ptrX,void const * ptrY)577 ddSymmUniqueCompare(
578 void const * ptrX,
579 void const * ptrY)
580 {
581 IndexKey const * pX = (IndexKey const *) ptrX;
582 IndexKey const * pY = (IndexKey const *) ptrY;
583 #if 0
584 if (pY->keys == pX->keys) {
585 return(pX->index - pY->index);
586 }
587 #endif
588 return(pY->keys - pX->keys);
589
590 } /* end of ddSymmUniqueCompare */
591
592
593 /**
594 @brief Given xLow <= x <= xHigh moves x up and down between the
595 boundaries.
596
597 @details Finds the best position and does the required changes.
598 Assumes that x is not part of a symmetry group.
599
600 @return 1 if successful; 0 otherwise.
601
602 @sideeffect None
603
604 */
605 static int
ddSymmSiftingAux(DdManager * table,int x,int xLow,int xHigh)606 ddSymmSiftingAux(
607 DdManager * table,
608 int x,
609 int xLow,
610 int xHigh)
611 {
612 Move *move;
613 Move *moveUp; /* list of up moves */
614 Move *moveDown; /* list of down moves */
615 int initialSize;
616 int result;
617 int i;
618 int topbot; /* index to either top or bottom of symmetry group */
619 int initGroupSize, finalGroupSize;
620
621
622 #ifdef DD_DEBUG
623 /* check for previously detected symmetry */
624 assert(table->subtables[x].next == (unsigned) x);
625 #endif
626
627 initialSize = (int) (table->keys - table->isolated);
628
629 moveDown = NULL;
630 moveUp = NULL;
631
632 if ((x - xLow) > (xHigh - x)) {
633 /* Will go down first, unless x == xHigh:
634 ** Look for consecutive symmetries above x.
635 */
636 for (i = x; i > xLow; i--) {
637 if (!cuddSymmCheck(table,i-1,i))
638 break;
639 topbot = table->subtables[i-1].next; /* find top of i-1's group */
640 table->subtables[i-1].next = i;
641 table->subtables[x].next = topbot; /* x is bottom of group so its */
642 /* next is top of i-1's group */
643 i = topbot + 1; /* add 1 for i--; new i is top of symm group */
644 }
645 } else {
646 /* Will go up first unless x == xlow:
647 ** Look for consecutive symmetries below x.
648 */
649 for (i = x; i < xHigh; i++) {
650 if (!cuddSymmCheck(table,i,i+1))
651 break;
652 /* find bottom of i+1's symm group */
653 topbot = i + 1;
654 while ((unsigned) topbot < table->subtables[topbot].next) {
655 topbot = table->subtables[topbot].next;
656 }
657 table->subtables[topbot].next = table->subtables[i].next;
658 table->subtables[i].next = i + 1;
659 i = topbot - 1; /* subtract 1 for i++; new i is bottom of group */
660 }
661 }
662
663 /* Now x may be in the middle of a symmetry group.
664 ** Find bottom of x's symm group.
665 */
666 while ((unsigned) x < table->subtables[x].next)
667 x = table->subtables[x].next;
668
669 if (x == xLow) { /* Sift down */
670
671 #ifdef DD_DEBUG
672 /* x must be a singleton */
673 assert((unsigned) x == table->subtables[x].next);
674 #endif
675 if (x == xHigh) return(1); /* just one variable */
676
677 initGroupSize = 1;
678
679 moveDown = ddSymmSiftingDown(table,x,xHigh);
680 /* after this point x --> xHigh, unless early term */
681 if (moveDown == MV_OOM) goto ddSymmSiftingAuxOutOfMem;
682 if (moveDown == NULL) return(1);
683
684 x = moveDown->y;
685 /* Find bottom of x's group */
686 i = x;
687 while ((unsigned) i < table->subtables[i].next) {
688 i = table->subtables[i].next;
689 }
690 #ifdef DD_DEBUG
691 /* x should be the top of the symmetry group and i the bottom */
692 assert((unsigned) i >= table->subtables[i].next);
693 assert((unsigned) x == table->subtables[i].next);
694 #endif
695 finalGroupSize = i - x + 1;
696
697 if (initGroupSize == finalGroupSize) {
698 /* No new symmetry groups detected, return to best position */
699 result = ddSymmSiftingBackward(table,moveDown,initialSize);
700 } else {
701 initialSize = (int) (table->keys - table->isolated);
702 moveUp = ddSymmSiftingUp(table,x,xLow);
703 result = ddSymmSiftingBackward(table,moveUp,initialSize);
704 }
705 if (!result) goto ddSymmSiftingAuxOutOfMem;
706
707 } else if (cuddNextHigh(table,x) > xHigh) { /* Sift up */
708 /* Find top of x's symm group */
709 i = x; /* bottom */
710 x = table->subtables[x].next; /* top */
711
712 if (x == xLow) return(1); /* just one big group */
713
714 initGroupSize = i - x + 1;
715
716 moveUp = ddSymmSiftingUp(table,x,xLow);
717 /* after this point x --> xLow, unless early term */
718 if (moveUp == MV_OOM) goto ddSymmSiftingAuxOutOfMem;
719 if (moveUp == NULL) return(1);
720
721 x = moveUp->x;
722 /* Find top of x's group */
723 i = table->subtables[x].next;
724 #ifdef DD_DEBUG
725 /* x should be the bottom of the symmetry group and i the top */
726 assert((unsigned) x >= table->subtables[x].next);
727 assert((unsigned) i == table->subtables[x].next);
728 #endif
729 finalGroupSize = x - i + 1;
730
731 if (initGroupSize == finalGroupSize) {
732 /* No new symmetry groups detected, return to best position */
733 result = ddSymmSiftingBackward(table,moveUp,initialSize);
734 } else {
735 initialSize = (int) (table->keys - table->isolated);
736 moveDown = ddSymmSiftingDown(table,x,xHigh);
737 result = ddSymmSiftingBackward(table,moveDown,initialSize);
738 }
739 if (!result) goto ddSymmSiftingAuxOutOfMem;
740
741 } else if ((x - xLow) > (xHigh - x)) { /* must go down first: shorter */
742
743 moveDown = ddSymmSiftingDown(table,x,xHigh);
744 /* at this point x == xHigh, unless early term */
745 if (moveDown == MV_OOM) goto ddSymmSiftingAuxOutOfMem;
746
747 if (moveDown != NULL) {
748 x = moveDown->y; /* x is top here */
749 i = x;
750 while ((unsigned) i < table->subtables[i].next) {
751 i = table->subtables[i].next;
752 }
753 } else {
754 i = x;
755 while ((unsigned) i < table->subtables[i].next) {
756 i = table->subtables[i].next;
757 }
758 x = table->subtables[i].next;
759 }
760 #ifdef DD_DEBUG
761 /* x should be the top of the symmetry group and i the bottom */
762 assert((unsigned) i >= table->subtables[i].next);
763 assert((unsigned) x == table->subtables[i].next);
764 #endif
765 initGroupSize = i - x + 1;
766
767 moveUp = ddSymmSiftingUp(table,x,xLow);
768 if (moveUp == MV_OOM) goto ddSymmSiftingAuxOutOfMem;
769
770 if (moveUp != NULL) {
771 x = moveUp->x;
772 i = table->subtables[x].next;
773 } else {
774 i = x;
775 while ((unsigned) x < table->subtables[x].next)
776 x = table->subtables[x].next;
777 }
778 #ifdef DD_DEBUG
779 /* x should be the bottom of the symmetry group and i the top */
780 assert((unsigned) x >= table->subtables[x].next);
781 assert((unsigned) i == table->subtables[x].next);
782 #endif
783 finalGroupSize = x - i + 1;
784
785 if (initGroupSize == finalGroupSize) {
786 /* No new symmetry groups detected, return to best position */
787 result = ddSymmSiftingBackward(table,moveUp,initialSize);
788 } else {
789 while (moveDown != NULL) {
790 move = moveDown->next;
791 cuddDeallocMove(table, moveDown);
792 moveDown = move;
793 }
794 initialSize = (int) (table->keys - table->isolated);
795 moveDown = ddSymmSiftingDown(table,x,xHigh);
796 result = ddSymmSiftingBackward(table,moveDown,initialSize);
797 }
798 if (!result) goto ddSymmSiftingAuxOutOfMem;
799
800 } else { /* moving up first: shorter */
801 /* Find top of x's symmetry group */
802 x = table->subtables[x].next;
803
804 moveUp = ddSymmSiftingUp(table,x,xLow);
805 /* at this point x == xHigh, unless early term */
806 if (moveUp == MV_OOM) goto ddSymmSiftingAuxOutOfMem;
807
808 if (moveUp != NULL) {
809 x = moveUp->x;
810 i = table->subtables[x].next;
811 } else {
812 while ((unsigned) x < table->subtables[x].next)
813 x = table->subtables[x].next;
814 i = table->subtables[x].next;
815 }
816 #ifdef DD_DEBUG
817 /* x is bottom of the symmetry group and i is top */
818 assert((unsigned) x >= table->subtables[x].next);
819 assert((unsigned) i == table->subtables[x].next);
820 #endif
821 initGroupSize = x - i + 1;
822
823 moveDown = ddSymmSiftingDown(table,x,xHigh);
824 if (moveDown == MV_OOM) goto ddSymmSiftingAuxOutOfMem;
825
826 if (moveDown != NULL) {
827 x = moveDown->y;
828 i = x;
829 while ((unsigned) i < table->subtables[i].next) {
830 i = table->subtables[i].next;
831 }
832 } else {
833 i = x;
834 x = table->subtables[x].next;
835 }
836 #ifdef DD_DEBUG
837 /* x should be the top of the symmetry group and i the bottom */
838 assert((unsigned) i >= table->subtables[i].next);
839 assert((unsigned) x == table->subtables[i].next);
840 #endif
841 finalGroupSize = i - x + 1;
842
843 if (initGroupSize == finalGroupSize) {
844 /* No new symmetries detected, go back to best position */
845 result = ddSymmSiftingBackward(table,moveDown,initialSize);
846 } else {
847 while (moveUp != NULL) {
848 move = moveUp->next;
849 cuddDeallocMove(table, moveUp);
850 moveUp = move;
851 }
852 initialSize = (int) (table->keys - table->isolated);
853 moveUp = ddSymmSiftingUp(table,x,xLow);
854 result = ddSymmSiftingBackward(table,moveUp,initialSize);
855 }
856 if (!result) goto ddSymmSiftingAuxOutOfMem;
857 }
858
859 while (moveDown != NULL) {
860 move = moveDown->next;
861 cuddDeallocMove(table, moveDown);
862 moveDown = move;
863 }
864 while (moveUp != NULL) {
865 move = moveUp->next;
866 cuddDeallocMove(table, moveUp);
867 moveUp = move;
868 }
869
870 return(1);
871
872 ddSymmSiftingAuxOutOfMem:
873 if (moveDown != MV_OOM) {
874 while (moveDown != NULL) {
875 move = moveDown->next;
876 cuddDeallocMove(table, moveDown);
877 moveDown = move;
878 }
879 }
880 if (moveUp != MV_OOM) {
881 while (moveUp != NULL) {
882 move = moveUp->next;
883 cuddDeallocMove(table, moveUp);
884 moveUp = move;
885 }
886 }
887
888 return(0);
889
890 } /* end of ddSymmSiftingAux */
891
892
893 /**
894 @brief Given xLow <= x <= xHigh moves x up and down between the
895 boundaries.
896
897 @details Finds the best position and does the required changes.
898 Assumes that x is either an isolated variable, or it is the bottom of
899 a symmetry group. All symmetries may not have been found, because of
900 exceeded growth limit.
901
902 @return 1 if successful; 0 otherwise.
903
904 @sideeffect None
905
906 */
907 static int
ddSymmSiftingConvAux(DdManager * table,int x,int xLow,int xHigh)908 ddSymmSiftingConvAux(
909 DdManager * table,
910 int x,
911 int xLow,
912 int xHigh)
913 {
914 Move *move;
915 Move *moveUp; /* list of up moves */
916 Move *moveDown; /* list of down moves */
917 int initialSize;
918 int result;
919 int i;
920 int initGroupSize, finalGroupSize;
921
922
923 initialSize = (int) (table->keys - table->isolated);
924
925 moveDown = NULL;
926 moveUp = NULL;
927
928 if (x == xLow) { /* Sift down */
929 #ifdef DD_DEBUG
930 /* x is bottom of symmetry group */
931 assert((unsigned) x >= table->subtables[x].next);
932 #endif
933 i = table->subtables[x].next;
934 initGroupSize = x - i + 1;
935
936 moveDown = ddSymmSiftingDown(table,x,xHigh);
937 /* at this point x == xHigh, unless early term */
938 if (moveDown == MV_OOM) goto ddSymmSiftingConvAuxOutOfMem;
939 if (moveDown == NULL) return(1);
940
941 x = moveDown->y;
942 i = x;
943 while ((unsigned) i < table->subtables[i].next) {
944 i = table->subtables[i].next;
945 }
946 #ifdef DD_DEBUG
947 /* x should be the top of the symmetric group and i the bottom */
948 assert((unsigned) i >= table->subtables[i].next);
949 assert((unsigned) x == table->subtables[i].next);
950 #endif
951 finalGroupSize = i - x + 1;
952
953 if (initGroupSize == finalGroupSize) {
954 /* No new symmetries detected, go back to best position */
955 result = ddSymmSiftingBackward(table,moveDown,initialSize);
956 } else {
957 initialSize = (int) (table->keys - table->isolated);
958 moveUp = ddSymmSiftingUp(table,x,xLow);
959 result = ddSymmSiftingBackward(table,moveUp,initialSize);
960 }
961 if (!result) goto ddSymmSiftingConvAuxOutOfMem;
962
963 } else if (cuddNextHigh(table,x) > xHigh) { /* Sift up */
964 /* Find top of x's symm group */
965 while ((unsigned) x < table->subtables[x].next)
966 x = table->subtables[x].next;
967 i = x; /* bottom */
968 x = table->subtables[x].next; /* top */
969
970 if (x == xLow) return(1);
971
972 initGroupSize = i - x + 1;
973
974 moveUp = ddSymmSiftingUp(table,x,xLow);
975 /* at this point x == xLow, unless early term */
976 if (moveUp == MV_OOM) goto ddSymmSiftingConvAuxOutOfMem;
977 if (moveUp == NULL) return(1);
978
979 x = moveUp->x;
980 i = table->subtables[x].next;
981 #ifdef DD_DEBUG
982 /* x should be the bottom of the symmetry group and i the top */
983 assert((unsigned) x >= table->subtables[x].next);
984 assert((unsigned) i == table->subtables[x].next);
985 #endif
986 finalGroupSize = x - i + 1;
987
988 if (initGroupSize == finalGroupSize) {
989 /* No new symmetry groups detected, return to best position */
990 result = ddSymmSiftingBackward(table,moveUp,initialSize);
991 } else {
992 initialSize = (int) (table->keys - table->isolated);
993 moveDown = ddSymmSiftingDown(table,x,xHigh);
994 result = ddSymmSiftingBackward(table,moveDown,initialSize);
995 }
996 if (!result)
997 goto ddSymmSiftingConvAuxOutOfMem;
998
999 } else if ((x - xLow) > (xHigh - x)) { /* must go down first: shorter */
1000 moveDown = ddSymmSiftingDown(table,x,xHigh);
1001 /* at this point x == xHigh, unless early term */
1002 if (moveDown == MV_OOM) goto ddSymmSiftingConvAuxOutOfMem;
1003
1004 if (moveDown != NULL) {
1005 x = moveDown->y;
1006 i = x;
1007 while ((unsigned) i < table->subtables[i].next) {
1008 i = table->subtables[i].next;
1009 }
1010 } else {
1011 while ((unsigned) x < table->subtables[x].next)
1012 x = table->subtables[x].next;
1013 i = x;
1014 x = table->subtables[x].next;
1015 }
1016 #ifdef DD_DEBUG
1017 /* x should be the top of the symmetry group and i the bottom */
1018 assert((unsigned) i >= table->subtables[i].next);
1019 assert((unsigned) x == table->subtables[i].next);
1020 #endif
1021 initGroupSize = i - x + 1;
1022
1023 moveUp = ddSymmSiftingUp(table,x,xLow);
1024 if (moveUp == MV_OOM) goto ddSymmSiftingConvAuxOutOfMem;
1025
1026 if (moveUp != NULL) {
1027 x = moveUp->x;
1028 i = table->subtables[x].next;
1029 } else {
1030 i = x;
1031 while ((unsigned) x < table->subtables[x].next)
1032 x = table->subtables[x].next;
1033 }
1034 #ifdef DD_DEBUG
1035 /* x should be the bottom of the symmetry group and i the top */
1036 assert((unsigned) x >= table->subtables[x].next);
1037 assert((unsigned) i == table->subtables[x].next);
1038 #endif
1039 finalGroupSize = x - i + 1;
1040
1041 if (initGroupSize == finalGroupSize) {
1042 /* No new symmetry groups detected, return to best position */
1043 result = ddSymmSiftingBackward(table,moveUp,initialSize);
1044 } else {
1045 while (moveDown != NULL) {
1046 move = moveDown->next;
1047 cuddDeallocMove(table, moveDown);
1048 moveDown = move;
1049 }
1050 initialSize = (int) (table->keys - table->isolated);
1051 moveDown = ddSymmSiftingDown(table,x,xHigh);
1052 result = ddSymmSiftingBackward(table,moveDown,initialSize);
1053 }
1054 if (!result) goto ddSymmSiftingConvAuxOutOfMem;
1055
1056 } else { /* moving up first: shorter */
1057 /* Find top of x's symmetry group */
1058 x = table->subtables[x].next;
1059
1060 moveUp = ddSymmSiftingUp(table,x,xLow);
1061 /* at this point x == xHigh, unless early term */
1062 if (moveUp == MV_OOM) goto ddSymmSiftingConvAuxOutOfMem;
1063
1064 if (moveUp != NULL) {
1065 x = moveUp->x;
1066 i = table->subtables[x].next;
1067 } else {
1068 i = x;
1069 while ((unsigned) x < table->subtables[x].next)
1070 x = table->subtables[x].next;
1071 }
1072 #ifdef DD_DEBUG
1073 /* x is bottom of the symmetry group and i is top */
1074 assert((unsigned) x >= table->subtables[x].next);
1075 assert((unsigned) i == table->subtables[x].next);
1076 #endif
1077 initGroupSize = x - i + 1;
1078
1079 moveDown = ddSymmSiftingDown(table,x,xHigh);
1080 if (moveDown == MV_OOM) goto ddSymmSiftingConvAuxOutOfMem;
1081
1082 if (moveDown != NULL) {
1083 x = moveDown->y;
1084 i = x;
1085 while ((unsigned) i < table->subtables[i].next) {
1086 i = table->subtables[i].next;
1087 }
1088 } else {
1089 i = x;
1090 x = table->subtables[x].next;
1091 }
1092 #ifdef DD_DEBUG
1093 /* x should be the top of the symmetry group and i the bottom */
1094 assert((unsigned) i >= table->subtables[i].next);
1095 assert((unsigned) x == table->subtables[i].next);
1096 #endif
1097 finalGroupSize = i - x + 1;
1098
1099 if (initGroupSize == finalGroupSize) {
1100 /* No new symmetries detected, go back to best position */
1101 result = ddSymmSiftingBackward(table,moveDown,initialSize);
1102 } else {
1103 while (moveUp != NULL) {
1104 move = moveUp->next;
1105 cuddDeallocMove(table, moveUp);
1106 moveUp = move;
1107 }
1108 initialSize = (int) (table->keys - table->isolated);
1109 moveUp = ddSymmSiftingUp(table,x,xLow);
1110 result = ddSymmSiftingBackward(table,moveUp,initialSize);
1111 }
1112 if (!result) goto ddSymmSiftingConvAuxOutOfMem;
1113 }
1114
1115 while (moveDown != NULL) {
1116 move = moveDown->next;
1117 cuddDeallocMove(table, moveDown);
1118 moveDown = move;
1119 }
1120 while (moveUp != NULL) {
1121 move = moveUp->next;
1122 cuddDeallocMove(table, moveUp);
1123 moveUp = move;
1124 }
1125
1126 return(1);
1127
1128 ddSymmSiftingConvAuxOutOfMem:
1129 if (moveDown != MV_OOM) {
1130 while (moveDown != NULL) {
1131 move = moveDown->next;
1132 cuddDeallocMove(table, moveDown);
1133 moveDown = move;
1134 }
1135 }
1136 if (moveUp != MV_OOM) {
1137 while (moveUp != NULL) {
1138 move = moveUp->next;
1139 cuddDeallocMove(table, moveUp);
1140 moveUp = move;
1141 }
1142 }
1143
1144 return(0);
1145
1146 } /* end of ddSymmSiftingConvAux */
1147
1148
1149 /**
1150 @brief Moves x up until either it reaches the bound (xLow) or
1151 the size of the %DD heap increases too much.
1152
1153 @details Assumes that x is the top of a symmetry group. Checks x
1154 for symmetry to the adjacent variables. If symmetry is found, the
1155 symmetry group of x is merged with the symmetry group of the other
1156 variable.
1157
1158 @return the set of moves in case of success; MV_OOM if memory is
1159 full.
1160
1161 @sideeffect None
1162
1163 */
1164 static Move *
ddSymmSiftingUp(DdManager * table,int y,int xLow)1165 ddSymmSiftingUp(
1166 DdManager * table,
1167 int y,
1168 int xLow)
1169 {
1170 Move *moves;
1171 Move *move;
1172 int x;
1173 int size;
1174 int i;
1175 int gxtop,gybot;
1176 int limitSize;
1177 int xindex, yindex;
1178 int zindex;
1179 int z;
1180 int isolated;
1181 int L; /* lower bound on DD size */
1182 #ifdef DD_DEBUG
1183 int checkL;
1184 #endif
1185
1186
1187 moves = NULL;
1188 yindex = table->invperm[y];
1189
1190 /* Initialize the lower bound.
1191 ** The part of the DD below the bottom of y' group will not change.
1192 ** The part of the DD above y that does not interact with y will not
1193 ** change. The rest may vanish in the best case, except for
1194 ** the nodes at level xLow, which will not vanish, regardless.
1195 */
1196 limitSize = L = (int) (table->keys - table->isolated);
1197 gybot = y;
1198 while ((unsigned) gybot < table->subtables[gybot].next)
1199 gybot = table->subtables[gybot].next;
1200 for (z = xLow + 1; z <= gybot; z++) {
1201 zindex = table->invperm[z];
1202 if (zindex == yindex || cuddTestInteract(table,zindex,yindex)) {
1203 isolated = table->vars[zindex]->ref == 1;
1204 L -= (int) table->subtables[z].keys - isolated;
1205 }
1206 }
1207
1208 x = cuddNextLow(table,y);
1209 while (x >= xLow && L <= limitSize) {
1210 #ifdef DD_DEBUG
1211 gybot = y;
1212 while ((unsigned) gybot < table->subtables[gybot].next)
1213 gybot = table->subtables[gybot].next;
1214 checkL = (int) (table->keys - table->isolated);
1215 for (z = xLow + 1; z <= gybot; z++) {
1216 zindex = table->invperm[z];
1217 if (zindex == yindex || cuddTestInteract(table,zindex,yindex)) {
1218 isolated = table->vars[zindex]->ref == 1;
1219 checkL -= (int) table->subtables[z].keys - isolated;
1220 }
1221 }
1222 assert(L == checkL);
1223 #endif
1224 gxtop = table->subtables[x].next;
1225 if (cuddSymmCheck(table,x,y)) {
1226 /* Symmetry found, attach symm groups */
1227 table->subtables[x].next = y;
1228 i = table->subtables[y].next;
1229 while (table->subtables[i].next != (unsigned) y)
1230 i = table->subtables[i].next;
1231 table->subtables[i].next = gxtop;
1232 } else if (table->subtables[x].next == (unsigned) x &&
1233 table->subtables[y].next == (unsigned) y) {
1234 /* x and y have self symmetry */
1235 xindex = table->invperm[x];
1236 size = cuddSwapInPlace(table,x,y);
1237 #ifdef DD_DEBUG
1238 assert(table->subtables[x].next == (unsigned) x);
1239 assert(table->subtables[y].next == (unsigned) y);
1240 #endif
1241 if (size == 0) goto ddSymmSiftingUpOutOfMem;
1242 /* Update the lower bound. */
1243 if (cuddTestInteract(table,xindex,yindex)) {
1244 isolated = table->vars[xindex]->ref == 1;
1245 L += (int) table->subtables[y].keys - isolated;
1246 }
1247 move = (Move *) cuddDynamicAllocNode(table);
1248 if (move == NULL) goto ddSymmSiftingUpOutOfMem;
1249 move->x = x;
1250 move->y = y;
1251 move->size = size;
1252 move->next = moves;
1253 moves = move;
1254 if ((double) size > (double) limitSize * table->maxGrowth)
1255 return(moves);
1256 if (size < limitSize) limitSize = size;
1257 } else { /* Group move */
1258 size = ddSymmGroupMove(table,x,y,&moves);
1259 if (size == 0) goto ddSymmSiftingUpOutOfMem;
1260 /* Update the lower bound. */
1261 z = moves->y;
1262 do {
1263 zindex = table->invperm[z];
1264 if (cuddTestInteract(table,zindex,yindex)) {
1265 isolated = table->vars[zindex]->ref == 1;
1266 L += (int) table->subtables[z].keys - isolated;
1267 }
1268 z = table->subtables[z].next;
1269 } while (z != (int) moves->y);
1270 if ((double) size > (double) limitSize * table->maxGrowth)
1271 return(moves);
1272 if (size < limitSize) limitSize = size;
1273 }
1274 y = gxtop;
1275 x = cuddNextLow(table,y);
1276 }
1277
1278 return(moves);
1279
1280 ddSymmSiftingUpOutOfMem:
1281 while (moves != NULL) {
1282 move = moves->next;
1283 cuddDeallocMove(table, moves);
1284 moves = move;
1285 }
1286 return(MV_OOM);
1287
1288 } /* end of ddSymmSiftingUp */
1289
1290
1291 /**
1292 @brief Moves x down until either it reaches the bound (xHigh) or
1293 the size of the %DD heap increases too much.
1294
1295 @details Assumes that x is the bottom of a symmetry group. Checks x
1296 for symmetry to the adjacent variables. If symmetry is found, the
1297 symmetry group of x is merged with the symmetry group of the other
1298 variable.
1299
1300 @return the set of moves in case of success; MV_OOM if memory is
1301 full.
1302
1303 @sideeffect None
1304
1305 */
1306 static Move *
ddSymmSiftingDown(DdManager * table,int x,int xHigh)1307 ddSymmSiftingDown(
1308 DdManager * table,
1309 int x,
1310 int xHigh)
1311 {
1312 Move *moves;
1313 Move *move;
1314 int y;
1315 int size;
1316 int limitSize;
1317 int gxtop,gybot;
1318 int R; /* upper bound on node decrease */
1319 int xindex, yindex;
1320 int isolated;
1321 int z;
1322 int zindex;
1323 #ifdef DD_DEBUG
1324 int checkR;
1325 #endif
1326
1327 moves = NULL;
1328 /* Initialize R */
1329 xindex = table->invperm[x];
1330 gxtop = table->subtables[x].next;
1331 limitSize = size = (int) (table->keys - table->isolated);
1332 R = 0;
1333 for (z = xHigh; z > gxtop; z--) {
1334 zindex = table->invperm[z];
1335 if (zindex == xindex || cuddTestInteract(table,xindex,zindex)) {
1336 isolated = table->vars[zindex]->ref == 1;
1337 R += (int) table->subtables[z].keys - isolated;
1338 }
1339 }
1340
1341 y = cuddNextHigh(table,x);
1342 while (y <= xHigh && size - R < limitSize) {
1343 #ifdef DD_DEBUG
1344 gxtop = table->subtables[x].next;
1345 checkR = 0;
1346 for (z = xHigh; z > gxtop; z--) {
1347 zindex = table->invperm[z];
1348 if (zindex == xindex || cuddTestInteract(table,xindex,zindex)) {
1349 isolated = table->vars[zindex]->ref == 1;
1350 checkR += (int) table->subtables[z].keys - isolated;
1351 }
1352 }
1353 assert(R == checkR);
1354 #endif
1355 gybot = table->subtables[y].next;
1356 while (table->subtables[gybot].next != (unsigned) y)
1357 gybot = table->subtables[gybot].next;
1358 if (cuddSymmCheck(table,x,y)) {
1359 /* Symmetry found, attach symm groups */
1360 gxtop = table->subtables[x].next;
1361 table->subtables[x].next = y;
1362 table->subtables[gybot].next = gxtop;
1363 } else if (table->subtables[x].next == (unsigned) x &&
1364 table->subtables[y].next == (unsigned) y) {
1365 /* x and y have self symmetry */
1366 /* Update upper bound on node decrease. */
1367 yindex = table->invperm[y];
1368 if (cuddTestInteract(table,xindex,yindex)) {
1369 isolated = table->vars[yindex]->ref == 1;
1370 R -= (int) table->subtables[y].keys - isolated;
1371 }
1372 size = cuddSwapInPlace(table,x,y);
1373 #ifdef DD_DEBUG
1374 assert(table->subtables[x].next == (unsigned) x);
1375 assert(table->subtables[y].next == (unsigned) y);
1376 #endif
1377 if (size == 0) goto ddSymmSiftingDownOutOfMem;
1378 move = (Move *) cuddDynamicAllocNode(table);
1379 if (move == NULL) goto ddSymmSiftingDownOutOfMem;
1380 move->x = x;
1381 move->y = y;
1382 move->size = size;
1383 move->next = moves;
1384 moves = move;
1385 if ((double) size > (double) limitSize * table->maxGrowth)
1386 return(moves);
1387 if (size < limitSize) limitSize = size;
1388 } else { /* Group move */
1389 /* Update upper bound on node decrease: first phase. */
1390 gxtop = table->subtables[x].next;
1391 z = gxtop + 1;
1392 do {
1393 zindex = table->invperm[z];
1394 if (zindex == xindex || cuddTestInteract(table,xindex,zindex)) {
1395 isolated = table->vars[zindex]->ref == 1;
1396 R -= (int) table->subtables[z].keys - isolated;
1397 }
1398 z++;
1399 } while (z <= gybot);
1400 size = ddSymmGroupMove(table,x,y,&moves);
1401 if (size == 0) goto ddSymmSiftingDownOutOfMem;
1402 if ((double) size > (double) limitSize * table->maxGrowth)
1403 return(moves);
1404 if (size < limitSize) limitSize = size;
1405 /* Update upper bound on node decrease: second phase. */
1406 gxtop = table->subtables[gybot].next;
1407 for (z = gxtop + 1; z <= gybot; z++) {
1408 zindex = table->invperm[z];
1409 if (zindex == xindex || cuddTestInteract(table,xindex,zindex)) {
1410 isolated = table->vars[zindex]->ref == 1;
1411 R += (int) table->subtables[z].keys - isolated;
1412 }
1413 }
1414 }
1415 x = gybot;
1416 y = cuddNextHigh(table,x);
1417 }
1418
1419 return(moves);
1420
1421 ddSymmSiftingDownOutOfMem:
1422 while (moves != NULL) {
1423 move = moves->next;
1424 cuddDeallocMove(table, moves);
1425 moves = move;
1426 }
1427 return(MV_OOM);
1428
1429 } /* end of ddSymmSiftingDown */
1430
1431
1432 /**
1433 @brief Swaps two groups.
1434
1435 @details x is assumed to be the bottom variable of the first
1436 group. y is assumed to be the top variable of the second group.
1437 Updates the list of moves.
1438
1439 @return the number of keys in the table if successful; 0 otherwise.
1440
1441 @sideeffect None
1442
1443 */
1444 static int
ddSymmGroupMove(DdManager * table,int x,int y,Move ** moves)1445 ddSymmGroupMove(
1446 DdManager * table,
1447 int x,
1448 int y,
1449 Move ** moves)
1450 {
1451 Move *move;
1452 int size = 0;
1453 int i,j;
1454 int xtop,xbot,xsize,ytop,ybot,ysize,newxtop;
1455 int swapx = 0, swapy = 0;
1456
1457 #ifdef DD_DEBUG
1458 assert(x < y); /* we assume that x < y */
1459 #endif
1460 /* Find top, bottom, and size for the two groups. */
1461 xbot = x;
1462 xtop = table->subtables[x].next;
1463 xsize = xbot - xtop + 1;
1464 ybot = y;
1465 while ((unsigned) ybot < table->subtables[ybot].next)
1466 ybot = table->subtables[ybot].next;
1467 ytop = y;
1468 ysize = ybot - ytop + 1;
1469
1470 /* Sift the variables of the second group up through the first group. */
1471 for (i = 1; i <= ysize; i++) {
1472 for (j = 1; j <= xsize; j++) {
1473 size = cuddSwapInPlace(table,x,y);
1474 if (size == 0) return(0);
1475 swapx = x; swapy = y;
1476 y = x;
1477 x = y - 1;
1478 }
1479 y = ytop + i;
1480 x = y - 1;
1481 }
1482
1483 /* fix symmetries */
1484 y = xtop; /* ytop is now where xtop used to be */
1485 for (i = 0; i < ysize-1 ; i++) {
1486 table->subtables[y].next = y + 1;
1487 y = y + 1;
1488 }
1489 table->subtables[y].next = xtop; /* y is bottom of its group, join */
1490 /* its symmetry to top of its group */
1491 x = y + 1;
1492 newxtop = x;
1493 for (i = 0; i < xsize - 1 ; i++) {
1494 table->subtables[x].next = x + 1;
1495 x = x + 1;
1496 }
1497 table->subtables[x].next = newxtop; /* x is bottom of its group, join */
1498 /* its symmetry to top of its group */
1499 /* Store group move */
1500 move = (Move *) cuddDynamicAllocNode(table);
1501 if (move == NULL) return(0);
1502 move->x = swapx;
1503 move->y = swapy;
1504 move->size = size;
1505 move->next = *moves;
1506 *moves = move;
1507
1508 return(size);
1509
1510 } /* end of ddSymmGroupMove */
1511
1512
1513 /**
1514 @brief Undoes the swap of two groups.
1515
1516 @details x is assumed to be the bottom variable of the first
1517 group. y is assumed to be the top variable of the second group.
1518
1519 @return the number of keys in the table if successful; 0 otherwise.
1520
1521 @sideeffect None
1522
1523 */
1524 static int
ddSymmGroupMoveBackward(DdManager * table,int x,int y)1525 ddSymmGroupMoveBackward(
1526 DdManager * table,
1527 int x,
1528 int y)
1529 {
1530 int size = (int) (table->keys - table->isolated);
1531 int i,j;
1532 int xtop,xbot,xsize,ytop,ybot,ysize,newxtop;
1533
1534 #ifdef DD_DEBUG
1535 assert(x < y); /* We assume that x < y */
1536 #endif
1537
1538 /* Find top, bottom, and size for the two groups. */
1539 xbot = x;
1540 xtop = table->subtables[x].next;
1541 xsize = xbot - xtop + 1;
1542 ybot = y;
1543 while ((unsigned) ybot < table->subtables[ybot].next)
1544 ybot = table->subtables[ybot].next;
1545 ytop = y;
1546 ysize = ybot - ytop + 1;
1547 #ifdef DD_DEBUG
1548 assert(xsize > 0);
1549 assert(ysize > 0);
1550 #endif
1551
1552 /* Sift the variables of the second group up through the first group. */
1553 for (i = 1; i <= ysize; i++) {
1554 for (j = 1; j <= xsize; j++) {
1555 size = cuddSwapInPlace(table,x,y);
1556 if (size == 0) return(0);
1557 y = x;
1558 x = cuddNextLow(table,y);
1559 }
1560 y = ytop + i;
1561 x = y - 1;
1562 }
1563
1564 /* Fix symmetries. */
1565 y = xtop;
1566 for (i = 0; i < ysize-1 ; i++) {
1567 table->subtables[y].next = y + 1;
1568 y = y + 1;
1569 }
1570 table->subtables[y].next = xtop; /* y is bottom of its group, join */
1571 /* its symmetry to top of its group */
1572 x = y + 1;
1573 newxtop = x;
1574 for (i = 0; i < xsize-1 ; i++) {
1575 table->subtables[x].next = x + 1;
1576 x = x + 1;
1577 }
1578 table->subtables[x].next = newxtop; /* x is bottom of its group, join */
1579 /* its symmetry to top of its group */
1580
1581 return(size);
1582
1583 } /* end of ddSymmGroupMoveBackward */
1584
1585
1586 /**
1587 @brief Given a set of moves, returns the %DD heap to the position
1588 giving the minimum size.
1589
1590 @details In case of ties, returns to the closest position giving the
1591 minimum size.
1592
1593 @return 1 in case of success; 0 otherwise.
1594
1595 @sideeffect None
1596
1597 */
1598 static int
ddSymmSiftingBackward(DdManager * table,Move * moves,int size)1599 ddSymmSiftingBackward(
1600 DdManager * table,
1601 Move * moves,
1602 int size)
1603 {
1604 Move *move;
1605 int res;
1606
1607 for (move = moves; move != NULL; move = move->next) {
1608 if (move->size < size) {
1609 size = move->size;
1610 }
1611 }
1612
1613 for (move = moves; move != NULL; move = move->next) {
1614 if (move->size == size) return(1);
1615 if (table->subtables[move->x].next == move->x && table->subtables[move->y].next == move->y) {
1616 res = cuddSwapInPlace(table,(int)move->x,(int)move->y);
1617 #ifdef DD_DEBUG
1618 assert(table->subtables[move->x].next == move->x);
1619 assert(table->subtables[move->y].next == move->y);
1620 #endif
1621 } else { /* Group move necessary */
1622 res = ddSymmGroupMoveBackward(table,(int)move->x,(int)move->y);
1623 }
1624 if (!res) return(0);
1625 }
1626
1627 return(1);
1628
1629 } /* end of ddSymmSiftingBackward */
1630
1631
1632 /**
1633 @brief Counts numbers of symmetric variables and symmetry groups.
1634
1635 @sideeffect None
1636
1637 */
1638 static void
ddSymmSummary(DdManager * table,int lower,int upper,int * symvars,int * symgroups)1639 ddSymmSummary(
1640 DdManager * table,
1641 int lower,
1642 int upper,
1643 int * symvars,
1644 int * symgroups)
1645 {
1646 int i,x,gbot;
1647 int TotalSymm = 0;
1648 int TotalSymmGroups = 0;
1649
1650 for (i = lower; i <= upper; i++) {
1651 if (table->subtables[i].next != (unsigned) i) {
1652 TotalSymmGroups++;
1653 x = i;
1654 do {
1655 TotalSymm++;
1656 gbot = x;
1657 x = table->subtables[x].next;
1658 } while (x != i);
1659 #ifdef DD_DEBUG
1660 assert(table->subtables[gbot].next == (unsigned) i);
1661 #endif
1662 i = gbot;
1663 }
1664 }
1665 *symvars = TotalSymm;
1666 *symgroups = TotalSymmGroups;
1667
1668 return;
1669
1670 } /* end of ddSymmSummary */
1671