diff --git a/src/storage/dd/CuddDd.cpp b/src/storage/dd/CuddDd.cpp index 23f148da0..648db72a4 100644 --- a/src/storage/dd/CuddDd.cpp +++ b/src/storage/dd/CuddDd.cpp @@ -172,7 +172,12 @@ namespace storm { } void Dd::setValue(std::unordered_map const& metaVariableNameToValueMap, double targetValue) { - // TODO: Fill this + Dd valueEncoding(this->getDdManager()->getOne()); + for (auto const& nameValuePair : metaVariableNameToValueMap) { + valueEncoding *= this->getDdManager()->getEncoding(nameValuePair.first, nameValuePair.second); + } + + this->cuddAdd = valueEncoding.getCuddAdd().Ite(this->getDdManager()->getConstant(targetValue).getCuddAdd(), this->cuddAdd); } bool Dd::containsMetaVariable(std::string const& metaVariableName) const { diff --git a/src/storage/dd/CuddDd.h b/src/storage/dd/CuddDd.h index b0a3e33eb..215e7e6a7 100644 --- a/src/storage/dd/CuddDd.h +++ b/src/storage/dd/CuddDd.h @@ -19,8 +19,9 @@ namespace storm { public: // Declare the DdManager class as friend so it can access the internals of a DD. friend class DdManager; - + // Instantiate all copy/move constructors/assignments with the default implementation. + Dd() = default; Dd(Dd const& other) = default; Dd(Dd&& other) = default; Dd& operator=(Dd const& other) = default; diff --git a/src/storage/dd/CuddDdManager.cpp b/src/storage/dd/CuddDdManager.cpp index 40c11fbaa..cce1edbfe 100644 --- a/src/storage/dd/CuddDdManager.cpp +++ b/src/storage/dd/CuddDdManager.cpp @@ -18,9 +18,34 @@ namespace storm { Dd DdManager::getConstant(double value) { return Dd(this->shared_from_this(), cuddManager.constant(value), {""}); } + + Dd DdManager::getEncoding(std::string const& metaVariableName, int_fast64_t value) { + std::vector> ddVariables = this->getMetaVariable(metaVariableName).getDdVariables(); + + Dd result; + if (value & (1ull << (ddVariables.size() - 1))) { + result = ddVariables[0]; + } else { + result = ddVariables[0]; + } + + for (std::size_t i = 1; i < ddVariables.size(); ++i) { + if (value & (1ull << (ddVariables.size() - i - 1))) { + result *= ddVariables[i]; + } else { + result *= ~ddVariables[i]; + } + } + + return result; + } void DdManager::addMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high) { - std::size_t numberOfBits = std::log2(high - low); + if (high == low) { + throw storm::exceptions::InvalidArgumentException() << "Range of meta variable must be at least 2 elements."; + } + + std::size_t numberOfBits = static_cast(std::ceil(std::log2(high - low))); std::vector> variables; for (std::size_t i = 0; i < numberOfBits; ++i) { @@ -36,7 +61,7 @@ namespace storm { } // Add the variables in interleaved order. - std::size_t numberOfBits = std::log2(high - low); + std::size_t numberOfBits = static_cast(std::ceil(std::log2(high - low))); std::vector>> variables; for (uint_fast64_t bit = 0; bit < numberOfBits; ++bit) { for (uint_fast64_t i = 0; i < names.size(); ++i) { diff --git a/src/storage/dd/CuddDdManager.h b/src/storage/dd/CuddDdManager.h index ede42104d..1d061b504 100644 --- a/src/storage/dd/CuddDdManager.h +++ b/src/storage/dd/CuddDdManager.h @@ -14,7 +14,8 @@ namespace storm { namespace dd { template<> - class DdManager : std::enable_shared_from_this> { + class DdManager : public std::enable_shared_from_this> { + public: // To break the cylic dependencies, we need to forward-declare the other DD-related classes. friend class Dd; @@ -50,6 +51,17 @@ namespace storm { */ Dd getConstant(double value); + /*! + * Retrieves the DD representing the function that maps all inputs which have the given meta variable equal + * to the given value one. + * + * @param metaVariableName The meta variable that is supposed to have the given value. + * @param value The value the meta variable is supposed to have. + * @return The DD representing the function that maps all inputs which have the given meta variable equal + * to the given value one. + */ + Dd getEncoding(std::string const& metaVariableName, int_fast64_t value); + /*! * Adds a meta variable with the given name and range. * diff --git a/src/storage/dd/DdMetaVariable.cpp b/src/storage/dd/DdMetaVariable.cpp index d5cae858c..72e7baba5 100644 --- a/src/storage/dd/DdMetaVariable.cpp +++ b/src/storage/dd/DdMetaVariable.cpp @@ -4,9 +4,8 @@ namespace storm { namespace dd { template - DdMetaVariable::DdMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high, std::vector> const& ddVariables, std::shared_ptr> manager) noexcept : name(name), low(low), high(high), ddVariables(ddVariables), manager(manager) { + DdMetaVariable::DdMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high, std::vector> const& ddVariables, std::shared_ptr> manager) noexcept : name(name), low(low), high(high), ddVariables(ddVariables), cube(manager->getOne()), manager(manager) { // Create the cube of all variables of this meta variable. - this->cube = this->getDdManager()->getOne(); for (auto const& ddVariable : this->ddVariables) { this->cube *= ddVariable; } @@ -27,6 +26,11 @@ namespace storm { return this->high; } + template + std::size_t DdMetaVariable::getNumberOfDdVariables() const { + return this->ddVariables.size(); + } + template std::shared_ptr> DdMetaVariable::getDdManager() const { return this->manager; @@ -43,6 +47,6 @@ namespace storm { } // Explicitly instantiate DdMetaVariable. - template<> class DdMetaVariable; + template class DdMetaVariable; } } \ No newline at end of file diff --git a/src/storage/dd/DdMetaVariable.h b/src/storage/dd/DdMetaVariable.h index 6bf5f6c3c..c5e7c00cf 100644 --- a/src/storage/dd/DdMetaVariable.h +++ b/src/storage/dd/DdMetaVariable.h @@ -65,6 +65,13 @@ namespace storm { */ std::shared_ptr> getDdManager() const; + + /*! + * Retrieves the number of DD variables for this meta variable. + * + * @return The number of DD variables for this meta variable. + */ + std::size_t getNumberOfDdVariables() const; private: /*! * Retrieves the variables used to encode the meta variable.