diff --git a/resources/3rdparty/cudd-3.0.0/cplusplus/cuddObj.cc b/resources/3rdparty/cudd-3.0.0/cplusplus/cuddObj.cc index 1666f3970..570d907b8 100644 --- a/resources/3rdparty/cudd-3.0.0/cplusplus/cuddObj.cc +++ b/resources/3rdparty/cudd-3.0.0/cplusplus/cuddObj.cc @@ -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); diff --git a/resources/3rdparty/cudd-3.0.0/cudd/cudd.h b/resources/3rdparty/cudd-3.0.0/cudd/cudd.h index 711f59bc9..d0abcb7f0 100644 --- a/resources/3rdparty/cudd-3.0.0/cudd/cudd.h +++ b/resources/3rdparty/cudd-3.0.0/cudd/cudd.h @@ -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); diff --git a/resources/3rdparty/cudd-3.0.0/cudd/cuddAddApply.c b/resources/3rdparty/cudd-3.0.0/cudd/cuddAddApply.c index 53b259db6..00c08089a 100644 --- a/resources/3rdparty/cudd-3.0.0/cudd/cuddAddApply.c +++ b/resources/3rdparty/cudd-3.0.0/cudd/cuddAddApply.c @@ -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. diff --git a/resources/3rdparty/cudd-3.0.0/cudd/cuddInt.h b/resources/3rdparty/cudd-3.0.0/cudd/cuddInt.h index 2b51b2f80..4ba5fef03 100644 --- a/resources/3rdparty/cudd-3.0.0/cudd/cuddInt.h +++ b/resources/3rdparty/cudd-3.0.0/cudd/cuddInt.h @@ -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); diff --git a/src/storage/dd/Add.cpp b/src/storage/dd/Add.cpp index 0c65233b1..ce93b7090 100644 --- a/src/storage/dd/Add.cpp +++ b/src/storage/dd/Add.cpp @@ -93,7 +93,6 @@ namespace storm { template Bdd Add::notEquals(Add const& other) const { return Bdd(this->getDdManager(), internalAdd.notEquals(other), Dd::joinMetaVariables(*this, other)); - } template @@ -104,7 +103,6 @@ namespace storm { template Bdd Add::lessOrEqual(Add const& other) const { return Bdd(this->getDdManager(), internalAdd.lessOrEqual(other), Dd::joinMetaVariables(*this, other)); - } template