自学教程：C++ DD_ZERO函数代码示例

/**Function********************************************************************  Synopsis    [Integer and floating point multiplication.]  Description [Integer and floating point multiplication. Returns NULL  if not a terminal case; f * g otherwise.  This function can be used also  to take the AND of two 0-1 ADDs.]  SideEffects [None]  SeeAlso     [Cudd_addApply]******************************************************************************/DdNode *Cudd_addTimes(  DdManager * dd,  DdNode ** f,  DdNode ** g){    DdNode *res;    DdNode *F, *G;    CUDD_VALUE_TYPE value;    F = *f; G = *g;    if (F == DD_ZERO(dd) || G == DD_ZERO(dd)) return(DD_ZERO(dd));    if (F == DD_ONE(dd)) return(G);    if (G == DD_ONE(dd)) return(F);    if (cuddIsConstant(F) && cuddIsConstant(G)) {	value = cuddV(F)*cuddV(G);	res = cuddUniqueConst(dd,value);	return(res);    }    if (F > G) { /* swap f and g */	*f = G;	*g = F;    }    return(NULL);} /* end of Cudd_addTimes */

/**Function********************************************************************  Synopsis [Performs the recursive step of Cudd_zddChange.]  Description []  SideEffects [None]  SeeAlso     []******************************************************************************/DdNode *cuddZddChangeAux(  DdManager * zdd,  DdNode * P,  DdNode * zvar){    int		top_var, level;    DdNode	*res, *t, *e;    DdNode	*base = DD_ONE(zdd);    DdNode	*empty = DD_ZERO(zdd);    statLine(zdd);    if (P == empty)	return(empty);    if (P == base)	return(zvar);    /* Check cache. */    res = cuddCacheLookup2Zdd(zdd, cuddZddChangeAux, P, zvar);    if (res != NULL)	return(res);    top_var = zdd->permZ[P->index];    level = zdd->permZ[zvar->index];    if (top_var > level) {	res = cuddZddGetNode(zdd, zvar->index, P, DD_ZERO(zdd));	if (res == NULL) return(NULL);    } else if (top_var == level) {	res = cuddZddGetNode(zdd, zvar->index, cuddE(P), cuddT(P));	if (res == NULL) return(NULL);    } else {	t = cuddZddChangeAux(zdd, cuddT(P), zvar);	if (t == NULL) return(NULL);	cuddRef(t);	e = cuddZddChangeAux(zdd, cuddE(P), zvar);	if (e == NULL) {	    Cudd_RecursiveDerefZdd(zdd, t);	    return(NULL);	}	cuddRef(e);	res = cuddZddGetNode(zdd, P->index, t, e);	if (res == NULL) {	    Cudd_RecursiveDerefZdd(zdd, t);	    Cudd_RecursiveDerefZdd(zdd, e);	    return(NULL);	}	cuddDeref(t);	cuddDeref(e);    }    cuddCacheInsert2(zdd, cuddZddChangeAux, P, zvar, res);    return(res);} /* end of cuddZddChangeAux */

/**Function********************************************************************  Synopsis    [Comparison of a pair of functions to the i-th ADD variable.]  Description [Comparison of a pair of functions to the i-th ADD  variable. Returns 1 if the functions are the i-th ADD variable and its  complement; 0 otherwise.]  SideEffects [None]  SeeAlso     []******************************************************************************/DD_INLINEstatic intddIsIthAddVarPair(  DdManager * dd,  DdNode * f,  DdNode * g,  unsigned int  i){    return(f->index == i && g->index == i && 	   cuddT(f) == DD_ONE(dd) && cuddE(f) == DD_ZERO(dd) &&	   cuddT(g) == DD_ZERO(dd) && cuddE(g) == DD_ONE(dd));} /* end of ddIsIthAddVarPair */

/**Function********************************************************************  Synopsis    [This operator sets f to the value of g wherever g != 0.]  Description [This operator sets f to the value of g wherever g != 0.  Returns NULL if not a terminal case; f op g otherwise.]  SideEffects [None]  SeeAlso     [Cudd_addApply]******************************************************************************/DdNode *Cudd_addSetNZ(  DdManager * dd,  DdNode ** f,  DdNode ** g){    DdNode *F, *G;    F = *f; G = *g;    if (F == DD_ZERO(dd)) return(G);    if (G == DD_ZERO(dd)) return(F);    if (cuddIsConstant(G)) return(G);    return(NULL);} /* end of Cudd_addSetNZ */

/**Function********************************************************************  Synopsis [Computes the negative cofactor of a ZDD w.r.t. a variable.]  Description [Computes the negative cofactor of a ZDD w.r.t. a  variable. In terms of combinations, the result is the set of all  combinations in which the variable is negated. Returns a pointer to  the result if successful; NULL otherwise. cuddZddSubset0 performs  the same function as Cudd_zddSubset0, but does not restart if  reordering has taken place. Therefore it can be called from within a  recursive procedure.]  SideEffects [None]  SeeAlso     [cuddZddSubset1 Cudd_zddSubset0]******************************************************************************/DdNode *cuddZddSubset0(  DdManager * dd,  DdNode * P,  int  var){    DdNode	*zvar, *r;    DdNode	*base, *empty;    base = DD_ONE(dd);    empty = DD_ZERO(dd);    zvar = cuddUniqueInterZdd(dd, var, base, empty);    if (zvar == NULL) {	return(NULL);    } else {	cuddRef(zvar);	r = zdd_subset0_aux(dd, P, zvar);	if (r == NULL) {	    Cudd_RecursiveDerefZdd(dd, zvar);	    return(NULL);	}	cuddRef(r);	Cudd_RecursiveDerefZdd(dd, zvar);    }    cuddDeref(r);    return(r);} /* end of cuddZddSubset0 */

