diff --git a/src/storage/dd/CuddOdd.cpp b/src/storage/dd/CuddOdd.cpp index 342f7458a..0a41ec736 100644 --- a/src/storage/dd/CuddOdd.cpp +++ b/src/storage/dd/CuddOdd.cpp @@ -16,9 +16,8 @@ namespace storm { // Prepare a unique table for each level that keeps the constructed ODD nodes unique. std::vector>>> uniqueTableForLevels(ddVariableIndices.size() + 1); - // Now construct the ODD structure. - // Currently, the DD needs to be an MTBDD, because complement edges are not supported. - std::shared_ptr> rootOdd = buildOddRec(add.getCuddDdNode(), manager->getCuddManager(), 0, ddVariableIndices.size(), ddVariableIndices, uniqueTableForLevels); + // Now construct the ODD structure from the ADD. + std::shared_ptr> rootOdd = buildOddFromAddRec(add.getCuddDdNode(), manager->getCuddManager(), 0, ddVariableIndices.size(), ddVariableIndices, uniqueTableForLevels); // Finally, move the children of the root ODD into this ODD. this->elseNode = std::move(rootOdd->elseNode); @@ -27,7 +26,41 @@ namespace storm { this->thenOffset = rootOdd->thenOffset; } + Odd::Odd(Bdd const& bdd) { + std::shared_ptr const> manager = bdd.getDdManager(); + + // First, we need to determine the involved DD variables indices. + std::vector ddVariableIndices = bdd.getSortedVariableIndices(); + + // Prepare a unique table for each level that keeps the constructed ODD nodes unique. + std::vector>>> uniqueTableForLevels(ddVariableIndices.size() + 1); + + // Now construct the ODD structure from the ADD. + bdd.exportToDot("bdd.dot"); + bdd.toAdd().exportToDot("add.dot"); + std::cout << "count: " << bdd.getNonZeroCount() << std::endl; + std::cout << "root cmpl? " << Cudd_IsComplement(bdd.getCuddDdNode()) << std::endl; + std::shared_ptr> rootOdd = buildOddFromBddRec(bdd.getCuddDdNode(), manager->getCuddManager(), 0, Cudd_IsComplement(bdd.getCuddDdNode()), ddVariableIndices.size(), ddVariableIndices, uniqueTableForLevels); + + // Finally, move the children of the root ODD into this ODD. + this->elseNode = std::move(rootOdd->elseNode); + this->thenNode = std::move(rootOdd->thenNode); + + // If the node is a complement node, + if (Cudd_IsComplement(bdd.getCuddDdNode())) { + this->elseOffset = (1ull << (ddVariableIndices.size() - 1)) - rootOdd->elseOffset; + this->thenOffset = (1ull << (ddVariableIndices.size() - 1)) - rootOdd->thenOffset; + } else { + this->elseOffset = rootOdd->elseOffset; + this->thenOffset = rootOdd->thenOffset; + } + + std::cout << "then offset is: " << this->thenOffset << std::endl; + std::cout << "else offset is: " << this->elseOffset << std::endl; + } + Odd::Odd(std::shared_ptr> elseNode, uint_fast64_t elseOffset, std::shared_ptr> thenNode, uint_fast64_t thenOffset) : elseNode(elseNode), thenNode(thenNode), elseOffset(elseOffset), thenOffset(thenOffset) { + std::cout << "creating ODD with offsets (" << elseOffset << ", " << thenOffset << ")" << std::endl; // Intentionally left empty. } @@ -73,7 +106,7 @@ namespace storm { } } - std::shared_ptr> Odd::buildOddRec(DdNode* dd, Cudd const& manager, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::vector const& ddVariableIndices, std::vector>>>& uniqueTableForLevels) { + std::shared_ptr> Odd::buildOddFromAddRec(DdNode* dd, Cudd const& manager, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::vector const& ddVariableIndices, std::vector>>>& uniqueTableForLevels) { // Check whether the ODD for this node has already been computed (for this level) and if so, return this instead. auto const& iterator = uniqueTableForLevels[currentLevel].find(dd); if (iterator != uniqueTableForLevels[currentLevel].end()) { @@ -81,29 +114,97 @@ namespace storm { } else { // Otherwise, we need to recursively compute the ODD. - // If we are already past the maximal level that is to be considered, we can simply create a Odd without + // If we are already past the maximal level that is to be considered, we can simply create an Odd without // successors if (currentLevel == maxLevel) { uint_fast64_t elseOffset = 0; uint_fast64_t thenOffset = 0; // If the DD is not the zero leaf, then the then-offset is 1. - if (dd != Cudd_ReadZero(manager.getManager())) { + if ((Cudd_IsComplement(dd) && dd != Cudd_ReadOne(manager.getManager())) || (!Cudd_IsComplement(dd) && dd != Cudd_ReadZero(manager.getManager()))) { thenOffset = 1; } return std::shared_ptr>(new Odd(nullptr, elseOffset, nullptr, thenOffset)); } else if (ddVariableIndices[currentLevel] < static_cast(dd->index)) { + // 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 = buildOddRec(dd, manager, currentLevel + 1, maxLevel, ddVariableIndices, uniqueTableForLevels); + std::shared_ptr> elseNode = buildOddFromAddRec(dd, manager, currentLevel + 1, maxLevel, ddVariableIndices, uniqueTableForLevels); std::shared_ptr> thenNode = elseNode; return std::shared_ptr>(new Odd(elseNode, elseNode->getElseOffset() + elseNode->getThenOffset(), thenNode, thenNode->getElseOffset() + thenNode->getThenOffset())); } else { // Otherwise, we compute the ODDs for both the then- and else successors. - std::shared_ptr> elseNode = buildOddRec(Cudd_E(dd), manager, currentLevel + 1, maxLevel, ddVariableIndices, uniqueTableForLevels); - std::shared_ptr> thenNode = buildOddRec(Cudd_T(dd), manager, currentLevel + 1, maxLevel, ddVariableIndices, uniqueTableForLevels); - return std::shared_ptr>(new Odd(elseNode, elseNode->getElseOffset() + elseNode->getThenOffset(), thenNode, thenNode->getElseOffset() + thenNode->getThenOffset())); + bool elseComplemented = Cudd_IsComplement(Cudd_E(dd)); + bool thenComplemented = Cudd_IsComplement(Cudd_T(dd)); + std::cout << "something complemented? " << elseComplemented << " // " << thenComplemented << std::endl; + std::shared_ptr> elseNode = buildOddFromAddRec(Cudd_E(dd), manager, currentLevel + 1, maxLevel, ddVariableIndices, uniqueTableForLevels); + std::shared_ptr> thenNode = buildOddFromAddRec(Cudd_T(dd), manager, currentLevel + 1, maxLevel, ddVariableIndices, uniqueTableForLevels); + uint_fast64_t totalElseOffset = elseNode->getElseOffset() + elseNode->getThenOffset(); + uint_fast64_t totalThenOffset = thenNode->getElseOffset() + thenNode->getThenOffset(); + return std::shared_ptr>(new Odd(elseNode, elseComplemented ? (1ull << (maxLevel - currentLevel - 1)) - totalElseOffset : totalElseOffset, thenNode, thenComplemented ? (1ull << (maxLevel - currentLevel - 1)) - totalThenOffset : totalThenOffset)); + } + } + } + + std::shared_ptr> Odd::buildOddFromBddRec(DdNode* dd, Cudd const& manager, uint_fast64_t currentLevel, bool complement, uint_fast64_t maxLevel, std::vector const& ddVariableIndices, std::vector>>>& uniqueTableForLevels) { + // Check whether the ODD for this node has already been computed (for this level) and if so, return this instead. + auto const& iterator = uniqueTableForLevels[currentLevel].find(dd); + if (iterator != uniqueTableForLevels[currentLevel].end()) { + return iterator->second; + } else { + std::cout << "treating level " << currentLevel << std::endl; + // Otherwise, we need to recursively compute the ODD. + + // If we are already past the maximal level that is to be considered, we can simply create an Odd without + // successors + if (currentLevel == maxLevel) { + std::cout << "curLev " << currentLevel << " and max " << maxLevel << std::endl; + uint_fast64_t elseOffset = 0; + uint_fast64_t thenOffset = 0; + + // If the DD is not the zero leaf, then the then-offset is 1. + std::cout << "complement flag set? " << complement << std::endl; + DdNode* node = Cudd_Regular(dd); + if (node != Cudd_ReadZero(manager.getManager())) { + std::cout << "offset is one" << std::endl; + thenOffset = 1; + } + + // If we need to complement the 'terminal' node, we need to negate its offset. + if (complement) { + std::cout << "negating offset" << std::endl; + thenOffset = 1 - thenOffset; + } + + std::cout << "(1) new ODD at level " << currentLevel << std::endl; + return std::shared_ptr>(new Odd(nullptr, elseOffset, nullptr, thenOffset)); + } else if (ddVariableIndices[currentLevel] < static_cast(dd->index)) { + // 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::cout << "following then/else node..." << std::endl; + std::shared_ptr> elseNode = buildOddFromBddRec(dd, manager, currentLevel + 1, complement, maxLevel, ddVariableIndices, uniqueTableForLevels); + std::shared_ptr> thenNode = elseNode; + uint_fast64_t totalOffset = elseNode->getElseOffset() + elseNode->getThenOffset(); + if (complement) { + totalOffset = (1ull << (maxLevel - currentLevel - 1)) - totalOffset; + } + + std::cout << "(2) new ODD at level " << currentLevel << std::endl; + return std::shared_ptr>(new Odd(elseNode, totalOffset, thenNode, totalOffset)); + } else { + // Otherwise, we compute the ODDs for both the then- and else successors. + bool elseComplemented = Cudd_IsComplement(Cudd_E(dd)) ^ complement; + bool thenComplemented = Cudd_IsComplement(Cudd_T(dd)) ^ complement; + std::cout << "something complemented? " << elseComplemented << " // " << thenComplemented << std::endl; + std::cout << "following else node..." << std::endl; + std::shared_ptr> elseNode = buildOddFromBddRec(Cudd_E(dd), manager, currentLevel + 1, elseComplemented, maxLevel, ddVariableIndices, uniqueTableForLevels); + std::cout << "following then node..." << std::endl; + std::shared_ptr> thenNode = buildOddFromBddRec(Cudd_T(dd), manager, currentLevel + 1, thenComplemented, maxLevel, ddVariableIndices, uniqueTableForLevels); + uint_fast64_t totalElseOffset = elseNode->getElseOffset() + elseNode->getThenOffset(); + uint_fast64_t totalThenOffset = thenNode->getElseOffset() + thenNode->getThenOffset(); + std::cout << "(3) new ODD at level " << currentLevel << std::endl; + return std::shared_ptr>(new Odd(elseNode, elseComplemented ? (1ull << (maxLevel - currentLevel - 1)) - totalElseOffset : totalElseOffset, thenNode, thenComplemented ? (1ull << (maxLevel - currentLevel - 1)) - totalThenOffset : totalThenOffset)); } } } diff --git a/src/storage/dd/CuddOdd.h b/src/storage/dd/CuddOdd.h index 9d93d6e47..f09bfed65 100644 --- a/src/storage/dd/CuddOdd.h +++ b/src/storage/dd/CuddOdd.h @@ -16,12 +16,19 @@ namespace storm { class Odd { public: /*! - * Constructs an offset-labeled DD from the given DD. + * Constructs an offset-labeled DD from the given ADD. * - * @param add The ADD for which to build the offset-labeled DD. + * @param add The ADD for which to build the offset-labeled ADD. */ Odd(Add const& add); + /*! + * Constructs an offset-labeled DD from the given BDD. + * + * @param bdd The BDD for which to build the offset-labeled ADD. + */ + Odd(Bdd const& bdd); + // Instantiate all copy/move constructors/assignments with the default implementation. Odd() = default; Odd(Odd const& other) = default; @@ -101,7 +108,7 @@ namespace storm { Odd(std::shared_ptr> elseNode, uint_fast64_t elseOffset, std::shared_ptr> thenNode, uint_fast64_t thenOffset); /*! - * Recursively builds the ODD. + * Recursively builds the ODD from an ADD (that has no complement edges). * * @param dd The DD for which to build the ODD. * @param manager The manager responsible for the DD. @@ -112,7 +119,9 @@ namespace storm { * ODD nodes for the same DD and level unique. * @return A pointer to the constructed ODD for the given arguments. */ - static std::shared_ptr> buildOddRec(DdNode* dd, Cudd const& manager, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::vector const& ddVariableIndices, std::vector>>>& uniqueTableForLevels); + static std::shared_ptr> buildOddFromAddRec(DdNode* dd, Cudd const& manager, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::vector const& ddVariableIndices, std::vector>>>& uniqueTableForLevels); + + static std::shared_ptr> buildOddFromBddRec(DdNode* dd, Cudd const& manager, uint_fast64_t currentLevel, bool complement, uint_fast64_t maxLevel, std::vector const& ddVariableIndices, std::vector>>>& uniqueTableForLevels); // The then- and else-nodes. std::shared_ptr> elseNode; diff --git a/test/functional/storage/CuddDdTest.cpp b/test/functional/storage/CuddDdTest.cpp index 654283a90..431661d00 100644 --- a/test/functional/storage/CuddDdTest.cpp +++ b/test/functional/storage/CuddDdTest.cpp @@ -318,7 +318,7 @@ TEST(CuddDd, OddTest) { std::shared_ptr> manager(new storm::dd::DdManager()); std::pair a = manager->addMetaVariable("a"); std::pair x = manager->addMetaVariable("x", 1, 9); - + storm::dd::Add dd = manager->getIdentity(x.first); storm::dd::Odd odd; ASSERT_NO_THROW(odd = storm::dd::Odd(dd)); @@ -356,4 +356,26 @@ TEST(CuddDd, OddTest) { EXPECT_EQ(9, matrix.getRowGroupCount()); EXPECT_EQ(9, matrix.getColumnCount()); EXPECT_EQ(106, matrix.getNonzeroEntryCount()); + + std::cout << "########################################################################################" << std::endl; + + // Recreate the ODDs, this time starting from a BDD. + ASSERT_NO_THROW(rowOdd = storm::dd::Odd(manager->getRange(x.first))); + ASSERT_NO_THROW(columnOdd = storm::dd::Odd(manager->getRange(x.second))); + + // Try to translate the matrix. + ASSERT_NO_THROW(matrix = dd.toMatrix({x.first}, {x.second}, rowOdd, columnOdd)); + + EXPECT_EQ(9, matrix.getRowCount()); + EXPECT_EQ(9, matrix.getColumnCount()); + + std::cout << matrix << std::endl; + EXPECT_EQ(25, matrix.getNonzeroEntryCount()); + + dd = manager->getRange(x.first).toAdd() * manager->getRange(x.second).toAdd() * manager->getEncoding(a.first, 0).toAdd().ite(dd, dd + manager->getConstant(1)); + ASSERT_NO_THROW(matrix = dd.toMatrix({x.first}, {x.second}, {a.first}, rowOdd, columnOdd)); + EXPECT_EQ(18, matrix.getRowCount()); + EXPECT_EQ(9, matrix.getRowGroupCount()); + EXPECT_EQ(9, matrix.getColumnCount()); + EXPECT_EQ(106, matrix.getNonzeroEntryCount()); } \ No newline at end of file