Merge branch 'mergeMenuGamesWithRationalFunction' into menu_games

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

@@ -5,6 +5,8 @@
 #include <sstream>
 #include <set>
 #include <map>
+#include <mutex>
+
 #include "storm/adapters/CarlAdapter.h"
 #include "sylvan_storm_rational_function.h"
 
@@ -13,224 +15,267 @@
 #include <sylvan_common.h>
 #include <sylvan_mtbdd.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
+std::mutex carlMutex;
 
 void storm_rational_function_init(storm_rational_function_ptr* a) {
-	LOG_I("init")
-#ifdef DEBUG_STORM_FUNCTION_WRAPPER
-	std::cout << "storm_rational_function_init - ptr of old = " << *a << ", value = " << *((storm::RationalFunction*)(*a)) << std::endl;
-#endif
-	storm_rational_function_ptr srf_ptr = new storm::RationalFunction(*((storm::RationalFunction*)(*a)));
+	std::lock_guard<std::mutex> lock(carlMutex);
+	{
+		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;
+		}
 	
-	if (srf_ptr == nullptr) {
-		std::cerr << "Could not allocate memory in storm_rational_function_init()!" << std::endl;
-		return;
+		*a = srf_ptr;
 	}
-
-	*a = srf_ptr;
-#ifdef DEBUG_STORM_FUNCTION_WRAPPER
-	std::cout << "storm_rational_function_init - ptr of new = " << *a << ", value = " << *((storm::RationalFunction*)(*a)) << std::endl;
-#endif
-	LOG_O("init")
 }
 
 void storm_rational_function_destroy(storm_rational_function_ptr a) {
-	LOG_I("destroy")
-	delete (storm::RationalFunction*)a;
-	LOG_O("destroy")
+	std::lock_guard<std::mutex> lock(carlMutex);
+	{
+		storm::RationalFunction* srf = (storm::RationalFunction*)a;
+		delete srf;
+	}
 }
 
 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")
-	
+	std::lock_guard<std::mutex> lock(carlMutex);
 	int result = 0;
-	if (srf_a == srf_b) {
-		result = 1;
-	}
+	{
+		storm::RationalFunction& srf_a = *(storm::RationalFunction*)a;
+		storm::RationalFunction& srf_b = *(storm::RationalFunction*)b;
 
-#ifdef DEBUG_STORM_FUNCTION_WRAPPER
-	std::cout << "storm_rational_function_equals called with ptr = " << a << " value a = " << srf_a << " and ptr = " << b << " value b = " << srf_b << " result = " << result << "." << std::endl;
-#endif
+		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;
+	std::lock_guard<std::mutex> lock(carlMutex);
+	storm_rational_function_ptr result = (storm_rational_function_ptr)nullptr;
 
-	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;
-	}
+	{
+		storm::RationalFunction& srf_a = *(storm::RationalFunction*)a;
+		storm::RationalFunction& srf_b = *(storm::RationalFunction*)b;
 	
-	*result_srf += srf_b;
-
-	storm_rational_function_ptr result = (storm_rational_function_ptr)result_srf;
+		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 result;
+		}
+		
+		*result_srf += srf_b;
+		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;
+	std::lock_guard<std::mutex> lock(carlMutex);
+	storm_rational_function_ptr result = (storm_rational_function_ptr)nullptr;
 
-	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;
-	}
+	{
+		storm::RationalFunction& srf_a = *(storm::RationalFunction*)a;
+		storm::RationalFunction& srf_b = *(storm::RationalFunction*)b;
 	
-	*result_srf -= srf_b;
-
-	storm_rational_function_ptr result = (storm_rational_function_ptr)result_srf;
-
-	LOG_O("minus")
+		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 result;
+		}
+		
+		*result_srf -= srf_b;
+		result = (storm_rational_function_ptr)result_srf;
+	}
 	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;
+	std::lock_guard<std::mutex> lock(carlMutex);
+	storm_rational_function_ptr result = (storm_rational_function_ptr)nullptr;
 
-	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;
-	}
+	{
+		storm::RationalFunction& srf_a = *(storm::RationalFunction*)a;
+		storm::RationalFunction& srf_b = *(storm::RationalFunction*)b;
 	
-	*result_srf *= srf_b;
-
-	storm_rational_function_ptr result = (storm_rational_function_ptr)result_srf;
-
-	LOG_O("times")
+		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 result;
+		}
+		
+		*result_srf *= srf_b;
+		result = (storm_rational_function_ptr)result_srf;
+	}
 	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;
+	std::lock_guard<std::mutex> lock(carlMutex);
+	storm_rational_function_ptr result = (storm_rational_function_ptr)nullptr;
 
-	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;
-	}
+	{
+		storm::RationalFunction& srf_a = *(storm::RationalFunction*)a;
+		storm::RationalFunction& srf_b = *(storm::RationalFunction*)b;
 	
-	*result_srf /= srf_b;
-
-	storm_rational_function_ptr result = (storm_rational_function_ptr)result_srf;
-
-	LOG_O("divide")
+		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 result;
+		}
+		
+		*result_srf /= srf_b;
+		result = (storm_rational_function_ptr)result_srf;
+	}
 	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);