/**Function********************************************************************  Synopsis    [Reads in a sparse matrix.]  Description [Reads in a sparse matrix specified in a simple format.  The first line of the input contains the numbers of rows and columns.  The remaining lines contain the elements of the matrix, one per line.  Given a background value  (specified by the background field of the manager), only the values  different from it are explicitly listed.  Each foreground element is  described by two integers, i.e., the row and column number, and a  real number, i.e., the value.<p>  Cudd_addRead produces an ADD that depends on two sets of variables: x  and y.  The x variables (x/[0/] ... x/[nx-1/]) encode the row index and  the y variables (y/[0/] ... y/[ny-1/]) encode the column index.  x/[0/] and y/[0/] are the most significant bits in the indices.  The variables may already exist or may be created by the function.  The index of x/[i/] is bx+i*sx, and the index of y/[i/] is by+i*sy.<p>  On input, nx and ny hold the numbers  of row and column variables already in existence. On output, they  hold the numbers of row and column variables actually used by the  matrix. When Cudd_addRead creates the variable arrays,  the index of x/[i/] is bx+i*sx, and the index of y/[i/] is by+i*sy.  When some variables already exist Cudd_addRead expects the indices  of the existing x variables to be bx+i*sx, and the indices of the  existing y variables to be by+i*sy.<p>  m and n are set to the numbers of rows and columns of the  matrix.  Their values on input are immaterial.  The ADD for the  sparse matrix is returned in E, and its reference count is > 0.  Cudd_addRead returns 1 in case of success; 0 otherwise.]  SideEffects [nx and ny are set to the numbers of row and column  variables. m and n are set to the numbers of rows and columns. x and y  are possibly extended to represent the array of row and column  variables. Similarly for xn and yn_, which hold on return from  Cudd_addRead the complements of the row and column variables.]  SeeAlso     [Cudd_addHarwell Cudd_bddRead]******************************************************************************/intCudd_addRead(  FILE * fp /* input file pointer */,  DdManager * dd /* DD manager */,  DdNode ** E /* characteristic function of the graph */,  DdNode *** x /* array of row variables */,  DdNode *** y /* array of column variables */,  DdNode *** xn /* array of complemented row variables */,  DdNode *** yn_ /* array of complemented column variables */,  int * nx /* number or row variables */,  int * ny /* number or column variables */,  int * m /* number of rows */,  int * n /* number of columns */,  int  bx /* first index of row variables */,  int  sx /* step of row variables */,  int  by /* first index of column variables */,  int  sy /* step of column variables */){    DdNode *one, *zero;    DdNode *w, *neW;    DdNode *minterm1;    int u, v, err, i, nv;    int lnx, lny;    CUDD_VALUE_TYPE val;    DdNode **lx, **ly, **lxn, **lyn;    one = DD_ONE(dd);    zero = DD_ZERO(dd);    err = fscanf(fp, "%d %d", &u, &v);    if (err == EOF) {	return(0);    } else if (err != 2) {	return(0);    }    *m = u;    /* Compute the number of x variables. */    lx = *x; lxn = *xn;    u--; 	/* row and column numbers start from 0 */    for (lnx=0; u > 0; lnx++) {	u >>= 1;    }    /* Here we rely on the fact that REALLOC of a null pointer is    ** translates to an ALLOC.    */    if (lnx > *nx) {	*x = lx = REALLOC(DdNode *, *x, lnx);	if (lx == NULL) {	    dd->errorCode = CUDD_MEMORY_OUT;	    return(0);	}	*xn = lxn =  REALLOC(DdNode *, *xn, lnx);	if (lxn == NULL) {	    dd->errorCode = CUDD_MEMORY_OUT;	    return(0);	}    }

/**Function********************************************************************  Synopsis    [NAND of two 0-1 ADDs.]  Description [NAND of two 0-1 ADDs. Returns NULL  if not a terminal case; f NAND g otherwise.]  SideEffects [None]  SeeAlso     [Cudd_addApply]******************************************************************************/DdNode *Cudd_addNand(  DdManager * dd,  DdNode ** f,  DdNode ** g){    DdNode *F, *G;    F = *f; G = *g;    if (F == DD_ZERO(dd) || G == DD_ZERO(dd)) return(DD_ONE(dd));    if (cuddIsConstant(F) && cuddIsConstant(G)) return(DD_ZERO(dd));    if (F > G) { /* swap f and g */	*f = G;	*g = F;    }    return(NULL);} /* end of Cudd_addNand */

/**Function********************************************************************  Synopsis [Performs the recursive step of Cudd_zddSubset1.]  Description []  SideEffects [None]  SeeAlso     []******************************************************************************/static DdNode *zdd_subset1_aux(  DdManager * zdd,  DdNode * P,  DdNode * zvar){    int		top_var, level;    DdNode	*res, *t, *e;    DdNode	*empty;    statLine(zdd);    empty = DD_ZERO(zdd);    /* Check cache. */    res = cuddCacheLookup2Zdd(zdd, zdd_subset1_aux, P, zvar);    if (res != NULL)	return(res);    if (cuddIsConstant(P)) {	res = empty;	cuddCacheInsert2(zdd, zdd_subset1_aux, P, zvar, res);	return(res);    }    top_var = zdd->permZ[P->index];    level = zdd->permZ[zvar->index];    if (top_var > level) {        res = empty;    } else if (top_var == level) {	res = cuddT(P);    } else {        t = zdd_subset1_aux(zdd, cuddT(P), zvar);	if (t == NULL) return(NULL);	cuddRef(t);        e = zdd_subset1_aux(zdd, cuddE(P), zvar);	if (e == NULL) {	    Cudd_RecursiveDerefZdd(zdd, t);	    return(NULL);	}	cuddRef(e);        res = cuddZddGetNode(zdd, P->index, t, e);	if (res == NULL) {	    Cudd_RecursiveDerefZdd(zdd, t);	    Cudd_RecursiveDerefZdd(zdd, e);	    return(NULL);	}	cuddDeref(t);	cuddDeref(e);    }    cuddCacheInsert2(zdd, zdd_subset1_aux, P, zvar, res);    return(res);} /* end of zdd_subset1_aux */

/**Function********************************************************************  Synopsis    [Returns 1 if f &gt g and 0 otherwise.]  Description [Returns 1 if f &gt g (both should be terminal cases) and 0   otherwise. Used in conjunction with Cudd_addApply. Returns NULL if not a   terminal case.]  SideEffects [None]  SeeAlso     [Cudd_addApply]******************************************************************************/DdNode *Cudd_addOneZeroMaximum(  DdManager * dd,  DdNode ** f,  DdNode ** g){    if (*g == DD_PLUS_INFINITY(dd))	return DD_ZERO(dd);    if (cuddIsConstant(*f) && cuddIsConstant(*g)) {	if (cuddV(*f) > cuddV(*g)) {	    return(DD_ONE(dd));	} else {	    return(DD_ZERO(dd));	}    }    return(NULL);} /* end of Cudd_addOneZeroMaximum */

/**Function********************************************************************  Synopsis    [Integer and floating point subtraction.]  Description [Integer and floating point subtraction. Returns NULL if  not a terminal case; f - g otherwise.]  SideEffects [None]  SeeAlso     [Cudd_addApply]******************************************************************************/DdNode *Cudd_addMinus(  DdManager * dd,  DdNode ** f,  DdNode ** g){    DdNode *res;    DdNode *F, *G;    CUDD_VALUE_TYPE value;    F = *f; G = *g;    if (F == DD_ZERO(dd)) return(cuddAddNegateRecur(dd,G));    if (G == DD_ZERO(dd)) return(F);    if (cuddIsConstant(F) && cuddIsConstant(G)) {	value = cuddV(F)-cuddV(G);	res = cuddUniqueConst(dd,value);	return(res);    }    return(NULL);} /* end of Cudd_addMinus */

/**Function********************************************************************  Synopsis    [Integer and floating point division.]  Description [Integer and floating point division. Returns NULL if not  a terminal case; f / g otherwise.]  SideEffects [None]  SeeAlso     [Cudd_addApply]******************************************************************************/DdNode *Cudd_addDivide(  DdManager * dd,  DdNode ** f,  DdNode ** g){    DdNode *res;    DdNode *F, *G;    CUDD_VALUE_TYPE value;    F = *f; G = *g;    if (F == DD_ZERO(dd)) return(DD_ZERO(dd));    if (G == DD_ONE(dd)) return(F);    if (cuddIsConstant(F) && cuddIsConstant(G)) {	value = cuddV(F)/cuddV(G);	res = cuddUniqueConst(dd,value);	return(res);    }    return(NULL);} /* end of Cudd_addDivide */

/**Function********************************************************************  Synopsis    [Performs the recursive step for Cudd_addIthBit.]  Description [Performs the recursive step for Cudd_addIthBit.  Returns a pointer to the BDD if successful; NULL otherwise.]  SideEffects [None]  SeeAlso     []******************************************************************************/static DdNode *addDoIthBit(  DdManager * dd,  DdNode * f,  DdNode * index){    DdNode *res, *T, *E;    DdNode *fv, *fvn;    int mask, value;    int v;    statLine(dd);    /* Check terminal case. */    if (cuddIsConstant(f)) {	mask = 1 << ((int) cuddV(index));	value = (int) cuddV(f);	return((value & mask) == 0 ? DD_ZERO(dd) : DD_ONE(dd));    }    /* Check cache. */    res = cuddCacheLookup2(dd,addDoIthBit,f,index);    if (res != NULL) return(res);    /* Recursive step. */    v = f->index;    fv = cuddT(f); fvn = cuddE(f);    T = addDoIthBit(dd,fv,index);    if (T == NULL) return(NULL);    cuddRef(T);    E = addDoIthBit(dd,fvn,index);    if (E == NULL) {	Cudd_RecursiveDeref(dd, T);	return(NULL);    }    cuddRef(E);    res = (T == E) ? T : cuddUniqueInter(dd,v,T,E);    if (res == NULL) {	Cudd_RecursiveDeref(dd, T);	Cudd_RecursiveDeref(dd, E);	return(NULL);    }    cuddDeref(T);    cuddDeref(E);    /* Store result. */    cuddCacheInsert2(dd,addDoIthBit,f,index,res);    return(res);} /* end of addDoIthBit */

/**Function********************************************************************  Synopsis    [Integer and floating point division.]  Description [Integer and floating point division. Returns NULL if not  a terminal case; f / g otherwise.]  SideEffects [None]  SeeAlso     [Cudd_addApply]******************************************************************************/DdNode *Cudd_addDivide(  DdManager * dd,  DdNode ** f,  DdNode ** g){    DdNode *res;    DdNode *F, *G;    CUDD_VALUE_TYPE value;    F = *f; G = *g;    /* We would like to use F == G -> F/G == 1, but F and G may    ** contain zeroes. */    if (F == DD_ZERO(dd)) return(DD_ZERO(dd));    if (G == DD_ONE(dd)) return(F);    if (cuddIsConstant(F) && cuddIsConstant(G)) {	value = cuddV(F)/cuddV(G);	res = cuddUniqueConst(dd,value);	return(res);    }    return(NULL);} /* end of Cudd_addDivide */

/**Function********************************************************************  Synopsis    [Checks whether cube is an ADD representing the product  of positive literals.]  Description [Checks whether cube is an ADD representing the product of  positive literals. Returns 1 in case of success; 0 otherwise.]  SideEffects [None]  SeeAlso     []******************************************************************************/static intaddCheckPositiveCube(  DdManager * manager,  DdNode * cube){    if (Cudd_IsComplement(cube)) return(0);    if (cube == DD_ONE(manager)) return(1);    if (cuddIsConstant(cube)) return(0);    if (cuddE(cube) == DD_ZERO(manager)) {        return(addCheckPositiveCube(manager, cuddT(cube)));    }    return(0);} /* end of addCheckPositiveCube */

/**Function********************************************************************  Synopsis [Performs the inclusion test for ZDDs (P implies Q).]  Description [Inclusion test for ZDDs (P implies Q). No new nodes are  generated by this procedure. Returns empty if true;  a valid pointer different from empty or DD_NON_CONSTANT otherwise.]  SideEffects [None]  SeeAlso     [Cudd_zddDiff]******************************************************************************/DdNode *Cudd_zddDiffConst(  DdManager * zdd,  DdNode * P,  DdNode * Q){    int		p_top, q_top;    DdNode	*empty = DD_ZERO(zdd), *t, *res;    DdManager	*table = zdd;    statLine(zdd);    if (P == empty)	return(empty);    if (Q == empty)	return(P);    if (P == Q)	return(empty);    /* Check cache.  The cache is shared by cuddZddDiff(). */    res = cuddCacheLookup2Zdd(table, cuddZddDiff, P, Q);    if (res != NULL)	return(res);    if (cuddIsConstant(P))	p_top = P->index;    else	p_top = zdd->permZ[P->index];    if (cuddIsConstant(Q))	q_top = Q->index;    else	q_top = zdd->permZ[Q->index];    if (p_top < q_top) {	res = DD_NON_CONSTANT;    } else if (p_top > q_top) {	res = Cudd_zddDiffConst(zdd, P, cuddE(Q));    } else {	t = Cudd_zddDiffConst(zdd, cuddT(P), cuddT(Q));	if (t != empty)	    res = DD_NON_CONSTANT;	else	    res = Cudd_zddDiffConst(zdd, cuddE(P), cuddE(Q));    }    cuddCacheInsert2(table, cuddZddDiff, P, Q, res);    return(res);} /* end of Cudd_zddDiffConst */

/**Function********************************************************************  Synopsis    [Performs the recursive step of Cudd_addCmpl.]  Description [Performs the recursive step of Cudd_addCmpl. Returns a  pointer to the resulting ADD if successful; NULL otherwise.]  SideEffects [None]  SeeAlso     [Cudd_addCmpl]******************************************************************************/DdNode *cuddAddCmplRecur(  DdManager * dd,  DdNode * f){    DdNode *one,*zero;    DdNode *r,*Fv,*Fnv,*t,*e;    statLine(dd);    one = DD_ONE(dd);    zero = DD_ZERO(dd);     if (cuddIsConstant(f)) {        if (f == zero) {	    return(one);	} else {	    return(zero);	}    }    r = cuddCacheLookup1(dd,Cudd_addCmpl,f);    if (r != NULL) {	return(r);    }    Fv = cuddT(f);    Fnv = cuddE(f);    t = cuddAddCmplRecur(dd,Fv);    if (t == NULL) return(NULL);    cuddRef(t);    e = cuddAddCmplRecur(dd,Fnv);    if (e == NULL) {	Cudd_RecursiveDeref(dd,t);	return(NULL);    }    cuddRef(e);    r = (t == e) ? t : cuddUniqueInter(dd,(int)f->index,t,e);    if (r == NULL) {	Cudd_RecursiveDeref(dd, t);	Cudd_RecursiveDeref(dd, e);	return(NULL);    }    cuddDeref(t);    cuddDeref(e);    cuddCacheInsert1(dd,Cudd_addCmpl,f,r);    return(r);} /* end of cuddAddCmplRecur */

/**Function********************************************************************  Synopsis    [Computes the Hamming distance ADD.]  Description [Computes the Hamming distance ADD. Returns an ADD that  gives the Hamming distance between its two arguments if successful;  NULL otherwise. The two vectors xVars and yVars identify the variables  that form the two arguments.]  SideEffects [None]  SeeAlso     []******************************************************************************/DdNode *Cudd_addHamming(  DdManager * dd,  DdNode ** xVars,  DdNode ** yVars,  int  nVars){    DdNode  *result,*tempBdd;    DdNode  *tempAdd,*temp;    int     i;    result = DD_ZERO(dd);    cuddRef(result);    for (i = 0; i < nVars; i++) {	tempBdd = Cudd_bddIte(dd,xVars[i],Cudd_Not(yVars[i]),yVars[i]);	if (tempBdd == NULL) {	    Cudd_RecursiveDeref(dd,result);	    return(NULL);	}	cuddRef(tempBdd);	tempAdd = Cudd_BddToAdd(dd,tempBdd);	if (tempAdd == NULL) {	    Cudd_RecursiveDeref(dd,tempBdd);	    Cudd_RecursiveDeref(dd,result);	    return(NULL);	}	cuddRef(tempAdd);	Cudd_RecursiveDeref(dd,tempBdd);	temp = Cudd_addApply(dd,Cudd_addPlus,tempAdd,result);	if (temp == NULL) {	    Cudd_RecursiveDeref(dd,tempAdd);	    Cudd_RecursiveDeref(dd,result);	    return(NULL);	}	cuddRef(temp);	Cudd_RecursiveDeref(dd,tempAdd);	Cudd_RecursiveDeref(dd,result);	result = temp;    }    cuddDeref(result);    return(result);} /* end of Cudd_addHamming */

/**Function********************************************************************  Synopsis    [f if f>=g; 0 if f<g.]  Description [Threshold operator for Apply (f if f >=g; 0 if f<g).  Returns NULL if not a terminal case; f op g otherwise.]  SideEffects [None]  SeeAlso     [Cudd_addApply]******************************************************************************/DdNode *Cudd_addThreshold(  DdManager * dd,  DdNode ** f,  DdNode ** g){    DdNode *F, *G;    F = *f; G = *g;    if (cuddIsConstant(F) && cuddIsConstant(G)) {	if (cuddV(F) >= cuddV(G)) {	    return(F);	} else {	    return(DD_ZERO(dd));	}    }    return(NULL);} /* end of Cudd_addThreshold */

/**Function********************************************************************  Synopsis    [Computes the cofactor of f with respect to g.]  Description [Computes the cofactor of f with respect to g; g must be  the BDD or the ADD of a cube. Returns a pointer to the cofactor if  successful; NULL otherwise.]  SideEffects [None]  SeeAlso     [Cudd_bddConstrain Cudd_bddRestrict]******************************************************************************/DdNode *Cudd_Cofactor(  DdManager * dd,  DdNode * f,  DdNode * g){    DdNode *res,*zero;    zero = Cudd_Not(DD_ONE(dd));    if (g == zero || g == DD_ZERO(dd)) {	(void) fprintf(stdout,"Cudd_Cofactor: Invalid restriction 1/n");	return(NULL);    }    do {	dd->reordered = 0;	res = cuddCofactorRecur(dd,f,g);    } while (dd->reordered == 1);    return(res);} /* end of Cudd_Cofactor */

/**Function********************************************************************  Synopsis [Counts the number of minterms in a ZDD.]  Description [Returns an integer representing the number of minterms  in a ZDD.]  SideEffects [None]  SeeAlso     [Cudd_zddCountDouble]******************************************************************************/intCudd_zddCount(  DdManager * zdd,  DdNode * P){    st_table	*table;    int		res;    DdNode	*base, *empty;    base  = DD_ONE(zdd);    empty = DD_ZERO(zdd);    table = st_init_table(st_ptrcmp, st_ptrhash);    if (table == NULL) return(CUDD_OUT_OF_MEM);    res = cuddZddCountStep(P, table, base, empty);    if (res == CUDD_OUT_OF_MEM) {	zdd->errorCode = CUDD_MEMORY_OUT;    }    st_foreach(table, st_zdd_countfree, NIL(char));    st_free_table(table);    return(res);} /* end of Cudd_zddCount */

/**Function********************************************************************  Synopsis [Substitutes a variable with its complement in a ZDD.]  Description [Substitutes a variable with its complement in a ZDD.  returns a pointer to the result if successful; NULL  otherwise. cuddZddChange performs the same function as  Cudd_zddChange, but does not restart if reordering has taken  place. Therefore it can be called from within a recursive  procedure.]  SideEffects [None]  SeeAlso     [Cudd_zddChange]******************************************************************************/DdNode *cuddZddChange(  DdManager * dd,  DdNode * P,  int  var){    DdNode	*zvar, *res;    zvar = cuddUniqueInterZdd(dd, var, DD_ONE(dd), DD_ZERO(dd));    if (zvar == NULL) return(NULL);    cuddRef(zvar);    res = cuddZddChangeAux(dd, P, zvar);    if (res == NULL) {	Cudd_RecursiveDerefZdd(dd,zvar);	return(NULL);    }    cuddRef(res);    Cudd_RecursiveDerefZdd(dd,zvar);    cuddDeref(res);    return(res);} /* end of cuddZddChange */

/**Function********************************************************************  Synopsis    [Calculates the product of two matrices represented as  ADDs.]  Description [Calculates the product of two matrices, A and B,  represented as ADDs, using the CMU matrix by matrix multiplication  procedure by Clarke et al..  Matrix A has x's as row variables and z's  as column variables, while matrix B has z's as row variables and y's  as column variables. Returns the pointer to the result if successful;  NULL otherwise. The resulting matrix has x's as row variables and y's  as column variables.]  SideEffects [None]  SeeAlso     [Cudd_addMatrixMultiply]******************************************************************************/DdNode *Cudd_addTimesPlus(  DdManager * dd,  DdNode * A,  DdNode * B,  DdNode ** z,  int  nz){    DdNode *w, *cube, *tmp, *res;     int i;    tmp = Cudd_addApply(dd,Cudd_addTimes,A,B);    if (tmp == NULL) return(NULL);    Cudd_Ref(tmp);    Cudd_Ref(cube = DD_ONE(dd));    for (i = nz-1; i >= 0; i--) {	 w = Cudd_addIte(dd,z[i],cube,DD_ZERO(dd));	 if (w == NULL) {	    Cudd_RecursiveDeref(dd,tmp);	    return(NULL);	 }	 Cudd_Ref(w);	 Cudd_RecursiveDeref(dd,cube);	 cube = w;    }    res = Cudd_addExistAbstract(dd,tmp,cube);    if (res == NULL) {	Cudd_RecursiveDeref(dd,tmp);	Cudd_RecursiveDeref(dd,cube);	return(NULL);    }    Cudd_Ref(res);    Cudd_RecursiveDeref(dd,cube);    Cudd_RecursiveDeref(dd,tmp);    Cudd_Deref(res);    return(res);} /* end of Cudd_addTimesPlus */

/**Function********************************************************************  Synopsis [Prints to the standard output a ZDD and its statistics.]  Description [Prints to the standard output a DD and its statistics.  The statistics include the number of nodes and the number of minterms.  (The number of minterms is also the number of combinations in the set.)  The statistics are printed if pr &gt; 0.  Specifically:  <ul>  <li> pr = 0 : prints nothing  <li> pr = 1 : prints counts of nodes and minterms  <li> pr = 2 : prints counts + disjoint sum of products  <li> pr = 3 : prints counts + list of nodes  <li> pr &gt; 3 : prints counts + disjoint sum of products + list of nodes  </ul>  Returns 1 if successful; 0 otherwise.  ]  SideEffects [None]  SeeAlso     []******************************************************************************/intCudd_zddPrintDebug(  DdManager * zdd,  DdNode * f,  int  n,  int  pr){    DdNode	*empty = DD_ZERO(zdd);    int		nodes;    double	minterms;    int		retval = 1;    if (f == empty && pr > 0) {	(void) fprintf(zdd->out,": is the empty ZDD/n");	(void) fflush(zdd->out);	return(1);    }    if (pr > 0) {	nodes = Cudd_zddDagSize(f);	if (nodes == CUDD_OUT_OF_MEM) retval = 0;	minterms = Cudd_zddCountMinterm(zdd, f, n);	if (minterms == (double)CUDD_OUT_OF_MEM) retval = 0;	(void) fprintf(zdd->out,": %d nodes %g minterms/n",		       nodes, minterms);	if (pr > 2)	    if (!cuddZddP(zdd, f)) retval = 0;	if (pr == 2 || pr > 3) {	    if (!Cudd_zddPrintMinterm(zdd, f)) retval = 0;	    (void) fprintf(zdd->out,"/n");	}	(void) fflush(zdd->out);    }    return(retval);} /* end of Cudd_zddPrintDebug */

/**  @brief Builds an %ADD for the residue modulo m of an n-bit  number.  @details The modulus must be at least 2, and the number of bits at  least 1. Parameter options specifies whether the MSB should be on top  or the LSB; and whther the number whose residue is computed is in  two's complement notation or not. The macro CUDD_RESIDUE_DEFAULT  specifies LSB on top and unsigned number. The macro CUDD_RESIDUE_MSB  specifies MSB on top, and the macro CUDD_RESIDUE_TC specifies two's  complement residue. To request MSB on top and two's complement residue  simultaneously, one can OR the two macros:  CUDD_RESIDUE_MSB | CUDD_RESIDUE_TC.  @return a pointer to the resulting %ADD if successful; NULL  otherwise.  @sideeffect None*/DdNode *Cudd_addResidue(  DdManager * dd /**< manager */,  int  n /**< number of bits */,  int  m /**< modulus */,  int  options /**< options */,  int  top /**< index of top variable */){    int msbLsb;	/* MSB on top (1) or LSB on top (0) */    int tc;	/* two's complement (1) or unsigned (0) */    int i, j, k, t, residue, thisOne, previous, index;    DdNode **array[2], *var, *tmp, *res;    /* Sanity check. */    if (n < 1 && m < 2) return(NULL);    msbLsb = options & CUDD_RESIDUE_MSB;    tc = options & CUDD_RESIDUE_TC;    /* Allocate and initialize working arrays. */    array[0] = ALLOC(DdNode *,m);    if (array[0] == NULL) {	dd->errorCode = CUDD_MEMORY_OUT;	return(NULL);    }    array[1] = ALLOC(DdNode *,m);    if (array[1] == NULL) {	FREE(array[0]);	dd->errorCode = CUDD_MEMORY_OUT;	return(NULL);    }    for (i = 0; i < m; i++) {	array[0][i] = array[1][i] = NULL;    }    /* Initialize residues. */    for (i = 0; i < m; i++) {	tmp = cuddUniqueConst(dd,(CUDD_VALUE_TYPE) i);	if (tmp == NULL) {	    for (j = 0; j < i; j++) {		Cudd_RecursiveDeref(dd,array[1][j]);	    }	    FREE(array[0]);	    FREE(array[1]);	    return(NULL);	}	cuddRef(tmp);	array[1][i] = tmp;    }    /* Main iteration. */    residue = 1;	/* residue of 2**0 */    for (k = 0; k < n; k++) {	/* Choose current and previous arrays. */	thisOne = k & 1;	previous = thisOne ^ 1;	/* Build an ADD projection function. */	if (msbLsb) {	    index = top+n-k-1;	} else {	    index = top+k;	}	var = cuddUniqueInter(dd,index,DD_ONE(dd),DD_ZERO(dd));	if (var == NULL) {	    for (j = 0; j < m; j++) {		Cudd_RecursiveDeref(dd,array[previous][j]);	    }	    FREE(array[0]);	    FREE(array[1]);	    return(NULL);	}	cuddRef(var);	for (i = 0; i < m; i ++) {	    t = (i + residue) % m;	    tmp = Cudd_addIte(dd,var,array[previous][t],array[previous][i]);	    if (tmp == NULL) {		for (j = 0; j < i; j++) {		    Cudd_RecursiveDeref(dd,array[thisOne][j]);		}		for (j = 0; j < m; j++) {//.........这里部分代码省略.........

/**Function********************************************************************  Synopsis    [Reads in a matrix in the format of the Harwell-Boeing  benchmark suite.]  Description [Reads in a matrix in the format of the Harwell-Boeing  benchmark suite. The variables are ordered as follows:  <blockquote>  x/[0/] y/[0/] x/[1/] y/[1/] ...  </blockquote>  0 is the most significant bit.  On input, nx and ny hold the numbers  of row and column variables already in existence. On output, they  hold the numbers of row and column variables actually used by the  matrix.  m and n are set to the numbers of rows and columns of the  matrix.  Their values on input are immaterial.  Returns 1 on  success; 0 otherwise. The ADD for the sparse matrix is returned in  E, and its reference count is > 0.]  SideEffects [None]  SeeAlso     [Cudd_addRead Cudd_bddRead]******************************************************************************/intCudd_addHarwell(  FILE * fp /* pointer to the input file */,  DdManager * dd /* DD manager */,  DdNode ** E /* characteristic function of the graph */,  DdNode *** x /* array of row variables */,  DdNode *** y /* array of column variables */,  DdNode *** xn /* array of complemented row variables */,  DdNode *** yn_ /* array of complemented column variables */,  int * nx /* number or row variables */,  int * ny /* number or column variables */,  int * m /* number of rows */,  int * n /* number of columns */,  int  bx /* first index of row variables */,  int  sx /* step of row variables */,  int  by /* first index of column variables */,  int  sy /* step of column variables */,  int  pr /* verbosity level */){    DdNode *one, *zero;    DdNode *w;    DdNode *cubex, *cubey, *minterm1;    int u, v, err, i, j, nv;    double val;    DdNode **lx, **ly, **lxn, **lyn;	/* local copies of x, y, xn, yn_ */    int lnx, lny;			/* local copies of nx and ny */    char title[73], key[9], mxtype[4], rhstyp[4];    int totcrd, ptrcrd, indcrd, valcrd, rhscrd,        nrow, ncol, nnzero, neltvl,	nrhs, nrhsix;    int *colptr, *rowind;#if 0    int nguess, nexact;    int	*rhsptr, *rhsind;#endif    if (*nx < 0 || *ny < 0) return(0);    one = DD_ONE(dd);    zero = DD_ZERO(dd);    /* Read the header */    err = fscanf(fp, "%72c %8c", title, key);    if (err == EOF) {	return(0);    } else if (err != 2) {        return(0);    }    title[72] = (char) 0;    key[8] = (char) 0;    err = fscanf(fp, "%d %d %d %d %d", &totcrd, &ptrcrd, &indcrd,    &valcrd, &rhscrd);    if (err == EOF) {	return(0);    } else if (err != 5) {        return(0);    }    err = fscanf(fp, "%3s %d %d %d %d", mxtype, &nrow, &ncol,    &nnzero, &neltvl);    if (err == EOF) {	return(0);    } else if (err != 5) {        return(0);    }    /* Skip FORTRAN formats */    if (rhscrd == 0) {	err = fscanf(fp, "%*s %*s %*s /n");    } else {	err = fscanf(fp, "%*s %*s %*s %*s /n");    }    if (err == EOF) {	return(0);    } else if (err != 0) {        return(0);//.........这里部分代码省略.........

/**Function********************************************************************  Synopsis    [Generates an ADD for the function x==y.]  Description [This function generates an ADD for the function x==y.  Both x and y are N-bit numbers, x/[0/] x/[1/] ... x/[N-1/] and  y/[0/] y/[1/] ...  y/[N-1/], with 0 the most significant bit.  The ADD is built bottom-up.  It has 3*N-1 internal nodes, if the variables are ordered as follows:   x/[0/] y/[0/] x/[1/] y/[1/] ... x/[N-1/] y/[N-1/]. ]  SideEffects [None]  SeeAlso     [Cudd_Xeqy]******************************************************************************/DdNode *Cudd_addXeqy(  DdManager * dd /* DD manager */,  int  N /* number of x and y variables */,  DdNode ** x /* array of x variables */,  DdNode ** y /* array of y variables */){    DdNode *one, *zero;    DdNode *u, *v, *w;    int     i;    one = DD_ONE(dd);    zero = DD_ZERO(dd);    /* Build bottom part of ADD outside loop. */    v = Cudd_addIte(dd, y[N-1], one, zero);    if (v == NULL) return(NULL);    cuddRef(v);    w = Cudd_addIte(dd, y[N-1], zero, one);    if (w == NULL) {	Cudd_RecursiveDeref(dd, v);	return(NULL);    }    cuddRef(w);    u = Cudd_addIte(dd, x[N-1], v, w);    if (w == NULL) {	Cudd_RecursiveDeref(dd, v);	Cudd_RecursiveDeref(dd, w);	return(NULL);    }    cuddRef(u);    Cudd_RecursiveDeref(dd, v);    Cudd_RecursiveDeref(dd, w);    /* Loop to build the rest of the ADD. */    for (i = N-2; i >= 0; i--) {	v = Cudd_addIte(dd, y[i], u, zero);	if (v == NULL) {	    Cudd_RecursiveDeref(dd, u);	    return(NULL);	}	cuddRef(v);	w = Cudd_addIte(dd, y[i], zero, u);	if (w == NULL) {	    Cudd_RecursiveDeref(dd, u);	    Cudd_RecursiveDeref(dd, v);	    return(NULL);	}	cuddRef(w);	Cudd_RecursiveDeref(dd, u);	u = Cudd_addIte(dd, x[i], v, w);	if (w == NULL) {	    Cudd_RecursiveDeref(dd, v);	    Cudd_RecursiveDeref(dd, w);	    return(NULL);	}	cuddRef(u);	Cudd_RecursiveDeref(dd, v);	Cudd_RecursiveDeref(dd, w);    }    cuddDeref(u);    return(u);} /* end of Cudd_addXeqy */

/**Function********************************************************************  Synopsis [Performs the recursive step of Cudd_zddIsop.]  Description []  SideEffects [None]  SeeAlso     [Cudd_zddIsop]******************************************************************************/DdNode	*cuddZddIsop(  DdManager * dd,  DdNode * L,  DdNode * U,  DdNode ** zdd_I){    DdNode	*one = DD_ONE(dd);    DdNode	*zero = Cudd_Not(one);    DdNode	*zdd_one = DD_ONE(dd);    DdNode	*zdd_zero = DD_ZERO(dd);    int		v, top_l, top_u;    DdNode	*Lsub0, *Usub0, *Lsub1, *Usub1, *Ld, *Ud;    DdNode	*Lsuper0, *Usuper0, *Lsuper1, *Usuper1;    DdNode	*Isub0, *Isub1, *Id;    DdNode	*zdd_Isub0, *zdd_Isub1, *zdd_Id;    DdNode	*x;    DdNode	*term0, *term1, *sum;    DdNode	*Lv, *Uv, *Lnv, *Unv;    DdNode	*r, *y, *z;    int		index;    DdNode *(*cacheOp)(DdManager *, DdNode *, DdNode *);    statLine(dd);    if (L == zero) {	*zdd_I = zdd_zero;    	return(zero);    }    if (U == one) {	*zdd_I = zdd_one;    	return(one);    }    if (U == zero || L == one) {	printf("*** ERROR : illegal condition for ISOP (U < L)./n");	exit(1);    }    /* Check the cache. We store two results for each recursive call.    ** One is the BDD, and the other is the ZDD. Both are needed.    ** Hence we need a double hit in the cache to terminate the    ** recursion. Clearly, collisions may evict only one of the two    ** results. */    cacheOp = (DdNode *(*)(DdManager *, DdNode *, DdNode *)) cuddZddIsop;    r = cuddCacheLookup2(dd, cuddBddIsop, L, U);    if (r) {	*zdd_I = cuddCacheLookup2Zdd(dd, cacheOp, L, U);	if (*zdd_I)	    return(r);	else {	    /* The BDD result may have been dead. In that case	    ** cuddCacheLookup2 would have called cuddReclaim,	    ** whose effects we now have to undo. */	    cuddRef(r);	    Cudd_RecursiveDeref(dd, r);	}    }    top_l = dd->perm[Cudd_Regular(L)->index];    top_u = dd->perm[Cudd_Regular(U)->index];    v = ddMin(top_l, top_u);    /* Compute cofactors. */    if (top_l == v) {	index = Cudd_Regular(L)->index;    	Lv = Cudd_T(L);    	Lnv = Cudd_E(L);    	if (Cudd_IsComplement(L)) {    	    Lv = Cudd_Not(Lv);    	    Lnv = Cudd_Not(Lnv);    	}    }    else {	index = Cudd_Regular(U)->index;        Lv = Lnv = L;    }    if (top_u == v) {    	Uv = Cudd_T(U);    	Unv = Cudd_E(U);    	if (Cudd_IsComplement(U)) {    	    Uv = Cudd_Not(Uv);    	    Unv = Cudd_Not(Unv);    	}    }    else {        Uv = Unv = U;    }//.........这里部分代码省略.........

/**Function********************************************************************  Synopsis [Performs the recursive step of Cudd_zddPortToBdd.]  Description []  SideEffects [None]  SeeAlso     []******************************************************************************/static DdNode *zddPortToBddStep(  DdManager * dd /* manager */,  DdNode * f /* ZDD to be converted */,  int  depth /* recursion depth */){    DdNode *one, *zero, *T, *E, *res, *var;    unsigned int index;    unsigned int level;    statLine(dd);    one = DD_ONE(dd);    zero = DD_ZERO(dd);    if (f == zero) return(Cudd_Not(one));    if (depth == dd->sizeZ) return(one);    index = dd->invpermZ[depth];    level = cuddIZ(dd,f->index);    var = cuddUniqueInter(dd,index,one,Cudd_Not(one));    if (var == NULL) return(NULL);    cuddRef(var);    if (level > (unsigned) depth) {	E = zddPortToBddStep(dd,f,depth+1);	if (E == NULL) {	    Cudd_RecursiveDeref(dd,var);	    return(NULL);	}	cuddRef(E);	res = cuddBddIteRecur(dd,var,Cudd_Not(one),E);	if (res == NULL) {	    Cudd_RecursiveDeref(dd,var);	    Cudd_RecursiveDeref(dd,E);	    return(NULL);	}	cuddRef(res);	Cudd_RecursiveDeref(dd,var);	Cudd_RecursiveDeref(dd,E);	cuddDeref(res);	return(res);    }    res = cuddCacheLookup1(dd,Cudd_zddPortToBdd,f);    if (res != NULL) {	Cudd_RecursiveDeref(dd,var);	return(res);    }    T = zddPortToBddStep(dd,cuddT(f),depth+1);    if (T == NULL) {	Cudd_RecursiveDeref(dd,var);	return(NULL);    }    cuddRef(T);    E = zddPortToBddStep(dd,cuddE(f),depth+1);    if (E == NULL) {	Cudd_RecursiveDeref(dd,var);	Cudd_RecursiveDeref(dd,T);	return(NULL);    }    cuddRef(E);    res = cuddBddIteRecur(dd,var,T,E);    if (res == NULL) {	Cudd_RecursiveDeref(dd,var);	Cudd_RecursiveDeref(dd,T);	Cudd_RecursiveDeref(dd,E);	return(NULL);    }    cuddRef(res);    Cudd_RecursiveDeref(dd,var);    Cudd_RecursiveDeref(dd,T);    Cudd_RecursiveDeref(dd,E);    cuddDeref(res);    cuddCacheInsert1(dd,Cudd_zddPortToBdd,f,res);    return(res);} /* end of zddPortToBddStep */

/**Function********************************************************************  Synopsis [Performs the recursive step of Cudd_zddPortFromBdd.]  Description []  SideEffects [None]  SeeAlso     []******************************************************************************/static DdNode *zddPortFromBddStep(  DdManager * dd,  DdNode * B,  int  expected){    DdNode	*res, *prevZdd, *t, *e;    DdNode	*Breg, *Bt, *Be;    int		id, level;    statLine(dd);    /* Terminal cases. */    if (B == Cudd_Not(DD_ONE(dd)))	return(DD_ZERO(dd));    if (B == DD_ONE(dd)) {	if (expected >= dd->sizeZ) {	    return(DD_ONE(dd));	} else {	    return(dd->univ[expected]);	}    }    Breg = Cudd_Regular(B);    /* Computed table look-up. */    res = cuddCacheLookup1Zdd(dd,Cudd_zddPortFromBdd,B);    if (res != NULL) {	level = cuddI(dd,Breg->index);	/* Adding DC vars. */	if (expected < level) {	    /* Add suppressed variables. */	    cuddRef(res);	    for (level--; level >= expected; level--) {		prevZdd = res;		id = dd->invperm[level];		res = cuddZddGetNode(dd, id, prevZdd, prevZdd);		if (res == NULL) {		    Cudd_RecursiveDerefZdd(dd, prevZdd);		    return(NULL);		}		cuddRef(res);		Cudd_RecursiveDerefZdd(dd, prevZdd);	    }	    cuddDeref(res);	}	return(res);    }	/* end of cache look-up */    if (Cudd_IsComplement(B)) {	Bt = Cudd_Not(cuddT(Breg));	Be = Cudd_Not(cuddE(Breg));    } else {	Bt = cuddT(Breg);	Be = cuddE(Breg);    }    id = Breg->index;    level = cuddI(dd,id);    t = zddPortFromBddStep(dd, Bt, level+1);    if (t == NULL) return(NULL);    cuddRef(t);    e = zddPortFromBddStep(dd, Be, level+1);    if (e == NULL) {	Cudd_RecursiveDerefZdd(dd, t);	return(NULL);    }    cuddRef(e);    res = cuddZddGetNode(dd, id, t, e);    if (res == NULL) {	Cudd_RecursiveDerefZdd(dd, t);	Cudd_RecursiveDerefZdd(dd, e);	return(NULL);    }    cuddRef(res);    Cudd_RecursiveDerefZdd(dd, t);    Cudd_RecursiveDerefZdd(dd, e);    cuddCacheInsert1(dd,Cudd_zddPortFromBdd,B,res);    for (level--; level >= expected; level--) {	prevZdd = res;	id = dd->invperm[level];	res = cuddZddGetNode(dd, id, prevZdd, prevZdd);	if (res == NULL) {	    Cudd_RecursiveDerefZdd(dd, prevZdd);	    return(NULL);	}	cuddRef(res);	Cudd_RecursiveDerefZdd(dd, prevZdd);//.........这里部分代码省略.........

/**Function********************************************************************  Synopsis [Performs the recursive step of Cudd_zddDiff.]  Description []  SideEffects [None]  SeeAlso     []******************************************************************************/DdNode *cuddZddDiff(  DdManager * zdd,  DdNode * P,  DdNode * Q){    int		p_top, q_top;    DdNode	*empty = DD_ZERO(zdd), *t, *e, *res;    DdManager	*table = zdd;    statLine(zdd);    if (P == empty)	return(empty);    if (Q == empty)	return(P);    if (P == Q)	return(empty);    /* Check cache.  The cache is shared by Cudd_zddDiffConst(). */    res = cuddCacheLookup2Zdd(table, cuddZddDiff, P, Q);    if (res != NULL && res != DD_NON_CONSTANT)	return(res);    if (cuddIsConstant(P))	p_top = P->index;    else	p_top = zdd->permZ[P->index];    if (cuddIsConstant(Q))	q_top = Q->index;    else	q_top = zdd->permZ[Q->index];    if (p_top < q_top) {	e = cuddZddDiff(zdd, cuddE(P), Q);	if (e == NULL) return(NULL);	cuddRef(e);	res = cuddZddGetNode(zdd, P->index, cuddT(P), e);	if (res == NULL) {	    Cudd_RecursiveDerefZdd(table, e);	    return(NULL);	}	cuddDeref(e);    } else if (p_top > q_top) {	res = cuddZddDiff(zdd, P, cuddE(Q));	if (res == NULL) return(NULL);    } else {	t = cuddZddDiff(zdd, cuddT(P), cuddT(Q));	if (t == NULL) return(NULL);	cuddRef(t);	e = cuddZddDiff(zdd, cuddE(P), cuddE(Q));	if (e == NULL) {	    Cudd_RecursiveDerefZdd(table, t);	    return(NULL);	}	cuddRef(e);	res = cuddZddGetNode(zdd, P->index, t, e);	if (res == NULL) {	    Cudd_RecursiveDerefZdd(table, t);	    Cudd_RecursiveDerefZdd(table, e);	    return(NULL);	}	cuddDeref(t);	cuddDeref(e);    }    cuddCacheInsert2(table, cuddZddDiff, P, Q, res);    return(res);} /* end of cuddZddDiff */