From 5b06259a05ff524d17a570df035c1f13f7eeb409 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Wed, 23 Apr 2014 16:09:33 +0200
Subject: [PATCH] Added ite operator for DDs in abstraction layer.

Former-commit-id: b1bc85e9e3f26bf1bf9c99a987af56a8dd2d42d8
---
 src/storage/dd/CuddDd.cpp | 8 ++++++++
 src/storage/dd/CuddDd.h   | 7 +++++++
 2 files changed, 15 insertions(+)

diff --git a/src/storage/dd/CuddDd.cpp b/src/storage/dd/CuddDd.cpp
index c1f42c0db..4daf835a6 100644
--- a/src/storage/dd/CuddDd.cpp
+++ b/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;
diff --git a/src/storage/dd/CuddDd.h b/src/storage/dd/CuddDd.h
index 33318ed38..32762b6cb 100644
--- a/src/storage/dd/CuddDd.h
+++ b/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.
              *