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::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::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 sylvan::Mtbdd InternalAdd::getSylvanMtbdd() const { return sylvanMtbdd;