diff --git a/src/storage/dd/sylvan/InternalSylvanAdd.cpp b/src/storage/dd/sylvan/InternalSylvanAdd.cpp index a244cc198..fe8eafec4 100644 --- a/src/storage/dd/sylvan/InternalSylvanAdd.cpp +++ b/src/storage/dd/sylvan/InternalSylvanAdd.cpp @@ -606,6 +606,13 @@ namespace storm { MTBDD InternalAdd::getLeaf(uint_fast64_t value) { return mtbdd_int64(value); } + + template + MTBDD InternalAdd::getLeaf(storm::RationalFunction const& value) { + storm_rational_function_ptr_struct helperStruct; + helperStruct.storm_rational_function = static_cast(&value); + return sylvan::Mtbdd::terminal(sylvan_storm_rational_function_get_type(), helperStruct); + } template ValueType InternalAdd::getValue(MTBDD const& node) { diff --git a/src/storage/dd/sylvan/InternalSylvanAdd.h b/src/storage/dd/sylvan/InternalSylvanAdd.h index e02e0107e..4c4859332 100644 --- a/src/storage/dd/sylvan/InternalSylvanAdd.h +++ b/src/storage/dd/sylvan/InternalSylvanAdd.h @@ -13,6 +13,8 @@ #include "src/storage/expressions/Variable.h" +#include "src/adapters/CarlAdapter.h" + namespace storm { namespace storage { template @@ -655,6 +657,13 @@ namespace storm { * @return The sylvan node for the given value. */ static MTBDD getLeaf(uint_fast64_t value); + + /*! + * Retrieves the sylvan representation of the given storm::RatíonalFunction value. + * + * @return The sylvan node for the given value. + */ + static MTBDD getLeaf(storm::RationalFunction const& value); /*! * Retrieves the value of the given node (that must be a leaf). diff --git a/src/storage/dd/sylvan/InternalSylvanDdManager.h b/src/storage/dd/sylvan/InternalSylvanDdManager.h index 0618b0dbe..79182a1ae 100644 --- a/src/storage/dd/sylvan/InternalSylvanDdManager.h +++ b/src/storage/dd/sylvan/InternalSylvanDdManager.h @@ -9,6 +9,12 @@ #include "src/adapters/CarlAdapter.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