Alpha version of DD abstraction layer.

Former-commit-id: 98cc5f3aa7

src/storage/dd/CuddDd.cpp

@@ -172,7 +172,12 @@ namespace storm {
         }
         
         void Dd<CUDD>::setValue(std::unordered_map<std::string, int_fast64_t> const& metaVariableNameToValueMap, double targetValue) {
-            // TODO: Fill this
+            Dd<CUDD> 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<CUDD>::containsMetaVariable(std::string const& metaVariableName) const {

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<CUDD>;
-
+            
             // Instantiate all copy/move constructors/assignments with the default implementation.
+            Dd() = default;
             Dd(Dd<CUDD> const& other) = default;
             Dd(Dd<CUDD>&& other) = default;
             Dd& operator=(Dd<CUDD> const& other) = default;

src/storage/dd/CuddDdManager.cpp

@@ -18,9 +18,34 @@ namespace storm {
         Dd<CUDD> DdManager<CUDD>::getConstant(double value) {
             return Dd<CUDD>(this->shared_from_this(), cuddManager.constant(value), {""});
         }
+        
+        Dd<CUDD> DdManager<CUDD>::getEncoding(std::string const& metaVariableName, int_fast64_t value) {
+            std::vector<Dd<CUDD>> ddVariables = this->getMetaVariable(metaVariableName).getDdVariables();
+
+            Dd<CUDD> 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<CUDD>::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::size_t>(std::ceil(std::log2(high - low)));
             
             std::vector<Dd<CUDD>> 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::size_t>(std::ceil(std::log2(high - low)));
             std::vector<std::vector<Dd<CUDD>>> variables;
             for (uint_fast64_t bit = 0; bit < numberOfBits; ++bit) {
                 for (uint_fast64_t i = 0; i < names.size(); ++i) {

src/storage/dd/CuddDdManager.h

@@ -14,7 +14,8 @@
 namespace storm {
     namespace dd {
         template<>
-        class DdManager<CUDD> : std::enable_shared_from_this<DdManager<CUDD>> {
+        class DdManager<CUDD> : public std::enable_shared_from_this<DdManager<CUDD>> {
+        public:
             // To break the cylic dependencies, we need to forward-declare the other DD-related classes.
             friend class Dd<CUDD>;
 
@@ -50,6 +51,17 @@ namespace storm {
              */
             Dd<CUDD> 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<CUDD> getEncoding(std::string const& metaVariableName, int_fast64_t value);
+            
             /*!
              * Adds a meta variable with the given name and range.
              *

src/storage/dd/DdMetaVariable.cpp

@@ -4,9 +4,8 @@
 namespace storm {
     namespace dd {
         template<DdType Type>
-        DdMetaVariable<Type>::DdMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high, std::vector<Dd<Type>> const& ddVariables, std::shared_ptr<DdManager<Type>> manager) noexcept : name(name), low(low), high(high), ddVariables(ddVariables), manager(manager) {
+        DdMetaVariable<Type>::DdMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high, std::vector<Dd<Type>> const& ddVariables, std::shared_ptr<DdManager<Type>> 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<DdType Type>
+        std::size_t DdMetaVariable<Type>::getNumberOfDdVariables() const {
+            return this->ddVariables.size();
+        }
+        
         template<DdType Type>
         std::shared_ptr<DdManager<Type>> DdMetaVariable<Type>::getDdManager() const {
             return this->manager;
@@ -43,6 +47,6 @@ namespace storm {
         }
         
         // Explicitly instantiate DdMetaVariable.
-        template<> class DdMetaVariable<CUDD>;
+        template class DdMetaVariable<CUDD>;
     }
 }

src/storage/dd/DdMetaVariable.h

@@ -65,6 +65,13 @@ namespace storm {
              */
             std::shared_ptr<DdManager<Type>> 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.