Fixed Sylvan bugs.

Added a lot of debugging options and output, controlled by #define's.
Added more template specializations for storm::RationalFunction.


Former-commit-id: 416c32d196

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

@@ -1,132 +1,192 @@
-#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;
-	}
-}
-
-storm_rational_function_ptr storm_rational_function_get_zero() {
-	static storm::RationalFunction zeroFunction(0);
-	static storm_rational_function_ptr_struct functionStruct;
-	functionStruct.storm_rational_function = (void*)&zeroFunction;
-	
-	return &functionStruct;
-}
-
-storm_rational_function_ptr storm_rational_function_get_one() {
-	static storm::RationalFunction oneFunction(1);
-	static storm_rational_function_ptr_struct functionStruct;
-	functionStruct.storm_rational_function = (void*)&oneFunction;
-	
-	return &functionStruct;
-}
+#include "storm_function_wrapper.h"
+
+#include <cstring>
+#include <iostream>
+#include <sstream>
+#include "src/adapters/CarlAdapter.h"
+
+#undef DEBUG_STORM_FUNCTION_WRAPPER
+
+#ifdef DEBUG_STORM_FUNCTION_WRAPPER
+#define LOG_I(funcName) std::cout << "Entering function " << funcName << std::endl;
+#define LOG_O(funcName) std::cout << "Leaving function " << funcName << std::endl;
+#else
+#define LOG_I(funcName)
+#define LOG_O(funcName)
+#endif
+
+void storm_rational_function_init(storm_rational_function_ptr* a) {
+	LOG_I("init")
+	storm_rational_function_ptr srf_ptr = new storm::RationalFunction(*((storm::RationalFunction*)(*a)));
+	
+	if (srf_ptr == nullptr) {
+		std::cerr << "Could not allocate memory in storm_rational_function_init()!" << std::endl;
+		return;
+	}
+
+	*a = srf_ptr;
+	LOG_O("init")
+}
+
+void storm_rational_function_destroy(storm_rational_function_ptr a) {
+	LOG_I("destroy")
+	delete (storm::RationalFunction*)a;
+	LOG_O("destroy")
+}
+
+int storm_rational_function_equals(storm_rational_function_ptr a, storm_rational_function_ptr b) {
+	LOG_I("equals")
+	storm::RationalFunction& srf_a = *(storm::RationalFunction*)a;
+	storm::RationalFunction& srf_b = *(storm::RationalFunction*)b;
+	
+	LOG_O("equals")
+	
+	int result = 0;
+	if (srf_a == srf_b) {
+		result = 1;
+	}
+	return result;
+}
+
+storm_rational_function_ptr storm_rational_function_plus(storm_rational_function_ptr a, storm_rational_function_ptr b) {
+	LOG_I("plus")
+	storm::RationalFunction& srf_a = *(storm::RationalFunction*)a;
+	storm::RationalFunction& srf_b = *(storm::RationalFunction*)b;
+
+	storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a);
+	if (result_srf == nullptr) {
+		std::cerr << "Could not allocate memory in storm_rational_function_plus()!" << std::endl;
+		return (storm_rational_function_ptr)nullptr;
+	}
+	
+	*result_srf += srf_b;
+
+	storm_rational_function_ptr result = (storm_rational_function_ptr)result_srf;
+
+	LOG_O("plus")
+	return result;
+}
+
+storm_rational_function_ptr storm_rational_function_minus(storm_rational_function_ptr a, storm_rational_function_ptr b) {
+	LOG_I("minus")
+	storm::RationalFunction& srf_a = *(storm::RationalFunction*)a;
+	storm::RationalFunction& srf_b = *(storm::RationalFunction*)b;
+
+	storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a);
+	if (result_srf == nullptr) {
+		std::cerr << "Could not allocate memory in storm_rational_function_minus()!" << std::endl;
+		return (storm_rational_function_ptr)nullptr;
+	}
+	
+	*result_srf -= srf_b;
+
+	storm_rational_function_ptr result = (storm_rational_function_ptr)result_srf;
+
+	LOG_O("minus")
+	return result;
+}
+
+storm_rational_function_ptr storm_rational_function_times(storm_rational_function_ptr a, storm_rational_function_ptr b) {
+	LOG_I("times")
+	storm::RationalFunction& srf_a = *(storm::RationalFunction*)a;
+	storm::RationalFunction& srf_b = *(storm::RationalFunction*)b;
+
+	storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a);
+	if (result_srf == nullptr) {
+		std::cerr << "Could not allocate memory in storm_rational_function_times()!" << std::endl;
+		return (storm_rational_function_ptr)nullptr;
+	}
+	
+	*result_srf *= srf_b;
+
+	storm_rational_function_ptr result = (storm_rational_function_ptr)result_srf;
+
+	LOG_O("times")
+	return result;
+}
+
+storm_rational_function_ptr storm_rational_function_divide(storm_rational_function_ptr a, storm_rational_function_ptr b) {
+	LOG_I("divide")
+	storm::RationalFunction& srf_a = *(storm::RationalFunction*)a;
+	storm::RationalFunction& srf_b = *(storm::RationalFunction*)b;
+
+	storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a);
+	if (result_srf == nullptr) {
+		std::cerr << "Could not allocate memory in storm_rational_function_divide()!" << std::endl;
+		return (storm_rational_function_ptr)nullptr;
+	}
+	
+	*result_srf /= srf_b;
+
+	storm_rational_function_ptr result = (storm_rational_function_ptr)result_srf;
+
+	LOG_O("divide")
+	return result;
+}
+
+uint64_t storm_rational_function_hash(storm_rational_function_ptr const a, uint64_t const seed) {
+	LOG_I("hash")
+	storm::RationalFunction& srf_a = *(storm::RationalFunction*)a;
+
+	size_t hash = carl::hash_value(srf_a);
+	uint64_t result = hash ^ seed;
+
+	LOG_O("hash")
+	return result;
+}
+
+storm_rational_function_ptr storm_rational_function_negate(storm_rational_function_ptr a) {
+	LOG_I("negate")
+	storm::RationalFunction& srf_a = *(storm::RationalFunction*)a;
+
+	storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a);
+	if (result_srf == nullptr) {
+		std::cerr << "Could not allocate memory in storm_rational_function_negate()!" << std::endl;
+		return (storm_rational_function_ptr)nullptr;
+	}
+	
+	*result_srf = -srf_a;
+
+	storm_rational_function_ptr result = (storm_rational_function_ptr)result_srf;
+
+	LOG_O("negate")
+	return result;
+}
+
+int storm_rational_function_is_zero(storm_rational_function_ptr a) {
+	LOG_I("isZero")
+	storm::RationalFunction& srf_a = *(storm::RationalFunction*)a;
+
+	if (srf_a.isZero()) {
+		return 1;
+	} else {
+		return 0;
+	}
+}
+
+storm_rational_function_ptr storm_rational_function_get_zero() {
+	static storm::RationalFunction zeroFunction(0);
+	LOG_I("getZero")
+	//return new storm::RationalFunction(0);
+	return (storm_rational_function_ptr)(&zeroFunction);
+}
+
+storm_rational_function_ptr storm_rational_function_get_one() {
+	static storm::RationalFunction oneFunction(1);
+	LOG_I("getOne")
+	//return new storm::RationalFunction(1);
+	return (storm_rational_function_ptr)(&oneFunction);
+}
+
+void print_storm_rational_function(storm_rational_function_ptr a) {
+	storm::RationalFunction& srf_a = *(storm::RationalFunction*)a;
+	std::cout << srf_a << std::flush;
+}
+
+void print_storm_rational_function_to_file(storm_rational_function_ptr a, FILE* out) {
+	std::stringstream ss;
+	storm::RationalFunction& srf_a = *(storm::RationalFunction*)a;
+	ss << srf_a;
+	std::string s = ss.str();
+	fprintf(out, "%s", s.c_str());
+}

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

@@ -2,17 +2,13 @@
 #define SYLVAN_STORM_FUNCTION_WRAPPER_H
 
 #include <stdint.h>
+#include <stdio.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;
-
+typedef void* storm_rational_function_ptr;
 
 // equals, plus, minus, divide, times, create, destroy
 void storm_rational_function_init(storm_rational_function_ptr* a);
@@ -29,8 +25,13 @@ int storm_rational_function_is_zero(storm_rational_function_ptr a);
 storm_rational_function_ptr storm_rational_function_get_zero();
 storm_rational_function_ptr storm_rational_function_get_one();
 
+void print_storm_rational_function(storm_rational_function_ptr a);
+void print_storm_rational_function_to_file(storm_rational_function_ptr a, FILE* out);
+
+int storm_rational_function_is_zero(storm_rational_function_ptr a);
+
 #ifdef __cplusplus
 }
 #endif
 
-#endif // SYLVAN_STORM_FUNCTION_WRAPPER_H
+#endif // SYLVAN_STORM_FUNCTION_WRAPPER_H

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

@@ -31,6 +31,11 @@
 #include <sylvan_common.h>
 #include <sylvan_mtbdd_int.h>
 
+#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL)
+#include <sylvan_storm_rational_function.h>
+#include <storm_function_wrapper.h>
+#endif
+
 /* Primitives */
 int
 mtbdd_isleaf(MTBDD bdd)
@@ -264,9 +269,15 @@ _mtbdd_create_cb(uint64_t *a, uint64_t *b)
     // for leaf
     if ((*a & 0x4000000000000000) == 0) return; // huh?
     uint32_t type = *a & 0xffffffff;
-    if (type >= cl_registry_count) return; // not in registry
+    if (type >= cl_registry_count) { // not in registry
+		printf("ERROR: type >= cl_registry_count!");
+		return;
+	}
     customleaf_t *c = cl_registry + type;
-    if (c->create_cb == NULL) return; // not in registry
+    if (c->create_cb == NULL) { // not in registry
+		printf("ERROR: create_cb is NULL!");
+		return;
+	}
     c->create_cb(b);
 }
 
@@ -276,9 +287,15 @@ _mtbdd_destroy_cb(uint64_t a, uint64_t b)
     // for leaf
     if ((a & 0x4000000000000000) == 0) return; // huh?
     uint32_t type = a & 0xffffffff;
