• 设为首页
  • 点击收藏
  • 手机版
    手机扫一扫访问
    迪恩网络手机版
  • 关注官方公众号
    微信扫一扫关注
    公众号
登陆 注册

C++ cuddRef函数代码示例

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

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



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

示例1: cuddZddChangeAux

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

  Synopsis [Performs the recursive step of Cudd_zddChange.]

  Description []

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
DdNode *
cuddZddChangeAux(
  DdManager * zdd,
  DdNode * P,
  DdNode * zvar)
{
    int		top_var, level;
    DdNode	*res, *t, *e;
    DdNode	*base = DD_ONE(zdd);
    DdNode	*empty = DD_ZERO(zdd);

    statLine(zdd);
    if (P == empty)
	return(empty);
    if (P == base)
	return(zvar);

    /* Check cache. */
    res = cuddCacheLookup2Zdd(zdd, cuddZddChangeAux, P, zvar);
    if (res != NULL)
	return(res);

    top_var = zdd->permZ[P->index];
    level = zdd->permZ[zvar->index];

    if (top_var > level) {
	res = cuddZddGetNode(zdd, zvar->index, P, DD_ZERO(zdd));
	if (res == NULL) return(NULL);
    } else if (top_var == level) {
	res = cuddZddGetNode(zdd, zvar->index, cuddE(P), cuddT(P));
	if (res == NULL) return(NULL);
    } else {
	t = cuddZddChangeAux(zdd, cuddT(P), zvar);
	if (t == NULL) return(NULL);
	cuddRef(t);
	e = cuddZddChangeAux(zdd, cuddE(P), zvar);
	if (e == NULL) {
	    Cudd_RecursiveDerefZdd(zdd, t);
	    return(NULL);
	}
	cuddRef(e);
	res = cuddZddGetNode(zdd, P->index, t, e);
	if (res == NULL) {
	    Cudd_RecursiveDerefZdd(zdd, t);
	    Cudd_RecursiveDerefZdd(zdd, e);
	    return(NULL);
	}
	cuddDeref(t);
	cuddDeref(e);
    }

    cuddCacheInsert2(zdd, cuddZddChangeAux, P, zvar, res);

    return(res);

} /* end of cuddZddChangeAux */
开发者ID:lucadealfaro，项目名称:ticc，代码行数:67，代码来源:cuddZddSetop.c


示例2: zdd_subset1_aux

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

  Synopsis [Performs the recursive step of Cudd_zddSubset1.]

  Description []

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
static DdNode *
zdd_subset1_aux(
  DdManager * zdd,
  DdNode * P,
  DdNode * zvar)
{
    int		top_var, level;
    DdNode	*res, *t, *e;
    DdNode	*empty;

    statLine(zdd);
    empty = DD_ZERO(zdd);

    /* Check cache. */
    res = cuddCacheLookup2Zdd(zdd, zdd_subset1_aux, P, zvar);
    if (res != NULL)
	return(res);

    if (cuddIsConstant(P)) {
	res = empty;
	cuddCacheInsert2(zdd, zdd_subset1_aux, P, zvar, res);
	return(res);
    }

    top_var = zdd->permZ[P->index];
    level = zdd->permZ[zvar->index];

    if (top_var > level) {
        res = empty;
    } else if (top_var == level) {
	res = cuddT(P);
    } else {
        t = zdd_subset1_aux(zdd, cuddT(P), zvar);
	if (t == NULL) return(NULL);
	cuddRef(t);
        e = zdd_subset1_aux(zdd, cuddE(P), zvar);
	if (e == NULL) {
	    Cudd_RecursiveDerefZdd(zdd, t);
	    return(NULL);
	}
	cuddRef(e);
        res = cuddZddGetNode(zdd, P->index, t, e);
	if (res == NULL) {
	    Cudd_RecursiveDerefZdd(zdd, t);
	    Cudd_RecursiveDerefZdd(zdd, e);
	    return(NULL);
	}
	cuddDeref(t);
	cuddDeref(e);
    }

    cuddCacheInsert2(zdd, zdd_subset1_aux, P, zvar, res);

    return(res);

} /* end of zdd_subset1_aux */
开发者ID:lucadealfaro，项目名称:ticc，代码行数:67，代码来源:cuddZddSetop.c


示例3: Cuddaux_ClassifySupport

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

  Synopsis    [Classifies the variables in the support of two DDs.]

  Description [Classifies the variables in the support of two DDs
  <code>f</code> and <code>g</code>, depending on whther they appear
  in both DDs, only in <code>f</code>, or only in <code>g</code>.
  Returns 1 if successful; 0 otherwise.]

  SideEffects [The cubes of the three classes of variables are
  returned as side effects.]

  SeeAlso     []

