Added functions for more efficiently retrieving the DD for 'greater than constant', 'greater or equal than constant' and 'notZero'.

Former-commit-id: 9d80c29f27

src/storage/dd/CuddDd.cpp

@@ -314,8 +314,16 @@ namespace storm {
             return Dd<DdType::CUDD>(this->getDdManager(), this->cuddAdd.MatrixMultiply(otherMatrix.getCuddAdd(), summationDdVariables), containedMetaVariableNames);
         }
         
-        Dd<DdType::CUDD> Dd<DdType::CUDD>::greaterZero() const {
-            return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddAdd().BddStrictThreshold(0).Add(), this->getContainedMetaVariableNames());
+        Dd<DdType::CUDD> Dd<DdType::CUDD>::greater(double value) const {
+            return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddAdd().BddStrictThreshold(value).Add(), this->getContainedMetaVariableNames());
+        }
+        
+        Dd<DdType::CUDD> Dd<DdType::CUDD>::greaterOrEqual(double value) const {
+            return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddAdd().BddThreshold(value).Add(), this->getContainedMetaVariableNames());
+        }
+
+        Dd<DdType::CUDD> Dd<DdType::CUDD>::notZero() const {
+            return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddAdd().BddPattern().Add(), this->getContainedMetaVariableNames());
         }
 
         uint_fast64_t Dd<DdType::CUDD>::getNonZeroCount() const {

src/storage/dd/CuddDd.h

@@ -293,11 +293,29 @@ namespace storm {
             
             /*!
              * Computes a DD that represents the function in which all assignments with a function value strictly larger
-             * than zero are mapped to one and all others to zero.
+             * than the given value are mapped to one and all others to zero.
              *
+             * @param value The value used for the comparison.
              * @return The resulting DD.
              */
-            Dd<DdType::CUDD> greaterZero() const;
+            Dd<DdType::CUDD> greater(double value) const;
+
+            /*!
+             * Computes a DD that represents the function in which all assignments with a function value larger or equal
+             * to the given value are mapped to one and all others to zero.
+             *
+             * @param value The value used for the comparison.
+             * @return The resulting DD.
+             */
+            Dd<DdType::CUDD> greaterOrEqual(double value) const;
+            
+            /*!
+             * Computes a DD that represents the function in which all assignments with a function value unequal to zero
+             * are mapped to one and all others to zero.
+             *
+             * @return The resulting DD.
+             */
+            Dd<DdType::CUDD> notZero() const;
             
             /*!
              * Retrieves the number of encodings that are mapped to a non-zero value.