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 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> manager(new storm::dd::DdManager()); + storm::dd::Add zero; + ASSERT_NO_THROW(zero = manager->template getAddZero()); + + EXPECT_EQ(0ul, zero.getNonZeroCount()); + EXPECT_EQ(1ul, zero.getLeafCount()); + EXPECT_EQ(1ul, zero.getNodeCount()); + + storm::dd::Add one; + ASSERT_NO_THROW(one = manager->template getAddOne()); + + EXPECT_EQ(0ul, one.getNonZeroCount()); + EXPECT_EQ(1ul, one.getLeafCount()); + EXPECT_EQ(1ul, one.getNodeCount()); + + storm::dd::Add two; + storm::RationalFunction constantTwo(2); + + ASSERT_NO_THROW(two = manager->template getConstant(constantTwo)); + + EXPECT_EQ(0ul, two.getNonZeroCount()); + EXPECT_EQ(1ul, two.getLeafCount()); + EXPECT_EQ(1ul, two.getNodeCount()); +} +#endif + TEST(SylvanDd, AddGetMetaVariableTest) { std::shared_ptr> manager(new storm::dd::DdManager()); ASSERT_NO_THROW(manager->addMetaVariable("x", 1, 9));