Implemented functions for BDD -> ADD conversion and some helpers.

Former-commit-id: 78c9003366

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

@@ -114,3 +114,19 @@ int storm_rational_function_is_zero(storm_rational_function_ptr a) {
 		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;
+}

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

@@ -26,6 +26,9 @@ storm_rational_function_ptr storm_rational_function_negate(storm_rational_functi
 uint64_t storm_rational_function_hash(storm_rational_function_ptr const a, uint64_t const seed);
 int storm_rational_function_is_zero(storm_rational_function_ptr a);
 
+storm_rational_function_ptr storm_rational_function_get_zero();
+storm_rational_function_ptr storm_rational_function_get_one();
+
 #ifdef __cplusplus
 }
 #endif

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

@@ -15,6 +15,7 @@
  */
 
 #include <sylvan_obj.hpp>
+#include <sylvan_storm_rational_function.h>
 
 using namespace sylvan;
 
@@ -604,6 +605,16 @@ Mtbdd::doubleTerminal(double value)
     return mtbdd_double(value);
 }
 
+#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL)
+Mtbdd
+Mtbdd::stormRationalFunctionTerminal(storm::RationalFunction const& value)
+{
+	storm_rational_function_t functionStruct;
+	functionStruct.storm_rational_function = (void*)(&value);
+    return mtbdd_storm_rational_function(functionStruct);
+}
+#endif
+
 Mtbdd
 Mtbdd::fractionTerminal(int64_t nominator, uint64_t denominator)
 {

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

@@ -23,6 +23,8 @@
 #include <lace.h>
 #include <sylvan.h>
 
+#include "src/adapters/CarlAdapter.h"
+
 namespace sylvan {
 
 class BddSet;
@@ -542,6 +544,13 @@ public:
      */
     static Mtbdd doubleTerminal(double value);
 
+#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL)
+	/**
+     * @brief Creates a Mtbdd leaf representing the rational function value <value>
+     */
+    static Mtbdd stormRationalFunctionTerminal(storm::RationalFunction const& value);
+#endif
+	
     /**
      * @brief Creates a Mtbdd leaf representing the fraction value <nominator>/<denominator>
      * Internally, Sylvan uses 32-bit values and reports overflows to stderr.

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

@@ -1,3 +1,6 @@
     Mtbdd toDoubleMtbdd() const;
     Mtbdd toInt64Mtbdd() const;
+#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL)
+	Mtbdd toStormRationalFunctionMtbdd() const;
+#endif
     Mtbdd Ite(Mtbdd const& thenDd, Mtbdd const& elseDd) const;

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

@@ -10,6 +10,14 @@ Bdd::toInt64Mtbdd() const {
     return mtbdd_bool_to_int64(bdd);
 }
 
+#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL)
+Mtbdd
+Bdd::toStormRationalFunctionMtbdd() const {
+    LACE_ME;
+    return mtbdd_bool_to_storm_rational_function(bdd);
+}
+#endif
+
 Mtbdd
 Bdd::Ite(Mtbdd const& thenDd, Mtbdd const& elseDd) const {
     LACE_ME;

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

@@ -90,7 +90,31 @@ uint32_t sylvan_storm_rational_function_get_type() {
 MTBDD
 mtbdd_storm_rational_function(storm_rational_function_t val)
 {
-    return mtbdd_makeleaf(sylvan_storm_rational_function_type, (size_t)val);
+	uint64_t terminalValue = (uint64_t)&val;
+	return mtbdd_makeleaf(sylvan_storm_rational_function_type, terminalValue);
+}
+
+/**
+ * Converts a BDD to a MTBDD with storm::RationalFunction leaves
+ */
+TASK_IMPL_2(MTBDD, mtbdd_op_bool_to_storm_rational_function, MTBDD, a, size_t, v)
+{
+	if (a == mtbdd_false) {
+		return mtbdd_storm_rational_function(*storm_rational_function_get_zero());
+	}
+	if (a == mtbdd_true) {
+		return mtbdd_storm_rational_function(*storm_rational_function_get_one());
+	}
+    
+    // Ugly hack to get rid of the error "unused variable v" (because there is no version of uapply without a parameter).
+    (void)v;
+    
+    return mtbdd_invalid;
+}
+
+TASK_IMPL_1(MTBDD, mtbdd_bool_to_storm_rational_function, MTBDD, dd)
+{
+    return mtbdd_uapply(dd, TASK(mtbdd_op_bool_to_storm_rational_function), 0);
 }
 
 /**

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

@@ -31,6 +31,13 @@ uint32_t sylvan_storm_rational_function_get_type();
  */
 MTBDD mtbdd_storm_rational_function(storm_rational_function_t val);
 
+/**
+ * Monad that converts Boolean to a storm::RationalFunction MTBDD, translate terminals true to 1 and to 0 otherwise;
+ */
+TASK_DECL_2(MTBDD, mtbdd_op_bool_to_storm_rational_function, MTBDD, size_t)
+TASK_DECL_1(MTBDD, mtbdd_bool_to_storm_rational_function, MTBDD)
+#define mtbdd_bool_to_storm_rational_function(dd) CALL(mtbdd_bool_to_storm_rational_function, dd)
+
 /**
  * Operation "plus" for two storm::RationalFunction MTBDDs
  */

src/storage/dd/sylvan/InternalSylvanAdd.cpp

@@ -617,9 +617,8 @@ namespace storm {
 		MTBDD InternalAdd<DdType::Sylvan, ValueType>::getLeaf(storm::RationalFunction const& value) {
 			storm_rational_function_ptr_struct helperStruct;
 			helperStruct.storm_rational_function = (void*)(&value);
-			uint64_t terminalValue = (uint64_t)&helperStruct;
 
-			return sylvan::Mtbdd::terminal(sylvan_storm_rational_function_get_type(), terminalValue).GetMTBDD();
+			return mtbdd_storm_rational_function(helperStruct);
 		}
         
         template<typename ValueType>

src/storage/dd/sylvan/InternalSylvanBdd.cpp

@@ -248,7 +248,7 @@ namespace storm {
 			} 
 #ifdef STORM_HAVE_CARL
 			else if (std::is_same<ValueType, storm::RationalFunction>::value) {
-				STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Conversion to ADD is currently unsupported for storm::RationalFunction.");
+				return InternalAdd<DdType::Sylvan, ValueType>(ddManager, this->sylvanBdd.toStormRationalFunctionMtbdd());
 			} 
 #endif
 			else {