src/bdd/cudd/testcudd.c File Reference

#include "util_hack.h"
#include "cuddInt.h"
Include dependency graph for testcudd.c:

Go to the source code of this file.

Defines

#define TESTCUDD_VERSION   "TestCudd Version #1.0, Release date 3/17/01"

Functions

static void usage ARGS ((char *prog))
static FILE *open_file ARGS ((char *filename, char *mode))
static int testIterators ARGS ((DdManager *dd, DdNode *M, DdNode *C, int pr))
static int testXor ARGS ((DdManager *dd, DdNode *f, int pr, int nvars))
static int testWalsh ARGS ((DdManager *dd, int N, int cmu, int approach, int pr))
int main (int argc, char **argv)
static void usage (char *prog)
static FILE * open_file (char *filename, char *mode)
static int testWalsh (DdManager *dd, int N, int cmu, int approach, int pr)
static int testIterators (DdManager *dd, DdNode *M, DdNode *C, int pr)
static int testXor (DdManager *dd, DdNode *f, int pr, int nvars)
static int testHamming (DdManager *dd, DdNode *f, int pr, int nvars)

Variables

static char rcsid[] DD_UNUSED = "$Id: testcudd.c,v 1.1.1.1 2003/02/24 22:23:54 wjiang Exp $"
static char * onames [] = { "C", "M" }

Define Documentation

#define TESTCUDD_VERSION   "TestCudd Version #1.0, Release date 3/17/01"

CFile***********************************************************************

FileName [testcudd.c]

PackageName [cudd]

Synopsis [Sanity check tests for some CUDD functions.]

Description [testcudd reads a matrix with real coefficients and transforms it into an ADD. It then performs various operations on the ADD and on the BDD corresponding to the ADD pattern. Finally, testcudd tests functions relate to Walsh matrices and matrix multiplication.]

SeeAlso []

Author [Fabio Somenzi]

Copyright [ This file was created at the University of Colorado at Boulder. The University of Colorado at Boulder makes no warranty about the suitability of this software for any purpose. It is presented on an AS IS basis.]

Definition at line 34 of file testcudd.c.

Function Documentation

static int testWalsh ARGS ( (DdManager *dd, int N, int cmu, int approach, int pr)   )  [static]
static int testHamming ARGS ( (DdManager *dd, DdNode *f, int pr, int nvars)   )  [static]
static int testIterators ARGS ( (DdManager *dd, DdNode *M, DdNode *C, int pr)   )  [static]
static FILE* open_file ARGS ( (char *filename, char *mode)   )  [static]
static void usage ARGS ( (char *prog)   )  [static]

AutomaticStart

int main ( int  argc,
char **  argv 
)

AutomaticEnd Function********************************************************************

Synopsis [Main function for testcudd.]

Description []

SideEffects [None]

SeeAlso []

Definition at line 74 of file testcudd.c.

