From 16e287ca8fe312ce9023dd8f9c7e2bc97183c16a Mon Sep 17 00:00:00 2001 From: PBerger Date: Mon, 18 Jul 2016 17:42:20 +0200 Subject: [PATCH] Fixes. Former-commit-id: 267bf081c4e2ed36a8a71bd09d43bfc44bf44e99 --- src/storage/dd/sylvan/InternalSylvanAdd.cpp | 7 +++++++ src/storage/dd/sylvan/InternalSylvanAdd.h | 9 +++++++++ src/storage/dd/sylvan/InternalSylvanDdManager.h | 6 ++++++ 3 files changed, 22 insertions(+) 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