From e0647f34eb937a0702cbe8a6c1d6b4ffca257b87 Mon Sep 17 00:00:00 2001
From: PBerger <philipp.berger@rwth-aachen.de>
Date: Tue, 19 Jul 2016 17:32:00 +0200
Subject: [PATCH] Added missing template instantiation. Added missing function
 implementation for sylvan OPs.

Former-commit-id: fb10555ca3c2e791533cf0b7da960e86dc348a65
---
 .../src/sylvan_storm_rational_function.c      | 36 +++++++++++++++++++
 src/storage/dd/sylvan/SylvanAddIterator.cpp   | 11 ++++++
 2 files changed, 47 insertions(+)

diff --git a/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.c b/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.c
index ebb5f7062..c2fb73016 100644
--- a/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.c
+++ b/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
  */
diff --git a/src/storage/dd/sylvan/SylvanAddIterator.cpp b/src/storage/dd/sylvan/SylvanAddIterator.cpp
index 8c97941a3..d4efc2fcb 100644
--- a/src/storage/dd/sylvan/SylvanAddIterator.cpp
+++ b/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
     }
 }