src/cuBdd/cuddUtil.c File Reference

#include "util.h"
#include "cuddInt.h"

Include dependency graph for cuddUtil.c:

Go to the source code of this file.

Defines
#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)
#define	bang(f)   ((Cudd_IsComplement(f)) ? '!' : ' ')
Functions
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)
int	Cudd_PrintMinterm (DdManager *manager, DdNode *node)
int	Cudd_bddPrintCover (DdManager *dd, DdNode *l, DdNode *u)
int	Cudd_PrintDebug (DdManager *dd, DdNode *f, int n, int pr)
int	Cudd_DagSize (DdNode *node)
int	Cudd_EstimateCofactor (DdManager *dd, DdNode *f, int i, int phase)
int	Cudd_EstimateCofactorSimple (DdNode *node, int i)
int	Cudd_SharingSize (DdNode **nodeArray, int n)
double	Cudd_CountMinterm (DdManager *manager, DdNode *node, int nvars)
double	Cudd_CountPath (DdNode *node)
int	Cudd_EpdCountMinterm (DdManager *manager, DdNode *node, int nvars, EpDouble *epd)
double	Cudd_CountPathsToNonZero (DdNode *node)
DdNode *	Cudd_Support (DdManager *dd, DdNode *f)
int *	Cudd_SupportIndex (DdManager *dd, DdNode *f)
int	Cudd_SupportSize (DdManager *dd, DdNode *f)
DdNode *	Cudd_VectorSupport (DdManager *dd, DdNode **F, int n)
int *	Cudd_VectorSupportIndex (DdManager *dd, DdNode **F, int n)
int	Cudd_VectorSupportSize (DdManager *dd, DdNode **F, int n)
int	Cudd_ClassifySupport (DdManager *dd, DdNode *f, DdNode *g, DdNode **common, DdNode **onlyF, DdNode **onlyG)
int	Cudd_CountLeaves (DdNode *node)
int	Cudd_bddPickOneCube (DdManager *ddm, DdNode *node, char *string)
DdNode *	Cudd_bddPickOneMinterm (DdManager *dd, DdNode *f, DdNode **vars, int n)
DdNode **	Cudd_bddPickArbitraryMinterms (DdManager *dd, DdNode *f, DdNode **vars, int n, int k)
DdNode *	Cudd_SubsetWithMaskVars (DdManager *dd, DdNode *f, DdNode **vars, int nvars, DdNode **maskVars, int mvars)
DdGen *	Cudd_FirstCube (DdManager *dd, DdNode *f, int **cube, CUDD_VALUE_TYPE *value)
int	Cudd_NextCube (DdGen *gen, int **cube, CUDD_VALUE_TYPE *value)
DdGen *	Cudd_FirstPrime (DdManager *dd, DdNode *l, DdNode *u, int **cube)
int	Cudd_NextPrime (DdGen *gen, int **cube)
DdNode *	Cudd_bddComputeCube (DdManager *dd, DdNode **vars, int *phase, int n)
DdNode *	Cudd_addComputeCube (DdManager *dd, DdNode **vars, int *phase, int n)
DdNode *	Cudd_CubeArrayToBdd (DdManager *dd, int *array)
int	Cudd_BddToCubeArray (DdManager *dd, DdNode *cube, int *array)
DdGen *	Cudd_FirstNode (DdManager *dd, DdNode *f, DdNode **node)
int	Cudd_NextNode (DdGen *gen, DdNode **node)
int	Cudd_GenFree (DdGen *gen)
int	Cudd_IsGenEmpty (DdGen *gen)
DdNode *	Cudd_IndicesToCube (DdManager *dd, int *array, int n)
void	Cudd_PrintVersion (FILE *fp)
double	Cudd_AverageDistance (DdManager *dd)
long	Cudd_Random (void)
void	Cudd_Srandom (long seed)
double	Cudd_Density (DdManager *dd, DdNode *f, int nvars)
void	Cudd_OutOfMem (long size)
int	cuddP (DdManager *dd, DdNode *f)
enum st_retval	cuddStCountfree (char *key, char *value, char *arg)
int	cuddCollectNodes (DdNode *f, st_table *visited)
DdNodePtr *	cuddNodeArray (DdNode *f, int *n)
Variables
static char rcsid[]	DD_UNUSED = "$Id: cuddUtil.c,v 1.81 2009/03/08 02:49:02 fabio Exp $"
static DdNode *	background
static DdNode *	zero
static long	cuddRand = 0
static long	cuddRand2
static long	shuffleSelect
static long	shuffleTable [STAB_SIZE]

---

Define Documentation

#define bang

(

f

)

((Cudd_IsComplement(f)) ? '!' : ' ')

Definition at line 155 of file cuddUtil.c.

#define LEQA1   40014

Definition at line 117 of file cuddUtil.c.

#define LEQA2   40692

Definition at line 121 of file cuddUtil.c.

#define LEQQ1   53668

Definition at line 118 of file cuddUtil.c.

#define LEQQ2   52774

Definition at line 122 of file cuddUtil.c.

#define LEQR1   12211

Definition at line 119 of file cuddUtil.c.

#define LEQR2   3791

Definition at line 123 of file cuddUtil.c.

#define MODULUS1   2147483563

CFile***********************************************************************

FileName [cuddUtil.c]

PackageName [cudd]

Synopsis [Utility functions.]

