From dea56e1bd407984b00b63ef974744e47c7af37e0 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 24 Mar 2014 00:08:23 +0100 Subject: [PATCH] Added some missing includes and some stubs for additional functionality of DD abstraction layer. Former-commit-id: d90d525993228f8d5255c6cbd1950e6f781e4f10 --- src/storage/dd/CuddDd.cpp | 80 +++++++++++++++++++++++++++++--- src/storage/dd/CuddDd.h | 57 +++++++++++++++++++++++ src/storage/dd/CuddDdManager.cpp | 2 + 3 files changed, 132 insertions(+), 7 deletions(-) diff --git a/src/storage/dd/CuddDd.cpp b/src/storage/dd/CuddDd.cpp index 648db72a4..2b1648a8c 100644 --- a/src/storage/dd/CuddDd.cpp +++ b/src/storage/dd/CuddDd.cpp @@ -1,12 +1,18 @@ #include "src/storage/dd/CuddDd.h" #include "src/storage/dd/CuddDdManager.h" +#include "src/exceptions/InvalidArgumentException.h" + namespace storm { namespace dd { Dd::Dd(std::shared_ptr> ddManager, ADD cuddAdd, std::unordered_set const& containedMetaVariableNames) noexcept : ddManager(ddManager), cuddAdd(cuddAdd), containedMetaVariableNames(containedMetaVariableNames) { // Intentionally left empty. } + bool Dd::operator==(Dd const& other) const { + return this->getCuddAdd() == other.getCuddAdd(); + } + Dd Dd::operator+(Dd const& other) const { Dd result(*this); result += other; @@ -14,7 +20,7 @@ namespace storm { } Dd& Dd::operator+=(Dd const& other) { - cuddAdd += other.getCuddAdd(); + this->getCuddAdd() += other.getCuddAdd(); // Join the variable sets of the two participating DDs. std::copy(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end(), std::inserter(this->containedMetaVariableNames, this->containedMetaVariableNames.end())); @@ -29,7 +35,7 @@ namespace storm { } Dd& Dd::operator*=(Dd const& other) { - cuddAdd *= other.getCuddAdd(); + this->getCuddAdd() *= other.getCuddAdd(); // Join the variable sets of the two participating DDs. std::copy(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end(), std::inserter(this->containedMetaVariableNames, this->containedMetaVariableNames.end())); @@ -44,7 +50,7 @@ namespace storm { } Dd& Dd::operator-=(Dd const& other) { - cuddAdd -= other.getCuddAdd(); + this->getCuddAdd() -= other.getCuddAdd(); // Join the variable sets of the two participating DDs. std::copy(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end(), std::inserter(this->containedMetaVariableNames, this->containedMetaVariableNames.end())); @@ -59,7 +65,7 @@ namespace storm { } Dd& Dd::operator/=(Dd const& other) { - cuddAdd.Divide(other.getCuddAdd()); + this->getCuddAdd().Divide(other.getCuddAdd()); // Join the variable sets of the two participating DDs. std::copy(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end(), std::inserter(this->containedMetaVariableNames, this->containedMetaVariableNames.end())); @@ -74,7 +80,7 @@ namespace storm { } Dd& Dd::complement() { - cuddAdd = ~cuddAdd; + this->getCuddAdd() = ~this->getCuddAdd(); return *this; } @@ -118,6 +124,12 @@ namespace storm { Dd cubeDd(this->getDdManager()->getOne()); for (auto const& metaVariableName : metaVariableNames) { + // First check whether the DD contains the meta variable and erase it, if this is the case. + if (!this->containsMetaVariable(metaVariableName)) { + throw storm::exceptions::InvalidArgumentException() << "Cannot abstract from meta variable that is not present in the DD."; + } + this->getContainedMetaVariableNames().erase(metaVariableName); + DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(metaVariableName); cubeDd *= metaVariable.getCube(); } @@ -129,6 +141,12 @@ namespace storm { Dd cubeDd(this->getDdManager()->getOne()); for (auto const& metaVariableName : metaVariableNames) { + // First check whether the DD contains the meta variable and erase it, if this is the case. + if (!this->containsMetaVariable(metaVariableName)) { + throw storm::exceptions::InvalidArgumentException() << "Cannot abstract from meta variable that is not present in the DD."; + } + this->getContainedMetaVariableNames().erase(metaVariableName); + DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(metaVariableName); cubeDd *= metaVariable.getCube(); } @@ -140,6 +158,12 @@ namespace storm { Dd cubeDd(this->getDdManager()->getOne()); for (auto const& metaVariableName : metaVariableNames) { + // First check whether the DD contains the meta variable and erase it, if this is the case. + if (!this->containsMetaVariable(metaVariableName)) { + throw storm::exceptions::InvalidArgumentException() << "Cannot abstract from meta variable that is not present in the DD."; + } + this->getContainedMetaVariableNames().erase(metaVariableName); + DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(metaVariableName); cubeDd *= metaVariable.getCube(); } @@ -151,6 +175,12 @@ namespace storm { Dd cubeDd(this->getDdManager()->getOne()); for (auto const& metaVariableName : metaVariableNames) { + // First check whether the DD contains the meta variable and erase it, if this is the case. + if (!this->containsMetaVariable(metaVariableName)) { + throw storm::exceptions::InvalidArgumentException() << "Cannot abstract from meta variable that is not present in the DD."; + } + this->getContainedMetaVariableNames().erase(metaVariableName); + DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(metaVariableName); cubeDd *= metaVariable.getCube(); } @@ -158,6 +188,30 @@ namespace storm { this->getCuddAdd().Maximum(cubeDd.getCuddAdd()); } + uint_fast64_t Dd::getNonZeroCount() const { + std::size_t numberOfDdVariables = 0; + for (auto const& metaVariableName : this->containedMetaVariableNames) { + numberOfDdVariables += this->getDdManager()->getMetaVariable(metaVariableName).getNumberOfDdVariables(); + } + return static_cast(this->cuddAdd.CountMinterm(static_cast(numberOfDdVariables))); + } + + uint_fast64_t Dd::getLeafCount() const { + return static_cast(this->cuddAdd.CountLeaves()); + } + + double Dd::getMin() const { + ADD constantMinAdd = this->getCuddAdd().FindMin(); + // FIXME + return 0; + } + + double Dd::getMax() const { + ADD constantMaxAdd = this->getCuddAdd().FindMax(); + // FIXME + return 0; + } + void Dd::setValue(std::string const& metaVariableName, int_fast64_t variableValue, double targetValue) { std::unordered_map metaVariableNameToValueMap; metaVariableNameToValueMap.emplace(metaVariableName, variableValue); @@ -177,7 +231,15 @@ namespace storm { valueEncoding *= this->getDdManager()->getEncoding(nameValuePair.first, nameValuePair.second); } - this->cuddAdd = valueEncoding.getCuddAdd().Ite(this->getDdManager()->getConstant(targetValue).getCuddAdd(), this->cuddAdd); + this->getCuddAdd() = valueEncoding.getCuddAdd().Ite(this->getDdManager()->getConstant(targetValue).getCuddAdd(), this->cuddAdd); + } + + bool Dd::isOne() const { + return *this == this->getDdManager()->getOne(); + } + + bool Dd::isZero() const { + return *this == this->getDdManager()->getZero(); } bool Dd::containsMetaVariable(std::string const& metaVariableName) const { @@ -197,7 +259,11 @@ namespace storm { } std::unordered_set const& Dd::getContainedMetaVariableNames() const { - return containedMetaVariableNames; + return this->containedMetaVariableNames; + } + + std::unordered_set& Dd::getContainedMetaVariableNames() { + return this->containedMetaVariableNames; } void Dd::exportToDot(std::string const& filename) const { diff --git a/src/storage/dd/CuddDd.h b/src/storage/dd/CuddDd.h index 215e7e6a7..ffb82f400 100644 --- a/src/storage/dd/CuddDd.h +++ b/src/storage/dd/CuddDd.h @@ -3,6 +3,7 @@ #include #include +#include #include "src/storage/dd/Dd.h" @@ -27,6 +28,13 @@ namespace storm { Dd& operator=(Dd const& other) = default; Dd& operator=(Dd&& other) = default; + /*! + * Retrieves whether the two DDs represent the same function. + * + * @param other The DD that is to be compared with the current one. + */ + bool operator==(Dd const& other) const; + /*! * Adds the two DDs. * @@ -194,6 +202,34 @@ namespace storm { */ void maxAbstract(std::unordered_set const& metaVariableNames); + /*! + * Retrieves the number of encodings that are mapped to a non-zero value. + * + * @return The number of encodings that are mapped to a non-zero value. + */ + uint_fast64_t getNonZeroCount() const; + + /*! + * Retrieves the number of leaves of the DD. + * + * @return The number of leaves of the DD. + */ + uint_fast64_t getLeafCount() const; + + /*! + * Retrieves the lowest function value of any encoding. + * + * @return The lowest function value of any encoding. + */ + double getMin() const; + + /*! + * Retrieves the highest function value of any encoding. + * + * @return The highest function value of any encoding. + */ + double getMax() const; + /*! * Sets the function values of all encodings that have the given value of the meta variable to the given * target value. @@ -231,6 +267,20 @@ namespace storm { */ void setValue(std::unordered_map const& metaVariableNameToValueMap, double targetValue); + /*! + * Retrieves whether this DD represents the constant one function. + * + * @return True if this DD represents the constant one function. + */ + bool isOne() const; + + /*! + * Retrieves whether this DD represents the constant zero function. + * + * @return True if this DD represents the constant zero function. + */ + bool isZero() const; + /*! * Retrieves whether the given meta variable is contained in the DD. * @@ -254,6 +304,13 @@ namespace storm { */ std::unordered_set const& getContainedMetaVariableNames() const; + /*! + * Retrieves the set of all names of meta variables contained in the DD. + * + * @return The set of names of all meta variables contained in the DD. + */ + std::unordered_set& getContainedMetaVariableNames(); + /*! * Exports the DD to the given file in the dot format. * diff --git a/src/storage/dd/CuddDdManager.cpp b/src/storage/dd/CuddDdManager.cpp index 15f51a3b7..1c691522d 100644 --- a/src/storage/dd/CuddDdManager.cpp +++ b/src/storage/dd/CuddDdManager.cpp @@ -1,3 +1,5 @@ +#include + #include "src/storage/dd/CuddDdManager.h" #include "src/exceptions/InvalidArgumentException.h"