diff --git a/src/storage/dd/Bdd.cpp b/src/storage/dd/Bdd.cpp
index 2bc04d168..5ea3bc376 100644
--- a/src/storage/dd/Bdd.cpp
+++ b/src/storage/dd/Bdd.cpp
@@ -2,6 +2,8 @@
 #include "src/storage/dd/Add.h"
 #include "src/storage/dd/Odd.h"
 
+#include "src/logic/ComparisonType.h"
+
 #include "src/storage/dd/DdMetaVariable.h"
 #include "src/storage/dd/DdManager.h"
 
@@ -19,22 +21,23 @@ namespace storm {
         }
         
         template<DdType LibraryType>
-        Bdd<LibraryType>::Bdd(std::shared_ptr<DdManager<LibraryType> const> ddManager, std::vector<double> const& explicitValues, storm::dd::Odd<LibraryType> const& odd, std::set<storm::expressions::Variable> const& metaVariables, storm::logic::ComparisonType comparisonType, double value) {
+        Bdd<LibraryType> Bdd<LibraryType>::fromVector(std::shared_ptr<DdManager<LibraryType> const> ddManager, std::vector<double> const& explicitValues, storm::dd::Odd<LibraryType> const& odd, std::set<storm::expressions::Variable> const& metaVariables, storm::logic::ComparisonType comparisonType, double value) {
             switch (comparisonType) {
                 case storm::logic::ComparisonType::Less:
-                    this->cuddBdd = fromVector<double>(ddManager, explicitValues, odd, metaVariables, std::bind(std::greater<double>(), value, std::placeholders::_1));
-                    break;
+                    return fromVector<double>(ddManager, explicitValues, odd, metaVariables, std::bind(std::greater<double>(), value, std::placeholders::_1));
                 case storm::logic::ComparisonType::LessEqual:
-                    this->cuddBdd = fromVector<double>(ddManager, explicitValues, odd, metaVariables, std::bind(std::greater_equal<double>(), value, std::placeholders::_1));
-                    break;
+                    return fromVector<double>(ddManager, explicitValues, odd, metaVariables, std::bind(std::greater_equal<double>(), value, std::placeholders::_1));
                 case storm::logic::ComparisonType::Greater:
-                    this->cuddBdd = fromVector<double>(ddManager, explicitValues, odd, metaVariables, std::bind(std::less<double>(), value, std::placeholders::_1));
-                    break;
+                    return fromVector<double>(ddManager, explicitValues, odd, metaVariables, std::bind(std::less<double>(), value, std::placeholders::_1));
                 case storm::logic::ComparisonType::GreaterEqual:
-                    this->cuddBdd = fromVector<double>(ddManager, explicitValues, odd, metaVariables, std::bind(std::less_equal<double>(), value, std::placeholders::_1));
-                    break;
+                    return fromVector<double>(ddManager, explicitValues, odd, metaVariables, std::bind(std::less_equal<double>(), value, std::placeholders::_1));
             }
-
+        }
+        
+        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);
         }
         
         template<DdType LibraryType>
