started integrating sylvan

Former-commit-id: 2aec043047

src/storage/dd/Bdd.cpp

@@ -188,10 +188,17 @@ namespace storm {
         template<DdType LibraryType>
         uint_fast64_t Bdd<LibraryType>::getNonZeroCount() const {
             std::size_t numberOfDdVariables = 0;
-            for (auto const& metaVariable : this->getContainedMetaVariables()) {
-                numberOfDdVariables += this->getDdManager()->getMetaVariable(metaVariable).getNumberOfDdVariables();
+            if (LibraryType == DdType::CUDD) {
+                std::size_t numberOfDdVariables = 0;
+                for (auto const& metaVariable : this->getContainedMetaVariables()) {
+                    numberOfDdVariables += this->getDdManager()->getMetaVariable(metaVariable).getNumberOfDdVariables();
+                }
+            }
+            Bdd<LibraryType> cube;
+            if (LibraryType == DdType::Sylvan) {
+                cube = Bdd<LibraryType>::getCube(*this->getDdManager(), this->getContainedMetaVariables());
             }
-            return internalBdd.getNonZeroCount(numberOfDdVariables);
+            return internalBdd.getNonZeroCount(cube, numberOfDdVariables);
         }
         
         template<DdType LibraryType>

src/storage/dd/cudd/InternalCuddBdd.cpp

@@ -110,7 +110,7 @@ namespace storm {
             return InternalBdd<DdType::CUDD>(ddManager, this->getCuddBdd().Support());
         }
         
-        uint_fast64_t InternalBdd<DdType::CUDD>::getNonZeroCount(uint_fast64_t numberOfDdVariables) const {
+        uint_fast64_t InternalBdd<DdType::CUDD>::getNonZeroCount(InternalBdd<DdType::CUDD> const& cube, uint_fast64_t numberOfDdVariables) const {
             return static_cast<uint_fast64_t>(this->getCuddBdd().CountMinterm(static_cast<int>(numberOfDdVariables)));
         }
         
@@ -149,8 +149,8 @@ namespace storm {
             }
             
             // Open the file, dump the DD and close it again.
-            FILE* filePointer = fopen(filename.c_str() , "w");
             std::vector<cudd::BDD> cuddBddVector = { this->getCuddBdd() };
+            FILE* filePointer = fopen(filename.c_str() , "w");
             ddManager->getCuddManager().DumpDot(cuddBddVector, &ddVariableNames[0], &ddNames[0], filePointer);
             fclose(filePointer);
             

src/storage/dd/cudd/InternalCuddBdd.h

@@ -219,10 +219,11 @@ namespace storm {
             /*!
              * Retrieves the number of encodings that are mapped to a non-zero value.
              *
-             * @param The number of DD variables contained in this BDD.
+             * @param cube A cube of variables that is ignored.
+             * @param numberOfDdVariables The number of DD variables contained in this BDD.
              * @return The number of encodings that are mapped to a non-zero value.
              */
-            uint_fast64_t getNonZeroCount(uint_fast64_t numberOfDdVariables) const;
+            uint_fast64_t getNonZeroCount(InternalBdd<DdType::CUDD> const& cube, uint_fast64_t numberOfDdVariables) const;
             
             /*!
              * Retrieves the number of leaves of the DD.

src/storage/dd/sylvan/InternalSylvanBdd.cpp

@@ -10,113 +10,139 @@
 
 namespace storm {
     namespace dd {
+        InternalBdd<DdType::Sylvan>::InternalBdd(InternalDdManager<DdType::Sylvan> const* ddManager, sylvan::Bdd const& sylvanBdd) : ddManager(ddManager), sylvanBdd(sylvanBdd) {
+            // Intentionally left empty.
+        }
+        
         template<typename ValueType>
         InternalBdd<DdType::Sylvan> InternalBdd<DdType::Sylvan>::fromVector(InternalDdManager<DdType::Sylvan> const* ddManager, std::vector<ValueType> const& values, Odd const& odd, std::vector<uint_fast64_t> const& sortedDdVariableIndices, std::function<bool (ValueType const&)> const& filter) {
             STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented.");
         }
         
         bool InternalBdd<DdType::Sylvan>::operator==(InternalBdd<DdType::Sylvan> const& other) const {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented.");
+            return sylvanBdd == other.sylvanBdd;
         }
         
         bool InternalBdd<DdType::Sylvan>::operator!=(InternalBdd<DdType::Sylvan> const& other) const {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented.");
+            return sylvanBdd != other.sylvanBdd;
         }
         
         InternalBdd<DdType::Sylvan> InternalBdd<DdType::Sylvan>::ite(InternalBdd<DdType::Sylvan> const& thenDd, InternalBdd<DdType::Sylvan> const& elseDd) const {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented.");
+            return InternalBdd<DdType::Sylvan>(ddManager, this->sylvanBdd.Ite(thenDd.sylvanBdd, elseDd.sylvanBdd));
         }
         
         InternalBdd<DdType::Sylvan> InternalBdd<DdType::Sylvan>::operator||(InternalBdd<DdType::Sylvan> const& other) const {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented.");
+            return InternalBdd<DdType::Sylvan>(ddManager, this->sylvanBdd | other.sylvanBdd);
         }
         
         InternalBdd<DdType::Sylvan>& InternalBdd<DdType::Sylvan>::operator|=(InternalBdd<DdType::Sylvan> const& other) {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented.");
+            this->sylvanBdd |= other.sylvanBdd;
+            return *this;
         }
         
         InternalBdd<DdType::Sylvan> InternalBdd<DdType::Sylvan>::operator&&(InternalBdd<DdType::Sylvan> const& other) const {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented.");
+            return InternalBdd<DdType::Sylvan>(ddManager, this->sylvanBdd & other.sylvanBdd);
         }
         
         InternalBdd<DdType::Sylvan>& InternalBdd<DdType::Sylvan>::operator&=(InternalBdd<DdType::Sylvan> const& other) {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented.");
+            this->sylvanBdd &= other.sylvanBdd;
+            return *this;
         }
         
         InternalBdd<DdType::Sylvan> InternalBdd<DdType::Sylvan>::iff(InternalBdd<DdType::Sylvan> const& other) const {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented.");
+            return InternalBdd<DdType::Sylvan>(ddManager, !(this->sylvanBdd ^ other.sylvanBdd));
         }
         
         InternalBdd<DdType::Sylvan> InternalBdd<DdType::Sylvan>::exclusiveOr(InternalBdd<DdType::Sylvan> const& other) const {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented.");
+            return InternalBdd<DdType::Sylvan>(ddManager, this->sylvanBdd ^ other.sylvanBdd);
         }
         
         InternalBdd<DdType::Sylvan> InternalBdd<DdType::Sylvan>::implies(InternalBdd<DdType::Sylvan> const& other) const {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented.");
+            return InternalBdd<DdType::Sylvan>(ddManager, !this->sylvanBdd | other.sylvanBdd);
         }
         
         InternalBdd<DdType::Sylvan> InternalBdd<DdType::Sylvan>::operator!() const {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented.");
+            return InternalBdd<DdType::Sylvan>(ddManager, !this->sylvanBdd);
         }
         
         InternalBdd<DdType::Sylvan>& InternalBdd<DdType::Sylvan>::complement() {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented.");
+            this->sylvanBdd = !this->sylvanBdd;
+            return *this;
         }
         
         InternalBdd<DdType::Sylvan> InternalBdd<DdType::Sylvan>::existsAbstract(InternalBdd<DdType::Sylvan> const& cube) const {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented.");
+            return InternalBdd<DdType::Sylvan>(ddManager, this->sylvanBdd.ExistAbstract(cube.sylvanBdd));
         }
         
         InternalBdd<DdType::Sylvan> InternalBdd<DdType::Sylvan>::universalAbstract(InternalBdd<DdType::Sylvan> const& cube) const {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented.");
+            return InternalBdd<DdType::Sylvan>(ddManager, this->sylvanBdd.UnivAbstract(cube.sylvanBdd));
         }
         
         InternalBdd<DdType::Sylvan> InternalBdd<DdType::Sylvan>::andExists(InternalBdd<DdType::Sylvan> const& other, InternalBdd<DdType::Sylvan> const& cube) const {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented.");
+            return InternalBdd<DdType::Sylvan>(ddManager, this->sylvanBdd.AndAbstract(other.sylvanBdd, cube.sylvanBdd));
         }
         
         InternalBdd<DdType::Sylvan> InternalBdd<DdType::Sylvan>::constrain(InternalBdd<DdType::Sylvan> const& constraint) const {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented.");
+            return InternalBdd<DdType::Sylvan>(ddManager, this->sylvanBdd.Constrain(constraint.sylvanBdd));
         }
         
         InternalBdd<DdType::Sylvan> InternalBdd<DdType::Sylvan>::restrict(InternalBdd<DdType::Sylvan> const& constraint) const {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented.");
+            return InternalBdd<DdType::Sylvan>(ddManager, this->sylvanBdd.Restrict(constraint.sylvanBdd));
         }
         
         InternalBdd<DdType::Sylvan> InternalBdd<DdType::Sylvan>::swapVariables(std::vector<InternalBdd<DdType::Sylvan>> const& from, std::vector<InternalBdd<DdType::Sylvan>> const& to) const {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented.");
+            std::vector<sylvan::Bdd> fromBdd;
+            std::vector<sylvan::Bdd> toBdd;
+            for (auto it1 = from.begin(), ite1 = from.end(), it2 = to.begin(); it1 != ite1; ++it1, ++it2) {
+                fromBdd.push_back(it1->getSylvanBdd());
+                toBdd.push_back(it2->getSylvanBdd());
+            }
+            return InternalBdd<DdType::Sylvan>(ddManager, this->sylvanBdd.Permute(fromBdd, toBdd));
         }
         
         InternalBdd<DdType::Sylvan> InternalBdd<DdType::Sylvan>::getSupport() const {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented.");
+            return InternalBdd<DdType::Sylvan>(ddManager, this->sylvanBdd.Support());
         }
         
-        uint_fast64_t InternalBdd<DdType::Sylvan>::getNonZeroCount(uint_fast64_t numberOfDdVariables) const {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented.");
+        uint_fast64_t InternalBdd<DdType::Sylvan>::getNonZeroCount(InternalBdd<DdType::Sylvan> const& cube, uint_fast64_t numberOfDdVariables) const {
+            return static_cast<uint_fast64_t>(this->sylvanBdd.SatCount(cube.sylvanBdd));
         }
         
         uint_fast64_t InternalBdd<DdType::Sylvan>::getLeafCount() const {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented.");
+            // For BDDs, the leaf count is always one, because the only leaf is the false leaf (and true is represented
+            // by a negation edge to false).
+            return 1;
         }
         
         uint_fast64_t InternalBdd<DdType::Sylvan>::getNodeCount() const {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented.");
+            // We have to add one to also count the false-leaf, which is the only leaf appearing in BDDs.
+            return static_cast<uint_fast64_t>(this->sylvanBdd.NodeCount()) + 1;
         }
         
         bool InternalBdd<DdType::Sylvan>::isOne() const {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented.");
+            return this->sylvanBdd.isOne();
         }
         
         bool InternalBdd<DdType::Sylvan>::isZero() const {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented.");
+            return this->sylvanBdd.isZero();
         }
         
         uint_fast64_t InternalBdd<DdType::Sylvan>::getIndex() const {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented.");
+            return static_cast<uint_fast64_t>(this->sylvanBdd.GetBDD());
         }
         
         void InternalBdd<DdType::Sylvan>::exportToDot(std::string const& filename, std::vector<std::string> const& ddVariableNamesAsStrings) const {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented.");
+            FILE* filePointer = fopen(filename.c_str() , "w");
+            this->sylvanBdd.PrintDot(filePointer);
+            fclose(filePointer);
+        }
+        
+        sylvan::Bdd& InternalBdd<DdType::Sylvan>::getSylvanBdd() {
+            return sylvanBdd;
+        }
+        
+        sylvan::Bdd const& InternalBdd<DdType::Sylvan>::getSylvanBdd() const {
+            return sylvanBdd;
         }
         
         template<typename ValueType>

src/storage/dd/sylvan/InternalSylvanBdd.h

@@ -26,6 +26,8 @@ namespace storm {
         public:
             friend class InternalAdd<DdType::Sylvan, double>;
             
+            InternalBdd(InternalDdManager<DdType::Sylvan> const* ddManager, sylvan::Bdd const& sylvanBdd);
+            
             // Instantiate all copy/move constructors/assignments with the default implementation.
             InternalBdd() = default;
             InternalBdd(InternalBdd<DdType::Sylvan> const& other) = default;
@@ -206,10 +208,11 @@ namespace storm {
             /*!
              * Retrieves the number of encodings that are mapped to a non-zero value.
              *
-             * @param The number of DD variables contained in this BDD.
+             * @param cube The cube of variables contained in this BDD.
+             * @param numberOfDdVariables The number of DD variables contained in this BDD. This is ignored.
              * @return The number of encodings that are mapped to a non-zero value.
              */
-            uint_fast64_t getNonZeroCount(uint_fast64_t numberOfDdVariables) const;
+            uint_fast64_t getNonZeroCount(InternalBdd<DdType::Sylvan> const& cube, uint_fast64_t numberOfDdVariables) const;
             
             /*!
              * Retrieves the number of leaves of the DD.
@@ -292,7 +295,12 @@ namespace storm {
             void filterExplicitVector(Odd const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<ValueType> const& sourceValues, std::vector<ValueType>& targetValues) const;
             
         private:
+            sylvan::Bdd& getSylvanBdd();
+            sylvan::Bdd const& getSylvanBdd() const;
+            
             InternalDdManager<DdType::Sylvan> const* ddManager;
+            
+            sylvan::Bdd sylvanBdd;
         };
     }
 }

src/storage/dd/sylvan/InternalSylvanDdManager.cpp

@@ -2,16 +2,35 @@
 
 #include "src/utility/macros.h"
 #include "src/exceptions/NotImplementedException.h"
+#include "src/exceptions/NotSupportedException.h"
 
 namespace storm {
     namespace dd {
+        uint_fast64_t InternalDdManager<DdType::Sylvan>::numberOfInstances = 0;
+        uint_fast64_t InternalDdManager<DdType::Sylvan>::nextFreeVariableIndex = 0;
         
         InternalDdManager<DdType::Sylvan>::InternalDdManager() {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented.");
+            if (numberOfInstances == 0) {
+                // Initialize lace: auto-detecting number of workers.
+                lace_init(0, 1000000);
+                lace_startup(0, 0, 0);
+                
+                sylvan::Sylvan::initPackage(1ull << 16, 1ull << 32, 1ull << 16, 1ull << 32);
+                sylvan::Sylvan::initBdd(1);
+                sylvan::Sylvan::initMtbdd();
+            }
+            ++numberOfInstances;
+        }
+        
+        InternalDdManager<DdType::Sylvan>::~InternalDdManager() {
+            --numberOfInstances;
+            if (numberOfInstances == 0) {
+                sylvan::Sylvan::quitPackage();
+            }
         }
         
         InternalBdd<DdType::Sylvan> InternalDdManager<DdType::Sylvan>::getBddOne() const {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented.");
+            return InternalBdd<DdType::Sylvan>(this, sylvan::Bdd::bddOne());
         }
         
         template<typename ValueType>
@@ -20,7 +39,7 @@ namespace storm {
         }
         
         InternalBdd<DdType::Sylvan> InternalDdManager<DdType::Sylvan>::getBddZero() const {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented.");
+            return InternalBdd<DdType::Sylvan>(this, sylvan::Bdd::bddZero());
         }
         
         template<typename ValueType>
@@ -34,19 +53,22 @@ namespace storm {
         }
         
         std::pair<InternalBdd<DdType::Sylvan>, InternalBdd<DdType::Sylvan>> InternalDdManager<DdType::Sylvan>::createNewDdVariablePair() {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented.");
+            InternalBdd<DdType::Sylvan> first = InternalBdd<DdType::Sylvan>(this, sylvan::Bdd::bddVar(nextFreeVariableIndex));
+            InternalBdd<DdType::Sylvan> second = InternalBdd<DdType::Sylvan>(this, sylvan::Bdd::bddVar(nextFreeVariableIndex + 1));
+            nextFreeVariableIndex += 2;
+            return std::make_pair(first, second);
         }
         
         void InternalDdManager<DdType::Sylvan>::allowDynamicReordering(bool value) {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented.");
+            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Operation is not supported by sylvan.");
         }
         
         bool InternalDdManager<DdType::Sylvan>::isDynamicReorderingAllowed() const {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented.");
+            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Operation is not supported by sylvan.");
         }
         
         void InternalDdManager<DdType::Sylvan>::triggerReordering() {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented.");
+            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Operation is not supported by sylvan.");
         }
                 
         template InternalAdd<DdType::Sylvan, double> InternalDdManager<DdType::Sylvan>::getAddOne() const;

src/storage/dd/sylvan/InternalSylvanDdManager.h

@@ -24,9 +24,14 @@ namespace storm {
             friend class InternalAdd;
             
             /*!
-             * Creates a new internal manager for CUDD DDs.
+             * Creates a new internal manager for Sylvan DDs.
              */
             InternalDdManager();
+
+            /*!
+             * Destroys the internal manager.
+             */
+            ~InternalDdManager();
             
             /*!
              * Retrieves a BDD representing the constant one function.
@@ -93,7 +98,14 @@ namespace storm {
             void triggerReordering();
             
         private:
-
+            // A counter for the number of instances of this class. This is used to determine when to initialize and
+            // quit the sylvan. This is because Sylvan does not know the concept of managers but implicitly has a
+            // 'global' manager.
+            static uint_fast64_t numberOfInstances;
+            
+            // The index of the next free variable index. This needs to be shared across all instances since the sylvan
+            // manager is implicitly 'global'.
+            static uint_fast64_t nextFreeVariableIndex;
         };
     }
 }

test/functional/storage/CuddDdTest.cpp

@@ -9,7 +9,7 @@
 
 #include "src/storage/SparseMatrix.h"
 
-TEST(CuddDdManager, Constants) {
+TEST(CuddDd, Constants) {
     std::shared_ptr<storm::dd::DdManager<storm::dd::DdType::CUDD>> manager(new storm::dd::DdManager<storm::dd::DdType::CUDD>());
     storm::dd::Add<storm::dd::DdType::CUDD, double> zero;
     ASSERT_NO_THROW(zero = manager->template getAddZero<double>());
@@ -39,7 +39,7 @@ TEST(CuddDdManager, Constants) {
     EXPECT_EQ(2, two.getMax());
 }
 
-TEST(CuddDdManager, AddGetMetaVariableTest) {
+TEST(CuddDd, AddGetMetaVariableTest) {
     std::shared_ptr<storm::dd::DdManager<storm::dd::DdType::CUDD>> manager(new storm::dd::DdManager<storm::dd::DdType::CUDD>());
     ASSERT_NO_THROW(manager->addMetaVariable("x", 1, 9));
     EXPECT_EQ(2ul, manager->getNumberOfMetaVariables());
@@ -56,7 +56,7 @@ TEST(CuddDdManager, AddGetMetaVariableTest) {
     EXPECT_EQ(metaVariableSet, manager->getAllMetaVariableNames());
 }
 
-TEST(CuddDdManager, EncodingTest) {
+TEST(CuddDd, EncodingTest) {
     std::shared_ptr<storm::dd::DdManager<storm::dd::DdType::CUDD>> manager(new storm::dd::DdManager<storm::dd::DdType::CUDD>());
     std::pair<storm::expressions::Variable, storm::expressions::Variable> x = manager->addMetaVariable("x", 1, 9);
     
@@ -76,7 +76,7 @@ TEST(CuddDdManager, EncodingTest) {
     EXPECT_EQ(2ul, encoding.template toAdd<double>().getLeafCount());
 }
 
-TEST(CuddDdManager, RangeTest) {
+TEST(CuddDd, RangeTest) {
     std::shared_ptr<storm::dd::DdManager<storm::dd::DdType::CUDD>> manager(new storm::dd::DdManager<storm::dd::DdType::CUDD>());
     std::pair<storm::expressions::Variable, storm::expressions::Variable> x;
     ASSERT_NO_THROW(x = manager->addMetaVariable("x", 1, 9));
@@ -89,7 +89,7 @@ TEST(CuddDdManager, RangeTest) {
     EXPECT_EQ(5ul, range.getNodeCount());
 }
 
-TEST(CuddDdManager, IdentityTest) {
+TEST(CuddDd, IdentityTest) {
     std::shared_ptr<storm::dd::DdManager<storm::dd::DdType::CUDD>> manager(new storm::dd::DdManager<storm::dd::DdType::CUDD>());
     std::pair<storm::expressions::Variable, storm::expressions::Variable> x = manager->addMetaVariable("x", 1, 9);
     

test/functional/storage/SylvanDdTest.cpp

@@ -0,0 +1,409 @@
+#include "gtest/gtest.h"
+#include "storm-config.h"
+
+#include "src/exceptions/InvalidArgumentException.h"
+#include "src/storage/dd/DdManager.h"
+#include "src/storage/dd/Add.h"
+#include "src/storage/dd/Odd.h"
+#include "src/storage/dd/DdMetaVariable.h"
+#include "src/settings/SettingsManager.h"
+
+#include "src/storage/SparseMatrix.h"
+
+//TEST(SylvanDd, Constants) {
+//    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, double> zero;
+//    ASSERT_NO_THROW(zero = manager->template getAddZero<double>());
+//    
+//    EXPECT_EQ(0ul, zero.getNonZeroCount());
+//    EXPECT_EQ(1ul, zero.getLeafCount());
+//    EXPECT_EQ(1ul, zero.getNodeCount());
+//    EXPECT_EQ(0, zero.getMin());
+//    EXPECT_EQ(0, zero.getMax());
+//    
+//    storm::dd::Add<storm::dd::DdType::Sylvan, double> one;
+//    ASSERT_NO_THROW(one = manager->template getAddOne<double>());
+//    
+//    EXPECT_EQ(1ul, one.getNonZeroCount());
+//    EXPECT_EQ(1ul, one.getLeafCount());
+//    EXPECT_EQ(1ul, one.getNodeCount());
+//    EXPECT_EQ(1, one.getMin());
+//    EXPECT_EQ(1, one.getMax());
+//    
+//    storm::dd::Add<storm::dd::DdType::Sylvan, double> two;
+//    ASSERT_NO_THROW(two = manager->template getConstant<double>(2));
+//    
+//    EXPECT_EQ(1ul, two.getNonZeroCount());
+//    EXPECT_EQ(1ul, two.getLeafCount());
+//    EXPECT_EQ(1ul, two.getNodeCount());
+//    EXPECT_EQ(2, two.getMin());
+//    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());
+    
+//    // As an MTBDD, the 0-leaf is there, so the count is actually 2 and the node count is 6.
+//    EXPECT_EQ(6ul, encoding.template toAdd<double>().getNodeCount());
+//    EXPECT_EQ(2ul, encoding.template toAdd<double>().getLeafCount());
+}
+//
+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;
+    ASSERT_NO_THROW(x = manager->addMetaVariable("x", 1, 9));
+    
+    storm::dd::Bdd<storm::dd::DdType::Sylvan> range;
+    ASSERT_NO_THROW(range = manager->getRange(x.first));
+    
+    EXPECT_EQ(9ul, range.getNonZeroCount());
+    EXPECT_EQ(1ul, range.getLeafCount());
+    EXPECT_EQ(5ul, range.getNodeCount());
+}
+
+//TEST(SylvanDd, IdentityTest) {
+//    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, double> identity;
+//    ASSERT_NO_THROW(identity = manager->getIdentity<double>(x.first));
+//    
+//    EXPECT_EQ(9ul, identity.getNonZeroCount());
+//    EXPECT_EQ(10ul, identity.getLeafCount());
+//    EXPECT_EQ(21ul, identity.getNodeCount());
+//}
+//
+//TEST(SylvanDd, OperatorTest) {
+//    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);
+//    EXPECT_TRUE(manager->template getAddZero<double>() == manager->template getAddZero<double>());
+//    EXPECT_FALSE(manager->template getAddZero<double>() == manager->template getAddOne<double>());
+//    
+//    EXPECT_FALSE(manager->template getAddZero<double>() != manager->template getAddZero<double>());
+//    EXPECT_TRUE(manager->template getAddZero<double>() != manager->template getAddOne<double>());
+//    
+//    storm::dd::Add<storm::dd::DdType::Sylvan, double> dd1 = manager->template getAddOne<double>();
+//    storm::dd::Add<storm::dd::DdType::Sylvan, double> dd2 = manager->template getAddOne<double>();
+//    storm::dd::Add<storm::dd::DdType::Sylvan, double> dd3 = dd1 + dd2;
+//    EXPECT_TRUE(dd3 == manager->template getConstant<double>(2));
+//    
+//    dd3 += manager->template getAddZero<double>();
+//    EXPECT_TRUE(dd3 == manager->template getConstant<double>(2));
+//    
+//    dd3 = dd1 * manager->template getConstant<double>(3);
+//    EXPECT_TRUE(dd3 == manager->template getConstant<double>(3));
+//    
+//    dd3 *= manager->template getConstant<double>(2);
+//    EXPECT_TRUE(dd3 == manager->template getConstant<double>(6));
+//    
+//    dd3 = dd1 - dd2;
+//    EXPECT_TRUE(dd3.isZero());
+//    
+//    dd3 -= manager->template getConstant<double>(-2);
+//    EXPECT_TRUE(dd3 == manager->template getConstant<double>(2));
+//    
+//    dd3 /= manager->template getConstant<double>(2);
+//    EXPECT_TRUE(dd3.isOne());
+//    
+//    dd3 = !dd3;
+//    EXPECT_TRUE(dd3.isZero());
+//    
+//    dd1 = !dd3;
+//    EXPECT_TRUE(dd1.isOne());
+//    
+//    dd3 = dd1 || dd2;
+//    EXPECT_TRUE(dd3.isOne());
+//    
+//    dd1 = manager->template getIdentity<double>(x.first);
+//    dd2 = manager->template getConstant<double>(5);
+//    
+//    dd3 = dd1.equals(dd2);
+//    EXPECT_EQ(1ul, dd3.getNonZeroCount());
+//    
+//    storm::dd::Add<storm::dd::DdType::Sylvan, double> dd4 = dd1.notEquals(dd2);
+//    EXPECT_TRUE(dd4.toBdd() == !dd3.toBdd());
+//    
+//    dd3 = dd1.less(dd2);
+//    EXPECT_EQ(11ul, dd3.getNonZeroCount());
+//    
+//    dd3 = dd1.lessOrEqual(dd2);
+//    EXPECT_EQ(12ul, dd3.getNonZeroCount());
+//    
+//    dd3 = dd1.greater(dd2);
+//    EXPECT_EQ(4ul, dd3.getNonZeroCount());
+//    
+//    dd3 = dd1.greaterOrEqual(dd2);
+//    EXPECT_EQ(5ul, dd3.getNonZeroCount());
+//    
+//    dd3 = (manager->getEncoding(x.first, 2).template toAdd<double>()).ite(dd2, dd1);
+//    dd4 = dd3.less(dd2);
+//    EXPECT_EQ(10ul, dd4.getNonZeroCount());
+//    
+//    dd4 = dd3.minimum(dd1);
+//    dd4 *= manager->getEncoding(x.first, 2).template toAdd<double>();
+//    dd4 = dd4.sumAbstract({x.first});
+//    EXPECT_EQ(2, dd4.getValue());
+//    
+//    dd4 = dd3.maximum(dd1);
+//    dd4 *= manager->getEncoding(x.first, 2).template toAdd<double>();
+//    dd4 = dd4.sumAbstract({x.first});
+//    EXPECT_EQ(5, dd4.getValue());
+//    
+//    dd1 = manager->template getConstant<double>(0.01);
+//    dd2 = manager->template getConstant<double>(0.01 + 1e-6);
+//    EXPECT_TRUE(dd1.equalModuloPrecision(dd2, 1e-6, false));
+//    EXPECT_FALSE(dd1.equalModuloPrecision(dd2, 1e-6));
+//}
+//
+//TEST(SylvanDd, AbstractionTest) {
+//    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, double> dd1;
+//    storm::dd::Add<storm::dd::DdType::Sylvan, double> dd2;
+//    storm::dd::Add<storm::dd::DdType::Sylvan, double> dd3;
+//    
+//    dd1 = manager->template getIdentity<double>(x.first);
+//    dd2 = manager->template getConstant<double>(5);
+//    dd3 = dd1.equals(dd2);
+//    storm::dd::Bdd<storm::dd::DdType::Sylvan> dd3Bdd = dd3.toBdd();
+//    EXPECT_EQ(1ul, dd3Bdd.getNonZeroCount());
+//    ASSERT_THROW(dd3Bdd = dd3Bdd.existsAbstract({x.second}), storm::exceptions::InvalidArgumentException);
+//    ASSERT_NO_THROW(dd3Bdd = dd3Bdd.existsAbstract({x.first}));
+//    EXPECT_EQ(1ul, dd3Bdd.getNonZeroCount());
+//    EXPECT_EQ(1, dd3Bdd.template toAdd<double>().getMax());
+//    
+//    dd3 = dd1.equals(dd2);
+//    dd3 *= manager->template getConstant<double>(3);
+//    EXPECT_EQ(1ul, dd3.getNonZeroCount());
+//    ASSERT_THROW(dd3Bdd = dd3.toBdd().existsAbstract({x.second}), storm::exceptions::InvalidArgumentException);
+//    ASSERT_NO_THROW(dd3Bdd = dd3.toBdd().existsAbstract({x.first}));
+//    EXPECT_TRUE(dd3Bdd.isOne());
+//    
+//    dd3 = dd1.equals(dd2);
+//    dd3 *= manager->template getConstant<double>(3);
+//    ASSERT_THROW(dd3 = dd3.sumAbstract({x.second}), storm::exceptions::InvalidArgumentException);
+//    ASSERT_NO_THROW(dd3 = dd3.sumAbstract({x.first}));
+//    EXPECT_EQ(1ul, dd3.getNonZeroCount());
+//    EXPECT_EQ(3, dd3.getMax());
+//    
+//    dd3 = dd1.equals(dd2);
+//    dd3 *= manager->template getConstant<double>(3);
+//    ASSERT_THROW(dd3 = dd3.minAbstract({x.second}), storm::exceptions::InvalidArgumentException);
+//    ASSERT_NO_THROW(dd3 = dd3.minAbstract({x.first}));
+//    EXPECT_EQ(0ul, dd3.getNonZeroCount());
+//    EXPECT_EQ(0, dd3.getMax());
+//    
+//    dd3 = dd1.equals(dd2);
+//    dd3 *= manager->template getConstant<double>(3);
+//    ASSERT_THROW(dd3 = dd3.maxAbstract({x.second}), storm::exceptions::InvalidArgumentException);
+//    ASSERT_NO_THROW(dd3 = dd3.maxAbstract({x.first}));
+//    EXPECT_EQ(1ul, dd3.getNonZeroCount());
+//    EXPECT_EQ(3, dd3.getMax());
+//}
+//
+//TEST(SylvanDd, SwapTest) {
+//    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);
+//    std::pair<storm::expressions::Variable, storm::expressions::Variable> z = manager->addMetaVariable("z", 2, 8);
+//    storm::dd::Add<storm::dd::DdType::Sylvan, double> dd1;
+//    storm::dd::Add<storm::dd::DdType::Sylvan, double> dd2;
+//    
+//    dd1 = manager->template getIdentity<double>(x.first);
+//    ASSERT_THROW(dd1 = dd1.swapVariables({std::make_pair(x.first, z.first)}), storm::exceptions::InvalidArgumentException);
+//    ASSERT_NO_THROW(dd1 = dd1.swapVariables({std::make_pair(x.first, x.second)}));
+//    EXPECT_TRUE(dd1 == manager->template getIdentity<double>(x.second));
+//}
+//
+//TEST(SylvanDd, MultiplyMatrixTest) {
+//    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, double> dd1 = manager->template getIdentity<double>(x.first).equals(manager->template getIdentity<double>(x.second));
+//    storm::dd::Add<storm::dd::DdType::Sylvan, double> dd2 = manager->getRange(x.second).template toAdd<double>();
+//    storm::dd::Add<storm::dd::DdType::Sylvan, double> dd3;
+//    dd1 *= manager->template getConstant<double>(2);
+//    
+//    ASSERT_NO_THROW(dd3 = dd1.multiplyMatrix(dd2, {x.second}));
+//    ASSERT_NO_THROW(dd3 = dd3.swapVariables({std::make_pair(x.first, x.second)}));
+//    EXPECT_TRUE(dd3 == dd2 * manager->template getConstant<double>(2));
+//}
+//
+//TEST(SylvanDd, GetSetValueTest) {
+//    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, double> dd1 = manager->template getAddOne<double>();
+//    ASSERT_NO_THROW(dd1.setValue(x.first, 4, 2));
+//    EXPECT_EQ(2ul, dd1.getLeafCount());
+//    
+//    std::map<storm::expressions::Variable, int_fast64_t> metaVariableToValueMap;
+//    metaVariableToValueMap.emplace(x.first, 1);
+//    EXPECT_EQ(1, dd1.getValue(metaVariableToValueMap));
+//    
+//    metaVariableToValueMap.clear();
+//    metaVariableToValueMap.emplace(x.first, 4);
+//    EXPECT_EQ(2, dd1.getValue(metaVariableToValueMap));
+//}
+//
+//TEST(SylvanDd, ForwardIteratorTest) {
+//    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);
+//    std::pair<storm::expressions::Variable, storm::expressions::Variable> y = manager->addMetaVariable("y", 0, 3);
+//    
+//    storm::dd::Add<storm::dd::DdType::Sylvan, double> dd;
+//    ASSERT_NO_THROW(dd = manager->getRange(x.first).template toAdd<double>());
+//    
+//    storm::dd::AddIterator<storm::dd::DdType::Sylvan, double> it, ite;
+//    ASSERT_NO_THROW(it = dd.begin());
+//    ASSERT_NO_THROW(ite = dd.end());
+//    std::pair<storm::expressions::SimpleValuation, double> valuationValuePair;
+//    uint_fast64_t numberOfValuations = 0;
+//    while (it != ite) {
+//        ASSERT_NO_THROW(valuationValuePair = *it);
+//        ASSERT_NO_THROW(++it);
+//        ++numberOfValuations;
+//    }
+//    EXPECT_EQ(9ul, numberOfValuations);
+//    
+//    dd = manager->getRange(x.first).template toAdd<double>();
+//    dd = dd.ite(manager->template getAddOne<double>(), manager->template getAddOne<double>());
+//    ASSERT_NO_THROW(it = dd.begin());
+//    ASSERT_NO_THROW(ite = dd.end());
+//    numberOfValuations = 0;
+//    while (it != ite) {
+//        ASSERT_NO_THROW(valuationValuePair = *it);
+//        ASSERT_NO_THROW(++it);
+//        ++numberOfValuations;
+//    }
+//    EXPECT_EQ(16ul, numberOfValuations);
+//    
+//    ASSERT_NO_THROW(it = dd.begin(false));
+//    ASSERT_NO_THROW(ite = dd.end());
+//    numberOfValuations = 0;
+//    while (it != ite) {
+//        ASSERT_NO_THROW(valuationValuePair = *it);
+//        ASSERT_NO_THROW(++it);
+//        ++numberOfValuations;
+//    }
+//    EXPECT_EQ(1ul, numberOfValuations);
+//}
+//
+//TEST(SylvanDd, AddOddTest) {
+//    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> a = manager->addMetaVariable("a");
+//    std::pair<storm::expressions::Variable, storm::expressions::Variable> x = manager->addMetaVariable("x", 1, 9);
+//    
+//    storm::dd::Add<storm::dd::DdType::Sylvan, double> dd = manager->template getIdentity<double>(x.first);
+//    storm::dd::Odd odd;
+//    ASSERT_NO_THROW(odd = dd.createOdd());
+//    EXPECT_EQ(9ul, odd.getTotalOffset());
+//    EXPECT_EQ(12ul, odd.getNodeCount());
+//    
+//    std::vector<double> ddAsVector;
+//    ASSERT_NO_THROW(ddAsVector = dd.toVector());
+//    EXPECT_EQ(9ul, ddAsVector.size());
+//    for (uint_fast64_t i = 0; i < ddAsVector.size(); ++i) {
+//        EXPECT_TRUE(i+1 == ddAsVector[i]);
+//    }
+//    
+//    // Create a non-trivial matrix.
+//    dd = manager->template getIdentity<double>(x.first).equals(manager->template getIdentity<double>(x.second)) * manager->getRange(x.first).template toAdd<double>();
+//    dd += manager->getEncoding(x.first, 1).template toAdd<double>() * manager->getRange(x.second).template toAdd<double>() + manager->getEncoding(x.second, 1).template toAdd<double>() * manager->getRange(x.first).template toAdd<double>();
+//    
+//    // Create the ODDs.
+//    storm::dd::Odd rowOdd;
+//    ASSERT_NO_THROW(rowOdd = manager->getRange(x.first).template toAdd<double>().createOdd());
+//    storm::dd::Odd columnOdd;
+//    ASSERT_NO_THROW(columnOdd = manager->getRange(x.second).template toAdd<double>().createOdd());
+//    
+//    // Try to translate the matrix.
+//    storm::storage::SparseMatrix<double> matrix;
+//    ASSERT_NO_THROW(matrix = dd.toMatrix({x.first}, {x.second}, rowOdd, columnOdd));
+//    
+//    EXPECT_EQ(9ul, matrix.getRowCount());
+//    EXPECT_EQ(9ul, matrix.getColumnCount());
+//    EXPECT_EQ(25ul, matrix.getNonzeroEntryCount());
+//    
+//    dd = manager->getRange(x.first).template toAdd<double>() * manager->getRange(x.second).template toAdd<double>() * manager->getEncoding(a.first, 0).template toAdd<double>().ite(dd, dd + manager->template getConstant<double>(1));
+//    ASSERT_NO_THROW(matrix = dd.toMatrix({a.first}, rowOdd, columnOdd));
+//    EXPECT_EQ(18ul, matrix.getRowCount());
+//    EXPECT_EQ(9ul, matrix.getRowGroupCount());
+//    EXPECT_EQ(9ul, matrix.getColumnCount());
+//    EXPECT_EQ(106ul, matrix.getNonzeroEntryCount());
+//}
+//
+//TEST(SylvanDd, BddOddTest) {
+//    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> a = manager->addMetaVariable("a");
+//    std::pair<storm::expressions::Variable, storm::expressions::Variable> x = manager->addMetaVariable("x", 1, 9);
+//    
+//    storm::dd::Add<storm::dd::DdType::Sylvan, double> dd = manager->template getIdentity<double>(x.first);
+//    storm::dd::Odd odd;
+//    ASSERT_NO_THROW(odd = dd.createOdd());
+//    EXPECT_EQ(9ul, odd.getTotalOffset());
+//    EXPECT_EQ(12ul, odd.getNodeCount());
+//    
+//    std::vector<double> ddAsVector;
+//    ASSERT_NO_THROW(ddAsVector = dd.toVector());
+//    EXPECT_EQ(9ul, ddAsVector.size());
+//    for (uint_fast64_t i = 0; i < ddAsVector.size(); ++i) {
+//        EXPECT_TRUE(i+1 == ddAsVector[i]);
+//    }
+//    
+//    storm::dd::Add<storm::dd::DdType::Sylvan, double> vectorAdd = storm::dd::Add<storm::dd::DdType::Sylvan, double>::fromVector(manager, ddAsVector, odd, {x.first});
+//    
+//    // Create a non-trivial matrix.
+//    dd = manager->template getIdentity<double>(x.first).equals(manager->template getIdentity<double>(x.second)) * manager->getRange(x.first).template toAdd<double>();
+//    dd += manager->getEncoding(x.first, 1).template toAdd<double>() * manager->getRange(x.second).template toAdd<double>() + manager->getEncoding(x.second, 1).template toAdd<double>() * manager->getRange(x.first).template toAdd<double>();
+//    
+//    // Create the ODDs.
+//    storm::dd::Odd rowOdd;
+//    ASSERT_NO_THROW(rowOdd = manager->getRange(x.first).createOdd());
+//    storm::dd::Odd columnOdd;
+//    ASSERT_NO_THROW(columnOdd = manager->getRange(x.second).createOdd());
+//    
+//    // Try to translate the matrix.
+//    storm::storage::SparseMatrix<double> matrix;
+//    ASSERT_NO_THROW(matrix = dd.toMatrix({x.first}, {x.second}, rowOdd, columnOdd));
+//    
+//    EXPECT_EQ(9ul, matrix.getRowCount());
+//    EXPECT_EQ(9ul, matrix.getColumnCount());
+//    EXPECT_EQ(25ul, matrix.getNonzeroEntryCount());
+//    
+//    dd = manager->getRange(x.first).template toAdd<double>() * manager->getRange(x.second).template toAdd<double>() * manager->getEncoding(a.first, 0).template toAdd<double>().ite(dd, dd + manager->template getConstant<double>(1));
+//    ASSERT_NO_THROW(matrix = dd.toMatrix({a.first}, rowOdd, columnOdd));
+//    EXPECT_EQ(18ul, matrix.getRowCount());
+//    EXPECT_EQ(9ul, matrix.getRowGroupCount());
+//    EXPECT_EQ(9ul, matrix.getColumnCount());
+//    EXPECT_EQ(106ul, matrix.getNonzeroEntryCount());
+//}