same shit, different day

Former-commit-id: 495b9fd952

src/storage/dd/Add.cpp

@@ -386,238 +386,424 @@ namespace storm {
         std::vector<ValueType> Add<LibraryType, ValueType>::toVector(Odd<LibraryType> const& rowOdd) const {
             std::vector<ValueType> result(rowOdd.getTotalOffset());
             std::vector<uint_fast64_t> ddVariableIndices = this->getDdManager()->getSortedVariableIndices();
-            addToVector(rowOdd, ddVariableIndices, result);
+            addToExplicitVector(rowOdd, ddVariableIndices, result);
             return result;
         }
+        
+        template<DdType LibraryType, typename ValueType>
+        void Add<LibraryType, ValueType>::addToExplicitVector(Odd<LibraryType> const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<ValueType>& targetVector) const {
+            internalAdd.composeWithExplicitVector(odd, ddVariableIndices, targetVector, std::plus<ValueType>());
+        }
+        
+        template<DdType LibraryType, typename ValueType>
+        std::vector<ValueType> Add<LibraryType, ValueType>::toVector(std::set<storm::expressions::Variable> const& groupMetaVariables, storm::dd::Odd<LibraryType> const& rowOdd, std::vector<uint_fast64_t> const& groupOffsets) const {
+            std::set<storm::expressions::Variable> rowMetaVariables;
+            
+            // Prepare the proper sets of meta variables.
+            for (auto const& variable : this->getContainedMetaVariables()) {
+                if (groupMetaVariables.find(variable) != groupMetaVariables.end()) {
+                    continue;
+                }
+                
+                rowMetaVariables.insert(variable);
+            }
+            std::vector<uint_fast64_t> ddGroupVariableIndices;
+            for (auto const& variable : groupMetaVariables) {
+                DdMetaVariable<LibraryType> const& metaVariable = this->getDdManager()->getMetaVariable(variable);
+                for (auto const& ddVariable : metaVariable.getDdVariables()) {
+                    ddGroupVariableIndices.push_back(ddVariable.getIndex());
+                }
+            }
+            std::vector<uint_fast64_t> ddRowVariableIndices;
+            for (auto const& variable : rowMetaVariables) {
+                DdMetaVariable<LibraryType> const& metaVariable = this->getDdManager()->getMetaVariable(variable);
+                for (auto const& ddVariable : metaVariable.getDdVariables()) {
+                    ddRowVariableIndices.push_back(ddVariable.getIndex());
+                }
+            }
+            
+            // Use the group variables to split the ADD into separate ADDs for each group.
+            std::vector<InternalAdd<LibraryType, ValueType>> groups = internalAdd.splitIntoGroups(ddGroupVariableIndices);
+            
+            // Now iterate over the groups and add them to the resulting vector.
+            std::vector<ValueType> result(groupOffsets.back(), storm::utility::zero<ValueType>());
+            for (uint_fast64_t i = 0; i < groups.size(); ++i) {
+                internalAdd.composeWithExplicitVector(rowOdd, ddRowVariableIndices, groupOffsets, result, std::plus<ValueType>());
+                
+                // FIXME: something more needed? modification of groupOffsets?
+            }
+            
+            return result;
+        }
+        
+        template<DdType LibraryType, typename ValueType>
+        storm::storage::SparseMatrix<ValueType> Add<LibraryType, ValueType>::toMatrix() const {
+            std::set<storm::expressions::Variable> rowVariables;
+            std::set<storm::expressions::Variable> columnVariables;
+            
+            for (auto const& variable : this->getContainedMetaVariables()) {
+                if (variable.getName().size() > 0 && variable.getName().back() == '\'') {
+                    columnVariables.insert(variable);
+                } else {
+                    rowVariables.insert(variable);
+                }
+            }
+            
+            return toMatrix(rowVariables, columnVariables, Odd<LibraryType>(this->sumAbstract(rowVariables)), Odd<LibraryType>(this->sumAbstract(columnVariables)));
+        }
+        
+        template<DdType LibraryType, typename ValueType>
+        storm::storage::SparseMatrix<ValueType> Add<LibraryType, ValueType>::toMatrix(storm::dd::Odd<LibraryType> const& rowOdd, storm::dd::Odd<LibraryType> const& columnOdd) const {
+            std::set<storm::expressions::Variable> rowMetaVariables;
+            std::set<storm::expressions::Variable> columnMetaVariables;
+            
+            for (auto const& variable : this->getContainedMetaVariables()) {
+                if (variable.getName().size() > 0 && variable.getName().back() == '\'') {
+                    columnMetaVariables.insert(variable);
+                } else {
+                    rowMetaVariables.insert(variable);
+                }
+            }
+            
+            return toMatrix(rowMetaVariables, columnMetaVariables, rowOdd, columnOdd);
+        }
+        
+        template<DdType LibraryType, typename ValueType>
+        storm::storage::SparseMatrix<ValueType> Add<LibraryType, ValueType>::toMatrix(std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, storm::dd::Odd<LibraryType> const& rowOdd, storm::dd::Odd<LibraryType> const& columnOdd) const {
+            std::vector<uint_fast64_t> ddRowVariableIndices;
+            std::vector<uint_fast64_t> ddColumnVariableIndices;
+            
+            for (auto const& variable : rowMetaVariables) {
+                DdMetaVariable<LibraryType> const& metaVariable = this->getDdManager()->getMetaVariable(variable);
+                for (auto const& ddVariable : metaVariable.getDdVariables()) {
+                    ddRowVariableIndices.push_back(ddVariable.getIndex());
+                }
+            }
+            std::sort(ddRowVariableIndices.begin(), ddRowVariableIndices.end());
+            
+            for (auto const& variable : columnMetaVariables) {
+                DdMetaVariable<LibraryType> const& metaVariable = this->getDdManager()->getMetaVariable(variable);
+                for (auto const& ddVariable : metaVariable.getDdVariables()) {
+                    ddColumnVariableIndices.push_back(ddVariable.getIndex());
+                }
+            }
+            std::sort(ddColumnVariableIndices.begin(), ddColumnVariableIndices.end());
+            
+            // Prepare the vectors that represent the matrix.
+            std::vector<uint_fast64_t> rowIndications(rowOdd.getTotalOffset() + 1);
+            std::vector<storm::storage::MatrixEntry<uint_fast64_t, double>> columnsAndValues(this->getNonZeroCount());
+            
+            // Create a trivial row grouping.
+            std::vector<uint_fast64_t> trivialRowGroupIndices(rowIndications.size());
+            uint_fast64_t i = 0;
+            for (auto& entry : trivialRowGroupIndices) {
+                entry = i;
+                ++i;
+            }
+            
+            // Use the toMatrix function to compute the number of elements in each row. Using the flag, we prevent
+            // it from actually generating the entries in the entry vector.
+            internalAdd.toMatrixComponents(trivialRowGroupIndices, rowIndications, columnsAndValues, rowOdd, columnOdd, ddRowVariableIndices, ddColumnVariableIndices, false);
+            
+            // TODO: counting might be faster by just summing over the primed variables and then using the ODD to convert
+            // the resulting (DD) vector to an explicit vector.
+            
+            // Now that we computed the number of entries in each row, compute the corresponding offsets in the entry vector.
+            uint_fast64_t tmp = 0;
+            uint_fast64_t tmp2 = 0;
+            for (uint_fast64_t i = 1; i < rowIndications.size(); ++i) {
+                tmp2 = rowIndications[i];
+                rowIndications[i] = rowIndications[i - 1] + tmp;
+                std::swap(tmp, tmp2);
+            }
+            rowIndications[0] = 0;
+            
+            // Now actually fill the entry vector.
+            internalAdd.toMatrixComponents(trivialRowGroupIndices, rowIndications, columnsAndValues, rowOdd, columnOdd, ddRowVariableIndices, ddColumnVariableIndices, true);
+            
+            // Since the last call to toMatrixRec modified the rowIndications, we need to restore the correct values.
+            for (uint_fast64_t i = rowIndications.size() - 1; i > 0; --i) {
+                rowIndications[i] = rowIndications[i - 1];
+            }
+            rowIndications[0] = 0;
+            
+            // Construct matrix and return result.
+            return storm::storage::SparseMatrix<double>(columnOdd.getTotalOffset(), std::move(rowIndications), std::move(columnsAndValues), std::move(trivialRowGroupIndices), false);
+        }
+        
+        template<DdType LibraryType, typename ValueType>
+        storm::storage::SparseMatrix<ValueType> Add<LibraryType, ValueType>::toMatrix(std::set<storm::expressions::Variable> const& groupMetaVariables, storm::dd::Odd<LibraryType> const& rowOdd, storm::dd::Odd<LibraryType> const& columnOdd) const {
+            std::set<storm::expressions::Variable> rowMetaVariables;
+            std::set<storm::expressions::Variable> columnMetaVariables;
+            
+            for (auto const& variable : this->getContainedMetaVariables()) {
+                // If the meta variable is a group meta variable, we do not insert it into the set of row/column meta variables.
+                if (groupMetaVariables.find(variable) != groupMetaVariables.end()) {
+                    continue;
+                }
+                
+                if (variable.getName().size() > 0 && variable.getName().back() == '\'') {
+                    columnMetaVariables.insert(variable);
+                } else {
+                    rowMetaVariables.insert(variable);
+                }
+            }
+            
+            // Create the canonical row group sizes and build the matrix.
+            return toMatrix(rowMetaVariables, columnMetaVariables, groupMetaVariables, rowOdd, columnOdd);
+        }
+
+        template<DdType LibraryType, typename ValueType>
+        storm::storage::SparseMatrix<ValueType> Add<LibraryType, ValueType>::toMatrix(std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::set<storm::expressions::Variable> const& groupMetaVariables, storm::dd::Odd<LibraryType> const& rowOdd, storm::dd::Odd<LibraryType> const& columnOdd) const {
+            std::vector<uint_fast64_t> ddRowVariableIndices;
+            std::vector<uint_fast64_t> ddColumnVariableIndices;
+            std::vector<uint_fast64_t> ddGroupVariableIndices;
+            std::set<storm::expressions::Variable> rowAndColumnMetaVariables;
+            
+            for (auto const& variable : rowMetaVariables) {
+                DdMetaVariable<LibraryType> const& metaVariable = this->getDdManager()->getMetaVariable(variable);
+                for (auto const& ddVariable : metaVariable.getDdVariables()) {
+                    ddRowVariableIndices.push_back(ddVariable.getIndex());
+                }
+                rowAndColumnMetaVariables.insert(variable);
+            }
+            std::sort(ddRowVariableIndices.begin(), ddRowVariableIndices.end());
+            for (auto const& variable : columnMetaVariables) {
+                DdMetaVariable<LibraryType> const& metaVariable = this->getDdManager()->getMetaVariable(variable);
+                for (auto const& ddVariable : metaVariable.getDdVariables()) {
+                    ddColumnVariableIndices.push_back(ddVariable.getIndex());
+                }
+                rowAndColumnMetaVariables.insert(variable);
+            }
+            std::sort(ddColumnVariableIndices.begin(), ddColumnVariableIndices.end());
+            for (auto const& variable : groupMetaVariables) {
+                DdMetaVariable<LibraryType> const& metaVariable = this->getDdManager()->getMetaVariable(variable);
+                for (auto const& ddVariable : metaVariable.getDdVariables()) {
+                    ddGroupVariableIndices.push_back(ddVariable.getIndex());
+                }
+            }
+            std::sort(ddGroupVariableIndices.begin(), ddGroupVariableIndices.end());
+            
+            Bdd<LibraryType> columnVariableCube = Bdd<LibraryType>::getCube(*this->getDdManager(), columnMetaVariables);
+            
+            // Start by computing the offsets (in terms of rows) for each row group.
+            Add<LibraryType, uint_fast64_t> stateToNumberOfChoices = this->notZero().existsAbstract(columnMetaVariables).template toAdd<uint_fast64_t>().sumAbstract(groupMetaVariables);
+            std::vector<uint_fast64_t> rowGroupIndices = stateToNumberOfChoices.toVector(rowOdd);
+            rowGroupIndices.resize(rowGroupIndices.size() + 1);
+            uint_fast64_t tmp = 0;
+            uint_fast64_t tmp2 = 0;
+            for (uint_fast64_t i = 1; i < rowGroupIndices.size(); ++i) {
+                tmp2 = rowGroupIndices[i];
+                rowGroupIndices[i] = rowGroupIndices[i - 1] + tmp;
+                std::swap(tmp, tmp2);
+            }
+            rowGroupIndices[0] = 0;
+            
+            // Next, we split the matrix into one for each group. Note that this only works if the group variables are
+            // at the very top.
+            std::vector<InternalAdd<LibraryType, ValueType>> groups = internalAdd.splitIntoGroups(ddGroupVariableIndices);
+            
+            // Create the actual storage for the non-zero entries.
+            std::vector<storm::storage::MatrixEntry<uint_fast64_t, double>> columnsAndValues(this->getNonZeroCount());
+            
+            // Now compute the indices at which the individual rows start.
+            std::vector<uint_fast64_t> rowIndications(rowGroupIndices.back() + 1);
+            
+            std::vector<InternalAdd<LibraryType, uint_fast64_t>> statesWithGroupEnabled(groups.size());
+            InternalAdd<LibraryType, uint_fast64_t> stateToRowGroupCount = this->getDdManager()->template getAddZero<uint_fast64_t>();
+            for (uint_fast64_t i = 0; i < groups.size(); ++i) {
+                auto const& dd = groups[i];
+                
+                dd.toMatrixComponents(rowGroupIndices, rowIndications, columnsAndValues, rowOdd, columnOdd, ddRowVariableIndices, ddColumnVariableIndices, false);
+                
+                statesWithGroupEnabled[i] = dd.notZero().existsAbstract(columnVariableCube).template toAdd<uint_fast64_t>();
+                stateToRowGroupCount += statesWithGroupEnabled[i];
+                statesWithGroupEnabled[i].composeWithExplicitVector(rowOdd, ddRowVariableIndices, rowGroupIndices, std::plus<uint_fast64_t>());
+            }
+            
+            // Since we modified the rowGroupIndices, we need to restore the correct values.
+            stateToRowGroupCount.composeWithExplicitVector(rowOdd, ddRowVariableIndices, rowGroupIndices, std::minus<uint_fast64_t>());
+            
+            // Now that we computed the number of entries in each row, compute the corresponding offsets in the entry vector.
+            tmp = 0;
+            tmp2 = 0;
+            for (uint_fast64_t i = 1; i < rowIndications.size(); ++i) {
+                tmp2 = rowIndications[i];
+                rowIndications[i] = rowIndications[i - 1] + tmp;
+                std::swap(tmp, tmp2);
+            }
+            rowIndications[0] = 0;
+            
+            // Now actually fill the entry vector.
+            for (uint_fast64_t i = 0; i < groups.size(); ++i) {
+                auto const& dd = groups[i];
+                
+                dd.toMatrixComponents(rowGroupIndices, rowIndications, columnsAndValues, rowOdd, columnOdd, ddRowVariableIndices, ddColumnVariableIndices, true);
+                
+                statesWithGroupEnabled[i].composeWithExplicitVector(rowOdd, ddRowVariableIndices, rowGroupIndices, std::plus<uint_fast64_t>());
+            }
+            
+            // Since we modified the rowGroupIndices, we need to restore the correct values.
+            stateToRowGroupCount.composeWithExplicitVector(rowOdd, ddRowVariableIndices, rowGroupIndices, std::minus<uint_fast64_t>());
+            
+            // Since the last call to toMatrixRec modified the rowIndications, we need to restore the correct values.
+            for (uint_fast64_t i = rowIndications.size() - 1; i > 0; --i) {
+                rowIndications[i] = rowIndications[i - 1];
+            }
+            rowIndications[0] = 0;
+            
+            return storm::storage::SparseMatrix<double>(columnOdd.getTotalOffset(), std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices), true);
+        }
+
+        template<DdType LibraryType, typename ValueType>
+        std::pair<storm::storage::SparseMatrix<ValueType>, std::vector<ValueType>> Add<LibraryType, ValueType>::toMatrixVector(storm::dd::Add<LibraryType, ValueType> const& vector, std::vector<uint_fast64_t>&& rowGroupSizes, std::set<storm::expressions::Variable> const& groupMetaVariables, storm::dd::Odd<LibraryType> const& rowOdd, storm::dd::Odd<LibraryType> const& columnOdd) const {
+            std::set<storm::expressions::Variable> rowMetaVariables;
+            std::set<storm::expressions::Variable> columnMetaVariables;
+            
+            for (auto const& variable : this->getContainedMetaVariables()) {
+                // If the meta variable is a group meta variable, we do not insert it into the set of row/column meta variables.
+                if (groupMetaVariables.find(variable) != groupMetaVariables.end()) {
+                    continue;
+                }
+                
+                if (variable.getName().size() > 0 && variable.getName().back() == '\'') {
+                    columnMetaVariables.insert(variable);
+                } else {
+                    rowMetaVariables.insert(variable);
+                }
+            }
+            
+            // Create the canonical row group sizes and build the matrix.
+            return toMatrixVector(vector, std::move(rowGroupSizes), rowMetaVariables, columnMetaVariables, groupMetaVariables, rowOdd, columnOdd);
+        }
+
+        template<DdType LibraryType, typename ValueType>
+        std::pair<storm::storage::SparseMatrix<ValueType>, std::vector<ValueType>> Add<LibraryType, ValueType>::toMatrixVector(storm::dd::Add<LibraryType, ValueType> const& vector, std::vector<uint_fast64_t>&& rowGroupIndices, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::set<storm::expressions::Variable> const& groupMetaVariables, storm::dd::Odd<LibraryType> const& rowOdd, storm::dd::Odd<LibraryType> const& columnOdd) const {
+            std::vector<uint_fast64_t> ddRowVariableIndices;
+            std::vector<uint_fast64_t> ddColumnVariableIndices;
+            std::vector<uint_fast64_t> ddGroupVariableIndices;
+            std::set<storm::expressions::Variable> rowAndColumnMetaVariables;
+            
+            for (auto const& variable : rowMetaVariables) {
+                DdMetaVariable<LibraryType> const& metaVariable = this->getDdManager()->getMetaVariable(variable);
+                for (auto const& ddVariable : metaVariable.getDdVariables()) {
+                    ddRowVariableIndices.push_back(ddVariable.getIndex());
+                }
+                rowAndColumnMetaVariables.insert(variable);
+            }
+            std::sort(ddRowVariableIndices.begin(), ddRowVariableIndices.end());
+            for (auto const& variable : columnMetaVariables) {
+                DdMetaVariable<LibraryType> const& metaVariable = this->getDdManager()->getMetaVariable(variable);
+                for (auto const& ddVariable : metaVariable.getDdVariables()) {
+                    ddColumnVariableIndices.push_back(ddVariable.getIndex());
+                }
+                rowAndColumnMetaVariables.insert(variable);
+            }
+            std::sort(ddColumnVariableIndices.begin(), ddColumnVariableIndices.end());
+            for (auto const& variable : groupMetaVariables) {
+                DdMetaVariable<LibraryType> const& metaVariable = this->getDdManager()->getMetaVariable(variable);
+                for (auto const& ddVariable : metaVariable.getDdVariables()) {
+                    ddGroupVariableIndices.push_back(ddVariable.getIndex());
+                }
+            }
+            std::sort(ddGroupVariableIndices.begin(), ddGroupVariableIndices.end());
+            
+            Bdd<LibraryType> columnVariableCube = Bdd<LibraryType>::getCube(*this->getDdManager(), columnMetaVariables);
+
+            // Transform the row group sizes to the actual row group indices.
+            rowGroupIndices.resize(rowGroupIndices.size() + 1);
+            uint_fast64_t tmp = 0;
+            uint_fast64_t tmp2 = 0;
+            for (uint_fast64_t i = 1; i < rowGroupIndices.size(); ++i) {
+                tmp2 = rowGroupIndices[i];
+                rowGroupIndices[i] = rowGroupIndices[i - 1] + tmp;
+                std::swap(tmp, tmp2);
+            }
+            rowGroupIndices[0] = 0;
+            
+            // Create the explicit vector we need to fill later.
+            std::vector<double> explicitVector(rowGroupIndices.back());
+            
+            // Next, we split the matrix into one for each group. Note that this only works if the group variables are at the very top.
+            std::vector<std::pair<InternalAdd<LibraryType, ValueType>, InternalAdd<LibraryType, ValueType>>> groups = internalAdd.splitIntoGroups(vector, ddGroupVariableIndices);
+
+            // Create the actual storage for the non-zero entries.
+            std::vector<storm::storage::MatrixEntry<uint_fast64_t, double>> columnsAndValues(this->getNonZeroCount());
+            
+            // Now compute the indices at which the individual rows start.
+            std::vector<uint_fast64_t> rowIndications(rowGroupIndices.back() + 1);
+            
+            std::vector<InternalAdd<LibraryType, uint_fast64_t>> statesWithGroupEnabled(groups.size());
+            InternalAdd<LibraryType, uint_fast64_t> stateToRowGroupCount = this->getDdManager()->template getAddZero<uint_fast64_t>();
+            for (uint_fast64_t i = 0; i < groups.size(); ++i) {
+                std::pair<InternalAdd<LibraryType, ValueType>, InternalAdd<LibraryType, ValueType>> const& ddPair = groups[i];
+                
+                ddPair.first.toMatrixComponents(rowGroupIndices, rowIndications, columnsAndValues, rowOdd, columnOdd, ddRowVariableIndices, ddColumnVariableIndices, false);
+                ddPair.second.composeWithExplicitVector(rowOdd, ddRowVariableIndices, rowGroupIndices, explicitVector, std::plus<uint_fast64_t>());
+                
+                statesWithGroupEnabled[i] = (ddPair.first.notZero().existsAbstract(columnVariableCube) || ddPair.second.notZero()).template toAdd<uint_fast64_t>();
+                stateToRowGroupCount += statesWithGroupEnabled[i];
+                statesWithGroupEnabled[i].composeWithExplicitVector(rowOdd, ddRowVariableIndices, rowGroupIndices, std::plus<uint_fast64_t>());
+            }
+            
+            // Since we modified the rowGroupIndices, we need to restore the correct values.
+            stateToRowGroupCount.composeWithExplicitVector(rowOdd, ddRowVariableIndices, rowGroupIndices, std::minus<uint_fast64_t>());
+
+            // Now that we computed the number of entries in each row, compute the corresponding offsets in the entry vector.
+            tmp = 0;
+            tmp2 = 0;
+            for (uint_fast64_t i = 1; i < rowIndications.size(); ++i) {
+                tmp2 = rowIndications[i];
+                rowIndications[i] = rowIndications[i - 1] + tmp;
+                std::swap(tmp, tmp2);
+            }
+            rowIndications[0] = 0;
+            
+            // Now actually fill the entry vector.
+            for (uint_fast64_t i = 0; i < groups.size(); ++i) {
+                auto const& dd = groups[i].first;
+                
+                dd.toMatrixComponents(rowGroupIndices, rowIndications, columnsAndValues, rowOdd, columnOdd, ddRowVariableIndices, ddColumnVariableIndices, true);
+                
+                statesWithGroupEnabled[i].composeWithExplicitVector(rowOdd, ddRowVariableIndices, rowGroupIndices, std::plus<uint_fast64_t>());
+            }
+            
+            // Since we modified the rowGroupIndices, we need to restore the correct values.
+            stateToRowGroupCount.composeWithExplicitVector(rowOdd, ddRowVariableIndices, rowGroupIndices, std::minus<uint_fast64_t>());
+            
+            // Since the last call to toMatrixRec modified the rowIndications, we need to restore the correct values.
+            for (uint_fast64_t i = rowIndications.size() - 1; i > 0; --i) {
+                rowIndications[i] = rowIndications[i - 1];
+            }
+            rowIndications[0] = 0;
+            
+            return std::make_pair(storm::storage::SparseMatrix<double>(columnOdd.getTotalOffset(), std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices), true), std::move(explicitVector));
+        }
 
