Initial commit.

The basic Implementation compiles. No tests yet.


Former-commit-id: 60b6d0f892

resources/3rdparty/CMakeLists.txt

@@ -47,7 +47,7 @@ ExternalProject_Add(
     DOWNLOAD_COMMAND ""
     PREFIX "sylvan"
     SOURCE_DIR ${CMAKE_CURRENT_SOURCE_DIR}/sylvan
-    CMAKE_ARGS -DSYLVAN_BUILD_TEST=Off -DSYLVAN_BUILD_EXAMPLES=Off -DCMAKE_BUILD_TYPE=Release
+    CMAKE_ARGS -DSYLVAN_BUILD_TEST=Off -DSYLVAN_BUILD_EXAMPLES=On -DCMAKE_BUILD_TYPE=Release
     BINARY_DIR "${PROJECT_BINARY_DIR}/sylvan"
     INSTALL_COMMAND ""
     INSTALL_DIR "${PROJECT_BINARY_DIR}/sylvan"

resources/3rdparty/sylvan/CMakeLists.txt

@@ -5,6 +5,7 @@ enable_testing()
 set(CMAKE_C_FLAGS "-O3 -Wextra -Wall -Werror -fno-strict-aliasing -std=gnu11 -fPIC")
 set(CMAKE_CXX_FLAGS "-O3 -Wextra -Wall -Werror -fno-strict-aliasing -Wno-deprecated-register -std=gnu++11 -fPIC")
 
+option(USE_CARL "Sets whether carl should be included." ON)
 option(WITH_COVERAGE "Add generation of test coverage" OFF)
 if(WITH_COVERAGE)
     set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -O0 -g -coverage")
@@ -28,9 +29,26 @@ if(WITH_COVERAGE)
     )
 endif()
 
+if(USE_CARL)
+	find_package(carl QUIET REQUIRED)
+	if(carl_FOUND)
+               add_definitions(-DSYLVAN_HAVE_CARL)
+		include_directories("${carl_INCLUDE_DIR}")
+		list(APPEND STORM_LINK_LIBRARIES ${carl_LIBRARIES})
+		message(STATUS "Sylvan - using CARL.")
+	else()
+		message(FATAL_ERROR "Sylvan - CARL was requested but not found")
+	endif()
+else()
+	message(STATUS "Sylvan - not using CARL.")
+endif()
+
+
 set(CMAKE_MODULE_PATH ${PROJECT_SOURCE_DIR}/cmake)
 find_package(GMP REQUIRED)
 include_directories(${GMP_INCLUDE_DIR})
+include_directories("${PROJECT_SOURCE_DIR}/../../../")
+include_directories("${PROJECT_BINARY_DIR}/../include")
 include_directories(src)
 
 include_directories(src)

resources/3rdparty/sylvan/examples/CMakeLists.txt

@@ -12,6 +12,12 @@ target_link_libraries(lddmc sylvan)
 add_executable(simple simple.cpp)
 target_link_libraries(simple sylvan stdc++)
 
+if(USE_CARL)
+   message(STATUS "Sylvan - Example for Storm enabled.")
+   add_executable(storm-rf storm.cpp)
+   target_link_libraries(storm-rf sylvan stdc++ ${carl_LIBRARIES})
+endif(USE_CARL)
+
 include(CheckIncludeFiles)
 check_include_files("gperftools/profiler.h" HAVE_PROFILER)
 

resources/3rdparty/sylvan/examples/storm.cpp

