Merge branch 'master' into SmtSolvers

Former-commit-id: 20effdeffe

src/solver/GlpkLpSolver.h

@@ -184,7 +184,7 @@ namespace storm {
                 throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
             }
             
-            virtual uint_fast64_t addBinaryVariable(std::string const& name, double objectiveFunctionCoefficient = 0) override {
+            virtual void addBinaryVariable(std::string const& name, double objectiveFunctionCoefficient = 0) override {
                 throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
             }
             

src/storage/dd/CuddDdManager.cpp

@@ -3,6 +3,7 @@
 #include <algorithm>
 
 #include "src/storage/dd/CuddDdManager.h"
+#include "src/exceptions/ExceptionMacros.h"
 #include "src/exceptions/InvalidArgumentException.h"
 #include "src/settings/Settings.h"
 
@@ -49,17 +50,9 @@ namespace storm {
         }
         
         Dd<DdType::CUDD> DdManager<DdType::CUDD>::getEncoding(std::string const& metaVariableName, int_fast64_t value) {
-            // Check whether the meta variable exists.
-            if (!this->hasMetaVariable(metaVariableName)) {
-                throw storm::exceptions::InvalidArgumentException() << "Unknown meta variable name '" << metaVariableName << "'.";
-            }
-            
             DdMetaVariable<DdType::CUDD> const& metaVariable = this->getMetaVariable(metaVariableName);
             
-            // Check whether the value is legal for this meta variable.
-            if (value < metaVariable.getLow() || value > metaVariable.getHigh()) {
-                throw storm::exceptions::InvalidArgumentException() << "Illegal value " << value << " for meta variable '" << metaVariableName << "'.";
-            }
+            LOG_THROW(value >= metaVariable.getLow() && value <= metaVariable.getHigh(), storm::exceptions::InvalidArgumentException, "Illegal value " << value << " for meta variable '" << metaVariableName << "'.");
             
             // Now compute the encoding relative to the low value of the meta variable.
             value -= metaVariable.getLow();
@@ -85,11 +78,6 @@ namespace storm {
         }
         
         Dd<DdType::CUDD> DdManager<DdType::CUDD>::getRange(std::string const& metaVariableName) {
-            // Check whether the meta variable exists.
-            if (!this->hasMetaVariable(metaVariableName)) {
-                throw storm::exceptions::InvalidArgumentException() << "Unknown meta variable name '" << metaVariableName << "'.";
-            }
-
             storm::dd::DdMetaVariable<DdType::CUDD> const& metaVariable = this->getMetaVariable(metaVariableName);
             
             Dd<DdType::CUDD> result = this->getZero();
@@ -101,11 +89,6 @@ namespace storm {
         }
         
         Dd<DdType::CUDD> DdManager<DdType::CUDD>::getIdentity(std::string const& metaVariableName) {
-            // Check whether the meta variable exists.
-            if (!this->hasMetaVariable(metaVariableName)) {
-                throw storm::exceptions::InvalidArgumentException() << "Unknown meta variable name '" << metaVariableName << "'.";
-            }
-            
             storm::dd::DdMetaVariable<DdType::CUDD> const& metaVariable = this->getMetaVariable(metaVariableName);
             
             Dd<DdType::CUDD> result = this->getZero();
@@ -116,91 +99,57 @@ namespace storm {
         }
 
         void DdManager<DdType::CUDD>::addMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high) {
+            // Check whether the variable name is legal.
+            LOG_THROW(name != "" && name.back() != '\'', storm::exceptions::InvalidArgumentException, "Illegal name of meta variable: '" << name << "'.");
+            
             // Check whether a meta variable already exists.
-            if (this->hasMetaVariable(name)) {
-                throw storm::exceptions::InvalidArgumentException() << "A meta variable '" << name << "' already exists.";
-            }
+            LOG_THROW(!this->hasMetaVariable(name), storm::exceptions::InvalidArgumentException, "A meta variable '" << name << "' already exists.");
 
             // Check that the range is legal.
-            if (high == low) {
-                throw storm::exceptions::InvalidArgumentException() << "Range of meta variable must be at least 2 elements.";
-            }
+            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)));
             
             std::vector<Dd<DdType::CUDD>> variables;
+            std::vector<Dd<DdType::CUDD>> variablesPrime;
             for (std::size_t i = 0; i < numberOfBits; ++i) {
                 variables.emplace_back(Dd<DdType::CUDD>(this->shared_from_this(), cuddManager.addVar(), {name}));
+                variablesPrime.emplace_back(Dd<DdType::CUDD>(this->shared_from_this(), cuddManager.addVar(), {name + "'"}));
+            }
+            
+            // Now group the non-primed and primed variable.
+            for (uint_fast64_t i = 0; i < numberOfBits; ++i) {
+                this->getCuddManager().MakeTreeNode(variables[i].getCuddAdd().NodeReadIndex(), 2, MTR_FIXED);
             }
             
             metaVariableMap.emplace(name, DdMetaVariable<DdType::CUDD>(name, low, high, variables, this->shared_from_this()));
+            metaVariableMap.emplace(name + "'", DdMetaVariable<DdType::CUDD>(name + "'", low, high, variablesPrime, this->shared_from_this()));
         }
         
         void DdManager<DdType::CUDD>::addMetaVariable(std::string const& name) {
+            // Check whether the variable name is legal.
+            LOG_THROW(name != "" && name.back() != '\'', storm::exceptions::InvalidArgumentException, "Illegal name of meta variable: '" << name << "'.");
+            
             // Check whether a meta variable already exists.
-            if (this->hasMetaVariable(name)) {
-                throw storm::exceptions::InvalidArgumentException() << "A meta variable '" << name << "' already exists.";
-            }
+            LOG_THROW(!this->hasMetaVariable(name), storm::exceptions::InvalidArgumentException, "A meta variable '" << name << "' already exists.");
             
             std::vector<Dd<DdType::CUDD>> variables;
+            std::vector<Dd<DdType::CUDD>> variablesPrime;
             variables.emplace_back(Dd<DdType::CUDD>(this->shared_from_this(), cuddManager.addVar(), {name}));
-            
-            metaVariableMap.emplace(name, DdMetaVariable<DdType::CUDD>(name, variables, this->shared_from_this()));
-        }
-        
-        void DdManager<DdType::CUDD>::addMetaVariablesInterleaved(std::vector<std::string> const& names, int_fast64_t low, int_fast64_t high, bool fixedGroup) {
-            // Make sure that at least one meta variable is added.
-            if (names.size() == 0) {
-                throw storm::exceptions::InvalidArgumentException() << "Illegal to add zero meta variables.";
-            }
-            
-            // Check that there are no duplicate names in the given name vector.
-            std::vector<std::string> nameCopy(names);
-            std::sort(nameCopy.begin(), nameCopy.end());
-            if (std::adjacent_find(nameCopy.begin(), nameCopy.end()) != nameCopy.end()) {
-                throw storm::exceptions::InvalidArgumentException() << "Cannot add duplicate meta variables.";
-            }
-            
-            // Check that the range is legal.
-            if (high == low) {
-                throw storm::exceptions::InvalidArgumentException() << "Range of meta variable must be at least 2 elements.";
-            }
+            variablesPrime.emplace_back(Dd<DdType::CUDD>(this->shared_from_this(), cuddManager.addVar(), {name + "'"}));
 
-            // Check whether a meta variable already exists.
-            for (auto const& metaVariableName : names) {
-                if (this->hasMetaVariable(metaVariableName)) {
-                    throw storm::exceptions::InvalidArgumentException() << "A meta variable '" << metaVariableName << "' already exists.";
-                }
-            }
-            
-            // Add the variables in interleaved order.
-            std::size_t numberOfBits = static_cast<std::size_t>(std::ceil(std::log2(high - low + 1)));
-            std::vector<std::vector<Dd<DdType::CUDD>>> variables(names.size());
-            for (uint_fast64_t bit = 0; bit < numberOfBits; ++bit) {
-                for (uint_fast64_t i = 0; i < names.size(); ++i) {
-                    variables[i].emplace_back(Dd<DdType::CUDD>(this->shared_from_this(), cuddManager.addVar(), {names[i]}));
-                }
-            }
-            
-            // If required, we group the bits on the same layer of the interleaved meta variables.
-            if (fixedGroup) {
-                for (uint_fast64_t i = 0; i < names.size(); ++i) {
-                    this->getCuddManager().MakeTreeNode(variables[i].front().getCuddAdd().NodeReadIndex(), names.size(), MTR_FIXED);
-                }
-            }
+            // Now group the non-primed and primed variable.
+            this->getCuddManager().MakeTreeNode(variables.front().getCuddAdd().NodeReadIndex(), 2, MTR_FIXED);
             
-            // Now add the meta variables.
-            for (uint_fast64_t i = 0; i < names.size(); ++i) {
-                metaVariableMap.emplace(names[i], DdMetaVariable<DdType::CUDD>(names[i], low, high, variables[i], this->shared_from_this()));
-            }
+            metaVariableMap.emplace(name, DdMetaVariable<DdType::CUDD>(name, variables, this->shared_from_this()));
+            metaVariableMap.emplace(name + "'", DdMetaVariable<DdType::CUDD>(name + "'", variablesPrime, this->shared_from_this()));
         }
         
         DdMetaVariable<DdType::CUDD> const& DdManager<DdType::CUDD>::getMetaVariable(std::string const& metaVariableName) const {
             auto const& nameVariablePair = metaVariableMap.find(metaVariableName);
             
-            if (!this->hasMetaVariable(metaVariableName)) {
-                throw storm::exceptions::InvalidArgumentException() << "Unknown meta variable name '" << metaVariableName << "'.";
-            }
+            // Check whether the meta variable exists.
+            LOG_THROW(nameVariablePair != metaVariableMap.end(), storm::exceptions::InvalidArgumentException, "Unknown meta variable name '" << metaVariableName << "'.");
             
             return nameVariablePair->second;
         }

