diff --git a/src/storage/dd/CuddDd.cpp b/src/storage/dd/CuddDd.cpp index 2b1648a8c..6276a422b 100644 --- a/src/storage/dd/CuddDd.cpp +++ b/src/storage/dd/CuddDd.cpp @@ -188,6 +188,33 @@ namespace storm { this->getCuddAdd().Maximum(cubeDd.getCuddAdd()); } + void Dd::swapVariables(std::vector> const& metaVariablePairs) { + std::vector from; + std::vector to; + for (auto const& metaVariablePair : metaVariablePairs) { + DdMetaVariable const& variable1 = this->getDdManager()->getMetaVariable(metaVariablePair.first); + DdMetaVariable const& variable2 = this->getDdManager()->getMetaVariable(metaVariablePair.second); + + // Check if it's legal so swap the meta variables. + if (variable1.getNumberOfDdVariables() != variable2.getNumberOfDdVariables()) { + throw storm::exceptions::InvalidArgumentException() << "Unable to swap meta variables with different size."; + } + + // Keep track of the contained meta variables in the DD. + bool containsVariable1 = this->containsMetaVariable(metaVariablePair.first); + bool containsVariable2 = this->containsMetaVariable(metaVariablePair.second); + if (containsVariable1 && !containsVariable2) { + this->removeContainedMetaVariable(metaVariablePair.first); + this->addContainedMetaVariable(metaVariablePair.second); + } else if (!containsVariable1 && containsVariable2) { + this->removeContainedMetaVariable(metaVariablePair.second); + this->addContainedMetaVariable(metaVariablePair.first); + } + } + + // FIXME: complete this and add matrix-matrix multiplication. + } + uint_fast64_t Dd::getNonZeroCount() const { std::size_t numberOfDdVariables = 0; for (auto const& metaVariableName : this->containedMetaVariableNames) { @@ -200,16 +227,18 @@ namespace storm { return static_cast(this->cuddAdd.CountLeaves()); } + uint_fast64_t Dd::getNodeCount() const { + return static_cast(this->cuddAdd.nodeCount()); + } + double Dd::getMin() const { ADD constantMinAdd = this->getCuddAdd().FindMin(); - // FIXME - return 0; + return static_cast(Cudd_V(constantMinAdd)); } double Dd::getMax() const { ADD constantMaxAdd = this->getCuddAdd().FindMax(); - // FIXME - return 0; + return static_cast(Cudd_V(constantMaxAdd)); } void Dd::setValue(std::string const& metaVariableName, int_fast64_t variableValue, double targetValue) { @@ -280,6 +309,14 @@ namespace storm { return this->cuddAdd; } + void Dd::addContainedMetaVariable(std::string const& metaVariableName) { + this->getContainedMetaVariableNames().insert(metaVariableName); + } + + void Dd::removeContainedMetaVariable(std::string const& metaVariableName) { + this->getContainedMetaVariableNames().erase(metaVariableName); + } + std::shared_ptr> Dd::getDdManager() const { return this->ddManager; } diff --git a/src/storage/dd/CuddDd.h b/src/storage/dd/CuddDd.h index ffb82f400..a07db98d6 100644 --- a/src/storage/dd/CuddDd.h +++ b/src/storage/dd/CuddDd.h @@ -202,6 +202,14 @@ namespace storm { */ void maxAbstract(std::unordered_set const& metaVariableNames); + /*! + * Swaps the given pairs of meta variables in the DD. The pairs of meta variables must be guaranteed to have + * the same number of underlying DD variables. + * + * @param metaVariablePairs A vector of meta variable pairs that are to be swapped for one another. + */ + void swapVariables(std::vector> const& metaVariablePairs); + /*! * Retrieves the number of encodings that are mapped to a non-zero value. * @@ -216,6 +224,13 @@ namespace storm { */ uint_fast64_t getLeafCount() const; + /*! + * Retrieves the number of nodes necessary to represent the DD. + * + * @return The number of nodes in this DD. + */ + uint_fast64_t getNodeCount() const; + /*! * Retrieves the lowest function value of any encoding. * @@ -340,6 +355,20 @@ namespace storm { */ ADD const& getCuddAdd() const; + /*! + * Adds the given meta variable name to the set of meta variables that are contained in this DD. + * + * @param metaVariableName The name of the meta variable to add. + */ + void addContainedMetaVariable(std::string const& metaVariableName); + + /*! + * Removes the given meta variable name to the set of meta variables that are contained in this DD. + * + * @param metaVariableName The name of the meta variable to remove. + */ + void removeContainedMetaVariable(std::string const& metaVariableName); + /*! * Creates a DD that encapsulates the given CUDD ADD. *