/**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);
}
/**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 */
/**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 */
/**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
示例8: 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 */
/**
@brief Implements the recursive step of Cudd_bddClippingAnd.
@details Takes the conjunction of two BDDs.
@return a pointer to the result is successful; NULL otherwise.
@sideeffect None
@see cuddBddClippingAnd
*/
static DdNode *
cuddBddClippingAndRecur(
DdManager * manager,
DdNode * f,
DdNode * g,
int distance,
int direction)
{
DdNode *F, *ft, *fe, *G, *gt, *ge;
DdNode *one, *zero, *r, *t, *e;
int topf, topg;
unsigned int index;
DD_CTFP cacheOp;
statLine(manager);
one = DD_ONE(manager);
zero = Cudd_Not(one);
/* Terminal cases. */
if (f == zero || g == zero || f == Cudd_Not(g)) return(zero);
if (f == g || g == one) return(f);
if (f == one) return(g);
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);
//.........这里部分代码省略.........
/**Function********************************************************************
Synopsis [Performs the recursive step of Cudd_addUnivAbstract.]
Description [Performs the recursive step of Cudd_addUnivAbstract.
Returns the ADD obtained by abstracting the variables of cube from f,
if successful; NULL otherwise.]
SideEffects [None]
SeeAlso []
******************************************************************************/
DdNode *
cuddAddUnivAbstractRecur(
DdManager * manager,
DdNode * f,
DdNode * cube)
{
DdNode *T, *E, *res, *res1, *res2, *one, *zero;
statLine(manager);
one = DD_ONE(manager);
zero = DD_ZERO(manager);
/* Cube is guaranteed to be a cube at this point.
** zero and one are the only constatnts c such that c*c=c.
*/
if (f == zero || f == one || cube == one) {
return(f);
}
/* Abstract a variable that does not appear in f. */
if (cuddI(manager,f->index) > cuddI(manager,cube->index)) {
res1 = cuddAddUnivAbstractRecur(manager, f, cuddT(cube));
if (res1 == NULL) return(NULL);
cuddRef(res1);
/* Use the "internal" procedure to be alerted in case of
** dynamic reordering. If dynamic reordering occurs, we
** have to abort the entire abstraction.
*/
res = cuddAddApplyRecur(manager, Cudd_addTimes, res1, res1);
if (res == NULL) {
Cudd_RecursiveDeref(manager,res1);
return(NULL);
}
cuddRef(res);
Cudd_RecursiveDeref(manager,res1);
cuddDeref(res);
return(res);
}
if ((res = cuddCacheLookup2(manager, Cudd_addUnivAbstract, 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 = cuddAddUnivAbstractRecur(manager, T, cuddT(cube));
if (res1 == NULL) return(NULL);
cuddRef(res1);
res2 = cuddAddUnivAbstractRecur(manager, E, cuddT(cube));
if (res2 == NULL) {
Cudd_RecursiveDeref(manager,res1);
return(NULL);
}
cuddRef(res2);
res = cuddAddApplyRecur(manager, Cudd_addTimes, 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);
cuddCacheInsert2(manager, Cudd_addUnivAbstract, f, cube, res);
cuddDeref(res);
return(res);
} else { /* if (cuddI(manager,f->index) < cuddI(manager,cube->index)) */
res1 = cuddAddUnivAbstractRecur(manager, T, cube);
if (res1 == NULL) return(NULL);
cuddRef(res1);
res2 = cuddAddUnivAbstractRecur(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);
//.........这里部分代码省略.........
开发者ID:Oliii，项目名称:MTBDD，代码行数:101，代码来源:cuddAddAbs.c
示例11: 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
示例12: 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 */
/**Function********************************************************************
Synopsis [Performs the recursive step of Cudd_Cofactor.]
Description [Performs the recursive step of Cudd_Cofactor. Returns a
pointer to the cofactor if successful; NULL otherwise.]
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 constant.
*/
if (g == one) return(f);
/* From now on, f and g are known not to be constants. */
comple = f != F;
r = cuddCacheLookup2(dd,Cudd_Cofactor,F,g);
if (r != NULL) {
return(Cudd_NotCond(r,comple));
}
topf = dd->perm[F->index];
G = Cudd_Regular(g);
topg = dd->perm[G->index];
/* We take the cofactors of F because we are going to rely on
** the fact that the cofactors of the complement are the complements
** of the cofactors to better utilize the cache. Variable comple
** remembers whether we have to complement the result or not.
*/
if (topf <= topg) {
f1 = cuddT(F); f0 = cuddE(F);
} else {
f1 = f0 = F;
}
if (topg <= topf) {
g1 = cuddT(G); g0 = cuddE(G);
if (g != G) { g1 = Cudd_Not(g1); g0 = Cudd_Not(g0); }
} else {
g1 = g0 = g;
}
zero = Cudd_Not(one);
if (topf >= topg) {
if (g0 == zero || g0 == DD_ZERO(dd)) {
r = cuddCofactorRecur(dd, f1, g1);
} else if (g1 == zero || g1 == DD_ZERO(dd)) {
r = cuddCofactorRecur(dd, f0, g0);
} else {
(void) fprintf(stdout,"Cudd_Cofactor: Invalid restriction 2\n");
return(NULL);
}
if (r == NULL) return(NULL);
} else /* if (topf < topg) */ {
t = cuddCofactorRecur(dd, f1, g);
if (t == NULL) return(NULL);
cuddRef(t);
e = cuddCofactorRecur(dd, f0, g);
if (e == NULL) {
Cudd_RecursiveDeref(dd, t);
return(NULL);
}
cuddRef(e);
if (t == e) {
r = t;
} else if (Cudd_IsComplement(t)) {
r = cuddUniqueInter(dd,(int)F->index,Cudd_Not(t),Cudd_Not(e));
if (r != NULL)
r = Cudd_Not(r);
} else {
r = cuddUniqueInter(dd,(int)F->index,t,e);
}
if (r == NULL) {
Cudd_RecursiveDeref(dd ,e);
Cudd_RecursiveDeref(dd ,t);
return(NULL);
}
cuddDeref(t);
cuddDeref(e);
}
//.........这里部分代码省略.........
/**Function********************************************************************
Synopsis [Implements the recursive step of Cudd_bddAnd.]
Description [Implements the recursive step of Cudd_bddAnd by taking
the conjunction of two BDDs. Returns a pointer to the result is
successful; NULL otherwise.]
SideEffects [None]
SeeAlso [Cudd_bddAnd]
******************************************************************************/
DdNode *
cuddBddAndRecur(
DdManager * manager,
DdNode * f,
DdNode * g)
{
DdNode *F, *fv, *fnv, *G, *gv, *gnv;
DdNode *one, *r, *t, *e;
unsigned int topf, topg, index;
statLine(manager);
one = DD_ONE(manager);
/* Terminal cases. */
F = Cudd_Regular(f);
G = Cudd_Regular(g);
if (F == G) {
if (f == g) return(f);
else return(Cudd_Not(one));
}
if (F == one) {
if (f == one) return(g);
else return(f);
}
if (G == one) {
if (g == one) return(f);
else return(g);
}
/* At this point f and g are not constant. */
if (cuddF2L(f) > cuddF2L(g)) { /* Try to increase cache efficiency. */
DdNode *tmp = f;
f = g;
g = tmp;
F = Cudd_Regular(f);
G = Cudd_Regular(g);
}
/* Check cache. */
if (F->ref != 1 || G->ref != 1) {
r = cuddCacheLookup2(manager, Cudd_bddAnd, f, g);
if (r != NULL) return(r);
}
if ( manager->TimeStop && Abc_Clock() > manager->TimeStop )
return NULL;
/* 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;
fv = cuddT(F);
fnv = cuddE(F);
if (Cudd_IsComplement(f)) {
fv = Cudd_Not(fv);
fnv = Cudd_Not(fnv);
}
} else {
index = G->index;
fv = fnv = f;
}
if (topg <= topf) {
gv = cuddT(G);
gnv = cuddE(G);
if (Cudd_IsComplement(g)) {
gv = Cudd_Not(gv);
gnv = Cudd_Not(gnv);
}
} else {
gv = gnv = g;
}
t = cuddBddAndRecur(manager, fv, gv);
if (t == NULL) return(NULL);
cuddRef(t);
e = cuddBddAndRecur(manager, fnv, gnv);
if (e == NULL) {
Cudd_IterDerefBdd(manager, t);
return(NULL);
}
//.........这里部分代码省略.........
/**Function********************************************************************
Synopsis [Performs the recursive steps of Cudd_bddExistAbstract.]
Description [Performs the recursive steps of Cudd_bddExistAbstract.
Returns the BDD obtained by abstracting the variables
of cube from f if successful; NULL otherwise. It is also used by
Cudd_bddUnivAbstract.]
SideEffects [None]
SeeAlso [Cudd_bddExistAbstract Cudd_bddUnivAbstract]
******************************************************************************/
DdNode *
cuddBddExistAbstractRecur(
DdManager * manager,
DdNode * f,
DdNode * cube)
{
DdNode *F, *T, *E, *res, *res1, *res2, *one;
statLine(manager);
one = DD_ONE(manager);
F = Cudd_Regular(f);
/* Cube is guaranteed to be a cube at this point. */
if (cube == one || F == one) {
return(f);
}
/* From now on, f and cube are non-constant. */
/* Abstract a variable that does not appear in f. */
while (manager->perm[F->index] > manager->perm[cube->index]) {
cube = cuddT(cube);
if (cube == one) return(f);
}
/* Check the cache. */
if (F->ref != 1 && (res = cuddCacheLookup2(manager, Cudd_bddExistAbstract, f, cube)) != NULL) {
return(res);
}
/* Compute the cofactors of f. */
T = cuddT(F); E = cuddE(F);
if (f != F) {
T = Cudd_Not(T); E = Cudd_Not(E);
}
/* If the two indices are the same, so are their levels. */
if (F->index == cube->index) {
if (T == one || E == one || T == Cudd_Not(E)) {
return(one);
}
res1 = cuddBddExistAbstractRecur(manager, T, cuddT(cube));
if (res1 == NULL) return(NULL);
if (res1 == one) {
if (F->ref != 1)
cuddCacheInsert2(manager, Cudd_bddExistAbstract, f, cube, one);
return(one);
}
cuddRef(res1);
res2 = cuddBddExistAbstractRecur(manager, E, cuddT(cube));
if (res2 == NULL) {
Cudd_IterDerefBdd(manager,res1);
return(NULL);
}
cuddRef(res2);
res = cuddBddAndRecur(manager, Cudd_Not(res1), Cudd_Not(res2));
if (res == NULL) {
Cudd_IterDerefBdd(manager, res1);
Cudd_IterDerefBdd(manager, res2);
return(NULL);
}
res = Cudd_Not(res);
cuddRef(res);
Cudd_IterDerefBdd(manager, res1);
Cudd_IterDerefBdd(manager, res2);
if (F->ref != 1)
cuddCacheInsert2(manager, Cudd_bddExistAbstract, f, cube, res);
cuddDeref(res);
return(res);
} else { /* if (cuddI(manager,F->index) < cuddI(manager,cube->index)) */
res1 = cuddBddExistAbstractRecur(manager, T, cube);
if (res1 == NULL) return(NULL);
cuddRef(res1);
res2 = cuddBddExistAbstractRecur(manager, E, cube);
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);
}
//.........这里部分代码省略.........
/**Function********************************************************************
Synopsis [Implements the recursive step of Cudd_bddIntersect.]
Description []
SideEffects [None]
SeeAlso [Cudd_bddIntersect]
******************************************************************************/
DdNode *
cuddBddIntersectRecur(
DdManager * dd,
DdNode * f,
DdNode * g)
{
DdNode *res;
DdNode *F, *G, *t, *e;
DdNode *fv, *fnv, *gv, *gnv;
DdNode *one, *zero;
unsigned int index, topf, topg;
statLine(dd);
one = DD_ONE(dd);
zero = Cudd_Not(one);
/* Terminal cases. */
if (f == zero || g == zero || f == Cudd_Not(g)) return(zero);
if (f == g || g == one) return(f);
if (f == one) return(g);
/* At this point f and g are not constant. */
if (cuddF2L(f) > cuddF2L(g)) { DdNode *tmp = f; f = g; g = tmp; }
res = cuddCacheLookup2(dd,Cudd_bddIntersect,f,g);
if (res != NULL) return(res);
/* Find splitting variable. Here we can skip the use of cuddI,
** because the operands are known to be non-constant.
*/
F = Cudd_Regular(f);
topf = dd->perm[F->index];
G = Cudd_Regular(g);
topg = dd->perm[G->index];
/* Compute cofactors. */
if (topf <= topg) {
index = F->index;
fv = cuddT(F);
fnv = cuddE(F);
if (Cudd_IsComplement(f)) {
fv = Cudd_Not(fv);
fnv = Cudd_Not(fnv);
}
} else {
index = G->index;
fv = fnv = f;
}
if (topg <= topf) {
gv = cuddT(G);
gnv = cuddE(G);
if (Cudd_IsComplement(g)) {
gv = Cudd_Not(gv);
gnv = Cudd_Not(gnv);
}
} else {
gv = gnv = g;
}
/* Compute partial results. */
t = cuddBddIntersectRecur(dd,fv,gv);
if (t == NULL) return(NULL);
cuddRef(t);
if (t != zero) {
e = zero;
} else {
e = cuddBddIntersectRecur(dd,fnv,gnv);
if (e == NULL) {
Cudd_IterDerefBdd(dd, t);
return(NULL);
}
}
cuddRef(e);
if (t == e) { /* both equal zero */
res = t;
} else if (Cudd_IsComplement(t)) {
res = cuddUniqueInter(dd,(int)index,Cudd_Not(t),Cudd_Not(e));
if (res == NULL) {
Cudd_IterDerefBdd(dd, t);
Cudd_IterDerefBdd(dd, e);
return(NULL);
}
res = Cudd_Not(res);
} else {
res = cuddUniqueInter(dd,(int)index,t,e);
if (res == NULL) {
Cudd_IterDerefBdd(dd, t);
Cudd_IterDerefBdd(dd, e);
//.........这里部分代码省略.........
/**Function********************************************************************
Synopsis [Performs the recursive step of Cudd_CProjection.]
Description [Performs the recursive step of Cudd_CProjection. Returns
the projection if successful; NULL otherwise.]
SideEffects [None]
SeeAlso [Cudd_CProjection]
******************************************************************************/
DdNode *
cuddCProjectionRecur(
DdManager * dd,
DdNode * R,
DdNode * Y,
DdNode * Ysupp)
{
DdNode *res, *res1, *res2, *resA;
DdNode *r, *y, *RT, *RE, *YT, *YE, *Yrest, *Ra, *Ran, *Gamma, *Alpha;
unsigned int topR, topY, top, index;
DdNode *one = DD_ONE(dd);
statLine(dd);
if (Y == one) return(R);
#ifdef DD_DEBUG
assert(!Cudd_IsConstant(Y));
#endif
if (R == Cudd_Not(one)) return(R);
res = cuddCacheLookup2(dd, Cudd_CProjection, R, Y);
if (res != NULL) return(res);
r = Cudd_Regular(R);
topR = cuddI(dd,r->index);
y = Cudd_Regular(Y);
topY = cuddI(dd,y->index);
top = ddMin(topR, topY);
/* Compute the cofactors of R */
if (topR == top) {
index = r->index;
RT = cuddT(r);
RE = cuddE(r);
if (r != R) {
RT = Cudd_Not(RT); RE = Cudd_Not(RE);
}
} else {
RT = RE = R;
}
if (topY > top) {
/* Y does not depend on the current top variable.
** We just need to compute the results on the two cofactors of R
** and make them the children of a node labeled r->index.
*/
res1 = cuddCProjectionRecur(dd,RT,Y,Ysupp);
if (res1 == NULL) return(NULL);
cuddRef(res1);
res2 = cuddCProjectionRecur(dd,RE,Y,Ysupp);
if (res2 == NULL) {
Cudd_RecursiveDeref(dd,res1);
return(NULL);
}
cuddRef(res2);
res = cuddBddIteRecur(dd, dd->vars[index], res1, res2);
if (res == NULL) {
Cudd_RecursiveDeref(dd,res1);
Cudd_RecursiveDeref(dd,res2);
return(NULL);
}
/* If we have reached this point, res1 and res2 are now
** incorporated in res. cuddDeref is therefore sufficient.
*/
cuddDeref(res1);
cuddDeref(res2);
} else {
/* Compute the cofactors of Y */
index = y->index;
YT = cuddT(y);
YE = cuddE(y);
if (y != Y) {
YT = Cudd_Not(YT); YE = Cudd_Not(YE);
}
if (YT == Cudd_Not(one)) {
Alpha = Cudd_Not(dd->vars[index]);
Yrest = YE;
Ra = RE;
Ran = RT;
} else {
Alpha = dd->vars[index];
Yrest = YT;
Ra = RT;
Ran = RE;
}
Gamma = cuddBddExistAbstractRecur(dd,Ra,cuddT(Ysupp));
//.........这里部分代码省略.........
客服电话
APP下载
官方微信
请发表评论