started optimizing some DdManager methods

resources/3rdparty/cudd-3.0.0/cudd/cudd.h

@@ -503,6 +503,9 @@ typedef void (*DD_TOHFP)(DdManager *, void *);
 extern "C" {
 #endif
 
+// Make this visible to the outside.
+extern DdNode * cuddUniqueInter(DdManager *unique, int index, DdNode *T, DdNode *E);
+    
 extern DdNode * Cudd_addNewVar(DdManager *dd);
 extern DdNode * Cudd_addNewVarAtLevel(DdManager *dd, int level);
 extern DdNode * Cudd_bddNewVar(DdManager *dd);

src/storm/abstraction/AbstractionInformation.cpp

@@ -499,7 +499,7 @@ namespace storm {
             allSuccessorLocationVariables.insert(newMetaVariable.second);
             successorVariables.insert(newMetaVariable.second);
             extendedPredicateDdVariables.emplace_back(newMetaVariable);
-            allLocationIdentities &= ddManager->template getIdentity<uint64_t>(newMetaVariable.first).equals(ddManager->template getIdentity<uint64_t>(newMetaVariable.second)) && ddManager->getRange(newMetaVariable.first) && ddManager->getRange(newMetaVariable.second);
+            allLocationIdentities &= ddManager->getIdentity(newMetaVariable.first, newMetaVariable.second);
             return std::make_pair(locationVariablePairs.back(), locationVariablePairs.size() - 1);
         }
         

src/storm/builder/DdJaniModelBuilder.cpp

@@ -368,8 +368,8 @@ namespace storm {
                     
                     // Add the identity and ranges of the location variables to the ones of the automaton.
                     std::pair<storm::expressions::Variable, storm::expressions::Variable> const& locationVariables = result.automatonToLocationDdVariableMap[automaton.getName()];
-                    storm::dd::Add<Type, ValueType> variableIdentity = result.manager->template getIdentity<ValueType>(locationVariables.first).equals(result.manager->template getIdentity<ValueType>(locationVariables.second)).template toAdd<ValueType>() * result.manager->getRange(locationVariables.first).template toAdd<ValueType>() * result.manager->getRange(locationVariables.second).template toAdd<ValueType>();
-                    identity &= variableIdentity.toBdd();
+                    storm::dd::Bdd<Type> variableIdentity = result.manager->getIdentity(locationVariables.first, locationVariables.second);
+                    identity &= variableIdentity;
                     range &= result.manager->getRange(locationVariables.first);
                     
                     // Then create variables for the variables of the automaton.
@@ -420,8 +420,8 @@ namespace storm {
                 result.columnMetaVariables.insert(variablePair.second);
                 result.variableToColumnMetaVariableMap->emplace(variable.getExpressionVariable(), variablePair.second);
                 
-                storm::dd::Add<Type, ValueType> variableIdentity = result.manager->template getIdentity<ValueType>(variablePair.first).equals(result.manager->template getIdentity<ValueType>(variablePair.second)).template toAdd<ValueType>() * result.manager->getRange(variablePair.first).template toAdd<ValueType>() * result.manager->getRange(variablePair.second).template toAdd<ValueType>();
-                result.variableToIdentityMap.emplace(variable.getExpressionVariable(), variableIdentity);
+                storm::dd::Bdd<Type> variableIdentity = result.manager->getIdentity(variablePair.first, variablePair.second);
+                result.variableToIdentityMap.emplace(variable.getExpressionVariable(), variableIdentity.template toAdd<ValueType>());
                 result.rowColumnMetaVariablePairs.push_back(variablePair);
                 result.variableToRangeMap.emplace(variablePair.first, result.manager->getRange(variablePair.first));
                 result.variableToRangeMap.emplace(variablePair.second, result.manager->getRange(variablePair.second));
@@ -440,8 +440,8 @@ namespace storm {
                 result.columnMetaVariables.insert(variablePair.second);
                 result.variableToColumnMetaVariableMap->emplace(variable.getExpressionVariable(), variablePair.second);
                 
-                storm::dd::Add<Type, ValueType> variableIdentity = result.manager->template getIdentity<ValueType>(variablePair.first).equals(result.manager->template getIdentity<ValueType>(variablePair.second)).template toAdd<ValueType>();
-                result.variableToIdentityMap.emplace(variable.getExpressionVariable(), variableIdentity);
+                storm::dd::Bdd<Type> variableIdentity = result.manager->getIdentity(variablePair.first, variablePair.second);
+                result.variableToIdentityMap.emplace(variable.getExpressionVariable(), variableIdentity.template toAdd<ValueType>());
                 
                 result.variableToRangeMap.emplace(variablePair.first, result.manager->getRange(variablePair.first));
                 result.variableToRangeMap.emplace(variablePair.second, result.manager->getRange(variablePair.second));

src/storm/builder/DdPrismModelBuilder.cpp

@@ -189,8 +189,8 @@ namespace storm {
                     columnMetaVariables.insert(variablePair.second);
                     variableToColumnMetaVariableMap->emplace(integerVariable.getExpressionVariable(), variablePair.second);
                     
-                    storm::dd::Add<Type, ValueType> variableIdentity = manager->template getIdentity<ValueType>(variablePair.first).equals(manager->template getIdentity<ValueType>(variablePair.second)).template toAdd<ValueType>() * manager->getRange(variablePair.first).template toAdd<ValueType>() * manager->getRange(variablePair.second).template toAdd<ValueType>();
-                    variableToIdentityMap.emplace(integerVariable.getExpressionVariable(), variableIdentity);
+                    storm::dd::Bdd<Type> variableIdentity = manager->getIdentity(variablePair.first, variablePair.second);
+                    variableToIdentityMap.emplace(integerVariable.getExpressionVariable(), variableIdentity.template toAdd<ValueType>());
                     rowColumnMetaVariablePairs.push_back(variablePair);
                     
                     allGlobalVariables.insert(integerVariable.getExpressionVariable());
@@ -206,8 +206,8 @@ namespace storm {
                     columnMetaVariables.insert(variablePair.second);
                     variableToColumnMetaVariableMap->emplace(booleanVariable.getExpressionVariable(), variablePair.second);
                     
-                    storm::dd::Add<Type, ValueType> variableIdentity = manager->template getIdentity<ValueType>(variablePair.first).equals(manager->template getIdentity<ValueType>(variablePair.second)).template toAdd<ValueType>();
-                    variableToIdentityMap.emplace(booleanVariable.getExpressionVariable(), variableIdentity);
+                    storm::dd::Bdd<Type> variableIdentity = manager->getIdentity(variablePair.first, variablePair.second);
+                    variableToIdentityMap.emplace(booleanVariable.getExpressionVariable(), variableIdentity.template toAdd<ValueType>());
                     
                     rowColumnMetaVariablePairs.push_back(variablePair);
                     allGlobalVariables.insert(booleanVariable.getExpressionVariable());
@@ -230,7 +230,7 @@ namespace storm {
                         columnMetaVariables.insert(variablePair.second);
                         variableToColumnMetaVariableMap->emplace(integerVariable.getExpressionVariable(), variablePair.second);
                         
-                        storm::dd::Bdd<Type> variableIdentity = manager->template getIdentity<ValueType>(variablePair.first).equals(manager->template getIdentity<ValueType>(variablePair.second)) && manager->getRange(variablePair.first) && manager->getRange(variablePair.second);
+                        storm::dd::Bdd<Type> variableIdentity = manager->getIdentity(variablePair.first, variablePair.second);
                         variableToIdentityMap.emplace(integerVariable.getExpressionVariable(), variableIdentity.template toAdd<ValueType>());
                         moduleIdentity &= variableIdentity;
                         moduleRange &= manager->getRange(variablePair.first);
@@ -247,7 +247,7 @@ namespace storm {
                         columnMetaVariables.insert(variablePair.second);
                         variableToColumnMetaVariableMap->emplace(booleanVariable.getExpressionVariable(), variablePair.second);
                         
-                        storm::dd::Bdd<Type> variableIdentity = manager->template getIdentity<ValueType>(variablePair.first).equals(manager->template getIdentity<ValueType>(variablePair.second)) && manager->getRange(variablePair.first) && manager->getRange(variablePair.second);
+                        storm::dd::Bdd<Type> variableIdentity = manager->getIdentity(variablePair.first, variablePair.second);
                         variableToIdentityMap.emplace(booleanVariable.getExpressionVariable(), variableIdentity.template toAdd<ValueType>());
                         moduleIdentity &= variableIdentity;
                         moduleRange &= manager->getRange(variablePair.first);

src/storm/models/symbolic/Model.cpp

@@ -208,7 +208,7 @@ namespace storm {
             
             template<storm::dd::DdType Type, typename ValueType>
             storm::dd::Add<Type, ValueType> Model<Type, ValueType>::getRowColumnIdentity() const {
-                return storm::utility::dd::getRowColumnDiagonal<Type, ValueType>(this->getManager(), this->getRowColumnMetaVariablePairs());
+                return (storm::utility::dd::getRowColumnDiagonal<Type>(this->getManager(), this->getRowColumnMetaVariablePairs()) && this->getReachableStates()).template toAdd<ValueType>();
             }
             
             template<storm::dd::DdType Type, typename ValueType>

src/storm/storage/dd/DdManager.cpp

@@ -122,16 +122,21 @@ namespace storm {
         template<DdType LibraryType>
         Bdd<LibraryType> DdManager<LibraryType>::getRange(storm::expressions::Variable const& variable) const {
             storm::dd::DdMetaVariable<LibraryType> const& metaVariable = this->getMetaVariable(variable);
-            STORM_LOG_THROW(metaVariable.hasHigh(), storm::exceptions::InvalidOperationException, "Cannot create range for meta variable.");
-            
-            Bdd<LibraryType> result = this->getBddZero();
-            
-            for (int_fast64_t value = metaVariable.getLow(); value <= metaVariable.getHigh(); ++value) {
-                result |= this->getEncoding(variable, value);
-            }
 
+            if (metaVariable.hasHigh()) {
+                return Bdd<LibraryType>(*this, internalDdManager.getBddEncodingLessOrEqualThan(static_cast<uint64_t>(metaVariable.getHigh() - metaVariable.getLow()), metaVariable.getCube().getInternalBdd(), metaVariable.getNumberOfDdVariables()), {variable});
+//                Bdd<LibraryType> result = this->getBddZero();
+//                for (int_fast64_t value = metaVariable.getLow(); value <= metaVariable.getHigh(); ++value) {
+//                    result |= this->getEncoding(variable, value);
+//                }
+//                return result;
+            } else {
+                // If there is no upper bound on this variable, the whole range is valid.
+                Bdd<LibraryType> result = this->getBddOne();
+                result.addMetaVariable(variable);
                 return result;
             }
+        }
 
         template<DdType LibraryType>
         template<typename ValueType>
@@ -146,6 +151,33 @@ namespace storm {
             return result;
         }
 		
+        template<DdType LibraryType>
+        Bdd<LibraryType> DdManager<LibraryType>::getIdentity(std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& variablePairs, bool restrictToFirstRange) const {
+            auto result = this->getBddOne();
+            for (auto const& pair : variablePairs) {
+                result &= this->getIdentity(pair.first, pair.second, restrictToFirstRange);
+            }
+            return result;
+        }
+        
+        template<DdType LibraryType>
+        Bdd<LibraryType> DdManager<LibraryType>::getIdentity(storm::expressions::Variable const& first, storm::expressions::Variable const& second, bool restrictToFirstRange) const {
+            auto const& firstMetaVariable = this->getMetaVariable(first);
+            auto const& secondMetaVariable = this->getMetaVariable(second);
+            
+            STORM_LOG_THROW(firstMetaVariable.getNumberOfDdVariables() == secondMetaVariable.getNumberOfDdVariables(), storm::exceptions::InvalidOperationException, "Mismatching sizes of meta variables.");
+            
+            auto const& firstDdVariables = firstMetaVariable.getDdVariables();
+            auto const& secondDdVariables = secondMetaVariable.getDdVariables();
+
+            auto result = restrictToFirstRange ? this->getRange(first) : this->getBddOne();
+            for (auto it1 = firstDdVariables.begin(), it2 = secondDdVariables.begin(), ite1 = firstDdVariables.end(); it1 != ite1; ++it1, ++it2) {
+                result &= it1->iff(*it2);
+            }
+            
+            return result;
+        }
+        
         template<DdType LibraryType>
         Bdd<LibraryType> DdManager<LibraryType>::getCube(storm::expressions::Variable const& variable) const {
             return getCube({variable});

src/storm/storage/dd/DdManager.h

@@ -131,6 +131,23 @@ namespace storm {
             template<typename ValueType>
             Add<LibraryType, ValueType> getIdentity(storm::expressions::Variable const& variable) const;
             
+            /*!
+             * Retrieves a BDD in which an encoding is mapped to true iff the meta variables of each pair encode the same value.
+             *
+             * @param variablePairs The variable pairs for which to compute the identity.
+             * @param restrictToFirstRange If set, the identity will be restricted to the legal range of the first variable.
+             */
+            Bdd<LibraryType> getIdentity(std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& variablePairs, bool restrictToFirstRange = true) const;
+
+            /*!
+             * Retrieves a BDD in which an encoding is mapped to true iff the two meta variables encode the same value.
+             * 
+             * @param first The first meta variable in the identity.
+             * @param second The second meta variable in the identity.
+             * @param restrictToFirstRange If set, the identity will be restricted to the legal range of the first variable.
+             */
+            Bdd<LibraryType> getIdentity(storm::expressions::Variable const& first, storm::expressions::Variable const& second, bool restrictToFirstRange = true) const;
+
             /*!
              * Retrieves a BDD that is the cube of the variables representing the given meta variable.
              *

src/storm/storage/dd/bisimulation/SignatureRefiner.cpp

@@ -198,18 +198,13 @@ namespace storm {
                             result = thenResult;
                         } else {
                             // Get the node to connect the subresults.
-                            DdNode* var = Cudd_addIthVar(ddman, Cudd_NodeReadIndex(nonBlockVariablesNode) + offset);
-                            Cudd_Ref(var);
-                            result = Cudd_addIte(ddman, var, thenResult, elseResult);
-                            Cudd_Ref(result);
-                            Cudd_RecursiveDeref(ddman, var);
+                            result = cuddUniqueInter(ddman, Cudd_NodeReadIndex(nonBlockVariablesNode) + offset, thenResult, elseResult);
                             Cudd_Deref(thenResult);
                             Cudd_Deref(elseResult);
                         }
                         
                         // Store the result in the cache.
                         signatureCache[nodePair] = result;
-                        Cudd_Deref(result);
                         
                         return result;
                     }

src/storm/storage/dd/cudd/InternalCuddDdManager.cpp

@@ -57,6 +57,42 @@ namespace storm {
             return InternalBdd<DdType::CUDD>(this, cuddManager.bddZero());
         }
         
+        InternalBdd<DdType::CUDD> InternalDdManager<DdType::CUDD>::getBddEncodingLessOrEqualThan(uint64_t bound, InternalBdd<DdType::CUDD> const& cube, uint64_t numberOfDdVariables) const {
+            DdNodePtr node = this->getBddEncodingLessOrEqualThanRec(0, (1ull << numberOfDdVariables) - 1, bound, cube.getCuddDdNode(), numberOfDdVariables);
+            STORM_LOG_ASSERT(node != nullptr, "Wut?");
+            FILE* fp = fopen("range.dot", "w");
+            Cudd_DumpDot(cuddManager.getManager(), 1, &node, nullptr, nullptr, fp);
+            fclose(fp);
+            
+            auto tmp = cudd::BDD(cuddManager, node);
+            return InternalBdd<DdType::CUDD>(this, tmp);
+        }
+        
+        DdNodePtr InternalDdManager<DdType::CUDD>::getBddEncodingLessOrEqualThanRec(uint64_t minimalValue, uint64_t maximalValue, uint64_t bound, DdNodePtr cube, uint64_t remainingDdVariables) const {
+            std::cout << minimalValue << " / " << maximalValue << " -> " << bound << std::endl;
+            if (maximalValue <= bound) {
+                return Cudd_ReadOne(cuddManager.getManager());
+            } else if (minimalValue > bound) {
+                return Cudd_ReadLogicZero(cuddManager.getManager());
+            }
+            
+            STORM_LOG_ASSERT(remainingDdVariables > 0, "Expected more remaining DD variables.");
+            STORM_LOG_ASSERT(!Cudd_IsConstant(cube), "Expected non-constant cube.");
+            uint64_t newRemainingDdVariables = remainingDdVariables - 1;
+            DdNodePtr elseResult = getBddEncodingLessOrEqualThanRec(minimalValue, maximalValue & ~(1ull << newRemainingDdVariables), bound, Cudd_T(cube), newRemainingDdVariables);
+            Cudd_Ref(elseResult);
+            DdNodePtr thenResult = getBddEncodingLessOrEqualThanRec(minimalValue | (1ull << newRemainingDdVariables), maximalValue, bound, Cudd_T(cube), newRemainingDdVariables);
+            Cudd_Ref(thenResult);
+            STORM_LOG_ASSERT(thenResult != elseResult, "Expected different results.");
+            
+            std::cout << "creating " << Cudd_NodeReadIndex(cube) << " -> " << thenResult << " / " << elseResult << std::endl;
+            DdNodePtr result = cuddUniqueInter(cuddManager.getManager(), Cudd_NodeReadIndex(cube), thenResult, elseResult);
+            std::cout << "result " << result << std::endl;
+            Cudd_Deref(thenResult);
+            Cudd_Deref(elseResult);
+            return result;
+        }
+        
         template<typename ValueType>
         InternalAdd<DdType::CUDD, ValueType> InternalDdManager<DdType::CUDD>::getAddZero() const {
             return InternalAdd<DdType::CUDD, ValueType>(this, cuddManager.addZero());

src/storm/storage/dd/cudd/InternalCuddDdManager.h

@@ -59,6 +59,13 @@ namespace storm {
              */
             InternalBdd<DdType::CUDD> getBddZero() const;
             
+            /*!
+             * Retrieves a BDD that maps to true iff the encoding is less or equal than the given bound.
+             *
+             * @return A BDD with encodings corresponding to values less or equal than the bound.
+             */
+            InternalBdd<DdType::CUDD> getBddEncodingLessOrEqualThan(uint64_t bound, InternalBdd<DdType::CUDD> const& cube, uint64_t numberOfDdVariables) const;
+            
             /*!
              * Retrieves an ADD representing the constant zero function.
              *
@@ -146,6 +153,9 @@ namespace storm {
             cudd::Cudd const& getCuddManager() const;
 
         private:
+            // Helper function to create the BDD whose encodings are below a given bound.
+            DdNodePtr getBddEncodingLessOrEqualThanRec(uint64_t minimalValue, uint64_t maximalValue, uint64_t bound, DdNodePtr cube, uint64_t remainingDdVariables) const;
+            
             // The manager responsible for the DDs created/modified with this DdManager.
             cudd::Cudd cuddManager;
             

src/storm/storage/dd/sylvan/InternalSylvanDdManager.cpp

@@ -129,6 +129,28 @@ namespace storm {
             return InternalBdd<DdType::Sylvan>(this, sylvan::Bdd::bddZero());
         }
         
+        InternalBdd<DdType::Sylvan> InternalDdManager<DdType::Sylvan>::getBddEncodingLessOrEqualThan(uint64_t bound, InternalBdd<DdType::Sylvan> const& cube, uint64_t numberOfDdVariables) const {
+            return InternalBdd<DdType::Sylvan>(this, sylvan::Bdd(this->getBddEncodingLessOrEqualThanRec(0, (1ull << numberOfDdVariables) - 1, bound, cube.getSylvanBdd().GetBDD(), numberOfDdVariables)));
+        }
+        
+        BDD InternalDdManager<DdType::Sylvan>::getBddEncodingLessOrEqualThanRec(uint64_t minimalValue, uint64_t maximalValue, uint64_t bound, BDD cube, uint64_t remainingDdVariables) const {
+            if (maximalValue <= bound) {
+                return sylvan_true;
+            } else if (minimalValue > bound) {
+                return sylvan_false;
+            }
+            
+            STORM_LOG_ASSERT(remainingDdVariables > 0, "Expected more remaining DD variables.");
+            uint64_t newRemainingDdVariables = remainingDdVariables - 1;
+            BDD elseResult = getBddEncodingLessOrEqualThanRec(minimalValue, maximalValue & ~(1ull << newRemainingDdVariables), bound, sylvan_high(cube), newRemainingDdVariables);
+            bdd_refs_push(elseResult);
+            BDD thenResult = getBddEncodingLessOrEqualThanRec(minimalValue | (1ull << newRemainingDdVariables), maximalValue, bound, sylvan_high(cube), newRemainingDdVariables);
+            bdd_refs_push(elseResult);
+            BDD result = sylvan_makenode(sylvan_var(cube), elseResult, thenResult);
+            bdd_refs_pop(2);
+            return result;
+        }
+        
         template<>
         InternalAdd<DdType::Sylvan, double> InternalDdManager<DdType::Sylvan>::getAddZero() const {
             return InternalAdd<DdType::Sylvan, double>(this, sylvan::Mtbdd::doubleTerminal(storm::utility::zero<double>()));

src/storm/storage/dd/sylvan/InternalSylvanDdManager.h

@@ -60,6 +60,13 @@ namespace storm {
              */
             InternalBdd<DdType::Sylvan> getBddZero() const;
             
+            /*!
+             * Retrieves a BDD that maps to true iff the encoding is less or equal than the given bound.
+             *
+             * @return A BDD with encodings corresponding to values less or equal than the bound.
+             */
+            InternalBdd<DdType::Sylvan> getBddEncodingLessOrEqualThan(uint64_t bound, InternalBdd<DdType::Sylvan> const& cube, uint64_t numberOfDdVariables) const;
+
             /*!
              * Retrieves an ADD representing the constant zero function.
              *
@@ -133,6 +140,9 @@ namespace storm {
             uint_fast64_t getNumberOfDdVariables() const;
             
         private:
+            // Helper function to create the BDD whose encodings are below a given bound.
+            BDD getBddEncodingLessOrEqualThanRec(uint64_t minimalValue, uint64_t maximalValue, uint64_t bound, BDD cube, uint64_t remainingDdVariables) const;
+            
             // A counter for the number of instances of this class. This is used to determine when to initialize and
             // quit the sylvan. This is because Sylvan does not know the concept of managers but implicitly has a
             // 'global' manager.

src/storm/utility/dd.cpp

@@ -45,38 +45,17 @@ namespace storm {
                 return reachableStates;
             }
             
-            template <storm::dd::DdType Type, typename ValueType>
-            storm::dd::Add<Type, ValueType> getRowColumnDiagonal(storm::dd::DdManager<Type> const& ddManager, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs) {
-                storm::dd::Add<Type, ValueType> result = ddManager.template getAddOne<ValueType>();
-                for (auto const& pair : rowColumnMetaVariablePairs) {
-                    result *= ddManager.template getIdentity<ValueType>(pair.first).equals(ddManager.template getIdentity<ValueType>(pair.second)).template toAdd<ValueType>();
-                    result *= ddManager.getRange(pair.first).template toAdd<ValueType>() * ddManager.getRange(pair.second).template toAdd<ValueType>();
-                }
-                return result;
-            }
-            
             template <storm::dd::DdType Type>
             storm::dd::Bdd<Type> getRowColumnDiagonal(storm::dd::DdManager<Type> const& ddManager, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs) {
-                storm::dd::Bdd<Type> diagonal = ddManager.getBddOne();
-                for (auto const& pair : rowColumnMetaVariablePairs) {
-                    diagonal &= ddManager.template getIdentity<uint64_t>(pair.first).equals(ddManager.template getIdentity<uint64_t>(pair.second));
-                    diagonal &= ddManager.getRange(pair.first) && ddManager.getRange(pair.second);
-                }
-                return diagonal;
+                return ddManager.getIdentity(rowColumnMetaVariablePairs);
             }
             
             template storm::dd::Bdd<storm::dd::DdType::CUDD> computeReachableStates(storm::dd::Bdd<storm::dd::DdType::CUDD> const& initialStates, storm::dd::Bdd<storm::dd::DdType::CUDD> const& transitions, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables);
             template storm::dd::Bdd<storm::dd::DdType::Sylvan> computeReachableStates(storm::dd::Bdd<storm::dd::DdType::Sylvan> const& initialStates, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& transitions, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables);
 
-            template storm::dd::Add<storm::dd::DdType::CUDD, double> getRowColumnDiagonal(storm::dd::DdManager<storm::dd::DdType::CUDD> const& ddManager, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs);
-            template storm::dd::Add<storm::dd::DdType::Sylvan, double> getRowColumnDiagonal(storm::dd::DdManager<storm::dd::DdType::Sylvan> const& ddManager, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs);
-
             template storm::dd::Bdd<storm::dd::DdType::CUDD> getRowColumnDiagonal(storm::dd::DdManager<storm::dd::DdType::CUDD> const& ddManager, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs);
             template storm::dd::Bdd<storm::dd::DdType::Sylvan> getRowColumnDiagonal(storm::dd::DdManager<storm::dd::DdType::Sylvan> const& ddManager, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs);
 
-            template storm::dd::Add<storm::dd::DdType::Sylvan, storm::RationalNumber> getRowColumnDiagonal(storm::dd::DdManager<storm::dd::DdType::Sylvan> const& ddManager, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs);
-            template storm::dd::Add<storm::dd::DdType::Sylvan, storm::RationalFunction> getRowColumnDiagonal(storm::dd::DdManager<storm::dd::DdType::Sylvan> const& ddManager, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs);
-
         }
     }
 }