00075 {
00076     FILE *fp;           /* pointer to input file */
00077     char *file = "";    /* input file name */
00078     FILE *dfp = NULL;   /* pointer to dump file */
00079     char *dfile;        /* file for DD dump */
00080     DdNode *dfunc[2];   /* addresses of the functions to be dumped */
00081     DdManager *dd;      /* pointer to DD manager */
00082     DdNode *one, *zero; /* fast access to constant functions */
00083     DdNode *M;
00084     DdNode **x;         /* pointers to variables */
00085     DdNode **y;         /* pointers to variables */
00086     DdNode **xn;        /* complements of row variables */
00087     DdNode **yn_;       /* complements of column variables */
00088     DdNode **xvars;
00089     DdNode **yvars;
00090     DdNode *C;          /* result of converting from ADD to BDD */
00091     DdNode *ess;        /* cube of essential variables */
00092     DdNode *shortP;     /* BDD cube of shortest path */
00093     DdNode *largest;    /* BDD of largest cube */
00094     DdNode *shortA;     /* ADD cube of shortest path */
00095     DdNode *constN;     /* value returned by evaluation of ADD */
00096     DdNode *ycube;      /* cube of the negated y vars for c-proj */
00097     DdNode *CP;         /* C-Projection of C */
00098     DdNode *CPr;        /* C-Selection of C */
00099     int    length;      /* length of the shortest path */
00100     int    nx;                  /* number of variables */
00101     int    ny;
00102     int    maxnx;
00103     int    maxny;
00104     int    m;
00105     int    n;
00106     int    N;
00107     int    cmu;                 /* use CMU multiplication */
00108     int    pr;                  /* verbose printout level */
00109     int    harwell;
00110     int    multiple;            /* read multiple matrices */
00111     int    ok;
00112     int    c;                   /* variable to read in options */
00113     int    approach;            /* reordering approach */
00114     int    autodyn;             /* automatic reordering */
00115     int    groupcheck;          /* option for group sifting */
00116     int    profile;             /* print heap profile if != 0 */
00117     int    keepperm;            /* keep track of permutation */
00118     int    clearcache;          /* clear the cache after each matrix */
00119     int    blifOrDot;           /* dump format: 0 -> dot, 1 -> blif, ... */
00120     int    retval;              /* return value */
00121     int    i;                   /* loop index */
00122     long   startTime;           /* initial time */
00123     long   lapTime;
00124     int    size;
00125     unsigned int cacheSize, maxMemory;
00126     unsigned int nvars,nslots;
00127 
00128     startTime = util_cpu_time();
00129 
00130     approach = CUDD_REORDER_NONE;
00131     autodyn = 0;
00132     pr = 0;
00133     harwell = 0;
00134     multiple = 0;
00135     profile = 0;
00136     keepperm = 0;
00137     cmu = 0;
00138     N = 4;
00139     nvars = 4;
00140     cacheSize = 127;
00141     maxMemory = 0;
00142     nslots = CUDD_UNIQUE_SLOTS;
00143     clearcache = 0;
00144     groupcheck = CUDD_GROUP_CHECK7;
00145     dfile = NULL;
00146     blifOrDot = 0; /* dot format */
00147 
00148     /* Parse command line. */
00149     while ((c = util_getopt(argc, argv, "CDHMPS:a:bcd:g:hkmn:p:v:x:X:"))
00150            != EOF) {
00151         switch(c) {
00152         case 'C':
00153             cmu = 1;
00154             break;
00155         case 'D':
00156             autodyn = 1;
00157             break;
00158         case 'H':
00159             harwell = 1;
00160             break;
00161         case 'M':
00162 #ifdef MNEMOSYNE
00163             (void) mnem_setrecording(0);
00164 #endif
00165             break;
00166         case 'P':
00167             profile = 1;
00168             break;
00169         case 'S':
00170             nslots = atoi(util_optarg);
00171             break;
00172         case 'X':
00173             maxMemory = atoi(util_optarg);
00174             break;
00175         case 'a':
00176             approach = atoi(util_optarg);
00177             break;
00178         case 'b':
00179             blifOrDot = 1; /* blif format */
00180             break;
00181         case 'c':
00182             clearcache = 1;
00183             break;
00184         case 'd':
00185             dfile = util_optarg;
00186             break;
00187         case 'g':
00188             groupcheck = atoi(util_optarg);
00189             break;
00190         case 'k':
00191             keepperm = 1;
00192             break;
00193         case 'm':
00194             multiple = 1;
00195             break;
00196         case 'n':
00197             N = atoi(util_optarg);
00198             break;
00199         case 'p':
00200             pr = atoi(util_optarg);
00201             break;
00202         case 'v':
00203             nvars = atoi(util_optarg);
00204             break;
00205         case 'x':
00206             cacheSize = atoi(util_optarg);
00207             break;
00208         case 'h':
00209         default:
00210             usage(argv[0]);
00211             break;
00212         }
00213     }
00214 
00215     if (argc - util_optind == 0) {
00216         file = "-";
00217     } else if (argc - util_optind == 1) {
00218         file = argv[util_optind];
00219     } else {
00220         usage(argv[0]);
00221     }
00222     if ((approach<0) || (approach>17)) {
00223         (void) fprintf(stderr,"Invalid approach: %d \n",approach);
00224         usage(argv[0]);
00225     }
00226 
00227     if (pr >= 0) {
00228         (void) printf("# %s\n", TESTCUDD_VERSION);
00229         /* Echo command line and arguments. */
00230         (void) printf("#");
00231         for (i = 0; i < argc; i++) {
00232             (void) printf(" %s", argv[i]);
00233         }
00234         (void) printf("\n");
00235         (void) fflush(stdout);
00236     }
00237 
00238     /* Initialize manager and provide easy reference to terminals. */
00239     dd = Cudd_Init(nvars,0,nslots,cacheSize,maxMemory);
00240     one = DD_ONE(dd);
00241     zero = DD_ZERO(dd);
00242     dd->groupcheck = (Cudd_AggregationType) groupcheck;
00243     if (autodyn) Cudd_AutodynEnable(dd,CUDD_REORDER_SAME);
00244 
00245     /* Open input file. */
00246     fp = open_file(file, "r");
00247 
00248     /* Open dump file if requested */
00249     if (dfile != NULL) {
00250         dfp = open_file(dfile, "w");
00251     }
00252 
00253     x = y = xn = yn_ = NULL;
00254     do {
00255         /* We want to start anew for every matrix. */
00256         maxnx = maxny = 0;
00257         nx = maxnx; ny = maxny;
00258         if (pr>0) lapTime = util_cpu_time();
00259         if (harwell) {
00260             if (pr >= 0) (void) printf(":name: ");
00261             ok = Cudd_addHarwell(fp, dd, &M, &x, &y, &xn, &yn_, &nx, &ny,
00262             &m, &n, 0, 2, 1, 2, pr);
00263         } else {
00264             ok = Cudd_addRead(fp, dd, &M, &x, &y, &xn, &yn_, &nx, &ny,
00265             &m, &n, 0, 2, 1, 2);
00266             if (pr >= 0)
00267                 (void) printf(":name: %s: %d rows %d columns\n", file, m, n);
00268         }
00269         if (!ok) {
00270             (void) fprintf(stderr, "Error reading matrix\n");
00271             exit(1);
00272         }
00273 
00274         if (nx > maxnx) maxnx = nx;
00275         if (ny > maxny) maxny = ny;
00276 
00277         /* Build cube of negated y's. */
00278         ycube = DD_ONE(dd);
00279         Cudd_Ref(ycube);
00280         for (i = maxny - 1; i >= 0; i--) {
00281             DdNode *tmpp;
00282             tmpp = Cudd_bddAnd(dd,Cudd_Not(dd->vars[y[i]->index]),ycube);
00283             if (tmpp == NULL) exit(2);
00284             Cudd_Ref(tmpp);
00285             Cudd_RecursiveDeref(dd,ycube);
00286             ycube = tmpp;
00287         }
00288         /* Initialize vectors of BDD variables used by priority func. */
00289         xvars = ALLOC(DdNode *, nx);
00290         if (xvars == NULL) exit(2);
00291         for (i = 0; i < nx; i++) {
00292             xvars[i] = dd->vars[x[i]->index];
00293         }
00294         yvars = ALLOC(DdNode *, ny);
00295         if (yvars == NULL) exit(2);
00296         for (i = 0; i < ny; i++) {
00297             yvars[i] = dd->vars[y[i]->index];
00298         }
00299 
00300         /* Clean up */
00301         for (i=0; i < maxnx; i++) {
00302             Cudd_RecursiveDeref(dd, x[i]);
00303             Cudd_RecursiveDeref(dd, xn[i]);
00304         }
00305         FREE(x);
00306         FREE(xn);
00307         for (i=0; i < maxny; i++) {
00308             Cudd_RecursiveDeref(dd, y[i]);
00309             Cudd_RecursiveDeref(dd, yn_[i]);
00310         }
00311         FREE(y);
00312         FREE(yn_);
00313 
00314         if (pr>0) {(void) printf(":1: M"); Cudd_PrintDebug(dd,M,nx+ny,pr);}
00315 
00316         if (pr>0) (void) printf(":2: time to read the matrix = %s\n",
00317                     util_print_time(util_cpu_time() - lapTime));
00318 
00319         C = Cudd_addBddPattern(dd, M);
00320         if (C == 0) exit(2);
00321         Cudd_Ref(C);
00322         if (pr>0) {(void) printf(":3: C"); Cudd_PrintDebug(dd,C,nx+ny,pr);}
00323 
00324         /* Test iterators. */
00325         retval = testIterators(dd,M,C,pr);
00326         if (retval == 0) exit(2);
00327 
00328         cuddCacheProfile(dd,stdout);
00329 
00330         /* Test XOR */
00331         retval = testXor(dd,C,pr,nx+ny);
00332         if (retval == 0) exit(2);
00333 
00334         /* Test Hamming distance functions. */
00335         retval = testHamming(dd,C,pr,nx+ny);
00336         if (retval == 0) exit(2);
00337 
00338         /* Test selection functions. */
00339         CP = Cudd_CProjection(dd,C,ycube);
00340         if (CP == NULL) exit(2);
00341         Cudd_Ref(CP);
00342         if (pr>0) {(void) printf("ycube"); Cudd_PrintDebug(dd,ycube,nx+ny,pr);}
00343         if (pr>0) {(void) printf("CP"); Cudd_PrintDebug(dd,CP,nx+ny,pr);}
00344 
00345         if (nx == ny) {
00346             CPr = Cudd_PrioritySelect(dd,C,xvars,yvars,(DdNode **)NULL,
00347                 (DdNode *)NULL,ny,Cudd_Xgty);
00348             if (CPr == NULL) exit(2);
00349             Cudd_Ref(CPr);
00350             if (pr>0) {(void) printf(":4: CPr"); Cudd_PrintDebug(dd,CPr,nx+ny,pr);}
00351             if (CP != CPr) {
00352                 (void) printf("CP != CPr!\n");
00353             }
00354             Cudd_RecursiveDeref(dd, CPr);
00355         }
00356         FREE(xvars); FREE(yvars);
00357 
00358         Cudd_RecursiveDeref(dd, CP);
00359         Cudd_RecursiveDeref(dd, ycube);
00360 
00361         /* Test functions for essential variables. */
00362         ess = Cudd_FindEssential(dd,C);
00363         if (ess == NULL) exit(2);
00364         Cudd_Ref(ess);
00365         if (pr>0) {(void) printf(":4: ess"); Cudd_PrintDebug(dd,ess,nx+ny,pr);}
00366         Cudd_RecursiveDeref(dd, ess);
00367 
00368         /* Test functions for shortest paths. */
00369         shortP = Cudd_ShortestPath(dd, M, NULL, NULL, &length);
00370         if (shortP == NULL) exit(2);
00371         Cudd_Ref(shortP);
00372         if (pr>0) {
00373             (void) printf(":5: shortP"); Cudd_PrintDebug(dd,shortP,nx+ny,pr);
00374         }
00375         /* Test functions for largest cubes. */
00376         largest = Cudd_LargestCube(dd, Cudd_Not(C), &length);
00377         if (largest == NULL) exit(2);
00378         Cudd_Ref(largest);
00379         if (pr>0) {
00380             (void) printf(":5b: largest");
00381             Cudd_PrintDebug(dd,largest,nx+ny,pr);
00382         }
00383         Cudd_RecursiveDeref(dd, largest);
00384 
00385         /* Test Cudd_addEvalConst and Cudd_addIteConstant. */
00386         shortA = Cudd_BddToAdd(dd,shortP);
00387         if (shortA == NULL) exit(2);
00388         Cudd_Ref(shortA);
00389         Cudd_RecursiveDeref(dd, shortP);
00390         constN = Cudd_addEvalConst(dd,shortA,M);
00391         if (constN == DD_NON_CONSTANT) exit(2);
00392         if (Cudd_addIteConstant(dd,shortA,M,constN) != constN) exit(2);
00393         if (pr>0) {(void) printf("The value of M along the chosen shortest path is %g\n", cuddV(constN));}
00394         Cudd_RecursiveDeref(dd, shortA);
00395 
00396         shortP = Cudd_ShortestPath(dd, C, NULL, NULL, &length);
00397         if (shortP == NULL) exit(2);
00398         Cudd_Ref(shortP);
00399         if (pr>0) {
00400             (void) printf(":6: shortP"); Cudd_PrintDebug(dd,shortP,nx+ny,pr);
00401         }
00402 
00403         /* Test Cudd_bddIteConstant and Cudd_bddLeq. */
00404         if (!Cudd_bddLeq(dd,shortP,C)) exit(2);
00405         if (Cudd_bddIteConstant(dd,Cudd_Not(shortP),one,C) != one) exit(2);
00406         Cudd_RecursiveDeref(dd, shortP);
00407 
00408         if (profile) {
00409             retval = cuddHeapProfile(dd);
00410         }
00411 
00412         size = dd->size;
00413 
00414         if (pr>0) {
00415             (void) printf("Average distance: %g\n", Cudd_AverageDistance(dd));
00416         }
00417 
00418         /* Reorder if so requested. */
00419         if (approach != CUDD_REORDER_NONE) {
00420 #ifndef DD_STATS
00421             retval = Cudd_EnableReorderingReporting(dd);
00422             if (retval == 0) {
00423                 (void) fprintf(stderr,"Error reported by Cudd_EnableReorderingReporting\n");
00424                 exit(3);
00425             }
00426 #endif
00427 #ifdef DD_DEBUG
00428             retval = Cudd_DebugCheck(dd);
00429             if (retval != 0) {
00430                 (void) fprintf(stderr,"Error reported by Cudd_DebugCheck\n");
00431                 exit(3);
00432             }
00433             retval = Cudd_CheckKeys(dd);
00434             if (retval != 0) {
00435                 (void) fprintf(stderr,"Error reported by Cudd_CheckKeys\n");
00436                 exit(3);
00437             }
00438 #endif
00439             retval = Cudd_ReduceHeap(dd,(Cudd_ReorderingType)approach,5);
00440             if (retval == 0) {
00441                 (void) fprintf(stderr,"Error reported by Cudd_ReduceHeap\n");
00442                 exit(3);
00443             }
00444 #ifndef DD_STATS
00445             retval = Cudd_DisableReorderingReporting(dd);
00446             if (retval == 0) {
00447                 (void) fprintf(stderr,"Error reported by Cudd_DisableReorderingReporting\n");
00448                 exit(3);
00449             }
00450 #endif
00451 #ifdef DD_DEBUG
00452             retval = Cudd_DebugCheck(dd);
00453             if (retval != 0) {
00454                 (void) fprintf(stderr,"Error reported by Cudd_DebugCheck\n");
00455                 exit(3);
00456             }
00457             retval = Cudd_CheckKeys(dd);
00458             if (retval != 0) {
00459                 (void) fprintf(stderr,"Error reported by Cudd_CheckKeys\n");
00460                 exit(3);
00461             }
00462 #endif
00463             if (approach == CUDD_REORDER_SYMM_SIFT ||
00464             approach == CUDD_REORDER_SYMM_SIFT_CONV) {
00465                 Cudd_SymmProfile(dd,0,dd->size-1);
00466             }
00467 
00468             if (pr>0) {
00469                 (void) printf("Average distance: %g\n", Cudd_AverageDistance(dd));
00470             }
00471 
00472             if (keepperm) {
00473                 /* Print variable permutation. */
00474                 (void) printf("Variable Permutation:");
00475                 for (i=0; i<size; i++) {
00476                     if (i%20 == 0) (void) printf("\n");
00477                     (void) printf("%d ", dd->invperm[i]);
00478                 }
00479                 (void) printf("\n");
00480                 (void) printf("Inverse Permutation:");
00481                 for (i=0; i<size; i++) {
00482                     if (i%20 == 0) (void) printf("\n");
00483                     (void) printf("%d ", dd->perm[i]);
00484                 }
00485                 (void) printf("\n");
00486             }
00487 
00488             if (pr>0) {(void) printf("M"); Cudd_PrintDebug(dd,M,nx+ny,pr);}
00489 
00490             if (profile) {
00491                 retval = cuddHeapProfile(dd);
00492             }
00493 
00494         }
00495 
00496         /* Dump DDs of C and M if so requested. */
00497         if (dfile != NULL) {
00498             dfunc[0] = C;
00499             dfunc[1] = M;
00500             if (blifOrDot == 1) {
00501                 /* Only dump C because blif cannot handle ADDs */
00502                 retval = Cudd_DumpBlif(dd,1,dfunc,NULL,onames,NULL,dfp);
00503             } else {
00504                 retval = Cudd_DumpDot(dd,2,dfunc,NULL,onames,dfp);
00505             }
00506             if (retval != 1) {
00507                 (void) fprintf(stderr,"abnormal termination\n");
00508                 exit(2);
00509             }
00510         }
00511 
00512         Cudd_RecursiveDeref(dd, C);
00513         Cudd_RecursiveDeref(dd, M);
00514 
00515         if (clearcache) {
00516             if (pr>0) {(void) printf("Clearing the cache... ");}
00517             for (i = dd->cacheSlots - 1; i>=0; i--) {
00518                 dd->cache[i].data = NIL(DdNode);
00519             }
00520             if (pr>0) {(void) printf("done\n");}
00521         }
00522         if (pr>0) {
00523             (void) printf("Number of variables = %6d\t",dd->size);
00524             (void) printf("Number of slots     = %6d\n",dd->slots);
00525             (void) printf("Number of keys      = %6d\t",dd->keys);
00526             (void) printf("Number of min dead  = %6d\n",dd->minDead);
00527         }
00528 
00529     } while (multiple && !feof(fp));
00530 
00531     fclose(fp);
00532     if (dfile != NULL) {
00533         fclose(dfp);
00534     }
00535 
00536     /* Second phase: experiment with Walsh matrices. */
00537     if (!testWalsh(dd,N,cmu,approach,pr)) {
00538         exit(2);
00539     }
00540 
00541     /* Check variable destruction. */
00542     assert(cuddDestroySubtables(dd,3));
00543     assert(Cudd_DebugCheck(dd) == 0);
00544     assert(Cudd_CheckKeys(dd) == 0);
00545 
00546     retval = Cudd_CheckZeroRef(dd);
00547     ok = retval != 0;  /* ok == 0 means O.K. */
00548     if (retval != 0) {
00549         (void) fprintf(stderr,
00550             "%d non-zero DD reference counts after dereferencing\n", retval);
00551     }
00552 
00553     if (pr >= 0) {
00554         (void) Cudd_PrintInfo(dd,stdout);
00555     }
00556 
00557     Cudd_Quit(dd);
00558 
00559 #ifdef MNEMOSYNE
00560     mnem_writestats();
00561 #endif
00562 
00563     if (pr>0) (void) printf("total time = %s\n",
00564                 util_print_time(util_cpu_time() - startTime));
00565 
00566     if (pr >= 0) util_print_cpu_stats(stdout);
00567     exit(ok);
00568     /* NOTREACHED */
00569 
00570 } /* end of main */

