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

/**Function********************************************************************  Synopsis    [Performs the recursive step of Cudd_addMatrixMultiply.]  Description [Performs the recursive step of Cudd_addMatrixMultiply.  Returns a pointer to the result if successful; NULL otherwise.]  SideEffects [None]******************************************************************************/static DdNode *addMMRecur(  DdManager * dd,  DdNode * A,  DdNode * B,  int  topP,  int * vars){    DdNode *zero,           *At,		/* positive cofactor of first operand */	   *Ae,		/* negative cofactor of first operand */	   *Bt,		/* positive cofactor of second operand */	   *Be,		/* negative cofactor of second operand */	   *t,		/* positive cofactor of result */	   *e,		/* negative cofactor of result */	   *scaled,	/* scaled result */	   *add_scale,	/* ADD representing the scaling factor */	   *res;    int	i;		/* loop index */    double scale;	/* scaling factor */    int index;		/* index of the top variable */    CUDD_VALUE_TYPE value;    unsigned int topA, topB, topV;    DD_CTFP cacheOp;    statLine(dd);    zero = DD_ZERO(dd);    if (A == zero || B == zero) {        return(zero);    }    if (cuddIsConstant(A) && cuddIsConstant(B)) {	/* Compute the scaling factor. It is 2^k, where k is the	** number of summation variables below the current variable.	** Indeed, these constants represent blocks of 2^k identical	** constant values in both A and B.	*/	value = cuddV(A) * cuddV(B);	for (i = 0; i < dd->size; i++) {	    if (vars[i]) {		if (dd->perm[i] > topP) {		    value *= (CUDD_VALUE_TYPE) 2;		}	    }	}	res = cuddUniqueConst(dd, value);	return(res);    }    /* Standardize to increase cache efficiency. Clearly, A*B != B*A    ** in matrix multiplication. However, which matrix is which is    ** determined by the variables appearing in the ADDs and not by    ** which one is passed as first argument.    */    if (A > B) {	DdNode *tmp = A;	A = B;	B = tmp;    }    topA = cuddI(dd,A->index); topB = cuddI(dd,B->index);    topV = ddMin(topA,topB);    cacheOp = (DD_CTFP) addMMRecur;    res = cuddCacheLookup2(dd,cacheOp,A,B);    if (res != NULL) {	/* If the result is 0, there is no need to normalize.	** Otherwise we count the number of z variables between	** the current depth and the top of the ADDs. These are	** the missing variables that determine the size of the	** constant blocks.	*/	if (res == zero) return(res);	scale = 1.0;	for (i = 0; i < dd->size; i++) {	    if (vars[i]) {		if (dd->perm[i] > topP && (unsigned) dd->perm[i] < topV) {		    scale *= 2;		}	    }	}	if (scale > 1.0) {	    cuddRef(res);	    add_scale = cuddUniqueConst(dd,(CUDD_VALUE_TYPE)scale);	    if (add_scale == NULL) {		Cudd_RecursiveDeref(dd, res);		return(NULL);	    }	    cuddRef(add_scale);//.........这里部分代码省略.........

/**Function********************************************************************  Synopsis [Performs the recursive step of Cudd_bddIsop.]  Description []  SideEffects [None]  SeeAlso     [Cudd_bddIsop]******************************************************************************/DdNode	*cuddBddIsop(    DdManager * dd,    DdNode * L,    DdNode * U){    DdNode	*one = DD_ONE(dd);    DdNode	*zero = Cudd_Not(one);    int		v, top_l, top_u;    DdNode	*Lsub0, *Usub0, *Lsub1, *Usub1, *Ld, *Ud;    DdNode	*Lsuper0, *Usuper0, *Lsuper1, *Usuper1;    DdNode	*Isub0, *Isub1, *Id;    DdNode	*x;    DdNode	*term0, *term1, *sum;    DdNode	*Lv, *Uv, *Lnv, *Unv;    DdNode	*r;    int		index;    statLine(dd);    if (L == zero)        return(zero);    if (U == one)        return(one);    /* Check cache */    r = cuddCacheLookup2(dd, cuddBddIsop, L, U);    if (r)        return(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;    }    Lsub0 = cuddBddAndRecur(dd, Lnv, Cudd_Not(Uv));    if (Lsub0 == NULL)        return(NULL);    Cudd_Ref(Lsub0);    Usub0 = Unv;    Lsub1 = cuddBddAndRecur(dd, Lv, Cudd_Not(Unv));    if (Lsub1 == NULL) {        Cudd_RecursiveDeref(dd, Lsub0);        return(NULL);    }    Cudd_Ref(Lsub1);    Usub1 = Uv;    Isub0 = cuddBddIsop(dd, Lsub0, Usub0);    if (Isub0 == NULL) {        Cudd_RecursiveDeref(dd, Lsub0);        Cudd_RecursiveDeref(dd, Lsub1);        return(NULL);    }    Cudd_Ref(Isub0);    Isub1 = cuddBddIsop(dd, Lsub1, Usub1);    if (Isub1 == NULL) {        Cudd_RecursiveDeref(dd, Lsub0);        Cudd_RecursiveDeref(dd, Lsub1);        Cudd_RecursiveDeref(dd, Isub0);        return(NULL);    }    Cudd_Ref(Isub1);    Cudd_RecursiveDeref(dd, Lsub0);//.........这里部分代码省略.........

/**Function********************************************************************  Synopsis    [Performs the recursive step of Cudd_addUnivAbstract.]  Description [Performs the recursive step of Cudd_addUnivAbstract.  Returns the ADD obtained by abstracting the variables of cube from f,  if successful; NULL otherwise.]  SideEffects [None]  SeeAlso     []******************************************************************************/DdNode *cuddAddUnivAbstractRecur(  DdManager * manager,  DdNode * f,  DdNode * cube){    DdNode	*T, *E, *res, *res1, *res2, *one, *zero;    statLine(manager);    one = DD_ONE(manager);    zero = DD_ZERO(manager);    /* Cube is guaranteed to be a cube at this point.    ** zero and one are the only constatnts c such that c*c=c.    */    if (f == zero || f == one || cube == one) {  	return(f);    }    /* Abstract a variable that does not appear in f. */    if (cuddI(manager,f->index) > cuddI(manager,cube->index)) {	res1 = cuddAddUnivAbstractRecur(manager, f, cuddT(cube));	if (res1 == NULL) return(NULL);	cuddRef(res1);	/* Use the "internal" procedure to be alerted in case of	** dynamic reordering. If dynamic reordering occurs, we	** have to abort the entire abstraction.	*/	res = cuddAddApplyRecur(manager, Cudd_addTimes, res1, res1);	if (res == NULL) {	    Cudd_RecursiveDeref(manager,res1);	    return(NULL);	}	cuddRef(res);	Cudd_RecursiveDeref(manager,res1);	cuddDeref(res);	return(res);    }    if ((res = cuddCacheLookup2(manager, Cudd_addUnivAbstract, f, cube)) != NULL) {	return(res);    }    T = cuddT(f);    E = cuddE(f);    /* If the two indices are the same, so are their levels. */    if (f->index == cube->index) {	res1 = cuddAddUnivAbstractRecur(manager, T, cuddT(cube));	if (res1 == NULL) return(NULL);        cuddRef(res1);	res2 = cuddAddUnivAbstractRecur(manager, E, cuddT(cube));	if (res2 == NULL) {	    Cudd_RecursiveDeref(manager,res1);	    return(NULL);	}        cuddRef(res2);	res = cuddAddApplyRecur(manager, Cudd_addTimes, res1, res2);	if (res == NULL) {	    Cudd_RecursiveDeref(manager,res1);	    Cudd_RecursiveDeref(manager,res2);	    return(NULL);	}	cuddRef(res);	Cudd_RecursiveDeref(manager,res1);	Cudd_RecursiveDeref(manager,res2);	cuddCacheInsert2(manager, Cudd_addUnivAbstract, f, cube, res);	cuddDeref(res);        return(res);    } else { /* if (cuddI(manager,f->index) < cuddI(manager,cube->index)) */	res1 = cuddAddUnivAbstractRecur(manager, T, cube);	if (res1 == NULL) return(NULL);        cuddRef(res1);	res2 = cuddAddUnivAbstractRecur(manager, E, cube);	if (res2 == NULL) {	    Cudd_RecursiveDeref(manager,res1);	    return(NULL);	}        cuddRef(res2);	res = (res1 == res2) ? res1 :	    cuddUniqueInter(manager, (int) f->index, res1, res2);	if (res == NULL) {	    Cudd_RecursiveDeref(manager,res1);	    Cudd_RecursiveDeref(manager,res2);	    return(NULL);	}	cuddDeref(res1);//.........这里部分代码省略.........

/**Function********************************************************************  Synopsis [Approximates the AND of two BDDs and simultaneously abstracts the  variables in cube.]  Description [Approximates the AND of two BDDs and simultaneously  abstracts the variables in cube. The variables are existentially  abstracted.  Returns a pointer to the result is successful; NULL  otherwise.]  SideEffects [None]  SeeAlso     [Cudd_bddClippingAndAbstract]******************************************************************************/static DdNode *cuddBddClipAndAbsRecur(  DdManager * manager,  DdNode * f,  DdNode * g,  DdNode * cube,  int  distance,  int  direction){    DdNode *F, *ft, *fe, *G, *gt, *ge;    DdNode *one, *zero, *r, *t, *e, *Cube;    unsigned int topf, topg, topcube, top, index;    ptruint cacheTag;    statLine(manager);    one = DD_ONE(manager);    zero = Cudd_Not(one);    /* Terminal cases. */    if (f == zero || g == zero || f == Cudd_Not(g)) return(zero);    if (f == one && g == one)	return(one);    if (cube == one) {	return(cuddBddClippingAndRecur(manager, f, g, distance, direction));    }    if (f == one || f == g) {	return (cuddBddExistAbstractRecur(manager, g, cube));    }    if (g == one) {	return (cuddBddExistAbstractRecur(manager, f, cube));    }    if (distance == 0) return(Cudd_NotCond(one,(direction == 0)));    /* At this point f, g, and cube are not constant. */    distance--;    /* Check cache. */    if (f > g) { /* Try to increase cache efficiency. */	DdNode *tmp = f;	f = g; g = tmp;    }    F = Cudd_Regular(f);    G = Cudd_Regular(g);    cacheTag = direction ? DD_BDD_CLIPPING_AND_ABSTRACT_UP_TAG :	DD_BDD_CLIPPING_AND_ABSTRACT_DOWN_TAG;    if (F->ref != 1 || G->ref != 1) {	r = cuddCacheLookup(manager, cacheTag,			    f, g, cube);	if (r != NULL) {	    return(r);	}    }    /* Here we can skip the use of cuddI, because the operands are known    ** to be non-constant.    */    topf = manager->perm[F->index];    topg = manager->perm[G->index];    top = ddMin(topf, topg);    topcube = manager->perm[cube->index];    if (topcube < top) {	return(cuddBddClipAndAbsRecur(manager, f, g, cuddT(cube),				      distance, direction));    }    /* Now, topcube >= top. */    if (topf == top) {	index = F->index;	ft = cuddT(F);	fe = cuddE(F);	if (Cudd_IsComplement(f)) {	    ft = Cudd_Not(ft);	    fe = Cudd_Not(fe);	}    } else {	index = G->index;	ft = fe = f;    }    if (topg == top) {	gt = cuddT(G);	ge = cuddE(G);	if (Cudd_IsComplement(g)) {	    gt = Cudd_Not(gt);	    ge = Cudd_Not(ge);//.........这里部分代码省略.........

/**Function********************************************************************  Synopsis    [Performs the recursive step of Cudd_addApply.]  Description [Performs the recursive step of Cudd_addApply. Returns a  pointer to the result if successful; NULL otherwise.]  SideEffects [None]  SeeAlso     [cuddAddMonadicApplyRecur]******************************************************************************/DdNode *cuddAddApplyRecur(  DdManager * dd,  DdNode * (*op)(DdManager *, DdNode **, DdNode **),  DdNode * f,  DdNode * g){    DdNode *res,	   *fv, *fvn, *gv, *gvn,	   *T, *E;    unsigned int ford, gord;    unsigned int index;    DdNode *(*cacheOp)(DdManager *, DdNode *, DdNode *);    /* Check terminal cases. Op may swap f and g to increase the     * cache hit rate.     */    statLine(dd);    res = (*op)(dd,&f,&g);    if (res != NULL) return(res);    /* Check cache. */    cacheOp = (DdNode *(*)(DdManager *, DdNode *, DdNode *)) op;    res = cuddCacheLookup2(dd,cacheOp,f,g);    if (res != NULL) return(res);    /* Recursive step. */    ford = cuddI(dd,f->index);    gord = cuddI(dd,g->index);    if (ford <= gord) {	index = f->index;	fv = cuddT(f);	fvn = cuddE(f);    } else {	index = g->index;	fv = fvn = f;    }    if (gord <= ford) {	gv = cuddT(g);	gvn = cuddE(g);    } else {	gv = gvn = g;    }    T = cuddAddApplyRecur(dd,op,fv,gv);    if (T == NULL) return(NULL);    cuddRef(T);    E = cuddAddApplyRecur(dd,op,fvn,gvn);    if (E == NULL) {	Cudd_RecursiveDeref(dd,T);	return(NULL);    }    cuddRef(E);    res = (T == E) ? T : cuddUniqueInter(dd,(int)index,T,E);    if (res == NULL) {	Cudd_RecursiveDeref(dd, T);	Cudd_RecursiveDeref(dd, E);	return(NULL);    }    cuddDeref(T);    cuddDeref(E);    /* Store result. */    cuddCacheInsert2(dd,cacheOp,f,g,res);    return(res);} /* end of cuddAddApplyRecur */

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

/**Function********************************************************************  Synopsis [Takes the AND of two BDDs and simultaneously abstracts the  variables in cube.]  Description [Takes the AND of two BDDs and simultaneously abstracts  the variables in cube. The variables are existentially abstracted.  Returns a pointer to the result is successful; NULL otherwise.]  SideEffects [None]  SeeAlso     [Cudd_bddAndAbstract]******************************************************************************/DdNode *cuddBddAndAbstractRecur(  DdManager * manager,  DdNode * f,  DdNode * g,  DdNode * cube){    DdNode *F, *ft, *fe, *G, *gt, *ge;    DdNode *one, *zero, *r, *t, *e;    unsigned int topf, topg, topcube, top, index;    statLine(manager);    one = DD_ONE(manager);    zero = Cudd_Not(one);    /* Terminal cases. */    if (f == zero || g == zero || f == Cudd_Not(g)) return(zero);    if (f == one && g == one)	return(one);    if (cube == one) {	return(cuddBddAndRecur(manager, f, g));    }    if (f == one || f == g) {	return(cuddBddExistAbstractRecur(manager, g, cube));    }    if (g == one) {	return(cuddBddExistAbstractRecur(manager, f, cube));    }    /* At this point f, g, and cube are not constant. */    if (f > g) { /* Try to increase cache efficiency. */	DdNode *tmp = f;	f = g;	g = tmp;    }    /* Here we can skip the use of cuddI, because the operands are known    ** to be non-constant.    */    F = Cudd_Regular(f);    G = Cudd_Regular(g);    topf = manager->perm[F->index];    topg = manager->perm[G->index];    top = ddMin(topf, topg);    topcube = manager->perm[cube->index];    while (topcube < top) {	cube = cuddT(cube);	if (cube == one) {	    return(cuddBddAndRecur(manager, f, g));	}	topcube = manager->perm[cube->index];    }    /* Now, topcube >= top. */    /* Check cache. */    if (F->ref != 1 || G->ref != 1) {	r = cuddCacheLookup(manager, DD_BDD_AND_ABSTRACT_TAG, f, g, cube);	if (r != NULL) {	    return(r);	}    }    if (topf == top) {	index = F->index;	ft = cuddT(F);	fe = cuddE(F);	if (Cudd_IsComplement(f)) {	    ft = Cudd_Not(ft);	    fe = Cudd_Not(fe);	}    } else {	index = G->index;	ft = fe = f;    }    if (topg == top) {	gt = cuddT(G);	ge = cuddE(G);	if (Cudd_IsComplement(g)) {	    gt = Cudd_Not(gt);	    ge = Cudd_Not(ge);	}    } else {	gt = ge = g;    }//.........这里部分代码省略.........

/**Function********************************************************************  Synopsis    [Implements the recursive step of Cudd_bddIntersect.]  Description []  SideEffects [None]  SeeAlso     [Cudd_bddIntersect]******************************************************************************/DdNode *cuddBddIntersectRecur(  DdManager * dd,  DdNode * f,  DdNode * g){    DdNode *res;    DdNode *F, *G, *t, *e;    DdNode *fv, *fnv, *gv, *gnv;    DdNode *one, *zero;    unsigned int index, topf, topg;    /* NuSMV: begin add */    abort(); /* NOT USED BY NUSMV */    /* NuSMV: begin end */    statLine(dd);    one = DD_TRUE(dd);    zero = Cudd_Not(one);    /* Terminal cases. */    if (f == zero || g == zero || f == Cudd_Not(g)) return(zero);    if (f == g || g == one) return(f);    if (f == one) return(g);    /* At this point f and g are not constant. */    if (f > g) { DdNode *tmp = f; f = g; g = tmp; }    res = cuddCacheLookup2(dd,Cudd_bddIntersect,f,g);    if (res != NULL) return(res);    /* Find splitting variable. Here we can skip the use of cuddI,    ** because the operands are known to be non-constant.    */    F = Cudd_Regular(f);    topf = dd->perm[F->index];    G = Cudd_Regular(g);    topg = dd->perm[G->index];    /* Compute cofactors. */    if (topf <= topg) {	index = F->index;	fv = cuddT(F);	fnv = cuddE(F);	if (Cudd_IsComplement(f)) {	    fv = Cudd_Not(fv);	    fnv = Cudd_Not(fnv);	}    } else {	index = G->index;	fv = fnv = f;    }    if (topg <= topf) {	gv = cuddT(G);	gnv = cuddE(G);	if (Cudd_IsComplement(g)) {	    gv = Cudd_Not(gv);	    gnv = Cudd_Not(gnv);	}    } else {	gv = gnv = g;    }    /* Compute partial results. */    t = cuddBddIntersectRecur(dd,fv,gv);    if (t == NULL) return(NULL);    cuddRef(t);    if (t != zero) {	e = zero;    } else {	e = cuddBddIntersectRecur(dd,fnv,gnv);	if (e == NULL) {	    Cudd_IterDerefBdd(dd, t);	    return(NULL);	}    }    cuddRef(e);    if (t == e) { /* both equal zero */	res = t;    } else if (Cudd_IsComplement(t)) {	res = cuddUniqueInter(dd,(int)index,Cudd_Not(t),Cudd_Not(e));	if (res == NULL) {	    Cudd_IterDerefBdd(dd, t);	    Cudd_IterDerefBdd(dd, e);	    return(NULL);	}	res = Cudd_Not(res);    } else {//.........这里部分代码省略.........

/**Function********************************************************************  Synopsis [Implements the recursive step of Cudd_bddAnd.]  Description [Implements the recursive step of Cudd_bddAnd by taking  the conjunction of two BDDs.  Returns a pointer to the result is  successful; NULL otherwise.]  SideEffects [None]  SeeAlso     [Cudd_bddAnd]******************************************************************************/DdNode *cuddBddAndRecur(  DdManager * manager,  DdNode * f,  DdNode * g){    DdNode *F, *fv, *fnv, *G, *gv, *gnv;    DdNode *_true, *r, *t, *e;    unsigned int topf, topg, index;    statLine(manager);    _true = DD_TRUE(manager);    /* Terminal cases. */    F = Cudd_Regular(f);    G = Cudd_Regular(g);    if (F == G) {	if (f == g) return(f);	else return(Cudd_Not(_true));    }    if (F == _true) {	if (f == _true) return(g);	else return(f);    }    if (G == _true) {	if (g == _true) return(f);	else return(g);    }    /* At this point f and g are not constant. */    if (f > g) { /* Try to increase cache efficiency. */	DdNode *tmp = f;	f = g;	g = tmp;	F = Cudd_Regular(f);	G = Cudd_Regular(g);    }    /* Check cache. */    if (F->ref != 1 || G->ref != 1) {	r = cuddCacheLookup2(manager, Cudd_bddAnd, f, g);	if (r != NULL) return(r);    }    /* Here we can skip the use of cuddI, because the operands are known    ** to be non-constant.    */    topf = manager->perm[F->index];    topg = manager->perm[G->index];    /* Compute cofactors. */    if (topf <= topg) {	index = F->index;	fv = cuddT(F);	fnv = cuddE(F);	if (Cudd_IsComplement(f)) {	    fv = Cudd_Not(fv);	    fnv = Cudd_Not(fnv);	}    } else {	index = G->index;	fv = fnv = f;    }    if (topg <= topf) {	gv = cuddT(G);	gnv = cuddE(G);	if (Cudd_IsComplement(g)) {	    gv = Cudd_Not(gv);	    gnv = Cudd_Not(gnv);	}    } else {	gv = gnv = g;    }    t = cuddBddAndRecur(manager, fv, gv);    if (t == NULL) return(NULL);    cuddRef(t);    e = cuddBddAndRecur(manager, fnv, gnv);    if (e == NULL) {	Cudd_IterDerefBdd(manager, t);	return(NULL);    }    cuddRef(e);    if (t == e) {//.........这里部分代码省略.........

/**Function********************************************************************  Synopsis    [Determines whether f is less than or equal to g.]  Description [Returns 1 if f is less than or equal to g; 0 otherwise.  No new nodes are created.]  SideEffects [None]  SeeAlso     [Cudd_bddIteConstant Cudd_addEvalConst]******************************************************************************/intCudd_bddLeq(  DdManager * dd,  DdNode * f,  DdNode * g){    DdNode *_true, *_false, *tmp, *F, *fv, *fvn, *gv, *gvn;    unsigned int topf, topg, res;    statLine(dd);    /* Terminal cases and normalization. */    if (f == g) return(1);    if (Cudd_IsComplement(g)) {	/* Special case: if f is regular and g is complemented,	** f(1,...,1) = 1 > 0 = g(1,...,1).	*/	if (!Cudd_IsComplement(f)) return(0);	/* Both are complemented: Swap and complement because	** f <= g <=> g' <= f' and we want the second argument to be regular.	*/	tmp = g;	g = Cudd_Not(f);	f = Cudd_Not(tmp);    } else if (Cudd_IsComplement(f) && g < f) {	tmp = g;	g = Cudd_Not(f);	f = Cudd_Not(tmp);    }    /* Now g is regular and, if f is not regular, f < g. */    _true = DD_TRUE(dd);    if (g == _true) return(1);	/* no need to test against _false */    if (f == _true) return(0);	/* since at this point g != _true */    if (Cudd_Not(f) == g) return(0); /* because neither is constant */    _false = Cudd_Not(_true);    if (f == _false) return(1);    /* Here neither f nor g is constant. */    /* Check cache. */    tmp = cuddCacheLookup2(dd,(DD_CTFP)Cudd_bddLeq,f,g);    if (tmp != NULL) {	return(tmp == _true);    }    /* Compute cofactors. */    F = Cudd_Regular(f);    topf = dd->perm[F->index];    topg = dd->perm[g->index];    if (topf <= topg) {	fv = cuddT(F); fvn = cuddE(F);	if (f != F) {	    fv = Cudd_Not(fv);	    fvn = Cudd_Not(fvn);	}    } else {	fv = fvn = f;    }    if (topg <= topf) {	gv = cuddT(g); gvn = cuddE(g);    } else {	gv = gvn = g;    }    /* Recursive calls. Since we want to maximize the probability of    ** the special case f(1,...,1) > g(1,...,1), we consider the negative    ** cofactors first. Indeed, the complementation parity of the positive    ** cofactors is the same as the one of the parent functions.    */    res = Cudd_bddLeq(dd,fvn,gvn) && Cudd_bddLeq(dd,fv,gv);    /* Store result in cache and return. */    cuddCacheInsert2(dd,(DD_CTFP)Cudd_bddLeq,f,g,(res ? _true : _false));    return(res);} /* end of Cudd_bddLeq */

/**Function********************************************************************  Synopsis    [Implements the recursive step of Cudd_bddIte.]  Description [Implements the recursive step of Cudd_bddIte. Returns a  pointer to the resulting BDD. NULL if the intermediate result blows  up or if reordering occurs.]  SideEffects [None]  SeeAlso     []******************************************************************************/DdNode *cuddBddIteRecur(  DdManager * dd,  DdNode * f,  DdNode * g,  DdNode * h){    DdNode	 *_true, *_false, *res;    DdNode	 *r, *Fv, *Fnv, *Gv, *Gnv, *H, *Hv, *Hnv, *t, *e;    unsigned int topf, topg, toph, v;    int		 index = 0;    int		 comple;    statLine(dd);    /* Terminal cases. */    /* _True variable cases. */    if (f == (_true = DD_TRUE(dd))) 	/* ITE(TRUE,G,H) = G */	return(g);        if (f == (_false = Cudd_Not(_true))) 	/* ITE(FALSE,G,H) = H */	return(h);        /* From now on, f is known not to be a constant. */    if (g == _true || f == g) {	/* ITE(F,F,H) = ITE(F,TRUE,H) = F + H */	if (h == _false) {	/* ITE(F,TRUE,FALSE) = F */	    return(f);	} else {	    res = cuddBddAndRecur(dd,Cudd_Not(f),Cudd_Not(h));	    return(Cudd_NotCond(res,res != NULL));	}    } else if (g == _false || f == Cudd_Not(g)) { /* ITE(F,!F,H) = ITE(F,FALSE,H) = !F * H */	if (h == _true) {		/* ITE(F,FALSE,TRUE) = !F */	    return(Cudd_Not(f));	} else {	    res = cuddBddAndRecur(dd,Cudd_Not(f),h);	    return(res);	}    }    if (h == _false || f == h) {    /* ITE(F,G,F) = ITE(F,G,FALSE) = F * G */	res = cuddBddAndRecur(dd,f,g);	return(res);    } else if (h == _true || f == Cudd_Not(h)) { /* ITE(F,G,!F) = ITE(F,G,TRUE) = !F + G */	res = cuddBddAndRecur(dd,f,Cudd_Not(g));	return(Cudd_NotCond(res,res != NULL));    }    /* Check remaining _true variable case. */    if (g == h) { 		/* ITE(F,G,G) = G */	return(g);    } else if (g == Cudd_Not(h)) { /* ITE(F,G,!G) = F <-> G */	res = cuddBddXorRecur(dd,f,h);	return(res);    }        /* From here, there are no constants. */    comple = bddVarToCanonicalSimple(dd, &f, &g, &h, &topf, &topg, &toph);    /* f & g are now regular pointers */    v = ddMin(topg, toph);    /* A shortcut: ITE(F,G,H) = (v,G,H) if F = (v,TRUE,FALSE), v < top(G,H). */    if (topf < v && cuddT(f) == _true && cuddE(f) == _false) {	r = cuddUniqueInter(dd, (int) f->index, g, h);	return(Cudd_NotCond(r,comple && r != NULL));    }    /* Check cache. */    r = cuddCacheLookup(dd, DD_BDD_ITE_TAG, f, g, h);    if (r != NULL) {	return(Cudd_NotCond(r,comple));    }    /* Compute cofactors. */    if (topf <= v) {	v = ddMin(topf, v);	/* v = top_var(F,G,H) */	index = f->index;	Fv = cuddT(f); Fnv = cuddE(f);    } else {	Fv = Fnv = f;    }    if (topg == v) {	index = g->index;	Gv = cuddT(g); Gnv = cuddE(g);    } else {	Gv = Gnv = g;//.........这里部分代码省略.........

/**Function********************************************************************  Synopsis    [Implements ITEconstant(f,g,h).]  Description [Implements ITEconstant(f,g,h). Returns a pointer to the  resulting BDD (which may or may not be constant) or DD_NON_CONSTANT.  No new nodes are created.]  SideEffects [None]  SeeAlso     [Cudd_bddIte Cudd_bddIntersect Cudd_bddLeq Cudd_addIteConstant]******************************************************************************/DdNode *Cudd_bddIteConstant(  DdManager * dd,  DdNode * f,  DdNode * g,  DdNode * h){    DdNode	 *r, *Fv, *Fnv, *Gv, *Gnv, *H, *Hv, *Hnv, *t, *e;    DdNode	 *one = DD_TRUE(dd);    DdNode	 *zero = Cudd_Not(one);    int		 comple;    unsigned int topf, topg, toph, v;    /* NuSMV: begin add */    abort(); /* NOT USED BY NUSMV */    /* NuSMV: begin end */    statLine(dd);    /* Trivial cases. */    if (f == one) 			/* ITE(TRUE,G,H) => G */	return(g);        if (f == zero)			/* ITE(FALSE,G,H) => H */	return(h);        /* f now not a constant. */    bddVarToConst(f, &g, &h, one);	/* possibly convert g or h */					/* to constants */    if (g == h) 			/* ITE(F,G,G) => G */	return(g);    if (Cudd_IsConstant(g) && Cudd_IsConstant(h)) 	return(DD_NON_CONSTANT);	/* ITE(F,1,0) or ITE(F,0,1) */					/* => DD_NON_CONSTANT */        if (g == Cudd_Not(h))	return(DD_NON_CONSTANT);	/* ITE(F,G,G') => DD_NON_CONSTANT */					/* if F != G and F != G' */        comple = bddVarToCanonical(dd, &f, &g, &h, &topf, &topg, &toph);    /* Cache lookup. */    r = cuddConstantLookup(dd, DD_BDD_ITE_CONSTANT_TAG, f, g, h);    if (r != NULL) {	return(Cudd_NotCond(r,comple && r != DD_NON_CONSTANT));    }    v = ddMin(topg, toph);    /* ITE(F,G,H) = (v,G,H) (non constant) if F = (v,1,0), v < top(G,H). */    if (topf < v && cuddT(f) == one && cuddE(f) == zero) {	return(DD_NON_CONSTANT);    }    /* Compute cofactors. */    if (topf <= v) {	v = ddMin(topf, v);		/* v = top_var(F,G,H) */	Fv = cuddT(f); Fnv = cuddE(f);    } else {	Fv = Fnv = f;    }    if (topg == v) {	Gv = cuddT(g); Gnv = cuddE(g);    } else {	Gv = Gnv = g;    }    if (toph == v) {	H = Cudd_Regular(h);	Hv = cuddT(H); Hnv = cuddE(H);	if (Cudd_IsComplement(h)) {	    Hv = Cudd_Not(Hv);	    Hnv = Cudd_Not(Hnv);	}    } else {	Hv = Hnv = h;    }    /* Recursion. */    t = Cudd_bddIteConstant(dd, Fv, Gv, Hv);    if (t == DD_NON_CONSTANT || !Cudd_IsConstant(t)) {	cuddCacheInsert(dd, DD_BDD_ITE_CONSTANT_TAG, f, g, h, DD_NON_CONSTANT);	return(DD_NON_CONSTANT);    }    e = Cudd_bddIteConstant(dd, Fnv, Gnv, Hnv);//.........这里部分代码省略.........

/**Function********************************************************************  Synopsis    [Performs the recursive step of Cudd_addOuterSum.]  Description [Performs the recursive step of Cudd_addOuterSum.  Returns a pointer to the result if successful; NULL otherwise.]  SideEffects [None]  SeeAlso     []******************************************************************************/static DdNode *cuddAddOuterSumRecur(  DdManager *dd,  DdNode *M,  DdNode *r,  DdNode *c){    DdNode *P, *R, *Mt, *Me, *rt, *re, *ct, *ce, *Rt, *Re;    int topM, topc, topr;    int v, index;    statLine(dd);    /* Check special cases. */    if (r == DD_PLUS_INFINITY(dd) || c == DD_PLUS_INFINITY(dd)) return(M);     if (cuddIsConstant(c) && cuddIsConstant(r)) {	R = cuddUniqueConst(dd,Cudd_V(c)+Cudd_V(r));	cuddRef(R);	if (cuddIsConstant(M)) {	    if (cuddV(R) <= cuddV(M)) {		cuddDeref(R);	        return(R);	    } else {	        Cudd_RecursiveDeref(dd,R);       		return(M);	    }	} else {	    P = Cudd_addApply(dd,Cudd_addMinimum,R,M);	    cuddRef(P);	    Cudd_RecursiveDeref(dd,R);	    cuddDeref(P);	    return(P);	}    }    /* Check the cache. */    R = cuddCacheLookup(dd,DD_ADD_OUT_SUM_TAG,M,r,c);    if (R != NULL) return(R);    topM = cuddI(dd,M->index); topr = cuddI(dd,r->index);    topc = cuddI(dd,c->index);    v = ddMin(topM,ddMin(topr,topc));    /* Compute cofactors. */    if (topM == v) { Mt = cuddT(M); Me = cuddE(M); } else { Mt = Me = M; }    if (topr == v) { rt = cuddT(r); re = cuddE(r); } else { rt = re = r; }    if (topc == v) { ct = cuddT(c); ce = cuddE(c); } else { ct = ce = c; }    /* Recursively solve. */    Rt = cuddAddOuterSumRecur(dd,Mt,rt,ct);    if (Rt == NULL) return(NULL);    cuddRef(Rt);    Re = cuddAddOuterSumRecur(dd,Me,re,ce);    if (Re == NULL) {	Cudd_RecursiveDeref(dd, Rt);	return(NULL);    }    cuddRef(Re);    index = dd->invperm[v];    R = (Rt == Re) ? Rt : cuddUniqueInter(dd,index,Rt,Re);    if (R == NULL) {	Cudd_RecursiveDeref(dd, Rt);	Cudd_RecursiveDeref(dd, Re);	return(NULL);    }    cuddDeref(Rt);    cuddDeref(Re);    /* Store the result in the cache. */    cuddCacheInsert(dd,DD_ADD_OUT_SUM_TAG,M,r,c,R);    return(R);} /* end of cuddAddOuterSumRecur */

/**Function********************************************************************  Synopsis    [Performs the recursive step of Cudd_addTriangle.]  Description [Performs the recursive step of Cudd_addTriangle. Returns  a pointer to the result if successful; NULL otherwise.]  SideEffects [None]******************************************************************************/static DdNode *addTriangleRecur(  DdManager * dd,  DdNode * f,  DdNode * g,  int * vars,  DdNode *cube){    DdNode *fv, *fvn, *gv, *gvn, *t, *e, *res;    CUDD_VALUE_TYPE value;    int top, topf, topg, index;    statLine(dd);    if (f == DD_PLUS_INFINITY(dd) || g == DD_PLUS_INFINITY(dd)) {	return(DD_PLUS_INFINITY(dd));    }    if (cuddIsConstant(f) && cuddIsConstant(g)) {	value = cuddV(f) + cuddV(g);	res = cuddUniqueConst(dd, value);	return(res);    }    if (f < g) {	DdNode *tmp = f;	f = g;	g = tmp;    }    if (f->ref != 1 || g->ref != 1) {	res = cuddCacheLookup(dd, DD_ADD_TRIANGLE_TAG, f, g, cube);	if (res != NULL) {	    return(res);	}    }    topf = cuddI(dd,f->index); topg = cuddI(dd,g->index);    top = ddMin(topf,topg);    if (top == topf) {fv = cuddT(f); fvn = cuddE(f);} else {fv = fvn = f;}    if (top == topg) {gv = cuddT(g); gvn = cuddE(g);} else {gv = gvn = g;}    t = addTriangleRecur(dd, fv, gv, vars, cube);    if (t == NULL) return(NULL);    cuddRef(t);    e = addTriangleRecur(dd, fvn, gvn, vars, cube);    if (e == NULL) {	Cudd_RecursiveDeref(dd, t);	return(NULL);    }    cuddRef(e);    index = dd->invperm[top];    if (vars[index] < 0) {	res = (t == e) ? t : cuddUniqueInter(dd,index,t,e);	if (res == NULL) {	    Cudd_RecursiveDeref(dd, t);	    Cudd_RecursiveDeref(dd, e);	    return(NULL);	}	cuddDeref(t);	cuddDeref(e);    } else {	res = cuddAddApplyRecur(dd,Cudd_addMinimum,t,e);	if (res == NULL) {	    Cudd_RecursiveDeref(dd, t);	    Cudd_RecursiveDeref(dd, e);	    return(NULL);	}	cuddRef(res);	Cudd_RecursiveDeref(dd, t);	Cudd_RecursiveDeref(dd, e);	cuddDeref(res);    }    if (f->ref != 1 || g->ref != 1) {	cuddCacheInsert(dd, DD_ADD_TRIANGLE_TAG, f, g, cube, res);    }    return(res);} /* end of addTriangleRecur */

/**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_zddDivideF.]  Description []  SideEffects [None]  SeeAlso     [Cudd_zddDivideF]******************************************************************************/DdNode  *cuddZddDivideF(  DdManager * dd,  DdNode * f,  DdNode * g){    int         v;    DdNode      *one = DD_ONE(dd);    DdNode      *zero = DD_ZERO(dd);    DdNode      *f0, *f1, *g0, *g1;    DdNode      *q, *r, *tmp;    int         flag;    statLine(dd);    if (g == one)        return(f);    if (f == zero || f == one)        return(zero);    if (f == g)        return(one);    /* Check cache. */    r = cuddCacheLookup2Zdd(dd, cuddZddDivideF, f, g);    if (r)        return(r);    v = g->index;    flag = cuddZddGetCofactors2(dd, f, v, &f1, &f0);    if (flag == 1)        return(NULL);    Cudd_Ref(f1);    Cudd_Ref(f0);    flag = cuddZddGetCofactors2(dd, g, v, &g1, &g0);    /* g1 != zero */    if (flag == 1) {        Cudd_RecursiveDerefZdd(dd, f1);        Cudd_RecursiveDerefZdd(dd, f0);        return(NULL);    }    Cudd_Ref(g1);    Cudd_Ref(g0);    r = cuddZddDivideF(dd, f1, g1);    if (r == NULL) {        Cudd_RecursiveDerefZdd(dd, f1);        Cudd_RecursiveDerefZdd(dd, f0);        Cudd_RecursiveDerefZdd(dd, g1);        Cudd_RecursiveDerefZdd(dd, g0);        return(NULL);    }    Cudd_Ref(r);    if (r != zero && g0 != zero) {        tmp = r;        q = cuddZddDivideF(dd, f0, g0);        if (q == NULL) {            Cudd_RecursiveDerefZdd(dd, f1);            Cudd_RecursiveDerefZdd(dd, f0);            Cudd_RecursiveDerefZdd(dd, g1);            Cudd_RecursiveDerefZdd(dd, g0);            return(NULL);        }        Cudd_Ref(q);        r = cuddZddIntersect(dd, r, q);        if (r == NULL) {            Cudd_RecursiveDerefZdd(dd, f1);            Cudd_RecursiveDerefZdd(dd, f0);            Cudd_RecursiveDerefZdd(dd, g1);            Cudd_RecursiveDerefZdd(dd, g0);            Cudd_RecursiveDerefZdd(dd, q);            return(NULL);        }        Cudd_Ref(r);        Cudd_RecursiveDerefZdd(dd, q);        Cudd_RecursiveDerefZdd(dd, tmp);    }    Cudd_RecursiveDerefZdd(dd, f1);    Cudd_RecursiveDerefZdd(dd, f0);    Cudd_RecursiveDerefZdd(dd, g1);    Cudd_RecursiveDerefZdd(dd, g0);        cuddCacheInsert2(dd, cuddZddDivideF, f, g, r);    Cudd_Deref(r);    return(r);} /* end of cuddZddDivideF */

/**Function********************************************************************  Synopsis    [Performs the recursive step of Cudd_zddIte.]  Description []  SideEffects [None]  SeeAlso     []******************************************************************************/DdNode *cuddZddIte(  DdManager * dd,  DdNode * f,  DdNode * g,  DdNode * h){    DdNode *tautology, *empty;    DdNode *r,*Gv,*Gvn,*Hv,*Hvn,*t,*e;    unsigned int topf,topg,toph,v,top;    int index;    statLine(dd);    /* Trivial cases. */    /* One variable cases. */    if (f == (empty = DD_ZERO(dd))) {	/* ITE(0,G,H) = H */	return(h);    }    topf = cuddIZ(dd,f->index);    topg = cuddIZ(dd,g->index);    toph = cuddIZ(dd,h->index);    v = ddMin(topg,toph);    top  = ddMin(topf,v);    tautology = (top == CUDD_MAXINDEX) ? DD_ONE(dd) : dd->univ[top];    if (f == tautology) {			/* ITE(1,G,H) = G */    	return(g);    }    /* From now on, f is known to not be a constant. */    zddVarToConst(f,&g,&h,tautology,empty);    /* Check remaining one variable cases. */    if (g == h) {			/* ITE(F,G,G) = G */	return(g);    }    if (g == tautology) {			/* ITE(F,1,0) = F */	if (h == empty) return(f);    }    /* Check cache. */    r = cuddCacheLookupZdd(dd,DD_ZDD_ITE_TAG,f,g,h);    if (r != NULL) {	return(r);    }    /* Recompute these because they may have changed in zddVarToConst. */    topg = cuddIZ(dd,g->index);    toph = cuddIZ(dd,h->index);    v = ddMin(topg,toph);    if (topf < v) {	r = cuddZddIte(dd,cuddE(f),g,h);	if (r == NULL) return(NULL);    } else if (topf > v) {	if (topg > v) {	    Gvn = g;	    index = h->index;	} else {	    Gvn = cuddE(g);	    index = g->index;	}	if (toph > v) {	    Hv = empty; Hvn = h;	} else {	    Hv = cuddT(h); Hvn = cuddE(h);	}	e = cuddZddIte(dd,f,Gvn,Hvn);	if (e == NULL) return(NULL);	cuddRef(e);	r = cuddZddGetNode(dd,index,Hv,e);	if (r == NULL) {	    Cudd_RecursiveDerefZdd(dd,e);	    return(NULL);	}	cuddDeref(e);    } else {	index = f->index;	if (topg > v) {	    Gv = empty; Gvn = g;	} else {	    Gv = cuddT(g); Gvn = cuddE(g);	}	if (toph > v) {	    Hv = empty; Hvn = h;	} else {	    Hv = cuddT(h); Hvn = cuddE(h);	}//.........这里部分代码省略.........

/**Function********************************************************************  Synopsis [Performs the recursive step of Cudd_zddProduct.]  Description []  SideEffects [None]  SeeAlso     [Cudd_zddProduct]******************************************************************************/DdNode  *cuddZddProduct(  DdManager * dd,  DdNode * f,  DdNode * g){    int         v, top_f, top_g;    DdNode      *tmp, *term1, *term2, *term3;    DdNode      *f0, *f1, *fd, *g0, *g1, *gd;    DdNode      *R0, *R1, *Rd, *N0, *N1;    DdNode      *r;    DdNode      *one = DD_ONE(dd);    DdNode      *zero = DD_ZERO(dd);    int         flag;    int         pv, nv;    statLine(dd);    if (f == zero || g == zero)        return(zero);    if (f == one)        return(g);    if (g == one)        return(f);    top_f = dd->permZ[f->index];    top_g = dd->permZ[g->index];    if (top_f > top_g)        return(cuddZddProduct(dd, g, f));    /* Check cache */    r = cuddCacheLookup2Zdd(dd, cuddZddProduct, f, g);    if (r)        return(r);    v = f->index;       /* either yi or zi */    flag = cuddZddGetCofactors3(dd, f, v, &f1, &f0, &fd);    if (flag == 1)        return(NULL);    Cudd_Ref(f1);    Cudd_Ref(f0);    Cudd_Ref(fd);    flag = cuddZddGetCofactors3(dd, g, v, &g1, &g0, &gd);    if (flag == 1) {        Cudd_RecursiveDerefZdd(dd, f1);        Cudd_RecursiveDerefZdd(dd, f0);        Cudd_RecursiveDerefZdd(dd, fd);        return(NULL);    }    Cudd_Ref(g1);    Cudd_Ref(g0);    Cudd_Ref(gd);    pv = cuddZddGetPosVarIndex(dd, v);    nv = cuddZddGetNegVarIndex(dd, v);    Rd = cuddZddProduct(dd, fd, gd);    if (Rd == NULL) {        Cudd_RecursiveDerefZdd(dd, f1);        Cudd_RecursiveDerefZdd(dd, f0);        Cudd_RecursiveDerefZdd(dd, fd);        Cudd_RecursiveDerefZdd(dd, g1);        Cudd_RecursiveDerefZdd(dd, g0);        Cudd_RecursiveDerefZdd(dd, gd);        return(NULL);    }    Cudd_Ref(Rd);    term1 = cuddZddProduct(dd, f0, g0);    if (term1 == NULL) {        Cudd_RecursiveDerefZdd(dd, f1);        Cudd_RecursiveDerefZdd(dd, f0);        Cudd_RecursiveDerefZdd(dd, fd);        Cudd_RecursiveDerefZdd(dd, g1);        Cudd_RecursiveDerefZdd(dd, g0);        Cudd_RecursiveDerefZdd(dd, gd);        Cudd_RecursiveDerefZdd(dd, Rd);        return(NULL);    }    Cudd_Ref(term1);    term2 = cuddZddProduct(dd, f0, gd);    if (term2 == NULL) {        Cudd_RecursiveDerefZdd(dd, f1);        Cudd_RecursiveDerefZdd(dd, f0);        Cudd_RecursiveDerefZdd(dd, fd);        Cudd_RecursiveDerefZdd(dd, g1);        Cudd_RecursiveDerefZdd(dd, g0);        Cudd_RecursiveDerefZdd(dd, gd);        Cudd_RecursiveDerefZdd(dd, Rd);        Cudd_RecursiveDerefZdd(dd, term1);//.........这里部分代码省略.........

/**Function********************************************************************  Synopsis    [Performs the recursive step of Cudd_Cofactor.]  Description [Performs the recursive step of Cudd_Cofactor. Returns a  pointer to the cofactor if successful; NULL otherwise.]  SideEffects [None]  SeeAlso     [Cudd_Cofactor]******************************************************************************/DdNode *cuddCofactorRecur(  DdManager * dd,  DdNode * f,  DdNode * g){    DdNode *one,*zero,*F,*G,*g1,*g0,*f1,*f0,*t,*e,*r;    unsigned int topf,topg;    int comple;    statLine(dd);    F = Cudd_Regular(f);    if (cuddIsConstant(F)) return(f);    one = DD_ONE(dd);    /* The invariant g != 0 is true on entry to this procedure and is    ** recursively maintained by it. Therefore it suffices to test g    ** against one to make sure it is not constant.    */    if (g == one) return(f);    /* From now on, f and g are known not to be constants. */    comple = f != F;    r = cuddCacheLookup2(dd,Cudd_Cofactor,F,g);    if (r != NULL) {	return(Cudd_NotCond(r,comple));    }    topf = dd->perm[F->index];    G = Cudd_Regular(g);    topg = dd->perm[G->index];    /* We take the cofactors of F because we are going to rely on    ** the fact that the cofactors of the complement are the complements    ** of the cofactors to better utilize the cache. Variable comple    ** remembers whether we have to complement the result or not.    */    if (topf <= topg) {	f1 = cuddT(F); f0 = cuddE(F);    } else {	f1 = f0 = F;    }    if (topg <= topf) {	g1 = cuddT(G); g0 = cuddE(G);	if (g != G) { g1 = Cudd_Not(g1); g0 = Cudd_Not(g0); }    } else {	g1 = g0 = g;    }    zero = Cudd_Not(one);    if (topf >= topg) {	if (g0 == zero || g0 == DD_ZERO(dd)) {	    r = cuddCofactorRecur(dd, f1, g1);	} else if (g1 == zero || g1 == DD_ZERO(dd)) {	    r = cuddCofactorRecur(dd, f0, g0);	} else {	    (void) fprintf(dd->out,			   "Cudd_Cofactor: Invalid restriction 2/n");	    dd->errorCode = CUDD_INVALID_ARG;	    return(NULL);	}	if (r == NULL) return(NULL);    } else /* if (topf < topg) */ {	t = cuddCofactorRecur(dd, f1, g);	if (t == NULL) return(NULL);    	cuddRef(t);    	e = cuddCofactorRecur(dd, f0, g);	if (e == NULL) {	    Cudd_RecursiveDeref(dd, t);	    return(NULL);	}	cuddRef(e);	if (t == e) {	    r = t;	} else if (Cudd_IsComplement(t)) {	    r = cuddUniqueInter(dd,(int)F->index,Cudd_Not(t),Cudd_Not(e));	    if (r != NULL)		r = Cudd_Not(r);	} else {	    r = cuddUniqueInter(dd,(int)F->index,t,e);	}	if (r == NULL) {	    Cudd_RecursiveDeref(dd ,e);	    Cudd_RecursiveDeref(dd ,t);	    return(NULL);	}//.........这里部分代码省略.........

/**Function********************************************************************  Synopsis    [Performs the recursive step of Cudd_zddUnateProduct.]  Description []  SideEffects [None]  SeeAlso     [Cudd_zddUnateProduct]******************************************************************************/DdNode  *cuddZddUnateProduct(  DdManager * dd,  DdNode * f,  DdNode * g){    int         v, top_f, top_g;    DdNode      *term1, *term2, *term3, *term4;    DdNode      *sum1, *sum2;    DdNode      *f0, *f1, *g0, *g1;    DdNode      *r;    DdNode      *one = DD_ONE(dd);    DdNode      *zero = DD_ZERO(dd);    int         flag;    statLine(dd);    if (f == zero || g == zero)        return(zero);    if (f == one)        return(g);    if (g == one)        return(f);    top_f = dd->permZ[f->index];    top_g = dd->permZ[g->index];    if (top_f > top_g)        return(cuddZddUnateProduct(dd, g, f));    /* Check cache */    r = cuddCacheLookup2Zdd(dd, cuddZddUnateProduct, f, g);    if (r)        return(r);    v = f->index;       /* either yi or zi */    flag = cuddZddGetCofactors2(dd, f, v, &f1, &f0);    if (flag == 1)        return(NULL);    Cudd_Ref(f1);    Cudd_Ref(f0);    flag = cuddZddGetCofactors2(dd, g, v, &g1, &g0);    if (flag == 1) {        Cudd_RecursiveDerefZdd(dd, f1);        Cudd_RecursiveDerefZdd(dd, f0);        return(NULL);    }    Cudd_Ref(g1);    Cudd_Ref(g0);    term1 = cuddZddUnateProduct(dd, f1, g1);    if (term1 == NULL) {        Cudd_RecursiveDerefZdd(dd, f1);        Cudd_RecursiveDerefZdd(dd, f0);        Cudd_RecursiveDerefZdd(dd, g1);        Cudd_RecursiveDerefZdd(dd, g0);        return(NULL);    }    Cudd_Ref(term1);    term2 = cuddZddUnateProduct(dd, f1, g0);    if (term2 == NULL) {        Cudd_RecursiveDerefZdd(dd, f1);        Cudd_RecursiveDerefZdd(dd, f0);        Cudd_RecursiveDerefZdd(dd, g1);        Cudd_RecursiveDerefZdd(dd, g0);        Cudd_RecursiveDerefZdd(dd, term1);        return(NULL);    }    Cudd_Ref(term2);    term3 = cuddZddUnateProduct(dd, f0, g1);    if (term3 == NULL) {        Cudd_RecursiveDerefZdd(dd, f1);        Cudd_RecursiveDerefZdd(dd, f0);        Cudd_RecursiveDerefZdd(dd, g1);        Cudd_RecursiveDerefZdd(dd, g0);        Cudd_RecursiveDerefZdd(dd, term1);        Cudd_RecursiveDerefZdd(dd, term2);        return(NULL);    }    Cudd_Ref(term3);    term4 = cuddZddUnateProduct(dd, f0, g0);    if (term4 == NULL) {        Cudd_RecursiveDerefZdd(dd, f1);        Cudd_RecursiveDerefZdd(dd, f0);        Cudd_RecursiveDerefZdd(dd, g1);        Cudd_RecursiveDerefZdd(dd, g0);        Cudd_RecursiveDerefZdd(dd, term1);        Cudd_RecursiveDerefZdd(dd, term2);        Cudd_RecursiveDerefZdd(dd, term3);        return(NULL);//.........这里部分代码省略.........

/**Function********************************************************************  Synopsis [Implements the recursive step of Cudd_bddClippingAnd.]  Description [Implements the recursive step of Cudd_bddClippingAnd by taking  the conjunction of two BDDs.  Returns a pointer to the result is  successful; NULL otherwise.]  SideEffects [None]  SeeAlso     [cuddBddClippingAnd]******************************************************************************/static DdNode *cuddBddClippingAndRecur(  DdManager * manager,  DdNode * f,  DdNode * g,  int  distance,  int  direction){    DdNode *F, *ft, *fe, *G, *gt, *ge;    DdNode *one, *zero, *r, *t, *e;    unsigned int topf, topg, index;    DD_CTFP cacheOp;    statLine(manager);    one = DD_ONE(manager);    zero = Cudd_Not(one);    /* Terminal cases. */    if (f == zero || g == zero || f == Cudd_Not(g)) return(zero);    if (f == g || g == one) return(f);    if (f == one) return(g);    if (distance == 0) {	/* One last attempt at returning the right result. We sort of	** cheat by calling Cudd_bddLeq. */	if (Cudd_bddLeq(manager,f,g)) return(f);	if (Cudd_bddLeq(manager,g,f)) return(g);	if (direction == 1) {	    if (Cudd_bddLeq(manager,f,Cudd_Not(g)) ||		Cudd_bddLeq(manager,g,Cudd_Not(f))) return(zero);	}	return(Cudd_NotCond(one,(direction == 0)));    }    /* At this point f and g are not constant. */    distance--;    /* Check cache. Try to increase cache efficiency by sorting the    ** pointers. */    if (f > g) {	DdNode *tmp = f;	f = g; g = tmp;    }    F = Cudd_Regular(f);    G = Cudd_Regular(g);    cacheOp = (DD_CTFP)	(direction ? Cudd_bddClippingAnd : cuddBddClippingAnd);    if (F->ref != 1 || G->ref != 1) {	r = cuddCacheLookup2(manager, cacheOp, f, g);	if (r != NULL) return(r);    }    /* Here we can skip the use of cuddI, because the operands are known    ** to be non-constant.    */    topf = manager->perm[F->index];    topg = manager->perm[G->index];    /* Compute cofactors. */    if (topf <= topg) {	index = F->index;	ft = cuddT(F);	fe = cuddE(F);	if (Cudd_IsComplement(f)) {	    ft = Cudd_Not(ft);	    fe = Cudd_Not(fe);	}    } else {	index = G->index;	ft = fe = f;    }    if (topg <= topf) {	gt = cuddT(G);	ge = cuddE(G);	if (Cudd_IsComplement(g)) {	    gt = Cudd_Not(gt);	    ge = Cudd_Not(ge);	}    } else {	gt = ge = g;    }    t = cuddBddClippingAndRecur(manager, ft, gt, distance, direction);    if (t == NULL) return(NULL);    cuddRef(t);    e = cuddBddClippingAndRecur(manager, fe, ge, distance, direction);    if (e == NULL) {//.........这里部分代码省略.........

/**Function********************************************************************  Synopsis    [Performs the recursive step of Cudd_zddWeakDiv.]  Description []  SideEffects [None]  SeeAlso     [Cudd_zddWeakDiv]******************************************************************************/DdNode  *cuddZddWeakDiv(  DdManager * dd,  DdNode * f,  DdNode * g){    int         v;    DdNode      *one = DD_ONE(dd);    DdNode      *zero = DD_ZERO(dd);    DdNode      *f0, *f1, *fd, *g0, *g1, *gd;    DdNode      *q, *tmp;    DdNode      *r;    int         flag;    statLine(dd);    if (g == one)        return(f);    if (f == zero || f == one)        return(zero);    if (f == g)        return(one);    /* Check cache. */    r = cuddCacheLookup2Zdd(dd, cuddZddWeakDiv, f, g);    if (r)        return(r);    v = g->index;    flag = cuddZddGetCofactors3(dd, f, v, &f1, &f0, &fd);    if (flag == 1)        return(NULL);    Cudd_Ref(f1);    Cudd_Ref(f0);    Cudd_Ref(fd);    flag = cuddZddGetCofactors3(dd, g, v, &g1, &g0, &gd);    if (flag == 1) {        Cudd_RecursiveDerefZdd(dd, f1);        Cudd_RecursiveDerefZdd(dd, f0);        Cudd_RecursiveDerefZdd(dd, fd);        return(NULL);    }    Cudd_Ref(g1);    Cudd_Ref(g0);    Cudd_Ref(gd);    q = g;    if (g0 != zero) {        q = cuddZddWeakDiv(dd, f0, g0);        if (q == NULL) {            Cudd_RecursiveDerefZdd(dd, f1);            Cudd_RecursiveDerefZdd(dd, f0);            Cudd_RecursiveDerefZdd(dd, fd);            Cudd_RecursiveDerefZdd(dd, g1);            Cudd_RecursiveDerefZdd(dd, g0);            Cudd_RecursiveDerefZdd(dd, gd);            return(NULL);        }        Cudd_Ref(q);    }    else        Cudd_Ref(q);    Cudd_RecursiveDerefZdd(dd, f0);    Cudd_RecursiveDerefZdd(dd, g0);    if (q == zero) {        Cudd_RecursiveDerefZdd(dd, f1);        Cudd_RecursiveDerefZdd(dd, g1);        Cudd_RecursiveDerefZdd(dd, fd);        Cudd_RecursiveDerefZdd(dd, gd);        cuddCacheInsert2(dd, cuddZddWeakDiv, f, g, zero);        Cudd_Deref(q);        return(zero);    }    if (g1 != zero) {        Cudd_RecursiveDerefZdd(dd, q);        tmp = cuddZddWeakDiv(dd, f1, g1);        if (tmp == NULL) {            Cudd_RecursiveDerefZdd(dd, f1);            Cudd_RecursiveDerefZdd(dd, g1);            Cudd_RecursiveDerefZdd(dd, fd);            Cudd_RecursiveDerefZdd(dd, gd);            return(NULL);        }        Cudd_Ref(tmp);        Cudd_RecursiveDerefZdd(dd, f1);        Cudd_RecursiveDerefZdd(dd, g1);//.........这里部分代码省略.........

/**Function********************************************************************  Synopsis    [Implements the recursive step of Cudd_SplitSet.]  Description [Implements the recursive step of Cudd_SplitSet. The  procedure recursively traverses the BDD and checks to see if any  node satisfies the minterm requirements as specified by 'n'. At any  node X, n is compared to the number of minterms in the onset of X's  children. If either of the child nodes have exactly n minterms, then  that node is returned; else, if n is greater than the onset of one  of the child nodes, that node is retained and the difference in the  number of minterms is extracted from the other child. In case n  minterms can be extracted from constant 1, the algorithm returns the  result with at most log(n) nodes.]  SideEffects [The array 'varSeen' is updated at every recursive call  to set the variables traversed by the procedure.]  SeeAlso     []******************************************************************************/DdNode*cuddSplitSetRecur(  DdManager * manager,  st_table * mtable,  int * varSeen,  DdNode * p,  double  n,  double  max,  int  index){    DdNode *one, *zero, *N, *Nv;    DdNode *Nnv, *q, *r, *v;    DdNode *result;    double *dummy, numT, numE;    int variable, positive;      statLine(manager);    one = DD_ONE(manager);    zero = Cudd_Not(one);    /* If p is constant, extract n minterms from constant 1.  The procedure by    ** construction guarantees that minterms will not be extracted from    ** constant 0.    */    if (Cudd_IsConstant(p)) {	q = selectMintermsFromUniverse(manager,varSeen,n);	return(q);    }    N = Cudd_Regular(p);    /* Set variable as seen. */    variable = N->index;    varSeen[manager->invperm[variable]] = -1;    Nv = cuddT(N);    Nnv = cuddE(N);    if (Cudd_IsComplement(p)) {	Nv = Cudd_Not(Nv);	Nnv = Cudd_Not(Nnv);    }    /* If both the children of 'p' are constants, extract n minterms from a    ** constant node.    */    if (Cudd_IsConstant(Nv) && Cudd_IsConstant(Nnv)) {	q = selectMintermsFromUniverse(manager,varSeen,n);	if (q == NULL) {	    return(NULL);	}	cuddRef(q);	r = cuddBddAndRecur(manager,p,q);	if (r == NULL) {	    Cudd_RecursiveDeref(manager,q);	    return(NULL);	}	cuddRef(r);	Cudd_RecursiveDeref(manager,q);	cuddDeref(r);	return(r);    }      /* Lookup the # of minterms in the onset of the node from the table. */    if (!Cudd_IsConstant(Nv)) {	st_lookup(mtable,(char *)Nv, (char **)&dummy);	numT = *dummy/(2*(1<<index));    } else if (Nv == one) {	numT = max/(2*(1<<index));    } else {	numT = 0;    }      if (!Cudd_IsConstant(Nnv)) {	st_lookup(mtable,(char *)Nnv, (char **)&dummy);	numE = *dummy/(2*(1<<index));    } else if (Nnv == one) {	numE = max/(2*(1<<index));    } else {	numE = 0;//.........这里部分代码省略.........

/**Function********************************************************************  Synopsis    [Performs the recursive step of Cudd_zddWeakDivF.]  Description []  SideEffects [None]  SeeAlso     [Cudd_zddWeakDivF]******************************************************************************/DdNode  *cuddZddWeakDivF(  DdManager * dd,  DdNode * f,  DdNode * g){    int         v, top_f, top_g, vf, vg;    DdNode      *one = DD_ONE(dd);    DdNode      *zero = DD_ZERO(dd);    DdNode      *f0, *f1, *fd, *g0, *g1, *gd;    DdNode      *q, *tmp;    DdNode      *r;    DdNode      *term1, *term0, *termd;    int         flag;    int         pv, nv;    statLine(dd);    if (g == one)        return(f);    if (f == zero || f == one)        return(zero);    if (f == g)        return(one);    /* Check cache. */    r = cuddCacheLookup2Zdd(dd, cuddZddWeakDivF, f, g);    if (r)        return(r);    top_f = dd->permZ[f->index];    top_g = dd->permZ[g->index];    vf = top_f >> 1;    vg = top_g >> 1;    v = ddMin(top_f, top_g);    if (v == top_f && vf < vg) {        v = f->index;        flag = cuddZddGetCofactors3(dd, f, v, &f1, &f0, &fd);        if (flag == 1)            return(NULL);        Cudd_Ref(f1);        Cudd_Ref(f0);        Cudd_Ref(fd);        pv = cuddZddGetPosVarIndex(dd, v);        nv = cuddZddGetNegVarIndex(dd, v);        term1 = cuddZddWeakDivF(dd, f1, g);        if (term1 == NULL) {            Cudd_RecursiveDerefZdd(dd, f1);            Cudd_RecursiveDerefZdd(dd, f0);            Cudd_RecursiveDerefZdd(dd, fd);            return(NULL);        }        Cudd_Ref(term1);        Cudd_RecursiveDerefZdd(dd, f1);        term0 = cuddZddWeakDivF(dd, f0, g);        if (term0 == NULL) {            Cudd_RecursiveDerefZdd(dd, f0);            Cudd_RecursiveDerefZdd(dd, fd);            Cudd_RecursiveDerefZdd(dd, term1);            return(NULL);        }        Cudd_Ref(term0);        Cudd_RecursiveDerefZdd(dd, f0);        termd = cuddZddWeakDivF(dd, fd, g);        if (termd == NULL) {            Cudd_RecursiveDerefZdd(dd, fd);            Cudd_RecursiveDerefZdd(dd, term1);            Cudd_RecursiveDerefZdd(dd, term0);            return(NULL);        }        Cudd_Ref(termd);        Cudd_RecursiveDerefZdd(dd, fd);        tmp = cuddZddGetNode(dd, nv, term0, termd); /* nv = zi */        if (tmp == NULL) {            Cudd_RecursiveDerefZdd(dd, term1);            Cudd_RecursiveDerefZdd(dd, term0);            Cudd_RecursiveDerefZdd(dd, termd);            return(NULL);        }        Cudd_Ref(tmp);        Cudd_RecursiveDerefZdd(dd, term0);        Cudd_RecursiveDerefZdd(dd, termd);        q = cuddZddGetNode(dd, pv, term1, tmp); /* pv = yi */        if (q == NULL) {            Cudd_RecursiveDerefZdd(dd, term1);            Cudd_RecursiveDerefZdd(dd, tmp);//.........这里部分代码省略.........

/**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_bddLiteralSetIntersection.]  Description [Performs the recursive step of  Cudd_bddLiteralSetIntersection. Scans the cubes for common variables,  and checks whether they agree in phase.  Returns a pointer to the  resulting cube if successful; NULL otherwise.]  SideEffects [None]******************************************************************************/DdNode *cuddBddLiteralSetIntersectionRecur(    DdManager * dd,    DdNode * f,    DdNode * g){    DdNode *res, *tmp;    DdNode *F, *G;    DdNode *fc, *gc;    DdNode *one;    DdNode *zero;    unsigned int topf, topg, comple;    int phasef, phaseg;    statLine(dd);    if (f == g) return(f);    F = Cudd_Regular(f);    G = Cudd_Regular(g);    one = DD_ONE(dd);    /* Here f != g. If F == G, then f and g are complementary.    ** Since they are two cubes, this case only occurs when f == v,    ** g == v', and v is a variable or its complement.    */    if (F == G) return(one);    zero = Cudd_Not(one);    topf = cuddI(dd,F->index);    topg = cuddI(dd,G->index);    /* Look for a variable common to both cubes. If there are none, this    ** loop will stop when the constant node is reached in both cubes.    */    while (topf != topg) {        if (topf < topg) {	/* move down on f */            comple = f != F;            f = cuddT(F);            if (comple) f = Cudd_Not(f);            if (f == zero) {                f = cuddE(F);                if (comple) f = Cudd_Not(f);            }            F = Cudd_Regular(f);            topf = cuddI(dd,F->index);        } else if (topg < topf) {            comple = g != G;            g = cuddT(G);            if (comple) g = Cudd_Not(g);            if (g == zero) {                g = cuddE(G);                if (comple) g = Cudd_Not(g);            }            G = Cudd_Regular(g);            topg = cuddI(dd,G->index);        }    }    /* At this point, f == one <=> g == 1. It suffices to test one of them. */    if (f == one) return(one);    res = cuddCacheLookup2(dd,Cudd_bddLiteralSetIntersection,f,g);    if (res != NULL) {        return(res);    }    /* Here f and g are both non constant and have the same top variable. */    comple = f != F;    fc = cuddT(F);    phasef = 1;    if (comple) fc = Cudd_Not(fc);    if (fc == zero) {        fc = cuddE(F);        phasef = 0;        if (comple) fc = Cudd_Not(fc);    }    comple = g != G;    gc = cuddT(G);    phaseg = 1;    if (comple) gc = Cudd_Not(gc);    if (gc == zero) {        gc = cuddE(G);        phaseg = 0;        if (comple) gc = Cudd_Not(gc);    }    tmp = cuddBddLiteralSetIntersectionRecur(dd,fc,gc);    if (tmp == NULL) {//.........这里部分代码省略.........

/**Function********************************************************************  Synopsis [Converts a ZDD cover to a BDD graph.]  Description [Converts a ZDD cover to a BDD graph. If successful, it  returns a BDD node, otherwise it returns NULL. It is a recursive  algorithm as the following. First computes 3 cofactors of a ZDD cover;  f1, f0 and fd. Second, compute BDDs(b1, b0 and bd) of f1, f0 and fd.  Third, compute T=b1+bd and E=b0+bd. Fourth, compute ITE(v,T,E) where v  is the variable which has the index of the top node of the ZDD cover.  In this case, since the index of v can be larger than either one of T or  one of E, cuddUniqueInterIVO is called, here IVO stands for  independent variable ordering.]  SideEffects []  SeeAlso     [Cudd_MakeBddFromZddCover]******************************************************************************/DdNode	*cuddMakeBddFromZddCover(    DdManager * dd,    DdNode * node){    DdNode	*neW;    int		v;    DdNode	*f1, *f0, *fd;    DdNode	*b1, *b0, *bd;    DdNode	*T, *E;    statLine(dd);    if (node == dd->one)        return(dd->one);    if (node == dd->zero)        return(Cudd_Not(dd->one));    /* Check cache */    neW = cuddCacheLookup1(dd, cuddMakeBddFromZddCover, node);    if (neW)        return(neW);    v = Cudd_Regular(node)->index;	/* either yi or zi */    cuddZddGetCofactors3(dd, node, v, &f1, &f0, &fd);    Cudd_Ref(f1);    Cudd_Ref(f0);    Cudd_Ref(fd);    b1 = cuddMakeBddFromZddCover(dd, f1);    if (!b1) {        Cudd_RecursiveDerefZdd(dd, f1);        Cudd_RecursiveDerefZdd(dd, f0);        Cudd_RecursiveDerefZdd(dd, fd);        return(NULL);    }    Cudd_Ref(b1);    b0 = cuddMakeBddFromZddCover(dd, f0);    if (!b1) {        Cudd_RecursiveDerefZdd(dd, f1);        Cudd_RecursiveDerefZdd(dd, f0);        Cudd_RecursiveDerefZdd(dd, fd);        Cudd_RecursiveDeref(dd, b1);        return(NULL);    }    Cudd_Ref(b0);    Cudd_RecursiveDerefZdd(dd, f1);    Cudd_RecursiveDerefZdd(dd, f0);    if (fd != dd->zero) {        bd = cuddMakeBddFromZddCover(dd, fd);        if (!bd) {            Cudd_RecursiveDerefZdd(dd, fd);            Cudd_RecursiveDeref(dd, b1);            Cudd_RecursiveDeref(dd, b0);            return(NULL);        }        Cudd_Ref(bd);        Cudd_RecursiveDerefZdd(dd, fd);        T = cuddBddAndRecur(dd, Cudd_Not(b1), Cudd_Not(bd));        if (!T) {            Cudd_RecursiveDeref(dd, b1);            Cudd_RecursiveDeref(dd, b0);            Cudd_RecursiveDeref(dd, bd);            return(NULL);        }        T = Cudd_NotCond(T, T != NULL);        Cudd_Ref(T);        Cudd_RecursiveDeref(dd, b1);        E = cuddBddAndRecur(dd, Cudd_Not(b0), Cudd_Not(bd));        if (!E) {            Cudd_RecursiveDeref(dd, b0);            Cudd_RecursiveDeref(dd, bd);            Cudd_RecursiveDeref(dd, T);            return(NULL);        }        E = Cudd_NotCond(E, E != NULL);        Cudd_Ref(E);        Cudd_RecursiveDeref(dd, b0);        Cudd_RecursiveDeref(dd, bd);    }    else {//.........这里部分代码省略.........

/**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_addOrAbstract.]  Description [Performs the recursive step of Cudd_addOrAbstract.  Returns the ADD obtained by abstracting the variables of cube from f,  if successful; NULL otherwise.]  SideEffects [None]  SeeAlso     []******************************************************************************/DdNode *cuddAddOrAbstractRecur(  DdManager * manager,  DdNode * f,  DdNode * cube){    DdNode	*T, *E, *res, *res1, *res2, *one;    statLine(manager);    one = DD_ONE(manager);    /* Cube is guaranteed to be a cube at this point. */    if (cuddIsConstant(f) || cube == one) {  	return(f);    }    /* Abstract a variable that does not appear in f. */    if (cuddI(manager,f->index) > cuddI(manager,cube->index)) {	res = cuddAddOrAbstractRecur(manager, f, cuddT(cube));	return(res);    }    if ((res = cuddCacheLookup2(manager, Cudd_addOrAbstract, f, cube)) != NULL) {	return(res);    }    T = cuddT(f);    E = cuddE(f);    /* If the two indices are the same, so are their levels. */    if (f->index == cube->index) {	res1 = cuddAddOrAbstractRecur(manager, T, cuddT(cube));	if (res1 == NULL) return(NULL);        cuddRef(res1);	if (res1 != one) {	    res2 = cuddAddOrAbstractRecur(manager, E, cuddT(cube));	    if (res2 == NULL) {		Cudd_RecursiveDeref(manager,res1);		return(NULL);	    }	    cuddRef(res2);	    res = cuddAddApplyRecur(manager, Cudd_addOr, res1, res2);	    if (res == NULL) {		Cudd_RecursiveDeref(manager,res1);		Cudd_RecursiveDeref(manager,res2);		return(NULL);	    }	    cuddRef(res);	    Cudd_RecursiveDeref(manager,res1);	    Cudd_RecursiveDeref(manager,res2);	} else {	    res = res1;	}	cuddCacheInsert2(manager, Cudd_addOrAbstract, f, cube, res);	cuddDeref(res);        return(res);    } else { /* if (cuddI(manager,f->index) < cuddI(manager,cube->index)) */	res1 = cuddAddOrAbstractRecur(manager, T, cube);	if (res1 == NULL) return(NULL);        cuddRef(res1);	res2 = cuddAddOrAbstractRecur(manager, E, cube);	if (res2 == NULL) {	    Cudd_RecursiveDeref(manager,res1);	    return(NULL);	}        cuddRef(res2);	res = (res1 == res2) ? res1 :	    cuddUniqueInter(manager, (int) f->index, res1, res2);	if (res == NULL) {	    Cudd_RecursiveDeref(manager,res1);	    Cudd_RecursiveDeref(manager,res2);	    return(NULL);	}	cuddDeref(res1);	cuddDeref(res2);	cuddCacheInsert2(manager, Cudd_addOrAbstract, f, cube, res);        return(res);    }} /* end of cuddAddOrAbstractRecur */

/**Function********************************************************************  Synopsis    [Performs the recursive step of Extra_TransferPermute.]  Description [Performs the recursive step of Extra_TransferPermute.  Returns a pointer to the result if successful; NULL otherwise.]  SideEffects [None]  SeeAlso     [extraTransferPermuteTime]******************************************************************************/static DdNode * extraTransferPermuteRecurTime(   DdManager * ddS,   DdManager * ddD,   DdNode * f,   st_table * table,   int * Permute,  int TimeOut ){    DdNode *ft, *fe, *t, *e, *var, *res;    DdNode *one, *zero;    int index;    int comple = 0;    statLine( ddD );    one = DD_ONE( ddD );    comple = Cudd_IsComplement( f );    /* Trivial cases. */    if ( Cudd_IsConstant( f ) )        return ( Cudd_NotCond( one, comple ) );    /* Make canonical to increase the utilization of the cache. */    f = Cudd_NotCond( f, comple );    /* Now f is a regular pointer to a non-constant node. */    /* Check the cache. */    if ( st_lookup( table, ( char * ) f, ( char ** ) &res ) )        return ( Cudd_NotCond( res, comple ) );    if ( TimeOut && TimeOut < clock() )        return NULL;    /* Recursive step. */    if ( Permute )        index = Permute[f->index];    else        index = f->index;    ft = cuddT( f );    fe = cuddE( f );    t = extraTransferPermuteRecurTime( ddS, ddD, ft, table, Permute, TimeOut );    if ( t == NULL )    {        return ( NULL );    }    cuddRef( t );    e = extraTransferPermuteRecurTime( ddS, ddD, fe, table, Permute, TimeOut );    if ( e == NULL )    {        Cudd_RecursiveDeref( ddD, t );        return ( NULL );    }    cuddRef( e );    zero = Cudd_Not(ddD->one);    var = cuddUniqueInter( ddD, index, one, zero );    if ( var == NULL )    {        Cudd_RecursiveDeref( ddD, t );        Cudd_RecursiveDeref( ddD, e );        return ( NULL );    }    res = cuddBddIteRecur( ddD, var, t, e );    if ( res == NULL )    {        Cudd_RecursiveDeref( ddD, t );        Cudd_RecursiveDeref( ddD, e );        return ( NULL );    }    cuddRef( res );    Cudd_RecursiveDeref( ddD, t );    Cudd_RecursiveDeref( ddD, e );    if ( st_add_direct( table, ( char * ) f, ( char * ) res ) ==         ST_OUT_OF_MEM )    {        Cudd_RecursiveDeref( ddD, res );        return ( NULL );    }    return ( Cudd_NotCond( res, comple ) );}  /* end of extraTransferPermuteRecurTime */