From 151324198508f619446cf56b1af0c3d3748efc67 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Fri, 30 May 2014 19:53:35 +0200
Subject: [PATCH] Added functions for more efficiently retrieving the DD for
 'greater than constant', 'greater or equal than constant' and 'notZero'.

Former-commit-id: 9d80c29f271a83bc492027443a8d2e430f97f47c
---
 src/storage/dd/CuddDd.cpp | 12 ++++++++++--
 src/storage/dd/CuddDd.h   | 22 ++++++++++++++++++++--
 2 files changed, 30 insertions(+), 4 deletions(-)

diff --git a/src/storage/dd/CuddDd.cpp b/src/storage/dd/CuddDd.cpp
index d3789d073..fde9d008a 100644
--- a/src/storage/dd/CuddDd.cpp
+++ b/src/storage/dd/CuddDd.cpp
@@ -314,10 +314,18 @@ 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 {
             std::size_t numberOfDdVariables = 0;
             for (auto const& metaVariableName : this->containedMetaVariableNames) {
diff --git a/src/storage/dd/CuddDd.h b/src/storage/dd/CuddDd.h
index 4de29e513..6d91960ba 100644
--- a/src/storage/dd/CuddDd.h
+++ b/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.