|
@ -626,19 +626,31 @@ namespace storm { |
|
|
} |
|
|
} |
|
|
#ifdef STORM_HAVE_CARL
|
|
|
#ifdef STORM_HAVE_CARL
|
|
|
else if (std::is_same<ValueType, storm::RationalFunction>::value) { |
|
|
else if (std::is_same<ValueType, storm::RationalFunction>::value) { |
|
|
|
|
|
STORM_LOG_ASSERT(false, "Non-specialized version of getValue() called for storm::RationalFunction value."); |
|
|
|
|
|
} |
|
|
|
|
|
#endif
|
|
|
|
|
|
else { |
|
|
|
|
|
STORM_LOG_ASSERT(false, "Illegal or unknown type in MTBDD."); |
|
|
|
|
|
} |
|
|
|
|
|
} |
|
|
|
|
|
|
|
|
|
|
|
#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."); |
|
|
STORM_LOG_ASSERT(mtbdd_gettype(node) == sylvan_storm_rational_function_get_type(), "Expected a storm::RationalFunction value."); |
|
|
uint64_t value = mtbdd_getvalue(node); |
|
|
uint64_t value = mtbdd_getvalue(node); |
|
|
storm_rational_function_ptr_struct* helperStructPtr = (storm_rational_function_ptr_struct*) value; |
|
|
|
|
|
|
|
|
storm_rational_function_ptr_struct* helperStructPtr = (storm_rational_function_ptr_struct*)value; |
|
|
|
|
|
|
|
|
storm::RationalFunction* rationalFunction = (storm::RationalFunction*)(helperStructPtr->storm_rational_function); |
|
|
storm::RationalFunction* rationalFunction = (storm::RationalFunction*)(helperStructPtr->storm_rational_function); |
|
|
|
|
|
|
|
|
return negated ? -(*rationalFunction) : (*rationalFunction); |
|
|
return negated ? -(*rationalFunction) : (*rationalFunction); |
|
|
} |
|
|
} |
|
|
#endif
|
|
|
#endif
|
|
|
else { |
|
|
|
|
|
STORM_LOG_ASSERT(false, "Illegal or unknown type in MTBDD."); |
|
|
|
|
|
} |
|
|
|
|
|
} |
|
|
|
|
|
|
|
|
|
|
|
template<typename ValueType> |
|
|
template<typename ValueType> |
|
|
sylvan::Mtbdd InternalAdd<DdType::Sylvan, ValueType>::getSylvanMtbdd() const { |
|
|
sylvan::Mtbdd InternalAdd<DdType::Sylvan, ValueType>::getSylvanMtbdd() const { |
|
|