cuddUtil.c

Go to the documentation of this file.

#include "CUDD/util.h"
#include "CUDD/cuddInt.h"

/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/

/* Random generator constants. */
#define MODULUS1 2147483563
#define LEQA1 40014
#define LEQQ1 53668
#define LEQR1 12211
#define MODULUS2 2147483399
#define LEQA2 40692
#define LEQQ2 52774
#define LEQR2 3791
#define STAB_SIZE 64
#define STAB_DIV (1 + (MODULUS1 - 1) / STAB_SIZE)

/*---------------------------------------------------------------------------*/
/* Stucture declarations                                                     */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/

#ifndef lint
static char rcsid[] DD_UNUSED = "$Id: cuddUtil.c,v 1.83 2012/02/05 01:07:19 fabio Exp $";
#endif

static  DdNode  *background, *zero;

static  long cuddRand = 0;
static  long cuddRand2;
static  long shuffleSelect;
static  long shuffleTable[STAB_SIZE];

/*---------------------------------------------------------------------------*/
/* Macro declarations                                                        */
/*---------------------------------------------------------------------------*/

#define bang(f) ((Cudd_IsComplement(f)) ? '!' : ' ')

#ifdef __cplusplus
extern "C" {
#endif

/*---------------------------------------------------------------------------*/
/* Static function prototypes                                                */
/*---------------------------------------------------------------------------*/

static int dp2 (DdManager *dd, DdNode *f, st_table *t);
static void ddPrintMintermAux (DdManager *dd, DdNode *node, int *list);
static int ddDagInt (DdNode *n);
static int cuddNodeArrayRecur (DdNode *f, DdNodePtr *table, int index);
static int cuddEstimateCofactor (DdManager *dd, st_table *table, DdNode * node, int i, int phase, DdNode ** ptr);
static DdNode * cuddUniqueLookup (DdManager * unique, int  index, DdNode * T, DdNode * E);
static int cuddEstimateCofactorSimple (DdNode * node, int i);
static double ddCountMintermAux (DdNode *node, double max, DdHashTable *table);
static int ddEpdCountMintermAux (DdNode *node, EpDouble *max, EpDouble *epd, st_table *table);
static double ddCountPathAux (DdNode *node, st_table *table);
static double ddCountPathsToNonZero (DdNode * N, st_table * table);
static void ddSupportStep (DdNode *f, int *support);
static void ddClearFlag (DdNode *f);
static int ddLeavesInt (DdNode *n);
static int ddPickArbitraryMinterms (DdManager *dd, DdNode *node, int nvars, int nminterms, char **string);
static int ddPickRepresentativeCube (DdManager *dd, DdNode *node, double *weight, char *string);
static enum st_retval ddEpdFree (char * key, char * value, char * arg);
static void ddFindSupport(DdManager *dd, DdNode *f, int *SP);
static void ddClearVars(DdManager *dd, int SP);
static int indexCompare(const void *a, const void *b);

#ifdef __cplusplus
}
#endif

/*---------------------------------------------------------------------------*/
/* Definition of exported functions                                          */
/*---------------------------------------------------------------------------*/


int
Cudd_PrintMinterm(
  DdManager * manager,
  DdNode * node)
{
    int     i, *list;

    background = manager->background;
    zero = Cudd_Not(manager->one);
    list = ALLOC(int,manager->size);
    if (list == NULL) {
    manager->errorCode = CUDD_MEMORY_OUT;
    return(0);
    }
    for (i = 0; i < manager->size; i++) list[i] = 2;
    ddPrintMintermAux(manager,node,list);
    FREE(list);
    return(1);

} /* end of Cudd_PrintMinterm */


int
Cudd_bddPrintCover(
  DdManager *dd,
  DdNode *l,
  DdNode *u)
{
    int *array;
    int q, result;
    DdNode *lb;
#ifdef DD_DEBUG
    DdNode *cover;
#endif

    array = ALLOC(int, Cudd_ReadSize(dd));
    if (array == NULL) return(0);
    lb = l;
    cuddRef(lb);
#ifdef DD_DEBUG
    cover = Cudd_ReadLogicZero(dd);
    cuddRef(cover);
#endif
    while (lb != Cudd_ReadLogicZero(dd)) {
    DdNode *implicant, *prime, *tmp;
    int length;
    implicant = Cudd_LargestCube(dd,lb,&length);
    if (implicant == NULL) {
        Cudd_RecursiveDeref(dd,lb);
        FREE(array);
        return(0);
    }
    cuddRef(implicant);
    prime = Cudd_bddMakePrime(dd,implicant,u);
    if (prime == NULL) {
        Cudd_RecursiveDeref(dd,lb);
        Cudd_RecursiveDeref(dd,implicant);
        FREE(array);
        return(0);
    }
    cuddRef(prime);
    Cudd_RecursiveDeref(dd,implicant);
    tmp = Cudd_bddAnd(dd,lb,Cudd_Not(prime));
    if (tmp == NULL) {
        Cudd_RecursiveDeref(dd,lb);
        Cudd_RecursiveDeref(dd,prime);
        FREE(array);
        return(0);
    }
    cuddRef(tmp);
    Cudd_RecursiveDeref(dd,lb);
    lb = tmp;
    result = Cudd_BddToCubeArray(dd,prime,array);
    if (result == 0) {
        Cudd_RecursiveDeref(dd,lb);
        Cudd_RecursiveDeref(dd,prime);
        FREE(array);
        return(0);
    }
    for (q = 0; q < dd->size; q++) {
        switch (array[q]) {
        case 0:
        (void) fprintf(dd->out, "0");
        break;
        case 1:
        (void) fprintf(dd->out, "1");
        break;
        case 2:
        (void) fprintf(dd->out, "-");
        break;
        default:
        (void) fprintf(dd->out, "?");
        }
    }
    (void) fprintf(dd->out, " 1\n");
#ifdef DD_DEBUG
    tmp = Cudd_bddOr(dd,prime,cover);
    if (tmp == NULL) {
        Cudd_RecursiveDeref(dd,cover);
        Cudd_RecursiveDeref(dd,lb);
        Cudd_RecursiveDeref(dd,prime);
        FREE(array);
        return(0);
    }
    cuddRef(tmp);
    Cudd_RecursiveDeref(dd,cover);
    cover = tmp;
#endif
    Cudd_RecursiveDeref(dd,prime);
    }
    (void) fprintf(dd->out, "\n");
    Cudd_RecursiveDeref(dd,lb);
    FREE(array);
#ifdef DD_DEBUG
    if (!Cudd_bddLeq(dd,cover,u) || !Cudd_bddLeq(dd,l,cover)) {
    Cudd_RecursiveDeref(dd,cover);
    return(0);
    }
    Cudd_RecursiveDeref(dd,cover);
#endif
    return(1);

} /* end of Cudd_bddPrintCover */


int
Cudd_PrintDebug(
  DdManager * dd,
  DdNode * f,
  int  n,
  int  pr)
{
    DdNode *azero, *bzero;
    int    nodes;
    int    leaves;
    double minterms;
    int    retval = 1;

    if (f == NULL) {
    (void) fprintf(dd->out,": is the NULL DD\n");
    (void) fflush(dd->out);
    return(0);
    }
    azero = DD_ZERO(dd);
    bzero = Cudd_Not(DD_ONE(dd));
    if ((f == azero || f == bzero) && pr > 0){
       (void) fprintf(dd->out,": is the zero DD\n");
       (void) fflush(dd->out);
       return(1);
    }
    if (pr > 0) {
    nodes = Cudd_DagSize(f);
    if (nodes == CUDD_OUT_OF_MEM) retval = 0;
    leaves = Cudd_CountLeaves(f);
    if (leaves == CUDD_OUT_OF_MEM) retval = 0;
    minterms = Cudd_CountMinterm(dd, f, n);
    if (minterms == (double)CUDD_OUT_OF_MEM) retval = 0;
    (void) fprintf(dd->out,": %d nodes %d leaves %g minterms\n",
               nodes, leaves, minterms);
    if (pr > 2) {
        if (!cuddP(dd, f)) retval = 0;
    }
    if (pr == 2 || pr > 3) {
        if (!Cudd_PrintMinterm(dd,f)) retval = 0;
        (void) fprintf(dd->out,"\n");
    }
    (void) fflush(dd->out);
    }
    return(retval);

} /* end of Cudd_PrintDebug */


int
Cudd_DagSize(
  DdNode * node)
{
    int i;

    i = ddDagInt(Cudd_Regular(node));
    ddClearFlag(Cudd_Regular(node));

    return(i);

} /* end of Cudd_DagSize */


int
Cudd_EstimateCofactor(
  DdManager *dd /* manager */,
  DdNode * f    /* function */,
  int i     /* index of variable */,
  int phase /* 1: positive; 0: negative */
  )
{
    int val;
    DdNode *ptr;
    st_table *table;

    table = st_init_table(st_ptrcmp,st_ptrhash);
    if (table == NULL) return(CUDD_OUT_OF_MEM);
    val = cuddEstimateCofactor(dd,table,Cudd_Regular(f),i,phase,&ptr);
    ddClearFlag(Cudd_Regular(f));
    st_free_table(table);

    return(val);

} /* end of Cudd_EstimateCofactor */


int
Cudd_EstimateCofactorSimple(
  DdNode * node,
  int i)
{
    int val;

    val = cuddEstimateCofactorSimple(Cudd_Regular(node),i);
    ddClearFlag(Cudd_Regular(node));

    return(val);

} /* end of Cudd_EstimateCofactorSimple */


int
Cudd_SharingSize(
  DdNode ** nodeArray,
  int  n)
{
    int i,j;

    i = 0;
    for (j = 0; j < n; j++) {
    i += ddDagInt(Cudd_Regular(nodeArray[j]));
    }
    for (j = 0; j < n; j++) {
    ddClearFlag(Cudd_Regular(nodeArray[j]));
    }
    return(i);

} /* end of Cudd_SharingSize */


double
Cudd_CountMinterm(
  DdManager * manager,
  DdNode * node,
  int  nvars)
{
    double  max;
    DdHashTable *table;
    double  res;
    CUDD_VALUE_TYPE epsilon;

    background = manager->background;
    zero = Cudd_Not(manager->one);

    max = pow(2.0,(double)nvars);
    table = cuddHashTableInit(manager,1,2);
    if (table == NULL) {
    return((double)CUDD_OUT_OF_MEM);
    }
    epsilon = Cudd_ReadEpsilon(manager);
    Cudd_SetEpsilon(manager,(CUDD_VALUE_TYPE)0.0);
    res = ddCountMintermAux(node,max,table);
    cuddHashTableQuit(table);
    Cudd_SetEpsilon(manager,epsilon);

    return(res);

} /* end of Cudd_CountMinterm */