-    if (type >= cl_registry_count) return; // not in registry
+    if (type >= cl_registry_count) { // not in registry
+		printf("ERROR: type >= cl_registry_count! (2)");
+		return;
+	}
     customleaf_t *c = cl_registry + type;
-    if (c->destroy_cb == NULL) return; // not in registry
+    if (c->destroy_cb == NULL) { // not in registry
+		printf("ERROR: destroy_cb is NULL!");
+		return;
+	}
     c->destroy_cb(b);
 }
 
@@ -833,6 +850,11 @@ TASK_2(MTBDD, mtbdd_uop_times_uint, MTBDD, a, size_t, k)
             uint32_t c = gcd(d, (uint32_t)k);
             return mtbdd_fraction(n*(k/c), d/c);
         }
+#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL)
+		else if (mtbddnode_gettype(na) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID) {
+			printf("ERROR mtbdd_uop_times_uint type SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID");
+		}
+#endif
     }
 
     return mtbdd_invalid;
@@ -857,6 +879,11 @@ TASK_2(MTBDD, mtbdd_uop_pow_uint, MTBDD, a, size_t, k)
             uint64_t v = mtbddnode_getvalue(na);
             return mtbdd_fraction(pow((int32_t)(v>>32), k), (uint32_t)v);
         }
+#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL)
+		else if (mtbddnode_gettype(na) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID) {
+			printf("ERROR mtbdd_uop_pow_uint type SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID");
+		}
+#endif
     }
 
     return mtbdd_invalid;
@@ -1017,6 +1044,11 @@ TASK_IMPL_2(MTBDD, mtbdd_op_plus, MTBDD*, pa, MTBDD*, pb)
             // add
             return mtbdd_fraction(nom_a + nom_b, denom_a);
         }
+#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL)
+		else if (mtbddnode_gettype(na) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID && mtbddnode_gettype(nb) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID) {
+			printf("ERROR mtbdd_op_plus type SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID");
+		}
+#endif
     }
 
     if (a < b) {
@@ -1066,6 +1098,11 @@ TASK_IMPL_2(MTBDD, mtbdd_op_minus, MTBDD*, pa, MTBDD*, pb)
             // subtract
             return mtbdd_fraction(nom_a - nom_b, denom_a);
         }
+#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL)
+		else if ((mtbddnode_gettype(na) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID) && (mtbddnode_gettype(nb) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID)) {
+			printf("ERROR: mtbdd_op_minus type SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID.\n");
+		}
+#endif
     }
 
     return mtbdd_invalid;
@@ -1113,6 +1150,11 @@ TASK_IMPL_2(MTBDD, mtbdd_op_times, MTBDD*, pa, MTBDD*, pb)
             denom_a *= (denom_b/d);
             return mtbdd_fraction(nom_a, denom_a);
         }
+#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL)
+		else if ((mtbddnode_gettype(na) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID) && (mtbddnode_gettype(nb) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID)) {
+			printf("ERROR: mtbdd_op_times type SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID.\n");
+		}
+#endif
     }
 
     if (a < b) {
@@ -1169,6 +1211,11 @@ TASK_IMPL_2(MTBDD, mtbdd_op_min, MTBDD*, pa, MTBDD*, pb)
             // compute lowest
             return nom_a < nom_b ? a : b;
         }
+#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL)
+		else if ((mtbddnode_gettype(na) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID) && (mtbddnode_gettype(nb) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID)) {
+			printf("ERROR: mtbdd_op_min type SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID.\n");
+		}
+#endif
     }
 
     if (a < b) {
@@ -1223,6 +1270,11 @@ TASK_IMPL_2(MTBDD, mtbdd_op_max, MTBDD*, pa, MTBDD*, pb)
             // compute highest
             return nom_a > nom_b ? a : b;
         }
+#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL)
+		else if ((mtbddnode_gettype(na) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID) && (mtbddnode_gettype(nb) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID)) {
+			printf("ERROR: mtbdd_op_max type SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID.\n");
+		}
+#endif
     }
 
     if (a < b) {
@@ -1252,6 +1304,11 @@ TASK_IMPL_2(MTBDD, mtbdd_op_negate, MTBDD, a, size_t, k)
             uint64_t v = mtbddnode_getvalue(na);
             return mtbdd_fraction(-(int32_t)(v>>32), (uint32_t)v);
         }
+#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL)
+		else if ((mtbddnode_gettype(na) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID)) {
+			printf("ERROR: mtbdd_op_negate type SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID.\n");
+		}
+#endif
     }
 
     return mtbdd_invalid;
@@ -1335,6 +1392,11 @@ TASK_IMPL_2(MTBDD, mtbdd_op_threshold_double, MTBDD, a, size_t, svalue)
             d /= mtbdd_getdenom(a);
             return d >= value ? mtbdd_true : mtbdd_false;
         }
+#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL)
+		else if ((mtbddnode_gettype(na) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID)) {
+			printf("ERROR: mtbdd_op_threshold_double type SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID.\n");
+		}
+#endif
     }
 
     return mtbdd_invalid;
@@ -1361,6 +1423,11 @@ TASK_IMPL_2(MTBDD, mtbdd_op_strict_threshold_double, MTBDD, a, size_t, svalue)
             d /= mtbdd_getdenom(a);
             return d > value ? mtbdd_true : mtbdd_false;
         }
+#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL)
+		else if ((mtbddnode_gettype(na) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID)) {
+			printf("ERROR: mtbdd_op_strict_threshold_double type SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID.\n");
+		}
+#endif
     }
 
     return mtbdd_invalid;
@@ -1566,6 +1633,11 @@ TASK_3(MTBDD, mtbdd_leq_rec, MTBDD, a, MTBDD, b, int*, shortcircuit)
             nom_b *= da/c;
             result = nom_a <= nom_b ? mtbdd_true : mtbdd_false;
         }
+#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL)
+		else if (mtbddnode_gettype(na) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID && mtbddnode_gettype(nb) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID) {
+            printf("ERROR: mtbdd_leq_rec type SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID\n");
+        }
+#endif
     } else {
         /* Get top variable */
         uint32_t va = la ? 0xffffffff : mtbddnode_getvariable(na);
@@ -1651,6 +1723,11 @@ TASK_3(MTBDD, mtbdd_less_rec, MTBDD, a, MTBDD, b, int*, shortcircuit)
             nom_b *= da/c;
             result = nom_a < nom_b ? mtbdd_true : mtbdd_false;
         }
+#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL)
+		else if (mtbddnode_gettype(na) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID && mtbddnode_gettype(nb) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID) {
+            printf("ERROR: mtbdd_less_rec type SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID\n");
+        }
+#endif
     } else {
         /* Get top variable */
         uint32_t va = la ? 0xffffffff : mtbddnode_getvariable(na);
@@ -1736,6 +1813,11 @@ TASK_3(MTBDD, mtbdd_geq_rec, MTBDD, a, MTBDD, b, int*, shortcircuit)
             nom_b *= da/c;
             result = nom_a >= nom_b ? mtbdd_true : mtbdd_false;
         }
+#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL)
+		else if (mtbddnode_gettype(na) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID && mtbddnode_gettype(nb) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID) {
+            printf("ERROR: mtbdd_geq_rec type SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID\n");
+        }
+#endif
     } else {
         /* Get top variable */
         uint32_t va = la ? 0xffffffff : mtbddnode_getvariable(na);
@@ -1821,6 +1903,11 @@ TASK_3(MTBDD, mtbdd_greater_rec, MTBDD, a, MTBDD, b, int*, shortcircuit)
             nom_b *= da/c;
             result = nom_a > nom_b ? mtbdd_true : mtbdd_false;
         }
+#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL)
+		else if (mtbddnode_gettype(na) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID && mtbddnode_gettype(nb) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID) {
+            printf("ERROR: mtbdd_greater_rec type SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID\n");
+        }
+#endif
     } else {
         /* Get top variable */
         uint32_t va = la ? 0xffffffff : mtbddnode_getvariable(na);
@@ -2041,6 +2128,11 @@ TASK_IMPL_1(MTBDD, mtbdd_minimum, MTBDD, a)
         nom_h *= denom_l/c;
         result = nom_l < nom_h ? low : high;
     }
+#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL)
+	else if (mtbddnode_gettype(nl) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID && mtbddnode_gettype(nh) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID) {
+		printf("ERROR: mtbdd_minimum type SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID\n");
+	}
+#endif
 
     /* Store in cache */
     cache_put3(CACHE_MTBDD_MINIMUM, a, 0, 0, result);
@@ -2089,6 +2181,11 @@ TASK_IMPL_1(MTBDD, mtbdd_maximum, MTBDD, a)
         nom_h *= denom_l/c;
         result = nom_l > nom_h ? low : high;
     }
+#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL)
+	else if (mtbddnode_gettype(nl) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID && mtbddnode_gettype(nh) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID) {
+		printf("ERROR: mtbdd_maximum type SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID\n");
+	}
+#endif
 
     /* Store in cache */
     cache_put3(CACHE_MTBDD_MAXIMUM, a, 0, 0, result);
@@ -2237,12 +2334,20 @@ mtbdd_unmark_rec(MTBDD mtbdd)
 static size_t
 mtbdd_leafcount_mark(MTBDD mtbdd)
 {
-    if (mtbdd == mtbdd_true) return 0; // do not count true/false leaf
-    if (mtbdd == mtbdd_false) return 0; // do not count true/false leaf
+    if (mtbdd == mtbdd_true) { // do not count true/false leaf
+		return 0;
+	}
+    if (mtbdd == mtbdd_false) { // do not count true/false leaf
+		return 0;
+	}
     mtbddnode_t n = GETNODE(mtbdd);
-    if (mtbddnode_getmark(n)) return 0;
+    if (mtbddnode_getmark(n)) {
+		return 0;
+	}
     mtbddnode_setmark(n, 1);
-    if (mtbddnode_isleaf(n)) return 1; // count leaf as 1
+    if (mtbddnode_isleaf(n)) { // count leaf as 1
+		return 1;
+	}
     return mtbdd_leafcount_mark(mtbddnode_getlow(n)) + mtbdd_leafcount_mark(mtbddnode_gethigh(n));
 }
 
