source: vis_dev/glu-2.3/src/cuBdd/cuddZddGroup.c @ 80

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

library glu 2.3
File size: 38.4 KB
RevLine 
[13]1/**CFile***********************************************************************
2
3  FileName    [cuddZddGroup.c]
4
5  PackageName [cudd]
6
7  Synopsis    [Functions for ZDD group sifting.]
8
9  Description [External procedures included in this file:
10                <ul>
11                <li> Cudd_MakeZddTreeNode()
12                </ul>
13        Internal procedures included in this file:
14                <ul>
15                <li> cuddZddTreeSifting()
16                </ul>
17        Static procedures included in this module:
18                <ul>
19                <li> zddTreeSiftingAux()
20                <li> zddCountInternalMtrNodes()
21                <li> zddReorderChildren()
22                <li> zddFindNodeHiLo()
23                <li> zddUniqueCompareGroup()
24                <li> zddGroupSifting()
25                <li> zddGroupSiftingAux()
26                <li> zddGroupSiftingUp()
27                <li> zddGroupSiftingDown()
28                <li> zddGroupMove()
29                <li> zddGroupMoveBackward()
30                <li> zddGroupSiftingBackward()
31                <li> zddMergeGroups()
32                </ul>]
33
34  Author      [Fabio Somenzi]
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/*---------------------------------------------------------------------------*/
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: cuddZddGroup.c,v 1.20 2009/02/19 16:25:36 fabio Exp $";
91#endif
92
93static  int     *entry;
94extern  int     zddTotalNumberSwapping;
95#ifdef DD_STATS
96static  int     extsymmcalls;
97static  int     extsymm;
98static  int     secdiffcalls;
99static  int     secdiff;
100static  int     secdiffmisfire;
101#endif
102#ifdef DD_DEBUG
103static  int     pr = 0; /* flag to enable printing while debugging */
104                        /* by depositing a 1 into it */
105#endif
106
107/*---------------------------------------------------------------------------*/
108/* Macro declarations                                                        */
109/*---------------------------------------------------------------------------*/
110
111/**AutomaticStart*************************************************************/
112
113/*---------------------------------------------------------------------------*/
114/* Static function prototypes                                                */
115/*---------------------------------------------------------------------------*/
116
117static int zddTreeSiftingAux (DdManager *table, MtrNode *treenode, Cudd_ReorderingType method);
118#ifdef DD_STATS
119static int zddCountInternalMtrNodes (DdManager *table, MtrNode *treenode);
120#endif
121static int zddReorderChildren (DdManager *table, MtrNode *treenode, Cudd_ReorderingType method);
122static void zddFindNodeHiLo (DdManager *table, MtrNode *treenode, int *lower, int *upper);
123static int zddUniqueCompareGroup (int *ptrX, int *ptrY);
124static int zddGroupSifting (DdManager *table, int lower, int upper);
125static int zddGroupSiftingAux (DdManager *table, int x, int xLow, int xHigh);
126static int zddGroupSiftingUp (DdManager *table, int y, int xLow, Move **moves);
127static int zddGroupSiftingDown (DdManager *table, int x, int xHigh, Move **moves);
128static int zddGroupMove (DdManager *table, int x, int y, Move **moves);
129static int zddGroupMoveBackward (DdManager *table, int x, int y);
130static int zddGroupSiftingBackward (DdManager *table, Move *moves, int size);
131static void zddMergeGroups (DdManager *table, MtrNode *treenode, int low, int high);
132
133/**AutomaticEnd***************************************************************/
134
135
136/*---------------------------------------------------------------------------*/
137/* Definition of exported functions                                          */
138/*---------------------------------------------------------------------------*/
139
140
141/**Function********************************************************************
142
143  Synopsis    [Creates a new ZDD variable group.]
144
145  Description [Creates a new ZDD variable group. The group starts at
146  variable and contains size variables. The parameter low is the index
147  of the first variable. If the variable already exists, its current
148  position in the order is known to the manager. If the variable does
149  not exist yet, the position is assumed to be the same as the index.
150  The group tree is created if it does not exist yet.
151  Returns a pointer to the group if successful; NULL otherwise.]
152
153  SideEffects [The ZDD variable tree is changed.]
154
155  SeeAlso     [Cudd_MakeTreeNode]
156
157******************************************************************************/
158MtrNode *
159Cudd_MakeZddTreeNode(
160  DdManager * dd /* manager */,
161  unsigned int  low /* index of the first group variable */,
162  unsigned int  size /* number of variables in the group */,
163  unsigned int  type /* MTR_DEFAULT or MTR_FIXED */)
164{
165    MtrNode *group;
166    MtrNode *tree;
167    unsigned int level;
168
169    /* If the variable does not exist yet, the position is assumed to be
170    ** the same as the index. Therefore, applications that rely on
171    ** Cudd_bddNewVarAtLevel or Cudd_addNewVarAtLevel to create new
172    ** variables have to create the variables before they group them.
173    */
174    level = (low < (unsigned int) dd->sizeZ) ? dd->permZ[low] : low;
175
176    if (level + size - 1> (int) MTR_MAXHIGH)
177        return(NULL);
178
179    /* If the tree does not exist yet, create it. */
180    tree = dd->treeZ;
181    if (tree == NULL) {
182        dd->treeZ = tree = Mtr_InitGroupTree(0, dd->sizeZ);
183        if (tree == NULL)
184            return(NULL);
185        tree->index = dd->invpermZ[0];
186    }
187
188    /* Extend the upper bound of the tree if necessary. This allows the
189    ** application to create groups even before the variables are created.
190    */
191    tree->size = ddMax(tree->size, level + size);
192
193    /* Create the group. */
194    group = Mtr_MakeGroup(tree, level, size, type);
195    if (group == NULL)
196        return(NULL);
197
198    /* Initialize the index field to the index of the variable currently
199    ** in position low. This field will be updated by the reordering
200    ** procedure to provide a handle to the group once it has been moved.
201    */
202    group->index = (MtrHalfWord) low;
203
204    return(group);
205
206} /* end of Cudd_MakeZddTreeNode */
207
208
209/*---------------------------------------------------------------------------*/
210/* Definition of internal functions                                          */
211/*---------------------------------------------------------------------------*/
212
213
214/**Function********************************************************************
215
216  Synopsis    [Tree sifting algorithm for ZDDs.]
217
218  Description [Tree sifting algorithm for ZDDs. Assumes that a tree
219  representing a group hierarchy is passed as a parameter. It then
220  reorders each group in postorder fashion by calling
221  zddTreeSiftingAux.  Assumes that no dead nodes are present.  Returns
222  1 if successful; 0 otherwise.]
223
224  SideEffects [None]
225
226******************************************************************************/
227int
228cuddZddTreeSifting(
229  DdManager * table /* DD table */,
230  Cudd_ReorderingType method /* reordering method for the groups of leaves */)
231{
232    int i;
233    int nvars;
234    int result;
235    int tempTree;
236
237    /* If no tree is provided we create a temporary one in which all
238    ** variables are in a single group. After reordering this tree is
239    ** destroyed.
240    */
241    tempTree = table->treeZ == NULL;
242    if (tempTree) {
243        table->treeZ = Mtr_InitGroupTree(0,table->sizeZ);
244        table->treeZ->index = table->invpermZ[0];
245    }
246    nvars = table->sizeZ;
247
248#ifdef DD_DEBUG
249    if (pr > 0 && !tempTree)
250        (void) fprintf(table->out,"cuddZddTreeSifting:");
251    Mtr_PrintGroups(table->treeZ,pr <= 0);
252#endif
253#if 0
254    /* Debugging code. */
255    if (table->tree && table->treeZ) {
256        (void) fprintf(table->out,"\n");
257        Mtr_PrintGroups(table->tree, 0);
258        cuddPrintVarGroups(table,table->tree,0,0);
259        for (i = 0; i < table->size; i++) {
260            (void) fprintf(table->out,"%s%d",
261                           (i == 0) ? "" : ",", table->invperm[i]);
262        }
263        (void) fprintf(table->out,"\n");
264        for (i = 0; i < table->size; i++) {
265            (void) fprintf(table->out,"%s%d",
266                           (i == 0) ? "" : ",", table->perm[i]);
267        }
268        (void) fprintf(table->out,"\n\n");
269        Mtr_PrintGroups(table->treeZ,0);
270        cuddPrintVarGroups(table,table->treeZ,1,0);
271        for (i = 0; i < table->sizeZ; i++) {
272            (void) fprintf(table->out,"%s%d",
273                           (i == 0) ? "" : ",", table->invpermZ[i]);
274        }
275        (void) fprintf(table->out,"\n");
276        for (i = 0; i < table->sizeZ; i++) {
277            (void) fprintf(table->out,"%s%d",
278                           (i == 0) ? "" : ",", table->permZ[i]);
279        }
280        (void) fprintf(table->out,"\n");
281    }
282    /* End of debugging code. */
283#endif
284#ifdef DD_STATS
285    extsymmcalls = 0;
286    extsymm = 0;
287    secdiffcalls = 0;
288    secdiff = 0;
289    secdiffmisfire = 0;
290
291    (void) fprintf(table->out,"\n");
292    if (!tempTree)
293        (void) fprintf(table->out,"#:IM_NODES  %8d: group tree nodes\n",
294                       zddCountInternalMtrNodes(table,table->treeZ));
295#endif
296
297    /* Initialize the group of each subtable to itself. Initially
298    ** there are no groups. Groups are created according to the tree
299    ** structure in postorder fashion.
300    */
301    for (i = 0; i < nvars; i++)
302        table->subtableZ[i].next = i;
303
304    /* Reorder. */
305    result = zddTreeSiftingAux(table, table->treeZ, method);
306
307#ifdef DD_STATS         /* print stats */
308    if (!tempTree && method == CUDD_REORDER_GROUP_SIFT &&
309        (table->groupcheck == CUDD_GROUP_CHECK7 ||
310         table->groupcheck == CUDD_GROUP_CHECK5)) {
311        (void) fprintf(table->out,"\nextsymmcalls = %d\n",extsymmcalls);
312        (void) fprintf(table->out,"extsymm = %d",extsymm);
313    }
314    if (!tempTree && method == CUDD_REORDER_GROUP_SIFT &&
315        table->groupcheck == CUDD_GROUP_CHECK7) {
316        (void) fprintf(table->out,"\nsecdiffcalls = %d\n",secdiffcalls);
317        (void) fprintf(table->out,"secdiff = %d\n",secdiff);
318        (void) fprintf(table->out,"secdiffmisfire = %d",secdiffmisfire);
319    }
320#endif
321
322    if (tempTree)
323        Cudd_FreeZddTree(table);
324    return(result);
325
326} /* end of cuddZddTreeSifting */
327
328
329/*---------------------------------------------------------------------------*/
330/* Definition of static functions                                            */
331/*---------------------------------------------------------------------------*/
332
333
334/**Function********************************************************************
335
336  Synopsis    [Visits the group tree and reorders each group.]
337
338  Description [Recursively visits the group tree and reorders each
339  group in postorder fashion.  Returns 1 if successful; 0 otherwise.]
340
341  SideEffects [None]
342
343******************************************************************************/
344static int
345zddTreeSiftingAux(
346  DdManager * table,
347  MtrNode * treenode,
348  Cudd_ReorderingType method)
349{
350    MtrNode  *auxnode;
351    int res;
352
353#ifdef DD_DEBUG
354    Mtr_PrintGroups(treenode,1);
355#endif
356
357    auxnode = treenode;
358    while (auxnode != NULL) {
359        if (auxnode->child != NULL) {
360            if (!zddTreeSiftingAux(table, auxnode->child, method))
361                return(0);
362            res = zddReorderChildren(table, auxnode, CUDD_REORDER_GROUP_SIFT);
363            if (res == 0)
364                return(0);
365        } else if (auxnode->size > 1) {
366            if (!zddReorderChildren(table, auxnode, method))
367                return(0);
368        }
369        auxnode = auxnode->younger;
370    }
371
372    return(1);
373
374} /* end of zddTreeSiftingAux */
375
376
377#ifdef DD_STATS
378/**Function********************************************************************
379
380  Synopsis    [Counts the number of internal nodes of the group tree.]
381
382  Description [Counts the number of internal nodes of the group tree.
383  Returns the count.]
384
385  SideEffects [None]
386
387******************************************************************************/
388static int
389zddCountInternalMtrNodes(
390  DdManager * table,
391  MtrNode * treenode)
392{
393    MtrNode *auxnode;
394    int     count,nodeCount;
395
396
397    nodeCount = 0;
398    auxnode = treenode;
399    while (auxnode != NULL) {
400        if (!(MTR_TEST(auxnode,MTR_TERMINAL))) {
401            nodeCount++;
402            count = zddCountInternalMtrNodes(table,auxnode->child);
403            nodeCount += count;
404        }
405        auxnode = auxnode->younger;
406    }
407
408    return(nodeCount);
409
410} /* end of zddCountInternalMtrNodes */
411#endif
412
413
414/**Function********************************************************************
415
416  Synopsis    [Reorders the children of a group tree node according to
417  the options.]
418
419  Description [Reorders the children of a group tree node according to
420  the options. After reordering puts all the variables in the group
421  and/or its descendents in a single group. This allows hierarchical
422  reordering.  If the variables in the group do not exist yet, simply
423  does nothing. Returns 1 if successful; 0 otherwise.]
424
425  SideEffects [None]
426
427******************************************************************************/
428static int
429zddReorderChildren(
430  DdManager * table,
431  MtrNode * treenode,
432  Cudd_ReorderingType method)
433{
434    int lower;
435    int upper;
436    int result;
437    unsigned int initialSize;
438
439    zddFindNodeHiLo(table,treenode,&lower,&upper);
440    /* If upper == -1 these variables do not exist yet. */
441    if (upper == -1)
442        return(1);
443
444    if (treenode->flags == MTR_FIXED) {
445        result = 1;
446    } else {
447#ifdef DD_STATS
448        (void) fprintf(table->out," ");
449#endif
450        switch (method) {
451        case CUDD_REORDER_RANDOM:
452        case CUDD_REORDER_RANDOM_PIVOT:
453            result = cuddZddSwapping(table,lower,upper,method);
454            break;
455        case CUDD_REORDER_SIFT:
456            result = cuddZddSifting(table,lower,upper);
457            break;
458        case CUDD_REORDER_SIFT_CONVERGE:
459            do {
460                initialSize = table->keysZ;
461                result = cuddZddSifting(table,lower,upper);
462                if (initialSize <= table->keysZ)
463                    break;
464#ifdef DD_STATS
465                else
466                    (void) fprintf(table->out,"\n");
467#endif
468            } while (result != 0);
469            break;
470        case CUDD_REORDER_SYMM_SIFT:
471            result = cuddZddSymmSifting(table,lower,upper);
472            break;
473        case CUDD_REORDER_SYMM_SIFT_CONV:
474            result = cuddZddSymmSiftingConv(table,lower,upper);
475            break;
476        case CUDD_REORDER_GROUP_SIFT:
477            result = zddGroupSifting(table,lower,upper);
478            break;
479        case CUDD_REORDER_LINEAR:
480            result = cuddZddLinearSifting(table,lower,upper);
481            break;
482        case CUDD_REORDER_LINEAR_CONVERGE:
483            do {
484                initialSize = table->keysZ;
485                result = cuddZddLinearSifting(table,lower,upper);
486                if (initialSize <= table->keysZ)
487                    break;
488#ifdef DD_STATS
489                else
490                    (void) fprintf(table->out,"\n");
491#endif
492            } while (result != 0);
493            break;
494        default:
495            return(0);
496        }
497    }
498
499    /* Create a single group for all the variables that were sifted,
500    ** so that they will be treated as a single block by successive
501    ** invocations of zddGroupSifting.
502    */
503    zddMergeGroups(table,treenode,lower,upper);
504
505#ifdef DD_DEBUG
506    if (pr > 0) (void) fprintf(table->out,"zddReorderChildren:");
507#endif
508
509    return(result);
510
511} /* end of zddReorderChildren */
512
513
514/**Function********************************************************************
515
516  Synopsis    [Finds the lower and upper bounds of the group represented
517  by treenode.]
518
519  Description [Finds the lower and upper bounds of the group represented
520  by treenode.  The high and low fields of treenode are indices.  From
521  those we need to derive the current positions, and find maximum and
522  minimum.]
523
524  SideEffects [The bounds are returned as side effects.]
525
526  SeeAlso     []
527
528******************************************************************************/
529static void
530zddFindNodeHiLo(
531  DdManager * table,
532  MtrNode * treenode,
533  int * lower,
534  int * upper)
535{
536    int low;
537    int high;
538
539    /* Check whether no variables in this group already exist.
540    ** If so, return immediately. The calling procedure will know from
541    ** the values of upper that no reordering is needed.
542    */
543    if ((int) treenode->low >= table->sizeZ) {
544        *lower = table->sizeZ;
545        *upper = -1;
546        return;
547    }
548
549    *lower = low = (unsigned int) table->permZ[treenode->index];
550    high = (int) (low + treenode->size - 1);
551
552    if (high >= table->sizeZ) {
553        /* This is the case of a partially existing group. The aim is to
554        ** reorder as many variables as safely possible.  If the tree
555        ** node is terminal, we just reorder the subset of the group
556        ** that is currently in existence.  If the group has
557        ** subgroups, then we only reorder those subgroups that are
558        ** fully instantiated.  This way we avoid breaking up a group.
559        */
560        MtrNode *auxnode = treenode->child;
561        if (auxnode == NULL) {
562            *upper = (unsigned int) table->sizeZ - 1;
563        } else {
564            /* Search the subgroup that strands the table->sizeZ line.
565            ** If the first group starts at 0 and goes past table->sizeZ
566            ** upper will get -1, thus correctly signaling that no reordering
567            ** should take place.
568            */
569            while (auxnode != NULL) {
570                int thisLower = table->permZ[auxnode->low];
571                int thisUpper = thisLower + auxnode->size - 1;
572                if (thisUpper >= table->sizeZ && thisLower < table->sizeZ)
573                    *upper = (unsigned int) thisLower - 1;
574                auxnode = auxnode->younger;
575            }
576        }
577    } else {
578        /* Normal case: All the variables of the group exist. */
579        *upper = (unsigned int) high;
580    }
581
582#ifdef DD_DEBUG
583    /* Make sure that all variables in group are contiguous. */
584    assert(treenode->size >= *upper - *lower + 1);
585#endif
586
587    return;
588
589} /* end of zddFindNodeHiLo */
590
591
592/**Function********************************************************************
593
594  Synopsis    [Comparison function used by qsort.]
595
596  Description [Comparison function used by qsort to order the variables
597  according to the number of keys in the subtables.  Returns the
598  difference in number of keys between the two variables being
599  compared.]
600
601  SideEffects [None]
602
603******************************************************************************/
604static int
605zddUniqueCompareGroup(
606  int * ptrX,
607  int * ptrY)
608{
609#if 0
610    if (entry[*ptrY] == entry[*ptrX]) {
611        return((*ptrX) - (*ptrY));
612    }
613#endif
614    return(entry[*ptrY] - entry[*ptrX]);
615
616} /* end of zddUniqueCompareGroup */
617
618
619/**Function********************************************************************
620
621  Synopsis    [Sifts from treenode->low to treenode->high.]
622
623  Description [Sifts from treenode->low to treenode->high. If
624  croupcheck == CUDD_GROUP_CHECK7, it checks for group creation at the
625  end of the initial sifting. If a group is created, it is then sifted
626  again. After sifting one variable, the group that contains it is
627  dissolved.  Returns 1 in case of success; 0 otherwise.]
628
629  SideEffects [None]
630
631******************************************************************************/
632static int
633zddGroupSifting(
634  DdManager * table,
635  int  lower,
636  int  upper)
637{
638    int         *var;
639    int         i,j,x,xInit;
640    int         nvars;
641    int         classes;
642    int         result;
643    int         *sifted;
644#ifdef DD_STATS
645    unsigned    previousSize;
646#endif
647    int         xindex;
648
649    nvars = table->sizeZ;
650
651    /* Order variables to sift. */
652    entry = NULL;
653    sifted = NULL;
654    var = ALLOC(int,nvars);
655    if (var == NULL) {
656        table->errorCode = CUDD_MEMORY_OUT;
657        goto zddGroupSiftingOutOfMem;
658    }
659    entry = ALLOC(int,nvars);
660    if (entry == NULL) {
661        table->errorCode = CUDD_MEMORY_OUT;
662        goto zddGroupSiftingOutOfMem;
663    }
664    sifted = ALLOC(int,nvars);
665    if (sifted == NULL) {
666        table->errorCode = CUDD_MEMORY_OUT;
667        goto zddGroupSiftingOutOfMem;
668    }
669
670    /* Here we consider only one representative for each group. */
671    for (i = 0, classes = 0; i < nvars; i++) {
672        sifted[i] = 0;
673        x = table->permZ[i];
674        if ((unsigned) x >= table->subtableZ[x].next) {
675            entry[i] = table->subtableZ[x].keys;
676            var[classes] = i;
677            classes++;
678        }
679    }
680
681    qsort((void *)var,classes,sizeof(int),(DD_QSFP)zddUniqueCompareGroup);
682
683    /* Now sift. */
684    for (i = 0; i < ddMin(table->siftMaxVar,classes); i++) {
685        if (zddTotalNumberSwapping >= table->siftMaxSwap)
686            break;
687        xindex = var[i];
688        if (sifted[xindex] == 1) /* variable already sifted as part of group */
689            continue;
690        x = table->permZ[xindex]; /* find current level of this variable */
691        if (x < lower || x > upper)
692            continue;
693#ifdef DD_STATS
694        previousSize = table->keysZ;
695#endif
696#ifdef DD_DEBUG
697        /* x is bottom of group */
698        assert((unsigned) x >= table->subtableZ[x].next);
699#endif
700        result = zddGroupSiftingAux(table,x,lower,upper);
701        if (!result) goto zddGroupSiftingOutOfMem;
702
703#ifdef DD_STATS
704        if (table->keysZ < previousSize) {
705            (void) fprintf(table->out,"-");
706        } else if (table->keysZ > previousSize) {
707            (void) fprintf(table->out,"+");
708        } else {
709            (void) fprintf(table->out,"=");
710        }
711        fflush(table->out);
712#endif
713
714        /* Mark variables in the group just sifted. */
715        x = table->permZ[xindex];
716        if ((unsigned) x != table->subtableZ[x].next) {
717            xInit = x;
718            do {
719                j = table->invpermZ[x];
720                sifted[j] = 1;
721                x = table->subtableZ[x].next;
722            } while (x != xInit);
723        }
724
725#ifdef DD_DEBUG
726        if (pr > 0) (void) fprintf(table->out,"zddGroupSifting:");
727#endif
728    } /* for */
729
730    FREE(sifted);
731    FREE(var);
732    FREE(entry);
733
734    return(1);
735
736zddGroupSiftingOutOfMem:
737    if (entry != NULL)  FREE(entry);
738    if (var != NULL)    FREE(var);
739    if (sifted != NULL) FREE(sifted);
740
741    return(0);
742
743} /* end of zddGroupSifting */
744
745
746/**Function********************************************************************
747
748  Synopsis    [Sifts one variable up and down until it has taken all
749  positions. Checks for aggregation.]
750
751  Description [Sifts one variable up and down until it has taken all
752  positions. Checks for aggregation. There may be at most two sweeps,
753  even if the group grows.  Assumes that x is either an isolated
754  variable, or it is the bottom of a group. All groups may not have
755  been found. The variable being moved is returned to the best position
756  seen during sifting.  Returns 1 in case of success; 0 otherwise.]
757
758  SideEffects [None]
759
760******************************************************************************/
761static int
762zddGroupSiftingAux(
763  DdManager * table,
764  int  x,
765  int  xLow,
766  int  xHigh)
767{
768    Move *move;
769    Move *moves;        /* list of moves */
770    int  initialSize;
771    int  result;
772
773
774#ifdef DD_DEBUG
775    if (pr > 0) (void) fprintf(table->out,"zddGroupSiftingAux from %d to %d\n",xLow,xHigh);
776    assert((unsigned) x >= table->subtableZ[x].next); /* x is bottom of group */
777#endif
778
779    initialSize = table->keysZ;
780    moves = NULL;
781
782    if (x == xLow) { /* Sift down */
783#ifdef DD_DEBUG
784        /* x must be a singleton */
785        assert((unsigned) x == table->subtableZ[x].next);
786#endif
787        if (x == xHigh) return(1);      /* just one variable */
788
789        if (!zddGroupSiftingDown(table,x,xHigh,&moves))
790            goto zddGroupSiftingAuxOutOfMem;
791        /* at this point x == xHigh, unless early term */
792
793        /* move backward and stop at best position */
794        result = zddGroupSiftingBackward(table,moves,initialSize);
795#ifdef DD_DEBUG
796        assert(table->keysZ <= (unsigned) initialSize);
797#endif
798        if (!result) goto zddGroupSiftingAuxOutOfMem;
799
800    } else if (cuddZddNextHigh(table,x) > xHigh) { /* Sift up */
801#ifdef DD_DEBUG
802        /* x is bottom of group */
803        assert((unsigned) x >= table->subtableZ[x].next);
804#endif
805        /* Find top of x's group */
806        x = table->subtableZ[x].next;
807
808        if (!zddGroupSiftingUp(table,x,xLow,&moves))
809            goto zddGroupSiftingAuxOutOfMem;
810        /* at this point x == xLow, unless early term */
811
812        /* move backward and stop at best position */
813        result = zddGroupSiftingBackward(table,moves,initialSize);
814#ifdef DD_DEBUG
815        assert(table->keysZ <= (unsigned) initialSize);
816#endif
817        if (!result) goto zddGroupSiftingAuxOutOfMem;
818
819    } else if (x - xLow > xHigh - x) { /* must go down first: shorter */
820        if (!zddGroupSiftingDown(table,x,xHigh,&moves))
821            goto zddGroupSiftingAuxOutOfMem;
822        /* at this point x == xHigh, unless early term */
823
824        /* Find top of group */
825        if (moves) {
826            x = moves->y;
827        }
828        while ((unsigned) x < table->subtableZ[x].next)
829            x = table->subtableZ[x].next;
830        x = table->subtableZ[x].next;
831#ifdef DD_DEBUG
832        /* x should be the top of a group */
833        assert((unsigned) x <= table->subtableZ[x].next);
834#endif
835
836        if (!zddGroupSiftingUp(table,x,xLow,&moves))
837            goto zddGroupSiftingAuxOutOfMem;
838
839        /* move backward and stop at best position */
840        result = zddGroupSiftingBackward(table,moves,initialSize);
841#ifdef DD_DEBUG
842        assert(table->keysZ <= (unsigned) initialSize);
843#endif
844        if (!result) goto zddGroupSiftingAuxOutOfMem;
845
846    } else { /* moving up first: shorter */
847        /* Find top of x's group */
848        x = table->subtableZ[x].next;
849
850        if (!zddGroupSiftingUp(table,x,xLow,&moves))
851            goto zddGroupSiftingAuxOutOfMem;
852        /* at this point x == xHigh, unless early term */
853
854        if (moves) {
855            x = moves->x;
856        }
857        while ((unsigned) x < table->subtableZ[x].next)
858            x = table->subtableZ[x].next;
859#ifdef DD_DEBUG
860        /* x is bottom of a group */
861        assert((unsigned) x >= table->subtableZ[x].next);
862#endif
863
864        if (!zddGroupSiftingDown(table,x,xHigh,&moves))
865            goto zddGroupSiftingAuxOutOfMem;
866
867        /* move backward and stop at best position */
868        result = zddGroupSiftingBackward(table,moves,initialSize);
869#ifdef DD_DEBUG
870        assert(table->keysZ <= (unsigned) initialSize);
871#endif
872        if (!result) goto zddGroupSiftingAuxOutOfMem;
873    }
874
875    while (moves != NULL) {
876        move = moves->next;
877        cuddDeallocMove(table, moves);
878        moves = move;
879    }
880
881    return(1);
882
883zddGroupSiftingAuxOutOfMem:
884    while (moves != NULL) {
885        move = moves->next;
886        cuddDeallocMove(table, moves);
887        moves = move;
888    }
889
890    return(0);
891
892} /* end of zddGroupSiftingAux */
893
894
895/**Function********************************************************************
896
897  Synopsis    [Sifts up a variable until either it reaches position xLow
898  or the size of the DD heap increases too much.]
899
900  Description [Sifts up a variable until either it reaches position
901  xLow or the size of the DD heap increases too much. Assumes that y is
902  the top of a group (or a singleton).  Checks y for aggregation to the
903  adjacent variables. Records all the moves that are appended to the
904  list of moves received as input and returned as a side effect.
905  Returns 1 in case of success; 0 otherwise.]
906
907  SideEffects [None]
908
909******************************************************************************/
910static int
911zddGroupSiftingUp(
912  DdManager * table,
913  int  y,
914  int  xLow,
915  Move ** moves)
916{
917    Move *move;
918    int  x;
919    int  size;
920    int  gxtop;
921    int  limitSize;
922
923    limitSize = table->keysZ;
924
925    x = cuddZddNextLow(table,y);
926    while (x >= xLow) {
927        gxtop = table->subtableZ[x].next;
928        if (table->subtableZ[x].next == (unsigned) x &&
929            table->subtableZ[y].next == (unsigned) y) {
930            /* x and y are self groups */
931            size = cuddZddSwapInPlace(table,x,y);
932#ifdef DD_DEBUG
933            assert(table->subtableZ[x].next == (unsigned) x);
934            assert(table->subtableZ[y].next == (unsigned) y);
935#endif
936            if (size == 0) goto zddGroupSiftingUpOutOfMem;
937            move = (Move *)cuddDynamicAllocNode(table);
938            if (move == NULL) goto zddGroupSiftingUpOutOfMem;
939            move->x = x;
940            move->y = y;
941            move->flags = MTR_DEFAULT;
942            move->size = size;
943            move->next = *moves;
944            *moves = move;
945
946#ifdef DD_DEBUG
947            if (pr > 0) (void) fprintf(table->out,"zddGroupSiftingUp (2 single groups):\n");
948#endif
949            if ((double) size > (double) limitSize * table->maxGrowth)
950                return(1);
951            if (size < limitSize) limitSize = size;
952        } else { /* group move */
953            size = zddGroupMove(table,x,y,moves);
954            if (size == 0) goto zddGroupSiftingUpOutOfMem;
955            if ((double) size > (double) limitSize * table->maxGrowth)
956                return(1);
957            if (size < limitSize) limitSize = size;
958        }
959        y = gxtop;
960        x = cuddZddNextLow(table,y);
961    }
962
963    return(1);
964
965zddGroupSiftingUpOutOfMem:
966    while (*moves != NULL) {
967        move = (*moves)->next;
968        cuddDeallocMove(table, *moves);
969        *moves = move;
970    }
971    return(0);
972
973} /* end of zddGroupSiftingUp */
974
975
976/**Function********************************************************************
977
978  Synopsis    [Sifts down a variable until it reaches position xHigh.]
979
980  Description [Sifts down a variable until it reaches position xHigh.
981  Assumes that x is the bottom of a group (or a singleton).  Records
982  all the moves.  Returns 1 in case of success; 0 otherwise.]
983
984  SideEffects [None]
985
986******************************************************************************/
987static int
988zddGroupSiftingDown(
989  DdManager * table,
990  int  x,
991  int  xHigh,
992  Move ** moves)
993{
994    Move *move;
995    int  y;
996    int  size;
997    int  limitSize;
998    int  gybot;
999
1000
1001    /* Initialize R */
1002    limitSize = size = table->keysZ;
1003    y = cuddZddNextHigh(table,x);
1004    while (y <= xHigh) {
1005        /* Find bottom of y group. */
1006        gybot = table->subtableZ[y].next;
1007        while (table->subtableZ[gybot].next != (unsigned) y)
1008            gybot = table->subtableZ[gybot].next;
1009
1010        if (table->subtableZ[x].next == (unsigned) x &&
1011            table->subtableZ[y].next == (unsigned) y) {
1012            /* x and y are self groups */
1013            size = cuddZddSwapInPlace(table,x,y);
1014#ifdef DD_DEBUG
1015            assert(table->subtableZ[x].next == (unsigned) x);
1016            assert(table->subtableZ[y].next == (unsigned) y);
1017#endif
1018            if (size == 0) goto zddGroupSiftingDownOutOfMem;
1019
1020            /* Record move. */
1021            move = (Move *) cuddDynamicAllocNode(table);
1022            if (move == NULL) goto zddGroupSiftingDownOutOfMem;
1023            move->x = x;
1024            move->y = y;
1025            move->flags = MTR_DEFAULT;
1026            move->size = size;
1027            move->next = *moves;
1028            *moves = move;
1029
1030#ifdef DD_DEBUG
1031            if (pr > 0) (void) fprintf(table->out,"zddGroupSiftingDown (2 single groups):\n");
1032#endif
1033            if ((double) size > (double) limitSize * table->maxGrowth)
1034                return(1);
1035            if (size < limitSize) limitSize = size;
1036            x = y;
1037            y = cuddZddNextHigh(table,x);
1038        } else { /* Group move */
1039            size = zddGroupMove(table,x,y,moves);
1040            if (size == 0) goto zddGroupSiftingDownOutOfMem;
1041            if ((double) size > (double) limitSize * table->maxGrowth)
1042                return(1);
1043            if (size < limitSize) limitSize = size;
1044        }
1045        x = gybot;
1046        y = cuddZddNextHigh(table,x);
1047    }
1048
1049    return(1);
1050
1051zddGroupSiftingDownOutOfMem:
1052    while (*moves != NULL) {
1053        move = (*moves)->next;
1054        cuddDeallocMove(table, *moves);
1055        *moves = move;
1056    }
1057
1058    return(0);
1059
1060} /* end of zddGroupSiftingDown */
1061
1062
1063/**Function********************************************************************
1064
1065  Synopsis    [Swaps two groups and records the move.]
1066
1067  Description [Swaps two groups and records the move. Returns the
1068  number of keys in the DD table in case of success; 0 otherwise.]
1069
1070  SideEffects [None]
1071
1072******************************************************************************/
1073static int
1074zddGroupMove(
1075  DdManager * table,
1076  int  x,
1077  int  y,
1078  Move ** moves)
1079{
1080    Move *move;
1081    int  size;
1082    int  i,j,xtop,xbot,xsize,ytop,ybot,ysize,newxtop;
1083    int  swapx,swapy;
1084#if defined(DD_DEBUG) && defined(DD_VERBOSE)
1085    int  initialSize,bestSize;
1086#endif
1087
1088#ifdef DD_DEBUG
1089    /* We assume that x < y */
1090    assert(x < y);
1091#endif
1092    /* Find top, bottom, and size for the two groups. */
1093    xbot = x;
1094    xtop = table->subtableZ[x].next;
1095    xsize = xbot - xtop + 1;
1096    ybot = y;
1097    while ((unsigned) ybot < table->subtableZ[ybot].next)
1098        ybot = table->subtableZ[ybot].next;
1099    ytop = y;
1100    ysize = ybot - ytop + 1;
1101
1102#if defined(DD_DEBUG) && defined(DD_VERBOSE)
1103    initialSize = bestSize = table->keysZ;
1104#endif
1105    /* Sift the variables of the second group up through the first group */
1106    for (i = 1; i <= ysize; i++) {
1107        for (j = 1; j <= xsize; j++) {
1108            size = cuddZddSwapInPlace(table,x,y);
1109            if (size == 0) goto zddGroupMoveOutOfMem;
1110#if defined(DD_DEBUG) && defined(DD_VERBOSE)
1111            if (size < bestSize)
1112                bestSize = size;
1113#endif
1114            swapx = x; swapy = y;
1115            y = x;
1116            x = cuddZddNextLow(table,y);
1117        }
1118        y = ytop + i;
1119        x = cuddZddNextLow(table,y);
1120    }
1121#if defined(DD_DEBUG) && defined(DD_VERBOSE)
1122    if ((bestSize < initialSize) && (bestSize < size))
1123        (void) fprintf(table->out,"Missed local minimum: initialSize:%d  bestSize:%d  finalSize:%d\n",initialSize,bestSize,size);
1124#endif
1125
1126    /* fix groups */
1127    y = xtop; /* ytop is now where xtop used to be */
1128    for (i = 0; i < ysize - 1; i++) {
1129        table->subtableZ[y].next = cuddZddNextHigh(table,y);
1130        y = cuddZddNextHigh(table,y);
1131    }
1132    table->subtableZ[y].next = xtop; /* y is bottom of its group, join */
1133                                    /* it to top of its group */
1134    x = cuddZddNextHigh(table,y);
1135    newxtop = x;
1136    for (i = 0; i < xsize - 1; i++) {
1137        table->subtableZ[x].next = cuddZddNextHigh(table,x);
1138        x = cuddZddNextHigh(table,x);
1139    }
1140    table->subtableZ[x].next = newxtop; /* x is bottom of its group, join */
1141                                    /* it to top of its group */
1142#ifdef DD_DEBUG
1143    if (pr > 0) (void) fprintf(table->out,"zddGroupMove:\n");
1144#endif
1145
1146    /* Store group move */
1147    move = (Move *) cuddDynamicAllocNode(table);
1148    if (move == NULL) goto zddGroupMoveOutOfMem;
1149    move->x = swapx;
1150    move->y = swapy;
1151    move->flags = MTR_DEFAULT;
1152    move->size = table->keysZ;
1153    move->next = *moves;
1154    *moves = move;
1155
1156    return(table->keysZ);
1157
1158zddGroupMoveOutOfMem:
1159    while (*moves != NULL) {
1160        move = (*moves)->next;
1161        cuddDeallocMove(table, *moves);
1162        *moves = move;
1163    }
1164    return(0);
1165
1166} /* end of zddGroupMove */
1167
1168
1169/**Function********************************************************************
1170
1171  Synopsis    [Undoes the swap two groups.]
1172
1173  Description [Undoes the swap two groups.  Returns 1 in case of
1174  success; 0 otherwise.]
1175
1176  SideEffects [None]
1177
1178******************************************************************************/
1179static int
1180zddGroupMoveBackward(
1181  DdManager * table,
1182  int  x,
1183  int  y)
1184{
1185    int size;
1186    int i,j,xtop,xbot,xsize,ytop,ybot,ysize,newxtop;
1187
1188
1189#ifdef DD_DEBUG
1190    /* We assume that x < y */
1191    assert(x < y);
1192#endif
1193
1194    /* Find top, bottom, and size for the two groups. */
1195    xbot = x;
1196    xtop = table->subtableZ[x].next;
1197    xsize = xbot - xtop + 1;
1198    ybot = y;
1199    while ((unsigned) ybot < table->subtableZ[ybot].next)
1200        ybot = table->subtableZ[ybot].next;
1201    ytop = y;
1202    ysize = ybot - ytop + 1;
1203
1204    /* Sift the variables of the second group up through the first group */
1205    for (i = 1; i <= ysize; i++) {
1206        for (j = 1; j <= xsize; j++) {
1207            size = cuddZddSwapInPlace(table,x,y);
1208            if (size == 0)
1209                return(0);
1210            y = x;
1211            x = cuddZddNextLow(table,y);
1212        }
1213        y = ytop + i;
1214        x = cuddZddNextLow(table,y);
1215    }
1216
1217    /* fix groups */
1218    y = xtop;
1219    for (i = 0; i < ysize - 1; i++) {
1220        table->subtableZ[y].next = cuddZddNextHigh(table,y);
1221        y = cuddZddNextHigh(table,y);
1222    }
1223    table->subtableZ[y].next = xtop; /* y is bottom of its group, join */
1224                                    /* to its top */
1225    x = cuddZddNextHigh(table,y);
1226    newxtop = x;
1227    for (i = 0; i < xsize - 1; i++) {
1228        table->subtableZ[x].next = cuddZddNextHigh(table,x);
1229        x = cuddZddNextHigh(table,x);
1230    }
1231    table->subtableZ[x].next = newxtop; /* x is bottom of its group, join */
1232                                    /* to its top */
1233#ifdef DD_DEBUG
1234    if (pr > 0) (void) fprintf(table->out,"zddGroupMoveBackward:\n");
1235#endif
1236
1237    return(1);
1238
1239} /* end of zddGroupMoveBackward */
1240
1241
1242/**Function********************************************************************
1243
1244  Synopsis    [Determines the best position for a variables and returns
1245  it there.]
1246
1247  Description [Determines the best position for a variables and returns
1248  it there.  Returns 1 in case of success; 0 otherwise.]
1249
1250  SideEffects [None]
1251
1252******************************************************************************/
1253static int
1254zddGroupSiftingBackward(
1255  DdManager * table,
1256  Move * moves,
1257  int  size)
1258{
1259    Move *move;
1260    int  res;
1261
1262
1263    for (move = moves; move != NULL; move = move->next) {
1264        if (move->size < size) {
1265            size = move->size;
1266        }
1267    }
1268
1269    for (move = moves; move != NULL; move = move->next) {
1270        if (move->size == size) return(1);
1271        if ((table->subtableZ[move->x].next == move->x) &&
1272        (table->subtableZ[move->y].next == move->y)) {
1273            res = cuddZddSwapInPlace(table,(int)move->x,(int)move->y);
1274            if (!res) return(0);
1275#ifdef DD_DEBUG
1276            if (pr > 0) (void) fprintf(table->out,"zddGroupSiftingBackward:\n");
1277            assert(table->subtableZ[move->x].next == move->x);
1278            assert(table->subtableZ[move->y].next == move->y);
1279#endif
1280        } else { /* Group move necessary */
1281            res = zddGroupMoveBackward(table,(int)move->x,(int)move->y);
1282            if (!res) return(0);
1283        }
1284    }
1285
1286    return(1);
1287
1288} /* end of zddGroupSiftingBackward */
1289
1290
1291/**Function********************************************************************
1292
1293  Synopsis    [Merges groups in the DD table.]
1294
1295  Description [Creates a single group from low to high and adjusts the
1296  idex field of the tree node.]
1297
1298  SideEffects [None]
1299
1300******************************************************************************/
1301static void
1302zddMergeGroups(
1303  DdManager * table,
1304  MtrNode * treenode,
1305  int  low,
1306  int  high)
1307{
1308    int i;
1309    MtrNode *auxnode;
1310    int saveindex;
1311    int newindex;
1312
1313    /* Merge all variables from low to high in one group, unless
1314    ** this is the topmost group. In such a case we do not merge lest
1315    ** we lose the symmetry information. */
1316    if (treenode != table->treeZ) {
1317        for (i = low; i < high; i++)
1318            table->subtableZ[i].next = i+1;
1319        table->subtableZ[high].next = low;
1320    }
1321
1322    /* Adjust the index fields of the tree nodes. If a node is the
1323    ** first child of its parent, then the parent may also need adjustment. */
1324    saveindex = treenode->index;
1325    newindex = table->invpermZ[low];
1326    auxnode = treenode;
1327    do {
1328        auxnode->index = newindex;
1329        if (auxnode->parent == NULL ||
1330                (int) auxnode->parent->index != saveindex)
1331            break;
1332        auxnode = auxnode->parent;
1333    } while (1);
1334    return;
1335
1336} /* end of zddMergeGroups */
Note: See TracBrowser for help on using the repository browser.