source: vis_dev/glu-2.3/src/cuBdd/cuddSymmetry.c @ 100

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

library glu 2.3

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