merged sylvan updates into the sylvan copy. made more tests work

Former-commit-id: 18023e03c2

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

@@ -53,14 +53,6 @@ VOID_TASK_0(llmsset_reset_region)
     SET_THREAD_LOCAL(my_region, my_region);
 }
 
-VOID_TASK_0(llmsset_init_worker)
-{
-    // yes, ugly. for now, we use a global thread-local value.
-    // that is a problem with multiple tables.
-    // so, for now, do NOT use multiple tables!!
-    CALL(llmsset_reset_region);
-}
-
 static uint64_t
 claim_data_bucket(const llmsset_t dbs)
 {
@@ -385,9 +377,13 @@ llmsset_create(size_t initial_size, size_t max_size)
     dbs->create_cb = NULL;
     dbs->destroy_cb = NULL;
 
+    // yes, ugly. for now, we use a global thread-local value.
+    // that is a problem with multiple tables.
+    // so, for now, do NOT use multiple tables!!
+
     LACE_ME;
     INIT_THREAD_LOCAL(my_region);
-    TOGETHER(llmsset_init_worker);
+    TOGETHER(llmsset_reset_region);
 
     return dbs;
 }

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

@@ -14,8 +14,8 @@
  * limitations under the License.
  */
 
+#include <sylvan_config.h>
 #include <stdint.h> // for uint32_t etc
-#include "sylvan_config.h"
 
 #ifndef REFS_INLINE_H
 #define REFS_INLINE_H

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

@@ -16,7 +16,7 @@
 
 /* Do not include this file directly. Instead, include sylvan.h */
 
-#include "tls.h"
+#include <tls.h>
 
 #ifndef SYLVAN_BDD_H
 #define SYLVAN_BDD_H
@@ -263,13 +263,10 @@ void sylvan_getsha(BDD bdd, char *target); // target must be at least 65 bytes..
 /**
  * Calculate number of satisfying variable assignments.
  * The set of variables must be >= the support of the BDD.
- * 
- * The cached version uses the operation cache, but is limited to 64-bit floating point numbers.
  */
 
 TASK_DECL_3(double, sylvan_satcount, BDD, BDDSET, BDDVAR);
 #define sylvan_satcount(bdd, variables) CALL(sylvan_satcount, bdd, variables, 0)
-#define sylvan_satcount_cached(bdd, variables) CALL(sylvan_satcount, bdd, variables, 0)
 
 /**
  * Create a BDD cube representing the conjunction of variables in their positive or negative

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

@@ -16,6 +16,7 @@
 
 #include <sylvan_config.h>
 
+#include <sylvan.h>
 #include <sylvan_common.h>
 
 #ifndef cas

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

@@ -14,11 +14,6 @@
  * limitations under the License.
  */
 
-#include <assert.h>
-#include "sylvan.h"
-#include "tls.h"
-#include "sylvan_config.h"
-
 #ifndef SYLVAN_COMMON_H
 #define SYLVAN_COMMON_H
 

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

@@ -14,7 +14,7 @@
  * limitations under the License.
  */
 
-#include "sylvan_obj.hpp"
+#include <sylvan_obj.hpp>
 
 using namespace sylvan;
 
@@ -340,10 +340,19 @@ Bdd::GetShaHash() const
 }
 
 double
-Bdd::SatCount(size_t variableCount) const
+Bdd::SatCount(const Bdd &variables) const
 {
     LACE_ME;
-    return mtbdd_satcount(bdd, variableCount);
+    return sylvan_satcount(bdd, variables.bdd);
+}
+
+
+double
+Bdd::SatCount(size_t nvars) const
+{
+    LACE_ME;
+    // Note: the mtbdd_satcount can be called without initializing the MTBDD module.
+    return mtbdd_satcount(bdd, nvars);
 }
 
 void
@@ -443,12 +452,6 @@ Bdd::NodeCount() const
     return sylvan_nodecount(bdd);
 }
 
