diff --git a/src/builder/DdPrismModelBuilder.cpp b/src/builder/DdPrismModelBuilder.cpp
index fb0707e77..3a897c1db 100644
--- a/src/builder/DdPrismModelBuilder.cpp
+++ b/src/builder/DdPrismModelBuilder.cpp
@@ -543,7 +543,7 @@ namespace storm {
         
         template <storm::dd::DdType Type, typename ValueType>
         typename DdPrismModelBuilder<Type, ValueType>::ActionDecisionDiagram DdPrismModelBuilder<Type, ValueType>::combineCommandsToActionMDP(GenerationInformation& generationInfo, std::vector<ActionDecisionDiagram>& commandDds, uint_fast64_t nondeterminismVariableOffset) {
-            storm::dd::Add<Type, ValueType> allGuards = generationInfo.manager->template getAddZero<ValueType>();
+            storm::dd::Bdd<Type> allGuards = generationInfo.manager->getBddZero();
             storm::dd::Add<Type, ValueType> allCommands = generationInfo.manager->template getAddZero<ValueType>();
             
             // Make all command DDs assign to the same global variables.
@@ -553,7 +553,7 @@ namespace storm {
             storm::dd::Add<Type, ValueType> sumOfGuards = generationInfo.manager->template getAddZero<ValueType>();
             for (auto const& commandDd : commandDds) {
                 sumOfGuards += commandDd.guardDd;
-                allGuards = allGuards || commandDd.guardDd;
+                allGuards |= commandDd.guardDd.toBdd();
             }
             uint_fast64_t maxChoices = static_cast<uint_fast64_t>(sumOfGuards.getMax());
 
@@ -634,7 +634,7 @@ namespace storm {
                     sumOfGuards = sumOfGuards * (!equalsNumberOfChoicesDd).template toAdd<ValueType>();
                 }
                 
-                return ActionDecisionDiagram(allGuards, allCommands, assignedGlobalVariables, nondeterminismVariableOffset + numberOfBinaryVariables);
+                return ActionDecisionDiagram(allGuards.template toAdd<ValueType>(), allCommands, assignedGlobalVariables, nondeterminismVariableOffset + numberOfBinaryVariables);
             }
         }
 
@@ -685,7 +685,7 @@ namespace storm {
                 // Add a new variable that resolves the nondeterminism between the two choices.
                 storm::dd::Add<Type, ValueType> combinedTransitions = generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[numberOfUsedNondeterminismVariables], 1).template toAdd<ValueType>().ite(action2Extended, action1Extended);
                 
-                return ActionDecisionDiagram(action1.guardDd || action2.guardDd, combinedTransitions, assignedGlobalVariables, numberOfUsedNondeterminismVariables + 1);
+                return ActionDecisionDiagram((action1.guardDd.toBdd() || action2.guardDd.toBdd()).template toAdd<ValueType>(), combinedTransitions, assignedGlobalVariables, numberOfUsedNondeterminismVariables + 1);
             } else {
                 STORM_LOG_THROW(false, storm::exceptions::InvalidStateException, "Illegal model type.");
             }
diff --git a/src/storage/dd/Add.cpp b/src/storage/dd/Add.cpp
index b3a504956..f43740418 100644
--- a/src/storage/dd/Add.cpp
+++ b/src/storage/dd/Add.cpp
@@ -35,23 +35,6 @@ namespace storm {
             metaVariables.insert(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end());
             return Add<LibraryType, ValueType>(this->getDdManager(), internalAdd.ite(thenAdd.internalAdd, elseAdd.internalAdd), metaVariables);
         }
