src/cuBdd/cuddUtil.c

Go to the documentation of this file.

#include "util.h"
#include "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.81 2009/03/08 02:49:02 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);

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


DdNode *
Cudd_Support(
  DdManager * dd /* manager */,
  DdNode * f /* DD whose support is sought */)
{
    int *support;
    DdNode *res, *tmp, *var;
    int i,j;
    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));

    /* Transform support from array to cube. */
    do {
        dd->reordered = 0;
        res = DD_ONE(dd);
        cuddRef(res);
        for (j = size - 1; j >= 0; j--) { /* for each level bottom-up */
            i = (j >= dd->size) ? j : dd->invperm[j];
            if (support[i] == 1) {
                /* The following call to cuddUniqueInter is guaranteed
                ** not to trigger reordering because the node we look up
                ** already exists. */
                var = cuddUniqueInter(dd,i,dd->one,Cudd_Not(dd->one));
                cuddRef(var);
                tmp = cuddBddAndRecur(dd,res,var);
                if (tmp == NULL) {
                    Cudd_RecursiveDeref(dd,res);
                    Cudd_RecursiveDeref(dd,var);
                    res = NULL;
                    break;
                }
                cuddRef(tmp);
                Cudd_RecursiveDeref(dd,res);
                Cudd_RecursiveDeref(dd,var);
                res = tmp;
            }
        }
    } while (dd->reordered == 1);

    FREE(support);
    if (res != NULL) 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 *support;
    int i;
    int size;
    int count;

    /* 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(CUDD_OUT_OF_MEM);
    }
    for (i = 0; i < size; i++) {
        support[i] = 0;
    }

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

    /* Count support variables. */
    count = 0;
    for (i = 0; i < size; i++) {
        if (support[i] == 1) count++;
    }

    FREE(support);
    return(count);

} /* end of Cudd_SupportSize */


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, *tmp, *var;
    int i,j;
    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]));
    }

    /* Transform support from array to cube. */
    res = DD_ONE(dd);
    cuddRef(res);
    for (j = size - 1; j >= 0; j--) { /* for each level bottom-up */
        i = (j >= dd->size) ? j : dd->invperm[j];
        if (support[i] == 1) {
            var = cuddUniqueInter(dd,i,dd->one,Cudd_Not(dd->one));
            cuddRef(var);
            tmp = Cudd_bddAnd(dd,res,var);
            if (tmp == NULL) {
                Cudd_RecursiveDeref(dd,res);
                Cudd_RecursiveDeref(dd,var);
                FREE(support);
                return(NULL);
            }
            cuddRef(tmp);
            Cudd_RecursiveDeref(dd,res);
            Cudd_RecursiveDeref(dd,var);
            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 *support;
    int i;
    int size;
    int count;

    /* 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(CUDD_OUT_OF_MEM);
    }
    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]));
    }

    /* Count vriables in support. */
    count = 0;
    for (i = 0; i < size; i++) {
        if (support[i] == 1) count++;
    }

    FREE(support);
    return(count);

} /* 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;
    DdNode *tmp, *var;
    int i,j;
    int size;

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

    /* Compute supports and clean up markers. */
    ddSupportStep(Cudd_Regular(f),supportF);
    ddClearFlag(Cudd_Regular(f));
    ddSupportStep(Cudd_Regular(g),supportG);
    ddClearFlag(Cudd_Regular(g));

    /* Classify variables and create cubes. */
    *common = *onlyF = *onlyG = DD_ONE(dd);
    cuddRef(*common); cuddRef(*onlyF); cuddRef(*onlyG);
    for (j = size - 1; j >= 0; j--) { /* for each level bottom-up */
        i = (j >= dd->size) ? j : dd->invperm[j];
        if (supportF[i] == 0 && supportG[i] == 0) continue;
        var = cuddUniqueInter(dd,i,dd->one,Cudd_Not(dd->one));
        cuddRef(var);
        if (supportG[i] == 0) {
            tmp = Cudd_bddAnd(dd,*onlyF,var);
            if (tmp == NULL) {
                Cudd_RecursiveDeref(dd,*common);
                Cudd_RecursiveDeref(dd,*onlyF);
                Cudd_RecursiveDeref(dd,*onlyG);
                Cudd_RecursiveDeref(dd,var);
                FREE(supportF); FREE(supportG);
                return(0);
            }
            cuddRef(tmp);
            Cudd_RecursiveDeref(dd,*onlyF);
            *onlyF = tmp;
        } else if (supportF[i] == 0) {
            tmp = Cudd_bddAnd(dd,*onlyG,var);
            if (tmp == NULL) {
                Cudd_RecursiveDeref(dd,*common);
                Cudd_RecursiveDeref(dd,*onlyF);
                Cudd_RecursiveDeref(dd,*onlyG);
                Cudd_RecursiveDeref(dd,var);
                FREE(supportF); FREE(supportG);
                return(0);
            }
            cuddRef(tmp);
            Cudd_RecursiveDeref(dd,*onlyG);
            *onlyG = tmp;
        } else {
            tmp = Cudd_bddAnd(dd,*common,var);
            if (tmp == NULL) {
                Cudd_RecursiveDeref(dd,*common);
                Cudd_RecursiveDeref(dd,*onlyF);
                Cudd_RecursiveDeref(dd,*onlyG);
                Cudd_RecursiveDeref(dd,var);
                FREE(supportF); FREE(supportG);
                return(0);
            }
            cuddRef(tmp);
            Cudd_RecursiveDeref(dd,*common);
            *common = tmp;
        }
        Cudd_RecursiveDeref(dd,var);
    }

    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_Not(f->next);
    return;

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

---