diff --git a/src/storage/dd/sylvan/InternalSylvanAdd.cpp b/src/storage/dd/sylvan/InternalSylvanAdd.cpp index fb9834aaa..a244cc198 100644 --- a/src/storage/dd/sylvan/InternalSylvanAdd.cpp +++ b/src/storage/dd/sylvan/InternalSylvanAdd.cpp @@ -10,6 +10,12 @@ #include "src/utility/constants.h" #include "src/exceptions/NotImplementedException.h" +#include "storm-config.h" +// TODO: Remove this later on. +#ifndef STORM_HAVE_CARL +#define STORM_HAVE_CARL 1 +#endif + namespace storm { namespace dd { template @@ -614,7 +620,19 @@ namespace storm { } else if (std::is_same::value) { STORM_LOG_ASSERT(mtbdd_gettype(node) == 0, "Expected an unsigned value."); return negated ? -mtbdd_getint64(node) : mtbdd_getint64(node); - } else { + } +#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(leaf); + 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 + else { STORM_LOG_ASSERT(false, "Illegal or unknown type in MTBDD."); } } @@ -626,5 +644,8 @@ namespace storm { template class InternalAdd; template class InternalAdd; +#ifdef STORM_HAVE_CARL + template class InternalAdd; +#endif } } \ No newline at end of file diff --git a/src/storage/dd/sylvan/InternalSylvanDdManager.cpp b/src/storage/dd/sylvan/InternalSylvanDdManager.cpp index 06fcd57bb..93445387f 100644 --- a/src/storage/dd/sylvan/InternalSylvanDdManager.cpp +++ b/src/storage/dd/sylvan/InternalSylvanDdManager.cpp @@ -9,6 +9,14 @@ #include "src/utility/macros.h" #include "src/exceptions/NotSupportedException.h" +#include "src/utility/sylvan.h" + +#include "storm-config.h" +// TODO: Remove this later on. +#ifndef STORM_HAVE_CARL +#define STORM_HAVE_CARL 1 +#endif + namespace storm { namespace dd { uint_fast64_t InternalDdManager::numberOfInstances = 0; @@ -75,7 +83,10 @@ namespace storm { #ifdef STORM_HAVE_CARL template<> InternalAdd InternalDdManager::getAddOne() const { - return InternalAdd(this, sylvan::Mtbdd::terminal(sylvan_storm_rational_function_get_type(), storm::utility::one())); + storm::RationalFunction rationalFunction = storm::utility::one(); + storm_rational_function_ptr_struct helperStruct; + helperStruct.storm_rational_function = static_cast(&rationalFunction); + return InternalAdd(this, sylvan::Mtbdd::terminal(sylvan_storm_rational_function_get_type(), helperStruct)); } #endif @@ -96,7 +107,10 @@ namespace storm { #ifdef STORM_HAVE_CARL template<> InternalAdd InternalDdManager::getAddZero() const { - return InternalAdd(this, sylvan::Mtbdd::terminal(sylvan_storm_rational_function_get_type(), storm::utility::zero())); + storm::RationalFunction rationalFunction = storm::utility::zero(); + storm_rational_function_ptr_struct helperStruct; + helperStruct.storm_rational_function = static_cast(&rationalFunction); + return InternalAdd(this, sylvan::Mtbdd::terminal(sylvan_storm_rational_function_get_type(), helperStruct)); } #endif @@ -113,7 +127,10 @@ namespace storm { #ifdef STORM_HAVE_CARL template<> InternalAdd InternalDdManager::getConstant(storm::RationalFunction const& value) const { - return InternalAdd(this, sylvan::Mtbdd::terminal(sylvan_storm_rational_function_get_type(), storm::utility::zero())); + storm::RationalFunction rationalFunction = value; + storm_rational_function_ptr_struct helperStruct; + helperStruct.storm_rational_function = static_cast(&rationalFunction); + return InternalAdd(this, sylvan::Mtbdd::terminal(sylvan_storm_rational_function_get_type(), helperStruct)); } #endif @@ -138,11 +155,20 @@ namespace storm { template InternalAdd InternalDdManager::getAddOne() const; template InternalAdd InternalDdManager::getAddOne() const; +#ifdef STORM_HAVE_CARL + template InternalAdd InternalDdManager::getAddOne() const; +#endif template InternalAdd InternalDdManager::getAddZero() const; template InternalAdd InternalDdManager::getAddZero() const; +#ifdef STORM_HAVE_CARL + template InternalAdd InternalDdManager::getAddZero() const; +#endif template InternalAdd InternalDdManager::getConstant(double const& value) const; template InternalAdd InternalDdManager::getConstant(uint_fast64_t const& value) const; +#ifdef STORM_HAVE_CARL + template InternalAdd InternalDdManager::getConstant(storm::RationalFunction const& value) const; +#endif } } \ No newline at end of file