source: vis_dev/glu-2.3/src/cuBdd/cuddZddReord.c @ 66

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

library glu 2.3
File size: 44.2 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [cuddZddReord.c]
4
5  PackageName [cudd]
6
7  Synopsis    [Procedures for dynamic variable ordering of ZDDs.]
8
9  Description [External procedures included in this module:
10                    <ul>
11                    <li> Cudd_zddReduceHeap()
12                    <li> Cudd_zddShuffleHeap()
13                    </ul>
14               Internal procedures included in this module:
15                    <ul>
16                    <li> cuddZddAlignToBdd()
17                    <li> cuddZddNextHigh()
18                    <li> cuddZddNextLow()
19                    <li> cuddZddUniqueCompare()
20                    <li> cuddZddSwapInPlace()
21                    <li> cuddZddSwapping()
22                    <li> cuddZddSifting()
23                    </ul>
24               Static procedures included in this module:
25                    <ul>
26                    <li> zddSwapAny()
27                    <li> cuddZddSiftingAux()
28                    <li> cuddZddSiftingUp()
29                    <li> cuddZddSiftingDown()
30                    <li> cuddZddSiftingBackward()
31                    <li> zddReorderPreprocess()
32                    <li> zddReorderPostprocess()
33                    <li> zddShuffle()
34                    <li> zddSiftUp()
35                    </ul>
36              ]
37
38  SeeAlso     []
39
40  Author      [Hyong-Kyoon Shin, In-Ho Moon]
41
42  Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado
43
44  All rights reserved.
45
46  Redistribution and use in source and binary forms, with or without
47  modification, are permitted provided that the following conditions
48  are met:
49
50  Redistributions of source code must retain the above copyright
51  notice, this list of conditions and the following disclaimer.
52
53  Redistributions in binary form must reproduce the above copyright
54  notice, this list of conditions and the following disclaimer in the
55  documentation and/or other materials provided with the distribution.
56
57  Neither the name of the University of Colorado nor the names of its
58  contributors may be used to endorse or promote products derived from
59  this software without specific prior written permission.
60
61  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
62  "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
63  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
64  FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
65  COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
66  INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
67  BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
68  LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
69  CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
70  LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
71  ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
72  POSSIBILITY OF SUCH DAMAGE.]
73
74******************************************************************************/
75
76#include "util.h"
77#include "cuddInt.h"
78
79/*---------------------------------------------------------------------------*/
80/* Constant declarations                                                     */
81/*---------------------------------------------------------------------------*/
82
83#define DD_MAX_SUBTABLE_SPARSITY 8
84#define DD_SHRINK_FACTOR 2
85
86/*---------------------------------------------------------------------------*/
87/* Stucture declarations                                                     */
88/*---------------------------------------------------------------------------*/
89
90
91/*---------------------------------------------------------------------------*/
92/* Type declarations                                                         */
93/*---------------------------------------------------------------------------*/
94
95
96/*---------------------------------------------------------------------------*/
97/* Variable declarations                                                     */
98/*---------------------------------------------------------------------------*/
99
100#ifndef lint
101static char rcsid[] DD_UNUSED = "$Id: cuddZddReord.c,v 1.47 2004/08/13 18:04:53 fabio Exp $";
102#endif
103
104int     *zdd_entry;
105
106int     zddTotalNumberSwapping;
107
108static  DdNode  *empty;
109
110
111/*---------------------------------------------------------------------------*/
112/* Macro declarations                                                        */
113/*---------------------------------------------------------------------------*/
114
115
116/**AutomaticStart*************************************************************/
117
118/*---------------------------------------------------------------------------*/
119/* Static function prototypes                                                */
120/*---------------------------------------------------------------------------*/
121
122static Move * zddSwapAny (DdManager *table, int x, int y);
123static int cuddZddSiftingAux (DdManager *table, int x, int x_low, int x_high);
124static Move * cuddZddSiftingUp (DdManager *table, int x, int x_low, int initial_size);
125static Move * cuddZddSiftingDown (DdManager *table, int x, int x_high, int initial_size);
126static int cuddZddSiftingBackward (DdManager *table, Move *moves, int size);
127static void zddReorderPreprocess (DdManager *table);
128static int zddReorderPostprocess (DdManager *table);
129static int zddShuffle (DdManager *table, int *permutation);
130static int zddSiftUp (DdManager *table, int x, int xLow);
131static void zddFixTree (DdManager *table, MtrNode *treenode);
132
133/**AutomaticEnd***************************************************************/
134
135
136/*---------------------------------------------------------------------------*/
137/* Definition of exported functions                                          */
138/*---------------------------------------------------------------------------*/
139
140
141/**Function********************************************************************
142
143  Synopsis    [Main dynamic reordering routine for ZDDs.]
144
145  Description [Main dynamic reordering routine for ZDDs.
146  Calls one of the possible reordering procedures:
147  <ul>
148  <li>Swapping
149  <li>Sifting
150  <li>Symmetric Sifting
151  </ul>
152
153  For sifting and symmetric sifting it is possible to request reordering
154  to convergence.<p>
155
156  The core of all methods is the reordering procedure
157  cuddZddSwapInPlace() which swaps two adjacent variables.
158  Returns 1 in case of success; 0 otherwise. In the case of symmetric
159  sifting (with and without convergence) returns 1 plus the number of
160  symmetric variables, in case of success.]
161
162  SideEffects [Changes the variable order for all ZDDs and clears
163  the cache.]
164
165******************************************************************************/
166int
167Cudd_zddReduceHeap(
168  DdManager * table /* DD manager */,
169  Cudd_ReorderingType heuristic /* method used for reordering */,
170  int minsize /* bound below which no reordering occurs */)
171{
172    DdHook       *hook;
173    int          result;
174    unsigned int nextDyn;
175#ifdef DD_STATS
176    unsigned int initialSize;
177    unsigned int finalSize;
178#endif
179    long         localTime;
180
181    /* Don't reorder if there are too many dead nodes. */
182    if (table->keysZ - table->deadZ < (unsigned) minsize)
183        return(1);
184
185    if (heuristic == CUDD_REORDER_SAME) {
186        heuristic = table->autoMethodZ;
187    }
188    if (heuristic == CUDD_REORDER_NONE) {
189        return(1);
190    }
191
192    /* This call to Cudd_zddReduceHeap does initiate reordering. Therefore
193    ** we count it.
194    */
195    table->reorderings++;
196    empty = table->zero;
197
198    localTime = util_cpu_time();
199
200    /* Run the hook functions. */
201    hook = table->preReorderingHook;
202    while (hook != NULL) {
203        int res = (hook->f)(table, "ZDD", (void *)heuristic);
204        if (res == 0) return(0);
205        hook = hook->next;
206    }
207
208    /* Clear the cache and collect garbage. */
209    zddReorderPreprocess(table);
210    zddTotalNumberSwapping = 0;
211
212#ifdef DD_STATS
213    initialSize = table->keysZ;
214
215    switch(heuristic) {
216    case CUDD_REORDER_RANDOM:
217    case CUDD_REORDER_RANDOM_PIVOT:
218        (void) fprintf(table->out,"#:I_RANDOM  ");
219        break;
220    case CUDD_REORDER_SIFT:
221    case CUDD_REORDER_SIFT_CONVERGE:
222    case CUDD_REORDER_SYMM_SIFT:
223    case CUDD_REORDER_SYMM_SIFT_CONV:
224        (void) fprintf(table->out,"#:I_SIFTING ");
225        break;
226    case CUDD_REORDER_LINEAR:
227    case CUDD_REORDER_LINEAR_CONVERGE:
228        (void) fprintf(table->out,"#:I_LINSIFT ");
229        break;
230    default:
231        (void) fprintf(table->err,"Unsupported ZDD reordering method\n");
232        return(0);
233    }
234    (void) fprintf(table->out,"%8d: initial size",initialSize); 
235#endif
236
237    result = cuddZddTreeSifting(table,heuristic);
238
239#ifdef DD_STATS
240    (void) fprintf(table->out,"\n");
241    finalSize = table->keysZ;
242    (void) fprintf(table->out,"#:F_REORDER %8d: final size\n",finalSize); 
243    (void) fprintf(table->out,"#:T_REORDER %8g: total time (sec)\n",
244                   ((double)(util_cpu_time() - localTime)/1000.0)); 
245    (void) fprintf(table->out,"#:N_REORDER %8d: total swaps\n",
246                   zddTotalNumberSwapping);
247#endif
248
249    if (result == 0)
250        return(0);
251
252    if (!zddReorderPostprocess(table))
253        return(0);
254
255    if (table->realignZ) {
256        if (!cuddBddAlignToZdd(table))
257            return(0);
258    }
259
260    nextDyn = table->keysZ * DD_DYN_RATIO;
261    if (table->reorderings < 20 || nextDyn > table->nextDyn)
262        table->nextDyn = nextDyn;
263    else
264        table->nextDyn += 20;
265
266    table->reordered = 1;
267
268    /* Run hook functions. */
269    hook = table->postReorderingHook;
270    while (hook != NULL) {
271        int res = (hook->f)(table, "ZDD", (void *)localTime);
272        if (res == 0) return(0);
273        hook = hook->next;
274    }
275    /* Update cumulative reordering time. */
276    table->reordTime += util_cpu_time() - localTime;
277
278    return(result);
279
280} /* end of Cudd_zddReduceHeap */
281
282
283/**Function********************************************************************
284
285  Synopsis    [Reorders ZDD variables according to given permutation.]
286
287  Description [Reorders ZDD variables according to given permutation.
288  The i-th entry of the permutation array contains the index of the variable
289  that should be brought to the i-th level.  The size of the array should be
290  equal or greater to the number of variables currently in use.
291  Returns 1 in case of success; 0 otherwise.]
292
293  SideEffects [Changes the ZDD variable order for all diagrams and clears
294  the cache.]
295
296  SeeAlso [Cudd_zddReduceHeap]
297
298******************************************************************************/
299int
300Cudd_zddShuffleHeap(
301  DdManager * table /* DD manager */,
302  int * permutation /* required variable permutation */)
303{
304
305    int result;
306
307    empty = table->zero;
308    zddReorderPreprocess(table);
309
310    result = zddShuffle(table,permutation);
311
312    if (!zddReorderPostprocess(table)) return(0);
313
314    return(result);
315
316} /* end of Cudd_zddShuffleHeap */
317
318
319/*---------------------------------------------------------------------------*/
320/* Definition of internal functions                                          */
321/*---------------------------------------------------------------------------*/
322
323
324/**Function********************************************************************
325
326  Synopsis    [Reorders ZDD variables according to the order of the BDD
327  variables.]
328
329  Description [Reorders ZDD variables according to the order of the
330  BDD variables. This function can be called at the end of BDD
331  reordering to insure that the order of the ZDD variables is
332  consistent with the order of the BDD variables. The number of ZDD
333  variables must be a multiple of the number of BDD variables. Let
334  <code>M</code> be the ratio of the two numbers. cuddZddAlignToBdd
335  then considers the ZDD variables from <code>M*i</code> to
336  <code>(M+1)*i-1</code> as corresponding to BDD variable
337  <code>i</code>.  This function should be normally called from
338  Cudd_ReduceHeap, which clears the cache.  Returns 1 in case of
339  success; 0 otherwise.]
340
341  SideEffects [Changes the ZDD variable order for all diagrams and performs
342  garbage collection of the ZDD unique table.]
343
344  SeeAlso [Cudd_zddShuffleHeap Cudd_ReduceHeap]
345
346******************************************************************************/
347int
348cuddZddAlignToBdd(
349  DdManager * table /* DD manager */)
350{
351    int *invpermZ;              /* permutation array */
352    int M;                      /* ratio of ZDD variables to BDD variables */
353    int i,j;                    /* loop indices */
354    int result;                 /* return value */
355
356    /* We assume that a ratio of 0 is OK. */
357    if (table->sizeZ == 0)
358        return(1);
359
360    empty = table->zero;
361    M = table->sizeZ / table->size;
362    /* Check whether the number of ZDD variables is a multiple of the
363    ** number of BDD variables.
364    */
365    if (M * table->size != table->sizeZ)
366        return(0);
367    /* Create and initialize the inverse permutation array. */
368    invpermZ = ALLOC(int,table->sizeZ);
369    if (invpermZ == NULL) {
370        table->errorCode = CUDD_MEMORY_OUT;
371        return(0);
372    }
373    for (i = 0; i < table->size; i++) {
374        int index = table->invperm[i];
375        int indexZ = index * M;
376        int levelZ = table->permZ[indexZ];
377        levelZ = (levelZ / M) * M;
378        for (j = 0; j < M; j++) {
379            invpermZ[M * i + j] = table->invpermZ[levelZ + j];
380        }
381    }
382    /* Eliminate dead nodes. Do not scan the cache again, because we
383    ** assume that Cudd_ReduceHeap has already cleared it.
384    */
385    cuddGarbageCollect(table,0);
386
387    result = zddShuffle(table, invpermZ);
388    FREE(invpermZ);
389    /* Fix the ZDD variable group tree. */
390    zddFixTree(table,table->treeZ);
391    return(result);
392   
393} /* end of cuddZddAlignToBdd */
394
395
396/**Function********************************************************************
397
398  Synopsis    [Finds the next subtable with a larger index.]
399
400  Description [Finds the next subtable with a larger index. Returns the
401  index.]
402
403  SideEffects [None]
404
405  SeeAlso     []
406
407******************************************************************************/
408int
409cuddZddNextHigh(
410  DdManager * table,
411  int  x)
412{
413    return(x + 1);
414
415} /* end of cuddZddNextHigh */
416
417
418/**Function********************************************************************
419
420  Synopsis    [Finds the next subtable with a smaller index.]
421
422  Description [Finds the next subtable with a smaller index. Returns the
423  index.]
424
425  SideEffects [None]
426
427  SeeAlso     []
428
429******************************************************************************/
430int
431cuddZddNextLow(
432  DdManager * table,
433  int  x)
434{
435    return(x - 1);
436
437} /* end of cuddZddNextLow */
438
439
440/**Function********************************************************************
441
442  Synopsis [Comparison function used by qsort.]
443
444  Description [Comparison function used by qsort to order the
445  variables according to the number of keys in the subtables.
446  Returns the difference in number of keys between the two
447  variables being compared.]
448
449  SideEffects [None]
450
451  SeeAlso     []
452
453******************************************************************************/
454int
455cuddZddUniqueCompare(
456  int * ptr_x,
457  int * ptr_y)
458{
459    return(zdd_entry[*ptr_y] - zdd_entry[*ptr_x]);
460
461} /* end of cuddZddUniqueCompare */
462
463
464/**Function********************************************************************
465
466  Synopsis    [Swaps two adjacent variables.]
467
468  Description [Swaps two adjacent variables. It assumes that no dead
469  nodes are present on entry to this procedure.  The procedure then
470  guarantees that no dead nodes will be present when it terminates.
471  cuddZddSwapInPlace assumes that x &lt; y.  Returns the number of keys in
472  the table if successful; 0 otherwise.]
473
474  SideEffects [None]
475
476  SeeAlso     []
477
478******************************************************************************/
479int
480cuddZddSwapInPlace(
481  DdManager * table,
482  int  x,
483  int  y)
484{
485    DdNodePtr   *xlist, *ylist;
486    int         xindex, yindex;
487    int         xslots, yslots;
488    int         xshift, yshift;
489    int         oldxkeys, oldykeys;
490    int         newxkeys, newykeys;
491    int         i;
492    int         posn;
493    DdNode      *f, *f1, *f0, *f11, *f10, *f01, *f00;
494    DdNode      *newf1, *newf0, *next;
495    DdNodePtr   g, *lastP, *previousP;
496
497#ifdef DD_DEBUG
498    assert(x < y);
499    assert(cuddZddNextHigh(table,x) == y);
500    assert(table->subtableZ[x].keys != 0);
501    assert(table->subtableZ[y].keys != 0);
502    assert(table->subtableZ[x].dead == 0);
503    assert(table->subtableZ[y].dead == 0);
504#endif
505
506    zddTotalNumberSwapping++;
507
508    /* Get parameters of x subtable. */
509    xindex   = table->invpermZ[x];
510    xlist    = table->subtableZ[x].nodelist;
511    oldxkeys = table->subtableZ[x].keys;
512    xslots   = table->subtableZ[x].slots;
513    xshift   = table->subtableZ[x].shift;
514    newxkeys = 0;
515
516    yindex   = table->invpermZ[y];
517    ylist    = table->subtableZ[y].nodelist;
518    oldykeys = table->subtableZ[y].keys;
519    yslots   = table->subtableZ[y].slots;
520    yshift   = table->subtableZ[y].shift;
521    newykeys = oldykeys;
522
523    /* The nodes in the x layer that don't depend on y directly
524    ** will stay there; the others are put in a chain.
525    ** The chain is handled as a FIFO; g points to the beginning and
526    ** last points to the end.
527    */
528
529    g = NULL;
530    lastP = &g;
531    for (i = 0; i < xslots; i++) {
532        previousP = &(xlist[i]);
533        f = *previousP;
534        while (f != NULL) {
535            next = f->next;
536            f1 = cuddT(f); f0 = cuddE(f);
537            if ((f1->index != (DdHalfWord) yindex) &&
538                (f0->index != (DdHalfWord) yindex)) { /* stays */
539                newxkeys++;
540                *previousP = f;
541                previousP = &(f->next);
542            } else {
543                f->index = yindex;
544                *lastP = f;
545                lastP = &(f->next);
546            }
547            f = next;
548        } /* while there are elements in the collision chain */
549        *previousP = NULL;
550    } /* for each slot of the x subtable */
551    *lastP = NULL;
552
553
554#ifdef DD_COUNT
555    table->swapSteps += oldxkeys - newxkeys;
556#endif
557    /* Take care of the x nodes that must be re-expressed.
558    ** They form a linked list pointed by g. Their index has been
559    ** changed to yindex already.
560    */
561    f = g;
562    while (f != NULL) {
563        next = f->next;
564        /* Find f1, f0, f11, f10, f01, f00. */
565        f1 = cuddT(f);
566        if ((int) f1->index == yindex) {
567            f11 = cuddT(f1); f10 = cuddE(f1);
568        } else {
569            f11 = empty; f10 = f1;
570        }
571        f0 = cuddE(f);
572        if ((int) f0->index == yindex) {
573            f01 = cuddT(f0); f00 = cuddE(f0);
574        } else {
575            f01 = empty; f00 = f0;
576        }
577
578        /* Decrease ref count of f1. */
579        cuddSatDec(f1->ref);
580        /* Create the new T child. */
581        if (f11 == empty) {
582            if (f01 != empty) {
583                newf1 = f01;
584                cuddSatInc(newf1->ref);
585            }
586            /* else case was already handled when finding nodes
587            ** with both children below level y
588            */
589        } else {
590            /* Check xlist for triple (xindex, f11, f01). */
591            posn = ddHash(f11, f01, xshift);
592            /* For each element newf1 in collision list xlist[posn]. */
593            newf1 = xlist[posn];
594            while (newf1 != NULL) {
595                if (cuddT(newf1) == f11 && cuddE(newf1) == f01) {
596                    cuddSatInc(newf1->ref);
597                    break; /* match */
598                }
599                newf1 = newf1->next;
600            } /* while newf1 */
601            if (newf1 == NULL) {        /* no match */
602                newf1 = cuddDynamicAllocNode(table);
603                if (newf1 == NULL)
604                    goto zddSwapOutOfMem;
605                newf1->index = xindex; newf1->ref = 1;
606                cuddT(newf1) = f11;
607                cuddE(newf1) = f01;
608                /* Insert newf1 in the collision list xlist[pos];
609                ** increase the ref counts of f11 and f01
610                */
611                newxkeys++;
612                newf1->next = xlist[posn];
613                xlist[posn] = newf1;
614                cuddSatInc(f11->ref);
615                cuddSatInc(f01->ref);
616            }
617        }
618        cuddT(f) = newf1;
619
620        /* Do the same for f0. */
621        /* Decrease ref count of f0. */
622        cuddSatDec(f0->ref);
623        /* Create the new E child. */
624        if (f10 == empty) {
625            newf0 = f00;
626            cuddSatInc(newf0->ref);
627        } else {
628            /* Check xlist for triple (xindex, f10, f00). */
629            posn = ddHash(f10, f00, xshift);
630            /* For each element newf0 in collision list xlist[posn]. */
631            newf0 = xlist[posn];
632            while (newf0 != NULL) {
633                if (cuddT(newf0) == f10 && cuddE(newf0) == f00) {
634                    cuddSatInc(newf0->ref);
635                    break; /* match */
636                }
637                newf0 = newf0->next;
638            } /* while newf0 */
639            if (newf0 == NULL) {        /* no match */
640                newf0 = cuddDynamicAllocNode(table);
641                if (newf0 == NULL)
642                    goto zddSwapOutOfMem;
643                newf0->index = xindex; newf0->ref = 1;
644                cuddT(newf0) = f10; cuddE(newf0) = f00;
645                /* Insert newf0 in the collision list xlist[posn];
646                ** increase the ref counts of f10 and f00.
647                */
648                newxkeys++;
649                newf0->next = xlist[posn];
650                xlist[posn] = newf0;
651                cuddSatInc(f10->ref);
652                cuddSatInc(f00->ref);
653            }
654        }
655        cuddE(f) = newf0;
656
657        /* Insert the modified f in ylist.
658        ** The modified f does not already exists in ylist.
659        ** (Because of the uniqueness of the cofactors.)
660        */
661        posn = ddHash(newf1, newf0, yshift);
662        newykeys++;
663        f->next = ylist[posn];
664        ylist[posn] = f;
665        f = next;
666    } /* while f != NULL */
667
668    /* GC the y layer. */
669
670    /* For each node f in ylist. */
671    for (i = 0; i < yslots; i++) {
672        previousP = &(ylist[i]);
673        f = *previousP;
674        while (f != NULL) {
675            next = f->next;
676            if (f->ref == 0) {
677                cuddSatDec(cuddT(f)->ref);
678                cuddSatDec(cuddE(f)->ref);
679                cuddDeallocNode(table, f);
680                newykeys--;
681            } else {
682                *previousP = f;
683                previousP = &(f->next);
684            }
685            f = next;
686        } /* while f */
687        *previousP = NULL;
688    } /* for i */
689
690    /* Set the appropriate fields in table. */
691    table->subtableZ[x].nodelist = ylist;
692    table->subtableZ[x].slots    = yslots;
693    table->subtableZ[x].shift    = yshift;
694    table->subtableZ[x].keys     = newykeys;
695    table->subtableZ[x].maxKeys  = yslots * DD_MAX_SUBTABLE_DENSITY;
696
697    table->subtableZ[y].nodelist = xlist;
698    table->subtableZ[y].slots    = xslots;
699    table->subtableZ[y].shift    = xshift;
700    table->subtableZ[y].keys     = newxkeys;
701    table->subtableZ[y].maxKeys  = xslots * DD_MAX_SUBTABLE_DENSITY;
702
703    table->permZ[xindex] = y; table->permZ[yindex] = x;
704    table->invpermZ[x] = yindex; table->invpermZ[y] = xindex;
705
706    table->keysZ += newxkeys + newykeys - oldxkeys - oldykeys;
707
708    /* Update univ section; univ[x] remains the same. */
709    table->univ[y] = cuddT(table->univ[x]);
710
711    return (table->keysZ);
712
713zddSwapOutOfMem:
714    (void) fprintf(table->err, "Error: cuddZddSwapInPlace out of memory\n");
715
716    return (0);
717
718} /* end of cuddZddSwapInPlace */
719
720
721/**Function********************************************************************
722
723  Synopsis    [Reorders variables by a sequence of (non-adjacent) swaps.]
724
725  Description [Implementation of Plessier's algorithm that reorders
726  variables by a sequence of (non-adjacent) swaps.
727    <ol>
728    <li> Select two variables (RANDOM or HEURISTIC).
729    <li> Permute these variables.
730    <li> If the nodes have decreased accept the permutation.
731    <li> Otherwise reconstruct the original heap.
732    <li> Loop.
733    </ol>
734  Returns 1 in case of success; 0 otherwise.]
735
736  SideEffects [None]
737
738  SeeAlso     []
739
740******************************************************************************/
741int
742cuddZddSwapping(
743  DdManager * table,
744  int lower,
745  int upper,
746  Cudd_ReorderingType heuristic)
747{
748    int i, j;
749    int max, keys;
750    int nvars;
751    int x, y;
752    int iterate;
753    int previousSize;
754    Move *moves, *move;
755    int pivot;
756    int modulo;
757    int result;
758
759#ifdef DD_DEBUG
760    /* Sanity check */
761    assert(lower >= 0 && upper < table->sizeZ && lower <= upper);
762#endif
763
764    nvars = upper - lower + 1;
765    iterate = nvars;
766
767    for (i = 0; i < iterate; i++) {
768        if (heuristic == CUDD_REORDER_RANDOM_PIVOT) {
769            /* Find pivot <= id with maximum keys. */
770            for (max = -1, j = lower; j <= upper; j++) {
771                if ((keys = table->subtableZ[j].keys) > max) {
772                    max = keys;
773                    pivot = j;
774                }
775            }
776
777            modulo = upper - pivot;
778            if (modulo == 0) {
779                y = pivot;      /* y = nvars-1 */
780            } else {
781                /* y = random # from {pivot+1 .. nvars-1} */
782                y = pivot + 1 + (int) (Cudd_Random() % modulo);
783            }
784
785            modulo = pivot - lower - 1;
786            if (modulo < 1) {   /* if pivot = 1 or 0 */
787                x = lower;
788            } else {
789                do { /* x = random # from {0 .. pivot-2} */
790                    x = (int) Cudd_Random() % modulo;
791                } while (x == y);
792                  /* Is this condition really needed, since x and y
793                     are in regions separated by pivot? */
794            }
795        } else {
796            x = (int) (Cudd_Random() % nvars) + lower;
797            do {
798                y = (int) (Cudd_Random() % nvars) + lower;
799            } while (x == y);
800        }
801
802        previousSize = table->keysZ;
803        moves = zddSwapAny(table, x, y);
804        if (moves == NULL)
805            goto cuddZddSwappingOutOfMem;
806
807        result = cuddZddSiftingBackward(table, moves, previousSize);
808        if (!result)
809            goto cuddZddSwappingOutOfMem;
810
811        while (moves != NULL) {
812            move = moves->next;
813            cuddDeallocMove(table, moves);
814            moves = move;
815        }
816#ifdef DD_STATS
817        if (table->keysZ < (unsigned) previousSize) {
818            (void) fprintf(table->out,"-");
819        } else if (table->keysZ > (unsigned) previousSize) {
820            (void) fprintf(table->out,"+");     /* should never happen */
821        } else {
822            (void) fprintf(table->out,"=");
823        }
824        fflush(table->out);
825#endif
826    }
827
828    return(1);
829
830cuddZddSwappingOutOfMem:
831    while (moves != NULL) {
832        move = moves->next;
833        cuddDeallocMove(table, moves);
834        moves = move;
835    }
836    return(0);
837
838} /* end of cuddZddSwapping */
839
840
841/**Function********************************************************************
842
843  Synopsis    [Implementation of Rudell's sifting algorithm.]
844
845  Description [Implementation of Rudell's sifting algorithm.
846  Assumes that no dead nodes are present.
847    <ol>
848    <li> Order all the variables according to the number of entries
849    in each unique table.
850    <li> Sift the variable up and down, remembering each time the
851    total size of the DD heap.
852    <li> Select the best permutation.
853    <li> Repeat 3 and 4 for all variables.
854    </ol>
855  Returns 1 if successful; 0 otherwise.]
856
857  SideEffects [None]
858
859  SeeAlso     []
860
861******************************************************************************/
862int
863cuddZddSifting(
864  DdManager * table,
865  int  lower,
866  int  upper)
867{
868    int i;
869    int *var;
870    int size;
871    int x;
872    int result;
873#ifdef DD_STATS
874    int previousSize;
875#endif
876
877    size = table->sizeZ;
878
879    /* Find order in which to sift variables. */
880    var = NULL;
881    zdd_entry = ALLOC(int, size);
882    if (zdd_entry == NULL) {
883        table->errorCode = CUDD_MEMORY_OUT;
884        goto cuddZddSiftingOutOfMem;
885    }
886    var = ALLOC(int, size);
887    if (var == NULL) {
888        table->errorCode = CUDD_MEMORY_OUT;
889        goto cuddZddSiftingOutOfMem;
890    }
891
892    for (i = 0; i < size; i++) {
893        x = table->permZ[i];
894        zdd_entry[i] = table->subtableZ[x].keys;
895        var[i] = i;
896    }
897
898    qsort((void *)var, size, sizeof(int), (DD_QSFP)cuddZddUniqueCompare);
899
900    /* Now sift. */
901    for (i = 0; i < ddMin(table->siftMaxVar, size); i++) {
902        if (zddTotalNumberSwapping >= table->siftMaxSwap)
903            break;
904        x = table->permZ[var[i]];
905        if (x < lower || x > upper) continue;
906#ifdef DD_STATS
907        previousSize = table->keysZ;
908#endif
909        result = cuddZddSiftingAux(table, x, lower, upper);
910        if (!result)
911            goto cuddZddSiftingOutOfMem;
912#ifdef DD_STATS
913        if (table->keysZ < (unsigned) previousSize) {
914            (void) fprintf(table->out,"-");
915        } else if (table->keysZ > (unsigned) previousSize) {
916            (void) fprintf(table->out,"+");     /* should never happen */
917            (void) fprintf(table->out,"\nSize increased from %d to %d while sifting variable %d\n", previousSize, table->keysZ , var[i]);
918        } else {
919            (void) fprintf(table->out,"=");
920        }
921        fflush(table->out);
922#endif
923    }
924
925    FREE(var);
926    FREE(zdd_entry);
927
928    return(1);
929
930cuddZddSiftingOutOfMem:
931
932    if (zdd_entry != NULL) FREE(zdd_entry);
933    if (var != NULL) FREE(var);
934
935    return(0);
936
937} /* end of cuddZddSifting */
938
939
940/*---------------------------------------------------------------------------*/
941/* Definition of static functions                                            */
942/*---------------------------------------------------------------------------*/
943
944
945/**Function********************************************************************
946
947  Synopsis    [Swaps any two variables.]
948
949  Description [Swaps any two variables. Returns the set of moves.]
950
951  SideEffects [None]
952
953  SeeAlso     []
954
955******************************************************************************/
956static Move *
957zddSwapAny(
958  DdManager * table,
959  int  x,
960  int  y)
961{
962    Move        *move, *moves;
963    int         tmp, size;
964    int         x_ref, y_ref;
965    int         x_next, y_next;
966    int         limit_size;
967
968    if (x > y) {        /* make x precede y */
969        tmp = x; x = y; y = tmp;
970    }
971
972    x_ref = x; y_ref = y;
973
974    x_next = cuddZddNextHigh(table, x);
975    y_next = cuddZddNextLow(table, y);
976    moves = NULL;
977    limit_size = table->keysZ;
978
979    for (;;) {
980        if (x_next == y_next) { /* x < x_next = y_next < y */
981            size = cuddZddSwapInPlace(table, x, x_next);
982            if (size == 0)
983                goto zddSwapAnyOutOfMem;
984            move = (Move *) cuddDynamicAllocNode(table);
985            if (move == NULL)
986                goto zddSwapAnyOutOfMem;
987            move->x = x;
988            move->y = x_next;
989            move->size = size;
990            move->next = moves;
991            moves = move;
992
993            size = cuddZddSwapInPlace(table, y_next, y);
994            if (size == 0)
995                goto zddSwapAnyOutOfMem;
996            move = (Move *)cuddDynamicAllocNode(table);
997            if (move == NULL)
998                goto zddSwapAnyOutOfMem;
999            move->x = y_next;
1000            move->y = y;
1001            move->size = size;
1002            move->next = moves;
1003            moves = move;
1004
1005            size = cuddZddSwapInPlace(table, x, x_next);
1006            if (size == 0)
1007                goto zddSwapAnyOutOfMem;
1008            move = (Move *)cuddDynamicAllocNode(table);
1009            if (move == NULL)
1010                goto zddSwapAnyOutOfMem;
1011            move->x = x;
1012            move->y = x_next;
1013            move->size = size;
1014            move->next = moves;
1015            moves = move;
1016
1017            tmp = x; x = y; y = tmp;
1018
1019        } else if (x == y_next) { /* x = y_next < y = x_next */
1020            size = cuddZddSwapInPlace(table, x, x_next);
1021            if (size == 0)
1022                goto zddSwapAnyOutOfMem;
1023            move = (Move *)cuddDynamicAllocNode(table);
1024            if (move == NULL)
1025                goto zddSwapAnyOutOfMem;
1026            move->x = x;
1027            move->y = x_next;
1028            move->size = size;
1029            move->next = moves;
1030            moves = move;
1031
1032            tmp = x; x = y;  y = tmp;
1033        } else {
1034            size = cuddZddSwapInPlace(table, x, x_next);
1035            if (size == 0)
1036                goto zddSwapAnyOutOfMem;
1037            move = (Move *)cuddDynamicAllocNode(table);
1038            if (move == NULL)
1039                goto zddSwapAnyOutOfMem;
1040            move->x = x;
1041            move->y = x_next;
1042            move->size = size;
1043            move->next = moves;
1044            moves = move;
1045
1046            size = cuddZddSwapInPlace(table, y_next, y);
1047            if (size == 0)
1048                goto zddSwapAnyOutOfMem;
1049            move = (Move *)cuddDynamicAllocNode(table);
1050            if (move == NULL)
1051                goto zddSwapAnyOutOfMem;
1052            move->x = y_next;
1053            move->y = y;
1054            move->size = size;
1055            move->next = moves;
1056            moves = move;
1057
1058            x = x_next; y = y_next;
1059        }
1060
1061        x_next = cuddZddNextHigh(table, x);
1062        y_next = cuddZddNextLow(table, y);
1063        if (x_next > y_ref)
1064            break;      /* if x == y_ref */
1065
1066        if ((double) size > table->maxGrowth * (double) limit_size)
1067            break;
1068        if (size < limit_size)
1069            limit_size = size;
1070    }
1071    if (y_next >= x_ref) {
1072        size = cuddZddSwapInPlace(table, y_next, y);
1073        if (size == 0)
1074            goto zddSwapAnyOutOfMem;
1075        move = (Move *)cuddDynamicAllocNode(table);
1076        if (move == NULL)
1077            goto zddSwapAnyOutOfMem;
1078        move->x = y_next;
1079        move->y = y;
1080        move->size = size;
1081        move->next = moves;
1082        moves = move;
1083    }
1084
1085    return(moves);
1086
1087zddSwapAnyOutOfMem:
1088    while (moves != NULL) {
1089        move = moves->next;
1090        cuddDeallocMove(table, moves);
1091        moves = move;
1092    }
1093    return(NULL);
1094
1095} /* end of zddSwapAny */
1096
1097
1098/**Function********************************************************************
1099
1100  Synopsis    [Given xLow <= x <= xHigh moves x up and down between the
1101  boundaries.]
1102
1103  Description [Given xLow <= x <= xHigh moves x up and down between the
1104  boundaries. Finds the best position and does the required changes.
1105  Returns 1 if successful; 0 otherwise.]
1106
1107  SideEffects [None]
1108
1109  SeeAlso     []
1110
1111******************************************************************************/
1112static int
1113cuddZddSiftingAux(
1114  DdManager * table,
1115  int  x,
1116  int  x_low,
1117  int  x_high)
1118{
1119    Move        *move;
1120    Move        *moveUp;        /* list of up move */
1121    Move        *moveDown;      /* list of down move */
1122
1123    int         initial_size;
1124    int         result;
1125
1126    initial_size = table->keysZ;
1127
1128#ifdef DD_DEBUG
1129    assert(table->subtableZ[x].keys > 0);
1130#endif
1131
1132    moveDown = NULL;
1133    moveUp = NULL;
1134
1135    if (x == x_low) {
1136        moveDown = cuddZddSiftingDown(table, x, x_high, initial_size);
1137        /* after that point x --> x_high */
1138        if (moveDown == NULL)
1139            goto cuddZddSiftingAuxOutOfMem;
1140        result = cuddZddSiftingBackward(table, moveDown,
1141            initial_size);
1142        /* move backward and stop at best position */
1143        if (!result)
1144            goto cuddZddSiftingAuxOutOfMem;
1145
1146    }
1147    else if (x == x_high) {
1148        moveUp = cuddZddSiftingUp(table, x, x_low, initial_size);
1149        /* after that point x --> x_low */
1150        if (moveUp == NULL)
1151            goto cuddZddSiftingAuxOutOfMem;
1152        result = cuddZddSiftingBackward(table, moveUp, initial_size);
1153        /* move backward and stop at best position */
1154        if (!result)
1155            goto cuddZddSiftingAuxOutOfMem;
1156    }
1157    else if ((x - x_low) > (x_high - x)) {
1158        /* must go down first:shorter */
1159        moveDown = cuddZddSiftingDown(table, x, x_high, initial_size);
1160        /* after that point x --> x_high */
1161        if (moveDown == NULL)
1162            goto cuddZddSiftingAuxOutOfMem;
1163        moveUp = cuddZddSiftingUp(table, moveDown->y, x_low,
1164            initial_size);
1165        if (moveUp == NULL)
1166            goto cuddZddSiftingAuxOutOfMem;
1167        result = cuddZddSiftingBackward(table, moveUp, initial_size);
1168        /* move backward and stop at best position */
1169        if (!result)
1170            goto cuddZddSiftingAuxOutOfMem;
1171    }
1172    else {
1173        moveUp = cuddZddSiftingUp(table, x, x_low, initial_size);
1174        /* after that point x --> x_high */
1175        if (moveUp == NULL)
1176            goto cuddZddSiftingAuxOutOfMem;
1177        moveDown = cuddZddSiftingDown(table, moveUp->x, x_high,
1178            initial_size);
1179        /* then move up */
1180        if (moveDown == NULL)
1181            goto cuddZddSiftingAuxOutOfMem;
1182        result = cuddZddSiftingBackward(table, moveDown,
1183            initial_size);
1184        /* move backward and stop at best position */
1185        if (!result)
1186            goto cuddZddSiftingAuxOutOfMem;
1187    }
1188
1189    while (moveDown != NULL) {
1190        move = moveDown->next;
1191        cuddDeallocMove(table, moveDown);
1192        moveDown = move;
1193    }
1194    while (moveUp != NULL) {
1195        move = moveUp->next;
1196        cuddDeallocMove(table, moveUp);
1197        moveUp = move;
1198    }
1199
1200    return(1);
1201
1202cuddZddSiftingAuxOutOfMem:
1203    while (moveDown != NULL) {
1204        move = moveDown->next;
1205        cuddDeallocMove(table, moveDown);
1206        moveDown = move;
1207    }
1208    while (moveUp != NULL) {
1209        move = moveUp->next;
1210        cuddDeallocMove(table, moveUp);
1211        moveUp = move;
1212    }
1213
1214    return(0);
1215
1216} /* end of cuddZddSiftingAux */
1217
1218
1219/**Function********************************************************************
1220
1221  Synopsis    [Sifts a variable up.]
1222
1223  Description [Sifts a variable up. Moves y up until either it reaches
1224  the bound (x_low) or the size of the ZDD heap increases too much.
1225  Returns the set of moves in case of success; NULL if memory is full.]
1226
1227  SideEffects [None]
1228
1229  SeeAlso     []
1230
1231******************************************************************************/
1232static Move *
1233cuddZddSiftingUp(
1234  DdManager * table,
1235  int  x,
1236  int  x_low,
1237  int  initial_size)
1238{
1239    Move        *moves;
1240    Move        *move;
1241    int         y;
1242    int         size;
1243    int         limit_size = initial_size;
1244
1245    moves = NULL;
1246    y = cuddZddNextLow(table, x);
1247    while (y >= x_low) {
1248        size = cuddZddSwapInPlace(table, y, x);
1249        if (size == 0)
1250            goto cuddZddSiftingUpOutOfMem;
1251        move = (Move *)cuddDynamicAllocNode(table);
1252        if (move == NULL)
1253            goto cuddZddSiftingUpOutOfMem;
1254        move->x = y;
1255        move->y = x;
1256        move->size = size;
1257        move->next = moves;
1258        moves = move;
1259
1260        if ((double)size > (double)limit_size * table->maxGrowth)
1261            break;
1262        if (size < limit_size)
1263            limit_size = size;
1264
1265        x = y;
1266        y = cuddZddNextLow(table, x);
1267    }
1268    return(moves);
1269
1270cuddZddSiftingUpOutOfMem:
1271    while (moves != NULL) {
1272        move = moves->next;
1273        cuddDeallocMove(table, moves);
1274        moves = move;
1275    }
1276    return(NULL);
1277
1278} /* end of cuddZddSiftingUp */
1279
1280
1281/**Function********************************************************************
1282
1283  Synopsis    [Sifts a variable down.]
1284
1285  Description [Sifts a variable down. Moves x down until either it
1286  reaches the bound (x_high) or the size of the ZDD heap increases too
1287  much. Returns the set of moves in case of success; NULL if memory is
1288  full.]
1289
1290  SideEffects [None]
1291
1292  SeeAlso     []
1293
1294******************************************************************************/
1295static Move *
1296cuddZddSiftingDown(
1297  DdManager * table,
1298  int  x,
1299  int  x_high,
1300  int  initial_size)
1301{
1302    Move        *moves;
1303    Move        *move;
1304    int         y;
1305    int         size;
1306    int         limit_size = initial_size;
1307
1308    moves = NULL;
1309    y = cuddZddNextHigh(table, x);
1310    while (y <= x_high) {
1311        size = cuddZddSwapInPlace(table, x, y);
1312        if (size == 0)
1313            goto cuddZddSiftingDownOutOfMem;
1314        move = (Move *)cuddDynamicAllocNode(table);
1315        if (move == NULL)
1316            goto cuddZddSiftingDownOutOfMem;
1317        move->x = x;
1318        move->y = y;
1319        move->size = size;
1320        move->next = moves;
1321        moves = move;
1322
1323        if ((double)size > (double)limit_size * table->maxGrowth)
1324            break;
1325        if (size < limit_size)
1326            limit_size = size;
1327
1328        x = y;
1329        y = cuddZddNextHigh(table, x);
1330    }
1331    return(moves);
1332
1333cuddZddSiftingDownOutOfMem:
1334    while (moves != NULL) {
1335        move = moves->next;
1336        cuddDeallocMove(table, moves);
1337        moves = move;
1338    }
1339    return(NULL);
1340
1341} /* end of cuddZddSiftingDown */
1342
1343
1344/**Function********************************************************************
1345
1346  Synopsis    [Given a set of moves, returns the ZDD heap to the position
1347  giving the minimum size.]
1348
1349  Description [Given a set of moves, returns the ZDD heap to the
1350  position giving the minimum size. In case of ties, returns to the
1351  closest position giving the minimum size. Returns 1 in case of
1352  success; 0 otherwise.]
1353
1354  SideEffects [None]
1355
1356  SeeAlso     []
1357
1358******************************************************************************/
1359static int
1360cuddZddSiftingBackward(
1361  DdManager * table,
1362  Move * moves,
1363  int  size)
1364{
1365    int         i;
1366    int         i_best;
1367    Move        *move;
1368    int         res;
1369
1370    /* Find the minimum size among moves. */
1371    i_best = -1;
1372    for (move = moves, i = 0; move != NULL; move = move->next, i++) {
1373        if (move->size < size) {
1374            i_best = i;
1375            size = move->size;
1376        }
1377    }
1378
1379    for (move = moves, i = 0; move != NULL; move = move->next, i++) {
1380        if (i == i_best)
1381            break;
1382        res = cuddZddSwapInPlace(table, move->x, move->y);
1383        if (!res)
1384            return(0);
1385        if (i_best == -1 && res == size)
1386            break;
1387    }
1388
1389    return(1);
1390
1391} /* end of cuddZddSiftingBackward */
1392
1393
1394/**Function********************************************************************
1395
1396  Synopsis    [Prepares the ZDD heap for dynamic reordering.]
1397
1398  Description [Prepares the ZDD heap for dynamic reordering. Does
1399  garbage collection, to guarantee that there are no dead nodes;
1400  and clears the cache, which is invalidated by dynamic reordering.]
1401
1402  SideEffects [None]
1403
1404******************************************************************************/
1405static void
1406zddReorderPreprocess(
1407  DdManager * table)
1408{
1409
1410    /* Clear the cache. */
1411    cuddCacheFlush(table);
1412
1413    /* Eliminate dead nodes. Do not scan the cache again. */
1414    cuddGarbageCollect(table,0);
1415
1416    return;
1417
1418} /* end of ddReorderPreprocess */
1419
1420
1421/**Function********************************************************************
1422
1423  Synopsis    [Shrinks almost empty ZDD subtables at the end of reordering
1424  to guarantee that they have a reasonable load factor.]
1425
1426  Description [Shrinks almost empty subtables at the end of reordering to
1427  guarantee that they have a reasonable load factor. However, if there many
1428  nodes are being reclaimed, then no resizing occurs. Returns 1 in case of
1429  success; 0 otherwise.]
1430
1431  SideEffects [None]
1432
1433******************************************************************************/
1434static int
1435zddReorderPostprocess(
1436  DdManager * table)
1437{
1438    int i, j, posn;
1439    DdNodePtr *nodelist, *oldnodelist;
1440    DdNode *node, *next;
1441    unsigned int slots, oldslots;
1442    extern DD_OOMFP MMoutOfMemory;
1443    DD_OOMFP saveHandler;
1444
1445#ifdef DD_VERBOSE
1446    (void) fflush(table->out);
1447#endif
1448
1449    /* If we have very many reclaimed nodes, we do not want to shrink
1450    ** the subtables, because this will lead to more garbage
1451    ** collections. More garbage collections mean shorter mean life for
1452    ** nodes with zero reference count; hence lower probability of finding
1453    ** a result in the cache.
1454    */
1455    if (table->reclaimed > table->allocated * 0.5) return(1);
1456
1457    /* Resize subtables. */
1458    for (i = 0; i < table->sizeZ; i++) {
1459        int shift;
1460        oldslots = table->subtableZ[i].slots;
1461        if (oldslots < table->subtableZ[i].keys * DD_MAX_SUBTABLE_SPARSITY ||
1462            oldslots <= table->initSlots) continue;
1463        oldnodelist = table->subtableZ[i].nodelist;
1464        slots = oldslots >> 1;
1465        saveHandler = MMoutOfMemory;
1466        MMoutOfMemory = Cudd_OutOfMem;
1467        nodelist = ALLOC(DdNodePtr, slots);
1468        MMoutOfMemory = saveHandler;
1469        if (nodelist == NULL) {
1470            return(1);
1471        }
1472        table->subtableZ[i].nodelist = nodelist;
1473        table->subtableZ[i].slots = slots;
1474        table->subtableZ[i].shift++;
1475        table->subtableZ[i].maxKeys = slots * DD_MAX_SUBTABLE_DENSITY;
1476#ifdef DD_VERBOSE
1477        (void) fprintf(table->err,
1478                       "shrunk layer %d (%d keys) from %d to %d slots\n",
1479                       i, table->subtableZ[i].keys, oldslots, slots);
1480#endif
1481
1482        for (j = 0; (unsigned) j < slots; j++) {
1483            nodelist[j] = NULL;
1484        }
1485        shift = table->subtableZ[i].shift;
1486        for (j = 0; (unsigned) j < oldslots; j++) {
1487            node = oldnodelist[j];
1488            while (node != NULL) {
1489                next = node->next;
1490                posn = ddHash(cuddT(node), cuddE(node), shift);
1491                node->next = nodelist[posn];
1492                nodelist[posn] = node;
1493                node = next;
1494            }
1495        }
1496        FREE(oldnodelist);
1497
1498        table->memused += (slots - oldslots) * sizeof(DdNode *);
1499        table->slots += slots - oldslots;
1500        table->minDead = (unsigned) (table->gcFrac * (double) table->slots);
1501        table->cacheSlack = (int) ddMin(table->maxCacheHard,
1502            DD_MAX_CACHE_TO_SLOTS_RATIO*table->slots) -
1503            2 * (int) table->cacheSlots;
1504    }
1505    /* We don't look at the constant subtable, because it is not
1506    ** affected by reordering.
1507    */
1508
1509    return(1);
1510
1511} /* end of zddReorderPostprocess */
1512
1513
1514/**Function********************************************************************
1515
1516  Synopsis    [Reorders ZDD variables according to a given permutation.]
1517
1518  Description [Reorders ZDD variables according to a given permutation.
1519  The i-th permutation array contains the index of the variable that
1520  should be brought to the i-th level. zddShuffle assumes that no
1521  dead nodes are present.  The reordering is achieved by a series of
1522  upward sifts.  Returns 1 if successful; 0 otherwise.]
1523
1524  SideEffects [None]
1525
1526  SeeAlso []
1527
1528******************************************************************************/
1529static int
1530zddShuffle(
1531  DdManager * table,
1532  int * permutation)
1533{
1534    int         index;
1535    int         level;
1536    int         position;
1537    int         numvars;
1538    int         result;
1539#ifdef DD_STATS
1540    long        localTime;
1541    int         initialSize;
1542    int         finalSize;
1543    int         previousSize;
1544#endif
1545
1546    zddTotalNumberSwapping = 0;
1547#ifdef DD_STATS
1548    localTime = util_cpu_time();
1549    initialSize = table->keysZ;
1550    (void) fprintf(table->out,"#:I_SHUFFLE %8d: initial size\n",
1551                   initialSize); 
1552#endif
1553
1554    numvars = table->sizeZ;
1555
1556    for (level = 0; level < numvars; level++) {
1557        index = permutation[level];
1558        position = table->permZ[index];
1559#ifdef DD_STATS
1560        previousSize = table->keysZ;
1561#endif
1562        result = zddSiftUp(table,position,level);
1563        if (!result) return(0);
1564#ifdef DD_STATS
1565        if (table->keysZ < (unsigned) previousSize) {
1566            (void) fprintf(table->out,"-");
1567        } else if (table->keysZ > (unsigned) previousSize) {
1568            (void) fprintf(table->out,"+");     /* should never happen */
1569        } else {
1570            (void) fprintf(table->out,"=");
1571        }
1572        fflush(table->out);
1573#endif
1574    }
1575
1576#ifdef DD_STATS
1577    (void) fprintf(table->out,"\n");
1578    finalSize = table->keysZ;
1579    (void) fprintf(table->out,"#:F_SHUFFLE %8d: final size\n",finalSize); 
1580    (void) fprintf(table->out,"#:T_SHUFFLE %8g: total time (sec)\n",
1581        ((double)(util_cpu_time() - localTime)/1000.0)); 
1582    (void) fprintf(table->out,"#:N_SHUFFLE %8d: total swaps\n",
1583                   zddTotalNumberSwapping);
1584#endif
1585
1586    return(1);
1587
1588} /* end of zddShuffle */
1589
1590
1591/**Function********************************************************************
1592
1593  Synopsis    [Moves one ZDD variable up.]
1594
1595  Description [Takes a ZDD variable from position x and sifts it up to
1596  position xLow;  xLow should be less than or equal to x.
1597  Returns 1 if successful; 0 otherwise]
1598
1599  SideEffects [None]
1600
1601  SeeAlso     []
1602
1603******************************************************************************/
1604static int
1605zddSiftUp(
1606  DdManager * table,
1607  int  x,
1608  int  xLow)
1609{
1610    int        y;
1611    int        size;
1612
1613    y = cuddZddNextLow(table,x);
1614    while (y >= xLow) {
1615        size = cuddZddSwapInPlace(table,y,x);
1616        if (size == 0) {
1617            return(0);
1618        }
1619        x = y;
1620        y = cuddZddNextLow(table,x);
1621    }
1622    return(1);
1623
1624} /* end of zddSiftUp */
1625
1626
1627/**Function********************************************************************
1628
1629  Synopsis    [Fixes the ZDD variable group tree after a shuffle.]
1630
1631  Description [Fixes the ZDD variable group tree after a
1632  shuffle. Assumes that the order of the variables in a terminal node
1633  has not been changed.]
1634
1635  SideEffects [Changes the ZDD variable group tree.]
1636
1637  SeeAlso     []
1638
1639******************************************************************************/
1640static void
1641zddFixTree(
1642  DdManager * table,
1643  MtrNode * treenode)
1644{
1645    if (treenode == NULL) return;
1646    treenode->low = ((int) treenode->index < table->sizeZ) ?
1647        table->permZ[treenode->index] : treenode->index;
1648    if (treenode->child != NULL) {
1649        zddFixTree(table, treenode->child);
1650    }
1651    if (treenode->younger != NULL)
1652        zddFixTree(table, treenode->younger);
1653    if (treenode->parent != NULL && treenode->low < treenode->parent->low) {
1654        treenode->parent->low = treenode->low;
1655        treenode->parent->index = treenode->index;
1656    }
1657    return;
1658
1659} /* end of zddFixTree */
1660
Note: See TracBrowser for help on using the repository browser.