Further work on abstraction layer for DDs.

Former-commit-id: 245986076b

src/storage/dd/CuddDd.cpp

@@ -0,0 +1,90 @@
+#include "src/storage/dd/CuddDd.h"
+
+namespace storm {
+    namespace dd {
+        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.
+        }
+        
+        Dd<CUDD> Dd<CUDD>::operator+(Dd<CUDD> const& other) const {
+            Dd<CUDD> result(*this);
+            result += other;
+            return result;
+        }
+        
+        Dd<CUDD>& Dd<CUDD>::operator+=(Dd<CUDD> const& other) {
+            cuddAdd += other;
+            
+            // Join the variable sets of the two participating DDs.
+            std::copy(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().containedMetaVariableNames.end(), std::inserter(this->containedMetaVariableNames, this->containedMetaVariableNames.end()));
+            
+            return *this;
+        }
+        
+        Dd<CUDD> Dd<CUDD>::operator*(Dd<CUDD> const& other) const {
+            Dd<CUDD> result(*this);
+            result *= other;
+            return result;
+        }
+        
+        Dd<CUDD>& Dd<CUDD>::operator*=(Dd<CUDD> const& other) {
+            cuddAdd *= other;
+            
+            // Join the variable sets of the two participating DDs.
+            std::copy(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().containedMetaVariableNames.end(), std::inserter(this->containedMetaVariableNames, this->containedMetaVariableNames.end()));
+            
+            return *this;
+        }
+        
+        Dd<CUDD> Dd<CUDD>::operator-(Dd<CUDD> const& other) const {
+            Dd<CUDD> result(*this);
+            result -= other;
+            return result;
+        }
+        
+        Dd<CUDD>& Dd<CUDD>::operator-=(Dd<CUDD> const& other) {
+            cuddAdd -= other;
+            
+            // Join the variable sets of the two participating DDs.
+            std::copy(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().containedMetaVariableNames.end(), std::inserter(this->containedMetaVariableNames, this->containedMetaVariableNames.end()));
+            
+            return *this;
+        }
+        
+        Dd<CUDD> Dd<CUDD>::operator/(Dd<CUDD> const& other) const {
+            Dd<CUDD> result(*this);
+            result /= other;
+            return result;
+        }
+        
+        Dd<CUDD>& Dd<CUDD>::operator/=(Dd<CUDD> const& other) {
+            cuddAdd.Divide(other);
+            
+            // Join the variable sets of the two participating DDs.
+            std::copy(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().containedMetaVariableNames.end(), std::inserter(this->containedMetaVariableNames, this->containedMetaVariableNames.end()));
+            
+            return *this;
+        }
+        
+        Dd<CUDD> Dd<CUDD>::operator~() const {
+            Dd<CUDD> result(*this);
+            result.complement();
+            return result;
+        }
+        
+        Dd<CUDD>& Dd<CUDD>::complement() {
+            cuddAdd = ~cuddAdd;
+            return *this;
+        }
+        
+        void Dd<CUDD>::exportToDot(std::string const& filename) const {
+            FILE* filePointer = fopen(filename.c_str() , "w");
+            this->getDdManager()->getCuddManager().DumpDot({this->cuddAdd}, nullptr, nullptr, filePointer);
+            fclose(filePointer);
+        }
+        
+        std::shared_ptr<DdManager<CUDD>> Dd<CUDD>::getDdManager() const {
+            return this->ddManager;
+        }
+    }
+}

src/storage/dd/CuddDd.h