src/storage/dd/CuddDdManager.h

@@ -4,7 +4,7 @@
 #include <unordered_map>
 
 #include "src/storage/dd/DdManager.h"
-#include "src/storage/dd/DdMetaVariable.h"
+#include "src/storage/dd/CuddDdMetaVariable.h"
 #include "src/utility/OsDetection.h"
 
 // Include the C++-interface of CUDD.
@@ -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 DdForwardIterator<DdType::CUDD>;
             
             /*!
              * Creates an empty manager without any meta variables.
@@ -83,7 +84,7 @@ namespace storm {
             /*!
              * Adds an integer meta variable with the given name and range.
              *
-             * @param name The name of the meta variable.
+             * @param name The (non-empty) 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.
              */
@@ -92,30 +93,10 @@ namespace storm {
             /*!
              * Adds a boolean meta variable with the given name.
              *
-             * @param name The name of the meta variable.
+             * @param name The (non-empty) name of the meta variable.
              */
             void addMetaVariable(std::string const& name);
             
-            /*!
-             * Adds integer meta variables with the given names and (equal) range and arranges the DD variables in an
-             * interleaved order.
-             *
-             * @param names The names of the variables.
-             * @param low The lowest value of the ranges of the variables.
-             * @param high The highest value of the ranges of the variables.
-             * @param fixedGroup If set to true, the interleaved bits of the meta variable are always kept together as
-             * a group during a potential reordering.
-             */
-            void addMetaVariablesInterleaved(std::vector<std::string> const& names, int_fast64_t low, int_fast64_t high, bool fixedGroup = true);
-            
-            /*!
-             * Retrieves the meta variable with the given name if it exists.
-             *
-             * @param metaVariableName The name of the meta variable to retrieve.
-             * @return The meta variable with the given name.
-             */
-            DdMetaVariable<DdType::CUDD> const& getMetaVariable(std::string const& metaVariableName) const;
-            
             /*!
              * Retrieves the names of all meta variables that have been added to the manager.
              *
@@ -157,6 +138,15 @@ namespace storm {
              */
             void triggerReordering();
             
+        protected:
+            /*!
+             * Retrieves the meta variable with the given name if it exists.
+             *
+             * @param metaVariableName The name of the meta variable to retrieve.
+             * @return The meta variable with the given name.
+             */
+            DdMetaVariable<DdType::CUDD> const& getMetaVariable(std::string const& metaVariableName) const;
+            
         private:
             /*!
              * Retrieves a list of names of the DD variables in the order of their index.

src/storage/dd/CuddDdMetaVariable.cpp

@@ -0,0 +1,52 @@
+#include "src/storage/dd/CuddDdMetaVariable.h"
+#include "src/storage/dd/CuddDdManager.h"
+
+namespace storm {
+    namespace dd {
+        DdMetaVariable<DdType::CUDD>::DdMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high, std::vector<Dd<DdType::CUDD>> const& ddVariables, std::shared_ptr<DdManager<DdType::CUDD>> manager) : name(name), type(MetaVariableType::Int), low(low), high(high), ddVariables(ddVariables), cube(manager->getOne()), manager(manager) {
+            // Create the cube of all variables of this meta variable.
+            for (auto const& ddVariable : this->ddVariables) {
+                this->cube *= ddVariable;
+            }
+        }
+        
+        DdMetaVariable<DdType::CUDD>::DdMetaVariable(std::string const& name, std::vector<Dd<DdType::CUDD>> const& ddVariables, std::shared_ptr<DdManager<DdType::CUDD>> manager) : name(name), type(MetaVariableType::Bool), ddVariables(ddVariables), cube(manager->getOne()), manager(manager) {
+            // Create the cube of all variables of this meta variable.
+            for (auto const& ddVariable : this->ddVariables) {
+                this->cube *= ddVariable;
+            }
+        }
+        
+        std::string const& DdMetaVariable<DdType::CUDD>::getName() const {
+            return this->name;
+        }
+        
+        typename DdMetaVariable<DdType::CUDD>::MetaVariableType DdMetaVariable<DdType::CUDD>::getType() const {
+            return this->type;
+        }
+        
+        int_fast64_t DdMetaVariable<DdType::CUDD>::getLow() const {
+            return this->low;
+        }
+
+        int_fast64_t DdMetaVariable<DdType::CUDD>::getHigh() const {
+            return this->high;
+        }
+        
+        std::size_t DdMetaVariable<DdType::CUDD>::getNumberOfDdVariables() const {
+            return this->ddVariables.size();
+        }
+        
+        std::shared_ptr<DdManager<DdType::CUDD>> DdMetaVariable<DdType::CUDD>::getDdManager() const {
+            return this->manager;
+        }
+
+        std::vector<Dd<DdType::CUDD>> const& DdMetaVariable<DdType::CUDD>::getDdVariables() const {
+            return this->ddVariables;
+        }
+        
+        Dd<DdType::CUDD> const& DdMetaVariable<DdType::CUDD>::getCube() const {
+            return this->cube;
+        }
+    }
+}

src/storage/dd/CuddDdMetaVariable.h

@@ -0,0 +1,138 @@
+#ifndef STORM_STORAGE_DD_DDMETAVARIABLE_H_
+#define STORM_STORAGE_DD_DDMETAVARIABLE_H_
+
+#include <memory>
+#include <vector>
+#include <cstdint>
+#include <string>
+
+#include "utility/OsDetection.h"
+#include "src/storage/dd/CuddDd.h"
+#include "src/storage/dd/DdMetaVariable.h"
+#include "src/storage/expressions/Expression.h"
+
+namespace storm {
+    namespace dd {
+        // Forward-declare the DdManager class.
+        template<DdType Type> class DdManager;
+        
+        template<>
+        class DdMetaVariable<DdType::CUDD> {
+        public:
+            // 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 DdForwardIterator<DdType::CUDD>;
+            
+            // An enumeration for all legal types of meta variables.
+            enum class MetaVariableType { Bool, Int };
+            
+            /*!
+             * 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<Dd<DdType::CUDD>> const& ddVariables, std::shared_ptr<DdManager<DdType::CUDD>> manager);
+            
+            /*!
+             * 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<Dd<DdType::CUDD>> const& ddVariables, std::shared_ptr<DdManager<DdType::CUDD>> manager);
+            
+            // Explictly generate all default versions of copy/move constructors/assignments.
+            DdMetaVariable(DdMetaVariable const& other) = default;
+			DdMetaVariable& operator=(DdMetaVariable const& other) = default;
+#ifndef WINDOWS
+            DdMetaVariable(DdMetaVariable&& other) = default;
+            DdMetaVariable& operator=(DdMetaVariable&& other) = default;
+#endif
+            
+            /*!
+             * 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 manager that is responsible for this meta variable.
+             *
+             * A pointer to the manager that is responsible for this meta variable.
+             */
+            std::shared_ptr<DdManager<DdType::CUDD>> getDdManager() 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;
+            
+        private:
+            /*!
+             * Retrieves the variables used to encode the meta variable.
+             *
+             * @return A vector of variables used to encode the meta variable.
+             */
+            std::vector<Dd<DdType::CUDD>> const& getDdVariables() const;
+            
+            /*!
+             * Retrieves the cube of all variables that encode this meta variable.
+             *
+             * @return The cube of all variables that encode this meta variable.
+             */
+            Dd<DdType::CUDD> const& getCube() const;
+            
+            // 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<Dd<DdType::CUDD>> ddVariables;
+            
+            // The cube consisting of all variables that encode the meta variable.
+            Dd<DdType::CUDD> cube;
+            
+            // A pointer to the manager responsible for this meta variable.
+            std::shared_ptr<DdManager<DdType::CUDD>> manager;
+        };
+    }
+}
+
+#endif /* STORM_STORAGE_DD_DDMETAVARIABLE_H_ */

