more work on sylvan

Former-commit-id: c1bfcd83ee

resources/3rdparty/sylvan/src/sylvan_obj.cpp

@@ -340,10 +340,10 @@ Bdd::GetShaHash() const
 }
 
 double
-Bdd::SatCount(const Bdd &variables) const
+Bdd::SatCount(size_t variableCount) const
 {
     LACE_ME;
-    return sylvan_satcount_cached(bdd, variables.bdd);
+    return mtbdd_satcount(bdd, variableCount);
 }
 
 void
@@ -986,6 +986,30 @@ Mtbdd::Logxy(const Mtbdd& other) const {
     return mtbdd_logxy(mtbdd, other.mtbdd);
 }
 
+size_t
+Mtbdd::CountLeaves() const {
+    LACE_ME;
+    return mtbdd_leafcount(mtbdd);
+}
+
+double
+Mtbdd::NonZeroCount(size_t variableCount) const {
+    LACE_ME;
+    return mtbdd_non_zero_count(mtbdd, variableCount);
+}
+
+Mtbdd
+Mtbdd::Permute(const std::vector<Bdd>& from, const std::vector<Bdd>& to) const {
+    LACE_ME;
+    
+    /* Create a map */
+    MtbddMap map;
+    for (int i=from.size()-1; i>=0; i--) {
+        map.put(from[i].TopVar(), to[i]);
+    }
+    
+    return sylvan_compose(mtbdd, map.mtbdd);
+}
 
 Mtbdd
 Mtbdd::Support() const
@@ -1008,10 +1032,10 @@ Mtbdd::Compose(MtbddMap &m) const
 }
 
 double
-Mtbdd::SatCount(const Mtbdd &variables) const
+Mtbdd::SatCount(size_t variableCount) const
 {
     LACE_ME;
-    return mtbdd_satcount(mtbdd, variables.mtbdd);
+    return mtbdd_satcount(mtbdd, variableCount);
 }
 
 size_t
@@ -1021,7 +1045,6 @@ Mtbdd::NodeCount() const
     return mtbdd_nodecount(mtbdd);
 }
 
-
 /***
  * Implementation of class MtbddMap
  */

resources/3rdparty/sylvan/src/sylvan_obj.hpp

@@ -273,7 +273,7 @@ public:
     /**
      * @brief Computes the number of satisfying variable assignments, using variables in cube.
      */
-    double SatCount(const Bdd &variables) const;
+    double SatCount(size_t variableCount) const;
 
     /**
      * @brief Gets one satisfying assignment according to the variables.
@@ -617,6 +617,10 @@ public:
     Mtbdd Mod(const Mtbdd& other) const;
 
     Mtbdd Logxy(const Mtbdd& other) const;
+    
+    size_t CountLeaves() const;
+    
+    Mtbdd Permute(const std::vector<Bdd>& from, const std::vector<Bdd>& to) const;
 
     /**
      * @brief Computes the support of a Mtbdd.
@@ -638,8 +642,13 @@ public:
     /**
      * @brief Compute the number of satisfying variable assignments, using variables in cube.
      */
-    double SatCount(const Mtbdd &variables) const;
+    double SatCount(size_t variableCount) const;
 
+    /**
+     * @brief Compute the number of non-zero variable assignments, using variables in cube.
+     */
+    double NonZeroCount(size_t variableCount) const;
+    
     /**
      * @brief Gets the number of nodes in this Bdd. Not thread-safe!
      */

resources/3rdparty/sylvan/src/sylvan_storm_custom.c

@@ -380,7 +380,9 @@ TASK_IMPL_2(MTBDD, mtbdd_op_not_zero, MTBDD, a, size_t, v)
     }
     
     // Ugly hack to get rid of the error "unused variable v" (because there is no version of uapply without a parameter).
-    return v > 0 ? mtbdd_invalid : mtbdd_invalid;
+    (void)v;
+    
+    return mtbdd_invalid;
 }
 
 TASK_IMPL_1(MTBDD, mtbdd_not_zero, MTBDD, dd)
