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

/**Function********************************************************************  Synopsis    [Bellman-Ford algorithm for single-source shortest paths.]  Description [Bellman-Ford algorithm for single-source shortest  paths.  Returns the vector of the distances of all states from the  initial states.  In case of multiple initial states the distance for  each state is from the nearest initial state.  Negative-weight  cycles are detected, though only in the naive way.  (Lack of  convergence after nodes-1 iterations.)  In such a case, a constant  ADD with value minus infinity is returned.  Bellman-Ford is based on  matrix-vector multiplication.  The matrix is the distance matrix  D(x,y), such that D(a,b) is the length of the arc connecting state a  to state b.  The vector V(x) stores the distances of all states from  the initial states.  The actual vector used in the matrix-vector  multiplication is diff(x), that holds those distances that have  changed during the last update.]  SideEffects []  SeeAlso     [ntrWarshall ntrSquare]******************************************************************************/static DdNode *ntrBellman(  DdManager *dd,  DdNode *D,  DdNode *source,  DdNode **x,  DdNode **y,  int vars,  int pr){    DdNode *u, *w, *V, *min, *diff;    DdApaNumber i, nodes, one;    int digits = vars + 1;    /* To avoid overflow when there are many variables, use APA. */    nodes = Cudd_NewApaNumber(digits);    Cudd_ApaPowerOfTwo(digits,nodes,vars);    i = Cudd_NewApaNumber(digits);    one = Cudd_NewApaNumber(digits);    Cudd_ApaSetToLiteral(digits,one,1);#if 0    /* Find the distances from the initial state along paths using one    ** arc. */    w = Cudd_Cofactor(dd,D,source); /* works only if source is a cube */    Cudd_Ref(w);    V = Cudd_addSwapVariables(dd,w,x,y,vars);    Cudd_Ref(V);    Cudd_RecursiveDeref(dd,w);#endif    /* The initial states are at distance 0. The other states are    ** initially at infinite distance. */    V = Cudd_addIte(dd,source,Cudd_ReadZero(dd),Cudd_ReadPlusInfinity(dd));    Cudd_Ref(V);    /* Selective trace algorithm.  For the next update, only consider the    ** nodes whose distance has changed in the last update. */    diff = V;    Cudd_Ref(diff);    for (Cudd_ApaSetToLiteral(digits,i,1);	 Cudd_ApaCompare(digits,i,digits,nodes) < 0;	 Cudd_ApaAdd(digits,i,one,i)) {	if (pr>2) {(void) printf("V"); Cudd_PrintDebug(dd,V,vars,pr);}	/* Compute the distances via triangulation as a function of x. */	w = Cudd_addTriangle(dd,diff,D,x,vars);	Cudd_Ref(w);	Cudd_RecursiveDeref(dd,diff);	u = Cudd_addSwapVariables(dd,w,x,y,vars);	Cudd_Ref(u);	Cudd_RecursiveDeref(dd,w);	if (pr>2) {(void) printf("u"); Cudd_PrintDebug(dd,u,vars,pr);}	/* Take the minimum of the previous distances and those just	** computed. */	min = Cudd_addApply(dd,Cudd_addMinimum,V,u);	Cudd_Ref(min);	Cudd_RecursiveDeref(dd,u);	if (pr>2) {(void) printf("min"); Cudd_PrintDebug(dd,min,vars,pr);}	if (V == min) {		/* convergence */	    Cudd_RecursiveDeref(dd,min);	    if (pr>0) {		(void) printf("Terminating after ");		Cudd_ApaPrintDecimal(stdout,digits,i);		(void) printf(" iterations/n");	    }	    break;	}	/* Find the distances that decreased. */	diff = Cudd_addApply(dd,Cudd_addDiff,V,min);	Cudd_Ref(diff);	if (pr>2) {(void) printf("diff"); Cudd_PrintDebug(dd,diff,vars,pr);}	Cudd_RecursiveDeref(dd,V);	V = min;    }//.........这里部分代码省略.........

/**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 {//.........这里部分代码省略.........

//.........这里部分代码省略.........    x = y = xn = yn_ = NULL;    do {	/* We want to start anew for every matrix. */	maxnx = maxny = 0;	nx = maxnx; ny = maxny;	if (pr>0) lapTime = util_cpu_time();	if (harwell) {	    if (pr >= 0) (void) printf(":name: ");	    ok = Cudd_addHarwell(fp, dd, &M, &x, &y, &xn, &yn_, &nx, &ny,	    &m, &n, 0, 2, 1, 2, pr);	} else {	    ok = Cudd_addRead(fp, dd, &M, &x, &y, &xn, &yn_, &nx, &ny,	    &m, &n, 0, 2, 1, 2);	    if (pr >= 0)		(void) printf(":name: %s: %d rows %d columns/n", file, m, n);	}	if (!ok) {	    (void) fprintf(stderr, "Error reading matrix/n");	    exit(1);	}	if (nx > maxnx) maxnx = nx;	if (ny > maxny) maxny = ny;	/* Build cube of negated y's. */	ycube = DD_TRUE(dd);	Cudd_Ref(ycube);	for (i = maxny - 1; i >= 0; i--) {	    DdNode *tmpp;	    tmpp = Cudd_bddAnd(dd,Cudd_Not(dd->vars[y[i]->index]),ycube);	    if (tmpp == NULL) exit(2);	    Cudd_Ref(tmpp);	    Cudd_RecursiveDeref(dd,ycube);	    ycube = tmpp;	}	/* Initialize vectors of BDD variables used by priority func. */	xvars = ALLOC(DdNode *, nx);	if (xvars == NULL) exit(2);	for (i = 0; i < nx; i++) {	    xvars[i] = dd->vars[x[i]->index];	}	yvars = ALLOC(DdNode *, ny);	if (yvars == NULL) exit(2);	for (i = 0; i < ny; i++) {	    yvars[i] = dd->vars[y[i]->index];	}	/* Clean up */	for (i=0; i < maxnx; i++) {	    Cudd_RecursiveDeref(dd, x[i]);	    Cudd_RecursiveDeref(dd, xn[i]);	}	FREE(x);	FREE(xn);	for (i=0; i < maxny; i++) {	    Cudd_RecursiveDeref(dd, y[i]);	    Cudd_RecursiveDeref(dd, yn_[i]);	}	FREE(y);	FREE(yn_);	if (pr>0) {(void) printf(":1: M"); Cudd_PrintDebug(dd,M,nx+ny,pr);}	if (pr>0) (void) printf(":2: time to read the matrix = %s/n",		    util_print_time(util_cpu_time() - lapTime));

//.........这里部分代码省略.........    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);    }    checkWhetherToGiveUp(manager);    /* 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) {	Cudd_RecursiveDeref(manager, t);	return(NULL);    }    cuddRef(e);    if (t == e) {	r = t;    } else {	if (Cudd_IsComplement(t)) {	    r = cuddUniqueInter(manager,(int)index,Cudd_Not(t),Cudd_Not(e));	    if (r == NULL) {		Cudd_RecursiveDeref(manager, t);		Cudd_RecursiveDeref(manager, e);		return(NULL);	    }	    r = Cudd_Not(r);	} else {	    r = cuddUniqueInter(manager,(int)index,t,e);	    if (r == NULL) {		Cudd_RecursiveDeref(manager, t);		Cudd_RecursiveDeref(manager, e);		return(NULL);	    }	}    }    cuddDeref(e);    cuddDeref(t);    if (F->ref != 1 || G->ref != 1)	cuddCacheInsert2(manager, cacheOp, f, g, r);    return(r);} /* end of cuddBddClippingAndRecur */

/**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    [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_CProjection.]  Description [Performs the recursive step of Cudd_CProjection. Returns  the projection if successful; NULL otherwise.]  SideEffects [None]  SeeAlso     [Cudd_CProjection]******************************************************************************/DdNode *cuddCProjectionRecur(  DdManager * dd,  DdNode * R,  DdNode * Y,  DdNode * Ysupp){    DdNode *res, *res1, *res2, *resA;    DdNode *r, *y, *RT, *RE, *YT, *YE, *Yrest, *Ra, *Ran, *Gamma, *Alpha;    unsigned int topR, topY, top, index;    DdNode *one = DD_ONE(dd);    statLine(dd);    if (Y == one) return(R);#ifdef DD_DEBUG    assert(!Cudd_IsConstant(Y));#endif    if (R == Cudd_Not(one)) return(R);    res = cuddCacheLookup2(dd, Cudd_CProjection, R, Y);    if (res != NULL) return(res);    r = Cudd_Regular(R);    topR = cuddI(dd,r->index);    y = Cudd_Regular(Y);    topY = cuddI(dd,y->index);    top = ddMin(topR, topY);    /* Compute the cofactors of R */    if (topR == top) {	index = r->index;	RT = cuddT(r);	RE = cuddE(r);	if (r != R) {	    RT = Cudd_Not(RT); RE = Cudd_Not(RE);	}    } else {	RT = RE = R;    }    if (topY > top) {	/* Y does not depend on the current top variable.	** We just need to compute the results on the two cofactors of R	** and make them the children of a node labeled r->index.	*/	res1 = cuddCProjectionRecur(dd,RT,Y,Ysupp);	if (res1 == NULL) return(NULL);	cuddRef(res1);	res2 = cuddCProjectionRecur(dd,RE,Y,Ysupp);	if (res2 == NULL) {	    Cudd_RecursiveDeref(dd,res1);	    return(NULL);	}	cuddRef(res2);	res = cuddBddIteRecur(dd, dd->vars[index], res1, res2);	if (res == NULL) {	    Cudd_RecursiveDeref(dd,res1);	    Cudd_RecursiveDeref(dd,res2);	    return(NULL);	}	/* If we have reached this point, res1 and res2 are now	** incorporated in res. cuddDeref is therefore sufficient.	*/	cuddDeref(res1);	cuddDeref(res2);    } else {	/* Compute the cofactors of Y */	index = y->index;	YT = cuddT(y);	YE = cuddE(y);	if (y != Y) {	    YT = Cudd_Not(YT); YE = Cudd_Not(YE);	}	if (YT == Cudd_Not(one)) {	    Alpha  = Cudd_Not(dd->vars[index]);	    Yrest = YE;	    Ra = RE;	    Ran = RT;	} else {	    Alpha = dd->vars[index];	    Yrest = YT;	    Ra = RT;	    Ran = RE;	}	Gamma = cuddBddExistAbstractRecur(dd,Ra,cuddT(Ysupp));//.........这里部分代码省略.........

//.........这里部分代码省略.........                fprintf( stderr,                         "Error while computing bitwise variable offsets./n" );                return -1;            }            free( all_vars );            init_state_acc = 0;            if (verbose) {                logprint_startline();                logprint_raw( "initial state for simulation:" );            }            for (i = 0; i < original_num_env+original_num_sys; i++) {                if (verbose)                    logprint_raw( " %d", *(init_state_ints+i) );                init_state_acc += *(init_state_ints+i) << *(offw + 2*i);            }            if (verbose)                logprint_endline();            free( offw );            init_state = int_to_bitvec( init_state_acc, num_env+num_sys );            if (init_state == NULL)                return -1;            play = sim_rhc( manager, W, etrans, strans, sgoals, metric_vars,                            horizon, init_state, max_sim_it, verbose );            if (play == NULL) {                fprintf( stderr,                         "Error while attempting receding horizon"                         " simulation./n" );                return -1;            }            free( init_state );            logprint( "play length: %d", aut_size( play ) );            tmppt = spc.nonbool_var_list;            while (tmppt) {                aut_compact_nonbool( play, spc.evar_list, spc.svar_list,                                     tmppt->name, tmppt->value );                tmppt = tmppt->left;            }            num_env = tree_size( spc.evar_list );            num_sys = tree_size( spc.svar_list );            /* Open output file if specified; else point to stdout. */            if (output_file_index >= 0) {                fp = fopen( argv[output_file_index], "w" );                if (fp == NULL) {                    perror( "grjit, fopen" );                    return -1;                }            } else {                fp = stdout;            }            /* Print simulation trace */            dump_simtrace( play, spc.evar_list, spc.svar_list, fp );            if (fp != stdout)                fclose( fp );        }        Cudd_RecursiveDeref( manager, W );        Cudd_RecursiveDeref( manager, etrans );        Cudd_RecursiveDeref( manager, strans );    }    /* Clean-up */    free( metric_vars );    delete_tree( spc.evar_list );    delete_tree( spc.svar_list );    delete_tree( spc.env_init );    delete_tree( spc.sys_init );    delete_tree( spc.env_trans );    delete_tree( spc.sys_trans );    for (i = 0; i < spc.num_egoals; i++)        delete_tree( *(spc.env_goals+i) );    if (spc.num_egoals > 0)        free( spc.env_goals );    for (i = 0; i < spc.num_sgoals; i++)        delete_tree( *(spc.sys_goals+i) );    if (spc.num_sgoals > 0)        free( spc.sys_goals );    if (T != NULL)        Cudd_RecursiveDeref( manager, T );    if (strategy)        delete_aut( strategy );    if (verbose > 1)        logprint( "Cudd_CheckZeroRef -> %d", Cudd_CheckZeroRef( manager ) );    Cudd_Quit(manager);    if (logging_flag)        closelogfile();    /* Return 0 if realizable, -1 if not realizable. */    if (T != NULL) {        return 0;    } else {        return -1;    }    return 0;}

/**Function********************************************************************  Synopsis    [Builds an ADD for the residue modulo m of an n-bit  number.]  Description [Builds an ADD for the residue modulo m of an n-bit  number. 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.  Cudd_addResidue returns a pointer to the resulting ADD if successful;  NULL otherwise.]  SideEffects [None]  SeeAlso     []******************************************************************************/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++) {//.........这里部分代码省略.........

/**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    [Writes a dot file representing the argument ZDDs.]  Description [Writes a file representing the argument ZDDs in a format  suitable for the graph drawing program dot.  It returns 1 in case of success; 0 otherwise (e.g., out-of-memory,  file system full).  Cudd_zddDumpDot does not close the file: This is the caller  responsibility. Cudd_zddDumpDot uses a minimal unique subset of the  hexadecimal address of a node as name for it.  If the argument inames is non-null, it is assumed to hold the pointers  to the names of the inputs. Similarly for onames.  Cudd_zddDumpDot uses the following convention to draw arcs:    <ul>    <li> solid line: THEN arcs;    <li> dashed line: ELSE arcs.    </ul>  The dot options are chosen so that the drawing fits on a letter-size  sheet.  ]  SideEffects [None]  SeeAlso     [Cudd_DumpDot Cudd_zddPrintDebug]******************************************************************************/intCudd_zddDumpDot(  DdManager * dd /* manager */,  int  n /* number of output nodes to be dumped */,  DdNode ** f /* array of output nodes to be dumped */,  char ** inames /* array of input names (or NULL) */,  char ** onames /* array of output names (or NULL) */,  FILE * fp /* pointer to the dump file */){    DdNode	*support = NULL;    DdNode	*scan;    int		*sorted = NULL;    int		nvars = dd->sizeZ;    st_table	*visited = NULL;    st_generator *gen;    int		retval;    int		i, j;    int		slots;    DdNodePtr	*nodelist;    long	refAddr, diff, mask;    /* Build a bit array with the support of f. */    sorted = ALLOC(int,nvars);    if (sorted == NULL) {	dd->errorCode = CUDD_MEMORY_OUT;	goto failure;    }    for (i = 0; i < nvars; i++) sorted[i] = 0;    /* Take the union of the supports of each output function. */    for (i = 0; i < n; i++) {	support = Cudd_Support(dd,f[i]);	if (support == NULL) goto failure;	cuddRef(support);	scan = support;	while (!cuddIsConstant(scan)) {	    sorted[scan->index] = 1;	    scan = cuddT(scan);	}	Cudd_RecursiveDeref(dd,support);    }    support = NULL; /* so that we do not try to free it in case of failure */    /* Initialize symbol table for visited nodes. */    visited = st_init_table(st_ptrcmp, st_ptrhash);    if (visited == NULL) goto failure;    /* Collect all the nodes of this DD in the symbol table. */    for (i = 0; i < n; i++) {	retval = cuddCollectNodes(f[i],visited);	if (retval == 0) goto failure;    }    /* Find how many most significant hex digits are identical    ** in the addresses of all the nodes. Build a mask based    ** on this knowledge, so that digits that carry no information    ** will not be printed. This is done in two steps.    **  1. We scan the symbol table to find the bits that differ    **     in at least 2 addresses.    **  2. We choose one of the possible masks. There are 8 possible    **     masks for 32-bit integer, and 16 possible masks for 64-bit    **     integers.    */    /* Find the bits that are different. */    refAddr = (long) f[0];    diff = 0;    gen = st_init_gen(visited);    while (st_gen(gen, (char **) &scan, NULL)) {	diff |= refAddr ^ (long) scan;    }    st_free_gen(gen);//.........这里部分代码省略.........

//.........这里部分代码省略.........#endif#ifdef EUROPE_YES    if (i < europeSize) {      europeState[europeOrder[i]] = tmp;    }    complete = complete && (i >= (europeSize-1));#endif    i++;  }#ifdef USA_YES  createGraph(usaSize,usaEdge,usaState,usaGraph);#endif#ifdef EUROPE_YES  createGraph(europeSize,europeEdge,europeState,europeGraph);#endif#ifdef USE_BIDDY  Biddy_Clean();#endif  r1 = Biddy_GetConstantZero();  r2 = Biddy_GetConstantZero();#ifdef USE_CUDD  Cudd_Ref(r1);  Cudd_Ref(r2);#endif#ifdef USA_YES  if (!CALCULATE_KERNELS) {    /* CALCULATING INDEPENDENCE SETS FOR USA */#ifdef USE_CUDD    Cudd_RecursiveDeref(manager,r1);#endif    r1 = calculateIndependence(usaSize,usaState,usaGraph);  } else {    /* CALCULATING KERNELS (MAXIMUM INDEPENDENCE SETS) FOR USA */#ifdef USE_CUDD    Cudd_RecursiveDeref(manager,r1);#endif    r1 = calculateKernels(usaSize,usaState,usaGraph);  }#ifdef USE_BIDDY  Biddy_AddPersistentFormula((Biddy_String)"usa",r1);  Biddy_Clean();#endif#ifdef USE_CUDD  for (i=0; i<usaSize; i++) {    Cudd_RecursiveDeref(manager,usaGraph[i]);  }#endif#endif#ifdef EUROPE_YES  if (!CALCULATE_KERNELS) {    /* CALCULATING INDEPENDENCE SETS FOR EUROPE */#ifdef USE_CUDD    Cudd_RecursiveDeref(manager,r2);#endif    r2 = calculateIndependence(europeSize,europeState,europeGraph);  } else {    /* CALCULATING KERNELS (MAXIMUM INDEPENDENCE SETS) FOR EUROPE */#ifdef USE_CUDD    Cudd_RecursiveDeref(manager,r2);#endif

/**Function********************************************************************  Synopsis    [Repeated squaring algorithm for all-pairs shortest paths.]  Description []  SideEffects []  SeeAlso     []******************************************************************************/static DdNode *ntrSquare(  DdManager *dd /* manager */,  DdNode *D /* D(z,y): distance matrix */,  DdNode **x /* array of x variables */,  DdNode **y /* array of y variables */,  DdNode **z /* array of z variables */,  int vars /* number of variables in each of the three arrays */,  int pr /* verbosity level */,  int st /* use the selective trace algorithm */){    DdNode *zero;    DdNode *I;              /* identity matirix */    DdNode *w, *V, *P, *M, *R, *RT;    DdNode *diff, *min, *minDiag;    int n;    int neg;    long start_time;    zero = Cudd_ReadZero(dd);    /* Make a working copy of the original matrix. */    R = D;    Cudd_Ref(R);    I = Cudd_addXeqy(dd,vars,z,y);    /* identity matrix */    Cudd_Ref(I);    /* Make a copy of the matrix for the selective trace algorithm. */    diff = R;    Cudd_Ref(diff);    start_time = util_cpu_time();    for (n = vars; n >= 0; n--) {	printf("Starting iteration %d at time %s/n",vars-n,	       util_print_time(util_cpu_time() - start_time));	/* Check for negative cycles: They are identified by negative	** elements on the diagonal.	*/	/* Extract values from the diagonal. */        Cudd_Ref(w = Cudd_addIte(dd,I,R,zero));	minDiag = Cudd_addFindMin(dd,w);	/* no need to ref */	neg = Cudd_V(minDiag) < 0;	Cudd_RecursiveDeref(dd,w);	if (neg) {	    Cudd_RecursiveDeref(dd,diff);            (void) printf("Negative cycle after %d iterations!/n",vars-n);            break;        }	/* Prepare the first operand of matrix multiplication:	**   diff(z,y) -> RT(x,y) -> V(x,z)	*/	/* RT(x,y) */	Cudd_Ref(RT = Cudd_addSwapVariables(dd,diff,x,z,vars));	Cudd_RecursiveDeref(dd,diff);	/* V(x,z) */	Cudd_Ref(V = Cudd_addSwapVariables(dd,RT,y,z,vars));	Cudd_RecursiveDeref(dd,RT);	if (pr > 0) {	    double pathcount;	    (void) printf("V"); Cudd_PrintDebug(dd,V,2*vars,pr);	    pathcount = Cudd_CountPath(V);	    (void) printf("Path count = %g/n", pathcount);	}	/* V(x,z) * R(z,y) -> P(x,y) */	Cudd_Ref(P = Cudd_addTriangle(dd,V,R,z,vars));	Cudd_RecursiveDeref(dd,V);	/* P(x,y) => M(z,y) */	Cudd_Ref(M = Cudd_addSwapVariables(dd,P,x,z,vars));	Cudd_RecursiveDeref(dd,P);	if (pr>0) {(void) printf("M"); Cudd_PrintDebug(dd,M,2*vars,pr);}	/* min(z,y) */	Cudd_Ref(min = Cudd_addApply(dd,Cudd_addMinimum,R,M));	Cudd_RecursiveDeref(dd,M);	if (R == min) {	    Cudd_RecursiveDeref(dd,min);	    if (pr>0) {printf("Done after %d iterations/n",vars-n+1); }	    break;	}	/* diff(z,y) */	if (st) {	    Cudd_Ref(diff = Cudd_addApply(dd,Cudd_addDiff,min,R));	} else {	    Cudd_Ref(diff = min);//.........这里部分代码省略.........

/**Function********************************************************************  Synopsis    [Floyd-Warshall algorithm for all-pair shortest paths.]  Description []  SideEffects []  SeeAlso     []******************************************************************************/static DdNode *ntrWarshall(  DdManager *dd,  DdNode *D,  DdNode **x,  DdNode **y,  int vars,  int pr){    DdNode *one, *zero;    DdNode *xminterm,  *w, *V, *V2;    DdNode *P, *R;    int i;    int nodes;    int k,u;    long start_time;    if (vars > 30)	nodes = 1000000000;    else	nodes = 1 << vars;    one = DD_ONE(dd);    zero = DD_ZERO(dd);    Cudd_Ref(R = D);                        /* make copy of original matrix */    /* Extract pivot row and column from D */    start_time = util_cpu_time();    for (k = 0; k < nodes; k++) {        if (k % 10000 == 0) {	    (void) printf("Starting iteration  %d  at time %s/n",			  k,util_print_time(util_cpu_time() - start_time));        }        Cudd_Ref(xminterm = one);        u = k;	for (i = vars-1; i >= 0; i--) {	    if (u&1) {	        Cudd_Ref(w = Cudd_addIte(dd,x[i],xminterm,zero));	    } else {	        Cudd_Ref(w = Cudd_addIte(dd,x[i],zero,xminterm));	    }	    Cudd_RecursiveDeref(dd,xminterm);	    xminterm = w;	    u >>= 1;	}	Cudd_Ref(V = Cudd_Cofactor(dd,R,xminterm));	Cudd_RecursiveDeref(dd,xminterm);	if (pr>2) {(void) printf("V"); Cudd_PrintDebug(dd,V,vars,pr);}	Cudd_Ref(xminterm = one);	u = k;	for (i = vars-1; i >= 0; i--) {	    if (u&1) {	        Cudd_Ref(w = Cudd_addIte(dd,y[i],xminterm,zero));	    } else {	        Cudd_Ref(w = Cudd_addIte(dd,y[i],zero,xminterm));	    }	    Cudd_RecursiveDeref(dd,xminterm);	    xminterm = w;	    u >>= 1;	}	Cudd_Ref(V2 = Cudd_Cofactor(dd,R,xminterm));	Cudd_RecursiveDeref(dd,xminterm);	if (pr>2) {(void) printf("V2"); Cudd_PrintDebug(dd,V2,vars,pr);}	Cudd_Ref(P = Cudd_addOuterSum(dd,R,V,V2));	Cudd_RecursiveDeref(dd,V);	Cudd_RecursiveDeref(dd,V2);	Cudd_RecursiveDeref(dd,R);	R = P;	if (pr>2) {(void) printf("R"); Cudd_PrintDebug(dd,R,vars,pr);}    }    Cudd_Deref(R);    return(R);} /* end of ntrWarshall */

/**Function********************************************************************  Synopsis    [Performs the recursive step of Cudd_MinHammingDist.]  Description [Performs the recursive step of Cudd_MinHammingDist.  It is based on the following identity. Let H(f) be the  minimum Hamming distance of the minterms of f from the reference  minterm. Then:  <xmp>    H(f) = min(H(f0)+h0,H(f1)+h1)  </xmp>  where f0 and f1 are the two cofactors of f with respect to its top  variable; h0 is 1 if the minterm assigns 1 to the top variable of f;  h1 is 1 if the minterm assigns 0 to the top variable of f.  The upper bound on the distance is used to bound the depth of the  recursion.  Returns the minimum distance unless it exceeds the upper bound or  computation fails.]  SideEffects [None]  SeeAlso     [Cudd_MinHammingDist]******************************************************************************/static intcuddMinHammingDistRecur(  DdNode * f,  int *minterm,  DdHashTable * table,  int upperBound){    DdNode	*F, *Ft, *Fe;    double	h, hT, hE;    DdNode	*zero, *res;    DdManager	*dd = table->manager;    statLine(dd);    if (upperBound == 0) return(0);    F = Cudd_Regular(f);    if (cuddIsConstant(F)) {	zero = Cudd_Not(DD_ONE(dd));	if (f == dd->background || f == zero) {	    return(upperBound);	} else {	    return(0);	}    }    if ((res = cuddHashTableLookup1(table,f)) != NULL) {	h = cuddV(res);	if (res->ref == 0) {	    dd->dead++;	    dd->constants.dead++;	}	return((int) h);    }    Ft = cuddT(F); Fe = cuddE(F);    if (Cudd_IsComplement(f)) {	Ft = Cudd_Not(Ft); Fe = Cudd_Not(Fe);    }    if (minterm[F->index] == 0) {	DdNode *temp = Ft;	Ft = Fe; Fe = temp;    }    hT = cuddMinHammingDistRecur(Ft,minterm,table,upperBound);    if (hT == CUDD_OUT_OF_MEM) return(CUDD_OUT_OF_MEM);    if (hT == 0) {	hE = upperBound;    } else {	hE = cuddMinHammingDistRecur(Fe,minterm,table,upperBound - 1);	if (hE == CUDD_OUT_OF_MEM) return(CUDD_OUT_OF_MEM);    }    h = ddMin(hT, hE + 1);    if (F->ref != 1) {	ptrint fanout = (ptrint) F->ref;	cuddSatDec(fanout);	res = cuddUniqueConst(dd, (CUDD_VALUE_TYPE) h);	if (!cuddHashTableInsert1(table,f,res,fanout)) {	    cuddRef(res); Cudd_RecursiveDeref(dd, res);	    return(CUDD_OUT_OF_MEM);	}    }    return((int) h);} /* end of cuddMinHammingDistRecur */

/**Function********************************************************************  Synopsis    [Implements the recursive step of Cudd_addWalsh.]  Description [Generates a Walsh matrix in ADD form. Returns a pointer  to the matrixi if successful; NULL otherwise.]  SideEffects [None]******************************************************************************/static DdNode *addWalshInt(  DdManager * dd,  DdNode ** x,  DdNode ** y,  int  n){    DdNode *one, *minusone;    DdNode *t, *u, *t1, *u1, *v, *w;    int     i;    one = DD_ONE(dd);    if (n == 0) return(one);    /* Build bottom part of ADD outside loop */    minusone = cuddUniqueConst(dd,(CUDD_VALUE_TYPE) -1);    if (minusone == NULL) return(NULL);    cuddRef(minusone);    v = Cudd_addIte(dd, y[n-1], minusone, one);    if (v == NULL) {	Cudd_RecursiveDeref(dd, minusone);	return(NULL);    }    cuddRef(v);    u = Cudd_addIte(dd, x[n-1], v, one);    if (u == NULL) {	Cudd_RecursiveDeref(dd, minusone);	Cudd_RecursiveDeref(dd, v);	return(NULL);    }    cuddRef(u);    Cudd_RecursiveDeref(dd, v);    if (n>1) {	w = Cudd_addIte(dd, y[n-1], one, minusone);	if (w == NULL) {	    Cudd_RecursiveDeref(dd, minusone);	    Cudd_RecursiveDeref(dd, u);	    return(NULL);	}	cuddRef(w);	t = Cudd_addIte(dd, x[n-1], w, minusone);	if (t == NULL) {	    Cudd_RecursiveDeref(dd, minusone);	    Cudd_RecursiveDeref(dd, u);	    Cudd_RecursiveDeref(dd, w);	    return(NULL);	}	cuddRef(t);	Cudd_RecursiveDeref(dd, w);    }    cuddDeref(minusone); /* minusone is in the result; it won't die */    /* Loop to build the rest of the ADD */    for (i=n-2; i>=0; i--) {	t1 = t; u1 = u;	v = Cudd_addIte(dd, y[i], t1, u1);	if (v == NULL) {	    Cudd_RecursiveDeref(dd, u1);	    Cudd_RecursiveDeref(dd, t1);	    return(NULL);	}	cuddRef(v);	u = Cudd_addIte(dd, x[i], v, u1);	if (u == NULL) {	    Cudd_RecursiveDeref(dd, u1);	    Cudd_RecursiveDeref(dd, t1);	    Cudd_RecursiveDeref(dd, v);	    return(NULL);	}	cuddRef(u);	Cudd_RecursiveDeref(dd, v);	if (i>0) {	    w = Cudd_addIte(dd, y[i], u1, t1);	    if (w == NULL) {		Cudd_RecursiveDeref(dd, u1);		Cudd_RecursiveDeref(dd, t1);		Cudd_RecursiveDeref(dd, u);		return(NULL);	    }	    cuddRef(w);	    t = Cudd_addIte(dd, x[i], w, t1);	    if (u == NULL) {		Cudd_RecursiveDeref(dd, u1);		Cudd_RecursiveDeref(dd, t1);		Cudd_RecursiveDeref(dd, u);		Cudd_RecursiveDeref(dd, w);		return(NULL);	    }	    cuddRef(t);	    Cudd_RecursiveDeref(dd, w);//.........这里部分代码省略.........

/**Function********************************************************************  Synopsis    [Selects pairs from R using a priority function.]  Description [Selects pairs from a relation R(x,y) (given as a BDD)  in such a way that a given x appears in one pair only. Uses a  priority function to determine which y should be paired to a given x.  Cudd_PrioritySelect returns a pointer to  the selected function if successful; NULL otherwise.  Three of the arguments--x, y, and z--are vectors of BDD variables.  The first two are the variables on which R depends. The third vectore  is a vector of auxiliary variables, used during the computation. This  vector is optional. If a NULL value is passed instead,  Cudd_PrioritySelect will create the working variables on the fly.  The sizes of x and y (and z if it is not NULL) should equal n.  The priority function Pi can be passed as a BDD, or can be built by  Cudd_PrioritySelect. If NULL is passed instead of a DdNode *,  parameter Pifunc is used by Cudd_PrioritySelect to build a BDD for the  priority function. (Pifunc is a pointer to a C function.) If Pi is not  NULL, then Pifunc is ignored. Pifunc should have the same interface as  the standard priority functions (e.g., Cudd_Dxygtdxz).  Cudd_PrioritySelect and Cudd_CProjection can sometimes be used  interchangeably. Specifically, calling Cudd_PrioritySelect with  Cudd_Xgty as Pifunc produces the same result as calling  Cudd_CProjection with the all-zero minterm as reference minterm.  However, depending on the application, one or the other may be  preferable:  <ul>  <li> When extracting representatives from an equivalence relation,  Cudd_CProjection has the advantage of nor requiring the auxiliary  variables.  <li> When computing matchings in general bipartite graphs,  Cudd_PrioritySelect normally obtains better results because it can use  more powerful matching schemes (e.g., Cudd_Dxygtdxz).  </ul>  ]  SideEffects [If called with z == NULL, will create new variables in  the manager.]  SeeAlso     [Cudd_Dxygtdxz Cudd_Dxygtdyz Cudd_Xgty  Cudd_bddAdjPermuteX Cudd_CProjection]******************************************************************************/DdNode *Cudd_PrioritySelect(  DdManager * dd /* manager */,  DdNode * R /* BDD of the relation */,  DdNode ** x /* array of x variables */,  DdNode ** y /* array of y variables */,  DdNode ** z /* array of z variables (optional: may be NULL) */,  DdNode * Pi /* BDD of the priority function (optional: may be NULL) */,  int  n /* size of x, y, and z */,  DdNode * (*Pifunc)(DdManager *, int, DdNode **, DdNode **, DdNode **) /* function used to build Pi if it is NULL */){    DdNode *res = NULL;    DdNode *zcube = NULL;    DdNode *Rxz, *Q;    int createdZ = 0;    int createdPi = 0;    int i;    /* Create z variables if needed. */    if (z == NULL) {	if (Pi != NULL) return(NULL);	z = ALLOC(DdNode *,n);	if (z == NULL) {	    dd->errorCode = CUDD_MEMORY_OUT;	    return(NULL);	}	createdZ = 1;	for (i = 0; i < n; i++) {	    if (dd->size >= (int) CUDD_MAXINDEX - 1) goto endgame;	    z[i] = cuddUniqueInter(dd,dd->size,dd->one,Cudd_Not(dd->one));	    if (z[i] == NULL) goto endgame;	}    }    /* Create priority function BDD if needed. */    if (Pi == NULL) {	Pi = Pifunc(dd,n,x,y,z);	if (Pi == NULL) goto endgame;	createdPi = 1;	cuddRef(Pi);    }    /* Initialize abstraction cube. */    zcube = DD_ONE(dd);    cuddRef(zcube);    for (i = n - 1; i >= 0; i--) {	DdNode *tmpp;	tmpp = Cudd_bddAnd(dd,z[i],zcube);	if (tmpp == NULL) goto endgame;	cuddRef(tmpp);	Cudd_RecursiveDeref(dd,zcube);	zcube = tmpp;    }    /* Compute subset of (x,y) pairs. */    Rxz = Cudd_bddSwapVariables(dd,R,y,z,n);//.........这里部分代码省略.........

/**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;    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(stdout,"Cudd_Cofactor: Invalid restriction 2/n");	    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);	}	cuddDeref(t);	cuddDeref(e);    }//.........这里部分代码省略.........

/**Function********************************************************************  Synopsis    [Generates a BDD for the function d(x,y) > d(y,z).]  Description [This function generates a BDD for the function d(x,y)  > d(y,z);  x, y, and z are N-bit numbers, x/[0/] x/[1/] ... x/[N-1/],  y/[0/] y/[1/] ...  y/[N-1/], and z/[0/] z/[1/] ...  z/[N-1/],  with 0 the most significant bit.  The distance d(x,y) is defined as:	/sum_{i=0}^{N-1}(|x_i - y_i| /cdot 2^{N-i-1}).  The BDD is built bottom-up.  It has 7*N-3 internal nodes, if the variables are ordered as follows:   x/[0/] y/[0/] z/[0/] x/[1/] y/[1/] z/[1/] ... x/[N-1/] y/[N-1/] z/[N-1/]. ]  SideEffects [None]  SeeAlso     [Cudd_PrioritySelect Cudd_Dxygtdxz Cudd_Xgty Cudd_bddAdjPermuteX]******************************************************************************/DdNode *Cudd_Dxygtdyz(  DdManager * dd /* DD manager */,  int  N /* number of x, y, and z variables */,  DdNode ** x /* array of x variables */,  DdNode ** y /* array of y variables */,  DdNode ** z /* array of z variables */){    DdNode *one, *zero;    DdNode *z1, *z2, *z3, *z4, *y1_, *y2, *x1;    int     i;    one = DD_ONE(dd);    zero = Cudd_Not(one);    /* Build bottom part of BDD outside loop. */    y1_ = Cudd_bddIte(dd, y[N-1], one, z[N-1]);    if (y1_ == NULL) return(NULL);    cuddRef(y1_);    y2 = Cudd_bddIte(dd, y[N-1], z[N-1], zero);    if (y2 == NULL) {	Cudd_RecursiveDeref(dd, y1_);	return(NULL);    }    cuddRef(y2);    x1 = Cudd_bddIte(dd, x[N-1], y1_, Cudd_Not(y2));    if (x1 == NULL) {	Cudd_RecursiveDeref(dd, y1_);	Cudd_RecursiveDeref(dd, y2);	return(NULL);    }    cuddRef(x1);    Cudd_RecursiveDeref(dd, y1_);    Cudd_RecursiveDeref(dd, y2);    /* Loop to build the rest of the BDD. */    for (i = N-2; i >= 0; i--) {	z1 = Cudd_bddIte(dd, z[i], x1, zero);	if (z1 == NULL) {	    Cudd_RecursiveDeref(dd, x1);	    return(NULL);	}	cuddRef(z1);	z2 = Cudd_bddIte(dd, z[i], x1, one);	if (z2 == NULL) {	    Cudd_RecursiveDeref(dd, x1);	    Cudd_RecursiveDeref(dd, z1);	    return(NULL);	}	cuddRef(z2);	z3 = Cudd_bddIte(dd, z[i], one, x1);	if (z3 == NULL) {	    Cudd_RecursiveDeref(dd, x1);	    Cudd_RecursiveDeref(dd, z1);	    Cudd_RecursiveDeref(dd, z2);	    return(NULL);	}	cuddRef(z3);	z4 = Cudd_bddIte(dd, z[i], one, Cudd_Not(x1));	if (z4 == NULL) {	    Cudd_RecursiveDeref(dd, x1);	    Cudd_RecursiveDeref(dd, z1);	    Cudd_RecursiveDeref(dd, z2);	    Cudd_RecursiveDeref(dd, z3);	    return(NULL);	}	cuddRef(z4);	Cudd_RecursiveDeref(dd, x1);	y1_ = Cudd_bddIte(dd, y[i], z2, z1);	if (y1_ == NULL) {	    Cudd_RecursiveDeref(dd, z1);	    Cudd_RecursiveDeref(dd, z2);	    Cudd_RecursiveDeref(dd, z3);	    Cudd_RecursiveDeref(dd, z4);	    return(NULL);	}	cuddRef(y1_);	y2 = Cudd_bddIte(dd, y[i], z4, Cudd_Not(z3));	if (y2 == NULL) {	    Cudd_RecursiveDeref(dd, z1);//.........这里部分代码省略.........

/**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)) {	if (!st_lookup(mtable, Nv, &dummy)) return(NULL);	numT = *dummy/(2*(1<<index));    } else if (Nv == one) {	numT = max/(2*(1<<index));    } else {	numT = 0;    }      if (!Cudd_IsConstant(Nnv)) {	if (!st_lookup(mtable, Nnv, &dummy)) return(NULL);	numE = *dummy/(2*(1<<index));    } else if (Nnv == one) {	numE = max/(2*(1<<index));    } else {	numE = 0;//.........这里部分代码省略.........

/**Function********************************************************************  Synopsis    [Implements the recursive step of Cudd_SolveEqn.]  Description [Implements the recursive step of Cudd_SolveEqn.   Returns NULL if the intermediate solution blows up  or reordering occurs. The parametric solutions are  stored in the array G.]  SideEffects [none]  SeeAlso     [Cudd_SolveEqn, Cudd_VerifySol]******************************************************************************/DdNode *cuddSolveEqnRecur(  DdManager * bdd,  DdNode * F /* the left-hand side of the equation */,  DdNode * Y /* the cube of remaining y variables */,  DdNode ** G /* the array of solutions */,  int  n /* number of unknowns */,  int * yIndex /* array holding the y variable indices */,  int  i /* level of recursion */){    DdNode *Fn, *Fm1, *Fv, *Fvbar, *T, *w, *nextY, *one;    DdNodePtr *variables;    int j;    statLine(bdd);    variables = bdd->vars;    one = DD_ONE(bdd);    /* Base condition. */    if (Y == one) {	return F;    }    /* Cofactor of Y. */    yIndex[i] = Y->index;    nextY = Cudd_T(Y);    /* Universal abstraction of F with respect to the top variable index. */    Fm1 = cuddBddExistAbstractRecur(bdd, Cudd_Not(F), variables[yIndex[i]]);    if (Fm1) {	Fm1 = Cudd_Not(Fm1);	cuddRef(Fm1);    } else {	return(NULL);    }    Fn = cuddSolveEqnRecur(bdd, Fm1, nextY, G, n, yIndex, i+1);    if (Fn) {	cuddRef(Fn);    } else {	Cudd_RecursiveDeref(bdd, Fm1);	return(NULL);    }    Fv = cuddCofactorRecur(bdd, F, variables[yIndex[i]]);    if (Fv) {	cuddRef(Fv);    } else {	Cudd_RecursiveDeref(bdd, Fm1);	Cudd_RecursiveDeref(bdd, Fn);	return(NULL);    }    Fvbar = cuddCofactorRecur(bdd, F, Cudd_Not(variables[yIndex[i]]));    if (Fvbar) {	cuddRef(Fvbar);    } else {	Cudd_RecursiveDeref(bdd, Fm1);	Cudd_RecursiveDeref(bdd, Fn);	Cudd_RecursiveDeref(bdd, Fv);	return(NULL);    }    /* Build i-th component of the solution. */    w = cuddBddIteRecur(bdd, variables[yIndex[i]], Cudd_Not(Fv), Fvbar);    if (w) {	cuddRef(w);    } else {	Cudd_RecursiveDeref(bdd, Fm1);	Cudd_RecursiveDeref(bdd, Fn);	Cudd_RecursiveDeref(bdd, Fv);	Cudd_RecursiveDeref(bdd, Fvbar);	return(NULL);    }    T = cuddBddRestrictRecur(bdd, w, Cudd_Not(Fm1));    if(T) {	cuddRef(T);    } else {	Cudd_RecursiveDeref(bdd, Fm1);	Cudd_RecursiveDeref(bdd, Fn);	Cudd_RecursiveDeref(bdd, Fv);	Cudd_RecursiveDeref(bdd, Fvbar);	Cudd_RecursiveDeref(bdd, w);	return(NULL);//.........这里部分代码省略.........

/**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);//.........这里部分代码省略.........

//.........这里部分代码省略.........    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);	}    } else {	gt = ge = g;    }    if (topcube == top) {	Cube = cuddT(cube);    } else {	Cube = cube;    }    t = cuddBddClipAndAbsRecur(manager, ft, gt, Cube, distance, direction);    if (t == NULL) return(NULL);    /* Special case: 1 OR anything = 1. Hence, no need to compute    ** the else branch if t is 1.    */    if (t == one && topcube == top) {	if (F->ref != 1 || G->ref != 1)	    cuddCacheInsert(manager, cacheTag, f, g, cube, one);	return(one);    }    cuddRef(t);    e = cuddBddClipAndAbsRecur(manager, fe, ge, Cube, distance, direction);    if (e == NULL) {	Cudd_RecursiveDeref(manager, t);	return(NULL);    }    cuddRef(e);    if (topcube == top) {	/* abstract */	r = cuddBddClippingAndRecur(manager, Cudd_Not(t), Cudd_Not(e),				    distance, (direction == 0));	if (r == NULL) {	    Cudd_RecursiveDeref(manager, t);	    Cudd_RecursiveDeref(manager, e);	    return(NULL);	}	r = Cudd_Not(r);	cuddRef(r);	Cudd_RecursiveDeref(manager, t);	Cudd_RecursiveDeref(manager, e);	cuddDeref(r);    } else if (t == e) {	r = t;	cuddDeref(t);	cuddDeref(e);    } else {	if (Cudd_IsComplement(t)) {	    r = cuddUniqueInter(manager,(int)index,Cudd_Not(t),Cudd_Not(e));	    if (r == NULL) {		Cudd_RecursiveDeref(manager, t);		Cudd_RecursiveDeref(manager, e);		return(NULL);	    }	    r = Cudd_Not(r);	} else {	    r = cuddUniqueInter(manager,(int)index,t,e);	    if (r == NULL) {		Cudd_RecursiveDeref(manager, t);		Cudd_RecursiveDeref(manager, e);		return(NULL);	    }	}	cuddDeref(e);	cuddDeref(t);    }    if (F->ref != 1 || G->ref != 1)	cuddCacheInsert(manager, cacheTag, f, g, cube, r);    return (r);} /* end of cuddBddClipAndAbsRecur */

/**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 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    [Writes a blif file representing the argument BDDs.]  Description [Writes a blif file representing the argument BDDs as a  network of multiplexers. One multiplexer is written for each BDD  node. It returns 1 in case of success; 0 otherwise (e.g.,  out-of-memory, file system full, or an ADD with constants different  from 0 and 1).  Cudd_DumpBlif does not close the file: This is the  caller responsibility. Cudd_DumpBlif uses a minimal unique subset of  the hexadecimal address of a node as name for it.  If the argument  inames is non-null, it is assumed to hold the pointers to the names  of the inputs. Similarly for onames.]  SideEffects [None]  SeeAlso     [Cudd_DumpBlifBody Cudd_DumpDot Cudd_PrintDebug Cudd_DumpDDcal  Cudd_DumpDaVinci Cudd_DumpFactoredForm]******************************************************************************/intCudd_DumpBlif(  DdManager * dd /* manager */,  int  n /* number of output nodes to be dumped */,  DdNode ** f /* array of output nodes to be dumped */,  char ** inames /* array of input names (or NULL) */,  char ** onames /* array of output names (or NULL) */,  char * mname /* model name (or NULL) */,  FILE * fp /* pointer to the dump file */,  int mv /* 0: blif, 1: blif-MV */){    DdNode	*support = NULL;    DdNode	*scan;    int		*sorted = NULL;    int		nvars = dd->size;    int		retval;    int		i;    /* Build a bit array with the support of f. */    sorted = ALLOC(int,nvars);    if (sorted == NULL) {	dd->errorCode = CUDD_MEMORY_OUT;	goto failure;    }    for (i = 0; i < nvars; i++) sorted[i] = 0;    /* Take the union of the supports of each output function. */    support = Cudd_VectorSupport(dd,f,n);    if (support == NULL) goto failure;    cuddRef(support);    scan = support;    while (!cuddIsConstant(scan)) {	sorted[scan->index] = 1;	scan = cuddT(scan);    }    Cudd_RecursiveDeref(dd,support);    support = NULL; /* so that we do not try to free it in case of failure */    /* Write the header (.model .inputs .outputs). */    if (mname == NULL) {	retval = fprintf(fp,".model DD/n.inputs");    } else {	retval = fprintf(fp,".model %s/n.inputs",mname);    }    if (retval == EOF) {	FREE(sorted);	return(0);    }    /* Write the input list by scanning the support array. */    for (i = 0; i < nvars; i++) {	if (sorted[i]) {	    if (inames == NULL) {		retval = fprintf(fp," %d", i);	    } else {		retval = fprintf(fp," %s", inames[i]);	    }	    if (retval == EOF) goto failure;	}    }    FREE(sorted);    sorted = NULL;    /* Write the .output line. */    retval = fprintf(fp,"/n.outputs");    if (retval == EOF) goto failure;    for (i = 0; i < n; i++) {	if (onames == NULL) {	    retval = fprintf(fp," f%d", i);	} else {	    retval = fprintf(fp," %s", onames[i]);	}	if (retval == EOF) goto failure;    }    retval = fprintf(fp,"/n");    if (retval == EOF) goto failure;    retval = Cudd_DumpBlifBody(dd, n, f, inames, onames, fp, mv);    if (retval == 0) goto failure;//.........这里部分代码省略.........

/**Function********************************************************************  Synopsis    [Tests Walsh matrix multiplication.]  Description [Tests Walsh matrix multiplication.  Return 1 if successful;  0 otherwise.]  SideEffects [May create new variables in the manager.]  SeeAlso     []******************************************************************************/static inttestWalsh(  DdManager *dd /* manager */,  int N /* number of variables */,  int cmu /* use CMU approach to matrix multiplication */,  int approach /* reordering approach */,  int pr /* verbosity level */){    DdNode *walsh1, *walsh2, *wtw;    DdNode **x, **v, **z;    int i, retval;    DdNode *_true = DD_TRUE(dd);    DdNode *_false = DD_FALSE(dd);    if (N > 3) {	x = ALLOC(DdNode *,N);	v = ALLOC(DdNode *,N);	z = ALLOC(DdNode *,N);	for (i = N-1; i >= 0; i--) {	    Cudd_Ref(x[i]=cuddUniqueInter(dd,3*i,_true,_false));	    Cudd_Ref(v[i]=cuddUniqueInter(dd,3*i+1,_true,_false));	    Cudd_Ref(z[i]=cuddUniqueInter(dd,3*i+2,_true,_false));	}	Cudd_Ref(walsh1 = Cudd_addWalsh(dd,v,z,N));	if (pr>0) {(void) printf("walsh1"); Cudd_PrintDebug(dd,walsh1,2*N,pr);}	Cudd_Ref(walsh2 = Cudd_addWalsh(dd,x,v,N));	if (cmu) {	    Cudd_Ref(wtw = Cudd_addTimesPlus(dd,walsh2,walsh1,v,N));	} else {	    Cudd_Ref(wtw = Cudd_addMatrixMultiply(dd,walsh2,walsh1,v,N));	}	if (pr>0) {(void) printf("wtw"); Cudd_PrintDebug(dd,wtw,2*N,pr);}	if (approach != CUDD_REORDER_NONE) {#ifdef DD_DEBUG	    retval = Cudd_DebugCheck(dd);	    if (retval != 0) {		(void) fprintf(stderr,"Error reported by Cudd_DebugCheck/n");		return(0);	    }#endif	    retval = Cudd_ReduceHeap(dd,(Cudd_ReorderingType)approach,5);	    if (retval == 0) {		(void) fprintf(stderr,"Error reported by Cudd_ReduceHeap/n");		return(0);	    }#ifdef DD_DEBUG	    retval = Cudd_DebugCheck(dd);	    if (retval != 0) {		(void) fprintf(stderr,"Error reported by Cudd_DebugCheck/n");		return(0);	    }#endif	    if (approach == CUDD_REORDER_SYMM_SIFT ||	    approach == CUDD_REORDER_SYMM_SIFT_CONV) {		Cudd_SymmProfile(dd,0,dd->size-1);	    }	}	/* Clean up. */	Cudd_RecursiveDeref(dd, wtw);	Cudd_RecursiveDeref(dd, walsh1);	Cudd_RecursiveDeref(dd, walsh2);	for (i=0; i < N; i++) {	    Cudd_RecursiveDeref(dd, x[i]);	    Cudd_RecursiveDeref(dd, v[i]);	    Cudd_RecursiveDeref(dd, z[i]);	}	FREE(x);	FREE(v);	FREE(z);    }

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

static inline void     Aig_ObjCleanGlobalBdd( DdManager * dd, Aig_Obj_t * pObj ) { Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData ); pObj->pData = NULL; }

/**Function********************************************************************  Synopsis    [Computes shortest paths in a state graph.]  Description [Computes shortest paths in the state transition graph of  a network.  Three methods are availabe:  <ul>  <li> Bellman-Ford algorithm for single-source shortest paths; the  algorithm computes the distance (number of transitions) from the initial  states to all states.  <li> Floyd-Warshall algorithm for all-pair shortest paths.  <li> Repeated squaring algorithm for all-pair shortest paths.  </ul>  The function returns 1 in case of success; 0 otherwise.  ]  SideEffects [ADD variables are created in the manager.]  SeeAlso     []******************************************************************************/intNtr_ShortestPaths(  DdManager * dd,  BnetNetwork * net,  NtrOptions * option){    NtrPartTR *TR;    DdNode *edges, *source, *res, *r, *q, *bddSource;    DdNode **xadd, **yadd, **zadd;    int i;    int pr = option->verb;    int algorithm = option->shortPath;    int selectiveTrace = option->selectiveTrace;    int nvars = net->nlatches;    /* Set background to infinity for shortest paths. */    Cudd_SetBackground(dd,Cudd_ReadPlusInfinity(dd));    /* Build the monolithic TR. */    TR = Ntr_buildTR(dd,net,option,NTR_IMAGE_MONO);    /* Build the ADD variable vectors for x and y. */    xadd = ALLOC(DdNode *, nvars);    yadd = ALLOC(DdNode *, nvars);    for(i = 0; i < nvars; i++) {	q = Cudd_addIthVar(dd,TR->x[i]->index);	Cudd_Ref(q);	xadd[i] = q;	q = Cudd_addIthVar(dd,TR->y[i]->index);	Cudd_Ref(q);	yadd[i] = q;    }    /* Convert the transition relation BDD into an ADD... */    q = Cudd_BddToAdd(dd,TR->part[0]);    Cudd_Ref(q);    /* ...replacing zeroes with infinities... */    r = Cudd_addIte(dd,q,Cudd_ReadOne(dd),Cudd_ReadPlusInfinity(dd));    Cudd_Ref(r);    Cudd_RecursiveDeref(dd,q);    /* ...and zeroing the diagonal. */    q = Cudd_addXeqy(dd,nvars,xadd,yadd);    Cudd_Ref(q);    edges = Cudd_addIte(dd,q,Cudd_ReadZero(dd),r);    Cudd_Ref(edges);    Cudd_RecursiveDeref(dd,r);    Cudd_RecursiveDeref(dd,q);    switch(algorithm) {    case NTR_SHORT_BELLMAN:	bddSource = Ntr_initState(dd,net,option);	source = Cudd_BddToAdd(dd,bddSource);	Cudd_Ref(source);	res = ntrBellman(dd,edges,source,xadd,yadd,nvars,pr);	if (res == NULL) return(0);	Cudd_Ref(res);	Cudd_RecursiveDeref(dd,source);	Cudd_RecursiveDeref(dd,bddSource);	if (pr >= 0) {	    (void) fprintf(stdout,"Distance Matrix");	    Cudd_PrintDebug(dd,res,nvars,pr);	}	break;    case NTR_SHORT_FLOYD:	res = ntrWarshall(dd,edges,xadd,yadd,nvars,pr);	if (res == NULL) return(0);	Cudd_Ref(res);	if (pr >= 0) {	    (void) fprintf(stdout,"Distance Matrix");	    Cudd_PrintDebug(dd,res,2*nvars,pr);	}	break;    case NTR_SHORT_SQUARE:	/* Create a third set of ADD variables. */	zadd = ALLOC(DdNode *, nvars);	for(i = 0; i < nvars; i++) {	    int level;	    level = Cudd_ReadIndex(dd,TR->x[i]->index);	    q = Cudd_addNewVarAtLevel(dd,level);//.........这里部分代码省略.........