src/storage/dd/DdMetaVariable.cpp

@@ -1,65 +0,0 @@
-#include "src/storage/dd/DdMetaVariable.h"
-#include "src/storage/dd/CuddDdManager.h"
-
-namespace storm {
-    namespace dd {
-        template<DdType Type>
-        DdMetaVariable<Type>::DdMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high, std::vector<Dd<Type>> const& ddVariables, std::shared_ptr<DdManager<Type>> manager) : name(name), type(MetaVariableType::Int), low(low), high(high), ddVariables(ddVariables), cube(manager->getOne()), manager(manager) {
-            // Create the cube of all variables of this meta variable.
-            for (auto const& ddVariable : this->ddVariables) {
-                this->cube *= ddVariable;
-            }
-        }
-        
-        template<DdType Type>
-        DdMetaVariable<Type>::DdMetaVariable(std::string const& name, std::vector<Dd<Type>> const& ddVariables, std::shared_ptr<DdManager<Type>> manager) : name(name), type(MetaVariableType::Bool), ddVariables(ddVariables), cube(manager->getOne()), manager(manager) {
-            // Create the cube of all variables of this meta variable.
-            for (auto const& ddVariable : this->ddVariables) {
-                this->cube *= ddVariable;
-            }
-        }
-        
-        template<DdType Type>
-        std::string const& DdMetaVariable<Type>::getName() const {
-            return this->name;
-        }
-        
-        template<DdType Type>
-        typename DdMetaVariable<Type>::MetaVariableType DdMetaVariable<Type>::getType() const {
-            return this->type;
-        }
-        
-        template<DdType Type>
-        int_fast64_t DdMetaVariable<Type>::getLow() const {
-            return this->low;
-        }
-
-        template<DdType Type>
-        int_fast64_t DdMetaVariable<Type>::getHigh() const {
-            return this->high;
-        }
-        
-        template<DdType Type>
-        std::size_t DdMetaVariable<Type>::getNumberOfDdVariables() const {
-            return this->ddVariables.size();
-        }
-        
-        template<DdType Type>
-        std::shared_ptr<DdManager<Type>> DdMetaVariable<Type>::getDdManager() const {
-            return this->manager;
-        }
-
-        template<DdType Type>
-        std::vector<Dd<Type>> const& DdMetaVariable<Type>::getDdVariables() const {
-            return this->ddVariables;
-        }
-        
-        template<DdType Type>
-        Dd<Type> const& DdMetaVariable<Type>::getCube() const {
-            return this->cube;
-        }
-        
-        // Explicitly instantiate DdMetaVariable.
-        template class DdMetaVariable<DdType::CUDD>;
-    }
-}

