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

C++ cuddV函数代码示例

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

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



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

示例1: Cudd_addTimes

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

  Synopsis    [Integer and floating point multiplication.]

  Description [Integer and floating point multiplication. Returns NULL
  if not a terminal case; f * g otherwise.  This function can be used also
  to take the AND of two 0-1 ADDs.]

  SideEffects [None]

  SeeAlso     [Cudd_addApply]

******************************************************************************/
DdNode *
Cudd_addTimes(
  DdManager * dd,
  DdNode ** f,
  DdNode ** g)
{
    DdNode *res;
    DdNode *F, *G;
    CUDD_VALUE_TYPE value;

    F = *f; G = *g;
    if (F == DD_ZERO(dd) || G == DD_ZERO(dd)) return(DD_ZERO(dd));
    if (F == DD_ONE(dd)) return(G);
    if (G == DD_ONE(dd)) return(F);
    if (cuddIsConstant(F) && cuddIsConstant(G)) {
	value = cuddV(F)*cuddV(G);
	res = cuddUniqueConst(dd,value);
	return(res);
    }
    if (F > G) { /* swap f and g */
	*f = G;
	*g = F;
    }
    return(NULL);

} /* end of Cudd_addTimes */
开发者ID:amusant，项目名称:vtr-verilog-to-routing，代码行数:39，代码来源:cuddAddApply.c


示例2: Cudd_addFindMax

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

  Synopsis    [Finds the maximum discriminant of f.]

  Description [Returns a pointer to a constant ADD.]

  SideEffects [None]

******************************************************************************/
DdNode *
Cudd_addFindMax(
  DdManager * dd,
  DdNode * f)
{
    DdNode *t, *e, *res;

    statLine(dd);
    if (cuddIsConstant(f)) {
	return(f);
    }

    res = cuddCacheLookup1(dd,Cudd_addFindMax,f);
    if (res != NULL) {
	return(res);
    }

    t  = Cudd_addFindMax(dd,cuddT(f));
    if (t == DD_PLUS_INFINITY(dd)) return(t);

    e  = Cudd_addFindMax(dd,cuddE(f));

    res = (cuddV(t) >= cuddV(e)) ? t : e;

    cuddCacheInsert1(dd,Cudd_addFindMax,f,res);

    return(res);

} /* end of Cudd_addFindMax */
开发者ID:amusant，项目名称:vtr-verilog-to-routing，代码行数:38，代码来源:cuddAddFind.c


示例3: min

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

  Synopsis    [Returns plusinfinity if f=g; returns min(f,g) if f!=g.]

  Description [Returns NULL if not a terminal case; f op g otherwise,
  where f op g is plusinfinity if f=g; min(f,g) if f!=g.]

  SideEffects [None]

  SeeAlso     [Cudd_addApply]

******************************************************************************/
DdNode *
Cudd_addDiff(
  DdManager * dd,
  DdNode ** f,
  DdNode ** g)
{
    DdNode *F, *G;

    F = *f; G = *g;
    if (F == G) return(DD_PLUS_INFINITY(dd));
    if (F == DD_PLUS_INFINITY(dd)) return(G);
    if (G == DD_PLUS_INFINITY(dd)) return(F);
    if (cuddIsConstant(F) && cuddIsConstant(G)) {
	if (cuddV(F) != cuddV(G)) {
            if (cuddV(F) < cuddV(G)) {
                return(F);
            } else {
                return(G);
            }
	} else {
	    return(DD_PLUS_INFINITY(dd));
	}
    }
    return(NULL);

} /* end of Cudd_addDiff */
开发者ID:amusant，项目名称:vtr-verilog-to-routing，代码行数:38，代码来源:cuddAddApply.c


示例4: max

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

  Synopsis    [Integer and floating point max.]

  Description [Integer and floating point max for Cudd_addApply.
  Returns NULL if not a terminal case; max(f,g) otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_addApply]