static FILE* open_file ( char *  filename,
char *  mode 
) [static]

Function********************************************************************

Synopsis [Opens a file.]

Description [Opens a file, or fails with an error message and exits. Allows '-' as a synonym for standard input.]

SideEffects [None]

SeeAlso []

Definition at line 643 of file testcudd.c.

00644 {
00645     FILE *fp;
00646 
00647     if (strcmp(filename, "-") == 0) {
00648         return mode[0] == 'r' ? stdin : stdout;
00649     } else if ((fp = fopen(filename, mode)) == NULL) {
00650         perror(filename);
00651         exit(1);
00652     }
00653     return fp;
00654 
00655 } /* end of open_file */

static int testHamming ( DdManager *  dd,
DdNode *  f,
int  pr,
int  nvars 
) [static]

Function********************************************************************

Synopsis [Tests the Hamming distance functions.]

Description [Tests the Hammming distance functions. Returns 1 if successful; 0 otherwise.]

SideEffects [None]

SeeAlso []

Definition at line 929 of file testcudd.c.

00934 {
00935     DdNode **vars, *minBdd, *zero, *scan;
00936     int i;
00937     int d;
00938     int *minterm;
00939     int size = Cudd_ReadSize(dd);
00940 
00941     vars = ALLOC(DdNode *, size);
00942     if (vars == NULL) return(0);
00943     for (i = 0; i < size; i++) {
00944         vars[i] = Cudd_bddIthVar(dd,i);
00945     }
00946 
00947     minBdd = Cudd_bddPickOneMinterm(dd,Cudd_Not(f),vars,size);
00948     Cudd_Ref(minBdd);
00949     if (pr > 0) {
00950         (void) printf("Chosen minterm for Hamming distance test: ");
00951         Cudd_PrintDebug(dd,minBdd,size,pr);
00952     }
00953 
00954     minterm = ALLOC(int,size);
00955     if (minterm == NULL) {
00956         FREE(vars);
00957         Cudd_RecursiveDeref(dd,minBdd);
00958         return(0);
00959     }
00960     scan = minBdd;
00961     zero = Cudd_Not(DD_ONE(dd));
00962     while (!Cudd_IsConstant(scan)) {
00963         DdNode *R = Cudd_Regular(scan);
00964         DdNode *T = Cudd_T(R);
00965         DdNode *E = Cudd_E(R);
00966         if (R != scan) {
00967             T = Cudd_Not(T);
00968             E = Cudd_Not(E);
00969         }
00970         if (T == zero) {
00971             minterm[R->index] = 0;
00972             scan = E;
00973         } else {
00974             minterm[R->index] = 1;
00975             scan = T;
00976         }
00977     }
00978     Cudd_RecursiveDeref(dd,minBdd);
00979 
00980     d = Cudd_MinHammingDist(dd,f,minterm,size);
00981 
00982     (void) printf("Minimum Hamming distance = %d\n", d);
00983 
00984     FREE(vars);
00985     FREE(minterm);
00986     return(1);
00987 
00988 } /* end of testHamming */