Description [External procedures included in this module:

• Cudd_PrintMinterm()
• Cudd_bddPrintCover()
• Cudd_PrintDebug()
• Cudd_DagSize()
• Cudd_EstimateCofactor()
• Cudd_EstimateCofactorSimple()
• Cudd_SharingSize()
• Cudd_CountMinterm()
• Cudd_EpdCountMinterm()
• Cudd_CountPath()
• Cudd_CountPathsToNonZero()
• Cudd_Support()
• Cudd_SupportIndex()
• Cudd_SupportSize()
• Cudd_VectorSupport()
• Cudd_VectorSupportIndex()
• Cudd_VectorSupportSize()
• Cudd_ClassifySupport()
• Cudd_CountLeaves()
• Cudd_bddPickOneCube()
• Cudd_bddPickOneMinterm()
• Cudd_bddPickArbitraryMinterms()
• Cudd_SubsetWithMaskVars()
• Cudd_FirstCube()
• Cudd_NextCube()
• Cudd_bddComputeCube()
• Cudd_addComputeCube()
• Cudd_FirstNode()
• Cudd_NextNode()
• Cudd_GenFree()
• Cudd_IsGenEmpty()
• Cudd_IndicesToCube()
• Cudd_PrintVersion()
• Cudd_AverageDistance()
• Cudd_Random()
• Cudd_Srandom()
• Cudd_Density()

Internal procedures included in this module:

• cuddP()
• cuddStCountfree()
• cuddCollectNodes()
• cuddNodeArray()

Static procedures included in this module:

• dp2()
• ddPrintMintermAux()
• ddDagInt()
• ddCountMintermAux()
• ddEpdCountMintermAux()
• ddCountPathAux()
• ddSupportStep()
• ddClearFlag()
• ddLeavesInt()
• ddPickArbitraryMinterms()
• ddPickRepresentativeCube()
• ddEpdFree()

]

Author [Fabio Somenzi]

Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado

All rights reserved.

Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:

Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.

Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.

Neither the name of the University of Colorado nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.

THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.]

Definition at line 116 of file cuddUtil.c.

#define MODULUS2   2147483399

Definition at line 120 of file cuddUtil.c.

#define STAB_DIV   (1 + (MODULUS1 - 1) / STAB_SIZE)

Definition at line 125 of file cuddUtil.c.

#define STAB_SIZE   64

Definition at line 124 of file cuddUtil.c.

---

Function Documentation

DdNode* Cudd_addComputeCube	(	DdManager *	dd,
		DdNode **	vars,
		int *	phase,
		int	n
	)

Function********************************************************************

Synopsis [Computes the cube of an array of ADD variables.]

Description [Computes the cube of an array of ADD variables. If non-null, the phase argument indicates which literal of each variable should appear in the cube. If phase\[i\] is nonzero, then the positive literal is used. If phase is NULL, the cube is positive unate. Returns a pointer to the result if successful; NULL otherwise.]

SideEffects [none]

SeeAlso [Cudd_bddComputeCube]

Definition at line 2242 of file cuddUtil.c.

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

double Cudd_AverageDistance

(

DdManager *

dd

)

Function********************************************************************

Synopsis [Computes the average distance between adjacent nodes.]

Description [Computes the average distance between adjacent nodes in the manager. Adjacent nodes are node pairs such that the second node is the then child, else child, or next node in the collision list.]

SideEffects [None]

SeeAlso []

Definition at line 2610 of file cuddUtil.c.

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

DdNode* Cudd_bddComputeCube	(	DdManager *	dd,
		DdNode **	vars,
		int *	phase,
		int	n
	)

Function********************************************************************

Synopsis [Computes the cube of an array of BDD variables.]

Description [Computes the cube of an array of BDD variables. If non-null, the phase argument indicates which literal of each variable should appear in the cube. If phase\[i\] is nonzero, then the positive literal is used. If phase is NULL, the cube is positive unate. Returns a pointer to the result if successful; NULL otherwise.]

SideEffects [None]

SeeAlso [Cudd_addComputeCube Cudd_IndicesToCube Cudd_CubeArrayToBdd]

Definition at line 2192 of file cuddUtil.c.

