Added missing template instantiation.

Added missing function implementation for sylvan OPs.


Former-commit-id: fb10555ca3

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

@@ -220,6 +220,42 @@ TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_divide, MTBDD*, pa, MTBDD*,
     return mtbdd_invalid;
 }
 
+/**
+ * The abstraction operators are called in either of two ways:
+ * - with k=0, then just calculate "a op b"
+ * - with k<>0, then just calculate "a := a op a", k times
+ */
+
+TASK_IMPL_3(MTBDD, sylvan_storm_rational_function_abstract_op_plus, MTBDD, a, MTBDD, b, int, k)
+{
+    if (k==0) {
+        return mtbdd_apply(a, b, TASK(sylvan_storm_rational_function_op_plus));
+    } else {
+        MTBDD res = a;
+        for (int i=0; i<k; i++) {
+            mtbdd_refs_push(res);
+            res = mtbdd_apply(res, res, TASK(sylvan_storm_rational_function_op_plus));
+            mtbdd_refs_pop(1);
+        }
+        return res;
+    }
+}
+
+TASK_IMPL_3(MTBDD, sylvan_storm_rational_function_abstract_op_times, MTBDD, a, MTBDD, b, int, k)
+{
+    if (k==0) {
+        return mtbdd_apply(a, b, TASK(sylvan_storm_rational_function_op_times));
+    } else {
+        MTBDD res = a;
+        for (int i=0; i<k; i++) {
+            mtbdd_refs_push(res);
+            res = mtbdd_apply(res, res, TASK(sylvan_storm_rational_function_op_times));
+            mtbdd_refs_pop(1);
+        }
+        return res;
+    }
+}
+
 /**
  * Operation "neg" for one storm::RationalFunction MTBDD
  */

src/storage/dd/sylvan/SylvanAddIterator.cpp

@@ -10,6 +10,14 @@
 
 #include <cmath>
 
+#include "src/adapters/CarlAdapter.h"
+
+#include "storm-config.h"
+// TODO: Remove this later on.
+#ifndef STORM_HAVE_CARL
+#define STORM_HAVE_CARL 1
+#endif
+
 namespace storm {
     namespace dd {
         template<typename ValueType>
@@ -187,5 +195,8 @@ namespace storm {
         
         template class AddIterator<DdType::Sylvan, double>;
         template class AddIterator<DdType::Sylvan, uint_fast64_t>;
+#ifdef STORM_HAVE_CARL
+		template class AddIterator<DdType::Sylvan, storm::RationalFunction>;
+#endif
     }
 }