Added ite operator for DDs in abstraction layer.

Former-commit-id: b1bc85e9e3

src/storage/dd/CuddDd.cpp

@@ -20,6 +20,14 @@ namespace storm {
             return this->cuddAdd != other.getCuddAdd();
         }
         
+        Dd<DdType::CUDD> Dd<DdType::CUDD>::ite(Dd<DdType::CUDD> const& thenDd, Dd<DdType::CUDD> const& elseDd) const {
+            std::set<std::string> metaVariableNames(this->getContainedMetaVariableNames());
+            metaVariableNames.insert(thenDd.getContainedMetaVariableNames().begin(), thenDd.getContainedMetaVariableNames().end());
+            metaVariableNames.insert(elseDd.getContainedMetaVariableNames().begin(), elseDd.getContainedMetaVariableNames().end());
+            
+            return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddAdd().Ite(thenDd.getCuddAdd(), elseDd.getCuddAdd()));
+        }
+        
         Dd<DdType::CUDD> Dd<DdType::CUDD>::operator+(Dd<DdType::CUDD> const& other) const {
             Dd<DdType::CUDD> result(*this);
             result += other;

src/storage/dd/CuddDd.h

@@ -50,6 +50,13 @@ namespace storm {
              */
             bool operator!=(Dd<DdType::CUDD> const& other) const;
             
+            /*!
+             * Performs an if-then-else with the given operands, i.e. maps all valuations that are mapped to a non-zero
+             * function value to the function values specified by the first DD and all others to the function values
+             * specified by the second DD.
+             */
+            Dd<DdType::CUDD> ite(Dd<DdType::CUDD> const& thenDd, Dd<DdType::CUDD> const& elseDd) const;
+            
             /*!
              * Performs a logical or of the current and the given DD.
              *