-        
-//        template<DdType LibraryType, typename ValueType>
-//        Add<LibraryType, ValueType> Add<LibraryType, ValueType>::operator!() const {
-//            return Add<LibraryType, ValueType>(this->getDdManager(), !internalAdd, this->getContainedMetaVariables());
-//        }
-        
-        template<DdType LibraryType, typename ValueType>
-        Add<LibraryType, ValueType> Add<LibraryType, ValueType>::operator||(Add<LibraryType, ValueType> const& other) const {
-            return Add<LibraryType, ValueType>(this->getDdManager(), internalAdd || other.internalAdd, Dd<LibraryType>::joinMetaVariables(*this, other));
-        }
-        
-        template<DdType LibraryType, typename ValueType>
-        Add<LibraryType, ValueType>& Add<LibraryType, ValueType>::operator|=(Add<LibraryType, ValueType> const& other) {
-            this->addMetaVariables(other.getContainedMetaVariables());
-            internalAdd |= other.internalAdd;
-            return *this;
-        }
 
         template<DdType LibraryType, typename ValueType>
         Add<LibraryType, ValueType> Add<LibraryType, ValueType>::operator+(Add<LibraryType, ValueType> const& other) const {
diff --git a/src/storage/dd/Add.h b/src/storage/dd/Add.h
index 36cd2d98e..5134044ec 100644
--- a/src/storage/dd/Add.h
+++ b/src/storage/dd/Add.h
@@ -75,32 +75,6 @@ namespace storm {
              */
             Add<LibraryType, ValueType> ite(Add<LibraryType, ValueType> const& thenAdd, Add<LibraryType, ValueType> const& elseAdd) const;
             
-            /*!
-             * Logically inverts the current ADD. That is, all inputs yielding non-zero values will be mapped to zero in
-             * the result and vice versa.
-             *
-             * @return The resulting ADD.
-             */
-//            Add<LibraryType, ValueType> operator!() const;
-            
-            /*!
-             * Performs a logical or of the current anBd the given ADD. As a prerequisite, the operand ADDs need to be
-             * 0/1 ADDs.
-             *
-             * @param other The second ADD used for the operation.
-             * @return The logical or of the operands.
-             */
-            Add<LibraryType, ValueType> operator||(Add<LibraryType, ValueType> const& other) const;
-            
-            /*!
-             * Performs a logical or of the current and the given ADD and assigns it to the current ADD. As a
-             * prerequisite, the operand ADDs need to be 0/1 ADDs.
-             *
-             * @param other The second ADD used for the operation.
-             * @return A reference to the current ADD after the operation
-             */
-            Add<LibraryType, ValueType>& operator|=(Add<LibraryType, ValueType> const& other);
-            
             /*!
              * Adds the two ADDs.
              *
diff --git a/src/storage/dd/cudd/InternalCuddAdd.cpp b/src/storage/dd/cudd/InternalCuddAdd.cpp
index 83e317d97..40defb627 100644
--- a/src/storage/dd/cudd/InternalCuddAdd.cpp
+++ b/src/storage/dd/cudd/InternalCuddAdd.cpp
@@ -31,23 +31,7 @@ namespace storm {
         InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::ite(InternalAdd<DdType::CUDD, ValueType> const& thenDd, InternalAdd<DdType::CUDD, ValueType> const& elseDd) const {
             return InternalAdd<DdType::CUDD, ValueType>(ddManager, this->getCuddAdd().Ite(thenDd.getCuddAdd(), elseDd.getCuddAdd()));
         }
-        
-        template<typename ValueType>
-        InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::operator!() const {
-            return InternalAdd<DdType::CUDD, ValueType>(ddManager, ~this->getCuddAdd());
-        }
-        
-        template<typename ValueType>
-        InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::operator||(InternalAdd<DdType::CUDD, ValueType> const& other) const {
-            return InternalAdd<DdType::CUDD, ValueType>(ddManager, this->getCuddAdd() | other.getCuddAdd());
-        }
-        
-        template<typename ValueType>
-        InternalAdd<DdType::CUDD, ValueType>& InternalAdd<DdType::CUDD, ValueType>::operator|=(InternalAdd<DdType::CUDD, ValueType> const& other) {
-            this->cuddAdd = this->getCuddAdd() | other.getCuddAdd();
-            return *this;
-        }
-        
+                
         template<typename ValueType>
         InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::operator+(InternalAdd<DdType::CUDD, ValueType> const& other) const {
             return InternalAdd<DdType::CUDD, ValueType>(ddManager, this->getCuddAdd() + other.getCuddAdd());
diff --git a/src/storage/dd/cudd/InternalCuddAdd.h b/src/storage/dd/cudd/InternalCuddAdd.h
index 2d5b2110d..44372e6aa 100644
--- a/src/storage/dd/cudd/InternalCuddAdd.h
+++ b/src/storage/dd/cudd/InternalCuddAdd.h
@@ -82,32 +82,6 @@ namespace storm {
              */
             InternalAdd<DdType::CUDD, ValueType> ite(InternalAdd<DdType::CUDD, ValueType> const& thenAdd, InternalAdd<DdType::CUDD, ValueType> const& elseAdd) const;
             
-            /*!
-             * Logically inverts the current ADD. That is, all inputs yielding non-zero values will be mapped to zero in
-             * the result and vice versa.
-             *
-             * @return The resulting ADD.
-             */
-            InternalAdd<DdType::CUDD, ValueType> operator!() const;
-            
-            /*!
-             * Performs a logical or of the current and the given ADD. As a prerequisite, the operand ADDs need to be
-             * 0/1 ADDs.
-             *
-             * @param other The second ADD used for the operation.
-             * @return The logical or of the operands.
-             */
-            InternalAdd<DdType::CUDD, ValueType> operator||(InternalAdd<DdType::CUDD, ValueType> const& other) const;
-            
-            /*!
-             * Performs a logical or of the current and the given ADD and assigns it to the current ADD. As a
-             * prerequisite, the operand ADDs need to be 0/1 ADDs.
-             *
-             * @param other The second ADD used for the operation.
-             * @return A reference to the current ADD after the operation
-             */
-            InternalAdd<DdType::CUDD, ValueType>& operator|=(InternalAdd<DdType::CUDD, ValueType> const& other);
-            
             /*!
              * Adds the two ADDs.
              *
diff --git a/src/storage/dd/sylvan/InternalSylvanAdd.cpp b/src/storage/dd/sylvan/InternalSylvanAdd.cpp
index 453445a5d..ba7d2ec21 100644
--- a/src/storage/dd/sylvan/InternalSylvanAdd.cpp
+++ b/src/storage/dd/sylvan/InternalSylvanAdd.cpp
@@ -26,22 +26,7 @@ namespace storm {
         InternalAdd<DdType::Sylvan, ValueType> InternalAdd<DdType::Sylvan, ValueType>::ite(InternalAdd<DdType::Sylvan, ValueType> const& thenDd, InternalAdd<DdType::Sylvan, ValueType> const& elseDd) const {
             STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented.");
         }
-        
-        template<typename ValueType>
-        InternalAdd<DdType::Sylvan, ValueType> InternalAdd<DdType::Sylvan, ValueType>::operator!() const {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented.");
-        }
-        
-        template<typename ValueType>
-        InternalAdd<DdType::Sylvan, ValueType> InternalAdd<DdType::Sylvan, ValueType>::operator||(InternalAdd<DdType::Sylvan, ValueType> const& other) const {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented.");
-        }
-        
-        template<typename ValueType>
-        InternalAdd<DdType::Sylvan, ValueType>& InternalAdd<DdType::Sylvan, ValueType>::operator|=(InternalAdd<DdType::Sylvan, ValueType> const& other) {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented.");
-        }
-        
+                
         template<typename ValueType>
         InternalAdd<DdType::Sylvan, ValueType> InternalAdd<DdType::Sylvan, ValueType>::operator+(InternalAdd<DdType::Sylvan, ValueType> const& other) const {
             return InternalAdd<DdType::Sylvan, ValueType>(ddManager, this->sylvanMtbdd.Plus(other.sylvanMtbdd));
diff --git a/src/storage/dd/sylvan/InternalSylvanAdd.h b/src/storage/dd/sylvan/InternalSylvanAdd.h
index 39696ae9b..3cc68a761 100644
--- a/src/storage/dd/sylvan/InternalSylvanAdd.h
+++ b/src/storage/dd/sylvan/InternalSylvanAdd.h
@@ -81,33 +81,7 @@ namespace storm {
              * @return The ADD corresponding to the if-then-else of the operands.
              */
             InternalAdd<DdType::Sylvan, ValueType> ite(InternalAdd<DdType::Sylvan, ValueType> const& thenAdd, InternalAdd<DdType::Sylvan, ValueType> const& elseAdd) const;
-            
-            /*!
-             * Logically inverts the current ADD. That is, all inputs yielding non-zero values will be mapped to zero in
-             * the result and vice versa.
-             *
-             * @return The resulting ADD.
-             */
-            InternalAdd<DdType::Sylvan, ValueType> operator!() const;
-            
-            /*!
-             * Performs a logical or of the current and the given ADD. As a prerequisite, the operand ADDs need to be
-             * 0/1 ADDs.
-             *
-             * @param other The second ADD used for the operation.
-             * @return The logical or of the operands.
-             */
-            InternalAdd<DdType::Sylvan, ValueType> operator||(InternalAdd<DdType::Sylvan, ValueType> const& other) const;
-            
-            /*!
-             * Performs a logical or of the current and the given ADD and assigns it to the current ADD. As a
-             * prerequisite, the operand ADDs need to be 0/1 ADDs.
-             *
-             * @param other The second ADD used for the operation.
-             * @return A reference to the current ADD after the operation
-             */
-            InternalAdd<DdType::Sylvan, ValueType>& operator|=(InternalAdd<DdType::Sylvan, ValueType> const& other);
-            
+                        
             /*!
              * Adds the two ADDs.
              *