source: vis_dev/glu-2.1/src/cuBdd/cuddExact.c @ 8

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

src glu
File size: 28.5 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [cuddExact.c]
4
5  PackageName [cudd]
6
7  Synopsis    [Functions for exact variable reordering.]
8
9  Description [External procedures included in this file:
10                <ul>
11                </ul>
12        Internal procedures included in this module:
13                <ul>
14                <li> cuddExact()
15                </ul>
16        Static procedures included in this module:
17                <ul>
18                <li> getMaxBinomial()
19                <li> gcd()
20                <li> getMatrix()
21                <li> freeMatrix()
22                <li> getLevelKeys()
23                <li> ddShuffle()
24                <li> ddSiftUp()
25                <li> updateUB()
26                <li> ddCountRoots()
27                <li> ddClearGlobal()
28                <li> computeLB()
29                <li> updateEntry()
30                <li> pushDown()
31                <li> initSymmInfo()
32                </ul>]
33
34  Author      [Cheng Hua, 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/*---------------------------------------------------------------------------*/
79/* Stucture declarations                                                     */
80/*---------------------------------------------------------------------------*/
81
82/*---------------------------------------------------------------------------*/
83/* Type declarations                                                         */
84/*---------------------------------------------------------------------------*/
85
86/*---------------------------------------------------------------------------*/
87/* Variable declarations                                                     */
88/*---------------------------------------------------------------------------*/
89
90#ifndef lint
91static char rcsid[] DD_UNUSED = "$Id: cuddExact.c,v 1.26 2004/08/13 18:04:48 fabio Exp $";
92#endif
93
94#ifdef DD_STATS
95static int ddTotalShuffles;
96#endif
97
98/*---------------------------------------------------------------------------*/
99/* Macro declarations                                                        */
100/*---------------------------------------------------------------------------*/
101
102/**AutomaticStart*************************************************************/
103
104/*---------------------------------------------------------------------------*/
105/* Static function prototypes                                                */
106/*---------------------------------------------------------------------------*/
107
108static int getMaxBinomial (int n);
109static DdHalfWord ** getMatrix (int rows, int cols);
110static void freeMatrix (DdHalfWord **matrix);
111static int getLevelKeys (DdManager *table, int l);
112static int ddShuffle (DdManager *table, DdHalfWord *permutation, int lower, int upper);
113static int ddSiftUp (DdManager *table, int x, int xLow);
114static int updateUB (DdManager *table, int oldBound, DdHalfWord *bestOrder, int lower, int upper);
115static int ddCountRoots (DdManager *table, int lower, int upper);
116static void ddClearGlobal (DdManager *table, int lower, int maxlevel);
117static int computeLB (DdManager *table, DdHalfWord *order, int roots, int cost, int lower, int upper, int level);
118static int updateEntry (DdManager *table, DdHalfWord *order, int level, int cost, DdHalfWord **orders, int *costs, int subsets, char *mask, int lower, int upper);
119static void pushDown (DdHalfWord *order, int j, int level);
120static DdHalfWord * initSymmInfo (DdManager *table, int lower, int upper);
121static int checkSymmInfo (DdManager *table, DdHalfWord *symmInfo, int index, int level);
122
123/**AutomaticEnd***************************************************************/
124
125
126/*---------------------------------------------------------------------------*/
127/* Definition of exported functions                                          */
128/*---------------------------------------------------------------------------*/
129
130/*---------------------------------------------------------------------------*/
131/* Definition of internal functions                                          */
132/*---------------------------------------------------------------------------*/
133
134
135/**Function********************************************************************
136
137  Synopsis    [Exact variable ordering algorithm.]
138
139  Description [Exact variable ordering algorithm. Finds an optimum
140  order for the variables between lower and upper.  Returns 1 if
141  successful; 0 otherwise.]
142
143  SideEffects [None]
144
145  SeeAlso     []
146
147******************************************************************************/
148int
149cuddExact(
150  DdManager * table,
151  int  lower,
152  int  upper)
153{
154    int k, i, j;
155    int maxBinomial, oldSubsets, newSubsets;
156    int subsetCost;
157    int size;                   /* number of variables to be reordered */
158    int unused, nvars, level, result;
159    int upperBound, lowerBound, cost;
160    int roots;
161    char *mask = NULL;
162    DdHalfWord  *symmInfo = NULL;
163    DdHalfWord **newOrder = NULL;
164    DdHalfWord **oldOrder = NULL;
165    int *newCost = NULL;
166    int *oldCost = NULL;
167    DdHalfWord **tmpOrder;
168    int *tmpCost;
169    DdHalfWord *bestOrder = NULL;
170    DdHalfWord *order;
171#ifdef DD_STATS
172    int  ddTotalSubsets;
173#endif
174
175    /* Restrict the range to be reordered by excluding unused variables
176    ** at the two ends. */
177    while (table->subtables[lower].keys == 1 &&
178           table->vars[table->invperm[lower]]->ref == 1 &&
179           lower < upper)
180        lower++;
181    while (table->subtables[upper].keys == 1 &&
182           table->vars[table->invperm[upper]]->ref == 1 &&
183           lower < upper)
184        upper--;
185    if (lower == upper) return(1); /* trivial problem */
186
187    /* Apply symmetric sifting to get a good upper bound and to extract
188    ** symmetry information. */
189    result = cuddSymmSiftingConv(table,lower,upper);
190    if (result == 0) goto cuddExactOutOfMem;
191
192#ifdef DD_STATS
193    (void) fprintf(table->out,"\n");
194    ddTotalShuffles = 0;
195    ddTotalSubsets = 0;
196#endif
197
198    /* Initialization. */
199    nvars = table->size;
200    size = upper - lower + 1;
201    /* Count unused variable among those to be reordered.  This is only
202    ** used to compute maxBinomial. */
203    unused = 0;
204    for (i = lower + 1; i < upper; i++) {
205        if (table->subtables[i].keys == 1 &&
206            table->vars[table->invperm[i]]->ref == 1)
207            unused++;
208    }
209
210    /* Find the maximum number of subsets we may have to store. */
211    maxBinomial = getMaxBinomial(size - unused);
212    if (maxBinomial == -1) goto cuddExactOutOfMem;
213
214    newOrder = getMatrix(maxBinomial, size);
215    if (newOrder == NULL) goto cuddExactOutOfMem;
216
217    newCost = ALLOC(int, maxBinomial);
218    if (newCost == NULL) goto cuddExactOutOfMem;
219
220    oldOrder = getMatrix(maxBinomial, size);
221    if (oldOrder == NULL) goto cuddExactOutOfMem;
222
223    oldCost = ALLOC(int, maxBinomial);
224    if (oldCost == NULL) goto cuddExactOutOfMem;
225
226    bestOrder = ALLOC(DdHalfWord, size);
227    if (bestOrder == NULL) goto cuddExactOutOfMem;
228
229    mask = ALLOC(char, nvars);
230    if (mask == NULL) goto cuddExactOutOfMem;
231
232    symmInfo = initSymmInfo(table, lower, upper);
233    if (symmInfo == NULL) goto cuddExactOutOfMem;
234
235    roots = ddCountRoots(table, lower, upper);
236
237    /* Initialize the old order matrix for the empty subset and the best
238    ** order to the current order. The cost for the empty subset includes
239    ** the cost of the levels between upper and the constants. These levels
240    ** are not going to change. Hence, we count them only once.
241    */
242    oldSubsets = 1;
243    for (i = 0; i < size; i++) {
244        oldOrder[0][i] = bestOrder[i] = (DdHalfWord) table->invperm[i+lower];
245    }
246    subsetCost = table->constants.keys;
247    for (i = upper + 1; i < nvars; i++)
248        subsetCost += getLevelKeys(table,i);
249    oldCost[0] = subsetCost;
250    /* The upper bound is initialized to the current size of the BDDs. */
251    upperBound = table->keys - table->isolated;
252
253    /* Now consider subsets of increasing size. */
254    for (k = 1; k <= size; k++) {
255#if DD_STATS
256        (void) fprintf(table->out,"Processing subsets of size %d\n", k);
257        fflush(table->out);
258#endif
259        newSubsets = 0;
260        level = size - k;               /* offset of first bottom variable */
261
262        for (i = 0; i < oldSubsets; i++) { /* for each subset of size k-1 */
263            order = oldOrder[i];
264            cost = oldCost[i];
265            lowerBound = computeLB(table, order, roots, cost, lower, upper,
266                                   level);
267            if (lowerBound >= upperBound)
268                continue;
269            /* Impose new order. */
270            result = ddShuffle(table, order, lower, upper);
271            if (result == 0) goto cuddExactOutOfMem;
272            upperBound = updateUB(table,upperBound,bestOrder,lower,upper);
273            /* For each top bottom variable. */
274            for (j = level; j >= 0; j--) {
275                /* Skip unused variables. */
276                if (table->subtables[j+lower-1].keys == 1 &&
277                    table->vars[table->invperm[j+lower-1]]->ref == 1) continue;
278                /* Find cost under this order. */
279                subsetCost = cost + getLevelKeys(table, lower + level);
280                newSubsets = updateEntry(table, order, level, subsetCost,
281                                         newOrder, newCost, newSubsets, mask,
282                                         lower, upper);
283                if (j == 0)
284                    break;
285                if (checkSymmInfo(table, symmInfo, order[j-1], level) == 0)
286                    continue;
287                pushDown(order,j-1,level);
288                /* Impose new order. */
289                result = ddShuffle(table, order, lower, upper);
290                if (result == 0) goto cuddExactOutOfMem;
291                upperBound = updateUB(table,upperBound,bestOrder,lower,upper);
292            } /* for each bottom variable */
293        } /* for each subset of size k */
294
295        /* New orders become old orders in preparation for next iteration. */
296        tmpOrder = oldOrder; tmpCost = oldCost;
297        oldOrder = newOrder; oldCost = newCost;
298        newOrder = tmpOrder; newCost = tmpCost;
299#ifdef DD_STATS
300        ddTotalSubsets += newSubsets;
301#endif
302        oldSubsets = newSubsets;
303    }
304    result = ddShuffle(table, bestOrder, lower, upper);
305    if (result == 0) goto cuddExactOutOfMem;
306#ifdef DD_STATS
307#ifdef DD_VERBOSE
308    (void) fprintf(table->out,"\n");
309#endif
310    (void) fprintf(table->out,"#:S_EXACT   %8d: total subsets\n",
311                   ddTotalSubsets);
312    (void) fprintf(table->out,"#:H_EXACT   %8d: total shuffles",
313                   ddTotalShuffles);
314#endif
315
316    freeMatrix(newOrder);
317    freeMatrix(oldOrder);
318    FREE(bestOrder);
319    FREE(oldCost);
320    FREE(newCost);
321    FREE(symmInfo);
322    FREE(mask);
323    return(1);
324
325cuddExactOutOfMem:
326
327    if (newOrder != NULL) freeMatrix(newOrder);
328    if (oldOrder != NULL) freeMatrix(oldOrder);
329    if (bestOrder != NULL) FREE(bestOrder);
330    if (oldCost != NULL) FREE(oldCost);
331    if (newCost != NULL) FREE(newCost);
332    if (symmInfo != NULL) FREE(symmInfo);
333    if (mask != NULL) FREE(mask);
334    table->errorCode = CUDD_MEMORY_OUT;
335    return(0);
336
337} /* end of cuddExact */
338
339
340/**Function********************************************************************
341
342  Synopsis    [Returns the maximum value of (n choose k) for a given n.]
343
344  Description [Computes the maximum value of (n choose k) for a given
345  n.  The maximum value occurs for k = n/2 when n is even, or k =
346  (n-1)/2 when n is odd.  The algorithm used in this procedure avoids
347  intermediate overflow problems.  It is based on the identity
348  <pre>
349    binomial(n,k) = n/k * binomial(n-1,k-1).
350  </pre>
351  Returns the computed value if successful; -1 if out of range.]
352
353  SideEffects [None]
354
355  SeeAlso     []
356
357******************************************************************************/
358static int
359getMaxBinomial(
360  int n)
361{
362    double i, j, result;
363
364    if (n < 0 || n > 33) return(-1); /* error */
365    if (n < 2) return(1);
366
367    for (result = (double)((n+3)/2), i = result+1, j=2; i <= n; i++, j++) {
368        result *= i;
369        result /= j;
370    }
371
372    return((int)result);
373
374} /* end of getMaxBinomial */
375
376
377#if 0
378/**Function********************************************************************
379
380  Synopsis    [Returns the gcd of two integers.]
381
382  Description [Returns the gcd of two integers. Uses the binary GCD
383  algorithm described in Cormen, Leiserson, and Rivest.]
384
385  SideEffects [None]
386
387  SeeAlso     []
388
389******************************************************************************/
390static int
391gcd(
392  int  x,
393  int  y)
394{
395    int a;
396    int b;
397    int lsbMask;
398
399    /* GCD(n,0) = n. */
400    if (x == 0) return(y);
401    if (y == 0) return(x);
402
403    a = x; b = y; lsbMask = 1;
404   
405    /* Here both a and b are != 0. The iteration maintains this invariant.
406    ** Hence, we only need to check for when they become equal.
407    */
408    while (a != b) {
409        if (a & lsbMask) {
410            if (b & lsbMask) {  /* both odd */
411                if (a < b) {
412                    b = (b - a) >> 1;
413                } else {
414                    a = (a - b) >> 1;
415                }
416            } else {            /* a odd, b even */
417                b >>= 1;
418            }
419        } else {
420            if (b & lsbMask) {  /* a even, b odd */
421                a >>= 1;
422            } else {            /* both even */
423                lsbMask <<= 1;
424            }
425        }
426    }
427
428    return(a);
429
430} /* end of gcd */
431#endif
432
433
434/**Function********************************************************************
435
436  Synopsis    [Allocates a two-dimensional matrix of ints.]
437
438  Description [Allocates a two-dimensional matrix of ints.
439  Returns the pointer to the matrix if successful; NULL otherwise.]
440
441  SideEffects [None]
442
443  SeeAlso     [freeMatrix]
444
445******************************************************************************/
446static DdHalfWord **
447getMatrix(
448  int  rows /* number of rows */,
449  int  cols /* number of columns */)
450{
451    DdHalfWord **matrix;
452    int i;
453
454    if (cols*rows == 0) return(NULL);
455    matrix = ALLOC(DdHalfWord *, rows);
456    if (matrix == NULL) return(NULL);
457    matrix[0] = ALLOC(DdHalfWord, cols*rows);
458    if (matrix[0] == NULL) return(NULL);
459    for (i = 1; i < rows; i++) {
460        matrix[i] = matrix[i-1] + cols;
461    }
462    return(matrix);
463
464} /* end of getMatrix */
465
466
467/**Function********************************************************************
468
469  Synopsis    [Frees a two-dimensional matrix allocated by getMatrix.]
470
471  Description []
472
473  SideEffects [None]
474
475  SeeAlso     [getMatrix]
476
477******************************************************************************/
478static void
479freeMatrix(
480  DdHalfWord ** matrix)
481{
482    FREE(matrix[0]);
483    FREE(matrix);
484    return;
485
486} /* end of freeMatrix */
487
488
489/**Function********************************************************************
490
491  Synopsis    [Returns the number of nodes at one level of a unique table.]
492
493  Description [Returns the number of nodes at one level of a unique table.
494  The projection function, if isolated, is not counted.]
495
496  SideEffects [None]
497
498  SeeAlso []
499
500******************************************************************************/
501static int
502getLevelKeys(
503  DdManager * table,
504  int  l)
505{
506    int isolated;
507    int x;        /* x is an index */
508
509    x = table->invperm[l];
510    isolated = table->vars[x]->ref == 1;
511
512    return(table->subtables[l].keys - isolated);
513
514} /* end of getLevelKeys */
515
516
517/**Function********************************************************************
518
519  Synopsis    [Reorders variables according to a given permutation.]
520
521  Description [Reorders variables according to a given permutation.
522  The i-th permutation array contains the index of the variable that
523  should be brought to the i-th level. ddShuffle assumes that no
524  dead nodes are present and that the interaction matrix is properly
525  initialized.  The reordering is achieved by a series of upward sifts.
526  Returns 1 if successful; 0 otherwise.]
527
528  SideEffects [None]
529
530  SeeAlso []
531
532******************************************************************************/
533static int
534ddShuffle(
535  DdManager * table,
536  DdHalfWord * permutation,
537  int  lower,
538  int  upper)
539{
540    DdHalfWord  index;
541    int         level;
542    int         position;
543#if 0
544    int         numvars;
545#endif
546    int         result;
547#ifdef DD_STATS
548    long        localTime;
549    int         initialSize;
550#ifdef DD_VERBOSE
551    int         finalSize;
552#endif
553    int         previousSize;
554#endif
555
556#ifdef DD_STATS
557    localTime = util_cpu_time();
558    initialSize = table->keys - table->isolated;
559#endif
560
561#if 0
562    numvars = table->size;
563
564    (void) fprintf(table->out,"%d:", ddTotalShuffles);
565    for (level = 0; level < numvars; level++) {
566        (void) fprintf(table->out," %d", table->invperm[level]);
567    }
568    (void) fprintf(table->out,"\n");
569#endif
570
571    for (level = 0; level <= upper - lower; level++) {
572        index = permutation[level];
573        position = table->perm[index];
574#ifdef DD_STATS
575        previousSize = table->keys - table->isolated;
576#endif
577        result = ddSiftUp(table,position,level+lower);
578        if (!result) return(0);
579    }
580
581#ifdef DD_STATS
582    ddTotalShuffles++;
583#ifdef DD_VERBOSE
584    finalSize = table->keys - table->isolated;
585    if (finalSize < initialSize) {
586        (void) fprintf(table->out,"-");
587    } else if (finalSize > initialSize) {
588        (void) fprintf(table->out,"+");
589    } else {
590        (void) fprintf(table->out,"=");
591    }
592    if ((ddTotalShuffles & 63) == 0) (void) fprintf(table->out,"\n");
593    fflush(table->out);
594#endif
595#endif
596
597    return(1);
598
599} /* end of ddShuffle */
600
601
602/**Function********************************************************************
603
604  Synopsis    [Moves one variable up.]
605
606  Description [Takes a variable from position x and sifts it up to
607  position xLow;  xLow should be less than or equal to x.
608  Returns 1 if successful; 0 otherwise]
609
610  SideEffects [None]
611
612  SeeAlso     []
613
614******************************************************************************/
615static int
616ddSiftUp(
617  DdManager * table,
618  int  x,
619  int  xLow)
620{
621    int        y;
622    int        size;
623
624    y = cuddNextLow(table,x);
625    while (y >= xLow) {
626        size = cuddSwapInPlace(table,y,x);
627        if (size == 0) {
628            return(0);
629        }
630        x = y;
631        y = cuddNextLow(table,x);
632    }
633    return(1);
634
635} /* end of ddSiftUp */
636
637
638/**Function********************************************************************
639
640  Synopsis    [Updates the upper bound and saves the best order seen so far.]
641
642  Description [Updates the upper bound and saves the best order seen so far.
643  Returns the current value of the upper bound.]
644
645  SideEffects [None]
646
647  SeeAlso     []
648
649******************************************************************************/
650static int
651updateUB(
652  DdManager * table,
653  int  oldBound,
654  DdHalfWord * bestOrder,
655  int  lower,
656  int  upper)
657{
658    int i;
659    int newBound = table->keys - table->isolated;
660
661    if (newBound < oldBound) {
662#ifdef DD_STATS
663        (void) fprintf(table->out,"New upper bound = %d\n", newBound);
664        fflush(table->out);
665#endif
666        for (i = lower; i <= upper; i++)
667            bestOrder[i-lower] = (DdHalfWord) table->invperm[i];
668        return(newBound);
669    } else {
670        return(oldBound);
671    }
672
673} /* end of updateUB */
674
675
676/**Function********************************************************************
677
678  Synopsis    [Counts the number of roots.]
679
680  Description [Counts the number of roots at the levels between lower and
681  upper.  The computation is based on breadth-first search.
682  A node is a root if it is not reachable from any previously visited node.
683  (All the nodes at level lower are therefore considered roots.)
684  The visited flag uses the LSB of the next pointer.  Returns the root
685  count. The roots that are constant nodes are always ignored.]
686
687  SideEffects [None]
688
689  SeeAlso     [ddClearGlobal]
690
691******************************************************************************/
692static int
693ddCountRoots(
694  DdManager * table,
695  int  lower,
696  int  upper)
697{
698    int i,j;
699    DdNode *f;
700    DdNodePtr *nodelist;
701    DdNode *sentinel = &(table->sentinel);
702    int slots;
703    int roots = 0;
704    int maxlevel = lower;
705
706    for (i = lower; i <= upper; i++) {
707        nodelist = table->subtables[i].nodelist;
708        slots = table->subtables[i].slots;
709        for (j = 0; j < slots; j++) {
710            f = nodelist[j];
711            while (f != sentinel) {
712                /* A node is a root of the DAG if it cannot be
713                ** reached by nodes above it. If a node was never
714                ** reached during the previous depth-first searches,
715                ** then it is a root, and we start a new depth-first
716                ** search from it.
717                */
718                if (!Cudd_IsComplement(f->next)) {
719                    if (f != table->vars[f->index]) {
720                        roots++;
721                    }
722                }
723                if (!Cudd_IsConstant(cuddT(f))) {
724                    cuddT(f)->next = Cudd_Complement(cuddT(f)->next);
725                    if (table->perm[cuddT(f)->index] > maxlevel)
726                        maxlevel = table->perm[cuddT(f)->index];
727                }
728                if (!Cudd_IsConstant(cuddE(f))) {
729                    Cudd_Regular(cuddE(f))->next =
730                        Cudd_Complement(Cudd_Regular(cuddE(f))->next);
731                    if (table->perm[Cudd_Regular(cuddE(f))->index] > maxlevel)
732                        maxlevel = table->perm[Cudd_Regular(cuddE(f))->index];
733                }
734                f = Cudd_Regular(f->next);
735            }
736        }
737    }
738    ddClearGlobal(table, lower, maxlevel);
739
740    return(roots);
741
742} /* end of ddCountRoots */
743
744
745/**Function********************************************************************
746
747  Synopsis    [Scans the DD and clears the LSB of the next pointers.]
748
749  Description [Scans the DD and clears the LSB of the next pointers.
750  The LSB of the next pointers are used as markers to tell whether a
751  node was reached. Once the roots are counted, these flags are
752  reset.]
753
754  SideEffects [None]
755
756  SeeAlso     [ddCountRoots]
757
758******************************************************************************/
759static void
760ddClearGlobal(
761  DdManager * table,
762  int  lower,
763  int  maxlevel)
764{
765    int i,j;
766    DdNode *f;
767    DdNodePtr *nodelist;
768    DdNode *sentinel = &(table->sentinel);
769    int slots;
770
771    for (i = lower; i <= maxlevel; i++) {
772        nodelist = table->subtables[i].nodelist;
773        slots = table->subtables[i].slots;
774        for (j = 0; j < slots; j++) {
775            f = nodelist[j];
776            while (f != sentinel) {
777                f->next = Cudd_Regular(f->next);
778                f = f->next;
779            }
780        }
781    }
782
783} /* end of ddClearGlobal */
784
785
786/**Function********************************************************************
787
788  Synopsis    [Computes a lower bound on the size of a BDD.]
789
790  Description [Computes a lower bound on the size of a BDD from the
791  following factors:
792  <ul>
793  <li> size of the lower part of it;
794  <li> size of the part of the upper part not subjected to reordering;
795  <li> number of roots in the part of the BDD subjected to reordering;
796  <li> variable in the support of the roots in the upper part of the
797       BDD subjected to reordering.
798  <ul/>]
799
800  SideEffects [None]
801
802  SeeAlso     []
803
804******************************************************************************/
805static int
806computeLB(
807  DdManager * table             /* manager */,
808  DdHalfWord * order            /* optimal order for the subset */,
809  int  roots                    /* roots between lower and upper */,
810  int  cost                     /* minimum cost for the subset */,
811  int  lower                    /* lower level to be reordered */,
812  int  upper                    /* upper level to be reordered */,
813  int  level                    /* offset for the current top bottom var */
814  )
815{
816    int i;
817    int lb = cost;
818    int lb1 = 0;
819    int lb2;
820    int support;
821    DdHalfWord ref;
822
823    /* The levels not involved in reordering are not going to change.
824    ** Add their sizes to the lower bound.
825    */
826    for (i = 0; i < lower; i++) {
827        lb += getLevelKeys(table,i);
828    }
829    /* If a variable is in the support, then there is going
830    ** to be at least one node labeled by that variable.
831    */
832    for (i = lower; i <= lower+level; i++) {
833        support = table->subtables[i].keys > 1 ||
834            table->vars[order[i-lower]]->ref > 1;
835        lb1 += support;
836    }
837
838    /* Estimate the number of nodes required to connect the roots to
839    ** the nodes in the bottom part. */
840    if (lower+level+1 < table->size) {
841        if (lower+level < upper)
842            ref = table->vars[order[level+1]]->ref;
843        else
844            ref = table->vars[table->invperm[upper+1]]->ref;
845        lb2 = table->subtables[lower+level+1].keys -
846            (ref > (DdHalfWord) 1) - roots;
847    } else {
848        lb2 = 0;
849    }
850
851    lb += lb1 > lb2 ? lb1 : lb2;
852
853    return(lb);
854
855} /* end of computeLB */
856
857
858/**Function********************************************************************
859
860  Synopsis    [Updates entry for a subset.]
861
862  Description [Updates entry for a subset. Finds the subset, if it exists.
863  If the new order for the subset has lower cost, or if the subset did not
864  exist, it stores the new order and cost. Returns the number of subsets
865  currently in the table.]
866
867  SideEffects [None]
868
869  SeeAlso     []
870
871******************************************************************************/
872static int
873updateEntry(
874  DdManager * table,
875  DdHalfWord * order,
876  int  level,
877  int  cost,
878  DdHalfWord ** orders,
879  int * costs,
880  int  subsets,
881  char * mask,
882  int  lower,
883  int  upper)
884{
885    int i, j;
886    int size = upper - lower + 1;
887
888    /* Build a mask that says what variables are in this subset. */
889    for (i = lower; i <= upper; i++)
890        mask[table->invperm[i]] = 0;
891    for (i = level; i < size; i++)
892        mask[order[i]] = 1;
893
894    /* Check each subset until a match is found or all subsets are examined. */
895    for (i = 0; i < subsets; i++) {
896        DdHalfWord *subset = orders[i];
897        for (j = level; j < size; j++) {
898            if (mask[subset[j]] == 0)
899                break;
900        }
901        if (j == size)          /* no mismatches: success */
902            break;
903    }
904    if (i == subsets || cost < costs[i]) {              /* add or replace */
905        for (j = 0; j < size; j++)
906            orders[i][j] = order[j];
907        costs[i] = cost;
908        subsets += (i == subsets);
909    }
910    return(subsets);
911
912} /* end of updateEntry */
913
914
915/**Function********************************************************************
916
917  Synopsis    [Pushes a variable in the order down to position "level."]
918
919  Description []
920
921  SideEffects [None]
922
923  SeeAlso     []
924
925******************************************************************************/
926static void
927pushDown(
928  DdHalfWord * order,
929  int  j,
930  int  level)
931{
932    int i;
933    DdHalfWord tmp;
934
935    tmp = order[j];
936    for (i = j; i < level; i++) {
937        order[i] = order[i+1];
938    }
939    order[level] = tmp;
940    return;
941
942} /* end of pushDown */
943
944
945/**Function********************************************************************
946
947  Synopsis    [Gathers symmetry information.]
948
949  Description [Translates the symmetry information stored in the next
950  field of each subtable from level to indices. This procedure is called
951  immediately after symmetric sifting, so that the next fields are correct.
952  By translating this informaton in terms of indices, we make it independent
953  of subsequent reorderings. The format used is that of the next fields:
954  a circular list where each variable points to the next variable in the
955  same symmetry group. Only the entries between lower and upper are
956  considered.  The procedure returns a pointer to an array
957  holding the symmetry information if successful; NULL otherwise.]
958
959  SideEffects [None]
960
961  SeeAlso     [checkSymmInfo]
962
963******************************************************************************/
964static DdHalfWord *
965initSymmInfo(
966  DdManager * table,
967  int  lower,
968  int  upper)
969{
970    int level, index, next, nextindex;
971    DdHalfWord *symmInfo;
972
973    symmInfo =  ALLOC(DdHalfWord, table->size);
974    if (symmInfo == NULL) return(NULL);
975
976    for (level = lower; level <= upper; level++) {
977        index = table->invperm[level];
978        next =  table->subtables[level].next;
979        nextindex = table->invperm[next];
980        symmInfo[index] = nextindex;
981    }
982    return(symmInfo);
983
984} /* end of initSymmInfo */
985
986
987/**Function********************************************************************
988
989  Synopsis    [Check symmetry condition.]
990
991  Description [Returns 1 if a variable is the one with the highest index
992  among those belonging to a symmetry group that are in the top part of
993  the BDD.  The top part is given by level.]
994
995  SideEffects [None]
996
997  SeeAlso     [initSymmInfo]
998
999******************************************************************************/
1000static int
1001checkSymmInfo(
1002  DdManager * table,
1003  DdHalfWord * symmInfo,
1004  int  index,
1005  int  level)
1006{
1007    int i;
1008
1009    i = symmInfo[index];
1010    while (i != index) {
1011        if (index < i && table->perm[i] <= level)
1012            return(0);
1013        i = symmInfo[i];
1014    }
1015    return(1);
1016
1017} /* end of checkSymmInfo */
1018
Note: See TracBrowser for help on using the repository browser.