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

00001 
00053 #include "util.h"
00054 #include "cuddInt.h"
00055 
00056 
00057 /*---------------------------------------------------------------------------*/
00058 /* Constant declarations                                                     */
00059 /*---------------------------------------------------------------------------*/
00060 
00061 #define TESTCUDD_VERSION        "TestCudd Version #1.0, Release date 3/17/01"
00062 
00063 /*---------------------------------------------------------------------------*/
00064 /* Variable declarations                                                     */
00065 /*---------------------------------------------------------------------------*/
00066 
00067 #ifndef lint
00068 static char rcsid[] DD_UNUSED = "$Id: testcudd.c,v 1.20 2009/03/08 02:49:02 fabio Exp $";
00069 #endif
00070 
00071 static const char *onames[] = { "C", "M" }; /* names of functions to be dumped */
00072 
00075 /*---------------------------------------------------------------------------*/
00076 /* Static function prototypes                                                */
00077 /*---------------------------------------------------------------------------*/
00078 
00079 static void usage (char * prog);
00080 static FILE *open_file (char *filename, const char *mode);
00081 static int testIterators (DdManager *dd, DdNode *M, DdNode *C, int pr);
00082 static int testXor (DdManager *dd, DdNode *f, int pr, int nvars);
00083 static int testHamming (DdManager *dd, DdNode *f, int pr);
00084 static int testWalsh (DdManager *dd, int N, int cmu, int approach, int pr);
00085 
00100 int
00101 main(int argc, char **argv)
00102 {
00103     FILE *fp;           /* pointer to input file */
00104     char *file = (char *) "";   /* input file name */
00105     FILE *dfp = NULL;   /* pointer to dump file */
00106     char *dfile;        /* file for DD dump */
00107     DdNode *dfunc[2];   /* addresses of the functions to be dumped */
00108     DdManager *dd;      /* pointer to DD manager */
00109     DdNode *one;        /* fast access to constant function */
00110     DdNode *M;
00111     DdNode **x;         /* pointers to variables */
00112     DdNode **y;         /* pointers to variables */
00113     DdNode **xn;        /* complements of row variables */
00114     DdNode **yn_;       /* complements of column variables */
00115     DdNode **xvars;
00116     DdNode **yvars;
00117     DdNode *C;          /* result of converting from ADD to BDD */
00118     DdNode *ess;        /* cube of essential variables */
00119     DdNode *shortP;     /* BDD cube of shortest path */
00120     DdNode *largest;    /* BDD of largest cube */
00121     DdNode *shortA;     /* ADD cube of shortest path */
00122     DdNode *constN;     /* value returned by evaluation of ADD */
00123     DdNode *ycube;      /* cube of the negated y vars for c-proj */
00124     DdNode *CP;         /* C-Projection of C */
00125     DdNode *CPr;        /* C-Selection of C */
00126     int    length;      /* length of the shortest path */
00127     int    nx;                  /* number of variables */
00128     int    ny;
00129     int    maxnx;
00130     int    maxny;
00131     int    m;
00132     int    n;
00133     int    N;
00134     int    cmu;                 /* use CMU multiplication */
00135     int    pr;                  /* verbose printout level */
00136     int    harwell;
00137     int    multiple;            /* read multiple matrices */
00138     int    ok;
00139     int    c;                   /* variable to read in options */
00140     int    approach;            /* reordering approach */
00141     int    autodyn;             /* automatic reordering */
00142     int    groupcheck;          /* option for group sifting */
00143     int    profile;             /* print heap profile if != 0 */
00144     int    keepperm;            /* keep track of permutation */
00145     int    clearcache;          /* clear the cache after each matrix */
00146     int    blifOrDot;           /* dump format: 0 -> dot, 1 -> blif, ... */
00147     int    retval;              /* return value */
00148     int    i;                   /* loop index */
00149     long   startTime;           /* initial time */
00150     long   lapTime;
00151     int    size;
00152     unsigned int cacheSize, maxMemory;
00153     unsigned int nvars,nslots;
00154 
00155     startTime = util_cpu_time();
00156 
00157     approach = CUDD_REORDER_NONE;
00158     autodyn = 0;
00159     pr = 0;
00160     harwell = 0;
00161     multiple = 0;
00162     profile = 0;
00163     keepperm = 0;
00164     cmu = 0;
00165     N = 4;
00166     nvars = 4;
00167     cacheSize = 127;
00168     maxMemory = 0;
00169     nslots = CUDD_UNIQUE_SLOTS;
00170     clearcache = 0;
00171     groupcheck = CUDD_GROUP_CHECK7;
00172     dfile = NULL;
00173     blifOrDot = 0; /* dot format */
00174 
00175     /* Parse command line. */
00176     while ((c = util_getopt(argc, argv, (char *) "CDHMPS:a:bcd:g:hkmn:p:v:x:X:"))
00177            != EOF) {
00178         switch(c) {
00179         case 'C':
00180             cmu = 1;
00181             break;
00182         case 'D':
00183             autodyn = 1;
00184             break;
00185         case 'H':
00186             harwell = 1;
00187             break;
00188         case 'M':
00189 #ifdef MNEMOSYNE
00190             (void) mnem_setrecording(0);
00191 #endif
00192             break;
00193         case 'P':
00194             profile = 1;
00195             break;
00196         case 'S':
00197             nslots = atoi(util_optarg);
00198             break;
00199         case 'X':
00200             maxMemory = atoi(util_optarg);
00201             break;
00202         case 'a':
00203             approach = atoi(util_optarg);
00204             break;
00205         case 'b':
00206             blifOrDot = 1; /* blif format */
00207             break;
00208         case 'c':
00209             clearcache = 1;
00210             break;
00211         case 'd':
00212             dfile = util_optarg;
00213             break;
00214         case 'g':
00215             groupcheck = atoi(util_optarg);
00216             break;
00217         case 'k':
00218             keepperm = 1;
00219             break;
00220         case 'm':
00221             multiple = 1;
00222             break;
00223         case 'n':
00224             N = atoi(util_optarg);
00225             break;
00226         case 'p':
00227             pr = atoi(util_optarg);
00228             break;
00229         case 'v':
00230             nvars = atoi(util_optarg);
00231             break;
00232         case 'x':
00233             cacheSize = atoi(util_optarg);
00234             break;
00235         case 'h':
00236         default:
00237             usage(argv[0]);
00238             break;
00239         }
00240     }
00241 
00242     if (argc - util_optind == 0) {
00243         file = (char *) "-";
00244     } else if (argc - util_optind == 1) {
00245         file = argv[util_optind];
00246     } else {
00247         usage(argv[0]);
00248     }
00249     if ((approach<0) || (approach>17)) {
00250         (void) fprintf(stderr,"Invalid approach: %d \n",approach);
00251         usage(argv[0]);
00252     }
00253 
00254     if (pr >= 0) {
00255         (void) printf("# %s\n", TESTCUDD_VERSION);
00256         /* Echo command line and arguments. */
00257         (void) printf("#");
00258         for (i = 0; i < argc; i++) {
00259             (void) printf(" %s", argv[i]);
00260         }
00261         (void) printf("\n");
00262         (void) fflush(stdout);
00263     }
00264 
00265     /* Initialize manager and provide easy reference to terminals. */
00266     dd = Cudd_Init(nvars,0,nslots,cacheSize,maxMemory);
00267     one = DD_ONE(dd);
00268     dd->groupcheck = (Cudd_AggregationType) groupcheck;
00269     if (autodyn) Cudd_AutodynEnable(dd,CUDD_REORDER_SAME);
00270 
00271     /* Open input file. */
00272     fp = open_file(file, "r");
00273 
00274     /* Open dump file if requested */
00275     if (dfile != NULL) {
00276         dfp = open_file(dfile, "w");
00277     }
00278 
00279     x = y = xn = yn_ = NULL;
00280     do {
00281         /* We want to start anew for every matrix. */
00282         maxnx = maxny = 0;
00283         nx = maxnx; ny = maxny;
00284         if (pr>0) lapTime = util_cpu_time();
00285         if (harwell) {
00286             if (pr >= 0) (void) printf(":name: ");
00287             ok = Cudd_addHarwell(fp, dd, &M, &x, &y, &xn, &yn_, &nx, &ny,
00288             &m, &n, 0, 2, 1, 2, pr);
00289         } else {
00290             ok = Cudd_addRead(fp, dd, &M, &x, &y, &xn, &yn_, &nx, &ny,
00291             &m, &n, 0, 2, 1, 2);
00292             if (pr >= 0)
00293                 (void) printf(":name: %s: %d rows %d columns\n", file, m, n);
00294         }
00295         if (!ok) {
00296             (void) fprintf(stderr, "Error reading matrix\n");
00297             exit(1);
00298         }
00299 
00300         if (nx > maxnx) maxnx = nx;
00301         if (ny > maxny) maxny = ny;
00302 
00303         /* Build cube of negated y's. */
00304         ycube = DD_ONE(dd);
00305         Cudd_Ref(ycube);
00306         for (i = maxny - 1; i >= 0; i--) {
00307             DdNode *tmpp;
00308             tmpp = Cudd_bddAnd(dd,Cudd_Not(dd->vars[y[i]->index]),ycube);
00309             if (tmpp == NULL) exit(2);
00310             Cudd_Ref(tmpp);
00311             Cudd_RecursiveDeref(dd,ycube);
00312             ycube = tmpp;
00313         }
00314         /* Initialize vectors of BDD variables used by priority func. */
00315         xvars = ALLOC(DdNode *, nx);
00316         if (xvars == NULL) exit(2);
00317         for (i = 0; i < nx; i++) {
00318             xvars[i] = dd->vars[x[i]->index];
00319         }
00320         yvars = ALLOC(DdNode *, ny);
00321         if (yvars == NULL) exit(2);
00322         for (i = 0; i < ny; i++) {
00323             yvars[i] = dd->vars[y[i]->index];
00324         }
00325 
00326         /* Clean up */
00327         for (i=0; i < maxnx; i++) {
00328             Cudd_RecursiveDeref(dd, x[i]);
00329             Cudd_RecursiveDeref(dd, xn[i]);
00330         }
00331         FREE(x);
00332         FREE(xn);
00333         for (i=0; i < maxny; i++) {
00334             Cudd_RecursiveDeref(dd, y[i]);
00335             Cudd_RecursiveDeref(dd, yn_[i]);
00336         }
00337         FREE(y);
00338         FREE(yn_);
00339 
00340         if (pr>0) {(void) printf(":1: M"); Cudd_PrintDebug(dd,M,nx+ny,pr);}
00341 
00342         if (pr>0) (void) printf(":2: time to read the matrix = %s\n",
00343                     util_print_time(util_cpu_time() - lapTime));
00344 
00345         C = Cudd_addBddPattern(dd, M);
00346         if (C == 0) exit(2);
00347         Cudd_Ref(C);
00348         if (pr>0) {(void) printf(":3: C"); Cudd_PrintDebug(dd,C,nx+ny,pr);}
00349 
00350         /* Test iterators. */
00351         retval = testIterators(dd,M,C,pr);
00352         if (retval == 0) exit(2);
00353 
00354         cuddCacheProfile(dd,stdout);
00355 
00356         /* Test XOR */
00357         retval = testXor(dd,C,pr,nx+ny);
00358         if (retval == 0) exit(2);
00359 
00360         /* Test Hamming distance functions. */
00361         retval = testHamming(dd,C,pr);
00362         if (retval == 0) exit(2);
00363 
00364         /* Test selection functions. */
00365         CP = Cudd_CProjection(dd,C,ycube);
00366         if (CP == NULL) exit(2);
00367         Cudd_Ref(CP);
00368         if (pr>0) {(void) printf("ycube"); Cudd_PrintDebug(dd,ycube,nx+ny,pr);}
00369         if (pr>0) {(void) printf("CP"); Cudd_PrintDebug(dd,CP,nx+ny,pr);}
00370 
00371         if (nx == ny) {
00372             CPr = Cudd_PrioritySelect(dd,C,xvars,yvars,(DdNode **)NULL,
00373                 (DdNode *)NULL,ny,Cudd_Xgty);
00374             if (CPr == NULL) exit(2);
00375             Cudd_Ref(CPr);
00376             if (pr>0) {(void) printf(":4: CPr"); Cudd_PrintDebug(dd,CPr,nx+ny,pr);}
00377             if (CP != CPr) {
00378                 (void) printf("CP != CPr!\n");
00379             }
00380             Cudd_RecursiveDeref(dd, CPr);
00381         }
00382 
00383         /* Test inequality generator. */
00384         {
00385             int Nmin = ddMin(nx,ny);
00386             int q;
00387             DdGen *gen;
00388             int *cube;
00389             DdNode *f = Cudd_Inequality(dd,Nmin,2,xvars,yvars);
00390             if (f == NULL) exit(2);
00391             Cudd_Ref(f);
00392             if (pr>0) {
00393                 (void) printf(":4: ineq");
00394                 Cudd_PrintDebug(dd,f,nx+ny,pr);
00395                 if (pr>1) {
00396                     Cudd_ForeachPrime(dd,Cudd_Not(f),Cudd_Not(f),gen,cube) {
00397                         for (q = 0; q < dd->size; q++) {
00398                             switch (cube[q]) {
00399                             case 0:
00400                                 (void) printf("1");
00401                                 break;
00402                             case 1:
00403                                 (void) printf("0");
00404                                 break;
00405                             case 2:
00406                                 (void) printf("-");
00407                                 break;
00408                             default:
00409                                 (void) printf("?");
00410                             }
00411                         }
00412                         (void) printf(" 1\n");
00413                     }
00414                     (void) printf("\n");
00415                 }
00416             }
00417             Cudd_IterDerefBdd(dd, f);
00418         }
00419         FREE(xvars); FREE(yvars);
00420 
00421         Cudd_RecursiveDeref(dd, CP);
00422         Cudd_RecursiveDeref(dd, ycube);
00423 
00424         /* Test functions for essential variables. */
00425         ess = Cudd_FindEssential(dd,C);
00426         if (ess == NULL) exit(2);
00427         Cudd_Ref(ess);
00428         if (pr>0) {(void) printf(":4: ess"); Cudd_PrintDebug(dd,ess,nx+ny,pr);}
00429         Cudd_RecursiveDeref(dd, ess);
00430 
00431         /* Test functions for shortest paths. */
00432         shortP = Cudd_ShortestPath(dd, M, NULL, NULL, &length);
00433         if (shortP == NULL) exit(2);
00434         Cudd_Ref(shortP);
00435         if (pr>0) {
00436             (void) printf(":5: shortP"); Cudd_PrintDebug(dd,shortP,nx+ny,pr);
00437         }
00438         /* Test functions for largest cubes. */
00439         largest = Cudd_LargestCube(dd, Cudd_Not(C), &length);
00440         if (largest == NULL) exit(2);
00441         Cudd_Ref(largest);
00442         if (pr>0) {
00443             (void) printf(":5b: largest");
00444             Cudd_PrintDebug(dd,largest,nx+ny,pr);
00445         }
00446         Cudd_RecursiveDeref(dd, largest);
00447 
00448         /* Test Cudd_addEvalConst and Cudd_addIteConstant. */
00449         shortA = Cudd_BddToAdd(dd,shortP);
00450         if (shortA == NULL) exit(2);
00451         Cudd_Ref(shortA);
00452         Cudd_RecursiveDeref(dd, shortP);
00453         constN = Cudd_addEvalConst(dd,shortA,M);
00454         if (constN == DD_NON_CONSTANT) exit(2);
00455         if (Cudd_addIteConstant(dd,shortA,M,constN) != constN) exit(2);
00456         if (pr>0) {(void) printf("The value of M along the chosen shortest path is %g\n", cuddV(constN));}
00457         Cudd_RecursiveDeref(dd, shortA);
00458 
00459         shortP = Cudd_ShortestPath(dd, C, NULL, NULL, &length);
00460         if (shortP == NULL) exit(2);
00461         Cudd_Ref(shortP);
00462         if (pr>0) {
00463             (void) printf(":6: shortP"); Cudd_PrintDebug(dd,shortP,nx+ny,pr);
00464         }
00465 
00466         /* Test Cudd_bddIteConstant and Cudd_bddLeq. */
00467         if (!Cudd_bddLeq(dd,shortP,C)) exit(2);
00468         if (Cudd_bddIteConstant(dd,Cudd_Not(shortP),one,C) != one) exit(2);
00469         Cudd_RecursiveDeref(dd, shortP);
00470 
00471         if (profile) {
00472             retval = cuddHeapProfile(dd);
00473         }
00474 
00475         size = dd->size;
00476 
00477         if (pr>0) {
00478             (void) printf("Average distance: %g\n", Cudd_AverageDistance(dd));
00479         }
00480 
00481         /* Reorder if so requested. */
00482         if (approach != CUDD_REORDER_NONE) {
00483 #ifndef DD_STATS
00484             retval = Cudd_EnableReorderingReporting(dd);
00485             if (retval == 0) {
00486                 (void) fprintf(stderr,"Error reported by Cudd_EnableReorderingReporting\n");
00487                 exit(3);
00488             }
00489 #endif
00490 #ifdef DD_DEBUG
00491             retval = Cudd_DebugCheck(dd);
00492             if (retval != 0) {
00493                 (void) fprintf(stderr,"Error reported by Cudd_DebugCheck\n");
00494                 exit(3);
00495             }
00496             retval = Cudd_CheckKeys(dd);
00497             if (retval != 0) {
00498                 (void) fprintf(stderr,"Error reported by Cudd_CheckKeys\n");
00499                 exit(3);
00500             }
00501 #endif
00502             retval = Cudd_ReduceHeap(dd,(Cudd_ReorderingType)approach,5);
00503             if (retval == 0) {
00504                 (void) fprintf(stderr,"Error reported by Cudd_ReduceHeap\n");
00505                 exit(3);
00506             }
00507 #ifndef DD_STATS
00508             retval = Cudd_DisableReorderingReporting(dd);
00509             if (retval == 0) {
00510                 (void) fprintf(stderr,"Error reported by Cudd_DisableReorderingReporting\n");
00511                 exit(3);
00512             }
00513 #endif
00514 #ifdef DD_DEBUG
00515             retval = Cudd_DebugCheck(dd);
00516             if (retval != 0) {
00517                 (void) fprintf(stderr,"Error reported by Cudd_DebugCheck\n");
00518                 exit(3);
00519             }
00520             retval = Cudd_CheckKeys(dd);
00521             if (retval != 0) {
00522                 (void) fprintf(stderr,"Error reported by Cudd_CheckKeys\n");
00523                 exit(3);
00524             }
00525 #endif
00526             if (approach == CUDD_REORDER_SYMM_SIFT ||
00527             approach == CUDD_REORDER_SYMM_SIFT_CONV) {
00528                 Cudd_SymmProfile(dd,0,dd->size-1);
00529             }
00530 
00531             if (pr>0) {
00532                 (void) printf("Average distance: %g\n", Cudd_AverageDistance(dd));
00533             }
00534 
00535             if (keepperm) {
00536                 /* Print variable permutation. */
00537                 (void) printf("Variable Permutation:");
00538                 for (i=0; i<size; i++) {
00539                     if (i%20 == 0) (void) printf("\n");
00540                     (void) printf("%d ", dd->invperm[i]);
00541                 }
00542                 (void) printf("\n");
00543                 (void) printf("Inverse Permutation:");
00544                 for (i=0; i<size; i++) {
00545                     if (i%20 == 0) (void) printf("\n");
00546                     (void) printf("%d ", dd->perm[i]);
00547                 }
00548                 (void) printf("\n");
00549             }
00550 
00551             if (pr>0) {(void) printf("M"); Cudd_PrintDebug(dd,M,nx+ny,pr);}
00552 
00553             if (profile) {
00554                 retval = cuddHeapProfile(dd);
00555             }
00556 
00557         }
00558 
00559         /* Dump DDs of C and M if so requested. */
00560         if (dfile != NULL) {
00561             dfunc[0] = C;
00562             dfunc[1] = M;
00563             if (blifOrDot == 1) {
00564                 /* Only dump C because blif cannot handle ADDs */
00565                 retval = Cudd_DumpBlif(dd,1,dfunc,NULL,(char **)onames,
00566                                        NULL,dfp,0);
00567             } else {
00568                 retval = Cudd_DumpDot(dd,2,dfunc,NULL,(char **)onames,dfp);
00569             }
00570             if (retval != 1) {
00571                 (void) fprintf(stderr,"abnormal termination\n");
00572                 exit(2);
00573             }
00574         }
00575 
00576         Cudd_RecursiveDeref(dd, C);
00577         Cudd_RecursiveDeref(dd, M);
00578 
00579         if (clearcache) {
00580             if (pr>0) {(void) printf("Clearing the cache... ");}
00581             for (i = dd->cacheSlots - 1; i>=0; i--) {
00582                 dd->cache[i].data = NIL(DdNode);
00583             }
00584             if (pr>0) {(void) printf("done\n");}
00585         }
00586         if (pr>0) {
00587             (void) printf("Number of variables = %6d\t",dd->size);
00588             (void) printf("Number of slots     = %6u\n",dd->slots);
00589             (void) printf("Number of keys      = %6u\t",dd->keys);
00590             (void) printf("Number of min dead  = %6u\n",dd->minDead);
00591         }
00592 
00593     } while (multiple && !feof(fp));
00594 
00595     fclose(fp);
00596     if (dfile != NULL) {
00597         fclose(dfp);
00598     }
00599 
00600     /* Second phase: experiment with Walsh matrices. */
00601     if (!testWalsh(dd,N,cmu,approach,pr)) {
00602         exit(2);
00603     }
00604 
00605     /* Check variable destruction. */
00606     assert(cuddDestroySubtables(dd,3));
00607     assert(Cudd_DebugCheck(dd) == 0);
00608     assert(Cudd_CheckKeys(dd) == 0);
00609 
00610     retval = Cudd_CheckZeroRef(dd);
00611     ok = retval != 0;  /* ok == 0 means O.K. */
00612     if (retval != 0) {
00613         (void) fprintf(stderr,
00614             "%d non-zero DD reference counts after dereferencing\n", retval);
00615     }
00616 
00617     if (pr >= 0) {
00618         (void) Cudd_PrintInfo(dd,stdout);
00619     }
00620 
00621     Cudd_Quit(dd);
00622 
00623 #ifdef MNEMOSYNE
00624     mnem_writestats();
00625 #endif
00626 
00627     if (pr>0) (void) printf("total time = %s\n",
00628                 util_print_time(util_cpu_time() - startTime));
00629 
00630     if (pr >= 0) util_print_cpu_stats(stdout);
00631     exit(ok);
00632     /* NOTREACHED */
00633 
00634 } /* end of main */
00635 
00636 
00637 /*---------------------------------------------------------------------------*/
00638 /* Definition of static functions                                            */
00639 /*---------------------------------------------------------------------------*/
00640 
00641 
00653 static void
00654 usage(char *prog)
00655 {
00656     (void) fprintf(stderr, "usage: %s [options] [file]\n", prog);
00657     (void) fprintf(stderr, "   -C\t\tuse CMU multiplication algorithm\n");
00658     (void) fprintf(stderr, "   -D\t\tenable automatic dynamic reordering\n");
00659     (void) fprintf(stderr, "   -H\t\tread matrix in Harwell format\n");
00660     (void) fprintf(stderr, "   -M\t\tturns off memory allocation recording\n");
00661     (void) fprintf(stderr, "   -P\t\tprint BDD heap profile\n");
00662     (void) fprintf(stderr, "   -S n\t\tnumber of slots for each subtable\n");
00663     (void) fprintf(stderr, "   -X n\t\ttarget maximum memory in bytes\n");
00664     (void) fprintf(stderr, "   -a n\t\tchoose reordering approach (0-13)\n");
00665     (void) fprintf(stderr, "   \t\t\t0: same as autoMethod\n");
00666     (void) fprintf(stderr, "   \t\t\t1: no reordering (default)\n");
00667     (void) fprintf(stderr, "   \t\t\t2: random\n");
00668     (void) fprintf(stderr, "   \t\t\t3: pivot\n");
00669     (void) fprintf(stderr, "   \t\t\t4: sifting\n");
00670     (void) fprintf(stderr, "   \t\t\t5: sifting to convergence\n");
00671     (void) fprintf(stderr, "   \t\t\t6: symmetric sifting\n");
00672     (void) fprintf(stderr, "   \t\t\t7: symmetric sifting to convergence\n");
00673     (void) fprintf(stderr, "   \t\t\t8-10: window of size 2-4\n");
00674     (void) fprintf(stderr, "   \t\t\t11-13: window of size 2-4 to conv.\n");
00675     (void) fprintf(stderr, "   \t\t\t14: group sifting\n");
00676     (void) fprintf(stderr, "   \t\t\t15: group sifting to convergence\n");
00677     (void) fprintf(stderr, "   \t\t\t16: simulated annealing\n");
00678     (void) fprintf(stderr, "   \t\t\t17: genetic algorithm\n");
00679     (void) fprintf(stderr, "   -b\t\tuse blif as format for dumps\n");
00680     (void) fprintf(stderr, "   -c\t\tclear the cache after each matrix\n");
00681     (void) fprintf(stderr, "   -d file\tdump DDs to file\n");
00682     (void) fprintf(stderr, "   -g\t\tselect aggregation criterion (0,5,7)\n");
00683     (void) fprintf(stderr, "   -h\t\tprints this message\n");
00684     (void) fprintf(stderr, "   -k\t\tprint the variable permutation\n");
00685     (void) fprintf(stderr, "   -m\t\tread multiple matrices (only with -H)\n");
00686     (void) fprintf(stderr, "   -n n\t\tnumber of variables\n");
00687     (void) fprintf(stderr, "   -p n\t\tcontrol verbosity\n");
00688     (void) fprintf(stderr, "   -v n\t\tinitial variables in the unique table\n");
00689     (void) fprintf(stderr, "   -x n\t\tinitial size of the cache\n");
00690     exit(2);
00691 } /* end of usage */
00692 
00693 
00706 static FILE *
00707 open_file(char *filename, const char *mode)
00708 {
00709     FILE *fp;
00710 
00711     if (strcmp(filename, "-") == 0) {
00712         return mode[0] == 'r' ? stdin : stdout;
00713     } else if ((fp = fopen(filename, mode)) == NULL) {
00714         perror(filename);
00715         exit(1);
00716     }
00717     return fp;
00718 
00719 } /* end of open_file */
00720 
00721 
00734 static int
00735 testWalsh(
00736   DdManager *dd /* manager */,
00737   int N /* number of variables */,
00738   int cmu /* use CMU approach to matrix multiplication */,
00739   int approach /* reordering approach */,
00740   int pr /* verbosity level */)
00741 {
00742     DdNode *walsh1, *walsh2, *wtw;
00743     DdNode **x, **v, **z;
00744     int i, retval;
00745     DdNode *one = DD_ONE(dd);
00746     DdNode *zero = DD_ZERO(dd);
00747 
00748     if (N > 3) {
00749         x = ALLOC(DdNode *,N);
00750         v = ALLOC(DdNode *,N);
00751         z = ALLOC(DdNode *,N);
00752 
00753         for (i = N-1; i >= 0; i--) {
00754             Cudd_Ref(x[i]=cuddUniqueInter(dd,3*i,one,zero));
00755             Cudd_Ref(v[i]=cuddUniqueInter(dd,3*i+1,one,zero));
00756             Cudd_Ref(z[i]=cuddUniqueInter(dd,3*i+2,one,zero));
00757         }
00758         Cudd_Ref(walsh1 = Cudd_addWalsh(dd,v,z,N));
00759         if (pr>0) {(void) printf("walsh1"); Cudd_PrintDebug(dd,walsh1,2*N,pr);}
00760         Cudd_Ref(walsh2 = Cudd_addWalsh(dd,x,v,N));
00761         if (cmu) {
00762             Cudd_Ref(wtw = Cudd_addTimesPlus(dd,walsh2,walsh1,v,N));
00763         } else {
00764             Cudd_Ref(wtw = Cudd_addMatrixMultiply(dd,walsh2,walsh1,v,N));
00765         }
00766         if (pr>0) {(void) printf("wtw"); Cudd_PrintDebug(dd,wtw,2*N,pr);}
00767 
00768         if (approach != CUDD_REORDER_NONE) {
00769 #ifdef DD_DEBUG
00770             retval = Cudd_DebugCheck(dd);
00771             if (retval != 0) {
00772                 (void) fprintf(stderr,"Error reported by Cudd_DebugCheck\n");
00773                 return(0);
00774             }
00775 #endif
00776             retval = Cudd_ReduceHeap(dd,(Cudd_ReorderingType)approach,5);
00777             if (retval == 0) {
00778                 (void) fprintf(stderr,"Error reported by Cudd_ReduceHeap\n");
00779                 return(0);
00780             }
00781 #ifdef DD_DEBUG
00782             retval = Cudd_DebugCheck(dd);
00783             if (retval != 0) {
00784                 (void) fprintf(stderr,"Error reported by Cudd_DebugCheck\n");
00785                 return(0);
00786             }
00787 #endif
00788             if (approach == CUDD_REORDER_SYMM_SIFT ||
00789             approach == CUDD_REORDER_SYMM_SIFT_CONV) {
00790                 Cudd_SymmProfile(dd,0,dd->size-1);
00791             }
00792         }
00793         /* Clean up. */
00794         Cudd_RecursiveDeref(dd, wtw);
00795         Cudd_RecursiveDeref(dd, walsh1);
00796         Cudd_RecursiveDeref(dd, walsh2);
00797         for (i=0; i < N; i++) {
00798             Cudd_RecursiveDeref(dd, x[i]);
00799             Cudd_RecursiveDeref(dd, v[i]);
00800             Cudd_RecursiveDeref(dd, z[i]);
00801         }
00802         FREE(x);
00803         FREE(v);
00804         FREE(z);
00805     }
00806     return(1);
00807 
00808 } /* end of testWalsh */
00809 
00821 static int
00822 testIterators(
00823   DdManager *dd,
00824   DdNode *M,
00825   DdNode *C,
00826   int pr)
00827 {
00828     int *cube;
00829     CUDD_VALUE_TYPE value;
00830     DdGen *gen;
00831     int q;
00832 
00833     /* Test iterator for cubes. */
00834     if (pr>1) {
00835         (void) printf("Testing iterator on cubes:\n");
00836         Cudd_ForeachCube(dd,M,gen,cube,value) {
00837             for (q = 0; q < dd->size; q++) {
00838                 switch (cube[q]) {
00839                 case 0:
00840                     (void) printf("0");
00841                     break;
00842                 case 1:
00843                     (void) printf("1");
00844                     break;
00845                 case 2:
00846                     (void) printf("-");
00847                     break;
00848                 default:
00849                     (void) printf("?");
00850                 }
00851             }
00852             (void) printf(" %g\n",value);
00853         }
00854         (void) printf("\n");
00855     }
00856 
00857     if (pr>1) {
00858         (void) printf("Testing prime expansion of cubes:\n");
00859         if (!Cudd_bddPrintCover(dd,C,C)) return(0);
00860     }
00861 
00862     if (pr>1) {
00863         (void) printf("Testing iterator on primes (CNF):\n");
00864         Cudd_ForeachPrime(dd,Cudd_Not(C),Cudd_Not(C),gen,cube) {
00865             for (q = 0; q < dd->size; q++) {
00866                 switch (cube[q]) {
00867                 case 0:
00868                     (void) printf("1");
00869                     break;
00870                 case 1:
00871                     (void) printf("0");
00872                     break;
00873                 case 2:
00874                     (void) printf("-");
00875                     break;
00876                 default:
00877                     (void) printf("?");
00878                 }
00879             }
00880             (void) printf(" 1\n");
00881         }
00882         (void) printf("\n");
00883     }
00884 
00885     /* Test iterator on nodes. */
00886     if (pr>2) {
00887         DdNode *node;
00888         (void) printf("Testing iterator on nodes:\n");
00889         Cudd_ForeachNode(dd,M,gen,node) {
00890             if (Cudd_IsConstant(node)) {
00891 #if SIZEOF_VOID_P == 8
00892                 (void) printf("ID = 0x%lx\tvalue = %-9g\n",
00893                               (ptruint) node /
00894                               (ptruint) sizeof(DdNode),
00895                               Cudd_V(node));
00896 #else
00897                 (void) printf("ID = 0x%x\tvalue = %-9g\n",
00898                               (ptruint) node /
00899                               (ptruint) sizeof(DdNode),
00900                               Cudd_V(node));
00901 #endif
00902             } else {
00903 #if SIZEOF_VOID_P == 8
00904                 (void) printf("ID = 0x%lx\tindex = %u\tr = %u\n",
00905                               (ptruint) node /
00906                               (ptruint) sizeof(DdNode),
00907                               node->index, node->ref);
00908 #else
00909                 (void) printf("ID = 0x%x\tindex = %u\tr = %u\n",
00910                               (ptruint) node /
00911                               (ptruint) sizeof(DdNode),
00912                               node->index, node->ref);
00913 #endif
00914             }
00915         }
00916         (void) printf("\n");
00917     }
00918     return(1);
00919 
00920 } /* end of testIterators */
00921 
00922 
00937 static int
00938 testXor(DdManager *dd, DdNode *f, int pr, int nvars)
00939 {
00940     DdNode *f1, *f0, *res1, *res2;
00941     int x;
00942 
00943     /* Extract cofactors w.r.t. mid variable. */
00944     x = nvars / 2;
00945     f1 = Cudd_Cofactor(dd,f,dd->vars[x]);
00946     if (f1 == NULL) return(0);
00947     Cudd_Ref(f1);
00948 
00949     f0 = Cudd_Cofactor(dd,f,Cudd_Not(dd->vars[x]));
00950     if (f0 == NULL) {
00951         Cudd_RecursiveDeref(dd,f1);
00952         return(0);
00953     }
00954     Cudd_Ref(f0);
00955 
00956     /* Compute XOR of cofactors with ITE. */
00957     res1 = Cudd_bddIte(dd,f1,Cudd_Not(f0),f0);
00958     if (res1 == NULL) return(0);
00959     Cudd_Ref(res1);
00960 
00961     if (pr>0) {(void) printf("xor1"); Cudd_PrintDebug(dd,res1,nvars,pr);}
00962 
00963     /* Compute XOR of cofactors with XOR. */
00964     res2 = Cudd_bddXor(dd,f1,f0);
00965     if (res2 == NULL) {
00966         Cudd_RecursiveDeref(dd,res1);
00967         return(0);
00968     }
00969     Cudd_Ref(res2);
00970 
00971     if (res1 != res2) {
00972         if (pr>0) {(void) printf("xor2"); Cudd_PrintDebug(dd,res2,nvars,pr);}
00973         Cudd_RecursiveDeref(dd,res1);
00974         Cudd_RecursiveDeref(dd,res2);
00975         return(0);
00976     }
00977     Cudd_RecursiveDeref(dd,res1);
00978     Cudd_RecursiveDeref(dd,f1);
00979     Cudd_RecursiveDeref(dd,f0);
00980 
00981     /* Compute boolean difference directly. */
00982     res1 = Cudd_bddBooleanDiff(dd,f,x);
00983     if (res1 == NULL) {
00984         Cudd_RecursiveDeref(dd,res2);
00985         return(0);
00986     }
00987     Cudd_Ref(res1);
00988 
00989     if (res1 != res2) {
00990         if (pr>0) {(void) printf("xor3"); Cudd_PrintDebug(dd,res1,nvars,pr);}
00991         Cudd_RecursiveDeref(dd,res1);
00992         Cudd_RecursiveDeref(dd,res2);
00993         return(0);
00994     }
00995     Cudd_RecursiveDeref(dd,res1);
00996     Cudd_RecursiveDeref(dd,res2);
00997     return(1);
00998 
00999 } /* end of testXor */
01000 
01001 
01014 static int
01015 testHamming(
01016   DdManager *dd,
01017   DdNode *f,
01018   int pr)
01019 {
01020     DdNode **vars, *minBdd, *zero, *scan;
01021     int i;
01022     int d;
01023     int *minterm;
01024     int size = Cudd_ReadSize(dd);
01025 
01026     vars = ALLOC(DdNode *, size);
01027     if (vars == NULL) return(0);
01028     for (i = 0; i < size; i++) {
01029         vars[i] = Cudd_bddIthVar(dd,i);
01030     }
01031 
01032     minBdd = Cudd_bddPickOneMinterm(dd,Cudd_Not(f),vars,size);
01033     Cudd_Ref(minBdd);
01034     if (pr > 0) {
01035         (void) printf("Chosen minterm for Hamming distance test: ");
01036         Cudd_PrintDebug(dd,minBdd,size,pr);
01037     }
01038 
01039     minterm = ALLOC(int,size);
01040     if (minterm == NULL) {
01041         FREE(vars);
01042         Cudd_RecursiveDeref(dd,minBdd);
01043         return(0);
01044     }
01045     scan = minBdd;
01046     zero = Cudd_Not(DD_ONE(dd));
01047     while (!Cudd_IsConstant(scan)) {
01048         DdNode *R = Cudd_Regular(scan);
01049         DdNode *T = Cudd_T(R);
01050         DdNode *E = Cudd_E(R);
01051         if (R != scan) {
01052             T = Cudd_Not(T);
01053             E = Cudd_Not(E);
01054         }
01055         if (T == zero) {
01056             minterm[R->index] = 0;
01057             scan = E;
01058         } else {
01059             minterm[R->index] = 1;
01060             scan = T;
01061         }
01062     }
01063     Cudd_RecursiveDeref(dd,minBdd);
01064 
01065     d = Cudd_MinHammingDist(dd,f,minterm,size);
01066 
01067     (void) printf("Minimum Hamming distance = %d\n", d);
01068 
01069     FREE(vars);
01070     FREE(minterm);
01071     return(1);
01072 
01073 } /* end of testHamming */