From 4de8d6c1213eda84ec9a36480c1426d17f2c9f80 Mon Sep 17 00:00:00 2001
From: PBerger <philipp.berger@rwth-aachen.de>
Date: Mon, 18 Jul 2016 19:29:33 +0200
Subject: [PATCH] Moved code to template specialization because of return type
 conversion.

Former-commit-id: cc2e57a22ecaf7f388c415a1d9dbefb9dd5d4d66
---
 src/storage/dd/sylvan/InternalSylvanAdd.cpp | 26 +++++++++++++++------
 1 file changed, 19 insertions(+), 7 deletions(-)

diff --git a/src/storage/dd/sylvan/InternalSylvanAdd.cpp b/src/storage/dd/sylvan/InternalSylvanAdd.cpp
index 1ceb02b01..560592c57 100644
--- a/src/storage/dd/sylvan/InternalSylvanAdd.cpp
+++ b/src/storage/dd/sylvan/InternalSylvanAdd.cpp
@@ -626,13 +626,7 @@ namespace storm {
 			} 
 #ifdef STORM_HAVE_CARL
 			else if (std::is_same<ValueType, storm::RationalFunction>::value) {
-				STORM_LOG_ASSERT(mtbdd_gettype(node) == sylvan_storm_rational_function_get_type(), "Expected a storm::RationalFunction value.");
-				uint64_t value = mtbdd_getvalue(node);
-				storm_rational_function_ptr_struct* helperStructPtr = (storm_rational_function_ptr_struct*) value;
-
-				storm::RationalFunction* rationalFunction = (storm::RationalFunction*)(helperStructPtr->storm_rational_function);
-
-				return negated ? -(*rationalFunction) : (*rationalFunction);
+				STORM_LOG_ASSERT(false, "Non-specialized version of getValue() called for storm::RationalFunction value.");
 			} 
 #endif			
 			else {
@@ -640,6 +634,24 @@ namespace storm {
             }
         }
         
+#ifdef STORM_HAVE_CARL
+		template<>
+		storm::RationalFunction InternalAdd<DdType::Sylvan, ValueType>::getValue(MTBDD const& node) {
+			STORM_LOG_ASSERT(mtbdd_isleaf(node), "Expected leaf, but got variable " << mtbdd_getvar(node) << ".");
+
+			bool negated = mtbdd_hascomp(node);
+			MTBDD n = mtbdd_regular(node);
+
+			STORM_LOG_ASSERT(mtbdd_gettype(node) == sylvan_storm_rational_function_get_type(), "Expected a storm::RationalFunction value.");
+			uint64_t value = mtbdd_getvalue(node);
+			storm_rational_function_ptr_struct* helperStructPtr = (storm_rational_function_ptr_struct*)value;
+
+			storm::RationalFunction* rationalFunction = (storm::RationalFunction*)(helperStructPtr->storm_rational_function);
+
+			return negated ? -(*rationalFunction) : (*rationalFunction);
+		}
+#endif
+
         template<typename ValueType>
         sylvan::Mtbdd InternalAdd<DdType::Sylvan, ValueType>::getSylvanMtbdd() const {
             return sylvanMtbdd;