double
Cudd_CountPath(
  DdNode * node)
{

    st_table    *table;
    double  i;

    table = st_init_table(st_ptrcmp,st_ptrhash);
    if (table == NULL) {
    return((double)CUDD_OUT_OF_MEM);
    }
    i = ddCountPathAux(Cudd_Regular(node),table);
    st_foreach(table, cuddStCountfree, NULL);
    st_free_table(table);
    return(i);

} /* end of Cudd_CountPath */


int
Cudd_EpdCountMinterm(
  DdManager * manager,
  DdNode * node,
  int  nvars,
  EpDouble * epd)
{
    EpDouble    max, tmp;
    st_table    *table;
    int     status;

    background = manager->background;
    zero = Cudd_Not(manager->one);

    EpdPow2(nvars, &max);
    table = st_init_table(EpdCmp, st_ptrhash);
    if (table == NULL) {
    EpdMakeZero(epd, 0);
    return(CUDD_OUT_OF_MEM);
    }
    status = ddEpdCountMintermAux(Cudd_Regular(node),&max,epd,table);
    st_foreach(table, ddEpdFree, NULL);
    st_free_table(table);
    if (status == CUDD_OUT_OF_MEM) {
    EpdMakeZero(epd, 0);
    return(CUDD_OUT_OF_MEM);
    }
    if (Cudd_IsComplement(node)) {
    EpdSubtract3(&max, epd, &tmp);
    EpdCopy(&tmp, epd);
    }
    return(0);

} /* end of Cudd_EpdCountMinterm */


double
Cudd_CountPathsToNonZero(
  DdNode * node)
{

    st_table    *table;
    double  i;

    table = st_init_table(st_ptrcmp,st_ptrhash);
    if (table == NULL) {
    return((double)CUDD_OUT_OF_MEM);
    }
    i = ddCountPathsToNonZero(node,table);
    st_foreach(table, cuddStCountfree, NULL);
    st_free_table(table);
    return(i);

} /* end of Cudd_CountPathsToNonZero */


int
Cudd_SupportIndices(
  DdManager * dd /* manager */,
  DdNode * f /* DD whose support is sought */,
  int **indices /* array containing (on return) the indices */)
{
    int SP = 0;

    ddFindSupport(dd, Cudd_Regular(f), &SP);
    ddClearFlag(Cudd_Regular(f));
    ddClearVars(dd, SP);
    if (SP > 0) {
        int i;
        *indices = ALLOC(int, SP);
        if (*indices == NULL) {
            dd->errorCode = CUDD_MEMORY_OUT;
            return(CUDD_OUT_OF_MEM);
        }

        for (i = 0; i < SP; i++)
            (*indices)[i] = (int) (ptrint) dd->stack[i];

        qsort(*indices, SP, sizeof(int), indexCompare);
    } else {
        *indices = NULL;
    }

    return(SP);

} /* end of Cudd_SupportIndices */


DdNode *
Cudd_Support(
  DdManager * dd /* manager */,
  DdNode * f /* DD whose support is sought */)
{
    int *support;
    DdNode *res;
    int j;

    int size = Cudd_SupportIndices(dd, f, &support);
    if (size == CUDD_OUT_OF_MEM)
        return(NULL);

    /* Transform support from array of indices to cube. */
    res = DD_ONE(dd);
    cuddRef(res);
    
    for (j = size - 1; j >= 0; j--) { /* for each index bottom-up (almost) */
        int index = support[j];
        DdNode *var = dd->vars[index];
        DdNode *tmp = Cudd_bddAnd(dd,res,var);
        if (tmp == NULL) {
            Cudd_RecursiveDeref(dd,res);
            FREE(support);
            return(NULL);
        }
        cuddRef(tmp);
        Cudd_RecursiveDeref(dd,res);
        res = tmp;
    }

    FREE(support);
    cuddDeref(res);
    return(res);

} /* end of Cudd_Support */


int *
Cudd_SupportIndex(
  DdManager * dd /* manager */,
  DdNode * f /* DD whose support is sought */)
{
    int *support;
    int i;
    int size;

    /* Allocate and initialize support array for ddSupportStep. */
    size = ddMax(dd->size, dd->sizeZ);
    support = ALLOC(int,size);
    if (support == NULL) {
    dd->errorCode = CUDD_MEMORY_OUT;
    return(NULL);
    }
    for (i = 0; i < size; i++) {
    support[i] = 0;
    }

    /* Compute support and clean up markers. */
    ddSupportStep(Cudd_Regular(f),support);
    ddClearFlag(Cudd_Regular(f));

    return(support);

} /* end of Cudd_SupportIndex */


int
Cudd_SupportSize(
  DdManager * dd /* manager */,
  DdNode * f /* DD whose support size is sought */)
{
    int SP = 0;

    ddFindSupport(dd, Cudd_Regular(f), &SP);
    ddClearFlag(Cudd_Regular(f));
    ddClearVars(dd, SP);

    return(SP);

} /* end of Cudd_SupportSize */


int
Cudd_VectorSupportIndices(
  DdManager * dd /* manager */,
  DdNode ** F /* DD whose support is sought */,
  int  n /* size of the array */,
  int **indices /* array containing (on return) the indices */)
{
    int i;
    int SP = 0;

    /* Compute support and clean up markers. */
    for (i = 0; i < n; i++) {
    ddFindSupport(dd, Cudd_Regular(F[i]), &SP);
    }
    for (i = 0; i < n; i++) {
    ddClearFlag(Cudd_Regular(F[i]));
    }
    ddClearVars(dd, SP);

    if (SP > 0) {
        int i;
        *indices = ALLOC(int, SP);
        if (*indices == NULL) {
            dd->errorCode = CUDD_MEMORY_OUT;
            return(CUDD_OUT_OF_MEM);
        }

        for (i = 0; i < SP; i++)
            (*indices)[i] = (int) (ptrint) dd->stack[i];

        qsort(*indices, SP, sizeof(int), indexCompare);
    } else {
        *indices = NULL;
    }

    return(SP);

} /* end of Cudd_VectorSupportIndices */


DdNode *
Cudd_VectorSupport(
  DdManager * dd /* manager */,
  DdNode ** F /* array of DDs whose support is sought */,
  int  n /* size of the array */)
{
    int *support;
    DdNode *res;
    int j;
    int size = Cudd_VectorSupportIndices(dd, F, n, &support);
    if (size == CUDD_OUT_OF_MEM)
        return(NULL);

    /* Transform support from array of indices to cube. */
    res = DD_ONE(dd);
    cuddRef(res);
    
    for (j = size - 1; j >= 0; j--) { /* for each index bottom-up (almost) */
        int index = support[j];
        DdNode *var = dd->vars[index];
        DdNode *tmp = Cudd_bddAnd(dd,res,var);
        if (tmp == NULL) {
            Cudd_RecursiveDeref(dd,res);
            FREE(support);
            return(NULL);
        }
        cuddRef(tmp);
        Cudd_RecursiveDeref(dd,res);
        res = tmp;
    }

    FREE(support);
    cuddDeref(res);
    return(res);

} /* end of Cudd_VectorSupport */


int *
Cudd_VectorSupportIndex(
  DdManager * dd /* manager */,
  DdNode ** F /* array of DDs whose support is sought */,
  int  n /* size of the array */)
{
    int *support;
    int i;
    int size;

    /* Allocate and initialize support array for ddSupportStep. */
    size = ddMax(dd->size, dd->sizeZ);
    support = ALLOC(int,size);
    if (support == NULL) {
    dd->errorCode = CUDD_MEMORY_OUT;
    return(NULL);
    }
    for (i = 0; i < size; i++) {
    support[i] = 0;
    }

    /* Compute support and clean up markers. */
    for (i = 0; i < n; i++) {
    ddSupportStep(Cudd_Regular(F[i]),support);
    }
    for (i = 0; i < n; i++) {
    ddClearFlag(Cudd_Regular(F[i]));
    }

    return(support);

} /* end of Cudd_VectorSupportIndex */


int
Cudd_VectorSupportSize(
  DdManager * dd /* manager */,
  DdNode ** F /* array of DDs whose support is sought */,
  int  n /* size of the array */)
{
    int i;
    int SP = 0;

    /* Compute support and clean up markers. */
    for (i = 0; i < n; i++) {
    ddFindSupport(dd, Cudd_Regular(F[i]), &SP);
    }
    for (i = 0; i < n; i++) {
    ddClearFlag(Cudd_Regular(F[i]));
    }
    ddClearVars(dd, SP);

    return(SP);

} /* end of Cudd_VectorSupportSize */


int
Cudd_ClassifySupport(
  DdManager * dd /* manager */,
  DdNode * f /* first DD */,
  DdNode * g /* second DD */,
  DdNode ** common /* cube of shared variables */,
  DdNode ** onlyF /* cube of variables only in f */,
  DdNode ** onlyG /* cube of variables only in g */)
{
    int *supportF, *supportG;
    int fi, gi;
    int sizeF, sizeG;

    sizeF = Cudd_SupportIndices(dd, f, &supportF);
    if (sizeF == CUDD_OUT_OF_MEM)
        return(0);

    sizeG = Cudd_SupportIndices(dd, g, &supportG);
    if (sizeG == CUDD_OUT_OF_MEM) {
        FREE(supportF);
        return(0);
    }

    /* Classify variables and create cubes. This part of the procedure
    ** relies on the sorting of the indices in the two support arrays.
    */
    *common = *onlyF = *onlyG = DD_ONE(dd);
    cuddRef(*common); cuddRef(*onlyF); cuddRef(*onlyG);
    fi = sizeF - 1;
    gi = sizeG - 1;
    while (fi >= 0 || gi >= 0) {
        int indexF = fi >= 0 ? supportF[fi] : -1;
        int indexG = gi >= 0 ? supportG[gi] : -1;
        int index = ddMax(indexF, indexG);
        DdNode *var = dd->vars[index];
#ifdef DD_DEBUG
        assert(index >= 0);
#endif
        if (indexF == indexG) {
            DdNode *tmp = Cudd_bddAnd(dd,*common,var);
        if (tmp == NULL) {
        Cudd_RecursiveDeref(dd,*common);
        Cudd_RecursiveDeref(dd,*onlyF);
        Cudd_RecursiveDeref(dd,*onlyG);
        FREE(supportF); FREE(supportG);
        return(0);
        }
        cuddRef(tmp);
        Cudd_RecursiveDeref(dd,*common);
        *common = tmp;
            fi--;
            gi--;
        } else if (index == indexF) {
        DdNode *tmp = Cudd_bddAnd(dd,*onlyF,var);
        if (tmp == NULL) {
        Cudd_RecursiveDeref(dd,*common);
        Cudd_RecursiveDeref(dd,*onlyF);
        Cudd_RecursiveDeref(dd,*onlyG);
        FREE(supportF); FREE(supportG);
        return(0);
        }
        cuddRef(tmp);
        Cudd_RecursiveDeref(dd,*onlyF);
        *onlyF = tmp;
            fi--;
        } else { /* index == indexG */
        DdNode *tmp = Cudd_bddAnd(dd,*onlyG,var);
        if (tmp == NULL) {
        Cudd_RecursiveDeref(dd,*common);
        Cudd_RecursiveDeref(dd,*onlyF);
        Cudd_RecursiveDeref(dd,*onlyG);
        FREE(supportF); FREE(supportG);
        return(0);
        }
        cuddRef(tmp);
        Cudd_RecursiveDeref(dd,*onlyG);
        *onlyG = tmp;
            gi--;
        }
    }

    FREE(supportF); FREE(supportG);
    cuddDeref(*common); cuddDeref(*onlyF); cuddDeref(*onlyG);
    return(1);

} /* end of Cudd_ClassifySupport */


