same same

Former-commit-id: 8a5597ca6f

src/storage/dd/Bdd.cpp

@@ -37,7 +37,7 @@ namespace storm {
         template<DdType LibraryType>
         template<typename ValueType>
         Bdd<LibraryType> Bdd<LibraryType>::fromVector(std::shared_ptr<DdManager<DdType::CUDD> const> ddManager, std::vector<ValueType> const& values, Odd<DdType::CUDD> const& odd, std::set<storm::expressions::Variable> const& metaVariables, std::function<bool (ValueType const&)> const& filter) {
-            return Bdd<LibraryType>(ddManager, InternalBdd<LibraryType>::fromVector(ddManager, values, odd, metaVariables, filter), metaVariables);
+            return Bdd<LibraryType>(ddManager, InternalBdd<LibraryType>::fromVector(ddManager, values, odd, ddManager->getSortedVariableIndices(metaVariables), filter), metaVariables);
         }
         
         template<DdType LibraryType>

src/storage/dd/Bdd.h

@@ -14,6 +14,7 @@ namespace storm {
         template<DdType LibraryType>
         class Bdd : public Dd<LibraryType> {
         public:
+            friend class DdManager<LibraryType>;
             
             // Instantiate all copy/move constructors/assignments with the default implementation.
             Bdd() = default;

src/storage/dd/DdManager.cpp

@@ -1,13 +1,274 @@
+#include "src/storage/dd/DdManager.h"
 
+#include "src/storage/expressions/ExpressionManager.h"
+
+#include "src/utility/macros.h"
+#include "src/exceptions/InvalidArgumentException.h"
 
 namespace storm {
     namespace dd {
         template<DdType LibraryType>
-        std::vector<uint_fast64_t> Dd<LibraryType>::getSortedVariableIndices(DdManager<LibraryType> const& manager, std::set<storm::expressions::Variable> const& metaVariables) {
+        DdManager<LibraryType>::DdManager() : metaVariableMap(), manager(new storm::expressions::ExpressionManager()), internalDdManager() {
+            // Intentionally left empty.
+        }
+        
+        template<DdType LibraryType>
+        Bdd<LibraryType> DdManager<LibraryType>::getBddOne() const {
+            return Bdd<LibraryType>(this->shared_from_this(), internalDdManager.getBddOne());
+        }
+        
+        template<DdType LibraryType>
+        template<typename ValueType>
+        Add<LibraryType, ValueType> DdManager<LibraryType>::getAddOne() const {
+            return Add<LibraryType, ValueType>(this->shared_from_this(), internalDdManager.template getAddOne<ValueType>());
+        }
+        
+        template<DdType LibraryType>
+        Bdd<LibraryType> DdManager<LibraryType>::getBddZero() const {
+            return Bdd<LibraryType>(this->shared_from_this(), internalDdManager.getBddZero());
+        }
+        
+        template<DdType LibraryType>
+        template<typename ValueType>
+        Add<LibraryType, ValueType> DdManager<LibraryType>::getAddZero() const {
+            return Add<LibraryType, ValueType>(this->shared_from_this(), internalDdManager.template getAddZero<ValueType>());
+        }
+        
+        template<DdType LibraryType>
+        template<typename ValueType>
+        Add<LibraryType, ValueType> DdManager<LibraryType>::getConstant(ValueType const& value) const {
+            return Add<LibraryType, ValueType>(this->shared_from_this(), internalDdManager.constant(value));
+        }
+        
+        template<DdType LibraryType>
+        Bdd<LibraryType> DdManager<LibraryType>::getEncoding(storm::expressions::Variable const& variable, int_fast64_t value) const {
+            DdMetaVariable<LibraryType> const& metaVariable = this->getMetaVariable(variable);
+            
+            STORM_LOG_THROW(value >= metaVariable.getLow() && value <= metaVariable.getHigh(), storm::exceptions::InvalidArgumentException, "Illegal value " << value << " for meta variable '" << variable.getName() << "'.");
+            
+            // Now compute the encoding relative to the low value of the meta variable.
+            value -= metaVariable.getLow();
+            
+            std::vector<Bdd<LibraryType>> const& ddVariables = metaVariable.getDdVariables();
+            
+            Bdd<DdType::CUDD> result;
+            if (value & (1ull << (ddVariables.size() - 1))) {
+                result = ddVariables[0];
+            } else {
+                result = !ddVariables[0];
+            }
+            
+            for (std::size_t i = 1; i < ddVariables.size(); ++i) {
+                if (value & (1ull << (ddVariables.size() - i - 1))) {
+                    result &= ddVariables[i];
+                } else {
+                    result &= !ddVariables[i];
+                }
+            }
+            
+            return result;
+        }
+        
+        template<DdType LibraryType>
+        Bdd<LibraryType> DdManager<LibraryType>::getRange(storm::expressions::Variable const& variable) const {
+            storm::dd::DdMetaVariable<LibraryType> const& metaVariable = this->getMetaVariable(variable);
+            
+            Bdd<LibraryType> result = this->getBddZero();
+            
+            for (int_fast64_t value = metaVariable.getLow(); value <= metaVariable.getHigh(); ++value) {
+                result |= this->getEncoding(variable, value);
+            }
+            
+            return result;
+        }
+
+        template<DdType LibraryType>
+        template<typename ValueType>
+        Add<LibraryType, ValueType> DdManager<LibraryType>::getIdentity(storm::expressions::Variable const& variable) const {
+            storm::dd::DdMetaVariable<LibraryType> const& metaVariable = this->getMetaVariable(variable);
+            
+            Add<LibraryType, ValueType> result = this->getAddZero<ValueType>();
+            for (int_fast64_t value = metaVariable.getLow(); value <= metaVariable.getHigh(); ++value) {
+                result += this->getEncoding(variable, value).toAdd() * this->getConstant(value);
+            }
+            return result;
+        }
+        
+        template<DdType LibraryType>
+        std::pair<storm::expressions::Variable, storm::expressions::Variable> DdManager<LibraryType>::addMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high) {
+            // Check whether the variable name is legal.
+            STORM_LOG_THROW(name != "" && name.back() != '\'', storm::exceptions::InvalidArgumentException, "Illegal name of meta variable: '" << name << "'.");
+            
+            // Check whether a meta variable already exists.
+            STORM_LOG_THROW(!this->hasMetaVariable(name), storm::exceptions::InvalidArgumentException, "A meta variable '" << name << "' already exists.");
+            
+            // Check that the range is legal.
+            STORM_LOG_THROW(high != low, storm::exceptions::InvalidArgumentException, "Range of meta variable must be at least 2 elements.");
+            
+            std::size_t numberOfBits = static_cast<std::size_t>(std::ceil(std::log2(high - low + 1)));
+            
+            storm::expressions::Variable unprimed = manager->declareBitVectorVariable(name, numberOfBits);
+            storm::expressions::Variable primed = manager->declareBitVectorVariable(name + "'", numberOfBits);
+            
+            std::vector<Bdd<LibraryType>> variables;
+            std::vector<Bdd<LibraryType>> variablesPrime;
+            for (std::size_t i = 0; i < numberOfBits; ++i) {
+                auto ddVariablePair = internalDdManager.createNewDdVariablePair();
+                variables.emplace_back(Bdd<DdType::CUDD>(this->shared_from_this(), ddVariablePair.first, {unprimed}));
+                variables.emplace_back(Bdd<DdType::CUDD>(this->shared_from_this(), ddVariablePair.second, {unprimed}));
+            }
+
+            metaVariableMap.emplace(unprimed, DdMetaVariable<LibraryType>(name, low, high, variables, this->shared_from_this()));
+            metaVariableMap.emplace(primed, DdMetaVariable<LibraryType>(name + "'", low, high, variablesPrime, this->shared_from_this()));
+            
+            return std::make_pair(unprimed, primed);
+        }
+        
+        template<DdType LibraryType>
+        std::pair<storm::expressions::Variable, storm::expressions::Variable> DdManager<LibraryType>::addMetaVariable(std::string const& name) {
+            // Check whether the variable name is legal.
+            STORM_LOG_THROW(name != "" && name.back() != '\'', storm::exceptions::InvalidArgumentException, "Illegal name of meta variable: '" << name << "'.");
+            
+            // Check whether a meta variable already exists.
+            STORM_LOG_THROW(!this->hasMetaVariable(name), storm::exceptions::InvalidArgumentException, "A meta variable '" << name << "' already exists.");
+            
+            storm::expressions::Variable unprimed = manager->declareBooleanVariable(name);
+            storm::expressions::Variable primed = manager->declareBooleanVariable(name + "'");
+            
+            std::vector<Bdd<LibraryType>> variables;
+            std::vector<Bdd<LibraryType>> variablesPrime;
+            auto ddVariablePair = internalDdManager.createNewDdVariablePair();
+            variables.emplace_back(Bdd<DdType::CUDD>(this->shared_from_this(), ddVariablePair.first, {unprimed}));
+            variablesPrime.emplace_back(Bdd<DdType::CUDD>(this->shared_from_this(), ddVariablePair.second, {primed}));
+            
+            metaVariableMap.emplace(unprimed, DdMetaVariable<LibraryType>(name, variables, this->shared_from_this()));
+            metaVariableMap.emplace(primed, DdMetaVariable<LibraryType>(name + "'", variablesPrime, this->shared_from_this()));
+            
+            return std::make_pair(unprimed, primed);
+        }
+        
+        template<DdType LibraryType>
+        DdMetaVariable<LibraryType> const& DdManager<LibraryType>::getMetaVariable(storm::expressions::Variable const& variable) const {
+            auto const& variablePair = metaVariableMap.find(variable);
+            
+            // Check whether the meta variable exists.
+            STORM_LOG_THROW(variablePair != metaVariableMap.end(), storm::exceptions::InvalidArgumentException, "Unknown meta variable name '" << variable.getName() << "'.");
+            
+            return variablePair->second;
+        }
+        
+        template<DdType LibraryType>
+        std::set<std::string> DdManager<LibraryType>::getAllMetaVariableNames() const {
+            std::set<std::string> result;
+            for (auto const& variablePair : metaVariableMap) {
+                result.insert(variablePair.first.getName());
+            }
+            return result;
+        }
+        
+        template<DdType LibraryType>
+        std::size_t DdManager<LibraryType>::getNumberOfMetaVariables() const {
+            return this->metaVariableMap.size();
+        }
+        
+        template<DdType LibraryType>
+        bool DdManager<LibraryType>::hasMetaVariable(std::string const& metaVariableName) const {
+            return manager->hasVariable(metaVariableName);
+        }
+        
+        template<DdType LibraryType>
+        storm::expressions::ExpressionManager const& DdManager<LibraryType>::getExpressionManager() const {
+            return *manager;
+        }
+        
+        template<DdType LibraryType>
+        storm::expressions::ExpressionManager& DdManager<LibraryType>::getExpressionManager() {
+            return *manager;
+        }
+        
+        template<DdType LibraryType>
+        std::vector<std::string> DdManager<LibraryType>::getDdVariableNames() const {
+            // First, we initialize a list DD variables and their names.
+            std::vector<std::pair<uint_fast64_t, std::string>> variablePairs;
+            for (auto const& variablePair : this->metaVariableMap) {
+                DdMetaVariable<LibraryType> const& metaVariable = variablePair.second;
+                // If the meta variable is of type bool, we don't need to suffix it with the bit number.
+                if (metaVariable.getType() == MetaVariableType::Bool) {
+                    variablePairs.emplace_back(metaVariable.getDdVariables().front().getIndex(), variablePair.first.getName());
+                } else {
+                    // For integer-valued meta variables, we, however, have to add the suffix.
+                    for (uint_fast64_t variableIndex = 0; variableIndex < metaVariable.getNumberOfDdVariables(); ++variableIndex) {
+                        variablePairs.emplace_back(metaVariable.getDdVariables()[variableIndex].getIndex(), variablePair.first.getName() + '.' + std::to_string(variableIndex));
+                    }
+                }
+            }
+            
+            // Then, we sort this list according to the indices of the ADDs.
+            std::sort(variablePairs.begin(), variablePairs.end(), [](std::pair<uint_fast64_t, std::string> const& a, std::pair<uint_fast64_t, std::string> const& b) { return a.first < b.first; });
+            
+            // Now, we project the sorted vector to its second component.
+            std::vector<std::string> result;
+            for (auto const& element : variablePairs) {
+                result.push_back(element.second);
+            }
+            
+            return result;
+        }
+        
+        template<DdType LibraryType>
+        std::vector<storm::expressions::Variable> DdManager<LibraryType>::getDdVariables() const {
+            // First, we initialize a list DD variables and their names.
+            std::vector<std::pair<uint_fast64_t, storm::expressions::Variable>> variablePairs;
+            for (auto const& variablePair : this->metaVariableMap) {
+                DdMetaVariable<DdType::CUDD> const& metaVariable = variablePair.second;
+                // If the meta variable is of type bool, we don't need to suffix it with the bit number.
+                if (metaVariable.getType() == MetaVariableType::Bool) {
+                    variablePairs.emplace_back(metaVariable.getDdVariables().front().getIndex(), variablePair.first);
+                } else {
+                    // For integer-valued meta variables, we, however, have to add the suffix.
+                    for (uint_fast64_t variableIndex = 0; variableIndex < metaVariable.getNumberOfDdVariables(); ++variableIndex) {
+                        variablePairs.emplace_back(metaVariable.getDdVariables()[variableIndex].getIndex(), variablePair.first);
+                    }
+                }
+            }
+            
+            // Then, we sort this list according to the indices of the ADDs.
+            std::sort(variablePairs.begin(), variablePairs.end(), [](std::pair<uint_fast64_t, storm::expressions::Variable> const& a, std::pair<uint_fast64_t, storm::expressions::Variable> const& b) { return a.first < b.first; });
+            
+            // Now, we project the sorted vector to its second component.
+            std::vector<storm::expressions::Variable> result;
+            for (auto const& element : variablePairs) {
+                result.push_back(element.second);
+            }
+            
+            return result;
+        }
+        
+        template<DdType LibraryType>
+        void DdManager<LibraryType>::allowDynamicReordering(bool value) {
+            internalDdManager.allowDynamicReordering(value);
+        }
+        
+        template<DdType LibraryType>
+        bool DdManager<LibraryType>::isDynamicReorderingAllowed() const {
+            return internalDdManager.isDynamicReorderingAllowed();
+        }
+        
+        template<DdType LibraryType>
+        void DdManager<LibraryType>::triggerReordering() {
+            internalDdManager.triggerReordering();
+        }
+        
+        template<DdType LibraryType>
+        std::shared_ptr<DdManager<LibraryType> const> DdManager<LibraryType>::asSharedPointer() const {
+            return this->shared_from_this();
+        }
+        
+        template<DdType LibraryType>
+        std::vector<uint_fast64_t> DdManager<LibraryType>::getSortedVariableIndices(std::set<storm::expressions::Variable> const& metaVariables) {
             std::vector<uint_fast64_t> ddVariableIndices;
-            for (auto const& metaVariableName : metaVariables) {
-                auto const& metaVariable = manager.getMetaVariable(metaVariableName);
-                for (auto const& ddVariable : metaVariable.getDdVariables()) {
+            for (auto const& metaVariable : metaVariableMap) {
+                for (auto const& ddVariable : metaVariable.second.getDdVariables()) {
                     ddVariableIndices.push_back(ddVariable.getIndex());
                 }
             }
@@ -16,5 +277,17 @@ namespace storm {
             std::sort(ddVariableIndices.begin(), ddVariableIndices.end());
             return ddVariableIndices;
         }
+        
+        template<DdType LibraryType>
+        InternalDdManager<LibraryType>& DdManager<LibraryType>::getInternalDdManager() {
+            return internalDdManager;
+        }
+        
+        template<DdType LibraryType>
+        InternalDdManager<LibraryType> const& DdManager<LibraryType>::getInternalDdManager() const {
+            return internalDdManager;
+        }
+        
+        template class DdManager<DdType::CUDD>;
     }
 }

src/storage/dd/DdManager.h

@@ -1,20 +1,174 @@
 #ifndef STORM_STORAGE_DD_DDMANAGER_H_
 #define STORM_STORAGE_DD_DDMANAGER_H_
 
+#include <set>
+#include <unordered_map>
+
 #include "src/storage/dd/DdType.h"
 #include "src/storage/dd/DdMetaVariable.h"
+#include "src/storage/dd/Bdd.h"
+#include "src/storage/dd/Add.h"
+
 #include "src/storage/expressions/Variable.h"
 
+#include "src/storage/dd/cudd/InternalCuddDdManager.h"
+
 namespace storm {
     namespace dd {
         // Declare DdManager class so we can then specialize it for the different DD types.
         template<DdType LibraryType>
-        class DdManager {
+        class DdManager : public std::enable_shared_from_this<DdManager<LibraryType>> {
         public:
+            /*!
+             * Creates an empty manager without any meta variables.
+             */
+            DdManager();
+            
+            // Explictly forbid copying a DdManager, but allow moving it.
+            DdManager(DdManager<LibraryType> const& other) = delete;
+            DdManager<LibraryType>& operator=(DdManager<LibraryType> const& other) = delete;
+            DdManager(DdManager<LibraryType>&& other) = default;
+            DdManager<LibraryType>& operator=(DdManager<LibraryType>&& other) = default;
+            
+            /*!
+             * Retrieves a BDD representing the constant one function.
+             *
+             * @return A BDD representing the constant one function.
+             */
             Bdd<LibraryType> getBddOne() const;
+            
+            /*!
+             * Retrieves an ADD representing the constant one function.
+             *
+             * @return An ADD representing the constant one function.
+             */
+            template<typename ValueType>
+            Add<LibraryType, ValueType> getAddOne() const;
+            
+            /*!
+             * Retrieves a BDD representing the constant zero function.
+             *
+             * @return A BDD representing the constant zero function.
+             */
             Bdd<LibraryType> getBddZero() const;
+            
+            /*!
+             * Retrieves an ADD representing the constant zero function.
+             *
+             * @return An ADD representing the constant zero function.
+             */
+            template<typename ValueType>
+            Add<LibraryType, ValueType> getAddZero() const;
+            
+            /*!
+             * Retrieves an ADD representing the constant function with the given value.
+             *
+             * @return An ADD representing the constant function with the given value.
+             */
+            template<typename ValueType>
+            Add<LibraryType, ValueType> getConstant(ValueType const& value) const;
+            
+            /*!
+             * Retrieves the BDD representing the function that maps all inputs which have the given meta variable equal
+             * to the given value one.
+             *
+             * @param variable The expression variable associated with the meta variable.
+             * @param value The value the meta variable is supposed to have.
+             * @return The DD representing the function that maps all inputs which have the given meta variable equal
+             * to the given value one.
+             */
+            Bdd<LibraryType> getEncoding(storm::expressions::Variable const& variable, int_fast64_t value) const;
+            
+            /*!
+             * Retrieves the BDD representing the range of the meta variable, i.e., a function that maps all legal values
+             * of the range of the meta variable to one.
+             *
+             * @param variable The expression variable associated with the meta variable.
+             * @return The range of the meta variable.
+             */
+            Bdd<LibraryType> getRange(storm::expressions::Variable const& variable) const;
+            
+            /*!
+             * Retrieves the ADD representing the identity of the meta variable, i.e., a function that maps all legal
+             * values of the range of the meta variable to themselves.
+             *
+             * @param variable The expression variable associated with the meta variable.
+             * @return The identity of the meta variable.
+             */
+            template<typename ValueType>
+            Add<LibraryType, ValueType> getIdentity(storm::expressions::Variable const& variable) const;
+            
+            /*!
+             * Adds an integer meta variable with the given range.
+             *
+             * @param variableName The name of the new variable.
+             * @param low The lowest value of the range of the variable.
+             * @param high The highest value of the range of the variable.
+             */
+            std::pair<storm::expressions::Variable, storm::expressions::Variable> addMetaVariable(std::string const& variableName, int_fast64_t low, int_fast64_t high);
+            
+            /*!
+             * Adds a boolean meta variable.
+             *
+             * @param variableName The name of the new variable.
+             */
+            std::pair<storm::expressions::Variable, storm::expressions::Variable> addMetaVariable(std::string const& variableName);
+            
+            /*!
+             * Retrieves the names of all meta variables that have been added to the manager.
+             *
+             * @return The set of all meta variable names of the manager.
+             */
+            std::set<std::string> getAllMetaVariableNames() const;
+            
+            /*!
+             * Retrieves the number of meta variables that are contained in this manager.
+             *
+             * @return The number of meta variables contained in this manager.
+             */
+            std::size_t getNumberOfMetaVariables() const;
+            
+            /*!
+             * Retrieves whether the given meta variable name is already in use.
+             *
+             * @param variableName The name of the variable.
+             * @return True if the given meta variable name is managed by this manager.
+             */
+            bool hasMetaVariable(std::string const& variableName) const;
+            
+            /*!
+             * Sets whether or not dynamic reordering is allowed for the DDs managed by this manager.
+             *
+             * @param value If set to true, dynamic reordering is allowed and forbidden otherwise.
+             */
+            void allowDynamicReordering(bool value);
+            
+            /*!
+             * Retrieves whether dynamic reordering is currently allowed.
+             *
+             * @return True iff dynamic reordering is currently allowed.
+             */
+            bool isDynamicReorderingAllowed() const;
+            
+            /*!
+             * Triggers a reordering of the DDs managed by this manager.
+             */
+            void triggerReordering();
+            
+            /*!
+             * Retrieves the meta variable with the given name if it exists.
+             *
+             * @param variable The expression variable associated with the meta variable.
+             * @return The corresponding meta variable.
+             */
             DdMetaVariable<LibraryType> const& getMetaVariable(storm::expressions::Variable const& variable) const;
-            std::vector<std::string> getDdVariableNames() const;
+            
+            /*!
+             * Retrieves the manager as a shared pointer.
+             *
+             * @return A shared pointer to the manager.
+             */
+            std::shared_ptr<DdManager<LibraryType> const> asSharedPointer() const;
             
             /*!
              * Retrieves the (sorted) list of the variable indices of the DD variables given by the meta variable set.
@@ -23,7 +177,59 @@ namespace storm {
              * @param metaVariable The set of meta variables for which to retrieve the index list.
              * @return The sorted list of variable indices.
              */
-            static std::vector<uint_fast64_t> getSortedVariableIndices(std::set<storm::expressions::Variable> const& metaVariables);
+            std::vector<uint_fast64_t> getSortedVariableIndices(std::set<storm::expressions::Variable> const& metaVariables);
+            
+            /*!
+             * Retrieves the internal DD manager.
+             *
+             * @return The internal DD manager.
+             */
+            InternalDdManager<LibraryType>& getInternalDdManager();
+
+            /*!
+             * Retrieves the internal DD manager.
+             *
+             * @return The internal DD manager.
+             */
+            InternalDdManager<LibraryType> const& getInternalDdManager() const;
+
+        private:
+            /*!
+             * Retrieves a list of names of the DD variables in the order of their index.
+             *
+             * @return A list of DD variable names.
+             */
+            std::vector<std::string> getDdVariableNames() const;
+            
+            /*!
+             * Retrieves a list of expression variables in the order of their index.
+             *
+             * @return A list of DD variables.
+             */
+            std::vector<storm::expressions::Variable> getDdVariables() const;
+            
+            /*!
+             * Retrieves the underlying expression manager.
+             *
+             * @return The underlying expression manager.
+             */
+            storm::expressions::ExpressionManager const& getExpressionManager() const;
+            
+            /*!
+             * Retrieves the underlying expression manager.
+             *
+             * @return The underlying expression manager.
+             */
+            storm::expressions::ExpressionManager& getExpressionManager();
+            
+            // A mapping from variables to the meta variable information.
+            std::unordered_map<storm::expressions::Variable, DdMetaVariable<LibraryType>> metaVariableMap;
+            
+            // The manager responsible for the variables.
+            std::shared_ptr<storm::expressions::ExpressionManager> manager;
+            
+            // The DD manager that is customized according to the selected library type.
+            InternalDdManager<LibraryType> internalDdManager;
         };
     }
 }

src/storage/dd/DdMetaVariable.cpp

@@ -0,0 +1,62 @@
+#include "src/storage/dd/DdMetaVariable.h"
+
+namespace storm {
+    namespace dd {
+        template<DdType LibraryType>
+        DdMetaVariable<LibraryType>::DdMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high, std::vector<Bdd<LibraryType>> const& ddVariables) : name(name), type(MetaVariableType::Int), low(low), high(high), ddVariables(ddVariables) {
+            this->createCube();
+        }
+        
+        template<DdType LibraryType>
+        DdMetaVariable<LibraryType>::DdMetaVariable(std::string const& name, std::vector<Bdd<LibraryType>> const& ddVariables) : name(name), type(MetaVariableType::Bool), low(0), high(1), ddVariables(ddVariables) {
+            this->createCube();
+        }
+        
+        template<DdType LibraryType>
+        std::string const& DdMetaVariable<LibraryType>::getName() const {
+            return this->name;
+        }
+        
+        template<DdType LibraryType>
+        MetaVariableType DdMetaVariable<LibraryType>::getType() const {
+            return this->type;
+        }
+        
+        template<DdType LibraryType>
+        int_fast64_t DdMetaVariable<LibraryType>::getLow() const {
+            return this->low;
+        }
+        
+        template<DdType LibraryType>
+        int_fast64_t DdMetaVariable<LibraryType>::getHigh() const {
+            return this->high;
+        }
+        
+        template<DdType LibraryType>
+        std::size_t DdMetaVariable<LibraryType>::getNumberOfDdVariables() const {
+            return this->ddVariables.size();
+        }
+        
+        template<DdType LibraryType>
+        std::vector<Bdd<LibraryType>> const& DdMetaVariable<LibraryType>::getDdVariables() const {
+            return this->ddVariables;
+        }
+        
+        template<DdType LibraryType>
+        Bdd<LibraryType> const& DdMetaVariable<LibraryType>::getCube() const {
+            return this->cube;
+        }
+        
+        template<DdType LibraryType>
+        void DdMetaVariable<LibraryType>::createCube() {
+            auto it = this->ddVariables.begin();
+            this->cube = *it;
+            ++it;
+            for (auto ite = this->ddVariables.end(); it != ite; ++it) {
+                this->cube &= *it;
+            }
+        }
+        
+        template class DdMetaVariable<DdType::CUDD>;
+    }
+}

src/storage/dd/DdMetaVariable.h

@@ -4,15 +4,113 @@
 #include <vector>
 
 #include "src/storage/dd/DdType.h"
+#include "src/storage/dd/Bdd.h"
 
 namespace storm {
     namespace dd {
+        template<DdType LibraryType>
+        class DdManager;
+        
+        // An enumeration for all legal types of meta variables.
+        enum class MetaVariableType { Bool, Int };
+        
         // Declare DdMetaVariable class so we can then specialize it for the different DD types.
         template<DdType LibraryType>
         class DdMetaVariable {
         public:
-            Bdd<LibraryType> getCube() const;
-            uint_fast64_t getNumberOfDdVariables() const;
+            friend class DdManager<LibraryType>;
+            
+            /*!
+             * Retrieves the name of the meta variable.
+             *
+             * @return The name of the variable.
+             */
+            std::string const& getName() const;
+            
+            /*!
+             * Retrieves the type of the meta variable.
+             *
+             * @return The type of the meta variable.
+             */
+            MetaVariableType getType() const;
+            
+            /*!
+             * Retrieves the lowest value of the range of the variable.
+             *
+             * @return The lowest value of the range of the variable.
+             */
+            int_fast64_t getLow() const;
+            
+            /*!
+             * Retrieves the highest value of the range of the variable.
+             *
+             * @return The highest value of the range of the variable.
+             */
+            int_fast64_t getHigh() const;
+
+            /*!
+             * Retrieves the number of DD variables for this meta variable.
+             *
+             * @return The number of DD variables for this meta variable.
+             */
+            std::size_t getNumberOfDdVariables() const;
+
+            /*!
+             * Retrieves the cube of all variables that encode this meta variable.
+             *
+             * @return The cube of all variables that encode this meta variable.
+             */
+            Bdd<LibraryType> const& getCube() const;
+            
+        private:
+            /*!
+             * Creates an integer meta variable with the given name and range bounds.
+             *
+             * @param name The name of the meta variable.
+             * @param low The lowest value of the range of the variable.
+             * @param high The highest value of the range of the variable.
+             * @param ddVariables The vector of variables used to encode this variable.
+             * @param manager A pointer to the manager that is responsible for this meta variable.
+             */
+            DdMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high, std::vector<Bdd<LibraryType>> const& ddVariables);
+            
+            /*!
+             * Creates a boolean meta variable with the given name.
+             * @param name The name of the meta variable.
+             * @param ddVariables The vector of variables used to encode this variable.
+             * @param manager A pointer to the manager that is responsible for this meta variable.
+             */
+            DdMetaVariable(std::string const& name, std::vector<Bdd<LibraryType>> const& ddVariables);
+            
+            /*!
+             * Retrieves the variables used to encode the meta variable.
+             *
+             * @return A vector of variables used to encode the meta variable.
+             */
+            std::vector<Bdd<LibraryType>> const& getDdVariables() const;
+            
+            /*!
+             * Creates the cube for this meta variable from the DD variables.
+             */
+            void createCube();
+            
+            // The name of the meta variable.
+            std::string name;
+            
+            // The type of the variable.
+            MetaVariableType type;
+            
+            // The lowest value of the range of the variable.
+            int_fast64_t low;
+            
+            // The highest value of the range of the variable.
+            int_fast64_t high;
+            
+            // The vector of variables that are used to encode the meta variable.
+            std::vector<Bdd<DdType::CUDD>> ddVariables;
+            
+            // The cube consisting of all variables that encode the meta variable.
+            Bdd<DdType::CUDD> cube;
         };
     }
 }

src/storage/dd/InternalDdManager.h

@@ -0,0 +1,14 @@
+#ifndef STORM_STORAGE_DD_INTERNALDDMANAGER_H_
+#define STORM_STORAGE_DD_INTERNALDDMANAGER_H_
+
+#include "src/storage/dd/DdType.h"
+
+namespace storm {
+    namespace dd {
+        template <storm::dd::DdType LibraryType>
+        class InternalDdManager;
+    }
+}
+
+
+#endif /* STORM_STORAGE_DD_INTERNALDDMANAGER_H_ */

src/storage/dd/cudd/CuddDdManager.cpp

@@ -15,258 +15,18 @@
 
 namespace storm {
     namespace dd {
-        DdManager<DdType::CUDD>::DdManager() : metaVariableMap(), cuddManager(), reorderingTechnique(CUDD_REORDER_NONE), manager(new storm::expressions::ExpressionManager()) {
-            this->cuddManager.SetMaxMemory(static_cast<unsigned long>(storm::settings::cuddSettings().getMaximalMemory() * 1024ul * 1024ul));
-            this->cuddManager.SetEpsilon(storm::settings::cuddSettings().getConstantPrecision());
-            
-            // Now set the selected reordering technique.
-            storm::settings::modules::CuddSettings::ReorderingTechnique reorderingTechniqueAsSetting = storm::settings::cuddSettings().getReorderingTechnique();
-            switch (reorderingTechniqueAsSetting) {
-                case storm::settings::modules::CuddSettings::ReorderingTechnique::None: this->reorderingTechnique = CUDD_REORDER_NONE; break;
-                case storm::settings::modules::CuddSettings::ReorderingTechnique::Random: this->reorderingTechnique = CUDD_REORDER_RANDOM; break;
-                case storm::settings::modules::CuddSettings::ReorderingTechnique::RandomPivot: this->reorderingTechnique = CUDD_REORDER_RANDOM_PIVOT; break;
-                case storm::settings::modules::CuddSettings::ReorderingTechnique::Sift: this->reorderingTechnique = CUDD_REORDER_SIFT; break;
-                case storm::settings::modules::CuddSettings::ReorderingTechnique::SiftConv: this->reorderingTechnique = CUDD_REORDER_SIFT_CONVERGE; break;
-                case storm::settings::modules::CuddSettings::ReorderingTechnique::SymmetricSift: this->reorderingTechnique = CUDD_REORDER_SYMM_SIFT; break;
-                case storm::settings::modules::CuddSettings::ReorderingTechnique::SymmetricSiftConv: this->reorderingTechnique = CUDD_REORDER_SYMM_SIFT_CONV; break;
-                case storm::settings::modules::CuddSettings::ReorderingTechnique::GroupSift: this->reorderingTechnique = CUDD_REORDER_GROUP_SIFT; break;
-                case storm::settings::modules::CuddSettings::ReorderingTechnique::GroupSiftConv: this->reorderingTechnique = CUDD_REORDER_GROUP_SIFT_CONV; break;
-                case storm::settings::modules::CuddSettings::ReorderingTechnique::Win2: this->reorderingTechnique = CUDD_REORDER_WINDOW2; break;
-                case storm::settings::modules::CuddSettings::ReorderingTechnique::Win2Conv: this->reorderingTechnique = CUDD_REORDER_WINDOW2_CONV; break;
-                case storm::settings::modules::CuddSettings::ReorderingTechnique::Win3: this->reorderingTechnique = CUDD_REORDER_WINDOW3; break;
-                case storm::settings::modules::CuddSettings::ReorderingTechnique::Win3Conv: this->reorderingTechnique = CUDD_REORDER_WINDOW3_CONV; break;
-                case storm::settings::modules::CuddSettings::ReorderingTechnique::Win4: this->reorderingTechnique = CUDD_REORDER_WINDOW4; break;
-                case storm::settings::modules::CuddSettings::ReorderingTechnique::Win4Conv: this->reorderingTechnique = CUDD_REORDER_WINDOW4_CONV; break;
-                case storm::settings::modules::CuddSettings::ReorderingTechnique::Annealing: this->reorderingTechnique = CUDD_REORDER_ANNEALING; break;
-                case storm::settings::modules::CuddSettings::ReorderingTechnique::Genetic: this->reorderingTechnique = CUDD_REORDER_GENETIC; break;
-                case storm::settings::modules::CuddSettings::ReorderingTechnique::Exact: this->reorderingTechnique = CUDD_REORDER_EXACT; break;
-            }
-        }
-        
-        Bdd<DdType::CUDD> DdManager<DdType::CUDD>::getBddOne() const {
-            return Bdd<DdType::CUDD>(this->shared_from_this(), cuddManager.bddOne());
-        }
 
-        Add<DdType::CUDD> DdManager<DdType::CUDD>::getAddOne() const {
-            return Add<DdType::CUDD>(this->shared_from_this(), cuddManager.addOne());
-        }
-        
-        Bdd<DdType::CUDD> DdManager<DdType::CUDD>::getBddZero() const {
-            return Bdd<DdType::CUDD>(this->shared_from_this(), cuddManager.bddZero());
-        }
-        
-        Add<DdType::CUDD> DdManager<DdType::CUDD>::getAddZero() const {
-            return Add<DdType::CUDD>(this->shared_from_this(), cuddManager.addZero());
-        }
-        
-        
-        Add<DdType::CUDD> DdManager<DdType::CUDD>::getConstant(double value) const {
-            return Add<DdType::CUDD>(this->shared_from_this(), cuddManager.constant(value));
-        }
-        
-        Bdd<DdType::CUDD> DdManager<DdType::CUDD>::getEncoding(storm::expressions::Variable const& variable, int_fast64_t value) const {
-            DdMetaVariable<DdType::CUDD> const& metaVariable = this->getMetaVariable(variable);
-            
-            STORM_LOG_THROW(value >= metaVariable.getLow() && value <= metaVariable.getHigh(), storm::exceptions::InvalidArgumentException, "Illegal value " << value << " for meta variable '" << variable.getName() << "'.");
-            
-            // Now compute the encoding relative to the low value of the meta variable.
-            value -= metaVariable.getLow();
-            
-            std::vector<Bdd<DdType::CUDD>> const& ddVariables = metaVariable.getDdVariables();
 
-            Bdd<DdType::CUDD> result;
-            if (value & (1ull << (ddVariables.size() - 1))) {
-                result = ddVariables[0];
-            } else {
-                result = !ddVariables[0];
-            }
-            
-            for (std::size_t i = 1; i < ddVariables.size(); ++i) {
-                if (value & (1ull << (ddVariables.size() - i - 1))) {
-                    result &= ddVariables[i];
-                } else {
-                    result &= !ddVariables[i];
-                }
-            }
-            
-            return result;
-        }
         
-        Bdd<DdType::CUDD> DdManager<DdType::CUDD>::getRange(storm::expressions::Variable const& variable) const {
-            storm::dd::DdMetaVariable<DdType::CUDD> const& metaVariable = this->getMetaVariable(variable);
-            
-            Bdd<DdType::CUDD> result = this->getBddZero();
-            
-            for (int_fast64_t value = metaVariable.getLow(); value <= metaVariable.getHigh(); ++value) {
-                result |= this->getEncoding(variable, value);
-            }
-            
-            return result;
-        }
         
-        Add<DdType::CUDD> DdManager<DdType::CUDD>::getIdentity(storm::expressions::Variable const& variable) const {
-            storm::dd::DdMetaVariable<DdType::CUDD> const& metaVariable = this->getMetaVariable(variable);
-            
-            Add<DdType::CUDD> result = this->getAddZero();
-            for (int_fast64_t value = metaVariable.getLow(); value <= metaVariable.getHigh(); ++value) {
-                result += this->getEncoding(variable, value).toAdd() * this->getConstant(value);
-            }
-            return result;
-        }
-
-        std::pair<storm::expressions::Variable, storm::expressions::Variable> DdManager<DdType::CUDD>::addMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high) {
-            // Check whether the variable name is legal.
-            STORM_LOG_THROW(name != "" && name.back() != '\'', storm::exceptions::InvalidArgumentException, "Illegal name of meta variable: '" << name << "'.");
-            
-            // Check whether a meta variable already exists.
-            STORM_LOG_THROW(!this->hasMetaVariable(name), storm::exceptions::InvalidArgumentException, "A meta variable '" << name << "' already exists.");
 
-            // Check that the range is legal.
-            STORM_LOG_THROW(high != low, storm::exceptions::InvalidArgumentException, "Range of meta variable must be at least 2 elements.");
-            
-            std::size_t numberOfBits = static_cast<std::size_t>(std::ceil(std::log2(high - low + 1)));
-            
-            storm::expressions::Variable unprimed = manager->declareBitVectorVariable(name, numberOfBits);
-            storm::expressions::Variable primed = manager->declareBitVectorVariable(name + "'", numberOfBits);
-            
-            std::vector<Bdd<DdType::CUDD>> variables;
-            std::vector<Bdd<DdType::CUDD>> variablesPrime;
-            for (std::size_t i = 0; i < numberOfBits; ++i) {
-                variables.emplace_back(Bdd<DdType::CUDD>(this->shared_from_this(), cuddManager.bddVar(), {unprimed}));
-                variablesPrime.emplace_back(Bdd<DdType::CUDD>(this->shared_from_this(), cuddManager.bddVar(), {primed}));
-            }
-            
-            // Now group the non-primed and primed variable.
-            for (uint_fast64_t i = 0; i < numberOfBits; ++i) {
-                this->getCuddManager().MakeTreeNode(variables[i].getIndex(), 2, MTR_FIXED);
-            }
-            
-            metaVariableMap.emplace(unprimed, DdMetaVariable<DdType::CUDD>(name, low, high, variables, this->shared_from_this()));
-            metaVariableMap.emplace(primed, DdMetaVariable<DdType::CUDD>(name + "'", low, high, variablesPrime, this->shared_from_this()));
-            
-            return std::make_pair(unprimed, primed);
-        }
         
-        std::pair<storm::expressions::Variable, storm::expressions::Variable> DdManager<DdType::CUDD>::addMetaVariable(std::string const& name) {
-            // Check whether the variable name is legal.
-            STORM_LOG_THROW(name != "" && name.back() != '\'', storm::exceptions::InvalidArgumentException, "Illegal name of meta variable: '" << name << "'.");
-            
-            // Check whether a meta variable already exists.
-            STORM_LOG_THROW(!this->hasMetaVariable(name), storm::exceptions::InvalidArgumentException, "A meta variable '" << name << "' already exists.");
-            
-            storm::expressions::Variable unprimed = manager->declareBooleanVariable(name);
-            storm::expressions::Variable primed = manager->declareBooleanVariable(name + "'");
 
-            std::vector<Bdd<DdType::CUDD>> variables;
-            std::vector<Bdd<DdType::CUDD>> variablesPrime;
-            variables.emplace_back(Bdd<DdType::CUDD>(this->shared_from_this(), cuddManager.bddVar(), {unprimed}));
-            variablesPrime.emplace_back(Bdd<DdType::CUDD>(this->shared_from_this(), cuddManager.bddVar(), {primed}));
-
-            // Now group the non-primed and primed variable.
-            this->getCuddManager().MakeTreeNode(variables.front().getIndex(), 2, MTR_FIXED);
-            
-            metaVariableMap.emplace(unprimed, DdMetaVariable<DdType::CUDD>(name, variables, this->shared_from_this()));
-            metaVariableMap.emplace(primed, DdMetaVariable<DdType::CUDD>(name + "'", variablesPrime, this->shared_from_this()));
-            
-            return std::make_pair(unprimed, primed);
-        }
-        
-        DdMetaVariable<DdType::CUDD> const& DdManager<DdType::CUDD>::getMetaVariable(storm::expressions::Variable const& variable) const {
-            auto const& variablePair = metaVariableMap.find(variable);
-            
-            // Check whether the meta variable exists.
-            STORM_LOG_THROW(variablePair != metaVariableMap.end(), storm::exceptions::InvalidArgumentException, "Unknown meta variable name '" << variable.getName() << "'.");
-            
-            return variablePair->second;
-        }
-        
-        std::set<std::string> DdManager<DdType::CUDD>::getAllMetaVariableNames() const {
-            std::set<std::string> result;
-            for (auto const& variablePair : metaVariableMap) {
-                result.insert(variablePair.first.getName());
-            }
-            return result;
-        }
-        
-        std::size_t DdManager<DdType::CUDD>::getNumberOfMetaVariables() const {
-            return this->metaVariableMap.size();
-        }
         
-        bool DdManager<DdType::CUDD>::hasMetaVariable(std::string const& metaVariableName) const {
-            return manager->hasVariable(metaVariableName);
-        }
         
-        Cudd& DdManager<DdType::CUDD>::getCuddManager() {
-            return this->cuddManager;
-        }
 
-        Cudd const& DdManager<DdType::CUDD>::getCuddManager() const {
-            return this->cuddManager;
-        }
         
-        storm::expressions::ExpressionManager const& DdManager<DdType::CUDD>::getExpressionManager() const {
-            return *manager;
-        }
-        
-        storm::expressions::ExpressionManager& DdManager<DdType::CUDD>::getExpressionManager() {
-            return *manager;
-        }
-        
-        std::vector<std::string> DdManager<DdType::CUDD>::getDdVariableNames() const {
-            // First, we initialize a list DD variables and their names.
-            std::vector<std::pair<uint_fast64_t, std::string>> variablePairs;
-            for (auto const& variablePair : this->metaVariableMap) {
-                DdMetaVariable<DdType::CUDD> const& metaVariable = variablePair.second;
-                // If the meta variable is of type bool, we don't need to suffix it with the bit number.
-                if (metaVariable.getType() == DdMetaVariable<storm::dd::DdType::CUDD>::MetaVariableType::Bool) {
-                    variablePairs.emplace_back(metaVariable.getDdVariables().front().getIndex(), variablePair.first.getName());
-                } else {
-                    // For integer-valued meta variables, we, however, have to add the suffix.
-                    for (uint_fast64_t variableIndex = 0; variableIndex < metaVariable.getNumberOfDdVariables(); ++variableIndex) {
-                        variablePairs.emplace_back(metaVariable.getDdVariables()[variableIndex].getIndex(), variablePair.first.getName() + '.' + std::to_string(variableIndex));
-                    }
-                }
-            }
-            
-            // Then, we sort this list according to the indices of the ADDs.
-            std::sort(variablePairs.begin(), variablePairs.end(), [](std::pair<uint_fast64_t, std::string> const& a, std::pair<uint_fast64_t, std::string> const& b) { return a.first < b.first; });
-            
-            // Now, we project the sorted vector to its second component.
-            std::vector<std::string> result;
-            for (auto const& element : variablePairs) {
-                result.push_back(element.second);
-            }
-            
-            return result;
-        }
-        
-        std::vector<storm::expressions::Variable> DdManager<DdType::CUDD>::getDdVariables() const {
-            // First, we initialize a list DD variables and their names.
-            std::vector<std::pair<uint_fast64_t, storm::expressions::Variable>> variablePairs;
-            for (auto const& variablePair : this->metaVariableMap) {
-                DdMetaVariable<DdType::CUDD> const& metaVariable = variablePair.second;
-                // If the meta variable is of type bool, we don't need to suffix it with the bit number.
-                if (metaVariable.getType() == DdMetaVariable<storm::dd::DdType::CUDD>::MetaVariableType::Bool) {
-                    variablePairs.emplace_back(metaVariable.getDdVariables().front().getIndex(), variablePair.first);
-                } else {
-                    // For integer-valued meta variables, we, however, have to add the suffix.
-                    for (uint_fast64_t variableIndex = 0; variableIndex < metaVariable.getNumberOfDdVariables(); ++variableIndex) {
-                        variablePairs.emplace_back(metaVariable.getDdVariables()[variableIndex].getIndex(), variablePair.first);
-                    }
-                }
-            }
-            
-            // Then, we sort this list according to the indices of the ADDs.
-            std::sort(variablePairs.begin(), variablePairs.end(), [](std::pair<uint_fast64_t, storm::expressions::Variable> const& a, std::pair<uint_fast64_t, storm::expressions::Variable> const& b) { return a.first < b.first; });
-            
-            // Now, we project the sorted vector to its second component.
-            std::vector<storm::expressions::Variable> result;
-            for (auto const& element : variablePairs) {
-                result.push_back(element.second);
-            }
-            
-            return result;
-        }
+
         
         void DdManager<DdType::CUDD>::allowDynamicReordering(bool value) {
             if (value) {

src/storage/dd/cudd/CuddDdManager.h

@@ -191,20 +191,6 @@ namespace storm {
              */
             std::vector<storm::expressions::Variable> getDdVariables() const;
             
-            /*!
-             * Retrieves the underlying CUDD manager.
-             *
-             * @return The underlying CUDD manager.
-             */
-            Cudd& getCuddManager();
-            
-            /*!
-             * Retrieves the underlying CUDD manager.
-             *
-             * @return The underlying CUDD manager.
-             */
-            Cudd const& getCuddManager() const;
-            
             /*!
              * Retrieves the underlying expression manager.
              *
@@ -221,12 +207,6 @@ namespace storm {
             
             // A mapping from variables to the meta variable information.
             std::unordered_map<storm::expressions::Variable, DdMetaVariable<DdType::CUDD>> metaVariableMap;
-            
-            // The manager responsible for the DDs created/modified with this DdManager.
-            Cudd cuddManager;
-            
-            // The technique that is used for dynamic reordering.
-            Cudd_ReorderingType reorderingTechnique;
 
             // The manager responsible for the variables.
             std::shared_ptr<storm::expressions::ExpressionManager> manager;

src/storage/dd/cudd/InternalCuddBdd.cpp

@@ -1,16 +1,17 @@
 #include "src/storage/dd/cudd/InternalCuddBdd.h"
 
+#include "src/storage/dd/cudd/InternalCuddDdManager.h"
+
 namespace storm {
     namespace dd {
-        InternalBdd<DdType::CUDD>::InternalBdd(std::shared_ptr<DdManager<DdType::CUDD> const> ddManager, BDD cuddBdd) : ddManager(ddManager), cuddBdd(cuddBdd) {
+        InternalBdd<DdType::CUDD>::InternalBdd(InternalDdManager<DdType::CUDD> const* ddManager, BDD cuddBdd) : ddManager(ddManager), cuddBdd(cuddBdd) {
             // Intentionally left empty.
         }
         
         template<typename ValueType>
-        InternalBdd<DdType::CUDD> InternalBdd<DdType::CUDD>::fromVector(std::shared_ptr<DdManager<DdType::CUDD> const> ddManager, std::vector<ValueType> const& values, Odd<DdType::CUDD> const& odd, std::set<storm::expressions::Variable> const& metaVariables, std::function<bool (ValueType const&)> const& filter) {
-            std::vector<uint_fast64_t> ddVariableIndices = ddManager->getSortedVariableIndices(metaVariables);
+        InternalBdd<DdType::CUDD> InternalBdd<DdType::CUDD>::fromVector(InternalDdManager<DdType::CUDD> const* ddManager, std::vector<ValueType> const& values, Odd<DdType::CUDD> const& odd, std::vector<uint_fast64_t> const& sortedDdVariableIndices, std::function<bool (ValueType const&)> const& filter) {
             uint_fast64_t offset = 0;
-            return BDD(ddManager->getCuddManager(), fromVectorRec(ddManager->getCuddManager().getManager(), offset, 0, ddVariableIndices.size(), values, odd, ddVariableIndices, filter));
+            return InternalBdd<DdType::CUDD>(ddManager, BDD(ddManager->getCuddManager(), fromVectorRec(ddManager->getCuddManager().getManager(), offset, 0, sortedDdVariableIndices.size(), values, odd, sortedDdVariableIndices, filter)));
         }
         
         bool InternalBdd<DdType::CUDD>::operator==(InternalBdd<DdType::CUDD> const& other) const {
@@ -22,7 +23,7 @@ namespace storm {
         }
         
         InternalBdd<DdType::CUDD> InternalBdd<DdType::CUDD>::ite(InternalBdd<DdType::CUDD> const& thenDd, InternalBdd<DdType::CUDD> const& elseDd) const {
-            return InternalBdd<DdType::CUDD>(this->getCuddBdd().Ite(thenDd.getCuddBdd(), elseDd.getCuddBdd()));
+            return InternalBdd<DdType::CUDD>(ddManager, this->getCuddBdd().Ite(thenDd.getCuddBdd(), elseDd.getCuddBdd()));
         }
         
         InternalBdd<DdType::CUDD> InternalBdd<DdType::CUDD>::operator||(InternalBdd<DdType::CUDD> const& other) const {
@@ -48,15 +49,15 @@ namespace storm {
         }
         
         InternalBdd<DdType::CUDD> InternalBdd<DdType::CUDD>::iff(InternalBdd<DdType::CUDD> const& other) const {
-            return InternalBdd<DdType::CUDD>(this->getCuddBdd().Xnor(other.getCuddBdd()));
+            return InternalBdd<DdType::CUDD>(ddManager, this->getCuddBdd().Xnor(other.getCuddBdd()));
         }
         
         InternalBdd<DdType::CUDD> InternalBdd<DdType::CUDD>::exclusiveOr(InternalBdd<DdType::CUDD> const& other) const {
-            return InternalBdd<DdType::CUDD>(this->getCuddBdd().Xor(other.getCuddBdd()));
+            return InternalBdd<DdType::CUDD>(ddManager, this->getCuddBdd().Xor(other.getCuddBdd()));
         }
         
         InternalBdd<DdType::CUDD> InternalBdd<DdType::CUDD>::implies(InternalBdd<DdType::CUDD> const& other) const {
-            return InternalBdd<DdType::CUDD>(this->getCuddBdd().Ite(other.getCuddBdd(), this->getDdManager()->getBddOne().getCuddBdd()), metaVariables);
+            return InternalBdd<DdType::CUDD>(ddManager, this->getCuddBdd().Ite(other.getCuddBdd(), ddManager->getBddOne().getCuddBdd()));
         }
         
         InternalBdd<DdType::CUDD> InternalBdd<DdType::CUDD>::operator!() const {
@@ -70,27 +71,27 @@ namespace storm {
             return *this;
         }
         
-        InternalBdd<DdType::CUDD> InternalBdd<DdType::CUDD>::existsAbstract(InternalBdd<DdType> const& cube) const {
-            return InternalBdd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().ExistAbstract(cube.getCuddBdd()), newMetaVariables);
+        InternalBdd<DdType::CUDD> InternalBdd<DdType::CUDD>::existsAbstract(InternalBdd<DdType::CUDD> const& cube) const {
+            return InternalBdd<DdType::CUDD>(ddManager, this->getCuddBdd().ExistAbstract(cube.getCuddBdd()));
         }
         
-        InternalBdd<DdType::CUDD> InternalBdd<DdType::CUDD>::universalAbstract(InternalBdd<DdType> const& cube) const {
-            return InternalBdd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().UnivAbstract(cube.getCuddBdd()), newMetaVariables);
+        InternalBdd<DdType::CUDD> InternalBdd<DdType::CUDD>::universalAbstract(InternalBdd<DdType::CUDD> const& cube) const {
+            return InternalBdd<DdType::CUDD>(ddManager, this->getCuddBdd().UnivAbstract(cube.getCuddBdd()));
         }
         
-        InternalBdd<DdType::CUDD> InternalBdd<DdType::CUDD>::andExists(InternalBdd<DdType::CUDD> const& other, InternalBdd<DdType> const& cube) const {
-            return InternalBdd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().AndAbstract(other.getCuddBdd(), cube.getCuddBdd()), containedMetaVariables);
+        InternalBdd<DdType::CUDD> InternalBdd<DdType::CUDD>::andExists(InternalBdd<DdType::CUDD> const& other, InternalBdd<DdType::CUDD> const& cube) const {
+            return InternalBdd<DdType::CUDD>(ddManager, this->getCuddBdd().AndAbstract(other.getCuddBdd(), cube.getCuddBdd()));
         }
         
         InternalBdd<DdType::CUDD> InternalBdd<DdType::CUDD>::constrain(InternalBdd<DdType::CUDD> const& constraint) const {
-            return InternalBdd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().Constrain(constraint.getCuddBdd()), metaVariables);
+            return InternalBdd<DdType::CUDD>(ddManager, this->getCuddBdd().Constrain(constraint.getCuddBdd()));
         }
         
         InternalBdd<DdType::CUDD> InternalBdd<DdType::CUDD>::restrict(InternalBdd<DdType::CUDD> const& constraint) const {
-            return InternalBdd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().Restrict(constraint.getCuddBdd()), metaVariables);
+            return InternalBdd<DdType::CUDD>(ddManager, this->getCuddBdd().Restrict(constraint.getCuddBdd()));
         }
         
-        InternalBdd<DdType::CUDD> InternalBdd<DdType::CUDD>::swapVariables(std::vector<std::pair<std::reference_wrapper<DdMetaVariable<LibraryType> const>, std::reference_wrapper<DdMetaVariable<LibraryType> const>>> const& fromTo) const {
+        InternalBdd<DdType::CUDD> InternalBdd<DdType::CUDD>::swapVariables(std::vector<std::pair<std::reference_wrapper<DdMetaVariable<DdType::CUDD> const>, std::reference_wrapper<DdMetaVariable<DdType::CUDD> const>>> const& fromTo) const {
             std::vector<BDD> fromBdd;
             std::vector<BDD> toBdd;
             for (auto const& metaVariablePair : fromTo) {
@@ -107,11 +108,11 @@ namespace storm {
             }
             
             // Finally, call CUDD to swap the variables.
-            return InternalBdd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().SwapVariables(fromBdd, toBdd), newContainedMetaVariables);
+            return InternalBdd<DdType::CUDD>(ddManager, this->getCuddBdd().SwapVariables(fromBdd, toBdd));
         }
         
         InternalBdd<DdType::CUDD> InternalBdd<DdType::CUDD>::getSupport() const {
-            return InternalBdd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().Support(), this->getContainedMetaVariables());
+            return InternalBdd<DdType::CUDD>(ddManager, this->getCuddBdd().Support());
         }
         
         uint_fast64_t InternalBdd<DdType::CUDD>::getNonZeroCount(uint_fast64_t numberOfDdVariables) const {
@@ -155,7 +156,7 @@ namespace storm {
             // Open the file, dump the DD and close it again.
             FILE* filePointer = fopen(filename.c_str() , "w");
             std::vector<BDD> cuddBddVector = { this->getCuddBdd() };
-            this->getDdManager()->getCuddManager().DumpDot(cuddBddVector, &ddVariableNames[0], &ddNames[0], filePointer);
+            ddManager->getCuddManager().DumpDot(cuddBddVector, &ddVariableNames[0], &ddNames[0], filePointer);
             fclose(filePointer);
             
             // Finally, delete the names.
@@ -176,27 +177,10 @@ namespace storm {
         }
         
         template<typename ValueType>
-        Add<DdType::CUDD, ValueType> InternalBdd<DdType::CUDD>::toAdd() const {
-            return Add<DdType::CUDD, ValueType>(this->getCuddBdd().Add());
+        InternalAdd<DdType::CUDD, ValueType> InternalBdd<DdType::CUDD>::toAdd() const {
+            return InternalAdd<DdType::CUDD, ValueType>(ddManager, this->getCuddBdd().Add());
         }
         
-        
-        
-        
-        
-        
-        
-        
-        
-        
-        
-        
-        
-        
-        
-        
-        
-        
         template<typename ValueType>
         DdNode* InternalBdd<DdType::CUDD>::fromVectorRec(::DdManager* manager, uint_fast64_t& currentOffset, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::vector<ValueType> const& values, Odd<DdType::CUDD> const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::function<bool (ValueType const&)> const& filter) {
             if (currentLevel == maxLevel) {

src/storage/dd/cudd/InternalCuddBdd.h

@@ -7,7 +7,6 @@
 #include "src/storage/dd/InternalBdd.h"
 #include "src/storage/dd/InternalAdd.h"
 
-#include "src/storage/dd/DdManager.h"
 #include "src/storage/dd/DdMetaVariable.h"
 
 // Include the C++-interface of CUDD.
@@ -27,6 +26,9 @@ namespace storm {
     }
 
     namespace dd {
+        template<DdType LibraryType>
+        class InternalDdManager;
+        
         template<storm::dd::DdType LibraryType>
         class Odd;
         
@@ -40,7 +42,7 @@ namespace storm {
              * @param cuddBdd The CUDD BDD to store.
              * @param containedMetaVariables The meta variables that appear in the DD.
              */
-            InternalBdd(std::shared_ptr<DdManager<DdType::CUDD> const> ddManager, BDD cuddBdd);
+            InternalBdd(InternalDdManager<DdType::CUDD> const* ddManager, BDD cuddBdd);
             
             // Instantiate all copy/move constructors/assignments with the default implementation.
             InternalBdd() = default;
@@ -60,7 +62,7 @@ namespace storm {
              * @return The resulting BDD.
              */
             template<typename ValueType>
-            static InternalBdd<storm::dd::DdType::CUDD> fromVector(std::shared_ptr<DdManager<DdType::CUDD> const> ddManager, std::vector<ValueType> const& values, Odd<DdType::CUDD> const& odd, std::set<storm::expressions::Variable> const& metaVariables, std::function<bool (ValueType const&)> const& filter);
+            static InternalBdd<storm::dd::DdType::CUDD> fromVector(InternalDdManager<DdType::CUDD> const* ddManager, std::vector<ValueType> const& values, Odd<DdType::CUDD> const& odd, std::vector<uint_fast64_t> const& sortedDdVariableIndices, std::function<bool (ValueType const&)> const& filter);
             
             /*!
              * Retrieves whether the two BDDs represent the same function.
@@ -330,7 +332,7 @@ namespace storm {
              */
             DdNode* getCuddDdNode() const;
             
-            std::shared_ptr<DdManager<DdType::CUDD> const> ddManager;
+            InternalDdManager<DdType::CUDD> const* ddManager;
             
             BDD cuddBdd;
         };

src/storage/dd/cudd/InternalCuddDdManager.cpp

@@ -0,0 +1,88 @@
+#include "src/storage/dd/cudd/InternalCuddDdManager.h"
+
+#include "src/settings/SettingsManager.h"
+#include "src/settings/modules/CuddSettings.h"
+
+namespace storm {
+    namespace dd {
+        
+        InternalDdManager<DdType::CUDD>::InternalDdManager() : cuddManager(), reorderingTechnique(CUDD_REORDER_NONE) {
+            this->cuddManager.SetMaxMemory(static_cast<unsigned long>(storm::settings::cuddSettings().getMaximalMemory() * 1024ul * 1024ul));
+            this->cuddManager.SetEpsilon(storm::settings::cuddSettings().getConstantPrecision());
+            
+            // Now set the selected reordering technique.
+            storm::settings::modules::CuddSettings::ReorderingTechnique reorderingTechniqueAsSetting = storm::settings::cuddSettings().getReorderingTechnique();
+            switch (reorderingTechniqueAsSetting) {
+                case storm::settings::modules::CuddSettings::ReorderingTechnique::None: this->reorderingTechnique = CUDD_REORDER_NONE; break;
+                case storm::settings::modules::CuddSettings::ReorderingTechnique::Random: this->reorderingTechnique = CUDD_REORDER_RANDOM; break;
+                case storm::settings::modules::CuddSettings::ReorderingTechnique::RandomPivot: this->reorderingTechnique = CUDD_REORDER_RANDOM_PIVOT; break;
+                case storm::settings::modules::CuddSettings::ReorderingTechnique::Sift: this->reorderingTechnique = CUDD_REORDER_SIFT; break;
+                case storm::settings::modules::CuddSettings::ReorderingTechnique::SiftConv: this->reorderingTechnique = CUDD_REORDER_SIFT_CONVERGE; break;
+                case storm::settings::modules::CuddSettings::ReorderingTechnique::SymmetricSift: this->reorderingTechnique = CUDD_REORDER_SYMM_SIFT; break;
+                case storm::settings::modules::CuddSettings::ReorderingTechnique::SymmetricSiftConv: this->reorderingTechnique = CUDD_REORDER_SYMM_SIFT_CONV; break;
+                case storm::settings::modules::CuddSettings::ReorderingTechnique::GroupSift: this->reorderingTechnique = CUDD_REORDER_GROUP_SIFT; break;
+                case storm::settings::modules::CuddSettings::ReorderingTechnique::GroupSiftConv: this->reorderingTechnique = CUDD_REORDER_GROUP_SIFT_CONV; break;
+                case storm::settings::modules::CuddSettings::ReorderingTechnique::Win2: this->reorderingTechnique = CUDD_REORDER_WINDOW2; break;
+                case storm::settings::modules::CuddSettings::ReorderingTechnique::Win2Conv: this->reorderingTechnique = CUDD_REORDER_WINDOW2_CONV; break;
+                case storm::settings::modules::CuddSettings::ReorderingTechnique::Win3: this->reorderingTechnique = CUDD_REORDER_WINDOW3; break;
+                case storm::settings::modules::CuddSettings::ReorderingTechnique::Win3Conv: this->reorderingTechnique = CUDD_REORDER_WINDOW3_CONV; break;
+                case storm::settings::modules::CuddSettings::ReorderingTechnique::Win4: this->reorderingTechnique = CUDD_REORDER_WINDOW4; break;
+                case storm::settings::modules::CuddSettings::ReorderingTechnique::Win4Conv: this->reorderingTechnique = CUDD_REORDER_WINDOW4_CONV; break;
+                case storm::settings::modules::CuddSettings::ReorderingTechnique::Annealing: this->reorderingTechnique = CUDD_REORDER_ANNEALING; break;
+                case storm::settings::modules::CuddSettings::ReorderingTechnique::Genetic: this->reorderingTechnique = CUDD_REORDER_GENETIC; break;
+                case storm::settings::modules::CuddSettings::ReorderingTechnique::Exact: this->reorderingTechnique = CUDD_REORDER_EXACT; break;
+            }
+        }
+        
+        InternalBdd<DdType::CUDD> InternalDdManager<DdType::CUDD>::getBddOne() const {
+            return InternalBdd<DdType::CUDD>(this, cuddManager.bddOne());
+        }
+        
+        template<typename ValueType>
+        InternalAdd<DdType::CUDD, ValueType> InternalDdManager<DdType::CUDD>::getAddOne() const {
+            return InternalAdd<DdType::CUDD, ValueType>(this, cuddManager.addOne());
+        }
+        
+        InternalBdd<DdType::CUDD> InternalDdManager<DdType::CUDD>::getBddZero() const {
+            return InternalBdd<DdType::CUDD>(this, cuddManager.bddZero());
+        }
+        
+        template<typename ValueType>
+        InternalAdd<DdType::CUDD, ValueType> InternalDdManager<DdType::CUDD>::getAddZero() const {
+            return InternalAdd<DdType::CUDD, ValueType>(this, cuddManager.addZero());
+        }
+        
+        template<typename ValueType>
+        InternalAdd<DdType::CUDD, ValueType> InternalDdManager<DdType::CUDD>::getConstant(ValueType const& value) const {
+            return InternalAdd<DdType::CUDD, ValueType>(this, cuddManager.constant(value));
+        }
+
+        std::pair<InternalBdd<DdType::CUDD>, InternalBdd<DdType::CUDD>> InternalDdManager<DdType::CUDD>::createNewDdVariablePair() {
+            std::pair<InternalBdd<DdType::CUDD>, InternalBdd<DdType::CUDD>> result;
+            result.first = InternalBdd<DdType::CUDD>(this, cuddManager.bddVar());
+            result.second = InternalBdd<DdType::CUDD>(this, cuddManager.bddVar());
+            
+            // Connect the two variables so they are not 'torn apart' during dynamic reordering.
+            cuddManager.MakeTreeNode(result.first.getIndex(), 2, MTR_FIXED);
+            
+            return result;
+        }
+        
+        void InternalDdManager<DdType::CUDD>::allowDynamicReordering(bool value) {
+            if (value) {
+                this->getCuddManager().AutodynEnable(this->reorderingTechnique);
+            } else {
+                this->getCuddManager().AutodynDisable();
+            }
+        }
+        
+        bool InternalDdManager<DdType::CUDD>::isDynamicReorderingAllowed() const {
+            Cudd_ReorderingType type;
+            return this->getCuddManager().ReorderingStatus(&type);
+        }
+        
+        void InternalDdManager<DdType::CUDD>::triggerReordering() {
+            this->getCuddManager().ReduceHeap(this->reorderingTechnique, 0);
+        }
+    }
+}

src/storage/dd/cudd/InternalCuddDdManager.h

@@ -0,0 +1,119 @@
+#ifndef STORM_STORAGE_DD_INTERNALCUDDDDMANAGER_H_
+#define STORM_STORAGE_DD_INTERNALCUDDDDMANAGER_H_
+
+#include "src/storage/dd/DdType.h"
+#include "src/storage/dd/InternalDdManager.h"
+
+#include "src/storage/dd/cudd/InternalCuddBdd.h"
+#include "src/storage/dd/cudd/InternalCuddAdd.h"
+
+#include "cuddObj.hh"
+
+namespace storm {
+    namespace dd {
+        template<DdType LibraryType, typename ValueType>
+        class InternalAdd;
+
+        template<DdType LibraryType>
+        class InternalBdd;
+        
+        template<>
+        class InternalDdManager<DdType::CUDD> {
+        public:
+            friend class InternalAdd<DdType::CUDD, double>;
+            friend class InternalBdd<DdType::CUDD>;
+            
+            /*!
+             * Creates a new internal manager for CUDD DDs.
+             */
+            InternalDdManager();
+            
+            /*!
+             * Retrieves a BDD representing the constant one function.
+             *
+             * @return A BDD representing the constant one function.
+             */
+            InternalBdd<DdType::CUDD> getBddOne() const;
+            
+            /*!
+             * Retrieves an ADD representing the constant one function.
+             *
+             * @return An ADD representing the constant one function.
+             */
+            template<typename ValueType>
+            InternalAdd<DdType::CUDD, ValueType> getAddOne() const;
+            
+            /*!
+             * Retrieves a BDD representing the constant zero function.
+             *
+             * @return A BDD representing the constant zero function.
+             */
+            InternalBdd<DdType::CUDD> getBddZero() const;
+            
+            /*!
+             * Retrieves an ADD representing the constant zero function.
+             *
+             * @return An ADD representing the constant zero function.
+             */
+            template<typename ValueType>
+            InternalAdd<DdType::CUDD, ValueType> getAddZero() const;
+            
+            /*!
+             * Retrieves an ADD representing the constant function with the given value.
+             *
+             * @return An ADD representing the constant function with the given value.
+             */
+            template<typename ValueType>
+            InternalAdd<DdType::CUDD, ValueType> getConstant(ValueType const& value) const;
+            
+            /*!
+             * Creates a new pair of DD variables and returns the two cubes as a result.
+             *
+             * @return The two cubes belonging to the DD variables.
+             */
+            std::pair<InternalBdd<DdType::CUDD>, InternalBdd<DdType::CUDD>> createNewDdVariablePair();
+            
+            /*!
+             * Sets whether or not dynamic reordering is allowed for the DDs managed by this manager.
+             *
+             * @param value If set to true, dynamic reordering is allowed and forbidden otherwise.
+             */
+            void allowDynamicReordering(bool value);
+            
+            /*!
+             * Retrieves whether dynamic reordering is currently allowed.
+             *
+             * @return True iff dynamic reordering is currently allowed.
+             */
+            bool isDynamicReorderingAllowed() const;
+            
+            /*!
+             * Triggers a reordering of the DDs managed by this manager.
+             */
+            void triggerReordering();
+            
+        private:
+            /*!
+             * Retrieves the underlying CUDD manager.
+             *
+             * @return The underlying CUDD manager.
+             */
+            Cudd& getCuddManager();
+            
+            /*!
+             * Retrieves the underlying CUDD manager.
+             *
+             * @return The underlying CUDD manager.
+             */
+            Cudd const& getCuddManager() const;
+            
+            // The manager responsible for the DDs created/modified with this DdManager.
+            Cudd cuddManager;
+            
+            // The technique that is used for dynamic reordering.
+            Cudd_ReorderingType reorderingTechnique;
+        };
+    }
+}
+
+#endif /* STORM_STORAGE_DD_INTERNALCUDDDDMANAGER_H_ */