sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

created separate version of Cudd_addToBddApply to deal with negated edges in resulting BDDs 

Former-commit-id: 8141cbddc2
tempestpy_adaptions
dehnert 8 years ago
parent
e234678668
commit
5fcc2e9e7e
5 changed files with 135 additions and 7 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 10
      resources/3rdparty/cudd-3.0.0/cplusplus/cuddObj.cc
  2. 1
      resources/3rdparty/cudd-3.0.0/cudd/cudd.h
  3. 128
      resources/3rdparty/cudd-3.0.0/cudd/cuddAddApply.c
  4. 1
      resources/3rdparty/cudd-3.0.0/cudd/cuddInt.h
  5. 2
      src/storage/dd/Add.cpp

10
resources/3rdparty/cudd-3.0.0/cplusplus/cuddObj.cc
View File

@ -3158,7 +3158,7 @@ BDD
ADD::EqualsBdd(const ADD& g) const
{
DdManager *mgr = checkSameManager(g);
DdNode *result = Cudd_addApply(mgr, Cudd_addToBddEquals, node, g.node);
DdNode *result = Cudd_addToBddApply(mgr, Cudd_addToBddEquals, node, g.node);
checkReturnValue(result);
return BDD(p, result);
@ -3168,7 +3168,7 @@ BDD
ADD::NotEqualsBdd(const ADD& g) const
{
DdManager *mgr = checkSameManager(g);
DdNode *result = Cudd_addApply(mgr, Cudd_addToBddNotEquals, node, g.node);
DdNode *result = Cudd_addToBddApply(mgr, Cudd_addToBddNotEquals, node, g.node);
checkReturnValue(result);
return BDD(p, result);
@ -3178,7 +3178,7 @@ BDD
ADD::LessThanBdd(const ADD& g) const
{
DdManager *mgr = checkSameManager(g);
DdNode *result = Cudd_addApply(mgr, Cudd_addToBddLessThan, node, g.node);
DdNode *result = Cudd_addToBddApply(mgr, Cudd_addToBddLessThan, node, g.node);
checkReturnValue(result);
return BDD(p, result);
@ -3188,7 +3188,7 @@ BDD
ADD::LessThanOrEqualBdd(const ADD& g) const
{
DdManager *mgr = checkSameManager(g);
DdNode *result = Cudd_addApply(mgr, Cudd_addToBddLessThanEquals, node, g.node);
DdNode *result = Cudd_addToBddApply(mgr, Cudd_addToBddLessThanEquals, node, g.node);
checkReturnValue(result);
return BDD(p, result);
@ -3198,7 +3198,7 @@ BDD
ADD::GreaterThanBdd(const ADD& g) const
{
DdManager *mgr = checkSameManager(g);
DdNode *result = Cudd_addApply(mgr, Cudd_addToBddGreaterThan, node, g.node);
DdNode *result = Cudd_addToBddApply(mgr, Cudd_addToBddGreaterThan, node, g.node);
checkReturnValue(result);
return BDD(p, result);

1
resources/3rdparty/cudd-3.0.0/cudd/cudd.h
View File

@ -671,6 +671,7 @@ extern DdNode * Cudd_addMaxAbstract(DdManager * manager, DdNode * f, DdNode * cu
extern DdNode * Cudd_addMinAbstractRepresentative(DdManager * manager, DdNode * f, DdNode * cube);
extern DdNode * Cudd_addMaxAbstractRepresentative(DdManager * manager, DdNode * f, DdNode * cube);
extern DdNode * Cudd_addApply(DdManager *dd, DD_AOP op, DdNode *f, DdNode *g);
extern DdNode * Cudd_addToBddApply(DdManager *dd, DD_AOP op, DdNode *f, DdNode *g);
extern DdNode * Cudd_addPlus(DdManager *dd, DdNode **f, DdNode **g);
extern DdNode * Cudd_addTimes(DdManager *dd, DdNode **f, DdNode **g);
extern DdNode * Cudd_addThreshold(DdManager *dd, DdNode **f, DdNode **g);

128
resources/3rdparty/cudd-3.0.0/cudd/cuddAddApply.c
View File

@ -117,6 +117,41 @@ Cudd_addApply(
} /* end of Cudd_addApply */
/**
@brief Applies op to the corresponding discriminants of f and g and produces a BDD as a result.
@return a pointer to the result if succssful; NULL otherwise.
@sideeffect None
@see Cudd_addMonadicApply Cudd_addPlus Cudd_addTimes
Cudd_addThreshold Cudd_addSetNZ Cudd_addDivide Cudd_addMinus Cudd_addMinimum
Cudd_addMaximum Cudd_addOneZeroMaximum Cudd_addDiff Cudd_addAgreement
Cudd_addOr Cudd_addNand Cudd_addNor Cudd_addXor Cudd_addXnor
added 23/08/2016 by Christian Dehnert
*/
DdNode *
Cudd_addToBddApply(
DdManager * dd /**< manager */,
DD_AOP op /**< operator */,
DdNode * f /**< first operand */,
DdNode * g /**< second operand */)
{
DdNode *res;
do {
dd->reordered = 0;
res = cuddAddToBddApplyRecur(dd,op,f,g);
} while (dd->reordered == 1);
if (dd->errorCode == CUDD_TIMEOUT_EXPIRED && dd->timeoutHandler) {
dd->timeoutHandler(dd, dd->tohArg);
}
return(res);
} /* end of Cudd_addToBddApply */
/**
@brief Integer and floating point addition.
@ -1361,6 +1396,99 @@ cuddAddApplyRecur(
} /* end of cuddAddApplyRecur */
/**
@brief Performs the recursive step of Cudd_addToBddApply.
@return a pointer to the result if successful; NULL otherwise.
@sideeffect None
@see cuddAddMonadicApplyRecur
added 23/08/2016 by Christian Dehnert
*/
DdNode *
cuddAddToBddApplyRecur(
DdManager * dd,
DD_AOP op,
DdNode * f,
DdNode * g)
{
DdNode *res,
*fv, *fvn, *gv, *gvn,
*T, *E;
int ford, gord;
unsigned int index;
DD_CTFP cacheOp;
/* Check terminal cases. Op may swap f and g to increase the
* cache hit rate.
*/
statLine(dd);
res = (*op)(dd,&f,&g);
if (res != NULL) return(res);
/* Check cache. */
cacheOp = (DD_CTFP) op;
res = cuddCacheLookup2(dd,cacheOp,f,g);
if (res != NULL) return(res);
checkWhetherToGiveUp(dd);
/* Recursive step. */
ford = cuddI(dd,f->index);
gord = cuddI(dd,g->index);
if (ford <= gord) {
index = f->index;
fv = cuddT(f);
fvn = cuddE(f);
} else {
index = g->index;
fv = fvn = f;
}
if (gord <= ford) {
gv = cuddT(g);
gvn = cuddE(g);
} else {
gv = gvn = g;
}
T = cuddAddApplyRecur(dd,op,fv,gv);
if (T == NULL) return(NULL);
cuddRef(T);
E = cuddAddApplyRecur(dd,op,fvn,gvn);
if (E == NULL) {
Cudd_IterDerefBdd(dd,T);
return(NULL);
}
cuddRef(E);
int complT = Cudd_IsComplement(T);
if (T == E) {
res = T;
} else {
res = cuddUniqueInter(dd,(int)index,Cudd_Regular(T),complT ? Cudd_Not(E) : E);
if (complT) {
res = Cudd_Not(res);
}
}
if (res == NULL) {
Cudd_IterDerefBdd(dd, T);
Cudd_IterDerefBdd(dd, E);
return(NULL);
}
cuddDeref(T);
cuddDeref(E);
/* Store result. */
cuddCacheInsert2(dd,cacheOp,f,g,res);
return(res);
} /* end of cuddAddToBddApplyRecur */
/**
@brief Performs the recursive step of Cudd_addMonadicApply.

1
resources/3rdparty/cudd-3.0.0/cudd/cuddInt.h
View File

@ -1066,6 +1066,7 @@ extern DdNode * cuddAddMaxAbstractRecur (DdManager *manager, DdNode *f, DdNode *
extern DdNode * cuddAddMinAbstractRepresentativeRecur(DdManager * manager, DdNode * f, DdNode * cube);
extern DdNode * cuddAddMaxAbstractRepresentativeRecur(DdManager * manager, DdNode * f, DdNode * cube);
extern DdNode * cuddAddApplyRecur(DdManager *dd, DdNode * (*)(DdManager *, DdNode **, DdNode **), DdNode *f, DdNode *g);
extern DdNode * cuddAddToBddApplyRecur(DdManager *dd, DdNode * (*)(DdManager *, DdNode **, DdNode **), DdNode *f, DdNode *g);
extern DdNode * cuddAddMonadicApplyRecur(DdManager * dd, DdNode * (*op)(DdManager *, DdNode *), DdNode * f);
extern DdNode * cuddAddScalarInverseRecur(DdManager *dd, DdNode *f, DdNode *epsilon);
extern DdNode * cuddAddIteRecur(DdManager *dd, DdNode *f, DdNode *g, DdNode *h);

2
src/storage/dd/Add.cpp
View File

@ -93,7 +93,6 @@ namespace storm {
template<DdType LibraryType, typename ValueType>
Bdd<LibraryType> Add<LibraryType, ValueType>::notEquals(Add<LibraryType, ValueType> const& other) const {
return Bdd<LibraryType>(this->getDdManager(), internalAdd.notEquals(other), Dd<LibraryType>::joinMetaVariables(*this, other));
}
template<DdType LibraryType, typename ValueType>
@ -104,7 +103,6 @@ namespace storm {
template<DdType LibraryType, typename ValueType>
Bdd<LibraryType> Add<LibraryType, ValueType>::lessOrEqual(Add<LibraryType, ValueType> const& other) const {
return Bdd<LibraryType>(this->getDdManager(), internalAdd.lessOrEqual(other), Dd<LibraryType>::joinMetaVariables(*this, other));
}
template<DdType LibraryType, typename ValueType>

Write Preview
Loading…
Cancel
Save