{
    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_bddPickArbitraryMinterms	(	DdManager *	dd,
		DdNode *	f,
		DdNode **	vars,
		int	n,
		int	k
	)

Function********************************************************************

Synopsis [Picks k on-set minterms evenly distributed from given DD.]

Description [Picks k on-set minterms evenly distributed from given DD. The minterms are in terms of vars. The array vars should contain at least all variables in the support of f; if this condition is not met the minterms built by this procedure may not be contained in f. Builds an array of BDDs for the minterms and returns a pointer to it if successful; NULL otherwise. There are three reasons why the procedure may fail:

• It may run out of memory;
• the function f may be the constant 0;
• the minterms may not be contained in f.

]

SideEffects [None]

SeeAlso [Cudd_bddPickOneMinterm Cudd_bddPickOneCube]

Definition at line 1389 of file cuddUtil.c.

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

int Cudd_bddPickOneCube	(	DdManager *	ddm,
		DdNode *	node,
		char *	string
	)

Function********************************************************************

Synopsis [Picks one on-set cube randomly from the given DD.]

Description [Picks one on-set cube randomly from the given DD. The cube is written into an array of characters. The array must have at least as many entries as there are variables. Returns 1 if successful; 0 otherwise.]

SideEffects [None]

SeeAlso [Cudd_bddPickOneMinterm]

Definition at line 1217 of file cuddUtil.c.

{
    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,
		DdNode *	f,
		DdNode **	vars,
		int	n
	)

Function********************************************************************

Synopsis [Picks one on-set minterm randomly from the given DD.]

Description [Picks one on-set minterm randomly from the given DD. The minterm is in terms of vars. The array vars should contain at least all variables in the support of f; if this condition is not met the minterm built by this procedure may not be contained in f. Builds a BDD for the minterm and returns a pointer to it if successful; NULL otherwise. There are three reasons why the procedure may fail:

• It may run out of memory;
• the function f may be the constant 0;
• the minterm may not be contained in f.

]

SideEffects [None]

SeeAlso [Cudd_bddPickOneCube]

Definition at line 1287 of file cuddUtil.c.

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

int Cudd_bddPrintCover	(	DdManager *	dd,
		DdNode *	l,
		DdNode *	u
	)

Function********************************************************************

Synopsis [Prints a sum of prime implicants of a BDD.]

Description [Prints a sum of product cover for an incompletely specified function given by a lower bound and an upper bound. Each product is a prime implicant obtained by expanding the product corresponding to a path from node to the constant one. Uses the package default output file. Returns 1 if successful; 0 otherwise.]

SideEffects [None]

SeeAlso [Cudd_PrintMinterm]

Definition at line 249 of file cuddUtil.c.

{
    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_BddToCubeArray	(	DdManager *	dd,
		DdNode *	cube,
		int *	array
	)

Function********************************************************************

Synopsis [Builds a positional array from the BDD of a cube.]

Description [Builds a positional array from the BDD of a cube. Array must have one entry for each BDD variable. The positional array has 1 in i-th position if the variable of index i appears in true form in the cube; it has 0 in i-th position if the variable of index i appears in complemented form in the cube; finally, it has 2 in i-th position if the variable of index i does not appear in the cube. Returns 1 if successful (the BDD is indeed a cube); 0 otherwise.]

SideEffects [The result is in the array passed by reference.]

SeeAlso [Cudd_CubeArrayToBdd]

Definition at line 2342 of file cuddUtil.c.

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

int Cudd_ClassifySupport	(	DdManager *	dd,
		DdNode *	f,
		DdNode *	g,
		DdNode **	common,
		DdNode **	onlyF,
		DdNode **	onlyG
	)

Function********************************************************************

Synopsis [Classifies the variables in the support of two DDs.]

Description [Classifies the variables in the support of two DDs f and g, depending on whther they appear in both DDs, only in f, or only in g. Returns 1 if successful; 0 otherwise.]

SideEffects [The cubes of the three classes of variables are returned as side effects.]

SeeAlso [Cudd_Support Cudd_VectorSupport]

Definition at line 1081 of file cuddUtil.c.

{
    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

)

Function********************************************************************

Synopsis [Counts the number of leaves in a DD.]

Description [Counts the number of leaves in a DD. Returns the number of leaves in the DD rooted at node if successful; CUDD_OUT_OF_MEM otherwise.]

SideEffects [None]

SeeAlso [Cudd_PrintDebug]

Definition at line 1190 of file cuddUtil.c.

{
    int i;

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

} /* end of Cudd_CountLeaves */

double Cudd_CountMinterm	(	DdManager *	manager,
		DdNode *	node,
		int	nvars
	)

Function********************************************************************

Synopsis [Counts the number of minterms of a DD.]

Description [Counts the number of minterms of a DD. The function is assumed to depend on nvars variables. The minterm count is represented as a double, to allow for a larger number of variables. Returns the number of minterms of the function rooted at node if successful; (double) CUDD_OUT_OF_MEM otherwise.]

SideEffects [None]

SeeAlso [Cudd_PrintDebug Cudd_CountPath]

Definition at line 574 of file cuddUtil.c.

{
    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

)

Function********************************************************************

Synopsis [Counts the number of paths of a DD.]

Description [Counts the number of paths of a DD. Paths to all terminal nodes are counted. The path count is represented as a double, to allow for a larger number of variables. Returns the number of paths of the function rooted at node if successful; (double) CUDD_OUT_OF_MEM otherwise.]

SideEffects [None]

SeeAlso [Cudd_CountMinterm]

Definition at line 619 of file cuddUtil.c.

{

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

double Cudd_CountPathsToNonZero

(

DdNode *

node

)

Function********************************************************************

Synopsis [Counts the number of paths to a non-zero terminal of a DD.]

Description [Counts the number of paths to a non-zero terminal of a DD. The path count is represented as a double, to allow for a larger number of variables. Returns the number of paths of the function rooted at node.]

SideEffects [None]

SeeAlso [Cudd_CountMinterm Cudd_CountPath]

Definition at line 703 of file cuddUtil.c.

{

    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_CubeArrayToBdd	(	DdManager *	dd,
		int *	array
	)

Function********************************************************************

Synopsis [Builds the BDD of a cube from a positional array.]

Description [Builds a cube from a positional array. The array must have one integer entry for each BDD variable. If the i-th entry is 1, the variable of index i appears in true form in the cube; If the i-th entry is 0, the variable of index i appears complemented in the cube; otherwise the variable does not appear in the cube. Returns a pointer to the BDD for the cube if successful; NULL otherwise.]

SideEffects [None]

SeeAlso [Cudd_bddComputeCube Cudd_IndicesToCube Cudd_BddToCubeArray]

Definition at line 2294 of file cuddUtil.c.

{
    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_DagSize

(

DdNode *

node

)

Function********************************************************************

Synopsis [Counts the number of nodes in a DD.]

Description [Counts the number of nodes in a DD. Returns the number of nodes in the graph rooted at node.]

SideEffects [None]

SeeAlso [Cudd_SharingSize Cudd_PrintDebug]

Definition at line 438 of file cuddUtil.c.

{
    int i;

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

    return(i);

} /* end of Cudd_DagSize */

double Cudd_Density	(	DdManager *	dd,
		DdNode *	f,
		int	nvars
	)

Function********************************************************************

Synopsis [Computes the density of a BDD or ADD.]

Description [Computes the density of a BDD or ADD. The density is the ratio of the number of minterms to the number of nodes. If 0 is passed as number of variables, the number of variables existing in the manager is used. Returns the density if successful; (double) CUDD_OUT_OF_MEM otherwise.]

SideEffects [None]

SeeAlso [Cudd_CountMinterm Cudd_DagSize]

Definition at line 2798 of file cuddUtil.c.

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

int Cudd_EpdCountMinterm	(	DdManager *	manager,
		DdNode *	node,
		int	nvars,
		EpDouble *	epd
	)

Function********************************************************************

Synopsis [Counts the number of minterms of a DD with extended precision.]

Description [Counts the number of minterms of a DD with extended precision. The function is assumed to depend on nvars variables. The minterm count is represented as an EpDouble, to allow any number of variables. Returns 0 if successful; CUDD_OUT_OF_MEM otherwise.]

SideEffects [None]

SeeAlso [Cudd_PrintDebug Cudd_CountPath]

Definition at line 653 of file cuddUtil.c.

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

int Cudd_EstimateCofactor	(	DdManager *	dd,
		DdNode *	f,
		int	i,
		int	phase
	)

Function********************************************************************

Synopsis [Estimates the number of nodes in a cofactor of a DD.]

Description [Estimates the number of nodes in a cofactor of a DD. Returns an estimate of the number of nodes in a cofactor of the graph rooted at node with respect to the variable whose index is i. In case of failure, returns CUDD_OUT_OF_MEM. This function uses a refinement of the algorithm of Cabodi et al. (ICCAD96). The refinement allows the procedure to account for part of the recombination that may occur in the part of the cofactor above the cofactoring variable. This procedure does no create any new node. It does keep a small table of results; therefore it may run out of memory. If this is a concern, one should use Cudd_EstimateCofactorSimple, which is faster, does not allocate any memory, but is less accurate.]

SideEffects [None]

SeeAlso [Cudd_DagSize Cudd_EstimateCofactorSimple]

Definition at line 473 of file cuddUtil.c.

                    : 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
	)

Function********************************************************************

Synopsis [Estimates the number of nodes in a cofactor of a DD.]

Description [Estimates the number of nodes in a cofactor of a DD. Returns an estimate of the number of nodes in the positive cofactor of the graph rooted at node with respect to the variable whose index is i. This procedure implements with minor changes the algorithm of Cabodi et al. (ICCAD96). It does not allocate any memory, it does not change the state of the manager, and it is fast. However, it has been observed to overestimate the size of the cofactor by as much as a factor of 2.]

SideEffects [None]

SeeAlso [Cudd_DagSize]

Definition at line 513 of file cuddUtil.c.

{
    int val;

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

    return(val);

} /* end of Cudd_EstimateCofactorSimple */

DdGen* Cudd_FirstCube	(	DdManager *	dd,
		DdNode *	f,
		int **	cube,
		CUDD_VALUE_TYPE *	value
	)

Function********************************************************************

Synopsis [Finds the first cube of a decision diagram.]

Description [Defines an iterator on the onset of a decision diagram and finds its first cube. Returns a generator that contains the information necessary to continue the enumeration if successful; NULL otherwise.

A cube is represented as an array of literals, which are integers in {0, 1, 2}; 0 represents a complemented literal, 1 represents an uncomplemented literal, and 2 stands for don't care. The enumeration produces a disjoint cover of the function associated with the diagram. The size of the array equals the number of variables in the manager at the time Cudd_FirstCube is called.

For each cube, a value is also returned. This value is always 1 for a BDD, while it may be different from 1 for an ADD. For BDDs, the offset is the set of cubes whose value is the logical zero. For ADDs, the offset is the set of cubes whose value is the background value. The cubes of the offset are not enumerated.]

SideEffects [The first cube and its value are returned as side effects.]

SeeAlso [Cudd_ForeachCube Cudd_NextCube Cudd_GenFree Cudd_IsGenEmpty Cudd_FirstNode]

Definition at line 1794 of file cuddUtil.c.

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

DdGen* Cudd_FirstNode	(	DdManager *	dd,
		DdNode *	f,
		DdNode **	node
	)

Function********************************************************************

Synopsis [Finds the first node of a decision diagram.]

Description [Defines an iterator on the nodes of a decision diagram and finds its first node. Returns a generator that contains the information necessary to continue the enumeration if successful; NULL otherwise. The nodes are enumerated in a reverse topological order, so that a node is always preceded in the enumeration by its descendants.]

SideEffects [The first node is returned as a side effect.]

SeeAlso [Cudd_ForeachNode Cudd_NextNode Cudd_GenFree Cudd_IsGenEmpty Cudd_FirstCube]

Definition at line 2396 of file cuddUtil.c.

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

DdGen* Cudd_FirstPrime	(	DdManager *	dd,
		DdNode *	l,
		DdNode *	u,
		int **	cube
	)

Function********************************************************************

Synopsis [Finds the first prime of a Boolean function.]

Description [Defines an iterator on a pair of BDDs describing a (possibly incompletely specified) Boolean functions and finds the first cube of a cover of the function. Returns a generator that contains the information necessary to continue the enumeration if successful; NULL otherwise.

The two argument BDDs are the lower and upper bounds of an interval. It is a mistake to call this function with a lower bound that is not less than or equal to the upper bound.

A cube is represented as an array of literals, which are integers in {0, 1, 2}; 0 represents a complemented literal, 1 represents an uncomplemented literal, and 2 stands for don't care. The enumeration produces a prime and irredundant cover of the function associated with the two BDDs. The size of the array equals the number of variables in the manager at the time Cudd_FirstCube is called.

This iterator can only be used on BDDs.]

SideEffects [The first cube is returned as side effect.]

SeeAlso [Cudd_ForeachPrime Cudd_NextPrime Cudd_GenFree Cudd_IsGenEmpty Cudd_FirstCube Cudd_FirstNode]

Definition at line 2024 of file cuddUtil.c.

{
    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_GenFree

(

DdGen *

gen

)

Function********************************************************************

Synopsis [Frees a CUDD generator.]

Description [Frees a CUDD generator. Always returns 0, so that it can be used in mis-like foreach constructs.]

SideEffects [None]

SeeAlso [Cudd_ForeachCube Cudd_ForeachNode Cudd_FirstCube Cudd_NextCube Cudd_FirstNode Cudd_NextNode Cudd_IsGenEmpty]

Definition at line 2487 of file cuddUtil.c.

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

DdNode* Cudd_IndicesToCube	(	DdManager *	dd,
		int *	array,
		int	n
	)

Function********************************************************************

Synopsis [Builds a cube of BDD variables from an array of indices.]

Description [Builds a cube of BDD variables from an array of indices. Returns a pointer to the result if successful; NULL otherwise.]

SideEffects [None]

SeeAlso [Cudd_bddComputeCube Cudd_CubeArrayToBdd]

Definition at line 2549 of file cuddUtil.c.

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

int Cudd_IsGenEmpty

(

DdGen *

gen

)

Function********************************************************************

Synopsis [Queries the status of a generator.]

Description [Queries the status of a generator. Returns 1 if the generator is empty or NULL; 0 otherswise.]

SideEffects [None]

SeeAlso [Cudd_ForeachCube Cudd_ForeachNode Cudd_FirstCube Cudd_NextCube Cudd_FirstNode Cudd_NextNode Cudd_GenFree]

Definition at line 2527 of file cuddUtil.c.

{
    if (gen == NULL) return(1);
    return(gen->status == CUDD_GEN_EMPTY);

} /* end of Cudd_IsGenEmpty */

int Cudd_NextCube	(	DdGen *	gen,
		int **	cube,
		CUDD_VALUE_TYPE *	value
	)

Function********************************************************************

Synopsis [Generates the next cube of a decision diagram onset.]

Description [Generates the next cube of a decision diagram onset, using generator gen. Returns 0 if the enumeration is completed; 1 otherwise.]

SideEffects [The cube and its value are returned as side effects. The generator is modified.]

SeeAlso [Cudd_ForeachCube Cudd_FirstCube Cudd_GenFree Cudd_IsGenEmpty Cudd_NextNode]

Definition at line 1913 of file cuddUtil.c.

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

int Cudd_NextNode	(	DdGen *	gen,
		DdNode **	node
	)

Function********************************************************************

Synopsis [Finds the next node of a decision diagram.]

Description [Finds the node of a decision diagram, using generator gen. Returns 0 if the enumeration is completed; 1 otherwise.]

SideEffects [The next node is returned as a side effect.]

SeeAlso [Cudd_ForeachNode Cudd_FirstNode Cudd_GenFree Cudd_IsGenEmpty Cudd_NextCube]

Definition at line 2455 of file cuddUtil.c.

{
    /* 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_NextPrime	(	DdGen *	gen,
		int **	cube
	)

Function********************************************************************

Synopsis [Generates the next prime of a Boolean function.]

Description [Generates the next cube of a Boolean function, using generator gen. Returns 0 if the enumeration is completed; 1 otherwise.]

SideEffects [The cube and is returned as side effects. The generator is modified.]

SeeAlso [Cudd_ForeachPrime Cudd_FirstPrime Cudd_GenFree Cudd_IsGenEmpty Cudd_NextCube Cudd_NextNode]

Definition at line 2126 of file cuddUtil.c.

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

void Cudd_OutOfMem

(

long

size

)

Function********************************************************************

Synopsis [Warns that a memory allocation failed.]

Description [Warns that a memory allocation failed. This function can be used as replacement of MMout_of_memory to prevent the safe_mem functions of the util package from exiting when malloc returns NULL. One possible use is in case of discretionary allocations; for instance, the allocation of memory to enlarge the computed table.]

SideEffects [None]

SeeAlso []

Definition at line 2833 of file cuddUtil.c.

{
    (void) fflush(stdout);
    (void) fprintf(stderr, "\nunable to allocate %ld bytes\n", size);
    return;

} /* end of Cudd_OutOfMem */

int Cudd_PrintDebug	(	DdManager *	dd,
		DdNode *	f,
		int	n,
		int	pr
	)

Function********************************************************************

Synopsis [Prints to the standard output a DD and its statistics.]

Description [Prints to the standard output a DD and its statistics. The statistics include the number of nodes, the number of leaves, and the number of minterms. (The number of minterms is the number of assignments to the variables that cause the function to be different from the logical zero (for BDDs) and from the background value (for ADDs.) The statistics are printed if pr > 0. Specifically:

• pr = 0 : prints nothing
• pr = 1 : prints counts of nodes and minterms
• pr = 2 : prints counts + disjoint sum of product
• pr = 3 : prints counts + list of nodes
• pr > 3 : prints counts + disjoint sum of product + list of nodes

For the purpose of counting the number of minterms, the function is supposed to depend on n variables. Returns 1 if successful; 0 otherwise.]

SideEffects [None]

SeeAlso [Cudd_DagSize Cudd_CountLeaves Cudd_CountMinterm Cudd_PrintMinterm]

Definition at line 378 of file cuddUtil.c.

{
    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_PrintMinterm	(	DdManager *	manager,
		DdNode *	node
	)

AutomaticEnd Function********************************************************************

Synopsis [Prints a disjoint sum of products.]

Description [Prints a disjoint sum of product cover for the function rooted at node. Each product corresponds to a path from node to a leaf node different from the logical zero, and different from the background value. Uses the package default output file. Returns 1 if successful; 0 otherwise.]

SideEffects [None]

SeeAlso [Cudd_PrintDebug Cudd_bddPrintCover]

Definition at line 212 of file cuddUtil.c.

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

void Cudd_PrintVersion

(

FILE *

fp

)

Function********************************************************************

Synopsis [Prints the package version number.]

Description []

SideEffects [None]

SeeAlso []

Definition at line 2588 of file cuddUtil.c.

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

} /* end of Cudd_PrintVersion */

long Cudd_Random

(

void

)

Function********************************************************************

Synopsis [Portable random number generator.]

Description [Portable number generator based on ran2 from "Numerical Recipes in C." It is a long period (> 2 * 10^18) random number generator of L'Ecuyer with Bays-Durham shuffle. Returns a long integer uniformly distributed between 0 and 2147483561 (inclusive of the endpoint values). The random generator can be explicitly initialized by calling Cudd_Srandom. If no explicit initialization is performed, then the seed 1 is assumed.]

SideEffects [None]

SeeAlso [Cudd_Srandom]

Definition at line 2698 of file cuddUtil.c.

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

int Cudd_SharingSize	(	DdNode **	nodeArray,
		int	n
	)

Function********************************************************************

Synopsis [Counts the number of nodes in an array of DDs.]

Description [Counts the number of nodes in an array of DDs. Shared nodes are counted only once. Returns the total number of nodes.]

SideEffects [None]

SeeAlso [Cudd_DagSize]

Definition at line 540 of file cuddUtil.c.

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

void Cudd_Srandom

(

long

seed

)

Function********************************************************************

Synopsis [Initializer for the portable random number generator.]

Description [Initializer for the portable number generator based on ran2 in "Numerical Recipes in C." The input is the seed for the generator. If it is negative, its absolute value is taken as seed. If it is 0, then 1 is taken as seed. The initialized sets up the two recurrences used to generate a long-period stream, and sets up the shuffle table.]

SideEffects [None]

SeeAlso [Cudd_Random]

Definition at line 2760 of file cuddUtil.c.

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

DdNode* Cudd_SubsetWithMaskVars	(	DdManager *	dd,
		DdNode *	f,
		DdNode **	vars,
		int	nvars,
		DdNode **	maskVars,
		int	mvars
	)

Function********************************************************************

Synopsis [Extracts a subset from a BDD.]

Description [Extracts a subset from a BDD in the following procedure. 1. Compute the weight for each mask variable by counting the number of minterms for both positive and negative cofactors of the BDD with respect to each mask variable. (weight = positive - negative) 2. Find a representative cube of the BDD by using the weight. From the top variable of the BDD, for each variable, if the weight is greater than 0.0, choose THEN branch, othereise ELSE branch, until meeting the constant 1. 3. Quantify out the variables not in maskVars from the representative cube and if a variable in maskVars is don't care, replace the variable with a constant(1 or 0) depending on the weight. 4. Make a subset of the BDD by multiplying with the modified cube.]

SideEffects [None]

SeeAlso []

Definition at line 1598 of file cuddUtil.c.

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

DdNode* Cudd_Support	(	DdManager *	dd,
		DdNode *	f
	)

Function********************************************************************

Synopsis [Finds the variables on which a DD depends.]

Description [Finds the variables on which a DD depends. Returns a BDD consisting of the product of the variables if successful; NULL otherwise.]

SideEffects [None]

SeeAlso [Cudd_VectorSupport Cudd_ClassifySupport]

Definition at line 736 of file cuddUtil.c.

{
    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,
		DdNode *	f
	)

Function********************************************************************

Synopsis [Finds the variables on which a DD depends.]

Description [Finds the variables on which a DD depends. Returns an index array of the variables if successful; NULL otherwise. The size of the array equals the number of variables in the manager. Each entry of the array is 1 if the corresponding variable is in the support of the DD and 0 otherwise.]

SideEffects [None]

SeeAlso [Cudd_Support Cudd_VectorSupport Cudd_ClassifySupport]

Definition at line 811 of file cuddUtil.c.

{
    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,
		DdNode *	f
	)

Function********************************************************************

Synopsis [Counts the variables on which a DD depends.]

Description [Counts the variables on which a DD depends. Returns the number of the variables if successful; CUDD_OUT_OF_MEM otherwise.]

SideEffects [None]

SeeAlso [Cudd_Support]

Definition at line 853 of file cuddUtil.c.

{
    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,
		DdNode **	F,
		int	n
	)

Function********************************************************************

Synopsis [Finds the variables on which a set of DDs depends.]

Description [Finds the variables on which a set of DDs depends. The set must contain either BDDs and ADDs, or ZDDs. Returns a BDD consisting of the product of the variables if successful; NULL otherwise.]

SideEffects [None]

SeeAlso [Cudd_Support Cudd_ClassifySupport]

Definition at line 904 of file cuddUtil.c.

{
    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,
		DdNode **	F,
		int	n
	)

Function********************************************************************

Synopsis [Finds the variables on which a set of DDs depends.]

Description [Finds the variables on which a set of DDs depends. The set must contain either BDDs and ADDs, or ZDDs. Returns an index array of the variables if successful; NULL otherwise.]

SideEffects [None]

SeeAlso [Cudd_SupportIndex Cudd_VectorSupport Cudd_ClassifySupport]

Definition at line 976 of file cuddUtil.c.

{
    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,
		DdNode **	F,
		int	n
	)

Function********************************************************************

Synopsis [Counts the variables on which a set of DDs depends.]

Description [Counts the variables on which a set of DDs depends. The set must contain either BDDs and ADDs, or ZDDs. Returns the number of the variables if successful; CUDD_OUT_OF_MEM otherwise.]

SideEffects [None]

SeeAlso [Cudd_VectorSupport Cudd_SupportSize]

Definition at line 1024 of file cuddUtil.c.

{
    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 cuddCollectNodes	(	DdNode *	f,
		st_table *	visited
	)

Function********************************************************************

Synopsis [Recursively collects all the nodes of a DD in a symbol table.]

Description [Traverses the DD f and collects all its nodes in a symbol table. f is assumed to be a regular pointer and cuddCollectNodes guarantees this assumption in the recursive calls. Returns 1 in case of success; 0 otherwise.]

SideEffects [None]

SeeAlso []

Definition at line 2921 of file cuddUtil.c.

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

static int cuddEstimateCofactor	(	DdManager *	dd,
		st_table *	table,
		DdNode *	node,
		int	i,
		int	phase,
		DdNode **	ptr
	)			[static]

Function********************************************************************

Synopsis [Performs the recursive step of Cudd_CofactorEstimate.]

Description [Performs the recursive step of Cudd_CofactorEstimate. Returns an estimate of the number of nodes in the DD of a cofactor of node. Uses the least significant bit of the next field as visited flag. node is supposed to be regular; the invariant is maintained by this procedure.]

SideEffects [None]

SeeAlso []

Definition at line 3236 of file cuddUtil.c.

{
    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 int cuddEstimateCofactorSimple	(	DdNode *	node,
		int	i
	)			[static]

Function********************************************************************

Synopsis [Performs the recursive step of Cudd_CofactorEstimateSimple.]

Description [Performs the recursive step of Cudd_CofactorEstimateSimple. Returns an estimate of the number of nodes in the DD of the positive cofactor of node. Uses the least significant bit of the next field as visited flag. node is supposed to be regular; the invariant is maintained by this procedure.]

SideEffects [None]

SeeAlso []

Definition at line 3395 of file cuddUtil.c.

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

DdNodePtr* cuddNodeArray	(	DdNode *	f,
		int *	n
	)

Function********************************************************************

Synopsis [Recursively collects all the nodes of a DD in an array.]

Description [Traverses the DD f and collects all its nodes in an array. The caller should free the array returned by cuddNodeArray. Returns a pointer to the array of nodes in case of success; NULL otherwise. The nodes are collected in reverse topological order, so that a node is always preceded in the array by all its descendants.]

SideEffects [The number of nodes is returned as a side effect.]

SeeAlso [Cudd_FirstNode]

Definition at line 2975 of file cuddUtil.c.

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

static int cuddNodeArrayRecur	(	DdNode *	f,
		DdNodePtr *	table,
		int	index
	)			[static]

Function********************************************************************

Synopsis [Performs the recursive step of cuddNodeArray.]

Description [Performs the recursive step of cuddNodeArray. Returns an the number of nodes in the DD. Clear the least significant bit of the next field that was used as visited flag by cuddNodeArrayRecur when counting the nodes. node is supposed to be regular; the invariant is maintained by this procedure.]

SideEffects [None]

SeeAlso []

Definition at line 3196 of file cuddUtil.c.

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

int cuddP	(	DdManager *	dd,
		DdNode *	f
	)

Function********************************************************************

Synopsis [Prints a DD to the standard output. One line per node is printed.]

Description [Prints a DD to the standard output. One line per node is printed. Returns 1 if successful; 0 otherwise.]

SideEffects [None]

SeeAlso [Cudd_PrintDebug]

Definition at line 2862 of file cuddUtil.c.

{
    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
	)

Function********************************************************************

Synopsis [Frees the memory used to store the minterm counts recorded in the visited table.]

Description [Frees the memory used to store the minterm counts recorded in the visited table. Returns ST_CONTINUE.]

SideEffects [None]

Definition at line 2891 of file cuddUtil.c.

{
    double      *d;

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

} /* end of cuddStCountfree */

static DdNode * cuddUniqueLookup	(	DdManager *	unique,
		int	index,
		DdNode *	T,
		DdNode *	E
	)			[static]

Function********************************************************************

Synopsis [Checks the unique table for the existence of an internal node.]

Description [Checks the unique table for the existence of an internal node. Returns a pointer to the node if it is in the table; NULL otherwise.]

SideEffects [None]

SeeAlso [cuddUniqueInter]

Definition at line 3336 of file cuddUtil.c.

{
    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 void ddClearFlag

(

DdNode *

f

)

[static]

Function********************************************************************

Synopsis [Performs a DFS from f, clearing the LSB of the next pointers.]

Description []

SideEffects [None]

SeeAlso [ddSupportStep ddDagInt]

Definition at line 3731 of file cuddUtil.c.

{
    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 double ddCountMintermAux	(	DdNode *	node,
		double	max,
		DdHashTable *	table
	)			[static]

Function********************************************************************

Synopsis [Performs the recursive step of Cudd_CountMinterm.]

Description [Performs the recursive step of Cudd_CountMinterm. It is based on the following identity. Let |f| be the number of minterms of f. Then: <xmp> |f| = (|f0|+|f1|)/2 </xmp> where f0 and f1 are the two cofactors of f. Does not use the identity |f'| = max - |f|, to minimize loss of accuracy due to roundoff. Returns the number of minterms of the function rooted at node.]

SideEffects [None]

Definition at line 3435 of file cuddUtil.c.

{
    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
	)			[static]

Function********************************************************************

Synopsis [Performs the recursive step of Cudd_CountPath.]

Description [Performs the recursive step of Cudd_CountPath. It is based on the following identity. Let |f| be the number of paths of f. Then: <xmp> |f| = |f0|+|f1| </xmp> where f0 and f1 are the two cofactors of f. Uses the identity |f'| = |f|, to improve the utilization of the (local) cache. Returns the number of paths of the function rooted at node.]

SideEffects [None]

Definition at line 3508 of file cuddUtil.c.

{

    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 double ddCountPathsToNonZero	(	DdNode *	N,
		st_table *	table
	)			[static]

Function********************************************************************

Synopsis [Performs the recursive step of Cudd_CountPathsToNonZero.]

Description [Performs the recursive step of Cudd_CountPathsToNonZero. It is based on the following identity. Let |f| be the number of paths of f. Then: <xmp> |f| = |f0|+|f1| </xmp> where f0 and f1 are the two cofactors of f. Returns the number of paths of the function rooted at node.]

SideEffects [None]

Definition at line 3641 of file cuddUtil.c.

{

    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 int ddDagInt

(

DdNode *

n

)

[static]

Function********************************************************************

Synopsis [Performs the recursive step of Cudd_DagSize.]

Description [Performs the recursive step of Cudd_DagSize. Returns the number of nodes in the graph rooted at n.]

SideEffects [None]

Definition at line 3161 of file cuddUtil.c.

{
    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 ddEpdCountMintermAux	(	DdNode *	node,
		EpDouble *	max,
		EpDouble *	epd,
		st_table *	table
	)			[static]

Function********************************************************************

Synopsis [Performs the recursive step of Cudd_EpdCountMinterm.]

Description [Performs the recursive step of Cudd_EpdCountMinterm. It is based on the following identity. Let |f| be the number of minterms of f. Then: <xmp> |f| = (|f0|+|f1|)/2 </xmp> where f0 and f1 are the two cofactors of f. Does not use the identity |f'| = max - |f|, to minimize loss of accuracy due to roundoff. Returns the number of minterms of the function rooted at node.]

SideEffects [None]

Definition at line 3569 of file cuddUtil.c.

{
    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 enum st_retval ddEpdFree	(	char *	key,
		char *	value,
		char *	arg
	)			[static]

Function********************************************************************

Synopsis [Frees the memory used to store the minterm counts recorded in the visited table.]

Description [Frees the memory used to store the minterm counts recorded in the visited table. Returns ST_CONTINUE.]

SideEffects [None]

Definition at line 3918 of file cuddUtil.c.

{
    EpDouble    *epd;

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

} /* end of ddEpdFree */

static int ddLeavesInt

(

DdNode *

n

)

[static]

Function********************************************************************

Synopsis [Performs the recursive step of Cudd_CountLeaves.]

Description [Performs the recursive step of Cudd_CountLeaves. Returns the number of leaves in the DD rooted at n.]

SideEffects [None]

SeeAlso [Cudd_CountLeaves]

Definition at line 3762 of file cuddUtil.c.

{
    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
	)			[static]

Function********************************************************************

Synopsis [Performs the recursive step of Cudd_bddPickArbitraryMinterms.]

Description [Performs the recursive step of Cudd_bddPickArbitraryMinterms. Returns 1 if successful; 0 otherwise.]

SideEffects [none]

SeeAlso [Cudd_bddPickArbitraryMinterms]

Definition at line 3794 of file cuddUtil.c.

{
    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
	)			[static]

Function********************************************************************

Synopsis [Finds a representative cube of a BDD.]

Description [Finds a representative cube of a BDD with the weight of each variable. From the top variable, if the weight is greater than or equal to 0.0, choose THEN branch unless the child is the constant 0. Otherwise, choose ELSE branch unless the child is the constant 0.]

SideEffects [Cudd_SubsetWithMaskVars Cudd_bddPickOneCube]

Definition at line 3855 of file cuddUtil.c.

{
    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 void ddPrintMintermAux	(	DdManager *	dd,
		DdNode *	node,
		int *	list
	)			[static]

Function********************************************************************

Synopsis [Performs the recursive step of Cudd_PrintMinterm.]

Description []

SideEffects [None]

Definition at line 3107 of file cuddUtil.c.

{
    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 void ddSupportStep	(	DdNode *	f,
		int *	support
	)			[static]

Function********************************************************************

Synopsis [Performs the recursive step of Cudd_Support.]

Description [Performs the recursive step of Cudd_Support. Performs a DFS from f. The support is accumulated in supp as a side effect. Uses the LSB of the then pointer as visited flag.]

SideEffects [None]

SeeAlso [ddClearFlag]

Definition at line 3700 of file cuddUtil.c.

{
    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 int dp2	(	DdManager *	dd,
		DdNode *	f,
		st_table *	t
	)			[static]

AutomaticStart

Function********************************************************************

Synopsis [Performs the recursive step of cuddP.]

Description [Performs the recursive step of cuddP. Returns 1 in case of success; 0 otherwise.]

SideEffects [None]

Definition at line 3014 of file cuddUtil.c.

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

---

Variable Documentation

DdNode* background [static]

Definition at line 144 of file cuddUtil.c.

long cuddRand = 0 [static]

Definition at line 146 of file cuddUtil.c.

long cuddRand2 [static]

Definition at line 147 of file cuddUtil.c.

char rcsid [] DD_UNUSED = "$Id: cuddUtil.c,v 1.81 2009/03/08 02:49:02 fabio Exp $" [static]

Definition at line 141 of file cuddUtil.c.

long shuffleSelect [static]

Definition at line 148 of file cuddUtil.c.

long shuffleTable[STAB_SIZE] [static]

Definition at line 149 of file cuddUtil.c.

DdNode * zero [static]

Definition at line 144 of file cuddUtil.c.