int
Cudd_CountLeaves(
  DdNode * node)
{
    int i;

    i = ddLeavesInt(Cudd_Regular(node));
    ddClearFlag(Cudd_Regular(node));
    return(i);

} /* end of Cudd_CountLeaves */


int
Cudd_bddPickOneCube(
  DdManager * ddm,
  DdNode * node,
  char * string)
{
    DdNode *N, *T, *E;
    DdNode *one, *bzero;
    char   dir;
    int    i;

    if (string == NULL || node == NULL) return(0);

    /* The constant 0 function has no on-set cubes. */
    one = DD_ONE(ddm);
    bzero = Cudd_Not(one);
    if (node == bzero) return(0);

    for (i = 0; i < ddm->size; i++) string[i] = 2;

    for (;;) {

    if (node == one) break;

    N = Cudd_Regular(node);

    T = cuddT(N); E = cuddE(N);
    if (Cudd_IsComplement(node)) {
        T = Cudd_Not(T); E = Cudd_Not(E);
    }
    if (T == bzero) {
        string[N->index] = 0;
        node = E;
    } else if (E == bzero) {
        string[N->index] = 1;
        node = T;
    } else {
        dir = (char) ((Cudd_Random() & 0x2000) >> 13);
        string[N->index] = dir;
        node = dir ? T : E;
    }
    }
    return(1);

} /* end of Cudd_bddPickOneCube */


DdNode *
Cudd_bddPickOneMinterm(
  DdManager * dd /* manager */,
  DdNode * f /* function from which to pick one minterm */,
  DdNode ** vars /* array of variables */,
  int  n /* size of <code>vars</code> */)
{
    char *string;
    int i, size;
    int *indices;
    int result;
    DdNode *old, *neW;

    size = dd->size;
    string = ALLOC(char, size);
    if (string == NULL) {
    dd->errorCode = CUDD_MEMORY_OUT;
    return(NULL);
    }
    indices = ALLOC(int,n);
    if (indices == NULL) {
    dd->errorCode = CUDD_MEMORY_OUT;
    FREE(string);
    return(NULL);
    }

    for (i = 0; i < n; i++) {
    indices[i] = vars[i]->index;
    }

    result = Cudd_bddPickOneCube(dd,f,string);
    if (result == 0) {
    FREE(string);
    FREE(indices);
    return(NULL);
    }

    /* Randomize choice for don't cares. */
    for (i = 0; i < n; i++) {
    if (string[indices[i]] == 2)
        string[indices[i]] = (char) ((Cudd_Random() & 0x20) >> 5);
    }

    /* Build result BDD. */
    old = Cudd_ReadOne(dd);
    cuddRef(old);

    for (i = n-1; i >= 0; i--) {
    neW = Cudd_bddAnd(dd,old,Cudd_NotCond(vars[i],string[indices[i]]==0));
    if (neW == NULL) {
        FREE(string);
        FREE(indices);
        Cudd_RecursiveDeref(dd,old);
        return(NULL);
    }
    cuddRef(neW);
    Cudd_RecursiveDeref(dd,old);
    old = neW;
    }

#ifdef DD_DEBUG
    /* Test. */
    if (Cudd_bddLeq(dd,old,f)) {
    cuddDeref(old);
    } else {
    Cudd_RecursiveDeref(dd,old);
    old = NULL;
    }
#else
    cuddDeref(old);
#endif

    FREE(string);
    FREE(indices);
    return(old);

}  /* end of Cudd_bddPickOneMinterm */


DdNode **
Cudd_bddPickArbitraryMinterms(
  DdManager * dd /* manager */,
  DdNode * f /* function from which to pick k minterms */,
  DdNode ** vars /* array of variables */,
  int  n /* size of <code>vars</code> */,
  int  k /* number of minterms to find */)
{
    char **string;
    int i, j, l, size;
    int *indices;
    int result;
    DdNode **old, *neW;
    double minterms;
    char *saveString;
    int saveFlag, savePoint, isSame;

    minterms = Cudd_CountMinterm(dd,f,n);
    if ((double)k > minterms) {
    return(NULL);
    }

    size = dd->size;
    string = ALLOC(char *, k);
    if (string == NULL) {
    dd->errorCode = CUDD_MEMORY_OUT;
    return(NULL);
    }
    for (i = 0; i < k; i++) {
    string[i] = ALLOC(char, size + 1);
    if (string[i] == NULL) {
        for (j = 0; j < i; j++)
        FREE(string[i]);
        FREE(string);
        dd->errorCode = CUDD_MEMORY_OUT;
        return(NULL);
    }
    for (j = 0; j < size; j++) string[i][j] = '2';
    string[i][size] = '\0';
    }
    indices = ALLOC(int,n);
    if (indices == NULL) {
    dd->errorCode = CUDD_MEMORY_OUT;
    for (i = 0; i < k; i++)
        FREE(string[i]);
    FREE(string);
    return(NULL);
    }

    for (i = 0; i < n; i++) {
    indices[i] = vars[i]->index;
    }

    result = ddPickArbitraryMinterms(dd,f,n,k,string);
    if (result == 0) {
    for (i = 0; i < k; i++)
        FREE(string[i]);
    FREE(string);
    FREE(indices);
    return(NULL);
    }

    old = ALLOC(DdNode *, k);
    if (old == NULL) {
    dd->errorCode = CUDD_MEMORY_OUT;
    for (i = 0; i < k; i++)
        FREE(string[i]);
    FREE(string);
    FREE(indices);
    return(NULL);
    }
    saveString = ALLOC(char, size + 1);
    if (saveString == NULL) {
    dd->errorCode = CUDD_MEMORY_OUT;
    for (i = 0; i < k; i++)
        FREE(string[i]);
    FREE(string);
    FREE(indices);
    FREE(old);
    return(NULL);
    }
    saveFlag = 0;

    /* Build result BDD array. */
    for (i = 0; i < k; i++) {
    isSame = 0;
    if (!saveFlag) {
        for (j = i + 1; j < k; j++) {
        if (strcmp(string[i], string[j]) == 0) {
            savePoint = i;
            strcpy(saveString, string[i]);
            saveFlag = 1;
            break;
        }
        }
    } else {
        if (strcmp(string[i], saveString) == 0) {
        isSame = 1;
        } else {
        saveFlag = 0;
        for (j = i + 1; j < k; j++) {
            if (strcmp(string[i], string[j]) == 0) {
            savePoint = i;
            strcpy(saveString, string[i]);
            saveFlag = 1;
            break;
            }
        }
        }
    }
    /* Randomize choice for don't cares. */
    for (j = 0; j < n; j++) {
        if (string[i][indices[j]] == '2')
        string[i][indices[j]] =
          (char) ((Cudd_Random() & 0x20) ? '1' : '0');
    }

    while (isSame) {
        isSame = 0;
        for (j = savePoint; j < i; j++) {
        if (strcmp(string[i], string[j]) == 0) {
            isSame = 1;
            break;
        }
        }
        if (isSame) {
        strcpy(string[i], saveString);
        /* Randomize choice for don't cares. */
        for (j = 0; j < n; j++) {
            if (string[i][indices[j]] == '2')
            string[i][indices[j]] =
              (char) ((Cudd_Random() & 0x20) ? '1' : '0');
        }
        }
    }

    old[i] = Cudd_ReadOne(dd);
    cuddRef(old[i]);

    for (j = 0; j < n; j++) {
        if (string[i][indices[j]] == '0') {
        neW = Cudd_bddAnd(dd,old[i],Cudd_Not(vars[j]));
        } else {
        neW = Cudd_bddAnd(dd,old[i],vars[j]);
        }
        if (neW == NULL) {
        FREE(saveString);
        for (l = 0; l < k; l++)
            FREE(string[l]);
        FREE(string);
        FREE(indices);
        for (l = 0; l <= i; l++)
            Cudd_RecursiveDeref(dd,old[l]);
        FREE(old);
        return(NULL);
        }
        cuddRef(neW);
        Cudd_RecursiveDeref(dd,old[i]);
        old[i] = neW;
    }

    /* Test. */
    if (!Cudd_bddLeq(dd,old[i],f)) {
        FREE(saveString);
        for (l = 0; l < k; l++)
        FREE(string[l]);
        FREE(string);
        FREE(indices);
        for (l = 0; l <= i; l++)
        Cudd_RecursiveDeref(dd,old[l]);
        FREE(old);
        return(NULL);
    }
    }

    FREE(saveString);
    for (i = 0; i < k; i++) {
    cuddDeref(old[i]);
    FREE(string[i]);
    }
    FREE(string);
    FREE(indices);
    return(old);

}  /* end of Cudd_bddPickArbitraryMinterms */