@@ -106,64 +109,36 @@ namespace storm {
 
         template<DdType LibraryType>
         Bdd<LibraryType> Bdd<LibraryType>::existsAbstract(std::set<storm::expressions::Variable> const& metaVariables) const {
-            Bdd<LibraryType> cubeBdd = this->getDdManager()->getBddOne();
-            
-            std::set<storm::expressions::Variable> newMetaVariables = this->getContainedMetaVariables();
-            for (auto const& metaVariable : metaVariables) {
-                // First check whether the BDD contains the meta variable and erase it, if this is the case.
-                STORM_LOG_THROW(this->containsMetaVariable(metaVariable), storm::exceptions::InvalidArgumentException, "Cannot abstract from meta variable '" << metaVariable.getName() << "' that is not present in the DD.");
-                newMetaVariables.erase(metaVariable);
-                
-                DdMetaVariable<DdType::CUDD> const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable);
-                cubeBdd &= ddMetaVariable.getCube();
-            }
-            
-            return Bdd<LibraryType>(internalBdd.existsAbstract(cubeBdd));
+            Bdd<LibraryType> cube = this->getCube(metaVariables);
+            return Bdd<LibraryType>(this->getDdManager(), internalBdd.existsAbstract(cube), Dd<LibraryType>::subtractMetaVariables(*this, cube));
         }
 
         template<DdType LibraryType>
         Bdd<LibraryType> Bdd<LibraryType>::universalAbstract(std::set<storm::expressions::Variable> const& metaVariables) const {
-            InternalBdd<LibraryType> cubeBdd = this->getDdManager()->getBddOne();
-            
-            std::set<storm::expressions::Variable> newMetaVariables = this->getContainedMetaVariables();
-            for (auto const& metaVariable : metaVariables) {
-                // First check whether the BDD contains the meta variable and erase it, if this is the case.
-                STORM_LOG_THROW(this->containsMetaVariable(metaVariable), storm::exceptions::InvalidArgumentException, "Cannot abstract from meta variable '" << metaVariable.getName() << "' that is not present in the DD.");
-                newMetaVariables.erase(metaVariable);
-                
-                DdMetaVariable<DdType::CUDD> const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable);
-                cubeBdd &= ddMetaVariable.getCube();
-            }
-            
-            return Bdd<LibraryType>(internalBdd.universalAbstract(cubeBdd));
+            Bdd<LibraryType> cube = this->getCube(metaVariables);
+            return Bdd<LibraryType>(this->getDdManager(), internalBdd.universalAbstract(cube), Dd<LibraryType>::subtractMetaVariables(*this, cube));
         }
         
         template<DdType LibraryType>
         Bdd<LibraryType> Bdd<LibraryType>::andExists(Bdd<LibraryType> const& other, std::set<storm::expressions::Variable> const& existentialVariables) const {
-            InternalBdd<DdType::CUDD> cubeBdd(this->getDdManager()->getBddOne());
-            for (auto const& metaVariable : existentialVariables) {
-                DdMetaVariable<DdType::CUDD> const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable);
-                cubeBdd &= ddMetaVariable.getCube();
-            }
+            Bdd<DdType::CUDD> cube = this->getCube(existentialVariables);
 
             std::set<storm::expressions::Variable> unionOfMetaVariables;
             std::set_union(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end(), other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end(), std::inserter(unionOfMetaVariables, unionOfMetaVariables.begin()));
             std::set<storm::expressions::Variable> containedMetaVariables;
             std::set_difference(unionOfMetaVariables.begin(), unionOfMetaVariables.end(), existentialVariables.begin(), existentialVariables.end(), std::inserter(containedMetaVariables, containedMetaVariables.begin()));
             
-            return Bdd<LibraryType>(internalBdd.andExists(other.internalBdd, cubeBdd));
+            return Bdd<LibraryType>(this->getDdManager(), internalBdd.andExists(other, cube), containedMetaVariables);
         }
         
         template<DdType LibraryType>
         Bdd<LibraryType> Bdd<LibraryType>::constrain(Bdd<LibraryType> const& constraint) const {
-            this->addMetaVariables(constraint.getContainedMetaVariables());
-            return internalBdd.constraint(constraint.internalBdd);
+            return Bdd<LibraryType>(this->getDdManager(), internalBdd.constrain(constraint), Dd<LibraryType>::joinMetaVariables(*this, constraint));
         }
         
         template<DdType LibraryType>
         Bdd<LibraryType> Bdd<LibraryType>::restrict(Bdd<LibraryType> const& constraint) const {
-            this->addMetaVariables(constraint.getContainedMetaVariables());
-            return internalBdd.constraint(constraint.internalBdd);
+            return Bdd<LibraryType>(this->getDdManager(), internalBdd.restrict(constraint), Dd<LibraryType>::joinMetaVariables(*this, constraint));
         }
         
         template<DdType LibraryType>