-
-#ifdef DEBUG_STORM_FUNCTION_WRAPPER
-	std::cout << "storm_rational_function_hash of value " << srf_a << " is " << hash << std::endl;
-#endif
-
-	uint64_t result = hash ^ seed;
-
-	LOG_O("hash")
+	std::lock_guard<std::mutex> lock(carlMutex);
+	
+	uint64_t result = 0;
+	{
+		storm::RationalFunction& srf_a = *(storm::RationalFunction*)a;
+		size_t hash = carl::hash_value(srf_a);
+	
+		result = hash ^ seed;
+	}
 	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;
+	std::lock_guard<std::mutex> lock(carlMutex);
+	storm_rational_function_ptr result = (storm_rational_function_ptr)nullptr;
 
-	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;
-	}
+	{
+		storm::RationalFunction& srf_a = *(storm::RationalFunction*)a;
 	
-	*result_srf = -srf_a;
-
-	storm_rational_function_ptr result = (storm_rational_function_ptr)result_srf;
-
-	LOG_O("negate")
+		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 result;
+		}
+		
+		*result_srf = -srf_a;
+		result = (storm_rational_function_ptr)result_srf;
+	}
 	return result;
 }
 
 int storm_rational_function_is_zero(storm_rational_function_ptr a) {
-	LOG_I("isZero")
-	storm::RationalFunction& srf_a = *(storm::RationalFunction*)a;
+	std::lock_guard<std::mutex> lock(carlMutex);
 
-	if (srf_a.isZero()) {
+	bool resultIsZero = false;
+	{
+		storm::RationalFunction& srf_a = *(storm::RationalFunction*)a;
+		resultIsZero = srf_a.isZero();
+	}
+
+	if (resultIsZero) {
 		return 1;
 	} else {
 		return 0;
 	}
 }
 
+double storm_rational_function_get_constant(storm_rational_function_ptr a) {
+	std::lock_guard<std::mutex> lock(carlMutex);
+
+	double result = -1.0;
+	{
+		storm::RationalFunction& srf_a = *(storm::RationalFunction*)a;
+	
+		if (srf_a.isConstant()) {
+			result = carl::toDouble(storm::RationalNumber(srf_a.nominatorAsNumber() / srf_a.denominatorAsNumber()));
+		} else {
+			std::cout << "Defaulting to -1.0 since this is not a constant: " << srf_a << std::endl;
+		}
+	}
+	return result;
+}
+
 storm_rational_function_ptr storm_rational_function_get_zero() {
-	static storm::RationalFunction zeroFunction(0);
-	LOG_I("getZero")
-	return (storm_rational_function_ptr)(&zeroFunction);
+	std::lock_guard<std::mutex> lock(carlMutex);
+	storm_rational_function_ptr result = (storm_rational_function_ptr)nullptr;
+
+	{
+		storm::RationalFunction* result_srf = new storm::RationalFunction(0);
+		if (result_srf == nullptr) {
+			std::cerr << "Could not allocate memory in storm_rational_function_get_zero()!" << std::endl;
+			return result;
+		}
+		result = (storm_rational_function_ptr)result_srf;
+	}
+	
+	return result;
 }
 
 storm_rational_function_ptr storm_rational_function_get_one() {
-	static storm::RationalFunction oneFunction(1);
-	LOG_I("getOne")
-	return (storm_rational_function_ptr)(&oneFunction);
+	std::lock_guard<std::mutex> lock(carlMutex);
+	storm_rational_function_ptr result = (storm_rational_function_ptr)nullptr;
+
+	{
+		storm::RationalFunction* result_srf = new storm::RationalFunction(1);
+		if (result_srf == nullptr) {
+			std::cerr << "Could not allocate memory in storm_rational_function_get_one()!" << std::endl;
+			return result;
+		}
+		result = (storm_rational_function_ptr)result_srf;
+	}
+	
+	return result;
 }
 
 void print_storm_rational_function(storm_rational_function_ptr a) {
-	storm::RationalFunction& srf_a = *(storm::RationalFunction*)a;
-	std::cout << srf_a << std::flush;
+	std::lock_guard<std::mutex> lock(carlMutex);
+	{
+		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());
+	std::lock_guard<std::mutex> lock(carlMutex);
+	{
+		std::stringstream ss;
+		storm::RationalFunction& srf_a = *(storm::RationalFunction*)a;
+		ss << srf_a;
+		std::string s = ss.str();
+		fprintf(out, "%s", s.c_str());
+	}
 }
 
-MTBDD testiTest(storm::RationalFunction const& currentFunction, std::map<storm::RationalFunctionVariable, std::pair<uint32_t, std::pair<storm::RationalNumber, storm::RationalNumber>>> const& replacements) {
+MTBDD testiTest(storm::RationalFunction const& currentFunction, std::map<uint32_t, std::pair<storm::RationalFunctionVariable, std::pair<storm::RationalNumber, storm::RationalNumber>>> const& replacements) {
 	if (currentFunction.isConstant()) {
 		return mtbdd_storm_rational_function((storm_rational_function_ptr)&currentFunction);
 	}
 
 	std::set<storm::RationalFunctionVariable> variablesInFunction = currentFunction.gatherVariables();
-	std::map<storm::RationalFunctionVariable, std::pair<uint32_t, std::pair<storm::RationalNumber, storm::RationalNumber>>>::const_iterator it = replacements.cbegin();
-	std::map<storm::RationalFunctionVariable, std::pair<uint32_t, std::pair<storm::RationalNumber, storm::RationalNumber>>>::const_iterator end = replacements.cend();
+	std::map<uint32_t, std::pair<storm::RationalFunctionVariable, std::pair<storm::RationalNumber, storm::RationalNumber>>>::const_iterator it = replacements.cbegin();
+	std::map<uint32_t, std::pair<storm::RationalFunctionVariable, std::pair<storm::RationalNumber, storm::RationalNumber>>>::const_iterator end = replacements.cend();
 
 	// Walking the (ordered) map enforces an ordering on the MTBDD
 	for (; it != end; ++it) {
-		if (variablesInFunction.find(it->first) != variablesInFunction.cend()) {
-			std::map<storm::RationalFunctionVariable, storm::RationalNumber> highReplacement = {{it->first, it->second.second.first}};
-			std::map<storm::RationalFunctionVariable, storm::RationalNumber> lowReplacement = {{it->first, it->second.second.second}};
-			MTBDD high = testiTest(currentFunction.substitute(highReplacement), replacements);
-			MTBDD low = testiTest(currentFunction.substitute(lowReplacement), replacements);
+		if (variablesInFunction.find(it->second.first) != variablesInFunction.cend()) {
+			std::map<storm::RationalFunctionVariable, storm::RationalNumber> highReplacement = {{it->second.first, it->second.second.first}};
+			std::map<storm::RationalFunctionVariable, storm::RationalNumber> lowReplacement = {{it->second.first, it->second.second.second}};
+
+			std::lock_guard<std::mutex>* lock = new std::lock_guard<std::mutex>(carlMutex);
+			storm::RationalFunction const highSrf = currentFunction.substitute(highReplacement);
+			storm::RationalFunction const lowSrf = currentFunction.substitute(lowReplacement);
+			delete lock;
+			
+			MTBDD high = testiTest(highSrf, replacements);
+			MTBDD low = testiTest(lowSrf, replacements);
 			LACE_ME
-			return mtbdd_ite(mtbdd_ithvar(it->second.first), high, low);
+			return mtbdd_ite(mtbdd_ithvar(it->first), high, low);
+		} else {
+			//std::cout << "No match for variable " << it->second.first << std::endl;
 		}
 	}
 
@@ -238,12 +283,16 @@ MTBDD testiTest(storm::RationalFunction const& currentFunction, std::map<storm::
 }
 
 
-MTBDD storm_rational_function_leaf_parameter_replacement(MTBDD dd, storm_rational_function_ptr a, void* context) {
+MTBDD storm_rational_function_leaf_parameter_replacement(MTBDD dd, storm_rational_function_ptr a, void* context) {	
 	storm::RationalFunction& srf_a = *(storm::RationalFunction*)a;
-	if (srf_a.isConstant()) {
-		return dd;
+	{
+		// Scope the lock.
+		std::lock_guard<std::mutex> lock(carlMutex);
+		if (srf_a.isConstant()) {
+			return dd;
+		}
 	}
 	
-	std::map<storm::RationalFunctionVariable, std::pair<uint32_t, std::pair<storm::RationalNumber, storm::RationalNumber>>>* replacements = (std::map<storm::RationalFunctionVariable, std::pair<uint32_t, std::pair<storm::RationalNumber, storm::RationalNumber>>>*)context;
+	std::map<uint32_t, std::pair<storm::RationalFunctionVariable, std::pair<storm::RationalNumber, storm::RationalNumber>>>* replacements = (std::map<uint32_t, std::pair<storm::RationalFunctionVariable, std::pair<storm::RationalNumber, storm::RationalNumber>>>*)context;
 	return testiTest(srf_a, *replacements);
 }

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

@@ -33,6 +33,8 @@ int storm_rational_function_is_zero(storm_rational_function_ptr a);
 
 MTBDD storm_rational_function_leaf_parameter_replacement(MTBDD dd, storm_rational_function_ptr a, void* context);
 
+double storm_rational_function_get_constant(storm_rational_function_ptr a);
+
 #ifdef __cplusplus
 }
 #endif

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

@@ -32,6 +32,8 @@
 	Mtbdd AbstractPlusRF(const BddSet &variables) const;
 	
 	Mtbdd ReplaceLeavesRF(void* context) const;
+	
+	Mtbdd ToDoubleRF() const;
 #endif
 	
 	/**

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

@@ -23,6 +23,12 @@ Bdd::toStormRationalFunctionMtbdd() const {
     return mtbdd_bool_to_storm_rational_function(bdd);
 }
 
+Mtbdd 
+Mtbdd::ToDoubleRF() const {
+    LACE_ME;
+    return sylvan_storm_rational_function_to_double(mtbdd);
+}
+
 Mtbdd
 Mtbdd::PlusRF(const Mtbdd &other) const
 {

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

@@ -205,7 +205,7 @@ TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_plus, MTBDD*, pa, MTBDD*, p
 		storm_rational_function_ptr mres = storm_rational_function_plus(ma, mb);
         MTBDD res = mtbdd_storm_rational_function(mres);
         
-		// TODO: Delete mres?
+		storm_rational_function_destroy(mres);
 
         return res;
     }
@@ -240,7 +240,7 @@ TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_minus, MTBDD*, pa, MTBDD*,
 		storm_rational_function_ptr mres = storm_rational_function_minus(ma, mb);
 		MTBDD res = mtbdd_storm_rational_function(mres);
 
-		// TODO: Delete mres?
+		storm_rational_function_destroy(mres);
 
         return res;
     }
@@ -273,7 +273,7 @@ TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_times, MTBDD*, pa, MTBDD*,
 		storm_rational_function_ptr mres = storm_rational_function_times(ma, mb);		
 		MTBDD res = mtbdd_storm_rational_function(mres);
 
-		// TODO: Delete mres?
+		storm_rational_function_destroy(mres);
 
         return res;
     }
@@ -307,7 +307,7 @@ TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_divide, MTBDD*, pa, MTBDD*,
 		storm_rational_function_ptr mres = storm_rational_function_divide(ma, mb);
 		MTBDD res = mtbdd_storm_rational_function(mres);
 
-		// TODO: Delete mres?
+		storm_rational_function_destroy(mres);
 
         return res;
     }
@@ -369,7 +369,8 @@ TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_neg, MTBDD, dd, size_t, p)
 		storm_rational_function_ptr mres = storm_rational_function_negate(mdd);
 		MTBDD res = mtbdd_storm_rational_function(mres);
 
-		// TODO: Delete mres?
+		storm_rational_function_destroy(mres);
+
         return res;
     }
 
@@ -398,6 +399,30 @@ TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_replace_leaves, MTBDD, dd,
 
     return mtbdd_invalid;
 }
+/**
+ * Operation to double for one storm::RationalFunction MTBDD
+ */
+TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_to_double, MTBDD, dd, size_t, p)
+{
+	LOG_I("task_impl_2 op_toDouble")
+    /* Handle partial functions */
+    if (dd == mtbdd_false) return mtbdd_false;
+
+    /* Compute result for leaf */
+    if (mtbdd_isleaf(dd)) {
+		if (mtbdd_gettype(dd) != sylvan_storm_rational_function_type) {
+			printf("Can not convert to double, this has type %u!\n", mtbdd_gettype(dd));
+			assert(0);
+		}
+
+		storm_rational_function_ptr mdd = (storm_rational_function_ptr)mtbdd_getvalue(dd);
+		MTBDD result = mtbdd_double(storm_rational_function_get_constant(mdd));
+		return result;
+    }
+
+    return mtbdd_invalid;
+	(void)p;
+}
 
 /**
  * Multiply <a> and <b>, and abstract variables <vars> using summation.
@@ -477,3 +502,40 @@ TASK_IMPL_3(MTBDD, sylvan_storm_rational_function_and_exists, MTBDD, a, MTBDD, b
     cache_put3(CACHE_STORM_RATIONAL_FUNCTION_AND_EXISTS, a, b, v, result);
     return result;
 }
+
+/**
+ * Apply a unary operation <op> to <dd>.
+ */
+TASK_IMPL_3(MTBDD, mtbdd_uapply_nocache, MTBDD, dd, mtbdd_uapply_op, op, size_t, param)
+{
+    /* Maybe perform garbage collection */
+    sylvan_gc_test();
+
+    /* Check cache */
+    MTBDD result;
+    //if (cache_get3(CACHE_MTBDD_UAPPLY, dd, (size_t)op, param, &result)) return result;
+
+    /* Check terminal case */
+    result = WRAP(op, dd, param);
+    if (result != mtbdd_invalid) {
+        /* Store in cache */
+        //cache_put3(CACHE_MTBDD_UAPPLY, dd, (size_t)op, param, result);
+        return result;
+    }
+
+    /* Get cofactors */
+    mtbddnode_t ndd = MTBDD_GETNODE(dd);
+    MTBDD ddlow = node_getlow(dd, ndd);
+    MTBDD ddhigh = node_gethigh(dd, ndd);
+
+    /* Recursive */
+    mtbdd_refs_spawn(SPAWN(mtbdd_uapply_nocache, ddhigh, op, param));
+    MTBDD low = mtbdd_refs_push(CALL(mtbdd_uapply_nocache, ddlow, op, param));
+    MTBDD high = mtbdd_refs_sync(SYNC(mtbdd_uapply_nocache));
+    mtbdd_refs_pop(1);
+    result = mtbdd_makenode(mtbddnode_getvariable(ndd), low, high);
+
+    /* Store in cache */
+    //cache_put3(CACHE_MTBDD_UAPPLY, dd, (size_t)op, param, result);
+    return result;
+}

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

@@ -104,14 +104,16 @@ TASK_DECL_3(MTBDD, sylvan_storm_rational_function_and_exists, MTBDD, MTBDD, MTBD
  */
 #define sylvan_storm_rational_function_abstract_plus(dd, v) mtbdd_abstract(dd, v, TASK(sylvan_storm_rational_function_abstract_op_plus))
 
+/**
+ * Apply a unary operation <op> to <dd>.
+ * Callback <op> is consulted after the cache, thus the application to a terminal is cached.
+ */
+TASK_DECL_3(MTBDD, mtbdd_uapply_nocache, MTBDD, mtbdd_uapply_op, size_t);
+#define mtbdd_uapply_nocache(dd, op, param) CALL(mtbdd_uapply_nocache, dd, op, param)
+
 /**
  * Functionality regarding the replacement of leaves in MTBDDs.
- *
- * uint64_t mtbdd_getvalue
- * uint32_t mtbdd_gettype
- * void* custom context ptr
  */
-typedef MTBDD (*mtbddLeaveReplacementFunction)(uint64_t, uint32_t, void*);
 
 /**
  * Operation "replace" for one storm::RationalFunction MTBDD
@@ -121,7 +123,17 @@ TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_replace_leaves, MTBDD, size
 /**
  * Compute the MTBDD that arises from a after calling the mtbddLeaveReplacementFunction on each leaf.
  */
-#define sylvan_storm_rational_function_replace_leaves(a, ctx) mtbdd_uapply(a, TASK(sylvan_storm_rational_function_op_replace_leaves), ctx)
+#define sylvan_storm_rational_function_replace_leaves(a, ctx) mtbdd_uapply_nocache(a, TASK(sylvan_storm_rational_function_op_replace_leaves), ctx)
+
+/**
+ * Takes a storm::RationalFunction MTBDD and transforms it into a double MTBDD
+ */
+TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_to_double, MTBDD, size_t)
+
+/**
+ * Compute the MTBDD that arises from a after calling the mtbddLeaveReplacementFunction on each leaf.
+ */
+#define sylvan_storm_rational_function_to_double(a) mtbdd_uapply_nocache(a, TASK(sylvan_storm_rational_function_op_to_double), 0)
 
 #ifdef __cplusplus
 }

src/storm/storage/dd/Add.cpp

@@ -791,10 +791,18 @@ namespace storm {
 		}
 
 		template<>
-        Add<storm::dd::DdType::Sylvan, storm::RationalFunction> Add<storm::dd::DdType::Sylvan, storm::RationalFunction>::replaceLeaves(std::map<storm::RationalFunctionVariable, std::pair<storm::expressions::Variable, std::pair<storm::RationalNumber, storm::RationalNumber>>> const& replacementMap) const {
-			std::map<storm::RationalFunctionVariable, std::pair<uint32_t, std::pair<storm::RationalNumber, storm::RationalNumber>>> internalReplacementMap;
+		Add<storm::dd::DdType::Sylvan, storm::RationalFunction> Add<storm::dd::DdType::Sylvan, storm::RationalFunction>::replaceLeaves(std::map<storm::RationalFunctionVariable, std::pair<storm::expressions::Variable, std::pair<storm::RationalNumber, storm::RationalNumber>>> const& replacementMap) const {
+			std::map<uint32_t, std::pair<storm::RationalFunctionVariable, std::pair<storm::RationalNumber, storm::RationalNumber>>> internalReplacementMap;
 			std::set<storm::expressions::Variable> containedMetaVariables = this->getContainedMetaVariables();
 			
+			uint32_t highestIndex = 0;
+			for (storm::expressions::Variable const& var: containedMetaVariables) {
+				uint32_t index = this->getDdManager().getMetaVariable(var).getDdVariables().at(0).getIndex();
+				if (index > highestIndex) {
+					highestIndex = index;
+				}
+			}
+			
 			std::map<storm::RationalFunctionVariable, std::pair<storm::expressions::Variable, std::pair<storm::RationalNumber, storm::RationalNumber>>>::const_iterator it = replacementMap.cbegin();
 			std::map<storm::RationalFunctionVariable, std::pair<storm::expressions::Variable, std::pair<storm::RationalNumber, storm::RationalNumber>>>::const_iterator end = replacementMap.cend();
 			
@@ -803,13 +811,24 @@ namespace storm {
 				STORM_LOG_THROW(metaVariable.getNumberOfDdVariables() == 1, storm::exceptions::InvalidArgumentException, "Cannot use MetaVariable with more then one internal DD variable.");
 				
 				auto const& ddVariable = metaVariable.getDdVariables().at(0);
+				STORM_LOG_ASSERT(ddVariable.getIndex() > highestIndex, "Can not replace leaves with DD variable that would not be at the bottom!");
 				
-				internalReplacementMap.insert(std::make_pair(it->first, std::make_pair(ddVariable.getIndex(), it->second.second)));
+				internalReplacementMap.insert(std::make_pair(ddVariable.getIndex(), std::make_pair(it->first, it->second.second)));
 				containedMetaVariables.insert(it->second.first);
 			}
 			
 			return Add<storm::dd::DdType::Sylvan, storm::RationalFunction>(this->getDdManager(), internalAdd.replaceLeaves(internalReplacementMap), containedMetaVariables);
 		}
+		
+		template<DdType LibraryType, typename ValueType>
+		Add<LibraryType, double> Add<LibraryType, ValueType>::toDouble() const {
+			STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Not yet implemented: replaceLeaves");
+		}
+
+		template<>
+		Add<storm::dd::DdType::Sylvan, double> Add<storm::dd::DdType::Sylvan, storm::RationalFunction>::toDouble() const {
+			return Add<storm::dd::DdType::Sylvan, double>(this->getDdManager(), internalAdd.toDouble(), this->getContainedMetaVariables());
+		}
 #endif
 		
         template class Add<storm::dd::DdType::CUDD, double>;

src/storm/storage/dd/Add.h

@@ -254,6 +254,13 @@ namespace storm {
              * @return The resulting function represented as an ADD.
              */
             Add<LibraryType, ValueType> replaceLeaves(std::map<storm::RationalFunctionVariable, std::pair<storm::expressions::Variable, std::pair<storm::RationalNumber, storm::RationalNumber>>> const& replacementMap) const;
+			
+			/*!
+             * Replaces the leaves in this MTBDD, converting them to double if possible, and -1.0 else.
+             *
+             * @return The resulting function represented as an ADD.
+             */
+            Add<LibraryType, double> toDouble() const;
 #endif
 			
             /*!

src/storm/storage/dd/DdManager.cpp

@@ -234,6 +234,14 @@ namespace storm {
         bool DdManager<LibraryType>::hasMetaVariable(std::string const& metaVariableName) const {
             return manager->hasVariable(metaVariableName);
         }
+
+		template<DdType LibraryType>
+		storm::expressions::Variable DdManager<LibraryType>::getMetaVariable(std::string const& metaVariableName) const {
+			// Check whether the meta variable exists.
+			STORM_LOG_THROW(hasMetaVariable(metaVariableName), storm::exceptions::InvalidArgumentException, "Unknown meta variable name '" << metaVariableName << "'.");
+			
+			return manager->getVariable(metaVariableName);
+		}
         
         template<DdType LibraryType>
         bool DdManager<LibraryType>::supportsOrderedInsertion() const {

src/storm/storage/dd/DdManager.h

@@ -163,6 +163,14 @@ namespace storm {
              * @return True if the given meta variable name is managed by this manager.
              */
             bool hasMetaVariable(std::string const& variableName) const;
+			
+			/*!
+             * Retrieves the given meta variable by name.
+             *
+             * @param variableName The name of the variable.
+             * @return The meta variable.
+             */
+            storm::expressions::Variable getMetaVariable(std::string const& variableName) const;
             
             /*!
              * Checks whether this manager supports the ordered insertion of variables, i.e. inserting variables at

src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp

@@ -290,17 +290,28 @@ namespace storm {
 #endif
 
         template<typename ValueType>
-        InternalAdd<DdType::Sylvan, ValueType> InternalAdd<DdType::Sylvan, ValueType>::replaceLeaves(std::map<storm::RationalFunctionVariable, std::pair<uint32_t, std::pair<storm::RationalNumber, storm::RationalNumber>>> const& replacementMap) const {
+        InternalAdd<DdType::Sylvan, ValueType> InternalAdd<DdType::Sylvan, ValueType>::replaceLeaves(std::map<uint32_t, std::pair<storm::RationalFunctionVariable, std::pair<storm::RationalNumber, storm::RationalNumber>>> const& replacementMap) const {
             STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: replaceLeaves");
         }
 
 #ifdef STORM_HAVE_CARL
 		template<>
-        InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalAdd<DdType::Sylvan, storm::RationalFunction>::replaceLeaves(std::map<storm::RationalFunctionVariable, std::pair<uint32_t, std::pair<storm::RationalNumber, storm::RationalNumber>>> const& replacementMap) const {
+        InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalAdd<DdType::Sylvan, storm::RationalFunction>::replaceLeaves(std::map<uint32_t, std::pair<storm::RationalFunctionVariable, std::pair<storm::RationalNumber, storm::RationalNumber>>> const& replacementMap) const {
             return InternalAdd<DdType::Sylvan, storm::RationalFunction>(ddManager, this->sylvanMtbdd.ReplaceLeavesRF((void*)&replacementMap));
         }
 #endif
 
+        template<typename ValueType>
+        InternalAdd<DdType::Sylvan, double> InternalAdd<DdType::Sylvan, ValueType>::toDouble() const {
+            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: toDouble");
+        }
+
+#ifdef STORM_HAVE_CARL
+		template<>
+        InternalAdd<DdType::Sylvan, double> InternalAdd<DdType::Sylvan, storm::RationalFunction>::toDouble() const {
+            return InternalAdd<DdType::Sylvan, double>(ddManager, this->sylvanMtbdd.ToDoubleRF());
+        }
+#endif
 
         template<typename ValueType>
         InternalAdd<DdType::Sylvan, ValueType> InternalAdd<DdType::Sylvan, ValueType>::sumAbstract(InternalBdd<DdType::Sylvan> const& cube) const {

src/storm/storage/dd/sylvan/InternalSylvanAdd.h

@@ -255,7 +255,14 @@ namespace storm {
              * @param replacementMap The variable replacement map.
              * @return The resulting function represented as an ADD.
              */
-            InternalAdd<DdType::Sylvan, ValueType> replaceLeaves(std::map<storm::RationalFunctionVariable, std::pair<uint32_t, std::pair<storm::RationalNumber, storm::RationalNumber>>> const& replacementMap) const;
+            InternalAdd<DdType::Sylvan, ValueType> replaceLeaves(std::map<uint32_t, std::pair<storm::RationalFunctionVariable, std::pair<storm::RationalNumber, storm::RationalNumber>>> const& replacementMap) const;
+			
+			/*!
+             * Replaces the leaves in this MTBDD, converting them to double if possible, and -1.0 else.
+             *
+             * @return The resulting function represented as an ADD.
+             */
+            InternalAdd<DdType::Sylvan, double> toDouble() const;
 #endif
 			
             /*!

src/test/storage/SylvanDdTest.cpp

@@ -136,7 +136,6 @@ TEST(SylvanDd, BddExistAbstractRepresentative) {
 	storm::dd::Bdd<storm::dd::DdType::Sylvan> bddX1Y1Z1 = (bddX1 && bddY1) && bddZ1;
 
 	storm::dd::Bdd<storm::dd::DdType::Sylvan> bddAllTrueOrAllFalse = bddX0Y0Z0 || bddX1Y1Z1;
-	//bddAllTrueOrAllFalse.template toAdd<double>().exportToDot("test_Sylvan_addAllTrueOrAllFalse.dot");
 
 	representative_x = bddAllTrueOrAllFalse.existsAbstractRepresentative({x.first});
 	EXPECT_EQ(2ul, representative_x.getNonZeroCount());
@@ -464,6 +463,11 @@ TEST(SylvanDd, RationalFunctionLeaveReplacementSimpleVariable) {
     EXPECT_EQ(2ul, replacedAddSimpleX.getLeafCount());
     EXPECT_EQ(3ul, replacedAddSimpleX.getNodeCount());
 	EXPECT_TRUE(replacedAddSimpleX == complexAdd);
+	
+	storm::dd::Add<storm::dd::DdType::Sylvan, double> abstractedAddMax = replacedAddSimpleX.toDouble().maxAbstract({xExpr.first});
+	storm::dd::Add<storm::dd::DdType::Sylvan, double> abstractedAddMin = replacedAddSimpleX.toDouble().minAbstract({xExpr.first});
+	EXPECT_TRUE(abstractedAddMax == manager->template getConstant<double>(0.66666666666666666666));
+	EXPECT_TRUE(abstractedAddMin == manager->template getConstant<double>(0.33333333333333333333));
 }
 
 TEST(SylvanDd, RationalFunctionLeaveReplacementTwoVariables) {
@@ -537,7 +541,6 @@ TEST(SylvanDd, RationalFunctionLeaveReplacementComplexFunction) {
 	parser.setVariables({"x", "y", "z"});
 	storm::RationalFunction zDivTwoY = storm::RationalFunction(storm::Polynomial(parser.template parseMultivariatePolynomial<storm::RationalNumber>("z"), cache), storm::Polynomial(parser.template parseMultivariatePolynomial<storm::RationalNumber>("2*y"), cache));
 
-	//storm::RationalFunction rationalFunction(two * x + x*y + constantOneDivTwo * z / y);
 	storm::RationalFunction rationalFunction = storm::RationalFunction(storm::Polynomial(parser.parseMultivariatePolynomial<storm::RationalNumber>("2*x+x*y"), cache), storm::Polynomial(parser.parseMultivariatePolynomial<storm::RationalNumber>("1"), cache)) + zDivTwoY;	
 	ASSERT_NO_THROW(function = manager->template getConstant<storm::RationalFunction>(rationalFunction));
 	
@@ -617,9 +620,6 @@ TEST(SylvanDd, RationalFunctionLeaveReplacementComplexFunction) {
     EXPECT_EQ(8ul, replacedAdd.getLeafCount());
     EXPECT_EQ(15ul, replacedAdd.getNodeCount());
 	EXPECT_TRUE(replacedAdd == complexAdd);
-	
-	replacedAdd.exportToDot("sylvan_replacedAddC.dot");
-	complexAdd.exportToDot("sylvan_complexAddC.dot");
 }
 
 TEST(SylvanDd, RationalFunctionConstants) {
@@ -664,6 +664,55 @@ TEST(SylvanDd, RationalFunctionConstants) {
     EXPECT_EQ(1ul, function.getNodeCount());
 }
 
+TEST(SylvanDd, RationalFunctionToDouble) {
+    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> xExpr;
+	std::pair<storm::expressions::Variable, storm::expressions::Variable> yExpr;
+	std::pair<storm::expressions::Variable, storm::expressions::Variable> zExpr;
+	ASSERT_NO_THROW(xExpr = manager->addMetaVariable("x", 0, 1));
+	ASSERT_NO_THROW(yExpr = manager->addMetaVariable("y", 0, 1));
+	ASSERT_NO_THROW(zExpr = manager->addMetaVariable("z", 0, 1));
+	
+	storm::dd::Bdd<storm::dd::DdType::Sylvan> bddX0 = manager->getEncoding(xExpr.first, 0);
+	storm::dd::Bdd<storm::dd::DdType::Sylvan> bddX1 = manager->getEncoding(xExpr.first, 1);
+	storm::dd::Bdd<storm::dd::DdType::Sylvan> bddY0 = manager->getEncoding(yExpr.first, 0);
+	storm::dd::Bdd<storm::dd::DdType::Sylvan> bddY1 = manager->getEncoding(yExpr.first, 1);
+	storm::dd::Bdd<storm::dd::DdType::Sylvan> bddZ0 = manager->getEncoding(zExpr.first, 0);
+	storm::dd::Bdd<storm::dd::DdType::Sylvan> bddZ1 = manager->getEncoding(zExpr.first, 1);
+	
+	storm::dd::Add<storm::dd::DdType::Sylvan, storm::RationalFunction> complexAdd = 
+          ((bddX0 && (bddY0 && bddZ0)).template toAdd<storm::RationalFunction>() * manager->template getConstant<storm::RationalFunction>(storm::RationalFunction(storm::RationalNumber(-1))))
+		+ ((bddX0 && (bddY0 && bddZ1)).template toAdd<storm::RationalFunction>() * manager->template getConstant<storm::RationalFunction>(storm::RationalFunction(storm::RationalNumber(0))))
+		+ ((bddX0 && (bddY1 && bddZ0)).template toAdd<storm::RationalFunction>() * manager->template getConstant<storm::RationalFunction>(storm::RationalFunction(storm::RationalNumber(1) / storm::RationalNumber(2))))
+		+ ((bddX0 && (bddY1 && bddZ1)).template toAdd<storm::RationalFunction>() * manager->template getConstant<storm::RationalFunction>(storm::RationalFunction(storm::RationalNumber(1) / storm::RationalNumber(3))))
+		+ ((bddX1 && (bddY0 && bddZ0)).template toAdd<storm::RationalFunction>() * manager->template getConstant<storm::RationalFunction>(storm::RationalFunction(storm::RationalNumber(100000))))
+		+ ((bddX1 && (bddY0 && bddZ1)).template toAdd<storm::RationalFunction>() * manager->template getConstant<storm::RationalFunction>(storm::RationalFunction(storm::RationalNumber(3))))
+		+ ((bddX1 && (bddY1 && bddZ0)).template toAdd<storm::RationalFunction>() * manager->template getConstant<storm::RationalFunction>(storm::RationalFunction(storm::RationalNumber(4))))
+		+ ((bddX1 && (bddY1 && bddZ1)).template toAdd<storm::RationalFunction>() * manager->template getConstant<storm::RationalFunction>(storm::RationalFunction(storm::RationalNumber(0))));
+	EXPECT_EQ(6ul, complexAdd.getNonZeroCount());
+    EXPECT_EQ(7ul, complexAdd.getLeafCount());
+    EXPECT_EQ(14ul, complexAdd.getNodeCount());
+	
+	storm::dd::Add<storm::dd::DdType::Sylvan, double> doubleAdd = complexAdd.toDouble();
+    
+    EXPECT_EQ(6ul, doubleAdd.getNonZeroCount());
+    EXPECT_EQ(7ul, doubleAdd.getLeafCount());
+    EXPECT_EQ(14ul, doubleAdd.getNodeCount());
+    
+    storm::dd::Add<storm::dd::DdType::Sylvan, double> comparisonAdd = 
+		  ((bddX0 && (bddY0 && bddZ0)).template toAdd<double>() * manager->template getConstant<double>(-1.0))
+		+ ((bddX0 && (bddY0 && bddZ1)).template toAdd<double>() * manager->template getConstant<double>(0.0))
+		+ ((bddX0 && (bddY1 && bddZ0)).template toAdd<double>() * manager->template getConstant<double>(0.5))
+		+ ((bddX0 && (bddY1 && bddZ1)).template toAdd<double>() * manager->template getConstant<double>(0.33333333333333333333))
+		+ ((bddX1 && (bddY0 && bddZ0)).template toAdd<double>() * manager->template getConstant<double>(100000.0))
+		+ ((bddX1 && (bddY0 && bddZ1)).template toAdd<double>() * manager->template getConstant<double>(3.0))
+		+ ((bddX1 && (bddY1 && bddZ0)).template toAdd<double>() * manager->template getConstant<double>(4.0))
+		+ ((bddX1 && (bddY1 && bddZ1)).template toAdd<double>() * manager->template getConstant<double>(0.0));
+
+    EXPECT_TRUE(comparisonAdd == doubleAdd);
+}
+
 TEST(SylvanDd, RationalFunctionEncodingTest) {
     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);