diff options
Diffstat (limited to 'src/bdd/cudd/testcudd.c')
| -rw-r--r-- | src/bdd/cudd/testcudd.c | 988 |
1 files changed, 0 insertions, 988 deletions
diff --git a/src/bdd/cudd/testcudd.c b/src/bdd/cudd/testcudd.c deleted file mode 100644 index d8affadc..00000000 --- a/src/bdd/cudd/testcudd.c +++ /dev/null @@ -1,988 +0,0 @@ -/**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.] - -******************************************************************************/ - -#include "util_hack.h" -#include "cuddInt.h" - - -/*---------------------------------------------------------------------------*/ -/* Constant declarations */ -/*---------------------------------------------------------------------------*/ - -#define TESTCUDD_VERSION "TestCudd Version #1.0, Release date 3/17/01" - -/*---------------------------------------------------------------------------*/ -/* Variable declarations */ -/*---------------------------------------------------------------------------*/ - -#ifndef lint -static char rcsid[] DD_UNUSED = "$Id: testcudd.c,v 1.1.1.1 2003/02/24 22:23:54 wjiang Exp $"; -#endif - -static char *onames[] = { "C", "M" }; /* names of functions to be dumped */ - -/**AutomaticStart*************************************************************/ - -/*---------------------------------------------------------------------------*/ -/* Static function prototypes */ -/*---------------------------------------------------------------------------*/ - -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 testHamming ARGS((DdManager *dd, DdNode *f, int pr, int nvars)); -static int testWalsh ARGS((DdManager *dd, int N, int cmu, int approach, int pr)); - -/**AutomaticEnd***************************************************************/ - - -/**Function******************************************************************** - - Synopsis [Main function for testcudd.] - - Description [] - - SideEffects [None] - - SeeAlso [] - -******************************************************************************/ -int -main(int argc, char **argv) -{ - FILE *fp; /* pointer to input file */ - char *file = ""; /* input file name */ - FILE *dfp = NULL; /* pointer to dump file */ - char *dfile; /* file for DD dump */ - DdNode *dfunc[2]; /* addresses of the functions to be dumped */ - DdManager *dd; /* pointer to DD manager */ - DdNode *one, *zero; /* fast access to constant functions */ - DdNode *M; - DdNode **x; /* pointers to variables */ - DdNode **y; /* pointers to variables */ - DdNode **xn; /* complements of row variables */ - DdNode **yn_; /* complements of column variables */ - DdNode **xvars; - DdNode **yvars; - DdNode *C; /* result of converting from ADD to BDD */ - DdNode *ess; /* cube of essential variables */ - DdNode *shortP; /* BDD cube of shortest path */ - DdNode *largest; /* BDD of largest cube */ - DdNode *shortA; /* ADD cube of shortest path */ - DdNode *constN; /* value returned by evaluation of ADD */ - DdNode *ycube; /* cube of the negated y vars for c-proj */ - DdNode *CP; /* C-Projection of C */ - DdNode *CPr; /* C-Selection of C */ - int length; /* length of the shortest path */ - int nx; /* number of variables */ - int ny; - int maxnx; - int maxny; - int m; - int n; - int N; - int cmu; /* use CMU multiplication */ - int pr; /* verbose printout level */ - int harwell; - int multiple; /* read multiple matrices */ - int ok; - int c; /* variable to read in options */ - int approach; /* reordering approach */ - int autodyn; /* automatic reordering */ - int groupcheck; /* option for group sifting */ - int profile; /* print heap profile if != 0 */ - int keepperm; /* keep track of permutation */ - int clearcache; /* clear the cache after each matrix */ - int blifOrDot; /* dump format: 0 -> dot, 1 -> blif, ... */ - int retval; /* return value */ - int i; /* loop index */ - long startTime; /* initial time */ - long lapTime; - int size; - unsigned int cacheSize, maxMemory; - unsigned int nvars,nslots; - - startTime = util_cpu_time(); - - approach = CUDD_REORDER_NONE; - autodyn = 0; - pr = 0; - harwell = 0; - multiple = 0; - profile = 0; - keepperm = 0; - cmu = 0; - N = 4; - nvars = 4; - cacheSize = 127; - maxMemory = 0; - nslots = CUDD_UNIQUE_SLOTS; - clearcache = 0; - groupcheck = CUDD_GROUP_CHECK7; - dfile = NULL; - blifOrDot = 0; /* dot format */ - - /* Parse command line. */ - while ((c = util_getopt(argc, argv, "CDHMPS:a:bcd:g:hkmn:p:v:x:X:")) - != EOF) { - switch(c) { - case 'C': - cmu = 1; - break; - case 'D': - autodyn = 1; - break; - case 'H': - harwell = 1; - break; - case 'M': -#ifdef MNEMOSYNE - (void) mnem_setrecording(0); -#endif - break; - case 'P': - profile = 1; - break; - case 'S': - nslots = atoi(util_optarg); - break; - case 'X': - maxMemory = atoi(util_optarg); - break; - case 'a': - approach = atoi(util_optarg); - break; - case 'b': - blifOrDot = 1; /* blif format */ - break; - case 'c': - clearcache = 1; - break; - case 'd': - dfile = util_optarg; - break; - case 'g': - groupcheck = atoi(util_optarg); - break; - case 'k': - keepperm = 1; - break; - case 'm': - multiple = 1; - break; - case 'n': - N = atoi(util_optarg); - break; - case 'p': - pr = atoi(util_optarg); - break; - case 'v': - nvars = atoi(util_optarg); - break; - case 'x': - cacheSize = atoi(util_optarg); - break; - case 'h': - default: - usage(argv[0]); - break; - } - } - - if (argc - util_optind == 0) { - file = "-"; - } else if (argc - util_optind == 1) { - file = argv[util_optind]; - } else { - usage(argv[0]); - } - if ((approach<0) || (approach>17)) { - (void) fprintf(stderr,"Invalid approach: %d \n",approach); - usage(argv[0]); - } - - if (pr >= 0) { - (void) printf("# %s\n", TESTCUDD_VERSION); - /* Echo command line and arguments. */ - (void) printf("#"); - for (i = 0; i < argc; i++) { - (void) printf(" %s", argv[i]); - } - (void) printf("\n"); - (void) fflush(stdout); - } - - /* Initialize manager and provide easy reference to terminals. */ - dd = Cudd_Init(nvars,0,nslots,cacheSize,maxMemory); - one = DD_ONE(dd); - zero = DD_ZERO(dd); - dd->groupcheck = (Cudd_AggregationType) groupcheck; - if (autodyn) Cudd_AutodynEnable(dd,CUDD_REORDER_SAME); - - /* Open input file. */ - fp = open_file(file, "r"); - - /* Open dump file if requested */ - if (dfile != NULL) { - dfp = open_file(dfile, "w"); - } - - x = y = xn = yn_ = NULL; - do { - /* We want to start anew for every matrix. */ - maxnx = maxny = 0; - nx = maxnx; ny = maxny; - if (pr>0) lapTime = util_cpu_time(); - if (harwell) { - if (pr >= 0) (void) printf(":name: "); - ok = Cudd_addHarwell(fp, dd, &M, &x, &y, &xn, &yn_, &nx, &ny, - &m, &n, 0, 2, 1, 2, pr); - } else { - ok = Cudd_addRead(fp, dd, &M, &x, &y, &xn, &yn_, &nx, &ny, - &m, &n, 0, 2, 1, 2); - if (pr >= 0) - (void) printf(":name: %s: %d rows %d columns\n", file, m, n); - } - if (!ok) { - (void) fprintf(stderr, "Error reading matrix\n"); - exit(1); - } - - if (nx > maxnx) maxnx = nx; - if (ny > maxny) maxny = ny; - - /* Build cube of negated y's. */ - ycube = DD_ONE(dd); - Cudd_Ref(ycube); - for (i = maxny - 1; i >= 0; i--) { - DdNode *tmpp; - tmpp = Cudd_bddAnd(dd,Cudd_Not(dd->vars[y[i]->index]),ycube); - if (tmpp == NULL) exit(2); - Cudd_Ref(tmpp); - Cudd_RecursiveDeref(dd,ycube); - ycube = tmpp; - } - /* Initialize vectors of BDD variables used by priority func. */ - xvars = ALLOC(DdNode *, nx); - if (xvars == NULL) exit(2); - for (i = 0; i < nx; i++) { - xvars[i] = dd->vars[x[i]->index]; - } - yvars = ALLOC(DdNode *, ny); - if (yvars == NULL) exit(2); - for (i = 0; i < ny; i++) { - yvars[i] = dd->vars[y[i]->index]; - } - - /* Clean up */ - for (i=0; i < maxnx; i++) { - Cudd_RecursiveDeref(dd, x[i]); - Cudd_RecursiveDeref(dd, xn[i]); - } - FREE(x); - FREE(xn); - for (i=0; i < maxny; i++) { - Cudd_RecursiveDeref(dd, y[i]); - Cudd_RecursiveDeref(dd, yn_[i]); - } - FREE(y); - FREE(yn_); - - if (pr>0) {(void) printf(":1: M"); Cudd_PrintDebug(dd,M,nx+ny,pr);} - - if (pr>0) (void) printf(":2: time to read the matrix = %s\n", - util_print_time(util_cpu_time() - lapTime)); - - C = Cudd_addBddPattern(dd, M); - if (C == 0) exit(2); - Cudd_Ref(C); - if (pr>0) {(void) printf(":3: C"); Cudd_PrintDebug(dd,C,nx+ny,pr);} - - /* Test iterators. */ - retval = testIterators(dd,M,C,pr); - if (retval == 0) exit(2); - - cuddCacheProfile(dd,stdout); - - /* Test XOR */ - retval = testXor(dd,C,pr,nx+ny); - if (retval == 0) exit(2); - - /* Test Hamming distance functions. */ - retval = testHamming(dd,C,pr,nx+ny); - if (retval == 0) exit(2); - - /* Test selection functions. */ - CP = Cudd_CProjection(dd,C,ycube); - if (CP == NULL) exit(2); - Cudd_Ref(CP); - if (pr>0) {(void) printf("ycube"); Cudd_PrintDebug(dd,ycube,nx+ny,pr);} - if (pr>0) {(void) printf("CP"); Cudd_PrintDebug(dd,CP,nx+ny,pr);} - - if (nx == ny) { - CPr = Cudd_PrioritySelect(dd,C,xvars,yvars,(DdNode **)NULL, - (DdNode *)NULL,ny,Cudd_Xgty); - if (CPr == NULL) exit(2); - Cudd_Ref(CPr); - if (pr>0) {(void) printf(":4: CPr"); Cudd_PrintDebug(dd,CPr,nx+ny,pr);} - if (CP != CPr) { - (void) printf("CP != CPr!\n"); - } - Cudd_RecursiveDeref(dd, CPr); - } - FREE(xvars); FREE(yvars); - - Cudd_RecursiveDeref(dd, CP); - Cudd_RecursiveDeref(dd, ycube); - - /* Test functions for essential variables. */ - ess = Cudd_FindEssential(dd,C); - if (ess == NULL) exit(2); - Cudd_Ref(ess); - if (pr>0) {(void) printf(":4: ess"); Cudd_PrintDebug(dd,ess,nx+ny,pr);} - Cudd_RecursiveDeref(dd, ess); - - /* Test functions for shortest paths. */ - shortP = Cudd_ShortestPath(dd, M, NULL, NULL, &length); - if (shortP == NULL) exit(2); - Cudd_Ref(shortP); - if (pr>0) { - (void) printf(":5: shortP"); Cudd_PrintDebug(dd,shortP,nx+ny,pr); - } - /* Test functions for largest cubes. */ - largest = Cudd_LargestCube(dd, Cudd_Not(C), &length); - if (largest == NULL) exit(2); - Cudd_Ref(largest); - if (pr>0) { - (void) printf(":5b: largest"); - Cudd_PrintDebug(dd,largest,nx+ny,pr); - } - Cudd_RecursiveDeref(dd, largest); - - /* Test Cudd_addEvalConst and Cudd_addIteConstant. */ - shortA = Cudd_BddToAdd(dd,shortP); - if (shortA == NULL) exit(2); - Cudd_Ref(shortA); - Cudd_RecursiveDeref(dd, shortP); - constN = Cudd_addEvalConst(dd,shortA,M); - if (constN == DD_NON_CONSTANT) exit(2); - if (Cudd_addIteConstant(dd,shortA,M,constN) != constN) exit(2); - if (pr>0) {(void) printf("The value of M along the chosen shortest path is %g\n", cuddV(constN));} - Cudd_RecursiveDeref(dd, shortA); - - shortP = Cudd_ShortestPath(dd, C, NULL, NULL, &length); - if (shortP == NULL) exit(2); - Cudd_Ref(shortP); - if (pr>0) { - (void) printf(":6: shortP"); Cudd_PrintDebug(dd,shortP,nx+ny,pr); - } - - /* Test Cudd_bddIteConstant and Cudd_bddLeq. */ - if (!Cudd_bddLeq(dd,shortP,C)) exit(2); - if (Cudd_bddIteConstant(dd,Cudd_Not(shortP),one,C) != one) exit(2); - Cudd_RecursiveDeref(dd, shortP); - - if (profile) { - retval = cuddHeapProfile(dd); - } - - size = dd->size; - - if (pr>0) { - (void) printf("Average distance: %g\n", Cudd_AverageDistance(dd)); - } - - /* Reorder if so requested. */ - if (approach != CUDD_REORDER_NONE) { -#ifndef DD_STATS - retval = Cudd_EnableReorderingReporting(dd); - if (retval == 0) { - (void) fprintf(stderr,"Error reported by Cudd_EnableReorderingReporting\n"); - exit(3); - } -#endif -#ifdef DD_DEBUG - retval = Cudd_DebugCheck(dd); - if (retval != 0) { - (void) fprintf(stderr,"Error reported by Cudd_DebugCheck\n"); - exit(3); - } - retval = Cudd_CheckKeys(dd); - if (retval != 0) { - (void) fprintf(stderr,"Error reported by Cudd_CheckKeys\n"); - exit(3); - } -#endif - retval = Cudd_ReduceHeap(dd,(Cudd_ReorderingType)approach,5); - if (retval == 0) { - (void) fprintf(stderr,"Error reported by Cudd_ReduceHeap\n"); - exit(3); - } -#ifndef DD_STATS - retval = Cudd_DisableReorderingReporting(dd); - if (retval == 0) { - (void) fprintf(stderr,"Error reported by Cudd_DisableReorderingReporting\n"); - exit(3); - } -#endif -#ifdef DD_DEBUG - retval = Cudd_DebugCheck(dd); - if (retval != 0) { - (void) fprintf(stderr,"Error reported by Cudd_DebugCheck\n"); - exit(3); - } - retval = Cudd_CheckKeys(dd); - if (retval != 0) { - (void) fprintf(stderr,"Error reported by Cudd_CheckKeys\n"); - exit(3); - } -#endif - if (approach == CUDD_REORDER_SYMM_SIFT || - approach == CUDD_REORDER_SYMM_SIFT_CONV) { - Cudd_SymmProfile(dd,0,dd->size-1); - } - - if (pr>0) { - (void) printf("Average distance: %g\n", Cudd_AverageDistance(dd)); - } - - if (keepperm) { - /* Print variable permutation. */ - (void) printf("Variable Permutation:"); - for (i=0; i<size; i++) { - if (i%20 == 0) (void) printf("\n"); - (void) printf("%d ", dd->invperm[i]); - } - (void) printf("\n"); - (void) printf("Inverse Permutation:"); - for (i=0; i<size; i++) { - if (i%20 == 0) (void) printf("\n"); - (void) printf("%d ", dd->perm[i]); - } - (void) printf("\n"); - } - - if (pr>0) {(void) printf("M"); Cudd_PrintDebug(dd,M,nx+ny,pr);} - - if (profile) { - retval = cuddHeapProfile(dd); - } - - } - - /* Dump DDs of C and M if so requested. */ - if (dfile != NULL) { - dfunc[0] = C; - dfunc[1] = M; - if (blifOrDot == 1) { - /* Only dump C because blif cannot handle ADDs */ - retval = Cudd_DumpBlif(dd,1,dfunc,NULL,onames,NULL,dfp); - } else { - retval = Cudd_DumpDot(dd,2,dfunc,NULL,onames,dfp); - } - if (retval != 1) { - (void) fprintf(stderr,"abnormal termination\n"); - exit(2); - } - } - - Cudd_RecursiveDeref(dd, C); - Cudd_RecursiveDeref(dd, M); - - if (clearcache) { - if (pr>0) {(void) printf("Clearing the cache... ");} - for (i = dd->cacheSlots - 1; i>=0; i--) { - dd->cache[i].data = NIL(DdNode); - } - if (pr>0) {(void) printf("done\n");} - } - if (pr>0) { - (void) printf("Number of variables = %6d\t",dd->size); - (void) printf("Number of slots = %6d\n",dd->slots); - (void) printf("Number of keys = %6d\t",dd->keys); - (void) printf("Number of min dead = %6d\n",dd->minDead); - } - - } while (multiple && !feof(fp)); - - fclose(fp); - if (dfile != NULL) { - fclose(dfp); - } - - /* Second phase: experiment with Walsh matrices. */ - if (!testWalsh(dd,N,cmu,approach,pr)) { - exit(2); - } - - /* Check variable destruction. */ - assert(cuddDestroySubtables(dd,3)); - assert(Cudd_DebugCheck(dd) == 0); - assert(Cudd_CheckKeys(dd) == 0); - - retval = Cudd_CheckZeroRef(dd); - ok = retval != 0; /* ok == 0 means O.K. */ - if (retval != 0) { - (void) fprintf(stderr, - "%d non-zero DD reference counts after dereferencing\n", retval); - } - - if (pr >= 0) { - (void) Cudd_PrintInfo(dd,stdout); - } - - Cudd_Quit(dd); - -#ifdef MNEMOSYNE - mnem_writestats(); -#endif - - if (pr>0) (void) printf("total time = %s\n", - util_print_time(util_cpu_time() - startTime)); - - if (pr >= 0) util_print_cpu_stats(stdout); - exit(ok); - /* NOTREACHED */ - -} /* end of main */ - - -/*---------------------------------------------------------------------------*/ -/* Definition of static functions */ -/*---------------------------------------------------------------------------*/ - - -/**Function******************************************************************** - - Synopsis [Prints usage info for testcudd.] - - Description [] - - SideEffects [None] - - SeeAlso [] - -******************************************************************************/ -static void -usage(char *prog) -{ - (void) fprintf(stderr, "usage: %s [options] [file]\n", prog); - (void) fprintf(stderr, " -C\t\tuse CMU multiplication algorithm\n"); - (void) fprintf(stderr, " -D\t\tenable automatic dynamic reordering\n"); - (void) fprintf(stderr, " -H\t\tread matrix in Harwell format\n"); - (void) fprintf(stderr, " -M\t\tturns off memory allocation recording\n"); - (void) fprintf(stderr, " -P\t\tprint BDD heap profile\n"); - (void) fprintf(stderr, " -S n\t\tnumber of slots for each subtable\n"); - (void) fprintf(stderr, " -X n\t\ttarget maximum memory in bytes\n"); - (void) fprintf(stderr, " -a n\t\tchoose reordering approach (0-13)\n"); - (void) fprintf(stderr, " \t\t\t0: same as autoMethod\n"); - (void) fprintf(stderr, " \t\t\t1: no reordering (default)\n"); - (void) fprintf(stderr, " \t\t\t2: random\n"); - (void) fprintf(stderr, " \t\t\t3: pivot\n"); - (void) fprintf(stderr, " \t\t\t4: sifting\n"); - (void) fprintf(stderr, " \t\t\t5: sifting to convergence\n"); - (void) fprintf(stderr, " \t\t\t6: symmetric sifting\n"); - (void) fprintf(stderr, " \t\t\t7: symmetric sifting to convergence\n"); - (void) fprintf(stderr, " \t\t\t8-10: window of size 2-4\n"); - (void) fprintf(stderr, " \t\t\t11-13: window of size 2-4 to conv.\n"); - (void) fprintf(stderr, " \t\t\t14: group sifting\n"); - (void) fprintf(stderr, " \t\t\t15: group sifting to convergence\n"); - (void) fprintf(stderr, " \t\t\t16: simulated annealing\n"); - (void) fprintf(stderr, " \t\t\t17: genetic algorithm\n"); - (void) fprintf(stderr, " -b\t\tuse blif as format for dumps\n"); - (void) fprintf(stderr, " -c\t\tclear the cache after each matrix\n"); - (void) fprintf(stderr, " -d file\tdump DDs to file\n"); - (void) fprintf(stderr, " -g\t\tselect aggregation criterion (0,5,7)\n"); - (void) fprintf(stderr, " -h\t\tprints this message\n"); - (void) fprintf(stderr, " -k\t\tprint the variable permutation\n"); - (void) fprintf(stderr, " -m\t\tread multiple matrices (only with -H)\n"); - (void) fprintf(stderr, " -n n\t\tnumber of variables\n"); - (void) fprintf(stderr, " -p n\t\tcontrol verbosity\n"); - (void) fprintf(stderr, " -v n\t\tinitial variables in the unique table\n"); - (void) fprintf(stderr, " -x n\t\tinitial size of the cache\n"); - exit(2); -} /* end of usage */ - - -/**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 [] - -******************************************************************************/ -static FILE * -open_file(char *filename, char *mode) -{ - FILE *fp; - - if (strcmp(filename, "-") == 0) { - return mode[0] == 'r' ? stdin : stdout; - } else if ((fp = fopen(filename, mode)) == NULL) { - perror(filename); - exit(1); - } - return fp; - -} /* end of open_file */ - - -/**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 [] - -******************************************************************************/ -static int -testWalsh( - DdManager *dd /* manager */, - int N /* number of variables */, - int cmu /* use CMU approach to matrix multiplication */, - int approach /* reordering approach */, - int pr /* verbosity level */) -{ - DdNode *walsh1, *walsh2, *wtw; - DdNode **x, **v, **z; - int i, retval; - DdNode *one = DD_ONE(dd); - DdNode *zero = DD_ZERO(dd); - - if (N > 3) { - x = ALLOC(DdNode *,N); - v = ALLOC(DdNode *,N); - z = ALLOC(DdNode *,N); - - for (i = N-1; i >= 0; i--) { - Cudd_Ref(x[i]=cuddUniqueInter(dd,3*i,one,zero)); - Cudd_Ref(v[i]=cuddUniqueInter(dd,3*i+1,one,zero)); - Cudd_Ref(z[i]=cuddUniqueInter(dd,3*i+2,one,zero)); - } - Cudd_Ref(walsh1 = Cudd_addWalsh(dd,v,z,N)); - if (pr>0) {(void) printf("walsh1"); Cudd_PrintDebug(dd,walsh1,2*N,pr);} - Cudd_Ref(walsh2 = Cudd_addWalsh(dd,x,v,N)); - if (cmu) { - Cudd_Ref(wtw = Cudd_addTimesPlus(dd,walsh2,walsh1,v,N)); - } else { - Cudd_Ref(wtw = Cudd_addMatrixMultiply(dd,walsh2,walsh1,v,N)); - } - if (pr>0) {(void) printf("wtw"); Cudd_PrintDebug(dd,wtw,2*N,pr);} - - if (approach != CUDD_REORDER_NONE) { -#ifdef DD_DEBUG - retval = Cudd_DebugCheck(dd); - if (retval != 0) { - (void) fprintf(stderr,"Error reported by Cudd_DebugCheck\n"); - return(0); - } -#endif - retval = Cudd_ReduceHeap(dd,(Cudd_ReorderingType)approach,5); - if (retval == 0) { - (void) fprintf(stderr,"Error reported by Cudd_ReduceHeap\n"); - return(0); - } -#ifdef DD_DEBUG - retval = Cudd_DebugCheck(dd); - if (retval != 0) { - (void) fprintf(stderr,"Error reported by Cudd_DebugCheck\n"); - return(0); - } -#endif - if (approach == CUDD_REORDER_SYMM_SIFT || - approach == CUDD_REORDER_SYMM_SIFT_CONV) { - Cudd_SymmProfile(dd,0,dd->size-1); - } - } - /* Clean up. */ - Cudd_RecursiveDeref(dd, wtw); - Cudd_RecursiveDeref(dd, walsh1); - Cudd_RecursiveDeref(dd, walsh2); - for (i=0; i < N; i++) { - Cudd_RecursiveDeref(dd, x[i]); - Cudd_RecursiveDeref(dd, v[i]); - Cudd_RecursiveDeref(dd, z[i]); - } - FREE(x); - FREE(v); - FREE(z); - } - return(1); - -} /* end of testWalsh */ - -/**Function******************************************************************** - - Synopsis [Tests iterators.] - - Description [Tests iterators on cubes and nodes.] - - SideEffects [None] - - SeeAlso [] - -******************************************************************************/ -static int -testIterators( - DdManager *dd, - DdNode *M, - DdNode *C, - int pr) -{ - int *cube; - CUDD_VALUE_TYPE value; - DdGen *gen; - int q; - - /* Test iterator for cubes. */ - if (pr>1) { - (void) printf("Testing iterator on cubes:\n"); - Cudd_ForeachCube(dd,M,gen,cube,value) { - for (q = 0; q < dd->size; q++) { - switch (cube[q]) { - case 0: - (void) printf("0"); - break; - case 1: - (void) printf("1"); - break; - case 2: - (void) printf("-"); - break; - default: - (void) printf("?"); - } - } - (void) printf(" %g\n",value); - } - (void) printf("\n"); - } - - if (pr>1) { - (void) printf("Testing prime expansion of cubes:\n"); - if (!Cudd_bddPrintCover(dd,C,C)) return(0); - } - - /* Test iterator on nodes. */ - if (pr>2) { - DdGen *gen; - DdNode *node; - (void) printf("Testing iterator on nodes:\n"); - Cudd_ForeachNode(dd,M,gen,node) { - if (Cudd_IsConstant(node)) { -#if SIZEOF_VOID_P == 8 - (void) printf("ID = 0x%lx\tvalue = %-9g\n", - (unsigned long) node / - (unsigned long) sizeof(DdNode), - Cudd_V(node)); -#else - (void) printf("ID = 0x%x\tvalue = %-9g\n", - (unsigned int) node / - (unsigned int) sizeof(DdNode), - Cudd_V(node)); -#endif - } else { -#if SIZEOF_VOID_P == 8 - (void) printf("ID = 0x%lx\tindex = %d\tr = %d\n", - (unsigned long) node / - (unsigned long) sizeof(DdNode), - node->index, node->ref); -#else - (void) printf("ID = 0x%x\tindex = %d\tr = %d\n", - (unsigned int) node / - (unsigned int) sizeof(DdNode), - node->index, node->ref); -#endif - } - } - (void) printf("\n"); - } - return(1); - -} /* end of testIterators */ - - -/**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 [] - -******************************************************************************/ -static int -testXor(DdManager *dd, DdNode *f, int pr, int nvars) -{ - DdNode *f1, *f0, *res1, *res2; - int x; - - /* Extract cofactors w.r.t. mid variable. */ - x = nvars / 2; - f1 = Cudd_Cofactor(dd,f,dd->vars[x]); - if (f1 == NULL) return(0); - Cudd_Ref(f1); - - f0 = Cudd_Cofactor(dd,f,Cudd_Not(dd->vars[x])); - if (f0 == NULL) { - Cudd_RecursiveDeref(dd,f1); - return(0); - } - Cudd_Ref(f0); - - /* Compute XOR of cofactors with ITE. */ - res1 = Cudd_bddIte(dd,f1,Cudd_Not(f0),f0); - if (res1 == NULL) return(0); - Cudd_Ref(res1); - - if (pr>0) {(void) printf("xor1"); Cudd_PrintDebug(dd,res1,nvars,pr);} - - /* Compute XOR of cofactors with XOR. */ - res2 = Cudd_bddXor(dd,f1,f0); - if (res2 == NULL) { - Cudd_RecursiveDeref(dd,res1); - return(0); - } - Cudd_Ref(res2); - - if (res1 != res2) { - if (pr>0) {(void) printf("xor2"); Cudd_PrintDebug(dd,res2,nvars,pr);} - Cudd_RecursiveDeref(dd,res1); - Cudd_RecursiveDeref(dd,res2); - return(0); - } - Cudd_RecursiveDeref(dd,res1); - Cudd_RecursiveDeref(dd,f1); - Cudd_RecursiveDeref(dd,f0); - - /* Compute boolean difference directly. */ - res1 = Cudd_bddBooleanDiff(dd,f,x); - if (res1 == NULL) { - Cudd_RecursiveDeref(dd,res2); - return(0); - } - Cudd_Ref(res1); - - if (res1 != res2) { - if (pr>0) {(void) printf("xor3"); Cudd_PrintDebug(dd,res1,nvars,pr);} - Cudd_RecursiveDeref(dd,res1); - Cudd_RecursiveDeref(dd,res2); - return(0); - } - Cudd_RecursiveDeref(dd,res1); - Cudd_RecursiveDeref(dd,res2); - return(1); - -} /* end of testXor */ - - -/**Function******************************************************************** - - Synopsis [Tests the Hamming distance functions.] - - Description [Tests the Hammming distance functions. Returns - 1 if successful; 0 otherwise.] - - SideEffects [None] - - SeeAlso [] - -******************************************************************************/ -static int -testHamming( - DdManager *dd, - DdNode *f, - int pr, - int nvars) -{ - DdNode **vars, *minBdd, *zero, *scan; - int i; - int d; - int *minterm; - int size = Cudd_ReadSize(dd); - - vars = ALLOC(DdNode *, size); - if (vars == NULL) return(0); - for (i = 0; i < size; i++) { - vars[i] = Cudd_bddIthVar(dd,i); - } - - minBdd = Cudd_bddPickOneMinterm(dd,Cudd_Not(f),vars,size); - Cudd_Ref(minBdd); - if (pr > 0) { - (void) printf("Chosen minterm for Hamming distance test: "); - Cudd_PrintDebug(dd,minBdd,size,pr); - } - - minterm = ALLOC(int,size); - if (minterm == NULL) { - FREE(vars); - Cudd_RecursiveDeref(dd,minBdd); - return(0); - } - scan = minBdd; - zero = Cudd_Not(DD_ONE(dd)); - while (!Cudd_IsConstant(scan)) { - DdNode *R = Cudd_Regular(scan); - DdNode *T = Cudd_T(R); - DdNode *E = Cudd_E(R); - if (R != scan) { - T = Cudd_Not(T); - E = Cudd_Not(E); - } - if (T == zero) { - minterm[R->index] = 0; - scan = E; - } else { - minterm[R->index] = 1; - scan = T; - } - } - Cudd_RecursiveDeref(dd,minBdd); - - d = Cudd_MinHammingDist(dd,f,minterm,size); - - (void) printf("Minimum Hamming distance = %d\n", d); - - FREE(vars); - FREE(minterm); - return(1); - -} /* end of testHamming */ |