******************************************************************************/
DdNode *
Cudd_addMaximum(
  DdManager * dd,
  DdNode ** f,
  DdNode ** g)
{
    DdNode *F, *G;

    F = *f; G = *g;
    if (F == G) return(F);
    if (F == DD_MINUS_INFINITY(dd)) return(G);
    if (G == DD_MINUS_INFINITY(dd)) return(F);
#if 0
    /* These special cases probably do not pay off. */
    if (F == DD_PLUS_INFINITY(dd)) return(F);
    if (G == DD_PLUS_INFINITY(dd)) return(G);
#endif
    if (cuddIsConstant(F) && cuddIsConstant(G)) {
	if (cuddV(F) >= cuddV(G)) {
	    return(F);
	} else {
	    return(G);
	}
    }
    if (F > G) { /* swap f and g */
	*f = G;
	*g = F;
    }
    return(NULL);

} /* end of Cudd_addMaximum */
开发者ID:amusant，项目名称:vtr-verilog-to-routing，代码行数:43，代码来源:cuddAddApply.c


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


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


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

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

  Synopsis    [Determines whether f is less than or equal to g.]

  Description [Returns 1 if f is less than or equal to g; 0 otherwise.
  No new nodes are created. This procedure works for arbitrary ADDs.
  For 0-1 ADDs Cudd_addEvalConst is more efficient.]

  SideEffects [None]

  SeeAlso     [Cudd_addIteConstant Cudd_addEvalConst Cudd_bddLeq]

******************************************************************************/
int
Cudd_addLeq(
  DdManager * dd,
  DdNode * f,
  DdNode * g)
{
    DdNode *tmp, *fv, *fvn, *gv, *gvn;
    unsigned int topf, topg, res;

    /* Terminal cases. */
    if (f == g) return(1);

    statLine(dd);
    if (cuddIsConstant(f)) {
	if (cuddIsConstant(g)) return(cuddV(f) <= cuddV(g));
	if (f == DD_MINUS_INFINITY(dd)) return(1);
	if (f == DD_PLUS_INFINITY(dd)) return(0); /* since f != g */
    }
    if (g == DD_PLUS_INFINITY(dd)) return(1);
    if (g == DD_MINUS_INFINITY(dd)) return(0); /* since f != g */

    /* Check cache. */
    tmp = cuddCacheLookup2(dd,(DD_CTFP)Cudd_addLeq,f,g);
    if (tmp != NULL) {
	return(tmp == DD_ONE(dd));
    }

    /* Compute cofactors. One of f and g is not constant. */
    topf = cuddI(dd,f->index);
    topg = cuddI(dd,g->index);
    if (topf <= topg) {
	fv = cuddT(f); fvn = cuddE(f);
    } else {
	fv = fvn = f;
    }
    if (topg <= topf) {
	gv = cuddT(g); gvn = cuddE(g);
    } else {
	gv = gvn = g;
    }

    res = Cudd_addLeq(dd,fvn,gvn) && Cudd_addLeq(dd,fv,gv);

    /* Store result in cache and return. */
    cuddCacheInsert2(dd,(DD_CTFP) Cudd_addLeq,f,g,
		     Cudd_NotCond(DD_ONE(dd),res==0));
    return(res);

} /* end of Cudd_addLeq */
开发者ID:maeon，项目名称:SBSAT，代码行数:62，代码来源:cuddAddIte.c


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


示例10: Apply

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

  Synopsis    [f if f&gt;=g; 0 if f&lt;g.]

  Description [Threshold operator for Apply (f if f &gt;=g; 0 if f&lt;g).
  Returns NULL if not a terminal case; f op g otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_addApply]