@@ -2372,6 +2477,12 @@ mtbdd_fprintdot_rec(FILE *out, MTBDD mtbdd, print_terminal_label_cb cb)
         case 2:
             fprintf(out, "%u/%u", (uint32_t)(value>>32), (uint32_t)value);
             break;
+#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL)
+		case SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID:
+			fprintf(out, "srf::");
+			print_storm_rational_function_to_file((storm_rational_function_ptr)value, out);
+			break;
+#endif
         default:
             cb(out, type, value);
             break;

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

@@ -97,6 +97,12 @@ TASK_IMPL_2(MTBDD, mtbdd_op_divide, MTBDD*, pa, MTBDD*, pb)
             MTBDD result = mtbdd_fraction(nom_a, denom_a);
             return result;
         }
+#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL)
+		else if (mtbddnode_gettype(na) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID && mtbddnode_gettype(nb) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID) {
+			printf("ERROR mtbdd_op_divide type SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID");
+			assert(0);
+		}
+#endif
     }
     
     return mtbdd_invalid;
@@ -140,6 +146,12 @@ TASK_IMPL_2(MTBDD, mtbdd_op_equals, MTBDD*, pa, MTBDD*, pb)
             if (nom_a == nom_b && denom_a == denom_b) return mtbdd_true;
             return mtbdd_false;
         }
+#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL)
+		else if (mtbddnode_gettype(na) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID && mtbddnode_gettype(nb) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID) {
+			printf("ERROR mtbdd_op_equals type SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID");
+			assert(0);
+		}
+#endif
     }
     
     if (a < b) {
@@ -187,6 +199,12 @@ TASK_IMPL_2(MTBDD, mtbdd_op_less, MTBDD*, pa, MTBDD*, pb)
             uint64_t denom_b = val_b&0xffffffff;
             return nom_a * denom_b < nom_b * denom_a ? mtbdd_true : mtbdd_false;
         }
+#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL)
+		else if (mtbddnode_gettype(na) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID && mtbddnode_gettype(nb) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID) {
+			printf("ERROR mtbdd_op_less type SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID");
+			assert(0);
+		}
+#endif
     }
     
     return mtbdd_invalid;
@@ -230,6 +248,12 @@ TASK_IMPL_2(MTBDD, mtbdd_op_less_or_equal, MTBDD*, pa, MTBDD*, pb)
             nom_b *= denom_a;
             return nom_a <= nom_b ? mtbdd_true : mtbdd_false;
         }
+#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL)
+		else if (mtbddnode_gettype(na) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID && mtbddnode_gettype(nb) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID) {
+			printf("ERROR mtbdd_op_less_or_equal type SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID");
+			assert(0);
+		}
+#endif
     }
     
     return mtbdd_invalid;
@@ -261,6 +285,12 @@ TASK_IMPL_2(MTBDD, mtbdd_op_pow, MTBDD*, pa, MTBDD*, pb)
         } else if (mtbddnode_gettype(na) == 2 && mtbddnode_gettype(nb) == 2) {
             assert(0);
         }
+#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL)
+		else if (mtbddnode_gettype(na) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID && mtbddnode_gettype(nb) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID) {
+			printf("ERROR mtbdd_op_pow type SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID");
+			assert(0);
+		}
+#endif
     }
     
     return mtbdd_invalid;
@@ -292,6 +322,12 @@ TASK_IMPL_2(MTBDD, mtbdd_op_mod, MTBDD*, pa, MTBDD*, pb)
         } else if (mtbddnode_gettype(na) == 2 && mtbddnode_gettype(nb) == 2) {
             assert(0);
         }
+#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL)
+		else if (mtbddnode_gettype(na) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID && mtbddnode_gettype(nb) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID) {
+			printf("ERROR mtbdd_op_mod type SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID");
+			assert(0);
+		}
+#endif
     }
     
     return mtbdd_invalid;
@@ -323,6 +359,12 @@ TASK_IMPL_2(MTBDD, mtbdd_op_logxy, MTBDD*, pa, MTBDD*, pb)
         } else if (mtbddnode_gettype(na) == 2 && mtbddnode_gettype(nb) == 2) {
             assert(0);
         }
+#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL)
+		else if (mtbddnode_gettype(na) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID && mtbddnode_gettype(nb) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID) {
+			printf("ERROR mtbdd_op_logxy type SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID");
+			assert(0);
+		}
+#endif
     }
     
     return mtbdd_invalid;
@@ -345,6 +387,11 @@ TASK_IMPL_2(MTBDD, mtbdd_op_not_zero, MTBDD, a, size_t, v)
         } else if (mtbddnode_gettype(na) == 2) {
             return mtbdd_getnumer(a) != 0 ? mtbdd_true : mtbdd_false;
         }
+#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL)
+		else if (mtbddnode_gettype(na) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID) {
+			return storm_rational_function_is_zero((storm_rational_function_ptr)mtbdd_getvalue(a)) == 0 ? mtbdd_true : mtbdd_false;
+		}
+#endif
     }
     
     // Ugly hack to get rid of the error "unused variable v" (because there is no version of uapply without a parameter).
@@ -377,6 +424,12 @@ TASK_IMPL_2(MTBDD, mtbdd_op_floor, MTBDD, a, size_t, v)
             MTBDD result = mtbdd_fraction(mtbdd_getnumer(a) / mtbdd_getdenom(a), 1);
             return result;
         }
+#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL)
+		else if (mtbddnode_gettype(na) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID) {
+			printf("ERROR mtbdd_op_floor type SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID");
+			assert(0);
+		}
+#endif
     }
     
     // Ugly hack to get rid of the error "unused variable v" (because there is no version of uapply without a parameter).
@@ -409,6 +462,12 @@ TASK_IMPL_2(MTBDD, mtbdd_op_ceil, MTBDD, a, size_t, v)
             MTBDD result = mtbdd_fraction(mtbdd_getnumer(a) / mtbdd_getdenom(a) + 1, 1);
             return result;
         }
+#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL)
+		else if (mtbddnode_gettype(na) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID) {
+			printf("ERROR mtbdd_op_ceil type SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID");
+			assert(0);
+		}
+#endif
     }
 
     // Ugly hack to get rid of the error "unused variable v" (because there is no version of uapply without a parameter).
@@ -474,6 +533,11 @@ TASK_IMPL_2(double, mtbdd_non_zero_count, MTBDD, dd, size_t, nvars)
         } else if (mtbddnode_gettype(na) == 2) {
             return mtbdd_getnumer(dd) != 0 ? powl(2.0L, nvars) : 0.0;
         }
+#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL)
+		else if (mtbddnode_gettype(na) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID) {
+			return storm_rational_function_is_zero((storm_rational_function_ptr)mtbdd_getvalue(dd)) == 0 ? powl(2.0L, nvars) : 0.0;
+		}
+#endif
     }
     
     /* Perhaps execute garbage collection */
@@ -506,6 +570,11 @@ int mtbdd_iszero(MTBDD dd) {
     } else if (mtbdd_gettype(dd) == 2) {
         return mtbdd_getnumer(dd) == 0;
     }
+#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL)
+	else if (mtbdd_gettype(dd) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID) {
+		return storm_rational_function_is_zero((storm_rational_function_ptr)mtbdd_getvalue(dd)) == 1 ? 1 : 0;
+	}
+#endif
     return 0;
 }
 

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

@@ -609,9 +609,8 @@ Mtbdd::doubleTerminal(double value)
 Mtbdd
 Mtbdd::stormRationalFunctionTerminal(storm::RationalFunction const& value)
 {
-	storm_rational_function_ptr_struct functionStruct;
-	functionStruct.storm_rational_function = (void*)(&value);
-    return mtbdd_storm_rational_function(&functionStruct);
+	storm_rational_function_ptr ptr = (storm_rational_function_ptr)(&value);
+    return mtbdd_storm_rational_function(ptr);
 }
 #endif
 
@@ -1039,6 +1038,7 @@ void
 Sylvan::initMtbdd()
 {
     sylvan_init_mtbdd();
+	sylvan_storm_rational_function_init();
 }
 
 void

resources/3rdparty/sylvan/src/sylvan_obj_mtbdd_storm.hpp

@@ -8,6 +8,28 @@
      */
     Mtbdd Divide(const Mtbdd &other) const;
     
+#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL)
+	/**
+     * @brief Computes f + g for Rational Functions
+     */
+    Mtbdd PlusRF(const Mtbdd &other) const;
+
+    /**
+     * @brief Computes f * g for Rational Functions
+     */
+    Mtbdd TimesRF(const Mtbdd &other) const;
+	
+	/**
+     * @brief Computes f - g for Rational Functions
+     */
+    Mtbdd MinusRF(const Mtbdd &other) const;
+
+    /**
+     * @brief Computes f / g for Rational Functions
+     */
+    Mtbdd DivideRF(const Mtbdd &other) const;
+#endif
+	
     Bdd NotZero() const;
     
     Bdd Equals(const Mtbdd& other) const;

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

@@ -16,6 +16,36 @@ Bdd::toStormRationalFunctionMtbdd() const {
     LACE_ME;
     return mtbdd_bool_to_storm_rational_function(bdd);
 }
+
+Mtbdd
+Mtbdd::PlusRF(const Mtbdd &other) const
+{
+    LACE_ME;
+    return sylvan_storm_rational_function_plus(mtbdd, other.mtbdd);
+}
+
+
+Mtbdd
+Mtbdd::TimesRF(const Mtbdd &other) const
+{
+    LACE_ME;
+    return sylvan_storm_rational_function_times(mtbdd, other.mtbdd);
+}
+
+Mtbdd
+Mtbdd::MinusRF(const Mtbdd &other) const
+{
+    LACE_ME;
+    return sylvan_storm_rational_function_minus(mtbdd, other.mtbdd);
+}
+
+Mtbdd
+Mtbdd::DivideRF(const Mtbdd &other) const
+{
+    LACE_ME;
+    return sylvan_storm_rational_function_divide(mtbdd, other.mtbdd);
+}
+
 #endif
 
 Mtbdd

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

@@ -15,6 +15,18 @@
 
 #include <storm_function_wrapper.h>
 