@@ -0,0 +1,127 @@
+#ifdef NDEBUG
+#undef NDEBUG
+#endif
+
+#include <assert.h>
+#include <stdio.h>
+#include <stdint.h>
+
+#include <sylvan.h>
+#include <sylvan_obj.hpp>
+#include <storm_function_wrapper.h>
+#include <sylvan_storm_rational_function.h>
+
+using namespace sylvan;
+
+VOID_TASK_0(storm_rf)
+{
+    Bdd one = Bdd::bddOne(); // the True terminal
+    Bdd zero = Bdd::bddZero(); // the False terminal
+
+    // check if they really are the True/False terminal
+    assert(one.GetBDD() == sylvan_true);
+    assert(zero.GetBDD() == sylvan_false);
+
+    Bdd a = Bdd::bddVar(0); // create a BDD variable x_0
+    Bdd b = Bdd::bddVar(1); // create a BDD variable x_1
+
+    // check if a really is the Boolean formula "x_0"
+    assert(!a.isConstant());
+    assert(a.TopVar() == 0);
+    assert(a.Then() == one);
+    assert(a.Else() == zero);
+
+    // check if b really is the Boolean formula "x_1"
+    assert(!b.isConstant());
+    assert(b.TopVar() == 1);
+    assert(b.Then() == one);
+    assert(b.Else() == zero);
+
+    // compute !a
+    Bdd not_a = !a;
+
+    // check if !!a is really a
+    assert((!not_a) == a);
+
+    // compute a * b and !(!a + !b) and check if they are equivalent
+    Bdd a_and_b = a * b;
+    Bdd not_not_a_or_not_b = !(!a + !b);
+    assert(a_and_b == not_not_a_or_not_b);
+
+    // perform some simple quantification and check the results
+    Bdd ex = a_and_b.ExistAbstract(a); // \exists a . a * b
+    assert(ex == b);
+    Bdd andabs = a.AndAbstract(b, a); // \exists a . a * b using AndAbstract
+    assert(ex == andabs);
+    Bdd univ = a_and_b.UnivAbstract(a); // \forall a . a * b
+    assert(univ == zero);
+
+    // alternative method to get the cube "ab" using bddCube
+    BddSet variables = a * b;
+    std::vector<unsigned char> vec = {1, 1};
+    assert(a_and_b == Bdd::bddCube(variables, vec));
+
+    // test the bddCube method for all combinations
+    assert((!a * !b) == Bdd::bddCube(variables, std::vector<uint8_t>({0, 0})));
+    assert((!a * b)  == Bdd::bddCube(variables, std::vector<uint8_t>({0, 1})));
+    assert((!a)      == Bdd::bddCube(variables, std::vector<uint8_t>({0, 2})));
+    assert((a * !b)  == Bdd::bddCube(variables, std::vector<uint8_t>({1, 0})));
+    assert((a * b)   == Bdd::bddCube(variables, std::vector<uint8_t>({1, 1})));
+    assert((a)       == Bdd::bddCube(variables, std::vector<uint8_t>({1, 2})));
+    assert((!b)      == Bdd::bddCube(variables, std::vector<uint8_t>({2, 0})));
+    assert((b)       == Bdd::bddCube(variables, std::vector<uint8_t>({2, 1})));
+    assert(one       == Bdd::bddCube(variables, std::vector<uint8_t>({2, 2})));
+}
+
+VOID_TASK_1(_main, void*, arg)
+{
+    // Initialize Sylvan
+    // With starting size of the nodes table 1 << 21, and maximum size 1 << 27.
+    // With starting size of the cache table 1 << 20, and maximum size 1 << 20.
+    // Memory usage: 24 bytes per node, and 36 bytes per cache bucket
+    // - 1<<24 nodes: 384 MB
+    // - 1<<25 nodes: 768 MB
+    // - 1<<26 nodes: 1536 MB
+    // - 1<<27 nodes: 3072 MB
+    // - 1<<24 cache: 576 MB
+    // - 1<<25 cache: 1152 MB
+    // - 1<<26 cache: 2304 MB
+    // - 1<<27 cache: 4608 MB
+    sylvan_init_package(1LL<<22, 1LL<<26, 1LL<<22, 1LL<<26);
+
+    // Initialize the BDD module with granularity 1 (cache every operation)
+    // A higher granularity (e.g. 6) often results in better performance in practice
+    sylvan_init_bdd(1);
+
+    // Now we can do some simple stuff using the C++ objects.
+    CALL(storm_rf);
+
+    // Report statistics (if SYLVAN_STATS is 1 in the configuration)
+    sylvan_stats_report(stdout, 1);
+
+    // And quit, freeing memory
+    sylvan_quit();
+
+    // We didn't use arg
+    (void)arg;
+}
+
+int
+main (int argc, char *argv[])
+{
+    int n_workers = 0; // automatically detect number of workers
+    size_t deque_size = 0; // default value for the size of task deques for the workers
+    size_t program_stack_size = 0; // default value for the program stack of each pthread
+
+    // Initialize the Lace framework for <n_workers> workers.
+    lace_init(n_workers, deque_size);
+
+    // Spawn and start all worker pthreads; suspends current thread until done.
+    lace_startup(program_stack_size, TASK(_main), NULL);
+
+    // The lace_startup command also exits Lace after _main is completed.
+
+    return 0;
+    (void)argc; // unused variable
+    (void)argv; // unused variable
+}

