From f2a01afbdfdf153cc4b09696e10734c33459d97b Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Sat, 5 Dec 2015 20:32:05 +0100
Subject: [PATCH] ODD-based stuff working for Sylvan. Almost all tests passing
Former-commit-id: a6eef37d375e8e80f9a1d62d4f65951abe563b6e
---
.../3rdparty/sylvan/src/sylvan_mtbdd_storm.c | 17 ++++++
.../3rdparty/sylvan/src/sylvan_mtbdd_storm.h | 7 +++
.../sylvan/src/sylvan_obj_bdd_storm.hpp | 1 +
.../3rdparty/sylvan/src/sylvan_obj_storm.cpp | 6 +++
src/storage/dd/Add.cpp | 2 +-
src/storage/dd/cudd/InternalCuddAdd.cpp | 5 ++
src/storage/dd/cudd/InternalCuddAdd.h | 7 +++
src/storage/dd/sylvan/InternalSylvanAdd.cpp | 37 +++++++++----
src/storage/dd/sylvan/InternalSylvanAdd.h | 12 ++++-
src/storage/dd/sylvan/InternalSylvanBdd.cpp | 21 +++++---
src/storage/dd/sylvan/InternalSylvanBdd.h | 4 +-
test/functional/storage/SylvanDdTest.cpp | 54 +++++++++----------
12 files changed, 123 insertions(+), 50 deletions(-)
diff --git a/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.c b/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.c
index 92bd3cb07..12dbbcc46 100644
--- a/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.c
+++ b/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.c
@@ -471,6 +471,23 @@ TASK_IMPL_1(MTBDD, mtbdd_bool_to_double, MTBDD, dd)
return mtbdd_uapply(dd, TASK(mtbdd_op_bool_to_double), 0);
}
+TASK_IMPL_2(MTBDD, mtbdd_op_bool_to_uint64, MTBDD, a, size_t, v)
+{
+ /* We only expect "double" terminals, or false */
+ if (a == mtbdd_false) return mtbdd_uint64(0);
+ if (a == mtbdd_true) return mtbdd_uint64(1);
+
+ // Ugly hack to get rid of the error "unused variable v" (because there is no version of uapply without a parameter).
+ (void)v;
+
+ return mtbdd_invalid;
+}
+
+TASK_IMPL_1(MTBDD, mtbdd_bool_to_uint64, MTBDD, dd)
+{
+ return mtbdd_uapply(dd, TASK(mtbdd_op_bool_to_uint64), 0);
+}
+
/**
* Calculate the number of satisfying variable assignments according to <variables>.
*/
diff --git a/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.h b/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.h
index 4f5250b56..ef8b1c17c 100644
--- a/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.h
+++ b/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.h
@@ -94,6 +94,13 @@ 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)
+/**
+ * Monad that converts Boolean to a uint MTBDD, translate terminals true to 1 and to 0 otherwise;
+ */
+TASK_DECL_2(MTBDD, mtbdd_op_bool_to_uint64, MTBDD, size_t)
+TASK_DECL_1(MTBDD, mtbdd_bool_to_uint64, MTBDD)
+#define mtbdd_bool_to_uint64(dd) CALL(mtbdd_bool_to_uint64, dd)
+
/**
* Count the number of assignments (minterms) leading to a non-zero
*/
diff --git a/resources/3rdparty/sylvan/src/sylvan_obj_bdd_storm.hpp b/resources/3rdparty/sylvan/src/sylvan_obj_bdd_storm.hpp
index c5020144b..3c453ae9f 100644
--- a/resources/3rdparty/sylvan/src/sylvan_obj_bdd_storm.hpp
+++ b/resources/3rdparty/sylvan/src/sylvan_obj_bdd_storm.hpp
@@ -1 +1,2 @@
Mtbdd toDoubleMtbdd() const;
+ Mtbdd toUint64Mtbdd() const;
diff --git a/resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp b/resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp
index d2687ac8e..71ca7256e 100644
--- a/resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp
+++ b/resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp
@@ -4,6 +4,12 @@ Bdd::toDoubleMtbdd() const {
return mtbdd_bool_to_double(bdd);
}
+Mtbdd
+Bdd::toUint64Mtbdd() const {
+ LACE_ME;
+ return mtbdd_bool_to_uint64(bdd);
+}
+
Mtbdd
Mtbdd::Minus(const Mtbdd &other) const
{
diff --git a/src/storage/dd/Add.cpp b/src/storage/dd/Add.cpp
index 4afc3fbc4..64d02c99f 100644
--- a/src/storage/dd/Add.cpp
+++ b/src/storage/dd/Add.cpp
@@ -338,7 +338,7 @@ namespace storm {
Add<LibraryType, ValueType> value = *this * valueEncoding.template toAdd<ValueType>();
value = value.sumAbstract(this->getContainedMetaVariables());
- return value.getMax();
+ return value.internalAdd.getValue();
}
template<DdType LibraryType, typename ValueType>
diff --git a/src/storage/dd/cudd/InternalCuddAdd.cpp b/src/storage/dd/cudd/InternalCuddAdd.cpp
index 6ba175ae4..1cbff380d 100644
--- a/src/storage/dd/cudd/InternalCuddAdd.cpp
+++ b/src/storage/dd/cudd/InternalCuddAdd.cpp
@@ -260,6 +260,11 @@ namespace storm {
return static_cast<double>(Cudd_V(constantMaxAdd.getNode()));
}
+ template<typename ValueType>
+ ValueType InternalAdd<DdType::CUDD, ValueType>::getValue() const {
+ return static_cast<ValueType>(Cudd_V(this->getCuddAdd().getNode()));
+ }
+
template<typename ValueType>
bool InternalAdd<DdType::CUDD, ValueType>::isOne() const {
return this->getCuddAdd().IsOne();
diff --git a/src/storage/dd/cudd/InternalCuddAdd.h b/src/storage/dd/cudd/InternalCuddAdd.h
index 8543ffda5..b93a6205b 100644
--- a/src/storage/dd/cudd/InternalCuddAdd.h
+++ b/src/storage/dd/cudd/InternalCuddAdd.h
@@ -414,6 +414,13 @@ namespace storm {
*/
ValueType getMax() const;
+ /*!
+ * Retrieves the value of this ADD that is required to be a leaf.
+ *
+ * @return The value of the leaf.
+ */
+ ValueType getValue() const;
+
/*!
* Retrieves whether this ADD represents the constant one function.
*
diff --git a/src/storage/dd/sylvan/InternalSylvanAdd.cpp b/src/storage/dd/sylvan/InternalSylvanAdd.cpp
index 7afffec7d..2fa479044 100644
--- a/src/storage/dd/sylvan/InternalSylvanAdd.cpp
+++ b/src/storage/dd/sylvan/InternalSylvanAdd.cpp
@@ -254,6 +254,11 @@ namespace storm {
return static_cast<ValueType>(this->sylvanMtbdd.getDoubleMax());
}
+ template<typename ValueType>
+ ValueType InternalAdd<DdType::Sylvan, ValueType>::getValue() const {
+ return getValue(this->sylvanMtbdd.GetMTBDD());
+ }
+
template<typename ValueType>
bool InternalAdd<DdType::Sylvan, ValueType>::isOne() const {
return *this == ddManager->getAddOne<ValueType>();
@@ -348,16 +353,16 @@ namespace storm {
template<typename ValueType>
void InternalAdd<DdType::Sylvan, ValueType>::composeWithExplicitVector(storm::dd::Odd const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<ValueType>& targetVector, std::function<ValueType (ValueType const&, ValueType const&)> const& function) const {
- composeWithExplicitVectorRec(this->getSylvanMtbdd().GetMTBDD(), nullptr, 0, ddVariableIndices.size(), 0, odd, ddVariableIndices, targetVector, function);
+ composeWithExplicitVectorRec(mtbdd_regular(this->getSylvanMtbdd().GetMTBDD()), mtbdd_isnegated(this->getSylvanMtbdd().GetMTBDD()), nullptr, 0, ddVariableIndices.size(), 0, odd, ddVariableIndices, targetVector, function);
}
template<typename ValueType>
void InternalAdd<DdType::Sylvan, ValueType>::composeWithExplicitVector(storm::dd::Odd const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<uint_fast64_t> const& offsets, std::vector<ValueType>& targetVector, std::function<ValueType (ValueType const&, ValueType const&)> const& function) const {
- composeWithExplicitVectorRec(mtbdd_regular(this->getSylvanMtbdd().GetMTBDD()), &offsets, 0, ddVariableIndices.size(), 0, odd, ddVariableIndices, targetVector, function);
+ composeWithExplicitVectorRec(mtbdd_regular(this->getSylvanMtbdd().GetMTBDD()), mtbdd_isnegated(this->getSylvanMtbdd().GetMTBDD()), &offsets, 0, ddVariableIndices.size(), 0, odd, ddVariableIndices, targetVector, function);
}
template<typename ValueType>
- void InternalAdd<DdType::Sylvan, ValueType>::composeWithExplicitVectorRec(MTBDD dd, std::vector<uint_fast64_t> const* offsets, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<ValueType>& targetVector, std::function<ValueType (ValueType const&, ValueType const&)> const& function) const {
+ void InternalAdd<DdType::Sylvan, ValueType>::composeWithExplicitVectorRec(MTBDD dd, bool negated, std::vector<uint_fast64_t> const* offsets, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<ValueType>& targetVector, std::function<ValueType (ValueType const&, ValueType const&)> const& function) const {
// For the empty DD, we do not need to add any entries.
if (mtbdd_isleaf(dd) && mtbdd_iszero(dd)) {
return;
@@ -370,12 +375,19 @@ namespace storm {
} else if (mtbdd_isleaf(dd) || ddVariableIndices[currentLevel] < mtbdd_getvar(dd)) {
// If we skipped a level, we need to enumerate the explicit entries for the case in which the bit is set
// and for the one in which it is not set.
- composeWithExplicitVectorRec(dd, offsets, currentLevel + 1, maxLevel, currentOffset, odd.getElseSuccessor(), ddVariableIndices, targetVector, function);
- composeWithExplicitVectorRec(dd, offsets, currentLevel + 1, maxLevel, currentOffset + odd.getElseOffset(), odd.getThenSuccessor(), ddVariableIndices, targetVector, function);
+ composeWithExplicitVectorRec(dd, negated, offsets, currentLevel + 1, maxLevel, currentOffset, odd.getElseSuccessor(), ddVariableIndices, targetVector, function);
+ composeWithExplicitVectorRec(dd, negated, offsets, currentLevel + 1, maxLevel, currentOffset + odd.getElseOffset(), odd.getThenSuccessor(), ddVariableIndices, targetVector, function);
} else {
// Otherwise, we simply recursively call the function for both (different) cases.
- composeWithExplicitVectorRec(mtbdd_regular(mtbdd_getlow(dd)), offsets, currentLevel + 1, maxLevel, currentOffset, odd.getElseSuccessor(), ddVariableIndices, targetVector, function);
- composeWithExplicitVectorRec(mtbdd_regular(mtbdd_gethigh(dd)), offsets, currentLevel + 1, maxLevel, currentOffset + odd.getElseOffset(), odd.getThenSuccessor(), ddVariableIndices, targetVector, function);
+ MTBDD thenNode = mtbdd_gethigh(dd);
+ MTBDD elseNode = mtbdd_getlow(dd);
+
+ // Determine whether we have to evaluate the successors as if they were complemented.
+ bool elseComplemented = mtbdd_isnegated(elseNode) ^ negated;
+ bool thenComplemented = mtbdd_isnegated(thenNode) ^ negated;
+
+ composeWithExplicitVectorRec(mtbdd_regular(elseNode), elseComplemented, offsets, currentLevel + 1, maxLevel, currentOffset, odd.getElseSuccessor(), ddVariableIndices, targetVector, function);
+ composeWithExplicitVectorRec(mtbdd_regular(thenNode), thenComplemented, offsets, currentLevel + 1, maxLevel, currentOffset + odd.getElseOffset(), odd.getThenSuccessor(), ddVariableIndices, targetVector, function);
}
}
@@ -594,14 +606,17 @@ namespace storm {
template<typename ValueType>
ValueType InternalAdd<DdType::Sylvan, ValueType>::getValue(MTBDD const& node) {
- STORM_LOG_ASSERT(mtbdd_isleaf(node), "Expected leaf.");
+ STORM_LOG_ASSERT(mtbdd_isleaf(node), "Expected leaf, but got variable " << mtbdd_getvar(node) << ".");
+
+ bool negated = mtbdd_isnegated(node);
+ MTBDD n = mtbdd_regular(node);
if (std::is_same<ValueType, double>::value) {
- STORM_LOG_ASSERT(mtbdd_gettype(node) == 1, "Expected a double value.");
- return mtbdd_getuint64(node);
+ STORM_LOG_ASSERT(mtbdd_gettype(n) == 1, "Expected a double value.");
+ return negated ? -mtbdd_getdouble(n) : mtbdd_getdouble(n);
} else if (std::is_same<ValueType, uint_fast64_t>::value) {
STORM_LOG_ASSERT(mtbdd_gettype(node) == 0, "Expected an unsigned value.");
- return mtbdd_getdouble(node);
+ return negated ? -mtbdd_getuint64(node) : mtbdd_getuint64(node);
} else {
STORM_LOG_ASSERT(false, "Illegal or unknown type in MTBDD.");
}
diff --git a/src/storage/dd/sylvan/InternalSylvanAdd.h b/src/storage/dd/sylvan/InternalSylvanAdd.h
index ea67289fb..c93793560 100644
--- a/src/storage/dd/sylvan/InternalSylvanAdd.h
+++ b/src/storage/dd/sylvan/InternalSylvanAdd.h
@@ -411,7 +411,14 @@ namespace storm {
* @return The highest function value of any encoding.
*/
ValueType getMax() const;
-
+
+ /*!
+ * Retrieves the value of this ADD that is required to be a leaf.
+ *
+ * @return The value of the leaf.
+ */
+ ValueType getValue() const;
+
/*!
* Retrieves whether this ADD represents the constant one function.
*
@@ -564,6 +571,7 @@ namespace storm {
* explicit vector.
*
* @param dd The DD to add to the explicit vector.
+ * @param negated A flag indicating whether the DD node is to be interpreted as being negated.
* @param currentLevel The currently considered level in the DD.
* @param maxLevel The number of levels that need to be considered.
* @param currentOffset The current offset.
@@ -571,7 +579,7 @@ namespace storm {
* @param ddVariableIndices The (sorted) indices of all DD variables that need to be considered.
* @param targetVector The vector to which the translated DD-based vector is to be added.
*/
- void composeWithExplicitVectorRec(MTBDD dd, std::vector<uint_fast64_t> const* offsets, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<ValueType>& targetVector, std::function<ValueType (ValueType const&, ValueType const&)> const& function) const;
+ void composeWithExplicitVectorRec(MTBDD dd, bool negated, std::vector<uint_fast64_t> const* offsets, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<ValueType>& targetVector, std::function<ValueType (ValueType const&, ValueType const&)> const& function) const;
/*!
* Splits the given matrix DD into the groups using the given group variables.
diff --git a/src/storage/dd/sylvan/InternalSylvanBdd.cpp b/src/storage/dd/sylvan/InternalSylvanBdd.cpp
index 8e9fd8c53..cccb2af2d 100644
--- a/src/storage/dd/sylvan/InternalSylvanBdd.cpp
+++ b/src/storage/dd/sylvan/InternalSylvanBdd.cpp
@@ -8,7 +8,8 @@
#include "src/storage/BitVector.h"
-#include <iostream>
+#include "src/utility/macros.h"
+#include "src/exceptions/InvalidOperationException.h"
namespace storm {
namespace dd {
@@ -227,7 +228,13 @@ namespace storm {
template<typename ValueType>
InternalAdd<DdType::Sylvan, ValueType> InternalBdd<DdType::Sylvan>::toAdd() const {
- return InternalAdd<DdType::Sylvan, ValueType>(ddManager, this->sylvanBdd.toDoubleMtbdd());
+ if (std::is_same<ValueType, double>::value) {
+ return InternalAdd<DdType::Sylvan, ValueType>(ddManager, this->sylvanBdd.toDoubleMtbdd());
+ } else if (std::is_same<ValueType, uint_fast64_t>::value) {
+ return InternalAdd<DdType::Sylvan, ValueType>(ddManager, this->sylvanBdd.toUint64Mtbdd());
+ } else {
+ STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Illegal ADD type.");
+ }
}
storm::storage::BitVector InternalBdd<DdType::Sylvan>::toVector(storm::dd::Odd const& rowOdd, std::vector<uint_fast64_t> const& ddVariableIndices) const {
@@ -269,7 +276,7 @@ namespace storm {
std::vector<std::unordered_map<std::pair<BDD, bool>, std::shared_ptr<Odd>, HashFunctor>> uniqueTableForLevels(ddVariableIndices.size() + 1);
// Now construct the ODD structure from the BDD.
- std::shared_ptr<Odd> rootOdd = createOddRec(bdd_regular(this->getSylvanBdd().GetBDD()), 0, bdd_isnegated(this->getSylvanBdd().GetBDD()), ddVariableIndices.size(), ddVariableIndices, uniqueTableForLevels);
+ std::shared_ptr<Odd> rootOdd = createOddRec(bdd_regular(this->getSylvanBdd().GetBDD()), bdd_isnegated(this->getSylvanBdd().GetBDD()), 0, ddVariableIndices.size(), ddVariableIndices, uniqueTableForLevels);
// Return a copy of the root node to remove the shared_ptr encapsulation.
return Odd(*rootOdd);
@@ -282,7 +289,7 @@ namespace storm {
return result;
}
- std::shared_ptr<Odd> InternalBdd<DdType::Sylvan>::createOddRec(BDD dd, uint_fast64_t currentLevel, bool complement, uint_fast64_t maxLevel, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<std::unordered_map<std::pair<BDD, bool>, std::shared_ptr<Odd>, HashFunctor>>& uniqueTableForLevels) {
+ std::shared_ptr<Odd> InternalBdd<DdType::Sylvan>::createOddRec(BDD dd, bool complement, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<std::unordered_map<std::pair<BDD, bool>, std::shared_ptr<Odd>, HashFunctor>>& uniqueTableForLevels) {
// Check whether the ODD for this node has already been computed (for this level) and if so, return this instead.
auto const& iterator = uniqueTableForLevels[currentLevel].find(std::make_pair(dd, complement));
if (iterator != uniqueTableForLevels[currentLevel].end()) {
@@ -310,7 +317,7 @@ namespace storm {
} else if (bdd_isterminal(dd) || ddVariableIndices[currentLevel] < sylvan_var(dd)) {
// If we skipped the level in the DD, we compute the ODD just for the else-successor and use the same
// node for the then-successor as well.
- std::shared_ptr<Odd> elseNode = createOddRec(dd, currentLevel + 1, complement, maxLevel, ddVariableIndices, uniqueTableForLevels);
+ std::shared_ptr<Odd> elseNode = createOddRec(dd, complement, currentLevel + 1, maxLevel, ddVariableIndices, uniqueTableForLevels);
std::shared_ptr<Odd> thenNode = elseNode;
uint_fast64_t totalOffset = elseNode->getElseOffset() + elseNode->getThenOffset();
return std::make_shared<Odd>(elseNode, totalOffset, thenNode, totalOffset);
@@ -323,8 +330,8 @@ namespace storm {
bool elseComplemented = bdd_isnegated(elseDdNode) ^ complement;
bool thenComplemented = bdd_isnegated(thenDdNode) ^ complement;
- std::shared_ptr<Odd> elseNode = createOddRec(bdd_regular(elseDdNode), currentLevel + 1, elseComplemented, maxLevel, ddVariableIndices, uniqueTableForLevels);
- std::shared_ptr<Odd> thenNode = createOddRec(bdd_regular(thenDdNode), currentLevel + 1, thenComplemented, maxLevel, ddVariableIndices, uniqueTableForLevels);
+ std::shared_ptr<Odd> elseNode = createOddRec(bdd_regular(elseDdNode), elseComplemented, currentLevel + 1, maxLevel, ddVariableIndices, uniqueTableForLevels);
+ std::shared_ptr<Odd> thenNode = createOddRec(bdd_regular(thenDdNode), thenComplemented, currentLevel + 1, maxLevel, ddVariableIndices, uniqueTableForLevels);
return std::make_shared<Odd>(elseNode, elseNode->getElseOffset() + elseNode->getThenOffset(), thenNode, thenNode->getElseOffset() + thenNode->getThenOffset());
}
diff --git a/src/storage/dd/sylvan/InternalSylvanBdd.h b/src/storage/dd/sylvan/InternalSylvanBdd.h
index 5fef343ae..b1effdf47 100644
--- a/src/storage/dd/sylvan/InternalSylvanBdd.h
+++ b/src/storage/dd/sylvan/InternalSylvanBdd.h
@@ -352,15 +352,15 @@ namespace storm {
* Recursively builds the ODD from a BDD (that potentially has complement edges).
*
* @param dd The BDD for which to build the ODD.
- * @param currentLevel The currently considered level in the DD.
* @param complement A flag indicating whether or not the given node is to be considered as complemented.
+ * @param currentLevel The currently considered level in the DD.
* @param maxLevel The number of levels that need to be considered.
* @param ddVariableIndices The (sorted) indices of all DD variables that need to be considered.
* @param uniqueTableForLevels A vector of unique tables, one for each level to be considered, that keeps
* ODD nodes for the same DD and level unique.
* @return A pointer to the constructed ODD for the given arguments.
*/
- static std::shared_ptr<Odd> createOddRec(BDD dd, uint_fast64_t currentLevel, bool complement, uint_fast64_t maxLevel, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<std::unordered_map<std::pair<BDD, bool>, std::shared_ptr<Odd>, HashFunctor>>& uniqueTableForLevels);
+ static std::shared_ptr<Odd> createOddRec(BDD dd, bool complement, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<std::unordered_map<std::pair<BDD, bool>, std::shared_ptr<Odd>, HashFunctor>>& uniqueTableForLevels);
/*!
* Helper function to convert the DD into a bit vector.
diff --git a/test/functional/storage/SylvanDdTest.cpp b/test/functional/storage/SylvanDdTest.cpp
index 3b7e8e06d..9cf188c24 100644
--- a/test/functional/storage/SylvanDdTest.cpp
+++ b/test/functional/storage/SylvanDdTest.cpp
@@ -339,30 +339,30 @@ TEST(SylvanDd, AddOddTest) {
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());
+ // Create a non-trivial matrix.
+ dd = manager->template getIdentity<double>(x.first).equals(manager->template getIdentity<double>(x.second)).template toAdd<double>() * 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) {
@@ -381,13 +381,13 @@ TEST(SylvanDd, BddOddTest) {
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]);
+ EXPECT_EQ(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});
+ 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->template getIdentity<double>(x.first).equals(manager->template getIdentity<double>(x.second)).template toAdd<double>() * 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.