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

/**Function********************************************************************  Synopsis [This function prepares an array of variables which have not been  encountered so far when traversing the procedure cuddSplitSetRecur.]  Description [This function prepares an array of variables which have not been  encountered so far when traversing the procedure cuddSplitSetRecur. This  array is then used to extract the required number of minterms from a constant  1. The algorithm guarantees that the size of BDD will be utmost /log(n).]  SideEffects [None]******************************************************************************/static DdNode *selectMintermsFromUniverse(  DdManager * manager,  int * varSeen,  double  n){    int numVars;    int i, size, j;     DdNode *one, *zero, *result;    DdNode **vars;    numVars = 0;    size = manager->size;    one = DD_ONE(manager);    zero = Cudd_Not(one);    /* Count the number of variables not encountered so far in procedure    ** cuddSplitSetRecur.    */    for (i = size-1; i >= 0; i--) {	if(varSeen[i] == 0)	    numVars++;    }    vars = ALLOC(DdNode *, numVars);    if (!vars) {	manager->errorCode = CUDD_MEMORY_OUT;	return(NULL);    }    j = 0;    for (i = size-1; i >= 0; i--) {	if(varSeen[i] == 0) {	    vars[j] = cuddUniqueInter(manager,manager->perm[i],one,zero);	    cuddRef(vars[j]);	    j++;	}    }    /* Compute a function which has n minterms and depends on at most    ** numVars variables.    */    result = mintermsFromUniverse(manager,vars,numVars,n, 0);    if (result) 	cuddRef(result);    for (i = 0; i < numVars; i++)	Cudd_RecursiveDeref(manager,vars[i]);    FREE(vars);    return(result);} /* end of selectMintermsFromUniverse */

/**Function********************************************************************  Synopsis [Replaces variables with constants if possible.]  Description [This function performs part of the transformation to  standard form by replacing variables with constants if possible.]  SideEffects [None]  SeeAlso     [bddVarToCanonical bddVarToCanonicalSimple]******************************************************************************/static voidbddVarToConst(  DdNode * f,  DdNode ** gp,  DdNode ** hp,  DdNode * one){    DdNode *g = *gp;    DdNode *h = *hp;    if (f == g) {    /* ITE(F,F,H) = ITE(F,1,H) = F + H */        *gp = one;    } else if (f == Cudd_Not(g)) {    /* ITE(F,!F,H) = ITE(F,0,H) = !F * H */        *gp = Cudd_Not(one);    }    if (f == h) {    /* ITE(F,G,F) = ITE(F,G,0) = F * G */        *hp = Cudd_Not(one);    } else if (f == Cudd_Not(h)) {    /* ITE(F,G,!F) = ITE(F,G,1) = !F + G */        *hp = one;    }} /* end of bddVarToConst */

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

/**Function********************************************************************  Synopsis    [Universally abstracts all the variables in cube from f.]  Description [Universally abstracts all the variables in cube from f.  Returns the abstracted BDD if successful; NULL otherwise.]  SideEffects [None]  SeeAlso     [Cudd_bddExistAbstract Cudd_addUnivAbstract]******************************************************************************/DdNode *Cudd_bddUnivAbstract(  DdManager * manager,  DdNode * f,  DdNode * cube){    DdNode	*res;    if (bddCheckPositiveCube(manager, cube) == 0) {	(void) fprintf(manager->err,		       "Error: Can only abstract positive cubes/n");	manager->errorCode = CUDD_INVALID_ARG;	return(NULL);    }    do {	manager->reordered = 0;	res = cuddBddExistAbstractRecur(manager, Cudd_Not(f), cube);    } while (manager->reordered == 1);    if (res != NULL) res = Cudd_Not(res);    return(res);} /* end of Cudd_bddUnivAbstract */

/**Function********************************************************************  Synopsis    [Computes the exclusive NOR of two BDDs f and g.]  Description [Computes the exclusive NOR of two BDDs f and g. Returns a  pointer to the resulting BDD if successful; NULL if the intermediate  result blows up.]  SideEffects [None]  SeeAlso     [Cudd_bddIte Cudd_addApply Cudd_bddAnd Cudd_bddOr  Cudd_bddNand Cudd_bddNor Cudd_bddXor]******************************************************************************/DdNode *Cudd_bddXnor(  DdManager * dd,  DdNode * f,  DdNode * g){    DdNode *res;    do {        dd->reordered = 0;        res = cuddBddXorRecur(dd,f,Cudd_Not(g));    } while (dd->reordered == 1);    return(res);} /* end of Cudd_bddXnor */

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

