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(this->getDdManager(), this->cuddAdd.MatrixMultiply(otherMatrix.getCuddAdd(), summationDdVariables), containedMetaVariableNames); } - Dd Dd::greaterZero() const { - return Dd(this->getDdManager(), this->getCuddAdd().BddStrictThreshold(0).Add(), this->getContainedMetaVariableNames()); + Dd Dd::greater(double value) const { + return Dd(this->getDdManager(), this->getCuddAdd().BddStrictThreshold(value).Add(), this->getContainedMetaVariableNames()); } + Dd Dd::greaterOrEqual(double value) const { + return Dd(this->getDdManager(), this->getCuddAdd().BddThreshold(value).Add(), this->getContainedMetaVariableNames()); + } + + Dd Dd::notZero() const { + return Dd(this->getDdManager(), this->getCuddAdd().BddPattern().Add(), this->getContainedMetaVariableNames()); + } + uint_fast64_t Dd::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 greaterZero() const; + Dd 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 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 notZero() const; /*! * Retrieves the number of encodings that are mapped to a non-zero value.