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

/**Function********************************************************************  Synopsis    [Performs the recursive step of Cuddaux_NodesBelowLevelRecur.]  Description [Performs the recursive step of  Cuddaux_NodesBelowLevelRecur.  F is supposed to be a regular  node. Returns 1 if successful, NULL otherwise.  The background node is not put in the list if take_background==0 ]  SideEffects [None]  SeeAlso     []******************************************************************************/static intcuddauxNodesBelowLevelRecur(DdManager* manager, DdNode* F, int level,			    cuddaux_list_t** plist, st_table* visited,			    size_t max, size_t* psize,			    bool take_background){  int topF,res;  if ((!take_background && F==DD_BACKGROUND(manager)) || st_is_member(visited, (char *) F) == 1){    return 1;  }  topF = cuddI(manager,F->index);  if (topF < level){    res = cuddauxNodesBelowLevelRecur(manager, Cudd_Regular(cuddT(F)), level, plist, visited, max, psize, take_background);    if (res==0) return 0;    if (max == 0 || *psize<max){      res = cuddauxNodesBelowLevelRecur(manager, Cudd_Regular(cuddE(F)), level, plist, visited, max, psize, take_background);      if (res==0) return 0;    }  }  else {    res = cuddaux_list_add(plist,F);    (*psize)++;    if (res==0) return 0;  }  if (st_add_direct(visited, (char *) F, NULL) == ST_OUT_OF_MEM){    cuddaux_list_free(*plist);    return 0;  }  return 1;}

void Forward(DdNode *root, int nex) {  int i, j;  if (boolVars_ex[nex]) {    nodesToVisit = (DdNode ***)malloc(sizeof(DdNode **) * boolVars_ex[nex]);    NnodesToVisit = (int *)malloc(sizeof(int) * boolVars_ex[nex]);    nodesToVisit[0] = (DdNode **)malloc(sizeof(DdNode *));    nodesToVisit[0][0] = root;    NnodesToVisit[0] = 1;    for (i = 1; i < boolVars_ex[nex]; i++) {      nodesToVisit[i] = NULL;      NnodesToVisit[i] = 0;    }    add_node(nodesF, Cudd_Regular(root), 1);    for (i = 0; i < boolVars_ex[nex]; i++) {      for (j = 0; j < NnodesToVisit[i]; j++)        UpdateForward(nodesToVisit[i][j], nex);    }    for (i = 0; i < boolVars_ex[nex]; i++) {      free(nodesToVisit[i]);    }    free(nodesToVisit);    free(NnodesToVisit);  } else {    add_node(nodesF, Cudd_Regular(root), 1);  }}

void UpdateForward(DdNode *node, int nex) {  int index, position, mVarIndex;  DdNode *T, *E, *nodereg;  variable v;  double *value_p, *value_p_T, *value_p_F, p;  if (Cudd_IsConstant(node)) {    return;  } else {    index = Cudd_NodeReadIndex(node);    mVarIndex = bVar2mVar_ex[nex][index];    v = vars_ex[nex][mVarIndex];    p = probs_ex[nex][index];    nodereg = Cudd_Regular(node);    value_p = get_value(nodesF, nodereg);    if (value_p == NULL) {      printf("Error/n");      return;    } else {      T = Cudd_T(node);      E = Cudd_E(node);      if (!Cudd_IsConstant(T)) {        value_p_T = get_value(nodesF, T);        if (value_p_T != NULL) {          *value_p_T = *value_p_T + *value_p * p;        } else {          add_or_replace_node(nodesF, Cudd_Regular(T), *value_p * p);          index = Cudd_NodeReadIndex(T);          position = Cudd_ReadPerm(mgr_ex[nex], index);          nodesToVisit[position] = (DdNode **)realloc(              nodesToVisit[position],              (NnodesToVisit[position] + 1) * sizeof(DdNode *));          nodesToVisit[position][NnodesToVisit[position]] = T;          NnodesToVisit[position] = NnodesToVisit[position] + 1;        }      }      if (!Cudd_IsConstant(E)) {        value_p_F = get_value(nodesF, Cudd_Regular(E));        if (value_p_F != NULL) {          *value_p_F = *value_p_F + *value_p * (1 - p);        } else {          add_or_replace_node(nodesF, Cudd_Regular(E), *value_p * (1 - p));          index = Cudd_NodeReadIndex(E);          position = Cudd_ReadPerm(mgr_ex[nex], index);          nodesToVisit[position] = (DdNode **)realloc(              nodesToVisit[position],              (NnodesToVisit[position] + 1) * sizeof(DdNode *));          nodesToVisit[position][NnodesToVisit[position]] = E;          NnodesToVisit[position] = NnodesToVisit[position] + 1;        }      }      return;    }  }}

