C++ cuddUniqueInter函数代码示例

OStack程序员社区-中国程序员成长平台 › 门户 › 编程› C++›C++教程

原作者: [db:作者] 来自: [db:来源] 收藏邀请

本文整理汇总了C++中cuddUniqueInter函数的典型用法代码示例。如果您正苦于以下问题：C++ cuddUniqueInter函数的具体用法？C++ cuddUniqueInter怎么用？C++ cuddUniqueInter使用的例子？那么恭喜您, 这里精选的函数代码示例或许可以为您提供帮助。

在下文中一共展示了cuddUniqueInter函数的20个代码示例，这些例子默认根据受欢迎程度排序。您可以为喜欢或者感觉有用的代码点赞，您的评价将有助于我们的系统推荐出更棒的C++代码示例。

示例1: cuddauxSupportRecur

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

开发者ID:thizanne，项目名称:mlcuddidl，代码行数:71，代码来源:cuddauxMisc.c

示例2: addBddDoInterval

/**Function********************************************************************

  Synopsis    [Performs the recursive step for Cudd_addBddInterval.]

  Description [Performs the recursive step for Cudd_addBddInterval.
  Returns a pointer to the BDD if successful; NULL otherwise.]

  SideEffects [None]

  SeeAlso     [addBddDoThreshold addBddDoStrictThreshold]

******************************************************************************/
static DdNode *
addBddDoInterval(
  DdManager * dd,
  DdNode * f,
  DdNode * l,
  DdNode * u)
{
    DdNode *res, *T, *E;
    DdNode *fv, *fvn;
    int v;

    statLine(dd);
    /* Check terminal case. */
    if (cuddIsConstant(f)) {
	return(Cudd_NotCond(DD_TRUE(dd),cuddV(f) < cuddV(l) || cuddV(f) > cuddV(u)));
    }

    /* Check cache. */
    res = cuddCacheLookup(dd,DD_ADD_BDD_DO_INTERVAL_TAG,f,l,u);
    if (res != NULL) return(res);

    /* Recursive step. */
    v = f->index;
    fv = cuddT(f); fvn = cuddE(f);

    T = addBddDoInterval(dd,fv,l,u);
    if (T == NULL) return(NULL);
    cuddRef(T);

    E = addBddDoInterval(dd,fvn,l,u);
    if (E == NULL) {
	Cudd_RecursiveDeref(dd, T);
	return(NULL);
    }
    cuddRef(E);
    if (Cudd_IsComplement(T)) {
	res = (T == E) ? Cudd_Not(T) : cuddUniqueInter(dd,v,Cudd_Not(T),Cudd_Not(E));
	if (res == NULL) {
	    Cudd_RecursiveDeref(dd, T);
	    Cudd_RecursiveDeref(dd, E);
	    return(NULL);
	}
	res = Cudd_Not(res);
    } else {
	res = (T == E) ? T : cuddUniqueInter(dd,v,T,E);
	if (res == NULL) {
	    Cudd_RecursiveDeref(dd, T);
	    Cudd_RecursiveDeref(dd, E);
	    return(NULL);
	}
    }
    cuddDeref(T);
    cuddDeref(E);

    /* Store result. */
    cuddCacheInsert(dd,DD_ADD_BDD_DO_INTERVAL_TAG,f,l,u,res);

    return(res);

} /* end of addBddDoInterval */

开发者ID:ancailliau，项目名称:pynusmv，代码行数:72，代码来源:cuddBridge.c

示例3: cuddauxAddGuardOfNodeRecur

DdNode*
cuddauxAddGuardOfNodeRecur(DdManager* manager, DdNode* f, DdNode* h)
{
  DdNode *one, *res, *T, *E;
  int topf, toph;

  /* Handle terminal cases */
  one = DD_ONE(manager);
  if (f==h){
    return(one);
  }
  topf = cuddI(manager,f->index);
  toph = cuddI(manager,h->index);
  if (topf >= toph){
    return Cudd_Not(one);
  }

  /* Look in the cache */
  res = cuddCacheLookup2(manager,Cuddaux_addGuardOfNode,f,h);
  if (res != NULL)
    return(res);

  T = cuddauxAddGuardOfNodeRecur(manager,cuddT(f),h);
  if (T == NULL)
    return(NULL);
  cuddRef(T);
  E = cuddauxAddGuardOfNodeRecur(manager,cuddE(f),h);
  if (E == NULL){
    Cudd_IterDerefBdd(manager, T);
    return(NULL);
  }
  cuddRef(E);
  if (T == E){
    res = T;
  }
  else {
    if (Cudd_IsComplement(T)){
      res = cuddUniqueInter(manager,f->index,Cudd_Not(T),Cudd_Not(E));
      if (res == NULL) {
	Cudd_IterDerefBdd(manager, T);
	Cudd_IterDerefBdd(manager, E);
	return(NULL);
      }
      res = Cudd_Not(res);
    }
    else {
      res = cuddUniqueInter(manager,f->index,T,E);
      if (res == NULL) {
	Cudd_IterDerefBdd(manager, T);
	Cudd_IterDerefBdd(manager, E);
	return(NULL);
      }
    }
  }
  cuddDeref(T);
  cuddDeref(E);
  cuddCacheInsert2(manager,Cuddaux_addGuardOfNode,f,h,res);
  return(res);
}