/** * @brief Basic BDD test. * @return 0 if successful; -1 otherwise. */static inttestBdd(int verbosity){    DdManager *dd;    DdNode *f, *var, *tmp;    int i, ret;    dd = Cudd_Init(0, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0);    if (!dd) {        if (verbosity) {            printf("initialization failed/n");        }        return -1;    }    if (verbosity) {        printf("Started CUDD version ");        Cudd_PrintVersion(stdout);    }    f = Cudd_ReadOne(dd);    Cudd_Ref(f);    for (i = 3; i >= 0; i--) {        var = Cudd_bddIthVar(dd, i);        tmp = Cudd_bddAnd(dd, Cudd_Not(var), f);        if (!tmp) {            if (verbosity) {                printf("computation failed/n");            }            return -1;        }        Cudd_Ref(tmp);        Cudd_RecursiveDeref(dd, f);        f = tmp;    }    if (verbosity) {        Cudd_bddPrintCover(dd, f, f);    }    Cudd_RecursiveDeref(dd, f);    ret = Cudd_CheckZeroRef(dd);    if (ret != 0 && verbosity) {        printf("%d unexpected non-zero references/n", ret);    }    Cudd_Quit(dd);    return 0;}

/**Function********************************************************************  Synopsis    [Computes the exclusive NOR of two BDDs f and g.  Returns  NULL if too many nodes are required.]  Description [Computes the exclusive NOR of two BDDs f and g. Returns a  pointer to the resulting BDD if successful; NULL if the intermediate  result blows up or more new nodes than <code>limit</code> are  required.]  SideEffects [None]  SeeAlso     [Cudd_bddXnor]******************************************************************************/DdNode *Cudd_bddXnorLimit(  DdManager * dd,  DdNode * f,  DdNode * g,  unsigned int limit){    DdNode *res;    unsigned int saveLimit = dd->maxLive;    dd->maxLive = (dd->keys - dd->dead) + (dd->keysZ - dd->deadZ) + limit;    do {	dd->reordered = 0;	res = cuddBddXorRecur(dd,f,Cudd_Not(g));    } while (dd->reordered == 1);    dd->maxLive = saveLimit;    return(res);} /* end of Cudd_bddXnorLimit */