-//        template<DdType LibraryType, typename ValueType>
-//        std::vector<ValueType> Add<LibraryType, ValueType>::toVector(std::set<storm::expressions::Variable> const& groupMetaVariables, storm::dd::Odd<LibraryType> const& rowOdd, std::vector<uint_fast64_t> const& groupOffsets) const {
-//            std::set<storm::expressions::Variable> rowMetaVariables;
-//            
-//            // Prepare the proper sets of meta variables.
-//            for (auto const& variable : this->getContainedMetaVariables()) {
-//                if (groupMetaVariables.find(variable) != groupMetaVariables.end()) {
-//                    continue;
-//                }
-//                
-//                rowMetaVariables.insert(variable);
-//            }
-//            std::vector<uint_fast64_t> ddGroupVariableIndices;
-//            for (auto const& variable : groupMetaVariables) {
-//                DdMetaVariable<LibraryType> const& metaVariable = this->getDdManager()->getMetaVariable(variable);
-//                for (auto const& ddVariable : metaVariable.getDdVariables()) {
-//                    ddGroupVariableIndices.push_back(ddVariable.getIndex());
-//                }
-//            }
-//            std::vector<uint_fast64_t> ddRowVariableIndices;
-//            for (auto const& variable : rowMetaVariables) {
-//                DdMetaVariable<LibraryType> const& metaVariable = this->getDdManager()->getMetaVariable(variable);
-//                for (auto const& ddVariable : metaVariable.getDdVariables()) {
-//                    ddRowVariableIndices.push_back(ddVariable.getIndex());
-//                }
-//            }
-//            
-//            return internalAdd.toVector(ddGroupVariableIndices, rowOdd, ddRowVariableIndices, groupOffsets);
-//        }
-//        
-//        template<DdType LibraryType, typename ValueType>
-//        storm::storage::SparseMatrix<ValueType> Add<LibraryType, ValueType>::toMatrix() const {
-//            std::set<storm::expressions::Variable> rowVariables;
-//            std::set<storm::expressions::Variable> columnVariables;
-//            
-//            for (auto const& variable : this->getContainedMetaVariables()) {
-//                if (variable.getName().size() > 0 && variable.getName().back() == '\'') {
-//                    columnVariables.insert(variable);
-//                } else {
-//                    rowVariables.insert(variable);
-//                }
-//            }
-//            
-//            return toMatrix(rowVariables, columnVariables, Odd<LibraryType>(this->sumAbstract(rowVariables)), Odd<LibraryType>(this->sumAbstract(columnVariables)));
-//        }
-//        
-//        template<DdType LibraryType, typename ValueType>
-//        storm::storage::SparseMatrix<ValueType> Add<LibraryType, ValueType>::toMatrix(storm::dd::Odd<LibraryType> const& rowOdd, storm::dd::Odd<LibraryType> const& columnOdd) const {
-//            std::set<storm::expressions::Variable> rowMetaVariables;
-//            std::set<storm::expressions::Variable> columnMetaVariables;
-//            
-//            for (auto const& variable : this->getContainedMetaVariables()) {
-//                if (variable.getName().size() > 0 && variable.getName().back() == '\'') {
-//                    columnMetaVariables.insert(variable);
-//                } else {
-//                    rowMetaVariables.insert(variable);
-//                }
-//            }
-//            
-//            return toMatrix(rowMetaVariables, columnMetaVariables, rowOdd, columnOdd);
-//        }
-//        
-//        template<DdType LibraryType, typename ValueType>
-//        storm::storage::SparseMatrix<ValueType> Add<LibraryType, ValueType>::toMatrix(std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, storm::dd::Odd<LibraryType> const& rowOdd, storm::dd::Odd<LibraryType> const& columnOdd) const {
-//            std::vector<uint_fast64_t> ddRowVariableIndices;
-//            std::vector<uint_fast64_t> ddColumnVariableIndices;
-//            
-//            for (auto const& variable : rowMetaVariables) {
-//                DdMetaVariable<LibraryType> const& metaVariable = this->getDdManager()->getMetaVariable(variable);
-//                for (auto const& ddVariable : metaVariable.getDdVariables()) {
-//                    ddRowVariableIndices.push_back(ddVariable.getIndex());
-//                }
-//            }
-//            std::sort(ddRowVariableIndices.begin(), ddRowVariableIndices.end());
-//            
-//            for (auto const& variable : columnMetaVariables) {
-//                DdMetaVariable<LibraryType> const& metaVariable = this->getDdManager()->getMetaVariable(variable);
-//                for (auto const& ddVariable : metaVariable.getDdVariables()) {
-//                    ddColumnVariableIndices.push_back(ddVariable.getIndex());
-//                }
-//            }
-//            std::sort(ddColumnVariableIndices.begin(), ddColumnVariableIndices.end());
-//            
-//            return internalAdd.toMatrix(rowOdd, ddRowVariableIndices, columnOdd, ddColumnVariableIndices);
-//        }
-//        
-//        template<DdType LibraryType, typename ValueType>
-//        storm::storage::SparseMatrix<ValueType> Add<LibraryType, ValueType>::toMatrix(std::set<storm::expressions::Variable> const& groupMetaVariables, storm::dd::Odd<LibraryType> const& rowOdd, storm::dd::Odd<LibraryType> const& columnOdd) const {
-//            std::set<storm::expressions::Variable> rowMetaVariables;
-//            std::set<storm::expressions::Variable> columnMetaVariables;
-//            
-//            for (auto const& variable : this->getContainedMetaVariables()) {
-//                // If the meta variable is a group meta variable, we do not insert it into the set of row/column meta variables.
-//                if (groupMetaVariables.find(variable) != groupMetaVariables.end()) {
-//                    continue;
-//                }
-//                
-//                if (variable.getName().size() > 0 && variable.getName().back() == '\'') {
-//                    columnMetaVariables.insert(variable);
-//                } else {
-//                    rowMetaVariables.insert(variable);
-//                }
-//            }
-//            
-//            // Create the canonical row group sizes and build the matrix.
-//            return toMatrix(rowMetaVariables, columnMetaVariables, groupMetaVariables, rowOdd, columnOdd);
-//        }
-//        
-//        template<DdType LibraryType, typename ValueType>
-//        storm::storage::SparseMatrix<ValueType> Add<LibraryType, ValueType>::toMatrix(std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::set<storm::expressions::Variable> const& groupMetaVariables, storm::dd::Odd<LibraryType> const& rowOdd, storm::dd::Odd<LibraryType> const& columnOdd) const {
-//            std::vector<uint_fast64_t> ddRowVariableIndices;
-//            std::vector<uint_fast64_t> ddColumnVariableIndices;
-//            std::vector<uint_fast64_t> ddGroupVariableIndices;
-//            std::set<storm::expressions::Variable> rowAndColumnMetaVariables;
-//            
-//            for (auto const& variable : rowMetaVariables) {
-//                DdMetaVariable<LibraryType> const& metaVariable = this->getDdManager()->getMetaVariable(variable);
-//                for (auto const& ddVariable : metaVariable.getDdVariables()) {
-//                    ddRowVariableIndices.push_back(ddVariable.getIndex());
-//                }
-//                rowAndColumnMetaVariables.insert(variable);
-//            }
-//            std::sort(ddRowVariableIndices.begin(), ddRowVariableIndices.end());
-//            for (auto const& variable : columnMetaVariables) {
-//                DdMetaVariable<LibraryType> const& metaVariable = this->getDdManager()->getMetaVariable(variable);
-//                for (auto const& ddVariable : metaVariable.getDdVariables()) {
-//                    ddColumnVariableIndices.push_back(ddVariable.getIndex());
-//                }
-//                rowAndColumnMetaVariables.insert(variable);
-//            }
-//            std::sort(ddColumnVariableIndices.begin(), ddColumnVariableIndices.end());
-//            for (auto const& variable : groupMetaVariables) {
-//                DdMetaVariable<LibraryType> const& metaVariable = this->getDdManager()->getMetaVariable(variable);
-//                for (auto const& ddVariable : metaVariable.getDdVariables()) {
-//                    ddGroupVariableIndices.push_back(ddVariable.getIndex());
-//                }
-//            }
-//            std::sort(ddGroupVariableIndices.begin(), ddGroupVariableIndices.end());
-//            
-//            return internalAdd.toMatrix(ddGroupVariableIndices, Bdd<LibraryType>::getCube(*this->getDdManager(), groupMetaVariables), rowOdd, ddRowVariableIndices, columnOdd, ddColumnVariableIndices, Bdd<LibraryType>::getCube(*this->getDdManager(), columnMetaVariables));
-//        }
-//        
-//        template<DdType LibraryType, typename ValueType>
-//        std::pair<storm::storage::SparseMatrix<ValueType>, std::vector<ValueType>> Add<LibraryType, ValueType>::toMatrixVector(storm::dd::Add<LibraryType, ValueType> const& vector, std::vector<uint_fast64_t>&& rowGroupSizes, std::set<storm::expressions::Variable> const& groupMetaVariables, storm::dd::Odd<LibraryType> const& rowOdd, storm::dd::Odd<LibraryType> const& columnOdd) const {
-//            std::set<storm::expressions::Variable> rowMetaVariables;
-//            std::set<storm::expressions::Variable> columnMetaVariables;
-//            
-//            for (auto const& variable : this->getContainedMetaVariables()) {
-//                // If the meta variable is a group meta variable, we do not insert it into the set of row/column meta variables.
-//                if (groupMetaVariables.find(variable) != groupMetaVariables.end()) {
-//                    continue;
-//                }
-//                
-//                if (variable.getName().size() > 0 && variable.getName().back() == '\'') {
-//                    columnMetaVariables.insert(variable);
-//                } else {
-//                    rowMetaVariables.insert(variable);
-//                }
-//            }
-//            
-//            // Create the canonical row group sizes and build the matrix.
-//            return toMatrixVector(vector, std::move(rowGroupSizes), rowMetaVariables, columnMetaVariables, groupMetaVariables, rowOdd, columnOdd);
-//        }
-//
-//        template<DdType LibraryType, typename ValueType>
-//        std::pair<storm::storage::SparseMatrix<ValueType>, std::vector<ValueType>> Add<LibraryType, ValueType>::toMatrixVector(storm::dd::Add<LibraryType, ValueType> const& vector, std::vector<uint_fast64_t>&& rowGroupIndices, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::set<storm::expressions::Variable> const& groupMetaVariables, storm::dd::Odd<LibraryType> const& rowOdd, storm::dd::Odd<LibraryType> const& columnOdd) const {
-//            std::vector<uint_fast64_t> ddRowVariableIndices;
-//            std::vector<uint_fast64_t> ddColumnVariableIndices;
-//            std::vector<uint_fast64_t> ddGroupVariableIndices;
-//            std::set<storm::expressions::Variable> rowAndColumnMetaVariables;
-//            
-//            for (auto const& variable : rowMetaVariables) {
-//                DdMetaVariable<LibraryType> const& metaVariable = this->getDdManager()->getMetaVariable(variable);
-//                for (auto const& ddVariable : metaVariable.getDdVariables()) {
-//                    ddRowVariableIndices.push_back(ddVariable.getIndex());
-//                }
-//                rowAndColumnMetaVariables.insert(variable);
-//            }
-//            std::sort(ddRowVariableIndices.begin(), ddRowVariableIndices.end());
-//            for (auto const& variable : columnMetaVariables) {
-//                DdMetaVariable<LibraryType> const& metaVariable = this->getDdManager()->getMetaVariable(variable);
-//                for (auto const& ddVariable : metaVariable.getDdVariables()) {
-//                    ddColumnVariableIndices.push_back(ddVariable.getIndex());
-//                }
-//                rowAndColumnMetaVariables.insert(variable);
-//            }
-//            std::sort(ddColumnVariableIndices.begin(), ddColumnVariableIndices.end());
-//            for (auto const& variable : groupMetaVariables) {
-//                DdMetaVariable<LibraryType> const& metaVariable = this->getDdManager()->getMetaVariable(variable);
-//                for (auto const& ddVariable : metaVariable.getDdVariables()) {
-//                    ddGroupVariableIndices.push_back(ddVariable.getIndex());
-//                }
-//            }
-//            std::sort(ddGroupVariableIndices.begin(), ddGroupVariableIndices.end());
-//            
-//            return internalAdd.toMatrixVector(vector.internalAdd, ddGroupVariableIndices, std::move(rowGroupIndices), rowOdd, ddRowVariableIndices, columnOdd, ddColumnVariableIndices, Bdd<LibraryType>::getCube(*this->getDdManager(), columnMetaVariables));
-//        }
-//
-//        template<DdType LibraryType, typename ValueType>
-//        void Add<LibraryType, ValueType>::exportToDot(std::string const& filename) const {
-//            internalAdd.exportToDot(filename, this->getDdManager()->getDdVariableNames());
-//        }
-//        
-//        template<DdType LibraryType, typename ValueType>
-//        AddIterator<LibraryType, ValueType> Add<LibraryType, ValueType>::begin(bool enumerateDontCareMetaVariables) const {
-//            return internalAdd.begin(this->getDdManager(), this->getContainedMetaVariables(), enumerateDontCareMetaVariables);
-//        }
-//        
-//        template<DdType LibraryType, typename ValueType>
-//        AddIterator<LibraryType, ValueType> Add<LibraryType, ValueType>::end(bool enumerateDontCareMetaVariables) const {
-//            return internalAdd.end(this->getDdManager(), enumerateDontCareMetaVariables);
-//        }
-//        
-//        template<DdType LibraryType, typename ValueType>
-//        std::ostream& operator<<(std::ostream& out, Add<LibraryType, ValueType> const& add) {
-//            out << "ADD with " << add.getNonZeroCount() << " nnz, " << add.getNodeCount() << " nodes, " << add.getLeafCount() << " leaves" << std::endl;
-//            std::vector<std::string> variableNames;
-//            for (auto const& variable : add.getContainedMetaVariables()) {
-//                variableNames.push_back(variable.getName());
-//            }
-//            out << "contained variables: " << boost::algorithm::join(variableNames, ", ") << std::endl;
-//            return out;
-//        }
-        
-        template<DdType LibraryType, typename ValueType>
-        void Add<LibraryType, ValueType>::addToVector(Odd<LibraryType> const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<ValueType>& targetVector) const {
-            std::function<ValueType (ValueType const&, ValueType const&)> fct = [] (ValueType const& a, ValueType const& b) -> ValueType { return a + b; };
-            return internalAdd.composeVectors(odd, ddVariableIndices, targetVector, fct);
+        template<DdType LibraryType, typename ValueType>
+        void Add<LibraryType, ValueType>::exportToDot(std::string const& filename) const {
+            internalAdd.exportToDot(filename, this->getDdManager()->getDdVariableNames());
+        }
+        
+        template<DdType LibraryType, typename ValueType>
+        AddIterator<LibraryType, ValueType> Add<LibraryType, ValueType>::begin(bool enumerateDontCareMetaVariables) const {
+            return internalAdd.begin(this->getDdManager(), this->getContainedMetaVariables(), enumerateDontCareMetaVariables);
+        }
+        
+        template<DdType LibraryType, typename ValueType>
+        AddIterator<LibraryType, ValueType> Add<LibraryType, ValueType>::end(bool enumerateDontCareMetaVariables) const {
+            return internalAdd.end(this->getDdManager(), enumerateDontCareMetaVariables);
+        }
+        
+        template<DdType LibraryType, typename ValueType>
+        std::ostream& operator<<(std::ostream& out, Add<LibraryType, ValueType> const& add) {
+            out << "ADD with " << add.getNonZeroCount() << " nnz, " << add.getNodeCount() << " nodes, " << add.getLeafCount() << " leaves" << std::endl;
+            std::vector<std::string> variableNames;
+            for (auto const& variable : add.getContainedMetaVariables()) {
+                variableNames.push_back(variable.getName());
+            }
+            out << "contained variables: " << boost::algorithm::join(variableNames, ", ") << std::endl;
+            return out;
         }
 
         template<DdType LibraryType, typename ValueType>

src/storage/dd/Add.h

@@ -27,6 +27,9 @@ namespace storm {
             friend class Bdd<LibraryType>;
             friend class Odd<LibraryType>;
             
+            template<DdType LibraryTypePrime, typename ValueTypePrime>
+            friend class Add;
+            
             // Instantiate all copy/move constructors/assignments with the default implementation.
             Add() = default;
             Add(Add<LibraryType, ValueType> const& other) = default;
@@ -673,7 +676,7 @@ namespace storm {
              * @param ddVariableIndices The (sorted) indices of all DD variables that need to be considered.
              * @param targetVector The vector to which the translated DD-based vector is to be added.
              */
-            void addToVector(Odd<LibraryType> const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<ValueType>& targetVector) const;
+            void addToExplicitVector(Odd<LibraryType> const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<ValueType>& targetVector) const;
             
             /*!
              * Builds an ADD representing the given vector.

src/storage/dd/cudd/InternalCuddAdd.cpp

@@ -343,12 +343,17 @@ namespace storm {
         }
 
         template<typename ValueType>
-        void InternalAdd<DdType::CUDD, ValueType>::composeVectors(storm::dd::Odd<DdType::CUDD> const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<ValueType>& targetVector, std::function<ValueType (ValueType const&, ValueType const&)> const& function) const {
-            composeVectorsRec(this->getCuddDdNode(), 0, ddVariableIndices.size(), 0, odd, ddVariableIndices, targetVector, function);
+        void InternalAdd<DdType::CUDD, ValueType>::composeWithExplicitVector(storm::dd::Odd<DdType::CUDD> const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<ValueType>& targetVector, std::function<ValueType (ValueType const&, ValueType const&)> const& function) const {
+            composeWithExplicitVectorRec(this->getCuddDdNode(), nullptr, 0, ddVariableIndices.size(), 0, odd, ddVariableIndices, targetVector, function);
+        }
+        
+        template<typename ValueType>
+        void InternalAdd<DdType::CUDD, ValueType>::composeWithExplicitVector(storm::dd::Odd<DdType::CUDD> const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<uint_fast64_t> const& offsets, std::vector<ValueType>& targetVector, std::function<ValueType (ValueType const&, ValueType const&)> const& function) const {
+            composeWithExplicitVectorRec(this->getCuddDdNode(), &offsets, 0, ddVariableIndices.size(), 0, odd, ddVariableIndices, targetVector, function);
         }
 
         template<typename ValueType>
-        void InternalAdd<DdType::CUDD, ValueType>::composeVectorsRec(DdNode const* dd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd<DdType::CUDD> const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<ValueType>& targetVector, std::function<ValueType (ValueType const&, ValueType const&)> const& function) const {
+        void InternalAdd<DdType::CUDD, ValueType>::composeWithExplicitVectorRec(DdNode const* dd, std::vector<uint_fast64_t> const* offsets, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd<DdType::CUDD> const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<ValueType>& targetVector, std::function<ValueType (ValueType const&, ValueType const&)> const& function) const {
             // For the empty DD, we do not need to add any entries.
             if (dd == Cudd_ReadZero(ddManager->getCuddManager().getManager())) {
                 return;
@@ -356,59 +361,137 @@ namespace storm {
             
             // If we are at the maximal level, the value to be set is stored as a constant in the DD.
             if (currentLevel == maxLevel) {
-                targetVector[currentOffset] = function(targetVector[currentOffset], Cudd_V(dd));
+                ValueType& targetValue = targetVector[offsets != nullptr ? (*offsets)[currentOffset] : currentOffset];
+                targetValue = function(targetValue, Cudd_V(dd));
             } else if (ddVariableIndices[currentLevel] < dd->index) {
                 // If we skipped a level, we need to enumerate the explicit entries for the case in which the bit is set
                 // and for the one in which it is not set.
-                composeVectorsRec(dd, currentLevel + 1, maxLevel, currentOffset, odd.getElseSuccessor(), ddVariableIndices, targetVector, function);
-                composeVectorsRec(dd, currentLevel + 1, maxLevel, currentOffset + odd.getElseOffset(), odd.getThenSuccessor(), ddVariableIndices, targetVector, function);
+                composeWithExplicitVectorRec(dd, offsets, currentLevel + 1, maxLevel, currentOffset, odd.getElseSuccessor(), ddVariableIndices, targetVector, function);
+                composeWithExplicitVectorRec(dd, offsets, currentLevel + 1, maxLevel, currentOffset + odd.getElseOffset(), odd.getThenSuccessor(), ddVariableIndices, targetVector, function);
             } else {
                 // Otherwise, we simply recursively call the function for both (different) cases.
-                composeVectorsRec(Cudd_E(dd), currentLevel + 1, maxLevel, currentOffset, odd.getElseSuccessor(), ddVariableIndices, targetVector, function);
-                composeVectorsRec(Cudd_T(dd), currentLevel + 1, maxLevel, currentOffset + odd.getElseOffset(), odd.getThenSuccessor(), ddVariableIndices, targetVector, function);
+                composeWithExplicitVectorRec(Cudd_E(dd), offsets, currentLevel + 1, maxLevel, currentOffset, odd.getElseSuccessor(), ddVariableIndices, targetVector, function);
+                composeWithExplicitVectorRec(Cudd_T(dd), offsets, currentLevel + 1, maxLevel, currentOffset + odd.getElseOffset(), odd.getThenSuccessor(), ddVariableIndices, targetVector, function);
             }
         }
+        
+        template<typename ValueType>
+        std::vector<InternalAdd<DdType::CUDD, ValueType>> InternalAdd<DdType::CUDD, ValueType>::splitIntoGroups(std::vector<uint_fast64_t> const& ddGroupVariableIndices) const {
+            std::vector<InternalAdd<DdType::CUDD, ValueType>> result;
+            splitIntoGroupsRec(this->getCuddDdNode(), result, ddGroupVariableIndices, 0, ddGroupVariableIndices.size());
+            return result;
+        }
+        
+        template<typename ValueType>
+        void InternalAdd<DdType::CUDD, ValueType>::splitIntoGroupsRec(DdNode* dd, std::vector<InternalAdd<DdType::CUDD, ValueType>>& groups, std::vector<uint_fast64_t> const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel) const {
+            // For the empty DD, we do not need to create a group.
+            if (dd == Cudd_ReadZero(ddManager->getCuddManager().getManager())) {
+                return;
+            }
+            
+            if (currentLevel == maxLevel) {
+                groups.push_back(InternalAdd<DdType::CUDD, ValueType>(ddManager, ADD(ddManager->getCuddManager(), dd)));
+            } else if (ddGroupVariableIndices[currentLevel] < dd->index) {
+                splitIntoGroupsRec(dd, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel);
+                splitIntoGroupsRec(dd, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel);
+            } else {
+                splitIntoGroupsRec(Cudd_E(dd), groups, ddGroupVariableIndices, currentLevel + 1, maxLevel);
+                splitIntoGroupsRec(Cudd_T(dd), groups, ddGroupVariableIndices, currentLevel + 1, maxLevel);
+            }
+        }
+        
+        template<typename ValueType>
+        std::vector<std::pair<InternalAdd<DdType::CUDD, ValueType>, InternalAdd<DdType::CUDD, ValueType>>> InternalAdd<DdType::CUDD, ValueType>::splitIntoGroups(InternalAdd<DdType::CUDD, ValueType> vector, std::vector<uint_fast64_t> const& ddGroupVariableIndices) const {
+            std::vector<std::pair<InternalAdd<DdType::CUDD, ValueType>, InternalAdd<DdType::CUDD, ValueType>>> result;
+            splitGroupsRec(this->getCuddDdNode(), vector.getCuddDdNode(), result, ddGroupVariableIndices, 0, ddGroupVariableIndices.size());
+            return result;
+        }
+        
+        template<typename ValueType>
+        void InternalAdd<DdType::CUDD, ValueType>::splitIntoGroupsRec(DdNode* dd1, DdNode* dd2, std::vector<std::pair<InternalAdd<DdType::CUDD, ValueType>, InternalAdd<DdType::CUDD, ValueType>>>& groups, std::vector<uint_fast64_t> const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel) const {
+            // For the empty DD, we do not need to create a group.
+            if (dd1 == Cudd_ReadZero(ddManager->getCuddManager().getManager()) && dd2 == Cudd_ReadZero(ddManager->getCuddManager().getManager())) {
+                return;
+            }
+            
+            if (currentLevel == maxLevel) {
+                groups.push_back(std::make_pair(InternalAdd<DdType::CUDD, ValueType>(ddManager, ADD(ddManager->getCuddManager(), dd1)), InternalAdd<DdType::CUDD, ValueType>(ddManager, ADD(ddManager->getCuddManager(), dd2))));
+            } else if (ddGroupVariableIndices[currentLevel] < dd1->index) {
+                if (ddGroupVariableIndices[currentLevel] < dd2->index) {
+                    splitGroupsRec(dd1, dd2, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel);
+                    splitGroupsRec(dd1, dd2, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel);
+                } else {
+                    splitGroupsRec(dd1, Cudd_T(dd2), groups, ddGroupVariableIndices, currentLevel + 1, maxLevel);
+                    splitGroupsRec(dd1, Cudd_E(dd2), groups, ddGroupVariableIndices, currentLevel + 1, maxLevel);
+                }
+            } else if (ddGroupVariableIndices[currentLevel] < dd2->index) {
+                splitGroupsRec(Cudd_T(dd1), dd2, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel);
+                splitGroupsRec(Cudd_E(dd1), dd2, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel);
+            } else {
+                splitGroupsRec(Cudd_T(dd1), Cudd_T(dd2), groups, ddGroupVariableIndices, currentLevel + 1, maxLevel);
+                splitGroupsRec(Cudd_E(dd1), Cudd_E(dd2), groups, ddGroupVariableIndices, currentLevel + 1, maxLevel);
+            }
+        }
+        
+        template<typename ValueType>
+        void InternalAdd<DdType::CUDD, ValueType>::toMatrixComponents(std::vector<uint_fast64_t> const& rowGroupIndices, std::vector<uint_fast64_t>& rowIndications, std::vector<storm::storage::MatrixEntry<uint_fast64_t, ValueType>>& columnsAndValues, Odd<DdType::CUDD> const& rowOdd, Odd<DdType::CUDD> const& columnOdd, std::vector<uint_fast64_t> const& ddRowVariableIndices, std::vector<uint_fast64_t> const& ddColumnVariableIndices, bool writeValues) const {
+            return toMatrixComponentsRec(this->getCuddDdNode(), rowGroupIndices, rowIndications, columnsAndValues, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices, writeValues);
+        }
 
+        template<typename ValueType>
+        void InternalAdd<DdType::CUDD, ValueType>::toMatrixComponentsRec(DdNode const* dd, std::vector<uint_fast64_t> const& rowGroupOffsets, std::vector<uint_fast64_t>& rowIndications, std::vector<storm::storage::MatrixEntry<uint_fast64_t, double>>& columnsAndValues, Odd<DdType::CUDD> const& rowOdd, Odd<DdType::CUDD> const& columnOdd, uint_fast64_t currentRowLevel, uint_fast64_t currentColumnLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, uint_fast64_t currentColumnOffset, std::vector<uint_fast64_t> const& ddRowVariableIndices, std::vector<uint_fast64_t> const& ddColumnVariableIndices, bool generateValues) const {
+            // For the empty DD, we do not need to add any entries.
+            if (dd == Cudd_ReadZero(ddManager->getCuddManager().getManager())) {
+                return;
+            }
+            
+            // If we are at the maximal level, the value to be set is stored as a constant in the DD.
+            if (currentRowLevel + currentColumnLevel == maxLevel) {
+                if (generateValues) {
+                    columnsAndValues[rowIndications[rowGroupOffsets[currentRowOffset]]] = storm::storage::MatrixEntry<uint_fast64_t, double>(currentColumnOffset, Cudd_V(dd));
+                }
+                ++rowIndications[rowGroupOffsets[currentRowOffset]];
+            } else {
+                DdNode const* elseElse;
+                DdNode const* elseThen;
+                DdNode const* thenElse;
+                DdNode const* thenThen;
+                
+                if (ddColumnVariableIndices[currentColumnLevel] < dd->index) {
+                    elseElse = elseThen = thenElse = thenThen = dd;
+                } else if (ddRowVariableIndices[currentColumnLevel] < dd->index) {
+                    elseElse = thenElse = Cudd_E(dd);
+                    elseThen = thenThen = Cudd_T(dd);
+                } else {
+                    DdNode const* elseNode = Cudd_E(dd);
+                    if (ddColumnVariableIndices[currentColumnLevel] < elseNode->index) {
+                        elseElse = elseThen = elseNode;
+                    } else {
+                        elseElse = Cudd_E(elseNode);
+                        elseThen = Cudd_T(elseNode);
+                    }
+                    
+                    DdNode const* thenNode = Cudd_T(dd);
+                    if (ddColumnVariableIndices[currentColumnLevel] < thenNode->index) {
+                        thenElse = thenThen = thenNode;
+                    } else {
+                        thenElse = Cudd_E(thenNode);
+                        thenThen = Cudd_T(thenNode);
+                    }
+                }
+                
+                // Visit else-else.
+                toMatrixComponentsRec(elseElse, rowGroupOffsets, rowIndications, columnsAndValues, rowOdd.getElseSuccessor(), columnOdd.getElseSuccessor(), currentRowLevel + 1, currentColumnLevel + 1, maxLevel, currentRowOffset, currentColumnOffset, ddRowVariableIndices, ddColumnVariableIndices, generateValues);
+                // Visit else-then.
+                toMatrixComponentsRec(elseThen, rowGroupOffsets, rowIndications, columnsAndValues, rowOdd.getElseSuccessor(), columnOdd.getThenSuccessor(), currentRowLevel + 1, currentColumnLevel + 1, maxLevel, currentRowOffset, currentColumnOffset + columnOdd.getElseOffset(), ddRowVariableIndices, ddColumnVariableIndices, generateValues);
+                // Visit then-else.
+                toMatrixComponentsRec(thenElse, rowGroupOffsets, rowIndications, columnsAndValues, rowOdd.getThenSuccessor(), columnOdd.getElseSuccessor(), currentRowLevel + 1, currentColumnLevel + 1, maxLevel, currentRowOffset + rowOdd.getElseOffset(), currentColumnOffset, ddRowVariableIndices, ddColumnVariableIndices, generateValues);
+                // Visit then-then.
+                toMatrixComponentsRec(thenThen, rowGroupOffsets, rowIndications, columnsAndValues, rowOdd.getThenSuccessor(), columnOdd.getThenSuccessor(), currentRowLevel + 1, currentColumnLevel + 1, maxLevel, currentRowOffset + rowOdd.getElseOffset(), currentColumnOffset + columnOdd.getElseOffset(), ddRowVariableIndices, ddColumnVariableIndices, generateValues);
+            }
+        }
         
-//        template<typename ValueType>
-//        std::vector<ValueType> InternalAdd<DdType::CUDD, ValueType>::toVector(std::vector<uint_fast64_t> const& ddGroupVariableIndices, storm::dd::Odd<DdType::CUDD> const& rowOdd, std::vector<uint_fast64_t> const& ddRowVariableIndices, std::vector<uint_fast64_t> const& groupOffsets) const {
-//            // Start by splitting the symbolic vector into groups.
-//            std::vector<InternalAdd<DdType::CUDD, ValueType>> groups;
-//            splitGroupsRec(this->getCuddDdNode(), groups, ddGroupVariableIndices, 0, ddGroupVariableIndices.size());
-//            
-//            // Now iterate over the groups and add them to the resulting vector.
-//            std::vector<ValueType> result(groupOffsets.back(), storm::utility::zero<ValueType>());
-//            for (uint_fast64_t i = 0; i < groups.size(); ++i) {
-//                toVectorRec(groups[i].getCuddDdNode(), result, groupOffsets, rowOdd, 0, ddRowVariableIndices.size(), 0, ddRowVariableIndices);
-//            }
-//            
-//            return result;
-//        }
-//
-//        template<typename ValueType>
-//        void InternalAdd<DdType::CUDD, ValueType>::addToExplicitVector(storm::dd::Odd<DdType::CUDD> const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<ValueType>& targetVector) const {
-//            composeVector(odd, ddVariableIndices, targetVector, std::plus<ValueType>());
-//        }
-//
-//        template<typename ValueType>
-//        void InternalAdd<DdType::CUDD, ValueType>::toVectorRec(DdNode const* dd, std::vector<ValueType>& result, std::vector<uint_fast64_t> const& rowGroupOffsets, Odd<DdType::CUDD> const& rowOdd, uint_fast64_t currentRowLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, std::vector<uint_fast64_t> const& ddRowVariableIndices) const {
-//            // For the empty DD, we do not need to add any entries.
-//            if (dd == Cudd_ReadZero(ddManager->getCuddManager().getManager())) {
-//                return;
-//            }
-//            
-//            // If we are at the maximal level, the value to be set is stored as a constant in the DD.
-//            if (currentRowLevel == maxLevel) {
-//                result[rowGroupOffsets[currentRowOffset]] = Cudd_V(dd);
-//            } else if (ddRowVariableIndices[currentRowLevel] < dd->index) {
-//                toVectorRec(dd, result, rowGroupOffsets, rowOdd.getElseSuccessor(), currentRowLevel + 1, maxLevel, currentRowOffset, ddRowVariableIndices);
-//                toVectorRec(dd, result, rowGroupOffsets, rowOdd.getThenSuccessor(), currentRowLevel + 1, maxLevel, currentRowOffset + rowOdd.getElseOffset(), ddRowVariableIndices);
-//            } else {
-//                toVectorRec(Cudd_E(dd), result, rowGroupOffsets, rowOdd.getElseSuccessor(), currentRowLevel + 1, maxLevel, currentRowOffset, ddRowVariableIndices);
-//                toVectorRec(Cudd_T(dd), result, rowGroupOffsets, rowOdd.getThenSuccessor(), currentRowLevel + 1, maxLevel, currentRowOffset + rowOdd.getElseOffset(), ddRowVariableIndices);
-//            }
-//        }
-//        
+
 //        template<typename ValueType>
 //        storm::storage::SparseMatrix<ValueType> InternalAdd<DdType::CUDD, ValueType>::toMatrix(uint_fast64_t numberOfDdVariables, storm::dd::Odd<DdType::CUDD> const& rowOdd, std::vector<uint_fast64_t> const& ddRowVariableIndices, storm::dd::Odd<DdType::CUDD> const& columnOdd, std::vector<uint_fast64_t> const& ddColumnVariableIndices) const {
 //            // Prepare the vectors that represent the matrix.
@@ -454,59 +537,6 @@ namespace storm {
 //        }
 //        
 //        template<typename ValueType>
-//        void InternalAdd<DdType::CUDD, ValueType>::toMatrixRec(DdNode const* dd, std::vector<uint_fast64_t>& rowIndications, std::vector<storm::storage::MatrixEntry<uint_fast64_t, double>>& columnsAndValues, std::vector<uint_fast64_t> const& rowGroupOffsets, Odd<DdType::CUDD> const& rowOdd, Odd<DdType::CUDD> const& columnOdd, uint_fast64_t currentRowLevel, uint_fast64_t currentColumnLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, uint_fast64_t currentColumnOffset, std::vector<uint_fast64_t> const& ddRowVariableIndices, std::vector<uint_fast64_t> const& ddColumnVariableIndices, bool generateValues) const {
-//            // For the empty DD, we do not need to add any entries.
-//            if (dd == Cudd_ReadZero(ddManager->getCuddManager().getManager())) {
-//                return;
-//            }
-//            
-//            // If we are at the maximal level, the value to be set is stored as a constant in the DD.
-//            if (currentRowLevel + currentColumnLevel == maxLevel) {
-//                if (generateValues) {
-//                    columnsAndValues[rowIndications[rowGroupOffsets[currentRowOffset]]] = storm::storage::MatrixEntry<uint_fast64_t, double>(currentColumnOffset, Cudd_V(dd));
-//                }
-//                ++rowIndications[rowGroupOffsets[currentRowOffset]];
-//            } else {
-//                DdNode const* elseElse;
-//                DdNode const* elseThen;
-//                DdNode const* thenElse;
-//                DdNode const* thenThen;
-//                
-//                if (ddColumnVariableIndices[currentColumnLevel] < dd->index) {
-//                    elseElse = elseThen = thenElse = thenThen = dd;
-//                } else if (ddRowVariableIndices[currentColumnLevel] < dd->index) {
-//                    elseElse = thenElse = Cudd_E(dd);
-//                    elseThen = thenThen = Cudd_T(dd);
-//                } else {
-//                    DdNode const* elseNode = Cudd_E(dd);
-//                    if (ddColumnVariableIndices[currentColumnLevel] < elseNode->index) {
-//                        elseElse = elseThen = elseNode;
-//                    } else {
-//                        elseElse = Cudd_E(elseNode);
-//                        elseThen = Cudd_T(elseNode);
-//                    }
-//                    
-//                    DdNode const* thenNode = Cudd_T(dd);
-//                    if (ddColumnVariableIndices[currentColumnLevel] < thenNode->index) {
-//                        thenElse = thenThen = thenNode;
-//                    } else {
-//                        thenElse = Cudd_E(thenNode);
-//                        thenThen = Cudd_T(thenNode);
-//                    }
-//                }
-//                
-//                // Visit else-else.
-//                toMatrixRec(elseElse, rowIndications, columnsAndValues, rowGroupOffsets, rowOdd.getElseSuccessor(), columnOdd.getElseSuccessor(), currentRowLevel + 1, currentColumnLevel + 1, maxLevel, currentRowOffset, currentColumnOffset, ddRowVariableIndices, ddColumnVariableIndices, generateValues);
-//                // Visit else-then.
-//                toMatrixRec(elseThen, rowIndications, columnsAndValues, rowGroupOffsets, rowOdd.getElseSuccessor(), columnOdd.getThenSuccessor(), currentRowLevel + 1, currentColumnLevel + 1, maxLevel, currentRowOffset, currentColumnOffset + columnOdd.getElseOffset(), ddRowVariableIndices, ddColumnVariableIndices, generateValues);
-//                // Visit then-else.
-//                toMatrixRec(thenElse, rowIndications, columnsAndValues, rowGroupOffsets, rowOdd.getThenSuccessor(), columnOdd.getElseSuccessor(), currentRowLevel + 1, currentColumnLevel + 1, maxLevel, currentRowOffset + rowOdd.getElseOffset(), currentColumnOffset, ddRowVariableIndices, ddColumnVariableIndices, generateValues);
-//                // Visit then-then.
-//                toMatrixRec(thenThen, rowIndications, columnsAndValues, rowGroupOffsets, rowOdd.getThenSuccessor(), columnOdd.getThenSuccessor(), currentRowLevel + 1, currentColumnLevel + 1, maxLevel, currentRowOffset + rowOdd.getElseOffset(), currentColumnOffset + columnOdd.getElseOffset(), ddRowVariableIndices, ddColumnVariableIndices, generateValues);
-//            }
-//        }
-//        
-//        template<typename ValueType>
 //        storm::storage::SparseMatrix<ValueType> InternalAdd<DdType::CUDD, ValueType>::toMatrix(std::vector<uint_fast64_t> const& ddGroupVariableIndices, InternalBdd<DdType::CUDD> const& groupVariableCube, storm::dd::Odd<DdType::CUDD> const& rowOdd, std::vector<uint_fast64_t> const& ddRowVariableIndices, storm::dd::Odd<DdType::CUDD> const& columnOdd, std::vector<uint_fast64_t> const& ddColumnVariableIndices, InternalBdd<DdType::CUDD> const& columnVariableCube) const {
 //            // Start by computing the offsets (in terms of rows) for each row group.
 //            InternalAdd<DdType::CUDD, uint_fast64_t> stateToNumberOfChoices = this->notZero().existsAbstract(columnVariableCube).template toAdd<uint_fast64_t>().sumAbstract(groupVariableCube);
@@ -654,24 +684,6 @@ namespace storm {
 //        }
 //        
 //        template<typename ValueType>
-//        void InternalAdd<DdType::CUDD, ValueType>::splitGroupsRec(DdNode* dd, std::vector<InternalAdd<DdType::CUDD, ValueType>>& groups, std::vector<uint_fast64_t> const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel) const {
-//            // For the empty DD, we do not need to create a group.
-//            if (dd == Cudd_ReadZero(this->getDdManager()->getCuddManager().getManager())) {
-//                return;
-//            }
-//            
-//            if (currentLevel == maxLevel) {
-//                groups.push_back(InternalAdd<DdType::CUDD, ValueType>(ddManager, ADD(ddManager->getCuddManager(), dd)));
-//            } else if (ddGroupVariableIndices[currentLevel] < dd->index) {
-//                splitGroupsRec(dd, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel);
-//                splitGroupsRec(dd, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel);
-//            } else {
-//                splitGroupsRec(Cudd_E(dd), groups, ddGroupVariableIndices, currentLevel + 1, maxLevel);
-//                splitGroupsRec(Cudd_T(dd), groups, ddGroupVariableIndices, currentLevel + 1, maxLevel);
-//            }
-//        }
-//        
-//        template<typename ValueType>
 //        void InternalAdd<DdType::CUDD, ValueType>::splitGroupsRec(DdNode* dd1, DdNode* dd2, std::vector<std::pair<InternalAdd<DdType::CUDD, ValueType>, InternalAdd<DdType::CUDD, ValueType>>>& groups, std::vector<uint_fast64_t> const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel) const {
 //            // For the empty DD, we do not need to create a group.
 //            if (dd1 == Cudd_ReadZero(ddManager->getCuddManager().getManager()) && dd2 == Cudd_ReadZero(ddManager->getCuddManager().getManager())) {

src/storage/dd/cudd/InternalCuddAdd.h

@@ -500,25 +500,15 @@ namespace storm {
              */
              AddIterator<DdType::CUDD, ValueType> end(std::shared_ptr<DdManager<DdType::CUDD> const> fullDdManager, bool enumerateDontCareMetaVariables = true) const;
             
-            void composeVectors(storm::dd::Odd<DdType::CUDD> const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<ValueType>& targetVector, std::function<ValueType (ValueType const&, ValueType const&)> const& function) const;
-            
-//            /*!
-//             * Converts the ADD to a vector. The given offset-labeled DD is used to determine the correct row of
-//             * each entry.
-//             *
-//             * @param rowOdd The ODD used for determining the correct row.
-//             * @return The vector that is represented by this ADD.
-//             */
-//            std::vector<ValueType> toVector(std::vector<uint_fast64_t> const& ddGroupVariableIndices, storm::dd::Odd<DdType::CUDD> const& rowOdd, std::vector<uint_fast64_t> const& ddRowVariableIndices, std::vector<uint_fast64_t> const& groupOffsets) const;
-//            
-//            void addToExplicitVector(storm::dd::Odd<DdType::CUDD> const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<ValueType>& targetVector) const;
-//            
-//
-//            storm::storage::SparseMatrix<ValueType> toMatrix(uint_fast64_t numberOfDdVariables, storm::dd::Odd<DdType::CUDD> const& rowOdd, std::vector<uint_fast64_t> const& ddRowVariableIndices, storm::dd::Odd<DdType::CUDD> const& columnOdd, std::vector<uint_fast64_t> const& ddColumnVariableIndices) const;
-//            
-//            storm::storage::SparseMatrix<ValueType> toMatrix(std::vector<uint_fast64_t> const& ddGroupVariableIndices, InternalBdd<DdType::CUDD> const& groupVariableCube, storm::dd::Odd<DdType::CUDD> const& rowOdd, std::vector<uint_fast64_t> const& ddRowVariableIndices, storm::dd::Odd<DdType::CUDD> const& columnOdd, std::vector<uint_fast64_t> const& ddColumnVariableIndices, InternalBdd<DdType::CUDD> const& columnVariableCube) const;
-//            
-//            std::pair<storm::storage::SparseMatrix<ValueType>, std::vector<ValueType>> toMatrixVector(InternalAdd<DdType::CUDD, ValueType> const& vector, std::vector<uint_fast64_t> const& ddGroupVariableIndices, std::vector<uint_fast64_t>&& rowGroupIndices, storm::dd::Odd<DdType::CUDD> const& rowOdd, std::vector<uint_fast64_t> const& ddRowVariableIndices, storm::dd::Odd<DdType::CUDD> const& columnOdd, std::vector<uint_fast64_t> const& ddColumnVariableIndices, InternalBdd<DdType::CUDD> const& columnVariableCube) const;
+            void composeWithExplicitVector(Odd<DdType::CUDD> const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<ValueType>& targetVector, std::function<ValueType (ValueType const&, ValueType const&)> const& function) const;
+            
+            void composeWithExplicitVector(Odd<DdType::CUDD> const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<uint_fast64_t> const& offsets, std::vector<ValueType>& targetVector, std::function<ValueType (ValueType const&, ValueType const&)> const& function) const;
+            
+            std::vector<InternalAdd<DdType::CUDD, ValueType>> splitIntoGroups(std::vector<uint_fast64_t> const& ddGroupVariableIndices) const;
+            
+            void toMatrixComponents(std::vector<uint_fast64_t> const& rowGroupIndices, std::vector<uint_fast64_t>& rowIndications, std::vector<storm::storage::MatrixEntry<uint_fast64_t, ValueType>>& columnsAndValues, Odd<DdType::CUDD> const& rowOdd, Odd<DdType::CUDD> const& columnOdd, std::vector<uint_fast64_t> const& ddRowVariableIndices, std::vector<uint_fast64_t> const& ddColumnVariableIndices, bool writeValues) const;
+            
+            std::vector<std::pair<InternalAdd<DdType::CUDD, ValueType>, InternalAdd<DdType::CUDD, ValueType>>> splitIntoGroups(InternalAdd<DdType::CUDD, ValueType> vector, std::vector<uint_fast64_t> const& ddGroupVariableIndices) const;
             
             static InternalAdd<DdType::CUDD, ValueType> fromVector(InternalDdManager<DdType::CUDD> const* ddManager, std::vector<ValueType> const& values, storm::dd::Odd<DdType::CUDD> const& odd, std::vector<uint_fast64_t> const& ddVariableIndices);
             
@@ -549,21 +539,21 @@ namespace storm {
              * @param ddVariableIndices The (sorted) indices of all DD variables that need to be considered.
              * @param targetVector The vector to which the translated DD-based vector is to be added.
              */
-            void composeVectorsRec(DdNode const* dd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd<DdType::CUDD> const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<ValueType>& targetVector, std::function<ValueType (ValueType const&, ValueType const&)> const& function) const;
+            void composeWithExplicitVectorRec(DdNode const* dd, std::vector<uint_fast64_t> const* offsets, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd<DdType::CUDD> const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<ValueType>& targetVector, std::function<ValueType (ValueType const&, ValueType const&)> const& function) const;
             
             /*!
-             * Helper function to convert the DD into an (explicit) vector.
+             * Splits the given matrix DD into the groups using the given group variables.
              *
-             * @param dd The DD to convert.
-             * @param result The vector that will hold the values upon successful completion.
-             * @param rowGroupOffsets The row offsets at which a given row group starts.
-             * @param rowOdd The ODD used for the row translation.
-             * @param currentRowLevel The currently considered row level in the DD.
+             * @param dd The DD to split.
+             * @param groups A vector that is to be filled with the DDs for the individual groups.
+             * @param ddGroupVariableIndices The (sorted) indices of all DD group variables that need to be considered.
+             * @param currentLevel The currently considered level in the DD.
              * @param maxLevel The number of levels that need to be considered.
-             * @param currentRowOffset The current row offset.
-             * @param ddRowVariableIndices The (sorted) indices of all DD row variables that need to be considered.
+             * @param remainingMetaVariables The meta variables that remain in the DDs after the groups have been split.
              */
-            void toVectorRec(DdNode const* dd, std::vector<ValueType>& result, std::vector<uint_fast64_t> const& rowGroupOffsets, Odd<DdType::CUDD> const& rowOdd, uint_fast64_t currentRowLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, std::vector<uint_fast64_t> const& ddRowVariableIndices) const;
+            void splitIntoGroupsRec(DdNode* dd, std::vector<InternalAdd<DdType::CUDD, ValueType>>& groups, std::vector<uint_fast64_t> const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel) const;
+            
+            void splitIntoGroupsRec(DdNode* dd1, DdNode* dd2, std::vector<std::pair<InternalAdd<DdType::CUDD, ValueType>, InternalAdd<DdType::CUDD, ValueType>>>& groups, std::vector<uint_fast64_t> const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel) const;
             
             /*!
              * Helper function to convert the DD into a (sparse) matrix.
@@ -590,33 +580,7 @@ namespace storm {
              * only works if the offsets given in rowIndications are already correct. If they need to be computed first,
              * this flag needs to be false.
              */
-            void toMatrixRec(DdNode const* dd, std::vector<uint_fast64_t>& rowIndications, std::vector<storm::storage::MatrixEntry<uint_fast64_t, double>>& columnsAndValues, std::vector<uint_fast64_t> const& rowGroupOffsets, Odd<DdType::CUDD> const& rowOdd, Odd<DdType::CUDD> const& columnOdd, uint_fast64_t currentRowLevel, uint_fast64_t currentColumnLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, uint_fast64_t currentColumnOffset, std::vector<uint_fast64_t> const& ddRowVariableIndices, std::vector<uint_fast64_t> const& ddColumnVariableIndices, bool generateValues = true) const;
-            
-            /*!
-             * Splits the given matrix DD into the groups using the given group variables.
-             *
-             * @param dd The DD to split.
-             * @param groups A vector that is to be filled with the DDs for the individual groups.
-             * @param ddGroupVariableIndices The (sorted) indices of all DD group variables that need to be considered.
-             * @param currentLevel The currently considered level in the DD.
-             * @param maxLevel The number of levels that need to be considered.
-             * @param remainingMetaVariables The meta variables that remain in the DDs after the groups have been split.
-             */
-            void splitGroupsRec(DdNode* dd, std::vector<InternalAdd<DdType::CUDD, ValueType>>& groups, std::vector<uint_fast64_t> const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel) const;
-            
-            /*!
-             * Splits the given matrix and vector DDs into the groups using the given group variables.
-             *
-             * @param dd1 The matrix DD to split.
-             * @param dd2 The vector DD to split.
-             * @param groups A vector that is to be filled with the pairs of matrix/vector DDs for the individual groups.
-             * @param ddGroupVariableIndices The (sorted) indices of all DD group variables that need to be considered.
-             * @param currentLevel The currently considered level in the DD.
-             * @param maxLevel The number of levels that need to be considered.
-             * @param remainingMetaVariables1 The meta variables that remain in the matrix DD after the groups have been split.
-             * @param remainingMetaVariables2 The meta variables that remain in the vector DD after the groups have been split.
-             */
-            void splitGroupsRec(DdNode* dd1, DdNode* dd2, std::vector<std::pair<InternalAdd<DdType::CUDD, ValueType>, InternalAdd<DdType::CUDD, ValueType>>>& groups, std::vector<uint_fast64_t> const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel) const;
+            void toMatrixComponentsRec(DdNode const* dd, std::vector<uint_fast64_t> const& rowGroupOffsets, std::vector<uint_fast64_t>& rowIndications, std::vector<storm::storage::MatrixEntry<uint_fast64_t, double>>& columnsAndValues, Odd<DdType::CUDD> const& rowOdd, Odd<DdType::CUDD> const& columnOdd, uint_fast64_t currentRowLevel, uint_fast64_t currentColumnLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, uint_fast64_t currentColumnOffset, std::vector<uint_fast64_t> const& ddRowVariableIndices, std::vector<uint_fast64_t> const& ddColumnVariableIndices, bool writeValues) const;
             
             /*!
              * Builds an ADD representing the given vector.