Version abc50729

1 files changed, 988 insertions, 0 deletions

diff --git a/src/bdd/cudd/testcudd.c b/src/bdd/cudd/testcudd.c
new file mode 100644
index 00000000..451bb190
--- /dev/null
+++ b/src/bdd/cudd/testcudd.c
@@ -0,0 +1,988 @@
+/**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.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 */