Added ODD-concept to easily convert between DD-based and explicit formats.

Former-commit-id: f2a2a002b7

src/storage/dd/CuddDd.cpp

@@ -2,6 +2,7 @@
 #include <algorithm>
 
 #include "src/storage/dd/CuddDd.h"
+#include "src/storage/dd/CuddOdd.h"
 #include "src/storage/dd/CuddDdManager.h"
 
 #include "src/exceptions/InvalidArgumentException.h"
@@ -425,6 +426,55 @@ namespace storm {
             return Cudd_IsConstant(this->cuddAdd.getNode());
         }
         
+        uint_fast64_t Dd<DdType::CUDD>::getIndex() const {
+            return static_cast<uint_fast64_t>(this->getCuddAdd().NodeReadIndex());
+        }
+        
+        std::vector<double> Dd<DdType::CUDD>::toDoubleVector() const {
+            return this->toDoubleVector(Odd<DdType::CUDD>(*this));
+        }
+        
+        std::vector<double> Dd<DdType::CUDD>::toDoubleVector(Odd<DdType::CUDD> const& odd) const {
+            std::vector<double> result(odd.getTotalOffset());
+            std::vector<uint_fast64_t> ddVariableIndices = this->getSortedVariableIndices();
+            toDoubleVectorRec(this->getCuddAdd().getNode(), result, odd, 0, ddVariableIndices.size(), 0, ddVariableIndices);
+            return result;
+        }
+        
+        void Dd<DdType::CUDD>::toDoubleVectorRec(DdNode const* dd, std::vector<double>& result, Odd<DdType::CUDD> const& odd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, std::vector<uint_fast64_t> const& ddVariableIndices) const {
+            if (dd == this->getDdManager()->getZero().getCuddAdd().getNode()) {
+                return;
+            }
+            
+            // If we are at the maximal level, the value to be set is stored as a constant in the DD.
+            if (currentLevel == maxLevel) {
+                result[currentOffset] = Cudd_V(dd);
+            } else if (ddVariableIndices[currentLevel] < dd->index) {
+                // If we skipped a level, we need to enumerate the explicit entries for the case in which the bit is set
+                // and for the one in which it is not set.
+                toDoubleVectorRec(dd, result, odd.getElseSuccessor(), currentLevel + 1, maxLevel, currentOffset, ddVariableIndices);
+                toDoubleVectorRec(dd, result, odd.getThenSuccessor(), currentLevel + 1, maxLevel, currentOffset + odd.getElseOffset(), ddVariableIndices);
+            } else {
+                // Otherwise, we simply recursively call the function for both (different) cases.
+                toDoubleVectorRec(Cudd_E(dd), result, odd.getElseSuccessor(), currentLevel + 1, maxLevel, currentOffset, ddVariableIndices);
+                toDoubleVectorRec(Cudd_T(dd), result, odd.getThenSuccessor(), currentLevel + 1, maxLevel, currentOffset + odd.getElseOffset(), ddVariableIndices);
+            }
+        }
+        
+        std::vector<uint_fast64_t> Dd<DdType::CUDD>::getSortedVariableIndices() const {
+            std::vector<uint_fast64_t> ddVariableIndices;
+            for (auto const& metaVariableName : this->getContainedMetaVariableNames()) {
+                auto const& metaVariable = this->getDdManager()->getMetaVariable(metaVariableName);
+                for (auto const& ddVariable : metaVariable.getDdVariables()) {
+                    ddVariableIndices.push_back(ddVariable.getIndex());
+                }
+            }
+            
+            // Next, we need to sort them, since they may be arbitrarily ordered otherwise.
+            std::sort(ddVariableIndices.begin(), ddVariableIndices.end());
+            return ddVariableIndices;
+        }
+        
         bool Dd<DdType::CUDD>::containsMetaVariable(std::string const& metaVariableName) const {
             auto const& metaVariable = containedMetaVariableNames.find(metaVariableName);
             return metaVariable != containedMetaVariableNames.end();

src/storage/dd/CuddDd.h

@@ -16,8 +16,9 @@
 
 namespace storm {
     namespace dd {
-        // Forward-declare the DdManager class.
+        // Forward-declare some classes.
         template<DdType Type> class DdManager;
+        template<DdType Type> class Odd;
         
         template<>
         class Dd<DdType::CUDD> {
@@ -25,6 +26,7 @@ namespace storm {
             // Declare the DdManager and DdIterator class as friend so it can access the internals of a DD.
             friend class DdManager<DdType::CUDD>;
             friend class DdForwardIterator<DdType::CUDD>;
+            friend class Odd<DdType::CUDD>;
             
             // Instantiate all copy/move constructors/assignments with the default implementation.
             Dd() = default;
@@ -447,6 +449,28 @@ namespace storm {
              */
             bool isConstant() const;
             
+            /*!
+             * Retrieves the index of the topmost variable in the DD.
+             *
+             * @return The index of the topmost variable in DD.
+             */
+            uint_fast64_t getIndex() const;
+            
+            /*!
+             * Converts the DD to a double vector.
+             *
+             * @return The double vector that is represented by this DD.
+             */
+            std::vector<double> toDoubleVector() const;
+            
+            /*!
+             * Converts the DD to a double vector using the given ODD (that needs to be constructed for the DD).
+             *
+             * @param odd The ODD for the DD.
+             * @return The double vector that is represented by this DD.
+             */
+            std::vector<double> toDoubleVector(Odd<DdType::CUDD> const& odd) const;
+            
             /*!
              * Retrieves whether the given meta variable is contained in the DD.
              *
@@ -587,6 +611,28 @@ namespace storm {
              */
             Dd(std::shared_ptr<DdManager<DdType::CUDD>> ddManager, ADD cuddAdd, std::set<std::string> const& containedMetaVariableNames = std::set<std::string>());
             
+            /*!
+             * Helper function to convert the DD into a double vector.
+             *
+             * @param dd The DD to convert.
+             * @param result The resulting vector whose entries are to be set appropriately. This vector needs to be
+             * preallocated.
+             * @param odd The ODD used for the translation.
+             * @param currentLevel The currently considered level in the DD.
+             * @param maxLevel The number of levels that need to be considered.
+             * @param currentOffset The current offset.
+             * @param ddVariableIndices The (sorted) indices of all DD variables that need to be considered.
+             */
+            void toDoubleVectorRec(DdNode const* dd, std::vector<double>& result, Odd<DdType::CUDD> const& odd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, std::vector<uint_fast64_t> const& ddVariableIndices) const;
+            
+            /*!
+             * Retrieves the indices of all DD variables that are contained in this DD (not necessarily in the support,
+             * because they could be "don't cares"). Additionally, the indices are sorted to allow for easy access.
+             *
+             * @return The (sorted) indices of all DD variables that are contained in this DD.
+             */
+            std::vector<uint_fast64_t> getSortedVariableIndices() const;
+            
             // A pointer to the manager responsible for this DD.
             std::shared_ptr<DdManager<DdType::CUDD>> ddManager;
             

src/storage/dd/CuddDdManager.h

@@ -16,6 +16,7 @@ namespace storm {
         class DdManager<DdType::CUDD> : public std::enable_shared_from_this<DdManager<DdType::CUDD>> {
         public:
             friend class Dd<DdType::CUDD>;
+            friend class Odd<DdType::CUDD>;
             friend class DdForwardIterator<DdType::CUDD>;
             
             /*!

src/storage/dd/CuddDdMetaVariable.h

@@ -13,8 +13,9 @@
 
 namespace storm {
     namespace dd {
-        // Forward-declare the DdManager class.
+        // Forward-declare some classes.
         template<DdType Type> class DdManager;
+        template<DdType Type> class Odd;
         
         template<>
         class DdMetaVariable<DdType::CUDD> {
@@ -22,6 +23,7 @@ namespace storm {
             // Declare the DdManager class as friend so it can access the internals of a meta variable.
             friend class DdManager<DdType::CUDD>;
             friend class Dd<DdType::CUDD>;
+            friend class Odd<DdType::CUDD>;
             friend class DdForwardIterator<DdType::CUDD>;
             
             // An enumeration for all legal types of meta variables.

src/storage/dd/CuddOdd.cpp

@@ -0,0 +1,97 @@
+#include "src/storage/dd/CuddOdd.h"
+
+#include <algorithm>
+
+#include "src/storage/dd/CuddDdManager.h"
+#include "src/storage/dd/CuddDdMetaVariable.h"
+
+namespace storm {
+    namespace dd {
+        Odd<DdType::CUDD>::Odd(Dd<DdType::CUDD> const& dd) {
+            std::shared_ptr<DdManager<DdType::CUDD>> manager = dd.getDdManager();
+            
+            // First, we need to determine the involved DD variables indices.
+            std::vector<uint_fast64_t> ddVariableIndices = dd.getSortedVariableIndices();
+            
+            // Prepare a unique table for each level that keeps the constructed ODD nodes unique.
+            std::vector<std::map<DdNode*, std::shared_ptr<Odd<DdType::CUDD>>>> uniqueTableForLevels(ddVariableIndices.size() + 1);
+            
+            // Now construct the ODD structure.
+            std::shared_ptr<Odd<DdType::CUDD>> rootOdd = buildOddRec(dd.getCuddAdd().getNode(), manager->getCuddManager(), 0, ddVariableIndices.size(), ddVariableIndices, uniqueTableForLevels);
+            
+            // Finally, move the children of the root ODD into this ODD.
+            this->dd = rootOdd->dd;
+            this->elseNode = std::move(rootOdd->elseNode);
+            this->thenNode = std::move(rootOdd->thenNode);
+            this->elseOffset = rootOdd->elseOffset;
+            this->thenOffset = rootOdd->thenOffset;
+        }
+        
+        Odd<DdType::CUDD>::Odd(ADD dd, std::shared_ptr<Odd<DdType::CUDD>>&& elseNode, uint_fast64_t elseOffset, std::shared_ptr<Odd<DdType::CUDD>>&& thenNode, uint_fast64_t thenOffset) : dd(dd), elseNode(elseNode), thenNode(thenNode), elseOffset(elseOffset), thenOffset(thenOffset) {
+            // Intentionally left empty.
+        }
+        
+        Odd<DdType::CUDD> const& Odd<DdType::CUDD>::getThenSuccessor() const {
+            return *this->thenNode;
+        }
+        
+        Odd<DdType::CUDD> const& Odd<DdType::CUDD>::getElseSuccessor() const {
+            return *this->elseNode;
+        }
+        
+        uint_fast64_t Odd<DdType::CUDD>::getElseOffset() const {
+            return this->elseOffset;
+        }
+        
+        void Odd<DdType::CUDD>::setElseOffset(uint_fast64_t newOffset) {
+            this->elseOffset = newOffset;
+        }
+        
+        uint_fast64_t Odd<DdType::CUDD>::getThenOffset() const {
+            return this->thenOffset;
+        }
+        
+        void Odd<DdType::CUDD>::setThenOffset(uint_fast64_t newOffset) {
+            this->thenOffset = newOffset;
+        }
+        
+        uint_fast64_t Odd<DdType::CUDD>::getTotalOffset() const {
+            return this->elseOffset + this->thenOffset;
+        }
+        
+        std::shared_ptr<Odd<DdType::CUDD>> Odd<DdType::CUDD>::buildOddRec(DdNode* dd, Cudd const& manager, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<std::map<DdNode*, std::shared_ptr<Odd<DdType::CUDD>>>>& 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 {
+                // 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
+                // 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())) {
+                        thenOffset = 1;
+                    }
+                    
+                    return std::shared_ptr<Odd<DdType::CUDD>>(new Odd<DdType::CUDD>(ADD(manager, dd), nullptr, elseOffset, nullptr, thenOffset));
+                } else if (ddVariableIndices[currentLevel] < static_cast<uint_fast64_t>(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<Odd<DdType::CUDD>> elseNode = buildOddRec(dd, manager, currentLevel + 1, maxLevel, ddVariableIndices, uniqueTableForLevels);
+                    std::shared_ptr<Odd<DdType::CUDD>> thenNode = elseNode;
+                    return std::shared_ptr<Odd<DdType::CUDD>>(new Odd<DdType::CUDD>(ADD(manager, dd), std::move(elseNode), elseNode->getElseOffset() + elseNode->getThenOffset(), std::move(thenNode), thenNode->getElseOffset() + thenNode->getThenOffset()));
+                } else {
+                    // Otherwise, we compute the ODDs for both the then- and else successors.
+                    std::shared_ptr<Odd<DdType::CUDD>> elseNode = buildOddRec(Cudd_E(dd), manager, currentLevel + 1, maxLevel, ddVariableIndices, uniqueTableForLevels);
+                    std::shared_ptr<Odd<DdType::CUDD>> thenNode = buildOddRec(Cudd_T(dd), manager, currentLevel + 1, maxLevel, ddVariableIndices, uniqueTableForLevels);
+                    return std::shared_ptr<Odd<DdType::CUDD>>(new Odd<DdType::CUDD>(ADD(manager, dd), std::move(elseNode), elseNode->getElseOffset() + elseNode->getThenOffset(), std::move(thenNode), thenNode->getElseOffset() + thenNode->getThenOffset()));
+                }
+            }
+        }
+    }
+}

src/storage/dd/CuddOdd.h

@@ -0,0 +1,123 @@
+#ifndef STORM_STORAGE_DD_CUDDODD_H_
+#define STORM_STORAGE_DD_CUDDODD_H_
+
+#include <memory>
+
+#include "src/storage/dd/Odd.h"
+#include "src/storage/dd/CuddDd.h"
+#include "src/utility/OsDetection.h"
+
+// Include the C++-interface of CUDD.
+#include "cuddObj.hh"
+
+namespace storm {
+    namespace dd {
+        template<>
+        class Odd<DdType::CUDD> {
+        public:
+            /*!
+             * Constructs an offset-labeled DD from the given DD.
+             *
+             * @param dd The DD for which to build the offset-labeled DD.
+             */
+            Odd(Dd<DdType::CUDD> const& dd);
+            
+            // Instantiate all copy/move constructors/assignments with the default implementation.
+            Odd() = default;
+            Odd(Odd<DdType::CUDD> const& other) = default;
+			Odd& operator=(Odd<DdType::CUDD> const& other) = default;
+#ifndef WINDOWS
+            Odd(Odd<DdType::CUDD>&& other) = default;
+            Odd& operator=(Odd<DdType::CUDD>&& other) = default;
+#endif
+            
+            /*!
+             * Retrieves the then-successor of this ODD node.
+             *
+             * @return The then-successor of this ODD node.
+             */
+            Odd<DdType::CUDD> const& getThenSuccessor() const;
+
+            /*!
+             * Retrieves the else-successor of this ODD node.
+             *
+             * @return The else-successor of this ODD node.
+             */
+            Odd<DdType::CUDD> const& getElseSuccessor() const;
+
+            /*!
+             * Retrieves the else-offset of this ODD node.
+             *
+             * @return The else-offset of this ODD node.
+             */
+            uint_fast64_t getElseOffset() const;
+            
+            /*!
+             * Sets the else-offset of this ODD node.
+             *
+             * @param newOffset The new else-offset of this ODD node.
+             */
+            void setElseOffset(uint_fast64_t newOffset);
+            
+            /*!
+             * Retrieves the then-offset of this ODD node.
+             *
+             * @return The then-offset of this ODD node.
+             */
+            uint_fast64_t getThenOffset() const;
+            
+            /*!
+             * Sets the then-offset of this ODD node.
+             *
+             * @param newOffset The new then-offset of this ODD node.
+             */
+            void setThenOffset(uint_fast64_t newOffset);
+            
+            /*!
+             * Retrieves the total offset, i.e., the sum of the then- and else-offset.
+             *
+             * @return The total offset of this ODD.
+             */
+            uint_fast64_t getTotalOffset() const;
+            
+        private:
+            /*!
+             * Constructs an offset-labeled DD with the given topmost DD node, else- and then-successor.
+             *
+             * @param dd The DD associated with this ODD node.
+             * @param elseNode The else-successor of thie ODD node.
+             * @param elseOffset The offset of the else-successor.
+             * @param thenNode The then-successor of thie ODD node.
+             * @param thenOffset The offset of the then-successor.
+             */
+            Odd(ADD dd, std::shared_ptr<Odd<DdType::CUDD>>&& elseNode, uint_fast64_t elseOffset, std::shared_ptr<Odd<DdType::CUDD>>&& thenNode, uint_fast64_t thenOffset);
+            
+            /*!
+             * Recursively builds the ODD.
+             *
+             * @param dd The DD for which to build the ODD.
+             * @param manager The manager responsible for the DD.
+             * @param currentLevel The currently considered level in the DD.
+             * @param maxLevel The number of levels that need to be considered.
+             * @param ddVariableIndices The (sorted) indices of all DD variables that need to be considered.
+             * @param uniqueTableForLevels A vector of unique tables, one for each level to be considered, that keeps
+             * ODD nodes for the same DD and level unique.
+             * @return A pointer to the constructed ODD for the given arguments.
+             */
+            static std::shared_ptr<Odd<DdType::CUDD>> buildOddRec(DdNode* dd, Cudd const& manager, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<std::map<DdNode*, std::shared_ptr<Odd<DdType::CUDD>>>>& uniqueTableForLevels);
+            
+            // The DD associated with this ODD node.
+            ADD dd;
+            
+            // The then- and else-nodes.
+            std::shared_ptr<Odd<DdType::CUDD>> elseNode;
+            std::shared_ptr<Odd<DdType::CUDD>> thenNode;
+            
+            // The offsets that need to be added if the then- or else-successor is taken, respectively.
+            uint_fast64_t elseOffset;
+            uint_fast64_t thenOffset;
+        };
+    }
+}
+
+#endif /* STORM_STORAGE_DD_CUDDODD_H_ */

src/storage/dd/Odd.h

@@ -0,0 +1,13 @@
+#ifndef STORM_STORAGE_DD_ODD_H_
+#define STORM_STORAGE_DD_ODD_H_
+
+#include "src/storage/dd/DdType.h"
+
+namespace storm {
+    namespace dd {
+        // Declare Odd class so we can then specialize it for the different DD types.
+        template<DdType Type> class Odd;
+    }
+}
+
+#endif /* STORM_STORAGE_DD_ODD_H_ */

test/functional/storage/CuddDdTest.cpp

@@ -3,6 +3,7 @@
 #include "src/exceptions/InvalidArgumentException.h"
 #include "src/storage/dd/CuddDdManager.h"
 #include "src/storage/dd/CuddDd.h"
+#include "src/storage/dd/CuddOdd.h"
 #include "src/storage/dd/DdMetaVariable.h"
 
 TEST(CuddDdManager, Constants) {
@@ -375,4 +376,20 @@ TEST(CuddDd, ToExpressionTest) {
         // same value as the current value obtained from the DD.
         EXPECT_FALSE(mintermExpression.evaluateAsBool(&valuation));
     }
+}
+
+TEST(CuddDd, OddTest) {
+    std::shared_ptr<storm::dd::DdManager<storm::dd::DdType::CUDD>> manager(new storm::dd::DdManager<storm::dd::DdType::CUDD>());
+    manager->addMetaVariable("x", 1, 9);
+    
+    storm::dd::Dd<storm::dd::DdType::CUDD> dd = manager->getIdentity("x");
+    storm::dd::Odd<storm::dd::DdType::CUDD> odd;
+    ASSERT_NO_THROW(odd = storm::dd::Odd<storm::dd::DdType::CUDD>(dd));
+    EXPECT_EQ(9, odd.getTotalOffset());
+    std::vector<double> ddAsVector;
+    ASSERT_NO_THROW(ddAsVector = dd.toDoubleVector());
+    EXPECT_EQ(9, ddAsVector.size());
+    for (uint_fast64_t i = 0; i < ddAsVector.size(); ++i) {
+        EXPECT_TRUE(i+1 == ddAsVector[i]);
+    }
 }