From 99f096635f29bc5d174db6046a904e163b138567 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 23 Nov 2015 15:56:09 +0100 Subject: [PATCH] started integrating sylvan Former-commit-id: 2aec04304777718ae541cc5e9c7199be09a34a6c --- src/storage/dd/Bdd.cpp | 13 +- src/storage/dd/cudd/InternalCuddBdd.cpp | 4 +- src/storage/dd/cudd/InternalCuddBdd.h | 5 +- src/storage/dd/sylvan/InternalSylvanBdd.cpp | 80 ++-- src/storage/dd/sylvan/InternalSylvanBdd.h | 12 +- .../dd/sylvan/InternalSylvanDdManager.cpp | 36 +- .../dd/sylvan/InternalSylvanDdManager.h | 16 +- test/functional/storage/CuddDdTest.cpp | 10 +- test/functional/storage/SylvanDdTest.cpp | 409 ++++++++++++++++++ 9 files changed, 535 insertions(+), 50 deletions(-) create mode 100644 test/functional/storage/SylvanDdTest.cpp diff --git a/src/storage/dd/Bdd.cpp b/src/storage/dd/Bdd.cpp index 882471d8c..3a18d9b2f 100644 --- a/src/storage/dd/Bdd.cpp +++ b/src/storage/dd/Bdd.cpp @@ -188,10 +188,17 @@ namespace storm { template uint_fast64_t Bdd::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 cube; + if (LibraryType == DdType::Sylvan) { + cube = Bdd::getCube(*this->getDdManager(), this->getContainedMetaVariables()); } - return internalBdd.getNonZeroCount(numberOfDdVariables); + return internalBdd.getNonZeroCount(cube, numberOfDdVariables); } template diff --git a/src/storage/dd/cudd/InternalCuddBdd.cpp b/src/storage/dd/cudd/InternalCuddBdd.cpp index b4c12e82d..cad95faa5 100644 --- a/src/storage/dd/cudd/InternalCuddBdd.cpp +++ b/src/storage/dd/cudd/InternalCuddBdd.cpp @@ -110,7 +110,7 @@ namespace storm { return InternalBdd(ddManager, this->getCuddBdd().Support()); } - uint_fast64_t InternalBdd::getNonZeroCount(uint_fast64_t numberOfDdVariables) const { + uint_fast64_t InternalBdd::getNonZeroCount(InternalBdd const& cube, uint_fast64_t numberOfDdVariables) const { return static_cast(this->getCuddBdd().CountMinterm(static_cast(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 cuddBddVector = { this->getCuddBdd() }; + FILE* filePointer = fopen(filename.c_str() , "w"); ddManager->getCuddManager().DumpDot(cuddBddVector, &ddVariableNames[0], &ddNames[0], filePointer); fclose(filePointer); diff --git a/src/storage/dd/cudd/InternalCuddBdd.h b/src/storage/dd/cudd/InternalCuddBdd.h index a20a7413e..1bec0aa09 100644 --- a/src/storage/dd/cudd/InternalCuddBdd.h +++ b/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 const& cube, uint_fast64_t numberOfDdVariables) const; /*! * Retrieves the number of leaves of the DD. diff --git a/src/storage/dd/sylvan/InternalSylvanBdd.cpp b/src/storage/dd/sylvan/InternalSylvanBdd.cpp index 02428ec89..6fc9cbe90 100644 --- a/src/storage/dd/sylvan/InternalSylvanBdd.cpp +++ b/src/storage/dd/sylvan/InternalSylvanBdd.cpp @@ -10,113 +10,139 @@ namespace storm { namespace dd { + InternalBdd::InternalBdd(InternalDdManager const* ddManager, sylvan::Bdd const& sylvanBdd) : ddManager(ddManager), sylvanBdd(sylvanBdd) { + // Intentionally left empty. + } + template InternalBdd InternalBdd::fromVector(InternalDdManager const* ddManager, std::vector const& values, Odd const& odd, std::vector const& sortedDdVariableIndices, std::function const& filter) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); } bool InternalBdd::operator==(InternalBdd const& other) const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + return sylvanBdd == other.sylvanBdd; } bool InternalBdd::operator!=(InternalBdd const& other) const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + return sylvanBdd != other.sylvanBdd; } InternalBdd InternalBdd::ite(InternalBdd const& thenDd, InternalBdd const& elseDd) const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + return InternalBdd(ddManager, this->sylvanBdd.Ite(thenDd.sylvanBdd, elseDd.sylvanBdd)); } InternalBdd InternalBdd::operator||(InternalBdd const& other) const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + return InternalBdd(ddManager, this->sylvanBdd | other.sylvanBdd); } InternalBdd& InternalBdd::operator|=(InternalBdd const& other) { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + this->sylvanBdd |= other.sylvanBdd; + return *this; } InternalBdd InternalBdd::operator&&(InternalBdd const& other) const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + return InternalBdd(ddManager, this->sylvanBdd & other.sylvanBdd); } InternalBdd& InternalBdd::operator&=(InternalBdd const& other) { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + this->sylvanBdd &= other.sylvanBdd; + return *this; } InternalBdd InternalBdd::iff(InternalBdd const& other) const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + return InternalBdd(ddManager, !(this->sylvanBdd ^ other.sylvanBdd)); } InternalBdd InternalBdd::exclusiveOr(InternalBdd const& other) const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + return InternalBdd(ddManager, this->sylvanBdd ^ other.sylvanBdd); } InternalBdd InternalBdd::implies(InternalBdd const& other) const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + return InternalBdd(ddManager, !this->sylvanBdd | other.sylvanBdd); } InternalBdd InternalBdd::operator!() const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + return InternalBdd(ddManager, !this->sylvanBdd); } InternalBdd& InternalBdd::complement() { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + this->sylvanBdd = !this->sylvanBdd; + return *this; } InternalBdd InternalBdd::existsAbstract(InternalBdd const& cube) const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + return InternalBdd(ddManager, this->sylvanBdd.ExistAbstract(cube.sylvanBdd)); } InternalBdd InternalBdd::universalAbstract(InternalBdd const& cube) const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + return InternalBdd(ddManager, this->sylvanBdd.UnivAbstract(cube.sylvanBdd)); } InternalBdd InternalBdd::andExists(InternalBdd const& other, InternalBdd const& cube) const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + return InternalBdd(ddManager, this->sylvanBdd.AndAbstract(other.sylvanBdd, cube.sylvanBdd)); } InternalBdd InternalBdd::constrain(InternalBdd const& constraint) const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + return InternalBdd(ddManager, this->sylvanBdd.Constrain(constraint.sylvanBdd)); } InternalBdd InternalBdd::restrict(InternalBdd const& constraint) const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + return InternalBdd(ddManager, this->sylvanBdd.Restrict(constraint.sylvanBdd)); } InternalBdd InternalBdd::swapVariables(std::vector> const& from, std::vector> const& to) const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + std::vector fromBdd; + std::vector 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(ddManager, this->sylvanBdd.Permute(fromBdd, toBdd)); } InternalBdd InternalBdd::getSupport() const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + return InternalBdd(ddManager, this->sylvanBdd.Support()); } - uint_fast64_t InternalBdd::getNonZeroCount(uint_fast64_t numberOfDdVariables) const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + uint_fast64_t InternalBdd::getNonZeroCount(InternalBdd const& cube, uint_fast64_t numberOfDdVariables) const { + return static_cast(this->sylvanBdd.SatCount(cube.sylvanBdd)); } uint_fast64_t InternalBdd::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::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(this->sylvanBdd.NodeCount()) + 1; } bool InternalBdd::isOne() const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + return this->sylvanBdd.isOne(); } bool InternalBdd::isZero() const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + return this->sylvanBdd.isZero(); } uint_fast64_t InternalBdd::getIndex() const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + return static_cast(this->sylvanBdd.GetBDD()); } void InternalBdd::exportToDot(std::string const& filename, std::vector 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::getSylvanBdd() { + return sylvanBdd; + } + + sylvan::Bdd const& InternalBdd::getSylvanBdd() const { + return sylvanBdd; } template diff --git a/src/storage/dd/sylvan/InternalSylvanBdd.h b/src/storage/dd/sylvan/InternalSylvanBdd.h index ff73837e0..4fd653253 100644 --- a/src/storage/dd/sylvan/InternalSylvanBdd.h +++ b/src/storage/dd/sylvan/InternalSylvanBdd.h @@ -26,6 +26,8 @@ namespace storm { public: friend class InternalAdd; + InternalBdd(InternalDdManager const* ddManager, sylvan::Bdd const& sylvanBdd); + // Instantiate all copy/move constructors/assignments with the default implementation. InternalBdd() = default; InternalBdd(InternalBdd 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 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 const& ddVariableIndices, std::vector const& sourceValues, std::vector& targetValues) const; private: + sylvan::Bdd& getSylvanBdd(); + sylvan::Bdd const& getSylvanBdd() const; + InternalDdManager const* ddManager; + + sylvan::Bdd sylvanBdd; }; } } diff --git a/src/storage/dd/sylvan/InternalSylvanDdManager.cpp b/src/storage/dd/sylvan/InternalSylvanDdManager.cpp index 322c6c540..b4da41d8f 100644 --- a/src/storage/dd/sylvan/InternalSylvanDdManager.cpp +++ b/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::numberOfInstances = 0; + uint_fast64_t InternalDdManager::nextFreeVariableIndex = 0; InternalDdManager::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::~InternalDdManager() { + --numberOfInstances; + if (numberOfInstances == 0) { + sylvan::Sylvan::quitPackage(); + } } InternalBdd InternalDdManager::getBddOne() const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + return InternalBdd(this, sylvan::Bdd::bddOne()); } template @@ -20,7 +39,7 @@ namespace storm { } InternalBdd InternalDdManager::getBddZero() const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + return InternalBdd(this, sylvan::Bdd::bddZero()); } template @@ -34,19 +53,22 @@ namespace storm { } std::pair, InternalBdd> InternalDdManager::createNewDdVariablePair() { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + InternalBdd first = InternalBdd(this, sylvan::Bdd::bddVar(nextFreeVariableIndex)); + InternalBdd second = InternalBdd(this, sylvan::Bdd::bddVar(nextFreeVariableIndex + 1)); + nextFreeVariableIndex += 2; + return std::make_pair(first, second); } void InternalDdManager::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::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::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 InternalDdManager::getAddOne() const; diff --git a/src/storage/dd/sylvan/InternalSylvanDdManager.h b/src/storage/dd/sylvan/InternalSylvanDdManager.h index 3dc203b2e..1c2941bf2 100644 --- a/src/storage/dd/sylvan/InternalSylvanDdManager.h +++ b/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; }; } } diff --git a/test/functional/storage/CuddDdTest.cpp b/test/functional/storage/CuddDdTest.cpp index 03ef4f304..42326b0d0 100644 --- a/test/functional/storage/CuddDdTest.cpp +++ b/test/functional/storage/CuddDdTest.cpp @@ -9,7 +9,7 @@ #include "src/storage/SparseMatrix.h" -TEST(CuddDdManager, Constants) { +TEST(CuddDd, Constants) { std::shared_ptr> manager(new storm::dd::DdManager()); storm::dd::Add zero; ASSERT_NO_THROW(zero = manager->template getAddZero()); @@ -39,7 +39,7 @@ TEST(CuddDdManager, Constants) { EXPECT_EQ(2, two.getMax()); } -TEST(CuddDdManager, AddGetMetaVariableTest) { +TEST(CuddDd, AddGetMetaVariableTest) { std::shared_ptr> manager(new storm::dd::DdManager()); 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> manager(new storm::dd::DdManager()); std::pair x = manager->addMetaVariable("x", 1, 9); @@ -76,7 +76,7 @@ TEST(CuddDdManager, EncodingTest) { EXPECT_EQ(2ul, encoding.template toAdd().getLeafCount()); } -TEST(CuddDdManager, RangeTest) { +TEST(CuddDd, RangeTest) { std::shared_ptr> manager(new storm::dd::DdManager()); std::pair 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> manager(new storm::dd::DdManager()); std::pair x = manager->addMetaVariable("x", 1, 9); diff --git a/test/functional/storage/SylvanDdTest.cpp b/test/functional/storage/SylvanDdTest.cpp new file mode 100644 index 000000000..dc595dbac --- /dev/null +++ b/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> manager(new storm::dd::DdManager()); +// storm::dd::Add zero; +// ASSERT_NO_THROW(zero = manager->template getAddZero()); +// +// 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 one; +// ASSERT_NO_THROW(one = manager->template getAddOne()); +// +// 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 two; +// ASSERT_NO_THROW(two = manager->template getConstant(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> manager(new storm::dd::DdManager()); + 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 metaVariableSet = {"x", "x'", "y", "y'"}; + EXPECT_EQ(metaVariableSet, manager->getAllMetaVariableNames()); +} + +TEST(SylvanDd, EncodingTest) { + std::shared_ptr> manager(new storm::dd::DdManager()); + std::pair x = manager->addMetaVariable("x", 1, 9); + + storm::dd::Bdd 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().getNodeCount()); +// EXPECT_EQ(2ul, encoding.template toAdd().getLeafCount()); +} +// +TEST(SylvanDd, RangeTest) { + std::shared_ptr> manager(new storm::dd::DdManager()); + std::pair x; + ASSERT_NO_THROW(x = manager->addMetaVariable("x", 1, 9)); + + storm::dd::Bdd 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> manager(new storm::dd::DdManager()); +// std::pair x = manager->addMetaVariable("x", 1, 9); +// +// storm::dd::Add identity; +// ASSERT_NO_THROW(identity = manager->getIdentity(x.first)); +// +// EXPECT_EQ(9ul, identity.getNonZeroCount()); +// EXPECT_EQ(10ul, identity.getLeafCount()); +// EXPECT_EQ(21ul, identity.getNodeCount()); +//} +// +//TEST(SylvanDd, OperatorTest) { +// std::shared_ptr> manager(new storm::dd::DdManager()); +// std::pair x = manager->addMetaVariable("x", 1, 9); +// EXPECT_TRUE(manager->template getAddZero() == manager->template getAddZero()); +// EXPECT_FALSE(manager->template getAddZero() == manager->template getAddOne()); +// +// EXPECT_FALSE(manager->template getAddZero() != manager->template getAddZero()); +// EXPECT_TRUE(manager->template getAddZero() != manager->template getAddOne()); +// +// storm::dd::Add dd1 = manager->template getAddOne(); +// storm::dd::Add dd2 = manager->template getAddOne(); +// storm::dd::Add dd3 = dd1 + dd2; +// EXPECT_TRUE(dd3 == manager->template getConstant(2)); +// +// dd3 += manager->template getAddZero(); +// EXPECT_TRUE(dd3 == manager->template getConstant(2)); +// +// dd3 = dd1 * manager->template getConstant(3); +// EXPECT_TRUE(dd3 == manager->template getConstant(3)); +// +// dd3 *= manager->template getConstant(2); +// EXPECT_TRUE(dd3 == manager->template getConstant(6)); +// +// dd3 = dd1 - dd2; +// EXPECT_TRUE(dd3.isZero()); +// +// dd3 -= manager->template getConstant(-2); +// EXPECT_TRUE(dd3 == manager->template getConstant(2)); +// +// dd3 /= manager->template getConstant(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(x.first); +// dd2 = manager->template getConstant(5); +// +// dd3 = dd1.equals(dd2); +// EXPECT_EQ(1ul, dd3.getNonZeroCount()); +// +// storm::dd::Add 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()).ite(dd2, dd1); +// dd4 = dd3.less(dd2); +// EXPECT_EQ(10ul, dd4.getNonZeroCount()); +// +// dd4 = dd3.minimum(dd1); +// dd4 *= manager->getEncoding(x.first, 2).template toAdd(); +// dd4 = dd4.sumAbstract({x.first}); +// EXPECT_EQ(2, dd4.getValue()); +// +// dd4 = dd3.maximum(dd1); +// dd4 *= manager->getEncoding(x.first, 2).template toAdd(); +// dd4 = dd4.sumAbstract({x.first}); +// EXPECT_EQ(5, dd4.getValue()); +// +// dd1 = manager->template getConstant(0.01); +// dd2 = manager->template getConstant(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> manager(new storm::dd::DdManager()); +// std::pair x = manager->addMetaVariable("x", 1, 9); +// storm::dd::Add dd1; +// storm::dd::Add dd2; +// storm::dd::Add dd3; +// +// dd1 = manager->template getIdentity(x.first); +// dd2 = manager->template getConstant(5); +// dd3 = dd1.equals(dd2); +// storm::dd::Bdd 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().getMax()); +// +// dd3 = dd1.equals(dd2); +// dd3 *= manager->template getConstant(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(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(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(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> manager(new storm::dd::DdManager()); +// +// std::pair x = manager->addMetaVariable("x", 1, 9); +// std::pair z = manager->addMetaVariable("z", 2, 8); +// storm::dd::Add dd1; +// storm::dd::Add dd2; +// +// dd1 = manager->template getIdentity(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(x.second)); +//} +// +//TEST(SylvanDd, MultiplyMatrixTest) { +// std::shared_ptr> manager(new storm::dd::DdManager()); +// std::pair x = manager->addMetaVariable("x", 1, 9); +// +// storm::dd::Add dd1 = manager->template getIdentity(x.first).equals(manager->template getIdentity(x.second)); +// storm::dd::Add dd2 = manager->getRange(x.second).template toAdd(); +// storm::dd::Add dd3; +// dd1 *= manager->template getConstant(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(2)); +//} +// +//TEST(SylvanDd, GetSetValueTest) { +// std::shared_ptr> manager(new storm::dd::DdManager()); +// std::pair x = manager->addMetaVariable("x", 1, 9); +// +// storm::dd::Add dd1 = manager->template getAddOne(); +// ASSERT_NO_THROW(dd1.setValue(x.first, 4, 2)); +// EXPECT_EQ(2ul, dd1.getLeafCount()); +// +// std::map 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> manager(new storm::dd::DdManager()); +// std::pair x = manager->addMetaVariable("x", 1, 9); +// std::pair y = manager->addMetaVariable("y", 0, 3); +// +// storm::dd::Add dd; +// ASSERT_NO_THROW(dd = manager->getRange(x.first).template toAdd()); +// +// storm::dd::AddIterator it, ite; +// ASSERT_NO_THROW(it = dd.begin()); +// ASSERT_NO_THROW(ite = dd.end()); +// std::pair 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(); +// dd = dd.ite(manager->template getAddOne(), manager->template getAddOne()); +// 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> manager(new storm::dd::DdManager()); +// std::pair a = manager->addMetaVariable("a"); +// std::pair x = manager->addMetaVariable("x", 1, 9); +// +// storm::dd::Add dd = manager->template getIdentity(x.first); +// storm::dd::Odd odd; +// ASSERT_NO_THROW(odd = dd.createOdd()); +// EXPECT_EQ(9ul, odd.getTotalOffset()); +// EXPECT_EQ(12ul, odd.getNodeCount()); +// +// std::vector 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(x.first).equals(manager->template getIdentity(x.second)) * manager->getRange(x.first).template toAdd(); +// dd += manager->getEncoding(x.first, 1).template toAdd() * manager->getRange(x.second).template toAdd() + manager->getEncoding(x.second, 1).template toAdd() * manager->getRange(x.first).template toAdd(); +// +// // Create the ODDs. +// storm::dd::Odd rowOdd; +// ASSERT_NO_THROW(rowOdd = manager->getRange(x.first).template toAdd().createOdd()); +// storm::dd::Odd columnOdd; +// ASSERT_NO_THROW(columnOdd = manager->getRange(x.second).template toAdd().createOdd()); +// +// // Try to translate the matrix. +// storm::storage::SparseMatrix 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() * manager->getRange(x.second).template toAdd() * manager->getEncoding(a.first, 0).template toAdd().ite(dd, dd + manager->template getConstant(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> manager(new storm::dd::DdManager()); +// std::pair a = manager->addMetaVariable("a"); +// std::pair x = manager->addMetaVariable("x", 1, 9); +// +// storm::dd::Add dd = manager->template getIdentity(x.first); +// storm::dd::Odd odd; +// ASSERT_NO_THROW(odd = dd.createOdd()); +// EXPECT_EQ(9ul, odd.getTotalOffset()); +// EXPECT_EQ(12ul, odd.getNodeCount()); +// +// std::vector 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 vectorAdd = storm::dd::Add::fromVector(manager, ddAsVector, odd, {x.first}); +// +// // Create a non-trivial matrix. +// dd = manager->template getIdentity(x.first).equals(manager->template getIdentity(x.second)) * manager->getRange(x.first).template toAdd(); +// dd += manager->getEncoding(x.first, 1).template toAdd() * manager->getRange(x.second).template toAdd() + manager->getEncoding(x.second, 1).template toAdd() * manager->getRange(x.first).template toAdd(); +// +// // 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 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() * manager->getRange(x.second).template toAdd() * manager->getEncoding(a.first, 0).template toAdd().ite(dd, dd + manager->template getConstant(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()); +//} \ No newline at end of file