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

added cudd functions for equal/less/less_equal/greater/greater_equal that directly return a BDD instead of an ADD 

Former-commit-id: 448b5e2f7c
main
dehnert 9 years ago
parent
cc550984b3
commit
24667fffc4
6 changed files with 266 additions and 25 deletions
Split View
  1. 60
      resources/3rdparty/cudd-3.0.0/cplusplus/cuddObj.cc
  2. 6
      resources/3rdparty/cudd-3.0.0/cplusplus/cuddObj.hh
  3. 187
      resources/3rdparty/cudd-3.0.0/cudd/cuddAddApply.c
  4. 24
      resources/3rdparty/cudd-3.0.0/cudd/cuddBddAbs.c
  5. 2
      src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp
  6. 12
      src/storage/dd/cudd/InternalCuddAdd.cpp

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

@ -3154,6 +3154,66 @@ ADD::GreaterThanOrEqual(const ADD& g) const
} // ADD::GreaterThanOrEqual
ADD
ADD::EqualsBdd(const ADD& g) const
{
DdManager *mgr = checkSameManager(g);
DdNode *result = Cudd_addApply(mgr, Cudd_addToBddEquals, node, g.node);
checkReturnValue(result);
return ADD(p, result);
} // ADD::EqualsBdd
ADD
ADD::NotEqualsBdd(const ADD& g) const
{
DdManager *mgr = checkSameManager(g);
DdNode *result = Cudd_addApply(mgr, Cudd_addToBddNotEquals, node, g.node);
checkReturnValue(result);
return ADD(p, result);
} // ADD::NotEqualsBdd
ADD
ADD::LessThanBdd(const ADD& g) const
{
DdManager *mgr = checkSameManager(g);
DdNode *result = Cudd_addApply(mgr, Cudd_addToBddLessThan, node, g.node);
checkReturnValue(result);
return ADD(p, result);
} // ADD::LessThanBdd
ADD
ADD::LessThanOrEqualBdd(const ADD& g) const
{
DdManager *mgr = checkSameManager(g);
DdNode *result = Cudd_addApply(mgr, Cudd_addToBddLessThanEquals, node, g.node);
checkReturnValue(result);
return ADD(p, result);
} // ADD::LessThanOrEqualBdd
ADD
ADD::GreaterThanBdd(const ADD& g) const
{
DdManager *mgr = checkSameManager(g);
DdNode *result = Cudd_addApply(mgr, Cudd_addToBddGreaterThan, node, g.node);
checkReturnValue(result);
return ADD(p, result);
} // ADD::GreaterThanBdd
ADD
ADD::GreaterThanOrEqualBdd(const ADD& g) const
{
DdManager *mgr = checkSameManager(g);
DdNode *result = Cudd_addApply(mgr, Cudd_addToBddGreaterThanEquals, node, g.node);
checkReturnValue(result);
return ADD(p, result);
} // ADD::GreaterThanOrEqualBdd
BDD
BDD::AndAbstract(
const BDD& g,

6
resources/3rdparty/cudd-3.0.0/cplusplus/cuddObj.hh
View File

@ -376,6 +376,12 @@ public:
ADD LessThanOrEqual(const ADD& g) const;
ADD GreaterThan(const ADD& g) const;
ADD GreaterThanOrEqual(const ADD& g) const;
BDD EqualsBdd(const ADD& g) const;
BDD NotEqualsBdd(const ADD& g) const;
BDD LessThanBdd(const ADD& g) const;
BDD LessThanOrEqualBdd(const ADD& g) const;
BDD GreaterThanBdd(const ADD& g) const;
BDD GreaterThanOrEqualBdd(const ADD& g) const;
BDD BddThreshold(CUDD_VALUE_TYPE value) const;
BDD BddStrictThreshold(CUDD_VALUE_TYPE value) const;
BDD BddInterval(CUDD_VALUE_TYPE lower, CUDD_VALUE_TYPE upper) const;

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

@ -817,6 +817,38 @@ Cudd_addEquals(
} /* end of Cudd_addEquals */
/**Function********************************************************************
Synopsis [1 if f==g; 0 otherwise.]
Description [Returns NULL if not a terminal case; f op g otherwise,
where f op g is 1 if f==g; 0 otherwise.]
SideEffects [None]
SeeAlso [Cudd_addApply]
Added 23/08/2016 by Christian Dehnert
******************************************************************************/
DdNode *
Cudd_addToBddEquals(
DdManager * dd,
DdNode ** f,
DdNode ** g)
{
DdNode *F, *G;
F = *f; G = *g;
if (F == G) return(DD_ONE(dd));
if (cuddIsConstant(F) && cuddIsConstant(G)) return(Cudd_Not(DD_ONE(dd)));
if (F > G) { /* swap f and g */
*f = G;
*g = F;
}
return(NULL);
} /* end of Cudd_addToBddEquals */
/**Function********************************************************************
@ -849,6 +881,39 @@ Cudd_addNotEquals(
} /* end of Cudd_addNotEquals */
/**Function********************************************************************
Synopsis [1 if f!=g; 0 otherwise.]
Description [Returns NULL if not a terminal case; f op g otherwise,
where f op g is 1 if f!=g; 0 otherwise.]
SideEffects [None]
SeeAlso [Cudd_addApply]
Added 23/08/2016 by Christian Dehnert
******************************************************************************/
DdNode *
Cudd_addToBddNotEquals(
DdManager * dd,
DdNode ** f,
DdNode ** g)
{
DdNode *F, *G;
F = *f; G = *g;
if (F == G) return(Cudd_Not(DD_ONE(dd)));
if (cuddIsConstant(F) && cuddIsConstant(G)) return(DD_ONE(dd));
if (F > G) { /* swap f and g */
*f = G;
*g = F;
}
return(NULL);
} /* end of Cudd_addToBddNotEquals */
/**Function********************************************************************
Synopsis [1 if f>g; 0 otherwise.]
@ -878,6 +943,37 @@ Cudd_addGreaterThan(
} /* end of Cudd_addGreaterThan */
/**Function********************************************************************
Synopsis [1 if f>g; 0 otherwise.]
Description [Returns NULL if not a terminal case; f op g otherwise,
where f op g is 1 if f>g; 0 otherwise.]
SideEffects [None]
SeeAlso [Cudd_addApply]
Added 23/08/2016 by Christian Dehnert
******************************************************************************/
DdNode *
Cudd_addToBddGreaterThan(
DdManager * dd,
DdNode ** f,
DdNode ** g)
{
DdNode *F, *G;
F = *f; G = *g;
if (F == G) return(Cudd_Not(DD_ONE(dd)));
if (cuddIsConstant(F) && cuddIsConstant(G)) {
if (cuddV(F)>cuddV(G)) return (DD_ONE(dd)); else return (Cudd_Not(DD_ONE(dd)));
}
return(NULL);
} /* end of Cudd_addToBddGreaterThan */
/**Function********************************************************************
@ -908,6 +1004,36 @@ Cudd_addGreaterThanEquals(
} /* end of Cudd_addGreaterThanEquals */
/**Function********************************************************************
Synopsis [1 if f>=g; 0 otherwise.]
Description [Returns NULL if not a terminal case; f op g otherwise,
where f op g is 1 if f>=g; 0 otherwise.]
SideEffects [None]
SeeAlso [Cudd_addApply]
Added 23/08/2016 by Christian Dehnert
******************************************************************************/
DdNode *
Cudd_addToBddGreaterThanEquals(
DdManager * dd,
DdNode ** f,
DdNode ** g)
{
DdNode *F, *G;
F = *f; G = *g;
if (F == G) return(DD_ONE(dd));
if (cuddIsConstant(F) && cuddIsConstant(G)) {
if (cuddV(F)>=cuddV(G)) return (DD_ONE(dd)); else return (Cudd_Not(DD_ONE(dd)));
}
return(NULL);
} /* end of Cudd_addToBddGreaterThanEquals */
/**Function********************************************************************
@ -938,6 +1064,36 @@ Cudd_addLessThan(
} /* end of Cudd_addLessThan */
/**Function********************************************************************
Synopsis [1 if f<g; 0 otherwise.]
Description [Returns NULL if not a terminal case; f op g otherwise,
where f op g is 1 if f<g; 0 otherwise.]
SideEffects [None]
SeeAlso [Cudd_addApply]
Added 23/08/2016 by Christian Dehnert
******************************************************************************/
DdNode *
Cudd_addToBddLessThan(
DdManager * dd,
DdNode ** f,
DdNode ** g)
{
DdNode *F, *G;
F = *f; G = *g;
if (F == G) return(Cudd_Not(DD_ONE(dd)));
if (cuddIsConstant(F) && cuddIsConstant(G)) {
if (cuddV(F)<cuddV(G)) return (DD_ONE(dd)); else return (Cudd_Not(DD_ONE(dd)));
}
return(NULL);
} /* end of Cudd_addToBddLessThan */
/**Function********************************************************************
@ -968,6 +1124,37 @@ Cudd_addLessThanEquals(
} /* end of Cudd_addLessThanEquals */
/**Function********************************************************************
Synopsis [1 if f<=g; 0 otherwise.]
Description [Returns NULL if not a terminal case; f op g otherwise,
where f op g is 1 if f<=g; 0 otherwise.]
SideEffects [None]
SeeAlso [Cudd_addApply]
Added 23/08/2016 by Christian Dehnert
******************************************************************************/
DdNode *
Cudd_addToBddLessThanEquals(
DdManager * dd,
DdNode ** f,
DdNode ** g)
{
DdNode *F, *G;
F = *f; G = *g;
if (F == G) return(DD_ONE(dd));
if (cuddIsConstant(F) && cuddIsConstant(G)) {
if (cuddV(F)<=cuddV(G)) return (DD_ONE(dd)); else return (Cudd_Not(DD_ONE(dd)));
}
return(NULL);
} /* end of Cudd_addToBddLessThanEquals */
/**Function********************************************************************
Synopsis [f to the power of g.]

24
resources/3rdparty/cudd-3.0.0/cudd/cuddBddAbs.c
View File

@ -521,7 +521,6 @@ cuddBddExistAbstractRepresentativeRecur(
DdNode * f,
DdNode * cube)
{
// printf("entering exists abstract...\n");
DdNode *F, *T, *E, *res, *res1, *res2, *one, *zero, *left, *right, *tmp, *res1Inf, *res2Inf;
statLine(manager);
@ -535,12 +534,10 @@ cuddBddExistAbstractRepresentativeRecur(
/* Cube is guaranteed to be a cube at this point. */
if (F == one) {
if (fIsNegated) {
// printf("return in preprocessing...\n");
return f;
}
if (cube == one) {
// printf("return in preprocessing...\n");
return one;
} else {
res = cuddBddExistAbstractRepresentativeRecur(manager, f, cuddT(cube));
@ -549,7 +546,7 @@ cuddBddExistAbstractRepresentativeRecur(
}
cuddRef(res);
res1 = cuddBddIteRecur(manager, manager->vars[cube->index], zero, res);
res1 = cuddUniqueInter(manager, (int) cube->index, zero, res);
if (res1 == NULL) {
Cudd_IterDerefBdd(manager,res);
Cudd_IterDerefBdd(manager,zero);
@ -559,12 +556,10 @@ cuddBddExistAbstractRepresentativeRecur(
return(res1);
}
} else if (cube == one) {
// printf("return in preprocessing...\n");
return f;
}
/* From now on, cube and f are non-constant. */
// printf("F perm %i and cube perm %i\n", manager->perm[F->index], manager->perm[cube->index]);
/* Abstract a variable that does not appear in f. */
if (manager->perm[F->index] > manager->perm[cube->index]) {
@ -574,8 +569,7 @@ cuddBddExistAbstractRepresentativeRecur(
}
cuddRef(res);
// res1 = cuddUniqueInter(manager, (int) cube->index, zero, res);
res1 = cuddBddIteRecur(manager, manager->vars[cube->index], zero, res);
res1 = cuddUniqueInter(manager, (int) cube->index, zero, res);
if (res1 == NULL) {
Cudd_IterDerefBdd(manager,res);
@ -584,20 +578,17 @@ cuddBddExistAbstractRepresentativeRecur(
}
cuddDeref(res);
// printf("return after abstr. var that does not appear in f...\n");
return(res1);
}
/* Check the cache. */
if (F->ref != 1 && (res = cuddCacheLookup2(manager, Cudd_bddExistAbstractRepresentative, f, cube)) != NULL) {
// printf("return because of cache hit...\n");
return(res);
}
/* Compute the cofactors of f. */
T = cuddT(F); E = cuddE(F);
if (f != F) {
// printf("negating T and E\n");
T = Cudd_Not(T); E = Cudd_Not(E);
}
@ -655,8 +646,7 @@ cuddBddExistAbstractRepresentativeRecur(
Cudd_IterDerefBdd(manager,left);
assert(res1Inf != res2Inf);
// res = cuddUniqueInter(manager, (int) f->index, res2Inf, res1Inf);
res = cuddBddIteRecur(manager, manager->vars[F->index], res2Inf, res1Inf);
res = cuddUniqueInter(manager, (int) F->index, res2Inf, res1Inf);
if (res == NULL) {
Cudd_IterDerefBdd(manager,res1Inf);
@ -665,12 +655,11 @@ cuddBddExistAbstractRepresentativeRecur(
}
cuddRef(res);
Cudd_IterDerefBdd(manager,res1Inf);
Cudd_IterDerefBdd(manager,res2Inf);
cuddDeref(res1Inf);
cuddDeref(res2Inf);
cuddCacheInsert2(manager, Cudd_bddExistAbstractRepresentative, f, cube, res);
cuddDeref(res);
// printf("return properly computed result...\n");
return(res);
} else { /* if (cuddI(manager,F->index) < cuddI(manager,cube->index)) */
res1 = cuddBddExistAbstractRepresentativeRecur(manager, E, cube);
@ -688,7 +677,7 @@ cuddBddExistAbstractRepresentativeRecur(
/* ITE takes care of possible complementation of res1 and of the
** case in which res1 == res2. */
res = cuddBddIteRecur(manager, manager->vars[F->index], res2, res1);
res = cuddUniqueInter(manager, (int)F->index, res2, res1);
if (res == NULL) {
Cudd_IterDerefBdd(manager, res1);
Cudd_IterDerefBdd(manager, res2);
@ -699,7 +688,6 @@ cuddBddExistAbstractRepresentativeRecur(
if (F->ref != 1) {
cuddCacheInsert2(manager, Cudd_bddExistAbstractRepresentative, f, cube, res);
}
// printf("return of last case...\n");
return(res);
}

2
src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp
View File

@ -203,7 +203,7 @@ namespace storm {
}
// Likewise, if all bits are set, we can avoid the computation and set.
if ((~psiStates).empty()) {
if (psiStates.full()) {
return std::vector<ValueType>(numberOfStates, storm::utility::one<ValueType>());
}

12
src/storage/dd/cudd/InternalCuddAdd.cpp
View File

@ -73,32 +73,32 @@ namespace storm {
template<typename ValueType>
InternalBdd<DdType::CUDD> InternalAdd<DdType::CUDD, ValueType>::equals(InternalAdd<DdType::CUDD, ValueType> const& other) const {
return InternalBdd<DdType::CUDD>(ddManager, this->getCuddAdd().Equals(other.getCuddAdd()).BddPattern());
return InternalBdd<DdType::CUDD>(ddManager, this->getCuddAdd().EqualsBdd(other.getCuddAdd()));
}
template<typename ValueType>
InternalBdd<DdType::CUDD> InternalAdd<DdType::CUDD, ValueType>::notEquals(InternalAdd<DdType::CUDD, ValueType> const& other) const {
return InternalBdd<DdType::CUDD>(ddManager, this->getCuddAdd().NotEquals(other.getCuddAdd()).BddPattern());
return InternalBdd<DdType::CUDD>(ddManager, this->getCuddAdd().NotEqualsBdd(other.getCuddAdd()));
}
template<typename ValueType>
InternalBdd<DdType::CUDD> InternalAdd<DdType::CUDD, ValueType>::less(InternalAdd<DdType::CUDD, ValueType> const& other) const {
return InternalBdd<DdType::CUDD>(ddManager, this->getCuddAdd().LessThan(other.getCuddAdd()).BddPattern());
return InternalBdd<DdType::CUDD>(ddManager, this->getCuddAdd().LessThanBdd(other.getCuddAdd()));
}
template<typename ValueType>
InternalBdd<DdType::CUDD> InternalAdd<DdType::CUDD, ValueType>::lessOrEqual(InternalAdd<DdType::CUDD, ValueType> const& other) const {
return InternalBdd<DdType::CUDD>(ddManager, this->getCuddAdd().LessThanOrEqual(other.getCuddAdd()).BddPattern());
return InternalBdd<DdType::CUDD>(ddManager, this->getCuddAdd().LessThanOrEqualBdd(other.getCuddAdd()));
}
template<typename ValueType>
InternalBdd<DdType::CUDD> InternalAdd<DdType::CUDD, ValueType>::greater(InternalAdd<DdType::CUDD, ValueType> const& other) const {
return InternalBdd<DdType::CUDD>(ddManager, this->getCuddAdd().GreaterThan(other.getCuddAdd()).BddPattern());
return InternalBdd<DdType::CUDD>(ddManager, this->getCuddAdd().GreaterThanBdd(other.getCuddAdd()));
}
template<typename ValueType>
InternalBdd<DdType::CUDD> InternalAdd<DdType::CUDD, ValueType>::greaterOrEqual(InternalAdd<DdType::CUDD, ValueType> const& other) const {
return InternalBdd<DdType::CUDD>(ddManager, this->getCuddAdd().GreaterThanOrEqual(other.getCuddAdd()).BddPattern());
return InternalBdd<DdType::CUDD>(ddManager, this->getCuddAdd().GreaterThanOrEqualBdd(other.getCuddAdd()));
}
template<typename ValueType>

Write Preview
|||||||
100:0
Loading…
Cancel
Save