resources/3rdparty/sylvan/src/CMakeLists.txt

@@ -13,6 +13,8 @@ add_library(sylvan
     sha2.c
     stats.h
     stats.c
+    storm_function_wrapper.h
+    storm_function_wrapper.cpp
     sylvan.h
     sylvan_bdd.h
     sylvan_bdd.c
@@ -30,6 +32,8 @@ add_library(sylvan
     sylvan_mtbdd_int.h
     sylvan_obj.hpp
     sylvan_obj.cpp
+    sylvan_storm_rational_function.h
+    sylvan_storm_rational_function.c
     tls.h
 )
 
@@ -42,6 +46,11 @@ set_target_properties(sylvan PROPERTIES
 
 target_link_libraries(sylvan m pthread)
 
+if(USE_CARL)
+   message(STATUS "Sylvan - linking CARL.")
+   target_link_libraries(sylvan ${carl_LIBRARIES})
+endif(USE_CARL)
+
 if(UNIX AND NOT APPLE)
     target_link_libraries(sylvan rt)
 endif()

resources/3rdparty/sylvan/src/storm_function_wrapper.cpp

@@ -0,0 +1,116 @@
+#include "storm_function_wrapper.h"
+
+#include <cstring>
+#include "src/adapters/CarlAdapter.h"
+
+void storm_rational_function_init(storm_rational_function_ptr* a) {
+	storm_rational_function_ptr srf_ptr = static_cast<storm_rational_function_ptr>(malloc(sizeof(storm_rational_function_ptr_struct)));
+	
+	if (srf_ptr == nullptr) {
+		return;
+	}
+	
+	srf_ptr->storm_rational_function = new storm::RationalFunction(*(storm::RationalFunction*)((*a)->storm_rational_function));
+
+	*a = srf_ptr;
+}
+
+void storm_rational_function_destroy(storm_rational_function_ptr a) {
+	delete (storm::RationalFunction*)a->storm_rational_function;
+	a->storm_rational_function = nullptr;
+	free((void*)a);
+}
+
+int storm_rational_function_equals(storm_rational_function_ptr a, storm_rational_function_ptr b) {
+	storm::RationalFunction* srf_a = (storm::RationalFunction*)a->storm_rational_function;
+	storm::RationalFunction* srf_b = (storm::RationalFunction*)b->storm_rational_function;
+
+	if (*srf_a == *srf_b) {
+		return 0;
+	}
+
+	return -1;
+}
+
+storm_rational_function_ptr storm_rational_function_plus(storm_rational_function_ptr a, storm_rational_function_ptr b) {
+	storm::RationalFunction& srf_a = *(storm::RationalFunction*)a->storm_rational_function;
+	storm::RationalFunction& srf_b = *(storm::RationalFunction*)b->storm_rational_function;
+
+	storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a);
+	*result_srf += srf_b;
+
+	storm_rational_function_ptr result = (storm_rational_function_ptr)malloc(sizeof(storm_rational_function_ptr_struct));
+	result->storm_rational_function = (void*)result_srf;
+
+	return result;
+}
+
+storm_rational_function_ptr storm_rational_function_minus(storm_rational_function_ptr a, storm_rational_function_ptr b) {
+	storm::RationalFunction& srf_a = *(storm::RationalFunction*)a->storm_rational_function;
+	storm::RationalFunction& srf_b = *(storm::RationalFunction*)b->storm_rational_function;
+
+	storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a);
+	*result_srf -= srf_b;
+
+	storm_rational_function_ptr result = (storm_rational_function_ptr)malloc(sizeof(storm_rational_function_ptr_struct));
+	result->storm_rational_function = (void*)result_srf;
+
+	return result;
+}
+
+storm_rational_function_ptr storm_rational_function_times(storm_rational_function_ptr a, storm_rational_function_ptr b) {
+	storm::RationalFunction& srf_a = *(storm::RationalFunction*)a->storm_rational_function;
+	storm::RationalFunction& srf_b = *(storm::RationalFunction*)b->storm_rational_function;
+
+	storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a);
+	*result_srf *= srf_b;
+
+	storm_rational_function_ptr result = (storm_rational_function_ptr)malloc(sizeof(storm_rational_function_ptr_struct));
+	result->storm_rational_function = (void*)result_srf;
+
+	return result;
+}
+
+storm_rational_function_ptr storm_rational_function_divide(storm_rational_function_ptr a, storm_rational_function_ptr b) {
+	storm::RationalFunction& srf_a = *(storm::RationalFunction*)a->storm_rational_function;
+	storm::RationalFunction& srf_b = *(storm::RationalFunction*)b->storm_rational_function;
+
+	storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a);
+	*result_srf /= srf_b;
+
+	storm_rational_function_ptr result = (storm_rational_function_ptr)malloc(sizeof(storm_rational_function_ptr_struct));
+	result->storm_rational_function = (void*)result_srf;
+
+	return result;
+}
+
+uint64_t storm_rational_function_hash(storm_rational_function_ptr const a, uint64_t const seed) {
+	storm::RationalFunction& srf_a = *(storm::RationalFunction*)a->storm_rational_function;
+
+	size_t hash = carl::hash_value(srf_a);
+	uint64_t result = hash ^ seed;
+
+	return result;
+}
+
+storm_rational_function_ptr storm_rational_function_negate(storm_rational_function_ptr a) {
+	storm::RationalFunction& srf_a = *(storm::RationalFunction*)a->storm_rational_function;
+
+	storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a);
+	*result_srf = -srf_a;
+
+	storm_rational_function_ptr result = (storm_rational_function_ptr)malloc(sizeof(storm_rational_function_ptr_struct));
+	result->storm_rational_function = (void*)result_srf;
+
+	return result;
+}
+
+int storm_rational_function_is_zero(storm_rational_function_ptr a) {
+	storm::RationalFunction& srf_a = *(storm::RationalFunction*)a->storm_rational_function;
+
+	if (srf_a.isZero()) {
+		return 1;
+	} else {
+		return 0;
+	}
+}