开发者ID:thizanne，项目名称:mlcuddidl，代码行数:59，代码来源:cuddauxMisc.c

示例4: addBddDoStrictThreshold

/**Function********************************************************************

  Synopsis    [Performs the recursive step for Cudd_addBddStrictThreshold.]

  Description [Performs the recursive step for Cudd_addBddStrictThreshold.
  Returns a pointer to the BDD if successful; NULL otherwise.]

  SideEffects [None]

  SeeAlso     [addBddDoThreshold]

******************************************************************************/
static DdNode *
addBddDoStrictThreshold(
  DdManager * dd,
  DdNode * f,
  DdNode * val)
{
    DdNode *res, *T, *E;
    DdNode *fv, *fvn;
    int v;

    statLine(dd);
    /* Check terminal case. */
    if (cuddIsConstant(f)) {
	return(Cudd_NotCond(DD_TRUE(dd),cuddV(f) <= cuddV(val)));
    }

    /* Check cache. */
    res = cuddCacheLookup2(dd,addBddDoStrictThreshold,f,val);
    if (res != NULL) return(res);

    /* Recursive step. */
    v = f->index;
    fv = cuddT(f); fvn = cuddE(f);

    T = addBddDoStrictThreshold(dd,fv,val);
    if (T == NULL) return(NULL);
    cuddRef(T);

    E = addBddDoStrictThreshold(dd,fvn,val);
    if (E == NULL) {
	Cudd_RecursiveDeref(dd, T);
	return(NULL);
    }
    cuddRef(E);
    if (Cudd_IsComplement(T)) {
	res = (T == E) ? Cudd_Not(T) : cuddUniqueInter(dd,v,Cudd_Not(T),Cudd_Not(E));
	if (res == NULL) {
	    Cudd_RecursiveDeref(dd, T);
	    Cudd_RecursiveDeref(dd, E);
	    return(NULL);
	}
	res = Cudd_Not(res);
    } else {
	res = (T == E) ? T : cuddUniqueInter(dd,v,T,E);
	if (res == NULL) {
	    Cudd_RecursiveDeref(dd, T);
	    Cudd_RecursiveDeref(dd, E);
	    return(NULL);
	}
    }
    cuddDeref(T);
    cuddDeref(E);

    /* Store result. */
    cuddCacheInsert2(dd,addBddDoStrictThreshold,f,val,res);

    return(res);

} /* end of addBddDoStrictThreshold */

开发者ID:ancailliau，项目名称:pynusmv，代码行数:71，代码来源:cuddBridge.c

示例5: Extra_bddSpaceCanonVars

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

开发者ID:kyotobay，项目名称:ABC_withFD_check，代码行数:70，代码来源:extraBddAuto.c

示例6: pair