static int testIterators ( DdManager *  dd,
DdNode *  M,
DdNode *  C,
int  pr 
) [static]

Function********************************************************************

Synopsis [Tests iterators.]

Description [Tests iterators on cubes and nodes.]

SideEffects [None]

SeeAlso []

Definition at line 758 of file testcudd.c.

00763 {
00764     int *cube;
00765     CUDD_VALUE_TYPE value;
00766     DdGen *gen;
00767     int q;
00768 
00769     /* Test iterator for cubes. */
00770     if (pr>1) {
00771         (void) printf("Testing iterator on cubes:\n");
00772         Cudd_ForeachCube(dd,M,gen,cube,value) {
00773             for (q = 0; q < dd->size; q++) {
00774                 switch (cube[q]) {
00775                 case 0:
00776                     (void) printf("0");
00777                     break;
00778                 case 1:
00779                     (void) printf("1");
00780                     break;
00781                 case 2:
00782                     (void) printf("-");
00783                     break;
00784                 default:
00785                     (void) printf("?");
00786                 }
00787             }
00788             (void) printf(" %g\n",value);
00789         }
00790         (void) printf("\n");
00791     }
00792 
00793     if (pr>1) {
00794         (void) printf("Testing prime expansion of cubes:\n");
00795         if (!Cudd_bddPrintCover(dd,C,C)) return(0);
00796     }
00797 
00798     /* Test iterator on nodes. */
00799     if (pr>2) {
00800         DdGen *gen;
00801         DdNode *node;
00802         (void) printf("Testing iterator on nodes:\n");
00803         Cudd_ForeachNode(dd,M,gen,node) {
00804             if (Cudd_IsConstant(node)) {
00805 #if SIZEOF_VOID_P == 8
00806                 (void) printf("ID = 0x%lx\tvalue = %-9g\n",
00807                               (unsigned long) node /
00808                               (unsigned long) sizeof(DdNode),
00809                               Cudd_V(node));
00810 #else
00811                 (void) printf("ID = 0x%x\tvalue = %-9g\n",
00812                               (unsigned int) node /
00813                               (unsigned int) sizeof(DdNode),
00814                               Cudd_V(node));
00815 #endif
00816             } else {
00817 #if SIZEOF_VOID_P == 8
00818                 (void) printf("ID = 0x%lx\tindex = %d\tr = %d\n",
00819                               (unsigned long) node /
00820                               (unsigned long) sizeof(DdNode),
00821                               node->index, node->ref);
00822 #else
00823                 (void) printf("ID = 0x%x\tindex = %d\tr = %d\n",
00824                               (unsigned int) node /
00825                               (unsigned int) sizeof(DdNode),
00826                               node->index, node->ref);
00827 #endif
00828             }
00829         }
00830         (void) printf("\n");
00831     }
00832     return(1);
00833 
00834 } /* end of testIterators */