@@ -191,7 +166,7 @@ namespace storm {
         
         template<DdType LibraryType>
         Bdd<LibraryType> Bdd<LibraryType>::getSupport() const {
-            return Bdd<LibraryType>(internalBdd.getSupport());
+            return Bdd<LibraryType>(this->getDdManager(), internalBdd.getSupport(), this->getContainedMetaVariables());
         }
         
         template<DdType LibraryType>
@@ -233,6 +208,26 @@ namespace storm {
             internalBdd.exportToDot(filename, this->getDdManager()->getDdVariableNames());
         }
         
+        template<DdType LibraryType>
+        Bdd<LibraryType> Bdd<LibraryType>::getCube(std::set<storm::expressions::Variable> const& metaVariables) const {
+            Bdd<LibraryType> cube = this->getDdManager()->getBddOne();
+            for (auto const& metaVariable : metaVariables) {
+                STORM_LOG_THROW(this->containsMetaVariable(metaVariable), storm::exceptions::InvalidArgumentException, "Cannot abstract from meta variable '" << metaVariable.getName() << "' that is not present in the DD.");
+                cube &= this->getDdManager()->getMetaVariable(metaVariable).getCube();
+            }
+            return cube;
+        }
+        
+        template<DdType LibraryType>
+        Bdd<LibraryType>::operator InternalBdd<LibraryType>() {
+            return internalBdd;
+        }
+
+        template<DdType LibraryType>
+        Bdd<LibraryType>::operator InternalBdd<LibraryType> const() const {
+            return internalBdd;
+        }
+        
         template class Bdd<storm::dd::DdType::CUDD>;
     }
 }
\ No newline at end of file
diff --git a/src/storage/dd/Bdd.h b/src/storage/dd/Bdd.h
index b116e95dd..ad9c55c08 100644
--- a/src/storage/dd/Bdd.h
+++ b/src/storage/dd/Bdd.h
@@ -215,7 +215,21 @@ namespace storm {
             
             virtual void exportToDot(std::string const& filename) const override;
             
+            /*!
+             * Retrieves the cube of all given meta variables.
+             *
+             * @param metaVariables The variables for which to create the cube.
+             * @return The resulting cube.
+             */
+            Bdd<LibraryType> getCube(std::set<storm::expressions::Variable> const& metaVariables) const;
+            
         private:
+            /*!
+             * We provide a conversion operator from the BDD to its internal type to ease calling the internal functions.
+             */
+            operator InternalBdd<LibraryType>();
+            operator InternalBdd<LibraryType> const() const;
+            
             /*!
              * Creates a DD that encapsulates the given CUDD ADD.
              *
@@ -235,8 +249,8 @@ namespace storm {
              * @param comparisonType The relation that needs to hold for the values (wrt. to the given value).
              * @param value The value to compare with.
              */
-            Bdd(std::shared_ptr<DdManager<LibraryType> const> ddManager, std::vector<double> const& explicitValues, storm::dd::Odd<LibraryType> const& odd, std::set<storm::expressions::Variable> const& metaVariables, storm::logic::ComparisonType comparisonType, double value);
-            
+            static Bdd<LibraryType> fromVector(std::shared_ptr<DdManager<LibraryType> const> ddManager, std::vector<double> const& explicitValues, storm::dd::Odd<LibraryType> const& odd, std::set<storm::expressions::Variable> const& metaVariables, storm::logic::ComparisonType comparisonType, double value);
+
             /*!
              * Builds a BDD representing the values that make the given filter function evaluate to true.
              *
@@ -248,8 +262,7 @@ namespace storm {
              * @return The resulting (CUDD) BDD.
              */
             template<typename ValueType>
-            static BDD 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 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);
             
             // The internal BDD that depends on the chosen library.
             InternalBdd<LibraryType> internalBdd;
diff --git a/src/storage/dd/Dd.cpp b/src/storage/dd/Dd.cpp
index 5d0b32cef..4f190a134 100644
--- a/src/storage/dd/Dd.cpp
+++ b/src/storage/dd/Dd.cpp
@@ -62,28 +62,20 @@ namespace storm {
         
         template<DdType LibraryType>
         std::vector<uint_fast64_t> Dd<LibraryType>::getSortedVariableIndices() const {
-            return getSortedVariableIndices(*this->getDdManager(), this->getContainedMetaVariables());
+            return this->getDdManager()->getSortedVariableIndices(this->getContainedMetaVariables());
         }
         
         template<DdType LibraryType>
-        std::vector<uint_fast64_t> Dd<LibraryType>::getSortedVariableIndices(DdManager<LibraryType> const& manager, 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()) {
-                    ddVariableIndices.push_back(ddVariable.getIndex());
-                }
-            }
-            
-            // Next, we need to sort them, since they may be arbitrarily ordered otherwise.
-            std::sort(ddVariableIndices.begin(), ddVariableIndices.end());
-            return ddVariableIndices;
+        std::set<storm::expressions::Variable> Dd<LibraryType>::joinMetaVariables(storm::dd::Dd<LibraryType> const& first, storm::dd::Dd<LibraryType> const& second) {
+            std::set<storm::expressions::Variable> metaVariables;
+            std::set_union(first.getContainedMetaVariables().begin(), first.getContainedMetaVariables().end(), second.getContainedMetaVariables().begin(), second.getContainedMetaVariables().end(), std::inserter(metaVariables, metaVariables.begin()));
+            return metaVariables;
         }
         
         template<DdType LibraryType>