resources/3rdparty/sylvan/src/storm_function_wrapper.h

@@ -0,0 +1,33 @@
+#ifndef SYLVAN_STORM_FUNCTION_WRAPPER_H
+#define SYLVAN_STORM_FUNCTION_WRAPPER_H
+
+#include <stdint.h>
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+typedef struct {
+	void* storm_rational_function;
+} storm_rational_function_ptr_struct;
+typedef storm_rational_function_ptr_struct storm_rational_function_t[1];
+typedef storm_rational_function_ptr_struct* storm_rational_function_ptr;
+
+
+// equals, plus, minus, divide, times, create, destroy
+void storm_rational_function_init(storm_rational_function_ptr* a);
+void storm_rational_function_destroy(storm_rational_function_ptr a);
+int storm_rational_function_equals(storm_rational_function_ptr a, storm_rational_function_ptr b);
+storm_rational_function_ptr storm_rational_function_plus(storm_rational_function_ptr a, storm_rational_function_ptr b);
+storm_rational_function_ptr storm_rational_function_minus(storm_rational_function_ptr a, storm_rational_function_ptr b);
+storm_rational_function_ptr storm_rational_function_times(storm_rational_function_ptr a, storm_rational_function_ptr b);
+storm_rational_function_ptr storm_rational_function_divide(storm_rational_function_ptr a, storm_rational_function_ptr b);
+storm_rational_function_ptr storm_rational_function_negate(storm_rational_function_ptr a);
+uint64_t storm_rational_function_hash(storm_rational_function_ptr const a, uint64_t const seed);
+int storm_rational_function_is_zero(storm_rational_function_ptr a);
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif // SYLVAN_STORM_FUNCTION_WRAPPER_H

