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