src/storage/dd/DdMetaVariable.h

@@ -1,137 +1,13 @@
-#ifndef STORM_STORAGE_DD_DDMETAVARIABLE_H_
-#define STORM_STORAGE_DD_DDMETAVARIABLE_H_
+#ifndef STORM_STORAGE_DD_DDMETAVARIBLE_H_
+#define STORM_STORAGE_DD_DDMETAVARIBLE_H_
 
-#include <memory>
-#include <vector>
-#include <cstdint>
-#include <string>
-
-#include "utility/OsDetection.h"
-#include "src/storage/dd/CuddDd.h"
-#include "src/storage/expressions/Expression.h"
+#include "src/storage/dd/DdType.h"
 
 namespace storm {
     namespace dd {
-        // Forward-declare the DdManager class.
-        template<DdType Type> class DdManager;
-        
-        template <DdType Type>
-        class DdMetaVariable {
-        public:
-            // Declare the DdManager class as friend so it can access the internals of a meta variable.
-            friend class DdManager<Type>;
-            friend class Dd<Type>;
-            friend class DdForwardIterator<Type>;
-            
-            // An enumeration for all legal types of meta variables.
-            enum class MetaVariableType { Bool, Int };
-            
-            /*!
-             * 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<Dd<Type>> const& ddVariables, std::shared_ptr<DdManager<Type>> manager);
-            
-            /*!
-             * 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<Dd<Type>> const& ddVariables, std::shared_ptr<DdManager<Type>> manager);
-            
-            // Explictly generate all default versions of copy/move constructors/assignments.
-            DdMetaVariable(DdMetaVariable const& other) = default;
-			DdMetaVariable& operator=(DdMetaVariable const& other) = default;
-#ifndef WINDOWS
-            DdMetaVariable(DdMetaVariable&& other) = default;
-            DdMetaVariable& operator=(DdMetaVariable&& other) = default;
-#endif
-            
-            /*!
-             * 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 manager that is responsible for this meta variable.
-             *
-             * A pointer to the manager that is responsible for this meta variable.
-             */
-            std::shared_ptr<DdManager<Type>> getDdManager() 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;
-            
-        private:
-            /*!
-             * Retrieves the variables used to encode the meta variable.
-             *
-             * @return A vector of variables used to encode the meta variable.
-             */
-            std::vector<Dd<Type>> const& getDdVariables() const;
-            
-            /*!
-             * Retrieves the cube of all variables that encode this meta variable.
-             *
-             * @return The cube of all variables that encode this meta variable.
-             */
-            Dd<Type> const& getCube() const;
-            
-            // 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<Dd<Type>> ddVariables;
-            
-            // The cube consisting of all variables that encode the meta variable.
-            Dd<Type> cube;
-            
-            // A pointer to the manager responsible for this meta variable.
-            std::shared_ptr<DdManager<Type>> manager;
-        };
+        // Declare DdMetaVariable class so we can then specialize it for the different DD types.
+        template<DdType Type> class DdMetaVariable;
     }
 }
 