uint Synth::walk(DdNode *a_dd) {    /**    Walk given DdNode node (recursively).    If a given node requires intermediate AND gates for its representation, the function adds them.        Literal representing given input node is `not` added to the spec.    :returns: literal representing input node    **/    // caching    static hmap<DdNode*, uint> cache;    {        auto cached_lit = cache.find(Cudd_Regular(a_dd));        if (cached_lit != cache.end())            return Cudd_IsComplement(a_dd) ? NEGATED(cached_lit->second) : cached_lit->second;    }    // end of caching    if (Cudd_IsConstant(a_dd))        return (uint) (a_dd == cudd.bddOne().getNode());  // in aiger: 0 is False and 1 is True    // get an index of the variable    uint a_lit = aiger_by_cudd[Cudd_NodeReadIndex(a_dd)];    DdNode *t_bdd = Cudd_T(a_dd);    DdNode *e_bdd = Cudd_E(a_dd);    uint t_lit = walk(t_bdd);    uint e_lit = walk(e_bdd);    // ite(a_bdd, then_bdd, else_bdd)    // = a*then + !a*else    // = !(!(a*then) * !(!a*else))    // -> in general case we need 3 more ANDs    uint a_t_lit = get_optimized_and_lit(a_lit, t_lit);    uint na_e_lit = get_optimized_and_lit(NEGATED(a_lit), e_lit);    uint n_a_t_lit = NEGATED(a_t_lit);    uint n_na_e_lit = NEGATED(na_e_lit);    uint and_lit = get_optimized_and_lit(n_a_t_lit, n_na_e_lit);    uint res = NEGATED(and_lit);    cache[Cudd_Regular(a_dd)] = res;    if (Cudd_IsComplement(a_dd))        res = NEGATED(res);    return res;}

/**Function********************************************************************  Synopsis    [Performs the recursive step of Cuddaux_IsVarIn.]  Description [Performs the recursive step of Cuddaux_IsVarIn. var is  supposed to be a BDD projection function. Returns the logical one or  zero.]  SideEffects [None]  SeeAlso     []******************************************************************************/DdNode*cuddauxIsVarInRecur(DdManager* manager, DdNode* f, DdNode* Var){  DdNode *zero,*one, *F, *res;  int topV,topF;  one = DD_ONE(manager);  zero = Cudd_Not(one);  F = Cudd_Regular(f);  if (cuddIsConstant(F)) return zero;  if (Var==F) return(one);  topV = Var->index;  topF = F->index;  if (topF == topV) return(one);  if (cuddI(manager,topV) < cuddI(manager,topF)) return(zero);  res = cuddCacheLookup2(manager,cuddauxIsVarInRecur, F, Var);  if (res != NULL) return(res);  res = cuddauxIsVarInRecur(manager,cuddT(F),Var);  if (res==zero){    res = cuddauxIsVarInRecur(manager,cuddE(F),Var);  }  cuddCacheInsert2(manager,cuddauxIsVarInRecur,F,Var,res);  return(res);}

/**Function********************************************************************  Synopsis    [Performs the recursive step of Cuddaux_Support.]  Description [Performs the recursive step of Cuddaux_Support.]  SideEffects [None]  SeeAlso     []******************************************************************************/DdNode*cuddauxSupportRecur(DdManager* dd,		    DdNode * f){  DdNode *one, *fv, *fvn, *T,*E, *res, *res1;  one = DD_ONE(dd);  if (cuddIsConstant(f)) {    return one;  }  fv = cuddT(f);  fvn = Cudd_Regular(cuddE(f));  if (cuddIsConstant(fv) && cuddIsConstant(fvn)){    return dd->vars[f->index];  }  /* Look in the cache */  res = cuddCacheLookup1(dd,Cuddaux_Support,f);  if (res != NULL)    return(res);  T = cuddIsConstant(fv) ? one : cuddauxSupportRecur(dd,fv);  if (T == NULL)    return(NULL);  cuddRef(T);  E = cuddIsConstant(fvn) ? one : cuddauxSupportRecur(dd,fvn);  if (E == NULL){    Cudd_IterDerefBdd(dd,T);    return(NULL);  }  if (T==E){    res = cuddUniqueInter(dd,f->index,T,Cudd_Not(one));    if (res == NULL){      Cudd_IterDerefBdd(dd,T);      return NULL;    }    cuddDeref(T);  }  else {    cuddRef(E);    res1 = cuddBddAndRecur(dd,T,E);    if (res1 == NULL){      Cudd_IterDerefBdd(dd,T);      Cudd_IterDerefBdd(dd,E);      return(NULL);    }    cuddRef(res1);    Cudd_IterDerefBdd(dd,T);    Cudd_IterDerefBdd(dd,E);    res = cuddUniqueInter(dd,f->index,res1,Cudd_Not(one));    if (res == NULL){      Cudd_IterDerefBdd(dd,T);      Cudd_IterDerefBdd(dd,E);      Cudd_IterDerefBdd(dd,res1);      return(NULL);    }    cuddDeref(res1);  }  cuddCacheInsert1(dd,Cuddaux_Support,f,res);  return(res);} /* end of cuddauxSupportRecur */

static intDddmpCuddDdArrayStorePrefixBody (  DdManager *ddMgr      /* IN: Manager */,  int n                 /* IN: Number of output nodes to be dumped */,  DdNode **f            /* IN: Array of output nodes to be dumped */,  char **inputNames     /* IN: Array of input names (or NULL) */,  char **outputNames    /* IN: Array of output names (or NULL) */,  FILE *fp              /* IN: Pointer to the dump file */  ){  st_table *visited = NULL;  int retValue;  int i;  /* Initialize symbol table for visited nodes. */  visited = st_init_table(st_ptrcmp, st_ptrhash);  Dddmp_CheckAndGotoLabel (visited==NULL,    "Error if function st_init_table.", failure);  /* Call the function that really gets the job done. */  for (i = 0; i < n; i++) {    retValue = DddmpCuddDdArrayStorePrefixStep (ddMgr, Cudd_Regular(f[i]),      fp, visited, inputNames);    Dddmp_CheckAndGotoLabel (retValue==0,      "Error if function DddmpCuddDdArrayStorePrefixStep.", failure);  }  /* To account for the possible complement on the root,   ** we put either a buffer or an inverter at the output of   ** the multiplexer representing the top node.   */  for (i=0; i<n; i++) {    if (outputNames == NULL) {      retValue = fprintf (fp,  "(BUF outNode%d ", i);    } else {      retValue = fprintf (fp,  "(BUF %s ", outputNames[i]);    }    Dddmp_CheckAndGotoLabel (retValue==EOF,      "Error during file store.", failure);    if (Cudd_IsComplement(f[i])) {      retValue = fprintf (fp, "(NOT node%" PRIxPTR "))/n",        (ptruint) f[i] / sizeof(DdNode));    } else {      retValue = fprintf (fp, "node%" PRIxPTR ")/n",        (ptruint) f[i] / sizeof(DdNode));    }    Dddmp_CheckAndGotoLabel (retValue==EOF,      "Error during file store.", failure);  }  st_free_table (visited);  return(1);failure:    if (visited != NULL) st_free_table(visited);    return(0);}

/**  @brief Computes the boolean difference of f with respect to x.  @details Computes the boolean difference of f with respect to the  variable with index x.  @return the %BDD of the boolean difference if successful; NULL  otherwise.  @sideeffect None*/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);    if (manager->errorCode == CUDD_TIMEOUT_EXPIRED && manager->timeoutHandler) {        manager->timeoutHandler(manager, manager->tohArg);    }    return(res);} /* end of Cudd_bddBooleanDiff */

