From 5bd6ca606f559bceb7c2a08d5c7ca5e454f54207 Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 27 Mar 2015 14:56:38 +0100 Subject: [PATCH] Started refactoring DD abstraction layer. Former-commit-id: 60f7713c24e23959bb93e01a898c369f02ee5215 --- src/storage/dd/Add.h | 14 + src/storage/dd/Bdd.h | 14 + src/storage/dd/CuddAdd.cpp | 1174 ++++++++++++++++++++++++++++++++++++ src/storage/dd/CuddAdd.h | 845 ++++++++++++++++++++++++++ src/storage/dd/CuddBdd.cpp | 321 ++++++++++ src/storage/dd/CuddBdd.h | 275 +++++++++ src/storage/dd/CuddDd.cpp | 1158 +---------------------------------- src/storage/dd/CuddDd.h | 731 +--------------------- 8 files changed, 2687 insertions(+), 1845 deletions(-) create mode 100644 src/storage/dd/Add.h create mode 100644 src/storage/dd/Bdd.h create mode 100644 src/storage/dd/CuddAdd.cpp create mode 100644 src/storage/dd/CuddAdd.h create mode 100644 src/storage/dd/CuddBdd.cpp create mode 100644 src/storage/dd/CuddBdd.h diff --git a/src/storage/dd/Add.h b/src/storage/dd/Add.h new file mode 100644 index 000000000..0c12fd586 --- /dev/null +++ b/src/storage/dd/Add.h @@ -0,0 +1,14 @@ +#ifndef STORM_STORAGE_DD_ADD_H_ +#define STORM_STORAGE_DD_ADD_H_ + +#include "src/storage/dd/Dd.h" +#include "src/storage/dd/DdType.h" + +namespace storm { + namespace dd { + // Declare Add class so we can then specialize it for the different ADD types. + template class Add; + } +} + +#endif /* STORM_STORAGE_DD_ADD_H_ */ \ No newline at end of file diff --git a/src/storage/dd/Bdd.h b/src/storage/dd/Bdd.h new file mode 100644 index 000000000..47c48474c --- /dev/null +++ b/src/storage/dd/Bdd.h @@ -0,0 +1,14 @@ +#ifndef STORM_STORAGE_DD_BDD_H_ +#define STORM_STORAGE_DD_BDD_H_ + +#include "src/storage/dd/Dd.h" +#include "src/storage/dd/DdType.h" + +namespace storm { + namespace dd { + // Declare Bdd class so we can then specialize it for the different BDD types. + template class Bdd; + } +} + +#endif /* STORM_STORAGE_DD_BDD_H_ */ \ No newline at end of file diff --git a/src/storage/dd/CuddAdd.cpp b/src/storage/dd/CuddAdd.cpp new file mode 100644 index 000000000..31476bc8e --- /dev/null +++ b/src/storage/dd/CuddAdd.cpp @@ -0,0 +1,1174 @@ +#include +#include + +#include "src/storage/dd/CuddDd.h" +#include "src/storage/dd/CuddOdd.h" +#include "src/storage/dd/CuddDdManager.h" +#include "src/utility/vector.h" +#include "src/utility/macros.h" + +#include "src/exceptions/IllegalFunctionCallException.h" +#include "src/exceptions/InvalidArgumentException.h" +#include "src/exceptions/NotImplementedException.h" + +namespace storm { + namespace dd { + Dd::Dd(std::shared_ptr const> ddManager, BDD cuddDd, std::set const& containedMetaVariables) : ddManager(ddManager), cuddDd(cuddDd), containedMetaVariables(containedMetaVariables) { + // Intentionally left empty. + } + + Dd::Dd(std::shared_ptr const> ddManager, ADD cuddDd, std::set const& containedMetaVariables) : ddManager(ddManager), cuddDd(cuddDd), containedMetaVariables(containedMetaVariables) { + // Intentionally left empty. + } + + bool Dd::isBdd() const { + return this->cuddDd.which() == 0; + } + + bool Dd::isMtbdd() const { + return this->cuddDd.which() == 1; + } + + Dd Dd::toBdd() const { + if (this->isBdd()) { + return *this; + } else { + return Dd(this->getDdManager(), this->getCuddMtbdd().BddPattern(), this->containedMetaVariables); + } + } + + Dd Dd::toMtbdd() const { + if (this->isMtbdd()) { + return *this; + } else { + return Dd(this->getDdManager(), this->getCuddBdd().Add(), this->containedMetaVariables); + } + } + + BDD Dd::getCuddBdd() const { + if (this->isBdd()) { + return boost::get(this->cuddDd); + } else { + STORM_LOG_WARN_COND(false, "Implicitly converting MTBDD to BDD."); + return this->getCuddMtbdd().BddPattern(); + } + } + + ADD Dd::getCuddMtbdd() const { + if (this->isMtbdd()) { + return boost::get(this->cuddDd); + } else { + STORM_LOG_WARN_COND(false, "Implicitly converting BDD to MTBDD."); + return this->getCuddBdd().Add(); + } + } + + ABDD const& Dd::getCuddDd() const { + if (this->isBdd()) { + return static_cast(boost::get(this->cuddDd)); + } else { + return static_cast(boost::get(this->cuddDd)); + } + } + + DdNode* Dd::getCuddDdNode() const { + if (this->isBdd()) { + return this->getCuddBdd().getNode(); + } else { + return this->getCuddMtbdd().getNode(); + } + } + + bool Dd::operator==(Dd const& other) const { + if (this->isBdd()) { + if (other.isBdd()) { + return this->getCuddBdd() == other.getCuddBdd(); + } else { + return false; + } + } else { + if (other.isMtbdd()) { + return this->getCuddMtbdd() == other.getCuddMtbdd(); + } else { + return false; + } + } + } + + bool Dd::operator!=(Dd const& other) const { + return !(*this == other); + } + + Dd Dd::ite(Dd const& thenDd, Dd const& elseDd) const { + std::set metaVariableNames(this->getContainedMetaVariables()); + metaVariableNames.insert(thenDd.getContainedMetaVariables().begin(), thenDd.getContainedMetaVariables().end()); + metaVariableNames.insert(elseDd.getContainedMetaVariables().begin(), elseDd.getContainedMetaVariables().end()); + + // If all involved DDs are BDDs, the result is also going to be a BDD. + if (this->isBdd() && thenDd.isBdd() && elseDd.isBdd()) { + return Dd(this->getDdManager(), this->getCuddBdd().Ite(thenDd.getCuddBdd(), elseDd.getCuddBdd()), metaVariableNames); + } else { + return Dd(this->getDdManager(), this->toMtbdd().getCuddMtbdd().Ite(thenDd.toMtbdd().getCuddMtbdd(), elseDd.toMtbdd().getCuddMtbdd()), metaVariableNames); + } + } + + Dd Dd::operator+(Dd const& other) const { + Dd result(*this); + result += other; + return result; + } + + Dd& Dd::operator+=(Dd const& other) { + STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing addition on BDDs."); + this->getContainedMetaVariables().insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end()); + this->cuddDd = this->getCuddMtbdd() + other.getCuddMtbdd(); + return *this; + } + + Dd Dd::operator*(Dd const& other) const { + Dd result(*this); + result *= other; + return result; + } + + Dd& Dd::operator*=(Dd const& other) { + this->getContainedMetaVariables().insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end()); + if (this->isMtbdd() && other.isMtbdd()) { + this->cuddDd = this->getCuddMtbdd() * other.getCuddMtbdd(); + } else if (this->isBdd() && other.isBdd()) { + this->cuddDd = this->getCuddBdd() & other.getCuddBdd(); + } else { + STORM_LOG_WARN_COND(false, "Performing multiplication on two DDs of different type."); + this->cuddDd = this->getCuddMtbdd() * other.getCuddMtbdd(); + } + return *this; + } + + Dd Dd::operator-(Dd const& other) const { + STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing arithmetical operation on BDD(s)."); + Dd result(*this); + result -= other; + return result; + } + + Dd Dd::operator-() const { + STORM_LOG_WARN_COND(this->isMtbdd(), "Performing arithmetical operation on BDD(s)."); + return this->getDdManager()->getZero(true) - *this; + } + + Dd& Dd::operator-=(Dd const& other) { + STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing arithmetical operation on BDD(s)."); + this->cuddDd = this->getCuddMtbdd() - other.getCuddMtbdd(); + this->getContainedMetaVariables().insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end()); + return *this; + } + + Dd Dd::operator/(Dd const& other) const { + STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing arithmetical operation on BDD(s)."); + Dd result(*this); + result /= other; + return result; + } + + Dd& Dd::operator/=(Dd const& other) { + STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing arithmetical operation on BDD(s)."); + this->cuddDd = this->getCuddMtbdd().Divide(other.getCuddMtbdd()); + this->getContainedMetaVariables().insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end()); + return *this; + } + + Dd Dd::operator!() const { + Dd result(*this); + result.complement(); + return result; + } + + Dd& Dd::complement() { + if (this->isBdd()) { + this->cuddDd = ~this->getCuddBdd(); + } else { + this->cuddDd = ~this->getCuddMtbdd(); + } + return *this; + } + + Dd Dd::operator&&(Dd const& other) const { + Dd result(*this); + result &= other; + return result; + } + + Dd& Dd::operator&=(Dd const& other) { + this->getContainedMetaVariables().insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end()); + if (this->isBdd() && other.isBdd()) { + this->cuddDd = this->getCuddBdd() & other.getCuddBdd(); + } else if (this->isMtbdd() && other.isMtbdd()) { + // We also tolerate (without a warning) if the two arguments are MTBDDs. The caller has to make sure that + // the two given DDs are 0-1-MTBDDs, because the operation may produce wrong results otherwise. + this->cuddDd = this->getCuddMtbdd() & other.getCuddMtbdd(); + } else { + STORM_LOG_WARN_COND(false, "Performing logical and on two DDs of different type."); + this->cuddDd = this->getCuddBdd() & other.getCuddBdd(); + } + return *this; + } + + Dd Dd::operator||(Dd const& other) const { + Dd result(*this); + result |= other; + return result; + } + + Dd& Dd::operator|=(Dd const& other) { + this->getContainedMetaVariables().insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end()); + if (this->isBdd() && other.isBdd()) { + this->cuddDd = this->getCuddBdd() | other.getCuddBdd(); + } else if (this->isMtbdd() && other.isMtbdd()) { + // We also tolerate (without a warning) if the two arguments are MTBDDs. The caller has to make sure that + // the two given DDs are 0-1-MTBDDs, because the operation may produce wrong results otherwise. + this->cuddDd = this->getCuddMtbdd() | other.getCuddMtbdd(); + } else { + STORM_LOG_WARN_COND(false, "Performing logical and on two DDs of different type."); + this->cuddDd = this->getCuddBdd() & other.getCuddBdd(); + } + return *this; + + STORM_LOG_WARN_COND(this->isBdd() && other.isBdd(), "Performing logical operation on MTBDD(s)."); + this->cuddDd = this->getCuddBdd() | other.getCuddBdd(); + this->getContainedMetaVariables().insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end()); + return *this; + } + + Dd Dd::iff(Dd const& other) const { + std::set metaVariables(this->getContainedMetaVariables()); + metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end()); + if (this->isBdd() && other.isBdd()) { + return Dd(this->getDdManager(), this->getCuddBdd().Xnor(other.getCuddBdd()), metaVariables); + } else if (this->isMtbdd() && other.isMtbdd()) { + // We also tolerate (without a warning) if the two arguments are MTBDDs. The caller has to make sure that + // the two given DDs are 0-1-MTBDDs, because the operation may produce wrong results otherwise. + return Dd(this->getDdManager(), this->getCuddMtbdd().Xnor(other.getCuddMtbdd()), metaVariables); + } else { + STORM_LOG_WARN_COND(false, "Performing logical iff on two DDs of different type."); + return Dd(this->getDdManager(), this->getCuddBdd().Xnor(other.getCuddBdd()), metaVariables); + } + } + + Dd Dd::exclusiveOr(Dd const& other) const { + std::set metaVariables(this->getContainedMetaVariables()); + metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end()); + if (this->isBdd() && other.isBdd()) { + return Dd(this->getDdManager(), this->getCuddBdd().Xor(other.getCuddBdd()), metaVariables); + } else if (this->isMtbdd() && other.isMtbdd()) { + // We also tolerate (without a warning) if the two arguments are MTBDDs. The caller has to make sure that + // the two given DDs are 0-1-MTBDDs, because the operation may produce wrong results otherwise. + return Dd(this->getDdManager(), this->getCuddMtbdd().Xor(other.getCuddMtbdd()), metaVariables); + } else { + STORM_LOG_WARN_COND(false, "Performing logical iff on two DDs of different type."); + return Dd(this->getDdManager(), this->getCuddBdd().Xor(other.getCuddBdd()), metaVariables); + } + } + + Dd Dd::implies(Dd const& other) const { + std::set metaVariables(this->getContainedMetaVariables()); + metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end()); + STORM_LOG_WARN_COND(this->isBdd() && other.isBdd(), "Performing logical operatiorn on MTBDDs."); + return Dd(this->getDdManager(), this->getCuddBdd().Ite(other.getCuddBdd(), this->getDdManager()->getOne().getCuddBdd()), metaVariables); + } + + Dd Dd::equals(Dd const& other) const { + STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing arithmetical operation on BDD(s)."); + std::set metaVariables(this->getContainedMetaVariables()); + metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end()); + return Dd(this->getDdManager(), this->getCuddMtbdd().Equals(other.getCuddMtbdd()), metaVariables); + } + + Dd Dd::notEquals(Dd const& other) const { + STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing arithmetical operation on BDD(s)."); + std::set metaVariables(this->getContainedMetaVariables()); + metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end()); + return Dd(this->getDdManager(), this->getCuddMtbdd().NotEquals(other.getCuddMtbdd()), metaVariables); + } + + Dd Dd::less(Dd const& other) const { + STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing arithmetical operation on BDD(s)."); + std::set metaVariables(this->getContainedMetaVariables()); + metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end()); + return Dd(this->getDdManager(), this->getCuddMtbdd().LessThan(other.getCuddMtbdd()), metaVariables); + } + + Dd Dd::lessOrEqual(Dd const& other) const { + STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing arithmetical operation on BDD(s)."); + std::set metaVariables(this->getContainedMetaVariables()); + metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end()); + return Dd(this->getDdManager(), this->getCuddMtbdd().LessThanOrEqual(other.getCuddMtbdd()), metaVariables); + } + + Dd Dd::greater(Dd const& other) const { + STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing arithmetical operation on BDD(s)."); + std::set metaVariables(this->getContainedMetaVariables()); + metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end()); + return Dd(this->getDdManager(), this->getCuddMtbdd().GreaterThan(other.getCuddMtbdd()), metaVariables); + } + + Dd Dd::greaterOrEqual(Dd const& other) const { + STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing arithmetical operation on BDD(s)."); + std::set metaVariables(this->getContainedMetaVariables()); + metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end()); + return Dd(this->getDdManager(), this->getCuddMtbdd().GreaterThanOrEqual(other.getCuddMtbdd()), metaVariables); + } + + Dd Dd::minimum(Dd const& other) const { + STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing arithmetical operation on BDD(s)."); + std::set metaVariables(this->getContainedMetaVariables()); + metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end()); + return Dd(this->getDdManager(), this->getCuddMtbdd().Minimum(other.getCuddMtbdd()), metaVariables); + } + + Dd Dd::maximum(Dd const& other) const { + STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing arithmetical operation on BDD(s)."); + std::set metaVariables(this->getContainedMetaVariables()); + metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end()); + return Dd(this->getDdManager(), this->getCuddMtbdd().Maximum(other.getCuddMtbdd()), metaVariables); + } + + Dd Dd::existsAbstract(std::set const& metaVariables) const { + STORM_LOG_WARN_COND(this->isBdd(), "Performing logical operation on MTBDD(s)."); + + Dd cubeDd(this->getDdManager()->getOne(false)); + std::set newMetaVariables = this->getContainedMetaVariables(); + for (auto const& metaVariable : metaVariables) { + // First check whether the DD contains the meta variable and erase it, if this is the case. + STORM_LOG_THROW(this->containsMetaVariable(metaVariable), storm::exceptions::InvalidArgumentException, "Cannot abstract from meta variable '" << metaVariable.getName() << "' that is not present in the DD."); + newMetaVariables.erase(metaVariable); + + DdMetaVariable const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable); + cubeDd &= ddMetaVariable.getCube(); + } + + return Dd(this->getDdManager(), this->getCuddBdd().ExistAbstract(cubeDd.getCuddBdd()), newMetaVariables); + } + + Dd Dd::universalAbstract(std::set const& metaVariables) const { + STORM_LOG_WARN_COND(this->isBdd(), "Performing logical operation on MTBDD(s)."); + + Dd cubeDd(this->getDdManager()->getOne()); + std::set newMetaVariables = this->getContainedMetaVariables(); + for (auto const& metaVariable : metaVariables) { + // First check whether the DD contains the meta variable and erase it, if this is the case. + STORM_LOG_THROW(this->containsMetaVariable(metaVariable), storm::exceptions::InvalidArgumentException, "Cannot abstract from meta variable '" << metaVariable.getName() << "' that is not present in the DD."); + newMetaVariables.erase(metaVariable); + + DdMetaVariable const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable); + cubeDd &= ddMetaVariable.getCube(); + } + + return Dd(this->getDdManager(), this->getCuddBdd().UnivAbstract(cubeDd.getCuddBdd()), newMetaVariables); + } + + Dd Dd::sumAbstract(std::set const& metaVariables) const { + STORM_LOG_WARN_COND(this->isMtbdd(), "Performing arithmetical operation on BDD(s)."); + + Dd cubeDd(this->getDdManager()->getOne(true)); + std::set newMetaVariables = this->getContainedMetaVariables(); + for (auto const& metaVariable : metaVariables) { + // First check whether the DD contains the meta variable and erase it, if this is the case. + STORM_LOG_THROW(this->containsMetaVariable(metaVariable), storm::exceptions::InvalidArgumentException, "Cannot abstract from meta variable '" << metaVariable.getName() << "' that is not present in the DD."); + newMetaVariables.erase(metaVariable); + + DdMetaVariable const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable); + cubeDd *= ddMetaVariable.getCubeAsMtbdd(); + } + + return Dd(this->getDdManager(), this->getCuddMtbdd().ExistAbstract(cubeDd.getCuddMtbdd()), newMetaVariables); + } + + Dd Dd::minAbstract(std::set const& metaVariables) const { + STORM_LOG_WARN_COND(this->isMtbdd(), "Performing arithmetical operation on BDD(s)."); + + Dd cubeDd(this->getDdManager()->getOne(true)); + std::set newMetaVariables = this->getContainedMetaVariables(); + for (auto const& metaVariable : metaVariables) { + // First check whether the DD contains the meta variable and erase it, if this is the case. + STORM_LOG_THROW(this->containsMetaVariable(metaVariable), storm::exceptions::InvalidArgumentException, "Cannot abstract from meta variable '" << metaVariable.getName() << "' that is not present in the DD."); + newMetaVariables.erase(metaVariable); + + DdMetaVariable const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable); + cubeDd *= ddMetaVariable.getCubeAsMtbdd(); + } + + return Dd(this->getDdManager(), this->getCuddMtbdd().MinAbstract(cubeDd.getCuddMtbdd()), newMetaVariables); + } + + Dd Dd::maxAbstract(std::set const& metaVariables) const { + STORM_LOG_WARN_COND(this->isMtbdd(), "Performing arithmetical operation on BDD(s)."); + + Dd cubeDd(this->getDdManager()->getOne(true)); + std::set newMetaVariables = this->getContainedMetaVariables(); + for (auto const& metaVariable : metaVariables) { + // First check whether the DD contains the meta variable and erase it, if this is the case. + STORM_LOG_THROW(this->containsMetaVariable(metaVariable), storm::exceptions::InvalidArgumentException, "Cannot abstract from meta variable '" << metaVariable.getName() << "' that is not present in the DD."); + newMetaVariables.erase(metaVariable); + + DdMetaVariable const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable); + cubeDd *= ddMetaVariable.getCubeAsMtbdd(); + } + + return Dd(this->getDdManager(), this->getCuddMtbdd().MaxAbstract(cubeDd.getCuddMtbdd()), newMetaVariables); + } + + bool Dd::equalModuloPrecision(Dd const& other, double precision, bool relative) const { + STORM_LOG_WARN_COND(this->isMtbdd(), "Performing arithmetical operation on BDD(s)."); + + if (relative) { + return this->getCuddMtbdd().EqualSupNormRel(other.getCuddMtbdd(), precision); + } else { + return this->getCuddMtbdd().EqualSupNorm(other.getCuddMtbdd(), precision); + } + } + + Dd Dd::swapVariables(std::vector> const& metaVariablePairs) { + std::set newContainedMetaVariables; + if (this->isBdd()) { + std::vector from; + std::vector to; + for (auto const& metaVariablePair : metaVariablePairs) { + DdMetaVariable const& variable1 = this->getDdManager()->getMetaVariable(metaVariablePair.first); + DdMetaVariable const& variable2 = this->getDdManager()->getMetaVariable(metaVariablePair.second); + + // Check if it's legal so swap the meta variables. + STORM_LOG_THROW(variable1.getNumberOfDdVariables() == variable2.getNumberOfDdVariables(), storm::exceptions::InvalidArgumentException, "Unable to swap meta variables with different size."); + + // Keep track of the contained meta variables in the DD. + if (this->containsMetaVariable(metaVariablePair.first)) { + newContainedMetaVariables.insert(metaVariablePair.second); + } + if (this->containsMetaVariable(metaVariablePair.second)) { + newContainedMetaVariables.insert(metaVariablePair.first); + } + + // Add the variables to swap to the corresponding vectors. + for (auto const& ddVariable : variable1.getDdVariables()) { + from.push_back(ddVariable.getCuddBdd()); + } + for (auto const& ddVariable : variable2.getDdVariables()) { + to.push_back(ddVariable.getCuddBdd()); + } + } + + // Finally, call CUDD to swap the variables. + return Dd(this->getDdManager(), this->getCuddBdd().SwapVariables(from, to), newContainedMetaVariables); + } else { + std::vector from; + std::vector to; + for (auto const& metaVariablePair : metaVariablePairs) { + DdMetaVariable const& variable1 = this->getDdManager()->getMetaVariable(metaVariablePair.first); + DdMetaVariable const& variable2 = this->getDdManager()->getMetaVariable(metaVariablePair.second); + + // Check if it's legal so swap the meta variables. + if (variable1.getNumberOfDdVariables() != variable2.getNumberOfDdVariables()) { + throw storm::exceptions::InvalidArgumentException() << "Unable to swap meta variables with different size."; + } + + // Keep track of the contained meta variables in the DD. + if (this->containsMetaVariable(metaVariablePair.first)) { + newContainedMetaVariables.insert(metaVariablePair.second); + } + if (this->containsMetaVariable(metaVariablePair.second)) { + newContainedMetaVariables.insert(metaVariablePair.first); + } + + // Add the variables to swap to the corresponding vectors. + for (auto const& ddVariable : variable1.getDdVariables()) { + from.push_back(ddVariable.getCuddMtbdd()); + } + for (auto const& ddVariable : variable2.getDdVariables()) { + to.push_back(ddVariable.getCuddMtbdd()); + } + } + + // Finally, call CUDD to swap the variables. + return Dd(this->getDdManager(), this->getCuddMtbdd().SwapVariables(from, to), newContainedMetaVariables); + } + } + + Dd Dd::multiplyMatrix(Dd const& otherMatrix, std::set const& summationMetaVariables) const { + STORM_LOG_WARN_COND(this->isMtbdd() && otherMatrix.isMtbdd(), "Performing arithmetical operation on BDD(s)."); + + // Create the CUDD summation variables. + std::vector summationDdVariables; + for (auto const& metaVariable : summationMetaVariables) { + for (auto const& ddVariable : this->getDdManager()->getMetaVariable(metaVariable).getDdVariables()) { + summationDdVariables.push_back(ddVariable.getCuddMtbdd()); + } + } + + std::set unionOfMetaVariables; + std::set_union(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end(), otherMatrix.getContainedMetaVariables().begin(), otherMatrix.getContainedMetaVariables().end(), std::inserter(unionOfMetaVariables, unionOfMetaVariables.begin())); + std::set containedMetaVariables; + std::set_difference(unionOfMetaVariables.begin(), unionOfMetaVariables.end(), summationMetaVariables.begin(), summationMetaVariables.end(), std::inserter(containedMetaVariables, containedMetaVariables.begin())); + + return Dd(this->getDdManager(), this->getCuddMtbdd().MatrixMultiply(otherMatrix.getCuddMtbdd(), summationDdVariables), containedMetaVariables); + } + + Dd Dd::andExists(Dd const& other, std::set const& existentialVariables) const { + STORM_LOG_WARN_COND(this->isBdd() && other.isBdd(), "Performing logical operation on MTBDD(s)."); + + Dd cubeDd(this->getDdManager()->getOne()); + for (auto const& metaVariable : existentialVariables) { + DdMetaVariable const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable); + cubeDd &= ddMetaVariable.getCube(); + } + + std::set unionOfMetaVariables; + std::set_union(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end(), other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end(), std::inserter(unionOfMetaVariables, unionOfMetaVariables.begin())); + std::set containedMetaVariables; + std::set_difference(unionOfMetaVariables.begin(), unionOfMetaVariables.end(), existentialVariables.begin(), existentialVariables.end(), std::inserter(containedMetaVariables, containedMetaVariables.begin())); + + return Dd(this->getDdManager(), this->getCuddBdd().AndAbstract(other.getCuddBdd(), cubeDd.getCuddBdd()), containedMetaVariables); + } + + Dd Dd::greater(double value) const { + STORM_LOG_WARN_COND(this->isMtbdd(), "Performing arithmetical operation on BDD(s)."); + return Dd(this->getDdManager(), this->getCuddMtbdd().BddStrictThreshold(value), this->getContainedMetaVariables()); + } + + Dd Dd::greaterOrEqual(double value) const { + STORM_LOG_WARN_COND(this->isMtbdd(), "Performing arithmetical operation on BDD(s)."); + return Dd(this->getDdManager(), this->getCuddMtbdd().BddThreshold(value), this->getContainedMetaVariables()); + } + + Dd Dd::notZero() const { + return this->toBdd(); + } + + Dd Dd::constrain(Dd const& constraint) const { + std::set metaVariables(this->getContainedMetaVariables()); + metaVariables.insert(constraint.getContainedMetaVariables().begin(), constraint.getContainedMetaVariables().end()); + + if (this->isBdd() && constraint.isBdd()) { + return Dd(this->getDdManager(), this->getCuddBdd().Constrain(constraint.getCuddBdd()), metaVariables); + } else { + return Dd(this->getDdManager(), this->getCuddMtbdd().Constrain(constraint.getCuddMtbdd()), metaVariables); + } + } + + Dd Dd::restrict(Dd const& constraint) const { + std::set metaVariables(this->getContainedMetaVariables()); + metaVariables.insert(constraint.getContainedMetaVariables().begin(), constraint.getContainedMetaVariables().end()); + + if (this->isBdd() && constraint.isBdd()) { + return Dd(this->getDdManager(), this->getCuddBdd().Restrict(constraint.getCuddBdd()), metaVariables); + } else { + return Dd(this->getDdManager(), this->getCuddMtbdd().Restrict(constraint.getCuddMtbdd()), metaVariables); + } + } + + Dd Dd::getSupport() const { + if (this->isBdd()) { + return Dd(this->getDdManager(), this->getCuddBdd().Support(), this->getContainedMetaVariables()); + } else { + return Dd(this->getDdManager(), this->getCuddMtbdd().Support(), this->getContainedMetaVariables()); + } + } + + uint_fast64_t Dd::getNonZeroCount() const { + std::size_t numberOfDdVariables = 0; + for (auto const& metaVariable : this->getContainedMetaVariables()) { + numberOfDdVariables += this->getDdManager()->getMetaVariable(metaVariable).getNumberOfDdVariables(); + } + if (this->isBdd()) { + return static_cast(this->getCuddBdd().CountMinterm(static_cast(numberOfDdVariables))); + } else { + return static_cast(this->getCuddMtbdd().CountMinterm(static_cast(numberOfDdVariables))); + } + } + + uint_fast64_t Dd::getLeafCount() const { + if (this->isBdd()) { + return static_cast(this->getCuddBdd().CountLeaves()); + } else { + return static_cast(this->getCuddMtbdd().CountLeaves()); + } + } + + uint_fast64_t Dd::getNodeCount() const { + if (this->isBdd()) { + return static_cast(this->getCuddBdd().nodeCount()); + } else { + return static_cast(this->getCuddMtbdd().nodeCount()); + } + } + + double Dd::getMin() const { + STORM_LOG_WARN_COND(this->isMtbdd(), "Performing arithmetical operation on BDD(s)."); + + ADD constantMinAdd = this->getCuddMtbdd().FindMin(); + return static_cast(Cudd_V(constantMinAdd.getNode())); + } + + double Dd::getMax() const { + STORM_LOG_WARN_COND(this->isMtbdd(), "Performing arithmetical operation on BDD(s)."); + + ADD constantMaxAdd = this->getCuddMtbdd().FindMax(); + return static_cast(Cudd_V(constantMaxAdd.getNode())); + } + + void Dd::setValue(storm::expressions::Variable const& metaVariable, int_fast64_t variableValue, double targetValue) { + std::map metaVariableToValueMap; + metaVariableToValueMap.emplace(metaVariable, variableValue); + this->setValue(metaVariableToValueMap, targetValue); + } + + void Dd::setValue(storm::expressions::Variable const& metaVariable1, int_fast64_t variableValue1, storm::expressions::Variable const& metaVariable2, int_fast64_t variableValue2, double targetValue) { + std::map metaVariableToValueMap; + metaVariableToValueMap.emplace(metaVariable1, variableValue1); + metaVariableToValueMap.emplace(metaVariable2, variableValue2); + this->setValue(metaVariableToValueMap, targetValue); + } + + void Dd::setValue(std::map const& metaVariableToValueMap, double targetValue) { + if (this->isBdd()) { + STORM_LOG_THROW(targetValue == storm::utility::zero() || targetValue == storm::utility::one(), storm::exceptions::InvalidArgumentException, "Cannot set encoding to non-0, non-1 value " << targetValue << " in BDD."); + Dd valueEncoding(this->getDdManager()->getOne()); + for (auto const& nameValuePair : metaVariableToValueMap) { + valueEncoding &= this->getDdManager()->getEncoding(nameValuePair.first, nameValuePair.second); + // Also record that the DD now contains the meta variable. + this->addContainedMetaVariable(nameValuePair.first); + } + if (targetValue == storm::utility::one()) { + this->cuddDd = valueEncoding.getCuddBdd().Ite(this->getDdManager()->getOne().getCuddBdd(), this->getCuddBdd()); + } else { + this->cuddDd = valueEncoding.getCuddBdd().Ite(this->getDdManager()->getZero().getCuddBdd(), this->getCuddBdd()); + } + } else { + Dd valueEncoding(this->getDdManager()->getOne()); + for (auto const& nameValuePair : metaVariableToValueMap) { + valueEncoding &= this->getDdManager()->getEncoding(nameValuePair.first, nameValuePair.second); + // Also record that the DD now contains the meta variable. + this->addContainedMetaVariable(nameValuePair.first); + } + + this->cuddDd = valueEncoding.toMtbdd().getCuddMtbdd().Ite(this->getDdManager()->getConstant(targetValue).getCuddMtbdd(), this->getCuddMtbdd()); + } + } + + double Dd::getValue(std::map const& metaVariableToValueMap) const { + std::set remainingMetaVariables(this->getContainedMetaVariables()); + Dd valueEncoding(this->getDdManager()->getOne()); + for (auto const& nameValuePair : metaVariableToValueMap) { + valueEncoding &= this->getDdManager()->getEncoding(nameValuePair.first, nameValuePair.second); + if (this->containsMetaVariable(nameValuePair.first)) { + remainingMetaVariables.erase(nameValuePair.first); + } + } + + STORM_LOG_THROW(remainingMetaVariables.empty(), storm::exceptions::InvalidArgumentException, "Cannot evaluate function for which not all inputs were given."); + + if (this->isBdd()) { + Dd value = *this && valueEncoding; + return value.isZero() ? 0 : 1; + } else { + Dd value = *this * valueEncoding.toMtbdd(); + value = value.sumAbstract(this->getContainedMetaVariables()); + return static_cast(Cudd_V(value.getCuddMtbdd().getNode())); + } + } + + bool Dd::isOne() const { + if (this->isBdd()) { + return this->getCuddBdd().IsOne(); + } else { + return this->getCuddMtbdd().IsOne(); + } + } + + bool Dd::isZero() const { + if (this->isBdd()) { + return this->getCuddBdd().IsZero(); + } else { + return this->getCuddMtbdd().IsZero(); + } + } + + bool Dd::isConstant() const { + if (this->isBdd()) { + return Cudd_IsConstant(this->getCuddBdd().getNode()); + } else { + return Cudd_IsConstant(this->getCuddMtbdd().getNode()); + } + } + + uint_fast64_t Dd::getIndex() const { + if (this->isBdd()) { + return static_cast(this->getCuddBdd().NodeReadIndex()); + } else { + return static_cast(this->getCuddMtbdd().NodeReadIndex()); + } + } + + template + std::vector Dd::toVector() const { + STORM_LOG_THROW(this->isMtbdd(), storm::exceptions::IllegalFunctionCallException, "Cannot create vector from BDD."); + return this->toVector(Odd(*this)); + } + + template + std::vector Dd::toVector(Odd const& rowOdd) const { + STORM_LOG_THROW(this->isMtbdd(), storm::exceptions::IllegalFunctionCallException, "Cannot create vector from BDD."); + std::vector result(rowOdd.getTotalOffset()); + std::vector ddVariableIndices = this->getSortedVariableIndices(); + addToVectorRec(this->getCuddDdNode(), 0, ddVariableIndices.size(), 0, rowOdd, ddVariableIndices, result); + return result; + } + + storm::storage::SparseMatrix Dd::toMatrix() const { + STORM_LOG_THROW(this->isMtbdd(), storm::exceptions::IllegalFunctionCallException, "Cannot create matrix from BDD."); + std::set rowVariables; + std::set columnVariables; + + for (auto const& variable : this->getContainedMetaVariables()) { + if (variable.getName().size() > 0 && variable.getName().back() == '\'') { + columnVariables.insert(variable); + } else { + rowVariables.insert(variable); + } + } + + return toMatrix(rowVariables, columnVariables, Odd(this->existsAbstract(rowVariables)), Odd(this->existsAbstract(columnVariables))); + } + + storm::storage::SparseMatrix Dd::toMatrix(storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const { + STORM_LOG_THROW(this->isMtbdd(), storm::exceptions::IllegalFunctionCallException, "Cannot create matrix from BDD."); + std::set rowMetaVariables; + std::set columnMetaVariables; + + for (auto const& variable : this->getContainedMetaVariables()) { + if (variable.getName().size() > 0 && variable.getName().back() == '\'') { + columnMetaVariables.insert(variable); + } else { + rowMetaVariables.insert(variable); + } + } + + return toMatrix(rowMetaVariables, columnMetaVariables, rowOdd, columnOdd); + } + + storm::storage::SparseMatrix Dd::toMatrix(std::set const& rowMetaVariables, std::set const& columnMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const { + STORM_LOG_THROW(this->isMtbdd(), storm::exceptions::IllegalFunctionCallException, "Cannot create matrix from BDD."); + std::vector ddRowVariableIndices; + std::vector ddColumnVariableIndices; + + for (auto const& variable : rowMetaVariables) { + DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(variable); + for (auto const& ddVariable : metaVariable.getDdVariables()) { + ddRowVariableIndices.push_back(ddVariable.getIndex()); + } + } + for (auto const& variable : columnMetaVariables) { + DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(variable); + for (auto const& ddVariable : metaVariable.getDdVariables()) { + ddColumnVariableIndices.push_back(ddVariable.getIndex()); + } + } + + // Prepare the vectors that represent the matrix. + std::vector rowIndications(rowOdd.getTotalOffset() + 1); + std::vector> columnsAndValues(this->getNonZeroCount()); + + // Create a trivial row grouping. + std::vector trivialRowGroupIndices(rowIndications.size()); + uint_fast64_t i = 0; + for (auto& entry : trivialRowGroupIndices) { + entry = i; + ++i; + } + + // Use the toMatrixRec function to compute the number of elements in each row. Using the flag, we prevent + // it from actually generating the entries in the entry vector. + toMatrixRec(this->getCuddDdNode(), rowIndications, columnsAndValues, trivialRowGroupIndices, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices, false); + + // TODO: counting might be faster by just summing over the primed variables and then using the ODD to convert + // the resulting (DD) vector to an explicit vector. + + // Now that we computed the number of entries in each row, compute the corresponding offsets in the entry vector. + uint_fast64_t tmp = 0; + uint_fast64_t tmp2 = 0; + for (uint_fast64_t i = 1; i < rowIndications.size(); ++i) { + tmp2 = rowIndications[i]; + rowIndications[i] = rowIndications[i - 1] + tmp; + std::swap(tmp, tmp2); + } + rowIndications[0] = 0; + + // Now actually fill the entry vector. + toMatrixRec(this->getCuddDdNode(), rowIndications, columnsAndValues, trivialRowGroupIndices, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices, true); + + // Since the last call to toMatrixRec modified the rowIndications, we need to restore the correct values. + for (uint_fast64_t i = rowIndications.size() - 1; i > 0; --i) { + rowIndications[i] = rowIndications[i - 1]; + } + rowIndications[0] = 0; + + // Construct matrix and return result. + return storm::storage::SparseMatrix(columnOdd.getTotalOffset(), std::move(rowIndications), std::move(columnsAndValues), std::move(trivialRowGroupIndices)); + } + + storm::storage::SparseMatrix Dd::toMatrix(std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const { + STORM_LOG_THROW(this->isMtbdd(), storm::exceptions::IllegalFunctionCallException, "Cannot create matrix from BDD."); + std::vector ddRowVariableIndices; + std::vector ddColumnVariableIndices; + std::vector ddGroupVariableIndices; + std::set rowAndColumnMetaVariables; + + for (auto const& variable : rowMetaVariables) { + DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(variable); + for (auto const& ddVariable : metaVariable.getDdVariables()) { + ddRowVariableIndices.push_back(ddVariable.getIndex()); + } + rowAndColumnMetaVariables.insert(variable); + } + for (auto const& variable : columnMetaVariables) { + DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(variable); + for (auto const& ddVariable : metaVariable.getDdVariables()) { + ddColumnVariableIndices.push_back(ddVariable.getIndex()); + } + rowAndColumnMetaVariables.insert(variable); + } + for (auto const& variable : groupMetaVariables) { + DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(variable); + for (auto const& ddVariable : metaVariable.getDdVariables()) { + ddGroupVariableIndices.push_back(ddVariable.getIndex()); + } + } + + // TODO: assert that the group variables are at the very top of the variable ordering? + + // Start by computing the offsets (in terms of rows) for each row group. + Dd stateToNumberOfChoices = this->notZero().existsAbstract(columnMetaVariables).sumAbstract(groupMetaVariables); + std::vector rowGroupIndices = stateToNumberOfChoices.toVector(rowOdd); + rowGroupIndices.resize(rowGroupIndices.size() + 1); + uint_fast64_t tmp = 0; + uint_fast64_t tmp2 = 0; + for (uint_fast64_t i = 1; i < rowGroupIndices.size(); ++i) { + tmp2 = rowGroupIndices[i]; + rowGroupIndices[i] = rowGroupIndices[i - 1] + tmp; + std::swap(tmp, tmp2); + } + rowGroupIndices[0] = 0; + + // Next, we split the matrix into one for each group. This only works if the group variables are at the very + // top. + std::vector> groups; + splitGroupsRec(this->getCuddDdNode(), groups, ddGroupVariableIndices, 0, ddGroupVariableIndices.size(), rowAndColumnMetaVariables); + + // Create the actual storage for the non-zero entries. + std::vector> columnsAndValues(this->getNonZeroCount()); + + // Now compute the indices at which the individual rows start. + std::vector rowIndications(rowGroupIndices.back() + 1); + std::vector> statesWithGroupEnabled(groups.size()); + for (uint_fast64_t i = 0; i < groups.size(); ++i) { + auto const& dd = groups[i]; + + toMatrixRec(dd.getCuddDdNode(), rowIndications, columnsAndValues, rowGroupIndices, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices, false); + + statesWithGroupEnabled[i] = dd.notZero().existsAbstract(columnMetaVariables); + addToVectorRec(statesWithGroupEnabled[i].getCuddDdNode(), 0, ddRowVariableIndices.size(), 0, rowOdd, ddRowVariableIndices, rowGroupIndices); + } + + // Since we modified the rowGroupIndices, we need to restore the correct values. + for (uint_fast64_t i = rowGroupIndices.size() - 1; i > 0; --i) { + rowGroupIndices[i] = rowGroupIndices[i - 1]; + } + rowGroupIndices[0] = 0; + + // Now that we computed the number of entries in each row, compute the corresponding offsets in the entry vector. + tmp = 0; + tmp2 = 0; + for (uint_fast64_t i = 1; i < rowIndications.size(); ++i) { + tmp2 = rowIndications[i]; + rowIndications[i] = rowIndications[i - 1] + tmp; + std::swap(tmp, tmp2); + } + rowIndications[0] = 0; + + // Now actually fill the entry vector. + for (uint_fast64_t i = 0; i < groups.size(); ++i) { + auto const& dd = groups[i]; + + toMatrixRec(dd.getCuddDdNode(), rowIndications, columnsAndValues, rowGroupIndices, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices, true); + + addToVectorRec(statesWithGroupEnabled[i].getCuddDdNode(), 0, ddRowVariableIndices.size(), 0, rowOdd, ddRowVariableIndices, rowGroupIndices); + } + + // Since we modified the rowGroupIndices, we need to restore the correct values. + for (uint_fast64_t i = rowGroupIndices.size() - 1; i > 0; --i) { + rowGroupIndices[i] = rowGroupIndices[i - 1]; + } + rowGroupIndices[0] = 0; + + // Since the last call to toMatrixRec modified the rowIndications, we need to restore the correct values. + for (uint_fast64_t i = rowIndications.size() - 1; i > 0; --i) { + rowIndications[i] = rowIndications[i - 1]; + } + rowIndications[0] = 0; + + return storm::storage::SparseMatrix(columnOdd.getTotalOffset(), std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices)); + } + + void Dd::toMatrixRec(DdNode const* dd, std::vector& rowIndications, std::vector>& columnsAndValues, std::vector const& rowGroupOffsets, Odd const& rowOdd, Odd const& columnOdd, uint_fast64_t currentRowLevel, uint_fast64_t currentColumnLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, uint_fast64_t currentColumnOffset, std::vector const& ddRowVariableIndices, std::vector const& ddColumnVariableIndices, bool generateValues) const { + // For the empty DD, we do not need to add any entries. + if (dd == Cudd_ReadZero(this->getDdManager()->getCuddManager().getManager())) { + return; + } + + // If we are at the maximal level, the value to be set is stored as a constant in the DD. + if (currentRowLevel + currentColumnLevel == maxLevel) { + if (generateValues) { + columnsAndValues[rowIndications[rowGroupOffsets[currentRowOffset]]] = storm::storage::MatrixEntry(currentColumnOffset, Cudd_V(dd)); + } + ++rowIndications[rowGroupOffsets[currentRowOffset]]; + } else { + DdNode const* elseElse; + DdNode const* elseThen; + DdNode const* thenElse; + DdNode const* thenThen; + + if (ddColumnVariableIndices[currentColumnLevel] < dd->index) { + elseElse = elseThen = thenElse = thenThen = dd; + } else if (ddRowVariableIndices[currentColumnLevel] < dd->index) { + elseElse = thenElse = Cudd_E(dd); + elseThen = thenThen = Cudd_T(dd); + } else { + DdNode const* elseNode = Cudd_E(dd); + if (ddColumnVariableIndices[currentColumnLevel] < elseNode->index) { + elseElse = elseThen = elseNode; + } else { + elseElse = Cudd_E(elseNode); + elseThen = Cudd_T(elseNode); + } + + DdNode const* thenNode = Cudd_T(dd); + if (ddColumnVariableIndices[currentColumnLevel] < thenNode->index) { + thenElse = thenThen = thenNode; + } else { + thenElse = Cudd_E(thenNode); + thenThen = Cudd_T(thenNode); + } + } + + // Visit else-else. + toMatrixRec(elseElse, rowIndications, columnsAndValues, rowGroupOffsets, rowOdd.getElseSuccessor(), columnOdd.getElseSuccessor(), currentRowLevel + 1, currentColumnLevel + 1, maxLevel, currentRowOffset, currentColumnOffset, ddRowVariableIndices, ddColumnVariableIndices, generateValues); + // Visit else-then. + toMatrixRec(elseThen, rowIndications, columnsAndValues, rowGroupOffsets, rowOdd.getElseSuccessor(), columnOdd.getThenSuccessor(), currentRowLevel + 1, currentColumnLevel + 1, maxLevel, currentRowOffset, currentColumnOffset + columnOdd.getElseOffset(), ddRowVariableIndices, ddColumnVariableIndices, generateValues); + // Visit then-else. + toMatrixRec(thenElse, rowIndications, columnsAndValues, rowGroupOffsets, rowOdd.getThenSuccessor(), columnOdd.getElseSuccessor(), currentRowLevel + 1, currentColumnLevel + 1, maxLevel, currentRowOffset + rowOdd.getElseOffset(), currentColumnOffset, ddRowVariableIndices, ddColumnVariableIndices, generateValues); + // Visit then-then. + toMatrixRec(thenThen, rowIndications, columnsAndValues, rowGroupOffsets, rowOdd.getThenSuccessor(), columnOdd.getThenSuccessor(), currentRowLevel + 1, currentColumnLevel + 1, maxLevel, currentRowOffset + rowOdd.getElseOffset(), currentColumnOffset + columnOdd.getElseOffset(), ddRowVariableIndices, ddColumnVariableIndices, generateValues); + } + } + + void Dd::splitGroupsRec(DdNode* dd, std::vector>& groups, std::vector const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::set const& remainingMetaVariables) const { + // For the empty DD, we do not need to create a group. + if (dd == Cudd_ReadZero(this->getDdManager()->getCuddManager().getManager())) { + return; + } + + if (currentLevel == maxLevel) { + groups.push_back(Dd(this->getDdManager(), ADD(this->getDdManager()->getCuddManager(), dd), remainingMetaVariables)); + } else if (ddGroupVariableIndices[currentLevel] < dd->index) { + splitGroupsRec(dd, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel, remainingMetaVariables); + splitGroupsRec(dd, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel, remainingMetaVariables); + } else { + splitGroupsRec(Cudd_E(dd), groups, ddGroupVariableIndices, currentLevel + 1, maxLevel, remainingMetaVariables); + splitGroupsRec(Cudd_T(dd), groups, ddGroupVariableIndices, currentLevel + 1, maxLevel, remainingMetaVariables); + } + } + + template + void Dd::addToVectorRec(DdNode const* dd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector) const { + // For the empty DD, we do not need to add any entries. + if (dd == Cudd_ReadZero(this->getDdManager()->getCuddManager().getManager())) { + return; + } + + // If we are at the maximal level, the value to be set is stored as a constant in the DD. + if (currentLevel == maxLevel) { + targetVector[currentOffset] += static_cast(Cudd_V(dd)); + } else if (ddVariableIndices[currentLevel] < dd->index) { + // If we skipped a level, we need to enumerate the explicit entries for the case in which the bit is set + // and for the one in which it is not set. + addToVectorRec(dd, currentLevel + 1, maxLevel, currentOffset, odd.getElseSuccessor(), ddVariableIndices, targetVector); + addToVectorRec(dd, currentLevel + 1, maxLevel, currentOffset + odd.getElseOffset(), odd.getThenSuccessor(), ddVariableIndices, targetVector); + } else { + // Otherwise, we simply recursively call the function for both (different) cases. + addToVectorRec(Cudd_E(dd), currentLevel + 1, maxLevel, currentOffset, odd.getElseSuccessor(), ddVariableIndices, targetVector); + addToVectorRec(Cudd_T(dd), currentLevel + 1, maxLevel, currentOffset + odd.getElseOffset(), odd.getThenSuccessor(), ddVariableIndices, targetVector); + } + } + + std::vector Dd::getSortedVariableIndices() const { + std::vector ddVariableIndices; + for (auto const& metaVariableName : this->getContainedMetaVariables()) { + auto const& metaVariable = this->getDdManager()->getMetaVariable(metaVariableName); + for (auto const& ddVariable : metaVariable.getDdVariables()) { + ddVariableIndices.push_back(ddVariable.getIndex()); + } + } + + // Next, we need to sort them, since they may be arbitrarily ordered otherwise. + std::sort(ddVariableIndices.begin(), ddVariableIndices.end()); + return ddVariableIndices; + } + + bool Dd::containsMetaVariable(storm::expressions::Variable const& metaVariable) const { + return containedMetaVariables.find(metaVariable) != containedMetaVariables.end(); + } + + bool Dd::containsMetaVariables(std::set const& metaVariables) const { + for (auto const& metaVariable : metaVariables) { + auto const& ddMetaVariable = containedMetaVariables.find(metaVariable); + + if (ddMetaVariable == containedMetaVariables.end()) { + return false; + } + } + return true; + } + + std::set const& Dd::getContainedMetaVariables() const { + return this->containedMetaVariables; + } + + std::set& Dd::getContainedMetaVariables() { + return this->containedMetaVariables; + } + + void Dd::exportToDot(std::string const& filename) const { + if (filename.empty()) { + if (this->isBdd()) { + std::vector cuddBddVector = { this->getCuddBdd() }; + this->getDdManager()->getCuddManager().DumpDot(cuddBddVector); + } else { + std::vector cuddAddVector = { this->getCuddMtbdd() }; + this->getDdManager()->getCuddManager().DumpDot(cuddAddVector); + } + } else { + // Build the name input of the DD. + std::vector ddNames; + std::string ddName("f"); + ddNames.push_back(new char[ddName.size() + 1]); + std::copy(ddName.c_str(), ddName.c_str() + 2, ddNames.back()); + + // Now build the variables names. + std::vector ddVariableNamesAsStrings = this->getDdManager()->getDdVariableNames(); + std::vector ddVariableNames; + for (auto const& element : ddVariableNamesAsStrings) { + ddVariableNames.push_back(new char[element.size() + 1]); + std::copy(element.c_str(), element.c_str() + element.size() + 1, ddVariableNames.back()); + } + + // Open the file, dump the DD and close it again. + FILE* filePointer = fopen(filename.c_str() , "w"); + if (this->isBdd()) { + std::vector cuddBddVector = { this->getCuddBdd() }; + this->getDdManager()->getCuddManager().DumpDot(cuddBddVector, &ddVariableNames[0], &ddNames[0], filePointer); + } else { + std::vector cuddAddVector = { this->getCuddMtbdd() }; + this->getDdManager()->getCuddManager().DumpDot(cuddAddVector, &ddVariableNames[0], &ddNames[0], filePointer); + } + fclose(filePointer); + + // Finally, delete the names. + for (char* element : ddNames) { + delete element; + } + for (char* element : ddVariableNames) { + delete element; + } + } + } + + void Dd::addContainedMetaVariable(storm::expressions::Variable const& metaVariable) { + this->getContainedMetaVariables().insert(metaVariable); + } + + void Dd::removeContainedMetaVariable(storm::expressions::Variable const& metaVariable) { + this->getContainedMetaVariables().erase(metaVariable); + } + + std::shared_ptr const> Dd::getDdManager() const { + return this->ddManager; + } + + DdForwardIterator Dd::begin(bool enumerateDontCareMetaVariables) const { + int* cube; + double value; + DdGen* generator = this->getCuddDd().FirstCube(&cube, &value); + return DdForwardIterator(this->getDdManager(), generator, cube, value, (Cudd_IsGenEmpty(generator) != 0), &this->getContainedMetaVariables(), enumerateDontCareMetaVariables); + } + + DdForwardIterator Dd::end(bool enumerateDontCareMetaVariables) const { + return DdForwardIterator(this->getDdManager(), nullptr, nullptr, 0, true, nullptr, enumerateDontCareMetaVariables); + } + + storm::expressions::Expression Dd::toExpression() const { + return toExpressionRecur(this->getCuddDdNode(), this->getDdManager()->getDdVariables()); + } + + storm::expressions::Expression Dd::getMintermExpression() const { + // Note that we first transform the ADD into a BDD to convert all non-zero terminals to ones and therefore + // make the DD more compact. + return getMintermExpressionRecur(this->getDdManager()->getCuddManager().getManager(), this->toBdd().getCuddDdNode(), this->getDdManager()->getDdVariables()); + } + + storm::expressions::Expression Dd::toExpressionRecur(DdNode const* dd, std::vector const& variables) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This feature is currently unavailable."); + // If the DD is a terminal node, we can simply return a constant expression. + // if (Cudd_IsConstant(dd)) { + // return storm::expressions::Expression::createDoubleLiteral(static_cast(Cudd_V(dd))); + // } else { + // return storm::expressions::Expression::createBooleanVariable(variableNames[dd->index]).ite(toExpressionRecur(Cudd_T(dd), variableNames), toExpressionRecur(Cudd_E(dd), variableNames)); + // } + } + + storm::expressions::Expression Dd::getMintermExpressionRecur(::DdManager* manager, DdNode const* dd, std::vector const& variables) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This feature is currently unavailable."); + // If the DD is a terminal node, we can simply return a constant expression. + // if (Cudd_IsConstant(dd)) { + // if (Cudd_IsComplement(dd)) { + // return storm::expressions::Expression::createBooleanLiteral(false); + // } else { + // return storm::expressions::Expression::createBooleanLiteral((dd == Cudd_ReadOne(manager)) ? true : false); + // } + // } else { + // // Get regular versions of the pointers. + // DdNode* regularDd = Cudd_Regular(dd); + // DdNode* thenDd = Cudd_T(regularDd); + // DdNode* elseDd = Cudd_E(regularDd); + // + // // Compute expression recursively. + // storm::expressions::Expression result = storm::expressions::Expression::createBooleanVariable(variableNames[dd->index]).ite(getMintermExpressionRecur(manager, thenDd, variableNames), getMintermExpressionRecur(manager, elseDd, variableNames)); + // if (Cudd_IsComplement(dd)) { + // result = !result; + // } + // + // return result; + // } + } + + std::ostream& operator<<(std::ostream& out, const Dd& dd) { + dd.exportToDot(); + return out; + } + + // Explicitly instantiate some templated functions. + template std::vector Dd::toVector() const; + template std::vector Dd::toVector(Odd const& rowOdd) const; + template void Dd::addToVectorRec(DdNode const* dd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector) const; + template std::vector Dd::toVector() const; + template std::vector Dd::toVector(Odd const& rowOdd) const; + template void Dd::addToVectorRec(DdNode const* dd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector) const; + } +} \ No newline at end of file diff --git a/src/storage/dd/CuddAdd.h b/src/storage/dd/CuddAdd.h new file mode 100644 index 000000000..f860e79bf --- /dev/null +++ b/src/storage/dd/CuddAdd.h @@ -0,0 +1,845 @@ +#ifndef STORM_STORAGE_DD_CUDDDD_H_ +#define STORM_STORAGE_DD_CUDDDD_H_ + +#include +#include +#include +#include +#include + +#include "src/storage/dd/Dd.h" +#include "src/storage/dd/CuddDdForwardIterator.h" +#include "src/storage/SparseMatrix.h" +#include "src/storage/expressions/Expression.h" +#include "src/storage/expressions/Variable.h" +#include "src/utility/OsDetection.h" + +// Include the C++-interface of CUDD. +#include "cuddObj.hh" + +namespace storm { + namespace dd { + // Forward-declare some classes. + template class DdManager; + template class Odd; + + template<> + class Dd { + public: + // Declare the DdManager and DdIterator class as friend so it can access the internals of a DD. + friend class DdManager; + friend class DdForwardIterator; + friend class Odd; + + // Instantiate all copy/move constructors/assignments with the default implementation. + Dd() = default; + Dd(Dd const& other) = default; + Dd& operator=(Dd const& other) = default; +#ifndef WINDOWS + Dd(Dd&& other) = default; + Dd& operator=(Dd&& other) = default; +#endif + + /*! + * Retrieves whether the two DDs represent the same function. + * + * @param other The DD that is to be compared with the current one. + * @return True if the DDs represent the same function. + */ + bool operator==(Dd const& other) const; + + /*! + * Retrieves whether the two DDs represent different functions. + * + * @param other The DD that is to be compared with the current one. + * @return True if the DDs represent the different functions. + */ + bool operator!=(Dd const& other) const; + + /*! + * Performs an if-then-else with the given operands, i.e. maps all valuations that are mapped to a non-zero + * function value to the function values specified by the first DD and all others to the function values + * specified by the second DD. + */ + Dd ite(Dd const& thenDd, Dd const& elseDd) const; + + /*! + * Performs a logical or of the current and the given DD. + * + * @param other The second DD used for the operation. + * @return The logical or of the operands. + */ + Dd operator||(Dd const& other) const; + + /*! + * Performs a logical or of the current and the given DD and assigns it to the current DD. + * + * @param other The second DD used for the operation. + * @return A reference to the current DD after the operation + */ + Dd& operator|=(Dd const& other); + + /*! + * Performs a logical and of the current and the given DD. + * + * @param other The second DD used for the operation. + * @return The logical and of the operands. + */ + Dd operator&&(Dd const& other) const; + + /*! + * Performs a logical and of the current and the given DD and assigns it to the current DD. + * + * @param other The second DD used for the operation. + * @return A reference to the current DD after the operation + */ + Dd& operator&=(Dd const& other); + + /*! + * Performs a logical iff of the current and the given DD. + * + * @param other The second DD used for the operation. + * @return The logical iff of the operands. + */ + Dd iff(Dd const& other) const; + + /*! + * Performs a logical exclusive-or of the current and the given DD. + * + * @param other The second DD used for the operation. + * @return The logical exclusive-or of the operands. + */ + Dd exclusiveOr(Dd const& other) const; + + /*! + * Performs a logical implication of the current and the given DD. + * + * @param other The second DD used for the operation. + * @return The logical implication of the operands. + */ + Dd implies(Dd const& other) const; + + /*! + * Adds the two DDs. + * + * @param other The DD to add to the current one. + * @return The result of the addition. + */ + Dd operator+(Dd const& other) const; + + /*! + * Adds the given DD to the current one. + * + * @param other The DD to add to the current one. + * @return A reference to the current DD after the operation. + */ + Dd& operator+=(Dd const& other); + + /*! + * Multiplies the two DDs. + * + * @param other The DD to multiply with the current one. + * @return The result of the multiplication. + */ + Dd operator*(Dd const& other) const; + + /*! + * Multiplies the given DD with the current one and assigns the result to the current DD. + * + * @param other The DD to multiply with the current one. + * @return A reference to the current DD after the operation. + */ + Dd& operator*=(Dd const& other); + + /*! + * Subtracts the given DD from the current one. + * + * @param other The DD to subtract from the current one. + * @return The result of the subtraction. + */ + Dd operator-(Dd const& other) const; + + /*! + * Subtracts the DD from the constant zero function. + * + * @return The resulting function represented as a DD. + */ + Dd operator-() const; + + /*! + * Subtracts the given DD from the current one and assigns the result to the current DD. + * + * @param other The DD to subtract from the current one. + * @return A reference to the current DD after the operation. + */ + Dd& operator-=(Dd const& other); + + /*! + * Divides the current DD by the given one. + * + * @param other The DD by which to divide the current one. + * @return The result of the division. + */ + Dd operator/(Dd const& other) const; + + /*! + * Divides the current DD by the given one and assigns the result to the current DD. + * + * @param other The DD by which to divide the current one. + * @return A reference to the current DD after the operation. + */ + Dd& operator/=(Dd const& other); + + /*! + * Retrieves the logical complement of the current DD. The result will map all encodings with a value + * unequal to zero to false and all others to true. + * + * @return The logical complement of the current DD. + */ + Dd operator!() const; + + /*! + * Logically complements the current DD. The result will map all encodings with a value + * unequal to zero to false and all others to true. + * + * @return A reference to the current DD after the operation. + */ + Dd& complement(); + + /*! + * Retrieves the function that maps all evaluations to one that have an identical function values. + * + * @param other The DD with which to perform the operation. + * @return The resulting function represented as a DD. + */ + Dd equals(Dd const& other) const; + + /*! + * Retrieves the function that maps all evaluations to one that have distinct function values. + * + * @param other The DD with which to perform the operation. + * @return The resulting function represented as a DD. + */ + Dd notEquals(Dd const& other) const; + + /*! + * Retrieves the function that maps all evaluations to one whose function value in the first DD are less + * than the one in the given DD. + * + * @param other The DD with which to perform the operation. + * @return The resulting function represented as a DD. + */ + Dd less(Dd const& other) const; + + /*! + * Retrieves the function that maps all evaluations to one whose function value in the first DD are less or + * equal than the one in the given DD. + * + * @param other The DD with which to perform the operation. + * @return The resulting function represented as a DD. + */ + Dd lessOrEqual(Dd const& other) const; + + /*! + * Retrieves the function that maps all evaluations to one whose function value in the first DD are greater + * than the one in the given DD. + * + * @param other The DD with which to perform the operation. + * @return The resulting function represented as a DD. + */ + Dd greater(Dd const& other) const; + + /*! + * Retrieves the function that maps all evaluations to one whose function value in the first DD are greater + * or equal than the one in the given DD. + * + * @param other The DD with which to perform the operation. + * @return The resulting function represented as a DD. + */ + Dd greaterOrEqual(Dd const& other) const; + + /*! + * Retrieves the function that maps all evaluations to the minimum of the function values of the two DDs. + * + * @param other The DD with which to perform the operation. + * @return The resulting function represented as a DD. + */ + Dd minimum(Dd const& other) const; + + /*! + * Retrieves the function that maps all evaluations to the maximum of the function values of the two DDs. + * + * @param other The DD with which to perform the operation. + * @return The resulting function represented as a DD. + */ + Dd maximum(Dd const& other) const; + + /*! + * Existentially abstracts from the given meta variables. + * + * @param metaVariables The meta variables from which to abstract. + */ + Dd existsAbstract(std::set const& metaVariables) const; + + /*! + * Universally abstracts from the given meta variables. + * + * @param metaVariables The meta variables from which to abstract. + */ + Dd universalAbstract(std::set const& metaVariables) const; + + /*! + * Sum-abstracts from the given meta variables. + * + * @param metaVariables The meta variables from which to abstract. + */ + Dd sumAbstract(std::set const& metaVariables) const; + + /*! + * Min-abstracts from the given meta variables. + * + * @param metaVariables The meta variables from which to abstract. + */ + Dd minAbstract(std::set const& metaVariables) const; + + /*! + * Max-abstracts from the given meta variables. + * + * @param metaVariables The meta variables from which to abstract. + */ + Dd maxAbstract(std::set const& metaVariables) const; + + /*! + * Checks whether the current and the given DD represent the same function modulo some given precision. + * + * @param other The DD with which to compare. + * @param precision An upper bound on the maximal difference between any two function values that is to be + * tolerated. + * @param relative If set to true, not the absolute values have to be within the precision, but the relative + * values. + */ + bool equalModuloPrecision(Dd const& other, double precision, bool relative = true) const; + + /*! + * Swaps the given pairs of meta variables in the DD. The pairs of meta variables must be guaranteed to have + * the same number of underlying DD variables. + * + * @param metaVariablePairs A vector of meta variable pairs that are to be swapped for one another. + * @return The resulting DD. + */ + Dd swapVariables(std::vector> const& metaVariablePairs); + + /*! + * Multiplies the current DD (representing a matrix) with the given matrix by summing over the given meta + * variables. + * + * @param otherMatrix The matrix with which to multiply. + * @param summationMetaVariables The names of the meta variables over which to sum during the matrix- + * matrix multiplication. + * @return A DD representing the result of the matrix-matrix multiplication. + */ + Dd multiplyMatrix(Dd const& otherMatrix, std::set const& summationMetaVariables) const; + + /*! + * Computes the logical and of the current and the given DD and existentially abstracts from the given set + * of variables. + * + * @param other The second DD for the logical and. + * @param existentialVariables The variables from which to existentially abstract. + * @return A DD representing the result. + */ + Dd andExists(Dd const& other, std::set const& existentialVariables) const; + + /*! + * Computes a DD that represents the function in which all assignments with a function value strictly larger + * 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 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; + + /*! + * Computes the constraint of the current DD with the given constraint. That is, the function value of the + * resulting DD will be the same as the current ones for all assignments mapping to one in the constraint + * and may be different otherwise. + * + * @param constraint The constraint to use for the operation. + * @return The resulting DD. + */ + Dd constrain(Dd const& constraint) const; + + /*! + * Computes the restriction of the current DD with the given constraint. That is, the function value of the + * resulting DD will be the same as the current ones for all assignments mapping to one in the constraint + * and may be different otherwise. + * + * @param constraint The constraint to use for the operation. + * @return The resulting DD. + */ + Dd restrict(Dd const& constraint) const; + + /*! + * Retrieves the support of the current DD. + * + * @return The support represented as a DD. + */ + Dd getSupport() const; + + /*! + * 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 number of nodes necessary to represent the DD. + * + * @return The number of nodes in this DD. + */ + uint_fast64_t getNodeCount() 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. + * + * @param metaVariable The meta variable that has to be equal to the given value. + * @param variableValue The value that the meta variable is supposed to have. This must be within the range + * of the meta variable. + * @param targetValue The new function value of the modified encodings. + */ + void setValue(storm::expressions::Variable const& metaVariable, int_fast64_t variableValue, double targetValue); + + /*! + * Sets the function values of all encodings that have the given values of the two meta variables to the + * given target value. + * + * @param metaVariable1 The first meta variable that has to be equal to the first given + * value. + * @param variableValue1 The value that the first meta variable is supposed to have. This must be within the + * range of the meta variable. + * @param metaVariable2 The second meta variable that has to be equal to the second given + * value. + * @param variableValue2 The value that the second meta variable is supposed to have. This must be within + * the range of the meta variable. + * @param targetValue The new function value of the modified encodings. + */ + void setValue(storm::expressions::Variable const& metaVariable1, int_fast64_t variableValue1, storm::expressions::Variable const& metaVariable2, int_fast64_t variableValue2, double targetValue); + + /*! + * Sets the function values of all encodings that have the given values of the given meta variables to the + * given target value. + * + * @param metaVariableToValueMap A mapping of meta variables to the values they are supposed to have. All + * values must be within the range of the respective meta variable. + * @param targetValue The new function value of the modified encodings. + */ + void setValue(std::map const& metaVariableToValueMap = std::map(), double targetValue = 0); + + /*! + * Retrieves the value of the function when all meta variables are assigned the values of the given mapping. + * Note that the mapping must specify values for all meta variables contained in the DD. + * + * @param metaVariableToValueMap A mapping of meta variables to their values. + * @return The value of the function evaluated with the given input. + */ + double getValue(std::map const& metaVariableToValueMap = std::map()) const; + + /*! + * 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 this DD represents a constant function. + * + * @return True if this DD represents a constants function. + */ + bool isConstant() const; + + /*! + * Retrieves the index of the topmost variable in the DD. + * + * @return The index of the topmost variable in DD. + */ + uint_fast64_t getIndex() const; + + /*! + * Converts the DD to a vector. + * + * @return The double vector that is represented by this DD. + */ + template + std::vector toVector() const; + + /*! + * Converts the DD to a vector. The given offset-labeled DD is used to determine the correct row of + * each entry. + * + * @param rowOdd The ODD used for determining the correct row. + * @return The double vector that is represented by this DD. + */ + template + std::vector toVector(storm::dd::Odd const& rowOdd) const; + + /*! + * Converts the DD to a (sparse) double matrix. All contained non-primed variables are assumed to encode the + * row, whereas all primed variables are assumed to encode the column. + * + * @return The matrix that is represented by this DD. + */ + storm::storage::SparseMatrix toMatrix() const; + + /*! + * Converts the DD to a (sparse) double matrix. All contained non-primed variables are assumed to encode the + * row, whereas all primed variables are assumed to encode the column. The given offset-labeled DDs are used + * to determine the correct row and column, respectively, for each entry. + * + * @param rowOdd The ODD used for determining the correct row. + * @param columnOdd The ODD used for determining the correct column. + * @return The matrix that is represented by this DD. + */ + storm::storage::SparseMatrix toMatrix(storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const; + + /*! + * Converts the DD to a (sparse) double matrix. The given offset-labeled DDs are used to determine the + * correct row and column, respectively, for each entry. + * + * @param rowMetaVariables The meta variables that encode the rows of the matrix. + * @param columnMetaVariables The meta variables that encode the columns of the matrix. + * @param rowOdd The ODD used for determining the correct row. + * @param columnOdd The ODD used for determining the correct column. + * @return The matrix that is represented by this DD. + */ + storm::storage::SparseMatrix toMatrix(std::set const& rowMetaVariables, std::set const& columnMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const; + + /*! + * Converts the DD to a row-grouped (sparse) double matrix. The given offset-labeled DDs are used to + * determine the correct row and column, respectively, for each entry. Note: this function assumes that + * the meta variables used to distinguish different row groups are at the very top of the DD. + * + * @param rowMetaVariables The meta variables that encode the rows of the matrix. + * @param columnMetaVariables The meta variables that encode the columns of the matrix. + * @param groupMetaVariables The meta variables that are used to distinguish different row groups. + * @param rowOdd The ODD used for determining the correct row. + * @param columnOdd The ODD used for determining the correct column. + * @return The matrix that is represented by this DD. + */ + storm::storage::SparseMatrix toMatrix(std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const; + + /*! + * Retrieves whether the given meta variable is contained in the DD. + * + * @param metaVariable The meta variable for which to query membership. + * @return True iff the meta variable is contained in the DD. + */ + bool containsMetaVariable(storm::expressions::Variable const& metaVariable) const; + + /*! + * Retrieves whether the given meta variables are all contained in the DD. + * + * @param metaVariables The meta variables for which to query membership. + * @return True iff all meta variables are contained in the DD. + */ + bool containsMetaVariables(std::set const& metaVariables) const; + + /*! + * Retrieves the set of all meta variables contained in the DD. + * + * @return The set of all meta variables contained in the DD. + */ + std::set const& getContainedMetaVariables() const; + + /*! + * Retrieves the set of all meta variables contained in the DD. + * + * @return The set of all meta variables contained in the DD. + */ + std::set& getContainedMetaVariables(); + + /*! + * Exports the DD to the given file in the dot format. + * + * @param filename The name of the file to which the DD is to be exported. + */ + void exportToDot(std::string const& filename = "") const; + + /*! + * Retrieves the manager that is responsible for this DD. + * + * A pointer to the manager that is responsible for this DD. + */ + std::shared_ptr const> getDdManager() const; + + /*! + * Retrieves an iterator that points to the first meta variable assignment with a non-zero function value. + * + * @param enumerateDontCareMetaVariables If set to true, all meta variable assignments are enumerated, even + * if a meta variable does not at all influence the the function value. + * @return An iterator that points to the first meta variable assignment with a non-zero function value. + */ + DdForwardIterator begin(bool enumerateDontCareMetaVariables = true) const; + + /*! + * Retrieves an iterator that points past the end of the container. + * + * @param enumerateDontCareMetaVariables If set to true, all meta variable assignments are enumerated, even + * if a meta variable does not at all influence the the function value. + * @return An iterator that points past the end of the container. + */ + DdForwardIterator end(bool enumerateDontCareMetaVariables = true) const; + + /*! + * Converts the DD into a (heavily nested) if-then-else expression that represents the very same function. + * The variable names used in the expression are derived from the meta variable name and are extended with a + * suffix ".i" if the meta variable is integer-valued, expressing that the variable is the i-th bit of the + * meta variable. + * + * @return The resulting expression. + */ + storm::expressions::Expression toExpression() const; + + /*! + * Converts the DD into a (heavily nested) if-then-else (with negations) expression that evaluates to true + * if and only if the assignment is minterm of the DD. The variable names used in the expression are derived + * from the meta variable name and are extended with a suffix ".i" if the meta variable is integer-valued, + * expressing that the variable is the i-th bit of the meta variable. + * + * @return The resulting expression. + */ + storm::expressions::Expression getMintermExpression() const; + + friend std::ostream & operator<<(std::ostream& out, const Dd& dd); + + /*! + * Converts an MTBDD to a BDD by mapping all values unequal to zero to 1. This effectively does the same as + * a call to notZero(). + * + * @return The corresponding BDD. + */ + Dd toBdd() const; + + /*! + * Converts a BDD to an equivalent MTBDD. + * + * @return The corresponding MTBDD. + */ + Dd toMtbdd() const; + + /*! + * Retrieves whether this DD is a BDD. + * + * @return True iff this DD is a BDD. + */ + bool isBdd() const; + + /*! + * Retrieves whether this DD is an MTBDD. Even though MTBDDs technicall subsume BDDs, this will return false + * if the DD is actually a BDD. + * + * @return True iff this DD is an MTBDD. + */ + bool isMtbdd() const; + + private: + /*! + * Retrieves the CUDD BDD object associated with this DD. + * + * @return The CUDD BDD object associated with this DD. + */ + BDD getCuddBdd() const; + + /*! + * Retrieves the CUDD MTBDD object associated with this DD. + * + * @return The CUDD MTBDD object associated with this DD. + */ + ADD getCuddMtbdd() const; + + /*! + * Retrieves the CUDD object associated with this DD. + * + * @return The CUDD object associated with this DD. + */ + ABDD const& getCuddDd() const; + + /*! + * Retrieves the raw DD node of CUDD associated with this DD. + * + * @return The DD node of CUDD associated with this DD. + */ + DdNode* getCuddDdNode() const; + + /*! + * Adds the given meta variable to the set of meta variables that are contained in this DD. + * + * @param metaVariable The name of the meta variable to add. + */ + void addContainedMetaVariable(storm::expressions::Variable const& metaVariable); + + /*! + * Removes the given meta variable to the set of meta variables that are contained in this DD. + * + * @param metaVariable The name of the meta variable to remove. + */ + void removeContainedMetaVariable(storm::expressions::Variable const& metaVariable); + + /*! + * Performs the recursive step of toExpression on the given DD. + * + * @param dd The dd to translate into an expression. + * @param variables The variables to use in the expression. + * @return The resulting expression. + */ + static storm::expressions::Expression toExpressionRecur(DdNode const* dd, std::vector const& variables); + + /*! + * Performs the recursive step of getMintermExpression on the given DD. + * + * @param manager The manager of the DD. + * @param dd The dd whose minterms to translate into an expression. + * @param variables The variables to use in the expression. + * @return The resulting expression. + */ + static storm::expressions::Expression getMintermExpressionRecur(::DdManager* manager, DdNode const* dd, std::vector const& variables); + + /*! + * Creates a DD that encapsulates the given CUDD ADD. + * + * @param ddManager The manager responsible for this DD. + * @param cuddDd The CUDD ADD to store. + * @param containedMetaVariables The meta variables that appear in the DD. + */ + Dd(std::shared_ptr const> ddManager, ADD cuddDd, std::set const& containedMetaVariables = std::set()); + + /*! + * Creates a DD that encapsulates the given CUDD ADD. + * + * @param ddManager The manager responsible for this DD. + * @param cuddDd The CUDD ADD to store. + * @param containedMetaVariables The meta variables that appear in the DD. + */ + Dd(std::shared_ptr const> ddManager, BDD cuddDd, std::set const& containedMetaVariables = std::set()); + + /*! + * Helper function to convert the DD into a (sparse) matrix. + * + * @param dd The DD to convert. + * @param rowIndications A vector indicating at which position in the columnsAndValues vector the entries + * of row i start. Note: this vector is modified in the computation. More concretely, each entry i in the + * vector will be increased by the number of entries in the row. This can be used to count the number + * of entries in each row. If the values are not to be modified, a copy needs to be provided or the entries + * need to be restored afterwards. + * @param columnsAndValues The vector that will hold the columns and values of non-zero entries upon successful + * completion. + * @param rowGroupOffsets The row offsets at which a given row group starts. + * @param rowOdd The ODD used for the row translation. + * @param columnOdd The ODD used for the column translation. + * @param currentRowLevel The currently considered row level in the DD. + * @param currentColumnLevel The currently considered row level in the DD. + * @param maxLevel The number of levels that need to be considered. + * @param currentRowOffset The current row offset. + * @param currentColumnOffset The current row offset. + * @param ddRowVariableIndices The (sorted) indices of all DD row variables that need to be considered. + * @param ddColumnVariableIndices The (sorted) indices of all DD row variables that need to be considered. + * @param generateValues If set to true, the vector columnsAndValues is filled with the actual entries, which + * only works if the offsets given in rowIndications are already correct. If they need to be computed first, + * this flag needs to be false. + */ + void toMatrixRec(DdNode const* dd, std::vector& rowIndications, std::vector>& columnsAndValues, std::vector const& rowGroupOffsets, Odd const& rowOdd, Odd const& columnOdd, uint_fast64_t currentRowLevel, uint_fast64_t currentColumnLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, uint_fast64_t currentColumnOffset, std::vector const& ddRowVariableIndices, std::vector const& ddColumnVariableIndices, bool generateValues = true) const; + + /*! + * Splits the given matrix DD into the groups using the given group variables. + * + * @param dd The DD to split. + * @param groups A vector that is to be filled with the DDs for the individual groups. + * @param ddGroupVariableIndices The (sorted) indices of all DD group variables that need to be considered. + * @param currentLevel The currently considered level in the DD. + * @param maxLevel The number of levels that need to be considered. + * @param remainingMetaVariables The meta variables that remain in the DDs after the groups have been split. + */ + void splitGroupsRec(DdNode* dd, std::vector>& groups, std::vector const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::set const& remainingMetaVariables) const; + + /*! + * Performs a recursive step to add the given DD-based vector to the given explicit vector. + * + * @param dd The DD to add to the explicit vector. + * @param currentLevel The currently considered level in the DD. + * @param maxLevel The number of levels that need to be considered. + * @param currentOffset The current offset. + * @param odd The ODD used for the translation. + * @param ddVariableIndices The (sorted) indices of all DD variables that need to be considered. + * @param targetVector The vector to which the translated DD-based vector is to be added. + */ + template + void addToVectorRec(DdNode const* dd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector) const; + + /*! + * Retrieves the indices of all DD variables that are contained in this DD (not necessarily in the support, + * because they could be "don't cares"). Additionally, the indices are sorted to allow for easy access. + * + * @return The (sorted) indices of all DD variables that are contained in this DD. + */ + std::vector getSortedVariableIndices() const; + + // A pointer to the manager responsible for this DD. + std::shared_ptr const> ddManager; + + // The ADD created by CUDD. + boost::variant cuddDd; + + // The meta variables that appear in this DD. + std::set containedMetaVariables; + }; + } +} + +#endif /* STORM_STORAGE_DD_CUDDDD_H_ */ \ No newline at end of file diff --git a/src/storage/dd/CuddBdd.cpp b/src/storage/dd/CuddBdd.cpp new file mode 100644 index 000000000..dd095af21 --- /dev/null +++ b/src/storage/dd/CuddBdd.cpp @@ -0,0 +1,321 @@ +#include +#include + +#include "src/storage/dd/CuddBdd.h" +#include "src/storage/dd/CuddAdd.h" +#include "src/storage/dd/CuddDdManager.h" + +namespace storm { + namespace dd { + Bdd::Bdd(std::shared_ptr const> ddManager, BDD cuddDd, std::set const& containedMetaVariables) : Dd(ddManager, containedMetaVariables) { + // Intentionally left empty. + } + + Add Bdd::toAdd() const { + return Add(this->getDdManager(), this->getCuddBdd().Add(), this->getContainedMetaVariables()); + } + + BDD Bdd::getCuddBdd() const { + return this->cuddBdd; + } + + DdNode* Bdd::getCuddDdNode() const { + return this->getCuddBdd().getNode(); + } + + bool Bdd::operator==(Bdd const& other) const { + return this->getCuddBdd() == other.getCuddBdd(); + } + + bool Bdd::operator!=(Bdd const& other) const { + return !(*this == other); + } + + Bdd Bdd::ite(Bdd const& thenDd, Bdd const& elseDd) const { + std::set metaVariableNames; + std::set_union(thenDd.getContainedMetaVariables().begin(), thenDd.getContainedMetaVariables().end(), elseDd.getContainedMetaVariables().begin(), elseDd.getContainedMetaVariables().end(), std::inserter(metaVariableNames, metaVariableNames.begin())); + metaVariableNames.insert(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end()); + + return Bdd(this->getDdManager(), this->getCuddBdd().Ite(thenDd.getCuddBdd(), elseDd.getCuddBdd()), metaVariableNames); + } + + Bdd Bdd::operator!() const { + Bdd result(*this); + result.complement(); + return result; + } + + Bdd& Bdd::complement() { + this->cuddBdd = ~this->getCuddBdd(); + } + + Bdd Bdd::operator&&(Bdd const& other) const { + Dd result(*this); + result &= other; + return result; + } + + Bdd& Bdd::operator&=(Bdd const& other) { + this->addMetaVariables(other.getContainedMetaVariables()); + this->cuddBdd = this->getCuddBdd() & other.getCuddBdd(); + return *this; + } + + Bdd Bdd::operator||(Bdd const& other) const { + Bdd result(*this); + result |= other; + return result; + } + + Bdd& Bdd::operator|=(Bdd const& other) { + this->addMetaVariables(other.getContainedMetaVariables()); + this->cuddBdd = this->getCuddBdd() | other.getCuddBdd(); + return *this; + } + + Bdd Bdd::iff(Bdd const& other) const { + std::set metaVariables(this->getContainedMetaVariables()); + metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end()); + return Bdd(this->getDdManager(), this->getCuddBdd().Xnor(other.getCuddBdd()), metaVariables); + } + + Bdd Bdd::exclusiveOr(Bdd const& other) const { + std::set metaVariables(this->getContainedMetaVariables()); + metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end()); + return Bdd(this->getDdManager(), this->getCuddBdd().Xor(other.getCuddBdd()), metaVariables); + } + + Bdd Bdd::implies(Bdd const& other) const { + std::set metaVariables(this->getContainedMetaVariables()); + metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end()); + return Bdd(this->getDdManager(), this->getCuddBdd().Ite(other.getCuddBdd(), this->getDdManager()->getBddOne().getCuddBdd()), metaVariables); + } + + Bdd Bdd::existsAbstract(std::set const& metaVariables) const { + Dd cubeDd(this->getDdManager()->getBddOne()); + + std::set newMetaVariables = this->getContainedMetaVariables(); + for (auto const& metaVariable : metaVariables) { + // First check whether the BDD contains the meta variable and erase it, if this is the case. + STORM_LOG_THROW(this->containsMetaVariable(metaVariable), storm::exceptions::InvalidArgumentException, "Cannot abstract from meta variable '" << metaVariable.getName() << "' that is not present in the DD."); + newMetaVariables.erase(metaVariable); + + DdMetaVariable const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable); + cubeDd &= ddMetaVariable.getCube(); + } + + return Bdd(this->getDdManager(), this->getCuddBdd().ExistAbstract(cubeDd.getCuddBdd()), newMetaVariables); + } + + Dd Bdd::universalAbstract(std::set const& metaVariables) const { + Dd cubeDd(this->getDdManager()->getBddOne()); + + std::set newMetaVariables = this->getContainedMetaVariables(); + for (auto const& metaVariable : metaVariables) { + // First check whether the BDD contains the meta variable and erase it, if this is the case. + STORM_LOG_THROW(this->containsMetaVariable(metaVariable), storm::exceptions::InvalidArgumentException, "Cannot abstract from meta variable '" << metaVariable.getName() << "' that is not present in the DD."); + newMetaVariables.erase(metaVariable); + + DdMetaVariable const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable); + cubeDd &= ddMetaVariable.getCube(); + } + + return Bdd(this->getDdManager(), this->getCuddBdd().UnivAbstract(cubeDd.getCuddBdd()), newMetaVariables); + } + + Dd Bdd::swapVariables(std::vector> const& metaVariablePairs) { + std::set newContainedMetaVariables; + std::vector from; + std::vector to; + for (auto const& metaVariablePair : metaVariablePairs) { + DdMetaVariable const& variable1 = this->getDdManager()->getMetaVariable(metaVariablePair.first); + DdMetaVariable const& variable2 = this->getDdManager()->getMetaVariable(metaVariablePair.second); + + // Check if it's legal so swap the meta variables. + STORM_LOG_THROW(variable1.getNumberOfDdVariables() == variable2.getNumberOfDdVariables(), storm::exceptions::InvalidArgumentException, "Unable to swap meta variables with different size."); + + // Keep track of the contained meta variables in the DD. + if (this->containsMetaVariable(metaVariablePair.first)) { + newContainedMetaVariables.insert(metaVariablePair.second); + } + if (this->containsMetaVariable(metaVariablePair.second)) { + newContainedMetaVariables.insert(metaVariablePair.first); + } + + // Add the variables to swap to the corresponding vectors. + for (auto const& ddVariable : variable1.getDdVariables()) { + from.push_back(ddVariable.getCuddBdd()); + } + for (auto const& ddVariable : variable2.getDdVariables()) { + to.push_back(ddVariable.getCuddBdd()); + } + } + + // Finally, call CUDD to swap the variables. + return Bdd(this->getDdManager(), this->getCuddBdd().SwapVariables(from, to), newContainedMetaVariables); + } + + Bdd Bdd::andExists(Bdd const& other, std::set const& existentialVariables) const { + STORM_LOG_WARN_COND(this->isBdd() && other.isBdd(), "Performing logical operation on MTBDD(s)."); + + Dd cubeDd(this->getDdManager()->getOne()); + for (auto const& metaVariable : existentialVariables) { + DdMetaVariable const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable); + cubeDd &= ddMetaVariable.getCube(); + } + + std::set unionOfMetaVariables; + std::set_union(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end(), other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end(), std::inserter(unionOfMetaVariables, unionOfMetaVariables.begin())); + std::set containedMetaVariables; + std::set_difference(unionOfMetaVariables.begin(), unionOfMetaVariables.end(), existentialVariables.begin(), existentialVariables.end(), std::inserter(containedMetaVariables, containedMetaVariables.begin())); + + return Dd(this->getDdManager(), this->getCuddBdd().AndAbstract(other.getCuddBdd(), cubeDd.getCuddBdd()), containedMetaVariables); + } + + Dd Bdd::constrain(Dd const& constraint) const { + std::set metaVariables(this->getContainedMetaVariables()); + metaVariables.insert(constraint.getContainedMetaVariables().begin(), constraint.getContainedMetaVariables().end()); + + if (this->isBdd() && constraint.isBdd()) { + return Dd(this->getDdManager(), this->getCuddBdd().Constrain(constraint.getCuddBdd()), metaVariables); + } else { + return Dd(this->getDdManager(), this->getCuddMtbdd().Constrain(constraint.getCuddMtbdd()), metaVariables); + } + } + + Dd Bdd::restrict(Dd const& constraint) const { + std::set metaVariables(this->getContainedMetaVariables()); + metaVariables.insert(constraint.getContainedMetaVariables().begin(), constraint.getContainedMetaVariables().end()); + + if (this->isBdd() && constraint.isBdd()) { + return Dd(this->getDdManager(), this->getCuddBdd().Restrict(constraint.getCuddBdd()), metaVariables); + } else { + return Dd(this->getDdManager(), this->getCuddMtbdd().Restrict(constraint.getCuddMtbdd()), metaVariables); + } + } + + Dd Bdd::getSupport() const { + if (this->isBdd()) { + return Dd(this->getDdManager(), this->getCuddBdd().Support(), this->getContainedMetaVariables()); + } else { + return Dd(this->getDdManager(), this->getCuddMtbdd().Support(), this->getContainedMetaVariables()); + } + } + + uint_fast64_t Bdd::getNonZeroCount() const { + std::size_t numberOfDdVariables = 0; + for (auto const& metaVariable : this->getContainedMetaVariables()) { + numberOfDdVariables += this->getDdManager()->getMetaVariable(metaVariable).getNumberOfDdVariables(); + } + if (this->isBdd()) { + return static_cast(this->getCuddBdd().CountMinterm(static_cast(numberOfDdVariables))); + } else { + return static_cast(this->getCuddMtbdd().CountMinterm(static_cast(numberOfDdVariables))); + } + } + + uint_fast64_t Bdd::getLeafCount() const { + if (this->isBdd()) { + return static_cast(this->getCuddBdd().CountLeaves()); + } else { + return static_cast(this->getCuddMtbdd().CountLeaves()); + } + } + + uint_fast64_t Bdd::getNodeCount() const { + if (this->isBdd()) { + return static_cast(this->getCuddBdd().nodeCount()); + } else { + return static_cast(this->getCuddMtbdd().nodeCount()); + } + } + + bool Bdd::isOne() const { + if (this->isBdd()) { + return this->getCuddBdd().IsOne(); + } else { + return this->getCuddMtbdd().IsOne(); + } + } + + bool Bdd::isZero() const { + if (this->isBdd()) { + return this->getCuddBdd().IsZero(); + } else { + return this->getCuddMtbdd().IsZero(); + } + } + + uint_fast64_t Bdd::getIndex() const { + if (this->isBdd()) { + return static_cast(this->getCuddBdd().NodeReadIndex()); + } else { + return static_cast(this->getCuddMtbdd().NodeReadIndex()); + } + } + + std::vector Bdd::getSortedVariableIndices() const { + std::vector ddVariableIndices; + for (auto const& metaVariableName : this->getContainedMetaVariables()) { + auto const& metaVariable = this->getDdManager()->getMetaVariable(metaVariableName); + for (auto const& ddVariable : metaVariable.getDdVariables()) { + ddVariableIndices.push_back(ddVariable.getIndex()); + } + } + + // Next, we need to sort them, since they may be arbitrarily ordered otherwise. + std::sort(ddVariableIndices.begin(), ddVariableIndices.end()); + return ddVariableIndices; + } + + void Bdd::exportToDot(std::string const& filename) const { + if (filename.empty()) { + if (this->isBdd()) { + std::vector cuddBddVector = { this->getCuddBdd() }; + this->getDdManager()->getCuddManager().DumpDot(cuddBddVector); + } else { + std::vector cuddAddVector = { this->getCuddMtbdd() }; + this->getDdManager()->getCuddManager().DumpDot(cuddAddVector); + } + } else { + // Build the name input of the DD. + std::vector ddNames; + std::string ddName("f"); + ddNames.push_back(new char[ddName.size() + 1]); + std::copy(ddName.c_str(), ddName.c_str() + 2, ddNames.back()); + + // Now build the variables names. + std::vector ddVariableNamesAsStrings = this->getDdManager()->getDdVariableNames(); + std::vector ddVariableNames; + for (auto const& element : ddVariableNamesAsStrings) { + ddVariableNames.push_back(new char[element.size() + 1]); + std::copy(element.c_str(), element.c_str() + element.size() + 1, ddVariableNames.back()); + } + + // Open the file, dump the DD and close it again. + FILE* filePointer = fopen(filename.c_str() , "w"); + if (this->isBdd()) { + std::vector cuddBddVector = { this->getCuddBdd() }; + this->getDdManager()->getCuddManager().DumpDot(cuddBddVector, &ddVariableNames[0], &ddNames[0], filePointer); + } else { + std::vector cuddAddVector = { this->getCuddMtbdd() }; + this->getDdManager()->getCuddManager().DumpDot(cuddAddVector, &ddVariableNames[0], &ddNames[0], filePointer); + } + fclose(filePointer); + + // Finally, delete the names. + for (char* element : ddNames) { + delete element; + } + for (char* element : ddVariableNames) { + delete element; + } + } + } + + std::ostream& operator<<(std::ostream& out, const Dd& dd) { + dd.exportToDot(); + return out; + } + } +} \ No newline at end of file diff --git a/src/storage/dd/CuddBdd.h b/src/storage/dd/CuddBdd.h new file mode 100644 index 000000000..19335a3f4 --- /dev/null +++ b/src/storage/dd/CuddBdd.h @@ -0,0 +1,275 @@ +#ifndef STORM_STORAGE_DD_CUDDBDD_H_ +#define STORM_STORAGE_DD_CUDDBDD_H_ + +#include "src/storage/dd/Bdd.h" +#include "src/storage/dd/CuddDd.h" +#include "src/storage/dd/CuddAdd.h" +#include "src/storage/expressions/Variable.h" +#include "src/utility/OsDetection.h" + +// Include the C++-interface of CUDD. +#include "cuddObj.hh" + +namespace storm { + namespace dd { + // Forward-declare some classes. + template class DdManager; + template class Odd; + template class Add; + + template<> + class Bdd : public Dd { + public: + // Declare the DdManager and DdIterator class as friend so it can access the internals of a DD. + friend class DdManager; + friend class DdForwardIterator; + friend class Odd; + + // Instantiate all copy/move constructors/assignments with the default implementation. + Bdd() = default; + Bdd(Bdd const& other) = default; + Bdd& operator=(Bdd const& other) = default; +#ifndef WINDOWS + Bdd(Bdd&& other) = default; + Bdd& operator=(Bdd&& other) = default; +#endif + + /*! + * Retrieves whether the two BDDs represent the same function. + * + * @param other The BDD that is to be compared with the current one. + * @return True if the BDDs represent the same function. + */ + bool operator==(Bdd const& other) const; + + /*! + * Retrieves whether the two BDDs represent different functions. + * + * @param other The BDD that is to be compared with the current one. + * @return True if the BDDs represent the different functions. + */ + bool operator!=(Bdd const& other) const; + + /*! + * Performs an if-then-else with the given operands, i.e. maps all valuations that are mapped to a non-zero + * function value to the function values specified by the first DD and all others to the function values + * specified by the second DD. + * + * @param thenBdd The BDD defining the 'then' part. + * @param elseBdd The BDD defining the 'else' part. + * @return The resulting BDD. + */ + Bdd ite(Bdd const& thenBdd, Bdd const& elseBdd) const; + + /*! + * Performs a logical or of the current and the given BDD. + * + * @param other The second BDD used for the operation. + * @return The logical or of the operands. + */ + Bdd operator||(Bdd const& other) const; + + /*! + * Performs a logical or of the current and the given BDD and assigns it to the current BDD. + * + * @param other The second BDD used for the operation. + * @return A reference to the current BDD after the operation + */ + Bdd& operator|=(Bdd const& other); + + /*! + * Performs a logical and of the current and the given BDD. + * + * @param other The second BDD used for the operation. + * @return The logical and of the operands. + */ + Bdd operator&&(Bdd const& other) const; + + /*! + * Performs a logical and of the current and the given BDD and assigns it to the current BDD. + * + * @param other The second BDD used for the operation. + * @return A reference to the current BDD after the operation + */ + Bdd& operator&=(Bdd const& other); + + /*! + * Performs a logical iff of the current and the given BDD. + * + * @param other The second BDD used for the operation. + * @return The logical iff of the operands. + */ + Bdd iff(Bdd const& other) const; + + /*! + * Performs a logical exclusive-or of the current and the given BDD. + * + * @param other The second BDD used for the operation. + * @return The logical exclusive-or of the operands. + */ + Bdd exclusiveOr(Bdd const& other) const; + + /*! + * Performs a logical implication of the current and the given BDD. + * + * @param other The second BDD used for the operation. + * @return The logical implication of the operands. + */ + Bdd implies(Bdd const& other) const; + + /*! + * Logically inverts the current BDD. + * + * @return The resulting BDD. + */ + Bdd operator!() const; + + /*! + * Logically complements the current BDD. + * + * @return A reference to the current BDD after the operation. + */ + Bdd& complement(); + + /*! + * Existentially abstracts from the given meta variables. + * + * @param metaVariables The meta variables from which to abstract. + */ + Bdd existsAbstract(std::set const& metaVariables) const; + + /*! + * Universally abstracts from the given meta variables. + * + * @param metaVariables The meta variables from which to abstract. + */ + Bdd universalAbstract(std::set const& metaVariables) const; + + /*! + * Swaps the given pairs of meta variables in the BDD. The pairs of meta variables must be guaranteed to have + * the same number of underlying BDD variables. + * + * @param metaVariablePairs A vector of meta variable pairs that are to be swapped for one another. + * @return The resulting BDD. + */ + Bdd swapVariables(std::vector> const& metaVariablePairs); + + /*! + * Computes the logical and of the current and the given BDD and existentially abstracts from the given set + * of variables. + * + * @param other The second BDD for the logical and. + * @param existentialVariables The variables from which to existentially abstract. + * @return A BDD representing the result. + */ + Bdd andExists(Bdd const& other, std::set const& existentialVariables) const; + + /*! + * Computes the constraint of the current BDD with the given constraint. That is, the function value of the + * resulting BDD will be the same as the current ones for all assignments mapping to one in the constraint + * and may be different otherwise. + * + * @param constraint The constraint to use for the operation. + * @return The resulting BDD. + */ + Bdd constrain(Bdd const& constraint) const; + + /*! + * Computes the restriction of the current BDD with the given constraint. That is, the function value of the + * resulting DD will be the same as the current ones for all assignments mapping to one in the constraint + * and may be different otherwise. + * + * @param constraint The constraint to use for the operation. + * @return The resulting BDD. + */ + Bdd restrict(Bdd const& constraint) const; + + /*! + * Retrieves the support of the current BDD. + * + * @return The support represented as a BDD. + */ + virtual Bdd getSupport() const override; + + /*! + * 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. + */ + virtual uint_fast64_t getNonZeroCount() const override; + + /*! + * Retrieves the number of nodes necessary to represent the DD. + * + * @return The number of nodes in this DD. + */ + virtual uint_fast64_t getNodeCount() const override; + + /*! + * 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 the index of the topmost variable in the BDD. + * + * @return The index of the topmost variable in BDD. + */ + virtual uint_fast64_t getIndex() const override; + + /*! + * Exports the BDD to the given file in the dot format. + * + * @param filename The name of the file to which the BDD is to be exported. + */ + virtual void exportToDot(std::string const& filename = "") const override; + + friend std::ostream & operator<<(std::ostream& out, const Bdd& bdd); + + /*! + * Converts a BDD to an equivalent ADD. + * + * @return The corresponding ADD. + */ + Add toAdd() const; + + private: + /*! + * Retrieves the CUDD BDD object associated with this DD. + * + * @return The CUDD BDD object associated with this DD. + */ + BDD getCuddBdd() const; + + /*! + * Retrieves the raw DD node of CUDD associated with this BDD. + * + * @return The DD node of CUDD associated with this BDD. + */ + DdNode* getCuddDdNode() const; + + /*! + * Creates a DD that encapsulates the given CUDD ADD. + * + * @param ddManager The manager responsible for this DD. + * @param cuddDd The CUDD ADD to store. + * @param containedMetaVariables The meta variables that appear in the DD. + */ + Bdd(std::shared_ptr const> ddManager, BDD cuddDd, std::set const& containedMetaVariables = std::set()); + + // The BDD created by CUDD. + BDD cuddBdd; + }; + } +} + +#endif /* STORM_STORAGE_DD_CUDDBDD_H_ */ \ No newline at end of file diff --git a/src/storage/dd/CuddDd.cpp b/src/storage/dd/CuddDd.cpp index a169403d0..3ec7328f4 100644 --- a/src/storage/dd/CuddDd.cpp +++ b/src/storage/dd/CuddDd.cpp @@ -1,1040 +1,20 @@ -#include #include #include "src/storage/dd/CuddDd.h" -#include "src/storage/dd/CuddOdd.h" #include "src/storage/dd/CuddDdManager.h" -#include "src/utility/vector.h" -#include "src/utility/macros.h" - -#include "src/exceptions/IllegalFunctionCallException.h" -#include "src/exceptions/InvalidArgumentException.h" -#include "src/exceptions/NotImplementedException.h" namespace storm { namespace dd { - Dd::Dd(std::shared_ptr const> ddManager, BDD cuddDd, std::set const& containedMetaVariables) : ddManager(ddManager), cuddDd(cuddDd), containedMetaVariables(containedMetaVariables) { - // Intentionally left empty. - } - - Dd::Dd(std::shared_ptr const> ddManager, ADD cuddDd, std::set const& containedMetaVariables) : ddManager(ddManager), cuddDd(cuddDd), containedMetaVariables(containedMetaVariables) { + Dd::Dd(std::shared_ptr const> ddManager, std::set const& containedMetaVariables) : ddManager(ddManager), containedMetaVariables(containedMetaVariables) { // Intentionally left empty. } - - bool Dd::isBdd() const { - return this->cuddDd.which() == 0; - } - - bool Dd::isMtbdd() const { - return this->cuddDd.which() == 1; - } - - Dd Dd::toBdd() const { - if (this->isBdd()) { - return *this; - } else { - return Dd(this->getDdManager(), this->getCuddMtbdd().BddPattern(), this->containedMetaVariables); - } - } - - Dd Dd::toMtbdd() const { - if (this->isMtbdd()) { - return *this; - } else { - return Dd(this->getDdManager(), this->getCuddBdd().Add(), this->containedMetaVariables); - } - } - - BDD Dd::getCuddBdd() const { - if (this->isBdd()) { - return boost::get(this->cuddDd); - } else { - STORM_LOG_WARN_COND(false, "Implicitly converting MTBDD to BDD."); - return this->getCuddMtbdd().BddPattern(); - } - } - - ADD Dd::getCuddMtbdd() const { - if (this->isMtbdd()) { - return boost::get(this->cuddDd); - } else { - STORM_LOG_WARN_COND(false, "Implicitly converting BDD to MTBDD."); - return this->getCuddBdd().Add(); - } - } - - ABDD const& Dd::getCuddDd() const { - if (this->isBdd()) { - return static_cast(boost::get(this->cuddDd)); - } else { - return static_cast(boost::get(this->cuddDd)); - } - } - - DdNode* Dd::getCuddDdNode() const { - if (this->isBdd()) { - return this->getCuddBdd().getNode(); - } else { - return this->getCuddMtbdd().getNode(); - } - } - - bool Dd::operator==(Dd const& other) const { - if (this->isBdd()) { - if (other.isBdd()) { - return this->getCuddBdd() == other.getCuddBdd(); - } else { - return false; - } - } else { - if (other.isMtbdd()) { - return this->getCuddMtbdd() == other.getCuddMtbdd(); - } else { - return false; - } - } - } - - bool Dd::operator!=(Dd const& other) const { - return !(*this == other); - } - - Dd Dd::ite(Dd const& thenDd, Dd const& elseDd) const { - std::set metaVariableNames(this->getContainedMetaVariables()); - metaVariableNames.insert(thenDd.getContainedMetaVariables().begin(), thenDd.getContainedMetaVariables().end()); - metaVariableNames.insert(elseDd.getContainedMetaVariables().begin(), elseDd.getContainedMetaVariables().end()); - - // If all involved DDs are BDDs, the result is also going to be a BDD. - if (this->isBdd() && thenDd.isBdd() && elseDd.isBdd()) { - return Dd(this->getDdManager(), this->getCuddBdd().Ite(thenDd.getCuddBdd(), elseDd.getCuddBdd()), metaVariableNames); - } else { - return Dd(this->getDdManager(), this->toMtbdd().getCuddMtbdd().Ite(thenDd.toMtbdd().getCuddMtbdd(), elseDd.toMtbdd().getCuddMtbdd()), metaVariableNames); - } - } - - Dd Dd::operator+(Dd const& other) const { - Dd result(*this); - result += other; - return result; - } - - Dd& Dd::operator+=(Dd const& other) { - STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing addition on BDDs."); - this->getContainedMetaVariables().insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end()); - this->cuddDd = this->getCuddMtbdd() + other.getCuddMtbdd(); - return *this; - } - - Dd Dd::operator*(Dd const& other) const { - Dd result(*this); - result *= other; - return result; - } - - Dd& Dd::operator*=(Dd const& other) { - this->getContainedMetaVariables().insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end()); - if (this->isMtbdd() && other.isMtbdd()) { - this->cuddDd = this->getCuddMtbdd() * other.getCuddMtbdd(); - } else if (this->isBdd() && other.isBdd()) { - this->cuddDd = this->getCuddBdd() & other.getCuddBdd(); - } else { - STORM_LOG_WARN_COND(false, "Performing multiplication on two DDs of different type."); - this->cuddDd = this->getCuddMtbdd() * other.getCuddMtbdd(); - } - return *this; - } - - Dd Dd::operator-(Dd const& other) const { - STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing arithmetical operation on BDD(s)."); - Dd result(*this); - result -= other; - return result; - } - - Dd Dd::operator-() const { - STORM_LOG_WARN_COND(this->isMtbdd(), "Performing arithmetical operation on BDD(s)."); - return this->getDdManager()->getZero(true) - *this; - } - - Dd& Dd::operator-=(Dd const& other) { - STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing arithmetical operation on BDD(s)."); - this->cuddDd = this->getCuddMtbdd() - other.getCuddMtbdd(); - this->getContainedMetaVariables().insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end()); - return *this; - } - - Dd Dd::operator/(Dd const& other) const { - STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing arithmetical operation on BDD(s)."); - Dd result(*this); - result /= other; - return result; - } - - Dd& Dd::operator/=(Dd const& other) { - STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing arithmetical operation on BDD(s)."); - this->cuddDd = this->getCuddMtbdd().Divide(other.getCuddMtbdd()); - this->getContainedMetaVariables().insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end()); - return *this; - } - - Dd Dd::operator!() const { - Dd result(*this); - result.complement(); - return result; - } - - Dd& Dd::complement() { - if (this->isBdd()) { - this->cuddDd = ~this->getCuddBdd(); - } else { - this->cuddDd = ~this->getCuddMtbdd(); - } - return *this; - } - - Dd Dd::operator&&(Dd const& other) const { - Dd result(*this); - result &= other; - return result; - } - - Dd& Dd::operator&=(Dd const& other) { - this->getContainedMetaVariables().insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end()); - if (this->isBdd() && other.isBdd()) { - this->cuddDd = this->getCuddBdd() & other.getCuddBdd(); - } else if (this->isMtbdd() && other.isMtbdd()) { - // We also tolerate (without a warning) if the two arguments are MTBDDs. The caller has to make sure that - // the two given DDs are 0-1-MTBDDs, because the operation may produce wrong results otherwise. - this->cuddDd = this->getCuddMtbdd() & other.getCuddMtbdd(); - } else { - STORM_LOG_WARN_COND(false, "Performing logical and on two DDs of different type."); - this->cuddDd = this->getCuddBdd() & other.getCuddBdd(); - } - return *this; - } - - Dd Dd::operator||(Dd const& other) const { - Dd result(*this); - result |= other; - return result; - } - - Dd& Dd::operator|=(Dd const& other) { - this->getContainedMetaVariables().insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end()); - if (this->isBdd() && other.isBdd()) { - this->cuddDd = this->getCuddBdd() | other.getCuddBdd(); - } else if (this->isMtbdd() && other.isMtbdd()) { - // We also tolerate (without a warning) if the two arguments are MTBDDs. The caller has to make sure that - // the two given DDs are 0-1-MTBDDs, because the operation may produce wrong results otherwise. - this->cuddDd = this->getCuddMtbdd() | other.getCuddMtbdd(); - } else { - STORM_LOG_WARN_COND(false, "Performing logical and on two DDs of different type."); - this->cuddDd = this->getCuddBdd() & other.getCuddBdd(); - } - return *this; - - STORM_LOG_WARN_COND(this->isBdd() && other.isBdd(), "Performing logical operation on MTBDD(s)."); - this->cuddDd = this->getCuddBdd() | other.getCuddBdd(); - this->getContainedMetaVariables().insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end()); - return *this; - } - - Dd Dd::iff(Dd const& other) const { - std::set metaVariables(this->getContainedMetaVariables()); - metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end()); - if (this->isBdd() && other.isBdd()) { - return Dd(this->getDdManager(), this->getCuddBdd().Xnor(other.getCuddBdd()), metaVariables); - } else if (this->isMtbdd() && other.isMtbdd()) { - // We also tolerate (without a warning) if the two arguments are MTBDDs. The caller has to make sure that - // the two given DDs are 0-1-MTBDDs, because the operation may produce wrong results otherwise. - return Dd(this->getDdManager(), this->getCuddMtbdd().Xnor(other.getCuddMtbdd()), metaVariables); - } else { - STORM_LOG_WARN_COND(false, "Performing logical iff on two DDs of different type."); - return Dd(this->getDdManager(), this->getCuddBdd().Xnor(other.getCuddBdd()), metaVariables); - } - } - - Dd Dd::exclusiveOr(Dd const& other) const { - std::set metaVariables(this->getContainedMetaVariables()); - metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end()); - if (this->isBdd() && other.isBdd()) { - return Dd(this->getDdManager(), this->getCuddBdd().Xor(other.getCuddBdd()), metaVariables); - } else if (this->isMtbdd() && other.isMtbdd()) { - // We also tolerate (without a warning) if the two arguments are MTBDDs. The caller has to make sure that - // the two given DDs are 0-1-MTBDDs, because the operation may produce wrong results otherwise. - return Dd(this->getDdManager(), this->getCuddMtbdd().Xor(other.getCuddMtbdd()), metaVariables); - } else { - STORM_LOG_WARN_COND(false, "Performing logical iff on two DDs of different type."); - return Dd(this->getDdManager(), this->getCuddBdd().Xor(other.getCuddBdd()), metaVariables); - } - } - - Dd Dd::implies(Dd const& other) const { - std::set metaVariables(this->getContainedMetaVariables()); - metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end()); - STORM_LOG_WARN_COND(this->isBdd() && other.isBdd(), "Performing logical operatiorn on MTBDDs."); - return Dd(this->getDdManager(), this->getCuddBdd().Ite(other.getCuddBdd(), this->getDdManager()->getOne().getCuddBdd()), metaVariables); - } - - Dd Dd::equals(Dd const& other) const { - STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing arithmetical operation on BDD(s)."); - std::set metaVariables(this->getContainedMetaVariables()); - metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end()); - return Dd(this->getDdManager(), this->getCuddMtbdd().Equals(other.getCuddMtbdd()), metaVariables); - } - - Dd Dd::notEquals(Dd const& other) const { - STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing arithmetical operation on BDD(s)."); - std::set metaVariables(this->getContainedMetaVariables()); - metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end()); - return Dd(this->getDdManager(), this->getCuddMtbdd().NotEquals(other.getCuddMtbdd()), metaVariables); - } - - Dd Dd::less(Dd const& other) const { - STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing arithmetical operation on BDD(s)."); - std::set metaVariables(this->getContainedMetaVariables()); - metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end()); - return Dd(this->getDdManager(), this->getCuddMtbdd().LessThan(other.getCuddMtbdd()), metaVariables); - } - - Dd Dd::lessOrEqual(Dd const& other) const { - STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing arithmetical operation on BDD(s)."); - std::set metaVariables(this->getContainedMetaVariables()); - metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end()); - return Dd(this->getDdManager(), this->getCuddMtbdd().LessThanOrEqual(other.getCuddMtbdd()), metaVariables); - } - - Dd Dd::greater(Dd const& other) const { - STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing arithmetical operation on BDD(s)."); - std::set metaVariables(this->getContainedMetaVariables()); - metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end()); - return Dd(this->getDdManager(), this->getCuddMtbdd().GreaterThan(other.getCuddMtbdd()), metaVariables); - } - - Dd Dd::greaterOrEqual(Dd const& other) const { - STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing arithmetical operation on BDD(s)."); - std::set metaVariables(this->getContainedMetaVariables()); - metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end()); - return Dd(this->getDdManager(), this->getCuddMtbdd().GreaterThanOrEqual(other.getCuddMtbdd()), metaVariables); - } - - Dd Dd::minimum(Dd const& other) const { - STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing arithmetical operation on BDD(s)."); - std::set metaVariables(this->getContainedMetaVariables()); - metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end()); - return Dd(this->getDdManager(), this->getCuddMtbdd().Minimum(other.getCuddMtbdd()), metaVariables); - } - - Dd Dd::maximum(Dd const& other) const { - STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing arithmetical operation on BDD(s)."); - std::set metaVariables(this->getContainedMetaVariables()); - metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end()); - return Dd(this->getDdManager(), this->getCuddMtbdd().Maximum(other.getCuddMtbdd()), metaVariables); - } - - Dd Dd::existsAbstract(std::set const& metaVariables) const { - STORM_LOG_WARN_COND(this->isBdd(), "Performing logical operation on MTBDD(s)."); - - Dd cubeDd(this->getDdManager()->getOne(false)); - std::set newMetaVariables = this->getContainedMetaVariables(); - for (auto const& metaVariable : metaVariables) { - // First check whether the DD contains the meta variable and erase it, if this is the case. - STORM_LOG_THROW(this->containsMetaVariable(metaVariable), storm::exceptions::InvalidArgumentException, "Cannot abstract from meta variable '" << metaVariable.getName() << "' that is not present in the DD."); - newMetaVariables.erase(metaVariable); - - DdMetaVariable const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable); - cubeDd &= ddMetaVariable.getCube(); - } - - return Dd(this->getDdManager(), this->getCuddBdd().ExistAbstract(cubeDd.getCuddBdd()), newMetaVariables); - } - - Dd Dd::universalAbstract(std::set const& metaVariables) const { - STORM_LOG_WARN_COND(this->isBdd(), "Performing logical operation on MTBDD(s)."); - - Dd cubeDd(this->getDdManager()->getOne()); - std::set newMetaVariables = this->getContainedMetaVariables(); - for (auto const& metaVariable : metaVariables) { - // First check whether the DD contains the meta variable and erase it, if this is the case. - STORM_LOG_THROW(this->containsMetaVariable(metaVariable), storm::exceptions::InvalidArgumentException, "Cannot abstract from meta variable '" << metaVariable.getName() << "' that is not present in the DD."); - newMetaVariables.erase(metaVariable); - - DdMetaVariable const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable); - cubeDd &= ddMetaVariable.getCube(); - } - - return Dd(this->getDdManager(), this->getCuddBdd().UnivAbstract(cubeDd.getCuddBdd()), newMetaVariables); - } - - Dd Dd::sumAbstract(std::set const& metaVariables) const { - STORM_LOG_WARN_COND(this->isMtbdd(), "Performing arithmetical operation on BDD(s)."); - - Dd cubeDd(this->getDdManager()->getOne(true)); - std::set newMetaVariables = this->getContainedMetaVariables(); - for (auto const& metaVariable : metaVariables) { - // First check whether the DD contains the meta variable and erase it, if this is the case. - STORM_LOG_THROW(this->containsMetaVariable(metaVariable), storm::exceptions::InvalidArgumentException, "Cannot abstract from meta variable '" << metaVariable.getName() << "' that is not present in the DD."); - newMetaVariables.erase(metaVariable); - - DdMetaVariable const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable); - cubeDd *= ddMetaVariable.getCubeAsMtbdd(); - } - - return Dd(this->getDdManager(), this->getCuddMtbdd().ExistAbstract(cubeDd.getCuddMtbdd()), newMetaVariables); - } - - Dd Dd::minAbstract(std::set const& metaVariables) const { - STORM_LOG_WARN_COND(this->isMtbdd(), "Performing arithmetical operation on BDD(s)."); - - Dd cubeDd(this->getDdManager()->getOne(true)); - std::set newMetaVariables = this->getContainedMetaVariables(); - for (auto const& metaVariable : metaVariables) { - // First check whether the DD contains the meta variable and erase it, if this is the case. - STORM_LOG_THROW(this->containsMetaVariable(metaVariable), storm::exceptions::InvalidArgumentException, "Cannot abstract from meta variable '" << metaVariable.getName() << "' that is not present in the DD."); - newMetaVariables.erase(metaVariable); - - DdMetaVariable const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable); - cubeDd *= ddMetaVariable.getCubeAsMtbdd(); - } - - return Dd(this->getDdManager(), this->getCuddMtbdd().MinAbstract(cubeDd.getCuddMtbdd()), newMetaVariables); - } - - Dd Dd::maxAbstract(std::set const& metaVariables) const { - STORM_LOG_WARN_COND(this->isMtbdd(), "Performing arithmetical operation on BDD(s)."); - - Dd cubeDd(this->getDdManager()->getOne(true)); - std::set newMetaVariables = this->getContainedMetaVariables(); - for (auto const& metaVariable : metaVariables) { - // First check whether the DD contains the meta variable and erase it, if this is the case. - STORM_LOG_THROW(this->containsMetaVariable(metaVariable), storm::exceptions::InvalidArgumentException, "Cannot abstract from meta variable '" << metaVariable.getName() << "' that is not present in the DD."); - newMetaVariables.erase(metaVariable); - - DdMetaVariable const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable); - cubeDd *= ddMetaVariable.getCubeAsMtbdd(); - } - - return Dd(this->getDdManager(), this->getCuddMtbdd().MaxAbstract(cubeDd.getCuddMtbdd()), newMetaVariables); - } - - bool Dd::equalModuloPrecision(Dd const& other, double precision, bool relative) const { - STORM_LOG_WARN_COND(this->isMtbdd(), "Performing arithmetical operation on BDD(s)."); - - if (relative) { - return this->getCuddMtbdd().EqualSupNormRel(other.getCuddMtbdd(), precision); - } else { - return this->getCuddMtbdd().EqualSupNorm(other.getCuddMtbdd(), precision); - } - } - - Dd Dd::swapVariables(std::vector> const& metaVariablePairs) { - std::set newContainedMetaVariables; - if (this->isBdd()) { - std::vector from; - std::vector to; - for (auto const& metaVariablePair : metaVariablePairs) { - DdMetaVariable const& variable1 = this->getDdManager()->getMetaVariable(metaVariablePair.first); - DdMetaVariable const& variable2 = this->getDdManager()->getMetaVariable(metaVariablePair.second); - - // Check if it's legal so swap the meta variables. - STORM_LOG_THROW(variable1.getNumberOfDdVariables() == variable2.getNumberOfDdVariables(), storm::exceptions::InvalidArgumentException, "Unable to swap meta variables with different size."); - - // Keep track of the contained meta variables in the DD. - if (this->containsMetaVariable(metaVariablePair.first)) { - newContainedMetaVariables.insert(metaVariablePair.second); - } - if (this->containsMetaVariable(metaVariablePair.second)) { - newContainedMetaVariables.insert(metaVariablePair.first); - } - - // Add the variables to swap to the corresponding vectors. - for (auto const& ddVariable : variable1.getDdVariables()) { - from.push_back(ddVariable.getCuddBdd()); - } - for (auto const& ddVariable : variable2.getDdVariables()) { - to.push_back(ddVariable.getCuddBdd()); - } - } - - // Finally, call CUDD to swap the variables. - return Dd(this->getDdManager(), this->getCuddBdd().SwapVariables(from, to), newContainedMetaVariables); - } else { - std::vector from; - std::vector to; - for (auto const& metaVariablePair : metaVariablePairs) { - DdMetaVariable const& variable1 = this->getDdManager()->getMetaVariable(metaVariablePair.first); - DdMetaVariable const& variable2 = this->getDdManager()->getMetaVariable(metaVariablePair.second); - - // Check if it's legal so swap the meta variables. - if (variable1.getNumberOfDdVariables() != variable2.getNumberOfDdVariables()) { - throw storm::exceptions::InvalidArgumentException() << "Unable to swap meta variables with different size."; - } - - // Keep track of the contained meta variables in the DD. - if (this->containsMetaVariable(metaVariablePair.first)) { - newContainedMetaVariables.insert(metaVariablePair.second); - } - if (this->containsMetaVariable(metaVariablePair.second)) { - newContainedMetaVariables.insert(metaVariablePair.first); - } - - // Add the variables to swap to the corresponding vectors. - for (auto const& ddVariable : variable1.getDdVariables()) { - from.push_back(ddVariable.getCuddMtbdd()); - } - for (auto const& ddVariable : variable2.getDdVariables()) { - to.push_back(ddVariable.getCuddMtbdd()); - } - } - - // Finally, call CUDD to swap the variables. - return Dd(this->getDdManager(), this->getCuddMtbdd().SwapVariables(from, to), newContainedMetaVariables); - } - } - - Dd Dd::multiplyMatrix(Dd const& otherMatrix, std::set const& summationMetaVariables) const { - STORM_LOG_WARN_COND(this->isMtbdd() && otherMatrix.isMtbdd(), "Performing arithmetical operation on BDD(s)."); - - // Create the CUDD summation variables. - std::vector summationDdVariables; - for (auto const& metaVariable : summationMetaVariables) { - for (auto const& ddVariable : this->getDdManager()->getMetaVariable(metaVariable).getDdVariables()) { - summationDdVariables.push_back(ddVariable.getCuddMtbdd()); - } - } - - std::set unionOfMetaVariables; - std::set_union(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end(), otherMatrix.getContainedMetaVariables().begin(), otherMatrix.getContainedMetaVariables().end(), std::inserter(unionOfMetaVariables, unionOfMetaVariables.begin())); - std::set containedMetaVariables; - std::set_difference(unionOfMetaVariables.begin(), unionOfMetaVariables.end(), summationMetaVariables.begin(), summationMetaVariables.end(), std::inserter(containedMetaVariables, containedMetaVariables.begin())); - - return Dd(this->getDdManager(), this->getCuddMtbdd().MatrixMultiply(otherMatrix.getCuddMtbdd(), summationDdVariables), containedMetaVariables); - } - - Dd Dd::andExists(Dd const& other, std::set const& existentialVariables) const { - STORM_LOG_WARN_COND(this->isBdd() && other.isBdd(), "Performing logical operation on MTBDD(s)."); - - Dd cubeDd(this->getDdManager()->getOne()); - for (auto const& metaVariable : existentialVariables) { - DdMetaVariable const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable); - cubeDd &= ddMetaVariable.getCube(); - } - - std::set unionOfMetaVariables; - std::set_union(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end(), other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end(), std::inserter(unionOfMetaVariables, unionOfMetaVariables.begin())); - std::set containedMetaVariables; - std::set_difference(unionOfMetaVariables.begin(), unionOfMetaVariables.end(), existentialVariables.begin(), existentialVariables.end(), std::inserter(containedMetaVariables, containedMetaVariables.begin())); - - return Dd(this->getDdManager(), this->getCuddBdd().AndAbstract(other.getCuddBdd(), cubeDd.getCuddBdd()), containedMetaVariables); - } - - Dd Dd::greater(double value) const { - STORM_LOG_WARN_COND(this->isMtbdd(), "Performing arithmetical operation on BDD(s)."); - return Dd(this->getDdManager(), this->getCuddMtbdd().BddStrictThreshold(value), this->getContainedMetaVariables()); - } - - Dd Dd::greaterOrEqual(double value) const { - STORM_LOG_WARN_COND(this->isMtbdd(), "Performing arithmetical operation on BDD(s)."); - return Dd(this->getDdManager(), this->getCuddMtbdd().BddThreshold(value), this->getContainedMetaVariables()); - } - - Dd Dd::notZero() const { - return this->toBdd(); - } - - Dd Dd::constrain(Dd const& constraint) const { - std::set metaVariables(this->getContainedMetaVariables()); - metaVariables.insert(constraint.getContainedMetaVariables().begin(), constraint.getContainedMetaVariables().end()); - - if (this->isBdd() && constraint.isBdd()) { - return Dd(this->getDdManager(), this->getCuddBdd().Constrain(constraint.getCuddBdd()), metaVariables); - } else { - return Dd(this->getDdManager(), this->getCuddMtbdd().Constrain(constraint.getCuddMtbdd()), metaVariables); - } - } - - Dd Dd::restrict(Dd const& constraint) const { - std::set metaVariables(this->getContainedMetaVariables()); - metaVariables.insert(constraint.getContainedMetaVariables().begin(), constraint.getContainedMetaVariables().end()); - - if (this->isBdd() && constraint.isBdd()) { - return Dd(this->getDdManager(), this->getCuddBdd().Restrict(constraint.getCuddBdd()), metaVariables); - } else { - return Dd(this->getDdManager(), this->getCuddMtbdd().Restrict(constraint.getCuddMtbdd()), metaVariables); - } - } - - Dd Dd::getSupport() const { - if (this->isBdd()) { - return Dd(this->getDdManager(), this->getCuddBdd().Support(), this->getContainedMetaVariables()); - } else { - return Dd(this->getDdManager(), this->getCuddMtbdd().Support(), this->getContainedMetaVariables()); - } - } - - uint_fast64_t Dd::getNonZeroCount() const { - std::size_t numberOfDdVariables = 0; - for (auto const& metaVariable : this->getContainedMetaVariables()) { - numberOfDdVariables += this->getDdManager()->getMetaVariable(metaVariable).getNumberOfDdVariables(); - } - if (this->isBdd()) { - return static_cast(this->getCuddBdd().CountMinterm(static_cast(numberOfDdVariables))); - } else { - return static_cast(this->getCuddMtbdd().CountMinterm(static_cast(numberOfDdVariables))); - } - } - - uint_fast64_t Dd::getLeafCount() const { - if (this->isBdd()) { - return static_cast(this->getCuddBdd().CountLeaves()); - } else { - return static_cast(this->getCuddMtbdd().CountLeaves()); - } - } - - uint_fast64_t Dd::getNodeCount() const { - if (this->isBdd()) { - return static_cast(this->getCuddBdd().nodeCount()); - } else { - return static_cast(this->getCuddMtbdd().nodeCount()); - } - } - - double Dd::getMin() const { - STORM_LOG_WARN_COND(this->isMtbdd(), "Performing arithmetical operation on BDD(s)."); - - ADD constantMinAdd = this->getCuddMtbdd().FindMin(); - return static_cast(Cudd_V(constantMinAdd.getNode())); - } - - double Dd::getMax() const { - STORM_LOG_WARN_COND(this->isMtbdd(), "Performing arithmetical operation on BDD(s)."); - - ADD constantMaxAdd = this->getCuddMtbdd().FindMax(); - return static_cast(Cudd_V(constantMaxAdd.getNode())); - } - - void Dd::setValue(storm::expressions::Variable const& metaVariable, int_fast64_t variableValue, double targetValue) { - std::map metaVariableToValueMap; - metaVariableToValueMap.emplace(metaVariable, variableValue); - this->setValue(metaVariableToValueMap, targetValue); - } - - void Dd::setValue(storm::expressions::Variable const& metaVariable1, int_fast64_t variableValue1, storm::expressions::Variable const& metaVariable2, int_fast64_t variableValue2, double targetValue) { - std::map metaVariableToValueMap; - metaVariableToValueMap.emplace(metaVariable1, variableValue1); - metaVariableToValueMap.emplace(metaVariable2, variableValue2); - this->setValue(metaVariableToValueMap, targetValue); - } - - void Dd::setValue(std::map const& metaVariableToValueMap, double targetValue) { - if (this->isBdd()) { - STORM_LOG_THROW(targetValue == storm::utility::zero() || targetValue == storm::utility::one(), storm::exceptions::InvalidArgumentException, "Cannot set encoding to non-0, non-1 value " << targetValue << " in BDD."); - Dd valueEncoding(this->getDdManager()->getOne()); - for (auto const& nameValuePair : metaVariableToValueMap) { - valueEncoding &= this->getDdManager()->getEncoding(nameValuePair.first, nameValuePair.second); - // Also record that the DD now contains the meta variable. - this->addContainedMetaVariable(nameValuePair.first); - } - if (targetValue == storm::utility::one()) { - this->cuddDd = valueEncoding.getCuddBdd().Ite(this->getDdManager()->getOne().getCuddBdd(), this->getCuddBdd()); - } else { - this->cuddDd = valueEncoding.getCuddBdd().Ite(this->getDdManager()->getZero().getCuddBdd(), this->getCuddBdd()); - } - } else { - Dd valueEncoding(this->getDdManager()->getOne()); - for (auto const& nameValuePair : metaVariableToValueMap) { - valueEncoding &= this->getDdManager()->getEncoding(nameValuePair.first, nameValuePair.second); - // Also record that the DD now contains the meta variable. - this->addContainedMetaVariable(nameValuePair.first); - } - this->cuddDd = valueEncoding.toMtbdd().getCuddMtbdd().Ite(this->getDdManager()->getConstant(targetValue).getCuddMtbdd(), this->getCuddMtbdd()); - } - } - - double Dd::getValue(std::map const& metaVariableToValueMap) const { - std::set remainingMetaVariables(this->getContainedMetaVariables()); - Dd valueEncoding(this->getDdManager()->getOne()); - for (auto const& nameValuePair : metaVariableToValueMap) { - valueEncoding &= this->getDdManager()->getEncoding(nameValuePair.first, nameValuePair.second); - if (this->containsMetaVariable(nameValuePair.first)) { - remainingMetaVariables.erase(nameValuePair.first); - } - } - - STORM_LOG_THROW(remainingMetaVariables.empty(), storm::exceptions::InvalidArgumentException, "Cannot evaluate function for which not all inputs were given."); - - if (this->isBdd()) { - Dd value = *this && valueEncoding; - return value.isZero() ? 0 : 1; - } else { - Dd value = *this * valueEncoding.toMtbdd(); - value = value.sumAbstract(this->getContainedMetaVariables()); - return static_cast(Cudd_V(value.getCuddMtbdd().getNode())); - } - } - - bool Dd::isOne() const { - if (this->isBdd()) { - return this->getCuddBdd().IsOne(); - } else { - return this->getCuddMtbdd().IsOne(); - } - } - - bool Dd::isZero() const { - if (this->isBdd()) { - return this->getCuddBdd().IsZero(); - } else { - return this->getCuddMtbdd().IsZero(); - } - } - - bool Dd::isConstant() const { - if (this->isBdd()) { - return Cudd_IsConstant(this->getCuddBdd().getNode()); - } else { - return Cudd_IsConstant(this->getCuddMtbdd().getNode()); - } - } - - uint_fast64_t Dd::getIndex() const { - if (this->isBdd()) { - return static_cast(this->getCuddBdd().NodeReadIndex()); - } else { - return static_cast(this->getCuddMtbdd().NodeReadIndex()); - } - } - - template - std::vector Dd::toVector() const { - STORM_LOG_THROW(this->isMtbdd(), storm::exceptions::IllegalFunctionCallException, "Cannot create vector from BDD."); - return this->toVector(Odd(*this)); - } - - template - std::vector Dd::toVector(Odd const& rowOdd) const { - STORM_LOG_THROW(this->isMtbdd(), storm::exceptions::IllegalFunctionCallException, "Cannot create vector from BDD."); - std::vector result(rowOdd.getTotalOffset()); - std::vector ddVariableIndices = this->getSortedVariableIndices(); - addToVectorRec(this->getCuddDdNode(), 0, ddVariableIndices.size(), 0, rowOdd, ddVariableIndices, result); - return result; - } - - storm::storage::SparseMatrix Dd::toMatrix() const { - STORM_LOG_THROW(this->isMtbdd(), storm::exceptions::IllegalFunctionCallException, "Cannot create matrix from BDD."); - std::set rowVariables; - std::set columnVariables; - - for (auto const& variable : this->getContainedMetaVariables()) { - if (variable.getName().size() > 0 && variable.getName().back() == '\'') { - columnVariables.insert(variable); - } else { - rowVariables.insert(variable); - } - } - - return toMatrix(rowVariables, columnVariables, Odd(this->existsAbstract(rowVariables)), Odd(this->existsAbstract(columnVariables))); - } - - storm::storage::SparseMatrix Dd::toMatrix(storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const { - STORM_LOG_THROW(this->isMtbdd(), storm::exceptions::IllegalFunctionCallException, "Cannot create matrix from BDD."); - std::set rowMetaVariables; - std::set columnMetaVariables; - - for (auto const& variable : this->getContainedMetaVariables()) { - if (variable.getName().size() > 0 && variable.getName().back() == '\'') { - columnMetaVariables.insert(variable); - } else { - rowMetaVariables.insert(variable); - } - } - - return toMatrix(rowMetaVariables, columnMetaVariables, rowOdd, columnOdd); - } - - storm::storage::SparseMatrix Dd::toMatrix(std::set const& rowMetaVariables, std::set const& columnMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const { - STORM_LOG_THROW(this->isMtbdd(), storm::exceptions::IllegalFunctionCallException, "Cannot create matrix from BDD."); - std::vector ddRowVariableIndices; - std::vector ddColumnVariableIndices; - - for (auto const& variable : rowMetaVariables) { - DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(variable); - for (auto const& ddVariable : metaVariable.getDdVariables()) { - ddRowVariableIndices.push_back(ddVariable.getIndex()); - } - } - for (auto const& variable : columnMetaVariables) { - DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(variable); - for (auto const& ddVariable : metaVariable.getDdVariables()) { - ddColumnVariableIndices.push_back(ddVariable.getIndex()); - } - } - - // Prepare the vectors that represent the matrix. - std::vector rowIndications(rowOdd.getTotalOffset() + 1); - std::vector> columnsAndValues(this->getNonZeroCount()); - - // Create a trivial row grouping. - std::vector trivialRowGroupIndices(rowIndications.size()); - uint_fast64_t i = 0; - for (auto& entry : trivialRowGroupIndices) { - entry = i; - ++i; - } - - // Use the toMatrixRec function to compute the number of elements in each row. Using the flag, we prevent - // it from actually generating the entries in the entry vector. - toMatrixRec(this->getCuddDdNode(), rowIndications, columnsAndValues, trivialRowGroupIndices, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices, false); - - // TODO: counting might be faster by just summing over the primed variables and then using the ODD to convert - // the resulting (DD) vector to an explicit vector. - - // Now that we computed the number of entries in each row, compute the corresponding offsets in the entry vector. - uint_fast64_t tmp = 0; - uint_fast64_t tmp2 = 0; - for (uint_fast64_t i = 1; i < rowIndications.size(); ++i) { - tmp2 = rowIndications[i]; - rowIndications[i] = rowIndications[i - 1] + tmp; - std::swap(tmp, tmp2); - } - rowIndications[0] = 0; - - // Now actually fill the entry vector. - toMatrixRec(this->getCuddDdNode(), rowIndications, columnsAndValues, trivialRowGroupIndices, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices, true); - - // Since the last call to toMatrixRec modified the rowIndications, we need to restore the correct values. - for (uint_fast64_t i = rowIndications.size() - 1; i > 0; --i) { - rowIndications[i] = rowIndications[i - 1]; - } - rowIndications[0] = 0; - - // Construct matrix and return result. - return storm::storage::SparseMatrix(columnOdd.getTotalOffset(), std::move(rowIndications), std::move(columnsAndValues), std::move(trivialRowGroupIndices)); - } - - storm::storage::SparseMatrix Dd::toMatrix(std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const { - STORM_LOG_THROW(this->isMtbdd(), storm::exceptions::IllegalFunctionCallException, "Cannot create matrix from BDD."); - std::vector ddRowVariableIndices; - std::vector ddColumnVariableIndices; - std::vector ddGroupVariableIndices; - std::set rowAndColumnMetaVariables; - - for (auto const& variable : rowMetaVariables) { - DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(variable); - for (auto const& ddVariable : metaVariable.getDdVariables()) { - ddRowVariableIndices.push_back(ddVariable.getIndex()); - } - rowAndColumnMetaVariables.insert(variable); - } - for (auto const& variable : columnMetaVariables) { - DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(variable); - for (auto const& ddVariable : metaVariable.getDdVariables()) { - ddColumnVariableIndices.push_back(ddVariable.getIndex()); - } - rowAndColumnMetaVariables.insert(variable); - } - for (auto const& variable : groupMetaVariables) { - DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(variable); - for (auto const& ddVariable : metaVariable.getDdVariables()) { - ddGroupVariableIndices.push_back(ddVariable.getIndex()); - } - } - - // TODO: assert that the group variables are at the very top of the variable ordering? - - // Start by computing the offsets (in terms of rows) for each row group. - Dd stateToNumberOfChoices = this->notZero().existsAbstract(columnMetaVariables).sumAbstract(groupMetaVariables); - std::vector rowGroupIndices = stateToNumberOfChoices.toVector(rowOdd); - rowGroupIndices.resize(rowGroupIndices.size() + 1); - uint_fast64_t tmp = 0; - uint_fast64_t tmp2 = 0; - for (uint_fast64_t i = 1; i < rowGroupIndices.size(); ++i) { - tmp2 = rowGroupIndices[i]; - rowGroupIndices[i] = rowGroupIndices[i - 1] + tmp; - std::swap(tmp, tmp2); - } - rowGroupIndices[0] = 0; - - // Next, we split the matrix into one for each group. This only works if the group variables are at the very - // top. - std::vector> groups; - splitGroupsRec(this->getCuddDdNode(), groups, ddGroupVariableIndices, 0, ddGroupVariableIndices.size(), rowAndColumnMetaVariables); - - // Create the actual storage for the non-zero entries. - std::vector> columnsAndValues(this->getNonZeroCount()); - - // Now compute the indices at which the individual rows start. - std::vector rowIndications(rowGroupIndices.back() + 1); - std::vector> statesWithGroupEnabled(groups.size()); - for (uint_fast64_t i = 0; i < groups.size(); ++i) { - auto const& dd = groups[i]; - - toMatrixRec(dd.getCuddDdNode(), rowIndications, columnsAndValues, rowGroupIndices, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices, false); - - statesWithGroupEnabled[i] = dd.notZero().existsAbstract(columnMetaVariables); - addToVectorRec(statesWithGroupEnabled[i].getCuddDdNode(), 0, ddRowVariableIndices.size(), 0, rowOdd, ddRowVariableIndices, rowGroupIndices); - } - - // Since we modified the rowGroupIndices, we need to restore the correct values. - for (uint_fast64_t i = rowGroupIndices.size() - 1; i > 0; --i) { - rowGroupIndices[i] = rowGroupIndices[i - 1]; - } - rowGroupIndices[0] = 0; - - // Now that we computed the number of entries in each row, compute the corresponding offsets in the entry vector. - tmp = 0; - tmp2 = 0; - for (uint_fast64_t i = 1; i < rowIndications.size(); ++i) { - tmp2 = rowIndications[i]; - rowIndications[i] = rowIndications[i - 1] + tmp; - std::swap(tmp, tmp2); - } - rowIndications[0] = 0; - - // Now actually fill the entry vector. - for (uint_fast64_t i = 0; i < groups.size(); ++i) { - auto const& dd = groups[i]; - - toMatrixRec(dd.getCuddDdNode(), rowIndications, columnsAndValues, rowGroupIndices, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices, true); - - addToVectorRec(statesWithGroupEnabled[i].getCuddDdNode(), 0, ddRowVariableIndices.size(), 0, rowOdd, ddRowVariableIndices, rowGroupIndices); - } - - // Since we modified the rowGroupIndices, we need to restore the correct values. - for (uint_fast64_t i = rowGroupIndices.size() - 1; i > 0; --i) { - rowGroupIndices[i] = rowGroupIndices[i - 1]; - } - rowGroupIndices[0] = 0; - - // Since the last call to toMatrixRec modified the rowIndications, we need to restore the correct values. - for (uint_fast64_t i = rowIndications.size() - 1; i > 0; --i) { - rowIndications[i] = rowIndications[i - 1]; - } - rowIndications[0] = 0; - - return storm::storage::SparseMatrix(columnOdd.getTotalOffset(), std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices)); - } - - void Dd::toMatrixRec(DdNode const* dd, std::vector& rowIndications, std::vector>& columnsAndValues, std::vector const& rowGroupOffsets, Odd const& rowOdd, Odd const& columnOdd, uint_fast64_t currentRowLevel, uint_fast64_t currentColumnLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, uint_fast64_t currentColumnOffset, std::vector const& ddRowVariableIndices, std::vector const& ddColumnVariableIndices, bool generateValues) const { - // For the empty DD, we do not need to add any entries. - if (dd == Cudd_ReadZero(this->getDdManager()->getCuddManager().getManager())) { - return; - } - - // If we are at the maximal level, the value to be set is stored as a constant in the DD. - if (currentRowLevel + currentColumnLevel == maxLevel) { - if (generateValues) { - columnsAndValues[rowIndications[rowGroupOffsets[currentRowOffset]]] = storm::storage::MatrixEntry(currentColumnOffset, Cudd_V(dd)); - } - ++rowIndications[rowGroupOffsets[currentRowOffset]]; - } else { - DdNode const* elseElse; - DdNode const* elseThen; - DdNode const* thenElse; - DdNode const* thenThen; - - if (ddColumnVariableIndices[currentColumnLevel] < dd->index) { - elseElse = elseThen = thenElse = thenThen = dd; - } else if (ddRowVariableIndices[currentColumnLevel] < dd->index) { - elseElse = thenElse = Cudd_E(dd); - elseThen = thenThen = Cudd_T(dd); - } else { - DdNode const* elseNode = Cudd_E(dd); - if (ddColumnVariableIndices[currentColumnLevel] < elseNode->index) { - elseElse = elseThen = elseNode; - } else { - elseElse = Cudd_E(elseNode); - elseThen = Cudd_T(elseNode); - } - - DdNode const* thenNode = Cudd_T(dd); - if (ddColumnVariableIndices[currentColumnLevel] < thenNode->index) { - thenElse = thenThen = thenNode; - } else { - thenElse = Cudd_E(thenNode); - thenThen = Cudd_T(thenNode); - } - } - - // Visit else-else. - toMatrixRec(elseElse, rowIndications, columnsAndValues, rowGroupOffsets, rowOdd.getElseSuccessor(), columnOdd.getElseSuccessor(), currentRowLevel + 1, currentColumnLevel + 1, maxLevel, currentRowOffset, currentColumnOffset, ddRowVariableIndices, ddColumnVariableIndices, generateValues); - // Visit else-then. - toMatrixRec(elseThen, rowIndications, columnsAndValues, rowGroupOffsets, rowOdd.getElseSuccessor(), columnOdd.getThenSuccessor(), currentRowLevel + 1, currentColumnLevel + 1, maxLevel, currentRowOffset, currentColumnOffset + columnOdd.getElseOffset(), ddRowVariableIndices, ddColumnVariableIndices, generateValues); - // Visit then-else. - toMatrixRec(thenElse, rowIndications, columnsAndValues, rowGroupOffsets, rowOdd.getThenSuccessor(), columnOdd.getElseSuccessor(), currentRowLevel + 1, currentColumnLevel + 1, maxLevel, currentRowOffset + rowOdd.getElseOffset(), currentColumnOffset, ddRowVariableIndices, ddColumnVariableIndices, generateValues); - // Visit then-then. - toMatrixRec(thenThen, rowIndications, columnsAndValues, rowGroupOffsets, rowOdd.getThenSuccessor(), columnOdd.getThenSuccessor(), currentRowLevel + 1, currentColumnLevel + 1, maxLevel, currentRowOffset + rowOdd.getElseOffset(), currentColumnOffset + columnOdd.getElseOffset(), ddRowVariableIndices, ddColumnVariableIndices, generateValues); - } - } - - void Dd::splitGroupsRec(DdNode* dd, std::vector>& groups, std::vector const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::set const& remainingMetaVariables) const { - // For the empty DD, we do not need to create a group. - if (dd == Cudd_ReadZero(this->getDdManager()->getCuddManager().getManager())) { - return; - } - - if (currentLevel == maxLevel) { - groups.push_back(Dd(this->getDdManager(), ADD(this->getDdManager()->getCuddManager(), dd), remainingMetaVariables)); - } else if (ddGroupVariableIndices[currentLevel] < dd->index) { - splitGroupsRec(dd, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel, remainingMetaVariables); - splitGroupsRec(dd, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel, remainingMetaVariables); - } else { - splitGroupsRec(Cudd_E(dd), groups, ddGroupVariableIndices, currentLevel + 1, maxLevel, remainingMetaVariables); - splitGroupsRec(Cudd_T(dd), groups, ddGroupVariableIndices, currentLevel + 1, maxLevel, remainingMetaVariables); - } - } - - template - void Dd::addToVectorRec(DdNode const* dd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector) const { - // For the empty DD, we do not need to add any entries. - if (dd == Cudd_ReadZero(this->getDdManager()->getCuddManager().getManager())) { - return; - } - - // If we are at the maximal level, the value to be set is stored as a constant in the DD. - if (currentLevel == maxLevel) { - targetVector[currentOffset] += static_cast(Cudd_V(dd)); - } else if (ddVariableIndices[currentLevel] < dd->index) { - // If we skipped a level, we need to enumerate the explicit entries for the case in which the bit is set - // and for the one in which it is not set. - addToVectorRec(dd, currentLevel + 1, maxLevel, currentOffset, odd.getElseSuccessor(), ddVariableIndices, targetVector); - addToVectorRec(dd, currentLevel + 1, maxLevel, currentOffset + odd.getElseOffset(), odd.getThenSuccessor(), ddVariableIndices, targetVector); - } else { - // Otherwise, we simply recursively call the function for both (different) cases. - addToVectorRec(Cudd_E(dd), currentLevel + 1, maxLevel, currentOffset, odd.getElseSuccessor(), ddVariableIndices, targetVector); - addToVectorRec(Cudd_T(dd), currentLevel + 1, maxLevel, currentOffset + odd.getElseOffset(), odd.getThenSuccessor(), ddVariableIndices, targetVector); - } - } - - std::vector Dd::getSortedVariableIndices() const { - std::vector ddVariableIndices; - for (auto const& metaVariableName : this->getContainedMetaVariables()) { - auto const& metaVariable = this->getDdManager()->getMetaVariable(metaVariableName); - for (auto const& ddVariable : metaVariable.getDdVariables()) { - ddVariableIndices.push_back(ddVariable.getIndex()); - } - } - - // Next, we need to sort them, since they may be arbitrarily ordered otherwise. - std::sort(ddVariableIndices.begin(), ddVariableIndices.end()); - return ddVariableIndices; - } - bool Dd::containsMetaVariable(storm::expressions::Variable const& metaVariable) const { return containedMetaVariables.find(metaVariable) != containedMetaVariables.end(); } bool Dd::containsMetaVariables(std::set const& metaVariables) const { - for (auto const& metaVariable : metaVariables) { - auto const& ddMetaVariable = containedMetaVariables.find(metaVariable); - - if (ddMetaVariable == containedMetaVariables.end()) { - return false; - } - } - return true; + return std::includes(containedMetaVariables.begin(), containedMetaVariables.end(), metaVariables.begin(), metaVariables.end()); } std::set const& Dd::getContainedMetaVariables() const { @@ -1045,130 +25,28 @@ namespace storm { return this->containedMetaVariables; } - void Dd::exportToDot(std::string const& filename) const { - if (filename.empty()) { - if (this->isBdd()) { - std::vector cuddBddVector = { this->getCuddBdd() }; - this->getDdManager()->getCuddManager().DumpDot(cuddBddVector); - } else { - std::vector cuddAddVector = { this->getCuddMtbdd() }; - this->getDdManager()->getCuddManager().DumpDot(cuddAddVector); - } - } else { - // Build the name input of the DD. - std::vector ddNames; - std::string ddName("f"); - ddNames.push_back(new char[ddName.size() + 1]); - std::copy(ddName.c_str(), ddName.c_str() + 2, ddNames.back()); - - // Now build the variables names. - std::vector ddVariableNamesAsStrings = this->getDdManager()->getDdVariableNames(); - std::vector ddVariableNames; - for (auto const& element : ddVariableNamesAsStrings) { - ddVariableNames.push_back(new char[element.size() + 1]); - std::copy(element.c_str(), element.c_str() + element.size() + 1, ddVariableNames.back()); - } - - // Open the file, dump the DD and close it again. - FILE* filePointer = fopen(filename.c_str() , "w"); - if (this->isBdd()) { - std::vector cuddBddVector = { this->getCuddBdd() }; - this->getDdManager()->getCuddManager().DumpDot(cuddBddVector, &ddVariableNames[0], &ddNames[0], filePointer); - } else { - std::vector cuddAddVector = { this->getCuddMtbdd() }; - this->getDdManager()->getCuddManager().DumpDot(cuddAddVector, &ddVariableNames[0], &ddNames[0], filePointer); - } - fclose(filePointer); - - // Finally, delete the names. - for (char* element : ddNames) { - delete element; - } - for (char* element : ddVariableNames) { - delete element; - } - } - } - - void Dd::addContainedMetaVariable(storm::expressions::Variable const& metaVariable) { - this->getContainedMetaVariables().insert(metaVariable); - } - - void Dd::removeContainedMetaVariable(storm::expressions::Variable const& metaVariable) { - this->getContainedMetaVariables().erase(metaVariable); - } - std::shared_ptr const> Dd::getDdManager() const { return this->ddManager; } - - DdForwardIterator Dd::begin(bool enumerateDontCareMetaVariables) const { - int* cube; - double value; - DdGen* generator = this->getCuddDd().FirstCube(&cube, &value); - return DdForwardIterator(this->getDdManager(), generator, cube, value, (Cudd_IsGenEmpty(generator) != 0), &this->getContainedMetaVariables(), enumerateDontCareMetaVariables); - } - - DdForwardIterator Dd::end(bool enumerateDontCareMetaVariables) const { - return DdForwardIterator(this->getDdManager(), nullptr, nullptr, 0, true, nullptr, enumerateDontCareMetaVariables); - } - - storm::expressions::Expression Dd::toExpression() const { - return toExpressionRecur(this->getCuddDdNode(), this->getDdManager()->getDdVariables()); - } - - storm::expressions::Expression Dd::getMintermExpression() const { - // Note that we first transform the ADD into a BDD to convert all non-zero terminals to ones and therefore - // make the DD more compact. - return getMintermExpressionRecur(this->getDdManager()->getCuddManager().getManager(), this->toBdd().getCuddDdNode(), this->getDdManager()->getDdVariables()); + + void Dd::addMetaVariables(std::set const& metaVariables) { + std::set result; + std::set_union(containedMetaVariables.begin(), containedMetaVariables.end(), metaVariables.begin(), metaVariables.end(), std::inserter(result, result.begin())); + containedMetaVariables = std::move(result); } - - storm::expressions::Expression Dd::toExpressionRecur(DdNode const* dd, std::vector const& variables) { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This feature is currently unavailable."); - // If the DD is a terminal node, we can simply return a constant expression. -// if (Cudd_IsConstant(dd)) { -// return storm::expressions::Expression::createDoubleLiteral(static_cast(Cudd_V(dd))); -// } else { -// return storm::expressions::Expression::createBooleanVariable(variableNames[dd->index]).ite(toExpressionRecur(Cudd_T(dd), variableNames), toExpressionRecur(Cudd_E(dd), variableNames)); -// } + + void Dd::addMetaVariable(storm::expressions::Variable const& metaVariable) { + this->getContainedMetaVariables().insert(metaVariable); } - - storm::expressions::Expression Dd::getMintermExpressionRecur(::DdManager* manager, DdNode const* dd, std::vector const& variables) { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This feature is currently unavailable."); - // If the DD is a terminal node, we can simply return a constant expression. -// if (Cudd_IsConstant(dd)) { -// if (Cudd_IsComplement(dd)) { -// return storm::expressions::Expression::createBooleanLiteral(false); -// } else { -// return storm::expressions::Expression::createBooleanLiteral((dd == Cudd_ReadOne(manager)) ? true : false); -// } -// } else { -// // Get regular versions of the pointers. -// DdNode* regularDd = Cudd_Regular(dd); -// DdNode* thenDd = Cudd_T(regularDd); -// DdNode* elseDd = Cudd_E(regularDd); -// -// // Compute expression recursively. -// storm::expressions::Expression result = storm::expressions::Expression::createBooleanVariable(variableNames[dd->index]).ite(getMintermExpressionRecur(manager, thenDd, variableNames), getMintermExpressionRecur(manager, elseDd, variableNames)); -// if (Cudd_IsComplement(dd)) { -// result = !result; -// } -// -// return result; -// } + + void Dd::removeMetaVariable(storm::expressions::Variable const& metaVariable) { + this->getContainedMetaVariables().erase(metaVariable); } - - std::ostream& operator<<(std::ostream& out, const Dd& dd) { - dd.exportToDot(); - return out; + + void Dd::removeMetaVariables(std::set const& metaVariables) { + std::set result; + std::set_difference(containedMetaVariables.begin(), containedMetaVariables.end(), metaVariables.begin(), metaVariables.end(), std::inserter(result, result.begin())); + containedMetaVariables = std::move(result); } - - // Explicitly instantiate some templated functions. - template std::vector Dd::toVector() const; - template std::vector Dd::toVector(Odd const& rowOdd) const; - template void Dd::addToVectorRec(DdNode const* dd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector) const; - template std::vector Dd::toVector() const; - template std::vector Dd::toVector(Odd const& rowOdd) const; - template void Dd::addToVectorRec(DdNode const* dd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector) const; } } \ No newline at end of file diff --git a/src/storage/dd/CuddDd.h b/src/storage/dd/CuddDd.h index fadbe06a9..197d2454c 100644 --- a/src/storage/dd/CuddDd.h +++ b/src/storage/dd/CuddDd.h @@ -1,16 +1,10 @@ #ifndef STORM_STORAGE_DD_CUDDDD_H_ #define STORM_STORAGE_DD_CUDDDD_H_ -#include #include #include -#include -#include #include "src/storage/dd/Dd.h" -#include "src/storage/dd/CuddDdForwardIterator.h" -#include "src/storage/SparseMatrix.h" -#include "src/storage/expressions/Expression.h" #include "src/storage/expressions/Variable.h" #include "src/utility/OsDetection.h" @@ -22,14 +16,13 @@ namespace storm { // Forward-declare some classes. template class DdManager; template class Odd; + template class Bdd; template<> class Dd { public: - // Declare the DdManager and DdIterator class as friend so it can access the internals of a DD. + // Declare the DdManager so it can access the internals of a DD. friend class DdManager; - friend class DdForwardIterator; - friend class Odd; // Instantiate all copy/move constructors/assignments with the default implementation. Dd() = default; @@ -40,540 +33,40 @@ namespace storm { Dd& operator=(Dd&& other) = default; #endif - /*! - * Retrieves whether the two DDs represent the same function. - * - * @param other The DD that is to be compared with the current one. - * @return True if the DDs represent the same function. - */ - bool operator==(Dd const& other) const; - - /*! - * Retrieves whether the two DDs represent different functions. - * - * @param other The DD that is to be compared with the current one. - * @return True if the DDs represent the different functions. - */ - bool operator!=(Dd const& other) const; - - /*! - * Performs an if-then-else with the given operands, i.e. maps all valuations that are mapped to a non-zero - * function value to the function values specified by the first DD and all others to the function values - * specified by the second DD. - */ - Dd ite(Dd const& thenDd, Dd const& elseDd) const; - - /*! - * Performs a logical or of the current and the given DD. - * - * @param other The second DD used for the operation. - * @return The logical or of the operands. - */ - Dd operator||(Dd const& other) const; - - /*! - * Performs a logical or of the current and the given DD and assigns it to the current DD. - * - * @param other The second DD used for the operation. - * @return A reference to the current DD after the operation - */ - Dd& operator|=(Dd const& other); - - /*! - * Performs a logical and of the current and the given DD. - * - * @param other The second DD used for the operation. - * @return The logical and of the operands. - */ - Dd operator&&(Dd const& other) const; - - /*! - * Performs a logical and of the current and the given DD and assigns it to the current DD. - * - * @param other The second DD used for the operation. - * @return A reference to the current DD after the operation - */ - Dd& operator&=(Dd const& other); - - /*! - * Performs a logical iff of the current and the given DD. - * - * @param other The second DD used for the operation. - * @return The logical iff of the operands. - */ - Dd iff(Dd const& other) const; - - /*! - * Performs a logical exclusive-or of the current and the given DD. - * - * @param other The second DD used for the operation. - * @return The logical exclusive-or of the operands. - */ - Dd exclusiveOr(Dd const& other) const; - - /*! - * Performs a logical implication of the current and the given DD. - * - * @param other The second DD used for the operation. - * @return The logical implication of the operands. - */ - Dd implies(Dd const& other) const; - - /*! - * Adds the two DDs. - * - * @param other The DD to add to the current one. - * @return The result of the addition. - */ - Dd operator+(Dd const& other) const; - - /*! - * Adds the given DD to the current one. - * - * @param other The DD to add to the current one. - * @return A reference to the current DD after the operation. - */ - Dd& operator+=(Dd const& other); - - /*! - * Multiplies the two DDs. - * - * @param other The DD to multiply with the current one. - * @return The result of the multiplication. - */ - Dd operator*(Dd const& other) const; - - /*! - * Multiplies the given DD with the current one and assigns the result to the current DD. - * - * @param other The DD to multiply with the current one. - * @return A reference to the current DD after the operation. - */ - Dd& operator*=(Dd const& other); - - /*! - * Subtracts the given DD from the current one. - * - * @param other The DD to subtract from the current one. - * @return The result of the subtraction. - */ - Dd operator-(Dd const& other) const; - - /*! - * Subtracts the DD from the constant zero function. - * - * @return The resulting function represented as a DD. - */ - Dd operator-() const; - - /*! - * Subtracts the given DD from the current one and assigns the result to the current DD. - * - * @param other The DD to subtract from the current one. - * @return A reference to the current DD after the operation. - */ - Dd& operator-=(Dd const& other); - - /*! - * Divides the current DD by the given one. - * - * @param other The DD by which to divide the current one. - * @return The result of the division. - */ - Dd operator/(Dd const& other) const; - - /*! - * Divides the current DD by the given one and assigns the result to the current DD. - * - * @param other The DD by which to divide the current one. - * @return A reference to the current DD after the operation. - */ - Dd& operator/=(Dd const& other); - - /*! - * Retrieves the logical complement of the current DD. The result will map all encodings with a value - * unequal to zero to false and all others to true. - * - * @return The logical complement of the current DD. - */ - Dd operator!() const; - - /*! - * Logically complements the current DD. The result will map all encodings with a value - * unequal to zero to false and all others to true. - * - * @return A reference to the current DD after the operation. - */ - Dd& complement(); - - /*! - * Retrieves the function that maps all evaluations to one that have an identical function values. - * - * @param other The DD with which to perform the operation. - * @return The resulting function represented as a DD. - */ - Dd equals(Dd const& other) const; - - /*! - * Retrieves the function that maps all evaluations to one that have distinct function values. - * - * @param other The DD with which to perform the operation. - * @return The resulting function represented as a DD. - */ - Dd notEquals(Dd const& other) const; - - /*! - * Retrieves the function that maps all evaluations to one whose function value in the first DD are less - * than the one in the given DD. - * - * @param other The DD with which to perform the operation. - * @return The resulting function represented as a DD. - */ - Dd less(Dd const& other) const; - - /*! - * Retrieves the function that maps all evaluations to one whose function value in the first DD are less or - * equal than the one in the given DD. - * - * @param other The DD with which to perform the operation. - * @return The resulting function represented as a DD. - */ - Dd lessOrEqual(Dd const& other) const; - - /*! - * Retrieves the function that maps all evaluations to one whose function value in the first DD are greater - * than the one in the given DD. - * - * @param other The DD with which to perform the operation. - * @return The resulting function represented as a DD. - */ - Dd greater(Dd const& other) const; - - /*! - * Retrieves the function that maps all evaluations to one whose function value in the first DD are greater - * or equal than the one in the given DD. - * - * @param other The DD with which to perform the operation. - * @return The resulting function represented as a DD. - */ - Dd greaterOrEqual(Dd const& other) const; - - /*! - * Retrieves the function that maps all evaluations to the minimum of the function values of the two DDs. - * - * @param other The DD with which to perform the operation. - * @return The resulting function represented as a DD. - */ - Dd minimum(Dd const& other) const; - - /*! - * Retrieves the function that maps all evaluations to the maximum of the function values of the two DDs. - * - * @param other The DD with which to perform the operation. - * @return The resulting function represented as a DD. - */ - Dd maximum(Dd const& other) const; - - /*! - * Existentially abstracts from the given meta variables. - * - * @param metaVariables The meta variables from which to abstract. - */ - Dd existsAbstract(std::set const& metaVariables) const; - - /*! - * Universally abstracts from the given meta variables. - * - * @param metaVariables The meta variables from which to abstract. - */ - Dd universalAbstract(std::set const& metaVariables) const; - - /*! - * Sum-abstracts from the given meta variables. - * - * @param metaVariables The meta variables from which to abstract. - */ - Dd sumAbstract(std::set const& metaVariables) const; - - /*! - * Min-abstracts from the given meta variables. - * - * @param metaVariables The meta variables from which to abstract. - */ - Dd minAbstract(std::set const& metaVariables) const; - - /*! - * Max-abstracts from the given meta variables. - * - * @param metaVariables The meta variables from which to abstract. - */ - Dd maxAbstract(std::set const& metaVariables) const; - - /*! - * Checks whether the current and the given DD represent the same function modulo some given precision. - * - * @param other The DD with which to compare. - * @param precision An upper bound on the maximal difference between any two function values that is to be - * tolerated. - * @param relative If set to true, not the absolute values have to be within the precision, but the relative - * values. - */ - bool equalModuloPrecision(Dd const& other, double precision, bool relative = true) const; - - /*! - * Swaps the given pairs of meta variables in the DD. The pairs of meta variables must be guaranteed to have - * the same number of underlying DD variables. - * - * @param metaVariablePairs A vector of meta variable pairs that are to be swapped for one another. - * @return The resulting DD. - */ - Dd swapVariables(std::vector> const& metaVariablePairs); - - /*! - * Multiplies the current DD (representing a matrix) with the given matrix by summing over the given meta - * variables. - * - * @param otherMatrix The matrix with which to multiply. - * @param summationMetaVariables The names of the meta variables over which to sum during the matrix- - * matrix multiplication. - * @return A DD representing the result of the matrix-matrix multiplication. - */ - Dd multiplyMatrix(Dd const& otherMatrix, std::set const& summationMetaVariables) const; - - /*! - * Computes the logical and of the current and the given DD and existentially abstracts from the given set - * of variables. - * - * @param other The second DD for the logical and. - * @param existentialVariables The variables from which to existentially abstract. - * @return A DD representing the result. - */ - Dd andExists(Dd const& other, std::set const& existentialVariables) const; - - /*! - * Computes a DD that represents the function in which all assignments with a function value strictly larger - * 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 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; - - /*! - * Computes the constraint of the current DD with the given constraint. That is, the function value of the - * resulting DD will be the same as the current ones for all assignments mapping to one in the constraint - * and may be different otherwise. - * - * @param constraint The constraint to use for the operation. - * @return The resulting DD. - */ - Dd constrain(Dd const& constraint) const; - - /*! - * Computes the restriction of the current DD with the given constraint. That is, the function value of the - * resulting DD will be the same as the current ones for all assignments mapping to one in the constraint - * and may be different otherwise. - * - * @param constraint The constraint to use for the operation. - * @return The resulting DD. - */ - Dd restrict(Dd const& constraint) const; - /*! * Retrieves the support of the current DD. * - * @return The support represented as a DD. + * @return The support represented as a BDD. */ - Dd getSupport() const; + virtual Bdd getSupport() const = 0; /*! * 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; + virtual uint_fast64_t getNonZeroCount() const = 0; /*! * Retrieves the number of leaves of the DD. * * @return The number of leaves of the DD. */ - uint_fast64_t getLeafCount() const; + virtual uint_fast64_t getLeafCount() const = 0; /*! * Retrieves the number of nodes necessary to represent the DD. * * @return The number of nodes in this DD. */ - uint_fast64_t getNodeCount() 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. - * - * @param metaVariable The meta variable that has to be equal to the given value. - * @param variableValue The value that the meta variable is supposed to have. This must be within the range - * of the meta variable. - * @param targetValue The new function value of the modified encodings. - */ - void setValue(storm::expressions::Variable const& metaVariable, int_fast64_t variableValue, double targetValue); - - /*! - * Sets the function values of all encodings that have the given values of the two meta variables to the - * given target value. - * - * @param metaVariable1 The first meta variable that has to be equal to the first given - * value. - * @param variableValue1 The value that the first meta variable is supposed to have. This must be within the - * range of the meta variable. - * @param metaVariable2 The second meta variable that has to be equal to the second given - * value. - * @param variableValue2 The value that the second meta variable is supposed to have. This must be within - * the range of the meta variable. - * @param targetValue The new function value of the modified encodings. - */ - void setValue(storm::expressions::Variable const& metaVariable1, int_fast64_t variableValue1, storm::expressions::Variable const& metaVariable2, int_fast64_t variableValue2, double targetValue); - - /*! - * Sets the function values of all encodings that have the given values of the given meta variables to the - * given target value. - * - * @param metaVariableToValueMap A mapping of meta variables to the values they are supposed to have. All - * values must be within the range of the respective meta variable. - * @param targetValue The new function value of the modified encodings. - */ - void setValue(std::map const& metaVariableToValueMap = std::map(), double targetValue = 0); - - /*! - * Retrieves the value of the function when all meta variables are assigned the values of the given mapping. - * Note that the mapping must specify values for all meta variables contained in the DD. - * - * @param metaVariableToValueMap A mapping of meta variables to their values. - * @return The value of the function evaluated with the given input. - */ - double getValue(std::map const& metaVariableToValueMap = std::map()) const; - - /*! - * 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 this DD represents a constant function. - * - * @return True if this DD represents a constants function. - */ - bool isConstant() const; + virtual uint_fast64_t getNodeCount() const = 0; /*! * Retrieves the index of the topmost variable in the DD. * * @return The index of the topmost variable in DD. */ - uint_fast64_t getIndex() const; - - /*! - * Converts the DD to a vector. - * - * @return The double vector that is represented by this DD. - */ - template - std::vector toVector() const; - - /*! - * Converts the DD to a vector. The given offset-labeled DD is used to determine the correct row of - * each entry. - * - * @param rowOdd The ODD used for determining the correct row. - * @return The double vector that is represented by this DD. - */ - template - std::vector toVector(storm::dd::Odd const& rowOdd) const; - - /*! - * Converts the DD to a (sparse) double matrix. All contained non-primed variables are assumed to encode the - * row, whereas all primed variables are assumed to encode the column. - * - * @return The matrix that is represented by this DD. - */ - storm::storage::SparseMatrix toMatrix() const; - - /*! - * Converts the DD to a (sparse) double matrix. All contained non-primed variables are assumed to encode the - * row, whereas all primed variables are assumed to encode the column. The given offset-labeled DDs are used - * to determine the correct row and column, respectively, for each entry. - * - * @param rowOdd The ODD used for determining the correct row. - * @param columnOdd The ODD used for determining the correct column. - * @return The matrix that is represented by this DD. - */ - storm::storage::SparseMatrix toMatrix(storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const; - - /*! - * Converts the DD to a (sparse) double matrix. The given offset-labeled DDs are used to determine the - * correct row and column, respectively, for each entry. - * - * @param rowMetaVariables The meta variables that encode the rows of the matrix. - * @param columnMetaVariables The meta variables that encode the columns of the matrix. - * @param rowOdd The ODD used for determining the correct row. - * @param columnOdd The ODD used for determining the correct column. - * @return The matrix that is represented by this DD. - */ - storm::storage::SparseMatrix toMatrix(std::set const& rowMetaVariables, std::set const& columnMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const; - - /*! - * Converts the DD to a row-grouped (sparse) double matrix. The given offset-labeled DDs are used to - * determine the correct row and column, respectively, for each entry. Note: this function assumes that - * the meta variables used to distinguish different row groups are at the very top of the DD. - * - * @param rowMetaVariables The meta variables that encode the rows of the matrix. - * @param columnMetaVariables The meta variables that encode the columns of the matrix. - * @param groupMetaVariables The meta variables that are used to distinguish different row groups. - * @param rowOdd The ODD used for determining the correct row. - * @param columnOdd The ODD used for determining the correct column. - * @return The matrix that is represented by this DD. - */ - storm::storage::SparseMatrix toMatrix(std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const; + virtual uint_fast64_t getIndex() const = 0; /*! * Retrieves whether the given meta variable is contained in the DD. @@ -598,19 +91,12 @@ namespace storm { */ std::set const& getContainedMetaVariables() const; - /*! - * Retrieves the set of all meta variables contained in the DD. - * - * @return The set of all meta variables contained in the DD. - */ - std::set& getContainedMetaVariables(); - /*! * Exports the DD to the given file in the dot format. * * @param filename The name of the file to which the DD is to be exported. */ - void exportToDot(std::string const& filename = "") const; + virtual void exportToDot(std::string const& filename = "") const = 0; /*! * Retrieves the manager that is responsible for this DD. @@ -618,224 +104,59 @@ namespace storm { * A pointer to the manager that is responsible for this DD. */ std::shared_ptr const> getDdManager() const; + + protected: /*! - * Retrieves an iterator that points to the first meta variable assignment with a non-zero function value. - * - * @param enumerateDontCareMetaVariables If set to true, all meta variable assignments are enumerated, even - * if a meta variable does not at all influence the the function value. - * @return An iterator that points to the first meta variable assignment with a non-zero function value. - */ - DdForwardIterator begin(bool enumerateDontCareMetaVariables = true) const; - - /*! - * Retrieves an iterator that points past the end of the container. - * - * @param enumerateDontCareMetaVariables If set to true, all meta variable assignments are enumerated, even - * if a meta variable does not at all influence the the function value. - * @return An iterator that points past the end of the container. - */ - DdForwardIterator end(bool enumerateDontCareMetaVariables = true) const; - - /*! - * Converts the DD into a (heavily nested) if-then-else expression that represents the very same function. - * The variable names used in the expression are derived from the meta variable name and are extended with a - * suffix ".i" if the meta variable is integer-valued, expressing that the variable is the i-th bit of the - * meta variable. - * - * @return The resulting expression. - */ - storm::expressions::Expression toExpression() const; - - /*! - * Converts the DD into a (heavily nested) if-then-else (with negations) expression that evaluates to true - * if and only if the assignment is minterm of the DD. The variable names used in the expression are derived - * from the meta variable name and are extended with a suffix ".i" if the meta variable is integer-valued, - * expressing that the variable is the i-th bit of the meta variable. - * - * @return The resulting expression. - */ - storm::expressions::Expression getMintermExpression() const; - - friend std::ostream & operator<<(std::ostream& out, const Dd& dd); - - /*! - * Converts an MTBDD to a BDD by mapping all values unequal to zero to 1. This effectively does the same as - * a call to notZero(). - * - * @return The corresponding BDD. - */ - Dd toBdd() const; - - /*! - * Converts a BDD to an equivalent MTBDD. - * - * @return The corresponding MTBDD. - */ - Dd toMtbdd() const; - - /*! - * Retrieves whether this DD is a BDD. - * - * @return True iff this DD is a BDD. - */ - bool isBdd() const; - - /*! - * Retrieves whether this DD is an MTBDD. Even though MTBDDs technicall subsume BDDs, this will return false - * if the DD is actually a BDD. - * - * @return True iff this DD is an MTBDD. - */ - bool isMtbdd() const; - - private: - /*! - * Retrieves the CUDD BDD object associated with this DD. - * - * @return The CUDD BDD object associated with this DD. - */ - BDD getCuddBdd() const; - - /*! - * Retrieves the CUDD MTBDD object associated with this DD. - * - * @return The CUDD MTBDD object associated with this DD. - */ - ADD getCuddMtbdd() const; - - /*! - * Retrieves the CUDD object associated with this DD. + * Retrieves the set of all meta variables contained in the DD. * - * @return The CUDD object associated with this DD. + * @return The set of all meta variables contained in the DD. */ - ABDD const& getCuddDd() const; + std::set& getContainedMetaVariables(); /*! - * Retrieves the raw DD node of CUDD associated with this DD. + * Adds the given set of meta variables to the DD. * - * @return The DD node of CUDD associated with this DD. + * @param metaVariables The set of meta variables to add. */ - DdNode* getCuddDdNode() const; + void addMetaVariables(std::set const& metaVariables); /*! * Adds the given meta variable to the set of meta variables that are contained in this DD. * * @param metaVariable The name of the meta variable to add. */ - void addContainedMetaVariable(storm::expressions::Variable const& metaVariable); + void addMetaVariable(storm::expressions::Variable const& metaVariable); /*! * Removes the given meta variable to the set of meta variables that are contained in this DD. * * @param metaVariable The name of the meta variable to remove. */ - void removeContainedMetaVariable(storm::expressions::Variable const& metaVariable); + void removeMetaVariable(storm::expressions::Variable const& metaVariable); /*! - * Performs the recursive step of toExpression on the given DD. + * Removes the given set of meta variables from the DD. * - * @param dd The dd to translate into an expression. - * @param variables The variables to use in the expression. - * @return The resulting expression. + * @param metaVariables The set of meta variables to remove. */ - static storm::expressions::Expression toExpressionRecur(DdNode const* dd, std::vector const& variables); + void removeMetaVariables(std::set const& metaVariables); - /*! - * Performs the recursive step of getMintermExpression on the given DD. - * - * @param manager The manager of the DD. - * @param dd The dd whose minterms to translate into an expression. - * @param variables The variables to use in the expression. - * @return The resulting expression. - */ - static storm::expressions::Expression getMintermExpressionRecur(::DdManager* manager, DdNode const* dd, std::vector const& variables); + protected: /*! - * Creates a DD that encapsulates the given CUDD ADD. - * - * @param ddManager The manager responsible for this DD. - * @param cuddDd The CUDD ADD to store. - * @param containedMetaVariables The meta variables that appear in the DD. - */ - Dd(std::shared_ptr const> ddManager, ADD cuddDd, std::set const& containedMetaVariables = std::set()); - - /*! - * Creates a DD that encapsulates the given CUDD ADD. + * Creates a DD with the given manager and meta variables. * * @param ddManager The manager responsible for this DD. - * @param cuddDd The CUDD ADD to store. * @param containedMetaVariables The meta variables that appear in the DD. */ - Dd(std::shared_ptr const> ddManager, BDD cuddDd, std::set const& containedMetaVariables = std::set()); - - /*! - * Helper function to convert the DD into a (sparse) matrix. - * - * @param dd The DD to convert. - * @param rowIndications A vector indicating at which position in the columnsAndValues vector the entries - * of row i start. Note: this vector is modified in the computation. More concretely, each entry i in the - * vector will be increased by the number of entries in the row. This can be used to count the number - * of entries in each row. If the values are not to be modified, a copy needs to be provided or the entries - * need to be restored afterwards. - * @param columnsAndValues The vector that will hold the columns and values of non-zero entries upon successful - * completion. - * @param rowGroupOffsets The row offsets at which a given row group starts. - * @param rowOdd The ODD used for the row translation. - * @param columnOdd The ODD used for the column translation. - * @param currentRowLevel The currently considered row level in the DD. - * @param currentColumnLevel The currently considered row level in the DD. - * @param maxLevel The number of levels that need to be considered. - * @param currentRowOffset The current row offset. - * @param currentColumnOffset The current row offset. - * @param ddRowVariableIndices The (sorted) indices of all DD row variables that need to be considered. - * @param ddColumnVariableIndices The (sorted) indices of all DD row variables that need to be considered. - * @param generateValues If set to true, the vector columnsAndValues is filled with the actual entries, which - * only works if the offsets given in rowIndications are already correct. If they need to be computed first, - * this flag needs to be false. - */ - void toMatrixRec(DdNode const* dd, std::vector& rowIndications, std::vector>& columnsAndValues, std::vector const& rowGroupOffsets, Odd const& rowOdd, Odd const& columnOdd, uint_fast64_t currentRowLevel, uint_fast64_t currentColumnLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, uint_fast64_t currentColumnOffset, std::vector const& ddRowVariableIndices, std::vector const& ddColumnVariableIndices, bool generateValues = true) const; - - /*! - * Splits the given matrix DD into the groups using the given group variables. - * - * @param dd The DD to split. - * @param groups A vector that is to be filled with the DDs for the individual groups. - * @param ddGroupVariableIndices The (sorted) indices of all DD group variables that need to be considered. - * @param currentLevel The currently considered level in the DD. - * @param maxLevel The number of levels that need to be considered. - * @param remainingMetaVariables The meta variables that remain in the DDs after the groups have been split. - */ - void splitGroupsRec(DdNode* dd, std::vector>& groups, std::vector const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::set const& remainingMetaVariables) const; + Dd(std::shared_ptr const> ddManager, std::set const& containedMetaVariables = std::set()); - /*! - * Performs a recursive step to add the given DD-based vector to the given explicit vector. - * - * @param dd The DD to add to the explicit vector. - * @param currentLevel The currently considered level in the DD. - * @param maxLevel The number of levels that need to be considered. - * @param currentOffset The current offset. - * @param odd The ODD used for the translation. - * @param ddVariableIndices The (sorted) indices of all DD variables that need to be considered. - * @param targetVector The vector to which the translated DD-based vector is to be added. - */ - template - void addToVectorRec(DdNode const* dd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector) const; - - /*! - * Retrieves the indices of all DD variables that are contained in this DD (not necessarily in the support, - * because they could be "don't cares"). Additionally, the indices are sorted to allow for easy access. - * - * @return The (sorted) indices of all DD variables that are contained in this DD. - */ - std::vector getSortedVariableIndices() const; + private: // A pointer to the manager responsible for this DD. std::shared_ptr const> ddManager; - // The ADD created by CUDD. - boost::variant cuddDd; - // The meta variables that appear in this DD. std::set containedMetaVariables; };