DdNode *
Cudd_SubsetWithMaskVars(
  DdManager * dd /* manager */,
  DdNode * f /* function from which to pick a cube */,
  DdNode ** vars /* array of variables */,
  int  nvars /* size of <code>vars</code> */,
  DdNode ** maskVars /* array of variables */,
  int  mvars /* size of <code>maskVars</code> */)
{
    double  *weight;
    char    *string;
    int     i, size;
    int     *indices, *mask;
    int     result;
    DdNode  *zero, *cube, *newCube, *subset;
    DdNode  *cof;

    DdNode  *support;
    support = Cudd_Support(dd,f);
    cuddRef(support);
    Cudd_RecursiveDeref(dd,support);

    zero = Cudd_Not(dd->one);
    size = dd->size;

    weight = ALLOC(double,size);
    if (weight == NULL) {
    dd->errorCode = CUDD_MEMORY_OUT;
    return(NULL);
    }
    for (i = 0; i < size; i++) {
    weight[i] = 0.0;
    }
    for (i = 0; i < mvars; i++) {
    cof = Cudd_Cofactor(dd, f, maskVars[i]);
    cuddRef(cof);
    weight[i] = Cudd_CountMinterm(dd, cof, nvars);
    Cudd_RecursiveDeref(dd,cof);

    cof = Cudd_Cofactor(dd, f, Cudd_Not(maskVars[i]));
    cuddRef(cof);
    weight[i] -= Cudd_CountMinterm(dd, cof, nvars);
    Cudd_RecursiveDeref(dd,cof);
    }

    string = ALLOC(char, size + 1);
    if (string == NULL) {
    dd->errorCode = CUDD_MEMORY_OUT;
    FREE(weight);
    return(NULL);
    }
    mask = ALLOC(int, size);
    if (mask == NULL) {
    dd->errorCode = CUDD_MEMORY_OUT;
    FREE(weight);
    FREE(string);
    return(NULL);
    }
    for (i = 0; i < size; i++) {
    string[i] = '2';
    mask[i] = 0;
    }
    string[size] = '\0';
    indices = ALLOC(int,nvars);
    if (indices == NULL) {
    dd->errorCode = CUDD_MEMORY_OUT;
    FREE(weight);
    FREE(string);
    FREE(mask);
    return(NULL);
    }
    for (i = 0; i < nvars; i++) {
    indices[i] = vars[i]->index;
    }

    result = ddPickRepresentativeCube(dd,f,weight,string);
    if (result == 0) {
    FREE(weight);
    FREE(string);
    FREE(mask);
    FREE(indices);
    return(NULL);
    }

    cube = Cudd_ReadOne(dd);
    cuddRef(cube);
    zero = Cudd_Not(Cudd_ReadOne(dd));
    for (i = 0; i < nvars; i++) {
    if (string[indices[i]] == '0') {
        newCube = Cudd_bddIte(dd,cube,Cudd_Not(vars[i]),zero);
    } else if (string[indices[i]] == '1') {
        newCube = Cudd_bddIte(dd,cube,vars[i],zero);
    } else
        continue;
    if (newCube == NULL) {
        FREE(weight);
        FREE(string);
        FREE(mask);
        FREE(indices);
        Cudd_RecursiveDeref(dd,cube);
        return(NULL);
    }
    cuddRef(newCube);
    Cudd_RecursiveDeref(dd,cube);
    cube = newCube;
    }
    Cudd_RecursiveDeref(dd,cube);

    for (i = 0; i < mvars; i++) {
    mask[maskVars[i]->index] = 1;
    }
    for (i = 0; i < nvars; i++) {
    if (mask[indices[i]]) {
        if (string[indices[i]] == '2') {
        if (weight[indices[i]] >= 0.0)
            string[indices[i]] = '1';
        else
            string[indices[i]] = '0';
        }
    } else {
        string[indices[i]] = '2';
    }
    }

    cube = Cudd_ReadOne(dd);
    cuddRef(cube);
    zero = Cudd_Not(Cudd_ReadOne(dd));

    /* Build result BDD. */
    for (i = 0; i < nvars; i++) {
    if (string[indices[i]] == '0') {
        newCube = Cudd_bddIte(dd,cube,Cudd_Not(vars[i]),zero);
    } else if (string[indices[i]] == '1') {
        newCube = Cudd_bddIte(dd,cube,vars[i],zero);
    } else
        continue;
    if (newCube == NULL) {
        FREE(weight);
        FREE(string);
        FREE(mask);
        FREE(indices);
        Cudd_RecursiveDeref(dd,cube);
        return(NULL);
    }
    cuddRef(newCube);
    Cudd_RecursiveDeref(dd,cube);
    cube = newCube;
    }

    subset = Cudd_bddAnd(dd,f,cube);
    cuddRef(subset);
    Cudd_RecursiveDeref(dd,cube);

    /* Test. */
    if (Cudd_bddLeq(dd,subset,f)) {
    cuddDeref(subset);
    } else {
    Cudd_RecursiveDeref(dd,subset);
    subset = NULL;
    }

    FREE(weight);
    FREE(string);
    FREE(mask);
    FREE(indices);
    return(subset);

} /* end of Cudd_SubsetWithMaskVars */


DdGen *
Cudd_FirstCube(
  DdManager * dd,
  DdNode * f,
  int ** cube,
  CUDD_VALUE_TYPE * value)
{
    DdGen *gen;
    DdNode *top, *treg, *next, *nreg, *prev, *preg;
    int i;
    int nvars;

    /* Sanity Check. */
    if (dd == NULL || f == NULL) return(NULL);

    /* Allocate generator an initialize it. */
    gen = ALLOC(DdGen,1);
    if (gen == NULL) {
    dd->errorCode = CUDD_MEMORY_OUT;
    return(NULL);
    }

    gen->manager = dd;
    gen->type = CUDD_GEN_CUBES;
    gen->status = CUDD_GEN_EMPTY;
    gen->gen.cubes.cube = NULL;
    gen->gen.cubes.value = DD_ZERO_VAL;
    gen->stack.sp = 0;
    gen->stack.stack = NULL;
    gen->node = NULL;

    nvars = dd->size;
    gen->gen.cubes.cube = ALLOC(int,nvars);
    if (gen->gen.cubes.cube == NULL) {
    dd->errorCode = CUDD_MEMORY_OUT;
    FREE(gen);
    return(NULL);
    }
    for (i = 0; i < nvars; i++) gen->gen.cubes.cube[i] = 2;

    /* The maximum stack depth is one plus the number of variables.
    ** because a path may have nodes at all levels, including the
    ** constant level.
    */
    gen->stack.stack = ALLOC(DdNodePtr, nvars+1);
    if (gen->stack.stack == NULL) {
    dd->errorCode = CUDD_MEMORY_OUT;
    FREE(gen->gen.cubes.cube);
    FREE(gen);
    return(NULL);
    }
    for (i = 0; i <= nvars; i++) gen->stack.stack[i] = NULL;

    /* Find the first cube of the onset. */
    gen->stack.stack[gen->stack.sp] = f; gen->stack.sp++;

    while (1) {
    top = gen->stack.stack[gen->stack.sp-1];
    treg = Cudd_Regular(top);
    if (!cuddIsConstant(treg)) {
        /* Take the else branch first. */
        gen->gen.cubes.cube[treg->index] = 0;
        next = cuddE(treg);
        if (top != treg) next = Cudd_Not(next);
        gen->stack.stack[gen->stack.sp] = next; gen->stack.sp++;
    } else if (top == Cudd_Not(DD_ONE(dd)) || top == dd->background) {
        /* Backtrack */
        while (1) {
        if (gen->stack.sp == 1) {
            /* The current node has no predecessor. */
            gen->status = CUDD_GEN_EMPTY;
            gen->stack.sp--;
            goto done;
        }
        prev = gen->stack.stack[gen->stack.sp-2];
        preg = Cudd_Regular(prev);
        nreg = cuddT(preg);
        if (prev != preg) {next = Cudd_Not(nreg);} else {next = nreg;}
        if (next != top) { /* follow the then branch next */
            gen->gen.cubes.cube[preg->index] = 1;
            gen->stack.stack[gen->stack.sp-1] = next;
            break;
        }
        /* Pop the stack and try again. */
        gen->gen.cubes.cube[preg->index] = 2;
        gen->stack.sp--;
        top = gen->stack.stack[gen->stack.sp-1];
        treg = Cudd_Regular(top);
        }
    } else {
        gen->status = CUDD_GEN_NONEMPTY;
        gen->gen.cubes.value = cuddV(top);
        goto done;
    }
    }

done:
    *cube = gen->gen.cubes.cube;
    *value = gen->gen.cubes.value;
    return(gen);

} /* end of Cudd_FirstCube */


int
Cudd_NextCube(
  DdGen * gen,
  int ** cube,
  CUDD_VALUE_TYPE * value)
{
    DdNode *top, *treg, *next, *nreg, *prev, *preg;
    DdManager *dd = gen->manager;

    /* Backtrack from previously reached terminal node. */
    while (1) {
    if (gen->stack.sp == 1) {
        /* The current node has no predecessor. */
        gen->status = CUDD_GEN_EMPTY;
        gen->stack.sp--;
        goto done;
    }
    top = gen->stack.stack[gen->stack.sp-1];
    treg = Cudd_Regular(top);
    prev = gen->stack.stack[gen->stack.sp-2];
    preg = Cudd_Regular(prev);
    nreg = cuddT(preg);
    if (prev != preg) {next = Cudd_Not(nreg);} else {next = nreg;}
    if (next != top) { /* follow the then branch next */
        gen->gen.cubes.cube[preg->index] = 1;
        gen->stack.stack[gen->stack.sp-1] = next;
        break;
    }
    /* Pop the stack and try again. */
    gen->gen.cubes.cube[preg->index] = 2;
    gen->stack.sp--;
    }

    while (1) {
    top = gen->stack.stack[gen->stack.sp-1];
    treg = Cudd_Regular(top);
    if (!cuddIsConstant(treg)) {
        /* Take the else branch first. */
        gen->gen.cubes.cube[treg->index] = 0;
        next = cuddE(treg);
        if (top != treg) next = Cudd_Not(next);
        gen->stack.stack[gen->stack.sp] = next; gen->stack.sp++;
    } else if (top == Cudd_Not(DD_ONE(dd)) || top == dd->background) {
        /* Backtrack */
        while (1) {
        if (gen->stack.sp == 1) {
            /* The current node has no predecessor. */
            gen->status = CUDD_GEN_EMPTY;
            gen->stack.sp--;
            goto done;
        }
        prev = gen->stack.stack[gen->stack.sp-2];
        preg = Cudd_Regular(prev);
        nreg = cuddT(preg);
        if (prev != preg) {next = Cudd_Not(nreg);} else {next = nreg;}
        if (next != top) { /* follow the then branch next */
            gen->gen.cubes.cube[preg->index] = 1;
            gen->stack.stack[gen->stack.sp-1] = next;
            break;
        }
        /* Pop the stack and try again. */
        gen->gen.cubes.cube[preg->index] = 2;
        gen->stack.sp--;
        top = gen->stack.stack[gen->stack.sp-1];
        treg = Cudd_Regular(top);
        }
    } else {
        gen->status = CUDD_GEN_NONEMPTY;
        gen->gen.cubes.value = cuddV(top);
        goto done;
    }
    }

done:
    if (gen->status == CUDD_GEN_EMPTY) return(0);
    *cube = gen->gen.cubes.cube;
    *value = gen->gen.cubes.value;
    return(1);

} /* end of Cudd_NextCube */


