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