-#endif /* STORM_STORAGE_DD_DDMETAVARIABLE_H_ */
+#endif /* STORM_STORAGE_DD_DDMETAVARIBLE_H_ */

test/functional/storage/CuddDdTest.cpp

@@ -38,26 +38,18 @@ TEST(CuddDdManager, Constants) {
 TEST(CuddDdManager, AddGetMetaVariableTest) {
     std::shared_ptr<storm::dd::DdManager<storm::dd::DdType::CUDD>> manager(new storm::dd::DdManager<storm::dd::DdType::CUDD>());
     ASSERT_NO_THROW(manager->addMetaVariable("x", 1, 9));
-    EXPECT_EQ(1, manager->getNumberOfMetaVariables());
+    EXPECT_EQ(2, manager->getNumberOfMetaVariables());
     
-    std::vector<std::string> names = {"x", "x'"};
-    ASSERT_THROW(manager->addMetaVariablesInterleaved(names, 0, 3), storm::exceptions::InvalidArgumentException);
+    ASSERT_THROW(manager->addMetaVariable("x", 0, 3), storm::exceptions::InvalidArgumentException);
 
-    names = {"y", "y"};
-    ASSERT_THROW(manager->addMetaVariablesInterleaved(names, 0, 3), storm::exceptions::InvalidArgumentException);
+    ASSERT_NO_THROW(manager->addMetaVariable("y", 0, 3));
+    EXPECT_EQ(4, manager->getNumberOfMetaVariables());
     
-    names = {"y", "y'"};
-    ASSERT_NO_THROW(manager->addMetaVariablesInterleaved(names, 0, 3));
-    EXPECT_EQ(3, manager->getNumberOfMetaVariables());
-    
-    EXPECT_FALSE(manager->hasMetaVariable("x'"));
+    EXPECT_TRUE(manager->hasMetaVariable("x'"));
     EXPECT_TRUE(manager->hasMetaVariable("y'"));
     
-    std::set<std::string> metaVariableSet = {"x", "y", "y'"};
+    std::set<std::string> metaVariableSet = {"x", "x'", "y", "y'"};
     EXPECT_EQ(metaVariableSet, manager->getAllMetaVariableNames());
-    
-    ASSERT_THROW(storm::dd::DdMetaVariable<storm::dd::DdType::CUDD> const& metaVariableX = manager->getMetaVariable("x'"), storm::exceptions::InvalidArgumentException);
-    ASSERT_NO_THROW(storm::dd::DdMetaVariable<storm::dd::DdType::CUDD> const& metaVariableX = manager->getMetaVariable("x"));
 }
 
 TEST(CuddDdManager, EncodingTest) {
@@ -99,20 +91,6 @@ TEST(CuddDdManager, IdentityTest) {
     EXPECT_EQ(21, range.getNodeCount());
 }
 
-TEST(CuddDdMetaVariable, AccessorTest) {
-    std::shared_ptr<storm::dd::DdManager<storm::dd::DdType::CUDD>> manager(new storm::dd::DdManager<storm::dd::DdType::CUDD>());
-    manager->addMetaVariable("x", 1, 9);
-    EXPECT_EQ(1, manager->getNumberOfMetaVariables());
-    ASSERT_NO_THROW(storm::dd::DdMetaVariable<storm::dd::DdType::CUDD> const& metaVariableX = manager->getMetaVariable("x"));
-    storm::dd::DdMetaVariable<storm::dd::DdType::CUDD> const& metaVariableX = manager->getMetaVariable("x");
-    
-    EXPECT_EQ(1, metaVariableX.getLow());
-    EXPECT_EQ(9, metaVariableX.getHigh());
-    EXPECT_EQ("x", metaVariableX.getName());
-    EXPECT_EQ(manager, metaVariableX.getDdManager());
-    EXPECT_EQ(4, metaVariableX.getNumberOfDdVariables());
-}
-
 TEST(CuddDd, OperatorTest) {
     std::shared_ptr<storm::dd::DdManager<storm::dd::DdType::CUDD>> manager(new storm::dd::DdManager<storm::dd::DdType::CUDD>());
     manager->addMetaVariable("x", 1, 9);
@@ -200,7 +178,7 @@ TEST(CuddDd, OperatorTest) {
 
 TEST(CuddDd, AbstractionTest) {
     std::shared_ptr<storm::dd::DdManager<storm::dd::DdType::CUDD>> manager(new storm::dd::DdManager<storm::dd::DdType::CUDD>());
-    manager->addMetaVariablesInterleaved({"x", "x'"}, 1, 9);
+    manager->addMetaVariable("x", 1, 9);
     storm::dd::Dd<storm::dd::DdType::CUDD> dd1;
     storm::dd::Dd<storm::dd::DdType::CUDD> dd2;
     storm::dd::Dd<storm::dd::DdType::CUDD> dd3;
@@ -246,7 +224,7 @@ TEST(CuddDd, AbstractionTest) {
 TEST(CuddDd, SwapTest) {
     std::shared_ptr<storm::dd::DdManager<storm::dd::DdType::CUDD>> manager(new storm::dd::DdManager<storm::dd::DdType::CUDD>());
     
-    manager->addMetaVariablesInterleaved({"x", "x'"}, 1, 9);
+    manager->addMetaVariable("x", 1, 9);
     manager->addMetaVariable("z", 2, 8);
     storm::dd::Dd<storm::dd::DdType::CUDD> dd1;
     storm::dd::Dd<storm::dd::DdType::CUDD> dd2;
@@ -259,7 +237,7 @@ TEST(CuddDd, SwapTest) {
 
 TEST(CuddDd, MultiplyMatrixTest) {
     std::shared_ptr<storm::dd::DdManager<storm::dd::DdType::CUDD>> manager(new storm::dd::DdManager<storm::dd::DdType::CUDD>());
-    manager->addMetaVariablesInterleaved({"x", "x'"}, 1, 9);
+    manager->addMetaVariable("x", 1, 9);
     
     storm::dd::Dd<storm::dd::DdType::CUDD> dd1 = manager->getIdentity("x").equals(manager->getIdentity("x'"));
     storm::dd::Dd<storm::dd::DdType::CUDD> dd2 = manager->getRange("x'");