@@ -410,7 +412,9 @@ TASK_IMPL_2(MTBDD, mtbdd_op_floor, MTBDD, a, size_t, v)
     }
     
     // Ugly hack to get rid of the error "unused variable v" (because there is no version of uapply without a parameter).
-    return v > 0 ? mtbdd_invalid : mtbdd_invalid;
+    (void)v;
+    
+    return mtbdd_invalid;
 }
 
 TASK_IMPL_1(MTBDD, mtbdd_floor, MTBDD, dd)
@@ -438,9 +442,11 @@ TASK_IMPL_2(MTBDD, mtbdd_op_ceil, MTBDD, a, size_t, v)
             return mtbdd_isnegated(a) ? mtbdd_negate(result) : result;
         }
     }
-    
+
     // Ugly hack to get rid of the error "unused variable v" (because there is no version of uapply without a parameter).
-    return v > 0 ? mtbdd_invalid : mtbdd_invalid;
+    (void)v;
+    
+    return mtbdd_invalid;
 }
 
 TASK_IMPL_1(MTBDD, mtbdd_ceil, MTBDD, dd)
@@ -455,10 +461,54 @@ TASK_IMPL_2(MTBDD, mtbdd_op_bool_to_double, MTBDD, a, size_t, v)
     if (a == mtbdd_true) return mtbdd_double(1.0);
     
     // Ugly hack to get rid of the error "unused variable v" (because there is no version of uapply without a parameter).
-    return v > 0 ? mtbdd_invalid : mtbdd_invalid;
+    (void)v;
+    
+    return mtbdd_invalid;
 }
 
 TASK_IMPL_1(MTBDD, mtbdd_bool_to_double, MTBDD, dd)
 {
     return mtbdd_uapply(dd, TASK(mtbdd_op_bool_to_double), 0);
 }
+
+/**
+ * Calculate the number of satisfying variable assignments according to <variables>.
+ */
+TASK_IMPL_2(double, mtbdd_non_zero_count, MTBDD, dd, size_t, nvars)
+{
+    /* Trivial cases */
+    if (dd == mtbdd_false) return 0.0;
+
+    mtbddnode_t na = GETNODE(dd);
+    
+    if (mtbdd_isleaf(dd)) {
+        if (mtbddnode_gettype(na) == 0) {
+            return mtbdd_getuint64(dd) != 0 ? powl(2.0L, nvars) : 0.0;
+        } else if (mtbddnode_gettype(na) == 1) {
+            return mtbdd_getdouble(dd) != 0 ? powl(2.0L, nvars) : 0.0;
+        } else if (mtbddnode_gettype(na) == 2) {
+            return mtbdd_getnumer(dd) != 0 ? powl(2.0L, nvars) : 0.0;
+        }
+    }
+    
+    /* Perhaps execute garbage collection */
+    sylvan_gc_test();
+    
+    union {
+        double d;
+        uint64_t s;
+    } hack;
+    
+    /* Consult cache */
+    if (cache_get3(CACHE_BDD_SATCOUNT, dd, 0, nvars, &hack.s)) {
+        sylvan_stats_count(BDD_SATCOUNT_CACHED);
+        return hack.d;
+    }
+    
+    SPAWN(mtbdd_non_zero_count, mtbdd_gethigh(dd), nvars-1);
+    double low = CALL(mtbdd_non_zero_count, mtbdd_getlow(dd), nvars-1);
+    hack.d = low + SYNC(mtbdd_non_zero_count);
+    
+    cache_put3(CACHE_BDD_SATCOUNT, dd, 0, nvars, hack.s);
+    return hack.d;
+}

resources/3rdparty/sylvan/src/sylvan_storm_custom.h

@@ -93,3 +93,10 @@ TASK_DECL_1(MTBDD, mtbdd_ceil, MTBDD)
 TASK_DECL_2(MTBDD, mtbdd_op_bool_to_double, MTBDD, size_t)
 TASK_DECL_1(MTBDD, mtbdd_bool_to_double, MTBDD)
 #define mtbdd_bool_to_double(dd) CALL(mtbdd_bool_to_double, dd)
