From cb35b3315daad61e20ddff3f7aa89104e210787c Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 24 Mar 2014 22:32:51 +0100 Subject: [PATCH] Added matrix-matrix multiplication to DD interface. (This includes matrix-vector multiplication as a special case). Former-commit-id: d5d8fef7386f39402514540143f19b73a147ae68 --- src/storage/dd/CuddDd.cpp | 54 ++++++++++++++++++++++++-------- src/storage/dd/CuddDd.h | 31 ++++++++++++------ src/storage/dd/CuddDdManager.cpp | 4 +-- src/storage/dd/CuddDdManager.h | 3 +- 4 files changed, 65 insertions(+), 27 deletions(-) diff --git a/src/storage/dd/CuddDd.cpp b/src/storage/dd/CuddDd.cpp index 6276a422b..be51d5a98 100644 --- a/src/storage/dd/CuddDd.cpp +++ b/src/storage/dd/CuddDd.cpp @@ -5,7 +5,7 @@ namespace storm { namespace dd { - Dd::Dd(std::shared_ptr> ddManager, ADD cuddAdd, std::unordered_set const& containedMetaVariableNames) noexcept : ddManager(ddManager), cuddAdd(cuddAdd), containedMetaVariableNames(containedMetaVariableNames) { + Dd::Dd(std::shared_ptr> ddManager, ADD cuddAdd, std::set const& containedMetaVariableNames) noexcept : ddManager(ddManager), cuddAdd(cuddAdd), containedMetaVariableNames(containedMetaVariableNames) { // Intentionally left empty. } @@ -23,7 +23,7 @@ namespace storm { this->getCuddAdd() += other.getCuddAdd(); // Join the variable sets of the two participating DDs. - std::copy(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end(), std::inserter(this->containedMetaVariableNames, this->containedMetaVariableNames.end())); + this->getContainedMetaVariableNames().insert(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end()); return *this; } @@ -38,7 +38,7 @@ namespace storm { this->getCuddAdd() *= other.getCuddAdd(); // Join the variable sets of the two participating DDs. - std::copy(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end(), std::inserter(this->containedMetaVariableNames, this->containedMetaVariableNames.end())); + this->getContainedMetaVariableNames().insert(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end()); return *this; } @@ -53,7 +53,7 @@ namespace storm { this->getCuddAdd() -= other.getCuddAdd(); // Join the variable sets of the two participating DDs. - std::copy(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end(), std::inserter(this->containedMetaVariableNames, this->containedMetaVariableNames.end())); + this->getContainedMetaVariableNames().insert(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end()); return *this; } @@ -68,7 +68,7 @@ namespace storm { this->getCuddAdd().Divide(other.getCuddAdd()); // Join the variable sets of the two participating DDs. - std::copy(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end(), std::inserter(this->containedMetaVariableNames, this->containedMetaVariableNames.end())); + this->getContainedMetaVariableNames().insert(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end()); return *this; } @@ -120,7 +120,7 @@ namespace storm { return result; } - void Dd::existsAbstract(std::unordered_set const& metaVariableNames) { + void Dd::existsAbstract(std::set const& metaVariableNames) { Dd cubeDd(this->getDdManager()->getOne()); for (auto const& metaVariableName : metaVariableNames) { @@ -137,7 +137,7 @@ namespace storm { this->getCuddAdd().OrAbstract(cubeDd.getCuddAdd()); } - void Dd::sumAbstract(std::unordered_set const& metaVariableNames) { + void Dd::sumAbstract(std::set const& metaVariableNames) { Dd cubeDd(this->getDdManager()->getOne()); for (auto const& metaVariableName : metaVariableNames) { @@ -154,7 +154,7 @@ namespace storm { this->getCuddAdd().ExistAbstract(cubeDd.getCuddAdd()); } - void Dd::minAbstract(std::unordered_set const& metaVariableNames) { + void Dd::minAbstract(std::set const& metaVariableNames) { Dd cubeDd(this->getDdManager()->getOne()); for (auto const& metaVariableName : metaVariableNames) { @@ -171,7 +171,7 @@ namespace storm { this->getCuddAdd().Minimum(cubeDd.getCuddAdd()); } - void Dd::maxAbstract(std::unordered_set const& metaVariableNames) { + void Dd::maxAbstract(std::set const& metaVariableNames) { Dd cubeDd(this->getDdManager()->getOne()); for (auto const& metaVariableName : metaVariableNames) { @@ -210,11 +210,39 @@ namespace storm { this->removeContainedMetaVariable(metaVariablePair.second); this->addContainedMetaVariable(metaVariablePair.first); } + + // Add the variables to swap to the corresponding vectors. + for (auto const& ddVariable : variable1.getDdVariables()) { + from.push_back(ddVariable.getCuddAdd()); + } + for (auto const& ddVariable : variable2.getDdVariables()) { + to.push_back(ddVariable.getCuddAdd()); + } } - // FIXME: complete this and add matrix-matrix multiplication. + // Finally, call CUDD to swap the variables. + this->getCuddAdd().SwapVariables(from, to); } + Dd Dd::multiplyMatrix(Dd const& otherMatrix, std::set const& summationMetaVariableNames) { + std::vector summationDdVariables; + + // Create the CUDD summation variables. + for (auto const& metaVariableName : summationMetaVariableNames) { + for (auto const& ddVariable : this->getDdManager()->getMetaVariable(metaVariableName).getDdVariables()) { + summationDdVariables.push_back(ddVariable.getCuddAdd()); + } + } + + std::set unionOfMetaVariableNames; + std::set_union(this->getContainedMetaVariableNames().begin(), this->getContainedMetaVariableNames().end(), otherMatrix.getContainedMetaVariableNames().begin(), otherMatrix.getContainedMetaVariableNames().end(), std::inserter(unionOfMetaVariableNames, unionOfMetaVariableNames.begin())); + std::set containedMetaVariableNames; + std::set_difference(unionOfMetaVariableNames.begin(), unionOfMetaVariableNames.end(), summationMetaVariableNames.begin(), summationMetaVariableNames.end(), std::inserter(containedMetaVariableNames, containedMetaVariableNames.begin())); + + return Dd(this->getDdManager(), this->getCuddAdd().MatrixMultiply(otherMatrix.getCuddAdd(), summationDdVariables), containedMetaVariableNames); + } + + uint_fast64_t Dd::getNonZeroCount() const { std::size_t numberOfDdVariables = 0; for (auto const& metaVariableName : this->containedMetaVariableNames) { @@ -276,7 +304,7 @@ namespace storm { return metaVariable != containedMetaVariableNames.end(); } - bool Dd::containsMetaVariables(std::unordered_set metaVariableNames) const { + bool Dd::containsMetaVariables(std::set metaVariableNames) const { for (auto const& metaVariableName : metaVariableNames) { auto const& metaVariable = containedMetaVariableNames.find(metaVariableName); @@ -287,11 +315,11 @@ namespace storm { return true; } - std::unordered_set const& Dd::getContainedMetaVariableNames() const { + std::set const& Dd::getContainedMetaVariableNames() const { return this->containedMetaVariableNames; } - std::unordered_set& Dd::getContainedMetaVariableNames() { + std::set& Dd::getContainedMetaVariableNames() { return this->containedMetaVariableNames; } diff --git a/src/storage/dd/CuddDd.h b/src/storage/dd/CuddDd.h index a07db98d6..0aa71889e 100644 --- a/src/storage/dd/CuddDd.h +++ b/src/storage/dd/CuddDd.h @@ -1,8 +1,8 @@ #ifndef STORM_STORAGE_DD_CUDDDD_H_ #define STORM_STORAGE_DD_CUDDDD_H_ -#include #include +#include #include #include "src/storage/dd/Dd.h" @@ -179,28 +179,28 @@ namespace storm { * * @param metaVariableNames The names of all meta variables from which to abstract. */ - void existsAbstract(std::unordered_set const& metaVariableNames); + void existsAbstract(std::set const& metaVariableNames); /*! * Sum-abstracts from the given meta variables. * * @param metaVariableNames The names of all meta variables from which to abstract. */ - void sumAbstract(std::unordered_set const& metaVariableNames); + void sumAbstract(std::set const& metaVariableNames); /*! * Min-abstracts from the given meta variables. * * @param metaVariableNames The names of all meta variables from which to abstract. */ - void minAbstract(std::unordered_set const& metaVariableNames); + void minAbstract(std::set const& metaVariableNames); /*! * Max-abstracts from the given meta variables. * * @param metaVariableNames The names of all meta variables from which to abstract. */ - void maxAbstract(std::unordered_set const& metaVariableNames); + void maxAbstract(std::set const& metaVariableNames); /*! * Swaps the given pairs of meta variables in the DD. The pairs of meta variables must be guaranteed to have @@ -210,6 +210,17 @@ namespace storm { */ void swapVariables(std::vector> const& metaVariablePairs); + /*! + * Multiplies the current DD (representing a matrix) with the given matrix by summing over the given meta + * variables. + * + * @param otherMatrix The matrix with which to multiply. + * @param summationMetaVariableNames The names of the meta variables over which to sum during the matrix- + * matrix multiplication. + * @return A DD representing the result of the matrix-matrix multiplication. + */ + Dd multiplyMatrix(Dd const& otherMatrix, std::set const& summationMetaVariableNames); + /*! * Retrieves the number of encodings that are mapped to a non-zero value. * @@ -310,21 +321,21 @@ namespace storm { * @param metaVariableNames The names of the meta variable for which to query membership. * @return True iff all meta variables are contained in the DD. */ - bool containsMetaVariables(std::unordered_set metaVariableNames) const; + bool containsMetaVariables(std::set metaVariableNames) const; /*! * Retrieves the set of all names of meta variables contained in the DD. * * @return The set of names of all meta variables contained in the DD. */ - std::unordered_set const& getContainedMetaVariableNames() const; + std::set const& getContainedMetaVariableNames() const; /*! * Retrieves the set of all names of meta variables contained in the DD. * * @return The set of names of all meta variables contained in the DD. */ - std::unordered_set& getContainedMetaVariableNames(); + std::set& getContainedMetaVariableNames(); /*! * Exports the DD to the given file in the dot format. @@ -376,7 +387,7 @@ namespace storm { * @param cuddAdd The CUDD ADD to store. * @param */ - Dd(std::shared_ptr> ddManager, ADD cuddAdd, std::unordered_set const& containedMetaVariableNames) noexcept; + Dd(std::shared_ptr> ddManager, ADD cuddAdd, std::set const& containedMetaVariableNames) noexcept; // A pointer to the manager responsible for this DD. std::shared_ptr> ddManager; @@ -385,7 +396,7 @@ namespace storm { ADD cuddAdd; // The names of all meta variables that appear in this DD. - std::unordered_set containedMetaVariableNames; + std::set containedMetaVariableNames; }; } } diff --git a/src/storage/dd/CuddDdManager.cpp b/src/storage/dd/CuddDdManager.cpp index 1c691522d..e6ca9e8e7 100644 --- a/src/storage/dd/CuddDdManager.cpp +++ b/src/storage/dd/CuddDdManager.cpp @@ -97,8 +97,8 @@ namespace storm { return nameVariablePair->second; } - std::unordered_set DdManager::getAllMetaVariableNames() const { - std::unordered_set result; + std::set DdManager::getAllMetaVariableNames() const { + std::set result; for (auto const& nameValuePair : metaVariableMap) { result.insert(nameValuePair.first); } diff --git a/src/storage/dd/CuddDdManager.h b/src/storage/dd/CuddDdManager.h index b826cce35..76da42bd5 100644 --- a/src/storage/dd/CuddDdManager.h +++ b/src/storage/dd/CuddDdManager.h @@ -1,7 +1,6 @@ #ifndef STORM_STORAGE_DD_CUDDDDMANAGER_H_ #define STORM_STORAGE_DD_CUDDDDMANAGER_H_ -#include #include #include "src/storage/dd/DdManager.h" @@ -102,7 +101,7 @@ namespace storm { * * @return The set of all meta variable names of the manager. */ - std::unordered_set getAllMetaVariableNames() const; + std::set getAllMetaVariableNames() const; private: /*!