From dbbae87962113cfbdfe16ae0caa3ab1198beff06 Mon Sep 17 00:00:00 2001
From: PBerger <philipp.berger@rwth-aachen.de>
Date: Wed, 27 Jul 2016 17:23:23 +0200
Subject: [PATCH] Fixed template specialization. Re-Implemented terminal
 generation.

Former-commit-id: 253f95b673e6415f069dc148d0cd6d015d4c029e
---
 src/storage/dd/DdManager.cpp                      | 3 ++-
 src/storage/dd/sylvan/InternalSylvanDdManager.cpp | 7 +------
 2 files changed, 3 insertions(+), 7 deletions(-)

diff --git a/src/storage/dd/DdManager.cpp b/src/storage/dd/DdManager.cpp
index 22dc7c753..7a1a9ab8d 100644
--- a/src/storage/dd/DdManager.cpp
+++ b/src/storage/dd/DdManager.cpp
@@ -108,13 +108,14 @@ namespace storm {
         
 #ifdef STORM_HAVE_CARL
 		template<>
+		template<>
         Add<DdType::Sylvan, storm::RationalFunction> DdManager<DdType::Sylvan>::getIdentity(storm::expressions::Variable const& variable) const {
             storm::dd::DdMetaVariable<DdType::Sylvan> const& metaVariable = this->getMetaVariable(variable);
             
             Add<DdType::Sylvan, storm::RationalFunction> result = this->getAddZero<storm::RationalFunction>();
             for (int_fast64_t value = metaVariable.getLow(); value <= metaVariable.getHigh(); ++value) {
 				storm::RationalFunction constantFunction(value);
-                result += this->getEncoding(variable, value).template toAdd<ValueType>() * this->getConstant(constantFunction);
+                result += this->getEncoding(variable, value).template toAdd<storm::RationalFunction>() * this->getConstant(constantFunction);
             }
             return result;
         }
diff --git a/src/storage/dd/sylvan/InternalSylvanDdManager.cpp b/src/storage/dd/sylvan/InternalSylvanDdManager.cpp
index c10235ca8..287fe55c3 100644
--- a/src/storage/dd/sylvan/InternalSylvanDdManager.cpp
+++ b/src/storage/dd/sylvan/InternalSylvanDdManager.cpp
@@ -131,12 +131,7 @@ namespace storm {
 #ifdef STORM_HAVE_CARL
 		template<>
 		InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalDdManager<DdType::Sylvan>::getConstant(storm::RationalFunction const& value) const {
-			storm::RationalFunction rationalFunction = value;
-			storm_rational_function_ptr_struct helperStruct;
-			helperStruct.storm_rational_function = (void*)(&rationalFunction);
-			uint64_t terminalValue = (uint64_t)&helperStruct;
-
-			return InternalAdd<DdType::Sylvan, storm::RationalFunction>(this, sylvan::Mtbdd::terminal(sylvan_storm_rational_function_get_type(), terminalValue));
+			return InternalAdd<DdType::Sylvan, storm::RationalFunction>(this, sylvan::Mtbdd::stormRationalFunctionTerminal(value));
 		}
 #endif