/**Function********************************************************************  Synopsis    [Implements the recursive step of Cudd_bddVarMap.]  Description [Implements the recursive step of Cudd_bddVarMap.  Returns a pointer to the result if successful; NULL otherwise.]  SideEffects [None]  SeeAlso     [Cudd_bddVarMap]******************************************************************************/static DdNode *cuddBddVarMapRecur(  DdManager *manager /* DD manager */,  DdNode *f /* BDD to be remapped */){    DdNode	*F, *T, *E;    DdNode	*res;    int		index;    statLine(manager);    F = Cudd_Regular(f);    /* Check for terminal case of constant node. */    if (cuddIsConstant(F)) {	return(f);    }    /* If problem already solved, look up answer and return. */    if (F->ref != 1 &&	(res = cuddCacheLookup1(manager,Cudd_bddVarMap,F)) != NULL) {	return(Cudd_NotCond(res,F != f));    }    /* Split and recur on children of this node. */    T = cuddBddVarMapRecur(manager,cuddT(F));    if (T == NULL) return(NULL);    cuddRef(T);    E = cuddBddVarMapRecur(manager,cuddE(F));    if (E == NULL) {	Cudd_IterDerefBdd(manager, T);	return(NULL);    }    cuddRef(E);    /* Move variable that should be in this position to this position    ** by retrieving the single var BDD for that variable, and calling    ** cuddBddIteRecur with the T and E we just created.    */    index = manager->map[F->index];    res = cuddBddIteRecur(manager,manager->vars[index],T,E);    if (res == NULL) {	Cudd_IterDerefBdd(manager, T);	Cudd_IterDerefBdd(manager, E);	return(NULL);    }    cuddRef(res);    Cudd_IterDerefBdd(manager, T);    Cudd_IterDerefBdd(manager, E);    /* Do not keep the result if the reference count is only 1, since    ** it will not be visited again.    */    if (F->ref != 1) {	cuddCacheInsert1(manager,Cudd_bddVarMap,F,res);    }    cuddDeref(res);    return(Cudd_NotCond(res,F != f));} /* end of cuddBddVarMapRecur */