-Mtbdd
-Bdd::toDoubleMtbdd() const {
-    LACE_ME;
-    return mtbdd_bool_to_double(bdd);
-}
-
 Bdd
 Bdd::bddOne()
 {
@@ -730,14 +733,6 @@ Mtbdd::Plus(const Mtbdd &other) const
     return mtbdd_plus(mtbdd, other.mtbdd);
 }
 
-Mtbdd
-Mtbdd::Minus(const Mtbdd &other) const
-{
-    LACE_ME;
-    return mtbdd_minus(mtbdd, other.mtbdd);
-}
-
-
 Mtbdd
 Mtbdd::Times(const Mtbdd &other) const
 {
@@ -745,13 +740,6 @@ Mtbdd::Times(const Mtbdd &other) const
     return mtbdd_times(mtbdd, other.mtbdd);
 }
 
-Mtbdd
-Mtbdd::Divide(const Mtbdd &other) const
-{
-    LACE_ME;
-    return mtbdd_divide(mtbdd, other.mtbdd);
-}
-
 Mtbdd
 Mtbdd::Min(const Mtbdd &other) const
 {
@@ -905,101 +893,29 @@ Mtbdd::BddStrictThreshold(double value) const
     return mtbdd_strict_threshold_double(mtbdd, value);
 }
 
-Bdd
-Mtbdd::NotZero() const
-{
-    LACE_ME;
-    return mtbdd_not_zero(mtbdd);
-}
-
-Bdd
-Mtbdd::Equals(const Mtbdd& other) const {
-    LACE_ME;
-    return mtbdd_equals(mtbdd, other.mtbdd);
-}
-
-Bdd
-Mtbdd::Less(const Mtbdd& other) const {
-    LACE_ME;
-    return mtbdd_less_as_bdd(mtbdd, other.mtbdd);
-}
-
-Bdd
-Mtbdd::LessOrEqual(const Mtbdd& other) const {
-    LACE_ME;
-    return mtbdd_less_or_equal_as_bdd(mtbdd, other.mtbdd);
-}
-
-double
-Mtbdd::getDoubleMax() const {
-    LACE_ME;
-    MTBDD maxNode = mtbdd_maximum(mtbdd);
-    return mtbdd_getdouble(maxNode);
-}
-
-double
-Mtbdd::getDoubleMin() const {
-    LACE_ME;
-    MTBDD minNode = mtbdd_minimum(mtbdd);
-    return mtbdd_getdouble(minNode);
-}
-
-bool
-Mtbdd::EqualNorm(const Mtbdd& other, double epsilon) const {
-    LACE_ME;
-    return mtbdd_equal_norm_d(mtbdd, other.mtbdd, epsilon);
-}
-
-bool
-Mtbdd::EqualNormRel(const Mtbdd& other, double epsilon) const {
-    LACE_ME;
-    return mtbdd_equal_norm_rel_d(mtbdd, other.mtbdd, epsilon);
-}
-
 Mtbdd
