source: vis_dev/glu-2.3/src/cuBdd/cuddZddSymm.c @ 88

Last change on this file since 88 was 13, checked in by cecile, 13 years ago

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