-        std::set<storm::expressions::Variable> Dd<LibraryType>::joinMetaVariables(storm::dd::Dd<LibraryType> const& first, storm::dd::Dd<LibraryType> const& second) {
+        std::set<storm::expressions::Variable> Dd<LibraryType>::subtractMetaVariables(storm::dd::Dd<LibraryType> const& first, storm::dd::Dd<LibraryType> const& second) {
             std::set<storm::expressions::Variable> metaVariables;
-            std::set_union(first.getContainedMetaVariables().begin(), first.getContainedMetaVariables().end(), second.getContainedMetaVariables().begin(), second.getContainedMetaVariables().end(), std::inserter(metaVariables, metaVariables.begin()));
+            std::set_difference(first.getContainedMetaVariables().begin(), first.getContainedMetaVariables().end(), second.getContainedMetaVariables().begin(), second.getContainedMetaVariables().end(), std::inserter(metaVariables, metaVariables.begin()));
             return metaVariables;
         }
         
diff --git a/src/storage/dd/Dd.h b/src/storage/dd/Dd.h
index 7d007153d..be3181f3c 100644
--- a/src/storage/dd/Dd.h
+++ b/src/storage/dd/Dd.h
@@ -114,15 +114,6 @@ namespace storm {
              */
             std::vector<uint_fast64_t> getSortedVariableIndices() const;
             
-            /*!
-             * Retrieves the (sorted) list of the variable indices of the DD variables given by the meta variable set.
-             *
-             * @param manager The manager responsible for the DD.
-             * @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(DdManager<LibraryType> const& manager, std::set<storm::expressions::Variable> const& metaVariables);
-            
             /*!
              * Adds the given set of meta variables to the DD.
              *
@@ -168,6 +159,15 @@ namespace storm {
              */
             static std::set<storm::expressions::Variable> joinMetaVariables(storm::dd::Dd<LibraryType> const& first, storm::dd::Dd<LibraryType> const& second);
             
+            /*!
+             * Retrieves the set of meta variables that are contained in the first but not the second DD.
+             *
+             * @param first The first DD.
+             * @param second The second DD.
+             * @return The resulting set of meta variables.
+             */
+            static std::set<storm::expressions::Variable> subtractMetaVariables(storm::dd::Dd<LibraryType> const& first, storm::dd::Dd<LibraryType> const& second);
+            
         private:
             // A pointer to the manager responsible for this DD.
             std::shared_ptr<DdManager<LibraryType> const> ddManager;
diff --git a/src/storage/dd/DdManager.cpp b/src/storage/dd/DdManager.cpp
index e69de29bb..e9a21873c 100644
--- a/src/storage/dd/DdManager.cpp
+++ b/src/storage/dd/DdManager.cpp
@@ -0,0 +1,20 @@
+
+
+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) {
+            std::vector<uint_fast64_t> ddVariableIndices;
+            for (auto const& metaVariableName : metaVariables) {
+                auto const& metaVariable = manager.getMetaVariable(metaVariableName);
+                for (auto const& ddVariable : metaVariable.getDdVariables()) {
+                    ddVariableIndices.push_back(ddVariable.getIndex());
+                }
+            }
+            
+            // Next, we need to sort them, since they may be arbitrarily ordered otherwise.
+            std::sort(ddVariableIndices.begin(), ddVariableIndices.end());
+            return ddVariableIndices;
+        }
+    }
+}
\ No newline at end of file
diff --git a/src/storage/dd/DdManager.h b/src/storage/dd/DdManager.h
index 3c1d5e70c..11d378e46 100644
--- a/src/storage/dd/DdManager.h
+++ b/src/storage/dd/DdManager.h
@@ -14,6 +14,16 @@ namespace storm {
             Bdd<LibraryType> getBddOne() const;
             Bdd<LibraryType> getBddZero() const;
             DdMetaVariable<LibraryType> const& getMetaVariable(storm::expressions::Variable const& variable) const;
+            std::vector<std::string> getDdVariableNames() const;
+            
+            /*!
+             * Retrieves the (sorted) list of the variable indices of the DD variables given by the meta variable set.
+             *
+             * @param manager The manager responsible for the DD.
+             * @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);
         };
     }
 }
diff --git a/src/storage/dd/DdMetaVariable.h b/src/storage/dd/DdMetaVariable.h
index 555569774..1cc920237 100644
--- a/src/storage/dd/DdMetaVariable.h
+++ b/src/storage/dd/DdMetaVariable.h
@@ -1,6 +1,8 @@
 #ifndef STORM_STORAGE_DD_DDMETAVARIBLE_H_
 #define STORM_STORAGE_DD_DDMETAVARIBLE_H_
 
+#include <vector>
+
 #include "src/storage/dd/DdType.h"
 
 namespace storm {
@@ -9,7 +11,8 @@ namespace storm {
         template<DdType LibraryType>
         class DdMetaVariable {
         public:
-            InternalBdd<LibraryType> getCube() const;
+            Bdd<LibraryType> getCube() const;
+            uint_fast64_t getNumberOfDdVariables() const;
         };
     }
 }
diff --git a/src/storage/dd/cudd/InternalCuddBdd.cpp b/src/storage/dd/cudd/InternalCuddBdd.cpp
index 52db5fab3..8ac0bac48 100644
--- a/src/storage/dd/cudd/InternalCuddBdd.cpp
+++ b/src/storage/dd/cudd/InternalCuddBdd.cpp
@@ -2,6 +2,17 @@
 
 namespace storm {
     namespace dd {
+        InternalBdd<DdType::CUDD>::InternalBdd(std::shared_ptr<DdManager<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);
+            uint_fast64_t offset = 0;
+            return BDD(ddManager->getCuddManager(), fromVectorRec(ddManager->getCuddManager().getManager(), offset, 0, ddVariableIndices.size(), values, odd, ddVariableIndices, filter));
+        }
+        
         bool InternalBdd<DdType::CUDD>::operator==(InternalBdd<DdType::CUDD> const& other) const {
             return this->getCuddBdd() == other.getCuddBdd();
         }
@@ -11,7 +22,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->getDdManager(), this->getCuddBdd().Ite(thenDd.getCuddBdd(), elseDd.getCuddBdd()), metaVariableNames);
+            return InternalBdd<DdType::CUDD>(this->getCuddBdd().Ite(thenDd.getCuddBdd(), elseDd.getCuddBdd()));
         }
         
         InternalBdd<DdType::CUDD> InternalBdd<DdType::CUDD>::operator||(InternalBdd<DdType::CUDD> const& other) const {
@@ -37,15 +48,15 @@ namespace storm {
         }
         
         InternalBdd<DdType::CUDD> InternalBdd<DdType::CUDD>::iff(InternalBdd<DdType::CUDD> const& other) const {
-            return InternalBdd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().Xnor(other.getCuddBdd()), metaVariables);
+            return InternalBdd<DdType::CUDD>(this->getCuddBdd().Xnor(other.getCuddBdd()));
         }
         
         InternalBdd<DdType::CUDD> InternalBdd<DdType::CUDD>::exclusiveOr(InternalBdd<DdType::CUDD> const& other) const {
-            return InternalBdd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().Xor(other.getCuddBdd()), metaVariables);
+            return InternalBdd<DdType::CUDD>(this->getCuddBdd().Xor(other.getCuddBdd()));
         }
         
         InternalBdd<DdType::CUDD> InternalBdd<DdType::CUDD>::implies(InternalBdd<DdType::CUDD> const& other) const {
-            return InternalBdd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().Ite(other.getCuddBdd(), this->getDdManager()->getBddOne().getCuddBdd()), metaVariables);
+            return InternalBdd<DdType::CUDD>(this->getCuddBdd().Ite(other.getCuddBdd(), this->getDdManager()->getBddOne().getCuddBdd()), metaVariables);
         }
         
         InternalBdd<DdType::CUDD> InternalBdd<DdType::CUDD>::operator!() const {
@@ -164,15 +175,9 @@ namespace storm {
             return this->getCuddBdd().getNode();
         }
         
-
-        
-        
-        
-        
-        
-        
-        Add<DdType::CUDD> InternalBdd<DdType::CUDD>::toAdd() const {
-            return Add<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().Add(), this->getContainedMetaVariables());
+        template<typename ValueType>
+        Add<DdType::CUDD, ValueType> InternalBdd<DdType::CUDD>::toAdd() const {
+            return Add<DdType::CUDD, ValueType>(this->getCuddBdd().Add());
         }
         
         
@@ -191,12 +196,6 @@ namespace storm {
         
         
         
-        template<typename ValueType>
-        BDD 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 = getSortedVariableIndices(*ddManager, metaVariables);
-            uint_fast64_t offset = 0;
-            return BDD(ddManager->getCuddManager(), fromVectorRec(ddManager->getCuddManager().getManager(), offset, 0, ddVariableIndices.size(), values, odd, ddVariableIndices, filter));
-        }
         
         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) {
@@ -290,27 +289,5 @@ namespace storm {
             }
         }
         
-        InternalBdd<DdType::CUDD>::InternalBdd(std::shared_ptr<DdManager<DdType::CUDD> const> ddManager, BDD cuddBdd, std::set<storm::expressions::Variable> const& containedMetaVariables) : Dd<DdType::CUDD>(ddManager, containedMetaVariables), cuddBdd(cuddBdd) {
-            // Intentionally left empty.
-        }
-        
-        InternalBdd<DdType::CUDD>::InternalBdd(std::shared_ptr<DdManager<DdType::CUDD> const> ddManager, std::vector<double> const& explicitValues, storm::dd::Odd<DdType::CUDD> const& odd, std::set<storm::expressions::Variable> const& metaVariables, storm::logic::ComparisonType comparisonType, double value) : Dd<DdType::CUDD>(ddManager, metaVariables) {
-            switch (comparisonType) {
-                case storm::logic::ComparisonType::Less:
-                    this->cuddBdd = fromVector<double>(ddManager, explicitValues, odd, metaVariables, std::bind(std::greater<double>(), value, std::placeholders::_1));
-                    break;
-                case storm::logic::ComparisonType::LessEqual:
-                    this->cuddBdd = fromVector<double>(ddManager, explicitValues, odd, metaVariables, std::bind(std::greater_equal<double>(), value, std::placeholders::_1));
-                    break;
-                case storm::logic::ComparisonType::Greater:
-                    this->cuddBdd = fromVector<double>(ddManager, explicitValues, odd, metaVariables, std::bind(std::less<double>(), value, std::placeholders::_1));
-                    break;
-                case storm::logic::ComparisonType::GreaterEqual:
-                    this->cuddBdd = fromVector<double>(ddManager, explicitValues, odd, metaVariables, std::bind(std::less_equal<double>(), value, std::placeholders::_1));
-                    break;
-            }
-            
-        }
-        
     }
 }
\ No newline at end of file
diff --git a/src/storage/dd/cudd/InternalCuddBdd.h b/src/storage/dd/cudd/InternalCuddBdd.h
index 5a8209aa9..f34481cc7 100644
--- a/src/storage/dd/cudd/InternalCuddBdd.h
+++ b/src/storage/dd/cudd/InternalCuddBdd.h
@@ -1,10 +1,15 @@
 #ifndef STORM_STORAGE_DD_CUDD_INTERNALCUDDBDD_H_
 #define STORM_STORAGE_DD_CUDD_INTERNALCUDDBDD_H_
 
+#include <set>
+
 #include "src/storage/dd/DdType.h"
 #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.
 #include "cuddObj.hh"
 
@@ -29,16 +34,13 @@ namespace storm {
         class InternalBdd<storm::dd::DdType::CUDD> {
         public:
             /*!
-             * Constructs a BDD representation of all encodings that are in the requested relation with the given value.
+             * Creates a DD that encapsulates the given CUDD ADD.
              *
-             * @param ddManager The DD manager responsible for the resulting BDD.
-             * @param explicitValues The explicit values to compare to the given value.
-             * @param odd The ODD used for the translation from the explicit representation to a symbolic one.
-             * @param metaVariables The meta variables to use for the symbolic encoding.
-             * @param comparisonType The relation that needs to hold for the values (wrt. to the given value).
-             * @param value The value to compare with.
+             * @param ddManager The manager responsible for this DD.
+             * @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, std::vector<double> const& explicitValues, storm::dd::Odd<DdType::CUDD> const& odd, std::set<storm::expressions::Variable> const& metaVariables, storm::logic::ComparisonType comparisonType, double value);
+            InternalBdd(std::shared_ptr<DdManager<DdType::CUDD> const> ddManager, BDD cuddBdd);
             
             // Instantiate all copy/move constructors/assignments with the default implementation.
             InternalBdd() = default;
@@ -47,6 +49,19 @@ namespace storm {
             InternalBdd(InternalBdd<DdType::CUDD>&& other) = default;
             InternalBdd& operator=(InternalBdd<DdType::CUDD>&& other) = default;
 
+            /*!
+             * Builds a BDD representing the values that make the given filter function evaluate to true.
+             *
+             * @param ddManager The manager responsible for the BDD.
+             * @param values The values that are to be checked against the filter function.
+             * @param odd The ODD used for the translation.
+             * @param metaVariables The meta variables used for the translation.
+             * @param filter The filter that evaluates whether an encoding is to be mapped to 0 or 1.
+             * @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);
+            
             /*!
              * Retrieves whether the two BDDs represent the same function.
              *
@@ -165,7 +180,7 @@ namespace storm {
              * @param metaVariablePairs A vector of meta variable pairs that are to be swapped for one another.
              * @return The resulting BDD.
              */
-            InternalBdd<DdType::CUDD> swapVariables(std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& metaVariablePairs) const;
+            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;
             
             /*!
              * Computes the logical and of the current and the given BDD and existentially abstracts from the given set
@@ -175,7 +190,7 @@ namespace storm {
              * @param existentialVariables The variables from which to existentially abstract.
              * @return A BDD representing the result.
              */
-            InternalBdd<DdType::CUDD> andExists(InternalBdd<DdType::CUDD> const& other, std::set<storm::expressions::Variable> const& existentialVariables) const;
+            InternalBdd<DdType::CUDD> andExists(InternalBdd<DdType::CUDD> const& other, InternalBdd<storm::dd::DdType::CUDD> const& cube) const;
             
             /*!
              * Computes the constraint of the current BDD with the given constraint. That is, the function value of the
@@ -209,7 +224,7 @@ namespace storm {
              *
              * @return The number of encodings that are mapped to a non-zero value.
              */
-            uint_fast64_t getNonZeroCount() const;
+            uint_fast64_t getNonZeroCount(uint_fast64_t numberOfDdVariables) const;
             
             /*!
              * Retrieves the number of leaves of the DD.
@@ -271,28 +286,6 @@ namespace storm {
             storm::storage::BitVector toVector(storm::dd::Odd<DdType::CUDD> const& rowOdd) const;
             
         private:
-            /*!
-             * Creates a DD that encapsulates the given CUDD ADD.
-             *
-             * @param ddManager The manager responsible for this DD.
-             * @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, std::set<storm::expressions::Variable> const& containedMetaVariables = std::set<storm::expressions::Variable>());
-            
-            /*!
-             * Builds a BDD representing the values that make the given filter function evaluate to true.
-             *
-             * @param ddManager The manager responsible for the BDD.
-             * @param values The values that are to be checked against the filter function.
-             * @param odd The ODD used for the translation.
-             * @param metaVariables The meta variables used for the translation.
-             * @param filter The filter that evaluates whether an encoding is to be mapped to 0 or 1.
-             * @return The resulting (CUDD) BDD.
-             */
-            template<typename ValueType>
-            static BDD 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);
-            
             /*!
              * Builds a BDD representing the values that make the given filter function evaluate to true.
              *
@@ -337,6 +330,8 @@ namespace storm {
              */
             DdNode* getCuddDdNode() const;
             
+            std::shared_ptr<DdManager<DdType::CUDD> const> ddManager;
+            
             BDD cuddBdd;
         };
     }