-Mtbdd::Floor() const {
-    LACE_ME;
-    return mtbdd_floor(mtbdd);
-}
-
-Mtbdd
-Mtbdd::Ceil() const {
-    LACE_ME;
-    return mtbdd_ceil(mtbdd);
-}
-
-Mtbdd
-Mtbdd::Pow(const Mtbdd& other) const {
+Mtbdd::Support() const
+{
     LACE_ME;
-    return mtbdd_pow(mtbdd, other.mtbdd);
+    return mtbdd_support(mtbdd);
 }
 
-Mtbdd
-Mtbdd::Mod(const Mtbdd& other) const {
-    LACE_ME;
-    return mtbdd_mod(mtbdd, other.mtbdd);
+MTBDD
+Mtbdd::GetMTBDD() const
+{
+    return mtbdd;
 }
 
 Mtbdd
-Mtbdd::Logxy(const Mtbdd& other) const {
-    LACE_ME;
-    return mtbdd_logxy(mtbdd, other.mtbdd);
-}
-
-size_t
-Mtbdd::CountLeaves() const {
-    LACE_ME;
-    return mtbdd_leafcount(mtbdd);
-}
-
-double
-Mtbdd::NonZeroCount(size_t variableCount) const {
+Mtbdd::Compose(MtbddMap &m) const
+{
     LACE_ME;
-    return mtbdd_non_zero_count(mtbdd, variableCount);
+    return mtbdd_compose(mtbdd, m.mtbdd);
 }
 
 Mtbdd
-Mtbdd::Permute(const std::vector<Bdd>& from, const std::vector<Bdd>& to) const {
+Mtbdd::Permute(const std::vector<Mtbdd>& from, const std::vector<Mtbdd>& to) const
+{
     LACE_ME;
     
     /* Create a map */
@@ -1008,34 +924,20 @@ Mtbdd::Permute(const std::vector<Bdd>& from, const std::vector<Bdd>& to) const {
         map.put(from[i].TopVar(), to[i]);
     }
     
-    return sylvan_compose(mtbdd, map.mtbdd);
+    return mtbdd_compose(mtbdd, map.mtbdd);
 }
 
-Mtbdd
-Mtbdd::Support() const
-{
-    LACE_ME;
-    return mtbdd_support(mtbdd);
-}
-
-MTBDD
-Mtbdd::GetMTBDD() const
-{
-    return mtbdd;
-}
-
-Mtbdd
-Mtbdd::Compose(MtbddMap &m) const
+double
+Mtbdd::SatCount(size_t nvars) const
 {
     LACE_ME;
-    return mtbdd_compose(mtbdd, m.mtbdd);
+    return mtbdd_satcount(mtbdd, nvars);
 }
 
 double
-Mtbdd::SatCount(size_t variableCount) const
+Mtbdd::SatCount(const Mtbdd &variables) const
 {
-    LACE_ME;
-    return mtbdd_satcount(mtbdd, variableCount);
+    return SatCount(sylvan_set_count(variables.mtbdd));
 }
 
 size_t
@@ -1045,6 +947,7 @@ Mtbdd::NodeCount() const
     return mtbdd_nodecount(mtbdd);
 }
 
+
 /***
  * Implementation of class MtbddMap
  */
@@ -1132,3 +1035,5 @@ Sylvan::quitPackage()
 {
     sylvan_quit();
 }
+
+#include "sylvan_obj_storm.cpp"

src/storage/dd/Add.cpp

@@ -213,10 +213,10 @@ namespace storm {
         template<DdType LibraryType, typename ValueType>
         Add<LibraryType, ValueType> Add<LibraryType, ValueType>::multiplyMatrix(Add<LibraryType, ValueType> const& otherMatrix, std::set<storm::expressions::Variable> const& summationMetaVariables) const {
             // Create the CUDD summation variables.
-            std::vector<InternalAdd<LibraryType, ValueType>> summationDdVariables;
+            std::vector<InternalBdd<LibraryType>> summationDdVariables;
             for (auto const& metaVariable : summationMetaVariables) {
                 for (auto const& ddVariable : this->getDdManager()->getMetaVariable(metaVariable).getDdVariables()) {
-                    summationDdVariables.push_back(ddVariable.template toAdd<ValueType>());
+                    summationDdVariables.push_back(ddVariable);
                 }
             }
             

src/storage/dd/cudd/InternalCuddAdd.cpp

@@ -178,11 +178,11 @@ namespace storm {
         }
         
         template<typename ValueType>
-        InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::multiplyMatrix(InternalAdd<DdType::CUDD, ValueType> const& otherMatrix, std::vector<InternalAdd<DdType::CUDD, ValueType>> const& summationDdVariables) const {
+        InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::multiplyMatrix(InternalAdd<DdType::CUDD, ValueType> const& otherMatrix, std::vector<InternalBdd<DdType::CUDD>> const& summationDdVariables) const {
             // Create the CUDD summation variables.
             std::vector<cudd::ADD> summationAdds;
             for (auto const& ddVariable : summationDdVariables) {
-                summationAdds.push_back(ddVariable.getCuddAdd());
+                summationAdds.push_back(ddVariable.toAdd<ValueType>().getCuddAdd());
             }
             
             return InternalAdd<DdType::CUDD, ValueType>(ddManager, this->getCuddAdd().MatrixMultiply(otherMatrix.getCuddAdd(), summationAdds));

src/storage/dd/cudd/InternalCuddAdd.h

@@ -303,7 +303,7 @@ namespace storm {
              * @param summationDdVariables The DD variables (represented as ADDs) over which to sum.
              * @return An ADD representing the result of the matrix-matrix multiplication.
              */
-            InternalAdd<DdType::CUDD, ValueType> multiplyMatrix(InternalAdd<DdType::CUDD, ValueType> const& otherMatrix, std::vector<InternalAdd<DdType::CUDD, ValueType>> const& summationDdVariables) const;
+            InternalAdd<DdType::CUDD, ValueType> multiplyMatrix(InternalAdd<DdType::CUDD, ValueType> const& otherMatrix, std::vector<InternalBdd<DdType::CUDD>> const& summationDdVariables) const;
             
             /*!
              * Computes a BDD that represents the function in which all assignments with a function value strictly

src/storage/dd/cudd/InternalCuddBdd.cpp

@@ -111,6 +111,11 @@ namespace storm {
         }
         
         uint_fast64_t InternalBdd<DdType::CUDD>::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->getCuddBdd().CountMinterm(static_cast<int>(numberOfDdVariables)));
         }
         

src/storage/dd/sylvan/InternalSylvanAdd.cpp

@@ -164,22 +164,23 @@ namespace storm {
         
         template<typename ValueType>
         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;
+            std::vector<sylvan::Mtbdd> fromMtbdd;
+            std::vector<sylvan::Mtbdd> toMtbdd;
             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());
+                fromMtbdd.push_back(it1->getSylvanBdd());
+                toMtbdd.push_back(it2->getSylvanBdd());
             }
-            return InternalAdd<DdType::Sylvan, ValueType>(ddManager, this->sylvanMtbdd.Permute(fromBdd, toBdd));
+            return InternalAdd<DdType::Sylvan, ValueType>(ddManager, this->sylvanMtbdd.Permute(fromMtbdd, toMtbdd));
         }
         
         template<typename ValueType>
-        InternalAdd<DdType::Sylvan, ValueType> InternalAdd<DdType::Sylvan, ValueType>::multiplyMatrix(InternalAdd<DdType::Sylvan, ValueType> const& otherMatrix, std::vector<InternalAdd<DdType::Sylvan, ValueType>> const& summationDdVariables) const {
-            sylvan::Mtbdd summationVariables = sylvan::Mtbdd::mtbddOne();
+        InternalAdd<DdType::Sylvan, ValueType> InternalAdd<DdType::Sylvan, ValueType>::multiplyMatrix(InternalAdd<DdType::Sylvan, ValueType> const& otherMatrix, std::vector<InternalBdd<DdType::Sylvan>> const& summationDdVariables) const {
+            InternalBdd<DdType::Sylvan> summationVariables = ddManager->getBddOne();
             for (auto const& ddVariable : summationDdVariables) {
-                summationVariables *= ddVariable.sylvanMtbdd;
+                summationVariables &= ddVariable;
             }
-            return InternalAdd<DdType::Sylvan, ValueType>(ddManager, this->sylvanMtbdd.AndExists(otherMatrix.sylvanMtbdd, summationVariables));
+            
+            return InternalAdd<DdType::Sylvan, ValueType>(ddManager, this->sylvanMtbdd.AndExists(otherMatrix.sylvanMtbdd, summationVariables.getSylvanBdd()));
         }
         
         template<typename ValueType>
@@ -323,6 +324,11 @@ namespace storm {
             STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented.");
         }
         
+        template<typename ValueType>
+        sylvan::Mtbdd InternalAdd<DdType::Sylvan, ValueType>::getSylvanMtbdd() const {
+            return sylvanMtbdd;
+        }
+        
         template class InternalAdd<DdType::Sylvan, double>;
         template class InternalAdd<DdType::Sylvan, uint_fast64_t>;
     }

src/storage/dd/sylvan/InternalSylvanAdd.h

@@ -303,7 +303,7 @@ namespace storm {
              * @param summationDdVariables The DD variables (represented as ADDs) over which to sum.
              * @return An ADD representing the result of the matrix-matrix multiplication.
              */
-            InternalAdd<DdType::Sylvan, ValueType> multiplyMatrix(InternalAdd<DdType::Sylvan, ValueType> const& otherMatrix, std::vector<InternalAdd<DdType::Sylvan, ValueType>> const& summationDdVariables) const;
+            InternalAdd<DdType::Sylvan, ValueType> multiplyMatrix(InternalAdd<DdType::Sylvan, ValueType> const& otherMatrix, std::vector<InternalBdd<DdType::Sylvan>> const& summationDdVariables) const;
             
             /*!
              * Computes a BDD that represents the function in which all assignments with a function value strictly
@@ -546,6 +546,8 @@ namespace storm {
             Odd createOdd(std::vector<uint_fast64_t> const& ddVariableIndices) const;
             
         private:
+            sylvan::Mtbdd getSylvanMtbdd() const;
+            
             InternalDdManager<DdType::Sylvan> const* ddManager;
             
             sylvan::Mtbdd sylvanMtbdd;

test/functional/storage/CuddDdTest.cpp

@@ -198,7 +198,7 @@ TEST(CuddDd, AbstractionTest) {
     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(0ul, dd3Bdd.getNonZeroCount());
     EXPECT_EQ(1, dd3Bdd.template toAdd<double>().getMax());
 
     dd3 = dd1.equals(dd2).template toAdd<double>();

test/functional/storage/SylvanDdTest.cpp

@@ -72,13 +72,10 @@ TEST(SylvanDd, EncodingTest) {
     EXPECT_EQ(5ul, encoding.getNodeCount());
     EXPECT_EQ(1ul, encoding.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());
 }
@@ -191,97 +188,96 @@ TEST(SylvanDd, OperatorTest) {
     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(0ul, 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(0ul, 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, 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;
+    storm::dd::Bdd<storm::dd::DdType::Sylvan> bdd;
+    
+    dd1 = manager->template getIdentity<double>(x.first);
+    dd2 = manager->template getConstant<double>(5);
+    bdd = dd1.equals(dd2);
+    EXPECT_EQ(1ul, bdd.getNonZeroCount());
+    ASSERT_THROW(bdd = bdd.existsAbstract({x.second}), storm::exceptions::InvalidArgumentException);
+    ASSERT_NO_THROW(bdd = bdd.existsAbstract({x.first}));
+    EXPECT_EQ(0ul, bdd.getNonZeroCount());
+    EXPECT_EQ(1, bdd.template toAdd<double>().getMax());
+    
+    dd3 = dd1.equals(dd2).template toAdd<double>();
+    dd3 *= manager->template getConstant<double>(3);
+    EXPECT_EQ(1ul, dd3.getNonZeroCount());
+    ASSERT_THROW(bdd = dd3.toBdd().existsAbstract({x.second}), storm::exceptions::InvalidArgumentException);
+    ASSERT_NO_THROW(bdd = dd3.toBdd().existsAbstract({x.first}));
+    EXPECT_TRUE(bdd.isOne());
+    
+    dd3 = dd1.equals(dd2).template toAdd<double>();
+    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(0ul, dd3.getNonZeroCount());
+    EXPECT_EQ(3, dd3.getMax());
+    
+    dd3 = dd1.equals(dd2).template toAdd<double>();
+    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).template toAdd<double>();
+    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(0ul, 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;
+    
+    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)).template toAdd<double>();
+    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);