DdGen *
Cudd_FirstPrime(
  DdManager *dd,
  DdNode *l,
  DdNode *u,
  int **cube)
{
    DdGen *gen;
    DdNode *implicant, *prime, *tmp;
    int length, result;

    /* Sanity Check. */
    if (dd == NULL || l == NULL || u == NULL) return(NULL);

    /* Allocate generator an initialize it. */
    gen = ALLOC(DdGen,1);
    if (gen == NULL) {
    dd->errorCode = CUDD_MEMORY_OUT;
    return(NULL);
    }

    gen->manager = dd;
    gen->type = CUDD_GEN_PRIMES;
    gen->status = CUDD_GEN_EMPTY;
    gen->gen.primes.cube = NULL;
    gen->gen.primes.ub = u;
    gen->stack.sp = 0;
    gen->stack.stack = NULL;
    gen->node = l;
    cuddRef(l);

    gen->gen.primes.cube = ALLOC(int,dd->size);
    if (gen->gen.primes.cube == NULL) {
    dd->errorCode = CUDD_MEMORY_OUT;
    FREE(gen);
    return(NULL);
    }

    if (gen->node == Cudd_ReadLogicZero(dd)) {
    gen->status = CUDD_GEN_EMPTY;
    } else {
    implicant = Cudd_LargestCube(dd,gen->node,&length);
    if (implicant == NULL) {
        Cudd_RecursiveDeref(dd,gen->node);
        FREE(gen->gen.primes.cube);
        FREE(gen);
        return(NULL);
    }
    cuddRef(implicant);
    prime = Cudd_bddMakePrime(dd,implicant,gen->gen.primes.ub);
    if (prime == NULL) {
        Cudd_RecursiveDeref(dd,gen->node);
        Cudd_RecursiveDeref(dd,implicant);
        FREE(gen->gen.primes.cube);
        FREE(gen);
        return(NULL);
    }
    cuddRef(prime);
    Cudd_RecursiveDeref(dd,implicant);
    tmp = Cudd_bddAnd(dd,gen->node,Cudd_Not(prime));
    if (tmp == NULL) {
        Cudd_RecursiveDeref(dd,gen->node);
        Cudd_RecursiveDeref(dd,prime);
        FREE(gen->gen.primes.cube);
        FREE(gen);
        return(NULL);
    }
    cuddRef(tmp);
    Cudd_RecursiveDeref(dd,gen->node);
    gen->node = tmp;
    result = Cudd_BddToCubeArray(dd,prime,gen->gen.primes.cube);
    if (result == 0) {
        Cudd_RecursiveDeref(dd,gen->node);
        Cudd_RecursiveDeref(dd,prime);
        FREE(gen->gen.primes.cube);
        FREE(gen);
        return(NULL);
    }
    Cudd_RecursiveDeref(dd,prime);
    gen->status = CUDD_GEN_NONEMPTY;
    }
    *cube = gen->gen.primes.cube;
    return(gen);

} /* end of Cudd_FirstPrime */


int
Cudd_NextPrime(
  DdGen *gen,
  int **cube)
{
    DdNode *implicant, *prime, *tmp;
    DdManager *dd = gen->manager;
    int length, result;

    if (gen->node == Cudd_ReadLogicZero(dd)) {
    gen->status = CUDD_GEN_EMPTY;
    } else {
    implicant = Cudd_LargestCube(dd,gen->node,&length);
    if (implicant == NULL) {
        gen->status = CUDD_GEN_EMPTY;
        return(0);
    }
    cuddRef(implicant);
    prime = Cudd_bddMakePrime(dd,implicant,gen->gen.primes.ub);
    if (prime == NULL) {
        Cudd_RecursiveDeref(dd,implicant);
        gen->status = CUDD_GEN_EMPTY;
        return(0);
    }
    cuddRef(prime);
    Cudd_RecursiveDeref(dd,implicant);
    tmp = Cudd_bddAnd(dd,gen->node,Cudd_Not(prime));
    if (tmp == NULL) {
        Cudd_RecursiveDeref(dd,prime);
        gen->status = CUDD_GEN_EMPTY;
        return(0);
    }
    cuddRef(tmp);
    Cudd_RecursiveDeref(dd,gen->node);
    gen->node = tmp;
    result = Cudd_BddToCubeArray(dd,prime,gen->gen.primes.cube);
    if (result == 0) {
        Cudd_RecursiveDeref(dd,prime);
        gen->status = CUDD_GEN_EMPTY;
        return(0);
    }
    Cudd_RecursiveDeref(dd,prime);
    gen->status = CUDD_GEN_NONEMPTY;
    }
    if (gen->status == CUDD_GEN_EMPTY) return(0);
    *cube = gen->gen.primes.cube;
    return(1);

} /* end of Cudd_NextPrime */


DdNode *
Cudd_bddComputeCube(
  DdManager * dd,
  DdNode ** vars,
  int * phase,
  int  n)
{
    DdNode  *cube;
    DdNode  *fn;
    int         i;

    cube = DD_ONE(dd);
    cuddRef(cube);

    for (i = n - 1; i >= 0; i--) {
    if (phase == NULL || phase[i] != 0) {
        fn = Cudd_bddAnd(dd,vars[i],cube);
    } else {
        fn = Cudd_bddAnd(dd,Cudd_Not(vars[i]),cube);
    }
    if (fn == NULL) {
        Cudd_RecursiveDeref(dd,cube);
        return(NULL);
    }
    cuddRef(fn);
    Cudd_RecursiveDeref(dd,cube);
    cube = fn;
    }
    cuddDeref(cube);

    return(cube);

}  /* end of Cudd_bddComputeCube */


DdNode *
Cudd_addComputeCube(
  DdManager * dd,
  DdNode ** vars,
  int * phase,
  int  n)
{
    DdNode  *cube, *zero;
    DdNode  *fn;
    int         i;

    cube = DD_ONE(dd);
    cuddRef(cube);
    zero = DD_ZERO(dd);

    for (i = n - 1; i >= 0; i--) {
    if (phase == NULL || phase[i] != 0) {
        fn = Cudd_addIte(dd,vars[i],cube,zero);
    } else {
        fn = Cudd_addIte(dd,vars[i],zero,cube);
    }
    if (fn == NULL) {
        Cudd_RecursiveDeref(dd,cube);
        return(NULL);
    }
    cuddRef(fn);
    Cudd_RecursiveDeref(dd,cube);
    cube = fn;
    }
    cuddDeref(cube);

    return(cube);

} /* end of Cudd_addComputeCube */


DdNode *
Cudd_CubeArrayToBdd(
  DdManager *dd,
  int *array)
{
    DdNode *cube, *var, *tmp;
    int i;
    int size = Cudd_ReadSize(dd);

    cube = DD_ONE(dd);
    cuddRef(cube);
    for (i = size - 1; i >= 0; i--) {
    if ((array[i] & ~1) == 0) {
        var = Cudd_bddIthVar(dd,i);
        tmp = Cudd_bddAnd(dd,cube,Cudd_NotCond(var,array[i]==0));
        if (tmp == NULL) {
        Cudd_RecursiveDeref(dd,cube);
        return(NULL);
        }
        cuddRef(tmp);
        Cudd_RecursiveDeref(dd,cube);
        cube = tmp;
    }
    }
    cuddDeref(cube);
    return(cube);

} /* end of Cudd_CubeArrayToBdd */


int
Cudd_BddToCubeArray(
  DdManager *dd,
  DdNode *cube,
  int *array)
{
    DdNode *scan, *t, *e;
    int i;
    int size = Cudd_ReadSize(dd);
    DdNode *zero = Cudd_Not(DD_ONE(dd));

    for (i = size-1; i >= 0; i--) {
    array[i] = 2;
    }
    scan = cube;
    while (!Cudd_IsConstant(scan)) {
    int index = Cudd_Regular(scan)->index;
    cuddGetBranches(scan,&t,&e);
    if (t == zero) {
        array[index] = 0;
        scan = e;
    } else if (e == zero) {
        array[index] = 1;
        scan = t;
    } else {
        return(0);  /* cube is not a cube */
    }
    }
    if (scan == zero) {
    return(0);
    } else {
    return(1);
    }

} /* end of Cudd_BddToCubeArray */


DdGen *
Cudd_FirstNode(
  DdManager * dd,
  DdNode * f,
  DdNode ** node)
{
    DdGen *gen;
    int size;

    /* Sanity Check. */
    if (dd == NULL || f == NULL) return(NULL);

    /* Allocate generator an initialize it. */
    gen = ALLOC(DdGen,1);
    if (gen == NULL) {
    dd->errorCode = CUDD_MEMORY_OUT;
    return(NULL);
    }

    gen->manager = dd;
    gen->type = CUDD_GEN_NODES;
    gen->status = CUDD_GEN_EMPTY;
    gen->stack.sp = 0;
    gen->node = NULL;

    /* Collect all the nodes on the generator stack for later perusal. */
    gen->stack.stack = cuddNodeArray(Cudd_Regular(f), &size);
    if (gen->stack.stack == NULL) {
    FREE(gen);
    dd->errorCode = CUDD_MEMORY_OUT;
    return(NULL);
    }
    gen->gen.nodes.size = size;

    /* Find the first node. */
    if (gen->stack.sp < gen->gen.nodes.size) {
    gen->status = CUDD_GEN_NONEMPTY;
    gen->node = gen->stack.stack[gen->stack.sp];
    *node = gen->node;
    }

    return(gen);

} /* end of Cudd_FirstNode */


int
Cudd_NextNode(
  DdGen * gen,
  DdNode ** node)
{
    /* Find the next node. */
    gen->stack.sp++;
    if (gen->stack.sp < gen->gen.nodes.size) {
    gen->node = gen->stack.stack[gen->stack.sp];
    *node = gen->node;
    return(1);
    } else {
    gen->status = CUDD_GEN_EMPTY;
    return(0);
    }

} /* end of Cudd_NextNode */


