本文整理汇总了C++中cuddDeref函数的典型用法代码示例。如果您正苦于以下问题:C++ cuddDeref函数的具体用法?C++ cuddDeref怎么用?C++ cuddDeref使用的例子?那么恭喜您, 这里精选的函数代码示例或许可以为您提供帮助。
在下文中一共展示了cuddDeref函数的20个代码示例,这些例子默认根据受欢迎程度排序。您可以为喜欢或者感觉有用的代码点赞,您的评价将有助于我们的系统推荐出更棒的C++代码示例。
示例1: Cudd_addExistAbstract
/**Function********************************************************************
Synopsis [Existentially Abstracts all the variables in cube from f.]
Description [Abstracts all the variables in cube from f by summing
over all possible values taken by the variables. Returns the
abstracted ADD.]
SideEffects [None]
SeeAlso [Cudd_addUnivAbstract Cudd_bddExistAbstract
Cudd_addOrAbstract]
******************************************************************************/
DdNode *
Cudd_addExistAbstract(
DdManager * manager,
DdNode * f,
DdNode * cube)
{
DdNode *res;
two = cuddUniqueConst(manager,(CUDD_VALUE_TYPE) 2);
if (two == NULL) return(NULL);
cuddRef(two);
if (addCheckPositiveCube(manager, cube) == 0) {
(void) fprintf(manager->err,"Error: Can only abstract cubes");
return(NULL);
}
do {
manager->reordered = 0;
res = cuddAddExistAbstractRecur(manager, f, cube);
} while (manager->reordered == 1);
if (res == NULL) {
Cudd_RecursiveDeref(manager,two);
return(NULL);
}
cuddRef(res);
Cudd_RecursiveDeref(manager,two);
cuddDeref(res);
return(res);
} /* end of Cudd_addExistAbstract */
开发者ID:dtzWill,项目名称:SVF,代码行数:47,代码来源:cuddAddAbs.c
示例2: Cudd_addBddStrictThreshold
/**Function********************************************************************
Synopsis [Converts an ADD to a BDD.]
Description [Converts an ADD to a BDD by replacing all
discriminants STRICTLY greater than value with 1, and all other
discriminants with 0. Returns a pointer to the resulting BDD if
successful; NULL otherwise.]
SideEffects [None]
SeeAlso [Cudd_addBddInterval Cudd_addBddPattern Cudd_BddToAdd
Cudd_addBddThreshold]
******************************************************************************/
DdNode *
Cudd_addBddStrictThreshold(
DdManager * dd,
DdNode * f,
CUDD_VALUE_TYPE value)
{
DdNode *res;
DdNode *val;
/* NuSMV: begin add */
abort(); /* NOT USED BY NUSMV */
/* NuSMV: begin end */
val = cuddUniqueConst(dd,value);
if (val == NULL) return(NULL);
cuddRef(val);
do {
dd->reordered = 0;
res = addBddDoStrictThreshold(dd, f, val);
} while (dd->reordered == 1);
if (res == NULL) {
Cudd_RecursiveDeref(dd, val);
return(NULL);
}
cuddRef(res);
Cudd_RecursiveDeref(dd, val);
cuddDeref(res);
return(res);
} /* end of Cudd_addBddStrictThreshold */
开发者ID:ancailliau,项目名称:pynusmv,代码行数:46,代码来源:cuddBridge.c
示例3: cuddZddComplement
/**Function********************************************************************
Synopsis [Computes a complement of a ZDD node.]
Description [Computes the complement of a ZDD node. So far, since we
couldn't find a direct way to get the complement of a ZDD cover, we first
convert a ZDD cover to a BDD, then make the complement of the ZDD cover
from the complement of the BDD node by using ISOP.]
SideEffects [The result depends on current variable order.]
SeeAlso []
******************************************************************************/
DdNode *
cuddZddComplement(
DdManager * dd,
DdNode *node)
{
DdNode *b, *isop, *zdd_I;
/* Check cache */
zdd_I = cuddCacheLookup1Zdd(dd, cuddZddComplement, node);
if (zdd_I)
return(zdd_I);
b = cuddMakeBddFromZddCover(dd, node);
if (!b)
return(NULL);
cuddRef(b);
isop = cuddZddIsop(dd, Cudd_Not(b), Cudd_Not(b), &zdd_I);
if (!isop) {
Cudd_RecursiveDeref(dd, b);
return(NULL);
}
cuddRef(isop);
cuddRef(zdd_I);
Cudd_RecursiveDeref(dd, b);
Cudd_RecursiveDeref(dd, isop);
cuddCacheInsert1(dd, cuddZddComplement, node, zdd_I);
cuddDeref(zdd_I);
return(zdd_I);
} /* end of cuddZddComplement */
开发者ID:maeon,项目名称:SBSAT,代码行数:44,代码来源:cuddZddFuncs.c
示例4: cuddZddSubset0
/**Function********************************************************************
Synopsis [Computes the negative cofactor of a ZDD w.r.t. a variable.]
Description [Computes the negative cofactor of a ZDD w.r.t. a
variable. In terms of combinations, the result is the set of all
combinations in which the variable is negated. Returns a pointer to
the result if successful; NULL otherwise. cuddZddSubset0 performs
the same function as Cudd_zddSubset0, but does not restart if
reordering has taken place. Therefore it can be called from within a
recursive procedure.]
SideEffects [None]
SeeAlso [cuddZddSubset1 Cudd_zddSubset0]
******************************************************************************/
DdNode *
cuddZddSubset0(
DdManager * dd,
DdNode * P,
int var)
{
DdNode *zvar, *r;
DdNode *base, *empty;
base = DD_TRUE(dd);
empty = DD_FALSE(dd);
zvar = cuddUniqueInterZdd(dd, var, base, empty);
if (zvar == NULL) {
return(NULL);
} else {
cuddRef(zvar);
r = zdd_subset0_aux(dd, P, zvar);
if (r == NULL) {
Cudd_RecursiveDerefZdd(dd, zvar);
return(NULL);
}
cuddRef(r);
Cudd_RecursiveDerefZdd(dd, zvar);
}
cuddDeref(r);
return(r);
} /* end of cuddZddSubset0 */
开发者ID:ancailliau,项目名称:pynusmv,代码行数:47,代码来源:cuddZddSetop.c
示例5: 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
示例6: cuddBddVarMapRecur
/**Function********************************************************************
Synopsis [Implements the recursive step of Cudd_bddVarMap.]
Description [Implements the recursive step of Cudd_bddVarMap.
Returns a pointer to the result if successful; NULL otherwise.]
SideEffects [None]
SeeAlso [Cudd_bddVarMap]
******************************************************************************/
static DdNode *
cuddBddVarMapRecur(
DdManager *manager /* DD manager */,
DdNode *f /* BDD to be remapped */)
{
DdNode *F, *T, *E;
DdNode *res;
int index;
statLine(manager);
F = Cudd_Regular(f);
/* Check for terminal case of constant node. */
if (cuddIsConstant(F)) {
return(f);
}
/* If problem already solved, look up answer and return. */
if (F->ref != 1 &&
(res = cuddCacheLookup1(manager,Cudd_bddVarMap,F)) != NULL) {
return(Cudd_NotCond(res,F != f));
}
/* Split and recur on children of this node. */
T = cuddBddVarMapRecur(manager,cuddT(F));
if (T == NULL) return(NULL);
cuddRef(T);
E = cuddBddVarMapRecur(manager,cuddE(F));
if (E == NULL) {
Cudd_IterDerefBdd(manager, T);
return(NULL);
}
cuddRef(E);
/* Move variable that should be in this position to this position
** by retrieving the single var BDD for that variable, and calling
** cuddBddIteRecur with the T and E we just created.
*/
index = manager->map[F->index];
res = cuddBddIteRecur(manager,manager->vars[index],T,E);
if (res == NULL) {
Cudd_IterDerefBdd(manager, T);
Cudd_IterDerefBdd(manager, E);
return(NULL);
}
cuddRef(res);
Cudd_IterDerefBdd(manager, T);
Cudd_IterDerefBdd(manager, E);
/* Do not keep the result if the reference count is only 1, since
** it will not be visited again.
*/
if (F->ref != 1) {
cuddCacheInsert1(manager,Cudd_bddVarMap,F,res);
}
cuddDeref(res);
return(Cudd_NotCond(res,F != f));
} /* end of cuddBddVarMapRecur */
开发者ID:lucadealfaro,项目名称:ticc,代码行数:71,代码来源:cuddCompose.c
示例7: Extra_bddSpaceCanonVars
/**Function*************************************************************
Synopsis [Performs the recursive step of Extra_bddSpaceCanonVars().]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
DdNode * extraBddSpaceCanonVars( DdManager * dd, DdNode * bF )
{
DdNode * bRes, * bFR;
statLine( dd );
bFR = Cudd_Regular(bF);
if ( cuddIsConstant(bFR) )
return bF;
if ( (bRes = cuddCacheLookup1(dd, extraBddSpaceCanonVars, bF)) )
return bRes;
else
{
DdNode * bF0, * bF1;
DdNode * bRes, * bRes0;
if ( bFR != bF ) // bF is complemented
{
bF0 = Cudd_Not( cuddE(bFR) );
bF1 = Cudd_Not( cuddT(bFR) );
}
else
{
bF0 = cuddE(bFR);
bF1 = cuddT(bFR);
}
if ( bF0 == b0 )
{
bRes = extraBddSpaceCanonVars( dd, bF1 );
if ( bRes == NULL )
return NULL;
}
else if ( bF1 == b0 )
{
bRes = extraBddSpaceCanonVars( dd, bF0 );
if ( bRes == NULL )
return NULL;
}
else
{
bRes0 = extraBddSpaceCanonVars( dd, bF0 );
if ( bRes0 == NULL )
return NULL;
cuddRef( bRes0 );
bRes = cuddUniqueInter( dd, bFR->index, bRes0, b0 );
if ( bRes == NULL )
{
Cudd_RecursiveDeref( dd,bRes0 );
return NULL;
}
cuddDeref( bRes0 );
}
cuddCacheInsert1( dd, extraBddSpaceCanonVars, bF, bRes );
return bRes;
}
}
开发者ID:kyotobay,项目名称:ABC_withFD_check,代码行数:70,代码来源:extraBddAuto.c
示例8: cuddAddCmplRecur
/**Function********************************************************************
Synopsis [Performs the recursive step of Cudd_addCmpl.]
Description [Performs the recursive step of Cudd_addCmpl. Returns a
pointer to the resulting ADD if successful; NULL otherwise.]
SideEffects [None]
SeeAlso [Cudd_addCmpl]
******************************************************************************/
DdNode *
cuddAddCmplRecur(
DdManager * dd,
DdNode * f)
{
DdNode *one,*zero;
DdNode *r,*Fv,*Fnv,*t,*e;
statLine(dd);
one = DD_ONE(dd);
zero = DD_ZERO(dd);
if (cuddIsConstant(f)) {
if (f == zero) {
return(one);
} else {
return(zero);
}
}
r = cuddCacheLookup1(dd,Cudd_addCmpl,f);
if (r != NULL) {
return(r);
}
Fv = cuddT(f);
Fnv = cuddE(f);
t = cuddAddCmplRecur(dd,Fv);
if (t == NULL) return(NULL);
cuddRef(t);
e = cuddAddCmplRecur(dd,Fnv);
if (e == NULL) {
Cudd_RecursiveDeref(dd,t);
return(NULL);
}
cuddRef(e);
r = (t == e) ? t : cuddUniqueInter(dd,(int)f->index,t,e);
if (r == NULL) {
Cudd_RecursiveDeref(dd, t);
Cudd_RecursiveDeref(dd, e);
return(NULL);
}
cuddDeref(t);
cuddDeref(e);
cuddCacheInsert1(dd,Cudd_addCmpl,f,r);
return(r);
} /* end of cuddAddCmplRecur */
开发者ID:maeon,项目名称:SBSAT,代码行数:58,代码来源:cuddAddIte.c
示例9: mintermsFromUniverse
/**Function********************************************************************
Synopsis [Recursive procedure to extract n mintems from constant 1.]
Description [Recursive procedure to extract n mintems from constant 1.]
SideEffects [None]
******************************************************************************/
static DdNode *
mintermsFromUniverse(
DdManager * manager,
DdNode ** vars,
int numVars,
double n,
int index)
{
DdNode *one, *zero;
DdNode *q, *result;
double max, max2;
statLine(manager);
one = DD_ONE(manager);
zero = Cudd_Not(one);
max = pow(2.0, (double)numVars);
max2 = max / 2.0;
if (n == max)
return(one);
if (n == 0.0)
return(zero);
/* if n == 2^(numVars-1), return a single variable */
if (n == max2)
return vars[index];
else if (n > max2) {
/* When n > 2^(numVars-1), a single variable vars[index]
** contains 2^(numVars-1) minterms. The rest are extracted
** from a constant with 1 less variable.
*/
q = mintermsFromUniverse(manager,vars,numVars-1,(n-max2),index+1);
if (q == NULL)
return(NULL);
cuddRef(q);
result = cuddBddIteRecur(manager,vars[index],one,q);
} else {
/* When n < 2^(numVars-1), a literal of variable vars[index]
** is selected. The required n minterms are extracted from a
** constant with 1 less variable.
*/
q = mintermsFromUniverse(manager,vars,numVars-1,n,index+1);
if (q == NULL)
return(NULL);
cuddRef(q);
result = cuddBddAndRecur(manager,vars[index],q);
}
if (result == NULL) {
Cudd_RecursiveDeref(manager,q);
return(NULL);
}
cuddRef(result);
Cudd_RecursiveDeref(manager,q);
cuddDeref(result);
return(result);
} /* end of mintermsFromUniverse */
开发者ID:Oliii,项目名称:MTBDD,代码行数:67,代码来源:cuddSplit.c
示例10: extraZddSelectOneSubset
/**Function********************************************************************
Synopsis [Performs the recursive step of Extra_zddSelectOneSubset.]
Description []
SideEffects [None]
SeeAlso []
******************************************************************************/
DdNode * extraZddSelectOneSubset(
DdManager * dd,
DdNode * zS )
// selects one subset from the ZDD zS
// returns z0 if and only if zS is an empty set of cubes
{
DdNode * zRes;
if ( zS == z0 ) return z0;
if ( zS == z1 ) return z1;
// check cache
if ( (zRes = cuddCacheLookup1Zdd( dd, extraZddSelectOneSubset, zS )) )
return zRes;
else
{
DdNode * zS0, * zS1, * zTemp;
zS0 = cuddE(zS);
zS1 = cuddT(zS);
if ( zS0 != z0 )
{
zRes = extraZddSelectOneSubset( dd, zS0 );
if ( zRes == NULL )
return NULL;
}
else // if ( zS0 == z0 )
{
assert( zS1 != z0 );
zRes = extraZddSelectOneSubset( dd, zS1 );
if ( zRes == NULL )
return NULL;
cuddRef( zRes );
zRes = cuddZddGetNode( dd, zS->index, zTemp = zRes, z0 );
if ( zRes == NULL )
{
Cudd_RecursiveDerefZdd( dd, zTemp );
return NULL;
}
cuddDeref( zTemp );
}
// insert the result into cache
cuddCacheInsert1( dd, extraZddSelectOneSubset, zS, zRes );
return zRes;
}
} /* end of extraZddSelectOneSubset */
开发者ID:kyotobay,项目名称:ABC_withFD_check,代码行数:60,代码来源:extraBddSymm.c
示例11: Cudd_Xgty
/**Function********************************************************************
Synopsis [Generates a BDD for the function x > y.]
Description [This function generates a BDD for the function x > y.
Both x and y are N-bit numbers, x\[0\] x\[1\] ... x\[N-1\] and
y\[0\] y\[1\] ... y\[N-1\], with 0 the most significant bit.
The BDD is built bottom-up.
It has 3*N-1 internal nodes, if the variables are ordered as follows:
x\[0\] y\[0\] x\[1\] y\[1\] ... x\[N-1\] y\[N-1\].
Argument z is not used by Cudd_Xgty: it is included to make it
call-compatible to Cudd_Dxygtdxz and Cudd_Dxygtdyz.]
SideEffects [None]
SeeAlso [Cudd_PrioritySelect Cudd_Dxygtdxz Cudd_Dxygtdyz]
******************************************************************************/
DdNode *
Cudd_Xgty(
DdManager * dd /* DD manager */,
int N /* number of x and y variables */,
DdNode ** z /* array of z variables: unused */,
DdNode ** x /* array of x variables */,
DdNode ** y /* array of y variables */)
{
DdNode *u, *v, *w;
int i;
/* Build bottom part of BDD outside loop. */
u = Cudd_bddAnd(dd, x[N-1], Cudd_Not(y[N-1]));
if (u == NULL) return(NULL);
cuddRef(u);
/* Loop to build the rest of the BDD. */
for (i = N-2; i >= 0; i--) {
v = Cudd_bddAnd(dd, y[i], Cudd_Not(u));
if (v == NULL) {
Cudd_RecursiveDeref(dd, u);
return(NULL);
}
cuddRef(v);
w = Cudd_bddAnd(dd, Cudd_Not(y[i]), u);
if (w == NULL) {
Cudd_RecursiveDeref(dd, u);
Cudd_RecursiveDeref(dd, v);
return(NULL);
}
cuddRef(w);
Cudd_RecursiveDeref(dd, u);
u = Cudd_bddIte(dd, x[i], Cudd_Not(v), w);
if (u == NULL) {
Cudd_RecursiveDeref(dd, v);
Cudd_RecursiveDeref(dd, w);
return(NULL);
}
cuddRef(u);
Cudd_RecursiveDeref(dd, v);
Cudd_RecursiveDeref(dd, w);
}
cuddDeref(u);
return(u);
} /* end of Cudd_Xgty */
开发者ID:saidalfaraby,项目名称:DTP4TC,代码行数:65,代码来源:cuddPriority.c
示例12: extraZddGetSingletons
/**Function********************************************************************
Synopsis [Performs a recursive step of Extra_zddGetSingletons.]
Description [Returns the set of ZDD singletons, containing those positive
polarity ZDD variables that correspond to the BDD variables in bVars.]
SideEffects []
SeeAlso []
******************************************************************************/
DdNode * extraZddGetSingletons(
DdManager * dd, /* the DD manager */
DdNode * bVars) /* the set of variables */
{
DdNode * zRes;
if ( bVars == b1 )
// if ( bVars == b0 ) // bug fixed by Jin Zhang, Jan 23, 2004
return z1;
if ( (zRes = cuddCacheLookup1Zdd(dd, extraZddGetSingletons, bVars)) )
return zRes;
else
{
DdNode * zTemp, * zPlus;
// solve subproblem
zRes = extraZddGetSingletons( dd, cuddT(bVars) );
if ( zRes == NULL )
return NULL;
cuddRef( zRes );
zPlus = cuddZddGetNode( dd, 2*bVars->index, z1, z0 );
if ( zPlus == NULL )
{
Cudd_RecursiveDerefZdd( dd, zRes );
return NULL;
}
cuddRef( zPlus );
// add these to the result
zRes = cuddZddUnion( dd, zTemp = zRes, zPlus );
if ( zRes == NULL )
{
Cudd_RecursiveDerefZdd( dd, zTemp );
Cudd_RecursiveDerefZdd( dd, zPlus );
return NULL;
}
cuddRef( zRes );
Cudd_RecursiveDerefZdd( dd, zTemp );
Cudd_RecursiveDerefZdd( dd, zPlus );
cuddDeref( zRes );
cuddCacheInsert1( dd, extraZddGetSingletons, bVars, zRes );
return zRes;
}
} /* end of extraZddGetSingletons */
开发者ID:kyotobay,项目名称:ABC_withFD_check,代码行数:59,代码来源:extraBddSymm.c
示例13: Cudd_addBddInterval
/**Function********************************************************************
Synopsis [Converts an ADD to a BDD.]
Description [Converts an ADD to a BDD by replacing all
discriminants greater than or equal to lower and less than or equal to
upper with 1, and all other discriminants with 0. Returns a pointer to
the resulting BDD if successful; NULL otherwise.]
SideEffects [None]
SeeAlso [Cudd_addBddThreshold Cudd_addBddStrictThreshold
Cudd_addBddPattern Cudd_BddToAdd]
******************************************************************************/
DdNode *
Cudd_addBddInterval(
DdManager * dd,
DdNode * f,
CUDD_VALUE_TYPE lower,
CUDD_VALUE_TYPE upper)
{
DdNode *res;
DdNode *l;
DdNode *u;
/* NuSMV: begin add */
abort(); /* NOT USED BY NUSMV */
/* NuSMV: begin end */
/* Create constant nodes for the interval bounds, so that we can use
** the global cache.
*/
l = cuddUniqueConst(dd,lower);
if (l == NULL) return(NULL);
cuddRef(l);
u = cuddUniqueConst(dd,upper);
if (u == NULL) {
Cudd_RecursiveDeref(dd,l);
return(NULL);
}
cuddRef(u);
do {
dd->reordered = 0;
res = addBddDoInterval(dd, f, l, u);
} while (dd->reordered == 1);
if (res == NULL) {
Cudd_RecursiveDeref(dd, l);
Cudd_RecursiveDeref(dd, u);
return(NULL);
}
cuddRef(res);
Cudd_RecursiveDeref(dd, l);
Cudd_RecursiveDeref(dd, u);
cuddDeref(res);
return(res);
} /* end of Cudd_addBddInterval */
开发者ID:ancailliau,项目名称:pynusmv,代码行数:60,代码来源:cuddBridge.c
示例14: Cudd_addHamming
/**Function********************************************************************
Synopsis [Computes the Hamming distance ADD.]
Description [Computes the Hamming distance ADD. Returns an ADD that
gives the Hamming distance between its two arguments if successful;
NULL otherwise. The two vectors xVars and yVars identify the variables
that form the two arguments.]
SideEffects [None]
SeeAlso []
******************************************************************************/
DdNode *
Cudd_addHamming(
DdManager * dd,
DdNode ** xVars,
DdNode ** yVars,
int nVars)
{
DdNode *result,*tempBdd;
DdNode *tempAdd,*temp;
int i;
result = DD_ZERO(dd);
cuddRef(result);
for (i = 0; i < nVars; i++) {
tempBdd = Cudd_bddIte(dd,xVars[i],Cudd_Not(yVars[i]),yVars[i]);
if (tempBdd == NULL) {
Cudd_RecursiveDeref(dd,result);
return(NULL);
}
cuddRef(tempBdd);
tempAdd = Cudd_BddToAdd(dd,tempBdd);
if (tempAdd == NULL) {
Cudd_RecursiveDeref(dd,tempBdd);
Cudd_RecursiveDeref(dd,result);
return(NULL);
}
cuddRef(tempAdd);
Cudd_RecursiveDeref(dd,tempBdd);
temp = Cudd_addApply(dd,Cudd_addPlus,tempAdd,result);
if (temp == NULL) {
Cudd_RecursiveDeref(dd,tempAdd);
Cudd_RecursiveDeref(dd,result);
return(NULL);
}
cuddRef(temp);
Cudd_RecursiveDeref(dd,tempAdd);
Cudd_RecursiveDeref(dd,result);
result = temp;
}
cuddDeref(result);
return(result);
} /* end of Cudd_addHamming */
开发者ID:saidalfaraby,项目名称:DTP4TC,代码行数:59,代码来源:cuddPriority.c
示例15: cuddZddInitUniv
/**Function********************************************************************
Synopsis [Initializes the ZDD universe.]
Description [Initializes the ZDD universe. Returns 1 if successful; 0
otherwise.]
SideEffects [None]
SeeAlso [cuddZddFreeUniv]
******************************************************************************/
int
cuddZddInitUniv(
DdManager * zdd)
{
DdNode *p, *res;
int i;
#ifdef __osf__
#pragma pointer_size save
#pragma pointer_size short
#endif
zdd->univ = ALLOC(DdNode *, zdd->sizeZ);
#ifdef __osf__
#pragma pointer_size restore
#endif
if (zdd->univ == NULL) {
zdd->errorCode = CUDD_MEMORY_OUT;
return(0);
}
res = DD_ONE(zdd);
cuddRef(res);
for (i = zdd->sizeZ - 1; i >= 0; i--) {
unsigned int index = zdd->invpermZ[i];
p = res;
res = cuddUniqueInterZdd(zdd, index, p, p);
if (res == NULL) {
Cudd_RecursiveDerefZdd(zdd,p);
FREE(zdd->univ);
return(0);
}
cuddRef(res);
cuddDeref(p);
zdd->univ[i] = res;
}
#ifdef DD_VERBOSE
cuddZddP(zdd, zdd->univ[0]);
#endif
return(1);
} /* end of cuddZddInitUniv */
开发者ID:invisibleboy,项目名称:mycompiler,代码行数:55,代码来源:cuddInit.c
示例16: extraTransferPermuteTime
/**Function********************************************************************
Synopsis [Convert a BDD from a manager to another one.]
Description [Convert a BDD from a manager to another one. Returns a
pointer to the BDD in the destination manager if successful; NULL
otherwise.]
SideEffects [None]
SeeAlso [Extra_TransferPermute]
******************************************************************************/
DdNode * extraTransferPermuteTime( DdManager * ddS, DdManager * ddD, DdNode * f, int * Permute, int TimeOut )
{
DdNode *res;
st_table *table = NULL;
st_generator *gen = NULL;
DdNode *key, *value;
table = st_init_table( st_ptrcmp, st_ptrhash );
if ( table == NULL )
goto failure;
res = extraTransferPermuteRecurTime( ddS, ddD, f, table, Permute, TimeOut );
if ( res != NULL )
cuddRef( res );
/* Dereference all elements in the table and dispose of the table.
** This must be done also if res is NULL to avoid leaks in case of
** reordering. */
gen = st_init_gen( table );
if ( gen == NULL )
goto failure;
while ( st_gen( gen, ( const char ** ) &key, ( char ** ) &value ) )
{
Cudd_RecursiveDeref( ddD, value );
}
st_free_gen( gen );
gen = NULL;
st_free_table( table );
table = NULL;
if ( res != NULL )
cuddDeref( res );
return ( res );
failure:
if ( table != NULL )
st_free_table( table );
if ( gen != NULL )
st_free_gen( gen );
return ( NULL );
} /* end of extraTransferPermuteTime */
开发者ID:kyotobay,项目名称:ABC_withFD_check,代码行数:54,代码来源:extraBddTime.c
示例17: cuddBddTransfer
/**Function********************************************************************
Synopsis [Convert a BDD from a manager to another one.]
Description [Convert a BDD from a manager to another one. Returns a
pointer to the BDD in the destination manager if successful; NULL
otherwise.]
SideEffects [None]
SeeAlso [Cudd_bddTransfer]
******************************************************************************/
DdNode *
cuddBddTransfer(
DdManager * ddS,
DdManager * ddD,
DdNode * f)
{
DdNode *res;
st_table *table = NULL;
st_generator *gen = NULL;
DdNode *key, *value;
/* NuSMV: begin add */
abort(); /* NOT USED BY NUSMV */
/* NuSMV: begin end */
table = st_init_table(st_ptrcmp,st_ptrhash);
if (table == NULL) goto failure;
res = cuddBddTransferRecur(ddS, ddD, f, table);
if (res != NULL) cuddRef(res);
/* Dereference all elements in the table and dispose of the table.
** This must be done also if res is NULL to avoid leaks in case of
** reordering. */
gen = st_init_gen(table);
if (gen == NULL) goto failure;
while (st_gen(gen, &key, &value)) {
Cudd_RecursiveDeref(ddD, value);
}
st_free_gen(gen); gen = NULL;
st_free_table(table); table = NULL;
if (res != NULL) cuddDeref(res);
return(res);
failure:
if (table != NULL) st_free_table(table);
if (gen != NULL) st_free_gen(gen);
return(NULL);
} /* end of cuddBddTransfer */
开发者ID:ancailliau,项目名称:pynusmv,代码行数:53,代码来源:cuddBridge.c
示例18: Cudd_CProjection
/**Function********************************************************************
Synopsis [Computes the compatible projection of R w.r.t. cube Y.]
Description [Computes the compatible projection of relation R with
respect to cube Y. Returns a pointer to the c-projection if
successful; NULL otherwise. For a comparison between Cudd_CProjection
and Cudd_PrioritySelect, see the documentation of the latter.]
SideEffects [None]
SeeAlso [Cudd_PrioritySelect]
******************************************************************************/
DdNode *
Cudd_CProjection(
DdManager * dd,
DdNode * R,
DdNode * Y)
{
DdNode *res;
DdNode *support;
if (cuddCheckCube(dd,Y) == 0) {
(void) fprintf(dd->err,
"Error: The third argument of Cudd_CProjection should be a cube\n");
dd->errorCode = CUDD_INVALID_ARG;
return(NULL);
}
/* Compute the support of Y, which is used by the abstraction step
** in cuddCProjectionRecur.
*/
support = Cudd_Support(dd,Y);
if (support == NULL) return(NULL);
cuddRef(support);
do {
dd->reordered = 0;
res = cuddCProjectionRecur(dd,R,Y,support);
} while (dd->reordered == 1);
if (res == NULL) {
Cudd_RecursiveDeref(dd,support);
return(NULL);
}
cuddRef(res);
Cudd_RecursiveDeref(dd,support);
cuddDeref(res);
return(res);
} /* end of Cudd_CProjection */
开发者ID:saidalfaraby,项目名称:DTP4TC,代码行数:53,代码来源:cuddPriority.c
示例19: Cudd_addGeneralVectorCompose
/**Function********************************************************************
Synopsis [Composes an ADD with a vector of ADDs.]
Description [Given a vector of ADDs, creates a new ADD by substituting the
ADDs for the variables of the ADD f. vectorOn contains ADDs to be substituted
for the x_v and vectorOff the ADDs to be substituted for x_v'. There should
be an entry in vector for each variable in the manager. If no substitution
is sought for a given variable, the corresponding projection function should
be specified in the vector. This function implements simultaneous
composition. Returns a pointer to the resulting ADD if successful; NULL
otherwise.]
SideEffects [None]
SeeAlso [Cudd_addVectorCompose Cudd_addNonSimCompose Cudd_addPermute
Cudd_addCompose Cudd_bddVectorCompose]
******************************************************************************/
DdNode *
Cudd_addGeneralVectorCompose(
DdManager * dd,
DdNode * f,
DdNode ** vectorOn,
DdNode ** vectorOff)
{
DdHashTable *table;
DdNode *res;
int deepest;
int i;
do {
dd->reordered = 0;
/* Initialize local cache. */
table = cuddHashTableInit(dd,1,2);
if (table == NULL) return(NULL);
/* Find deepest real substitution. */
for (deepest = dd->size - 1; deepest >= 0; deepest--) {
i = dd->invperm[deepest];
if (!ddIsIthAddVarPair(dd,vectorOn[i],vectorOff[i],i)) {
break;
}
}
/* Recursively solve the problem. */
res = cuddAddGeneralVectorComposeRecur(dd,table,f,vectorOn,
vectorOff,deepest);
if (res != NULL) cuddRef(res);
/* Dispose of local cache. */
cuddHashTableQuit(table);
} while (dd->reordered == 1);
if (res != NULL) cuddDeref(res);
return(res);
} /* end of Cudd_addGeneralVectorCompose */
开发者ID:lucadealfaro,项目名称:ticc,代码行数:58,代码来源:cuddCompose.c
示例20: cuddZddChange
/**Function********************************************************************
Synopsis [Substitutes a variable with its complement in a ZDD.]
Description [Substitutes a variable with its complement in a ZDD.
returns a pointer to the result if successful; NULL
otherwise. cuddZddChange performs the same function as
Cudd_zddChange, but does not restart if reordering has taken
place. Therefore it can be called from within a recursive
procedure.]
SideEffects [None]
SeeAlso [Cudd_zddChange]
******************************************************************************/
DdNode *
cuddZddChange(
DdManager * dd,
DdNode * P,
int var)
{
DdNode *zvar, *res;
zvar = cuddUniqueInterZdd(dd, var, DD_ONE(dd), DD_ZERO(dd));
if (zvar == NULL) return(NULL);
cuddRef(zvar);
res = cuddZddChangeAux(dd, P, zvar);
if (res == NULL) {
Cudd_RecursiveDerefZdd(dd,zvar);
return(NULL);
}
cuddRef(res);
Cudd_RecursiveDerefZdd(dd,zvar);
cuddDeref(res);
return(res);
} /* end of cuddZddChange */
开发者ID:lucadealfaro,项目名称:ticc,代码行数:39,代码来源:cuddZddSetop.c
注:本文中的cuddDeref函数示例由纯净天空整理自Github/MSDocs等源码及文档管理平台,相关代码片段筛选自各路编程大神贡献的开源项目,源码版权归原作者所有,传播和使用请参考对应项目的License;未经允许,请勿转载。 |
请发表评论