+#undef SYLVAN_STORM_RATIONAL_FUNCTION_DEBUG
+
+#ifdef SYLVAN_STORM_RATIONAL_FUNCTION_DEBUG
+int depth = 0;
+
+#define LOG_I(funcName) do { for (int i = 0; i < depth; ++i) { printf(" "); } ++depth; printf("Entering function " funcName "\n"); } while (0 != 0);
+#define LOG_O(funcName) do { --depth; for (int i = 0; i < depth; ++i) { printf(" "); } printf("Leaving function " funcName "\n"); } while (0 != 0);
+#else
+#define LOG_I(funcName)
+#define LOG_O(funcName)
+#endif
+
 /**
  * helper function for hash
  */
@@ -29,42 +41,73 @@ rotl64(uint64_t x, int8_t r)
 static uint64_t
 sylvan_storm_rational_function_hash(const uint64_t v, const uint64_t seed)
 {
+	LOG_I("i-hash")
     /* Hash the storm::RationalFunction in pointer v */
     
-	storm_rational_function_ptr x = (storm_rational_function_ptr)(size_t)v;
+	storm_rational_function_ptr x = (storm_rational_function_ptr)v;
+
+	uint64_t hash = storm_rational_function_hash(x, seed);
+
+#ifdef SYLVAN_STORM_RATIONAL_FUNCTION_DEBUG
+	printf("Hashing ptr %p with contents ", x);
+	print_storm_rational_function(x);
+	printf(" with seed %zu, hash = %zu\n", seed, hash);
+#endif
 
-	return storm_rational_function_hash(x, seed);
+	LOG_O("i-hash")
+	return hash;
 }
 
 static int
 sylvan_storm_rational_function_equals(const uint64_t left, const uint64_t right)
 {
+	LOG_I("i-equals")
     /* 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;
+	int result = storm_rational_function_equals(a, b);
+	
+	LOG_O("i-equals")
+    return result;
 }
 
 static void
 sylvan_storm_rational_function_create(uint64_t *val)
 {
-	printf("sylvan_storm_rational_function_create(val = %zu)\n", *val);
+	LOG_I("i-create")
+	
+#ifdef SYLVAN_STORM_RATIONAL_FUNCTION_DEBUG
+	void* tmp = (void*)*val;
+	printf("sylvan_storm_rational_function_create(ptr = %p, value = ", tmp);
+	print_storm_rational_function(*((storm_rational_function_ptr*)(size_t)val));
+	printf(")\n");
+#endif
+	
     /* 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);
+	
+#ifdef SYLVAN_STORM_RATIONAL_FUNCTION_DEBUG
+	tmp = (void*)*val;
+	printf("sylvan_storm_rational_function_create_2(ptr = %p)\n", tmp);
+#endif
+	
+	LOG_O("i-create")
 }
 
 static void
 sylvan_storm_rational_function_destroy(uint64_t val)
 {
+	LOG_I("i-destroy")
     /* 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);
+	LOG_O("i-destroy")
 }
 
 static uint32_t sylvan_storm_rational_function_type;
@@ -78,6 +121,12 @@ 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);
+	
+	if (SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID != sylvan_storm_rational_function_type) {
+		printf("ERROR - ERROR - ERROR\nThe Sylvan Type ID is NOT correct.\nIt was assumed to be %u, but it is actually %u!\nYou NEED to fix this by changing the macro \"SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID\" and recompiling StoRM!\n\n", SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID, sylvan_storm_rational_function_type);
+		assert(0);
+	}	
+	
 	CACHE_STORM_RATIONAL_FUNCTION_AND_EXISTS = cache_next_opid();
 }
 
@@ -89,11 +138,21 @@ uint32_t sylvan_storm_rational_function_get_type() {
  * Create storm::RationalFunction leaf
  */
 MTBDD
-mtbdd_storm_rational_function(storm_rational_function_t val)
+mtbdd_storm_rational_function(storm_rational_function_ptr val)
 {
+	LOG_I("i-mtbdd_")
 	uint64_t terminalValue = (uint64_t)val;
-	printf("mtbdd_storm_rational_function(val = %zu)\n", terminalValue);
-	return mtbdd_makeleaf(sylvan_storm_rational_function_type, terminalValue);
+	
+#ifdef SYLVAN_STORM_RATIONAL_FUNCTION_DEBUG
+	printf("mtbdd_storm_rational_function(ptr = %p, value = ", val);
+	print_storm_rational_function(val);
+	printf(")\n");
+#endif
+	
+	MTBDD result = mtbdd_makeleaf(sylvan_storm_rational_function_type, terminalValue);
+	
+	LOG_O("i-mtbdd_")
+	return result;
 }
 
 /**
@@ -101,21 +160,30 @@ mtbdd_storm_rational_function(storm_rational_function_t val)
  */
 TASK_IMPL_2(MTBDD, mtbdd_op_bool_to_storm_rational_function, MTBDD, a, size_t, v)
 {
+	LOG_I("task_impl_2 to_srf")
 	if (a == mtbdd_false) {
-		return mtbdd_storm_rational_function(storm_rational_function_get_zero());
+		storm_rational_function_ptr srf_zero = storm_rational_function_get_zero();
+		MTBDD result = mtbdd_storm_rational_function(srf_zero);
+		LOG_O("task_impl_2 to_srf - ZERO")
+		return result;
 	}
 	if (a == mtbdd_true) {
-		return mtbdd_storm_rational_function(storm_rational_function_get_one());
+		storm_rational_function_ptr srf_one = storm_rational_function_get_one();
+		MTBDD result = mtbdd_storm_rational_function(srf_one);
+		LOG_O("task_impl_2 to_srf - ONE")
+		return result;
 	}
     
     // Ugly hack to get rid of the error "unused variable v" (because there is no version of uapply without a parameter).
     (void)v;
-    
+	
+    LOG_O("task_impl_2 to_srf - INVALID")
     return mtbdd_invalid;
 }
 
 TASK_IMPL_1(MTBDD, mtbdd_bool_to_storm_rational_function, MTBDD, dd)
 {
+	LOG_I("task_impl_1 to_srf")
     return mtbdd_uapply(dd, TASK(mtbdd_op_bool_to_storm_rational_function), 0);
 }
 
@@ -125,6 +193,7 @@ TASK_IMPL_1(MTBDD, mtbdd_bool_to_storm_rational_function, MTBDD, dd)
  */
 TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_plus, MTBDD*, pa, MTBDD*, pb)
 {
+	LOG_I("task_impl_2 op_plus")
     MTBDD a = *pa, b = *pb;
 
     /* Check for partial functions */
@@ -159,7 +228,8 @@ TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_plus, MTBDD*, pa, MTBDD*, p
  */
 TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_minus, MTBDD*, pa, MTBDD*, pb)
 {
-    MTBDD a = *pa, b = *pb;
+    LOG_I("task_impl_2 op_minus")
+	MTBDD a = *pa, b = *pb;
 
     /* Check for partial functions */
     if (a == mtbdd_false) return sylvan_storm_rational_function_neg(b);
@@ -188,6 +258,7 @@ TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_minus, MTBDD*, pa, MTBDD*,
  */
 TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_times, MTBDD*, pa, MTBDD*, pb)
 {
+	LOG_I("task_impl_2 op_times")
     MTBDD a = *pa, b = *pb;
 
     /* Check for partial functions and for Boolean (filter) */
@@ -202,7 +273,7 @@ TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_times, MTBDD*, pa, MTBDD*,
 		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);
+		storm_rational_function_ptr mres = storm_rational_function_times(ma, mb);		
 		MTBDD res = mtbdd_storm_rational_function(mres);
 
 		// TODO: Delete mres?