/**Function********************************************************************

  Synopsis    [Computes a caching cube.]

  Description [It is known that bVars is a cube representing a subset of bVarsAll
  this function computes the canonical representation of the pair (bVarsAll, bVars) 
  by one DD node the convention is the following: if ( bVars == bVarsAll), return bVarsAll,
  otherwise return ITE(x, cuddT(bVarsAll), bVars), where x is the topmost var in bVarsAll.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
DdNode * extraCachingCube( DdManager * dd, DdNode * bVarsAll, DdNode * bVars )
{
	if ( bVars == bVarsAll)  
		return bVarsAll;
	else
		return cuddUniqueInter( dd, bVarsAll->index, cuddT(bVarsAll), bVars );
	// because bVarsAll is positive cube, cuddT(bVarsAll) is never complemented
}

开发者ID:chastell，项目名称:cirkit，代码行数:22，代码来源:extraAddSpectra.c

示例7: addDoIthBit

/**Function********************************************************************

  Synopsis    [Performs the recursive step for Cudd_addIthBit.]

  Description [Performs the recursive step for Cudd_addIthBit.
  Returns a pointer to the BDD if successful; NULL otherwise.]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
static DdNode *
addDoIthBit(
  DdManager * dd,
  DdNode * f,
  DdNode * index)
{
    DdNode *res, *T, *E;
    DdNode *fv, *fvn;
    int mask, value;
    int v;

    statLine(dd);
    /* Check terminal case. */
    if (cuddIsConstant(f)) {
	mask = 1 << ((int) cuddV(index));
	value = (int) cuddV(f);
	return((value & mask) == 0 ? DD_ZERO(dd) : DD_ONE(dd));
    }

    /* Check cache. */
    res = cuddCacheLookup2(dd,addDoIthBit,f,index);
    if (res != NULL) return(res);

    /* Recursive step. */
    v = f->index;
    fv = cuddT(f); fvn = cuddE(f);

    T = addDoIthBit(dd,fv,index);
    if (T == NULL) return(NULL);
    cuddRef(T);

    E = addDoIthBit(dd,fvn,index);
    if (E == NULL) {
	Cudd_RecursiveDeref(dd, T);
	return(NULL);
    }
    cuddRef(E);

    res = (T == E) ? T : cuddUniqueInter(dd,v,T,E);
    if (res == NULL) {
	Cudd_RecursiveDeref(dd, T);
	Cudd_RecursiveDeref(dd, E);
	return(NULL);
    }
    cuddDeref(T);
    cuddDeref(E);

    /* Store result. */
    cuddCacheInsert2(dd,addDoIthBit,f,index,res);

    return(res);

} /* end of addDoIthBit */

开发者ID:amusant，项目名称:vtr-verilog-to-routing，代码行数:65，代码来源:cuddAddFind.c

示例8: selectMintermsFromUniverse

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

开发者ID:Oliii，项目名称:MTBDD，代码行数:65，代码来源:cuddSplit.c

示例9: cuddAddRoundOffRecur

/**
  @brief Implements the recursive step of Cudd_addRoundOff.

  @return a pointer to the result.

  @sideeffect None

*/
DdNode *
cuddAddRoundOffRecur(
  DdManager * dd,
  DdNode * f,
  double  trunc)
{

    DdNode *res, *fv, *fvn, *T, *E;
    double n;
    DD_CTFP1 cacheOp;

    statLine(dd);
    if (cuddIsConstant(f)) {
	n = ceil(cuddV(f)*trunc)/trunc;
	res = cuddUniqueConst(dd,n);
	return(res);
    }
    cacheOp = (DD_CTFP1) Cudd_addRoundOff;
    res = cuddCacheLookup1(dd,cacheOp,f);
    if (res != NULL) {
	return(res);
    }
    checkWhetherToGiveUp(dd);
    /* Recursive Step */
    fv = cuddT(f);
    fvn = cuddE(f);
    T = cuddAddRoundOffRecur(dd,fv,trunc);
    if (T == NULL) {
       return(NULL);
    }
    cuddRef(T);
    E = cuddAddRoundOffRecur(dd,fvn,trunc);
    if (E == NULL) {
	Cudd_RecursiveDeref(dd,T);
	return(NULL);
    }
    cuddRef(E);
    res = (T == E) ? T : cuddUniqueInter(dd,(int)f->index,T,E);
    if (res == NULL) {
	Cudd_RecursiveDeref(dd,T);
	Cudd_RecursiveDeref(dd,E);
	return(NULL);
    }
    cuddDeref(T);
    cuddDeref(E);

    /* Store result. */
    cuddCacheInsert1(dd,cacheOp,f,res);
    return(res);

} /* end of cuddAddRoundOffRecur */

开发者ID:VerifiableRobotics，项目名称:slugs，代码行数:59，代码来源:cuddAddNeg.c

示例10: cuddAddMonadicApplyWithDataRecur

DdNode *
cuddAddMonadicApplyWithDataRecur(
  DdManager * dd,
  DD_MAOPD op,
  DdNode * f,
	void * data)
{
    DdNode *res, *ft, *fe, *T, *E;
    unsigned int index;

    /* Check terminal cases. */
    statLine(dd);
    res = (*op)(dd,f, data);
    if (res != NULL) return(res);


    /* Check cache. */
    res = cuddCacheLookup1(dd,(DD_MAOP)global_bloody_counter_unary,f);
    if (res != NULL) return(res);

    /* Recursive step. */
    index = f->index;
    ft = cuddT(f);
    fe = cuddE(f);

    T = cuddAddMonadicApplyWithDataRecur(dd,op,ft, data);
    if (T == NULL) return(NULL);
    cuddRef(T);

    E = cuddAddMonadicApplyWithDataRecur(dd,op,fe, data);
    if (E == NULL) {
	Cudd_RecursiveDeref(dd,T);
	return(NULL);
    }
    cuddRef(E);

    res = (T == E) ? T : cuddUniqueInter(dd,(int)index,T,E);
    if (res == NULL) {
	Cudd_RecursiveDeref(dd, T);
	Cudd_RecursiveDeref(dd, E);
	return(NULL);
    }
    cuddDeref(T);
    cuddDeref(E);

    /* Store result. */
    cuddCacheInsert1(dd,(DD_MAOP)global_bloody_counter_unary,f,res);

    return(res);

} /* end of cuddAddMonadicApplyWithDataRecur */