@@ -12,13 +12,10 @@ namespace storm {
         
         template<>
         class Dd<CUDD> {
-            /*!
-             * Creates a DD that encapsulates the given CUDD ADD.
-             *
-             * @param cuddAdd The CUDD ADD to store.
-             */
-            Dd(ADD cuddAdd);
-            
+        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(Dd<CUDD> const& other) = default;
             Dd(Dd<CUDD>&& other) = default;
@@ -89,6 +86,13 @@ namespace storm {
              */
             Dd<CUDD>& operator/=(Dd<CUDD> const& other);
             
+            /*!
+             * Subtracts the DD from the constant zero function.
+             *
+             * @return The resulting function represented as a DD.
+             */
+            Dd<CUDD> minus() const;
+            
             /*!
              * Retrieves the logical complement of the current DD. The result will map all encodings with a value
              * unequal to zero to false and all others to true.
@@ -100,8 +104,157 @@ namespace storm {
             /*!
              * Logically complements the current DD. The result will map all encodings with a value
              * unequal to zero to false and all others to true.
+             *
+             * @return A reference to the current DD after the operation.
+             */
+            Dd<CUDD>& complement();
+            
+            /*!
+             * Retrieves the function that maps all evaluations to one that have an identical function values.
+             *
+             * @param other The DD with which to perform the operation.
+             * @return The resulting function represented as a DD.
+             */
+            Dd<CUDD> equals(Dd<CUDD> const& other) const;
+            
+            /*!
+             * Retrieves the function that maps all evaluations to one that have distinct function values.
+             *
+             * @param other The DD with which to perform the operation.
+             * @return The resulting function represented as a DD.
+             */
+            Dd<CUDD> notEquals(Dd<CUDD> const& other) const;
+            
+            /*!
+             * Retrieves the function that maps all evaluations to one whose function value in the first DD are less
+             * than the one in the given DD.
+             *
+             * @param other The DD with which to perform the operation.
+             * @return The resulting function represented as a DD.
+             */
+            Dd<CUDD> less(Dd<CUDD> const& other) const;
+            
+            /*!
+             * Retrieves the function that maps all evaluations to one whose function value in the first DD are less or
+             * equal than the one in the given DD.
+             *
+             * @param other The DD with which to perform the operation.
+             * @return The resulting function represented as a DD.
+             */
+            Dd<CUDD> lessOrEqual(Dd<CUDD> const& other) const;
+            
+            /*!
+             * Retrieves the function that maps all evaluations to one whose function value in the first DD are greater
+             * than the one in the given DD.
+             *
+             * @param other The DD with which to perform the operation.
+             * @return The resulting function represented as a DD.
              */
-            void complement();
+            Dd<CUDD> greater(Dd<CUDD> const& other) const;
+            
+            /*!
+             * Retrieves the function that maps all evaluations to one whose function value in the first DD are greater
+             * or equal than the one in the given DD.
+             *
+             * @param other The DD with which to perform the operation.
+             * @return The resulting function represented as a DD.
+             */
+            Dd<CUDD> greaterOrEqual(Dd<CUDD> const& other) const;
+            
+            /*!
+             * Existentially abstracts from the given meta variables.
+             *
+             * @param metaVariableNames The names of all meta variables from which to abstract.
+             */
+            void existsAbstract(std::unordered_set<std::string> 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<std::string> 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<std::string> 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<std::string> const& metaVariableNames);
+
+            /*!
+             * Sets the function values of all encodings that have the given value of the meta variable to the given
+             * target value.
+             *
+             * @param metaVariableName The name of the meta variable that has to be equal to the given value.
+             * @param variableValue The value that the meta variable is supposed to have. This must be within the range
+             * of the meta variable.
+             * @param targetValue The new function value of the modified encodings.
+             */
+            void setValue(std::string const& metaVariableName, int_fast64_t variableValue, double targetValue);
+
+            /*!
+             * Sets the function values of all encodings that have the given values of the two meta variables to the
+             * given target value.
+             *
+             * @param metaVariableName1 The name of the first meta variable that has to be equal to the first given
+             * value.
+             * @param variableValue1 The value that the first meta variable is supposed to have. This must be within the
+             * range of the meta variable.
+             * @param metaVariableName2 The name of the first meta variable that has to be equal to the second given
+             * value.
+             * @param variableValue2 The value that the second meta variable is supposed to have. This must be within
+             * the range of the meta variable.
+             * @param targetValue The new function value of the modified encodings.
+             */
+            void setValue(std::string const& metaVariableName1, int_fast64_t variableValue1, std::string const& metaVariableName2, int_fast64_t variableValue2, double targetValue);
+            
+            /*!
+             * Sets the function values of all encodings that have the given values of the given meta variables to the
+             * given target value.
+             *
+             * @param metaVariableNameToValueMap A mapping of meta variable names to the values they are supposed to
+             * have. All values must be within the range of the respective meta variable.
+             * @param targetValue The new function value of the modified encodings.
+             */
+            void setValue(std::unordered_map<std::string, int_fast64_t> const& metaVariableNameToValueMap, double targetValue);
+            
+            /*!
+             * Retrieves whether the given meta variable is contained in the DD.
+             *
+             * @param metaVariableName The name of the meta variable for which to query membership.
+             * @return True iff the meta variable is contained in the DD.
+             */
+            bool containsMetaVariable(std::string const& metaVariableName) const;
+            
+            /*!
+             * Retrieves whether the given meta variables are all contained in the DD.
+             *
+             * @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<std::string> 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<std::string> const& getContainedMetaVariableNames() const;
+            
+            /*!
+             * Exports the DD to the given file in the dot format.
+             *
+             * @param filename The name of the file to which the DD is to be exported.
+             */
+            void exportToDot(std::string const& filename) const;
             
             /*!
              * Retrieves the manager that is responsible for this DD.
@@ -111,6 +264,15 @@ namespace storm {
             std::shared_ptr<DdManager<CUDD>> getDdManager() const;
             
         private:
+            /*!
+             * Creates a DD that encapsulates the given CUDD ADD.
+             *
+             * @param ddManager The manager responsible for this DD.
+             * @param cuddAdd The CUDD ADD to store.
+             * @param
+             */
+            Dd(std::shared_ptr<DdManager<CUDD>> ddManager, ADD cuddAdd, std::unordered_set<std::string> const& containedMetaVariableNames) noexcept;
+            
             // A pointer to the manager responsible for this DD.
             std::shared_ptr<DdManager<CUDD>> ddManager;
 

src/storage/dd/CuddDdManager.cpp

@@ -1,7 +1,75 @@
 #include "src/storage/dd/CuddDdManager.h"
+#include "src/exceptions/InvalidArgumentException.h"
 
 namespace storm {
     namespace dd {
+        DdManager<CUDD>::DdManager() noexcept : metaVariableMap(), cuddManager() {
+            // Intentionally left empty.
+        }
         
+        Dd<CUDD> DdManager<CUDD>::getOne() {
+            return Dd<CUDD>(this->shared_from_this(), cuddManager.addOne(), {""});
+        }
+        
+        Dd<CUDD> DdManager<CUDD>::getZero() {
+            return Dd<CUDD>(this->shared_from_this(), cuddManager.addZero(), {""});
+        }
+        
+        Dd<CUDD> DdManager<CUDD>::getConstant(double value) {
+            return Dd<CUDD>(this->shared_from_this(), cuddManager.constant(value), {""});
+        }
+
+        void DdManager<CUDD>::addMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high) {
+            std::size_t numberOfBits = std::log2(high - low);
+            
+            std::vector<Dd<CUDD>> variables;
+            for (std::size_t i = 0; i < numberOfBits; ++i) {
+                variables.emplace_back(cuddManager.addVar());
+            }
+            
+            metaVariableMap.emplace(name, low, high, variables, this->shared_from_this());
+        }
+        
+        void DdManager<CUDD>::addMetaVariablesInterleaved(std::vector<std::string> const& names, int_fast64_t low, int_fast64_t high) {
+            if (names.size() == 0) {
+                throw storm::exceptions::InvalidArgumentException() << "Illegal to add zero meta variables.";
+            }
+            
+            // Add the variables in interleaved order.
+            std::size_t numberOfBits = 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) {
+                    variables[i].emplace_back(cuddManager.addVar());
+                }
+            }
+            
+            // Now add the meta variables.
+            for (uint_fast64_t i = 0; i < names.size(); ++i) {
+                metaVariableMap.emplace(names[i], low, high, variables[i], this->shared_from_this());
+            }
+        }
+        
+        DdMetaVariable<CUDD> const& DdManager<CUDD>::getMetaVariable(std::string const& metaVariableName) const {
+            auto const& nameVariablePair = metaVariableMap.find(metaVariableName);
+            
+            if (nameVariablePair == metaVariableMap.end()) {
+                throw storm::exceptions::InvalidArgumentException() << "Unknown meta variable name.";
+            }
+            
+            return nameVariablePair->second;
+        }
+        
+        std::unordered_set<std::string> DdManager<CUDD>::getAllMetaVariableNames() const {
+            std::unordered_set<std::string> result;
+            for (auto const& nameValuePair : metaVariableMap) {
+                result.insert(nameValuePair.first);
+            }
+            return result;
+        }
+        
+        Cudd& DdManager<CUDD>::getCuddManager() {
+            return this->cuddManager;
+        }
     }
 }