int
Cudd_GenFree(
  DdGen * gen)
{
    if (gen == NULL) return(0);
    switch (gen->type) {
    case CUDD_GEN_CUBES:
    case CUDD_GEN_ZDD_PATHS:
    FREE(gen->gen.cubes.cube);
    FREE(gen->stack.stack);
    break;
    case CUDD_GEN_PRIMES:
    FREE(gen->gen.primes.cube);
    Cudd_RecursiveDeref(gen->manager,gen->node);
    break;
    case CUDD_GEN_NODES:
    FREE(gen->stack.stack);
    break;
    default:
    return(0);
    }
    FREE(gen);
    return(0);

} /* end of Cudd_GenFree */


int
Cudd_IsGenEmpty(
  DdGen * gen)
{
    if (gen == NULL) return(1);
    return(gen->status == CUDD_GEN_EMPTY);

} /* end of Cudd_IsGenEmpty */


DdNode *
Cudd_IndicesToCube(
  DdManager * dd,
  int * array,
  int  n)
{
    DdNode *cube, *tmp;
    int i;

    cube = DD_ONE(dd);
    cuddRef(cube);
    for (i = n - 1; i >= 0; i--) {
    tmp = Cudd_bddAnd(dd,Cudd_bddIthVar(dd,array[i]),cube);
    if (tmp == NULL) {
        Cudd_RecursiveDeref(dd,cube);
        return(NULL);
    }
    cuddRef(tmp);
    Cudd_RecursiveDeref(dd,cube);
    cube = tmp;
    }

    cuddDeref(cube);
    return(cube);

} /* end of Cudd_IndicesToCube */


void
Cudd_PrintVersion(
  FILE * fp)
{
    (void) fprintf(fp, "%s\n", CUDD_VERSION);

} /* end of Cudd_PrintVersion */


double
Cudd_AverageDistance(
  DdManager * dd)
{
    double tetotal, nexttotal;
    double tesubtotal, nextsubtotal;
    double temeasured, nextmeasured;
    int i, j;
    int slots, nvars;
    long diff;
    DdNode *scan;
    DdNodePtr *nodelist;
    DdNode *sentinel = &(dd->sentinel);

    nvars = dd->size;
    if (nvars == 0) return(0.0);

    /* Initialize totals. */
    tetotal = 0.0;
    nexttotal = 0.0;
    temeasured = 0.0;
    nextmeasured = 0.0;

    /* Scan the variable subtables. */
    for (i = 0; i < nvars; i++) {
    nodelist = dd->subtables[i].nodelist;
    tesubtotal = 0.0;
    nextsubtotal = 0.0;
    slots = dd->subtables[i].slots;
    for (j = 0; j < slots; j++) {
        scan = nodelist[j];
        while (scan != sentinel) {
        diff = (long) scan - (long) cuddT(scan);
        tesubtotal += (double) ddAbs(diff);
        diff = (long) scan - (long) Cudd_Regular(cuddE(scan));
        tesubtotal += (double) ddAbs(diff);
        temeasured += 2.0;
        if (scan->next != sentinel) {
            diff = (long) scan - (long) scan->next;
            nextsubtotal += (double) ddAbs(diff);
            nextmeasured += 1.0;
        }
        scan = scan->next;
        }
    }
    tetotal += tesubtotal;
    nexttotal += nextsubtotal;
    }

    /* Scan the constant table. */
    nodelist = dd->constants.nodelist;
    nextsubtotal = 0.0;
    slots = dd->constants.slots;
    for (j = 0; j < slots; j++) {
    scan = nodelist[j];
    while (scan != NULL) {
        if (scan->next != NULL) {
        diff = (long) scan - (long) scan->next;
        nextsubtotal += (double) ddAbs(diff);
        nextmeasured += 1.0;
        }
        scan = scan->next;
    }
    }
    nexttotal += nextsubtotal;

    return((tetotal + nexttotal) / (temeasured + nextmeasured));

} /* end of Cudd_AverageDistance */


long
Cudd_Random(void)
{
    int i;  /* index in the shuffle table */
    long int w; /* work variable */

    /* cuddRand == 0 if the geneartor has not been initialized yet. */
    if (cuddRand == 0) Cudd_Srandom(1);

    /* Compute cuddRand = (cuddRand * LEQA1) % MODULUS1 avoiding
    ** overflows by Schrage's method.
    */
    w          = cuddRand / LEQQ1;
    cuddRand   = LEQA1 * (cuddRand - w * LEQQ1) - w * LEQR1;
    cuddRand  += (cuddRand < 0) * MODULUS1;

    /* Compute cuddRand2 = (cuddRand2 * LEQA2) % MODULUS2 avoiding
    ** overflows by Schrage's method.
    */
    w          = cuddRand2 / LEQQ2;
    cuddRand2  = LEQA2 * (cuddRand2 - w * LEQQ2) - w * LEQR2;
    cuddRand2 += (cuddRand2 < 0) * MODULUS2;

    /* cuddRand is shuffled with the Bays-Durham algorithm.
    ** shuffleSelect and cuddRand2 are combined to generate the output.
    */

    /* Pick one element from the shuffle table; "i" will be in the range
    ** from 0 to STAB_SIZE-1.
    */
    i = (int) (shuffleSelect / STAB_DIV);
    /* Mix the element of the shuffle table with the current iterate of
    ** the second sub-generator, and replace the chosen element of the
    ** shuffle table with the current iterate of the first sub-generator.
    */
    shuffleSelect   = shuffleTable[i] - cuddRand2;
    shuffleTable[i] = cuddRand;
    shuffleSelect  += (shuffleSelect < 1) * (MODULUS1 - 1);
    /* Since shuffleSelect != 0, and we want to be able to return 0,
    ** here we subtract 1 before returning.
    */
    return(shuffleSelect - 1);

} /* end of Cudd_Random */


void
Cudd_Srandom(
  long  seed)
{
    int i;

    if (seed < 0)       cuddRand = -seed;
    else if (seed == 0) cuddRand = 1;
    else                cuddRand = seed;
    cuddRand2 = cuddRand;
    /* Load the shuffle table (after 11 warm-ups). */
    for (i = 0; i < STAB_SIZE + 11; i++) {
    long int w;
    w = cuddRand / LEQQ1;
    cuddRand = LEQA1 * (cuddRand - w * LEQQ1) - w * LEQR1;
    cuddRand += (cuddRand < 0) * MODULUS1;
    shuffleTable[i % STAB_SIZE] = cuddRand;
    }
    shuffleSelect = shuffleTable[1 % STAB_SIZE];

} /* end of Cudd_Srandom */


double
Cudd_Density(
  DdManager * dd /* manager */,
  DdNode * f /* function whose density is sought */,
  int  nvars /* size of the support of f */)
{
    double minterms;
    int nodes;
    double density;

    if (nvars == 0) nvars = dd->size;
    minterms = Cudd_CountMinterm(dd,f,nvars);
    if (minterms == (double) CUDD_OUT_OF_MEM) return(minterms);
    nodes = Cudd_DagSize(f);
    density = minterms / (double) nodes;
    return(density);

} /* end of Cudd_Density */


void
Cudd_OutOfMem(
  long size /* size of the allocation that failed */)
{
    (void) fflush(stdout);
    (void) fprintf(stderr, "\nunable to allocate %ld bytes\n", size);
    return;

} /* end of Cudd_OutOfMem */


/*---------------------------------------------------------------------------*/
/* Definition of internal functions                                          */
/*---------------------------------------------------------------------------*/


int
cuddP(
  DdManager * dd,
  DdNode * f)
{
    int retval;
    st_table *table = st_init_table(st_ptrcmp,st_ptrhash);

    if (table == NULL) return(0);

    retval = dp2(dd,f,table);
    st_free_table(table);
    (void) fputc('\n',dd->out);
    return(retval);

} /* end of cuddP */


enum st_retval
cuddStCountfree(
  char * key,
  char * value,
  char * arg)
{
    double  *d;

    d = (double *)value;
    FREE(d);
    return(ST_CONTINUE);

} /* end of cuddStCountfree */


int
cuddCollectNodes(
  DdNode * f,
  st_table * visited)
{
    DdNode  *T, *E;
    int     retval;

#ifdef DD_DEBUG
    assert(!Cudd_IsComplement(f));
#endif

    /* If already visited, nothing to do. */
    if (st_is_member(visited, (char *) f) == 1)
    return(1);

    /* Check for abnormal condition that should never happen. */
    if (f == NULL)
    return(0);

    /* Mark node as visited. */
    if (st_add_direct(visited, (char *) f, NULL) == ST_OUT_OF_MEM)
    return(0);

    /* Check terminal case. */
    if (cuddIsConstant(f))
    return(1);

    /* Recursive calls. */
    T = cuddT(f);
    retval = cuddCollectNodes(T,visited);
    if (retval != 1) return(retval);
    E = Cudd_Regular(cuddE(f));
    retval = cuddCollectNodes(E,visited);
    return(retval);

} /* end of cuddCollectNodes */


DdNodePtr *
cuddNodeArray(
  DdNode *f,
  int *n)
{
    DdNodePtr *table;
    int size, retval;

    size = ddDagInt(Cudd_Regular(f));
    table = ALLOC(DdNodePtr, size);
    if (table == NULL) {
    ddClearFlag(Cudd_Regular(f));
    return(NULL);
    }

    retval = cuddNodeArrayRecur(f, table, 0);
    assert(retval == size);

    *n = size;
    return(table);

} /* cuddNodeArray */


/*---------------------------------------------------------------------------*/
/* Definition of static functions                                            */
/*---------------------------------------------------------------------------*/


