From 07d4848f55d0b46d4dc83df2b07a3e2d677fe537 Mon Sep 17 00:00:00 2001
From: PBerger <philipp.berger@rwth-aachen.de>
Date: Thu, 21 Jul 2016 19:56:32 +0200
Subject: [PATCH] Fixed missing include in InternalSylvanAdd.cpp Added simple
 test for Sylvan + RationalFunctions.

Former-commit-id: ffb747a861f06422bebc1e5a1146f9150c55e710
---
 src/storage/dd/sylvan/InternalSylvanAdd.cpp |  2 ++
 test/functional/storage/SylvanDdTest.cpp    | 29 +++++++++++++++++++++
 2 files changed, 31 insertions(+)

diff --git a/src/storage/dd/sylvan/InternalSylvanAdd.cpp b/src/storage/dd/sylvan/InternalSylvanAdd.cpp
index 9b6303f54..92c6ca642 100644
--- a/src/storage/dd/sylvan/InternalSylvanAdd.cpp
+++ b/src/storage/dd/sylvan/InternalSylvanAdd.cpp
@@ -10,6 +10,8 @@
 #include "src/utility/constants.h"
 #include "src/exceptions/NotImplementedException.h"
 
+#include "storm-config.h"
+
 namespace storm {
     namespace dd {
         template<typename ValueType>
diff --git a/test/functional/storage/SylvanDdTest.cpp b/test/functional/storage/SylvanDdTest.cpp
index fdb60e5c0..75a2c8947 100644
--- a/test/functional/storage/SylvanDdTest.cpp
+++ b/test/functional/storage/SylvanDdTest.cpp
@@ -1,6 +1,7 @@
 #include "gtest/gtest.h"
 #include "storm-config.h"
 
+#include "src/adapters/CarlAdapter.h"
 #include "src/exceptions/InvalidArgumentException.h"
 #include "src/storage/dd/DdManager.h"
 #include "src/storage/dd/Add.h"
@@ -40,6 +41,34 @@ TEST(SylvanDd, Constants) {
     EXPECT_EQ(2, two.getMax());
 }
 
+#ifdef STORM_HAVE_CARL
+TEST(SylvanDd, RationalFunctionConstants) {
+    std::shared_ptr<storm::dd::DdManager<storm::dd::DdType::Sylvan>> manager(new storm::dd::DdManager<storm::dd::DdType::Sylvan>());
+    storm::dd::Add<storm::dd::DdType::Sylvan, storm::RationalFunction> zero;
+    ASSERT_NO_THROW(zero = manager->template getAddZero<storm::RationalFunction>());
+    
+    EXPECT_EQ(0ul, zero.getNonZeroCount());
+    EXPECT_EQ(1ul, zero.getLeafCount());
+    EXPECT_EQ(1ul, zero.getNodeCount());
+    
+    storm::dd::Add<storm::dd::DdType::Sylvan, storm::RationalFunction> one;
+    ASSERT_NO_THROW(one = manager->template getAddOne<storm::RationalFunction>());
+    
+    EXPECT_EQ(0ul, one.getNonZeroCount());
+    EXPECT_EQ(1ul, one.getLeafCount());
+    EXPECT_EQ(1ul, one.getNodeCount());
+    
+    storm::dd::Add<storm::dd::DdType::Sylvan, storm::RationalFunction> two;
+	storm::RationalFunction constantTwo(2);
+	
+    ASSERT_NO_THROW(two = manager->template getConstant<storm::RationalFunction>(constantTwo));
+    
+    EXPECT_EQ(0ul, two.getNonZeroCount());
+    EXPECT_EQ(1ul, two.getLeafCount());
+    EXPECT_EQ(1ul, two.getNodeCount());
+}
+#endif
+
 TEST(SylvanDd, AddGetMetaVariableTest) {
     std::shared_ptr<storm::dd::DdManager<storm::dd::DdType::Sylvan>> manager(new storm::dd::DdManager<storm::dd::DdType::Sylvan>());
     ASSERT_NO_THROW(manager->addMetaVariable("x", 1, 9));