resources/3rdparty/sylvan/src/sylvan_storm_rational_function.c

@@ -0,0 +1,240 @@
+#include <sylvan_config.h>
+
+#include <assert.h>
+#include <inttypes.h>
+#include <math.h>
+#include <stdint.h>
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+
+#include <sylvan.h>
+#include <sylvan_common.h>
+/*#include <sylvan_mtbdd_int.h>*/
+#include <sylvan_storm_rational_function.h>
+
+#include <storm_function_wrapper.h>
+
+/**
+ * helper function for hash
+ */
+#ifndef rotl64
+static inline uint64_t
+rotl64(uint64_t x, int8_t r)
+{
+    return ((x<<r) | (x>>(64-r)));
+}
+#endif
+
+static uint64_t
+sylvan_storm_rational_function_hash(const uint64_t v, const uint64_t seed)
+{
+    /* Hash the storm::RationalFunction in pointer v */
+    
+	storm_rational_function_ptr x = (storm_rational_function_ptr)(size_t)v;
+
+	return storm_rational_function_hash(x, seed);
+}
+
+static int
+sylvan_storm_rational_function_equals(const uint64_t left, const uint64_t right)
+{
+    /* This function is called by the unique table when comparing a new
+       leaf with an existing leaf */
+	storm_rational_function_ptr a = (storm_rational_function_ptr)(size_t)left;
+	storm_rational_function_ptr b = (storm_rational_function_ptr)(size_t)right;
+
+    /* Just compare x and y */
+    return (storm_rational_function_equals(a, b) == 0) ? 1 : 0;
+}
+
+static void
+sylvan_storm_rational_function_create(uint64_t *val)
+{
+    /* This function is called by the unique table when a leaf does not yet exist.
+       We make a copy, which will be stored in the hash table. */
+	storm_rational_function_ptr* x = (storm_rational_function_ptr*)(size_t)val;
+	storm_rational_function_init(x);
+}
+
+static void
+sylvan_storm_rational_function_destroy(uint64_t val)
+{
+    /* This function is called by the unique table
+       when a leaf is removed during garbage collection. */
+	storm_rational_function_ptr x = (storm_rational_function_ptr)(size_t)val;
+	storm_rational_function_destroy(x);
+}
+
+static uint32_t sylvan_storm_rational_function_type;
+static uint64_t CACHE_STORM_RATIONAL_FUNCTION_AND_EXISTS;
+
+/**
+ * Initialize storm::RationalFunction custom leaves
+ */
+void
+sylvan_storm_rational_function_init()
+{
+    /* Register custom leaf 3 */
+    sylvan_storm_rational_function_type = mtbdd_register_custom_leaf(sylvan_storm_rational_function_hash, sylvan_storm_rational_function_equals, sylvan_storm_rational_function_create, sylvan_storm_rational_function_destroy);
+	CACHE_STORM_RATIONAL_FUNCTION_AND_EXISTS = cache_next_opid();
+}
+
+/**
+ * Create storm::RationalFunction leaf
+ */
+MTBDD
+mtbdd_storm_rational_function(storm_rational_function_t val)
+{
+    return mtbdd_makeleaf(sylvan_storm_rational_function_type, (size_t)val);
+}
+
+/**
+ * Operation "plus" for two storm::RationalFunction MTBDDs
+ * Interpret partial function as "0"
+ */
+TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_plus, MTBDD*, pa, MTBDD*, pb)
+{
+    MTBDD a = *pa, b = *pb;
+
+    /* Check for partial functions */
+    if (a == mtbdd_false) return b;
+    if (b == mtbdd_false) return a;
+
+    /* If both leaves, compute plus */
+    if (mtbdd_isleaf(a) && mtbdd_isleaf(b)) {
+		storm_rational_function_ptr ma = (storm_rational_function_ptr)mtbdd_getvalue(a);
+		storm_rational_function_ptr mb = (storm_rational_function_ptr)mtbdd_getvalue(b);
+
+		storm_rational_function_ptr mres = storm_rational_function_plus(ma, mb);
+        MTBDD res = mtbdd_storm_rational_function(mres);
+        
+		// TODO: Delete mres?
+
+        return res;
+    }
+
+    /* Commutative, so swap a,b for better cache performance */
+    if (a < b) {
+        *pa = b;
+        *pb = a;
+    }
+
+    return mtbdd_invalid;
+}
+
+/**
+ * Operation "minus" for two storm::RationalFunction MTBDDs
+ * Interpret partial function as "0"
+ */
+TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_minus, MTBDD*, pa, MTBDD*, pb)
+{
+    MTBDD a = *pa, b = *pb;
+
+    /* Check for partial functions */
+    if (a == mtbdd_false) return sylvan_storm_rational_function_neg(b);
+    if (b == mtbdd_false) return a;
+
+    /* If both leaves, compute plus */
+    if (mtbdd_isleaf(a) && mtbdd_isleaf(b)) {
+		storm_rational_function_ptr ma = (storm_rational_function_ptr)mtbdd_getvalue(a);
+		storm_rational_function_ptr mb = (storm_rational_function_ptr)mtbdd_getvalue(b);
+
+		storm_rational_function_ptr mres = storm_rational_function_minus(ma, mb);
+		MTBDD res = mtbdd_storm_rational_function(mres);
+
+		// TODO: Delete mres?
+
+        return res;
+    }
+
+    return mtbdd_invalid;
+}
+
+/**
+ * Operation "times" for two storm::RationalFunction MTBDDs.
+ * One of the parameters can be a BDD, then it is interpreted as a filter.
+ * For partial functions, domain is intersection
+ */
+TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_times, MTBDD*, pa, MTBDD*, pb)
+{
+    MTBDD a = *pa, b = *pb;
+
+    /* Check for partial functions and for Boolean (filter) */
+    if (a == mtbdd_false || b == mtbdd_false) return mtbdd_false;
+
+    /* If one of Boolean, interpret as filter */
+    if (a == mtbdd_true) return b;
+    if (b == mtbdd_true) return a;
+
+    /* Handle multiplication of leaves */
+    if (mtbdd_isleaf(a) && mtbdd_isleaf(b)) {
+		storm_rational_function_ptr ma = (storm_rational_function_ptr)mtbdd_getvalue(a);
+		storm_rational_function_ptr mb = (storm_rational_function_ptr)mtbdd_getvalue(b);
+
+		storm_rational_function_ptr mres = storm_rational_function_times(ma, mb);
+		MTBDD res = mtbdd_storm_rational_function(mres);
+
+		// TODO: Delete mres?
+
+        return res;
+    }
+
+    /* Commutative, so make "a" the lowest for better cache performance */
+    if (a < b) {
+        *pa = b;
+        *pb = a;
+    }
+
+    return mtbdd_invalid;
+}
+
+/**
+ * Operation "divide" for two storm::RationalFunction MTBDDs.
+ * For partial functions, domain is intersection
+ */
+TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_divide, MTBDD*, pa, MTBDD*, pb)
+{
+    MTBDD a = *pa, b = *pb;
+
+    /* Check for partial functions */
+    if (a == mtbdd_false || b == mtbdd_false) return mtbdd_false;
+
+    /* Handle division of leaves */
+    if (mtbdd_isleaf(a) && mtbdd_isleaf(b)) {
+		storm_rational_function_ptr ma = (storm_rational_function_ptr)mtbdd_getvalue(a);
+		storm_rational_function_ptr mb = (storm_rational_function_ptr)mtbdd_getvalue(b);
+
+		storm_rational_function_ptr mres = storm_rational_function_divide(ma, mb);
+		MTBDD res = mtbdd_storm_rational_function(mres);
+
+		// TODO: Delete mres?
+
+        return res;
+    }
+
+    return mtbdd_invalid;
+}
+
+/**
+ * Operation "neg" for one storm::RationalFunction MTBDD
+ */
+TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_neg, MTBDD, dd, size_t, p)
+{
+    /* Handle partial functions */
+    if (dd == mtbdd_false) return mtbdd_false;
+
+    /* Compute result for leaf */
+    if (mtbdd_isleaf(dd)) {
+		storm_rational_function_ptr mdd = (storm_rational_function_ptr)mtbdd_getvalue(dd);
+
+		storm_rational_function_ptr mres = storm_rational_function_negate(mdd);
+		MTBDD res = mtbdd_storm_rational_function(mres);
+
+		// TODO: Delete mres?
+        return res;
+    }
+
+    return mtbdd_invalid;
+    (void)p;
+}

