本文整理汇总了C++中cuddCacheInsert2函数的典型用法代码示例。如果您正苦于以下问题:C++ cuddCacheInsert2函数的具体用法?C++ cuddCacheInsert2怎么用?C++ cuddCacheInsert2使用的例子?那么恭喜您, 这里精选的函数代码示例或许可以为您提供帮助。
在下文中一共展示了cuddCacheInsert2函数的20个代码示例,这些例子默认根据受欢迎程度排序。您可以为喜欢或者感觉有用的代码点赞,您的评价将有助于我们的系统推荐出更棒的C++代码示例。
示例1: 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
示例2: cuddauxIsVarInRecur
/**Function********************************************************************
Synopsis [Performs the recursive step of Cuddaux_IsVarIn.]
Description [Performs the recursive step of Cuddaux_IsVarIn. var is
supposed to be a BDD projection function. Returns the logical one or
zero.]
SideEffects [None]
SeeAlso []
******************************************************************************/
DdNode*
cuddauxIsVarInRecur(DdManager* manager, DdNode* f, DdNode* Var)
{
DdNode *zero,*one, *F, *res;
int topV,topF;
one = DD_ONE(manager);
zero = Cudd_Not(one);
F = Cudd_Regular(f);
if (cuddIsConstant(F)) return zero;
if (Var==F) return(one);
topV = Var->index;
topF = F->index;
if (topF == topV) return(one);
if (cuddI(manager,topV) < cuddI(manager,topF)) return(zero);
res = cuddCacheLookup2(manager,cuddauxIsVarInRecur, F, Var);
if (res != NULL) return(res);
res = cuddauxIsVarInRecur(manager,cuddT(F),Var);
if (res==zero){
res = cuddauxIsVarInRecur(manager,cuddE(F),Var);
}
cuddCacheInsert2(manager,cuddauxIsVarInRecur,F,Var,res);
return(res);
}
开发者ID:thizanne,项目名称:mlcuddidl,代码行数:40,代码来源:cuddauxMisc.c
示例3: 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
示例4: 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
示例5: 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
示例6: 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
示例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_bddVarIsDependent
/**Function********************************************************************
Synopsis [Checks whether a variable is dependent on others in a
function.]
Description [Checks whether a variable is dependent on others in a
function. Returns 1 if the variable is dependent; 0 otherwise. No
new nodes are created.]
SideEffects [None]
SeeAlso []
******************************************************************************/
int
Cudd_bddVarIsDependent(
DdManager *dd, /* manager */
DdNode *f, /* function */
DdNode *var /* variable */)
{
DdNode *F, *res, *zero, *ft, *fe;
unsigned topf, level;
DD_CTFP cacheOp;
int retval;
/* NuSMV: begin add */
abort(); /* NOT USED BY NUSMV */
/* NuSMV: begin end */
zero = Cudd_Not(DD_TRUE(dd));
if (Cudd_IsConstant(f)) return(f == zero);
/* From now on f is not constant. */
F = Cudd_Regular(f);
topf = (unsigned) dd->perm[F->index];
level = (unsigned) dd->perm[var->index];
/* Check terminal case. If topf > index of var, f does not depend on var.
** Therefore, var is not dependent in f. */
if (topf > level) {
return(0);
}
cacheOp = (DD_CTFP) Cudd_bddVarIsDependent;
res = cuddCacheLookup2(dd,cacheOp,f,var);
if (res != NULL) {
return(res != zero);
}
/* Compute cofactors. */
ft = Cudd_NotCond(cuddT(F), f != F);
fe = Cudd_NotCond(cuddE(F), f != F);
if (topf == level) {
retval = Cudd_bddLeq(dd,ft,Cudd_Not(fe));
} else {
retval = Cudd_bddVarIsDependent(dd,ft,var) &&
Cudd_bddVarIsDependent(dd,fe,var);
}
cuddCacheInsert2(dd,cacheOp,f,var,Cudd_NotCond(zero,retval));
return(retval);
} /* Cudd_bddVarIsDependent */
开发者ID:ancailliau,项目名称:pynusmv,代码行数:65,代码来源:cuddBddAbs.c
示例9: 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
示例10: ZDDs
/**Function********************************************************************
Synopsis [Performs the inclusion test for ZDDs (P implies Q).]
Description [Inclusion test for ZDDs (P implies Q). No new nodes are
generated by this procedure. Returns empty if true;
a valid pointer different from empty or DD_NON_CONSTANT otherwise.]
SideEffects [None]
SeeAlso [Cudd_zddDiff]
******************************************************************************/
DdNode *
Cudd_zddDiffConst(
DdManager * zdd,
DdNode * P,
DdNode * Q)
{
int p_top, q_top;
DdNode *empty = DD_ZERO(zdd), *t, *res;
DdManager *table = zdd;
statLine(zdd);
if (P == empty)
return(empty);
if (Q == empty)
return(P);
if (P == Q)
return(empty);
/* Check cache. The cache is shared by cuddZddDiff(). */
res = cuddCacheLookup2Zdd(table, cuddZddDiff, P, Q);
if (res != NULL)
return(res);
if (cuddIsConstant(P))
p_top = P->index;
else
p_top = zdd->permZ[P->index];
if (cuddIsConstant(Q))
q_top = Q->index;
else
q_top = zdd->permZ[Q->index];
if (p_top < q_top) {
res = DD_NON_CONSTANT;
} else if (p_top > q_top) {
res = Cudd_zddDiffConst(zdd, P, cuddE(Q));
} else {
t = Cudd_zddDiffConst(zdd, cuddT(P), cuddT(Q));
if (t != empty)
res = DD_NON_CONSTANT;
else
res = Cudd_zddDiffConst(zdd, cuddE(P), cuddE(Q));
}
cuddCacheInsert2(table, cuddZddDiff, P, Q, res);
return(res);
} /* end of Cudd_zddDiffConst */
开发者ID:lucadealfaro,项目名称:ticc,代码行数:61,代码来源:cuddZddSetop.c
示例11: 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
示例12: 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
示例13: cuddZddIsop
//.........这里部分代码省略.........
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);
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));
if (sum == NULL) {
Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
Cudd_RecursiveDeref(dd, Id);
Cudd_RecursiveDerefZdd(dd, zdd_Id);
Cudd_RecursiveDeref(dd, term0);
Cudd_RecursiveDeref(dd, term1);
return(NULL);
}
sum = Cudd_Not(sum);
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_RecursiveDerefZdd(dd, zdd_Isub0);
Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
Cudd_RecursiveDeref(dd, Id);
Cudd_RecursiveDerefZdd(dd, zdd_Id);
Cudd_RecursiveDeref(dd, sum);
return(NULL);
}
Cudd_Ref(r);
Cudd_RecursiveDeref(dd, sum);
Cudd_RecursiveDeref(dd, Id);
if (zdd_Isub0 != zdd_zero) {
z = cuddZddGetNodeIVO(dd, index * 2 + 1, zdd_Isub0, zdd_Id);
if (z == NULL) {
Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
Cudd_RecursiveDerefZdd(dd, zdd_Id);
Cudd_RecursiveDeref(dd, r);
return(NULL);
}
}
else {
z = zdd_Id;
}
Cudd_Ref(z);
if (zdd_Isub1 != zdd_zero) {
y = cuddZddGetNodeIVO(dd, index * 2, zdd_Isub1, z);
if (y == NULL) {
Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
Cudd_RecursiveDerefZdd(dd, zdd_Id);
Cudd_RecursiveDeref(dd, r);
Cudd_RecursiveDerefZdd(dd, z);
return(NULL);
}
}
else
y = z;
Cudd_Ref(y);
Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
Cudd_RecursiveDerefZdd(dd, zdd_Id);
Cudd_RecursiveDerefZdd(dd, z);
cuddCacheInsert2(dd, cuddBddIsop, L, U, r);
cuddCacheInsert2(dd, cacheOp, L, U, y);
Cudd_Deref(r);
Cudd_Deref(y);
*zdd_I = y;
/*
if (Cudd_Regular(r)->index != y->index / 2) {
printf("*** ERROR : mismatch in indices between BDD and ZDD. ***\n");
}
*/
return(r);
} /* end of cuddZddIsop */
开发者ID:ansonn,项目名称:esl_systemc,代码行数:101,代码来源:cuddZddIsop.c
示例14: 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,代码行数:101,代码来源:cuddClip.c
示例15: Cudd_bddLeq
/**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.]
SideEffects [None]
SeeAlso [Cudd_bddIteConstant Cudd_addEvalConst]
******************************************************************************/
int
Cudd_bddLeq(
DdManager * dd,
DdNode * f,
DdNode * g)
{
DdNode *one, *zero, *tmp, *F, *fv, *fvn, *gv, *gvn;
unsigned int topf, topg, res;
statLine(dd);
/* Terminal cases and normalization. */
if (f == g) return(1);
if (Cudd_IsComplement(g)) {
/* Special case: if f is regular and g is complemented,
** f(1,...,1) = 1 > 0 = g(1,...,1).
*/
if (!Cudd_IsComplement(f)) return(0);
/* Both are complemented: Swap and complement because
** f <= g <=> g' <= f' and we want the second argument to be regular.
*/
tmp = g;
g = Cudd_Not(f);
f = Cudd_Not(tmp);
} else if (Cudd_IsComplement(f) && cuddF2L(g) < cuddF2L(f)) {
tmp = g;
g = Cudd_Not(f);
f = Cudd_Not(tmp);
}
/* Now g is regular and, if f is not regular, f < g. */
one = DD_ONE(dd);
if (g == one) return(1); /* no need to test against zero */
if (f == one) return(0); /* since at this point g != one */
if (Cudd_Not(f) == g) return(0); /* because neither is constant */
zero = Cudd_Not(one);
if (f == zero) return(1);
/* Here neither f nor g is constant. */
/* Check cache. */
tmp = cuddCacheLookup2(dd,(DD_CTFP)Cudd_bddLeq,f,g);
if (tmp != NULL) {
return(tmp == one);
}
/* Compute cofactors. */
F = Cudd_Regular(f);
topf = dd->perm[F->index];
topg = dd->perm[g->index];
if (topf <= topg) {
fv = cuddT(F); fvn = cuddE(F);
if (f != F) {
fv = Cudd_Not(fv);
fvn = Cudd_Not(fvn);
}
} else {
fv = fvn = f;
}
if (topg <= topf) {
gv = cuddT(g); gvn = cuddE(g);
} else {
gv = gvn = g;
}
/* Recursive calls. Since we want to maximize the probability of
** the special case f(1,...,1) > g(1,...,1), we consider the negative
** cofactors first. Indeed, the complementation parity of the positive
** cofactors is the same as the one of the parent functions.
*/
res = Cudd_bddLeq(dd,fvn,gvn) && Cudd_bddLeq(dd,fv,gv);
/* Store result in cache and return. */
cuddCacheInsert2(dd,(DD_CTFP)Cudd_bddLeq,f,g,(res ? one : zero));
return(res);
} /* end of Cudd_bddLeq */
开发者ID:Shubhankar007,项目名称:ECEN-699,代码行数:89,代码来源:cuddBddIte.c
示例16: extraZddSymmPairsCompute
//.........这里部分代码省略.........
// there is no need to do so, if zSymmVars is empty
if ( zSymmVars == z0 )
Cudd_RecursiveDerefZdd( dd, zSymmVars );
else
{
zPlus = cuddZddGetNode( dd, 2*bFR->index, zSymmVars, z0 );
if ( zPlus == NULL )
{
Cudd_RecursiveDerefZdd( dd, zRes );
Cudd_RecursiveDerefZdd( dd, zSymmVars );
return NULL;
}
cuddRef( zPlus );
cuddDeref( zSymmVars );
// add these variable pairs 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 );
}
// only zRes is referenced at this point
// if we skipped some variables, these variables cannot be symmetric with
// any variables that are currently in the support of bF, but they can be
// symmetric with the variables that are in bVars but not in the support of bF
if ( nVarsExtra )
{
// it is possible to improve this step:
// (1) there is no need to enter here, if nVarsExtra < 2
// create the set of topmost nVarsExtra in bVars
DdNode * bVarsExtra;
int nVars;
// remove from bVars all the variable that are in the support of bFunc
bVarsExtra = extraBddReduceVarSet( dd, bVars, bFunc );
if ( bVarsExtra == NULL )
{
Cudd_RecursiveDerefZdd( dd, zRes );
return NULL;
}
cuddRef( bVarsExtra );
// determine how many vars are in the bVarsExtra
nVars = Extra_bddSuppSize( dd, bVarsExtra );
if ( nVars < 2 )
{
Cudd_RecursiveDeref( dd, bVarsExtra );
}
else
{
int i;
DdNode * bVarsK;
// create the BDD bVarsK corresponding to K = 2;
bVarsK = bVarsExtra;
for ( i = 0; i < nVars-2; i++ )
bVarsK = cuddT( bVarsK );
// create the 2 variable tuples
zPlus = extraZddTuplesFromBdd( dd, bVarsK, bVarsExtra );
if ( zPlus == NULL )
{
Cudd_RecursiveDeref( dd, bVarsExtra );
Cudd_RecursiveDerefZdd( dd, zRes );
return NULL;
}
cuddRef( zPlus );
Cudd_RecursiveDeref( dd, bVarsExtra );
// 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 );
/* insert the result into cache */
cuddCacheInsert2(dd, extraZddSymmPairsCompute, bFunc, bVars, zRes);
return zRes;
}
} /* end of extraZddSymmPairsCompute */
开发者ID:kyotobay,项目名称:ABC_withFD_check,代码行数:101,代码来源:extraBddSymm.c
示例17: Extra_bddCheckVarsSymmetric
//.........这里部分代码省略.........
{
bF0 = cuddE(bFR);
bF1 = cuddT(bFR);
}
}
else
bF0 = bF1 = NULL;
// consider five cases:
// (1) F is above iLev1
// (2) F is on the level iLev1
// (3) F is between iLev1 and iLev2
// (4) F is on the level iLev2
// (5) F is below iLev2
// (1) F is above iLev1
if ( LevelF < iLev1 )
{
// the returned result cannot have the hash attribute
// because we still did not reach the level of Var1;
// the attribute never travels above the level of Var1
bRes0 = extraBddCheckVarsSymmetric( dd, bF0, bVars );
// assert( !Hash_IsComplement( bRes0 ) );
assert( bRes0 != z0 );
if ( bRes0 == b0 )
bRes = b0;
else
bRes = extraBddCheckVarsSymmetric( dd, bF1, bVars );
// assert( !Hash_IsComplement( bRes ) );
assert( bRes != z0 );
}
// (2) F is on the level iLev1
else if ( LevelF == iLev1 )
{
bRes0 = extraBddCheckVarsSymmetric( dd, bF0, Cudd_Not( cuddT(bVars) ) );
if ( bRes0 == b0 )
bRes = b0;
else
{
bRes1 = extraBddCheckVarsSymmetric( dd, bF1, Cudd_Not( cuddT(bVars) ) );
if ( bRes1 == b0 )
bRes = b0;
else
{
// if ( Hash_IsComplement( bRes0 ) || Hash_IsComplement( bRes1 ) )
if ( bRes0 == z0 || bRes1 == z0 )
bRes = b1;
else
bRes = b0;
}
}
}
// (3) F is between iLev1 and iLev2
else if ( LevelF < iLev2 )
{
bRes0 = extraBddCheckVarsSymmetric( dd, bF0, bVars );
if ( bRes0 == b0 )
bRes = b0;
else
{
bRes1 = extraBddCheckVarsSymmetric( dd, bF1, bVars );
if ( bRes1 == b0 )
bRes = b0;
else
{
// if ( Hash_IsComplement( bRes0 ) || Hash_IsComplement( bRes1 ) )
// bRes = Hash_Not( b1 );
if ( bRes0 == z0 || bRes1 == z0 )
bRes = z0;
else
bRes = b1;
}
}
}
// (4) F is on the level iLev2
else if ( LevelF == iLev2 )
{
// this is the only place where the hash attribute (Hash_Not) can be added
// to the result; it can be added only if the path came through the node
// lebeled with Var1; therefore, the hash attribute cannot be returned
// to the caller function
if ( fVar1Pres )
// bRes = Hash_Not( b1 );
bRes = z0;
else
bRes = b0;
}
// (5) F is below iLev2
else // if ( LevelF > iLev2 )
{
// it is possible that the path goes through the node labeled by Var1
// and still everything is okay; we do not label with Hash_Not here
// because the path does not go through node labeled by Var2
bRes = b1;
}
cuddCacheInsert2(dd, extraBddCheckVarsSymmetric, bF, bVars, bRes);
return bRes;
}
} /* end of extraBddCheckVarsSymmetric */
开发者ID:kyotobay,项目名称:ABC_withFD_check,代码行数:101,代码来源:extraBddSymm.c
示例18: cuddAddOrAbstractRecur
/**Function********************************************************************
Synopsis [Performs the recursive step of Cudd_addOrAbstract.]
Description [Performs the recursive step of Cudd_addOrAbstract.
Returns the ADD obtained by abstracting the variables of cube from f,
if successful; NULL otherwise.]
SideEffects [None]
SeeAlso []
******************************************************************************/
DdNode *
cuddAddOrAbstractRecur(
DdManager * manager,
DdNode * f,
DdNode * cube)
{
DdNode *T, *E, *res, *res1, *res2, *one;
statLine(manager);
one = DD_ONE(manager);
/* Cube is guaranteed to be a cube at this point. */
if (cuddIsConstant(f) || cube == one) {
return(f);
}
/* Abstract a variable that does not appear in f. */
if (cuddI(manager,f->index) > cuddI(manager,cube->index)) {
res = cuddAddOrAbstractRecur(manager, f, cuddT(cube));
return(res);
}
if ((res = cuddCacheLookup2(manager, Cudd_addOrAbstract, f, cube)) != NULL) {
return(res);
}
T = cuddT(f);
E = cuddE(f);
/* If the two indices are the same, so are their levels. */
if (f->index == cube->index) {
res1 = cuddAddOrAbstractRecur(manager, T, cuddT(cube));
if (res1 == NULL) return(NULL);
cuddRef(res1);
if (res1 != one) {
res2 = cuddAddOrAbstractRecur(manager, E, cuddT(cube));
if (res2 == NULL) {
Cudd_RecursiveDeref(manager,res1);
return(NULL);
}
cuddRef(res2);
res = cuddAddApplyRecur(manager, Cudd_addOr, res1, res2);
if (res == NULL) {
Cudd_RecursiveDeref(manager,res1);
Cudd_RecursiveDeref(manager,res2);
return(NULL);
}
cuddRef(res);
Cudd_RecursiveDeref(manager,res1);
Cudd_RecursiveDeref(manager,res2);
} else {
res = res1;
}
cuddCacheInsert2(manager, Cudd_addOrAbstract, f, cube, res);
cuddDeref(res);
return(res);
} else { /* if (cuddI(manager,f->index) < cuddI(manager,cube->index)) */
res1 = cuddAddOrAbstractRecur(manager, T, cube);
if (res1 == NULL) return(NULL);
cuddRef(res1);
res2 = cuddAddOrAbstractRecur(manager, E, cube);
if (res2 == NULL) {
Cudd_RecursiveDeref(manager,res1);
return(NULL);
}
cuddRef(res2);
res = (res1 == res2) ? res1 :
cuddUniqueInter(manager, (int) f->index, res1, res2);
if (res == NULL) {
Cudd_RecursiveDeref(manager,res1);
Cudd_RecursiveDeref(manager,res2);
return(NULL);
}
cuddDeref(res1);
cuddDeref(res2);
cuddCacheInsert2(manager, Cudd_addOrAbstract, f, cube, res);
return(res);
}
} /* end of cuddAddOrAbstractRecur */
开发者ID:Oliii,项目名称:MTBDD,代码行数:93,代码来源:cuddAddAbs.c
示例19: cuddCofactorRecur
//.........这里部分代码省略.........
SideEffects [None]
SeeAlso [Cudd_Cofactor]
******************************************************************************/
DdNode *
cuddCofactorRecur(
DdManager * dd,
DdNode * f,
DdNode * g)
{
DdNode *one,*zero,*F,*G,*g1,*g0,*f1,*f0,*t,*e,*r;
unsigned int topf,topg;
int comple;
F = Cudd_Regular(f);
if (cuddIsConstant(F)) return(f);
one = DD_ONE(dd);
/* The invariant g != 0 is true on entry to this procedure and is
** recursively maintained by it. Therefore it suffices to test g
** against one to make sure it is not co
|
请发表评论