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 Dd::ite(Dd const& thenDd, Dd const& elseDd) const { + std::set metaVariableNames(this->getContainedMetaVariableNames()); + metaVariableNames.insert(thenDd.getContainedMetaVariableNames().begin(), thenDd.getContainedMetaVariableNames().end()); + metaVariableNames.insert(elseDd.getContainedMetaVariableNames().begin(), elseDd.getContainedMetaVariableNames().end()); + + return Dd(this->getDdManager(), this->getCuddAdd().Ite(thenDd.getCuddAdd(), elseDd.getCuddAdd())); + } + Dd Dd::operator+(Dd const& other) const { Dd 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 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 ite(Dd const& thenDd, Dd const& elseDd) const; + /*! * Performs a logical or of the current and the given DD. *