From 291f120cc0cc802aa01a9969aa39e05d4255829d Mon Sep 17 00:00:00 2001
From: PBerger <philipp.berger@rwth-aachen.de>
Date: Tue, 26 Jul 2016 14:20:09 +0200
Subject: [PATCH] Added the encoding and identity test for Rational Functions.

Former-commit-id: ed9695a5e235196e67158d4b1051b85ef374afda
---
 test/functional/storage/SylvanDdTest.cpp | 80 +++++++++++++++++-------
 1 file changed, 58 insertions(+), 22 deletions(-)

diff --git a/test/functional/storage/SylvanDdTest.cpp b/test/functional/storage/SylvanDdTest.cpp
index 75a2c8947..ad5566050 100644
--- a/test/functional/storage/SylvanDdTest.cpp
+++ b/test/functional/storage/SylvanDdTest.cpp
@@ -41,6 +41,46 @@ TEST(SylvanDd, Constants) {
     EXPECT_EQ(2, two.getMax());
 }
 
+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));
+    EXPECT_EQ(2ul, manager->getNumberOfMetaVariables());
+    
+    ASSERT_THROW(manager->addMetaVariable("x", 0, 3), storm::exceptions::InvalidArgumentException);
+    
+    ASSERT_NO_THROW(manager->addMetaVariable("y", 0, 3));
+    EXPECT_EQ(4ul, manager->getNumberOfMetaVariables());
+    
+    EXPECT_TRUE(manager->hasMetaVariable("x'"));
+    EXPECT_TRUE(manager->hasMetaVariable("y'"));
+    
+    std::set<std::string> metaVariableSet = {"x", "x'", "y", "y'"};
+    EXPECT_EQ(metaVariableSet, manager->getAllMetaVariableNames());
+}
+
+TEST(SylvanDd, EncodingTest) {
+    std::shared_ptr<storm::dd::DdManager<storm::dd::DdType::Sylvan>> manager(new storm::dd::DdManager<storm::dd::DdType::Sylvan>());
+    std::pair<storm::expressions::Variable, storm::expressions::Variable> x = manager->addMetaVariable("x", 1, 9);
+    
+    storm::dd::Bdd<storm::dd::DdType::Sylvan> encoding;
+    ASSERT_THROW(encoding = manager->getEncoding(x.first, 0), storm::exceptions::InvalidArgumentException);
+    ASSERT_THROW(encoding = manager->getEncoding(x.first, 10), storm::exceptions::InvalidArgumentException);
+    ASSERT_NO_THROW(encoding = manager->getEncoding(x.first, 4));
+    EXPECT_EQ(1ul, encoding.getNonZeroCount());
+    
+    // As a BDD, this DD has one only leaf, because there does not exist a 0-leaf, and (consequently) one node less
+    // than the MTBDD.
+    EXPECT_EQ(5ul, encoding.getNodeCount());
+    EXPECT_EQ(1ul, encoding.getLeafCount());
+    
+    storm::dd::Add<storm::dd::DdType::Sylvan, double> add;
+    ASSERT_NO_THROW(add = encoding.template toAdd<double>());
+
+    // As an MTBDD, the 0-leaf is there, so the count is actually 2 and the node count is 6.
+    EXPECT_EQ(6ul, add.getNodeCount());
+    EXPECT_EQ(2ul, add.getLeafCount());
+}
+
 #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>());
@@ -67,26 +107,8 @@ TEST(SylvanDd, RationalFunctionConstants) {
     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));
-    EXPECT_EQ(2ul, manager->getNumberOfMetaVariables());
-    
-    ASSERT_THROW(manager->addMetaVariable("x", 0, 3), storm::exceptions::InvalidArgumentException);
-    
-    ASSERT_NO_THROW(manager->addMetaVariable("y", 0, 3));
-    EXPECT_EQ(4ul, manager->getNumberOfMetaVariables());
-    
-    EXPECT_TRUE(manager->hasMetaVariable("x'"));
-    EXPECT_TRUE(manager->hasMetaVariable("y'"));
-    
-    std::set<std::string> metaVariableSet = {"x", "x'", "y", "y'"};
-    EXPECT_EQ(metaVariableSet, manager->getAllMetaVariableNames());
-}
 
-TEST(SylvanDd, EncodingTest) {
+TEST(SylvanDd, RationalFunctionEncodingTest) {
     std::shared_ptr<storm::dd::DdManager<storm::dd::DdType::Sylvan>> manager(new storm::dd::DdManager<storm::dd::DdType::Sylvan>());
     std::pair<storm::expressions::Variable, storm::expressions::Variable> x = manager->addMetaVariable("x", 1, 9);
     
@@ -101,14 +123,28 @@ TEST(SylvanDd, EncodingTest) {
     EXPECT_EQ(5ul, encoding.getNodeCount());
     EXPECT_EQ(1ul, encoding.getLeafCount());
     
-    storm::dd::Add<storm::dd::DdType::Sylvan, double> add;
-    ASSERT_NO_THROW(add = encoding.template toAdd<double>());
+    storm::dd::Add<storm::dd::DdType::Sylvan, storm::RationalFunction> add;
+    ASSERT_NO_THROW(add = encoding.template toAdd<storm::RationalFunction>());
 
     // As an MTBDD, the 0-leaf is there, so the count is actually 2 and the node count is 6.
     EXPECT_EQ(6ul, add.getNodeCount());
     EXPECT_EQ(2ul, add.getLeafCount());
 }
 
+TEST(SylvanDd, RationalFunctionIdentityTest) {
+    std::shared_ptr<storm::dd::DdManager<storm::dd::DdType::Sylvan>> manager(new storm::dd::DdManager<storm::dd::DdType::Sylvan>());
+    std::pair<storm::expressions::Variable, storm::expressions::Variable> x = manager->addMetaVariable("x", 1, 9);
+    
+    storm::dd::Add<storm::dd::DdType::Sylvan, storm::RationalFunction> identity;
+    ASSERT_NO_THROW(identity = manager->getIdentity<storm::RationalFunction>(x.first));
+
+    EXPECT_EQ(9ul, identity.getNonZeroCount());
+    EXPECT_EQ(10ul, identity.getLeafCount());
+    EXPECT_EQ(21ul, identity.getNodeCount());
+}
+
+#endif
+
 TEST(SylvanDd, RangeTest) {
     std::shared_ptr<storm::dd::DdManager<storm::dd::DdType::Sylvan>> manager(new storm::dd::DdManager<storm::dd::DdType::Sylvan>());
     std::pair<storm::expressions::Variable, storm::expressions::Variable> x;
@@ -440,4 +476,4 @@ TEST(SylvanDd, BddOddTest) {
     EXPECT_EQ(9ul, matrix.getRowGroupCount());
     EXPECT_EQ(9ul, matrix.getColumnCount());
     EXPECT_EQ(106ul, matrix.getNonzeroEntryCount());
-}
\ No newline at end of file
+}