diff --git a/src/storm/storage/dd/cudd/InternalCuddAdd.cpp b/src/storm/storage/dd/cudd/InternalCuddAdd.cpp index 58d8b5bf3..4cf197970 100644 --- a/src/storm/storage/dd/cudd/InternalCuddAdd.cpp +++ b/src/storm/storage/dd/cudd/InternalCuddAdd.cpp @@ -386,13 +386,17 @@ namespace storm { thenOffset = 1; } - return std::make_shared(nullptr, elseOffset, nullptr, thenOffset); + auto oddNode = std::make_shared(nullptr, elseOffset, nullptr, thenOffset); + uniqueTableForLevels[currentLevel].emplace(dd, oddNode); + return oddNode; } else if (ddVariableIndices[currentLevel] < Cudd_NodeReadIndex(dd)) { // If we skipped the level in the DD, we compute the ODD just for the else-successor and use the same // node for the then-successor as well. std::shared_ptr elseNode = createOddRec(dd, manager, currentLevel + 1, maxLevel, ddVariableIndices, uniqueTableForLevels); std::shared_ptr thenNode = elseNode; - return std::make_shared(elseNode, elseNode->getElseOffset() + elseNode->getThenOffset(), thenNode, thenNode->getElseOffset() + thenNode->getThenOffset()); + auto oddNode = std::make_shared(elseNode, elseNode->getElseOffset() + elseNode->getThenOffset(), thenNode, thenNode->getElseOffset() + thenNode->getThenOffset()); + uniqueTableForLevels[currentLevel].emplace(dd, oddNode); + return oddNode; } else { // Otherwise, we compute the ODDs for both the then- and else successors. std::shared_ptr elseNode = createOddRec(Cudd_E(dd), manager, currentLevel + 1, maxLevel, ddVariableIndices, uniqueTableForLevels); @@ -401,7 +405,9 @@ namespace storm { uint_fast64_t totalElseOffset = elseNode->getElseOffset() + elseNode->getThenOffset(); uint_fast64_t totalThenOffset = thenNode->getElseOffset() + thenNode->getThenOffset(); - return std::make_shared(elseNode, totalElseOffset, thenNode, totalThenOffset); + auto oddNode = std::make_shared(elseNode, totalElseOffset, thenNode, totalThenOffset); + uniqueTableForLevels[currentLevel].emplace(dd, oddNode); + return oddNode; } } } diff --git a/src/storm/storage/dd/cudd/InternalCuddBdd.cpp b/src/storm/storage/dd/cudd/InternalCuddBdd.cpp index 5ad9b5846..8cea861b6 100644 --- a/src/storm/storage/dd/cudd/InternalCuddBdd.cpp +++ b/src/storm/storage/dd/cudd/InternalCuddBdd.cpp @@ -355,14 +355,19 @@ namespace storm { thenOffset = 1 - thenOffset; } - return std::make_shared(nullptr, elseOffset, nullptr, thenOffset); + auto oddNode = std::make_shared(nullptr, elseOffset, nullptr, thenOffset); + uniqueTableForLevels[currentLevel].emplace(std::make_pair(dd, complement), oddNode); + return oddNode; } else if (ddVariableIndices[currentLevel] < Cudd_NodeReadIndex(dd)) { // If we skipped the level in the DD, we compute the ODD just for the else-successor and use the same // node for the then-successor as well. std::shared_ptr elseNode = createOddRec(dd, manager, currentLevel + 1, complement, maxLevel, ddVariableIndices, uniqueTableForLevels); std::shared_ptr thenNode = elseNode; uint_fast64_t totalOffset = elseNode->getElseOffset() + elseNode->getThenOffset(); - return std::make_shared(elseNode, totalOffset, thenNode, totalOffset); + + auto oddNode = std::make_shared(elseNode, totalOffset, thenNode, totalOffset); + uniqueTableForLevels[currentLevel].emplace(std::make_pair(dd, complement), oddNode); + return oddNode; } else { // Otherwise, we compute the ODDs for both the then- and else successors. DdNode const* thenDdNode = Cudd_T_const(dd); @@ -375,7 +380,9 @@ namespace storm { std::shared_ptr elseNode = createOddRec(Cudd_Regular(elseDdNode), manager, currentLevel + 1, elseComplemented, maxLevel, ddVariableIndices, uniqueTableForLevels); std::shared_ptr thenNode = createOddRec(Cudd_Regular(thenDdNode), manager, currentLevel + 1, thenComplemented, maxLevel, ddVariableIndices, uniqueTableForLevels); - return std::make_shared(elseNode, elseNode->getElseOffset() + elseNode->getThenOffset(), thenNode, thenNode->getElseOffset() + thenNode->getThenOffset()); + auto oddNode = std::make_shared(elseNode, elseNode->getElseOffset() + elseNode->getThenOffset(), thenNode, thenNode->getElseOffset() + thenNode->getThenOffset()); + uniqueTableForLevels[currentLevel].emplace(std::make_pair(dd, complement), oddNode); + return oddNode; } } } diff --git a/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp b/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp index eecfe55bb..5e5043246 100644 --- a/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp +++ b/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp @@ -570,13 +570,17 @@ namespace storm { thenOffset = 1; } - return std::make_shared(nullptr, elseOffset, nullptr, thenOffset); + auto oddNode = std::make_shared(nullptr, elseOffset, nullptr, thenOffset); + uniqueTableForLevels[currentLevel].emplace(dd, oddNode); + return oddNode; } else if (mtbdd_isleaf(dd) || ddVariableIndices[currentLevel] < mtbdd_getvar(dd)) { // If we skipped the level in the DD, we compute the ODD just for the else-successor and use the same // node for the then-successor as well. std::shared_ptr elseNode = createOddRec(dd, currentLevel + 1, maxLevel, ddVariableIndices, uniqueTableForLevels); std::shared_ptr thenNode = elseNode; - return std::make_shared(elseNode, elseNode->getElseOffset() + elseNode->getThenOffset(), thenNode, thenNode->getElseOffset() + thenNode->getThenOffset()); + auto oddNode = std::make_shared(elseNode, elseNode->getElseOffset() + elseNode->getThenOffset(), thenNode, thenNode->getElseOffset() + thenNode->getThenOffset()); + uniqueTableForLevels[currentLevel].emplace(dd, oddNode); + return oddNode; } else { // Otherwise, we compute the ODDs for both the then- and else successors. std::shared_ptr elseNode = createOddRec(mtbdd_regular(mtbdd_getlow(dd)), currentLevel + 1, maxLevel, ddVariableIndices, uniqueTableForLevels); @@ -585,7 +589,9 @@ namespace storm { uint_fast64_t totalElseOffset = elseNode->getElseOffset() + elseNode->getThenOffset(); uint_fast64_t totalThenOffset = thenNode->getElseOffset() + thenNode->getThenOffset(); - return std::make_shared(elseNode, totalElseOffset, thenNode, totalThenOffset); + auto oddNode = std::make_shared(elseNode, totalElseOffset, thenNode, totalThenOffset); + uniqueTableForLevels[currentLevel].emplace(dd, oddNode); + return oddNode; } } } diff --git a/src/storm/storage/dd/sylvan/InternalSylvanBdd.cpp b/src/storm/storage/dd/sylvan/InternalSylvanBdd.cpp index e6a51eb23..7097ac999 100644 --- a/src/storm/storage/dd/sylvan/InternalSylvanBdd.cpp +++ b/src/storm/storage/dd/sylvan/InternalSylvanBdd.cpp @@ -337,14 +337,18 @@ namespace storm { thenOffset = 1 - thenOffset; } - return std::make_shared(nullptr, elseOffset, nullptr, thenOffset); + auto oddNode = std::make_shared(nullptr, elseOffset, nullptr, thenOffset); + uniqueTableForLevels[currentLevel].emplace(std::make_pair(dd, complement), oddNode); + return oddNode; } else if (bdd_isterminal(dd) || ddVariableIndices[currentLevel] < sylvan_var(dd)) { // If we skipped the level in the DD, we compute the ODD just for the else-successor and use the same // node for the then-successor as well. std::shared_ptr elseNode = createOddRec(dd, complement, currentLevel + 1, maxLevel, ddVariableIndices, uniqueTableForLevels); std::shared_ptr thenNode = elseNode; uint_fast64_t totalOffset = elseNode->getElseOffset() + elseNode->getThenOffset(); - return std::make_shared(elseNode, totalOffset, thenNode, totalOffset); + auto oddNode = std::make_shared(elseNode, totalOffset, thenNode, totalOffset); + uniqueTableForLevels[currentLevel].emplace(std::make_pair(dd, complement), oddNode); + return oddNode; } else { // Otherwise, we compute the ODDs for both the then- and else successors. BDD thenDdNode = sylvan_high(dd); @@ -357,7 +361,9 @@ namespace storm { std::shared_ptr elseNode = createOddRec(bdd_regular(elseDdNode), elseComplemented, currentLevel + 1, maxLevel, ddVariableIndices, uniqueTableForLevels); std::shared_ptr thenNode = createOddRec(bdd_regular(thenDdNode), thenComplemented, currentLevel + 1, maxLevel, ddVariableIndices, uniqueTableForLevels); - return std::make_shared(elseNode, elseNode->getElseOffset() + elseNode->getThenOffset(), thenNode, thenNode->getElseOffset() + thenNode->getThenOffset()); + auto oddNode = std::make_shared(elseNode, elseNode->getElseOffset() + elseNode->getThenOffset(), thenNode, thenNode->getElseOffset() + thenNode->getThenOffset()); + uniqueTableForLevels[currentLevel].emplace(std::make_pair(dd, complement), oddNode); + return oddNode; } } }