src/cuBdd/testcudd.c File Reference

#include "util.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 (char *prog)
static FILE * open_file (char *filename, const char *mode)
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)
static int testWalsh (DdManager *dd, int N, int cmu, int approach, int pr)
int main (int argc, char **argv)

Variables

static char rcsid[] DD_UNUSED = "$Id: testcudd.c,v 1.20 2009/03/08 02:49:02 fabio Exp $"
static const 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 [Copyright (c) 1995-2004, Regents of the University of Colorado

All rights reserved.

Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:

Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.

Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.

Neither the name of the University of Colorado nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.

THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.]

Definition at line 61 of file testcudd.c.

Function Documentation

int main ( int  argc,
char **  argv 
)

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

Synopsis [Main function for testcudd.]

Description []

SideEffects [None]

SeeAlso []

Definition at line 101 of file testcudd.c.

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 */

static FILE * open_file ( char *  filename,
const 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 707 of file testcudd.c.

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 */

static int testHamming ( DdManager *  dd,
DdNode *  f,
int  pr 
) [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 1015 of file testcudd.c.

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 */

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 822 of file testcudd.c.

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 */

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 735 of file testcudd.c.

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 */

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 938 of file testcudd.c.

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 */

static void usage ( char *  prog  )  [static]

AutomaticStart

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

Synopsis [Prints usage info for testcudd.]

Description []

SideEffects [None]

SeeAlso []

Definition at line 654 of file testcudd.c.

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 */

Variable Documentation

char rcsid [] DD_UNUSED = "$Id: testcudd.c,v 1.20 2009/03/08 02:49:02 fabio Exp $" [static]

Definition at line 68 of file testcudd.c.

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

Definition at line 71 of file testcudd.c.

Generated on Tue Jan 12 13:57:22 2010 for glu-2.2 by  doxygen 1.6.1