static int testWalsh ( DdManager *  dd,
int  N,
int  cmu,
int  approach,
int  pr 
) [static]

Function********************************************************************

Synopsis [Tests Walsh matrix multiplication.]

Description [Tests Walsh matrix multiplication. Return 1 if successful; 0 otherwise.]

SideEffects [May create new variables in the manager.]

SeeAlso []

Definition at line 671 of file testcudd.c.

00677 {
00678     DdNode *walsh1, *walsh2, *wtw;
00679     DdNode **x, **v, **z;
00680     int i, retval;
00681     DdNode *one = DD_ONE(dd);
00682     DdNode *zero = DD_ZERO(dd);
00683 
00684     if (N > 3) {
00685         x = ALLOC(DdNode *,N);
00686         v = ALLOC(DdNode *,N);
00687         z = ALLOC(DdNode *,N);
00688 
00689         for (i = N-1; i >= 0; i--) {
00690             Cudd_Ref(x[i]=cuddUniqueInter(dd,3*i,one,zero));
00691             Cudd_Ref(v[i]=cuddUniqueInter(dd,3*i+1,one,zero));
00692             Cudd_Ref(z[i]=cuddUniqueInter(dd,3*i+2,one,zero));
00693         }
00694         Cudd_Ref(walsh1 = Cudd_addWalsh(dd,v,z,N));
00695         if (pr>0) {(void) printf("walsh1"); Cudd_PrintDebug(dd,walsh1,2*N,pr);}
00696         Cudd_Ref(walsh2 = Cudd_addWalsh(dd,x,v,N));
00697         if (cmu) {
00698             Cudd_Ref(wtw = Cudd_addTimesPlus(dd,walsh2,walsh1,v,N));
00699         } else {
00700             Cudd_Ref(wtw = Cudd_addMatrixMultiply(dd,walsh2,walsh1,v,N));
00701         }
00702         if (pr>0) {(void) printf("wtw"); Cudd_PrintDebug(dd,wtw,2*N,pr);}
00703 
00704         if (approach != CUDD_REORDER_NONE) {
00705 #ifdef DD_DEBUG
00706             retval = Cudd_DebugCheck(dd);
00707             if (retval != 0) {
00708                 (void) fprintf(stderr,"Error reported by Cudd_DebugCheck\n");
00709                 return(0);
00710             }
00711 #endif
00712             retval = Cudd_ReduceHeap(dd,(Cudd_ReorderingType)approach,5);
00713             if (retval == 0) {
00714                 (void) fprintf(stderr,"Error reported by Cudd_ReduceHeap\n");
00715                 return(0);
00716             }
00717 #ifdef DD_DEBUG
00718             retval = Cudd_DebugCheck(dd);
00719             if (retval != 0) {
00720                 (void) fprintf(stderr,"Error reported by Cudd_DebugCheck\n");
00721                 return(0);
00722             }
00723 #endif
00724             if (approach == CUDD_REORDER_SYMM_SIFT ||
00725             approach == CUDD_REORDER_SYMM_SIFT_CONV) {
00726                 Cudd_SymmProfile(dd,0,dd->size-1);
00727             }
00728         }
00729         /* Clean up. */
00730         Cudd_RecursiveDeref(dd, wtw);
00731         Cudd_RecursiveDeref(dd, walsh1);
00732         Cudd_RecursiveDeref(dd, walsh2);
00733         for (i=0; i < N; i++) {
00734             Cudd_RecursiveDeref(dd, x[i]);
00735             Cudd_RecursiveDeref(dd, v[i]);
00736             Cudd_RecursiveDeref(dd, z[i]);
00737         }
00738         FREE(x);
00739         FREE(v);
00740         FREE(z);
00741     }
00742     return(1);
00743 
00744 } /* end of testWalsh */