static int
dp2(
  DdManager *dd,
  DdNode * f,
  st_table * t)
{
    DdNode *g, *n, *N;
    int T,E;

    if (f == NULL) {
    return(0);
    }
    g = Cudd_Regular(f);
    if (cuddIsConstant(g)) {
#if SIZEOF_VOID_P == 8
    (void) fprintf(dd->out,"ID = %c0x%lx\tvalue = %-9g\n", bang(f),
        (ptruint) g / (ptruint) sizeof(DdNode),cuddV(g));
#else
    (void) fprintf(dd->out,"ID = %c0x%x\tvalue = %-9g\n", bang(f),
        (ptruint) g / (ptruint) sizeof(DdNode),cuddV(g));
#endif
    return(1);
    }
    if (st_is_member(t,(char *) g) == 1) {
    return(1);
    }
    if (st_add_direct(t,(char *) g,NULL) == ST_OUT_OF_MEM)
    return(0);
#ifdef DD_STATS
#if SIZEOF_VOID_P == 8
    (void) fprintf(dd->out,"ID = %c0x%lx\tindex = %d\tr = %d\t", bang(f),
        (ptruint) g / (ptruint) sizeof(DdNode), g->index, g->ref);
#else
    (void) fprintf(dd->out,"ID = %c0x%x\tindex = %d\tr = %d\t", bang(f),
        (ptruint) g / (ptruint) sizeof(DdNode),g->index,g->ref);
#endif
#else
#if SIZEOF_VOID_P == 8
    (void) fprintf(dd->out,"ID = %c0x%lx\tindex = %u\t", bang(f),
        (ptruint) g / (ptruint) sizeof(DdNode),g->index);
#else
    (void) fprintf(dd->out,"ID = %c0x%x\tindex = %hu\t", bang(f),
        (ptruint) g / (ptruint) sizeof(DdNode),g->index);
#endif
#endif
    n = cuddT(g);
    if (cuddIsConstant(n)) {
    (void) fprintf(dd->out,"T = %-9g\t",cuddV(n));
    T = 1;
    } else {
#if SIZEOF_VOID_P == 8
    (void) fprintf(dd->out,"T = 0x%lx\t",(ptruint) n / (ptruint) sizeof(DdNode));
#else
    (void) fprintf(dd->out,"T = 0x%x\t",(ptruint) n / (ptruint) sizeof(DdNode));
#endif
    T = 0;
    }

    n = cuddE(g);
    N = Cudd_Regular(n);
    if (cuddIsConstant(N)) {
    (void) fprintf(dd->out,"E = %c%-9g\n",bang(n),cuddV(N));
    E = 1;
    } else {
#if SIZEOF_VOID_P == 8
    (void) fprintf(dd->out,"E = %c0x%lx\n", bang(n), (ptruint) N/(ptruint) sizeof(DdNode));
#else
    (void) fprintf(dd->out,"E = %c0x%x\n", bang(n), (ptruint) N/(ptruint) sizeof(DdNode));
#endif
    E = 0;
    }
    if (E == 0) {
    if (dp2(dd,N,t) == 0)
        return(0);
    }
    if (T == 0) {
    if (dp2(dd,cuddT(g),t) == 0)
        return(0);
    }
    return(1);

} /* end of dp2 */


static void
ddPrintMintermAux(
  DdManager * dd /* manager */,
  DdNode * node /* current node */,
  int * list /* current recursion path */)
{
    DdNode  *N,*Nv,*Nnv;
    int     i,v,index;

    N = Cudd_Regular(node);

    if (cuddIsConstant(N)) {
    /* Terminal case: Print one cube based on the current recursion
    ** path, unless we have reached the background value (ADDs) or
    ** the logical zero (BDDs).
    */
    if (node != background && node != zero) {
        for (i = 0; i < dd->size; i++) {
        v = list[i];
        if (v == 0) (void) fprintf(dd->out,"0");
        else if (v == 1) (void) fprintf(dd->out,"1");
        else (void) fprintf(dd->out,"-");
        }
        (void) fprintf(dd->out," % g\n", cuddV(node));
    }
    } else {
    Nv  = cuddT(N);
    Nnv = cuddE(N);
    if (Cudd_IsComplement(node)) {
        Nv  = Cudd_Not(Nv);
        Nnv = Cudd_Not(Nnv);
    }
    index = N->index;
    list[index] = 0;
    ddPrintMintermAux(dd,Nnv,list);
    list[index] = 1;
    ddPrintMintermAux(dd,Nv,list);
    list[index] = 2;
    }
    return;

} /* end of ddPrintMintermAux */


static int
ddDagInt(
  DdNode * n)
{
    int tval, eval;

    if (Cudd_IsComplement(n->next)) {
    return(0);
    }
    n->next = Cudd_Not(n->next);
    if (cuddIsConstant(n)) {
    return(1);
    }
    tval = ddDagInt(cuddT(n));
    eval = ddDagInt(Cudd_Regular(cuddE(n)));
    return(1 + tval + eval);

} /* end of ddDagInt */


static int
cuddNodeArrayRecur(
  DdNode *f,
  DdNodePtr *table,
  int index)
{
    int tindex, eindex;

    if (!Cudd_IsComplement(f->next)) {
    return(index);
    }
    /* Clear visited flag. */
    f->next = Cudd_Regular(f->next);
    if (cuddIsConstant(f)) {
    table[index] = f;
    return(index + 1);
    }
    tindex = cuddNodeArrayRecur(cuddT(f), table, index);
    eindex = cuddNodeArrayRecur(Cudd_Regular(cuddE(f)), table, tindex);
    table[eindex] = f;
    return(eindex + 1);

} /* end of cuddNodeArrayRecur */


static int
cuddEstimateCofactor(
  DdManager *dd,
  st_table *table,
  DdNode * node,
  int i,
  int phase,
  DdNode ** ptr)
{
    int tval, eval, val;
    DdNode *ptrT, *ptrE;

    if (Cudd_IsComplement(node->next)) {
    if (!st_lookup(table,(char *)node,(char **)ptr)) {
        if (st_add_direct(table,(char *)node,(char *)node) ==
        ST_OUT_OF_MEM)
        return(CUDD_OUT_OF_MEM);
        *ptr = node;
    }
    return(0);
    }
    node->next = Cudd_Not(node->next);
    if (cuddIsConstant(node)) {
    *ptr = node;
    if (st_add_direct(table,(char *)node,(char *)node) == ST_OUT_OF_MEM)
        return(CUDD_OUT_OF_MEM);
    return(1);
    }
    if ((int) node->index == i) {
    if (phase == 1) {
        *ptr = cuddT(node);
        val = ddDagInt(cuddT(node));
    } else {
        *ptr = cuddE(node);
        val = ddDagInt(Cudd_Regular(cuddE(node)));
    }
    if (node->ref > 1) {
        if (st_add_direct(table,(char *)node,(char *)*ptr) ==
        ST_OUT_OF_MEM)
        return(CUDD_OUT_OF_MEM);
    }
    return(val);
    }
    if (dd->perm[node->index] > dd->perm[i]) {
    *ptr = node;
    tval = ddDagInt(cuddT(node));
    eval = ddDagInt(Cudd_Regular(cuddE(node)));
    if (node->ref > 1) {
        if (st_add_direct(table,(char *)node,(char *)node) ==
        ST_OUT_OF_MEM)
        return(CUDD_OUT_OF_MEM);
    }
    val = 1 + tval + eval;
    return(val);
    }
    tval = cuddEstimateCofactor(dd,table,cuddT(node),i,phase,&ptrT);
    eval = cuddEstimateCofactor(dd,table,Cudd_Regular(cuddE(node)),i,
                phase,&ptrE);
    ptrE = Cudd_NotCond(ptrE,Cudd_IsComplement(cuddE(node)));
    if (ptrT == ptrE) {     /* recombination */
    *ptr = ptrT;
    val = tval;
    if (node->ref > 1) {
        if (st_add_direct(table,(char *)node,(char *)*ptr) ==
            ST_OUT_OF_MEM)
        return(CUDD_OUT_OF_MEM);
    }
    } else if ((ptrT != cuddT(node) || ptrE != cuddE(node)) &&
           (*ptr = cuddUniqueLookup(dd,node->index,ptrT,ptrE)) != NULL) {
    if (Cudd_IsComplement((*ptr)->next)) {
        val = 0;
    } else {
        val = 1 + tval + eval;
    }
    if (node->ref > 1) {
        if (st_add_direct(table,(char *)node,(char *)*ptr) ==
            ST_OUT_OF_MEM)
        return(CUDD_OUT_OF_MEM);
    }
    } else {
    *ptr = node;
    val = 1 + tval + eval;
    }
    return(val);

} /* end of cuddEstimateCofactor */


static DdNode *
cuddUniqueLookup(
  DdManager * unique,
  int  index,
  DdNode * T,
  DdNode * E)
{
    int posn;
    unsigned int level;
    DdNodePtr *nodelist;
    DdNode *looking;
    DdSubtable *subtable;

    if (index >= unique->size) {
    return(NULL);
    }

    level = unique->perm[index];
    subtable = &(unique->subtables[level]);

#ifdef DD_DEBUG
    assert(level < (unsigned) cuddI(unique,T->index));
    assert(level < (unsigned) cuddI(unique,Cudd_Regular(E)->index));
#endif

    posn = ddHash(T, E, subtable->shift);
    nodelist = subtable->nodelist;
    looking = nodelist[posn];

    while (T < cuddT(looking)) {
    looking = Cudd_Regular(looking->next);
    }
    while (T == cuddT(looking) && E < cuddE(looking)) {
    looking = Cudd_Regular(looking->next);
    }
    if (cuddT(looking) == T && cuddE(looking) == E) {
    return(looking);
    }

    return(NULL);

} /* end of cuddUniqueLookup */


static int
cuddEstimateCofactorSimple(
  DdNode * node,
  int i)
{
    int tval, eval;

    if (Cudd_IsComplement(node->next)) {
    return(0);
    }
    node->next = Cudd_Not(node->next);
    if (cuddIsConstant(node)) {
    return(1);
    }
    tval = cuddEstimateCofactorSimple(cuddT(node),i);
    if ((int) node->index == i) return(tval);
    eval = cuddEstimateCofactorSimple(Cudd_Regular(cuddE(node)),i);
    return(1 + tval + eval);

} /* end of cuddEstimateCofactorSimple */


static double
ddCountMintermAux(
  DdNode * node,
  double  max,
  DdHashTable * table)
{
    DdNode  *N, *Nt, *Ne;
    double  min, minT, minE;
    DdNode  *res;

    N = Cudd_Regular(node);

    if (cuddIsConstant(N)) {
    if (node == background || node == zero) {
        return(0.0);
    } else {
        return(max);
    }
    }
    if (N->ref != 1 && (res = cuddHashTableLookup1(table,node)) != NULL) {
    min = cuddV(res);
    if (res->ref == 0) {
        table->manager->dead++;
        table->manager->constants.dead++;
    }
    return(min);
    }

    Nt = cuddT(N); Ne = cuddE(N);
    if (Cudd_IsComplement(node)) {
    Nt = Cudd_Not(Nt); Ne = Cudd_Not(Ne);
    }

    minT = ddCountMintermAux(Nt,max,table);
    if (minT == (double)CUDD_OUT_OF_MEM) return((double)CUDD_OUT_OF_MEM);
    minT *= 0.5;
    minE = ddCountMintermAux(Ne,max,table);
    if (minE == (double)CUDD_OUT_OF_MEM) return((double)CUDD_OUT_OF_MEM);
    minE *= 0.5;
    min = minT + minE;

    if (N->ref != 1) {
    ptrint fanout = (ptrint) N->ref;
    cuddSatDec(fanout);
    res = cuddUniqueConst(table->manager,min);
    if (!cuddHashTableInsert1(table,node,res,fanout)) {
        cuddRef(res); Cudd_RecursiveDeref(table->manager, res);
        return((double)CUDD_OUT_OF_MEM);
    }
    }

    return(min);

} /* end of ddCountMintermAux */