/**Function*************************************************************  Synopsis    [Performs the recursive step of Extra_bddSpaceCanonVars().]  Description []  SideEffects []  SeeAlso     []***********************************************************************/DdNode * extraBddSpaceCanonVars( DdManager * dd, DdNode * bF ){	DdNode * bRes, * bFR;	statLine( dd );	bFR = Cudd_Regular(bF);	if ( cuddIsConstant(bFR) )		return bF;    if ( (bRes = cuddCacheLookup1(dd, extraBddSpaceCanonVars, bF)) )    	return bRes;	else	{		DdNode * bF0,  * bF1;		DdNode * bRes, * bRes0; 		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 )		{			bRes = extraBddSpaceCanonVars( dd, bF1 );			if ( bRes == NULL )				return NULL;		}		else if ( bF1 == b0 )		{			bRes = extraBddSpaceCanonVars( dd, bF0 );			if ( bRes == NULL )				return NULL;		}		else		{			bRes0 = extraBddSpaceCanonVars( dd, bF0 );			if ( bRes0 == NULL )				return NULL;			cuddRef( bRes0 );			bRes = cuddUniqueInter( dd, bFR->index, bRes0, b0 );			if ( bRes == NULL ) 			{				Cudd_RecursiveDeref( dd,bRes0 );				return NULL;			}			cuddDeref( bRes0 );		}		cuddCacheInsert1( dd, extraBddSpaceCanonVars, bF, bRes );		return bRes;	}}

/**Function********************************************************************  Synopsis    [Annotates every node in the BDD node with its minterm count.]  Description [Annotates every node in the BDD node with its minterm count.  In this function, every node and the minterm count represented by it are  stored in a hash table.]  SideEffects [Fills up 'table' with the pair <node,minterm_count>.]******************************************************************************/static doublebddAnnotateMintermCount(  DdManager * manager,  DdNode * node,  double  max,  st_table * table){    DdNode *N,*Nv,*Nnv;    register double min_v,min_nv;    register double min_N;    double *pmin;    double *dummy;    statLine(manager);    N = Cudd_Regular(node);    if (cuddIsConstant(N)) {	if (node == DD_ONE(manager)) {	    return(max);	} else {	    return(0.0);	}    }    if (st_lookup(table, node, &dummy)) {	return(*dummy);    }	      Nv = cuddT(N);    Nnv = cuddE(N);    if (N != node) {	Nv = Cudd_Not(Nv);	Nnv = Cudd_Not(Nnv);    }    /* Recur on the two branches. */    min_v  = bddAnnotateMintermCount(manager,Nv,max,table) / 2.0;    if (min_v == (double)CUDD_OUT_OF_MEM)	return ((double)CUDD_OUT_OF_MEM);    min_nv = bddAnnotateMintermCount(manager,Nnv,max,table) / 2.0;    if (min_nv == (double)CUDD_OUT_OF_MEM)	return ((double)CUDD_OUT_OF_MEM);    min_N  = min_v + min_nv;    pmin = ALLOC(double,1);    if (pmin == NULL) {	manager->errorCode = CUDD_MEMORY_OUT;	return((double)CUDD_OUT_OF_MEM);    }    *pmin = min_N;    if (st_insert(table,(char *)node, (char *)pmin) == ST_OUT_OF_MEM) {	FREE(pmin);	return((double)CUDD_OUT_OF_MEM);    }        return(min_N);} /* end of bddAnnotateMintermCount */