开发者ID:ondrik，项目名称:cudd4libsfta，代码行数:51，代码来源:cuddAddApply.c

示例11: cuddAddMonadicApplyRecur

/**Function********************************************************************

  Synopsis    [Performs the recursive step of Cudd_addMonadicApply.]

  Description [Performs the recursive step of Cudd_addMonadicApply. Returns a
  pointer to the result if successful; NULL otherwise.]

  SideEffects [None]

  SeeAlso     [cuddAddApplyRecur]

******************************************************************************/
DdNode *
cuddAddMonadicApplyRecur(
  DdManager * dd,
  DdNode * (*op)(DdManager *, DdNode *),
  DdNode * f)
{
    DdNode *res, *ft, *fe, *T, *E;
    unsigned int ford;
    unsigned int index;

    /* Check terminal cases. */
    statLine(dd);
    res = (*op)(dd,f);
    if (res != NULL) return(res);

    /* Check cache. */
    res = cuddCacheLookup1(dd,op,f);
    if (res != NULL) return(res);

    /* Recursive step. */
    ford = cuddI(dd,f->index);
    index = f->index;
    ft = cuddT(f);
    fe = cuddE(f);

    T = cuddAddMonadicApplyRecur(dd,op,ft);
    if (T == NULL) return(NULL);
    cuddRef(T);

    E = cuddAddMonadicApplyRecur(dd,op,fe);
    if (E == NULL) {
	Cudd_RecursiveDeref(dd,T);
	return(NULL);
    }
    cuddRef(E);

    res = (T == E) ? T : cuddUniqueInter(dd,(int)index,T,E);
    if (res == NULL) {
	Cudd_RecursiveDeref(dd, T);
	Cudd_RecursiveDeref(dd, E);
	return(NULL);
    }
    cuddDeref(T);
    cuddDeref(E);

    /* Store result. */
    cuddCacheInsert1(dd,op,f,res);

    return(res);

} /* end of cuddAddMonadicApplyRecur */

开发者ID:amusant，项目名称:vtr-verilog-to-routing，代码行数:63，代码来源:cuddAddApply.c

示例12: cuddAddNegateRecur

/**
  @brief Implements the recursive step of Cudd_addNegate.

  @return a pointer to the result.

  @sideeffect None

*/
DdNode *
cuddAddNegateRecur(
  DdManager * dd,
  DdNode * f)
{
    DdNode *res,
	    *fv, *fvn,
	    *T, *E;

    statLine(dd);
    /* Check terminal cases. */
    if (cuddIsConstant(f)) {
	res = cuddUniqueConst(dd,-cuddV(f));
	return(res);
    }

    /* Check cache */
    res = cuddCacheLookup1(dd,Cudd_addNegate,f);
    if (res != NULL) return(res);

    checkWhetherToGiveUp(dd);

    /* Recursive Step */
    fv = cuddT(f);
    fvn = cuddE(f);
    T = cuddAddNegateRecur(dd,fv);
    if (T == NULL) return(NULL);
    cuddRef(T);

    E = cuddAddNegateRecur(dd,fvn);
    if (E == NULL) {
	Cudd_RecursiveDeref(dd,T);
	return(NULL);
    }
    cuddRef(E);
    res = (T == E) ? T : cuddUniqueInter(dd,(int)f->index,T,E);
    if (res == NULL) {
	Cudd_RecursiveDeref(dd, T);
	Cudd_RecursiveDeref(dd, E);
	return(NULL);
    }
    cuddDeref(T);
    cuddDeref(E);

    /* Store result. */
    cuddCacheInsert1(dd,Cudd_addNegate,f,res);

    return(res);

} /* end of cuddAddNegateRecur */

开发者ID:VerifiableRobotics，项目名称:slugs，代码行数:58，代码来源:cuddAddNeg.c

示例13: cuddAddScalarInverseRecur