******************************************************************************/
DdNode *
Cudd_addThreshold(
  DdManager * dd,
  DdNode ** f,
  DdNode ** g)
{
    DdNode *F, *G;

    F = *f; G = *g;
    if (cuddIsConstant(F) && cuddIsConstant(G)) {
	if (cuddV(F) >= cuddV(G)) {
	    return(F);
	} else {
	    return(DD_ZERO(dd));
	}
    }
    return(NULL);

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


示例11: g

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

  Synopsis    [Returns 1 if f &gt g and 0 otherwise.]

  Description [Returns 1 if f &gt g (both should be terminal cases) and 0 
  otherwise. Used in conjunction with Cudd_addApply. Returns NULL if not a 
  terminal case.]

  SideEffects [None]

  SeeAlso     [Cudd_addApply]

******************************************************************************/
DdNode *
Cudd_addOneZeroMaximum(
  DdManager * dd,
  DdNode ** f,
  DdNode ** g)
{

    if (*g == DD_PLUS_INFINITY(dd))
	return DD_ZERO(dd);
    if (cuddIsConstant(*f) && cuddIsConstant(*g)) {
	if (cuddV(*f) > cuddV(*g)) {
	    return(DD_ONE(dd));
	} else {
	    return(DD_ZERO(dd));
	}
    }

    return(NULL);

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


示例12: Cudd_addMinus

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

  Synopsis    [Integer and floating point subtraction.]

  Description [Integer and floating point subtraction. Returns NULL if
  not a terminal case; f - g otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_addApply]

******************************************************************************/
DdNode *
Cudd_addMinus(
  DdManager * dd,
  DdNode ** f,
  DdNode ** g)
{
    DdNode *res;
    DdNode *F, *G;
    CUDD_VALUE_TYPE value;

    F = *f; G = *g;
    if (F == DD_ZERO(dd)) return(cuddAddNegateRecur(dd,G));
    if (G == DD_ZERO(dd)) return(F);
    if (cuddIsConstant(F) && cuddIsConstant(G)) {
	value = cuddV(F)-cuddV(G);
	res = cuddUniqueConst(dd,value);
	return(res);
    }
    return(NULL);

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


示例13: Cudd_addDivide

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

  Synopsis    [Integer and floating point division.]

  Description [Integer and floating point division. Returns NULL if not
  a terminal case; f / g otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_addApply]

******************************************************************************/
DdNode *
Cudd_addDivide(
  DdManager * dd,
  DdNode ** f,
  DdNode ** g)
{
    DdNode *res;
    DdNode *F, *G;
    CUDD_VALUE_TYPE value;

    F = *f; G = *g;
    if (F == DD_ZERO(dd)) return(DD_ZERO(dd));
    if (G == DD_ONE(dd)) return(F);
    if (cuddIsConstant(F) && cuddIsConstant(G)) {
	value = cuddV(F)/cuddV(G);
	res = cuddUniqueConst(dd,value);
	return(res);
    }
    return(NULL);

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


示例14: log

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

  Synopsis    [Natural logarithm of an ADD.]

  Description [Natural logarithm of an ADDs. Returns NULL
  if not a terminal case; log(f) otherwise.  The discriminants of f must
  be positive double's.]

  SideEffects [None]

  SeeAlso     [Cudd_addMonadicApply]

******************************************************************************/
DdNode *
Cudd_addLog(
  DdManager * dd,
  DdNode * f)
{
    if (cuddIsConstant(f)) {
	CUDD_VALUE_TYPE value = log(cuddV(f));
	DdNode *res = cuddUniqueConst(dd,value);
	return(res);
    }
    return(NULL);

} /* end of Cudd_addLog */
开发者ID:amusant，项目名称:vtr-verilog-to-routing，代码行数:26，代码来源:cuddAddApply.c


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


示例16: Cudd_addDivide

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

  Synopsis    [Integer and floating point division.]

  Description [Integer and floating point division. Returns NULL if not
  a terminal case; f / g otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_addApply]

******************************************************************************/
DdNode *
Cudd_addDivide(
  DdManager * dd,
  DdNode ** f,
  DdNode ** g)
{
    DdNode *res;
    DdNode *F, *G;
    CUDD_VALUE_TYPE value;

    F = *f; G = *g;
    /* We would like to use F == G -> F/G == 1, but F and G may
    ** contain zeroes. */
    if (F == DD_ZERO(dd)) return(DD_ZERO(dd));
    if (G == DD_ONE(dd)) return(F);
    if (cuddIsConstant(F) && cuddIsConstant(G)) {
	value = cuddV(F)/cuddV(G);
	res = cuddUniqueConst(dd,value);
	return(res);
    }
    return(NULL);

} /* end of Cudd_addDivide */
开发者ID:amusant，项目名称:vtr-verilog-to-routing，代码行数:35，代码来源:cuddAddApply.c


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


示例18: I_BDD_minterms_aux

static void
I_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;
}
开发者ID:invisibleboy，项目名称:mycompiler，代码行数:49，代码来源:i_bdd_interface.c


示例19: addBddDoIthBit

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

  Synopsis    [Performs the recursive step for Cudd_addBddIthBit.]

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

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
static DdNode *
addBddDoIthBit(
  DdManager * dd,
  DdNode * f,
  DdNode * index)
{
    DdNode *res, *T, *E;
    DdNode *fv, *fvn;
    /* NuSMV: add begin */
    ptrint mask, value;
      /* WAS: long mask, value; */
    /* NuSMV: add end */

    int v;

    statLine(dd);
    /* Check terminal case. */
    if (cuddIsConstant(f)) {
      /* NuSMV: add begin */
	mask = 1 << ((ptrint) cuddV(index));
	value = (ptrint) cuddV(f);
        /* WAS: mask = 1 << ((long) cuddV(index));
                value = (long) cuddV(f); */
      /* NuSMV: add end */
	return(Cudd_NotCond(DD_TRUE(dd),(value & mask) == 0));
    }

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

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

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

    E = addBddDoIthBit(dd,fvn,index);
    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,addBddDoIthBit,f,index,res);

    return(res);

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


示例20: Extra_bddHaar

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

  Synopsis    [Performs the reordering-sensitive step of Extra_bddHaar().]

  Description [Generates in a bottom-up fashion an ADD for all spectral
               coefficients of the functions represented by a BDD.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
DdNode* extraBddHaar( 
  DdManager * dd,    /* the manager */
  DdNode * bFunc,    /* the function whose spectrum is being computed */
  DdNode * bVars)    /* the variables on which the function depends */
{
	DdNode * aRes;
    statLine(dd); 

	/* terminal cases */
	if ( bVars == b1 )
	{
		assert( Cudd_IsConstant(bFunc) );
		if ( bFunc == b0 )
			return a0;
		else
			return a1;
	}

    /* check cache */
//	if ( bFunc->ref != 1 )
    if ( aRes = cuddCacheLookup2(dd, extraBddHaar, bFunc, bVars) )
    	return aRes;
	else
	{
		DdNode * bFunc0, * bFunc1;   /* cofactors of the function */
		DdNode * aHaar0, * aHaar1;   /* partial solutions of the problem */
		DdNode * aNode0, * aNode1;   /* the special terminal nodes */
		DdNode * aRes0,  * aRes1;    /* partial results to be composed by ITE */
		DdNode * bFuncR = Cudd_Regular(bFunc); /* the regular pointer to the function */
		DdNode * aTemp;
		double   dValue0, dValue1;

		/* bFunc cannot depend on a variable that is not in bVars */
		assert( cuddI(dd,bFuncR->index) >= cuddI(dd,bVars->index) );


		/* cofactor the BDD */
		if ( bFuncR->index == bVars->index )
		{
			if ( bFuncR != bFunc ) /* bFunc is complemented */
			{
				bFunc0 = Cudd_Not( cuddE(bFuncR) );
				bFunc1 = Cudd_Not( cuddT(bFuncR) );
			}
			else
			{
				bFunc0 = cuddE(bFuncR);
				bFunc1 = cuddT(bFuncR);
			}
		}
		else /* bVars is higher in the variable order */
			bFunc0 = bFunc1 = bFunc;


		/* solve subproblems */
		aHaar0 = extraBddHaar( dd, bFunc0, cuddT(bVars) );
		if ( aHaar0 == NULL )
			return NULL;
		cuddRef( aHaar0 );

		aHaar1 = extraBddHaar( dd, bFunc1, cuddT(bVars) );
		if ( aHaar1 == NULL )
		{
			Cudd_RecursiveDeref( dd, aHaar0 );
			return NULL;
		}
		cuddRef( aHaar1 );

		/* retrieve the terminal values in aHaar0 and aHaar1 */
		for ( aTemp = aHaar0; aTemp->index != CUDD_CONST_INDEX; aTemp = cuddE(aTemp) );
		dValue0 = cuddV( aTemp );
		for ( aTemp = aHaar1; aTemp->index != CUDD_CONST_INDEX; aTemp = cuddE(aTemp) );
		dValue1 = cuddV( aTemp );

		/* get the new terminal nodes */
		aNode0 = cuddUniqueConst( dd, dValue0 + dValue1 );
		if ( aNode0 == NULL )
		{
			Cudd_RecursiveDeref( dd, aHaar0 );
			Cudd_RecursiveDeref( dd, aHaar1 );
			return NULL;
		}
		cuddRef( aNode0 );

		aNode1 = cuddUniqueConst( dd, dValue0 - dValue1 );
		if ( aNode1 == NULL )
		{
			Cudd_RecursiveDeref( dd, aHaar0 );
//.........这里部分代码省略.........
开发者ID:chastell，项目名称:cirkit，代码行数:101，代码来源:extraAddSpectra.c



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

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

请发表评论

全部评论

专题导读
More+
上一篇：
C++ cueDidChange函数代码示例发布时间：2022-05-30
下一篇：
C++ cuddUniqueInter函数代码示例发布时间：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