本文整理汇总了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>=g; 0 if f<g.]
Description [Threshold operator for Apply (f if f >=g; 0 if f<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 > g and 0 otherwise.]
Description [Returns 1 if f > 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;未经允许,请勿转载。 |
请发表评论