static int testXor ( DdManager *  dd,
DdNode *  f,
int  pr,
int  nvars 
) [static]

Function********************************************************************

Synopsis [Tests the functions related to the exclusive OR.]

Description [Tests the functions related to the exclusive OR. It builds the boolean difference of the given function in three different ways and checks that the results is the same. Returns 1 if successful; 0 otherwise.]

SideEffects [None]

SeeAlso []

Definition at line 852 of file testcudd.c.

00853 {
00854     DdNode *f1, *f0, *res1, *res2;
00855     int x;
00856 
00857     /* Extract cofactors w.r.t. mid variable. */
00858     x = nvars / 2;
00859     f1 = Cudd_Cofactor(dd,f,dd->vars[x]);
00860     if (f1 == NULL) return(0);
00861     Cudd_Ref(f1);
00862 
00863     f0 = Cudd_Cofactor(dd,f,Cudd_Not(dd->vars[x]));
00864     if (f0 == NULL) {
00865         Cudd_RecursiveDeref(dd,f1);
00866         return(0);
00867     }
00868     Cudd_Ref(f0);
00869 
00870     /* Compute XOR of cofactors with ITE. */
00871     res1 = Cudd_bddIte(dd,f1,Cudd_Not(f0),f0);
00872     if (res1 == NULL) return(0);
00873     Cudd_Ref(res1);
00874 
00875     if (pr>0) {(void) printf("xor1"); Cudd_PrintDebug(dd,res1,nvars,pr);}
00876 
00877     /* Compute XOR of cofactors with XOR. */
00878     res2 = Cudd_bddXor(dd,f1,f0);
00879     if (res2 == NULL) {
00880         Cudd_RecursiveDeref(dd,res1);
00881         return(0);
00882     }
00883     Cudd_Ref(res2);
00884 
00885     if (res1 != res2) {
00886         if (pr>0) {(void) printf("xor2"); Cudd_PrintDebug(dd,res2,nvars,pr);}
00887         Cudd_RecursiveDeref(dd,res1);
00888         Cudd_RecursiveDeref(dd,res2);
00889         return(0);
00890     }
00891     Cudd_RecursiveDeref(dd,res1);
00892     Cudd_RecursiveDeref(dd,f1);
00893     Cudd_RecursiveDeref(dd,f0);
00894 
00895     /* Compute boolean difference directly. */
00896     res1 = Cudd_bddBooleanDiff(dd,f,x);
00897     if (res1 == NULL) {
00898         Cudd_RecursiveDeref(dd,res2);
00899         return(0);
00900     }
00901     Cudd_Ref(res1);
00902 
00903     if (res1 != res2) {
00904         if (pr>0) {(void) printf("xor3"); Cudd_PrintDebug(dd,res1,nvars,pr);}
00905         Cudd_RecursiveDeref(dd,res1);
00906         Cudd_RecursiveDeref(dd,res2);
00907         return(0);
00908     }
00909     Cudd_RecursiveDeref(dd,res1);
00910     Cudd_RecursiveDeref(dd,res2);
00911     return(1);
00912 
00913 } /* end of testXor */