resources/3rdparty/sylvan/src/sylvan_storm_rational_function.h

@@ -0,0 +1,87 @@
+/**
+ * This is an implementation of storm::RationalFunction custom leaves of MTBDDs
+ */
+
+#ifndef SYLVAN_STORM_RATIONAL_FUNCTION_H
+#define SYLVAN_STORM_RATIONAL_FUNCTION_H
+
+#include <sylvan.h>
+#include <storm_function_wrapper.h>
+
+#define SYLVAN_HAVE_CARL 1
+
+#ifdef SYLVAN_HAVE_CARL
+
+#ifdef __cplusplus
+extern "C" {
+#endif /* __cplusplus */
+
+/**
+ * Initialize storm::RationalFunction custom leaves
+ */
+void sylvan_storm_rational_function_init();
+
+/**
+ * Create storm::RationalFunction leaf
+ */
+MTBDD mtbdd_storm_rational_function(storm_rational_function_t val);
+
+/**
+ * Operation "plus" for two storm::RationalFunction MTBDDs
+ */
+TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_plus, MTBDD*, MTBDD*);
+TASK_DECL_3(MTBDD, sylvan_storm_rational_function_abstract_op_plus, MTBDD, MTBDD, int);
+
+/**
+ * Operation "minus" for two storm::RationalFunction MTBDDs
+ */
+TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_minus, MTBDD*, MTBDD*);
+
+/**
+ * Operation "times" for two storm::RationalFunction MTBDDs
+ */
+TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_times, MTBDD*, MTBDD*);
+TASK_DECL_3(MTBDD, sylvan_storm_rational_function_abstract_op_times, MTBDD, MTBDD, int);
+
+/**
+ * Operation "divide" for two storm::RationalFunction MTBDDs
+ */
+TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_divide, MTBDD*, MTBDD*);
+
+/**
+ * Operation "negate" for one storm::RationalFunction MTBDD
+ */
+TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_neg, MTBDD, size_t);
+
+/**
+ * Compute a + b
+ */
+#define sylvan_storm_rational_function_plus(a, b) mtbdd_apply(a, b, TASK(sylvan_storm_rational_function_op_plus))
+
+/**
+ * Compute a - b
+ */
+#define sylvan_storm_rational_function_minus(a, b) mtbdd_apply(a, b, TASK(sylvan_storm_rational_function_op_minus))
+
+/**
+ * Compute a * b
+ */
+#define sylvan_storm_rational_function_times(a, b) mtbdd_apply(a, b, TASK(sylvan_storm_rational_function_op_times))
+
+/**
+ * Compute a / b
+ */
+#define sylvan_storm_rational_function_divide(a, b) mtbdd_apply(a, b, TASK(sylvan_storm_rational_function_op_divide))
+
+/**
+ * Compute -a
+ */
+#define sylvan_storm_rational_function_neg(a) mtbdd_uapply(a, TASK(sylvan_storm_rational_function_op_neg), 0);
+
+#ifdef __cplusplus
+}
+#endif /* __cplusplus */
+
+#endif // SYLVAN_HAVE_CARL
+
+#endif // SYLVAN_STORM_RATIONAL_FUNCTION_H