******************************************************************************/
int
Cuddaux_ClassifySupport(
			DdManager * dd /* manager */,
			DdNode * f /* first DD */,
			DdNode * g /* second DD */,
			DdNode ** common /* cube of shared variables */,
			DdNode ** onlyF /* cube of variables only in f */,
			DdNode ** onlyG /* cube of variables only in g */)
{
  DdNode *suppF, *suppG;

  suppF = suppG = *common = *onlyF = *onlyG = NULL;

  suppF = Cuddaux_Support(dd,f);
  if (suppF == NULL) goto Cuddaux_ClassifySupport_error;
  cuddRef(suppF);

  suppG = Cuddaux_Support(dd,g);
  if (suppG == NULL) goto Cuddaux_ClassifySupport_error;
  cuddRef(suppG);

  *common = Cudd_bddLiteralSetIntersection(dd,suppF,suppG);
  if (*common == NULL) goto Cuddaux_ClassifySupport_error;
  cuddRef(*common);

  *onlyF = Cudd_Cofactor(dd,suppF,*common);
  if (*onlyF == NULL) goto Cuddaux_ClassifySupport_error;
  cuddRef(*onlyF);

  *onlyG = Cudd_Cofactor(dd,suppG,*common);
  if (*onlyG == NULL) goto Cuddaux_ClassifySupport_error;
  cuddRef(*onlyG);
  Cudd_IterDerefBdd(dd,suppF);
  Cudd_IterDerefBdd(dd,suppG);
  cuddDeref(*common);
  cuddDeref(*onlyF);
  cuddDeref(*onlyG);
  return 1;
 Cuddaux_ClassifySupport_error:
  if (suppF) Cudd_IterDerefBdd(dd,suppF);
  if (suppG) Cudd_IterDerefBdd(dd,suppG);
  if (*common){
    Cudd_IterDerefBdd(dd,*common);
    *common = NULL;
  }
  if (*onlyF){
    Cudd_IterDerefBdd(dd,*onlyF);
    *onlyF = NULL;
  }
  if (*onlyG){
    Cudd_IterDerefBdd(dd,*onlyG);
    *onlyG = NULL;
  }
  dd->errorCode = CUDD_MEMORY_OUT;
  return(0);
} /* end of Cuddaux_ClassifySupport */
开发者ID:thizanne，项目名称:mlcuddidl，代码行数:71，代码来源:cuddauxMisc.c


示例4: cuddBddBooleanDiffRecur

/**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 */
开发者ID:AndrewSmart，项目名称:CS5600，代码行数:70，代码来源:cuddBddAbs.c


示例5: 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


示例6: 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


示例7: 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


示例8: 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


示例9: 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


示例10: 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


示例11: Cudd_Xgty

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

  Synopsis    [Generates a BDD for the function x &gt; y.]

  Description [This function generates a BDD for the function x &gt; y.
  Both x and y are N-bit numbers, x\[0\] x\[1\] ... x\[N-1\] and
  y\[0\] y\[1\] ...  y\[N-1\], with 0 the most significant bit.
  The BDD is built bottom-up.
  It has 3*N-1 internal nodes, if the variables are ordered as follows: 
  x\[0\] y\[0\] x\[1\] y\[1\] ... x\[N-1\] y\[N-1\].
  Argument z is not used by Cudd_Xgty: it is included to make it
  call-compatible to Cudd_Dxygtdxz and Cudd_Dxygtdyz.]

  SideEffects [None]

  SeeAlso     [Cudd_PrioritySelect Cudd_Dxygtdxz Cudd_Dxygtdyz]

******************************************************************************/
DdNode *
Cudd_Xgty(
  DdManager * dd /* DD manager */,
  int  N /* number of x and y variables */,
  DdNode ** z /* array of z variables: unused */,
  DdNode ** x /* array of x variables */,
  DdNode ** y /* array of y variables */)
{
    DdNode *u, *v, *w;
    int     i;

    /* Build bottom part of BDD outside loop. */
    u = Cudd_bddAnd(dd, x[N-1], Cudd_Not(y[N-1]));
    if (u == NULL) return(NULL);
    cuddRef(u);

    /* Loop to build the rest of the BDD. */
    for (i = N-2; i >= 0; i--) {
	v = Cudd_bddAnd(dd, y[i], Cudd_Not(u));
	if (v == NULL) {
	    Cudd_RecursiveDeref(dd, u);
	    return(NULL);
	}
	cuddRef(v);
	w = Cudd_bddAnd(dd, Cudd_Not(y[i]), u);
	if (w == NULL) {
	    Cudd_RecursiveDeref(dd, u);
	    Cudd_RecursiveDeref(dd, v);
	    return(NULL);
	}
	cuddRef(w);
	Cudd_RecursiveDeref(dd, u);
	u = Cudd_bddIte(dd, x[i], Cudd_Not(v), w);
	if (u == NULL) {
	    Cudd_RecursiveDeref(dd, v);
	    Cudd_RecursiveDeref(dd, w);
	    return(NULL);
	}
	cuddRef(u);
	Cudd_RecursiveDeref(dd, v);
	Cudd_RecursiveDeref(dd, w);

    }
    cuddDeref(u);
    return(u);

} /* end of Cudd_Xgty */
开发者ID:saidalfaraby，项目名称:DTP4TC，代码行数:65，代码来源:cuddPriority.c