static double
ddCountPathAux(
  DdNode * node,
  st_table * table)
{

    DdNode  *Nv, *Nnv;
    double  paths, *ppaths, paths1, paths2;
    double  *dummy;


    if (cuddIsConstant(node)) {
    return(1.0);
    }
    if (st_lookup(table, node, &dummy)) {
    paths = *dummy;
    return(paths);
    }

    Nv = cuddT(node); Nnv = cuddE(node);

    paths1 = ddCountPathAux(Nv,table);
    if (paths1 == (double)CUDD_OUT_OF_MEM) return((double)CUDD_OUT_OF_MEM);
    paths2 = ddCountPathAux(Cudd_Regular(Nnv),table);
    if (paths2 == (double)CUDD_OUT_OF_MEM) return((double)CUDD_OUT_OF_MEM);
    paths = paths1 + paths2;

    ppaths = ALLOC(double,1);
    if (ppaths == NULL) {
    return((double)CUDD_OUT_OF_MEM);
    }

    *ppaths = paths;

    if (st_add_direct(table,(char *)node, (char *)ppaths) == ST_OUT_OF_MEM) {
    FREE(ppaths);
    return((double)CUDD_OUT_OF_MEM);
    }
    return(paths);

} /* end of ddCountPathAux */


static int
ddEpdCountMintermAux(
  DdNode * node,
  EpDouble * max,
  EpDouble * epd,
  st_table * table)
{
    DdNode  *Nt, *Ne;
    EpDouble    *min, minT, minE;
    EpDouble    *res;
    int     status;

    /* node is assumed to be regular */
    if (cuddIsConstant(node)) {
    if (node == background || node == zero) {
        EpdMakeZero(epd, 0);
    } else {
        EpdCopy(max, epd);
    }
    return(0);
    }
    if (node->ref != 1 && st_lookup(table, node, &res)) {
    EpdCopy(res, epd);
    return(0);
    }

    Nt = cuddT(node); Ne = cuddE(node);

    status = ddEpdCountMintermAux(Nt,max,&minT,table);
    if (status == CUDD_OUT_OF_MEM) return(CUDD_OUT_OF_MEM);
    EpdMultiply(&minT, (double)0.5);
    status = ddEpdCountMintermAux(Cudd_Regular(Ne),max,&minE,table);
    if (status == CUDD_OUT_OF_MEM) return(CUDD_OUT_OF_MEM);
    if (Cudd_IsComplement(Ne)) {
    EpdSubtract3(max, &minE, epd);
    EpdCopy(epd, &minE);
    }
    EpdMultiply(&minE, (double)0.5);
    EpdAdd3(&minT, &minE, epd);

    if (node->ref > 1) {
    min = EpdAlloc();
    if (!min)
        return(CUDD_OUT_OF_MEM);
    EpdCopy(epd, min);
    if (st_insert(table, (char *)node, (char *)min) == ST_OUT_OF_MEM) {
        EpdFree(min);
        return(CUDD_OUT_OF_MEM);
    }
    }

    return(0);

} /* end of ddEpdCountMintermAux */


static double
ddCountPathsToNonZero(
  DdNode * N,
  st_table * table)
{

    DdNode  *node, *Nt, *Ne;
    double  paths, *ppaths, paths1, paths2;
    double  *dummy;

    node = Cudd_Regular(N);
    if (cuddIsConstant(node)) {
    return((double) !(Cudd_IsComplement(N) || cuddV(node)==DD_ZERO_VAL));
    }
    if (st_lookup(table, N, &dummy)) {
    paths = *dummy;
    return(paths);
    }

    Nt = cuddT(node); Ne = cuddE(node);
    if (node != N) {
    Nt = Cudd_Not(Nt); Ne = Cudd_Not(Ne);
    }

    paths1 = ddCountPathsToNonZero(Nt,table);
    if (paths1 == (double)CUDD_OUT_OF_MEM) return((double)CUDD_OUT_OF_MEM);
    paths2 = ddCountPathsToNonZero(Ne,table);
    if (paths2 == (double)CUDD_OUT_OF_MEM) return((double)CUDD_OUT_OF_MEM);
    paths = paths1 + paths2;

    ppaths = ALLOC(double,1);
    if (ppaths == NULL) {
    return((double)CUDD_OUT_OF_MEM);
    }

    *ppaths = paths;

    if (st_add_direct(table,(char *)N, (char *)ppaths) == ST_OUT_OF_MEM) {
    FREE(ppaths);
    return((double)CUDD_OUT_OF_MEM);
    }
    return(paths);

} /* end of ddCountPathsToNonZero */


static void
ddSupportStep(
  DdNode * f,
  int * support)
{
    if (cuddIsConstant(f) || Cudd_IsComplement(f->next))
    return;

    support[f->index] = 1;
    ddSupportStep(cuddT(f),support);
    ddSupportStep(Cudd_Regular(cuddE(f)),support);
    /* Mark as visited. */
    f->next = Cudd_Complement(f->next);

} /* end of ddSupportStep */


static void
ddClearFlag(
  DdNode * f)
{
    if (!Cudd_IsComplement(f->next)) {
    return;
    }
    /* Clear visited flag. */
    f->next = Cudd_Regular(f->next);
    if (cuddIsConstant(f)) {
    return;
    }
    ddClearFlag(cuddT(f));
    ddClearFlag(Cudd_Regular(cuddE(f)));
    return;

} /* end of ddClearFlag */


static int
ddLeavesInt(
  DdNode * n)
{
    int tval, eval;

    if (Cudd_IsComplement(n->next)) {
    return(0);
    }
    n->next = Cudd_Not(n->next);
    if (cuddIsConstant(n)) {
    return(1);
    }
    tval = ddLeavesInt(cuddT(n));
    eval = ddLeavesInt(Cudd_Regular(cuddE(n)));
    return(tval + eval);

} /* end of ddLeavesInt */


static int
ddPickArbitraryMinterms(
  DdManager *dd,
  DdNode *node,
  int nvars,
  int nminterms,
  char **string)
{
    DdNode *N, *T, *E;
    DdNode *one, *bzero;
    int    i, t, result;
    double min1, min2;

    if (string == NULL || node == NULL) return(0);

    /* The constant 0 function has no on-set cubes. */
    one = DD_ONE(dd);
    bzero = Cudd_Not(one);
    if (nminterms == 0 || node == bzero) return(1);
    if (node == one) {
    return(1);
    }

    N = Cudd_Regular(node);
    T = cuddT(N); E = cuddE(N);
    if (Cudd_IsComplement(node)) {
    T = Cudd_Not(T); E = Cudd_Not(E);
    }

    min1 = Cudd_CountMinterm(dd, T, nvars) / 2.0;
    if (min1 == (double)CUDD_OUT_OF_MEM) return(0);
    min2 = Cudd_CountMinterm(dd, E, nvars) / 2.0;
    if (min2 == (double)CUDD_OUT_OF_MEM) return(0);

    t = (int)((double)nminterms * min1 / (min1 + min2) + 0.5);
    for (i = 0; i < t; i++)
    string[i][N->index] = '1';
    for (i = t; i < nminterms; i++)
    string[i][N->index] = '0';

    result = ddPickArbitraryMinterms(dd,T,nvars,t,&string[0]);
    if (result == 0)
    return(0);
    result = ddPickArbitraryMinterms(dd,E,nvars,nminterms-t,&string[t]);
    return(result);

} /* end of ddPickArbitraryMinterms */


static int
ddPickRepresentativeCube(
  DdManager *dd,
  DdNode *node,
  double *weight,
  char *string)
{
    DdNode *N, *T, *E;
    DdNode *one, *bzero;

    if (string == NULL || node == NULL) return(0);

    /* The constant 0 function has no on-set cubes. */
    one = DD_ONE(dd);
    bzero = Cudd_Not(one);
    if (node == bzero) return(0);

    if (node == DD_ONE(dd)) return(1);

    for (;;) {
    N = Cudd_Regular(node);
    if (N == one)
        break;
    T = cuddT(N);
    E = cuddE(N);
    if (Cudd_IsComplement(node)) {
        T = Cudd_Not(T);
        E = Cudd_Not(E);
    }
    if (weight[N->index] >= 0.0) {
        if (T == bzero) {
        node = E;
        string[N->index] = '0';
        } else {
        node = T;
        string[N->index] = '1';
        }
    } else {
        if (E == bzero) {
        node = T;
        string[N->index] = '1';
        } else {
        node = E;
        string[N->index] = '0';
        }
    }
    }
    return(1);

} /* end of ddPickRepresentativeCube */


static enum st_retval
ddEpdFree(
  char * key,
  char * value,
  char * arg)
{
    EpDouble    *epd;

    epd = (EpDouble *) value;
    EpdFree(epd);
    return(ST_CONTINUE);

} /* end of ddEpdFree */


static void
ddFindSupport(
  DdManager *dd,
  DdNode *f,
  int *SP)
{
    int index;
    DdNode *var;

    if (cuddIsConstant(f) || Cudd_IsComplement(f->next)) {
    return;
    }

    index = f->index;
    var = dd->vars[index];
    /* It is possible that var is embedded in f.  That causes no problem,
    ** though, because if we see it after encountering another node with
    ** the same index, nothing is supposed to happen.
    */
    if (!Cudd_IsComplement(var->next)) {
        var->next = Cudd_Complement(var->next);
        dd->stack[*SP] = (DdNode *)(ptrint) index;
        (*SP)++;
    }
    ddFindSupport(dd, cuddT(f), SP);
    ddFindSupport(dd, Cudd_Regular(cuddE(f)), SP);
    /* Mark as visited. */
    f->next = Cudd_Complement(f->next);

} /* end of ddFindSupport */


static void
ddClearVars(
  DdManager *dd,
  int SP)
{
    int i;

    for (i = 0; i < SP; i++) {
        int index = (int) (ptrint) dd->stack[i];
        DdNode *var = dd->vars[index];
        var->next = Cudd_Regular(var->next);
    }
    
} /* end of ddClearVars */


static int
indexCompare(
  const void *a,
  const void *b)
{
    int ia = *((int *) a);
    int ib = *((int *) b);
    return(ia - ib);

} /* end of indexCompare */