From b8f08c41c73e98f0569eac40a87421538e918079 Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 15 Apr 2016 15:20:20 +0200 Subject: [PATCH] adapted the custom dd operations to work again Former-commit-id: 9a38e8d56408858c38e4a0efcedbcf782f0bdefc --- .../3rdparty/cudd-3.0.0/cplusplus/cuddObj.cc | 14 +------------- resources/3rdparty/cudd-3.0.0/cudd/cudd.h | 1 + resources/3rdparty/cudd-3.0.0/cudd/cuddAPI.c | 15 ++++++++++++++- src/storage/dd/cudd/InternalCuddBdd.cpp | 18 +++++++++--------- 4 files changed, 25 insertions(+), 23 deletions(-) diff --git a/resources/3rdparty/cudd-3.0.0/cplusplus/cuddObj.cc b/resources/3rdparty/cudd-3.0.0/cplusplus/cuddObj.cc index 2f91c20a7..d59080a7d 100644 --- a/resources/3rdparty/cudd-3.0.0/cplusplus/cuddObj.cc +++ b/resources/3rdparty/cudd-3.0.0/cplusplus/cuddObj.cc @@ -3504,25 +3504,13 @@ BDD::ExistAbstract( } // BDD::ExistAbstract BDD -ExistAbstractRepresentative(const BDD& cube) const { +BDD::ExistAbstractRepresentative(const BDD& cube) const { DdManager *mgr = checkSameManager(cube); DdNode *result; result = Cudd_bddExistAbstractRepresentative(mgr, node, cube.node); checkReturnValue(result); return BDD(p, result); } // BDD::ExistAbstractRepresentative - -BDD -BDD::ExistAbstractRepresentative( - const BDD& cube) const -{ - DdManager *mgr = checkSameManager(cube); - DdNode *result; - result = Cudd_bddExistAbstractRepresentative(mgr, node, cube.node); - checkReturnValue(result); - return BDD(p, result); - -} // BDD::ExistAbstractRepresentative BDD BDD::XorExistAbstract( diff --git a/resources/3rdparty/cudd-3.0.0/cudd/cudd.h b/resources/3rdparty/cudd-3.0.0/cudd/cudd.h index 5180b0d5c..e7bdbf0c1 100644 --- a/resources/3rdparty/cudd-3.0.0/cudd/cudd.h +++ b/resources/3rdparty/cudd-3.0.0/cudd/cudd.h @@ -515,6 +515,7 @@ extern int Cudd_zddVarsFromBddVars(DdManager *dd, int multiplicity); extern unsigned int Cudd_ReadMaxIndex(void); extern DdNode * Cudd_addConst(DdManager *dd, CUDD_VALUE_TYPE c); extern int Cudd_IsConstant(DdNode *node); +extern int Cudd_IsConstant_const(DdNode const *node); extern int Cudd_IsNonConstant(DdNode *f); extern DdNode * Cudd_T(DdNode *node); extern DdNode * Cudd_E(DdNode *node); diff --git a/resources/3rdparty/cudd-3.0.0/cudd/cuddAPI.c b/resources/3rdparty/cudd-3.0.0/cudd/cuddAPI.c index 78214567e..45cbc714a 100644 --- a/resources/3rdparty/cudd-3.0.0/cudd/cuddAPI.c +++ b/resources/3rdparty/cudd-3.0.0/cudd/cuddAPI.c @@ -553,6 +553,20 @@ int Cudd_IsConstant(DdNode *node) } /* end of Cudd_IsConstant */ +/** + @brief Returns 1 if the node is a constant node. + + @details A constant node is not an internal node. The pointer + passed to Cudd_IsConstant may be either regular or complemented. + + @sideeffect none + + */ +int Cudd_IsConstant_const(DdNode const*node) +{ + return Cudd_Regular(node)->index == CUDD_CONST_INDEX; + +} /* end of Cudd_IsConstant_const */ /** @brief Returns 1 if a %DD node is not constant. @@ -576,7 +590,6 @@ Cudd_IsNonConstant( } /* end of Cudd_IsNonConstant */ - /** @brief Returns the then child of an internal node. diff --git a/src/storage/dd/cudd/InternalCuddBdd.cpp b/src/storage/dd/cudd/InternalCuddBdd.cpp index 2c0daf7da..88a22bec2 100644 --- a/src/storage/dd/cudd/InternalCuddBdd.cpp +++ b/src/storage/dd/cudd/InternalCuddBdd.cpp @@ -448,7 +448,7 @@ namespace storm { auto nodeCounterIt = nodeToCounterMap.find(dd); if (nodeCounterIt != nodeToCounterMap.end()) { // If we have found the node, this means we can look up the counter-index pair and get the corresponding variable. - auto variableIt = countIndexToVariablePair.find(std::make_pair(nodeCounterIt->second, dd->index)); + auto variableIt = countIndexToVariablePair.find(std::make_pair(nodeCounterIt->second, Cudd_NodeReadIndex(dd))); STORM_LOG_ASSERT(variableIt != countIndexToVariablePair.end(), "Unable to find node."); return variableIt->second; } @@ -458,15 +458,15 @@ namespace storm { storm::expressions::Variable newVariable = manager.declareFreshBooleanVariable(); // Since we want to reuse the variable whenever possible, we insert the appropriate entries in the hash table. - if (!Cudd_IsConstant(dd)) { + if (!Cudd_IsConstant_const(dd)) { // If we are dealing with a non-terminal node, we count it as a new node with this index. - nodeToCounterMap[dd] = nextCounterForIndex[dd->index]; - countIndexToVariablePair[std::make_pair(nextCounterForIndex[dd->index], dd->index)] = newVariable; - ++nextCounterForIndex[dd->index]; + nodeToCounterMap[dd] = nextCounterForIndex[Cudd_NodeReadIndex(dd)]; + countIndexToVariablePair[std::make_pair(nextCounterForIndex[Cudd_NodeReadIndex(dd)], Cudd_NodeReadIndex(dd))] = newVariable; + ++nextCounterForIndex[Cudd_NodeReadIndex(dd)]; } else { // If it's a terminal node, it is the one leaf and there's no need to keep track of a counter for this level. nodeToCounterMap[dd] = 0; - countIndexToVariablePair[std::make_pair(0, dd->index)] = newVariable; + countIndexToVariablePair[std::make_pair(0, Cudd_NodeReadIndex(dd))] = newVariable; } // In the terminal case, we can only have a one since we are considering non-negated nodes only. @@ -475,15 +475,15 @@ namespace storm { expressions.push_back(storm::expressions::implies(manager.boolean(true), newVariable)); } else { // In the non-terminal case, we recursively translate the children nodes and then construct and appropriate ite-expression. - DdNode const* t = Cudd_T(dd); - DdNode const* e = Cudd_E(dd); + DdNode const* t = Cudd_T_const(dd); + DdNode const* e = Cudd_E_const(dd); DdNode const* T = Cudd_Regular(t); DdNode const* E = Cudd_Regular(e); storm::expressions::Variable thenVariable = toExpressionRec(T, manager, expressions, countIndexToVariablePair, nodeToCounterMap, nextCounterForIndex, indexToExpressionMap); storm::expressions::Variable elseVariable = toExpressionRec(E, manager, expressions, countIndexToVariablePair, nodeToCounterMap, nextCounterForIndex, indexToExpressionMap); // Create the appropriate expression. - auto expressionIt = indexToExpressionMap.find(dd->index); + auto expressionIt = indexToExpressionMap.find(Cudd_NodeReadIndex(dd)); STORM_LOG_ASSERT(expressionIt != indexToExpressionMap.end(), "Unable to find expression for variable index."); expressions.push_back(storm::expressions::iff(newVariable, storm::expressions::ite(expressionIt->second, t == T ? thenVariable : !thenVariable, e == E ? elseVariable : !elseVariable))); }