/**Function*************************************************************  Synopsis    []  Description []                 SideEffects []  SeeAlso     []***********************************************************************/DdNode * Abc_MvReadCube( DdManager * dd, char * pLine, int nVars ){    DdNode * bCube, * bVar, * bTemp;    int i;    bCube = Cudd_ReadOne(dd);  Cudd_Ref( bCube );    for ( i = 0; i < nVars; i++ )    {        if ( pLine[i] == '-' )            continue;        else if ( pLine[i] == '0' ) // 0            bVar = Cudd_Not( Cudd_bddIthVar(dd, 29-i) );        else if ( pLine[i] == '1' ) // 1            bVar = Cudd_bddIthVar(dd, 29-i);        else assert(0);        bCube = Cudd_bddAnd( dd, bTemp = bCube, bVar );  Cudd_Ref( bCube );        Cudd_RecursiveDeref( dd, bTemp );    }    Cudd_Deref( bCube );    return bCube;}

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

/**Function********************************************************************  Synopsis    [Computes the boolean difference of f with respect to x.]  Description [Computes the boolean difference of f with respect to the  variable with index x.  Returns the BDD of the boolean difference if  successful; NULL otherwise.]  SideEffects [None]  SeeAlso     []******************************************************************************/DdNode *Cudd_bddBooleanDiff(  DdManager * manager,  DdNode * f,  int  x){    DdNode *res, *var;    /* If the variable is not currently in the manager, f cannot    ** depend on it.    */    if (x >= manager->size) return(Cudd_Not(DD_ONE(manager)));    var = manager->vars[x];    do {	manager->reordered = 0;	res = cuddBddBooleanDiffRecur(manager, Cudd_Regular(f), var);    } while (manager->reordered == 1);    return(res);} /* end of Cudd_bddBooleanDiff */

/**Function********************************************************************  Synopsis    [Checks whether g is the BDD of a cube.]  Description [Checks whether g is the BDD of a cube. Returns 1 in case  of success; 0 otherwise. The constant 1 is a valid cube, but all other  constant functions cause cuddCheckCube to return 0.]  SideEffects [None]  SeeAlso     []******************************************************************************/intcuddCheckCube(  DdManager * dd,  DdNode * g){    DdNode *g1,*g0,*one,*zero;        one = DD_ONE(dd);    if (g == one) return(1);    if (Cudd_IsConstant(g)) return(0);    zero = Cudd_Not(one);    cuddGetBranches(g,&g1,&g0);    if (g0 == zero) {        return(cuddCheckCube(dd, g1));    }    if (g1 == zero) {        return(cuddCheckCube(dd, g0));    }    return(0);} /* end of cuddCheckCube */

/* encode the program counter in an array of boolean variables */DdNode* bdd_encode_pc(DdManager* m, DdNode* node, int** pc_array, int pc_size,                      int proc, int pc) {    int i;    DdNode* tmp, *var;    DdNode* ret = Cudd_ReadOne(m);    Cudd_Ref(ret);    for (i=0; i<pc_size; i++) {          /* iterate for each bit in pc_size */        var = Cudd_bddIthVar(m, pc_array[proc][i]);        if (pc % 2)                        /* encode true bit */            tmp = Cudd_bddAnd(m, var, ret);        else                               /* encode false bit */            tmp = Cudd_bddAnd(m, Cudd_Not(var), ret);        Cudd_Ref(tmp);        Cudd_RecursiveDeref(m, ret);       /* release the old bdd each time a new */        ret = tmp;                         /* one is made */        pc /= 2;    }    tmp = Cudd_bddAnd(m, ret, node);     /* add encoding to existing edge */    Cudd_Ref(tmp);    Cudd_RecursiveDeref(m, ret);    Cudd_RecursiveDeref(m, node);    return tmp;                          /* return updated edge */}

/* Compute negation.  Creates CUDD reference.  For ZDDs, records as reference */ref_t shadow_negate(shadow_mgr mgr, ref_t a) {    ref_t r = REF_INVALID;    if (REF_IS_INVALID(a))	return a;    if (do_ref(mgr))	r = REF_NEGATE(a);    else {	DdNode *an = get_ddnode(mgr, a);	if (is_zdd(mgr, a)) {	    DdNode *zone = Cudd_ReadZddOne(mgr->bdd_manager, 0);	    reference_dd(mgr, zone);	    DdNode *ann = Cudd_zddDiff(mgr->bdd_manager, zone, an);	    reference_dd(mgr, ann);	    unreference_dd(mgr, zone, IS_ZDD);	    r = dd2ref(ann, IS_ZDD);	    // For ZDDs, don't already have negated values recorded	    add_ref(mgr, r, ann);	} else if (is_add(mgr, a)) {	    DdNode *ann = Cudd_addCmpl(mgr->bdd_manager, an);	    reference_dd(mgr, ann);	    r = dd2ref(ann, IS_ADD);	    // For ADDs, don't already have negated values recorded	    add_ref(mgr, r, ann);	} else {	    DdNode *ann = Cudd_Not(an);	    reference_dd(mgr, ann);	    r = dd2ref(ann, IS_BDD);	}    }#if RPT >= 5    char buf[24], nbuf[24];    shadow_show(mgr, a, buf);    shadow_show(mgr, r, nbuf);    report(5, "Negated %s to get %s", buf, nbuf);#endif    return r;}

/**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    [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) {      //Rob Apr 6 2001: might need to change this, not sure what it does.....      h = (*cuddV(res)).get_val();      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);	Terminal hTerminal;	hTerminal.set((double) h);	res = cuddUniqueConst(dd,&hTerminal);	//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    [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    []  Description []                 SideEffects []  SeeAlso     []***********************************************************************/void Abc_MvRead( Mv_Man_t * p ){    FILE * pFile;    char Buffer[1000], * pLine;    DdNode * bCube, * bTemp, * bProd, * bVar0, * bVar1, * bCubeSum;    int i, v;    // start the cube    bCubeSum = Cudd_ReadLogicZero(p->dd);  Cudd_Ref( bCubeSum );    // start the values    for ( i = 0; i < 15; i++ )    for ( v = 0; v < 4; v++ )    {        p->bValues[i][v]   = Cudd_ReadLogicZero(p->dd);  Cudd_Ref( p->bValues[i][v] );        p->bValueDcs[i][v] = Cudd_ReadLogicZero(p->dd);  Cudd_Ref( p->bValueDcs[i][v] );    }    // read the file    pFile = fopen( "input.pla", "r" );    while ( fgets( Buffer, 1000, pFile ) )    {        if ( Buffer[0] == '#' )            continue;        if ( Buffer[0] == '.' )        {            if ( Buffer[1] == 'e' )                break;            continue;        }        // get the cube         bCube = Abc_MvReadCube( p->dd, Buffer, 18 );  Cudd_Ref( bCube );        // add it to the values of the output functions        pLine = Buffer + 19;        for ( i = 0; i < 15; i++ )        {            if ( pLine[2*i] == '-' && pLine[2*i+1] == '-' )            {                for ( v = 0; v < 4; v++ )                {                    p->bValueDcs[i][v] = Cudd_bddOr( p->dd, bTemp = p->bValueDcs[i][v], bCube );  Cudd_Ref( p->bValueDcs[i][v] );                    Cudd_RecursiveDeref( p->dd, bTemp );                }                continue;            }            else if ( pLine[2*i] == '0' && pLine[2*i+1] == '0' ) // 0                v = 0;            else if ( pLine[2*i] == '1' && pLine[2*i+1] == '0' ) // 1                v = 1;            else if ( pLine[2*i] == '0' && pLine[2*i+1] == '1' ) // 2                v = 2;            else if ( pLine[2*i] == '1' && pLine[2*i+1] == '1' ) // 3                v = 3;            else assert( 0 );            // add the value            p->bValues[i][v] = Cudd_bddOr( p->dd, bTemp = p->bValues[i][v], bCube );  Cudd_Ref( p->bValues[i][v] );            Cudd_RecursiveDeref( p->dd, bTemp );        }        // add the cube        bCubeSum = Cudd_bddOr( p->dd, bTemp = bCubeSum, bCube );  Cudd_Ref( bCubeSum );        Cudd_RecursiveDeref( p->dd, bTemp );        Cudd_RecursiveDeref( p->dd, bCube );    }    // add the complement of the domain to all values    for ( i = 0; i < 15; i++ )        for ( v = 0; v < 4; v++ )        {            if ( p->bValues[i][v] == Cudd_Not(Cudd_ReadOne(p->dd)) )                continue;            p->bValues[i][v] = Cudd_bddOr( p->dd, bTemp = p->bValues[i][v], p->bValueDcs[i][v] );  Cudd_Ref( p->bValues[i][v] );            Cudd_RecursiveDeref( p->dd, bTemp );            p->bValues[i][v] = Cudd_bddOr( p->dd, bTemp = p->bValues[i][v], Cudd_Not(bCubeSum) );  Cudd_Ref( p->bValues[i][v] );            Cudd_RecursiveDeref( p->dd, bTemp );        }    printf( "Domain = %5.2f %%./n", 100.0*Cudd_CountMinterm(p->dd, bCubeSum, 32)/Cudd_CountMinterm(p->dd, Cudd_ReadOne(p->dd), 32) );     Cudd_RecursiveDeref( p->dd, bCubeSum );    // create each output function    for ( i = 0; i < 15; i++ )    {        p->bFuncs[i] = Cudd_ReadLogicZero(p->dd);  Cudd_Ref( p->bFuncs[i] );        for ( v = 0; v < 4; v++ )        {            bVar0 = Cudd_NotCond( Cudd_bddIthVar(p->dd, 30), ((v & 1) == 0) );            bVar1 = Cudd_NotCond( Cudd_bddIthVar(p->dd, 31), ((v & 2) == 0) );//.........这里部分代码省略.........

/**Function********************************************************************  Synopsis    [Performs a recursive step of Extra_bddReduceVarSet.]  Description [Returns the set of all variables in the given set that are not in the   support of the given function.]  SideEffects []  SeeAlso     []******************************************************************************/DdNode * extraBddReduceVarSet(   DdManager * dd,    /* the DD manager */  DdNode * bVars,    /* the set of variables to be reduced */  DdNode * bF)       /* the function whose support is used for reduction */{    DdNode * bRes;    DdNode * bFR = Cudd_Regular(bF);    if ( cuddIsConstant(bFR) || bVars == b1 )        return bVars;    if ( (bRes = cuddCacheLookup2(dd, extraBddReduceVarSet, bVars, bF)) )        return bRes;    else    {        DdNode * bF0, * bF1;                     DdNode * bVarsThis, * bVarsLower, * bTemp;        int LevelF;        // if LevelF is below LevelV, scroll through the vars in bVars         LevelF = dd->perm[bFR->index];        for ( bVarsThis = bVars; LevelF > cuddI(dd,bVarsThis->index); bVarsThis = cuddT(bVarsThis) );        // scroll also through the current var, because it should be not be added        if ( LevelF == cuddI(dd,bVarsThis->index) )            bVarsLower = cuddT(bVarsThis);        else            bVarsLower = bVarsThis;        // cofactor the function        if ( bFR != bF ) // bFunc is complemented         {            bF0 = Cudd_Not( cuddE(bFR) );            bF1 = Cudd_Not( cuddT(bFR) );        }        else        {            bF0 = cuddE(bFR);            bF1 = cuddT(bFR);        }        // solve subproblems        bRes = extraBddReduceVarSet( dd, bVarsLower, bF0 );        if ( bRes == NULL )             return NULL;        cuddRef( bRes );        bRes = extraBddReduceVarSet( dd, bTemp = bRes, bF1 );        if ( bRes == NULL )         {            Cudd_RecursiveDeref( dd, bTemp );            return NULL;        }        cuddRef( bRes );        Cudd_RecursiveDeref( dd, bTemp );        // the current var should not be added        // add the skipped vars        if ( bVarsThis != bVars )        {            DdNode * bVarsExtra;            // extract the skipped variables            bVarsExtra = cuddBddExistAbstractRecur( dd, bVars, bVarsThis );            if ( bVarsExtra == NULL )            {                Cudd_RecursiveDeref( dd, bRes );                return NULL;            }            cuddRef( bVarsExtra );            // add these variables            bRes = cuddBddAndRecur( dd, bTemp = bRes, bVarsExtra );            if ( bRes == NULL )             {                Cudd_RecursiveDeref( dd, bTemp );                Cudd_RecursiveDeref( dd, bVarsExtra );                return NULL;            }            cuddRef( bRes );            Cudd_RecursiveDeref( dd, bTemp );            Cudd_RecursiveDeref( dd, bVarsExtra );        }        cuddDeref( bRes );        cuddCacheInsert2( dd, extraBddReduceVarSet, bVars, bF, bRes );        return bRes;    }}   /* end of extraBddReduceVarSet */

/**Function********************************************************************  Synopsis    [Creates a new DD manager.]  Description [Creates a new DD manager, initializes the table, the  basic constants and the projection functions. If maxMemory is 0,  Cudd_Init decides suitable values for the maximum size of the cache  and for the limit for fast unique table growth based on the available  memory. Returns a pointer to the manager if successful; NULL  otherwise.]  SideEffects [None]  SeeAlso     [Cudd_Quit]******************************************************************************/DdManager *Cudd_Init(  unsigned int numVars /* initial number of BDD variables (i.e., subtables) */,  unsigned int numVarsZ /* initial number of ZDD variables (i.e., subtables) */,  unsigned int numSlots /* initial size of the unique tables */,  unsigned int cacheSize /* initial size of the cache */,  unsigned long maxMemory /* target maximum memory occupation */){    DdManager *unique;    int i,result;    DdNode *one, *zero;    unsigned int maxCacheSize;    unsigned int looseUpTo;    extern void (*MMoutOfMemory)(long);    void (*saveHandler)(long);    if (maxMemory == 0) {	maxMemory = getSoftDataLimit();    }    looseUpTo = (unsigned int) ((maxMemory / sizeof(DdNode)) /				DD_MAX_LOOSE_FRACTION);    unique = cuddInitTable(numVars,numVarsZ,numSlots,looseUpTo);    unique->maxmem = (unsigned) maxMemory / 10 * 9;    if (unique == NULL) return(NULL);    maxCacheSize = (unsigned int) ((maxMemory / sizeof(DdCache)) /				   DD_MAX_CACHE_FRACTION);    result = cuddInitCache(unique,cacheSize,maxCacheSize);    if (result == 0) return(NULL);    saveHandler = MMoutOfMemory;    MMoutOfMemory = Cudd_OutOfMem;    unique->stash = ALLOC(char,(maxMemory / DD_STASH_FRACTION) + 4);    MMoutOfMemory = saveHandler;    if (unique->stash == NULL) {	(void) fprintf(unique->err,"Unable to set aside memory/n");    }    /* Initialize constants. */    unique->one = cuddUniqueConst(unique,1.0);    if (unique->one == NULL) return(0);    cuddRef(unique->one);    unique->zero = cuddUniqueConst(unique,0.0);    if (unique->zero == NULL) return(0);    cuddRef(unique->zero);#ifdef HAVE_IEEE_754    if (DD_PLUS_INF_VAL != DD_PLUS_INF_VAL * 3 ||	DD_PLUS_INF_VAL != DD_PLUS_INF_VAL / 3) {	(void) fprintf(unique->err,"Warning: Crippled infinite values/n");	(void) fprintf(unique->err,"Recompile without -DHAVE_IEEE_754/n");    }#endif    unique->plusinfinity = cuddUniqueConst(unique,DD_PLUS_INF_VAL);    if (unique->plusinfinity == NULL) return(0);    cuddRef(unique->plusinfinity);    unique->minusinfinity = cuddUniqueConst(unique,DD_MINUS_INF_VAL);    if (unique->minusinfinity == NULL) return(0);    cuddRef(unique->minusinfinity);    unique->background = unique->zero;    /* The logical zero is different from the CUDD_VALUE_TYPE zero! */    one = unique->one;    zero = Cudd_Not(one);    /* Create the projection functions. */    unique->vars = ALLOC(DdNodePtr,unique->maxSize);    if (unique->vars == NULL) {	unique->errorCode = CUDD_MEMORY_OUT;	return(NULL);    }    for (i = 0; i < unique->size; i++) {	unique->vars[i] = cuddUniqueInter(unique,i,one,zero);	if (unique->vars[i] == NULL) return(0);	cuddRef(unique->vars[i]);    }    if (unique->sizeZ)	cuddZddInitUniv(unique);    unique->memused += sizeof(DdNode *) * unique->maxSize;    return(unique);} /* end of Cudd_Init */

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

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

/**Function********************************************************************  Synopsis    [Performs the recursive step of Extra_bddCheckVarsSymmetric().]  Description [Returns b0 if the variables are not symmetric. Returns b1 if the  variables can be symmetric. The variables are represented in the form of a   two-variable cube. In case the cube contains one variable (below Var1 level),  the cube's pointer is complemented if the variable Var1 occurred on the   current path; otherwise, the cube's pointer is regular. Uses additional   complemented bit (Hash_Not) to mark the result if in the BDD rooted that this  node there is a branch passing though the node labeled with Var2.]  SideEffects []  SeeAlso     []******************************************************************************/DdNode * extraBddCheckVarsSymmetric(   DdManager * dd,    /* the DD manager */  DdNode * bF,  DdNode * bVars) {    DdNode * bRes;    if ( bF == b0 )        return b1;    assert( bVars != b1 );        if ( (bRes = cuddCacheLookup2(dd, extraBddCheckVarsSymmetric, bF, bVars)) )        return bRes;    else    {        DdNode * bRes0, * bRes1;        DdNode * bF0, * bF1;                     DdNode * bFR = Cudd_Regular(bF);        int LevelF = cuddI(dd,bFR->index);        DdNode * bVarsR = Cudd_Regular(bVars);        int fVar1Pres;        int iLev1;        int iLev2;        if ( bVarsR != bVars ) // cube's pointer is complemented        {            assert( cuddT(bVarsR) == b1 );            fVar1Pres = 1;                    // the first var is present on the path            iLev1 = -1;                       // we are already below the first var level            iLev2 = dd->perm[bVarsR->index];  // the level of the second var        }        else  // cube's pointer is NOT complemented        {            fVar1Pres = 0;                    // the first var is absent on the path            if ( cuddT(bVars) == b1 )            {                iLev1 = -1;                             // we are already below the first var level                 iLev2 = dd->perm[bVars->index];         // the level of the second var            }            else            {                assert( cuddT(cuddT(bVars)) == b1 );                iLev1 = dd->perm[bVars->index];         // the level of the first var                 iLev2 = dd->perm[cuddT(bVars)->index];  // the level of the second var            }        }        // cofactor the function        // the cofactors are needed only if we are above the second level        if ( LevelF < iLev2 )        {            if ( bFR != bF ) // bFunc is complemented             {                bF0 = Cudd_Not( cuddE(bFR) );                bF1 = Cudd_Not( cuddT(bFR) );            }            else            {                bF0 = cuddE(bFR);                bF1 = cuddT(bFR);            }        }        else            bF0 = bF1 = NULL;        // consider five cases:        // (1) F is above iLev1        // (2) F is on the level iLev1        // (3) F is between iLev1 and iLev2        // (4) F is on the level iLev2        // (5) F is below iLev2        // (1) F is above iLev1        if ( LevelF < iLev1 )        {            // the returned result cannot have the hash attribute            // because we still did not reach the level of Var1;            // the attribute never travels above the level of Var1            bRes0 = extraBddCheckVarsSymmetric( dd, bF0, bVars );//          assert( !Hash_IsComplement( bRes0 ) );            assert( bRes0 != z0 );//.........这里部分代码省略.........

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

/**Function********************************************************************  Synopsis    [Performs a recursive step of Extra_zddGetSymmetricVars.]  Description [Returns the set of ZDD singletons, containing those positive  ZDD variables that correspond to BDD variables x, for which it is true   that bF(x=0) == bG(x=1).]  SideEffects []  SeeAlso     []******************************************************************************/DdNode * extraZddGetSymmetricVars(   DdManager * dd,    /* the DD manager */  DdNode * bF,       /* the first function  - originally, the positive cofactor */  DdNode * bG,       /* the second function - originally, the negative cofactor */  DdNode * bVars)    /* the set of variables, on which F and G depend */{    DdNode * zRes;    DdNode * bFR = Cudd_Regular(bF);     DdNode * bGR = Cudd_Regular(bG);     if ( cuddIsConstant(bFR) && cuddIsConstant(bGR) )    {        if ( bF == bG )            return extraZddGetSingletons( dd, bVars );        else             return z0;    }    assert( bVars != b1 );    if ( (zRes = cuddCacheLookupZdd(dd, DD_GET_SYMM_VARS_TAG, bF, bG, bVars)) )        return zRes;    else    {        DdNode * zRes0, * zRes1;                     DdNode * zPlus, * zTemp;        DdNode * bF0, * bF1;                     DdNode * bG0, * bG1;                     DdNode * bVarsNew;            int LevelF = cuddI(dd,bFR->index);        int LevelG = cuddI(dd,bGR->index);        int LevelFG;        if ( LevelF < LevelG )            LevelFG = LevelF;        else            LevelFG = LevelG;        // at least one of the arguments is not a constant        assert( LevelFG < dd->size );        // every variable in bF and bG should be also in bVars, therefore LevelFG cannot be above LevelV        // if LevelFG is below LevelV, scroll through the vars in bVars to the same level as LevelFG        for ( bVarsNew = bVars; LevelFG > dd->perm[bVarsNew->index]; bVarsNew = cuddT(bVarsNew) );        assert( LevelFG == dd->perm[bVarsNew->index] );        // cofactor the functions        if ( LevelF == LevelFG )        {            if ( bFR != bF ) // bF is complemented             {                bF0 = Cudd_Not( cuddE(bFR) );                bF1 = Cudd_Not( cuddT(bFR) );            }            else            {                bF0 = cuddE(bFR);                bF1 = cuddT(bFR);            }        }        else             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//.........这里部分代码省略.........

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

// Returns the variable v. if b is 0 it will be negatedDdNode* getVar(DdManager *manager, int v, int b) {  return b ?    Cudd_bddIthVar(manager,v) :    Cudd_Not(Cudd_bddIthVar(manager,v));}

//.........这里部分代码省略.........    if (dfile != NULL) {	dfp = open_file(dfile, "w");    }    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);}