diff --git a/src/storage/dd/CuddDd.cpp b/src/storage/dd/CuddDd.cpp index 648db72a4..2b1648a8c 100644 --- a/src/storage/dd/CuddDd.cpp +++ b/src/storage/dd/CuddDd.cpp @@ -1,12 +1,18 @@ #include "src/storage/dd/CuddDd.h" #include "src/storage/dd/CuddDdManager.h" +#include "src/exceptions/InvalidArgumentException.h" + namespace storm { namespace dd { Dd<CUDD>::Dd(std::shared_ptr<DdManager<CUDD>> ddManager, ADD cuddAdd, std::unordered_set<std::string> const& containedMetaVariableNames) noexcept : ddManager(ddManager), cuddAdd(cuddAdd), containedMetaVariableNames(containedMetaVariableNames) { // Intentionally left empty. } + bool Dd<CUDD>::operator==(Dd<CUDD> const& other) const { + return this->getCuddAdd() == other.getCuddAdd(); + } + Dd<CUDD> Dd<CUDD>::operator+(Dd<CUDD> const& other) const { Dd<CUDD> result(*this); result += other; @@ -14,7 +20,7 @@ namespace storm { } Dd<CUDD>& Dd<CUDD>::operator+=(Dd<CUDD> const& other) { - cuddAdd += other.getCuddAdd(); + 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())); @@ -29,7 +35,7 @@ namespace storm { } Dd<CUDD>& Dd<CUDD>::operator*=(Dd<CUDD> const& other) { - cuddAdd *= other.getCuddAdd(); + 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())); @@ -44,7 +50,7 @@ namespace storm { } Dd<CUDD>& Dd<CUDD>::operator-=(Dd<CUDD> const& other) { - cuddAdd -= other.getCuddAdd(); + 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())); @@ -59,7 +65,7 @@ namespace storm { } Dd<CUDD>& Dd<CUDD>::operator/=(Dd<CUDD> const& other) { - cuddAdd.Divide(other.getCuddAdd()); + 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())); @@ -74,7 +80,7 @@ namespace storm { } Dd<CUDD>& Dd<CUDD>::complement() { - cuddAdd = ~cuddAdd; + this->getCuddAdd() = ~this->getCuddAdd(); return *this; } @@ -118,6 +124,12 @@ namespace storm { Dd<CUDD> cubeDd(this->getDdManager()->getOne()); for (auto const& metaVariableName : metaVariableNames) { + // First check whether the DD contains the meta variable and erase it, if this is the case. + if (!this->containsMetaVariable(metaVariableName)) { + throw storm::exceptions::InvalidArgumentException() << "Cannot abstract from meta variable that is not present in the DD."; + } + this->getContainedMetaVariableNames().erase(metaVariableName); + DdMetaVariable<CUDD> const& metaVariable = this->getDdManager()->getMetaVariable(metaVariableName); cubeDd *= metaVariable.getCube(); } @@ -129,6 +141,12 @@ namespace storm { Dd<CUDD> cubeDd(this->getDdManager()->getOne()); for (auto const& metaVariableName : metaVariableNames) { + // First check whether the DD contains the meta variable and erase it, if this is the case. + if (!this->containsMetaVariable(metaVariableName)) { + throw storm::exceptions::InvalidArgumentException() << "Cannot abstract from meta variable that is not present in the DD."; + } + this->getContainedMetaVariableNames().erase(metaVariableName); + DdMetaVariable<CUDD> const& metaVariable = this->getDdManager()->getMetaVariable(metaVariableName); cubeDd *= metaVariable.getCube(); } @@ -140,6 +158,12 @@ namespace storm { Dd<CUDD> cubeDd(this->getDdManager()->getOne()); for (auto const& metaVariableName : metaVariableNames) { + // First check whether the DD contains the meta variable and erase it, if this is the case. + if (!this->containsMetaVariable(metaVariableName)) { + throw storm::exceptions::InvalidArgumentException() << "Cannot abstract from meta variable that is not present in the DD."; + } + this->getContainedMetaVariableNames().erase(metaVariableName); + DdMetaVariable<CUDD> const& metaVariable = this->getDdManager()->getMetaVariable(metaVariableName); cubeDd *= metaVariable.getCube(); } @@ -151,6 +175,12 @@ namespace storm { Dd<CUDD> cubeDd(this->getDdManager()->getOne()); for (auto const& metaVariableName : metaVariableNames) { + // First check whether the DD contains the meta variable and erase it, if this is the case. + if (!this->containsMetaVariable(metaVariableName)) { + throw storm::exceptions::InvalidArgumentException() << "Cannot abstract from meta variable that is not present in the DD."; + } + this->getContainedMetaVariableNames().erase(metaVariableName); + DdMetaVariable<CUDD> const& metaVariable = this->getDdManager()->getMetaVariable(metaVariableName); cubeDd *= metaVariable.getCube(); } @@ -158,6 +188,30 @@ namespace storm { this->getCuddAdd().Maximum(cubeDd.getCuddAdd()); } + uint_fast64_t Dd<CUDD>::getNonZeroCount() const { + std::size_t numberOfDdVariables = 0; + for (auto const& metaVariableName : this->containedMetaVariableNames) { + numberOfDdVariables += this->getDdManager()->getMetaVariable(metaVariableName).getNumberOfDdVariables(); + } + return static_cast<uint_fast64_t>(this->cuddAdd.CountMinterm(static_cast<int>(numberOfDdVariables))); + } + + uint_fast64_t Dd<CUDD>::getLeafCount() const { + return static_cast<uint_fast64_t>(this->cuddAdd.CountLeaves()); + } + + double Dd<CUDD>::getMin() const { + ADD constantMinAdd = this->getCuddAdd().FindMin(); + // FIXME + return 0; + } + + double Dd<CUDD>::getMax() const { + ADD constantMaxAdd = this->getCuddAdd().FindMax(); + // FIXME + return 0; + } + void Dd<CUDD>::setValue(std::string const& metaVariableName, int_fast64_t variableValue, double targetValue) { std::unordered_map<std::string, int_fast64_t> metaVariableNameToValueMap; metaVariableNameToValueMap.emplace(metaVariableName, variableValue); @@ -177,7 +231,15 @@ namespace storm { valueEncoding *= this->getDdManager()->getEncoding(nameValuePair.first, nameValuePair.second); } - this->cuddAdd = valueEncoding.getCuddAdd().Ite(this->getDdManager()->getConstant(targetValue).getCuddAdd(), this->cuddAdd); + this->getCuddAdd() = valueEncoding.getCuddAdd().Ite(this->getDdManager()->getConstant(targetValue).getCuddAdd(), this->cuddAdd); + } + + bool Dd<CUDD>::isOne() const { + return *this == this->getDdManager()->getOne(); + } + + bool Dd<CUDD>::isZero() const { + return *this == this->getDdManager()->getZero(); } bool Dd<CUDD>::containsMetaVariable(std::string const& metaVariableName) const { @@ -197,7 +259,11 @@ namespace storm { } std::unordered_set<std::string> const& Dd<CUDD>::getContainedMetaVariableNames() const { - return containedMetaVariableNames; + return this->containedMetaVariableNames; + } + + std::unordered_set<std::string>& Dd<CUDD>::getContainedMetaVariableNames() { + return this->containedMetaVariableNames; } void Dd<CUDD>::exportToDot(std::string const& filename) const { diff --git a/src/storage/dd/CuddDd.h b/src/storage/dd/CuddDd.h index 215e7e6a7..ffb82f400 100644 --- a/src/storage/dd/CuddDd.h +++ b/src/storage/dd/CuddDd.h @@ -3,6 +3,7 @@ #include <unordered_set> #include <unordered_map> +#include <memory> #include "src/storage/dd/Dd.h" @@ -27,6 +28,13 @@ namespace storm { Dd& operator=(Dd<CUDD> const& other) = default; Dd& operator=(Dd<CUDD>&& other) = default; + /*! + * Retrieves whether the two DDs represent the same function. + * + * @param other The DD that is to be compared with the current one. + */ + bool operator==(Dd<CUDD> const& other) const; + /*! * Adds the two DDs. * @@ -194,6 +202,34 @@ namespace storm { */ void maxAbstract(std::unordered_set<std::string> const& metaVariableNames); + /*! + * Retrieves the number of encodings that are mapped to a non-zero value. + * + * @return The number of encodings that are mapped to a non-zero value. + */ + uint_fast64_t getNonZeroCount() const; + + /*! + * Retrieves the number of leaves of the DD. + * + * @return The number of leaves of the DD. + */ + uint_fast64_t getLeafCount() const; + + /*! + * Retrieves the lowest function value of any encoding. + * + * @return The lowest function value of any encoding. + */ + double getMin() const; + + /*! + * Retrieves the highest function value of any encoding. + * + * @return The highest function value of any encoding. + */ + double getMax() const; + /*! * Sets the function values of all encodings that have the given value of the meta variable to the given * target value. @@ -231,6 +267,20 @@ namespace storm { */ void setValue(std::unordered_map<std::string, int_fast64_t> const& metaVariableNameToValueMap, double targetValue); + /*! + * Retrieves whether this DD represents the constant one function. + * + * @return True if this DD represents the constant one function. + */ + bool isOne() const; + + /*! + * Retrieves whether this DD represents the constant zero function. + * + * @return True if this DD represents the constant zero function. + */ + bool isZero() const; + /*! * Retrieves whether the given meta variable is contained in the DD. * @@ -254,6 +304,13 @@ namespace storm { */ std::unordered_set<std::string> 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<std::string>& getContainedMetaVariableNames(); + /*! * Exports the DD to the given file in the dot format. * diff --git a/src/storage/dd/CuddDdManager.cpp b/src/storage/dd/CuddDdManager.cpp index 15f51a3b7..1c691522d 100644 --- a/src/storage/dd/CuddDdManager.cpp +++ b/src/storage/dd/CuddDdManager.cpp @@ -1,3 +1,5 @@ +#include <cmath> + #include "src/storage/dd/CuddDdManager.h" #include "src/exceptions/InvalidArgumentException.h"