@@ -225,6 +296,7 @@ TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_times, MTBDD*, pa, MTBDD*,
  */
 TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_divide, MTBDD*, pa, MTBDD*, pb)
 {
+	LOG_I("task_impl_2 op_divide")
     MTBDD a = *pa, b = *pb;
 
     /* Check for partial functions */
@@ -254,6 +326,7 @@ TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_divide, MTBDD*, pa, MTBDD*,
 
 TASK_IMPL_3(MTBDD, sylvan_storm_rational_function_abstract_op_plus, MTBDD, a, MTBDD, b, int, k)
 {
+	LOG_I("task_impl_3 abstract_op_plus")
     if (k==0) {
         return mtbdd_apply(a, b, TASK(sylvan_storm_rational_function_op_plus));
     } else {
@@ -269,6 +342,7 @@ TASK_IMPL_3(MTBDD, sylvan_storm_rational_function_abstract_op_plus, MTBDD, a, MT
 
 TASK_IMPL_3(MTBDD, sylvan_storm_rational_function_abstract_op_times, MTBDD, a, MTBDD, b, int, k)
 {
+	LOG_I("task_impl_3 abstract_op_times")
     if (k==0) {
         return mtbdd_apply(a, b, TASK(sylvan_storm_rational_function_op_times));
     } else {
@@ -287,6 +361,7 @@ TASK_IMPL_3(MTBDD, sylvan_storm_rational_function_abstract_op_times, MTBDD, a, M
  */
 TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_neg, MTBDD, dd, size_t, p)
 {
+	LOG_I("task_impl_2 op_neg")
     /* Handle partial functions */
     if (dd == mtbdd_false) return mtbdd_false;
 

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

@@ -12,6 +12,8 @@
 
 #if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL)
 
+#define SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID (3)
+
 #ifdef __cplusplus
 extern "C" {
 #endif /* __cplusplus */
@@ -29,7 +31,7 @@ uint32_t sylvan_storm_rational_function_get_type();
 /**
  * Create storm::RationalFunction leaf
  */
-MTBDD mtbdd_storm_rational_function(storm_rational_function_t val);
+MTBDD mtbdd_storm_rational_function(storm_rational_function_ptr val);
 
 /**
  * Monad that converts Boolean to a storm::RationalFunction MTBDD, translate terminals true to 1 and to 0 otherwise;

src/storage/dd/DdManager.cpp

@@ -10,6 +10,7 @@
 #include "src/adapters/CarlAdapter.h"
 
 #include <cmath>
+#include <iostream>
 
 namespace storm {
     namespace dd {
@@ -105,21 +106,6 @@ namespace storm {
             }
             return result;
         }
-        
-#ifdef STORM_HAVE_CARL
-		template<>
-		template<>
-        Add<DdType::Sylvan, storm::RationalFunction> DdManager<DdType::Sylvan>::getIdentity(storm::expressions::Variable const& variable) const {
-            storm::dd::DdMetaVariable<DdType::Sylvan> const& metaVariable = this->getMetaVariable(variable);
-            
-            Add<DdType::Sylvan, storm::RationalFunction> result = this->getAddZero<storm::RationalFunction>();
-            for (int_fast64_t value = metaVariable.getLow(); value <= metaVariable.getHigh(); ++value) {
-				storm::RationalFunction constantFunction(value);
-                result += this->getEncoding(variable, value).template toAdd<storm::RationalFunction>() * this->getConstant(constantFunction);
-            }
-            return result;
-        }
-#endif
 		
         template<DdType LibraryType>
         std::pair<storm::expressions::Variable, storm::expressions::Variable> DdManager<LibraryType>::addMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high) {

src/storage/dd/sylvan/InternalSylvanAdd.cpp

@@ -33,126 +33,298 @@ namespace storm {
         InternalAdd<DdType::Sylvan, ValueType> InternalAdd<DdType::Sylvan, ValueType>::operator+(InternalAdd<DdType::Sylvan, ValueType> const& other) const {
             return InternalAdd<DdType::Sylvan, ValueType>(ddManager, this->sylvanMtbdd.Plus(other.sylvanMtbdd));
         }
-        
+
+#ifdef STORM_HAVE_CARL
+		template<>
+        InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalAdd<DdType::Sylvan, storm::RationalFunction>::operator+(InternalAdd<DdType::Sylvan, storm::RationalFunction> const& other) const {
+            return InternalAdd<DdType::Sylvan, storm::RationalFunction>(ddManager, this->sylvanMtbdd.PlusRF(other.sylvanMtbdd));
+        }
+#endif
+
         template<typename ValueType>
         InternalAdd<DdType::Sylvan, ValueType>& InternalAdd<DdType::Sylvan, ValueType>::operator+=(InternalAdd<DdType::Sylvan, ValueType> const& other) {
             this->sylvanMtbdd = this->sylvanMtbdd.Plus(other.sylvanMtbdd);
             return *this;
         }
-        
+
+#ifdef STORM_HAVE_CARL
+		template<>
+        InternalAdd<DdType::Sylvan, storm::RationalFunction>& InternalAdd<DdType::Sylvan, storm::RationalFunction>::operator+=(InternalAdd<DdType::Sylvan, storm::RationalFunction> const& other) {
+            this->sylvanMtbdd = this->sylvanMtbdd.PlusRF(other.sylvanMtbdd);
+            return *this;
+        }
+#endif
+
         template<typename ValueType>
         InternalAdd<DdType::Sylvan, ValueType> InternalAdd<DdType::Sylvan, ValueType>::operator*(InternalAdd<DdType::Sylvan, ValueType> const& other) const {
             return InternalAdd<DdType::Sylvan, ValueType>(ddManager, this->sylvanMtbdd.Times(other.sylvanMtbdd));
         }
-        
+
+#ifdef STORM_HAVE_CARL
+		template<>
+        InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalAdd<DdType::Sylvan, storm::RationalFunction>::operator*(InternalAdd<DdType::Sylvan, storm::RationalFunction> const& other) const {
+            return InternalAdd<DdType::Sylvan, storm::RationalFunction>(ddManager, this->sylvanMtbdd.TimesRF(other.sylvanMtbdd));
+        }
+#endif
+
         template<typename ValueType>
         InternalAdd<DdType::Sylvan, ValueType>& InternalAdd<DdType::Sylvan, ValueType>::operator*=(InternalAdd<DdType::Sylvan, ValueType> const& other) {
             this->sylvanMtbdd = this->sylvanMtbdd.Times(other.sylvanMtbdd);
             return *this;
         }
-        
+
+#ifdef STORM_HAVE_CARL
+		template<>
+        InternalAdd<DdType::Sylvan, storm::RationalFunction>& InternalAdd<DdType::Sylvan, storm::RationalFunction>::operator*=(InternalAdd<DdType::Sylvan, storm::RationalFunction> const& other) {
+            this->sylvanMtbdd = this->sylvanMtbdd.TimesRF(other.sylvanMtbdd);
+            return *this;
+        }
+#endif
+
         template<typename ValueType>
         InternalAdd<DdType::Sylvan, ValueType> InternalAdd<DdType::Sylvan, ValueType>::operator-(InternalAdd<DdType::Sylvan, ValueType> const& other) const {
             return InternalAdd<DdType::Sylvan, ValueType>(ddManager,  this->sylvanMtbdd.Minus(other.sylvanMtbdd));
         }
-        
+
+#ifdef STORM_HAVE_CARL
+		template<>
+        InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalAdd<DdType::Sylvan, storm::RationalFunction>::operator-(InternalAdd<DdType::Sylvan, storm::RationalFunction> const& other) const {
+            return InternalAdd<DdType::Sylvan, storm::RationalFunction>(ddManager,  this->sylvanMtbdd.MinusRF(other.sylvanMtbdd));
+        }
+#endif
+
         template<typename ValueType>
         InternalAdd<DdType::Sylvan, ValueType>& InternalAdd<DdType::Sylvan, ValueType>::operator-=(InternalAdd<DdType::Sylvan, ValueType> const& other) {
             this->sylvanMtbdd = this->sylvanMtbdd.Minus(other.sylvanMtbdd);
             return *this;
         }
-        
+
+#ifdef STORM_HAVE_CARL
+		template<>
+        InternalAdd<DdType::Sylvan, storm::RationalFunction>& InternalAdd<DdType::Sylvan, storm::RationalFunction>::operator-=(InternalAdd<DdType::Sylvan, storm::RationalFunction> const& other) {
+            this->sylvanMtbdd = this->sylvanMtbdd.MinusRF(other.sylvanMtbdd);
+            return *this;
+        }
+#endif
+
         template<typename ValueType>
         InternalAdd<DdType::Sylvan, ValueType> InternalAdd<DdType::Sylvan, ValueType>::operator/(InternalAdd<DdType::Sylvan, ValueType> const& other) const {
             return InternalAdd<DdType::Sylvan, ValueType>(ddManager,  this->sylvanMtbdd.Divide(other.sylvanMtbdd));
         }
-        
+
+#ifdef STORM_HAVE_CARL
+		template<>
+        InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalAdd<DdType::Sylvan, storm::RationalFunction>::operator/(InternalAdd<DdType::Sylvan, storm::RationalFunction> const& other) const {
+            return InternalAdd<DdType::Sylvan, storm::RationalFunction>(ddManager,  this->sylvanMtbdd.DivideRF(other.sylvanMtbdd));
+        }
+#endif
+
         template<typename ValueType>
         InternalAdd<DdType::Sylvan, ValueType>& InternalAdd<DdType::Sylvan, ValueType>::operator/=(InternalAdd<DdType::Sylvan, ValueType> const& other) {
             this->sylvanMtbdd = this->sylvanMtbdd.Divide(other.sylvanMtbdd);
             return *this;
         }
-        
+
+#ifdef STORM_HAVE_CARL
+		template<>
+        InternalAdd<DdType::Sylvan, storm::RationalFunction>& InternalAdd<DdType::Sylvan, storm::RationalFunction>::operator/=(InternalAdd<DdType::Sylvan, storm::RationalFunction> const& other) {
+            this->sylvanMtbdd = this->sylvanMtbdd.DivideRF(other.sylvanMtbdd);
+            return *this;
+        }
+#endif
+
         template<typename ValueType>
         InternalBdd<DdType::Sylvan> InternalAdd<DdType::Sylvan, ValueType>::equals(InternalAdd<DdType::Sylvan, ValueType> const& other) const {
             return InternalBdd<DdType::Sylvan>(ddManager,  this->sylvanMtbdd.Equals(other.sylvanMtbdd));
         }
-        
+
+#ifdef STORM_HAVE_CARL
+		template<>
+        InternalBdd<DdType::Sylvan> InternalAdd<DdType::Sylvan, storm::RationalFunction>::equals(InternalAdd<DdType::Sylvan, storm::RationalFunction> const& other) const {
+            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: Equals");
+        }
+#endif
+
         template<typename ValueType>
         InternalBdd<DdType::Sylvan> InternalAdd<DdType::Sylvan, ValueType>::notEquals(InternalAdd<DdType::Sylvan, ValueType> const& other) const {
             return !this->equals(other);
         }
-        
+
+#ifdef STORM_HAVE_CARL
+		template<>
+        InternalBdd<DdType::Sylvan> InternalAdd<DdType::Sylvan, storm::RationalFunction>::notEquals(InternalAdd<DdType::Sylvan, storm::RationalFunction> const& other) const {
+            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: Not Equals");
+        }
+#endif
+
         template<typename ValueType>
         InternalBdd<DdType::Sylvan> InternalAdd<DdType::Sylvan, ValueType>::less(InternalAdd<DdType::Sylvan, ValueType> const& other) const {
             return InternalBdd<DdType::Sylvan>(ddManager, this->sylvanMtbdd.Less(other.sylvanMtbdd));
         }
-        
+
+#ifdef STORM_HAVE_CARL
+		template<>
+        InternalBdd<DdType::Sylvan> InternalAdd<DdType::Sylvan, storm::RationalFunction>::less(InternalAdd<DdType::Sylvan, storm::RationalFunction> const& other) const {
+            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: Less");
+        }
+#endif
+
         template<typename ValueType>
         InternalBdd<DdType::Sylvan> InternalAdd<DdType::Sylvan, ValueType>::lessOrEqual(InternalAdd<DdType::Sylvan, ValueType> const& other) const {
             return InternalBdd<DdType::Sylvan>(ddManager, this->sylvanMtbdd.LessOrEqual(other.sylvanMtbdd));
         }
-        
+
+#ifdef STORM_HAVE_CARL
+		template<>
+        InternalBdd<DdType::Sylvan> InternalAdd<DdType::Sylvan, storm::RationalFunction>::lessOrEqual(InternalAdd<DdType::Sylvan, storm::RationalFunction> const& other) const {
+            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: Less or Equal");
+        }
+#endif
+
         template<typename ValueType>
         InternalBdd<DdType::Sylvan> InternalAdd<DdType::Sylvan, ValueType>::greater(InternalAdd<DdType::Sylvan, ValueType> const& other) const {
             return !this->lessOrEqual(other);
         }
-        
+
+#ifdef STORM_HAVE_CARL
+		template<>
+        InternalBdd<DdType::Sylvan> InternalAdd<DdType::Sylvan, storm::RationalFunction>::greater(InternalAdd<DdType::Sylvan, storm::RationalFunction> const& other) const {
+            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: Greater");
+        }
+#endif
+
         template<typename ValueType>
         InternalBdd<DdType::Sylvan> InternalAdd<DdType::Sylvan, ValueType>::greaterOrEqual(InternalAdd<DdType::Sylvan, ValueType> const& other) const {
             return !this->less(other);
         }
-        
+
+#ifdef STORM_HAVE_CARL
+		template<>
+        InternalBdd<DdType::Sylvan> InternalAdd<DdType::Sylvan, storm::RationalFunction>::greaterOrEqual(InternalAdd<DdType::Sylvan, storm::RationalFunction> const& other) const {
+            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: Greater or Equal");
+        }
+#endif
+
         template<typename ValueType>
         InternalAdd<DdType::Sylvan, ValueType> InternalAdd<DdType::Sylvan, ValueType>::pow(InternalAdd<DdType::Sylvan, ValueType> const& other) const {
             return InternalAdd<DdType::Sylvan, ValueType>(ddManager, this->sylvanMtbdd.Pow(other.sylvanMtbdd));
         }
-        
+
+#ifdef STORM_HAVE_CARL
+		template<>
+        InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalAdd<DdType::Sylvan, storm::RationalFunction>::pow(InternalAdd<DdType::Sylvan, storm::RationalFunction> const& other) const {
+            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: Pow");
+        }
+#endif
+
         template<typename ValueType>
         InternalAdd<DdType::Sylvan, ValueType> InternalAdd<DdType::Sylvan, ValueType>::mod(InternalAdd<DdType::Sylvan, ValueType> const& other) const {
             return InternalAdd<DdType::Sylvan, ValueType>(ddManager, this->sylvanMtbdd.Mod(other.sylvanMtbdd));
         }
-        
+
+#ifdef STORM_HAVE_CARL
+		template<>
+        InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalAdd<DdType::Sylvan, storm::RationalFunction>::mod(InternalAdd<DdType::Sylvan, storm::RationalFunction> const& other) const {
+            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: Mod");
+        }
+#endif
+
         template<typename ValueType>
         InternalAdd<DdType::Sylvan, ValueType> InternalAdd<DdType::Sylvan, ValueType>::logxy(InternalAdd<DdType::Sylvan, ValueType> const& other) const {
             return InternalAdd<DdType::Sylvan, ValueType>(ddManager, this->sylvanMtbdd.Logxy(other.sylvanMtbdd));
         }
-        
+
+#ifdef STORM_HAVE_CARL
+		template<>
+        InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalAdd<DdType::Sylvan, storm::RationalFunction>::logxy(InternalAdd<DdType::Sylvan, storm::RationalFunction> const& other) const {
+            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: logxy");
+        }
+#endif
+
         template<typename ValueType>
         InternalAdd<DdType::Sylvan, ValueType> InternalAdd<DdType::Sylvan, ValueType>::floor() const {
             return InternalAdd<DdType::Sylvan, ValueType>(ddManager, this->sylvanMtbdd.Floor());
         }
-        
+
+#ifdef STORM_HAVE_CARL
+		template<>
+        InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalAdd<DdType::Sylvan, storm::RationalFunction>::floor() const {
+            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: Floor");
+        }
+#endif
+
         template<typename ValueType>
         InternalAdd<DdType::Sylvan, ValueType> InternalAdd<DdType::Sylvan, ValueType>::ceil() const {
             return InternalAdd<DdType::Sylvan, ValueType>(ddManager, this->sylvanMtbdd.Ceil());
         }
-        
+
+#ifdef STORM_HAVE_CARL
+		template<>
+        InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalAdd<DdType::Sylvan, storm::RationalFunction>::ceil() const {
+            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: Ceil");
+        }
+#endif
+
         template<typename ValueType>
         InternalAdd<DdType::Sylvan, ValueType> InternalAdd<DdType::Sylvan, ValueType>::minimum(InternalAdd<DdType::Sylvan, ValueType> const& other) const {
             return InternalAdd<DdType::Sylvan, ValueType>(ddManager, this->sylvanMtbdd.Min(other.sylvanMtbdd));
         }
-        
+
+#ifdef STORM_HAVE_CARL
+		template<>
+        InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalAdd<DdType::Sylvan, storm::RationalFunction>::minimum(InternalAdd<DdType::Sylvan, storm::RationalFunction> const& other) const {
+            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: Minimum");
+        }
+#endif
+
         template<typename ValueType>
         InternalAdd<DdType::Sylvan, ValueType> InternalAdd<DdType::Sylvan, ValueType>::maximum(InternalAdd<DdType::Sylvan, ValueType> const& other) const {
             return InternalAdd<DdType::Sylvan, ValueType>(ddManager, this->sylvanMtbdd.Max(other.sylvanMtbdd));
         }
-        
+
+#ifdef STORM_HAVE_CARL
+		template<>
+        InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalAdd<DdType::Sylvan, storm::RationalFunction>::maximum(InternalAdd<DdType::Sylvan, storm::RationalFunction> const& other) const {
+            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: Maximum");
+        }
+#endif
+
         template<typename ValueType>
         InternalAdd<DdType::Sylvan, ValueType> InternalAdd<DdType::Sylvan, ValueType>::sumAbstract(InternalBdd<DdType::Sylvan> const& cube) const {
             return InternalAdd<DdType::Sylvan, ValueType>(ddManager, this->sylvanMtbdd.AbstractPlus(cube.sylvanBdd));
         }
-        
+
+#ifdef STORM_HAVE_CARL
+		template<>
+        InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalAdd<DdType::Sylvan, storm::RationalFunction>::sumAbstract(InternalBdd<DdType::Sylvan> const& cube) const {
+            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: sumAbstract");
+        }
+#endif
+
         template<typename ValueType>
         InternalAdd<DdType::Sylvan, ValueType> InternalAdd<DdType::Sylvan, ValueType>::minAbstract(InternalBdd<DdType::Sylvan> const& cube) const {
             return InternalAdd<DdType::Sylvan, ValueType>(ddManager, this->sylvanMtbdd.AbstractMin(cube.sylvanBdd));
         }
-        
+
+#ifdef STORM_HAVE_CARL
+		template<>
+        InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalAdd<DdType::Sylvan, storm::RationalFunction>::minAbstract(InternalBdd<DdType::Sylvan> const& cube) const {
+            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: minAbstract");
+        }
+#endif
+
         template<typename ValueType>
         InternalAdd<DdType::Sylvan, ValueType> InternalAdd<DdType::Sylvan, ValueType>::maxAbstract(InternalBdd<DdType::Sylvan> const& cube) const {
             return InternalAdd<DdType::Sylvan, ValueType>(ddManager, this->sylvanMtbdd.AbstractMax(cube.sylvanBdd));
         }
-        
+
+#ifdef STORM_HAVE_CARL
+		template<>
+        InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalAdd<DdType::Sylvan, storm::RationalFunction>::maxAbstract(InternalBdd<DdType::Sylvan> const& cube) const {
+            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: maxAbstract");
+        }
+#endif
+
         template<typename ValueType>
         bool InternalAdd<DdType::Sylvan, ValueType>::equalModuloPrecision(InternalAdd<DdType::Sylvan, ValueType> const& other, double precision, bool relative) const {
             if (relative) {
@@ -161,7 +333,14 @@ namespace storm {
                 return this->sylvanMtbdd.EqualNorm(other.sylvanMtbdd, precision);
             }
         }
-        
+
+#ifdef STORM_HAVE_CARL
+		template<>
+        bool InternalAdd<DdType::Sylvan, storm::RationalFunction>::equalModuloPrecision(InternalAdd<DdType::Sylvan, storm::RationalFunction> const& other, double precision, bool relative) const {
+            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: equalModuloPrecision");
+        }
+#endif
+
         template<typename ValueType>
         InternalAdd<DdType::Sylvan, ValueType> InternalAdd<DdType::Sylvan, ValueType>::swapVariables(std::vector<InternalBdd<DdType::Sylvan>> const& from, std::vector<InternalBdd<DdType::Sylvan>> const& to) const {
             std::vector<uint32_t> fromIndices;
@@ -615,10 +794,9 @@ namespace storm {
 
 		template<typename ValueType>
 		MTBDD InternalAdd<DdType::Sylvan, ValueType>::getLeaf(storm::RationalFunction const& value) {
-			storm_rational_function_ptr_struct helperStruct;
-			helperStruct.storm_rational_function = (void*)(&value);
+			storm_rational_function_ptr ptr = (storm_rational_function_ptr)(&value);
 
-			return mtbdd_storm_rational_function(&helperStruct);
+			return mtbdd_storm_rational_function(ptr);
 		}
         
         template<typename ValueType>
@@ -639,7 +817,7 @@ namespace storm {
 			else if (std::is_same<ValueType, storm::RationalFunction>::value) {
 				STORM_LOG_ASSERT(false, "Non-specialized version of getValue() called for storm::RationalFunction value.");
 			} 
-#endif			
+#endif
 			else {
                 STORM_LOG_ASSERT(false, "Illegal or unknown type in MTBDD.");
             }
@@ -655,9 +833,9 @@ namespace storm {
 
 			STORM_LOG_ASSERT(mtbdd_gettype(node) == sylvan_storm_rational_function_get_type(), "Expected a storm::RationalFunction value.");
 			uint64_t value = mtbdd_getvalue(node);
-			storm_rational_function_ptr_struct* helperStructPtr = (storm_rational_function_ptr_struct*)value;
+			storm_rational_function_ptr ptr = (storm_rational_function_ptr)value;
 
-			storm::RationalFunction* rationalFunction = (storm::RationalFunction*)(helperStructPtr->storm_rational_function);
+			storm::RationalFunction* rationalFunction = (storm::RationalFunction*)(ptr);
 
 			return negated ? -(*rationalFunction) : (*rationalFunction);
 		}

src/storage/dd/sylvan/InternalSylvanDdManager.cpp

@@ -1,175 +1,166 @@
-#include "src/storage/dd/sylvan/InternalSylvanDdManager.h"
-
-#include <cmath>
-
-#include "src/settings/SettingsManager.h"
-#include "src/settings/modules/SylvanSettings.h"
-
-#include "src/utility/constants.h"
-#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<DdType::Sylvan>::numberOfInstances = 0;
-        
-        // It is important that the variable pairs start at an even offset, because sylvan assumes this to be true for
-        // some operations.
-        uint_fast64_t InternalDdManager<DdType::Sylvan>::nextFreeVariableIndex = 0;
-        
-        uint_fast64_t findLargestPowerOfTwoFitting(uint_fast64_t number) {
-            for (uint_fast64_t index = 0; index < 64; ++index) {
-                if ((number & (1ull << (63 - index))) != 0) {
-                    return 63 - index;
-                }
-            }
-            return 0;
-        }
-        
-        InternalDdManager<DdType::Sylvan>::InternalDdManager() {
-            if (numberOfInstances == 0) {
-                // Initialize lace: auto-detect number of workers.
-                lace_init(storm::settings::getModule<storm::settings::modules::SylvanSettings>().getNumberOfThreads(), 1000000);
-                lace_startup(0, 0, 0);
-                
-                // Each node takes 24 bytes and the maximal memory is specified in megabytes.
-                uint_fast64_t totalNodesToStore = storm::settings::getModule<storm::settings::modules::SylvanSettings>().getMaximalMemory() * 1024 * 1024 / 24;
-                
-                // Compute the power of two that still fits within the total numbers to store.
-                uint_fast64_t powerOfTwo = findLargestPowerOfTwoFitting(totalNodesToStore);
-                
-                sylvan::Sylvan::initPackage(1ull << std::max(16ull, powerOfTwo > 24 ? powerOfTwo - 8 : 0ull), 1ull << (powerOfTwo - 1), 1ull << std::max(16ull, powerOfTwo > 24 ? powerOfTwo - 12 : 0ull), 1ull << (powerOfTwo - 1));
-                sylvan::Sylvan::initBdd(1);
-                sylvan::Sylvan::initMtbdd();
-            }
-            ++numberOfInstances;
-        }
-        
-        InternalDdManager<DdType::Sylvan>::~InternalDdManager() {
-            --numberOfInstances;
-            if (numberOfInstances == 0) {
-                // Enable this to print the sylvan statistics to a file.
-//                FILE* filePointer = fopen("sylvan.stats", "w");
-//                sylvan_stats_report(filePointer, 0);
-//                fclose(filePointer);
-                
-                sylvan::Sylvan::quitPackage();
-                lace_exit();
-            }
-        }
-        
-        InternalBdd<DdType::Sylvan> InternalDdManager<DdType::Sylvan>::getBddOne() const {
-            return InternalBdd<DdType::Sylvan>(this, sylvan::Bdd::bddOne());
-        }
-        
-        template<>
-        InternalAdd<DdType::Sylvan, double> InternalDdManager<DdType::Sylvan>::getAddOne() const {
-            return InternalAdd<DdType::Sylvan, double>(this, sylvan::Mtbdd::doubleTerminal(storm::utility::one<double>()));
-        }
-
-        template<>
-        InternalAdd<DdType::Sylvan, uint_fast64_t> InternalDdManager<DdType::Sylvan>::getAddOne() const {
-            return InternalAdd<DdType::Sylvan, uint_fast64_t>(this, sylvan::Mtbdd::int64Terminal(storm::utility::one<uint_fast64_t>()));
-        }
-
-#ifdef STORM_HAVE_CARL
-		template<>
-		InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalDdManager<DdType::Sylvan>::getAddOne() const {
-			storm::RationalFunction rationalFunction = storm::utility::one<storm::RationalFunction>();
-			storm_rational_function_ptr_struct helperStruct;
-			helperStruct.storm_rational_function = (void*)(&rationalFunction);
-			uint64_t value = (uint64_t)&helperStruct;
-
-			return InternalAdd<DdType::Sylvan, storm::RationalFunction>(this, sylvan::Mtbdd::terminal(sylvan_storm_rational_function_get_type(), value));
-		}
-#endif
-        
-        InternalBdd<DdType::Sylvan> InternalDdManager<DdType::Sylvan>::getBddZero() const {
-            return InternalBdd<DdType::Sylvan>(this, sylvan::Bdd::bddZero());
-        }
-        
-        template<>
-        InternalAdd<DdType::Sylvan, double> InternalDdManager<DdType::Sylvan>::getAddZero() const {
-            return InternalAdd<DdType::Sylvan, double>(this, sylvan::Mtbdd::doubleTerminal(storm::utility::zero<double>()));
-        }
-
-        template<>
-        InternalAdd<DdType::Sylvan, uint_fast64_t> InternalDdManager<DdType::Sylvan>::getAddZero() const {
-            return InternalAdd<DdType::Sylvan, uint_fast64_t>(this, sylvan::Mtbdd::int64Terminal(storm::utility::zero<uint_fast64_t>()));
-        }
-
-#ifdef STORM_HAVE_CARL
-		template<>
-		InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalDdManager<DdType::Sylvan>::getAddZero() const {
-			storm::RationalFunction rationalFunction = storm::utility::zero<storm::RationalFunction>();
-			storm_rational_function_ptr_struct helperStruct;
-			helperStruct.storm_rational_function = (void*)(&rationalFunction);
-			uint64_t value = (uint64_t)&helperStruct;
-
-			return InternalAdd<DdType::Sylvan, storm::RationalFunction>(this, sylvan::Mtbdd::terminal(sylvan_storm_rational_function_get_type(), value));
-		}
-#endif
-        
-        template<>
-        InternalAdd<DdType::Sylvan, double> InternalDdManager<DdType::Sylvan>::getConstant(double const& value) const {
-            return InternalAdd<DdType::Sylvan, double>(this, sylvan::Mtbdd::doubleTerminal(value));
-        }
-
-        template<>
-        InternalAdd<DdType::Sylvan, uint_fast64_t> InternalDdManager<DdType::Sylvan>::getConstant(uint_fast64_t const& value) const {
-            return InternalAdd<DdType::Sylvan, uint_fast64_t>(this, sylvan::Mtbdd::int64Terminal(value));
-        }
-        
-#ifdef STORM_HAVE_CARL
-		template<>
-		InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalDdManager<DdType::Sylvan>::getConstant(storm::RationalFunction const& value) const {
-			return InternalAdd<DdType::Sylvan, storm::RationalFunction>(this, sylvan::Mtbdd::stormRationalFunctionTerminal(value));
-		}
-#endif
-
-        std::pair<InternalBdd<DdType::Sylvan>, InternalBdd<DdType::Sylvan>> InternalDdManager<DdType::Sylvan>::createNewDdVariablePair() {
-            InternalBdd<DdType::Sylvan> first = InternalBdd<DdType::Sylvan>(this, sylvan::Bdd::bddVar(nextFreeVariableIndex));
-            InternalBdd<DdType::Sylvan> second = InternalBdd<DdType::Sylvan>(this, sylvan::Bdd::bddVar(nextFreeVariableIndex + 1));
-            nextFreeVariableIndex += 2;
-            return std::make_pair(first, second);
-        }
-        
-        void InternalDdManager<DdType::Sylvan>::allowDynamicReordering(bool value) {
-            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Operation is not supported by sylvan.");
-        }
-        
-        bool InternalDdManager<DdType::Sylvan>::isDynamicReorderingAllowed() const {
-            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Operation is not supported by sylvan.");
-        }
-        
-        void InternalDdManager<DdType::Sylvan>::triggerReordering() {
-            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Operation is not supported by sylvan.");
-        }
-                
-        template InternalAdd<DdType::Sylvan, double> InternalDdManager<DdType::Sylvan>::getAddOne() const;
-        template InternalAdd<DdType::Sylvan, uint_fast64_t> InternalDdManager<DdType::Sylvan>::getAddOne() const;
-#ifdef STORM_HAVE_CARL
-		template InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalDdManager<DdType::Sylvan>::getAddOne() const;
-#endif
-        
-        template InternalAdd<DdType::Sylvan, double> InternalDdManager<DdType::Sylvan>::getAddZero() const;
-        template InternalAdd<DdType::Sylvan, uint_fast64_t> InternalDdManager<DdType::Sylvan>::getAddZero() const;
-#ifdef STORM_HAVE_CARL
-		template InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalDdManager<DdType::Sylvan>::getAddZero() const;
-#endif
-        
-        template InternalAdd<DdType::Sylvan, double> InternalDdManager<DdType::Sylvan>::getConstant(double const& value) const;
-        template InternalAdd<DdType::Sylvan, uint_fast64_t> InternalDdManager<DdType::Sylvan>::getConstant(uint_fast64_t const& value) const;
-#ifdef STORM_HAVE_CARL
-		template InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalDdManager<DdType::Sylvan>::getConstant(storm::RationalFunction const& value) const;
-#endif
-    }
-}
+#include "src/storage/dd/sylvan/InternalSylvanDdManager.h"
+
+#include <cmath>
+#include <iostream>
+
+#include "src/settings/SettingsManager.h"
+#include "src/settings/modules/SylvanSettings.h"
+
+#include "src/utility/constants.h"
+#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<DdType::Sylvan>::numberOfInstances = 0;
+        
+        // It is important that the variable pairs start at an even offset, because sylvan assumes this to be true for
+        // some operations.
+        uint_fast64_t InternalDdManager<DdType::Sylvan>::nextFreeVariableIndex = 0;
+        
+        uint_fast64_t findLargestPowerOfTwoFitting(uint_fast64_t number) {
+            for (uint_fast64_t index = 0; index < 64; ++index) {
+                if ((number & (1ull << (63 - index))) != 0) {
+                    return 63 - index;
+                }
+            }
+            return 0;
+        }
+        
+        InternalDdManager<DdType::Sylvan>::InternalDdManager() {
+            if (numberOfInstances == 0) {
+                // Initialize lace: auto-detect number of workers.
+                lace_init(storm::settings::getModule<storm::settings::modules::SylvanSettings>().getNumberOfThreads(), 1000000);
+                lace_startup(0, 0, 0);
+                
+                // Each node takes 24 bytes and the maximal memory is specified in megabytes.
+                uint_fast64_t totalNodesToStore = storm::settings::getModule<storm::settings::modules::SylvanSettings>().getMaximalMemory() * 1024 * 1024 / 24;
+                
+                // Compute the power of two that still fits within the total numbers to store.
+                uint_fast64_t powerOfTwo = findLargestPowerOfTwoFitting(totalNodesToStore);
+                
+                sylvan::Sylvan::initPackage(1ull << std::max(16ull, powerOfTwo > 24 ? powerOfTwo - 8 : 0ull), 1ull << (powerOfTwo - 1), 1ull << std::max(16ull, powerOfTwo > 24 ? powerOfTwo - 12 : 0ull), 1ull << (powerOfTwo - 1));
+                sylvan::Sylvan::initBdd(1);
+                sylvan::Sylvan::initMtbdd();
+            }
+            ++numberOfInstances;
+        }
+        
+        InternalDdManager<DdType::Sylvan>::~InternalDdManager() {
+            --numberOfInstances;
+            if (numberOfInstances == 0) {
+                // Enable this to print the sylvan statistics to a file.
+//                FILE* filePointer = fopen("sylvan.stats", "w");
+//                sylvan_stats_report(filePointer, 0);
+//                fclose(filePointer);
+                
+                sylvan::Sylvan::quitPackage();
+                lace_exit();
+            }
+        }
+        
+        InternalBdd<DdType::Sylvan> InternalDdManager<DdType::Sylvan>::getBddOne() const {
+            return InternalBdd<DdType::Sylvan>(this, sylvan::Bdd::bddOne());
+        }
+        
+        template<>
+        InternalAdd<DdType::Sylvan, double> InternalDdManager<DdType::Sylvan>::getAddOne() const {
+            return InternalAdd<DdType::Sylvan, double>(this, sylvan::Mtbdd::doubleTerminal(storm::utility::one<double>()));
+        }
+
+        template<>
+        InternalAdd<DdType::Sylvan, uint_fast64_t> InternalDdManager<DdType::Sylvan>::getAddOne() const {
+            return InternalAdd<DdType::Sylvan, uint_fast64_t>(this, sylvan::Mtbdd::int64Terminal(storm::utility::one<uint_fast64_t>()));
+        }
+
+#ifdef STORM_HAVE_CARL
+		template<>
+		InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalDdManager<DdType::Sylvan>::getAddOne() const {
+			return InternalAdd<DdType::Sylvan, storm::RationalFunction>(this, sylvan::Mtbdd::stormRationalFunctionTerminal(storm::utility::one<storm::RationalFunction>()));
+		}
+#endif
+        
+        InternalBdd<DdType::Sylvan> InternalDdManager<DdType::Sylvan>::getBddZero() const {
+            return InternalBdd<DdType::Sylvan>(this, sylvan::Bdd::bddZero());
+        }
+        
+        template<>
+        InternalAdd<DdType::Sylvan, double> InternalDdManager<DdType::Sylvan>::getAddZero() const {
+            return InternalAdd<DdType::Sylvan, double>(this, sylvan::Mtbdd::doubleTerminal(storm::utility::zero<double>()));
+        }
+
+        template<>
+        InternalAdd<DdType::Sylvan, uint_fast64_t> InternalDdManager<DdType::Sylvan>::getAddZero() const {
+            return InternalAdd<DdType::Sylvan, uint_fast64_t>(this, sylvan::Mtbdd::int64Terminal(storm::utility::zero<uint_fast64_t>()));
+        }
+
+#ifdef STORM_HAVE_CARL
+		template<>
+		InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalDdManager<DdType::Sylvan>::getAddZero() const {
+			return InternalAdd<DdType::Sylvan, storm::RationalFunction>(this, sylvan::Mtbdd::stormRationalFunctionTerminal(storm::utility::zero<storm::RationalFunction>()));
+		}
+#endif
+        
+        template<>
+        InternalAdd<DdType::Sylvan, double> InternalDdManager<DdType::Sylvan>::getConstant(double const& value) const {
+            return InternalAdd<DdType::Sylvan, double>(this, sylvan::Mtbdd::doubleTerminal(value));
+        }
+
+        template<>
+        InternalAdd<DdType::Sylvan, uint_fast64_t> InternalDdManager<DdType::Sylvan>::getConstant(uint_fast64_t const& value) const {
+            return InternalAdd<DdType::Sylvan, uint_fast64_t>(this, sylvan::Mtbdd::int64Terminal(value));
+        }
+        
+#ifdef STORM_HAVE_CARL
+		template<>
+		InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalDdManager<DdType::Sylvan>::getConstant(storm::RationalFunction const& value) const {
+			return InternalAdd<DdType::Sylvan, storm::RationalFunction>(this, sylvan::Mtbdd::stormRationalFunctionTerminal(value));
+		}
+#endif
+
+        std::pair<InternalBdd<DdType::Sylvan>, InternalBdd<DdType::Sylvan>> InternalDdManager<DdType::Sylvan>::createNewDdVariablePair() {
+            InternalBdd<DdType::Sylvan> first = InternalBdd<DdType::Sylvan>(this, sylvan::Bdd::bddVar(nextFreeVariableIndex));
+            InternalBdd<DdType::Sylvan> second = InternalBdd<DdType::Sylvan>(this, sylvan::Bdd::bddVar(nextFreeVariableIndex + 1));
+            nextFreeVariableIndex += 2;
+            return std::make_pair(first, second);
+        }
+        
+        void InternalDdManager<DdType::Sylvan>::allowDynamicReordering(bool value) {
+            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Operation is not supported by sylvan.");
+        }
+        
+        bool InternalDdManager<DdType::Sylvan>::isDynamicReorderingAllowed() const {
+            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Operation is not supported by sylvan.");
+        }
+        
+        void InternalDdManager<DdType::Sylvan>::triggerReordering() {
+            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Operation is not supported by sylvan.");
+        }
+                
+        template InternalAdd<DdType::Sylvan, double> InternalDdManager<DdType::Sylvan>::getAddOne() const;
+        template InternalAdd<DdType::Sylvan, uint_fast64_t> InternalDdManager<DdType::Sylvan>::getAddOne() const;
+#ifdef STORM_HAVE_CARL
+		template InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalDdManager<DdType::Sylvan>::getAddOne() const;
+#endif
+        
+        template InternalAdd<DdType::Sylvan, double> InternalDdManager<DdType::Sylvan>::getAddZero() const;
+        template InternalAdd<DdType::Sylvan, uint_fast64_t> InternalDdManager<DdType::Sylvan>::getAddZero() const;
+#ifdef STORM_HAVE_CARL
+		template InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalDdManager<DdType::Sylvan>::getAddZero() const;
+#endif
+        
+        template InternalAdd<DdType::Sylvan, double> InternalDdManager<DdType::Sylvan>::getConstant(double const& value) const;
+        template InternalAdd<DdType::Sylvan, uint_fast64_t> InternalDdManager<DdType::Sylvan>::getConstant(uint_fast64_t const& value) const;
+#ifdef STORM_HAVE_CARL
+		template InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalDdManager<DdType::Sylvan>::getConstant(storm::RationalFunction const& value) const;
+#endif
+    }
+}

test/functional/storage/SylvanDdTest.cpp

@@ -142,26 +142,25 @@ TEST(SylvanDd, RationalFunctionIdentityTest) {
     EXPECT_EQ(10ul, identity.getLeafCount());
     EXPECT_EQ(21ul, identity.getNodeCount());
 }
-
 #endif
 
 TEST(SylvanDd, RangeTest) {
     std::shared_ptr<storm::dd::DdManager<storm::dd::DdType::Sylvan>> manager(new storm::dd::DdManager<storm::dd::DdType::Sylvan>());
     std::pair<storm::expressions::Variable, storm::expressions::Variable> x;
     ASSERT_NO_THROW(x = manager->addMetaVariable("x", 1, 9));
-    
+
     storm::dd::Bdd<storm::dd::DdType::Sylvan> range;
     ASSERT_NO_THROW(range = manager->getRange(x.first));
-    
+ 
     EXPECT_EQ(9ul, range.getNonZeroCount());
     EXPECT_EQ(1ul, range.getLeafCount());
     EXPECT_EQ(5ul, range.getNodeCount());
 }
 
-TEST(SylvanDd, IdentityTest) {
+TEST(SylvanDd, DoubleIdentityTest) {
     std::shared_ptr<storm::dd::DdManager<storm::dd::DdType::Sylvan>> manager(new storm::dd::DdManager<storm::dd::DdType::Sylvan>());
     std::pair<storm::expressions::Variable, storm::expressions::Variable> x = manager->addMetaVariable("x", 1, 9);
-    
+
     storm::dd::Add<storm::dd::DdType::Sylvan, double> identity;
     ASSERT_NO_THROW(identity = manager->getIdentity<double>(x.first));
 
@@ -170,6 +169,18 @@ TEST(SylvanDd, IdentityTest) {
     EXPECT_EQ(21ul, identity.getNodeCount());
 }
 
+TEST(SylvanDd, UintIdentityTest) {
+    std::shared_ptr<storm::dd::DdManager<storm::dd::DdType::Sylvan>> manager(new storm::dd::DdManager<storm::dd::DdType::Sylvan>());
+    std::pair<storm::expressions::Variable, storm::expressions::Variable> x = manager->addMetaVariable("x", 1, 9);
+
+    storm::dd::Add<storm::dd::DdType::Sylvan, uint_fast64_t> identity;
+    ASSERT_NO_THROW(identity = manager->getIdentity<uint_fast64_t>(x.first));
+
+    EXPECT_EQ(9ul, identity.getNonZeroCount());
+    EXPECT_EQ(10ul, identity.getLeafCount());
+    EXPECT_EQ(21ul, identity.getNodeCount());
+}
+
 TEST(SylvanDd, OperatorTest) {
     std::shared_ptr<storm::dd::DdManager<storm::dd::DdType::Sylvan>> manager(new storm::dd::DdManager<storm::dd::DdType::Sylvan>());
     std::pair<storm::expressions::Variable, storm::expressions::Variable> x = manager->addMetaVariable("x", 1, 9);