+
+/**
+ * Count the number of assignments (minterms) leading to a non-zero
+ */
+TASK_DECL_2(double, mtbdd_non_zero_count, MTBDD, size_t);
+#define mtbdd_non_zero_count(dd, nvars) CALL(mtbdd_non_zero_count, dd, nvars)
+

src/storage/dd/Add.cpp

@@ -185,8 +185,8 @@ namespace storm {
         template<DdType LibraryType, typename ValueType>
         Add<LibraryType, ValueType> Add<LibraryType, ValueType>::swapVariables(std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& metaVariablePairs) const {
             std::set<storm::expressions::Variable> newContainedMetaVariables;
-            std::vector<InternalAdd<LibraryType, ValueType>> from;
-            std::vector<InternalAdd<LibraryType, ValueType>> to;
+            std::vector<InternalBdd<LibraryType>> from;
+            std::vector<InternalBdd<LibraryType>> to;
             for (auto const& metaVariablePair : metaVariablePairs) {
                 DdMetaVariable<LibraryType> const& variable1 = this->getDdManager()->getMetaVariable(metaVariablePair.first);
                 DdMetaVariable<LibraryType> const& variable2 = this->getDdManager()->getMetaVariable(metaVariablePair.second);
@@ -200,10 +200,10 @@ namespace storm {
                 }
                 
                 for (auto const& ddVariable : variable1.getDdVariables()) {
-                    from.push_back(ddVariable.template toAdd<ValueType>());
+                    from.push_back(ddVariable);
                 }
                 for (auto const& ddVariable : variable2.getDdVariables()) {
-                    to.push_back(ddVariable.template toAdd<ValueType>());
+                    to.push_back(ddVariable);
                 }
             }
             STORM_LOG_THROW(from.size() == to.size(), storm::exceptions::InvalidArgumentException, "Unable to swap mismatching meta variables.");
@@ -270,16 +270,10 @@ namespace storm {
         template<DdType LibraryType, typename ValueType>
         uint_fast64_t Add<LibraryType, ValueType>::getNonZeroCount() const {
             std::size_t numberOfDdVariables = 0;
-            if (LibraryType == DdType::CUDD) {
-                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());
+            for (auto const& metaVariable : this->getContainedMetaVariables()) {
+                numberOfDdVariables += this->getDdManager()->getMetaVariable(metaVariable).getNumberOfDdVariables();
             }
-            return internalAdd.getNonZeroCount(cube, numberOfDdVariables);
+            return internalAdd.getNonZeroCount(numberOfDdVariables);
         }
         
         template<DdType LibraryType, typename ValueType>

src/storage/dd/Bdd.cpp

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

src/storage/dd/cudd/InternalCuddAdd.cpp

@@ -166,13 +166,13 @@ namespace storm {
         }
         
         template<typename ValueType>
-        InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::swapVariables(std::vector<InternalAdd<DdType::CUDD, ValueType>> const& from, std::vector<InternalAdd<DdType::CUDD, ValueType>> const& to) const {
+        InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::swapVariables(std::vector<InternalBdd<DdType::CUDD>> const& from, std::vector<InternalBdd<DdType::CUDD>> const& to) const {
             std::vector<cudd::ADD> fromAdd;
             std::vector<cudd::ADD> toAdd;
             STORM_LOG_ASSERT(fromAdd.size() == toAdd.size(), "Sizes of vectors do not match.");
             for (auto it1 = from.begin(), ite1 = from.end(), it2 = to.begin(); it1 != ite1; ++it1, ++it2) {
-                fromAdd.push_back(it1->getCuddAdd());
-                toAdd.push_back(it2->getCuddAdd());
+                fromAdd.push_back(it1->getCuddBdd().Add());
+                toAdd.push_back(it2->getCuddBdd().Add());
             }
             return InternalAdd<DdType::CUDD, ValueType>(ddManager, this->getCuddAdd().SwapVariables(fromAdd, toAdd));
         }
@@ -229,7 +229,12 @@ namespace storm {
         }
         
         template<typename ValueType>
-        uint_fast64_t InternalAdd<DdType::CUDD, ValueType>::getNonZeroCount(InternalBdd<DdType::CUDD> const& cube, uint_fast64_t numberOfDdVariables) const {
+        uint_fast64_t InternalAdd<DdType::CUDD, ValueType>::getNonZeroCount(uint_fast64_t numberOfDdVariables) const {
+            // If the number of DD variables is zero, CUDD returns a number greater 0 for constant nodes different from
+            // zero, which is not the behaviour we expect.
+            if (numberOfDdVariables == 0) {
+                return 0;
+            }
             return static_cast<uint_fast64_t>(this->getCuddAdd().CountMinterm(static_cast<int>(numberOfDdVariables)));
         }
         

src/storage/dd/cudd/InternalCuddAdd.h

@@ -287,13 +287,13 @@ namespace storm {
             
             /*!
              * Swaps the given pairs of DD variables in the ADD. The pairs of meta variables have to be represented by
-             * ADDs must have equal length.
+             * vectors of BDDs must have equal length.
              *
              * @param from The vector that specifies the 'from' part of the variable renaming.
              * @param to The vector that specifies the 'to' part of the variable renaming.
              * @return The resulting ADD.
              */
-            InternalAdd<DdType::CUDD, ValueType> swapVariables(std::vector<InternalAdd<DdType::CUDD, ValueType>> const& from, std::vector<InternalAdd<DdType::CUDD, ValueType>> const& to) const;
+            InternalAdd<DdType::CUDD, ValueType> swapVariables(std::vector<InternalBdd<DdType::CUDD>> const& from, std::vector<InternalBdd<DdType::CUDD>> const& to) const;
             
             /*!
              * Multiplies the current ADD (representing a matrix) with the given matrix by summing over the given meta
@@ -379,11 +379,10 @@ namespace storm {
             /*!
              * Retrieves the number of encodings that are mapped to a non-zero value.
              *
-             * @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(InternalBdd<DdType::CUDD> const& cube, uint_fast64_t numberOfDdVariables) const;
+            uint_fast64_t getNonZeroCount(uint_fast64_t numberOfDdVariables) const;
             
             /*!
              * Retrieves the number of leaves of the ADD.

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(InternalBdd<DdType::CUDD> const& cube, uint_fast64_t numberOfDdVariables) const {
+        uint_fast64_t InternalBdd<DdType::CUDD>::getNonZeroCount(uint_fast64_t numberOfDdVariables) const {
             return static_cast<uint_fast64_t>(this->getCuddBdd().CountMinterm(static_cast<int>(numberOfDdVariables)));
         }
         

src/storage/dd/cudd/InternalCuddBdd.h

@@ -220,11 +220,10 @@ namespace storm {
             /*!
              * Retrieves the number of encodings that are mapped to a non-zero value.
              *
-             * @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(InternalBdd<DdType::CUDD> const& cube, uint_fast64_t numberOfDdVariables) const;
+            uint_fast64_t getNonZeroCount(uint_fast64_t numberOfDdVariables) const;
             
             /*!
              * Retrieves the number of leaves of the DD.

src/storage/dd/sylvan/InternalSylvanAdd.cpp

@@ -1,5 +1,7 @@
 #include "src/storage/dd/sylvan/InternalSylvanAdd.h"
 
+#include <iostream>
+
 #include "src/storage/dd/sylvan/InternalSylvanDdManager.h"
 
 #include "src/utility/macros.h"
@@ -161,8 +163,14 @@ namespace storm {
         }
         
         template<typename ValueType>
-        InternalAdd<DdType::Sylvan, ValueType> InternalAdd<DdType::Sylvan, ValueType>::swapVariables(std::vector<InternalAdd<DdType::Sylvan, ValueType>> const& from, std::vector<InternalAdd<DdType::Sylvan, ValueType>> const& to) const {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented.");
+        InternalAdd<DdType::Sylvan, ValueType> InternalAdd<DdType::Sylvan, ValueType>::swapVariables(std::vector<InternalBdd<DdType::Sylvan>> const& from, std::vector<InternalBdd<DdType::Sylvan>> const& to) const {
+            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 InternalAdd<DdType::Sylvan, ValueType>(ddManager, this->sylvanMtbdd.Permute(fromBdd, toBdd));
         }
         
         template<typename ValueType>
@@ -215,18 +223,21 @@ namespace storm {
         }
         
         template<typename ValueType>
-        uint_fast64_t InternalAdd<DdType::Sylvan, ValueType>::getNonZeroCount(InternalBdd<DdType::Sylvan> const& cube, uint_fast64_t numberOfDdVariables) const {
-            return static_cast<uint_fast64_t>(this->sylvanMtbdd.SatCount(cube.sylvanBdd));
+        uint_fast64_t InternalAdd<DdType::Sylvan, ValueType>::getNonZeroCount(uint_fast64_t numberOfDdVariables) const {
+            if (numberOfDdVariables == 0) {
+                return 0;
+            }
+            return static_cast<uint_fast64_t>(this->sylvanMtbdd.NonZeroCount(numberOfDdVariables));
         }
         
         template<typename ValueType>
         uint_fast64_t InternalAdd<DdType::Sylvan, ValueType>::getLeafCount() const {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented.");
+            return static_cast<uint_fast64_t>(this->sylvanMtbdd.CountLeaves());
         }
         
         template<typename ValueType>
         uint_fast64_t InternalAdd<DdType::Sylvan, ValueType>::getNodeCount() const {
-            return static_cast<uint_fast64_t>(this->sylvanMtbdd.NodeCount()) + this->getLeafCount();
+            return static_cast<uint_fast64_t>(this->sylvanMtbdd.NodeCount());
         }
         
         template<typename ValueType>

src/storage/dd/sylvan/InternalSylvanAdd.h

@@ -293,7 +293,7 @@ namespace storm {
              * @param to The vector that specifies the 'to' part of the variable renaming.
              * @return The resulting ADD.
              */
-            InternalAdd<DdType::Sylvan, ValueType> swapVariables(std::vector<InternalAdd<DdType::Sylvan, ValueType>> const& from, std::vector<InternalAdd<DdType::Sylvan, ValueType>> const& to) const;
+            InternalAdd<DdType::Sylvan, ValueType> swapVariables(std::vector<InternalBdd<DdType::Sylvan>> const& from, std::vector<InternalBdd<DdType::Sylvan>> const& to) const;
             
             /*!
              * Multiplies the current ADD (representing a matrix) with the given matrix by summing over the given meta
@@ -379,11 +379,10 @@ namespace storm {
             /*!
              * Retrieves the number of encodings that are mapped to a non-zero value.
              *
-             * @param cube The cube of variables contained in this BDD.
-             * @param numberOfDdVariables The number of DD variables contained in this BDD. This 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.
              */
-            virtual uint_fast64_t getNonZeroCount(InternalBdd<DdType::Sylvan> const& cube, uint_fast64_t numberOfDdVariables) const;
+            virtual uint_fast64_t getNonZeroCount(uint_fast64_t numberOfDdVariables) const;
             
             /*!
              * Retrieves the number of leaves of the ADD.

src/storage/dd/sylvan/InternalSylvanBdd.cpp

@@ -104,8 +104,11 @@ namespace storm {
             return InternalBdd<DdType::Sylvan>(ddManager, this->sylvanBdd.Support());
         }
         
-        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>::getNonZeroCount(uint_fast64_t numberOfDdVariables) const {
+            if (numberOfDdVariables == 0) {
+                return 0;
+            }
+            return static_cast<uint_fast64_t>(this->sylvanBdd.SatCount(numberOfDdVariables));
         }
         
         uint_fast64_t InternalBdd<DdType::Sylvan>::getLeafCount() const {

src/storage/dd/sylvan/InternalSylvanBdd.h

@@ -209,11 +209,10 @@ namespace storm {
             /*!
              * Retrieves the number of encodings that are mapped to a non-zero value.
              *
-             * @param cube The cube of variables contained in this BDD.
-             * @param numberOfDdVariables The number of DD variables contained in this BDD. This 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(InternalBdd<DdType::Sylvan> const& cube, uint_fast64_t numberOfDdVariables) const;
+            uint_fast64_t getNonZeroCount(uint_fast64_t numberOfDdVariables) const;
             
             /*!
              * Retrieves the number of leaves of the DD.

src/storage/dd/sylvan/InternalSylvanDdManager.cpp

@@ -12,7 +12,7 @@ namespace storm {
         
         InternalDdManager<DdType::Sylvan>::InternalDdManager() {
             if (numberOfInstances == 0) {
-                // Initialize lace: auto-detecting number of workers.
+                // Initialize lace: auto-detect number of workers.
                 lace_init(0, 1000000);
                 lace_startup(0, 0, 0);
                 
@@ -27,6 +27,7 @@ namespace storm {
             --numberOfInstances;
             if (numberOfInstances == 0) {
                 sylvan::Sylvan::quitPackage();
+                lace_exit();
             }
         }
         

test/functional/storage/CuddDdTest.cpp

@@ -23,7 +23,7 @@ TEST(CuddDd, Constants) {
     storm::dd::Add<storm::dd::DdType::CUDD, double> one;
     ASSERT_NO_THROW(one = manager->template getAddOne<double>());
     
-    EXPECT_EQ(1ul, one.getNonZeroCount());
+    EXPECT_EQ(0ul, one.getNonZeroCount());
     EXPECT_EQ(1ul, one.getLeafCount());
     EXPECT_EQ(1ul, one.getNodeCount());
     EXPECT_EQ(1, one.getMin());
@@ -32,7 +32,7 @@ TEST(CuddDd, Constants) {
     storm::dd::Add<storm::dd::DdType::CUDD, double> two;
     ASSERT_NO_THROW(two = manager->template getConstant<double>(2));
     
-    EXPECT_EQ(1ul, two.getNonZeroCount());
+    EXPECT_EQ(0ul, two.getNonZeroCount());
     EXPECT_EQ(1ul, two.getLeafCount());
     EXPECT_EQ(1ul, two.getNodeCount());
     EXPECT_EQ(2, two.getMin());
@@ -212,7 +212,7 @@ TEST(CuddDd, AbstractionTest) {
     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(0ul, dd3.getNonZeroCount());
     EXPECT_EQ(3, dd3.getMax());
 
     dd3 = dd1.equals(dd2).template toAdd<double>();
@@ -226,7 +226,7 @@ TEST(CuddDd, AbstractionTest) {
     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(0ul, dd3.getNonZeroCount());
     EXPECT_EQ(3, dd3.getMax());
 }
 

test/functional/storage/SylvanDdTest.cpp

@@ -10,35 +10,35 @@
 
 #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, 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(0ul, 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(0ul, 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>());
@@ -72,11 +72,17 @@ TEST(SylvanDd, EncodingTest) {
     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());
+    encoding.exportToDot("encoding.dot");
+    
+    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.
+    add.exportToDot("add.dot");
+    EXPECT_EQ(6ul, add.getNodeCount());
+    EXPECT_EQ(2ul, add.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;
@@ -90,18 +96,18 @@ TEST(SylvanDd, RangeTest) {
     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, 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);
@@ -213,7 +219,7 @@ TEST(SylvanDd, OperatorTest) {
 //    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(0ul, dd3.getNonZeroCount());
 //    EXPECT_EQ(3, dd3.getMax());
 //    
 //    dd3 = dd1.equals(dd2);
@@ -227,7 +233,7 @@ TEST(SylvanDd, OperatorTest) {
 //    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(0ul, dd3.getNonZeroCount());
 //    EXPECT_EQ(3, dd3.getMax());
 //}
 //