/**
  @brief Performs the recursive step of addScalarInverse.

  @return a pointer to the resulting %ADD in case of success. Returns
  NULL if any discriminants smaller than epsilon is encountered.

  @sideeffect None

*/
DdNode *
cuddAddScalarInverseRecur(
  DdManager * dd,
  DdNode * f,
  DdNode * epsilon)
{
    DdNode *t, *e, *res;
    CUDD_VALUE_TYPE value;

    statLine(dd);
    if (cuddIsConstant(f)) {
	if (ddAbs(cuddV(f)) < cuddV(epsilon)) return(NULL);
	value = 1.0 / cuddV(f);
	res = cuddUniqueConst(dd,value);
	return(res);
    }

    res = cuddCacheLookup2(dd,Cudd_addScalarInverse,f,epsilon);
    if (res != NULL) return(res);

    checkWhetherToGiveUp(dd);

    t = cuddAddScalarInverseRecur(dd,cuddT(f),epsilon);
    if (t == NULL) return(NULL);
    cuddRef(t);

    e = cuddAddScalarInverseRecur(dd,cuddE(f),epsilon);
    if (e == NULL) {
	Cudd_RecursiveDeref(dd, t);
	return(NULL);
    }
    cuddRef(e);

    res = (t == e) ? t : cuddUniqueInter(dd,(int)f->index,t,e);
    if (res == NULL) {
	Cudd_RecursiveDeref(dd, t);
	Cudd_RecursiveDeref(dd, e);
	return(NULL);
    }
    cuddDeref(t);
    cuddDeref(e);

    cuddCacheInsert2(dd,Cudd_addScalarInverse,f,epsilon,res);

    return(res);

} /* end of cuddAddScalarInverseRecur */

开发者ID:VerifiableRobotics，项目名称:slugs，代码行数:56，代码来源:cuddAddInv.c

示例14: cuddAddCmplRecur

/**Function********************************************************************

  Synopsis    [Performs the recursive step of Cudd_addCmpl.]

  Description [Performs the recursive step of Cudd_addCmpl. Returns a
  pointer to the resulting ADD if successful; NULL otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_addCmpl]

******************************************************************************/
DdNode *
cuddAddCmplRecur(
  DdManager * dd,
  DdNode * f)
{
    DdNode *one,*zero;
    DdNode *r,*Fv,*Fnv,*t,*e;

    statLine(dd);
    one = DD_ONE(dd);
    zero = DD_ZERO(dd); 

    if (cuddIsConstant(f)) {
        if (f == zero) {
	    return(one);
	} else {
	    return(zero);
	}
    }
    r = cuddCacheLookup1(dd,Cudd_addCmpl,f);
    if (r != NULL) {
	return(r);
    }
    Fv = cuddT(f);
    Fnv = cuddE(f);
    t = cuddAddCmplRecur(dd,Fv);
    if (t == NULL) return(NULL);
    cuddRef(t);
    e = cuddAddCmplRecur(dd,Fnv);
    if (e == NULL) {
	Cudd_RecursiveDeref(dd,t);
	return(NULL);
    }
    cuddRef(e);
    r = (t == e) ? t : cuddUniqueInter(dd,(int)f->index,t,e);
    if (r == NULL) {
	Cudd_RecursiveDeref(dd, t);
	Cudd_RecursiveDeref(dd, e);
	return(NULL);
    }
    cuddDeref(t);
    cuddDeref(e);
    cuddCacheInsert1(dd,Cudd_addCmpl,f,r);
    return(r);

} /* end of cuddAddCmplRecur */

开发者ID:maeon，项目名称:SBSAT，代码行数:58，代码来源:cuddAddIte.c

示例15: R

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

开发者ID:saidalfaraby，项目名称:DTP4TC，代码行数:101，代码来源:cuddPriority.c

示例16: testWalsh