示例12: 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


示例13: extraZddGetSingletons

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

  Synopsis    [Performs a recursive step of Extra_zddGetSingletons.]

  Description [Returns the set of ZDD singletons, containing those positive 
  polarity ZDD variables that correspond to the BDD variables in bVars.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
DdNode * extraZddGetSingletons( 
  DdManager * dd,    /* the DD manager */
  DdNode * bVars)    /* the set of variables */
{
    DdNode * zRes;

    if ( bVars == b1 )
//    if ( bVars == b0 )  // bug fixed by Jin Zhang, Jan 23, 2004
        return z1;

    if ( (zRes = cuddCacheLookup1Zdd(dd, extraZddGetSingletons, bVars)) )
        return zRes;
    else
    {
        DdNode * zTemp, * zPlus;          

        // solve subproblem
        zRes = extraZddGetSingletons( dd, cuddT(bVars) );
        if ( zRes == NULL ) 
            return NULL;
        cuddRef( zRes );
        
        zPlus = cuddZddGetNode( dd, 2*bVars->index, z1, z0 );
        if ( zPlus == NULL ) 
        {
            Cudd_RecursiveDerefZdd( dd, zRes );
            return NULL;
        }
        cuddRef( zPlus );

        // add these to the result
        zRes = cuddZddUnion( dd, zTemp = zRes, zPlus );
        if ( zRes == NULL )
        {
            Cudd_RecursiveDerefZdd( dd, zTemp );
            Cudd_RecursiveDerefZdd( dd, zPlus );
            return NULL;
        }
        cuddRef( zRes );
        Cudd_RecursiveDerefZdd( dd, zTemp );
        Cudd_RecursiveDerefZdd( dd, zPlus );
        cuddDeref( zRes );

        cuddCacheInsert1( dd, extraZddGetSingletons, bVars, zRes );
        return zRes;
    }
}   /* end of extraZddGetSingletons */
开发者ID:kyotobay，项目名称:ABC_withFD_check，代码行数:59，代码来源:extraBddSymm.c


示例14: 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


示例15: 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


示例16: Cudd_addHamming

/**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 */
开发者ID:saidalfaraby，项目名称:DTP4TC，代码行数:59，代码来源:cuddPriority.c


示例17: Cudd_addBddInterval

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

  Synopsis    [Converts an ADD to a BDD.]

  Description [Converts an ADD to a BDD by replacing all
  discriminants greater than or equal to lower and less than or equal to
  upper with 1, and all other discriminants with 0. Returns a pointer to
  the resulting BDD if successful; NULL otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_addBddThreshold Cudd_addBddStrictThreshold 
  Cudd_addBddPattern Cudd_BddToAdd]

******************************************************************************/
DdNode *
Cudd_addBddInterval(
  DdManager * dd,
  DdNode * f,
  CUDD_VALUE_TYPE  lower,
  CUDD_VALUE_TYPE  upper)
{
    DdNode *res;
    DdNode *l;
    DdNode *u;

    /* NuSMV: begin add */
    abort(); /* NOT USED BY NUSMV */
    /* NuSMV: begin end */

    /* Create constant nodes for the interval bounds, so that we can use
    ** the global cache.
    */
    l = cuddUniqueConst(dd,lower);
    if (l == NULL) return(NULL);
    cuddRef(l);
    u = cuddUniqueConst(dd,upper);
    if (u == NULL) {
	Cudd_RecursiveDeref(dd,l);
	return(NULL);
    }
    cuddRef(u);

    do {
	dd->reordered = 0;
	res = addBddDoInterval(dd, f, l, u);
    } while (dd->reordered == 1);

    if (res == NULL) {
	Cudd_RecursiveDeref(dd, l);
	Cudd_RecursiveDeref(dd, u);
	return(NULL);
    }
    cuddRef(res);
    Cudd_RecursiveDeref(dd, l);
    Cudd_RecursiveDeref(dd, u);
    cuddDeref(res);
    return(res);

} /* end of Cudd_addBddInterval */
开发者ID:ancailliau，项目名称:pynusmv，代码行数:60，代码来源:cuddBridge.c


示例18: cuddZddInitUniv

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

  Synopsis    [Initializes the ZDD universe.]

  Description [Initializes the ZDD universe. Returns 1 if successful; 0
  otherwise.]

  SideEffects [None]

  SeeAlso     [cuddZddFreeUniv]

******************************************************************************/
int
cuddZddInitUniv(
  DdManager * zdd)
{
    DdNode	*p, *res;
    int		i;

#ifdef __osf__
#pragma pointer_size save
#pragma pointer_size short
#endif
    zdd->univ = ALLOC(DdNode *, zdd->sizeZ);
#ifdef __osf__
#pragma pointer_size restore
#endif
    if (zdd->univ == NULL) {
	zdd->errorCode = CUDD_MEMORY_OUT;
	return(0);
    }

    res = DD_ONE(zdd);
    cuddRef(res);
    for (i = zdd->sizeZ - 1; i >= 0; i--) {
	unsigned int index = zdd->invpermZ[i];
	p = res;
	res = cuddUniqueInterZdd(zdd, index, p, p);
	if (res == NULL) {
	    Cudd_RecursiveDerefZdd(zdd,p);
	    FREE(zdd->univ);
	    return(0);
	}
	cuddRef(res);
	cuddDeref(p);
	zdd->univ[i] = res;
    }

#ifdef DD_VERBOSE
    cuddZddP(zdd, zdd->univ[0]);
#endif

    return(1);

} /* end of cuddZddInitUniv */
开发者ID:invisibleboy，项目名称:mycompiler，代码行数:55，代码来源:cuddInit.c


示例19: Cuddaux_SupportSize

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

  Synopsis    [Finds the number of variables on which a DD depends, using Cuddaux_Support.]

  Description []

  SideEffects [None]

  SeeAlso     [Cudd_SupportSize]

******************************************************************************/
int Cuddaux_SupportSize(DdManager* dd, DdNode* f)
{
  DdNode* res;
  int size;
  res = Cuddaux_Support(dd,f);
  cuddRef(res);
  size = Cudd_DagSize(res) - 1;
  assert(size>=0);
  Cudd_IterDerefBdd(dd,res);
  return size;
}
开发者ID:thizanne，项目名称:mlcuddidl，代码行数:22，代码来源:cuddauxMisc.c


示例20: Cudd_CProjection

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

  Synopsis    [Computes the compatible projection of R w.r.t. cube Y.]

  Description [Computes the compatible projection of relation R with
  respect to cube Y. Returns a pointer to the c-projection if
  successful; NULL otherwise. For a comparison between Cudd_CProjection
  and Cudd_PrioritySelect, see the documentation of the latter.]

  SideEffects [None]

  SeeAlso     [Cudd_PrioritySelect]

******************************************************************************/
DdNode *
Cudd_CProjection(
  DdManager * dd,
  DdNode * R,
  DdNode * Y)
{
    DdNode *res;
    DdNode *support;

    if (cuddCheckCube(dd,Y) == 0) {
	(void) fprintf(dd->err,
	"Error: The third argument of Cudd_CProjection should be a cube\n");
	dd->errorCode = CUDD_INVALID_ARG;
	return(NULL);
    }

    /* Compute the support of Y, which is used by the abstraction step
    ** in cuddCProjectionRecur.
    */
    support = Cudd_Support(dd,Y);
    if (support == NULL) return(NULL);
    cuddRef(support);

    do {
	dd->reordered = 0;
	res = cuddCProjectionRecur(dd,R,Y,support);
    } while (dd->reordered == 1);

    if (res == NULL) {
	Cudd_RecursiveDeref(dd,support);
	return(NULL);
    }
    cuddRef(res);
    Cudd_RecursiveDeref(dd,support);
    cuddDeref(res);

    return(res);

} /* end of Cudd_CProjection */
开发者ID:saidalfaraby，项目名称:DTP4TC，代码行数:53，代码来源:cuddPriority.c



注：本文中的cuddRef函数示例由纯净天空整理自Github/MSDocs等源码及文档管理平台，相关代码片段筛选自各路编程大神贡献的开源项目，源码版权归原作者所有，传播和使用请参考对应项目的License；未经允许，请勿转载。

鲜花
握手
雷人
路过
鸡蛋
该文章已有0人参与评论

请发表评论

全部评论

专题导读
More+
上一篇：
C++ cuddUniqueInter函数代码示例发布时间：2022-05-30
下一篇：
C++ cuddIsConstant函数代码示例发布时间：2022-05-30
热门推荐
More+
热门话题
More+
阅读排行榜

扫描微信二维码

查看手机版网站

随时了解更新最新资讯

139-2527-9053

在线客服（服务时间 9:00～18:00）

在线QQ客服
地址：深圳市南山区西丽大学城创智工业园
电邮：jeky_zhao#qq.com
移动电话：139-2527-9053

Powered by 互联科技 X3.4© 2001-2213 极客世界.|Sitemap