/**Function********************************************************************  Synopsis [Computes the fraction of minterms in the on-set of all the  positive cofactors of a BDD or ADD.]  Description [Computes the fraction of minterms in the on-set of all  the positive cofactors of DD. Returns the pointer to an array of  doubles if successful; NULL otherwise. The array hs as many  positions as there are BDD variables in the manager plus one. The  last position of the array contains the fraction of the minterms in  the ON-set of the function represented by the BDD or ADD. The other  positions of the array hold the variable signatures.]  SideEffects [None]******************************************************************************/double *Cudd_CofMinterm(  DdManager * dd,  DdNode * node){    st_table	*table;    double	*values;    double	*result = NULL;    int		i, firstLevel;#ifdef DD_STATS    long startTime;    startTime = util_cpu_time();    num_calls = 0;    table_mem = sizeof(st_table);#endif    table = st_init_table(st_ptrcmp, st_ptrhash);    if (table == NULL) {	(void) fprintf(stdout,"out-of-memory, couldn't measure DD cofactors./n");	return(NULL);    }    size = dd->size;    values = ddCofMintermAux(dd, node, table);    if (values != NULL) {	result = ALLOC(double,size + 1);	if (result != NULL) {#ifdef DD_STATS	    table_mem += (size + 1) * sizeof(double);#endif	    if (Cudd_IsConstant(node))		firstLevel = 1;	    else		firstLevel = cuddI(dd,Cudd_Regular(node)->index);	    for (i = 0; i < size; i++) {		if (i >= cuddI(dd,Cudd_Regular(node)->index)) {		    result[dd->invperm[i]] = values[i - firstLevel];		} else {		    result[dd->invperm[i]] = values[size - firstLevel];		}	    }	    result[size] = values[size - firstLevel];	} else {	    dd->errorCode = CUDD_MEMORY_OUT;	}    }

/**Function********************************************************************  Synopsis    [Decreases the reference count of node.]  Description [Decreases the reference count of node. It is primarily  used in recursive procedures to decrease the ref count of a result  node before returning it. This accomplishes the goal of removing the  protection applied by a previous Cudd_Ref.]  SideEffects [None]  SeeAlso     [Cudd_RecursiveDeref Cudd_RecursiveDerefZdd Cudd_Ref]******************************************************************************/voidCudd_Deref(  DdNode * node){    node = Cudd_Regular(node);    cuddSatDec(node->ref);} /* end of Cudd_Deref */

/** * Internal function */double recurse_getNofSatisfyingAssignments(DdManager *dd, DdNode *orig, DdNode *cube, std::map<DdNode*,double> &buffer) {	// Normalize the cube	DdNode *cubeNext;	if (Cudd_Regular(cube)==cube) {		cubeNext = cuddT(cube);	} else {		if (!Cudd_IsConstant(cube)) {			cube = Cudd_Regular(cube);			cubeNext = (DdNode*)(((size_t)(cuddE(cube)) ^ 0x1));		} else {			// Constant			return (orig==dd->one)?1:0;		}	}	if (buffer.count(orig)>0) return buffer[orig];	if (Cudd_IsConstant(orig)) {		if (Cudd_IsConstant(cube)) {			return (orig==dd->one)?1:0;		} else {			return 2*recurse_getNofSatisfyingAssignments(dd,orig,cubeNext,buffer);		}	}	size_t xoring = (Cudd_Regular(orig)==orig?0:1);	DdNode *reference = Cudd_Regular(orig);	if (Cudd_IsConstant(cube)) return std::numeric_limits<double>::quiet_NaN(); // Missing variable!	int i1 = cuddI(dd,cube->index);	int i2 = cuddI(dd,reference->index);	if (i1<i2) {		double value = 2*recurse_getNofSatisfyingAssignments(dd,(DdNode*)((size_t)reference ^ xoring),cubeNext,buffer);		buffer[orig] = value;		return value;	} else if (i1>i2) {		return std::numeric_limits<double>::quiet_NaN();	} else {		double value = recurse_getNofSatisfyingAssignments(dd,(DdNode*)((size_t)(cuddT(reference)) ^ xoring),cubeNext,buffer)			+ recurse_getNofSatisfyingAssignments(dd,(DdNode*)((size_t)(cuddE(reference)) ^ xoring),cubeNext,buffer);		buffer[orig] = value;		return value;	}}

intDddmpVisitedCnf (  DdNode *f      /* IN: BDD node to be tested */  ){  f = Cudd_Regular(f);  return ((int)((uintptr_t)(f->next)) & (01));}

/**Function********************************************************************  Synopsis    [Finds the variables on which a DD depends.]  Description [Finds the variables on which a DD depends.  Returns a BDD  consisting of the product of the variables if successful; NULL otherwise.  Variant of [Cudd_Support] using global cache.]  SideEffects [None]  SeeAlso     [Cudd_Support]******************************************************************************/DdNode* Cuddaux_Support(DdManager* dd, DdNode* f){  DdNode* res;  do {    dd->reordered = 0;    res = cuddauxSupportRecur(dd, Cudd_Regular(f));  } while (dd->reordered == 1);  return res;}

/**Function********************************************************************  Synopsis    [Decreases the reference count of node n.]  Description [Decreases the reference count of node n. If n dies,  recursively decreases the reference counts of its children.  It is  used to dispose of a DD that is no longer needed.]  SideEffects [None]  SeeAlso     [Cudd_Deref Cudd_Ref Cudd_RecursiveDerefZdd]******************************************************************************/voidCudd_RecursiveDeref(  DdManager * table,  DdNode * n){    DdNode *N;    int ord;    DdNodePtr *stack = table->stack;    int SP = 1;    unsigned int live = table->keys - table->dead;    if (live > table->peakLiveNodes) {        table->peakLiveNodes = live;    }    N = Cudd_Regular(n);    do {#ifdef DD_DEBUG        assert(N->ref != 0);#endif        if (N->ref == 1) {            N->ref = 0;            table->dead++;#ifdef DD_STATS            table->nodesDropped++;#endif            if (cuddIsConstant(N)) {                table->constants.dead++;                N = stack[--SP];            } else {                ord = table->perm[N->index];                stack[SP++] = Cudd_Regular(cuddE(N));                table->subtables[ord].dead++;                N = cuddT(N);            }        } else {            cuddSatDec(N->ref);            N = stack[--SP];        }    } while (SP != 0);} /* end of Cudd_RecursiveDeref */

/**Function********************************************************************  Synopsis    [Performs the recursive steps of Cudd_bddBoleanDiff.]  Description [Performs the recursive steps of Cudd_bddBoleanDiff.  Returns the BDD obtained by XORing the cofactors of f with respect to  var if successful; NULL otherwise. Exploits the fact that dF/dx =  dF'/dx.]  SideEffects [None]  SeeAlso     []******************************************************************************/DdNode *cuddBddBooleanDiffRecur(  DdManager * manager,  DdNode * f,  DdNode * var){    DdNode *T, *E, *res, *res1, *res2;    statLine(manager);    if (cuddI(manager,f->index) > manager->perm[var->index]) {	/* f does not depend on var. */	return(Cudd_Not(DD_ONE(manager)));    }    /* From now on, f is non-constant. */    /* If the two indices are the same, so are their levels. */    if (f->index == var->index) {	res = cuddBddXorRecur(manager, cuddT(f), cuddE(f));        return(res);    }    /* From now on, cuddI(manager,f->index) < cuddI(manager,cube->index). */    /* Check the cache. */    res = cuddCacheLookup2(manager, cuddBddBooleanDiffRecur, f, var);    if (res != NULL) {	return(res);    }    /* Compute the cofactors of f. */    T = cuddT(f); E = cuddE(f);    res1 = cuddBddBooleanDiffRecur(manager, T, var);    if (res1 == NULL) return(NULL);    cuddRef(res1);    res2 = cuddBddBooleanDiffRecur(manager, Cudd_Regular(E), var);    if (res2 == NULL) {	Cudd_IterDerefBdd(manager, res1);	return(NULL);    }    cuddRef(res2);    /* ITE takes care of possible complementation of res1 and of the    ** case in which res1 == res2. */    res = cuddBddIteRecur(manager, manager->vars[f->index], res1, res2);    if (res == NULL) {	Cudd_IterDerefBdd(manager, res1);	Cudd_IterDerefBdd(manager, res2);	return(NULL);    }    cuddDeref(res1);    cuddDeref(res2);    cuddCacheInsert2(manager, cuddBddBooleanDiffRecur, f, var, res);    return(res);} /* end of cuddBddBooleanDiffRecur */

/**Function********************************************************************  Synopsis [Increases the reference count of a node, if it is not  saturated.]  Description []  SideEffects [None]  SeeAlso     [Cudd_RecursiveDeref Cudd_Deref]******************************************************************************/voidCudd_Ref(  DdNode * n){    n = Cudd_Regular(n);    cuddSatInc(n->ref);} /* end of Cudd_Ref */

ref_t shadow_absval(shadow_mgr mgr, ref_t r) {    if (do_ref(mgr))	return REF_ABSVAL(r);    else {	dd_type_t dtype = find_type(mgr, r);	DdNode *n = ref2dd(mgr, r);	DdNode *an = Cudd_Regular(n);	return dd2ref(an, dtype);    }}

double Prob(DdNode *node )/* compute the probability of the expression rooted at nodenodes is used to store nodes for which the probability has alread been computedso that it is not recomputed */{    int comp;    int index;    double res,resT,resF;    double p;    double * value_p;    DdNode **key,*T,*F,*nodereg;    double *rp;    comp=Cudd_IsComplement(node);    if (Cudd_IsConstant(node))    {        if (comp)            return 0.0;        else            return 1.0;    }    else    {        nodereg=Cudd_Regular(node);        value_p=g_hash_table_lookup(nodes,&node);        if (value_p!=NULL)        {            if (comp)                return 1-*value_p;            else                return *value_p;        }        else        {            index=Cudd_NodeReadIndex(node);            p=probs[index];            T = Cudd_T(node);            F = Cudd_E(node);            resT=Prob(T);            resF=Prob(F);            res=p*resT+(1-p)*resF;            key=(DdNode **)malloc(sizeof(DdNode *));            *key=nodereg;            rp=(double *)malloc(sizeof(double));            *rp=res;            g_hash_table_insert(nodes, key, rp);            if (comp)                return 1-res;            else                return res;        }    }}

voidDddmpSetVisitedCnf (  DdNode *f     /* IN: BDD node to be marked (as visited) */  ){  f = Cudd_Regular(f);  f->next = (DdNode *)(uintptr_t)((int)((uintptr_t)(f->next))|01);  return;}

/**Function********************************************************************  Synopsis    [Brings children of a dead node back.]  Description []  SideEffects [None]  SeeAlso     [cuddReclaimZdd]******************************************************************************/voidcuddReclaim(  DdManager * table,  DdNode * n){    DdNode *N;    int ord;    DdNodePtr *stack = table->stack;    int SP = 1;    double initialDead = table->dead;    N = Cudd_Regular(n);#ifdef DD_DEBUG    assert(N->ref == 0);#endif    do {        if (N->ref == 0) {            N->ref = 1;            table->dead--;            if (cuddIsConstant(N)) {                table->constants.dead--;                N = stack[--SP];            } else {                ord = table->perm[N->index];                stack[SP++] = Cudd_Regular(cuddE(N));                table->subtables[ord].dead--;                N = cuddT(N);            }        } else {            cuddSatInc(N->ref);            N = stack[--SP];        }    } while (SP != 0);    N = Cudd_Regular(n);    cuddSatDec(N->ref);    table->reclaimed += initialDead - table->dead;} /* end of cuddReclaim */

/**Function********************************************************************  Synopsis    [Checks whether a variable is dependent on others in a  function.]  Description [Checks whether a variable is dependent on others in a  function.  Returns 1 if the variable is dependent; 0 otherwise. No  new nodes are created.]  SideEffects [None]  SeeAlso     []******************************************************************************/intCudd_bddVarIsDependent(  DdManager *dd,		/* manager */  DdNode *f,			/* function */  DdNode *var			/* variable */){    DdNode *F, *res, *zero, *ft, *fe;    unsigned topf, level;    DD_CTFP cacheOp;    int retval;    /* NuSMV: begin add */    abort(); /* NOT USED BY NUSMV */    /* NuSMV: begin end */    zero = Cudd_Not(DD_TRUE(dd));    if (Cudd_IsConstant(f)) return(f == zero);    /* From now on f is not constant. */    F = Cudd_Regular(f);    topf = (unsigned) dd->perm[F->index];    level = (unsigned) dd->perm[var->index];    /* Check terminal case. If topf > index of var, f does not depend on var.    ** Therefore, var is not dependent in f. */    if (topf > level) {	return(0);    }    cacheOp = (DD_CTFP) Cudd_bddVarIsDependent;    res = cuddCacheLookup2(dd,cacheOp,f,var);    if (res != NULL) {	return(res != zero);    }    /* Compute cofactors. */    ft = Cudd_NotCond(cuddT(F), f != F);    fe = Cudd_NotCond(cuddE(F), f != F);    if (topf == level) {	retval = Cudd_bddLeq(dd,ft,Cudd_Not(fe));    } else {	retval = Cudd_bddVarIsDependent(dd,ft,var) &&	    Cudd_bddVarIsDependent(dd,fe,var);    }    cuddCacheInsert2(dd,cacheOp,f,var,Cudd_NotCond(zero,retval));    return(retval);} /* Cudd_bddVarIsDependent */

/**Function********************************************************************  Synopsis [Picks unique member from equiv expressions.]  Description [Makes sure the first two pointers are regular.  This  mat require the complementation of the result, which is signaled by  returning 1 instead of 0.  This function is simpler than the general  case because it assumes that no two arguments are the same or  complementary, and no argument is constant.]  SideEffects [None]  SeeAlso     [bddVarToConst bddVarToCanonical]******************************************************************************/static intbddVarToCanonicalSimple(  DdManager * dd,  DdNode ** fp,  DdNode ** gp,  DdNode ** hp,  unsigned int * topfp,  unsigned int * topgp,  unsigned int * tophp){    register DdNode             *r, *f, *g, *h;    int                         comple, change;    f = *fp;    g = *gp;    h = *hp;    change = 0;    /* adjust pointers so that the first 2 arguments to ITE are regular */    if (Cudd_IsComplement(f)) { /* ITE(!F,G,H) = ITE(F,H,G) */        f = Cudd_Not(f);        r = g;        g = h;        h = r;        change = 1;    }    comple = 0;    if (Cudd_IsComplement(g)) { /* ITE(F,!G,H) = !ITE(F,G,!H) */        g = Cudd_Not(g);        h = Cudd_Not(h);        change = 1;        comple = 1;    }    if (change) {        *fp = f;        *gp = g;        *hp = h;    }    /* Here we can skip the use of cuddI, because the operands are known    ** to be non-constant.    */    *topfp = dd->perm[f->index];    *topgp = dd->perm[g->index];    *tophp = dd->perm[Cudd_Regular(h)->index];    return(comple);} /* end of bddVarToCanonicalSimple */

static voidI_BDD_minterms_aux (DdManager * dd, DdNode * node, char *list,                    List * minterm_list){  DdNode *N, *Nv, *Nnv;  int i, index;  char *new_list;  N = Cudd_Regular (node);  if (cuddIsConstant (N))    {      /* Terminal case: Print one cube based on the current recursion         ** path, unless we have reached the background value (ADDs) or         ** the logical zero (BDDs).       */      if (node != dd->background && node != Cudd_Not (dd->one))        {          if (!(new_list = (char *) malloc (sizeof (char) * dd->size)))            I_punt ("I_BDD_minterms_aux: cannot allocate array");          for (i = 0; i < dd->size; i++)	    new_list[i] = list[i];          if (cuddV (node) != 1)            I_punt ("I_BDD_minterms_aux: bad BDD");          *minterm_list = List_insert_last (*minterm_list, new_list);        }    }  else    {      Nv = cuddT (N);      Nnv = cuddE (N);      if (Cudd_IsComplement (node))        {          Nv = Cudd_Not (Nv);          Nnv = Cudd_Not (Nnv);        }      index = N->index;      list[index] = 0;      I_BDD_minterms_aux (dd, Nnv, list, minterm_list);      list[index] = 1;      I_BDD_minterms_aux (dd, Nv, list, minterm_list);      list[index] = 2;    }  return;}

/**Function********************************************************************  Synopsis    [List of nodes below some level reachable from a root node.]  Description [List of nodes below some level reachable from a root  node. if max>0, the list is at most of size max (partial list).  Given a BDD/ADD f and a variable level level the function  performs a depth-first search of the graph rooted at $f$ and select  the first nodes encountered such that their variable level is equal  or below the level level. If level==CUDD_MAXINDEX, then the  functions collects only constant nodes. The background node is not  returned in the result if take_background==0.  Returns the list of nodes, the index of which has its level equal or below  level, and the size of the list in *psize, if successful; NULL  otherwise. Nodes in the list are NOT referenced.]  SideEffects [None]  SeeAlso     []******************************************************************************/cuddaux_list_t*Cuddaux_NodesBelowLevel(DdManager* manager, DdNode* f, int level, size_t max, size_t* psize, bool take_background){  cuddaux_list_t* res = 0;  st_table* visited;  visited = st_init_table(st_ptrcmp,st_ptrhash);  if (visited==NULL) return NULL;  *psize = 0;  cuddauxNodesBelowLevelRecur(manager, Cudd_Regular(f), level, &res, visited, max, psize, take_background);  if (res==NULL) *psize=0;  assert (max>0 ? *psize<=max : 1);  st_free_table(visited);  return(res);}

double Prob(DdNode *node, int comp_par)/* compute the probability of the expression rooted at node.table is used to store nodeB for which the probability has alread been computedso that it is not recomputed */{  int index, mVarIndex, comp, pos;  variable v;  double res;  double p, pt, pf, BChild0, BChild1;  double *value_p;  DdNode *nodekey, *T, *F;  comp = Cudd_IsComplement(node);  comp = (comp && !comp_par) || (!comp && comp_par);  if (Cudd_IsConstant(node)) {    if (comp)      return 0.0;    else      return 1.0;  } else {    nodekey = Cudd_Regular(node);    value_p = get_value(table, nodekey);    if (value_p != NULL)      return *value_p;    else {      index = Cudd_NodeReadIndex(node); // Returns the index of the node. The                                        // node pointer can be either regular or                                        // complemented.      // The index field holds the name of the variable that labels the node.      // The index of a variable is a permanent attribute that reflects the      // order of creation.      p = probs_ex[ex][index];      T = Cudd_T(node);      F = Cudd_E(node);      pf = Prob(F, comp);      pt = Prob(T, comp);      BChild0 = pf * (1 - p);      BChild1 = pt * p;      mVarIndex = bVar2mVar_ex[ex][index];      v = vars_ex[ex][mVarIndex];      pos = index - v.firstBoolVar;      res = BChild0 + BChild1;      add_node(table, nodekey, res);      return res;    }  }}

/**Function********************************************************************  Synopsis    [Computes the children of g.]  Description []  SideEffects [None]  SeeAlso     []******************************************************************************/voidcuddGetBranches(  DdNode * g,  DdNode ** g1,  DdNode ** g0){    DdNode	*G = Cudd_Regular(g);    *g1 = cuddT(G);    *g0 = cuddE(G);    if (Cudd_IsComplement(g)) {	*g1 = Cudd_Not(*g1);	*g0 = Cudd_Not(*g0);    }} /* end of cuddGetBranches */

/** * Groups some variables such that they "stick" together during the reordering process. * @param which The variables that should be grouped. They must have not been allocated a non-grouped variable in between the allocation of two grouped variables. */void BFBddManager::groupVariables(const std::vector<BFBdd> &which) {	// Only allow continuous variables to be grouped.	std::set<DdHalfWord> indices;	DdHalfWord min = std::numeric_limits<DdHalfWord>::max();	DdHalfWord max = std::numeric_limits<DdHalfWord>::min();	for (unsigned int i = 0; i < which.size(); i++) {		DdNode *node = which[i].node;		DdHalfWord index = ((Cudd_Regular(node))->index);		if (index < min)			min = index;		if (index > max)			max = index;		indices.insert(index);	}	if ((unsigned int) (max - min + 1) != indices.size())		throw std::runtime_error("Error in BFBddManager::groupVariables(const std::vector<BFBdd> &which) - Can only group continuous variables!/n");	Cudd_MakeTreeNode(mgr, min, max - min + 1, MTR_DEFAULT);}