/**Function********************************************************************

  Synopsis    [Tests Walsh matrix multiplication.]

  Description [Tests Walsh matrix multiplication.  Return 1 if successful;
  0 otherwise.]

  SideEffects [May create new variables in the manager.]

  SeeAlso     []

******************************************************************************/
static int
testWalsh(
  DdManager *dd /* manager */,
  int N /* number of variables */,
  int cmu /* use CMU approach to matrix multiplication */,
  int approach /* reordering approach */,
  int pr /* verbosity level */)
{
    DdNode *walsh1, *walsh2, *wtw;
    DdNode **x, **v, **z;
    int i, retval;
    DdNode *_true = DD_TRUE(dd);
    DdNode *_false = DD_FALSE(dd);

    if (N > 3) {
	x = ALLOC(DdNode *,N);
	v = ALLOC(DdNode *,N);
	z = ALLOC(DdNode *,N);

	for (i = N-1; i >= 0; i--) {
	    Cudd_Ref(x[i]=cuddUniqueInter(dd,3*i,_true,_false));
	    Cudd_Ref(v[i]=cuddUniqueInter(dd,3*i+1,_true,_false));
	    Cudd_Ref(z[i]=cuddUniqueInter(dd,3*i+2,_true,_false));
	}
	Cudd_Ref(walsh1 = Cudd_addWalsh(dd,v,z,N));
	if (pr>0) {(void) printf("walsh1"); Cudd_PrintDebug(dd,walsh1,2*N,pr);}
	Cudd_Ref(walsh2 = Cudd_addWalsh(dd,x,v,N));
	if (cmu) {
	    Cudd_Ref(wtw = Cudd_addTimesPlus(dd,walsh2,walsh1,v,N));
	} else {
	    Cudd_Ref(wtw = Cudd_addMatrixMultiply(dd,walsh2,walsh1,v,N));
	}
	if (pr>0) {(void) printf("wtw"); Cudd_PrintDebug(dd,wtw,2*N,pr);}

	if (approach != CUDD_REORDER_NONE) {
#ifdef DD_DEBUG
	    retval = Cudd_DebugCheck(dd);
	    if (retval != 0) {
		(void) fprintf(stderr,"Error reported by Cudd_DebugCheck\n");
		return(0);
	    }
#endif
	    retval = Cudd_ReduceHeap(dd,(Cudd_ReorderingType)approach,5);
	    if (retval == 0) {
		(void) fprintf(stderr,"Error reported by Cudd_ReduceHeap\n");
		return(0);
	    }
#ifdef DD_DEBUG
	    retval = Cudd_DebugCheck(dd);
	    if (retval != 0) {
		(void) fprintf(stderr,"Error reported by Cudd_DebugCheck\n");
		return(0);
	    }
#endif
	    if (approach == CUDD_REORDER_SYMM_SIFT ||
	    approach == CUDD_REORDER_SYMM_SIFT_CONV) {
		Cudd_SymmProfile(dd,0,dd->size-1);
	    }
	}
	/* Clean up. */
	Cudd_RecursiveDeref(dd, wtw);
	Cudd_RecursiveDeref(dd, walsh1);
	Cudd_RecursiveDeref(dd, walsh2);
	for (i=0; i < N; i++) {
	    Cudd_RecursiveDeref(dd, x[i]);
	    Cudd_RecursiveDeref(dd, v[i]);
	    Cudd_RecursiveDeref(dd, z[i]);
	}
	FREE(x);
	FREE(v);
	FREE(z);
    }

开发者ID:ancailliau，项目名称:pynusmv，代码行数:84，代码来源:testcudd.c

示例17: Cudd_Init

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

开发者ID:EliasVansteenkiste，项目名称:ConnectionRouter，代码行数:98，代码来源:cuddInit.c

示例18: cuddZddIsop


//.........这里部分代码省略.........
	Cudd_RecursiveDeref(dd, Isub1);
	Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
	Cudd_RecursiveDeref(dd, Lsuper0);
	Cudd_RecursiveDeref(dd, Lsuper1);
	Cudd_RecursiveDeref(dd, Ld);
	return(NULL);
    }
    Cudd_Ref(Ud);
    Cudd_RecursiveDeref(dd, Lsuper0);
    Cudd_RecursiveDeref(dd, Lsuper1);

    Id = cuddZddIsop(dd, Ld, Ud, &zdd_Id);
    if (Id == NULL) {
	Cudd_RecursiveDeref(dd, Isub0);
	Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
	Cudd_RecursiveDeref(dd, Isub1);
	Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
	Cudd_RecursiveDeref(dd, Ld);
	Cudd_RecursiveDeref(dd, Ud);
	return(NULL);
    }
    /*
    if ((!cuddIsConstant(Cudd_Regular(Id))) &&
	(Cudd_Regular(Id)->index != zdd_Id->index / 2 ||
	dd->permZ[index * 2] > dd->permZ[zdd_Id->index])) {
	printf("*** ERROR : illegal permutation in ZDD. ***\n");
    }
    */
    Cudd_Ref(Id);
    Cudd_Ref(zdd_Id);
    Cudd_RecursiveDeref(dd, Ld);
    Cudd_RecursiveDeref(dd, Ud);

    x = cuddUniqueInter(dd, index, one, zero);
    if (x == NULL) {
	Cudd_RecursiveDeref(dd, Isub0);
	Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
	Cudd_RecursiveDeref(dd, Isub1);
	Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
	Cudd_RecursiveDeref(dd, Id);
	Cudd_RecursiveDerefZdd(dd, zdd_Id);
	return(NULL);
    }
    Cudd_Ref(x);
    /* term0 = x * Isub0 */
    term0 = cuddBddAndRecur(dd, Cudd_Not(x), Isub0);
    if (term0 == NULL) {
	Cudd_RecursiveDeref(dd, Isub0);
	Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
	Cudd_RecursiveDeref(dd, Isub1);
	Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
	Cudd_RecursiveDeref(dd, Id);
	Cudd_RecursiveDerefZdd(dd, zdd_Id);
	Cudd_RecursiveDeref(dd, x);
	return(NULL);
    }
    Cudd_Ref(term0);
    Cudd_RecursiveDeref(dd, Isub0);
    /* term1 = x * Isub1 */
    term1 = cuddBddAndRecur(dd, x, Isub1);
    if (term1 == NULL) {
	Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
	Cudd_RecursiveDeref(dd, Isub1);
	Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
	Cudd_RecursiveDeref(dd, Id);
	Cudd_RecursiveDerefZdd(dd, zdd_Id);

开发者ID:ansonn，项目名称:esl_systemc，代码行数:67，代码来源:cuddZddIsop.c

示例19: cuddBddIsop


//.........这里部分代码省略.........
    }
    Cudd_Ref(Lsuper1);
    Usuper0 = Unv;
    Usuper1 = Uv;

    /* Ld = Lsuper0 + Lsuper1 */
    Ld = cuddBddAndRecur(dd, Cudd_Not(Lsuper0), Cudd_Not(Lsuper1));
    Ld = Cudd_NotCond(Ld, Ld != NULL);
    if (Ld == NULL) {
	Cudd_RecursiveDeref(dd, Isub0);
	Cudd_RecursiveDeref(dd, Isub1);
	Cudd_RecursiveDeref(dd, Lsuper0);
	Cudd_RecursiveDeref(dd, Lsuper1);
	return(NULL);
    }
    Cudd_Ref(Ld);
    Ud = cuddBddAndRecur(dd, Usuper0, Usuper1);
    if (Ud == NULL) {
	Cudd_RecursiveDeref(dd, Isub0);
	Cudd_RecursiveDeref(dd, Isub1);
	Cudd_RecursiveDeref(dd, Lsuper0);
	Cudd_RecursiveDeref(dd, Lsuper1);
	Cudd_RecursiveDeref(dd, Ld);
	return(NULL);
    }
    Cudd_Ref(Ud);
    Cudd_RecursiveDeref(dd, Lsuper0);
    Cudd_RecursiveDeref(dd, Lsuper1);

    Id = cuddBddIsop(dd, Ld, Ud);
    if (Id == NULL) {
	Cudd_RecursiveDeref(dd, Isub0);
	Cudd_RecursiveDeref(dd, Isub1);
	Cudd_RecursiveDeref(dd, Ld);
	Cudd_RecursiveDeref(dd, Ud);
	return(NULL);
    }
    Cudd_Ref(Id);
    Cudd_RecursiveDeref(dd, Ld);
    Cudd_RecursiveDeref(dd, Ud);

    x = cuddUniqueInter(dd, index, one, zero);
    if (x == NULL) {
	Cudd_RecursiveDeref(dd, Isub0);
	Cudd_RecursiveDeref(dd, Isub1);
	Cudd_RecursiveDeref(dd, Id);
	return(NULL);
    }
    Cudd_Ref(x);
    term0 = cuddBddAndRecur(dd, Cudd_Not(x), Isub0);
    if (term0 == NULL) {
	Cudd_RecursiveDeref(dd, Isub0);
	Cudd_RecursiveDeref(dd, Isub1);
	Cudd_RecursiveDeref(dd, Id);
	Cudd_RecursiveDeref(dd, x);
	return(NULL);
    }
    Cudd_Ref(term0);
    Cudd_RecursiveDeref(dd, Isub0);
    term1 = cuddBddAndRecur(dd, x, Isub1);
    if (term1 == NULL) {
	Cudd_RecursiveDeref(dd, Isub1);
	Cudd_RecursiveDeref(dd, Id);
	Cudd_RecursiveDeref(dd, x);
	Cudd_RecursiveDeref(dd, term0);
	return(NULL);
    }
    Cudd_Ref(term1);
    Cudd_RecursiveDeref(dd, x);
    Cudd_RecursiveDeref(dd, Isub1);
    /* sum = term0 + term1 */
    sum = cuddBddAndRecur(dd, Cudd_Not(term0), Cudd_Not(term1));
    sum = Cudd_NotCond(sum, sum != NULL);
    if (sum == NULL) {
	Cudd_RecursiveDeref(dd, Id);
	Cudd_RecursiveDeref(dd, term0);
	Cudd_RecursiveDeref(dd, term1);
	return(NULL);
    }
    Cudd_Ref(sum);
    Cudd_RecursiveDeref(dd, term0);
    Cudd_RecursiveDeref(dd, term1);
    /* r = sum + Id */
    r = cuddBddAndRecur(dd, Cudd_Not(sum), Cudd_Not(Id));
    r = Cudd_NotCond(r, r != NULL);
    if (r == NULL) {
	Cudd_RecursiveDeref(dd, Id);
	Cudd_RecursiveDeref(dd, sum);
	return(NULL);
    }
    Cudd_Ref(r);
    Cudd_RecursiveDeref(dd, sum);
    Cudd_RecursiveDeref(dd, Id);

    cuddCacheInsert2(dd, cuddBddIsop, L, U, r);

    Cudd_Deref(r);
    return(r);

} /* end of cuddBddIsop */

