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

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

/**Function********************************************************************  Synopsis    [Creates the symmetry information structure from ZDD.]  Description [ZDD representation of symmetries is the set of cubes, each  of which has two variables in the positive polarity. These variables correspond  to the symmetric variable pair.]  SideEffects []  SeeAlso     []******************************************************************************/Extra_SymmInfo_t * Extra_SymmPairsCreateFromZdd( DdManager * dd, DdNode * zPairs, DdNode * bSupp ){    int i;    int nSuppSize;    Extra_SymmInfo_t * p;    int * pMapVars2Nums;    DdNode * bTemp;    DdNode * zSet, * zCube, * zTemp;    int iVar1, iVar2;    nSuppSize = Extra_bddSuppSize( dd, bSupp );    // allocate and clean the storage for symmetry info    p = Extra_SymmPairsAllocate( nSuppSize );    // allocate the storage for the temporary map    pMapVars2Nums = ABC_ALLOC( int, dd->size );    memset( pMapVars2Nums, 0, dd->size * sizeof(int) );    // assign the variables    p->nVarsMax = dd->size;//  p->nNodes   = Cudd_DagSize( zPairs );    p->nNodes   = 0;    for ( i = 0, bTemp = bSupp; bTemp != b1; bTemp = cuddT(bTemp), i++ )    {        p->pVars[i] = bTemp->index;        pMapVars2Nums[bTemp->index] = i;    }    // write the symmetry info into the structure    zSet = zPairs;   Cudd_Ref( zSet );    while ( zSet != z0 )    {        // get the next cube        zCube  = Extra_zddSelectOneSubset( dd, zSet );    Cudd_Ref( zCube );        // add these two variables to the data structure        assert( cuddT( cuddT(zCube) ) == z1 );        iVar1 = zCube->index/2;        iVar2 = cuddT(zCube)->index/2;        if ( pMapVars2Nums[iVar1] < pMapVars2Nums[iVar2] )            p->pSymms[ pMapVars2Nums[iVar1] ][ pMapVars2Nums[iVar2] ] = 1;        else            p->pSymms[ pMapVars2Nums[iVar2] ][ pMapVars2Nums[iVar1] ] = 1;        // count the symmetric pairs        p->nSymms ++;        // update the cuver and deref the cube        zSet = Cudd_zddDiff( dd, zTemp = zSet, zCube );     Cudd_Ref( zSet );        Cudd_RecursiveDerefZdd( dd, zTemp );        Cudd_RecursiveDerefZdd( dd, zCube );    } // for each cube     Cudd_RecursiveDerefZdd( dd, zSet );    ABC_FREE( pMapVars2Nums );    return p;} /* end of Extra_SymmPairsCreateFromZdd */

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

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

/**Function*************************************************************  Synopsis    []  Description []  SideEffects []  SeeAlso     []***********************************************************************/DdNode * Extra_bddSpaceEquations( DdManager * dd, DdNode * bSpace ){    DdNode * zRes;	DdNode * zEquPos;	DdNode * zEquNeg;	zEquPos = Extra_bddSpaceEquationsPos( dd, bSpace );  Cudd_Ref( zEquPos );	zEquNeg = Extra_bddSpaceEquationsNeg( dd, bSpace );  Cudd_Ref( zEquNeg );	zRes    = Cudd_zddUnion( dd, zEquPos, zEquNeg );     Cudd_Ref( zRes );	Cudd_RecursiveDerefZdd( dd, zEquPos );	Cudd_RecursiveDerefZdd( dd, zEquNeg );	Cudd_Deref( zRes );    return zRes;}

/**Function********************************************************************  Synopsis    [Performs a recursive step of Extra_zddGetSingletons.]  Description [Returns the set of ZDD singletons, containing those positive   polarity ZDD variables that correspond to the BDD variables in bVars.]  SideEffects []  SeeAlso     []******************************************************************************/DdNode * extraZddGetSingletons(   DdManager * dd,    /* the DD manager */  DdNode * bVars)    /* the set of variables */{    DdNode * zRes;    if ( bVars == b1 )//    if ( bVars == b0 )  // bug fixed by Jin Zhang, Jan 23, 2004        return z1;    if ( (zRes = cuddCacheLookup1Zdd(dd, extraZddGetSingletons, bVars)) )        return zRes;    else    {        DdNode * zTemp, * zPlus;                  // solve subproblem        zRes = extraZddGetSingletons( dd, cuddT(bVars) );        if ( zRes == NULL )             return NULL;        cuddRef( zRes );                zPlus = cuddZddGetNode( dd, 2*bVars->index, z1, z0 );        if ( zPlus == NULL )         {            Cudd_RecursiveDerefZdd( dd, zRes );            return NULL;        }        cuddRef( zPlus );        // add these to the result        zRes = cuddZddUnion( dd, zTemp = zRes, zPlus );        if ( zRes == NULL )        {            Cudd_RecursiveDerefZdd( dd, zTemp );            Cudd_RecursiveDerefZdd( dd, zPlus );            return NULL;        }        cuddRef( zRes );        Cudd_RecursiveDerefZdd( dd, zTemp );        Cudd_RecursiveDerefZdd( dd, zPlus );        cuddDeref( zRes );        cuddCacheInsert1( dd, extraZddGetSingletons, bVars, zRes );        return zRes;    }}   /* end of extraZddGetSingletons */

static void unreference_dd(shadow_mgr mgr, DdNode *n, dd_type_t dtype) {    if (!mgr->do_cudd)	return;    if (dtype == IS_ZDD) {	Cudd_RecursiveDerefZdd(mgr->bdd_manager, n);    } else {	Cudd_RecursiveDeref(mgr->bdd_manager, n);    }}

/**Function********************************************************************  Synopsis    [Frees the ZDD universe.]  Description [Frees the ZDD universe.]  SideEffects [None]  SeeAlso     [cuddZddInitUniv]******************************************************************************/voidcuddZddFreeUniv(  DdManager * zdd){    if (zdd->univ) {	Cudd_RecursiveDerefZdd(zdd, zdd->univ[0]);	FREE(zdd->univ);    }} /* end of cuddZddFreeUniv */

/** * @brief Basic test of ZDDs. * @return 0 if successful; -1 otherwise. */static inttestZdd(int verbosity){    DdManager *manager;    DdNode *f, *var, *tmp;    int i, ret;    manager = Cudd_Init(0,4,CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS,0);    if (!manager) {        if (verbosity) {            printf("initialization failed/n");        }        return -1;    }    tmp = Cudd_ReadZddOne(manager,0);    Cudd_Ref(tmp);    for (i = 3; i >= 0; i--) {        var = Cudd_zddIthVar(manager,i);        Cudd_Ref(var);        f = Cudd_zddIntersect(manager,var,tmp);        Cudd_Ref(f);        Cudd_RecursiveDerefZdd(manager,tmp);        Cudd_RecursiveDerefZdd(manager,var);        tmp = f;    }    f = Cudd_zddDiff(manager,Cudd_ReadZddOne(manager,0),tmp);    Cudd_Ref(f);    Cudd_RecursiveDerefZdd(manager,tmp);    if (verbosity) {        Cudd_zddPrintMinterm(manager,f);        printf("/n");    }    Cudd_RecursiveDerefZdd(manager,f);    ret = Cudd_CheckZeroRef(manager);    if (ret != 0 && verbosity) {        printf("%d unexpected non-zero references/n", ret);    }    Cudd_Quit(manager);    return 0;}

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

/**Function********************************************************************  Synopsis    [Performs the recursive step of Extra_zddSelectOneSubset.]  Description []  SideEffects [None]  SeeAlso     []******************************************************************************/DdNode * extraZddSelectOneSubset(   DdManager * dd,   DdNode * zS )// selects one subset from the ZDD zS// returns z0 if and only if zS is an empty set of cubes{    DdNode * zRes;    if ( zS == z0 )    return z0;    if ( zS == z1 )    return z1;        // check cache    if ( (zRes = cuddCacheLookup1Zdd( dd, extraZddSelectOneSubset, zS )) )        return zRes;    else    {        DdNode * zS0, * zS1, * zTemp;         zS0 = cuddE(zS);        zS1 = cuddT(zS);        if ( zS0 != z0 )        {            zRes = extraZddSelectOneSubset( dd, zS0 );            if ( zRes == NULL )                return NULL;        }        else // if ( zS0 == z0 )        {            assert( zS1 != z0 );            zRes = extraZddSelectOneSubset( dd, zS1 );            if ( zRes == NULL )                return NULL;            cuddRef( zRes );            zRes = cuddZddGetNode( dd, zS->index, zTemp = zRes, z0 );            if ( zRes == NULL )             {                Cudd_RecursiveDerefZdd( dd, zTemp );                return NULL;            }            cuddDeref( zTemp );        }        // insert the result into cache        cuddCacheInsert1( dd, extraZddSelectOneSubset, zS, zRes );        return zRes;    }       } /* end of extraZddSelectOneSubset */

/**Function********************************************************************  Synopsis    [Initializes the ZDD universe.]  Description [Initializes the ZDD universe. Returns 1 if successful; 0  otherwise.]  SideEffects [None]  SeeAlso     [cuddZddFreeUniv]******************************************************************************/intcuddZddInitUniv(  DdManager * zdd){    DdNode	*p, *res;    int		i;#ifdef __osf__#pragma pointer_size save#pragma pointer_size short#endif    zdd->univ = ALLOC(DdNode *, zdd->sizeZ);#ifdef __osf__#pragma pointer_size restore#endif    if (zdd->univ == NULL) {	zdd->errorCode = CUDD_MEMORY_OUT;	return(0);    }    res = DD_ONE(zdd);    cuddRef(res);    for (i = zdd->sizeZ - 1; i >= 0; i--) {	unsigned int index = zdd->invpermZ[i];	p = res;	res = cuddUniqueInterZdd(zdd, index, p, p);	if (res == NULL) {	    Cudd_RecursiveDerefZdd(zdd,p);	    FREE(zdd->univ);	    return(0);	}	cuddRef(res);	cuddDeref(p);	zdd->univ[i] = res;    }#ifdef DD_VERBOSE    cuddZddP(zdd, zdd->univ[0]);#endif    return(1);} /* end of cuddZddInitUniv */

/**Function********************************************************************  Synopsis    [Computes the two-way decomposition of f w.r.t. v.]  Description []  SideEffects [The results are returned in f1 and f0.]  SeeAlso     [cuddZddGetCofactors3]******************************************************************************/intcuddZddGetCofactors2(  DdManager * dd,  DdNode * f,  int  v,  DdNode ** f1,  DdNode ** f0){    *f1 = cuddZddSubset1(dd, f, v);    if (*f1 == NULL)        return(1);    *f0 = cuddZddSubset0(dd, f, v);    if (*f0 == NULL) {        Cudd_RecursiveDerefZdd(dd, *f1);        return(1);    }    return(0);} /* end of cuddZddGetCofactors2 */

ABC_NAMESPACE_IMPL_START/*---------------------------------------------------------------------------*//* Constant declarations                                                     *//*---------------------------------------------------------------------------*//*---------------------------------------------------------------------------*//* Stucture declarations                                                     *//*---------------------------------------------------------------------------*//*---------------------------------------------------------------------------*//* Type declarations                                                         *//*---------------------------------------------------------------------------*//*---------------------------------------------------------------------------*//* Variable declarations                                                     *//*---------------------------------------------------------------------------*//*---------------------------------------------------------------------------*//* Macro declarations                                                        *//*---------------------------------------------------------------------------*/#define DD_GET_SYMM_VARS_TAG          0x0a /* former DD_BDD_XOR_EXIST_ABSTRACT_TAG *//**AutomaticStart*************************************************************//*---------------------------------------------------------------------------*//* Static function prototypes                                                *//*---------------------------------------------------------------------------*//**AutomaticEnd***************************************************************//*---------------------------------------------------------------------------*//* Definition of exported functions                                          *//*---------------------------------------------------------------------------*//**Function********************************************************************  Synopsis    [Computes the classical symmetry information for the function.]  Description [Returns the symmetry information in the form of Extra_SymmInfo_t structure.]  SideEffects [If the ZDD variables are not derived from BDD variables with  multiplicity 2, this function may derive them in a wrong way.]  SeeAlso     []******************************************************************************/Extra_SymmInfo_t * Extra_SymmPairsCompute(   DdManager * dd,   /* the manager */  DdNode * bFunc)   /* the function whose symmetries are computed */{    DdNode * bSupp;    DdNode * zRes;    Extra_SymmInfo_t * p;    bSupp = Cudd_Support( dd, bFunc );                      Cudd_Ref( bSupp );    zRes  = Extra_zddSymmPairsCompute( dd, bFunc, bSupp );  Cudd_Ref( zRes );    p = Extra_SymmPairsCreateFromZdd( dd, zRes, bSupp );    Cudd_RecursiveDeref( dd, bSupp );    Cudd_RecursiveDerefZdd( dd, zRes );    return p;} /* end of Extra_SymmPairsCompute */

/**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    [Performs the reordering-sensitive step of Extra_zddTupleFromBdd().]  Description [Generates in a bottom-up fashion ZDD for all combinations               composed of k variables out of variables belonging to Support.]  SideEffects []  SeeAlso     []******************************************************************************/DdNode* extraZddTuplesFromBdd(   DdManager * dd,   /* the DD manager */  DdNode * bVarsK,   /* the number of variables in tuples */  DdNode * bVarsN)   /* the set of all variables */{    DdNode *zRes, *zRes0, *zRes1;    statLine(dd);     /* terminal cases *//*  if ( k < 0 || k > n ) *      return dd->zero; *  if ( n == 0 ) *      return dd->one;  */    if ( cuddI( dd, bVarsK->index ) < cuddI( dd, bVarsN->index ) )        return z0;    if ( bVarsN == b1 )        return z1;    /* check cache */    zRes = cuddCacheLookup2Zdd(dd, extraZddTuplesFromBdd, bVarsK, bVarsN);    if (zRes)        return(zRes);    /* ZDD in which this variable is 0 *//*  zRes0 = extraZddTuplesFromBdd( dd, k,     n-1 ); */    zRes0 = extraZddTuplesFromBdd( dd, bVarsK, cuddT(bVarsN) );    if ( zRes0 == NULL )         return NULL;    cuddRef( zRes0 );    /* ZDD in which this variable is 1 *//*  zRes1 = extraZddTuplesFromBdd( dd, k-1,          n-1 ); */    if ( bVarsK == b1 )    {        zRes1 = z0;        cuddRef( zRes1 );    }    else    {        zRes1 = extraZddTuplesFromBdd( dd, cuddT(bVarsK), cuddT(bVarsN) );        if ( zRes1 == NULL )         {            Cudd_RecursiveDerefZdd( dd, zRes0 );            return NULL;        }        cuddRef( zRes1 );    }    /* compose Res0 and Res1 with the given ZDD variable */    zRes = cuddZddGetNode( dd, 2*bVarsN->index, zRes1, zRes0 );    if ( zRes == NULL )     {        Cudd_RecursiveDerefZdd( dd, zRes0 );        Cudd_RecursiveDerefZdd( dd, zRes1 );        return NULL;    }    cuddDeref( zRes0 );    cuddDeref( zRes1 );    /* insert the result into cache */    cuddCacheInsert2(dd, extraZddTuplesFromBdd, bVarsK, bVarsN, zRes);    return zRes;} /* end of extraZddTuplesFromBdd */

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

//.........这里部分代码省略.........    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 = cuddZddIsop(dd, Lsub0, Usub0, &zdd_Isub0);    if (Isub0 == NULL) {	Cudd_RecursiveDeref(dd, Lsub0);	Cudd_RecursiveDeref(dd, Lsub1);	return(NULL);    }    /*    if ((!cuddIsConstant(Cudd_Regular(Isub0))) &&	(Cudd_Regular(Isub0)->index != zdd_Isub0->index / 2 ||	dd->permZ[index * 2] > dd->permZ[zdd_Isub0->index])) {	printf("*** ERROR : illegal permutation in ZDD. ***/n");    }    */    Cudd_Ref(Isub0);    Cudd_Ref(zdd_Isub0);    Isub1 = cuddZddIsop(dd, Lsub1, Usub1, &zdd_Isub1);    if (Isub1 == NULL) {	Cudd_RecursiveDeref(dd, Lsub0);	Cudd_RecursiveDeref(dd, Lsub1);	Cudd_RecursiveDeref(dd, Isub0);	Cudd_RecursiveDerefZdd(dd, zdd_Isub0);	return(NULL);    }    /*    if ((!cuddIsConstant(Cudd_Regular(Isub1))) &&	(Cudd_Regular(Isub1)->index != zdd_Isub1->index / 2 ||	dd->permZ[index * 2] > dd->permZ[zdd_Isub1->index])) {	printf("*** ERROR : illegal permutation in ZDD. ***/n");    }    */    Cudd_Ref(Isub1);    Cudd_Ref(zdd_Isub1);    Cudd_RecursiveDeref(dd, Lsub0);    Cudd_RecursiveDeref(dd, Lsub1);    Lsuper0 = cuddBddAndRecur(dd, Lnv, Cudd_Not(Isub0));    if (Lsuper0 == NULL) {	Cudd_RecursiveDeref(dd, Isub0);	Cudd_RecursiveDerefZdd(dd, zdd_Isub0);	Cudd_RecursiveDeref(dd, Isub1);	Cudd_RecursiveDerefZdd(dd, zdd_Isub1);	return(NULL);    }    Cudd_Ref(Lsuper0);    Lsuper1 = cuddBddAndRecur(dd, Lv, Cudd_Not(Isub1));    if (Lsuper1 == NULL) {	Cudd_RecursiveDeref(dd, Isub0);	Cudd_RecursiveDerefZdd(dd, zdd_Isub0);	Cudd_RecursiveDeref(dd, Isub1);	Cudd_RecursiveDerefZdd(dd, zdd_Isub1);	Cudd_RecursiveDeref(dd, Lsuper0);	return(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    [Computes the three-way decomposition of f w.r.t. v.]  Description [Computes the three-way decomposition of function f (represented  by a ZDD) wit respect to variable v.  Returns 0 if successful; 1 otherwise.]  SideEffects [The results are returned in f1, f0, and fd.]  SeeAlso     [cuddZddGetCofactors2]******************************************************************************/intcuddZddGetCofactors3(  DdManager * dd,  DdNode * f,  int  v,  DdNode ** f1,  DdNode ** f0,  DdNode ** fd){    DdNode      *pc, *nc;    DdNode      *zero = DD_ZERO(dd);    int         top, hv, ht, pv, nv;    int         level;    top = dd->permZ[f->index];    level = dd->permZ[v];    hv = level >> 1;    ht = top >> 1;    if (hv < ht) {        *f1 = zero;        *f0 = zero;        *fd = f;    }    else {        pv = cuddZddGetPosVarIndex(dd, v);        nv = cuddZddGetNegVarIndex(dd, v);        /* not to create intermediate ZDD node */        if (cuddZddGetPosVarLevel(dd, v) < cuddZddGetNegVarLevel(dd, v)) {            pc = cuddZddSubset1(dd, f, pv);            if (pc == NULL)                return(1);            Cudd_Ref(pc);            nc = cuddZddSubset0(dd, f, pv);            if (nc == NULL) {                Cudd_RecursiveDerefZdd(dd, pc);                return(1);            }            Cudd_Ref(nc);            *f1 = cuddZddSubset0(dd, pc, nv);            if (*f1 == NULL) {                Cudd_RecursiveDerefZdd(dd, pc);                Cudd_RecursiveDerefZdd(dd, nc);                return(1);            }            Cudd_Ref(*f1);            *f0 = cuddZddSubset1(dd, nc, nv);            if (*f0 == NULL) {                Cudd_RecursiveDerefZdd(dd, pc);                Cudd_RecursiveDerefZdd(dd, nc);                Cudd_RecursiveDerefZdd(dd, *f1);                return(1);            }            Cudd_Ref(*f0);            *fd = cuddZddSubset0(dd, nc, nv);            if (*fd == NULL) {                Cudd_RecursiveDerefZdd(dd, pc);                Cudd_RecursiveDerefZdd(dd, nc);                Cudd_RecursiveDerefZdd(dd, *f1);                Cudd_RecursiveDerefZdd(dd, *f0);                return(1);            }            Cudd_Ref(*fd);        } else {            pc = cuddZddSubset1(dd, f, nv);            if (pc == NULL)                return(1);            Cudd_Ref(pc);            nc = cuddZddSubset0(dd, f, nv);            if (nc == NULL) {                Cudd_RecursiveDerefZdd(dd, pc);                return(1);            }            Cudd_Ref(nc);            *f0 = cuddZddSubset0(dd, pc, pv);            if (*f0 == NULL) {                Cudd_RecursiveDerefZdd(dd, pc);                Cudd_RecursiveDerefZdd(dd, nc);                return(1);            }            Cudd_Ref(*f0);            *f1 = cuddZddSubset1(dd, nc, pv);            if (*f1 == NULL) {                Cudd_RecursiveDerefZdd(dd, pc);//.........这里部分代码省略.........

/**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_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 Extra_bddSpaceEquationsNev().]  Description []  SideEffects []  SeeAlso     []***********************************************************************/DdNode * extraBddSpaceEquationsNeg( DdManager * dd, DdNode * bF ){	DdNode * zRes;	statLine( dd );	if ( bF == b0 )		return z1;	if ( bF == b1 )		return z0;	    if ( (zRes = cuddCacheLookup1Zdd(dd, extraBddSpaceEquationsNeg, bF)) )    	return zRes;	else	{		DdNode * bFR, * bF0,  * bF1;		DdNode * zPos0, * zPos1, * zNeg1; 		DdNode * zRes, * zRes0, * zRes1;		bFR = Cudd_Regular(bF);		if ( bFR != bF ) // bF is complemented 		{			bF0 = Cudd_Not( cuddE(bFR) );			bF1 = Cudd_Not( cuddT(bFR) );		}		else		{			bF0 = cuddE(bFR);			bF1 = cuddT(bFR);		}		if ( bF0 == b0 )		{			zRes = extraBddSpaceEquationsNeg( dd, bF1 );			if ( zRes == NULL )				return NULL;		}		else if ( bF1 == b0 )		{			zRes0 = extraBddSpaceEquationsNeg( dd, bF0 );			if ( zRes0 == NULL )				return NULL;			cuddRef( zRes0 );			// add the current element to the set			zRes = cuddZddGetNode( dd, 2*bFR->index, z1, zRes0 );			if ( zRes == NULL ) 			{				Cudd_RecursiveDerefZdd(dd, zRes0);				return NULL;			}			cuddDeref( zRes0 );		}		else		{			zPos0 = extraBddSpaceEquationsNeg( dd, bF0 );			if ( zPos0 == NULL )				return NULL;			cuddRef( zPos0 );			zPos1 = extraBddSpaceEquationsNeg( dd, bF1 );			if ( zPos1 == NULL )			{				Cudd_RecursiveDerefZdd(dd, zPos0);				return NULL;			}			cuddRef( zPos1 );			zNeg1 = extraBddSpaceEquationsPos( dd, bF1 );			if ( zNeg1 == NULL )			{				Cudd_RecursiveDerefZdd(dd, zPos0);				Cudd_RecursiveDerefZdd(dd, zPos1);				return NULL;			}			cuddRef( zNeg1 );			zRes0 = cuddZddIntersect( dd, zPos0, zPos1 );			if ( zRes0 == NULL )			{				Cudd_RecursiveDerefZdd(dd, zNeg1);				Cudd_RecursiveDerefZdd(dd, zPos0);				Cudd_RecursiveDerefZdd(dd, zPos1);				return NULL;			}			cuddRef( zRes0 );			zRes1 = cuddZddIntersect( dd, zPos0, zNeg1 );			if ( zRes1 == NULL )//.........这里部分代码省略.........

/**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 a recursive step of Extra_SymmPairsCompute.]  Description [Returns the set of symmetric variable pairs represented as a set   of two-literal ZDD cubes. Both variables always appear in the positive polarity  in the cubes. This function works without building new BDD nodes. Some relatively   small number of ZDD nodes may be built to ensure proper bookkeeping of the   symmetry information.]  SideEffects []  SeeAlso     []******************************************************************************/DdNode * extraZddSymmPairsCompute(   DdManager * dd,   /* the manager */  DdNode * bFunc,   /* the function whose symmetries are computed */  DdNode * bVars )  /* the set of variables on which this function depends */{    DdNode * zRes;    DdNode * bFR = Cudd_Regular(bFunc);     if ( cuddIsConstant(bFR) )    {        int nVars, i;        // determine how many vars are in the bVars        nVars = Extra_bddSuppSize( dd, bVars );        if ( nVars < 2 )            return z0;        else        {            DdNode * bVarsK;            // create the BDD bVarsK corresponding to K = 2;            bVarsK = bVars;            for ( i = 0; i < nVars-2; i++ )                bVarsK = cuddT( bVarsK );            return extraZddTuplesFromBdd( dd, bVarsK, bVars );        }    }    assert( bVars != b1 );    if ( (zRes = cuddCacheLookup2Zdd(dd, extraZddSymmPairsCompute, bFunc, bVars)) )        return zRes;    else    {        DdNode * zRes0, * zRes1;        DdNode * zTemp, * zPlus, * zSymmVars;                     DdNode * bF0, * bF1;                     DdNode * bVarsNew;        int nVarsExtra;        int LevelF;        // every variable in bF should be also in bVars, therefore LevelF cannot be above LevelV        // if LevelF is below LevelV, scroll through the vars in bVars to the same level as F        // count how many extra vars are there in bVars        nVarsExtra = 0;        LevelF = dd->perm[bFR->index];        for ( bVarsNew = bVars; LevelF > dd->perm[bVarsNew->index]; bVarsNew = cuddT(bVarsNew) )            nVarsExtra++;         // the indexes (level) of variables should be synchronized now        assert( bFR->index == bVarsNew->index );        // cofactor the function        if ( bFR != bFunc ) // bFunc is complemented         {            bF0 = Cudd_Not( cuddE(bFR) );            bF1 = Cudd_Not( cuddT(bFR) );        }        else        {            bF0 = cuddE(bFR);            bF1 = cuddT(bFR);        }        // solve subproblems        zRes0 = extraZddSymmPairsCompute( dd, bF0, cuddT(bVarsNew) );        if ( zRes0 == NULL )            return NULL;        cuddRef( zRes0 );        // if there is no symmetries in the negative cofactor        // there is no need to test the positive cofactor        if ( zRes0 == z0 )            zRes = zRes0;  // zRes takes reference        else        {            zRes1 = extraZddSymmPairsCompute( dd, bF1, cuddT(bVarsNew) );            if ( zRes1 == NULL )            {                Cudd_RecursiveDerefZdd( dd, zRes0 );                return NULL;            }            cuddRef( zRes1 );            // only those variables are pair-wise symmetric             // that are pair-wise symmetric in both cofactors//.........这里部分代码省略.........

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

//.........这里部分代码省略.........            bF0 = bF1 = bF;        if ( LevelG == LevelFG )        {            if ( bGR != bG ) // bG is complemented             {                bG0 = Cudd_Not( cuddE(bGR) );                bG1 = Cudd_Not( cuddT(bGR) );            }            else            {                bG0 = cuddE(bGR);                bG1 = cuddT(bGR);            }        }        else             bG0 = bG1 = bG;        // solve subproblems        zRes0 = extraZddGetSymmetricVars( dd, bF0, bG0, cuddT(bVarsNew) );        if ( zRes0 == NULL )             return NULL;        cuddRef( zRes0 );        // if there is not symmetries in the negative cofactor        // there is no need to test the positive cofactor        if ( zRes0 == z0 )            zRes = zRes0;  // zRes takes reference        else        {            zRes1 = extraZddGetSymmetricVars( dd, bF1, bG1, cuddT(bVarsNew) );            if ( zRes1 == NULL )             {                Cudd_RecursiveDerefZdd( dd, zRes0 );                return NULL;            }            cuddRef( zRes1 );            // only those variables should belong to the resulting set             // for which the property is true for both cofactors            zRes = cuddZddIntersect( dd, zRes0, zRes1 );            if ( zRes == NULL )            {                Cudd_RecursiveDerefZdd( dd, zRes0 );                Cudd_RecursiveDerefZdd( dd, zRes1 );                return NULL;            }            cuddRef( zRes );            Cudd_RecursiveDerefZdd( dd, zRes0 );            Cudd_RecursiveDerefZdd( dd, zRes1 );        }        // add one more singleton if the property is true for this variable        if ( bF0 == bG1 )        {            zPlus = cuddZddGetNode( dd, 2*bVarsNew->index, z1, z0 );            if ( zPlus == NULL )             {                Cudd_RecursiveDerefZdd( dd, zRes );                return NULL;            }            cuddRef( zPlus );            // add these variable pairs to the result            zRes = cuddZddUnion( dd, zTemp = zRes, zPlus );            if ( zRes == NULL )

/**Function********************************************************************  Synopsis [Performs the recursive step of Cudd_zddUnion.]  Description []  SideEffects [None]  SeeAlso     []******************************************************************************/DdNode *cuddZddUnion(  DdManager * zdd,  DdNode * P,  DdNode * Q){    int		p_top, q_top;    DdNode	*empty = DD_FALSE(zdd), *t, *e, *res;    DdManager	*table = zdd;    statLine(zdd);    if (P == empty)	return(Q);    if (Q == empty)	return(P);    if (P == Q)	return(P);    /* Check cache */    res = cuddCacheLookup2Zdd(table, cuddZddUnion, P, Q);    if (res != NULL)	return(res);    if (cuddIsConstant(P))	p_top = P->index;    else	p_top = zdd->permZ[P->index];    if (cuddIsConstant(Q))	q_top = Q->index;    else	q_top = zdd->permZ[Q->index];    if (p_top < q_top) {	e = cuddZddUnion(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) {	e = cuddZddUnion(zdd, P, cuddE(Q));	if (e == NULL) return(NULL);	cuddRef(e);	res = cuddZddGetNode(zdd, Q->index, cuddT(Q), e);	if (res == NULL) {	    Cudd_RecursiveDerefZdd(table, e);	    return(NULL);	}	cuddDeref(e);    } else {	t = cuddZddUnion(zdd, cuddT(P), cuddT(Q));	if (t == NULL) return(NULL);	cuddRef(t);	e = cuddZddUnion(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, cuddZddUnion, P, Q, res);    return(res);} /* end of cuddZddUnion */