diff --git a/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.cc b/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.cc index b8f7d3983..e15f399f6 100644 --- a/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.cc +++ b/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.cc @@ -72,6 +72,7 @@ static char rcsid[] UNUSED = "$Id: cuddObj.cc,v 1.15 2012/02/05 01:06:40 fabio E // Members of class DD // --------------------------------------------------------------------------- +namespace cudd { DD::DD() : p(0), node(0) {} @@ -5835,3 +5836,5 @@ Cudd::DumpDot( checkReturnValue(result); } // vector::DumpDot + +} // end namespace cudd diff --git a/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.hh b/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.hh index 0b5acf051..9302688b9 100644 --- a/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.hh +++ b/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.hh @@ -72,6 +72,8 @@ #include #include "cudd.h" +namespace cudd { + /*---------------------------------------------------------------------------*/ /* Type definitions */ /*---------------------------------------------------------------------------*/ @@ -770,7 +772,8 @@ public: }; // Cudd - extern void defaultError(std::string message); +} // end namespace cudd + #endif diff --git a/src/storage/dd/cudd/CuddAddIterator.cpp b/src/storage/dd/cudd/CuddAddIterator.cpp index 5b3761cd8..3f8f1a75c 100644 --- a/src/storage/dd/cudd/CuddAddIterator.cpp +++ b/src/storage/dd/cudd/CuddAddIterator.cpp @@ -67,7 +67,7 @@ namespace storm { // found solutions and get the next "first" cube. if (this->relevantDontCareDdVariables.empty() || this->cubeCounter >= std::pow(2, this->relevantDontCareDdVariables.size()) - 1) { // Get the next cube and check for emptiness. - ABDD::NextCube(generator, &cube, &valueAsDouble); + cudd::ABDD::NextCube(generator, &cube, &valueAsDouble); this->isAtEnd = (Cudd_IsGenEmpty(generator) != 0); // In case we are not done yet, we get ready to treat the next cube. diff --git a/src/storage/dd/cudd/InternalCuddAdd.cpp b/src/storage/dd/cudd/InternalCuddAdd.cpp index f9bc567b5..aac311481 100644 --- a/src/storage/dd/cudd/InternalCuddAdd.cpp +++ b/src/storage/dd/cudd/InternalCuddAdd.cpp @@ -13,7 +13,7 @@ namespace storm { namespace dd { template - InternalAdd::InternalAdd(InternalDdManager const* ddManager, ADD cuddAdd) : ddManager(ddManager), cuddAdd(cuddAdd) { + InternalAdd::InternalAdd(InternalDdManager const* ddManager, cudd::ADD cuddAdd) : ddManager(ddManager), cuddAdd(cuddAdd) { // Intentionally left empty. } @@ -183,8 +183,8 @@ namespace storm { template InternalAdd InternalAdd::swapVariables(std::vector> const& from, std::vector> const& to) const { - std::vector fromAdd; - std::vector toAdd; + std::vector fromAdd; + std::vector toAdd; STORM_LOG_ASSERT(fromAdd.size() == toAdd.size(), "Sizes of vectors do not match."); for (auto it1 = from.begin(), ite1 = from.end(), it2 = to.begin(); it1 != ite1; ++it1, ++it2) { fromAdd.push_back(it1->getCuddAdd()); @@ -196,7 +196,7 @@ namespace storm { template InternalAdd InternalAdd::multiplyMatrix(InternalAdd const& otherMatrix, std::vector> const& summationDdVariables) const { // Create the CUDD summation variables. - std::vector summationAdds; + std::vector summationAdds; for (auto const& ddVariable : summationDdVariables) { summationAdds.push_back(ddVariable.getCuddAdd()); } @@ -261,13 +261,13 @@ namespace storm { template ValueType InternalAdd::getMin() const { - ADD constantMinAdd = this->getCuddAdd().FindMin(); + cudd::ADD constantMinAdd = this->getCuddAdd().FindMin(); return static_cast(Cudd_V(constantMinAdd.getNode())); } template ValueType InternalAdd::getMax() const { - ADD constantMaxAdd = this->getCuddAdd().FindMax(); + cudd::ADD constantMaxAdd = this->getCuddAdd().FindMax(); return static_cast(Cudd_V(constantMaxAdd.getNode())); } @@ -313,7 +313,7 @@ namespace storm { // Open the file, dump the DD and close it again. FILE* filePointer = fopen(filename.c_str() , "w"); - std::vector cuddAddVector = { this->getCuddAdd() }; + std::vector cuddAddVector = { this->getCuddAdd() }; ddManager->getCuddManager().DumpDot(cuddAddVector, &ddVariableNames[0], &ddNames[0], filePointer); fclose(filePointer); @@ -340,7 +340,7 @@ namespace storm { } template - ADD InternalAdd::getCuddAdd() const { + cudd::ADD InternalAdd::getCuddAdd() const { return this->cuddAdd; } @@ -362,7 +362,7 @@ namespace storm { } template - std::shared_ptr InternalAdd::createOddRec(DdNode* dd, Cudd const& manager, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::vector const& ddVariableIndices, std::vector>>& uniqueTableForLevels) { + std::shared_ptr InternalAdd::createOddRec(DdNode* dd, cudd::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()) { @@ -449,7 +449,7 @@ namespace storm { } if (currentLevel == maxLevel) { - groups.push_back(InternalAdd(ddManager, ADD(ddManager->getCuddManager(), dd))); + groups.push_back(InternalAdd(ddManager, cudd::ADD(ddManager->getCuddManager(), dd))); } else if (ddGroupVariableIndices[currentLevel] < dd->index) { splitIntoGroupsRec(dd, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); splitIntoGroupsRec(dd, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); @@ -474,7 +474,7 @@ namespace storm { } if (currentLevel == maxLevel) { - groups.push_back(std::make_pair(InternalAdd(ddManager, ADD(ddManager->getCuddManager(), dd1)), InternalAdd(ddManager, ADD(ddManager->getCuddManager(), dd2)))); + groups.push_back(std::make_pair(InternalAdd(ddManager, cudd::ADD(ddManager->getCuddManager(), dd1)), InternalAdd(ddManager, cudd::ADD(ddManager->getCuddManager(), dd2)))); } else if (ddGroupVariableIndices[currentLevel] < dd1->index) { if (ddGroupVariableIndices[currentLevel] < dd2->index) { splitIntoGroupsRec(dd1, dd2, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); @@ -553,7 +553,7 @@ namespace storm { template InternalAdd InternalAdd::fromVector(InternalDdManager const* ddManager, std::vector const& values, storm::dd::Odd const& odd, std::vector const& ddVariableIndices) { uint_fast64_t offset = 0; - return InternalAdd(ddManager, ADD(ddManager->getCuddManager(), fromVectorRec(ddManager->getCuddManager().getManager(), offset, 0, ddVariableIndices.size(), values, odd, ddVariableIndices))); + return InternalAdd(ddManager, cudd::ADD(ddManager->getCuddManager(), fromVectorRec(ddManager->getCuddManager().getManager(), offset, 0, ddVariableIndices.size(), values, odd, ddVariableIndices))); } template diff --git a/src/storage/dd/cudd/InternalCuddAdd.h b/src/storage/dd/cudd/InternalCuddAdd.h index 45abce994..c62dbe04d 100644 --- a/src/storage/dd/cudd/InternalCuddAdd.h +++ b/src/storage/dd/cudd/InternalCuddAdd.h @@ -47,7 +47,7 @@ namespace storm { * @param cuddAdd The CUDD ADD to store. * @param containedMetaVariables The meta variables that appear in the DD. */ - InternalAdd(InternalDdManager const* ddManager, ADD cuddAdd); + InternalAdd(InternalDdManager const* ddManager, cudd::ADD cuddAdd); // Instantiate all copy/move constructors/assignments with the default implementation. InternalAdd() = default; @@ -586,7 +586,7 @@ namespace storm { * * @return The CUDD ADD object associated with this ADD. */ - ADD getCuddAdd() const; + cudd::ADD getCuddAdd() const; /*! * Retrieves the raw DD node of CUDD associated with this ADD. @@ -687,11 +687,11 @@ 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 createOddRec(DdNode* dd, Cudd const& manager, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::vector const& ddVariableIndices, std::vector>>& uniqueTableForLevels); + static std::shared_ptr createOddRec(DdNode* dd, cudd::Cudd const& manager, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::vector const& ddVariableIndices, std::vector>>& uniqueTableForLevels); InternalDdManager const* ddManager; - ADD cuddAdd; + cudd::ADD cuddAdd; }; } } diff --git a/src/storage/dd/cudd/InternalCuddBdd.cpp b/src/storage/dd/cudd/InternalCuddBdd.cpp index 3bfb98c5c..b4c12e82d 100644 --- a/src/storage/dd/cudd/InternalCuddBdd.cpp +++ b/src/storage/dd/cudd/InternalCuddBdd.cpp @@ -9,14 +9,14 @@ namespace storm { namespace dd { - InternalBdd::InternalBdd(InternalDdManager const* ddManager, BDD cuddBdd) : ddManager(ddManager), cuddBdd(cuddBdd) { + InternalBdd::InternalBdd(InternalDdManager const* ddManager, cudd::BDD cuddBdd) : ddManager(ddManager), cuddBdd(cuddBdd) { // Intentionally left empty. } template InternalBdd InternalBdd::fromVector(InternalDdManager const* ddManager, std::vector const& values, Odd const& odd, std::vector const& sortedDdVariableIndices, std::function const& filter) { uint_fast64_t offset = 0; - return InternalBdd(ddManager, BDD(ddManager->getCuddManager(), fromVectorRec(ddManager->getCuddManager().getManager(), offset, 0, sortedDdVariableIndices.size(), values, odd, sortedDdVariableIndices, filter))); + return InternalBdd(ddManager, cudd::BDD(ddManager->getCuddManager(), fromVectorRec(ddManager->getCuddManager().getManager(), offset, 0, sortedDdVariableIndices.size(), values, odd, sortedDdVariableIndices, filter))); } bool InternalBdd::operator==(InternalBdd const& other) const { @@ -97,8 +97,8 @@ namespace storm { } InternalBdd InternalBdd::swapVariables(std::vector> const& from, std::vector> const& to) const { - std::vector fromBdd; - std::vector toBdd; + std::vector fromBdd; + std::vector toBdd; for (auto it1 = from.begin(), ite1 = from.end(), it2 = to.begin(); it1 != ite1; ++it1, ++it2) { fromBdd.push_back(it1->getCuddBdd()); toBdd.push_back(it2->getCuddBdd()); @@ -150,7 +150,7 @@ namespace storm { // Open the file, dump the DD and close it again. FILE* filePointer = fopen(filename.c_str() , "w"); - std::vector cuddBddVector = { this->getCuddBdd() }; + std::vector cuddBddVector = { this->getCuddBdd() }; ddManager->getCuddManager().DumpDot(cuddBddVector, &ddVariableNames[0], &ddNames[0], filePointer); fclose(filePointer); @@ -163,7 +163,7 @@ namespace storm { } } - BDD InternalBdd::getCuddBdd() const { + cudd::BDD InternalBdd::getCuddBdd() const { return this->cuddBdd; } @@ -239,7 +239,7 @@ namespace storm { return result; } - void InternalBdd::toVectorRec(DdNode const* dd, Cudd const& manager, storm::storage::BitVector& result, Odd const& rowOdd, bool complement, uint_fast64_t currentRowLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, std::vector const& ddRowVariableIndices) const { + void InternalBdd::toVectorRec(DdNode const* dd, cudd::Cudd const& manager, storm::storage::BitVector& result, Odd const& rowOdd, bool complement, uint_fast64_t currentRowLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, std::vector const& ddRowVariableIndices) const { // If there are no more values to select, we can directly return. if (dd == Cudd_ReadLogicZero(manager.getManager()) && !complement) { return; @@ -285,7 +285,7 @@ namespace storm { return result; } - std::shared_ptr InternalBdd::createOddRec(DdNode* dd, Cudd const& manager, uint_fast64_t currentLevel, bool complement, uint_fast64_t maxLevel, std::vector const& ddVariableIndices, std::vector, std::shared_ptr, HashFunctor>>& uniqueTableForLevels) { + std::shared_ptr InternalBdd::createOddRec(DdNode* dd, cudd::Cudd const& manager, uint_fast64_t currentLevel, bool complement, uint_fast64_t maxLevel, std::vector const& ddVariableIndices, std::vector, std::shared_ptr, HashFunctor>>& 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(std::make_pair(dd, complement)); if (iterator != uniqueTableForLevels[currentLevel].end()) { @@ -341,7 +341,7 @@ namespace storm { } template - void InternalBdd::filterExplicitVectorRec(DdNode* dd, Cudd const& manager, uint_fast64_t currentLevel, bool complement, uint_fast64_t maxLevel, std::vector const& ddVariableIndices, uint_fast64_t currentOffset, storm::dd::Odd const& odd, std::vector& result, uint_fast64_t& currentIndex, std::vector const& values) { + void InternalBdd::filterExplicitVectorRec(DdNode* dd, cudd::Cudd const& manager, uint_fast64_t currentLevel, bool complement, uint_fast64_t maxLevel, std::vector const& ddVariableIndices, uint_fast64_t currentOffset, storm::dd::Odd const& odd, std::vector& result, uint_fast64_t& currentIndex, std::vector const& values) { // If there are no more values to select, we can directly return. if (dd == Cudd_ReadLogicZero(manager.getManager()) && !complement) { return; @@ -384,8 +384,8 @@ namespace storm { template InternalAdd InternalBdd::toAdd() const; template InternalAdd InternalBdd::toAdd() const; - template void InternalBdd::filterExplicitVectorRec(DdNode* dd, Cudd const& manager, uint_fast64_t currentLevel, bool complement, uint_fast64_t maxLevel, std::vector const& ddVariableIndices, uint_fast64_t currentOffset, storm::dd::Odd const& odd, std::vector& result, uint_fast64_t& currentIndex, std::vector const& values); - template void InternalBdd::filterExplicitVectorRec(DdNode* dd, Cudd const& manager, uint_fast64_t currentLevel, bool complement, uint_fast64_t maxLevel, std::vector const& ddVariableIndices, uint_fast64_t currentOffset, storm::dd::Odd const& odd, std::vector& result, uint_fast64_t& currentIndex, std::vector const& values); + template void InternalBdd::filterExplicitVectorRec(DdNode* dd, cudd::Cudd const& manager, uint_fast64_t currentLevel, bool complement, uint_fast64_t maxLevel, std::vector const& ddVariableIndices, uint_fast64_t currentOffset, storm::dd::Odd const& odd, std::vector& result, uint_fast64_t& currentIndex, std::vector const& values); + template void InternalBdd::filterExplicitVectorRec(DdNode* dd, cudd::Cudd const& manager, uint_fast64_t currentLevel, bool complement, uint_fast64_t maxLevel, std::vector const& ddVariableIndices, uint_fast64_t currentOffset, storm::dd::Odd const& odd, std::vector& result, uint_fast64_t& currentIndex, std::vector const& values); template void InternalBdd::filterExplicitVector(Odd const& odd, std::vector const& ddVariableIndices, std::vector const& sourceValues, std::vector& targetValues) const; template void InternalBdd::filterExplicitVector(Odd const& odd, std::vector const& ddVariableIndices, std::vector const& sourceValues, std::vector& targetValues) const; diff --git a/src/storage/dd/cudd/InternalCuddBdd.h b/src/storage/dd/cudd/InternalCuddBdd.h index 38c31cdcb..a20a7413e 100644 --- a/src/storage/dd/cudd/InternalCuddBdd.h +++ b/src/storage/dd/cudd/InternalCuddBdd.h @@ -37,7 +37,7 @@ namespace storm { * @param cuddBdd The CUDD BDD to store. * @param containedMetaVariables The meta variables that appear in the DD. */ - InternalBdd(InternalDdManager const* ddManager, BDD cuddBdd); + InternalBdd(InternalDdManager const* ddManager, cudd::BDD cuddBdd); // Instantiate all copy/move constructors/assignments with the default implementation. InternalBdd() = default; @@ -310,7 +310,7 @@ namespace storm { * * @return The CUDD BDD object associated with this DD. */ - BDD getCuddBdd() const; + cudd::BDD getCuddBdd() const; /*! * Retrieves the raw DD node of CUDD associated with this BDD. @@ -348,7 +348,7 @@ namespace storm { * @param currentRowOffset The current row offset. * @param ddRowVariableIndices The (sorted) indices of all DD row variables that need to be considered. */ - void toVectorRec(DdNode const* dd, Cudd const& manager, storm::storage::BitVector& result, Odd const& rowOdd, bool complement, uint_fast64_t currentRowLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, std::vector const& ddRowVariableIndices) const; + void toVectorRec(DdNode const* dd, cudd::Cudd const& manager, storm::storage::BitVector& result, Odd const& rowOdd, bool complement, uint_fast64_t currentRowLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, std::vector const& ddRowVariableIndices) const; // Declare a hash functor that is used for the unique tables in the construction process of ODDs. class HashFunctor { @@ -369,7 +369,7 @@ 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 createOddRec(DdNode* dd, Cudd const& manager, uint_fast64_t currentLevel, bool complement, uint_fast64_t maxLevel, std::vector const& ddVariableIndices, std::vector, std::shared_ptr, HashFunctor>>& uniqueTableForLevels); + static std::shared_ptr createOddRec(DdNode* dd, cudd::Cudd const& manager, uint_fast64_t currentLevel, bool complement, uint_fast64_t maxLevel, std::vector const& ddVariableIndices, std::vector, std::shared_ptr, HashFunctor>>& uniqueTableForLevels); /*! * Adds the selected values the target vector. @@ -386,11 +386,11 @@ namespace storm { * @param values The value vector from which to select the values. */ template - static void filterExplicitVectorRec(DdNode* dd, Cudd const& manager, uint_fast64_t currentLevel, bool complement, uint_fast64_t maxLevel, std::vector const& ddVariableIndices, uint_fast64_t currentOffset, storm::dd::Odd const& odd, std::vector& result, uint_fast64_t& currentIndex, std::vector const& values); + static void filterExplicitVectorRec(DdNode* dd, cudd::Cudd const& manager, uint_fast64_t currentLevel, bool complement, uint_fast64_t maxLevel, std::vector const& ddVariableIndices, uint_fast64_t currentOffset, storm::dd::Odd const& odd, std::vector& result, uint_fast64_t& currentIndex, std::vector const& values); InternalDdManager const* ddManager; - BDD cuddBdd; + cudd::BDD cuddBdd; }; } } diff --git a/src/storage/dd/cudd/InternalCuddDdManager.cpp b/src/storage/dd/cudd/InternalCuddDdManager.cpp index 2e95913ea..b6c7fdbb0 100644 --- a/src/storage/dd/cudd/InternalCuddDdManager.cpp +++ b/src/storage/dd/cudd/InternalCuddDdManager.cpp @@ -85,11 +85,11 @@ namespace storm { this->getCuddManager().ReduceHeap(this->reorderingTechnique, 0); } - Cudd& InternalDdManager::getCuddManager() { + cudd::Cudd& InternalDdManager::getCuddManager() { return cuddManager; } - Cudd const& InternalDdManager::getCuddManager() const { + cudd::Cudd const& InternalDdManager::getCuddManager() const { return cuddManager; } diff --git a/src/storage/dd/cudd/InternalCuddDdManager.h b/src/storage/dd/cudd/InternalCuddDdManager.h index e56bad54d..884b69abb 100644 --- a/src/storage/dd/cudd/InternalCuddDdManager.h +++ b/src/storage/dd/cudd/InternalCuddDdManager.h @@ -100,17 +100,17 @@ namespace storm { * * @return The underlying CUDD manager. */ - Cudd& getCuddManager(); + cudd::Cudd& getCuddManager(); /*! * Retrieves the underlying CUDD manager. * * @return The underlying CUDD manager. */ - Cudd const& getCuddManager() const; + cudd::Cudd const& getCuddManager() const; // The manager responsible for the DDs created/modified with this DdManager. - Cudd cuddManager; + cudd::Cudd cuddManager; // The technique that is used for dynamic reordering. Cudd_ReorderingType reorderingTechnique; diff --git a/src/storage/dd/sylvan/InternalSylvanBdd.cpp b/src/storage/dd/sylvan/InternalSylvanBdd.cpp index bc2444273..02428ec89 100644 --- a/src/storage/dd/sylvan/InternalSylvanBdd.cpp +++ b/src/storage/dd/sylvan/InternalSylvanBdd.cpp @@ -2,7 +2,6 @@ #include "src/storage/dd/sylvan/InternalSylvanAdd.h" #include "src/storage/dd/sylvan/SylvanAddIterator.h" -# #include "src/storage/BitVector.h" diff --git a/src/storage/dd/sylvan/InternalSylvanBdd.h b/src/storage/dd/sylvan/InternalSylvanBdd.h index bacc4efca..ff73837e0 100644 --- a/src/storage/dd/sylvan/InternalSylvanBdd.h +++ b/src/storage/dd/sylvan/InternalSylvanBdd.h @@ -8,6 +8,8 @@ #include "src/storage/dd/InternalBdd.h" #include "src/storage/dd/InternalAdd.h" +#include "sylvan_obj.hpp" + namespace storm { namespace storage { class BitVector; @@ -17,9 +19,6 @@ namespace storm { template class InternalDdManager; - template - class InternalAdd; - class Odd; template<>