开发者ID:ansonn，项目名称:esl_systemc，代码行数:101，代码来源:cuddZddIsop.c

示例20: cuddBddClippingAndRecur


//.........这里部分代码省略.........
    if (distance == 0) {
	/* One last attempt at returning the right result. We sort of
	** cheat by calling Cudd_bddLeq. */
	if (Cudd_bddLeq(manager,f,g)) return(f);
	if (Cudd_bddLeq(manager,g,f)) return(g);
	if (direction == 1) {
	    if (Cudd_bddLeq(manager,f,Cudd_Not(g)) ||
		Cudd_bddLeq(manager,g,Cudd_Not(f))) return(zero);
	}
	return(Cudd_NotCond(one,(direction == 0)));
    }

    /* At this point f and g are not constant. */
    distance--;

    /* Check cache. Try to increase cache efficiency by sorting the
    ** pointers. */
    if (f > g) {
	DdNode *tmp = f;
	f = g; g = tmp;
    }
    F = Cudd_Regular(f);
    G = Cudd_Regular(g);
    cacheOp = (DD_CTFP)
	(direction ? Cudd_bddClippingAnd : cuddBddClippingAnd);
    if (F->ref != 1 || G->ref != 1) {
	r = cuddCacheLookup2(manager, cacheOp, f, g);
	if (r != NULL) return(r);
    }

    checkWhetherToGiveUp(manager);

    /* Here we can skip the use of cuddI, because the operands are known
    ** to be non-constant.
    */
    topf = manager->perm[F->index];
    topg = manager->perm[G->index];

    /* Compute cofactors. */
    if (topf <= topg) {
	index = F->index;
	ft = cuddT(F);
	fe = cuddE(F);
	if (Cudd_IsComplement(f)) {
	    ft = Cudd_Not(ft);
	    fe = Cudd_Not(fe);
	}
    } else {
	index = G->index;
	ft = fe = f;
    }

    if (topg <= topf) {
	gt = cuddT(G);
	ge = cuddE(G);
	if (Cudd_IsComplement(g)) {
	    gt = Cudd_Not(gt);
	    ge = Cudd_Not(ge);
	}
    } else {
	gt = ge = g;
    }

    t = cuddBddClippingAndRecur(manager, ft, gt, distance, direction);
    if (t == NULL) return(NULL);
    cuddRef(t);
    e = cuddBddClippingAndRecur(manager, fe, ge, distance, direction);
    if (e == NULL) {
	Cudd_RecursiveDeref(manager, t);
	return(NULL);
    }
    cuddRef(e);

    if (t == e) {
	r = t;
    } else {
	if (Cudd_IsComplement(t)) {
	    r = cuddUniqueInter(manager,(int)index,Cudd_Not(t),Cudd_Not(e));
	    if (r == NULL) {
		Cudd_RecursiveDeref(manager, t);
		Cudd_RecursiveDeref(manager, e);
		return(NULL);
	    }
	    r = Cudd_Not(r);
	} else {
	    r = cuddUniqueInter(manager,(int)index,t,e);
	    if (r == NULL) {
		Cudd_RecursiveDeref(manager, t);
		Cudd_RecursiveDeref(manager, e);
		return(NULL);
	    }
	}
    }
    cuddDeref(e);
    cuddDeref(t);
    if (F->ref != 1 || G->ref != 1)
	cuddCacheInsert2(manager, cacheOp, f, g, r);
    return(r);

} /* end of cuddBddClippingAndRecur */

开发者ID:VerifiableRobotics，项目名称:slugs