abc70930: src/bdd/cudd/cuddUtil.c Source File

00001 
00079 #include "util_hack.h"
00080 #include "cuddInt.h"
00081 
00082 /*---------------------------------------------------------------------------*/
00083 /* Constant declarations                                                     */
00084 /*---------------------------------------------------------------------------*/
00085 
00086 /* Random generator constants. */
00087 #define MODULUS1 2147483563
00088 #define LEQA1 40014
00089 #define LEQQ1 53668
00090 #define LEQR1 12211
00091 #define MODULUS2 2147483399
00092 #define LEQA2 40692
00093 #define LEQQ2 52774
00094 #define LEQR2 3791
00095 #define STAB_SIZE 64
00096 #define STAB_DIV (1 + (MODULUS1 - 1) / STAB_SIZE)
00097 
00098 /*---------------------------------------------------------------------------*/
00099 /* Stucture declarations                                                     */
00100 /*---------------------------------------------------------------------------*/
00101 
00102 /*---------------------------------------------------------------------------*/
00103 /* Type declarations                                                         */
00104 /*---------------------------------------------------------------------------*/
00105 
00106 
00107 /*---------------------------------------------------------------------------*/
00108 /* Variable declarations                                                     */
00109 /*---------------------------------------------------------------------------*/
00110 
00111 #ifndef lint
00112 static char rcsid[] DD_UNUSED = "$Id: cuddUtil.c,v 1.1.1.1 2003/02/24 22:23:53 wjiang Exp $";
00113 #endif
00114 
00115 static  DdNode  *background, *zero;
00116 
00117 static  long cuddRand = 0;
00118 static  long cuddRand2;
00119 static  long shuffleSelect;
00120 static  long shuffleTable[STAB_SIZE];
00121 
00122 /*---------------------------------------------------------------------------*/
00123 /* Macro declarations                                                        */
00124 /*---------------------------------------------------------------------------*/
00125 
00126 #define bang(f) ((Cudd_IsComplement(f)) ? '!' : ' ')
00127 
00130 /*---------------------------------------------------------------------------*/
00131 /* Static function prototypes                                                */
00132 /*---------------------------------------------------------------------------*/
00133 
00134 static int dp2 ARGS((DdManager *dd, DdNode *f, st_table *t));
00135 static void ddPrintMintermAux ARGS((DdManager *dd, DdNode *node, int *list));
00136 static int ddDagInt ARGS((DdNode *n));
00137 static int cuddEstimateCofactor ARGS((DdManager *dd, st_table *table, DdNode * node, int i, int phase, DdNode ** ptr));
00138 static DdNode * cuddUniqueLookup ARGS((DdManager * unique, int  index, DdNode * T, DdNode * E));
00139 static int cuddEstimateCofactorSimple ARGS((DdNode * node, int i));
00140 static double ddCountMintermAux ARGS((DdNode *node, double max, DdHashTable *table));
00141 static int ddEpdCountMintermAux ARGS((DdNode *node, EpDouble *max, EpDouble *epd, st_table *table));
00142 static double ddCountPathAux ARGS((DdNode *node, st_table *table));
00143 static double ddCountPathsToNonZero ARGS((DdNode * N, st_table * table));
00144 static void ddSupportStep ARGS((DdNode *f, int *support));
00145 static void ddClearFlag ARGS((DdNode *f));
00146 static int ddLeavesInt ARGS((DdNode *n));
00147 static int ddPickArbitraryMinterms ARGS((DdManager *dd, DdNode *node, int nvars, int nminterms, char **string));
00148 static int ddPickRepresentativeCube ARGS((DdManager *dd, DdNode *node, int nvars, double *weight, char *string));
00149 static enum st_retval ddEpdFree ARGS((char * key, char * value, char * arg));
00150 
00154 /*---------------------------------------------------------------------------*/
00155 /* Definition of exported functions                                          */
00156 /*---------------------------------------------------------------------------*/
00157 
00158 
00174 int
00175 Cudd_PrintMinterm(
00176   DdManager * manager,
00177   DdNode * node)
00178 {
00179     int         i, *list;
00180 
00181     background = manager->background;
00182     zero = Cudd_Not(manager->one);
00183     list = ALLOC(int,manager->size);
00184     if (list == NULL) {
00185         manager->errorCode = CUDD_MEMORY_OUT;
00186         return(0);
00187     }
00188     for (i = 0; i < manager->size; i++) list[i] = 2;
00189     ddPrintMintermAux(manager,node,list);
00190     FREE(list);
00191     return(1);
00192 
00193 } /* end of Cudd_PrintMinterm */
00194 
00195 
00211 int
00212 Cudd_bddPrintCover(
00213   DdManager *dd,
00214   DdNode *l,
00215   DdNode *u)
00216 {
00217     int *array;
00218     int q, result;
00219     DdNode *lb;
00220 #ifdef DD_DEBUG
00221     DdNode *cover;
00222 #endif
00223 
00224     array = ALLOC(int, Cudd_ReadSize(dd));
00225     if (array == NULL) return(0);
00226     lb = l;
00227     cuddRef(lb);
00228 #ifdef DD_DEBUG
00229     cover = Cudd_ReadLogicZero(dd);
00230     cuddRef(cover);
00231 #endif
00232     while (lb != Cudd_ReadLogicZero(dd)) {
00233         DdNode *implicant, *prime, *tmp;
00234         int length;
00235         implicant = Cudd_LargestCube(dd,lb,&length);
00236         if (implicant == NULL) {
00237             Cudd_RecursiveDeref(dd,lb);
00238             FREE(array);
00239             return(0);
00240         }
00241         cuddRef(implicant);
00242         prime = Cudd_bddMakePrime(dd,implicant,u);
00243         if (prime == NULL) {
00244             Cudd_RecursiveDeref(dd,lb);
00245             Cudd_RecursiveDeref(dd,implicant);
00246             FREE(array);
00247             return(0);
00248         }
00249         cuddRef(prime);
00250         Cudd_RecursiveDeref(dd,implicant);
00251         tmp = Cudd_bddAnd(dd,lb,Cudd_Not(prime));
00252         if (tmp == NULL) {
00253             Cudd_RecursiveDeref(dd,lb);
00254             Cudd_RecursiveDeref(dd,prime);
00255             FREE(array);
00256             return(0);
00257         }
00258         cuddRef(tmp);
00259         Cudd_RecursiveDeref(dd,lb);
00260         lb = tmp;
00261         result = Cudd_BddToCubeArray(dd,prime,array);
00262         if (result == 0) {
00263             Cudd_RecursiveDeref(dd,lb);
00264             Cudd_RecursiveDeref(dd,prime);
00265             FREE(array);
00266             return(0);
00267         }
00268         for (q = 0; q < dd->size; q++) {
00269             switch (array[q]) {
00270             case 0:
00271                 (void) fprintf(dd->out, "0");
00272                 break;
00273             case 1:
00274                 (void) fprintf(dd->out, "1");
00275                 break;
00276             case 2:
00277                 (void) fprintf(dd->out, "-");
00278                 break;
00279             default:
00280                 (void) fprintf(dd->out, "?");
00281             }
00282         }
00283         (void) fprintf(dd->out, " 1\n");
00284 #ifdef DD_DEBUG
00285         tmp = Cudd_bddOr(dd,prime,cover);
00286         if (tmp == NULL) {
00287             Cudd_RecursiveDeref(dd,cover);
00288             Cudd_RecursiveDeref(dd,lb);
00289             Cudd_RecursiveDeref(dd,prime);
00290             FREE(array);
00291             return(0);
00292         }
00293         cuddRef(tmp);
00294         Cudd_RecursiveDeref(dd,cover);
00295         cover = tmp;
00296 #endif
00297         Cudd_RecursiveDeref(dd,prime);
00298     }
00299     (void) fprintf(dd->out, "\n");
00300     Cudd_RecursiveDeref(dd,lb);
00301     FREE(array);
00302 #ifdef DD_DEBUG
00303     if (!Cudd_bddLeq(dd,cover,u) || !Cudd_bddLeq(dd,l,cover)) {
00304         Cudd_RecursiveDeref(dd,cover);
00305         return(0);
00306     }
00307     Cudd_RecursiveDeref(dd,cover);
00308 #endif
00309     return(1);
00310 
00311 } /* end of Cudd_bddPrintCover */
00312 
00313 
00340 int
00341 Cudd_PrintDebug(
00342   DdManager * dd,
00343   DdNode * f,
00344   int  n,
00345   int  pr)
00346 {
00347     DdNode *azero, *bzero;
00348     int    nodes;
00349     int    leaves;
00350     double minterms;
00351     int    retval = 1;
00352 
00353     if (f == NULL) {
00354         (void) fprintf(dd->out,": is the NULL DD\n");
00355         (void) fflush(dd->out);
00356         return(0);
00357     }
00358     azero = DD_ZERO(dd);
00359     bzero = Cudd_Not(DD_ONE(dd));
00360     if ((f == azero || f == bzero) && pr > 0){
00361        (void) fprintf(dd->out,": is the zero DD\n");
00362        (void) fflush(dd->out);
00363        return(1);
00364     }
00365     if (pr > 0) {
00366         nodes = Cudd_DagSize(f);
00367         if (nodes == CUDD_OUT_OF_MEM) retval = 0;
00368         leaves = Cudd_CountLeaves(f);
00369         if (leaves == CUDD_OUT_OF_MEM) retval = 0;
00370         minterms = Cudd_CountMinterm(dd, f, n);
00371         if (minterms == (double)CUDD_OUT_OF_MEM) retval = 0;
00372         (void) fprintf(dd->out,": %d nodes %d leaves %g minterms\n",
00373                        nodes, leaves, minterms);
00374         if (pr > 2) {
00375             if (!cuddP(dd, f)) retval = 0;
00376         }
00377         if (pr == 2 || pr > 3) {
00378             if (!Cudd_PrintMinterm(dd,f)) retval = 0;
00379             (void) fprintf(dd->out,"\n");
00380         }
00381         (void) fflush(dd->out);
00382     }
00383     return(retval);
00384 
00385 } /* end of Cudd_PrintDebug */
00386 
00387 
00400 int
00401 Cudd_DagSize(
00402   DdNode * node)
00403 {
00404     int i;      
00405 
00406     i = ddDagInt(Cudd_Regular(node));
00407     ddClearFlag(Cudd_Regular(node));
00408 
00409     return(i);
00410 
00411 } /* end of Cudd_DagSize */
00412 
00413 
00435 int
00436 Cudd_EstimateCofactor(
00437   DdManager *dd /* manager */,
00438   DdNode * f    /* function */,
00439   int i         /* index of variable */,
00440   int phase     /* 1: positive; 0: negative */
00441   )
00442 {
00443     int val;
00444     DdNode *ptr;
00445     st_table *table;
00446 
00447     table = st_init_table(st_ptrcmp,st_ptrhash);
00448     if (table == NULL) return(CUDD_OUT_OF_MEM);
00449     val = cuddEstimateCofactor(dd,table,Cudd_Regular(f),i,phase,&ptr);
00450     ddClearFlag(Cudd_Regular(f));
00451     st_free_table(table);
00452 
00453     return(val);
00454 
00455 } /* end of Cudd_EstimateCofactor */
00456 
00457 
00475 int
00476 Cudd_EstimateCofactorSimple(
00477   DdNode * node,
00478   int i)
00479 {
00480     int val;    
00481 
00482     val = cuddEstimateCofactorSimple(Cudd_Regular(node),i);
00483     ddClearFlag(Cudd_Regular(node));
00484 
00485     return(val);
00486 
00487 } /* end of Cudd_EstimateCofactorSimple */
00488 
00489 
00502 int
00503 Cudd_SharingSize(
00504   DdNode ** nodeArray,
00505   int  n)
00506 {
00507     int i,j;    
00508 
00509     i = 0;
00510     for (j = 0; j < n; j++) {
00511         i += ddDagInt(Cudd_Regular(nodeArray[j]));
00512     }
00513     for (j = 0; j < n; j++) {
00514         ddClearFlag(Cudd_Regular(nodeArray[j]));
00515     }
00516     return(i);
00517 
00518 } /* end of Cudd_SharingSize */
00519 
00520 
00536 double
00537 Cudd_CountMinterm(
00538   DdManager * manager,
00539   DdNode * node,
00540   int  nvars)
00541 {
00542     double      max;
00543     DdHashTable *table;
00544     double      res;
00545     CUDD_VALUE_TYPE epsilon;
00546 
00547     background = manager->background;
00548     zero = Cudd_Not(manager->one);
00549     
00550     max = pow(2.0,(double)nvars);
00551     table = cuddHashTableInit(manager,1,2);
00552     if (table == NULL) {
00553         return((double)CUDD_OUT_OF_MEM);
00554     }
00555     epsilon = Cudd_ReadEpsilon(manager);
00556     Cudd_SetEpsilon(manager,(CUDD_VALUE_TYPE)0.0);
00557     res = ddCountMintermAux(node,max,table);
00558     cuddHashTableQuit(table);
00559     Cudd_SetEpsilon(manager,epsilon);
00560 
00561     return(res);
00562 
00563 } /* end of Cudd_CountMinterm */
00564 
00565 
00581 double
00582 Cudd_CountPath(
00583   DdNode * node)
00584 {
00585 
00586     st_table    *table;
00587     double      i;      
00588 
00589     table = st_init_table(st_ptrcmp,st_ptrhash);
00590     if (table == NULL) {
00591         return((double)CUDD_OUT_OF_MEM);
00592     }
00593     i = ddCountPathAux(Cudd_Regular(node),table);
00594     st_foreach(table, cuddStCountfree, NULL);
00595     st_free_table(table);
00596     return(i);
00597 
00598 } /* end of Cudd_CountPath */
00599 
00600 
00615 int
00616 Cudd_EpdCountMinterm(
00617   DdManager * manager,
00618   DdNode * node,
00619   int  nvars,
00620   EpDouble * epd)
00621 {
00622     EpDouble    max, tmp;
00623     st_table    *table;
00624     int         status;
00625 
00626     background = manager->background;
00627     zero = Cudd_Not(manager->one);
00628     
00629     EpdPow2(nvars, &max);
00630     table = st_init_table(EpdCmp, st_ptrhash);
00631     if (table == NULL) {
00632         EpdMakeZero(epd, 0);
00633         return(CUDD_OUT_OF_MEM);
00634     }
00635     status = ddEpdCountMintermAux(Cudd_Regular(node),&max,epd,table);
00636     st_foreach(table, ddEpdFree, NULL);
00637     st_free_table(table);
00638     if (status == CUDD_OUT_OF_MEM) {
00639         EpdMakeZero(epd, 0);
00640         return(CUDD_OUT_OF_MEM);
00641     }
00642     if (Cudd_IsComplement(node)) {
00643         EpdSubtract3(&max, epd, &tmp);
00644         EpdCopy(&tmp, epd);
00645     }
00646     return(0);
00647 
00648 } /* end of Cudd_EpdCountMinterm */
00649 
00650 
00665 double
00666 Cudd_CountPathsToNonZero(
00667   DdNode * node)
00668 {
00669 
00670     st_table    *table;
00671     double      i;      
00672 
00673     table = st_init_table(st_ptrcmp,st_ptrhash);
00674     if (table == NULL) {
00675         return((double)CUDD_OUT_OF_MEM);
00676     }
00677     i = ddCountPathsToNonZero(node,table);
00678     st_foreach(table, cuddStCountfree, NULL);
00679     st_free_table(table);
00680     return(i);
00681 
00682 } /* end of Cudd_CountPathsToNonZero */
00683 
00684 
00698 DdNode *
00699 Cudd_Support(
00700   DdManager * dd /* manager */,
00701   DdNode * f /* DD whose support is sought */)
00702 {
00703     int *support;
00704     DdNode *res, *tmp, *var;
00705     int i,j;
00706     int size;
00707 
00708     /* Allocate and initialize support array for ddSupportStep. */
00709     size = ddMax(dd->size, dd->sizeZ);
00710     support = ALLOC(int,size);
00711     if (support == NULL) {
00712         dd->errorCode = CUDD_MEMORY_OUT;
00713         return(NULL);
00714     }
00715     for (i = 0; i < size; i++) {
00716         support[i] = 0;
00717     }
00718 
00719     /* Compute support and clean up markers. */
00720     ddSupportStep(Cudd_Regular(f),support);
00721     ddClearFlag(Cudd_Regular(f));
00722 
00723     /* Transform support from array to cube. */
00724     do {
00725         dd->reordered = 0;
00726         res = DD_ONE(dd);
00727         cuddRef(res);
00728         for (j = size - 1; j >= 0; j--) { /* for each level bottom-up */
00729             i = (j >= dd->size) ? j : dd->invperm[j];
00730             if (support[i] == 1) {
00731                 var = cuddUniqueInter(dd,i,dd->one,Cudd_Not(dd->one));
00732                 cuddRef(var);
00733                 tmp = cuddBddAndRecur(dd,res,var);
00734                 if (tmp == NULL) {
00735                     Cudd_RecursiveDeref(dd,res);
00736                     Cudd_RecursiveDeref(dd,var);
00737                     res = NULL;
00738                     break;
00739                 }
00740                 cuddRef(tmp);
00741                 Cudd_RecursiveDeref(dd,res);
00742                 Cudd_RecursiveDeref(dd,var);
00743                 res = tmp;
00744             }
00745         }
00746     } while (dd->reordered == 1);
00747 
00748     FREE(support);
00749     if (res != NULL) cuddDeref(res);
00750     return(res);
00751 
00752 } /* end of Cudd_Support */
00753 
00754 
00767 int *
00768 Cudd_SupportIndex(
00769   DdManager * dd /* manager */,
00770   DdNode * f /* DD whose support is sought */)
00771 {
00772     int *support;
00773     int i;
00774     int size;
00775 
00776     /* Allocate and initialize support array for ddSupportStep. */
00777     size = ddMax(dd->size, dd->sizeZ);
00778     support = ALLOC(int,size);
00779     if (support == NULL) {
00780         dd->errorCode = CUDD_MEMORY_OUT;
00781         return(NULL);
00782     }
00783     for (i = 0; i < size; i++) {
00784         support[i] = 0;
00785     }
00786 
00787     /* Compute support and clean up markers. */
00788     ddSupportStep(Cudd_Regular(f),support);
00789     ddClearFlag(Cudd_Regular(f));
00790 
00791     return(support);
00792 
00793 } /* end of Cudd_SupportIndex */
00794 
00795 
00809 int
00810 Cudd_SupportSize(
00811   DdManager * dd /* manager */,
00812   DdNode * f /* DD whose support size is sought */)
00813 {
00814     int *support;
00815     int i;
00816     int size;
00817     int count;
00818 
00819     /* Allocate and initialize support array for ddSupportStep. */
00820     size = ddMax(dd->size, dd->sizeZ);
00821     support = ALLOC(int,size);
00822     if (support == NULL) {
00823         dd->errorCode = CUDD_MEMORY_OUT;
00824         return(CUDD_OUT_OF_MEM);
00825     }
00826     for (i = 0; i < size; i++) {
00827         support[i] = 0;
00828     }
00829 
00830     /* Compute support and clean up markers. */
00831     ddSupportStep(Cudd_Regular(f),support);
00832     ddClearFlag(Cudd_Regular(f));
00833 
00834     /* Count support variables. */
00835     count = 0;
00836     for (i = 0; i < size; i++) {
00837         if (support[i] == 1) count++;
00838     }
00839 
00840     FREE(support);
00841     return(count);
00842 
00843 } /* end of Cudd_SupportSize */
00844 
00845 
00860 DdNode *
00861 Cudd_VectorSupport(
00862   DdManager * dd /* manager */,
00863   DdNode ** F /* array of DDs whose support is sought */,
00864   int  n /* size of the array */)
00865 {
00866     int *support;
00867     DdNode *res, *tmp, *var;
00868     int i,j;
00869     int size;
00870 
00871     /* Allocate and initialize support array for ddSupportStep. */
00872     size = ddMax(dd->size, dd->sizeZ);
00873     support = ALLOC(int,size);
00874     if (support == NULL) {
00875         dd->errorCode = CUDD_MEMORY_OUT;
00876         return(NULL);
00877     }
00878     for (i = 0; i < size; i++) {
00879         support[i] = 0;
00880     }
00881 
00882     /* Compute support and clean up markers. */
00883     for (i = 0; i < n; i++) {
00884         ddSupportStep(Cudd_Regular(F[i]),support);
00885     }
00886     for (i = 0; i < n; i++) {
00887         ddClearFlag(Cudd_Regular(F[i]));
00888     }
00889 
00890     /* Transform support from array to cube. */
00891     res = DD_ONE(dd);
00892     cuddRef(res);
00893     for (j = size - 1; j >= 0; j--) { /* for each level bottom-up */
00894         i = (j >= dd->size) ? j : dd->invperm[j];
00895         if (support[i] == 1) {
00896             var = cuddUniqueInter(dd,i,dd->one,Cudd_Not(dd->one));
00897             cuddRef(var);
00898             tmp = Cudd_bddAnd(dd,res,var);
00899             if (tmp == NULL) {
00900                 Cudd_RecursiveDeref(dd,res);
00901                 Cudd_RecursiveDeref(dd,var);
00902                 FREE(support);
00903                 return(NULL);
00904             }
00905             cuddRef(tmp);
00906             Cudd_RecursiveDeref(dd,res);
00907             Cudd_RecursiveDeref(dd,var);
00908             res = tmp;
00909         }
00910     }
00911 
00912     FREE(support);
00913     cuddDeref(res);
00914     return(res);
00915 
00916 } /* end of Cudd_VectorSupport */
00917 
00918 
00932 int *
00933 Cudd_VectorSupportIndex(
00934   DdManager * dd /* manager */,
00935   DdNode ** F /* array of DDs whose support is sought */,
00936   int  n /* size of the array */)
00937 {
00938     int *support;
00939     int i;
00940     int size;
00941 
00942     /* Allocate and initialize support array for ddSupportStep. */
00943     size = ddMax(dd->size, dd->sizeZ);
00944     support = ALLOC(int,size);
00945     if (support == NULL) {
00946         dd->errorCode = CUDD_MEMORY_OUT;
00947         return(NULL);
00948     }
00949     for (i = 0; i < size; i++) {
00950         support[i] = 0;
00951     }
00952 
00953     /* Compute support and clean up markers. */
00954     for (i = 0; i < n; i++) {
00955         ddSupportStep(Cudd_Regular(F[i]),support);
00956     }
00957     for (i = 0; i < n; i++) {
00958         ddClearFlag(Cudd_Regular(F[i]));
00959     }
00960 
00961     return(support);
00962 
00963 } /* end of Cudd_VectorSupportIndex */
00964 
00965 
00980 int
00981 Cudd_VectorSupportSize(
00982   DdManager * dd /* manager */,
00983   DdNode ** F /* array of DDs whose support is sought */,
00984   int  n /* size of the array */)
00985 {
00986     int *support;
00987     int i;
00988     int size;
00989     int count;
00990 
00991     /* Allocate and initialize support array for ddSupportStep. */
00992     size = ddMax(dd->size, dd->sizeZ);
00993     support = ALLOC(int,size);
00994     if (support == NULL) {
00995         dd->errorCode = CUDD_MEMORY_OUT;
00996         return(CUDD_OUT_OF_MEM);
00997     }
00998     for (i = 0; i < size; i++) {
00999         support[i] = 0;
01000     }
01001 
01002     /* Compute support and clean up markers. */
01003     for (i = 0; i < n; i++) {
01004         ddSupportStep(Cudd_Regular(F[i]),support);
01005     }
01006     for (i = 0; i < n; i++) {
01007         ddClearFlag(Cudd_Regular(F[i]));
01008     }
01009 
01010     /* Count vriables in support. */
01011     count = 0;
01012     for (i = 0; i < size; i++) {
01013         if (support[i] == 1) count++;
01014     }
01015 
01016     FREE(support);
01017     return(count);
01018 
01019 } /* end of Cudd_VectorSupportSize */
01020 
01021 
01037 int
01038 Cudd_ClassifySupport(
01039   DdManager * dd /* manager */,
01040   DdNode * f /* first DD */,
01041   DdNode * g /* second DD */,
01042   DdNode ** common /* cube of shared variables */,
01043   DdNode ** onlyF /* cube of variables only in f */,
01044   DdNode ** onlyG /* cube of variables only in g */)
01045 {
01046     int *supportF, *supportG;
01047     DdNode *tmp, *var;
01048     int i,j;
01049     int size;
01050 
01051     /* Allocate and initialize support arrays for ddSupportStep. */
01052     size = ddMax(dd->size, dd->sizeZ);
01053     supportF = ALLOC(int,size);
01054     if (supportF == NULL) {
01055         dd->errorCode = CUDD_MEMORY_OUT;
01056         return(0);
01057     }
01058     supportG = ALLOC(int,size);
01059     if (supportG == NULL) {
01060         dd->errorCode = CUDD_MEMORY_OUT;
01061         FREE(supportF);
01062         return(0);
01063     }
01064     for (i = 0; i < size; i++) {
01065         supportF[i] = 0;
01066         supportG[i] = 0;
01067     }
01068 
01069     /* Compute supports and clean up markers. */
01070     ddSupportStep(Cudd_Regular(f),supportF);
01071     ddClearFlag(Cudd_Regular(f));
01072     ddSupportStep(Cudd_Regular(g),supportG);
01073     ddClearFlag(Cudd_Regular(g));
01074 
01075     /* Classify variables and create cubes. */
01076     *common = *onlyF = *onlyG = DD_ONE(dd);
01077     cuddRef(*common); cuddRef(*onlyF); cuddRef(*onlyG);
01078     for (j = size - 1; j >= 0; j--) { /* for each level bottom-up */
01079         i = (j >= dd->size) ? j : dd->invperm[j];
01080         if (supportF[i] == 0 && supportG[i] == 0) continue;
01081         var = cuddUniqueInter(dd,i,dd->one,Cudd_Not(dd->one));
01082         cuddRef(var);
01083         if (supportG[i] == 0) {
01084             tmp = Cudd_bddAnd(dd,*onlyF,var);
01085             if (tmp == NULL) {
01086                 Cudd_RecursiveDeref(dd,*common);
01087                 Cudd_RecursiveDeref(dd,*onlyF);
01088                 Cudd_RecursiveDeref(dd,*onlyG);
01089                 Cudd_RecursiveDeref(dd,var);
01090                 FREE(supportF); FREE(supportG);
01091                 return(0);
01092             }
01093             cuddRef(tmp);
01094             Cudd_RecursiveDeref(dd,*onlyF);
01095             *onlyF = tmp;
01096         } else if (supportF[i] == 0) {
01097             tmp = Cudd_bddAnd(dd,*onlyG,var);
01098             if (tmp == NULL) {
01099                 Cudd_RecursiveDeref(dd,*common);
01100                 Cudd_RecursiveDeref(dd,*onlyF);
01101                 Cudd_RecursiveDeref(dd,*onlyG);
01102                 Cudd_RecursiveDeref(dd,var);
01103                 FREE(supportF); FREE(supportG);
01104                 return(0);
01105             }
01106             cuddRef(tmp);
01107             Cudd_RecursiveDeref(dd,*onlyG);
01108             *onlyG = tmp;
01109         } else {
01110             tmp = Cudd_bddAnd(dd,*common,var);
01111             if (tmp == NULL) {
01112                 Cudd_RecursiveDeref(dd,*common);
01113                 Cudd_RecursiveDeref(dd,*onlyF);
01114                 Cudd_RecursiveDeref(dd,*onlyG);
01115                 Cudd_RecursiveDeref(dd,var);
01116                 FREE(supportF); FREE(supportG);
01117                 return(0);
01118             }
01119             cuddRef(tmp);
01120             Cudd_RecursiveDeref(dd,*common);
01121             *common = tmp;
01122         }
01123         Cudd_RecursiveDeref(dd,var);
01124     }
01125 
01126     FREE(supportF); FREE(supportG);
01127     cuddDeref(*common); cuddDeref(*onlyF); cuddDeref(*onlyG);
01128     return(1);
01129 
01130 } /* end of Cudd_ClassifySupport */
01131 
01132 
01146 int
01147 Cudd_CountLeaves(
01148   DdNode * node)
01149 {
01150     int i;      
01151 
01152     i = ddLeavesInt(Cudd_Regular(node));
01153     ddClearFlag(Cudd_Regular(node));
01154     return(i);
01155 
01156 } /* end of Cudd_CountLeaves */
01157 
01158 
01173 int
01174 Cudd_bddPickOneCube(
01175   DdManager * ddm,
01176   DdNode * node,
01177   char * string)
01178 {
01179     DdNode *N, *T, *E;
01180     DdNode *one, *bzero;
01181     char   dir;
01182     int    i;
01183 
01184     if (string == NULL || node == NULL) return(0);
01185 
01186     /* The constant 0 function has no on-set cubes. */
01187     one = DD_ONE(ddm);
01188     bzero = Cudd_Not(one);
01189     if (node == bzero) return(0);
01190 
01191     for (i = 0; i < ddm->size; i++) string[i] = 2;
01192 
01193     for (;;) {
01194 
01195         if (node == one) break;
01196 
01197         N = Cudd_Regular(node);
01198 
01199         T = cuddT(N); E = cuddE(N);
01200         if (Cudd_IsComplement(node)) {
01201             T = Cudd_Not(T); E = Cudd_Not(E);
01202         }
01203         if (T == bzero) {
01204             string[N->index] = 0;
01205             node = E;
01206         } else if (E == bzero) {
01207             string[N->index] = 1;
01208             node = T;
01209         } else {
01210             dir = (char) ((Cudd_Random() & 0x2000) >> 13);
01211             string[N->index] = dir;
01212             node = dir ? T : E;
01213         }
01214     }
01215     return(1);
01216 
01217 } /* end of Cudd_bddPickOneCube */
01218 
01219 
01243 DdNode *
01244 Cudd_bddPickOneMinterm(
01245   DdManager * dd /* manager */,
01246   DdNode * f /* function from which to pick one minterm */,
01247   DdNode ** vars /* array of variables */,
01248   int  n /* size of <code>vars</code> */)
01249 {
01250     char *string;
01251     int i, size;
01252     int *indices;
01253     int result;
01254     DdNode *old, *neW;
01255 
01256     size = dd->size;
01257     string = ALLOC(char, size);
01258     if (string == NULL) {
01259         dd->errorCode = CUDD_MEMORY_OUT;
01260         return(NULL);
01261     }
01262     indices = ALLOC(int,n);
01263     if (indices == NULL) {
01264         dd->errorCode = CUDD_MEMORY_OUT;
01265         FREE(string);
01266         return(NULL);
01267     }
01268 
01269     for (i = 0; i < n; i++) {
01270         indices[i] = vars[i]->index;
01271     }
01272 
01273     result = Cudd_bddPickOneCube(dd,f,string);
01274     if (result == 0) {
01275         FREE(string);
01276         FREE(indices);
01277         return(NULL);
01278     }
01279 
01280     /* Randomize choice for don't cares. */
01281     for (i = 0; i < n; i++) {
01282         if (string[indices[i]] == 2) 
01283             string[indices[i]] = (char) ((Cudd_Random() & 0x20) >> 5);
01284     }
01285 
01286     /* Build result BDD. */
01287     old = Cudd_ReadOne(dd);
01288     cuddRef(old);
01289 
01290     for (i = n-1; i >= 0; i--) {
01291         neW = Cudd_bddAnd(dd,old,Cudd_NotCond(vars[i],string[indices[i]]==0));
01292         if (neW == NULL) {
01293             FREE(string);
01294             FREE(indices);
01295             Cudd_RecursiveDeref(dd,old);
01296             return(NULL);
01297         }
01298         cuddRef(neW);
01299         Cudd_RecursiveDeref(dd,old);
01300         old = neW;
01301     }
01302 
01303 #ifdef DD_DEBUG
01304     /* Test. */
01305     if (Cudd_bddLeq(dd,old,f)) {
01306         cuddDeref(old);
01307     } else {
01308         Cudd_RecursiveDeref(dd,old);
01309         old = NULL;
01310     }
01311 #else
01312     cuddDeref(old);
01313 #endif
01314 
01315     FREE(string);
01316     FREE(indices);
01317     return(old);
01318 
01319 }  /* end of Cudd_bddPickOneMinterm */
01320 
01321 
01345 DdNode **
01346 Cudd_bddPickArbitraryMinterms(
01347   DdManager * dd /* manager */,
01348   DdNode * f /* function from which to pick k minterms */,
01349   DdNode ** vars /* array of variables */,
01350   int  n /* size of <code>vars</code> */,
01351   int  k /* number of minterms to find */)
01352 {
01353     char **string;
01354     int i, j, l, size;
01355     int *indices;
01356     int result;
01357     DdNode **old, *neW;
01358     double minterms;
01359     char *saveString;
01360     int saveFlag, savePoint, isSame;
01361 
01362     minterms = Cudd_CountMinterm(dd,f,n);
01363     if ((double)k > minterms) {
01364         return(NULL);
01365     }
01366 
01367     size = dd->size;
01368     string = ALLOC(char *, k);
01369     if (string == NULL) {
01370         dd->errorCode = CUDD_MEMORY_OUT;
01371         return(NULL);
01372     }
01373     for (i = 0; i < k; i++) {
01374         string[i] = ALLOC(char, size + 1);
01375         if (string[i] == NULL) {
01376             for (j = 0; j < i; j++)
01377                 FREE(string[i]);
01378             FREE(string);
01379             dd->errorCode = CUDD_MEMORY_OUT;
01380             return(NULL);
01381         }
01382         for (j = 0; j < size; j++) string[i][j] = '2';
01383         string[i][size] = '\0';
01384     }
01385     indices = ALLOC(int,n);
01386     if (indices == NULL) {
01387         dd->errorCode = CUDD_MEMORY_OUT;
01388         for (i = 0; i < k; i++)
01389             FREE(string[i]);
01390         FREE(string);
01391         return(NULL);
01392     }
01393 
01394     for (i = 0; i < n; i++) {
01395         indices[i] = vars[i]->index;
01396     }
01397 
01398     result = ddPickArbitraryMinterms(dd,f,n,k,string);
01399     if (result == 0) {
01400         for (i = 0; i < k; i++)
01401             FREE(string[i]);
01402         FREE(string);
01403         FREE(indices);
01404         return(NULL);
01405     }
01406 
01407     old = ALLOC(DdNode *, k);
01408     if (old == NULL) {
01409         dd->errorCode = CUDD_MEMORY_OUT;
01410         for (i = 0; i < k; i++)
01411             FREE(string[i]);
01412         FREE(string);
01413         FREE(indices);
01414         return(NULL);
01415     }
01416     saveString = ALLOC(char, size + 1);
01417     if (saveString == NULL) {
01418         dd->errorCode = CUDD_MEMORY_OUT;
01419         for (i = 0; i < k; i++)
01420             FREE(string[i]);
01421         FREE(string);
01422         FREE(indices);
01423         FREE(old);
01424         return(NULL);
01425     }
01426     saveFlag = 0;
01427 
01428     /* Build result BDD array. */
01429     for (i = 0; i < k; i++) {
01430         isSame = 0;
01431         if (!saveFlag) {
01432             for (j = i + 1; j < k; j++) {
01433                 if (strcmp(string[i], string[j]) == 0) {
01434                     savePoint = i;
01435                     strcpy(saveString, string[i]);
01436                     saveFlag = 1;
01437                     break;
01438                 }
01439             }
01440         } else {
01441             if (strcmp(string[i], saveString) == 0) {
01442                 isSame = 1;
01443             } else {
01444                 saveFlag = 0;
01445                 for (j = i + 1; j < k; j++) {
01446                     if (strcmp(string[i], string[j]) == 0) {
01447                         savePoint = i;
01448                         strcpy(saveString, string[i]);
01449                         saveFlag = 1;
01450                         break;
01451                     }
01452                 }
01453             }
01454         }
01455         /* Randomize choice for don't cares. */
01456         for (j = 0; j < n; j++) {
01457             if (string[i][indices[j]] == '2')
01458                 string[i][indices[j]] = (Cudd_Random() & 0x20) ? '1' : '0';
01459         }
01460 
01461         while (isSame) {
01462             isSame = 0;
01463             for (j = savePoint; j < i; j++) {
01464                 if (strcmp(string[i], string[j]) == 0) {
01465                     isSame = 1;
01466                     break;
01467                 }
01468             }
01469             if (isSame) {
01470                 strcpy(string[i], saveString);
01471                 /* Randomize choice for don't cares. */
01472                 for (j = 0; j < n; j++) {
01473                     if (string[i][indices[j]] == '2') 
01474                         string[i][indices[j]] = (Cudd_Random() & 0x20) ?
01475                             '1' : '0';
01476                 }
01477             }
01478         }
01479 
01480         old[i] = Cudd_ReadOne(dd);
01481         cuddRef(old[i]);
01482 
01483         for (j = 0; j < n; j++) {
01484             if (string[i][indices[j]] == '0') {
01485                 neW = Cudd_bddAnd(dd,old[i],Cudd_Not(vars[j]));
01486             } else {
01487                 neW = Cudd_bddAnd(dd,old[i],vars[j]);
01488             }
01489             if (neW == NULL) {
01490                 FREE(saveString);
01491                 for (l = 0; l < k; l++)
01492                     FREE(string[l]);
01493                 FREE(string);
01494                 FREE(indices);
01495                 for (l = 0; l <= i; l++)
01496                     Cudd_RecursiveDeref(dd,old[l]);
01497                 FREE(old);
01498                 return(NULL);
01499             }
01500             cuddRef(neW);
01501             Cudd_RecursiveDeref(dd,old[i]);
01502             old[i] = neW;
01503         }
01504 
01505         /* Test. */
01506         if (!Cudd_bddLeq(dd,old[i],f)) {
01507             FREE(saveString);
01508             for (l = 0; l < k; l++)
01509                 FREE(string[l]);
01510             FREE(string);
01511             FREE(indices);
01512             for (l = 0; l <= i; l++)
01513                 Cudd_RecursiveDeref(dd,old[l]);
01514             FREE(old);
01515             return(NULL);
01516         }
01517     }
01518 
01519     FREE(saveString);
01520     for (i = 0; i < k; i++) {
01521         cuddDeref(old[i]);
01522         FREE(string[i]);
01523     }
01524     FREE(string);
01525     FREE(indices);
01526     return(old);
01527 
01528 }  /* end of Cudd_bddPickArbitraryMinterms */
01529 
01530 
01553 DdNode *
01554 Cudd_SubsetWithMaskVars(
01555   DdManager * dd /* manager */,
01556   DdNode * f /* function from which to pick a cube */,
01557   DdNode ** vars /* array of variables */,
01558   int  nvars /* size of <code>vars</code> */,
01559   DdNode ** maskVars /* array of variables */,
01560   int  mvars /* size of <code>maskVars</code> */)
01561 {
01562     double      *weight;
01563     char        *string;
01564     int         i, size;
01565     int         *indices, *mask;
01566     int         result;
01567     DdNode      *zero, *cube, *newCube, *subset;
01568     DdNode      *cof;
01569 
01570     DdNode      *support;
01571     support = Cudd_Support(dd,f);
01572     cuddRef(support);
01573     Cudd_RecursiveDeref(dd,support);
01574 
01575     zero = Cudd_Not(dd->one);
01576     size = dd->size;
01577     
01578     weight = ALLOC(double,size);
01579     if (weight == NULL) {
01580         dd->errorCode = CUDD_MEMORY_OUT;
01581         return(NULL);
01582     }
01583     for (i = 0; i < size; i++) {
01584         weight[i] = 0.0;
01585     }
01586     for (i = 0; i < mvars; i++) {
01587         cof = Cudd_Cofactor(dd, f, maskVars[i]);
01588         cuddRef(cof);
01589         weight[i] = Cudd_CountMinterm(dd, cof, nvars);
01590         Cudd_RecursiveDeref(dd,cof);
01591 
01592         cof = Cudd_Cofactor(dd, f, Cudd_Not(maskVars[i]));
01593         cuddRef(cof);
01594         weight[i] -= Cudd_CountMinterm(dd, cof, nvars);
01595         Cudd_RecursiveDeref(dd,cof);
01596     }
01597 
01598     string = ALLOC(char, size + 1);
01599     if (string == NULL) {
01600         dd->errorCode = CUDD_MEMORY_OUT;
01601         return(NULL);
01602     }
01603     mask = ALLOC(int, size);
01604     if (mask == NULL) {
01605         dd->errorCode = CUDD_MEMORY_OUT;
01606         FREE(string);
01607         return(NULL);
01608     }
01609     for (i = 0; i < size; i++) {
01610         string[i] = '2';
01611         mask[i] = 0;
01612     }
01613     string[size] = '\0';
01614     indices = ALLOC(int,nvars);
01615     if (indices == NULL) {
01616         dd->errorCode = CUDD_MEMORY_OUT;
01617         FREE(string);
01618         FREE(mask);
01619         return(NULL);
01620     }
01621     for (i = 0; i < nvars; i++) {
01622         indices[i] = vars[i]->index;
01623     }
01624 
01625     result = ddPickRepresentativeCube(dd,f,nvars,weight,string);
01626     if (result == 0) {
01627         FREE(string);
01628         FREE(mask);
01629         FREE(indices);
01630         return(NULL);
01631     }
01632 
01633     cube = Cudd_ReadOne(dd);
01634     cuddRef(cube);
01635     zero = Cudd_Not(Cudd_ReadOne(dd));
01636     for (i = 0; i < nvars; i++) {
01637         if (string[indices[i]] == '0') {
01638             newCube = Cudd_bddIte(dd,cube,Cudd_Not(vars[i]),zero);
01639         } else if (string[indices[i]] == '1') {
01640             newCube = Cudd_bddIte(dd,cube,vars[i],zero);
01641         } else
01642             continue;
01643         if (newCube == NULL) {
01644             FREE(string);
01645             FREE(mask);
01646             FREE(indices);
01647             Cudd_RecursiveDeref(dd,cube);
01648             return(NULL);
01649         }
01650         cuddRef(newCube);
01651         Cudd_RecursiveDeref(dd,cube);
01652         cube = newCube;
01653     }
01654     Cudd_RecursiveDeref(dd,cube);
01655 
01656     for (i = 0; i < mvars; i++) {
01657         mask[maskVars[i]->index] = 1;
01658     }
01659     for (i = 0; i < nvars; i++) {
01660         if (mask[indices[i]]) {
01661             if (string[indices[i]] == '2') {
01662                 if (weight[indices[i]] >= 0.0)
01663                     string[indices[i]] = '1';
01664                 else
01665                     string[indices[i]] = '0';
01666             }
01667         } else {
01668             string[indices[i]] = '2';
01669         }
01670     }
01671 
01672     cube = Cudd_ReadOne(dd);
01673     cuddRef(cube);
01674     zero = Cudd_Not(Cudd_ReadOne(dd));
01675 
01676     /* Build result BDD. */
01677     for (i = 0; i < nvars; i++) {
01678         if (string[indices[i]] == '0') {
01679             newCube = Cudd_bddIte(dd,cube,Cudd_Not(vars[i]),zero);
01680         } else if (string[indices[i]] == '1') {
01681             newCube = Cudd_bddIte(dd,cube,vars[i],zero);
01682         } else
01683             continue;
01684         if (newCube == NULL) {
01685             FREE(string);
01686             FREE(mask);
01687             FREE(indices);
01688             Cudd_RecursiveDeref(dd,cube);
01689             return(NULL);
01690         }
01691         cuddRef(newCube);
01692         Cudd_RecursiveDeref(dd,cube);
01693         cube = newCube;
01694     }
01695 
01696     subset = Cudd_bddAnd(dd,f,cube);
01697     cuddRef(subset);
01698     Cudd_RecursiveDeref(dd,cube);
01699 
01700     /* Test. */
01701     if (Cudd_bddLeq(dd,subset,f)) {
01702         cuddDeref(subset);
01703     } else {
01704         Cudd_RecursiveDeref(dd,subset);
01705         subset = NULL;
01706     }
01707 
01708     FREE(string);
01709     FREE(mask);
01710     FREE(indices);
01711     FREE(weight);
01712     return(subset);
01713 
01714 } /* end of Cudd_SubsetWithMaskVars */
01715 
01716 
01743 DdGen *
01744 Cudd_FirstCube(
01745   DdManager * dd,
01746   DdNode * f,
01747   int ** cube,
01748   CUDD_VALUE_TYPE * value)
01749 {
01750     DdGen *gen;
01751     DdNode *top, *treg, *next, *nreg, *prev, *preg;
01752     int i;
01753     int nvars;
01754 
01755     /* Sanity Check. */
01756     if (dd == NULL || f == NULL) return(NULL);
01757 
01758     /* Allocate generator an initialize it. */
01759     gen = ALLOC(DdGen,1);
01760     if (gen == NULL) {
01761         dd->errorCode = CUDD_MEMORY_OUT;
01762         return(NULL);
01763     }
01764 
01765     gen->manager = dd;
01766     gen->type = CUDD_GEN_CUBES;
01767     gen->status = CUDD_GEN_EMPTY;
01768     gen->gen.cubes.cube = NULL;
01769     gen->gen.cubes.value = DD_ZERO_VAL;
01770     gen->stack.sp = 0;
01771     gen->stack.stack = NULL;
01772     gen->node = NULL;
01773 
01774     nvars = dd->size;
01775     gen->gen.cubes.cube = ALLOC(int,nvars);
01776     if (gen->gen.cubes.cube == NULL) {
01777         dd->errorCode = CUDD_MEMORY_OUT;
01778         FREE(gen);
01779         return(NULL);
01780     }
01781     for (i = 0; i < nvars; i++) gen->gen.cubes.cube[i] = 2;
01782 
01783     /* The maximum stack depth is one plus the number of variables.
01784     ** because a path may have nodes at all levels, including the
01785     ** constant level.
01786     */
01787     gen->stack.stack = ALLOC(DdNode *, nvars+1);
01788     if (gen->stack.stack == NULL) {
01789         dd->errorCode = CUDD_MEMORY_OUT;
01790         FREE(gen->gen.cubes.cube);
01791         FREE(gen);
01792         return(NULL);
01793     }
01794     for (i = 0; i <= nvars; i++) gen->stack.stack[i] = NULL;
01795 
01796     /* Find the first cube of the onset. */
01797     gen->stack.stack[gen->stack.sp] = f; gen->stack.sp++;
01798 
01799     while (1) {
01800         top = gen->stack.stack[gen->stack.sp-1];
01801         treg = Cudd_Regular(top);
01802         if (!cuddIsConstant(treg)) {
01803             /* Take the else branch first. */
01804             gen->gen.cubes.cube[treg->index] = 0;
01805             next = cuddE(treg);
01806             if (top != treg) next = Cudd_Not(next);
01807             gen->stack.stack[gen->stack.sp] = next; gen->stack.sp++;
01808         } else if (top == Cudd_Not(DD_ONE(dd)) || top == dd->background) {
01809             /* Backtrack */
01810             while (1) {
01811                 if (gen->stack.sp == 1) {
01812                     /* The current node has no predecessor. */
01813                     gen->status = CUDD_GEN_EMPTY;
01814                     gen->stack.sp--;
01815                     goto done;
01816                 }
01817                 prev = gen->stack.stack[gen->stack.sp-2];
01818                 preg = Cudd_Regular(prev);
01819                 nreg = cuddT(preg);
01820                 if (prev != preg) {next = Cudd_Not(nreg);} else {next = nreg;}
01821                 if (next != top) { /* follow the then branch next */
01822                     gen->gen.cubes.cube[preg->index] = 1;
01823                     gen->stack.stack[gen->stack.sp-1] = next;
01824                     break;
01825                 }
01826                 /* Pop the stack and try again. */
01827                 gen->gen.cubes.cube[preg->index] = 2;
01828                 gen->stack.sp--;
01829                 top = gen->stack.stack[gen->stack.sp-1];
01830                 treg = Cudd_Regular(top);
01831             }
01832         } else {
01833             gen->status = CUDD_GEN_NONEMPTY;
01834             gen->gen.cubes.value = cuddV(top);
01835             goto done;
01836         }
01837     }
01838 
01839 done:
01840     *cube = gen->gen.cubes.cube;
01841     *value = gen->gen.cubes.value;
01842     return(gen);
01843 
01844 } /* end of Cudd_FirstCube */
01845 
01846 
01862 int
01863 Cudd_NextCube(
01864   DdGen * gen,
01865   int ** cube,
01866   CUDD_VALUE_TYPE * value)
01867 {
01868     DdNode *top, *treg, *next, *nreg, *prev, *preg;
01869     DdManager *dd = gen->manager;
01870 
01871     /* Backtrack from previously reached terminal node. */
01872     while (1) {
01873         if (gen->stack.sp == 1) {
01874             /* The current node has no predecessor. */
01875             gen->status = CUDD_GEN_EMPTY;
01876             gen->stack.sp--;
01877             goto done;
01878         }
01879         top = gen->stack.stack[gen->stack.sp-1];
01880         treg = Cudd_Regular(top);
01881         prev = gen->stack.stack[gen->stack.sp-2];
01882         preg = Cudd_Regular(prev);
01883         nreg = cuddT(preg);
01884         if (prev != preg) {next = Cudd_Not(nreg);} else {next = nreg;}
01885         if (next != top) { /* follow the then branch next */
01886             gen->gen.cubes.cube[preg->index] = 1;
01887             gen->stack.stack[gen->stack.sp-1] = next;
01888             break;
01889         }
01890         /* Pop the stack and try again. */
01891         gen->gen.cubes.cube[preg->index] = 2;
01892         gen->stack.sp--;
01893     }
01894 
01895     while (1) {
01896         top = gen->stack.stack[gen->stack.sp-1];
01897         treg = Cudd_Regular(top);
01898         if (!cuddIsConstant(treg)) {
01899             /* Take the else branch first. */
01900             gen->gen.cubes.cube[treg->index] = 0;
01901             next = cuddE(treg);
01902             if (top != treg) next = Cudd_Not(next);
01903             gen->stack.stack[gen->stack.sp] = next; gen->stack.sp++;
01904         } else if (top == Cudd_Not(DD_ONE(dd)) || top == dd->background) {
01905             /* Backtrack */
01906             while (1) {
01907                 if (gen->stack.sp == 1) {
01908                     /* The current node has no predecessor. */
01909                     gen->status = CUDD_GEN_EMPTY;
01910                     gen->stack.sp--;
01911                     goto done;
01912                 }
01913                 prev = gen->stack.stack[gen->stack.sp-2];
01914                 preg = Cudd_Regular(prev);
01915                 nreg = cuddT(preg);
01916                 if (prev != preg) {next = Cudd_Not(nreg);} else {next = nreg;}
01917                 if (next != top) { /* follow the then branch next */
01918                     gen->gen.cubes.cube[preg->index] = 1;
01919                     gen->stack.stack[gen->stack.sp-1] = next;
01920                     break;
01921                 }
01922                 /* Pop the stack and try again. */
01923                 gen->gen.cubes.cube[preg->index] = 2;
01924                 gen->stack.sp--;
01925                 top = gen->stack.stack[gen->stack.sp-1];
01926                 treg = Cudd_Regular(top);
01927             }
01928         } else {
01929             gen->status = CUDD_GEN_NONEMPTY;
01930             gen->gen.cubes.value = cuddV(top);
01931             goto done;
01932         }
01933     }
01934 
01935 done:
01936     if (gen->status == CUDD_GEN_EMPTY) return(0);
01937     *cube = gen->gen.cubes.cube;
01938     *value = gen->gen.cubes.value;
01939     return(1);
01940 
01941 } /* end of Cudd_NextCube */
01942 
01943 
01959 DdNode *
01960 Cudd_bddComputeCube(
01961   DdManager * dd,
01962   DdNode ** vars,
01963   int * phase,
01964   int  n)
01965 {
01966     DdNode      *cube;
01967     DdNode      *fn;
01968     int         i;
01969 
01970     cube = DD_ONE(dd);
01971     cuddRef(cube);
01972 
01973     for (i = n - 1; i >= 0; i--) {
01974         if (phase == NULL || phase[i] != 0) {
01975             fn = Cudd_bddAnd(dd,vars[i],cube);
01976         } else {
01977             fn = Cudd_bddAnd(dd,Cudd_Not(vars[i]),cube);
01978         }
01979         if (fn == NULL) {
01980             Cudd_RecursiveDeref(dd,cube);
01981             return(NULL);
01982         }
01983         cuddRef(fn);
01984         Cudd_RecursiveDeref(dd,cube);
01985         cube = fn;
01986     }
01987     cuddDeref(cube);
01988 
01989     return(cube);
01990 
01991 }  /* end of Cudd_bddComputeCube */
01992 
01993 
02009 DdNode *
02010 Cudd_addComputeCube(
02011   DdManager * dd,
02012   DdNode ** vars,
02013   int * phase,
02014   int  n)
02015 {
02016     DdNode      *cube, *zero;
02017     DdNode      *fn;
02018     int         i;
02019 
02020     cube = DD_ONE(dd);
02021     cuddRef(cube);
02022     zero = DD_ZERO(dd);
02023 
02024     for (i = n - 1; i >= 0; i--) {
02025         if (phase == NULL || phase[i] != 0) {
02026             fn = Cudd_addIte(dd,vars[i],cube,zero);
02027         } else {
02028             fn = Cudd_addIte(dd,vars[i],zero,cube);
02029         }
02030         if (fn == NULL) {
02031             Cudd_RecursiveDeref(dd,cube);
02032             return(NULL);
02033         }
02034         cuddRef(fn);
02035         Cudd_RecursiveDeref(dd,cube);
02036         cube = fn;
02037     }
02038     cuddDeref(cube);
02039 
02040     return(cube);
02041 
02042 } /* end of Cudd_addComputeCube */
02043 
02044 
02061 DdNode *
02062 Cudd_CubeArrayToBdd(
02063   DdManager *dd,
02064   int *array)
02065 {
02066     DdNode *cube, *var, *tmp;
02067     int i;
02068     int size = Cudd_ReadSize(dd);
02069 
02070     cube = DD_ONE(dd);
02071     cuddRef(cube);
02072     for (i = size - 1; i >= 0; i--) {
02073         if ((array[i] & ~1) == 0) {
02074             var = Cudd_bddIthVar(dd,i);
02075             tmp = Cudd_bddAnd(dd,cube,Cudd_NotCond(var,array[i]==0));
02076             if (tmp == NULL) {
02077                 Cudd_RecursiveDeref(dd,cube);
02078                 return(NULL);
02079             }
02080             cuddRef(tmp);
02081             Cudd_RecursiveDeref(dd,cube);
02082             cube = tmp;
02083         }
02084     }
02085     cuddDeref(cube);
02086     return(cube);
02087 
02088 } /* end of Cudd_CubeArrayToBdd */
02089 
02090 
02109 int
02110 Cudd_BddToCubeArray(
02111   DdManager *dd,
02112   DdNode *cube,
02113   int *array)
02114 {
02115     DdNode *scan, *t, *e;
02116     int i;
02117     int size = Cudd_ReadSize(dd);
02118     DdNode *zero = Cudd_Not(DD_ONE(dd));
02119 
02120     for (i = size-1; i >= 0; i--) {
02121         array[i] = 2;
02122     }
02123     scan = cube;
02124     while (!Cudd_IsConstant(scan)) {
02125         int index = Cudd_Regular(scan)->index;
02126         cuddGetBranches(scan,&t,&e);
02127         if (t == zero) {
02128             array[index] = 0;
02129             scan = e;
02130         } else if (e == zero) {
02131             array[index] = 1;
02132             scan = t;
02133         } else {
02134             return(0);  /* cube is not a cube */
02135         }
02136     }
02137     if (scan == zero) {
02138         return(0);
02139     } else {
02140         return(1);
02141     }
02142 
02143 } /* end of Cudd_BddToCubeArray */
02144 
02145 
02161 DdGen *
02162 Cudd_FirstNode(
02163   DdManager * dd,
02164   DdNode * f,
02165   DdNode ** node)
02166 {
02167     DdGen *gen;
02168     int retval;
02169 
02170     /* Sanity Check. */
02171     if (dd == NULL || f == NULL) return(NULL);
02172 
02173     /* Allocate generator an initialize it. */
02174     gen = ALLOC(DdGen,1);
02175     if (gen == NULL) {
02176         dd->errorCode = CUDD_MEMORY_OUT;
02177         return(NULL);
02178     }
02179 
02180     gen->manager = dd;
02181     gen->type = CUDD_GEN_NODES;
02182     gen->status = CUDD_GEN_EMPTY;
02183     gen->gen.nodes.visited = NULL;
02184     gen->gen.nodes.stGen = NULL;
02185     gen->stack.sp = 0;
02186     gen->stack.stack = NULL;
02187     gen->node = NULL;
02188 
02189     gen->gen.nodes.visited = st_init_table(st_ptrcmp,st_ptrhash);
02190     if (gen->gen.nodes.visited == NULL) {
02191         FREE(gen);
02192         return(NULL);
02193     }
02194 
02195     /* Collect all the nodes in a st table for later perusal. */
02196     retval = cuddCollectNodes(Cudd_Regular(f),gen->gen.nodes.visited);
02197     if (retval == 0) {
02198         st_free_table(gen->gen.nodes.visited);
02199         FREE(gen);
02200         return(NULL);
02201     }
02202 
02203     /* Initialize the st table generator. */
02204     gen->gen.nodes.stGen = st_init_gen(gen->gen.nodes.visited);
02205     if (gen->gen.nodes.stGen == NULL) {
02206         st_free_table(gen->gen.nodes.visited);
02207         FREE(gen);
02208         return(NULL);
02209     }
02210 
02211     /* Find the first node. */
02212     retval = st_gen(gen->gen.nodes.stGen, (char **) &(gen->node), NULL);
02213     if (retval != 0) {
02214         gen->status = CUDD_GEN_NONEMPTY;
02215         *node = gen->node;
02216     }
02217 
02218     return(gen);
02219 
02220 } /* end of Cudd_FirstNode */
02221 
02222 
02236 int
02237 Cudd_NextNode(
02238   DdGen * gen,
02239   DdNode ** node)
02240 {
02241     int retval;
02242 
02243     /* Find the next node. */
02244     retval = st_gen(gen->gen.nodes.stGen, (char **) &(gen->node), NULL);
02245     if (retval == 0) {
02246         gen->status = CUDD_GEN_EMPTY;
02247     } else {
02248         *node = gen->node;
02249     }
02250 
02251     return(retval);
02252 
02253 } /* end of Cudd_NextNode */
02254 
02255 
02269 int
02270 Cudd_GenFree(
02271   DdGen * gen)
02272 {
02273 
02274     if (gen == NULL) return(0);
02275     switch (gen->type) {
02276     case CUDD_GEN_CUBES:
02277     case CUDD_GEN_ZDD_PATHS:
02278         FREE(gen->gen.cubes.cube);
02279         FREE(gen->stack.stack);
02280         break;
02281     case CUDD_GEN_NODES:
02282         st_free_gen(gen->gen.nodes.stGen);
02283         st_free_table(gen->gen.nodes.visited);
02284         break;
02285     default:
02286         return(0);
02287     }
02288     FREE(gen);
02289     return(0);
02290 
02291 } /* end of Cudd_GenFree */
02292 
02293 
02307 int
02308 Cudd_IsGenEmpty(
02309   DdGen * gen)
02310 {
02311     if (gen == NULL) return(1);
02312     return(gen->status == CUDD_GEN_EMPTY);
02313 
02314 } /* end of Cudd_IsGenEmpty */
02315 
02316 
02329 DdNode *
02330 Cudd_IndicesToCube(
02331   DdManager * dd,
02332   int * array,
02333   int  n)
02334 {
02335     DdNode *cube, *tmp;
02336     int i;
02337 
02338     cube = DD_ONE(dd);
02339     cuddRef(cube);
02340     for (i = n - 1; i >= 0; i--) {
02341         tmp = Cudd_bddAnd(dd,Cudd_bddIthVar(dd,array[i]),cube);
02342         if (tmp == NULL) {
02343             Cudd_RecursiveDeref(dd,cube);
02344             return(NULL);
02345         }
02346         cuddRef(tmp);
02347         Cudd_RecursiveDeref(dd,cube);
02348         cube = tmp;
02349     }
02350 
02351     cuddDeref(cube);
02352     return(cube);
02353 
02354 } /* end of Cudd_IndicesToCube */
02355 
02356 
02368 void
02369 Cudd_PrintVersion(
02370   FILE * fp)
02371 {
02372     (void) fprintf(fp, "%s\n", CUDD_VERSION);
02373 
02374 } /* end of Cudd_PrintVersion */
02375 
02376 
02390 double
02391 Cudd_AverageDistance(
02392   DdManager * dd)
02393 {
02394     double tetotal, nexttotal;
02395     double tesubtotal, nextsubtotal;
02396     double temeasured, nextmeasured;
02397     int i, j;
02398     int slots, nvars;
02399     long diff;
02400     DdNode *scan;
02401     DdNodePtr *nodelist;
02402     DdNode *sentinel = &(dd->sentinel);
02403 
02404     nvars = dd->size;
02405     if (nvars == 0) return(0.0);
02406 
02407     /* Initialize totals. */
02408     tetotal = 0.0;
02409     nexttotal = 0.0;
02410     temeasured = 0.0;
02411     nextmeasured = 0.0;
02412 
02413     /* Scan the variable subtables. */
02414     for (i = 0; i < nvars; i++) {
02415         nodelist = dd->subtables[i].nodelist;
02416         tesubtotal = 0.0;
02417         nextsubtotal = 0.0;
02418         slots = dd->subtables[i].slots;
02419         for (j = 0; j < slots; j++) {
02420             scan = nodelist[j];
02421             while (scan != sentinel) {
02422                 diff = (long) scan - (long) cuddT(scan);
02423                 tesubtotal += (double) ddAbs(diff);
02424                 diff = (long) scan - (long) Cudd_Regular(cuddE(scan));
02425                 tesubtotal += (double) ddAbs(diff);
02426                 temeasured += 2.0;
02427                 if (scan->next != NULL) {
02428                     diff = (long) scan - (long) scan->next;
02429                     nextsubtotal += (double) ddAbs(diff);
02430                     nextmeasured += 1.0;
02431                 }
02432                 scan = scan->next;
02433             }
02434         }
02435         tetotal += tesubtotal;
02436         nexttotal += nextsubtotal;
02437     }
02438 
02439     /* Scan the constant table. */
02440     nodelist = dd->constants.nodelist;
02441     nextsubtotal = 0.0;
02442     slots = dd->constants.slots;
02443     for (j = 0; j < slots; j++) {
02444         scan = nodelist[j];
02445         while (scan != NULL) {
02446             if (scan->next != NULL) {
02447                 diff = (long) scan - (long) scan->next;
02448                 nextsubtotal += (double) ddAbs(diff);
02449                 nextmeasured += 1.0;
02450             }
02451             scan = scan->next;
02452         }
02453     }
02454     nexttotal += nextsubtotal;
02455 
02456     return((tetotal + nexttotal) / (temeasured + nextmeasured));
02457 
02458 } /* end of Cudd_AverageDistance */
02459 
02460 
02478 long
02479 Cudd_Random(
02480    )
02481 {
02482     int i;      /* index in the shuffle table */
02483     long int w; /* work variable */
02484 
02485     /* cuddRand == 0 if the geneartor has not been initialized yet. */
02486     if (cuddRand == 0) Cudd_Srandom(1);
02487 
02488     /* Compute cuddRand = (cuddRand * LEQA1) % MODULUS1 avoiding
02489     ** overflows by Schrage's method.
02490     */
02491     w          = cuddRand / LEQQ1;
02492     cuddRand   = LEQA1 * (cuddRand - w * LEQQ1) - w * LEQR1;
02493     cuddRand  += (cuddRand < 0) * MODULUS1;
02494 
02495     /* Compute cuddRand2 = (cuddRand2 * LEQA2) % MODULUS2 avoiding
02496     ** overflows by Schrage's method.
02497     */
02498     w          = cuddRand2 / LEQQ2;
02499     cuddRand2  = LEQA2 * (cuddRand2 - w * LEQQ2) - w * LEQR2;
02500     cuddRand2 += (cuddRand2 < 0) * MODULUS2;
02501 
02502     /* cuddRand is shuffled with the Bays-Durham algorithm.
02503     ** shuffleSelect and cuddRand2 are combined to generate the output.
02504     */
02505 
02506     /* Pick one element from the shuffle table; "i" will be in the range
02507     ** from 0 to STAB_SIZE-1.
02508     */
02509     i = (int) (shuffleSelect / STAB_DIV);
02510     /* Mix the element of the shuffle table with the current iterate of
02511     ** the second sub-generator, and replace the chosen element of the
02512     ** shuffle table with the current iterate of the first sub-generator.
02513     */
02514     shuffleSelect   = shuffleTable[i] - cuddRand2;
02515     shuffleTable[i] = cuddRand;
02516     shuffleSelect  += (shuffleSelect < 1) * (MODULUS1 - 1);
02517     /* Since shuffleSelect != 0, and we want to be able to return 0,
02518     ** here we subtract 1 before returning.
02519     */
02520     return(shuffleSelect - 1);
02521 
02522 } /* end of Cudd_Random */
02523 
02524 
02541 void
02542 Cudd_Srandom(
02543   long  seed)
02544 {
02545     int i;
02546 
02547     if (seed < 0)       cuddRand = -seed;
02548     else if (seed == 0) cuddRand = 1;
02549     else                cuddRand = seed;
02550     cuddRand2 = cuddRand;
02551     /* Load the shuffle table (after 11 warm-ups). */
02552     for (i = 0; i < STAB_SIZE + 11; i++) {
02553         long int w;
02554         w = cuddRand / LEQQ1;
02555         cuddRand = LEQA1 * (cuddRand - w * LEQQ1) - w * LEQR1;
02556         cuddRand += (cuddRand < 0) * MODULUS1;
02557         shuffleTable[i % STAB_SIZE] = cuddRand;
02558     }
02559     shuffleSelect = shuffleTable[1 % STAB_SIZE];
02560 
02561 } /* end of Cudd_Srandom */
02562 
02563 
02579 double
02580 Cudd_Density(
02581   DdManager * dd /* manager */,
02582   DdNode * f /* function whose density is sought */,
02583   int  nvars /* size of the support of f */)
02584 {
02585     double minterms;
02586     int nodes;
02587     double density;
02588 
02589     if (nvars == 0) nvars = dd->size;
02590     minterms = Cudd_CountMinterm(dd,f,nvars);
02591     if (minterms == (double) CUDD_OUT_OF_MEM) return(minterms);
02592     nodes = Cudd_DagSize(f);
02593     density = minterms / (double) nodes;
02594     return(density);
02595 
02596 } /* end of Cudd_Density */
02597 
02598 
02614 void
02615 Cudd_OutOfMem(
02616   long size /* size of the allocation that failed */)
02617 {
02618     (void) fflush(stdout);
02619     (void) fprintf(stderr, "\nunable to allocate %ld bytes\n", size);
02620     return;
02621 
02622 } /* end of Cudd_OutOfMem */
02623 
02624 
02625 /*---------------------------------------------------------------------------*/
02626 /* Definition of internal functions                                          */
02627 /*---------------------------------------------------------------------------*/
02628 
02629 
02643 int
02644 cuddP(
02645   DdManager * dd,
02646   DdNode * f)
02647 {
02648     int retval;
02649     st_table *table = st_init_table(st_ptrcmp,st_ptrhash);
02650 
02651     if (table == NULL) return(0);
02652 
02653     retval = dp2(dd,f,table);
02654     st_free_table(table);
02655     (void) fputc('\n',dd->out);
02656     return(retval);
02657 
02658 } /* end of cuddP */
02659 
02660 
02672 enum st_retval
02673 cuddStCountfree(
02674   char * key,
02675   char * value,
02676   char * arg)
02677 {
02678     double      *d;
02679 
02680     d = (double *)value;
02681     FREE(d);
02682     return(ST_CONTINUE);
02683 
02684 } /* end of cuddStCountfree */
02685 
02686 
02702 int
02703 cuddCollectNodes(
02704   DdNode * f,
02705   st_table * visited)
02706 {
02707     DdNode      *T, *E;
02708     int         retval;
02709 
02710 #ifdef DD_DEBUG
02711     assert(!Cudd_IsComplement(f));
02712 #endif
02713 
02714     /* If already visited, nothing to do. */
02715     if (st_is_member(visited, (char *) f) == 1)
02716         return(1);
02717 
02718     /* Check for abnormal condition that should never happen. */
02719     if (f == NULL)
02720         return(0);
02721 
02722     /* Mark node as visited. */
02723     if (st_add_direct(visited, (char *) f, NULL) == ST_OUT_OF_MEM)
02724         return(0);
02725 
02726     /* Check terminal case. */
02727     if (cuddIsConstant(f))
02728         return(1);
02729 
02730     /* Recursive calls. */
02731     T = cuddT(f);
02732     retval = cuddCollectNodes(T,visited);
02733     if (retval != 1) return(retval);
02734     E = Cudd_Regular(cuddE(f));
02735     retval = cuddCollectNodes(E,visited);
02736     return(retval);
02737 
02738 } /* end of cuddCollectNodes */
02739 
02740 
02741 /*---------------------------------------------------------------------------*/
02742 /* Definition of static functions                                            */
02743 /*---------------------------------------------------------------------------*/
02744 
02745 
02756 static int
02757 dp2(
02758   DdManager *dd,
02759   DdNode * f,
02760   st_table * t)
02761 {
02762     DdNode *g, *n, *N;
02763     int T,E;
02764     
02765     if (f == NULL) {
02766         return(0);
02767     }
02768     g = Cudd_Regular(f);
02769     if (cuddIsConstant(g)) {
02770 #if SIZEOF_VOID_P == 8
02771         (void) fprintf(dd->out,"ID = %c0x%lx\tvalue = %-9g\n", bang(f),
02772                 (unsigned long) g / (unsigned long) sizeof(DdNode),cuddV(g));
02773 #else
02774         (void) fprintf(dd->out,"ID = %c0x%x\tvalue = %-9g\n", bang(f),
02775                 (unsigned) g / (unsigned) sizeof(DdNode),cuddV(g));
02776 #endif
02777         return(1);
02778     }
02779     if (st_is_member(t,(char *) g) == 1) {
02780         return(1);
02781     }
02782     if (st_add_direct(t,(char *) g,NULL) == ST_OUT_OF_MEM)
02783         return(0);
02784 #ifdef DD_STATS
02785 #if SIZEOF_VOID_P == 8
02786     (void) fprintf(dd->out,"ID = %c0x%lx\tindex = %d\tr = %d\t", bang(f),
02787                 (unsigned long) g / (unsigned long) sizeof(DdNode), g->index, g->ref);
02788 #else
02789     (void) fprintf(dd->out,"ID = %c0x%x\tindex = %d\tr = %d\t", bang(f),
02790                 (unsigned) g / (unsigned) sizeof(DdNode),g->index,g->ref);
02791 #endif
02792 #else
02793 #if SIZEOF_VOID_P == 8
02794     (void) fprintf(dd->out,"ID = %c0x%lx\tindex = %d\t", bang(f),
02795                 (unsigned long) g / (unsigned long) sizeof(DdNode),g->index);
02796 #else
02797     (void) fprintf(dd->out,"ID = %c0x%x\tindex = %d\t", bang(f),
02798                 (unsigned) g / (unsigned) sizeof(DdNode),g->index);
02799 #endif
02800 #endif
02801     n = cuddT(g);
02802     if (cuddIsConstant(n)) {
02803         (void) fprintf(dd->out,"T = %-9g\t",cuddV(n));
02804         T = 1;
02805     } else {
02806 #if SIZEOF_VOID_P == 8
02807         (void) fprintf(dd->out,"T = 0x%lx\t",(unsigned long) n / (unsigned long) sizeof(DdNode));
02808 #else
02809         (void) fprintf(dd->out,"T = 0x%x\t",(unsigned) n / (unsigned) sizeof(DdNode));
02810 #endif
02811         T = 0;
02812     }
02813 
02814     n = cuddE(g);
02815     N = Cudd_Regular(n);
02816     if (cuddIsConstant(N)) {
02817         (void) fprintf(dd->out,"E = %c%-9g\n",bang(n),cuddV(N));
02818         E = 1;
02819     } else {
02820 #if SIZEOF_VOID_P == 8
02821         (void) fprintf(dd->out,"E = %c0x%lx\n", bang(n), (unsigned long) N/(unsigned long) sizeof(DdNode));
02822 #else
02823         (void) fprintf(dd->out,"E = %c0x%x\n", bang(n), (unsigned) N/(unsigned) sizeof(DdNode));
02824 #endif
02825         E = 0;
02826     }
02827     if (E == 0) {
02828         if (dp2(dd,N,t) == 0)
02829             return(0);
02830     }
02831     if (T == 0) {
02832         if (dp2(dd,cuddT(g),t) == 0)
02833             return(0);
02834     }
02835     return(1);
02836 
02837 } /* end of dp2 */
02838 
02839 
02849 static void
02850 ddPrintMintermAux(
02851   DdManager * dd /* manager */,
02852   DdNode * node /* current node */,
02853   int * list /* current recursion path */)
02854 {
02855     DdNode      *N,*Nv,*Nnv;
02856     int         i,v,index;
02857 
02858     N = Cudd_Regular(node);
02859 
02860     if (cuddIsConstant(N)) {
02861         /* Terminal case: Print one cube based on the current recursion
02862         ** path, unless we have reached the background value (ADDs) or
02863         ** the logical zero (BDDs).
02864         */
02865         if (node != background && node != zero) {
02866             for (i = 0; i < dd->size; i++) {
02867                 v = list[i];
02868                 if (v == 0) (void) fprintf(dd->out,"0");
02869                 else if (v == 1) (void) fprintf(dd->out,"1");
02870                 else (void) fprintf(dd->out,"-");
02871             }
02872             (void) fprintf(dd->out," % g\n", cuddV(node));
02873         }
02874     } else {
02875         Nv  = cuddT(N);
02876         Nnv = cuddE(N);
02877         if (Cudd_IsComplement(node)) {
02878             Nv  = Cudd_Not(Nv);
02879             Nnv = Cudd_Not(Nnv);
02880         }
02881         index = N->index;
02882         list[index] = 0;
02883         ddPrintMintermAux(dd,Nnv,list); 
02884         list[index] = 1;
02885         ddPrintMintermAux(dd,Nv,list);
02886         list[index] = 2;
02887     }
02888     return;
02889 
02890 } /* end of ddPrintMintermAux */
02891 
02892 
02903 static int
02904 ddDagInt(
02905   DdNode * n)
02906 {
02907     int tval, eval;
02908 
02909     if (Cudd_IsComplement(n->next)) {
02910         return(0);
02911     }
02912     n->next = Cudd_Not(n->next);
02913     if (cuddIsConstant(n)) {
02914         return(1);
02915     }
02916     tval = ddDagInt(cuddT(n));
02917     eval = ddDagInt(Cudd_Regular(cuddE(n)));
02918     return(1 + tval + eval);
02919 
02920 } /* end of ddDagInt */
02921 
02922 
02938 static int
02939 cuddEstimateCofactor(
02940   DdManager *dd,
02941   st_table *table,
02942   DdNode * node,
02943   int i,
02944   int phase,
02945   DdNode ** ptr)
02946 {
02947     int tval, eval, val;
02948     DdNode *ptrT, *ptrE;
02949 
02950     if (Cudd_IsComplement(node->next)) {
02951         if (!st_lookup(table,(char *)node,(char **)ptr)) {
02952             st_add_direct(table,(char *)node,(char *)node);
02953             *ptr = node;
02954         }
02955         return(0);
02956     }
02957     node->next = Cudd_Not(node->next);
02958     if (cuddIsConstant(node)) {
02959         *ptr = node;
02960         if (st_add_direct(table,(char *)node,(char *)node) == ST_OUT_OF_MEM)
02961             return(CUDD_OUT_OF_MEM);
02962         return(1);
02963     }
02964     if ((int) node->index == i) {
02965         if (phase == 1) {
02966             *ptr = cuddT(node);
02967             val = ddDagInt(cuddT(node));
02968         } else {
02969             *ptr = cuddE(node);
02970             val = ddDagInt(Cudd_Regular(cuddE(node)));
02971         }
02972         if (node->ref > 1) {
02973             if (st_add_direct(table,(char *)node,(char *)*ptr) ==
02974                 ST_OUT_OF_MEM)
02975                 return(CUDD_OUT_OF_MEM);
02976         }
02977         return(val);
02978     }
02979     if (dd->perm[node->index] > dd->perm[i]) {
02980         *ptr = node;
02981         tval = ddDagInt(cuddT(node));
02982         eval = ddDagInt(Cudd_Regular(cuddE(node)));
02983         if (node->ref > 1) {
02984             if (st_add_direct(table,(char *)node,(char *)node) ==
02985                 ST_OUT_OF_MEM)
02986                 return(CUDD_OUT_OF_MEM);
02987         }
02988         val = 1 + tval + eval;
02989         return(val);
02990     }
02991     tval = cuddEstimateCofactor(dd,table,cuddT(node),i,phase,&ptrT);
02992     eval = cuddEstimateCofactor(dd,table,Cudd_Regular(cuddE(node)),i,
02993                                 phase,&ptrE);
02994     ptrE = Cudd_NotCond(ptrE,Cudd_IsComplement(cuddE(node)));
02995     if (ptrT == ptrE) {         /* recombination */
02996         *ptr = ptrT;
02997         val = tval;
02998         if (node->ref > 1) {
02999             if (st_add_direct(table,(char *)node,(char *)*ptr) ==
03000                     ST_OUT_OF_MEM)
03001                 return(CUDD_OUT_OF_MEM);
03002         }
03003     } else if ((ptrT != cuddT(node) || ptrE != cuddE(node)) &&
03004                (*ptr = cuddUniqueLookup(dd,node->index,ptrT,ptrE)) != NULL) {
03005         if (Cudd_IsComplement((*ptr)->next)) {
03006             val = 0;
03007         } else {
03008             val = 1 + tval + eval;
03009         }
03010         if (node->ref > 1) {
03011             if (st_add_direct(table,(char *)node,(char *)*ptr) ==
03012                     ST_OUT_OF_MEM)
03013                 return(CUDD_OUT_OF_MEM);
03014         }
03015     } else {
03016         *ptr = node;
03017         val = 1 + tval + eval;
03018     }
03019     return(val);
03020 
03021 } /* end of cuddEstimateCofactor */
03022 
03023 
03036 static DdNode *
03037 cuddUniqueLookup(
03038   DdManager * unique,
03039   int  index,
03040   DdNode * T,
03041   DdNode * E)
03042 {
03043     int posn;
03044     unsigned int level;
03045     DdNodePtr *nodelist;
03046     DdNode *looking;
03047     DdSubtable *subtable;
03048 
03049     if (index >= unique->size) {
03050         return(NULL);
03051     }
03052 
03053     level = unique->perm[index];
03054     subtable = &(unique->subtables[level]);
03055 
03056 #ifdef DD_DEBUG
03057     assert(level < (unsigned) cuddI(unique,T->index));
03058     assert(level < (unsigned) cuddI(unique,Cudd_Regular(E)->index));
03059 #endif
03060 
03061     posn = ddHash(T, E, subtable->shift);
03062     nodelist = subtable->nodelist;
03063     looking = nodelist[posn];
03064 
03065     while (T < cuddT(looking)) {
03066         looking = Cudd_Regular(looking->next);
03067     }
03068     while (T == cuddT(looking) && E < cuddE(looking)) {
03069         looking = Cudd_Regular(looking->next);
03070     }
03071     if (cuddT(looking) == T && cuddE(looking) == E) {
03072         return(looking);
03073     }
03074 
03075     return(NULL);
03076 
03077 } /* end of cuddUniqueLookup */
03078 
03079 
03095 static int
03096 cuddEstimateCofactorSimple(
03097   DdNode * node,
03098   int i)
03099 {
03100     int tval, eval;
03101 
03102     if (Cudd_IsComplement(node->next)) {
03103         return(0);
03104     }
03105     node->next = Cudd_Not(node->next);
03106     if (cuddIsConstant(node)) {
03107         return(1);
03108     }
03109     tval = cuddEstimateCofactorSimple(cuddT(node),i);
03110     if ((int) node->index == i) return(tval);
03111     eval = cuddEstimateCofactorSimple(Cudd_Regular(cuddE(node)),i);
03112     return(1 + tval + eval);
03113 
03114 } /* end of cuddEstimateCofactorSimple */
03115 
03116 
03135 static double
03136 ddCountMintermAux(
03137   DdNode * node,
03138   double  max,
03139   DdHashTable * table)
03140 {
03141     DdNode      *N, *Nt, *Ne;
03142     double      min, minT, minE;
03143     DdNode      *res;
03144 
03145     N = Cudd_Regular(node);
03146 
03147     if (cuddIsConstant(N)) {
03148         if (node == background || node == zero) {
03149             return(0.0);
03150         } else {
03151             return(max);
03152         }
03153     }
03154     if (N->ref != 1 && (res = cuddHashTableLookup1(table,node)) != NULL) {
03155         min = cuddV(res);
03156         if (res->ref == 0) {
03157             table->manager->dead++;
03158             table->manager->constants.dead++;
03159         }
03160         return(min);
03161     }
03162 
03163     Nt = cuddT(N); Ne = cuddE(N);
03164     if (Cudd_IsComplement(node)) {
03165         Nt = Cudd_Not(Nt); Ne = Cudd_Not(Ne);
03166     }
03167 
03168     minT = ddCountMintermAux(Nt,max,table);
03169     if (minT == (double)CUDD_OUT_OF_MEM) return((double)CUDD_OUT_OF_MEM);
03170     minT *= 0.5;
03171     minE = ddCountMintermAux(Ne,max,table);
03172     if (minE == (double)CUDD_OUT_OF_MEM) return((double)CUDD_OUT_OF_MEM);
03173     minE *= 0.5;
03174     min = minT + minE;
03175 
03176     if (N->ref != 1) {
03177         ptrint fanout = (ptrint) N->ref;
03178         cuddSatDec(fanout);
03179         res = cuddUniqueConst(table->manager,min);
03180         if (!cuddHashTableInsert1(table,node,res,fanout)) {
03181             cuddRef(res); Cudd_RecursiveDeref(table->manager, res);
03182             return((double)CUDD_OUT_OF_MEM);
03183         }
03184     }
03185 
03186     return(min);
03187 
03188 } /* end of ddCountMintermAux */
03189 
03190 
03208 static double
03209 ddCountPathAux(
03210   DdNode * node,
03211   st_table * table)
03212 {
03213 
03214     DdNode      *Nv, *Nnv;
03215     double      paths, *ppaths, paths1, paths2;
03216     double      *dummy;
03217 
03218 
03219     if (cuddIsConstant(node)) {
03220         return(1.0);
03221     }
03222     if (st_lookup(table, (char *)node, (char **)&dummy)) {
03223         paths = *dummy;
03224         return(paths);
03225     }
03226 
03227     Nv = cuddT(node); Nnv = cuddE(node);
03228 
03229     paths1 = ddCountPathAux(Nv,table);
03230     if (paths1 == (double)CUDD_OUT_OF_MEM) return((double)CUDD_OUT_OF_MEM);
03231     paths2 = ddCountPathAux(Cudd_Regular(Nnv),table);
03232     if (paths2 == (double)CUDD_OUT_OF_MEM) return((double)CUDD_OUT_OF_MEM);
03233     paths = paths1 + paths2;
03234     
03235     ppaths = ALLOC(double,1);
03236     if (ppaths == NULL) {
03237         return((double)CUDD_OUT_OF_MEM);
03238     }
03239 
03240     *ppaths = paths;
03241 
03242     if (st_add_direct(table,(char *)node, (char *)ppaths) == ST_OUT_OF_MEM) {
03243         FREE(ppaths);
03244         return((double)CUDD_OUT_OF_MEM);
03245     }
03246     return(paths);
03247 
03248 } /* end of ddCountPathAux */
03249 
03250 
03269 static int
03270 ddEpdCountMintermAux(
03271   DdNode * node,
03272   EpDouble * max,
03273   EpDouble * epd,
03274   st_table * table)
03275 {
03276     DdNode      *Nt, *Ne;
03277     EpDouble    *min, minT, minE;
03278     EpDouble    *res;
03279     int         status;
03280 
03281     if (cuddIsConstant(node)) {
03282         if (node == background || node == zero) {
03283             EpdMakeZero(epd, 0);
03284         } else {
03285             EpdCopy(max, epd);
03286         }
03287         return(0);
03288     }
03289     if (node->ref != 1 && st_lookup(table, (char *)node, (char **)&res)) {
03290         EpdCopy(res, epd);
03291         return(0);
03292     }
03293 
03294     Nt = cuddT(node); Ne = cuddE(node);
03295     if (Cudd_IsComplement(node)) {
03296         Nt = Cudd_Not(Nt); Ne = Cudd_Not(Ne);
03297     }
03298 
03299     status = ddEpdCountMintermAux(Nt,max,&minT,table);
03300     if (status == CUDD_OUT_OF_MEM) return(CUDD_OUT_OF_MEM);
03301     EpdMultiply(&minT, (double)0.5);
03302     status = ddEpdCountMintermAux(Ne,max,&minE,table);
03303     if (status == CUDD_OUT_OF_MEM) return(CUDD_OUT_OF_MEM);
03304     if (Cudd_IsComplement(Ne)) {
03305         EpdSubtract3(max, &minE, epd);
03306         EpdCopy(epd, &minE);
03307     }
03308     EpdMultiply(&minE, (double)0.5);
03309     EpdAdd3(&minT, &minE, epd);
03310 
03311     if (node->ref > 1) {
03312         min = EpdAlloc();
03313         if (!min)
03314             return(CUDD_OUT_OF_MEM);
03315         EpdCopy(epd, min);
03316         if (st_insert(table, (char *)node, (char *)min) == ST_OUT_OF_MEM) {
03317             EpdFree(min);
03318             return(CUDD_OUT_OF_MEM);
03319         }
03320     }
03321 
03322     return(0);
03323 
03324 } /* end of ddEpdCountMintermAux */
03325 
03326 
03343 static double
03344 ddCountPathsToNonZero(
03345   DdNode * N,
03346   st_table * table)
03347 {
03348 
03349     DdNode      *node, *Nt, *Ne;
03350     double      paths, *ppaths, paths1, paths2;
03351     double      *dummy;
03352 
03353     node = Cudd_Regular(N);
03354     if (cuddIsConstant(node)) {
03355         return((double) !(Cudd_IsComplement(N) || cuddV(node)==DD_ZERO_VAL));
03356     }
03357     if (st_lookup(table, (char *)N, (char **)&dummy)) {
03358         paths = *dummy;
03359         return(paths);
03360     }
03361 
03362     Nt = cuddT(node); Ne = cuddE(node);
03363     if (node != N) {
03364         Nt = Cudd_Not(Nt); Ne = Cudd_Not(Ne);
03365     }
03366 
03367     paths1 = ddCountPathsToNonZero(Nt,table);
03368     if (paths1 == (double)CUDD_OUT_OF_MEM) return((double)CUDD_OUT_OF_MEM);
03369     paths2 = ddCountPathsToNonZero(Ne,table);
03370     if (paths2 == (double)CUDD_OUT_OF_MEM) return((double)CUDD_OUT_OF_MEM);
03371     paths = paths1 + paths2;
03372 
03373     ppaths = ALLOC(double,1);
03374     if (ppaths == NULL) {
03375         return((double)CUDD_OUT_OF_MEM);
03376     }
03377 
03378     *ppaths = paths;
03379 
03380     if (st_add_direct(table,(char *)N, (char *)ppaths) == ST_OUT_OF_MEM) {
03381         FREE(ppaths);
03382         return((double)CUDD_OUT_OF_MEM);
03383     }
03384     return(paths);
03385 
03386 } /* end of ddCountPathsToNonZero */
03387 
03388 
03402 static void
03403 ddSupportStep(
03404   DdNode * f,
03405   int * support)
03406 {
03407     if (cuddIsConstant(f) || Cudd_IsComplement(f->next)) {
03408         return;
03409     }
03410 
03411     support[f->index] = 1;
03412     ddSupportStep(cuddT(f),support);
03413     ddSupportStep(Cudd_Regular(cuddE(f)),support);
03414     /* Mark as visited. */
03415     f->next = Cudd_Not(f->next);
03416     return;
03417 
03418 } /* end of ddSupportStep */
03419 
03420 
03433 static void
03434 ddClearFlag(
03435   DdNode * f)
03436 {
03437     if (!Cudd_IsComplement(f->next)) {
03438         return;
03439     }
03440     /* Clear visited flag. */
03441     f->next = Cudd_Regular(f->next);
03442     if (cuddIsConstant(f)) {
03443         return;
03444     }
03445     ddClearFlag(cuddT(f));
03446     ddClearFlag(Cudd_Regular(cuddE(f)));
03447     return;
03448 
03449 } /* end of ddClearFlag */
03450 
03451 
03464 static int
03465 ddLeavesInt(
03466   DdNode * n)
03467 {
03468     int tval, eval;
03469 
03470     if (Cudd_IsComplement(n->next)) {
03471         return(0);
03472     }
03473     n->next = Cudd_Not(n->next);
03474     if (cuddIsConstant(n)) {
03475         return(1);
03476     }
03477     tval = ddLeavesInt(cuddT(n));
03478     eval = ddLeavesInt(Cudd_Regular(cuddE(n)));
03479     return(tval + eval);
03480 
03481 } /* end of ddLeavesInt */
03482 
03483 
03496 static int
03497 ddPickArbitraryMinterms(
03498   DdManager *dd,
03499   DdNode *node,
03500   int nvars,
03501   int nminterms,
03502   char **string)
03503 {
03504     DdNode *N, *T, *E;
03505     DdNode *one, *bzero;
03506     int    i, t, result;
03507     double min1, min2;
03508 
03509     if (string == NULL || node == NULL) return(0);
03510 
03511     /* The constant 0 function has no on-set cubes. */
03512     one = DD_ONE(dd);
03513     bzero = Cudd_Not(one);
03514     if (nminterms == 0 || node == bzero) return(1);
03515     if (node == one) {
03516         return(1);
03517     }
03518 
03519     N = Cudd_Regular(node);
03520     T = cuddT(N); E = cuddE(N);
03521     if (Cudd_IsComplement(node)) {
03522         T = Cudd_Not(T); E = Cudd_Not(E);
03523     }
03524 
03525     min1 = Cudd_CountMinterm(dd, T, nvars) / 2.0;
03526     if (min1 == (double)CUDD_OUT_OF_MEM) return(0);
03527     min2 = Cudd_CountMinterm(dd, E, nvars) / 2.0;
03528     if (min2 == (double)CUDD_OUT_OF_MEM) return(0);
03529 
03530     t = (int)((double)nminterms * min1 / (min1 + min2) + 0.5);
03531     for (i = 0; i < t; i++)
03532         string[i][N->index] = '1';
03533     for (i = t; i < nminterms; i++)
03534         string[i][N->index] = '0';
03535 
03536     result = ddPickArbitraryMinterms(dd,T,nvars,t,&string[0]);
03537     if (result == 0)
03538         return(0);
03539     result = ddPickArbitraryMinterms(dd,E,nvars,nminterms-t,&string[t]);
03540     return(result);
03541 
03542 } /* end of ddPickArbitraryMinterms */
03543 
03544 
03557 static int
03558 ddPickRepresentativeCube(
03559   DdManager *dd,
03560   DdNode *node,
03561   int nvars,
03562   double *weight,
03563   char *string)
03564 {
03565     DdNode *N, *T, *E;
03566     DdNode *one, *bzero;
03567 
03568     if (string == NULL || node == NULL) return(0);
03569 
03570     /* The constant 0 function has no on-set cubes. */
03571     one = DD_ONE(dd);
03572     bzero = Cudd_Not(one);
03573     if (node == bzero) return(0);
03574 
03575     if (node == DD_ONE(dd)) return(1);
03576 
03577     for (;;) {
03578         N = Cudd_Regular(node);
03579         if (N == one)
03580             break;
03581         T = cuddT(N);
03582         E = cuddE(N);
03583         if (Cudd_IsComplement(node)) {
03584             T = Cudd_Not(T);
03585             E = Cudd_Not(E);
03586         }
03587         if (weight[N->index] >= 0.0) {
03588             if (T == bzero) {
03589                 node = E;
03590                 string[N->index] = '0';
03591             } else {
03592                 node = T;
03593                 string[N->index] = '1';
03594             }
03595         } else {
03596             if (E == bzero) {
03597                 node = T;
03598                 string[N->index] = '1';
03599             } else {
03600                 node = E;
03601                 string[N->index] = '0';
03602             }
03603         }
03604     }
03605     return(1);
03606 
03607 } /* end of ddPickRepresentativeCube */
03608 
03609 
03621 static enum st_retval
03622 ddEpdFree(
03623   char * key,
03624   char * value,
03625   char * arg)
03626 {
03627     EpDouble    *epd;
03628 
03629     epd = (EpDouble *) value;
03630     EpdFree(epd);
03631     return(ST_CONTINUE);
03632 
03633 } /* end of ddEpdFree */