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

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

library glu 2.3
File size: 28.4 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.28 2009/02/19 16:19:19 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#ifdef 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) {
459        FREE(matrix);
460        return(NULL);
461    }
462    for (i = 1; i < rows; i++) {
463        matrix[i] = matrix[i-1] + cols;
464    }
465    return(matrix);
466
467} /* end of getMatrix */
468
469
470/**Function********************************************************************
471
472  Synopsis    [Frees a two-dimensional matrix allocated by getMatrix.]
473
474  Description []
475
476  SideEffects [None]
477
478  SeeAlso     [getMatrix]
479
480******************************************************************************/
481static void
482freeMatrix(
483  DdHalfWord ** matrix)
484{
485    FREE(matrix[0]);
486    FREE(matrix);
487    return;
488
489} /* end of freeMatrix */
490
491
492/**Function********************************************************************
493
494  Synopsis    [Returns the number of nodes at one level of a unique table.]
495
496  Description [Returns the number of nodes at one level of a unique table.
497  The projection function, if isolated, is not counted.]
498
499  SideEffects [None]
500
501  SeeAlso []
502
503******************************************************************************/
504static int
505getLevelKeys(
506  DdManager * table,
507  int  l)
508{
509    int isolated;
510    int x;        /* x is an index */
511
512    x = table->invperm[l];
513    isolated = table->vars[x]->ref == 1;
514
515    return(table->subtables[l].keys - isolated);
516
517} /* end of getLevelKeys */
518
519
520/**Function********************************************************************
521
522  Synopsis    [Reorders variables according to a given permutation.]
523
524  Description [Reorders variables according to a given permutation.
525  The i-th permutation array contains the index of the variable that
526  should be brought to the i-th level. ddShuffle assumes that no
527  dead nodes are present and that the interaction matrix is properly
528  initialized.  The reordering is achieved by a series of upward sifts.
529  Returns 1 if successful; 0 otherwise.]
530
531  SideEffects [None]
532
533  SeeAlso []
534
535******************************************************************************/
536static int
537ddShuffle(
538  DdManager * table,
539  DdHalfWord * permutation,
540  int  lower,
541  int  upper)
542{
543    DdHalfWord  index;
544    int         level;
545    int         position;
546#if 0
547    int         numvars;
548#endif
549    int         result;
550#ifdef DD_STATS
551    long        localTime;
552    int         initialSize;
553#ifdef DD_VERBOSE
554    int         finalSize;
555#endif
556    int         previousSize;
557#endif
558
559#ifdef DD_STATS
560    localTime = util_cpu_time();
561    initialSize = table->keys - table->isolated;
562#endif
563
564#if 0
565    numvars = table->size;
566
567    (void) fprintf(table->out,"%d:", ddTotalShuffles);
568    for (level = 0; level < numvars; level++) {
569        (void) fprintf(table->out," %d", table->invperm[level]);
570    }
571    (void) fprintf(table->out,"\n");
572#endif
573
574    for (level = 0; level <= upper - lower; level++) {
575        index = permutation[level];
576        position = table->perm[index];
577#ifdef DD_STATS
578        previousSize = table->keys - table->isolated;
579#endif
580        result = ddSiftUp(table,position,level+lower);
581        if (!result) return(0);
582    }
583
584#ifdef DD_STATS
585    ddTotalShuffles++;
586#ifdef DD_VERBOSE
587    finalSize = table->keys - table->isolated;
588    if (finalSize < initialSize) {
589        (void) fprintf(table->out,"-");
590    } else if (finalSize > initialSize) {
591        (void) fprintf(table->out,"+");
592    } else {
593        (void) fprintf(table->out,"=");
594    }
595    if ((ddTotalShuffles & 63) == 0) (void) fprintf(table->out,"\n");
596    fflush(table->out);
597#endif
598#endif
599
600    return(1);
601
602} /* end of ddShuffle */
603
604
605/**Function********************************************************************
606
607  Synopsis    [Moves one variable up.]
608
609  Description [Takes a variable from position x and sifts it up to
610  position xLow;  xLow should be less than or equal to x.
611  Returns 1 if successful; 0 otherwise]
612
613  SideEffects [None]
614
615  SeeAlso     []
616
617******************************************************************************/
618static int
619ddSiftUp(
620  DdManager * table,
621  int  x,
622  int  xLow)
623{
624    int        y;
625    int        size;
626
627    y = cuddNextLow(table,x);
628    while (y >= xLow) {
629        size = cuddSwapInPlace(table,y,x);
630        if (size == 0) {
631            return(0);
632        }
633        x = y;
634        y = cuddNextLow(table,x);
635    }
636    return(1);
637
638} /* end of ddSiftUp */
639
640
641/**Function********************************************************************
642
643  Synopsis    [Updates the upper bound and saves the best order seen so far.]
644
645  Description [Updates the upper bound and saves the best order seen so far.
646  Returns the current value of the upper bound.]
647
648  SideEffects [None]
649
650  SeeAlso     []
651
652******************************************************************************/
653static int
654updateUB(
655  DdManager * table,
656  int  oldBound,
657  DdHalfWord * bestOrder,
658  int  lower,
659  int  upper)
660{
661    int i;
662    int newBound = table->keys - table->isolated;
663
664    if (newBound < oldBound) {
665#ifdef DD_STATS
666        (void) fprintf(table->out,"New upper bound = %d\n", newBound);
667        fflush(table->out);
668#endif
669        for (i = lower; i <= upper; i++)
670            bestOrder[i-lower] = (DdHalfWord) table->invperm[i];
671        return(newBound);
672    } else {
673        return(oldBound);
674    }
675
676} /* end of updateUB */
677
678
679/**Function********************************************************************
680
681  Synopsis    [Counts the number of roots.]
682
683  Description [Counts the number of roots at the levels between lower and
684  upper.  The computation is based on breadth-first search.
685  A node is a root if it is not reachable from any previously visited node.
686  (All the nodes at level lower are therefore considered roots.)
687  The visited flag uses the LSB of the next pointer.  Returns the root
688  count. The roots that are constant nodes are always ignored.]
689
690  SideEffects [None]
691
692  SeeAlso     [ddClearGlobal]
693
694******************************************************************************/
695static int
696ddCountRoots(
697  DdManager * table,
698  int  lower,
699  int  upper)
700{
701    int i,j;
702    DdNode *f;
703    DdNodePtr *nodelist;
704    DdNode *sentinel = &(table->sentinel);
705    int slots;
706    int roots = 0;
707    int maxlevel = lower;
708
709    for (i = lower; i <= upper; i++) {
710        nodelist = table->subtables[i].nodelist;
711        slots = table->subtables[i].slots;
712        for (j = 0; j < slots; j++) {
713            f = nodelist[j];
714            while (f != sentinel) {
715                /* A node is a root of the DAG if it cannot be
716                ** reached by nodes above it. If a node was never
717                ** reached during the previous depth-first searches,
718                ** then it is a root, and we start a new depth-first
719                ** search from it.
720                */
721                if (!Cudd_IsComplement(f->next)) {
722                    if (f != table->vars[f->index]) {
723                        roots++;
724                    }
725                }
726                if (!Cudd_IsConstant(cuddT(f))) {
727                    cuddT(f)->next = Cudd_Complement(cuddT(f)->next);
728                    if (table->perm[cuddT(f)->index] > maxlevel)
729                        maxlevel = table->perm[cuddT(f)->index];
730                }
731                if (!Cudd_IsConstant(cuddE(f))) {
732                    Cudd_Regular(cuddE(f))->next =
733                        Cudd_Complement(Cudd_Regular(cuddE(f))->next);
734                    if (table->perm[Cudd_Regular(cuddE(f))->index] > maxlevel)
735                        maxlevel = table->perm[Cudd_Regular(cuddE(f))->index];
736                }
737                f = Cudd_Regular(f->next);
738            }
739        }
740    }
741    ddClearGlobal(table, lower, maxlevel);
742
743    return(roots);
744
745} /* end of ddCountRoots */
746
747
748/**Function********************************************************************
749
750  Synopsis    [Scans the DD and clears the LSB of the next pointers.]
751
752  Description [Scans the DD and clears the LSB of the next pointers.
753  The LSB of the next pointers are used as markers to tell whether a
754  node was reached. Once the roots are counted, these flags are
755  reset.]
756
757  SideEffects [None]
758
759  SeeAlso     [ddCountRoots]
760
761******************************************************************************/
762static void
763ddClearGlobal(
764  DdManager * table,
765  int  lower,
766  int  maxlevel)
767{
768    int i,j;
769    DdNode *f;
770    DdNodePtr *nodelist;
771    DdNode *sentinel = &(table->sentinel);
772    int slots;
773
774    for (i = lower; i <= maxlevel; i++) {
775        nodelist = table->subtables[i].nodelist;
776        slots = table->subtables[i].slots;
777        for (j = 0; j < slots; j++) {
778            f = nodelist[j];
779            while (f != sentinel) {
780                f->next = Cudd_Regular(f->next);
781                f = f->next;
782            }
783        }
784    }
785
786} /* end of ddClearGlobal */
787
788
789/**Function********************************************************************
790
791  Synopsis    [Computes a lower bound on the size of a BDD.]
792
793  Description [Computes a lower bound on the size of a BDD from the
794  following factors:
795  <ul>
796  <li> size of the lower part of it;
797  <li> size of the part of the upper part not subjected to reordering;
798  <li> number of roots in the part of the BDD subjected to reordering;
799  <li> variable in the support of the roots in the upper part of the
800       BDD subjected to reordering.
801  <ul/>]
802
803  SideEffects [None]
804
805  SeeAlso     []
806
807******************************************************************************/
808static int
809computeLB(
810  DdManager * table             /* manager */,
811  DdHalfWord * order            /* optimal order for the subset */,
812  int  roots                    /* roots between lower and upper */,
813  int  cost                     /* minimum cost for the subset */,
814  int  lower                    /* lower level to be reordered */,
815  int  upper                    /* upper level to be reordered */,
816  int  level                    /* offset for the current top bottom var */
817  )
818{
819    int i;
820    int lb = cost;
821    int lb1 = 0;
822    int lb2;
823    int support;
824    DdHalfWord ref;
825
826    /* The levels not involved in reordering are not going to change.
827    ** Add their sizes to the lower bound.
828    */
829    for (i = 0; i < lower; i++) {
830        lb += getLevelKeys(table,i);
831    }
832    /* If a variable is in the support, then there is going
833    ** to be at least one node labeled by that variable.
834    */
835    for (i = lower; i <= lower+level; i++) {
836        support = table->subtables[i].keys > 1 ||
837            table->vars[order[i-lower]]->ref > 1;
838        lb1 += support;
839    }
840
841    /* Estimate the number of nodes required to connect the roots to
842    ** the nodes in the bottom part. */
843    if (lower+level+1 < table->size) {
844        if (lower+level < upper)
845            ref = table->vars[order[level+1]]->ref;
846        else
847            ref = table->vars[table->invperm[upper+1]]->ref;
848        lb2 = table->subtables[lower+level+1].keys -
849            (ref > (DdHalfWord) 1) - roots;
850    } else {
851        lb2 = 0;
852    }
853
854    lb += lb1 > lb2 ? lb1 : lb2;
855
856    return(lb);
857
858} /* end of computeLB */
859
860
861/**Function********************************************************************
862
863  Synopsis    [Updates entry for a subset.]
864
865  Description [Updates entry for a subset. Finds the subset, if it exists.
866  If the new order for the subset has lower cost, or if the subset did not
867  exist, it stores the new order and cost. Returns the number of subsets
868  currently in the table.]
869
870  SideEffects [None]
871
872  SeeAlso     []
873
874******************************************************************************/
875static int
876updateEntry(
877  DdManager * table,
878  DdHalfWord * order,
879  int  level,
880  int  cost,
881  DdHalfWord ** orders,
882  int * costs,
883  int  subsets,
884  char * mask,
885  int  lower,
886  int  upper)
887{
888    int i, j;
889    int size = upper - lower + 1;
890
891    /* Build a mask that says what variables are in this subset. */
892    for (i = lower; i <= upper; i++)
893        mask[table->invperm[i]] = 0;
894    for (i = level; i < size; i++)
895        mask[order[i]] = 1;
896
897    /* Check each subset until a match is found or all subsets are examined. */
898    for (i = 0; i < subsets; i++) {
899        DdHalfWord *subset = orders[i];
900        for (j = level; j < size; j++) {
901            if (mask[subset[j]] == 0)
902                break;
903        }
904        if (j == size)          /* no mismatches: success */
905            break;
906    }
907    if (i == subsets || cost < costs[i]) {              /* add or replace */
908        for (j = 0; j < size; j++)
909            orders[i][j] = order[j];
910        costs[i] = cost;
911        subsets += (i == subsets);
912    }
913    return(subsets);
914
915} /* end of updateEntry */
916
917
918/**Function********************************************************************
919
920  Synopsis    [Pushes a variable in the order down to position "level."]
921
922  Description []
923
924  SideEffects [None]
925
926  SeeAlso     []
927
928******************************************************************************/
929static void
930pushDown(
931  DdHalfWord * order,
932  int  j,
933  int  level)
934{
935    int i;
936    DdHalfWord tmp;
937
938    tmp = order[j];
939    for (i = j; i < level; i++) {
940        order[i] = order[i+1];
941    }
942    order[level] = tmp;
943    return;
944
945} /* end of pushDown */
946
947
948/**Function********************************************************************
949
950  Synopsis    [Gathers symmetry information.]
951
952  Description [Translates the symmetry information stored in the next
953  field of each subtable from level to indices. This procedure is called
954  immediately after symmetric sifting, so that the next fields are correct.
955  By translating this informaton in terms of indices, we make it independent
956  of subsequent reorderings. The format used is that of the next fields:
957  a circular list where each variable points to the next variable in the
958  same symmetry group. Only the entries between lower and upper are
959  considered.  The procedure returns a pointer to an array
960  holding the symmetry information if successful; NULL otherwise.]
961
962  SideEffects [None]
963
964  SeeAlso     [checkSymmInfo]
965
966******************************************************************************/
967static DdHalfWord *
968initSymmInfo(
969  DdManager * table,
970  int  lower,
971  int  upper)
972{
973    int level, index, next, nextindex;
974    DdHalfWord *symmInfo;
975
976    symmInfo =  ALLOC(DdHalfWord, table->size);
977    if (symmInfo == NULL) return(NULL);
978
979    for (level = lower; level <= upper; level++) {
980        index = table->invperm[level];
981        next =  table->subtables[level].next;
982        nextindex = table->invperm[next];
983        symmInfo[index] = nextindex;
984    }
985    return(symmInfo);
986
987} /* end of initSymmInfo */
988
989
990/**Function********************************************************************
991
992  Synopsis    [Check symmetry condition.]
993
994  Description [Returns 1 if a variable is the one with the highest index
995  among those belonging to a symmetry group that are in the top part of
996  the BDD.  The top part is given by level.]
997
998  SideEffects [None]
999
1000  SeeAlso     [initSymmInfo]
1001
1002******************************************************************************/
1003static int
1004checkSymmInfo(
1005  DdManager * table,
1006  DdHalfWord * symmInfo,
1007  int  index,
1008  int  level)
1009{
1010    int i;
1011
1012    i = symmInfo[index];
1013    while (i != index) {
1014        if (index < i && table->perm[i] <= level)
1015            return(0);
1016        i = symmInfo[i];
1017    }
1018    return(1);
1019
1020} /* end of checkSymmInfo */
Note: See TracBrowser for help on using the repository browser.