src/storage/dd/CuddDdManager.h

@@ -5,22 +5,24 @@
 #include <unordered_map>
 
 #include "src/storage/dd/DdManager.h"
+#include "src/storage/dd/DdMetaVariable.h"
+#include "src/storage/dd/CuddDd.h"
 
 // Include the C++-interface of CUDD.
 #include "cuddObj.hh"
 
 namespace storm {
     namespace dd {
-        // To break the cylic dependencies, we need to forward-declare the other DD-related classes.
-        template<DdType Type> class DdMetaVariable;
-        template<DdType Type> class Dd;
-        
         template<>
         class DdManager<CUDD> : std::enable_shared_from_this<DdManager<CUDD>> {
+            // To break the cylic dependencies, we need to forward-declare the other DD-related classes.
+            friend class DdMetaVariable<CUDD>;
+            friend class Dd<CUDD>;
+
             /*!
              * Creates an empty manager without any meta variables.
              */
-            DdManager();
+            DdManager() noexcept;
             
             // Explictly forbid copying a DdManager, but allow moving it.
             DdManager(DdManager<CUDD> const& other) = delete;
@@ -55,12 +57,17 @@ namespace storm {
              * @param name The name of the meta variable.
              * @param low The lowest value of the range of the variable.
              * @param high The highest value of the range of the variable.
-             * @param addSuccessorVariable If set, a second meta variable is added. This can then be used, for example,
-             * to encode the value of the meta variable in a successor state.
-             * @param useInterleavedVariableOrdering If set, the variables used for the successor meta variable are
-             * interleaved with the ones for the added meta variable.
              */
-            void addMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high, bool addSuccessorVariable = false, bool useInterleavedVariableOrdering = true);
+            void addMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high);
+            
+            /*!
+             * Adds meta variables with the given names and (equal) range and arranges the DD variables in an interleaved order.
+             *
+             * @param names The names of the variables.
+             * @param low The lowest value of the ranges of the variables.
+             * @param high The highest value of the ranges of the variables.
+             */
+            void addMetaVariablesInterleaved(std::vector<std::string> const& names, int_fast64_t low, int_fast64_t high);
             
             /*!
              * Retrieves the meta variable with the given name if it exists.
@@ -71,21 +78,20 @@ namespace storm {
             DdMetaVariable<CUDD> const& getMetaVariable(std::string const& metaVariableName) const;
             
             /*!
-             * Retrieves the successor meta variable of the one with the given name if it exists.
+             * Retrieves the names of all meta variables that have been added to the manager.
              *
-             * @param metaVariableName The name of the meta variable whose successor meta variable to retrieve.
-             * @return The successor meta variable of the one with the given name.
+             * @return The set of all meta variable names of the manager.
              */
-            DdMetaVariable<CUDD> const& getSuccessorMetaVariable(std::string const& metaVariableName) const;
+            std::unordered_set<std::string> getAllMetaVariableNames() const;
             
+        private:
             /*!
-             * Retrieves the names of all meta variables that have been added to the manager.
+             * Retrieves the underlying CUDD manager.
              *
-             * @return The set of all meta variable names of the manager.
+             * @return The underlying CUDD manager.
              */
-            std::unordered_set<std::string> getAllMetaVariableNames();
+            Cudd& getCuddManager();
             
-        private:
             // A mapping from variable names to the meta variable information.
             std::unordered_map<std::string, DdMetaVariable<CUDD>> metaVariableMap;
             

src/storage/dd/DdMetaVariable.cpp

@@ -3,8 +3,12 @@
 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) : name(name), low(low), high(high), ddVariables(ddVariables), manager(manager) {
-            // Intentionally left empty.
+        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) {
+            // Create the cube of all variables of this meta variable.
+            this->cube = this->getDdManager()->getOne();
+            for (auto const& ddVariable : this->ddVariables) {
+                this->cube *= ddVariable;
+            }
         }
         
         template<DdType Type>
@@ -21,6 +25,11 @@ namespace storm {
         int_fast64_t DdMetaVariable<Type>::getHigh() const {
             return this->high;
         }
+        
+        template<DdType Type>
+        std::shared_ptr<DdManager<Type>> DdMetaVariable<Type>::getDdManager() const {
+            return this->manager;
+        }
 
         template<DdType Type>
         std::vector<Dd<Type>> const& DdMetaVariable<Type>::getDdVariables() const {

src/storage/dd/DdMetaVariable.h

@@ -14,8 +14,8 @@ namespace storm {
         
         template <DdType Type>
         class DdMetaVariable {
-            // Declare the other DD-related classes as friends so they can access the internals of a meta variable.
-            friend class Dd<Type>;
+            // Declare the DdManager class as friend so it can access the internals of a meta variable.
+            friend class DdManager<Type>;
             
             /*!
              * Creates a meta variable with the given name, range bounds.
@@ -26,7 +26,7 @@ namespace storm {
              * @param ddVariables The vector of variables used to encode this variable.
              * @param manager A pointer to the manager that is responsible for this meta variable.
              */
-            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);
+            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;
             
             // Explictly generate all default versions of copy/move constructors/assignments.
             DdMetaVariable(DdMetaVariable const& other) = default;

src/storage/dd/DdType.h

@@ -0,0 +1,12 @@
+#ifndef STORM_STORAGE_DD_DDTYPE_H_
+#define STORM_STORAGE_DD_DDTYPE_H_
+
+namespace storm {
+    namespace dd {
+        enum DdType {
+            CUDD
+        };
+    }
+}
+
+#endif /* STORM_STORAGE_DD_DDTYPE_H_ */