glu-2.2: src/cuBdd/cuddExact.c Source File

00001 
00070 #include "util.h"
00071 #include "cuddInt.h"
00072 
00073 /*---------------------------------------------------------------------------*/
00074 /* Constant declarations                                                     */
00075 /*---------------------------------------------------------------------------*/
00076 
00077 
00078 /*---------------------------------------------------------------------------*/
00079 /* Stucture declarations                                                     */
00080 /*---------------------------------------------------------------------------*/
00081 
00082 /*---------------------------------------------------------------------------*/
00083 /* Type declarations                                                         */
00084 /*---------------------------------------------------------------------------*/
00085 
00086 /*---------------------------------------------------------------------------*/
00087 /* Variable declarations                                                     */
00088 /*---------------------------------------------------------------------------*/
00089 
00090 #ifndef lint
00091 static char rcsid[] DD_UNUSED = "$Id: cuddExact.c,v 1.28 2009/02/19 16:19:19 fabio Exp $";
00092 #endif
00093 
00094 #ifdef DD_STATS
00095 static int ddTotalShuffles;
00096 #endif
00097 
00098 /*---------------------------------------------------------------------------*/
00099 /* Macro declarations                                                        */
00100 /*---------------------------------------------------------------------------*/
00101 
00104 /*---------------------------------------------------------------------------*/
00105 /* Static function prototypes                                                */
00106 /*---------------------------------------------------------------------------*/
00107 
00108 static int getMaxBinomial (int n);
00109 static DdHalfWord ** getMatrix (int rows, int cols);
00110 static void freeMatrix (DdHalfWord **matrix);
00111 static int getLevelKeys (DdManager *table, int l);
00112 static int ddShuffle (DdManager *table, DdHalfWord *permutation, int lower, int upper);
00113 static int ddSiftUp (DdManager *table, int x, int xLow);
00114 static int updateUB (DdManager *table, int oldBound, DdHalfWord *bestOrder, int lower, int upper);
00115 static int ddCountRoots (DdManager *table, int lower, int upper);
00116 static void ddClearGlobal (DdManager *table, int lower, int maxlevel);
00117 static int computeLB (DdManager *table, DdHalfWord *order, int roots, int cost, int lower, int upper, int level);
00118 static int updateEntry (DdManager *table, DdHalfWord *order, int level, int cost, DdHalfWord **orders, int *costs, int subsets, char *mask, int lower, int upper);
00119 static void pushDown (DdHalfWord *order, int j, int level);
00120 static DdHalfWord * initSymmInfo (DdManager *table, int lower, int upper);
00121 static int checkSymmInfo (DdManager *table, DdHalfWord *symmInfo, int index, int level);
00122 
00126 /*---------------------------------------------------------------------------*/
00127 /* Definition of exported functions                                          */
00128 /*---------------------------------------------------------------------------*/
00129 
00130 /*---------------------------------------------------------------------------*/
00131 /* Definition of internal functions                                          */
00132 /*---------------------------------------------------------------------------*/
00133 
00134 
00148 int
00149 cuddExact(
00150   DdManager * table,
00151   int  lower,
00152   int  upper)
00153 {
00154     int k, i, j;
00155     int maxBinomial, oldSubsets, newSubsets;
00156     int subsetCost;
00157     int size;                   /* number of variables to be reordered */
00158     int unused, nvars, level, result;
00159     int upperBound, lowerBound, cost;
00160     int roots;
00161     char *mask = NULL;
00162     DdHalfWord  *symmInfo = NULL;
00163     DdHalfWord **newOrder = NULL;
00164     DdHalfWord **oldOrder = NULL;
00165     int *newCost = NULL;
00166     int *oldCost = NULL;
00167     DdHalfWord **tmpOrder;
00168     int *tmpCost;
00169     DdHalfWord *bestOrder = NULL;
00170     DdHalfWord *order;
00171 #ifdef DD_STATS
00172     int  ddTotalSubsets;
00173 #endif
00174 
00175     /* Restrict the range to be reordered by excluding unused variables
00176     ** at the two ends. */
00177     while (table->subtables[lower].keys == 1 &&
00178            table->vars[table->invperm[lower]]->ref == 1 &&
00179            lower < upper)
00180         lower++;
00181     while (table->subtables[upper].keys == 1 &&
00182            table->vars[table->invperm[upper]]->ref == 1 &&
00183            lower < upper)
00184         upper--;
00185     if (lower == upper) return(1); /* trivial problem */
00186 
00187     /* Apply symmetric sifting to get a good upper bound and to extract
00188     ** symmetry information. */
00189     result = cuddSymmSiftingConv(table,lower,upper);
00190     if (result == 0) goto cuddExactOutOfMem;
00191 
00192 #ifdef DD_STATS
00193     (void) fprintf(table->out,"\n");
00194     ddTotalShuffles = 0;
00195     ddTotalSubsets = 0;
00196 #endif
00197 
00198     /* Initialization. */
00199     nvars = table->size;
00200     size = upper - lower + 1;
00201     /* Count unused variable among those to be reordered.  This is only
00202     ** used to compute maxBinomial. */
00203     unused = 0;
00204     for (i = lower + 1; i < upper; i++) {
00205         if (table->subtables[i].keys == 1 &&
00206             table->vars[table->invperm[i]]->ref == 1)
00207             unused++;
00208     }
00209 
00210     /* Find the maximum number of subsets we may have to store. */
00211     maxBinomial = getMaxBinomial(size - unused);
00212     if (maxBinomial == -1) goto cuddExactOutOfMem;
00213 
00214     newOrder = getMatrix(maxBinomial, size);
00215     if (newOrder == NULL) goto cuddExactOutOfMem;
00216 
00217     newCost = ALLOC(int, maxBinomial);
00218     if (newCost == NULL) goto cuddExactOutOfMem;
00219 
00220     oldOrder = getMatrix(maxBinomial, size);
00221     if (oldOrder == NULL) goto cuddExactOutOfMem;
00222 
00223     oldCost = ALLOC(int, maxBinomial);
00224     if (oldCost == NULL) goto cuddExactOutOfMem;
00225 
00226     bestOrder = ALLOC(DdHalfWord, size);
00227     if (bestOrder == NULL) goto cuddExactOutOfMem;
00228 
00229     mask = ALLOC(char, nvars);
00230     if (mask == NULL) goto cuddExactOutOfMem;
00231 
00232     symmInfo = initSymmInfo(table, lower, upper);
00233     if (symmInfo == NULL) goto cuddExactOutOfMem;
00234 
00235     roots = ddCountRoots(table, lower, upper);
00236 
00237     /* Initialize the old order matrix for the empty subset and the best
00238     ** order to the current order. The cost for the empty subset includes
00239     ** the cost of the levels between upper and the constants. These levels
00240     ** are not going to change. Hence, we count them only once.
00241     */
00242     oldSubsets = 1;
00243     for (i = 0; i < size; i++) {
00244         oldOrder[0][i] = bestOrder[i] = (DdHalfWord) table->invperm[i+lower];
00245     }
00246     subsetCost = table->constants.keys;
00247     for (i = upper + 1; i < nvars; i++)
00248         subsetCost += getLevelKeys(table,i);
00249     oldCost[0] = subsetCost;
00250     /* The upper bound is initialized to the current size of the BDDs. */
00251     upperBound = table->keys - table->isolated;
00252 
00253     /* Now consider subsets of increasing size. */
00254     for (k = 1; k <= size; k++) {
00255 #ifdef DD_STATS
00256         (void) fprintf(table->out,"Processing subsets of size %d\n", k);
00257         fflush(table->out);
00258 #endif
00259         newSubsets = 0;
00260         level = size - k;               /* offset of first bottom variable */
00261 
00262         for (i = 0; i < oldSubsets; i++) { /* for each subset of size k-1 */
00263             order = oldOrder[i];
00264             cost = oldCost[i];
00265             lowerBound = computeLB(table, order, roots, cost, lower, upper,
00266                                    level);
00267             if (lowerBound >= upperBound)
00268                 continue;
00269             /* Impose new order. */
00270             result = ddShuffle(table, order, lower, upper);
00271             if (result == 0) goto cuddExactOutOfMem;
00272             upperBound = updateUB(table,upperBound,bestOrder,lower,upper);
00273             /* For each top bottom variable. */
00274             for (j = level; j >= 0; j--) {
00275                 /* Skip unused variables. */
00276                 if (table->subtables[j+lower-1].keys == 1 &&
00277                     table->vars[table->invperm[j+lower-1]]->ref == 1) continue;
00278                 /* Find cost under this order. */
00279                 subsetCost = cost + getLevelKeys(table, lower + level);
00280                 newSubsets = updateEntry(table, order, level, subsetCost,
00281                                          newOrder, newCost, newSubsets, mask,
00282                                          lower, upper);
00283                 if (j == 0)
00284                     break;
00285                 if (checkSymmInfo(table, symmInfo, order[j-1], level) == 0)
00286                     continue;
00287                 pushDown(order,j-1,level);
00288                 /* Impose new order. */
00289                 result = ddShuffle(table, order, lower, upper);
00290                 if (result == 0) goto cuddExactOutOfMem;
00291                 upperBound = updateUB(table,upperBound,bestOrder,lower,upper);
00292             } /* for each bottom variable */
00293         } /* for each subset of size k */
00294 
00295         /* New orders become old orders in preparation for next iteration. */
00296         tmpOrder = oldOrder; tmpCost = oldCost;
00297         oldOrder = newOrder; oldCost = newCost;
00298         newOrder = tmpOrder; newCost = tmpCost;
00299 #ifdef DD_STATS
00300         ddTotalSubsets += newSubsets;
00301 #endif
00302         oldSubsets = newSubsets;
00303     }
00304     result = ddShuffle(table, bestOrder, lower, upper);
00305     if (result == 0) goto cuddExactOutOfMem;
00306 #ifdef DD_STATS
00307 #ifdef DD_VERBOSE
00308     (void) fprintf(table->out,"\n");
00309 #endif
00310     (void) fprintf(table->out,"#:S_EXACT   %8d: total subsets\n",
00311                    ddTotalSubsets);
00312     (void) fprintf(table->out,"#:H_EXACT   %8d: total shuffles",
00313                    ddTotalShuffles);
00314 #endif
00315 
00316     freeMatrix(newOrder);
00317     freeMatrix(oldOrder);
00318     FREE(bestOrder);
00319     FREE(oldCost);
00320     FREE(newCost);
00321     FREE(symmInfo);
00322     FREE(mask);
00323     return(1);
00324 
00325 cuddExactOutOfMem:
00326 
00327     if (newOrder != NULL) freeMatrix(newOrder);
00328     if (oldOrder != NULL) freeMatrix(oldOrder);
00329     if (bestOrder != NULL) FREE(bestOrder);
00330     if (oldCost != NULL) FREE(oldCost);
00331     if (newCost != NULL) FREE(newCost);
00332     if (symmInfo != NULL) FREE(symmInfo);
00333     if (mask != NULL) FREE(mask);
00334     table->errorCode = CUDD_MEMORY_OUT;
00335     return(0);
00336 
00337 } /* end of cuddExact */
00338 
00339 
00358 static int
00359 getMaxBinomial(
00360   int n)
00361 {
00362     double i, j, result;
00363 
00364     if (n < 0 || n > 33) return(-1); /* error */
00365     if (n < 2) return(1);
00366 
00367     for (result = (double)((n+3)/2), i = result+1, j=2; i <= n; i++, j++) {
00368         result *= i;
00369         result /= j;
00370     }
00371 
00372     return((int)result);
00373 
00374 } /* end of getMaxBinomial */
00375 
00376 
00377 #if 0
00378 
00390 static int
00391 gcd(
00392   int  x,
00393   int  y)
00394 {
00395     int a;
00396     int b;
00397     int lsbMask;
00398 
00399     /* GCD(n,0) = n. */
00400     if (x == 0) return(y);
00401     if (y == 0) return(x);
00402 
00403     a = x; b = y; lsbMask = 1;
00404 
00405     /* Here both a and b are != 0. The iteration maintains this invariant.
00406     ** Hence, we only need to check for when they become equal.
00407     */
00408     while (a != b) {
00409         if (a & lsbMask) {
00410             if (b & lsbMask) {  /* both odd */
00411                 if (a < b) {
00412                     b = (b - a) >> 1;
00413                 } else {
00414                     a = (a - b) >> 1;
00415                 }
00416             } else {            /* a odd, b even */
00417                 b >>= 1;
00418             }
00419         } else {
00420             if (b & lsbMask) {  /* a even, b odd */
00421                 a >>= 1;
00422             } else {            /* both even */
00423                 lsbMask <<= 1;
00424             }
00425         }
00426     }
00427 
00428     return(a);
00429 
00430 } /* end of gcd */
00431 #endif
00432 
00433 
00446 static DdHalfWord **
00447 getMatrix(
00448   int  rows /* number of rows */,
00449   int  cols /* number of columns */)
00450 {
00451     DdHalfWord **matrix;
00452     int i;
00453 
00454     if (cols*rows == 0) return(NULL);
00455     matrix = ALLOC(DdHalfWord *, rows);
00456     if (matrix == NULL) return(NULL);
00457     matrix[0] = ALLOC(DdHalfWord, cols*rows);
00458     if (matrix[0] == NULL) {
00459         FREE(matrix);
00460         return(NULL);
00461     }
00462     for (i = 1; i < rows; i++) {
00463         matrix[i] = matrix[i-1] + cols;
00464     }
00465     return(matrix);
00466 
00467 } /* end of getMatrix */
00468 
00469 
00481 static void
00482 freeMatrix(
00483   DdHalfWord ** matrix)
00484 {
00485     FREE(matrix[0]);
00486     FREE(matrix);
00487     return;
00488 
00489 } /* end of freeMatrix */
00490 
00491 
00504 static int
00505 getLevelKeys(
00506   DdManager * table,
00507   int  l)
00508 {
00509     int isolated;
00510     int x;        /* x is an index */
00511 
00512     x = table->invperm[l];
00513     isolated = table->vars[x]->ref == 1;
00514 
00515     return(table->subtables[l].keys - isolated);
00516 
00517 } /* end of getLevelKeys */
00518 
00519 
00536 static int
00537 ddShuffle(
00538   DdManager * table,
00539   DdHalfWord * permutation,
00540   int  lower,
00541   int  upper)
00542 {
00543     DdHalfWord  index;
00544     int         level;
00545     int         position;
00546 #if 0
00547     int         numvars;
00548 #endif
00549     int         result;
00550 #ifdef DD_STATS
00551     long        localTime;
00552     int         initialSize;
00553 #ifdef DD_VERBOSE
00554     int         finalSize;
00555 #endif
00556     int         previousSize;
00557 #endif
00558 
00559 #ifdef DD_STATS
00560     localTime = util_cpu_time();
00561     initialSize = table->keys - table->isolated;
00562 #endif
00563 
00564 #if 0
00565     numvars = table->size;
00566 
00567     (void) fprintf(table->out,"%d:", ddTotalShuffles);
00568     for (level = 0; level < numvars; level++) {
00569         (void) fprintf(table->out," %d", table->invperm[level]);
00570     }
00571     (void) fprintf(table->out,"\n");
00572 #endif
00573 
00574     for (level = 0; level <= upper - lower; level++) {
00575         index = permutation[level];
00576         position = table->perm[index];
00577 #ifdef DD_STATS
00578         previousSize = table->keys - table->isolated;
00579 #endif
00580         result = ddSiftUp(table,position,level+lower);
00581         if (!result) return(0);
00582     }
00583 
00584 #ifdef DD_STATS
00585     ddTotalShuffles++;
00586 #ifdef DD_VERBOSE
00587     finalSize = table->keys - table->isolated;
00588     if (finalSize < initialSize) {
00589         (void) fprintf(table->out,"-");
00590     } else if (finalSize > initialSize) {
00591         (void) fprintf(table->out,"+");
00592     } else {
00593         (void) fprintf(table->out,"=");
00594     }
00595     if ((ddTotalShuffles & 63) == 0) (void) fprintf(table->out,"\n");
00596     fflush(table->out);
00597 #endif
00598 #endif
00599 
00600     return(1);
00601 
00602 } /* end of ddShuffle */
00603 
00604 
00618 static int
00619 ddSiftUp(
00620   DdManager * table,
00621   int  x,
00622   int  xLow)
00623 {
00624     int        y;
00625     int        size;
00626 
00627     y = cuddNextLow(table,x);
00628     while (y >= xLow) {
00629         size = cuddSwapInPlace(table,y,x);
00630         if (size == 0) {
00631             return(0);
00632         }
00633         x = y;
00634         y = cuddNextLow(table,x);
00635     }
00636     return(1);
00637 
00638 } /* end of ddSiftUp */
00639 
00640 
00653 static int
00654 updateUB(
00655   DdManager * table,
00656   int  oldBound,
00657   DdHalfWord * bestOrder,
00658   int  lower,
00659   int  upper)
00660 {
00661     int i;
00662     int newBound = table->keys - table->isolated;
00663 
00664     if (newBound < oldBound) {
00665 #ifdef DD_STATS
00666         (void) fprintf(table->out,"New upper bound = %d\n", newBound);
00667         fflush(table->out);
00668 #endif
00669         for (i = lower; i <= upper; i++)
00670             bestOrder[i-lower] = (DdHalfWord) table->invperm[i];
00671         return(newBound);
00672     } else {
00673         return(oldBound);
00674     }
00675 
00676 } /* end of updateUB */
00677 
00678 
00695 static int
00696 ddCountRoots(
00697   DdManager * table,
00698   int  lower,
00699   int  upper)
00700 {
00701     int i,j;
00702     DdNode *f;
00703     DdNodePtr *nodelist;
00704     DdNode *sentinel = &(table->sentinel);
00705     int slots;
00706     int roots = 0;
00707     int maxlevel = lower;
00708 
00709     for (i = lower; i <= upper; i++) {
00710         nodelist = table->subtables[i].nodelist;
00711         slots = table->subtables[i].slots;
00712         for (j = 0; j < slots; j++) {
00713             f = nodelist[j];
00714             while (f != sentinel) {
00715                 /* A node is a root of the DAG if it cannot be
00716                 ** reached by nodes above it. If a node was never
00717                 ** reached during the previous depth-first searches,
00718                 ** then it is a root, and we start a new depth-first
00719                 ** search from it.
00720                 */
00721                 if (!Cudd_IsComplement(f->next)) {
00722                     if (f != table->vars[f->index]) {
00723                         roots++;
00724                     }
00725                 }
00726                 if (!Cudd_IsConstant(cuddT(f))) {
00727                     cuddT(f)->next = Cudd_Complement(cuddT(f)->next);
00728                     if (table->perm[cuddT(f)->index] > maxlevel)
00729                         maxlevel = table->perm[cuddT(f)->index];
00730                 }
00731                 if (!Cudd_IsConstant(cuddE(f))) {
00732                     Cudd_Regular(cuddE(f))->next =
00733                         Cudd_Complement(Cudd_Regular(cuddE(f))->next);
00734                     if (table->perm[Cudd_Regular(cuddE(f))->index] > maxlevel)
00735                         maxlevel = table->perm[Cudd_Regular(cuddE(f))->index];
00736                 }
00737                 f = Cudd_Regular(f->next);
00738             }
00739         }
00740     }
00741     ddClearGlobal(table, lower, maxlevel);
00742 
00743     return(roots);
00744 
00745 } /* end of ddCountRoots */
00746 
00747 
00762 static void
00763 ddClearGlobal(
00764   DdManager * table,
00765   int  lower,
00766   int  maxlevel)
00767 {
00768     int i,j;
00769     DdNode *f;
00770     DdNodePtr *nodelist;
00771     DdNode *sentinel = &(table->sentinel);
00772     int slots;
00773 
00774     for (i = lower; i <= maxlevel; i++) {
00775         nodelist = table->subtables[i].nodelist;
00776         slots = table->subtables[i].slots;
00777         for (j = 0; j < slots; j++) {
00778             f = nodelist[j];
00779             while (f != sentinel) {
00780                 f->next = Cudd_Regular(f->next);
00781                 f = f->next;
00782             }
00783         }
00784     }
00785 
00786 } /* end of ddClearGlobal */
00787 
00788 
00808 static int
00809 computeLB(
00810   DdManager * table             /* manager */,
00811   DdHalfWord * order            /* optimal order for the subset */,
00812   int  roots                    /* roots between lower and upper */,
00813   int  cost                     /* minimum cost for the subset */,
00814   int  lower                    /* lower level to be reordered */,
00815   int  upper                    /* upper level to be reordered */,
00816   int  level                    /* offset for the current top bottom var */
00817   )
00818 {
00819     int i;
00820     int lb = cost;
00821     int lb1 = 0;
00822     int lb2;
00823     int support;
00824     DdHalfWord ref;
00825 
00826     /* The levels not involved in reordering are not going to change.
00827     ** Add their sizes to the lower bound.
00828     */
00829     for (i = 0; i < lower; i++) {
00830         lb += getLevelKeys(table,i);
00831     }
00832     /* If a variable is in the support, then there is going
00833     ** to be at least one node labeled by that variable.
00834     */
00835     for (i = lower; i <= lower+level; i++) {
00836         support = table->subtables[i].keys > 1 ||
00837             table->vars[order[i-lower]]->ref > 1;
00838         lb1 += support;
00839     }
00840 
00841     /* Estimate the number of nodes required to connect the roots to
00842     ** the nodes in the bottom part. */
00843     if (lower+level+1 < table->size) {
00844         if (lower+level < upper)
00845             ref = table->vars[order[level+1]]->ref;
00846         else
00847             ref = table->vars[table->invperm[upper+1]]->ref;
00848         lb2 = table->subtables[lower+level+1].keys -
00849             (ref > (DdHalfWord) 1) - roots;
00850     } else {
00851         lb2 = 0;
00852     }
00853 
00854     lb += lb1 > lb2 ? lb1 : lb2;
00855 
00856     return(lb);
00857 
00858 } /* end of computeLB */
00859 
00860 
00875 static int
00876 updateEntry(
00877   DdManager * table,
00878   DdHalfWord * order,
00879   int  level,
00880   int  cost,
00881   DdHalfWord ** orders,
00882   int * costs,
00883   int  subsets,
00884   char * mask,
00885   int  lower,
00886   int  upper)
00887 {
00888     int i, j;
00889     int size = upper - lower + 1;
00890 
00891     /* Build a mask that says what variables are in this subset. */
00892     for (i = lower; i <= upper; i++)
00893         mask[table->invperm[i]] = 0;
00894     for (i = level; i < size; i++)
00895         mask[order[i]] = 1;
00896 
00897     /* Check each subset until a match is found or all subsets are examined. */
00898     for (i = 0; i < subsets; i++) {
00899         DdHalfWord *subset = orders[i];
00900         for (j = level; j < size; j++) {
00901             if (mask[subset[j]] == 0)
00902                 break;
00903         }
00904         if (j == size)          /* no mismatches: success */
00905             break;
00906     }
00907     if (i == subsets || cost < costs[i]) {              /* add or replace */
00908         for (j = 0; j < size; j++)
00909             orders[i][j] = order[j];
00910         costs[i] = cost;
00911         subsets += (i == subsets);
00912     }
00913     return(subsets);
00914 
00915 } /* end of updateEntry */
00916 
00917 
00929 static void
00930 pushDown(
00931   DdHalfWord * order,
00932   int  j,
00933   int  level)
00934 {
00935     int i;
00936     DdHalfWord tmp;
00937 
00938     tmp = order[j];
00939     for (i = j; i < level; i++) {
00940         order[i] = order[i+1];
00941     }
00942     order[level] = tmp;
00943     return;
00944 
00945 } /* end of pushDown */
00946 
00947 
00967 static DdHalfWord *
00968 initSymmInfo(
00969   DdManager * table,
00970   int  lower,
00971   int  upper)
00972 {
00973     int level, index, next, nextindex;
00974     DdHalfWord *symmInfo;
00975 
00976     symmInfo =  ALLOC(DdHalfWord, table->size);
00977     if (symmInfo == NULL) return(NULL);
00978 
00979     for (level = lower; level <= upper; level++) {
00980         index = table->invperm[level];
00981         next =  table->subtables[level].next;
00982         nextindex = table->invperm[next];
00983         symmInfo[index] = nextindex;
00984     }
00985     return(symmInfo);
00986 
00987 } /* end of initSymmInfo */
00988 
00989 
01003 static int
01004 checkSymmInfo(
01005   DdManager * table,
01006   DdHalfWord * symmInfo,
01007   int  index,
01008   int  level)
01009 {
01010     int i;
01011 
01012     i = symmInfo[index];
01013     while (i != index) {
01014         if (index < i && table->perm[i] <= level)
01015             return(0);
01016         i = symmInfo[i];
01017     }
01018     return(1);
01019 
01020 } /* end of checkSymmInfo */