static void usage ( char *  prog  )  [static]

Function********************************************************************

Synopsis [Prints usage info for testcudd.]

Description []

SideEffects [None]

SeeAlso []

Definition at line 590 of file testcudd.c.

00591 {
00592     (void) fprintf(stderr, "usage: %s [options] [file]\n", prog);
00593     (void) fprintf(stderr, "   -C\t\tuse CMU multiplication algorithm\n");
00594     (void) fprintf(stderr, "   -D\t\tenable automatic dynamic reordering\n");
00595     (void) fprintf(stderr, "   -H\t\tread matrix in Harwell format\n");
00596     (void) fprintf(stderr, "   -M\t\tturns off memory allocation recording\n");
00597     (void) fprintf(stderr, "   -P\t\tprint BDD heap profile\n");
00598     (void) fprintf(stderr, "   -S n\t\tnumber of slots for each subtable\n");
00599     (void) fprintf(stderr, "   -X n\t\ttarget maximum memory in bytes\n");
00600     (void) fprintf(stderr, "   -a n\t\tchoose reordering approach (0-13)\n");
00601     (void) fprintf(stderr, "   \t\t\t0: same as autoMethod\n");
00602     (void) fprintf(stderr, "   \t\t\t1: no reordering (default)\n");
00603     (void) fprintf(stderr, "   \t\t\t2: random\n");
00604     (void) fprintf(stderr, "   \t\t\t3: pivot\n");
00605     (void) fprintf(stderr, "   \t\t\t4: sifting\n");
00606     (void) fprintf(stderr, "   \t\t\t5: sifting to convergence\n");
00607     (void) fprintf(stderr, "   \t\t\t6: symmetric sifting\n");
00608     (void) fprintf(stderr, "   \t\t\t7: symmetric sifting to convergence\n");
00609     (void) fprintf(stderr, "   \t\t\t8-10: window of size 2-4\n");
00610     (void) fprintf(stderr, "   \t\t\t11-13: window of size 2-4 to conv.\n");
00611     (void) fprintf(stderr, "   \t\t\t14: group sifting\n");
00612     (void) fprintf(stderr, "   \t\t\t15: group sifting to convergence\n");
00613     (void) fprintf(stderr, "   \t\t\t16: simulated annealing\n");
00614     (void) fprintf(stderr, "   \t\t\t17: genetic algorithm\n");
00615     (void) fprintf(stderr, "   -b\t\tuse blif as format for dumps\n");
00616     (void) fprintf(stderr, "   -c\t\tclear the cache after each matrix\n");
00617     (void) fprintf(stderr, "   -d file\tdump DDs to file\n");
00618     (void) fprintf(stderr, "   -g\t\tselect aggregation criterion (0,5,7)\n");
00619     (void) fprintf(stderr, "   -h\t\tprints this message\n");
00620     (void) fprintf(stderr, "   -k\t\tprint the variable permutation\n");
00621     (void) fprintf(stderr, "   -m\t\tread multiple matrices (only with -H)\n");
00622     (void) fprintf(stderr, "   -n n\t\tnumber of variables\n");
00623     (void) fprintf(stderr, "   -p n\t\tcontrol verbosity\n");
00624     (void) fprintf(stderr, "   -v n\t\tinitial variables in the unique table\n");
00625     (void) fprintf(stderr, "   -x n\t\tinitial size of the cache\n");
00626     exit(2);
00627 } /* end of usage */

Variable Documentation

char rcsid [] DD_UNUSED = "$Id: testcudd.c,v 1.1.1.1 2003/02/24 22:23:54 wjiang Exp $" [static]

Definition at line 41 of file testcudd.c.

char* onames[] = { "C", "M" } [static]

Definition at line 44 of file testcudd.c.

Generated on Tue Jan 5 12:18:58 2010 for abc70930 by  doxygen 1.6.1