src/bdd/cudd/testcudd.c

Go to the documentation of this file.

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

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

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


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


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


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

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


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


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

---