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<DdType Type> 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<DdType Type> 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 <cstring>
+#include <algorithm>
+
+#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<DdType::CUDD>::Dd(std::shared_ptr<DdManager<DdType::CUDD> const> ddManager, BDD cuddDd, std::set<storm::expressions::Variable> const& containedMetaVariables) : ddManager(ddManager), cuddDd(cuddDd), containedMetaVariables(containedMetaVariables) {
+ // Intentionally left empty.
+ }
+
+ Dd<DdType::CUDD>::Dd(std::shared_ptr<DdManager<DdType::CUDD> const> ddManager, ADD cuddDd, std::set<storm::expressions::Variable> const& containedMetaVariables) : ddManager(ddManager), cuddDd(cuddDd), containedMetaVariables(containedMetaVariables) {
+ // Intentionally left empty.
+ }
+
+ bool Dd<DdType::CUDD>::isBdd() const {
+ return this->cuddDd.which() == 0;
+ }
+
+ bool Dd<DdType::CUDD>::isMtbdd() const {
+ return this->cuddDd.which() == 1;
+ }
+
+ Dd<DdType::CUDD> Dd<DdType::CUDD>::toBdd() const {
+ if (this->isBdd()) {
+ return *this;
+ } else {
+ return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().BddPattern(), this->containedMetaVariables);
+ }
+ }
+
+ Dd<DdType::CUDD> Dd<DdType::CUDD>::toMtbdd() const {
+ if (this->isMtbdd()) {
+ return *this;
+ } else {
+ return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().Add(), this->containedMetaVariables);
+ }
+ }
+
+ BDD Dd<DdType::CUDD>::getCuddBdd() const {
+ if (this->isBdd()) {
+ return boost::get<BDD>(this->cuddDd);
+ } else {
+ STORM_LOG_WARN_COND(false, "Implicitly converting MTBDD to BDD.");
+ return this->getCuddMtbdd().BddPattern();
+ }
+ }
+
+ ADD Dd<DdType::CUDD>::getCuddMtbdd() const {
+ if (this->isMtbdd()) {
+ return boost::get<ADD>(this->cuddDd);
+ } else {
+ STORM_LOG_WARN_COND(false, "Implicitly converting BDD to MTBDD.");
+ return this->getCuddBdd().Add();
+ }
+ }
+
+ ABDD const& Dd<DdType::CUDD>::getCuddDd() const {
+ if (this->isBdd()) {
+ return static_cast<ABDD const&>(boost::get<BDD>(this->cuddDd));
+ } else {
+ return static_cast<ABDD const&>(boost::get<ADD>(this->cuddDd));
+ }
+ }
+
+ DdNode* Dd<DdType::CUDD>::getCuddDdNode() const {
+ if (this->isBdd()) {
+ return this->getCuddBdd().getNode();
+ } else {
+ return this->getCuddMtbdd().getNode();
+ }
+ }
+
+ bool Dd<DdType::CUDD>::operator==(Dd<DdType::CUDD> 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<DdType::CUDD>::operator!=(Dd<DdType::CUDD> const& other) const {
+ return !(*this == other);
+ }
+
+ Dd<DdType::CUDD> Dd<DdType::CUDD>::ite(Dd<DdType::CUDD> const& thenDd, Dd<DdType::CUDD> const& elseDd) const {
+ std::set<storm::expressions::Variable> 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<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().Ite(thenDd.getCuddBdd(), elseDd.getCuddBdd()), metaVariableNames);
+ } else {
+ return Dd<DdType::CUDD>(this->getDdManager(), this->toMtbdd().getCuddMtbdd().Ite(thenDd.toMtbdd().getCuddMtbdd(), elseDd.toMtbdd().getCuddMtbdd()), metaVariableNames);
+ }
+ }
+
+ Dd<DdType::CUDD> Dd<DdType::CUDD>::operator+(Dd<DdType::CUDD> const& other) const {
+ Dd<DdType::CUDD> result(*this);
+ result += other;
+ return result;
+ }
+
+ Dd<DdType::CUDD>& Dd<DdType::CUDD>::operator+=(Dd<DdType::CUDD> 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<DdType::CUDD> Dd<DdType::CUDD>::operator*(Dd<DdType::CUDD> const& other) const {
+ Dd<DdType::CUDD> result(*this);
+ result *= other;
+ return result;
+ }
+
+ Dd<DdType::CUDD>& Dd<DdType::CUDD>::operator*=(Dd<DdType::CUDD> 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<DdType::CUDD> Dd<DdType::CUDD>::operator-(Dd<DdType::CUDD> const& other) const {
+ STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing arithmetical operation on BDD(s).");
+ Dd<DdType::CUDD> result(*this);
+ result -= other;
+ return result;
+ }
+
+ Dd<DdType::CUDD> Dd<DdType::CUDD>::operator-() const {
+ STORM_LOG_WARN_COND(this->isMtbdd(), "Performing arithmetical operation on BDD(s).");
+ return this->getDdManager()->getZero(true) - *this;
+ }
+
+ Dd<DdType::CUDD>& Dd<DdType::CUDD>::operator-=(Dd<DdType::CUDD> 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<DdType::CUDD> Dd<DdType::CUDD>::operator/(Dd<DdType::CUDD> const& other) const {
+ STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing arithmetical operation on BDD(s).");
+ Dd<DdType::CUDD> result(*this);
+ result /= other;
+ return result;
+ }
+
+ Dd<DdType::CUDD>& Dd<DdType::CUDD>::operator/=(Dd<DdType::CUDD> 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<DdType::CUDD> Dd<DdType::CUDD>::operator!() const {
+ Dd<DdType::CUDD> result(*this);
+ result.complement();
+ return result;
+ }
+
+ Dd<DdType::CUDD>& Dd<DdType::CUDD>::complement() {
+ if (this->isBdd()) {
+ this->cuddDd = ~this->getCuddBdd();
+ } else {
+ this->cuddDd = ~this->getCuddMtbdd();
+ }
+ return *this;
+ }
+
+ Dd<DdType::CUDD> Dd<DdType::CUDD>::operator&&(Dd<DdType::CUDD> const& other) const {
+ Dd<DdType::CUDD> result(*this);
+ result &= other;
+ return result;
+ }
+
+ Dd<DdType::CUDD>& Dd<DdType::CUDD>::operator&=(Dd<DdType::CUDD> 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<DdType::CUDD> Dd<DdType::CUDD>::operator||(Dd<DdType::CUDD> const& other) const {
+ Dd<DdType::CUDD> result(*this);
+ result |= other;
+ return result;
+ }
+
+ Dd<DdType::CUDD>& Dd<DdType::CUDD>::operator|=(Dd<DdType::CUDD> 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<DdType::CUDD> Dd<DdType::CUDD>::iff(Dd<DdType::CUDD> const& other) const {
+ std::set<storm::expressions::Variable> metaVariables(this->getContainedMetaVariables());
+ metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end());
+ if (this->isBdd() && other.isBdd()) {
+ return Dd<DdType::CUDD>(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<DdType::CUDD>(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<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().Xnor(other.getCuddBdd()), metaVariables);
+ }
+ }
+
+ Dd<DdType::CUDD> Dd<DdType::CUDD>::exclusiveOr(Dd<DdType::CUDD> const& other) const {
+ std::set<storm::expressions::Variable> metaVariables(this->getContainedMetaVariables());
+ metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end());
+ if (this->isBdd() && other.isBdd()) {
+ return Dd<DdType::CUDD>(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<DdType::CUDD>(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<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().Xor(other.getCuddBdd()), metaVariables);
+ }
+ }
+
+ Dd<DdType::CUDD> Dd<DdType::CUDD>::implies(Dd<DdType::CUDD> const& other) const {
+ std::set<storm::expressions::Variable> 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<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().Ite(other.getCuddBdd(), this->getDdManager()->getOne().getCuddBdd()), metaVariables);
+ }
+
+ Dd<DdType::CUDD> Dd<DdType::CUDD>::equals(Dd<DdType::CUDD> const& other) const {
+ STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing arithmetical operation on BDD(s).");
+ std::set<storm::expressions::Variable> metaVariables(this->getContainedMetaVariables());
+ metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end());
+ return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().Equals(other.getCuddMtbdd()), metaVariables);
+ }
+
+ Dd<DdType::CUDD> Dd<DdType::CUDD>::notEquals(Dd<DdType::CUDD> const& other) const {
+ STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing arithmetical operation on BDD(s).");
+ std::set<storm::expressions::Variable> metaVariables(this->getContainedMetaVariables());
+ metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end());
+ return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().NotEquals(other.getCuddMtbdd()), metaVariables);
+ }
+
+ Dd<DdType::CUDD> Dd<DdType::CUDD>::less(Dd<DdType::CUDD> const& other) const {
+ STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing arithmetical operation on BDD(s).");
+ std::set<storm::expressions::Variable> metaVariables(this->getContainedMetaVariables());
+ metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end());
+ return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().LessThan(other.getCuddMtbdd()), metaVariables);
+ }
+
+ Dd<DdType::CUDD> Dd<DdType::CUDD>::lessOrEqual(Dd<DdType::CUDD> const& other) const {
+ STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing arithmetical operation on BDD(s).");
+ std::set<storm::expressions::Variable> metaVariables(this->getContainedMetaVariables());
+ metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end());
+ return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().LessThanOrEqual(other.getCuddMtbdd()), metaVariables);
+ }
+
+ Dd<DdType::CUDD> Dd<DdType::CUDD>::greater(Dd<DdType::CUDD> const& other) const {
+ STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing arithmetical operation on BDD(s).");
+ std::set<storm::expressions::Variable> metaVariables(this->getContainedMetaVariables());
+ metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end());
+ return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().GreaterThan(other.getCuddMtbdd()), metaVariables);
+ }
+
+ Dd<DdType::CUDD> Dd<DdType::CUDD>::greaterOrEqual(Dd<DdType::CUDD> const& other) const {
+ STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing arithmetical operation on BDD(s).");
+ std::set<storm::expressions::Variable> metaVariables(this->getContainedMetaVariables());
+ metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end());
+ return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().GreaterThanOrEqual(other.getCuddMtbdd()), metaVariables);
+ }
+
+ Dd<DdType::CUDD> Dd<DdType::CUDD>::minimum(Dd<DdType::CUDD> const& other) const {
+ STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing arithmetical operation on BDD(s).");
+ std::set<storm::expressions::Variable> metaVariables(this->getContainedMetaVariables());
+ metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end());
+ return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().Minimum(other.getCuddMtbdd()), metaVariables);
+ }
+
+ Dd<DdType::CUDD> Dd<DdType::CUDD>::maximum(Dd<DdType::CUDD> const& other) const {
+ STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing arithmetical operation on BDD(s).");
+ std::set<storm::expressions::Variable> metaVariables(this->getContainedMetaVariables());
+ metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end());
+ return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().Maximum(other.getCuddMtbdd()), metaVariables);
+ }
+
+ Dd<DdType::CUDD> Dd<DdType::CUDD>::existsAbstract(std::set<storm::expressions::Variable> const& metaVariables) const {
+ STORM_LOG_WARN_COND(this->isBdd(), "Performing logical operation on MTBDD(s).");
+
+ Dd<DdType::CUDD> cubeDd(this->getDdManager()->getOne(false));
+ std::set<storm::expressions::Variable> 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<DdType::CUDD> const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable);
+ cubeDd &= ddMetaVariable.getCube();
+ }
+
+ return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().ExistAbstract(cubeDd.getCuddBdd()), newMetaVariables);
+ }
+
+ Dd<DdType::CUDD> Dd<DdType::CUDD>::universalAbstract(std::set<storm::expressions::Variable> const& metaVariables) const {
+ STORM_LOG_WARN_COND(this->isBdd(), "Performing logical operation on MTBDD(s).");
+
+ Dd<DdType::CUDD> cubeDd(this->getDdManager()->getOne());
+ std::set<storm::expressions::Variable> 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<DdType::CUDD> const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable);
+ cubeDd &= ddMetaVariable.getCube();
+ }
+
+ return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().UnivAbstract(cubeDd.getCuddBdd()), newMetaVariables);
+ }
+
+ Dd<DdType::CUDD> Dd<DdType::CUDD>::sumAbstract(std::set<storm::expressions::Variable> const& metaVariables) const {
+ STORM_LOG_WARN_COND(this->isMtbdd(), "Performing arithmetical operation on BDD(s).");
+
+ Dd<DdType::CUDD> cubeDd(this->getDdManager()->getOne(true));
+ std::set<storm::expressions::Variable> 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<DdType::CUDD> const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable);
+ cubeDd *= ddMetaVariable.getCubeAsMtbdd();
+ }
+
+ return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().ExistAbstract(cubeDd.getCuddMtbdd()), newMetaVariables);
+ }
+
+ Dd<DdType::CUDD> Dd<DdType::CUDD>::minAbstract(std::set<storm::expressions::Variable> const& metaVariables) const {
+ STORM_LOG_WARN_COND(this->isMtbdd(), "Performing arithmetical operation on BDD(s).");
+
+ Dd<DdType::CUDD> cubeDd(this->getDdManager()->getOne(true));
+ std::set<storm::expressions::Variable> 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<DdType::CUDD> const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable);
+ cubeDd *= ddMetaVariable.getCubeAsMtbdd();
+ }
+
+ return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().MinAbstract(cubeDd.getCuddMtbdd()), newMetaVariables);
+ }
+
+ Dd<DdType::CUDD> Dd<DdType::CUDD>::maxAbstract(std::set<storm::expressions::Variable> const& metaVariables) const {
+ STORM_LOG_WARN_COND(this->isMtbdd(), "Performing arithmetical operation on BDD(s).");
+
+ Dd<DdType::CUDD> cubeDd(this->getDdManager()->getOne(true));
+ std::set<storm::expressions::Variable> 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<DdType::CUDD> const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable);
+ cubeDd *= ddMetaVariable.getCubeAsMtbdd();
+ }
+
+ return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().MaxAbstract(cubeDd.getCuddMtbdd()), newMetaVariables);
+ }
+
+ bool Dd<DdType::CUDD>::equalModuloPrecision(Dd<DdType::CUDD> 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<DdType::CUDD> Dd<DdType::CUDD>::swapVariables(std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& metaVariablePairs) {
+ std::set<storm::expressions::Variable> newContainedMetaVariables;
+ if (this->isBdd()) {
+ std::vector<BDD> from;
+ std::vector<BDD> to;
+ for (auto const& metaVariablePair : metaVariablePairs) {
+ DdMetaVariable<DdType::CUDD> const& variable1 = this->getDdManager()->getMetaVariable(metaVariablePair.first);
+ DdMetaVariable<DdType::CUDD> 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<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().SwapVariables(from, to), newContainedMetaVariables);
+ } else {
+ std::vector<ADD> from;
+ std::vector<ADD> to;
+ for (auto const& metaVariablePair : metaVariablePairs) {
+ DdMetaVariable<DdType::CUDD> const& variable1 = this->getDdManager()->getMetaVariable(metaVariablePair.first);
+ DdMetaVariable<DdType::CUDD> 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<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().SwapVariables(from, to), newContainedMetaVariables);
+ }
+ }
+
+ Dd<DdType::CUDD> Dd<DdType::CUDD>::multiplyMatrix(Dd<DdType::CUDD> const& otherMatrix, std::set<storm::expressions::Variable> const& summationMetaVariables) const {
+ STORM_LOG_WARN_COND(this->isMtbdd() && otherMatrix.isMtbdd(), "Performing arithmetical operation on BDD(s).");
+
+ // Create the CUDD summation variables.
+ std::vector<ADD> summationDdVariables;
+ for (auto const& metaVariable : summationMetaVariables) {
+ for (auto const& ddVariable : this->getDdManager()->getMetaVariable(metaVariable).getDdVariables()) {
+ summationDdVariables.push_back(ddVariable.getCuddMtbdd());
+ }
+ }
+
+ std::set<storm::expressions::Variable> unionOfMetaVariables;
+ std::set_union(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end(), otherMatrix.getContainedMetaVariables().begin(), otherMatrix.getContainedMetaVariables().end(), std::inserter(unionOfMetaVariables, unionOfMetaVariables.begin()));
+ std::set<storm::expressions::Variable> containedMetaVariables;
+ std::set_difference(unionOfMetaVariables.begin(), unionOfMetaVariables.end(), summationMetaVariables.begin(), summationMetaVariables.end(), std::inserter(containedMetaVariables, containedMetaVariables.begin()));
+
+ return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().MatrixMultiply(otherMatrix.getCuddMtbdd(), summationDdVariables), containedMetaVariables);
+ }
+
+ Dd<DdType::CUDD> Dd<DdType::CUDD>::andExists(Dd<DdType::CUDD> const& other, std::set<storm::expressions::Variable> const& existentialVariables) const {
+ STORM_LOG_WARN_COND(this->isBdd() && other.isBdd(), "Performing logical operation on MTBDD(s).");
+
+ Dd<DdType::CUDD> cubeDd(this->getDdManager()->getOne());
+ for (auto const& metaVariable : existentialVariables) {
+ DdMetaVariable<DdType::CUDD> const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable);
+ cubeDd &= ddMetaVariable.getCube();
+ }
+
+ std::set<storm::expressions::Variable> unionOfMetaVariables;
+ std::set_union(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end(), other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end(), std::inserter(unionOfMetaVariables, unionOfMetaVariables.begin()));
+ std::set<storm::expressions::Variable> containedMetaVariables;
+ std::set_difference(unionOfMetaVariables.begin(), unionOfMetaVariables.end(), existentialVariables.begin(), existentialVariables.end(), std::inserter(containedMetaVariables, containedMetaVariables.begin()));
+
+ return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().AndAbstract(other.getCuddBdd(), cubeDd.getCuddBdd()), containedMetaVariables);
+ }
+
+ Dd<DdType::CUDD> Dd<DdType::CUDD>::greater(double value) const {
+ STORM_LOG_WARN_COND(this->isMtbdd(), "Performing arithmetical operation on BDD(s).");
+ return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().BddStrictThreshold(value), this->getContainedMetaVariables());
+ }
+
+ Dd<DdType::CUDD> Dd<DdType::CUDD>::greaterOrEqual(double value) const {
+ STORM_LOG_WARN_COND(this->isMtbdd(), "Performing arithmetical operation on BDD(s).");
+ return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().BddThreshold(value), this->getContainedMetaVariables());
+ }
+
+ Dd<DdType::CUDD> Dd<DdType::CUDD>::notZero() const {
+ return this->toBdd();
+ }
+
+ Dd<DdType::CUDD> Dd<DdType::CUDD>::constrain(Dd<DdType::CUDD> const& constraint) const {
+ std::set<storm::expressions::Variable> metaVariables(this->getContainedMetaVariables());
+ metaVariables.insert(constraint.getContainedMetaVariables().begin(), constraint.getContainedMetaVariables().end());
+
+ if (this->isBdd() && constraint.isBdd()) {
+ return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().Constrain(constraint.getCuddBdd()), metaVariables);
+ } else {
+ return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().Constrain(constraint.getCuddMtbdd()), metaVariables);
+ }
+ }
+
+ Dd<DdType::CUDD> Dd<DdType::CUDD>::restrict(Dd<DdType::CUDD> const& constraint) const {
+ std::set<storm::expressions::Variable> metaVariables(this->getContainedMetaVariables());
+ metaVariables.insert(constraint.getContainedMetaVariables().begin(), constraint.getContainedMetaVariables().end());
+
+ if (this->isBdd() && constraint.isBdd()) {
+ return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().Restrict(constraint.getCuddBdd()), metaVariables);
+ } else {
+ return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().Restrict(constraint.getCuddMtbdd()), metaVariables);
+ }
+ }
+
+ Dd<DdType::CUDD> Dd<DdType::CUDD>::getSupport() const {
+ if (this->isBdd()) {
+ return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().Support(), this->getContainedMetaVariables());
+ } else {
+ return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().Support(), this->getContainedMetaVariables());
+ }
+ }
+
+ uint_fast64_t Dd<DdType::CUDD>::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<uint_fast64_t>(this->getCuddBdd().CountMinterm(static_cast<int>(numberOfDdVariables)));
+ } else {
+ return static_cast<uint_fast64_t>(this->getCuddMtbdd().CountMinterm(static_cast<int>(numberOfDdVariables)));
+ }
+ }
+
+ uint_fast64_t Dd<DdType::CUDD>::getLeafCount() const {
+ if (this->isBdd()) {
+ return static_cast<uint_fast64_t>(this->getCuddBdd().CountLeaves());
+ } else {
+ return static_cast<uint_fast64_t>(this->getCuddMtbdd().CountLeaves());
+ }
+ }
+
+ uint_fast64_t Dd<DdType::CUDD>::getNodeCount() const {
+ if (this->isBdd()) {
+ return static_cast<uint_fast64_t>(this->getCuddBdd().nodeCount());
+ } else {
+ return static_cast<uint_fast64_t>(this->getCuddMtbdd().nodeCount());
+ }
+ }
+
+ double Dd<DdType::CUDD>::getMin() const {
+ STORM_LOG_WARN_COND(this->isMtbdd(), "Performing arithmetical operation on BDD(s).");
+
+ ADD constantMinAdd = this->getCuddMtbdd().FindMin();
+ return static_cast<double>(Cudd_V(constantMinAdd.getNode()));
+ }
+
+ double Dd<DdType::CUDD>::getMax() const {
+ STORM_LOG_WARN_COND(this->isMtbdd(), "Performing arithmetical operation on BDD(s).");
+
+ ADD constantMaxAdd = this->getCuddMtbdd().FindMax();
+ return static_cast<double>(Cudd_V(constantMaxAdd.getNode()));
+ }
+
+ void Dd<DdType::CUDD>::setValue(storm::expressions::Variable const& metaVariable, int_fast64_t variableValue, double targetValue) {
+ std::map<storm::expressions::Variable, int_fast64_t> metaVariableToValueMap;
+ metaVariableToValueMap.emplace(metaVariable, variableValue);
+ this->setValue(metaVariableToValueMap, targetValue);
+ }
+
+ void Dd<DdType::CUDD>::setValue(storm::expressions::Variable const& metaVariable1, int_fast64_t variableValue1, storm::expressions::Variable const& metaVariable2, int_fast64_t variableValue2, double targetValue) {
+ std::map<storm::expressions::Variable, int_fast64_t> metaVariableToValueMap;
+ metaVariableToValueMap.emplace(metaVariable1, variableValue1);
+ metaVariableToValueMap.emplace(metaVariable2, variableValue2);
+ this->setValue(metaVariableToValueMap, targetValue);
+ }
+
+ void Dd<DdType::CUDD>::setValue(std::map<storm::expressions::Variable, int_fast64_t> const& metaVariableToValueMap, double targetValue) {
+ if (this->isBdd()) {
+ STORM_LOG_THROW(targetValue == storm::utility::zero<double>() || targetValue == storm::utility::one<double>(), storm::exceptions::InvalidArgumentException, "Cannot set encoding to non-0, non-1 value " << targetValue << " in BDD.");
+ Dd<DdType::CUDD> 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<double>()) {
+ 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<DdType::CUDD> 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<DdType::CUDD>::getValue(std::map<storm::expressions::Variable, int_fast64_t> const& metaVariableToValueMap) const {
+ std::set<storm::expressions::Variable> remainingMetaVariables(this->getContainedMetaVariables());
+ Dd<DdType::CUDD> 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<DdType::CUDD> value = *this && valueEncoding;
+ return value.isZero() ? 0 : 1;
+ } else {
+ Dd<DdType::CUDD> value = *this * valueEncoding.toMtbdd();
+ value = value.sumAbstract(this->getContainedMetaVariables());
+ return static_cast<double>(Cudd_V(value.getCuddMtbdd().getNode()));
+ }
+ }
+
+ bool Dd<DdType::CUDD>::isOne() const {
+ if (this->isBdd()) {
+ return this->getCuddBdd().IsOne();
+ } else {
+ return this->getCuddMtbdd().IsOne();
+ }
+ }
+
+ bool Dd<DdType::CUDD>::isZero() const {
+ if (this->isBdd()) {
+ return this->getCuddBdd().IsZero();
+ } else {
+ return this->getCuddMtbdd().IsZero();
+ }
+ }
+
+ bool Dd<DdType::CUDD>::isConstant() const {
+ if (this->isBdd()) {
+ return Cudd_IsConstant(this->getCuddBdd().getNode());
+ } else {
+ return Cudd_IsConstant(this->getCuddMtbdd().getNode());
+ }
+ }
+
+ uint_fast64_t Dd<DdType::CUDD>::getIndex() const {
+ if (this->isBdd()) {
+ return static_cast<uint_fast64_t>(this->getCuddBdd().NodeReadIndex());
+ } else {
+ return static_cast<uint_fast64_t>(this->getCuddMtbdd().NodeReadIndex());
+ }
+ }
+
+ template<typename ValueType>
+ std::vector<ValueType> Dd<DdType::CUDD>::toVector() const {
+ STORM_LOG_THROW(this->isMtbdd(), storm::exceptions::IllegalFunctionCallException, "Cannot create vector from BDD.");
+ return this->toVector<ValueType>(Odd<DdType::CUDD>(*this));
+ }
+
+ template<typename ValueType>
+ std::vector<ValueType> Dd<DdType::CUDD>::toVector(Odd<DdType::CUDD> const& rowOdd) const {
+ STORM_LOG_THROW(this->isMtbdd(), storm::exceptions::IllegalFunctionCallException, "Cannot create vector from BDD.");
+ std::vector<ValueType> result(rowOdd.getTotalOffset());
+ std::vector<uint_fast64_t> ddVariableIndices = this->getSortedVariableIndices();
+ addToVectorRec(this->getCuddDdNode(), 0, ddVariableIndices.size(), 0, rowOdd, ddVariableIndices, result);
+ return result;
+ }
+
+ storm::storage::SparseMatrix<double> Dd<DdType::CUDD>::toMatrix() const {
+ STORM_LOG_THROW(this->isMtbdd(), storm::exceptions::IllegalFunctionCallException, "Cannot create matrix from BDD.");
+ std::set<storm::expressions::Variable> rowVariables;
+ std::set<storm::expressions::Variable> 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<DdType::CUDD>(this->existsAbstract(rowVariables)), Odd<DdType::CUDD>(this->existsAbstract(columnVariables)));
+ }
+
+ storm::storage::SparseMatrix<double> Dd<DdType::CUDD>::toMatrix(storm::dd::Odd<DdType::CUDD> const& rowOdd, storm::dd::Odd<DdType::CUDD> const& columnOdd) const {
+ STORM_LOG_THROW(this->isMtbdd(), storm::exceptions::IllegalFunctionCallException, "Cannot create matrix from BDD.");
+ std::set<storm::expressions::Variable> rowMetaVariables;
+ std::set<storm::expressions::Variable> 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<double> Dd<DdType::CUDD>::toMatrix(std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, storm::dd::Odd<DdType::CUDD> const& rowOdd, storm::dd::Odd<DdType::CUDD> const& columnOdd) const {
+ STORM_LOG_THROW(this->isMtbdd(), storm::exceptions::IllegalFunctionCallException, "Cannot create matrix from BDD.");
+ std::vector<uint_fast64_t> ddRowVariableIndices;
+ std::vector<uint_fast64_t> ddColumnVariableIndices;
+
+ for (auto const& variable : rowMetaVariables) {
+ DdMetaVariable<DdType::CUDD> const& metaVariable = this->getDdManager()->getMetaVariable(variable);
+ for (auto const& ddVariable : metaVariable.getDdVariables()) {
+ ddRowVariableIndices.push_back(ddVariable.getIndex());
+ }
+ }
+ for (auto const& variable : columnMetaVariables) {
+ DdMetaVariable<DdType::CUDD> 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<uint_fast64_t> rowIndications(rowOdd.getTotalOffset() + 1);
+ std::vector<storm::storage::MatrixEntry<uint_fast64_t, double>> columnsAndValues(this->getNonZeroCount());
+
+ // Create a trivial row grouping.
+ std::vector<uint_fast64_t> 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<double>(columnOdd.getTotalOffset(), std::move(rowIndications), std::move(columnsAndValues), std::move(trivialRowGroupIndices));
+ }
+
+ storm::storage::SparseMatrix<double> Dd<DdType::CUDD>::toMatrix(std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::set<storm::expressions::Variable> const& groupMetaVariables, storm::dd::Odd<DdType::CUDD> const& rowOdd, storm::dd::Odd<DdType::CUDD> const& columnOdd) const {
+ STORM_LOG_THROW(this->isMtbdd(), storm::exceptions::IllegalFunctionCallException, "Cannot create matrix from BDD.");
+ std::vector<uint_fast64_t> ddRowVariableIndices;
+ std::vector<uint_fast64_t> ddColumnVariableIndices;
+ std::vector<uint_fast64_t> ddGroupVariableIndices;
+ std::set<storm::expressions::Variable> rowAndColumnMetaVariables;
+
+ for (auto const& variable : rowMetaVariables) {
+ DdMetaVariable<DdType::CUDD> 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<DdType::CUDD> 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<DdType::CUDD> 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<DdType::CUDD> stateToNumberOfChoices = this->notZero().existsAbstract(columnMetaVariables).sumAbstract(groupMetaVariables);
+ std::vector<uint_fast64_t> rowGroupIndices = stateToNumberOfChoices.toVector<uint_fast64_t>(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<Dd<DdType::CUDD>> groups;
+ splitGroupsRec(this->getCuddDdNode(), groups, ddGroupVariableIndices, 0, ddGroupVariableIndices.size(), rowAndColumnMetaVariables);
+
+ // Create the actual storage for the non-zero entries.
+ std::vector<storm::storage::MatrixEntry<uint_fast64_t, double>> columnsAndValues(this->getNonZeroCount());
+
+ // Now compute the indices at which the individual rows start.
+ std::vector<uint_fast64_t> rowIndications(rowGroupIndices.back() + 1);
+ std::vector<storm::dd::Dd<DdType::CUDD>> 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<double>(columnOdd.getTotalOffset(), std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices));
+ }
+
+ void Dd<DdType::CUDD>::toMatrixRec(DdNode const* dd, std::vector<uint_fast64_t>& rowIndications, std::vector<storm::storage::MatrixEntry<uint_fast64_t, double>>& columnsAndValues, std::vector<uint_fast64_t> const& rowGroupOffsets, Odd<DdType::CUDD> const& rowOdd, Odd<DdType::CUDD> const& columnOdd, uint_fast64_t currentRowLevel, uint_fast64_t currentColumnLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, uint_fast64_t currentColumnOffset, std::vector<uint_fast64_t> const& ddRowVariableIndices, std::vector<uint_fast64_t> 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<uint_fast64_t, double>(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<DdType::CUDD>::splitGroupsRec(DdNode* dd, std::vector<Dd<DdType::CUDD>>& groups, std::vector<uint_fast64_t> const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::set<storm::expressions::Variable> 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<DdType::CUDD>(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<typename ValueType>
+ void Dd<DdType::CUDD>::addToVectorRec(DdNode const* dd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd<DdType::CUDD> const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<ValueType>& 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<ValueType>(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<uint_fast64_t> Dd<DdType::CUDD>::getSortedVariableIndices() const {
+ std::vector<uint_fast64_t> 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<DdType::CUDD>::containsMetaVariable(storm::expressions::Variable const& metaVariable) const {
+ return containedMetaVariables.find(metaVariable) != containedMetaVariables.end();
+ }
+
+ bool Dd<DdType::CUDD>::containsMetaVariables(std::set<storm::expressions::Variable> const& metaVariables) const {
+ for (auto const& metaVariable : metaVariables) {
+ auto const& ddMetaVariable = containedMetaVariables.find(metaVariable);
+
+ if (ddMetaVariable == containedMetaVariables.end()) {
+ return false;
+ }
+ }
+ return true;
+ }
+
+ std::set<storm::expressions::Variable> const& Dd<DdType::CUDD>::getContainedMetaVariables() const {
+ return this->containedMetaVariables;
+ }
+
+ std::set<storm::expressions::Variable>& Dd<DdType::CUDD>::getContainedMetaVariables() {
+ return this->containedMetaVariables;
+ }
+
+ void Dd<DdType::CUDD>::exportToDot(std::string const& filename) const {
+ if (filename.empty()) {
+ if (this->isBdd()) {
+ std::vector<BDD> cuddBddVector = { this->getCuddBdd() };
+ this->getDdManager()->getCuddManager().DumpDot(cuddBddVector);
+ } else {
+ std::vector<ADD> cuddAddVector = { this->getCuddMtbdd() };
+ this->getDdManager()->getCuddManager().DumpDot(cuddAddVector);
+ }
+ } else {
+ // Build the name input of the DD.
+ std::vector<char*> 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<std::string> ddVariableNamesAsStrings = this->getDdManager()->getDdVariableNames();
+ std::vector<char*> 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<BDD> cuddBddVector = { this->getCuddBdd() };
+ this->getDdManager()->getCuddManager().DumpDot(cuddBddVector, &ddVariableNames[0], &ddNames[0], filePointer);
+ } else {
+ std::vector<ADD> 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<DdType::CUDD>::addContainedMetaVariable(storm::expressions::Variable const& metaVariable) {
+ this->getContainedMetaVariables().insert(metaVariable);
+ }
+
+ void Dd<DdType::CUDD>::removeContainedMetaVariable(storm::expressions::Variable const& metaVariable) {
+ this->getContainedMetaVariables().erase(metaVariable);
+ }
+
+ std::shared_ptr<DdManager<DdType::CUDD> const> Dd<DdType::CUDD>::getDdManager() const {
+ return this->ddManager;
+ }
+
+ DdForwardIterator<DdType::CUDD> Dd<DdType::CUDD>::begin(bool enumerateDontCareMetaVariables) const {
+ int* cube;
+ double value;
+ DdGen* generator = this->getCuddDd().FirstCube(&cube, &value);
+ return DdForwardIterator<DdType::CUDD>(this->getDdManager(), generator, cube, value, (Cudd_IsGenEmpty(generator) != 0), &this->getContainedMetaVariables(), enumerateDontCareMetaVariables);
+ }
+
+ DdForwardIterator<DdType::CUDD> Dd<DdType::CUDD>::end(bool enumerateDontCareMetaVariables) const {
+ return DdForwardIterator<DdType::CUDD>(this->getDdManager(), nullptr, nullptr, 0, true, nullptr, enumerateDontCareMetaVariables);
+ }
+
+ storm::expressions::Expression Dd<DdType::CUDD>::toExpression() const {
+ return toExpressionRecur(this->getCuddDdNode(), this->getDdManager()->getDdVariables());
+ }
+
+ storm::expressions::Expression Dd<DdType::CUDD>::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<DdType::CUDD>::toExpressionRecur(DdNode const* dd, std::vector<storm::expressions::Variable> 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<double>(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<DdType::CUDD>::getMintermExpressionRecur(::DdManager* manager, DdNode const* dd, std::vector<storm::expressions::Variable> 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<DdType::CUDD>& dd) {
+ dd.exportToDot();
+ return out;
+ }
+
+ // Explicitly instantiate some templated functions.
+ template std::vector<double> Dd<DdType::CUDD>::toVector() const;
+ template std::vector<double> Dd<DdType::CUDD>::toVector(Odd<DdType::CUDD> const& rowOdd) const;
+ template void Dd<DdType::CUDD>::addToVectorRec(DdNode const* dd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd<DdType::CUDD> const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<double>& targetVector) const;
+ template std::vector<uint_fast64_t> Dd<DdType::CUDD>::toVector() const;
+ template std::vector<uint_fast64_t> Dd<DdType::CUDD>::toVector(Odd<DdType::CUDD> const& rowOdd) const;
+ template void Dd<DdType::CUDD>::addToVectorRec(DdNode const* dd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd<DdType::CUDD> const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<uint_fast64_t>& 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 <map>
+#include <set>
+#include <memory>
+#include <iostream>
+#include <boost/variant.hpp>
+
+#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<DdType Type> class DdManager;
+ template<DdType Type> class Odd;
+
+ template<>
+ class Dd<DdType::CUDD> {
+ public:
+ // Declare the DdManager and DdIterator class as friend so it can access the internals of a DD.
+ friend class DdManager<DdType::CUDD>;
+ friend class DdForwardIterator<DdType::CUDD>;
+ friend class Odd<DdType::CUDD>;
+
+ // Instantiate all copy/move constructors/assignments with the default implementation.
+ Dd() = default;
+ Dd(Dd<DdType::CUDD> const& other) = default;
+ Dd& operator=(Dd<DdType::CUDD> const& other) = default;
+#ifndef WINDOWS
+ Dd(Dd<DdType::CUDD>&& other) = default;
+ Dd& operator=(Dd<DdType::CUDD>&& 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<DdType::CUDD> 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<DdType::CUDD> 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<DdType::CUDD> ite(Dd<DdType::CUDD> const& thenDd, Dd<DdType::CUDD> 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<DdType::CUDD> operator||(Dd<DdType::CUDD> 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<DdType::CUDD>& operator|=(Dd<DdType::CUDD> 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<DdType::CUDD> operator&&(Dd<DdType::CUDD> 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<DdType::CUDD>& operator&=(Dd<DdType::CUDD> 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<DdType::CUDD> iff(Dd<DdType::CUDD> 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<DdType::CUDD> exclusiveOr(Dd<DdType::CUDD> 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<DdType::CUDD> implies(Dd<DdType::CUDD> const& other) const;
+
+ /*!
+ * Adds the two DDs.
+ *
+ * @param other The DD to add to the current one.
+ * @return The result of the addition.
+ */
+ Dd<DdType::CUDD> operator+(Dd<DdType::CUDD> 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<DdType::CUDD>& operator+=(Dd<DdType::CUDD> const& other);
+
+ /*!
+ * Multiplies the two DDs.
+ *
+ * @param other The DD to multiply with the current one.
+ * @return The result of the multiplication.
+ */
+ Dd<DdType::CUDD> operator*(Dd<DdType::CUDD> 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<DdType::CUDD>& operator*=(Dd<DdType::CUDD> 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<DdType::CUDD> operator-(Dd<DdType::CUDD> const& other) const;
+
+ /*!
+ * Subtracts the DD from the constant zero function.
+ *
+ * @return The resulting function represented as a DD.
+ */
+ Dd<DdType::CUDD> 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<DdType::CUDD>& operator-=(Dd<DdType::CUDD> 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<DdType::CUDD> operator/(Dd<DdType::CUDD> 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<DdType::CUDD>& operator/=(Dd<DdType::CUDD> 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<DdType::CUDD> 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<DdType::CUDD>& 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<DdType::CUDD> equals(Dd<DdType::CUDD> 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<DdType::CUDD> notEquals(Dd<DdType::CUDD> 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<DdType::CUDD> less(Dd<DdType::CUDD> 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<DdType::CUDD> lessOrEqual(Dd<DdType::CUDD> 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<DdType::CUDD> greater(Dd<DdType::CUDD> 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<DdType::CUDD> greaterOrEqual(Dd<DdType::CUDD> 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<DdType::CUDD> minimum(Dd<DdType::CUDD> 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<DdType::CUDD> maximum(Dd<DdType::CUDD> const& other) const;
+
+ /*!
+ * Existentially abstracts from the given meta variables.
+ *
+ * @param metaVariables The meta variables from which to abstract.
+ */
+ Dd<DdType::CUDD> existsAbstract(std::set<storm::expressions::Variable> const& metaVariables) const;
+
+ /*!
+ * Universally abstracts from the given meta variables.
+ *
+ * @param metaVariables The meta variables from which to abstract.
+ */
+ Dd<DdType::CUDD> universalAbstract(std::set<storm::expressions::Variable> const& metaVariables) const;
+
+ /*!
+ * Sum-abstracts from the given meta variables.
+ *
+ * @param metaVariables The meta variables from which to abstract.
+ */
+ Dd<DdType::CUDD> sumAbstract(std::set<storm::expressions::Variable> const& metaVariables) const;
+
+ /*!
+ * Min-abstracts from the given meta variables.
+ *
+ * @param metaVariables The meta variables from which to abstract.
+ */
+ Dd<DdType::CUDD> minAbstract(std::set<storm::expressions::Variable> const& metaVariables) const;
+
+ /*!
+ * Max-abstracts from the given meta variables.
+ *
+ * @param metaVariables The meta variables from which to abstract.
+ */
+ Dd<DdType::CUDD> maxAbstract(std::set<storm::expressions::Variable> 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<DdType::CUDD> 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<DdType::CUDD> swapVariables(std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> 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<DdType::CUDD> multiplyMatrix(Dd<DdType::CUDD> const& otherMatrix, std::set<storm::expressions::Variable> 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<DdType::CUDD> andExists(Dd<DdType::CUDD> const& other, std::set<storm::expressions::Variable> 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<DdType::CUDD> greater(double value) const;
+
+ /*!
+ * Computes a DD that represents the function in which all assignments with a function value larger or equal
+ * to the given value are mapped to one and all others to zero.
+ *
+ * @param value The value used for the comparison.
+ * @return The resulting DD.
+ */
+ Dd<DdType::CUDD> greaterOrEqual(double value) const;
+
+ /*!
+ * Computes a DD that represents the function in which all assignments with a function value unequal to zero
+ * are mapped to one and all others to zero.
+ *
+ * @return The resulting DD.
+ */
+ Dd<DdType::CUDD> notZero() const;
+
+ /*!
+ * 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<DdType::CUDD> constrain(Dd<DdType::CUDD> 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<DdType::CUDD> restrict(Dd<DdType::CUDD> const& constraint) const;
+
+ /*!
+ * Retrieves the support of the current DD.
+ *
+ * @return The support represented as a DD.
+ */
+ Dd<DdType::CUDD> 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<storm::expressions::Variable, int_fast64_t> const& metaVariableToValueMap = std::map<storm::expressions::Variable, int_fast64_t>(), 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<storm::expressions::Variable, int_fast64_t> const& metaVariableToValueMap = std::map<storm::expressions::Variable, int_fast64_t>()) 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<typename ValueType>
+ std::vector<ValueType> 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<typename ValueType>
+ std::vector<ValueType> toVector(storm::dd::Odd<DdType::CUDD> 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<double> 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<double> toMatrix(storm::dd::Odd<DdType::CUDD> const& rowOdd, storm::dd::Odd<DdType::CUDD> 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<double> toMatrix(std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, storm::dd::Odd<DdType::CUDD> const& rowOdd, storm::dd::Odd<DdType::CUDD> 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<double> toMatrix(std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::set<storm::expressions::Variable> const& groupMetaVariables, storm::dd::Odd<DdType::CUDD> const& rowOdd, storm::dd::Odd<DdType::CUDD> 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<storm::expressions::Variable> 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<storm::expressions::Variable> 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<storm::expressions::Variable>& 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<DdManager<DdType::CUDD> 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<DdType::CUDD> 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<DdType::CUDD> 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<DdType::CUDD>& 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<DdType::CUDD> toBdd() const;
+
+ /*!
+ * Converts a BDD to an equivalent MTBDD.
+ *
+ * @return The corresponding MTBDD.
+ */
+ Dd<DdType::CUDD> 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<storm::expressions::Variable> 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<storm::expressions::Variable> 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<DdManager<DdType::CUDD> const> ddManager, ADD cuddDd, std::set<storm::expressions::Variable> const& containedMetaVariables = std::set<storm::expressions::Variable>());
+
+ /*!
+ * 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<DdManager<DdType::CUDD> const> ddManager, BDD cuddDd, std::set<storm::expressions::Variable> const& containedMetaVariables = std::set<storm::expressions::Variable>());
+
+ /*!
+ * 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<uint_fast64_t>& rowIndications, std::vector<storm::storage::MatrixEntry<uint_fast64_t, double>>& columnsAndValues, std::vector<uint_fast64_t> const& rowGroupOffsets, Odd<DdType::CUDD> const& rowOdd, Odd<DdType::CUDD> const& columnOdd, uint_fast64_t currentRowLevel, uint_fast64_t currentColumnLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, uint_fast64_t currentColumnOffset, std::vector<uint_fast64_t> const& ddRowVariableIndices, std::vector<uint_fast64_t> 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<Dd<DdType::CUDD>>& groups, std::vector<uint_fast64_t> const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::set<storm::expressions::Variable> 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<typename ValueType>
+ void addToVectorRec(DdNode const* dd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd<DdType::CUDD> const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<ValueType>& 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<uint_fast64_t> getSortedVariableIndices() const;
+
+ // A pointer to the manager responsible for this DD.
+ std::shared_ptr<DdManager<DdType::CUDD> const> ddManager;
+
+ // The ADD created by CUDD.
+ boost::variant<BDD, ADD> cuddDd;
+
+ // The meta variables that appear in this DD.
+ std::set<storm::expressions::Variable> 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 <cstring>
+#include <algorithm>
+
+#include "src/storage/dd/CuddBdd.h"
+#include "src/storage/dd/CuddAdd.h"
+#include "src/storage/dd/CuddDdManager.h"
+
+namespace storm {
+ namespace dd {
+ Bdd<DdType::CUDD>::Bdd(std::shared_ptr<DdManager<DdType::CUDD> const> ddManager, BDD cuddDd, std::set<storm::expressions::Variable> const& containedMetaVariables) : Dd<DdType::CUDD>(ddManager, containedMetaVariables) {
+ // Intentionally left empty.
+ }
+
+ Add<DdType::CUDD> Bdd<DdType::CUDD>::toAdd() const {
+ return Add<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().Add(), this->getContainedMetaVariables());
+ }
+
+ BDD Bdd<DdType::CUDD>::getCuddBdd() const {
+ return this->cuddBdd;
+ }
+
+ DdNode* Bdd<DdType::CUDD>::getCuddDdNode() const {
+ return this->getCuddBdd().getNode();
+ }
+
+ bool Bdd<DdType::CUDD>::operator==(Bdd<DdType::CUDD> const& other) const {
+ return this->getCuddBdd() == other.getCuddBdd();
+ }
+
+ bool Bdd<DdType::CUDD>::operator!=(Bdd<DdType::CUDD> const& other) const {
+ return !(*this == other);
+ }
+
+ Bdd<DdType::CUDD> Bdd<DdType::CUDD>::ite(Bdd<DdType::CUDD> const& thenDd, Bdd<DdType::CUDD> const& elseDd) const {
+ std::set<storm::expressions::Variable> 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<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().Ite(thenDd.getCuddBdd(), elseDd.getCuddBdd()), metaVariableNames);
+ }
+
+ Bdd<DdType::CUDD> Bdd<DdType::CUDD>::operator!() const {
+ Bdd<DdType::CUDD> result(*this);
+ result.complement();
+ return result;
+ }
+
+ Bdd<DdType::CUDD>& Bdd<DdType::CUDD>::complement() {
+ this->cuddBdd = ~this->getCuddBdd();
+ }
+
+ Bdd<DdType::CUDD> Bdd<DdType::CUDD>::operator&&(Bdd<DdType::CUDD> const& other) const {
+ Dd<DdType::CUDD> result(*this);
+ result &= other;
+ return result;
+ }
+
+ Bdd<DdType::CUDD>& Bdd<DdType::CUDD>::operator&=(Bdd<DdType::CUDD> const& other) {
+ this->addMetaVariables(other.getContainedMetaVariables());
+ this->cuddBdd = this->getCuddBdd() & other.getCuddBdd();
+ return *this;
+ }
+
+ Bdd<DdType::CUDD> Bdd<DdType::CUDD>::operator||(Bdd<DdType::CUDD> const& other) const {
+ Bdd<DdType::CUDD> result(*this);
+ result |= other;
+ return result;
+ }
+
+ Bdd<DdType::CUDD>& Bdd<DdType::CUDD>::operator|=(Bdd<DdType::CUDD> const& other) {
+ this->addMetaVariables(other.getContainedMetaVariables());
+ this->cuddBdd = this->getCuddBdd() | other.getCuddBdd();
+ return *this;
+ }
+
+ Bdd<DdType::CUDD> Bdd<DdType::CUDD>::iff(Bdd<DdType::CUDD> const& other) const {
+ std::set<storm::expressions::Variable> metaVariables(this->getContainedMetaVariables());
+ metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end());
+ return Bdd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().Xnor(other.getCuddBdd()), metaVariables);
+ }
+
+ Bdd<DdType::CUDD> Bdd<DdType::CUDD>::exclusiveOr(Bdd<DdType::CUDD> const& other) const {
+ std::set<storm::expressions::Variable> metaVariables(this->getContainedMetaVariables());
+ metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end());
+ return Bdd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().Xor(other.getCuddBdd()), metaVariables);
+ }
+
+ Bdd<DdType::CUDD> Bdd<DdType::CUDD>::implies(Bdd<DdType::CUDD> const& other) const {
+ std::set<storm::expressions::Variable> metaVariables(this->getContainedMetaVariables());
+ metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end());
+ return Bdd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().Ite(other.getCuddBdd(), this->getDdManager()->getBddOne().getCuddBdd()), metaVariables);
+ }
+
+ Bdd<DdType::CUDD> Bdd<DdType::CUDD>::existsAbstract(std::set<storm::expressions::Variable> const& metaVariables) const {
+ Dd<DdType::CUDD> cubeDd(this->getDdManager()->getBddOne());
+
+ std::set<storm::expressions::Variable> 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<DdType::CUDD> const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable);
+ cubeDd &= ddMetaVariable.getCube();
+ }
+
+ return Bdd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().ExistAbstract(cubeDd.getCuddBdd()), newMetaVariables);
+ }
+
+ Dd<DdType::CUDD> Bdd<DdType::CUDD>::universalAbstract(std::set<storm::expressions::Variable> const& metaVariables) const {
+ Dd<DdType::CUDD> cubeDd(this->getDdManager()->getBddOne());
+
+ std::set<storm::expressions::Variable> 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<DdType::CUDD> const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable);
+ cubeDd &= ddMetaVariable.getCube();
+ }
+
+ return Bdd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().UnivAbstract(cubeDd.getCuddBdd()), newMetaVariables);
+ }
+
+ Dd<DdType::CUDD> Bdd<DdType::CUDD>::swapVariables(std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& metaVariablePairs) {
+ std::set<storm::expressions::Variable> newContainedMetaVariables;
+ std::vector<BDD> from;
+ std::vector<BDD> to;
+ for (auto const& metaVariablePair : metaVariablePairs) {
+ DdMetaVariable<DdType::CUDD> const& variable1 = this->getDdManager()->getMetaVariable(metaVariablePair.first);
+ DdMetaVariable<DdType::CUDD> 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<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().SwapVariables(from, to), newContainedMetaVariables);
+ }
+
+ Bdd<DdType::CUDD> Bdd<DdType::CUDD>::andExists(Bdd<DdType::CUDD> const& other, std::set<storm::expressions::Variable> const& existentialVariables) const {
+ STORM_LOG_WARN_COND(this->isBdd() && other.isBdd(), "Performing logical operation on MTBDD(s).");
+
+ Dd<DdType::CUDD> cubeDd(this->getDdManager()->getOne());
+ for (auto const& metaVariable : existentialVariables) {
+ DdMetaVariable<DdType::CUDD> const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable);
+ cubeDd &= ddMetaVariable.getCube();
+ }
+
+ std::set<storm::expressions::Variable> unionOfMetaVariables;
+ std::set_union(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end(), other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end(), std::inserter(unionOfMetaVariables, unionOfMetaVariables.begin()));
+ std::set<storm::expressions::Variable> containedMetaVariables;
+ std::set_difference(unionOfMetaVariables.begin(), unionOfMetaVariables.end(), existentialVariables.begin(), existentialVariables.end(), std::inserter(containedMetaVariables, containedMetaVariables.begin()));
+
+ return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().AndAbstract(other.getCuddBdd(), cubeDd.getCuddBdd()), containedMetaVariables);
+ }
+
+ Dd<DdType::CUDD> Bdd<DdType::CUDD>::constrain(Dd<DdType::CUDD> const& constraint) const {
+ std::set<storm::expressions::Variable> metaVariables(this->getContainedMetaVariables());
+ metaVariables.insert(constraint.getContainedMetaVariables().begin(), constraint.getContainedMetaVariables().end());
+
+ if (this->isBdd() && constraint.isBdd()) {
+ return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().Constrain(constraint.getCuddBdd()), metaVariables);
+ } else {
+ return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().Constrain(constraint.getCuddMtbdd()), metaVariables);
+ }
+ }
+
+ Dd<DdType::CUDD> Bdd<DdType::CUDD>::restrict(Dd<DdType::CUDD> const& constraint) const {
+ std::set<storm::expressions::Variable> metaVariables(this->getContainedMetaVariables());
+ metaVariables.insert(constraint.getContainedMetaVariables().begin(), constraint.getContainedMetaVariables().end());
+
+ if (this->isBdd() && constraint.isBdd()) {
+ return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().Restrict(constraint.getCuddBdd()), metaVariables);
+ } else {
+ return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().Restrict(constraint.getCuddMtbdd()), metaVariables);
+ }
+ }
+
+ Dd<DdType::CUDD> Bdd<DdType::CUDD>::getSupport() const {
+ if (this->isBdd()) {
+ return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().Support(), this->getContainedMetaVariables());
+ } else {
+ return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().Support(), this->getContainedMetaVariables());
+ }
+ }
+
+ uint_fast64_t Bdd<DdType::CUDD>::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<uint_fast64_t>(this->getCuddBdd().CountMinterm(static_cast<int>(numberOfDdVariables)));
+ } else {
+ return static_cast<uint_fast64_t>(this->getCuddMtbdd().CountMinterm(static_cast<int>(numberOfDdVariables)));
+ }
+ }
+
+ uint_fast64_t Bdd<DdType::CUDD>::getLeafCount() const {
+ if (this->isBdd()) {
+ return static_cast<uint_fast64_t>(this->getCuddBdd().CountLeaves());
+ } else {
+ return static_cast<uint_fast64_t>(this->getCuddMtbdd().CountLeaves());
+ }
+ }
+
+ uint_fast64_t Bdd<DdType::CUDD>::getNodeCount() const {
+ if (this->isBdd()) {
+ return static_cast<uint_fast64_t>(this->getCuddBdd().nodeCount());
+ } else {
+ return static_cast<uint_fast64_t>(this->getCuddMtbdd().nodeCount());
+ }
+ }
+
+ bool Bdd<DdType::CUDD>::isOne() const {
+ if (this->isBdd()) {
+ return this->getCuddBdd().IsOne();
+ } else {
+ return this->getCuddMtbdd().IsOne();
+ }
+ }
+
+ bool Bdd<DdType::CUDD>::isZero() const {
+ if (this->isBdd()) {
+ return this->getCuddBdd().IsZero();
+ } else {
+ return this->getCuddMtbdd().IsZero();
+ }
+ }
+
+ uint_fast64_t Bdd<DdType::CUDD>::getIndex() const {
+ if (this->isBdd()) {
+ return static_cast<uint_fast64_t>(this->getCuddBdd().NodeReadIndex());
+ } else {
+ return static_cast<uint_fast64_t>(this->getCuddMtbdd().NodeReadIndex());
+ }
+ }
+
+ std::vector<uint_fast64_t> Bdd<DdType::CUDD>::getSortedVariableIndices() const {
+ std::vector<uint_fast64_t> 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<DdType::CUDD>::exportToDot(std::string const& filename) const {
+ if (filename.empty()) {
+ if (this->isBdd()) {
+ std::vector<BDD> cuddBddVector = { this->getCuddBdd() };
+ this->getDdManager()->getCuddManager().DumpDot(cuddBddVector);
+ } else {
+ std::vector<ADD> cuddAddVector = { this->getCuddMtbdd() };
+ this->getDdManager()->getCuddManager().DumpDot(cuddAddVector);
+ }
+ } else {
+ // Build the name input of the DD.
+ std::vector<char*> 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<std::string> ddVariableNamesAsStrings = this->getDdManager()->getDdVariableNames();
+ std::vector<char*> 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<BDD> cuddBddVector = { this->getCuddBdd() };
+ this->getDdManager()->getCuddManager().DumpDot(cuddBddVector, &ddVariableNames[0], &ddNames[0], filePointer);
+ } else {
+ std::vector<ADD> 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<DdType::CUDD>& 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<DdType Type> class DdManager;
+ template<DdType Type> class Odd;
+ template<DdType Type> class Add;
+
+ template<>
+ class Bdd<DdType::CUDD> : public Dd<DdType::CUDD> {
+ public:
+ // Declare the DdManager and DdIterator class as friend so it can access the internals of a DD.
+ friend class DdManager<DdType::CUDD>;
+ friend class DdForwardIterator<DdType::CUDD>;
+ friend class Odd<DdType::CUDD>;
+
+ // Instantiate all copy/move constructors/assignments with the default implementation.
+ Bdd() = default;
+ Bdd(Bdd<DdType::CUDD> const& other) = default;
+ Bdd& operator=(Bdd<DdType::CUDD> const& other) = default;
+#ifndef WINDOWS
+ Bdd(Bdd<DdType::CUDD>&& other) = default;
+ Bdd& operator=(Bdd<DdType::CUDD>&& 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<DdType::CUDD> 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<DdType::CUDD> 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<DdType::CUDD> ite(Bdd<DdType::CUDD> const& thenBdd, Bdd<DdType::CUDD> 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<DdType::CUDD> operator||(Bdd<DdType::CUDD> 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<DdType::CUDD>& operator|=(Bdd<DdType::CUDD> 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<DdType::CUDD> operator&&(Bdd<DdType::CUDD> 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<DdType::CUDD>& operator&=(Bdd<DdType::CUDD> 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<DdType::CUDD> iff(Bdd<DdType::CUDD> 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<DdType::CUDD> exclusiveOr(Bdd<DdType::CUDD> 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<DdType::CUDD> implies(Bdd<DdType::CUDD> const& other) const;
+
+ /*!
+ * Logically inverts the current BDD.
+ *
+ * @return The resulting BDD.
+ */
+ Bdd<DdType::CUDD> operator!() const;
+
+ /*!
+ * Logically complements the current BDD.
+ *
+ * @return A reference to the current BDD after the operation.
+ */
+ Bdd<DdType::CUDD>& complement();
+
+ /*!
+ * Existentially abstracts from the given meta variables.
+ *
+ * @param metaVariables The meta variables from which to abstract.
+ */
+ Bdd<DdType::CUDD> existsAbstract(std::set<storm::expressions::Variable> const& metaVariables) const;
+
+ /*!
+ * Universally abstracts from the given meta variables.
+ *
+ * @param metaVariables The meta variables from which to abstract.
+ */
+ Bdd<DdType::CUDD> universalAbstract(std::set<storm::expressions::Variable> 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<DdType::CUDD> swapVariables(std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> 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<DdType::CUDD> andExists(Bdd<DdType::CUDD> const& other, std::set<storm::expressions::Variable> 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<DdType::CUDD> constrain(Bdd<DdType::CUDD> 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<DdType::CUDD> restrict(Bdd<DdType::CUDD> const& constraint) const;
+
+ /*!
+ * Retrieves the support of the current BDD.
+ *
+ * @return The support represented as a BDD.
+ */
+ virtual Bdd<DdType::CUDD> 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<DdType::CUDD>& bdd);
+
+ /*!
+ * Converts a BDD to an equivalent ADD.
+ *
+ * @return The corresponding ADD.
+ */
+ Add<DdType::CUDD> 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<DdManager<DdType::CUDD> const> ddManager, BDD cuddDd, std::set<storm::expressions::Variable> const& containedMetaVariables = std::set<storm::expressions::Variable>());
+
+ // 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 <cstring>
#include <algorithm>
#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<DdType::CUDD>::Dd(std::shared_ptr<DdManager<DdType::CUDD> const> ddManager, BDD cuddDd, std::set<storm::expressions::Variable> const& containedMetaVariables) : ddManager(ddManager), cuddDd(cuddDd), containedMetaVariables(containedMetaVariables) {
- // Intentionally left empty.
- }
-
- Dd<DdType::CUDD>::Dd(std::shared_ptr<DdManager<DdType::CUDD> const> ddManager, ADD cuddDd, std::set<storm::expressions::Variable> const& containedMetaVariables) : ddManager(ddManager), cuddDd(cuddDd), containedMetaVariables(containedMetaVariables) {
+ Dd<DdType::CUDD>::Dd(std::shared_ptr<DdManager<DdType::CUDD> const> ddManager, std::set<storm::expressions::Variable> const& containedMetaVariables) : ddManager(ddManager), containedMetaVariables(containedMetaVariables) {
// Intentionally left empty.
}
-
- bool Dd<DdType::CUDD>::isBdd() const {
- return this->cuddDd.which() == 0;
- }
-
- bool Dd<DdType::CUDD>::isMtbdd() const {
- return this->cuddDd.which() == 1;
- }
-
- Dd<DdType::CUDD> Dd<DdType::CUDD>::toBdd() const {
- if (this->isBdd()) {
- return *this;
- } else {
- return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().BddPattern(), this->containedMetaVariables);
- }
- }
-
- Dd<DdType::CUDD> Dd<DdType::CUDD>::toMtbdd() const {
- if (this->isMtbdd()) {
- return *this;
- } else {
- return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().Add(), this->containedMetaVariables);
- }
- }
-
- BDD Dd<DdType::CUDD>::getCuddBdd() const {
- if (this->isBdd()) {
- return boost::get<BDD>(this->cuddDd);
- } else {
- STORM_LOG_WARN_COND(false, "Implicitly converting MTBDD to BDD.");
- return this->getCuddMtbdd().BddPattern();
- }
- }
-
- ADD Dd<DdType::CUDD>::getCuddMtbdd() const {
- if (this->isMtbdd()) {
- return boost::get<ADD>(this->cuddDd);
- } else {
- STORM_LOG_WARN_COND(false, "Implicitly converting BDD to MTBDD.");
- return this->getCuddBdd().Add();
- }
- }
-
- ABDD const& Dd<DdType::CUDD>::getCuddDd() const {
- if (this->isBdd()) {
- return static_cast<ABDD const&>(boost::get<BDD>(this->cuddDd));
- } else {
- return static_cast<ABDD const&>(boost::get<ADD>(this->cuddDd));
- }
- }
-
- DdNode* Dd<DdType::CUDD>::getCuddDdNode() const {
- if (this->isBdd()) {
- return this->getCuddBdd().getNode();
- } else {
- return this->getCuddMtbdd().getNode();
- }
- }
-
- bool Dd<DdType::CUDD>::operator==(Dd<DdType::CUDD> 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<DdType::CUDD>::operator!=(Dd<DdType::CUDD> const& other) const {
- return !(*this == other);
- }
-
- Dd<DdType::CUDD> Dd<DdType::CUDD>::ite(Dd<DdType::CUDD> const& thenDd, Dd<DdType::CUDD> const& elseDd) const {
- std::set<storm::expressions::Variable> 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<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().Ite(thenDd.getCuddBdd(), elseDd.getCuddBdd()), metaVariableNames);
- } else {
- return Dd<DdType::CUDD>(this->getDdManager(), this->toMtbdd().getCuddMtbdd().Ite(thenDd.toMtbdd().getCuddMtbdd(), elseDd.toMtbdd().getCuddMtbdd()), metaVariableNames);
- }
- }
-
- Dd<DdType::CUDD> Dd<DdType::CUDD>::operator+(Dd<DdType::CUDD> const& other) const {
- Dd<DdType::CUDD> result(*this);
- result += other;
- return result;
- }
-
- Dd<DdType::CUDD>& Dd<DdType::CUDD>::operator+=(Dd<DdType::CUDD> 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<DdType::CUDD> Dd<DdType::CUDD>::operator*(Dd<DdType::CUDD> const& other) const {
- Dd<DdType::CUDD> result(*this);
- result *= other;
- return result;
- }
-
- Dd<DdType::CUDD>& Dd<DdType::CUDD>::operator*=(Dd<DdType::CUDD> 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<DdType::CUDD> Dd<DdType::CUDD>::operator-(Dd<DdType::CUDD> const& other) const {
- STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing arithmetical operation on BDD(s).");
- Dd<DdType::CUDD> result(*this);
- result -= other;
- return result;
- }
-
- Dd<DdType::CUDD> Dd<DdType::CUDD>::operator-() const {
- STORM_LOG_WARN_COND(this->isMtbdd(), "Performing arithmetical operation on BDD(s).");
- return this->getDdManager()->getZero(true) - *this;
- }
-
- Dd<DdType::CUDD>& Dd<DdType::CUDD>::operator-=(Dd<DdType::CUDD> 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<DdType::CUDD> Dd<DdType::CUDD>::operator/(Dd<DdType::CUDD> const& other) const {
- STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing arithmetical operation on BDD(s).");
- Dd<DdType::CUDD> result(*this);
- result /= other;
- return result;
- }
-
- Dd<DdType::CUDD>& Dd<DdType::CUDD>::operator/=(Dd<DdType::CUDD> 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<DdType::CUDD> Dd<DdType::CUDD>::operator!() const {
- Dd<DdType::CUDD> result(*this);
- result.complement();
- return result;
- }
-
- Dd<DdType::CUDD>& Dd<DdType::CUDD>::complement() {
- if (this->isBdd()) {
- this->cuddDd = ~this->getCuddBdd();
- } else {
- this->cuddDd = ~this->getCuddMtbdd();
- }
- return *this;
- }
-
- Dd<DdType::CUDD> Dd<DdType::CUDD>::operator&&(Dd<DdType::CUDD> const& other) const {
- Dd<DdType::CUDD> result(*this);
- result &= other;
- return result;
- }
-
- Dd<DdType::CUDD>& Dd<DdType::CUDD>::operator&=(Dd<DdType::CUDD> 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<DdType::CUDD> Dd<DdType::CUDD>::operator||(Dd<DdType::CUDD> const& other) const {
- Dd<DdType::CUDD> result(*this);
- result |= other;
- return result;
- }
-
- Dd<DdType::CUDD>& Dd<DdType::CUDD>::operator|=(Dd<DdType::CUDD> 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<DdType::CUDD> Dd<DdType::CUDD>::iff(Dd<DdType::CUDD> const& other) const {
- std::set<storm::expressions::Variable> metaVariables(this->getContainedMetaVariables());
- metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end());
- if (this->isBdd() && other.isBdd()) {
- return Dd<DdType::CUDD>(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<DdType::CUDD>(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<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().Xnor(other.getCuddBdd()), metaVariables);
- }
- }
-
- Dd<DdType::CUDD> Dd<DdType::CUDD>::exclusiveOr(Dd<DdType::CUDD> const& other) const {
- std::set<storm::expressions::Variable> metaVariables(this->getContainedMetaVariables());
- metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end());
- if (this->isBdd() && other.isBdd()) {
- return Dd<DdType::CUDD>(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<DdType::CUDD>(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<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().Xor(other.getCuddBdd()), metaVariables);
- }
- }
-
- Dd<DdType::CUDD> Dd<DdType::CUDD>::implies(Dd<DdType::CUDD> const& other) const {
- std::set<storm::expressions::Variable> 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<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().Ite(other.getCuddBdd(), this->getDdManager()->getOne().getCuddBdd()), metaVariables);
- }
-
- Dd<DdType::CUDD> Dd<DdType::CUDD>::equals(Dd<DdType::CUDD> const& other) const {
- STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing arithmetical operation on BDD(s).");
- std::set<storm::expressions::Variable> metaVariables(this->getContainedMetaVariables());
- metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end());
- return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().Equals(other.getCuddMtbdd()), metaVariables);
- }
-
- Dd<DdType::CUDD> Dd<DdType::CUDD>::notEquals(Dd<DdType::CUDD> const& other) const {
- STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing arithmetical operation on BDD(s).");
- std::set<storm::expressions::Variable> metaVariables(this->getContainedMetaVariables());
- metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end());
- return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().NotEquals(other.getCuddMtbdd()), metaVariables);
- }
-
- Dd<DdType::CUDD> Dd<DdType::CUDD>::less(Dd<DdType::CUDD> const& other) const {
- STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing arithmetical operation on BDD(s).");
- std::set<storm::expressions::Variable> metaVariables(this->getContainedMetaVariables());
- metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end());
- return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().LessThan(other.getCuddMtbdd()), metaVariables);
- }
-
- Dd<DdType::CUDD> Dd<DdType::CUDD>::lessOrEqual(Dd<DdType::CUDD> const& other) const {
- STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing arithmetical operation on BDD(s).");
- std::set<storm::expressions::Variable> metaVariables(this->getContainedMetaVariables());
- metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end());
- return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().LessThanOrEqual(other.getCuddMtbdd()), metaVariables);
- }
-
- Dd<DdType::CUDD> Dd<DdType::CUDD>::greater(Dd<DdType::CUDD> const& other) const {
- STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing arithmetical operation on BDD(s).");
- std::set<storm::expressions::Variable> metaVariables(this->getContainedMetaVariables());
- metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end());
- return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().GreaterThan(other.getCuddMtbdd()), metaVariables);
- }
-
- Dd<DdType::CUDD> Dd<DdType::CUDD>::greaterOrEqual(Dd<DdType::CUDD> const& other) const {
- STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing arithmetical operation on BDD(s).");
- std::set<storm::expressions::Variable> metaVariables(this->getContainedMetaVariables());
- metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end());
- return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().GreaterThanOrEqual(other.getCuddMtbdd()), metaVariables);
- }
-
- Dd<DdType::CUDD> Dd<DdType::CUDD>::minimum(Dd<DdType::CUDD> const& other) const {
- STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing arithmetical operation on BDD(s).");
- std::set<storm::expressions::Variable> metaVariables(this->getContainedMetaVariables());
- metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end());
- return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().Minimum(other.getCuddMtbdd()), metaVariables);
- }
-
- Dd<DdType::CUDD> Dd<DdType::CUDD>::maximum(Dd<DdType::CUDD> const& other) const {
- STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing arithmetical operation on BDD(s).");
- std::set<storm::expressions::Variable> metaVariables(this->getContainedMetaVariables());
- metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end());
- return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().Maximum(other.getCuddMtbdd()), metaVariables);
- }
-
- Dd<DdType::CUDD> Dd<DdType::CUDD>::existsAbstract(std::set<storm::expressions::Variable> const& metaVariables) const {
- STORM_LOG_WARN_COND(this->isBdd(), "Performing logical operation on MTBDD(s).");
-
- Dd<DdType::CUDD> cubeDd(this->getDdManager()->getOne(false));
- std::set<storm::expressions::Variable> 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<DdType::CUDD> const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable);
- cubeDd &= ddMetaVariable.getCube();
- }
-
- return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().ExistAbstract(cubeDd.getCuddBdd()), newMetaVariables);
- }
-
- Dd<DdType::CUDD> Dd<DdType::CUDD>::universalAbstract(std::set<storm::expressions::Variable> const& metaVariables) const {
- STORM_LOG_WARN_COND(this->isBdd(), "Performing logical operation on MTBDD(s).");
-
- Dd<DdType::CUDD> cubeDd(this->getDdManager()->getOne());
- std::set<storm::expressions::Variable> 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<DdType::CUDD> const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable);
- cubeDd &= ddMetaVariable.getCube();
- }
-
- return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().UnivAbstract(cubeDd.getCuddBdd()), newMetaVariables);
- }
-
- Dd<DdType::CUDD> Dd<DdType::CUDD>::sumAbstract(std::set<storm::expressions::Variable> const& metaVariables) const {
- STORM_LOG_WARN_COND(this->isMtbdd(), "Performing arithmetical operation on BDD(s).");
-
- Dd<DdType::CUDD> cubeDd(this->getDdManager()->getOne(true));
- std::set<storm::expressions::Variable> 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<DdType::CUDD> const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable);
- cubeDd *= ddMetaVariable.getCubeAsMtbdd();
- }
-
- return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().ExistAbstract(cubeDd.getCuddMtbdd()), newMetaVariables);
- }
-
- Dd<DdType::CUDD> Dd<DdType::CUDD>::minAbstract(std::set<storm::expressions::Variable> const& metaVariables) const {
- STORM_LOG_WARN_COND(this->isMtbdd(), "Performing arithmetical operation on BDD(s).");
-
- Dd<DdType::CUDD> cubeDd(this->getDdManager()->getOne(true));
- std::set<storm::expressions::Variable> 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<DdType::CUDD> const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable);
- cubeDd *= ddMetaVariable.getCubeAsMtbdd();
- }
-
- return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().MinAbstract(cubeDd.getCuddMtbdd()), newMetaVariables);
- }
-
- Dd<DdType::CUDD> Dd<DdType::CUDD>::maxAbstract(std::set<storm::expressions::Variable> const& metaVariables) const {
- STORM_LOG_WARN_COND(this->isMtbdd(), "Performing arithmetical operation on BDD(s).");
-
- Dd<DdType::CUDD> cubeDd(this->getDdManager()->getOne(true));
- std::set<storm::expressions::Variable> 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<DdType::CUDD> const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable);
- cubeDd *= ddMetaVariable.getCubeAsMtbdd();
- }
-
- return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().MaxAbstract(cubeDd.getCuddMtbdd()), newMetaVariables);
- }
-
- bool Dd<DdType::CUDD>::equalModuloPrecision(Dd<DdType::CUDD> 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<DdType::CUDD> Dd<DdType::CUDD>::swapVariables(std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& metaVariablePairs) {
- std::set<storm::expressions::Variable> newContainedMetaVariables;
- if (this->isBdd()) {
- std::vector<BDD> from;
- std::vector<BDD> to;
- for (auto const& metaVariablePair : metaVariablePairs) {
- DdMetaVariable<DdType::CUDD> const& variable1 = this->getDdManager()->getMetaVariable(metaVariablePair.first);
- DdMetaVariable<DdType::CUDD> 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<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().SwapVariables(from, to), newContainedMetaVariables);
- } else {
- std::vector<ADD> from;
- std::vector<ADD> to;
- for (auto const& metaVariablePair : metaVariablePairs) {
- DdMetaVariable<DdType::CUDD> const& variable1 = this->getDdManager()->getMetaVariable(metaVariablePair.first);
- DdMetaVariable<DdType::CUDD> 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<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().SwapVariables(from, to), newContainedMetaVariables);
- }
- }
-
- Dd<DdType::CUDD> Dd<DdType::CUDD>::multiplyMatrix(Dd<DdType::CUDD> const& otherMatrix, std::set<storm::expressions::Variable> const& summationMetaVariables) const {
- STORM_LOG_WARN_COND(this->isMtbdd() && otherMatrix.isMtbdd(), "Performing arithmetical operation on BDD(s).");
-
- // Create the CUDD summation variables.
- std::vector<ADD> summationDdVariables;
- for (auto const& metaVariable : summationMetaVariables) {
- for (auto const& ddVariable : this->getDdManager()->getMetaVariable(metaVariable).getDdVariables()) {
- summationDdVariables.push_back(ddVariable.getCuddMtbdd());
- }
- }
-
- std::set<storm::expressions::Variable> unionOfMetaVariables;
- std::set_union(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end(), otherMatrix.getContainedMetaVariables().begin(), otherMatrix.getContainedMetaVariables().end(), std::inserter(unionOfMetaVariables, unionOfMetaVariables.begin()));
- std::set<storm::expressions::Variable> containedMetaVariables;
- std::set_difference(unionOfMetaVariables.begin(), unionOfMetaVariables.end(), summationMetaVariables.begin(), summationMetaVariables.end(), std::inserter(containedMetaVariables, containedMetaVariables.begin()));
-
- return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().MatrixMultiply(otherMatrix.getCuddMtbdd(), summationDdVariables), containedMetaVariables);
- }
-
- Dd<DdType::CUDD> Dd<DdType::CUDD>::andExists(Dd<DdType::CUDD> const& other, std::set<storm::expressions::Variable> const& existentialVariables) const {
- STORM_LOG_WARN_COND(this->isBdd() && other.isBdd(), "Performing logical operation on MTBDD(s).");
-
- Dd<DdType::CUDD> cubeDd(this->getDdManager()->getOne());
- for (auto const& metaVariable : existentialVariables) {
- DdMetaVariable<DdType::CUDD> const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable);
- cubeDd &= ddMetaVariable.getCube();
- }
-
- std::set<storm::expressions::Variable> unionOfMetaVariables;
- std::set_union(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end(), other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end(), std::inserter(unionOfMetaVariables, unionOfMetaVariables.begin()));
- std::set<storm::expressions::Variable> containedMetaVariables;
- std::set_difference(unionOfMetaVariables.begin(), unionOfMetaVariables.end(), existentialVariables.begin(), existentialVariables.end(), std::inserter(containedMetaVariables, containedMetaVariables.begin()));
-
- return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().AndAbstract(other.getCuddBdd(), cubeDd.getCuddBdd()), containedMetaVariables);
- }
-
- Dd<DdType::CUDD> Dd<DdType::CUDD>::greater(double value) const {
- STORM_LOG_WARN_COND(this->isMtbdd(), "Performing arithmetical operation on BDD(s).");
- return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().BddStrictThreshold(value), this->getContainedMetaVariables());
- }
-
- Dd<DdType::CUDD> Dd<DdType::CUDD>::greaterOrEqual(double value) const {
- STORM_LOG_WARN_COND(this->isMtbdd(), "Performing arithmetical operation on BDD(s).");
- return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().BddThreshold(value), this->getContainedMetaVariables());
- }
-
- Dd<DdType::CUDD> Dd<DdType::CUDD>::notZero() const {
- return this->toBdd();
- }
-
- Dd<DdType::CUDD> Dd<DdType::CUDD>::constrain(Dd<DdType::CUDD> const& constraint) const {
- std::set<storm::expressions::Variable> metaVariables(this->getContainedMetaVariables());
- metaVariables.insert(constraint.getContainedMetaVariables().begin(), constraint.getContainedMetaVariables().end());
-
- if (this->isBdd() && constraint.isBdd()) {
- return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().Constrain(constraint.getCuddBdd()), metaVariables);
- } else {
- return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().Constrain(constraint.getCuddMtbdd()), metaVariables);
- }
- }
-
- Dd<DdType::CUDD> Dd<DdType::CUDD>::restrict(Dd<DdType::CUDD> const& constraint) const {
- std::set<storm::expressions::Variable> metaVariables(this->getContainedMetaVariables());
- metaVariables.insert(constraint.getContainedMetaVariables().begin(), constraint.getContainedMetaVariables().end());
-
- if (this->isBdd() && constraint.isBdd()) {
- return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().Restrict(constraint.getCuddBdd()), metaVariables);
- } else {
- return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().Restrict(constraint.getCuddMtbdd()), metaVariables);
- }
- }
-
- Dd<DdType::CUDD> Dd<DdType::CUDD>::getSupport() const {
- if (this->isBdd()) {
- return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().Support(), this->getContainedMetaVariables());
- } else {
- return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().Support(), this->getContainedMetaVariables());
- }
- }
-
- uint_fast64_t Dd<DdType::CUDD>::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<uint_fast64_t>(this->getCuddBdd().CountMinterm(static_cast<int>(numberOfDdVariables)));
- } else {
- return static_cast<uint_fast64_t>(this->getCuddMtbdd().CountMinterm(static_cast<int>(numberOfDdVariables)));
- }
- }
-
- uint_fast64_t Dd<DdType::CUDD>::getLeafCount() const {
- if (this->isBdd()) {
- return static_cast<uint_fast64_t>(this->getCuddBdd().CountLeaves());
- } else {
- return static_cast<uint_fast64_t>(this->getCuddMtbdd().CountLeaves());
- }
- }
-
- uint_fast64_t Dd<DdType::CUDD>::getNodeCount() const {
- if (this->isBdd()) {
- return static_cast<uint_fast64_t>(this->getCuddBdd().nodeCount());
- } else {
- return static_cast<uint_fast64_t>(this->getCuddMtbdd().nodeCount());
- }
- }
-
- double Dd<DdType::CUDD>::getMin() const {
- STORM_LOG_WARN_COND(this->isMtbdd(), "Performing arithmetical operation on BDD(s).");
-
- ADD constantMinAdd = this->getCuddMtbdd().FindMin();
- return static_cast<double>(Cudd_V(constantMinAdd.getNode()));
- }
-
- double Dd<DdType::CUDD>::getMax() const {
- STORM_LOG_WARN_COND(this->isMtbdd(), "Performing arithmetical operation on BDD(s).");
-
- ADD constantMaxAdd = this->getCuddMtbdd().FindMax();
- return static_cast<double>(Cudd_V(constantMaxAdd.getNode()));
- }
-
- void Dd<DdType::CUDD>::setValue(storm::expressions::Variable const& metaVariable, int_fast64_t variableValue, double targetValue) {
- std::map<storm::expressions::Variable, int_fast64_t> metaVariableToValueMap;
- metaVariableToValueMap.emplace(metaVariable, variableValue);
- this->setValue(metaVariableToValueMap, targetValue);
- }
-
- void Dd<DdType::CUDD>::setValue(storm::expressions::Variable const& metaVariable1, int_fast64_t variableValue1, storm::expressions::Variable const& metaVariable2, int_fast64_t variableValue2, double targetValue) {
- std::map<storm::expressions::Variable, int_fast64_t> metaVariableToValueMap;
- metaVariableToValueMap.emplace(metaVariable1, variableValue1);
- metaVariableToValueMap.emplace(metaVariable2, variableValue2);
- this->setValue(metaVariableToValueMap, targetValue);
- }
-
- void Dd<DdType::CUDD>::setValue(std::map<storm::expressions::Variable, int_fast64_t> const& metaVariableToValueMap, double targetValue) {
- if (this->isBdd()) {
- STORM_LOG_THROW(targetValue == storm::utility::zero<double>() || targetValue == storm::utility::one<double>(), storm::exceptions::InvalidArgumentException, "Cannot set encoding to non-0, non-1 value " << targetValue << " in BDD.");
- Dd<DdType::CUDD> 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<double>()) {
- 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<DdType::CUDD> 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<DdType::CUDD>::getValue(std::map<storm::expressions::Variable, int_fast64_t> const& metaVariableToValueMap) const {
- std::set<storm::expressions::Variable> remainingMetaVariables(this->getContainedMetaVariables());
- Dd<DdType::CUDD> 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<DdType::CUDD> value = *this && valueEncoding;
- return value.isZero() ? 0 : 1;
- } else {
- Dd<DdType::CUDD> value = *this * valueEncoding.toMtbdd();
- value = value.sumAbstract(this->getContainedMetaVariables());
- return static_cast<double>(Cudd_V(value.getCuddMtbdd().getNode()));
- }
- }
-
- bool Dd<DdType::CUDD>::isOne() const {
- if (this->isBdd()) {
- return this->getCuddBdd().IsOne();
- } else {
- return this->getCuddMtbdd().IsOne();
- }
- }
-
- bool Dd<DdType::CUDD>::isZero() const {
- if (this->isBdd()) {
- return this->getCuddBdd().IsZero();
- } else {
- return this->getCuddMtbdd().IsZero();
- }
- }
-
- bool Dd<DdType::CUDD>::isConstant() const {
- if (this->isBdd()) {
- return Cudd_IsConstant(this->getCuddBdd().getNode());
- } else {
- return Cudd_IsConstant(this->getCuddMtbdd().getNode());
- }
- }
-
- uint_fast64_t Dd<DdType::CUDD>::getIndex() const {
- if (this->isBdd()) {
- return static_cast<uint_fast64_t>(this->getCuddBdd().NodeReadIndex());
- } else {
- return static_cast<uint_fast64_t>(this->getCuddMtbdd().NodeReadIndex());
- }
- }
-
- template<typename ValueType>
- std::vector<ValueType> Dd<DdType::CUDD>::toVector() const {
- STORM_LOG_THROW(this->isMtbdd(), storm::exceptions::IllegalFunctionCallException, "Cannot create vector from BDD.");
- return this->toVector<ValueType>(Odd<DdType::CUDD>(*this));
- }
-
- template<typename ValueType>
- std::vector<ValueType> Dd<DdType::CUDD>::toVector(Odd<DdType::CUDD> const& rowOdd) const {
- STORM_LOG_THROW(this->isMtbdd(), storm::exceptions::IllegalFunctionCallException, "Cannot create vector from BDD.");
- std::vector<ValueType> result(rowOdd.getTotalOffset());
- std::vector<uint_fast64_t> ddVariableIndices = this->getSortedVariableIndices();
- addToVectorRec(this->getCuddDdNode(), 0, ddVariableIndices.size(), 0, rowOdd, ddVariableIndices, result);
- return result;
- }
-
- storm::storage::SparseMatrix<double> Dd<DdType::CUDD>::toMatrix() const {
- STORM_LOG_THROW(this->isMtbdd(), storm::exceptions::IllegalFunctionCallException, "Cannot create matrix from BDD.");
- std::set<storm::expressions::Variable> rowVariables;
- std::set<storm::expressions::Variable> 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<DdType::CUDD>(this->existsAbstract(rowVariables)), Odd<DdType::CUDD>(this->existsAbstract(columnVariables)));
- }
-
- storm::storage::SparseMatrix<double> Dd<DdType::CUDD>::toMatrix(storm::dd::Odd<DdType::CUDD> const& rowOdd, storm::dd::Odd<DdType::CUDD> const& columnOdd) const {
- STORM_LOG_THROW(this->isMtbdd(), storm::exceptions::IllegalFunctionCallException, "Cannot create matrix from BDD.");
- std::set<storm::expressions::Variable> rowMetaVariables;
- std::set<storm::expressions::Variable> 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<double> Dd<DdType::CUDD>::toMatrix(std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, storm::dd::Odd<DdType::CUDD> const& rowOdd, storm::dd::Odd<DdType::CUDD> const& columnOdd) const {
- STORM_LOG_THROW(this->isMtbdd(), storm::exceptions::IllegalFunctionCallException, "Cannot create matrix from BDD.");
- std::vector<uint_fast64_t> ddRowVariableIndices;
- std::vector<uint_fast64_t> ddColumnVariableIndices;
-
- for (auto const& variable : rowMetaVariables) {
- DdMetaVariable<DdType::CUDD> const& metaVariable = this->getDdManager()->getMetaVariable(variable);
- for (auto const& ddVariable : metaVariable.getDdVariables()) {
- ddRowVariableIndices.push_back(ddVariable.getIndex());
- }
- }
- for (auto const& variable : columnMetaVariables) {
- DdMetaVariable<DdType::CUDD> 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<uint_fast64_t> rowIndications(rowOdd.getTotalOffset() + 1);
- std::vector<storm::storage::MatrixEntry<uint_fast64_t, double>> columnsAndValues(this->getNonZeroCount());
-
- // Create a trivial row grouping.
- std::vector<uint_fast64_t> 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<double>(columnOdd.getTotalOffset(), std::move(rowIndications), std::move(columnsAndValues), std::move(trivialRowGroupIndices));
- }
-
- storm::storage::SparseMatrix<double> Dd<DdType::CUDD>::toMatrix(std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::set<storm::expressions::Variable> const& groupMetaVariables, storm::dd::Odd<DdType::CUDD> const& rowOdd, storm::dd::Odd<DdType::CUDD> const& columnOdd) const {
- STORM_LOG_THROW(this->isMtbdd(), storm::exceptions::IllegalFunctionCallException, "Cannot create matrix from BDD.");
- std::vector<uint_fast64_t> ddRowVariableIndices;
- std::vector<uint_fast64_t> ddColumnVariableIndices;
- std::vector<uint_fast64_t> ddGroupVariableIndices;
- std::set<storm::expressions::Variable> rowAndColumnMetaVariables;
-
- for (auto const& variable : rowMetaVariables) {
- DdMetaVariable<DdType::CUDD> 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<DdType::CUDD> 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<DdType::CUDD> 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<DdType::CUDD> stateToNumberOfChoices = this->notZero().existsAbstract(columnMetaVariables).sumAbstract(groupMetaVariables);
- std::vector<uint_fast64_t> rowGroupIndices = stateToNumberOfChoices.toVector<uint_fast64_t>(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<Dd<DdType::CUDD>> groups;
- splitGroupsRec(this->getCuddDdNode(), groups, ddGroupVariableIndices, 0, ddGroupVariableIndices.size(), rowAndColumnMetaVariables);
-
- // Create the actual storage for the non-zero entries.
- std::vector<storm::storage::MatrixEntry<uint_fast64_t, double>> columnsAndValues(this->getNonZeroCount());
-
- // Now compute the indices at which the individual rows start.
- std::vector<uint_fast64_t> rowIndications(rowGroupIndices.back() + 1);
- std::vector<storm::dd::Dd<DdType::CUDD>> 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<double>(columnOdd.getTotalOffset(), std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices));
- }
-
- void Dd<DdType::CUDD>::toMatrixRec(DdNode const* dd, std::vector<uint_fast64_t>& rowIndications, std::vector<storm::storage::MatrixEntry<uint_fast64_t, double>>& columnsAndValues, std::vector<uint_fast64_t> const& rowGroupOffsets, Odd<DdType::CUDD> const& rowOdd, Odd<DdType::CUDD> const& columnOdd, uint_fast64_t currentRowLevel, uint_fast64_t currentColumnLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, uint_fast64_t currentColumnOffset, std::vector<uint_fast64_t> const& ddRowVariableIndices, std::vector<uint_fast64_t> 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<uint_fast64_t, double>(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<DdType::CUDD>::splitGroupsRec(DdNode* dd, std::vector<Dd<DdType::CUDD>>& groups, std::vector<uint_fast64_t> const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::set<storm::expressions::Variable> 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<DdType::CUDD>(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<typename ValueType>
- void Dd<DdType::CUDD>::addToVectorRec(DdNode const* dd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd<DdType::CUDD> const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<ValueType>& 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<ValueType>(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<uint_fast64_t> Dd<DdType::CUDD>::getSortedVariableIndices() const {
- std::vector<uint_fast64_t> 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<DdType::CUDD>::containsMetaVariable(storm::expressions::Variable const& metaVariable) const {
return containedMetaVariables.find(metaVariable) != containedMetaVariables.end();
}
bool Dd<DdType::CUDD>::containsMetaVariables(std::set<storm::expressions::Variable> 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<storm::expressions::Variable> const& Dd<DdType::CUDD>::getContainedMetaVariables() const {
@@ -1045,130 +25,28 @@ namespace storm {
return this->containedMetaVariables;
}
- void Dd<DdType::CUDD>::exportToDot(std::string const& filename) const {
- if (filename.empty()) {
- if (this->isBdd()) {
- std::vector<BDD> cuddBddVector = { this->getCuddBdd() };
- this->getDdManager()->getCuddManager().DumpDot(cuddBddVector);
- } else {
- std::vector<ADD> cuddAddVector = { this->getCuddMtbdd() };
- this->getDdManager()->getCuddManager().DumpDot(cuddAddVector);
- }
- } else {
- // Build the name input of the DD.
- std::vector<char*> 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<std::string> ddVariableNamesAsStrings = this->getDdManager()->getDdVariableNames();
- std::vector<char*> 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<BDD> cuddBddVector = { this->getCuddBdd() };
- this->getDdManager()->getCuddManager().DumpDot(cuddBddVector, &ddVariableNames[0], &ddNames[0], filePointer);
- } else {
- std::vector<ADD> 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<DdType::CUDD>::addContainedMetaVariable(storm::expressions::Variable const& metaVariable) {
- this->getContainedMetaVariables().insert(metaVariable);
- }
-
- void Dd<DdType::CUDD>::removeContainedMetaVariable(storm::expressions::Variable const& metaVariable) {
- this->getContainedMetaVariables().erase(metaVariable);
- }
-
std::shared_ptr<DdManager<DdType::CUDD> const> Dd<DdType::CUDD>::getDdManager() const {
return this->ddManager;
}
-
- DdForwardIterator<DdType::CUDD> Dd<DdType::CUDD>::begin(bool enumerateDontCareMetaVariables) const {
- int* cube;
- double value;
- DdGen* generator = this->getCuddDd().FirstCube(&cube, &value);
- return DdForwardIterator<DdType::CUDD>(this->getDdManager(), generator, cube, value, (Cudd_IsGenEmpty(generator) != 0), &this->getContainedMetaVariables(), enumerateDontCareMetaVariables);
- }
-
- DdForwardIterator<DdType::CUDD> Dd<DdType::CUDD>::end(bool enumerateDontCareMetaVariables) const {
- return DdForwardIterator<DdType::CUDD>(this->getDdManager(), nullptr, nullptr, 0, true, nullptr, enumerateDontCareMetaVariables);
- }
-
- storm::expressions::Expression Dd<DdType::CUDD>::toExpression() const {
- return toExpressionRecur(this->getCuddDdNode(), this->getDdManager()->getDdVariables());
- }
-
- storm::expressions::Expression Dd<DdType::CUDD>::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<DdType::CUDD>::addMetaVariables(std::set<storm::expressions::Variable> const& metaVariables) {
+ std::set<storm::expressions::Variable> 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<DdType::CUDD>::toExpressionRecur(DdNode const* dd, std::vector<storm::expressions::Variable> 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<double>(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<DdType::CUDD>::addMetaVariable(storm::expressions::Variable const& metaVariable) {
+ this->getContainedMetaVariables().insert(metaVariable);
}
-
- storm::expressions::Expression Dd<DdType::CUDD>::getMintermExpressionRecur(::DdManager* manager, DdNode const* dd, std::vector<storm::expressions::Variable> 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<DdType::CUDD>::removeMetaVariable(storm::expressions::Variable const& metaVariable) {
+ this->getContainedMetaVariables().erase(metaVariable);
}
-
- std::ostream& operator<<(std::ostream& out, const Dd<DdType::CUDD>& dd) {
- dd.exportToDot();
- return out;
+
+ void Dd<DdType::CUDD>::removeMetaVariables(std::set<storm::expressions::Variable> const& metaVariables) {
+ std::set<storm::expressions::Variable> 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<double> Dd<DdType::CUDD>::toVector() const;
- template std::vector<double> Dd<DdType::CUDD>::toVector(Odd<DdType::CUDD> const& rowOdd) const;
- template void Dd<DdType::CUDD>::addToVectorRec(DdNode const* dd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd<DdType::CUDD> const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<double>& targetVector) const;
- template std::vector<uint_fast64_t> Dd<DdType::CUDD>::toVector() const;
- template std::vector<uint_fast64_t> Dd<DdType::CUDD>::toVector(Odd<DdType::CUDD> const& rowOdd) const;
- template void Dd<DdType::CUDD>::addToVectorRec(DdNode const* dd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd<DdType::CUDD> const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<uint_fast64_t>& 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 <map>
#include <set>
#include <memory>
-#include <iostream>
-#include <boost/variant.hpp>
#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<DdType Type> class DdManager;
template<DdType Type> class Odd;
+ template<DdType Type> class Bdd;
template<>
class Dd<DdType::CUDD> {
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<DdType::CUDD>;
- friend class DdForwardIterator<DdType::CUDD>;
- friend class Odd<DdType::CUDD>;
// Instantiate all copy/move constructors/assignments with the default implementation.
Dd() = default;
@@ -40,540 +33,40 @@ namespace storm {
Dd& operator=(Dd<DdType::CUDD>&& 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<DdType::CUDD> 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<DdType::CUDD> 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<DdType::CUDD> ite(Dd<DdType::CUDD> const& thenDd, Dd<DdType::CUDD> 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<DdType::CUDD> operator||(Dd<DdType::CUDD> 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<DdType::CUDD>& operator|=(Dd<DdType::CUDD> 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<DdType::CUDD> operator&&(Dd<DdType::CUDD> 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<DdType::CUDD>& operator&=(Dd<DdType::CUDD> 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<DdType::CUDD> iff(Dd<DdType::CUDD> 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<DdType::CUDD> exclusiveOr(Dd<DdType::CUDD> 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<DdType::CUDD> implies(Dd<DdType::CUDD> const& other) const;
-
- /*!
- * Adds the two DDs.
- *
- * @param other The DD to add to the current one.
- * @return The result of the addition.
- */
- Dd<DdType::CUDD> operator+(Dd<DdType::CUDD> 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<DdType::CUDD>& operator+=(Dd<DdType::CUDD> const& other);
-
- /*!
- * Multiplies the two DDs.
- *
- * @param other The DD to multiply with the current one.
- * @return The result of the multiplication.
- */
- Dd<DdType::CUDD> operator*(Dd<DdType::CUDD> 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<DdType::CUDD>& operator*=(Dd<DdType::CUDD> 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<DdType::CUDD> operator-(Dd<DdType::CUDD> const& other) const;
-
- /*!
- * Subtracts the DD from the constant zero function.
- *
- * @return The resulting function represented as a DD.
- */
- Dd<DdType::CUDD> 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<DdType::CUDD>& operator-=(Dd<DdType::CUDD> 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<DdType::CUDD> operator/(Dd<DdType::CUDD> 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<DdType::CUDD>& operator/=(Dd<DdType::CUDD> 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<DdType::CUDD> 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<DdType::CUDD>& 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<DdType::CUDD> equals(Dd<DdType::CUDD> 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<DdType::CUDD> notEquals(Dd<DdType::CUDD> 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<DdType::CUDD> less(Dd<DdType::CUDD> 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<DdType::CUDD> lessOrEqual(Dd<DdType::CUDD> 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<DdType::CUDD> greater(Dd<DdType::CUDD> 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<DdType::CUDD> greaterOrEqual(Dd<DdType::CUDD> 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<DdType::CUDD> minimum(Dd<DdType::CUDD> 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<DdType::CUDD> maximum(Dd<DdType::CUDD> const& other) const;
-
- /*!
- * Existentially abstracts from the given meta variables.
- *
- * @param metaVariables The meta variables from which to abstract.
- */
- Dd<DdType::CUDD> existsAbstract(std::set<storm::expressions::Variable> const& metaVariables) const;
-
- /*!
- * Universally abstracts from the given meta variables.
- *
- * @param metaVariables The meta variables from which to abstract.
- */
- Dd<DdType::CUDD> universalAbstract(std::set<storm::expressions::Variable> const& metaVariables) const;
-
- /*!
- * Sum-abstracts from the given meta variables.
- *
- * @param metaVariables The meta variables from which to abstract.
- */
- Dd<DdType::CUDD> sumAbstract(std::set<storm::expressions::Variable> const& metaVariables) const;
-
- /*!
- * Min-abstracts from the given meta variables.
- *
- * @param metaVariables The meta variables from which to abstract.
- */
- Dd<DdType::CUDD> minAbstract(std::set<storm::expressions::Variable> const& metaVariables) const;
-
- /*!
- * Max-abstracts from the given meta variables.
- *
- * @param metaVariables The meta variables from which to abstract.
- */
- Dd<DdType::CUDD> maxAbstract(std::set<storm::expressions::Variable> 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<DdType::CUDD> 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<DdType::CUDD> swapVariables(std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> 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<DdType::CUDD> multiplyMatrix(Dd<DdType::CUDD> const& otherMatrix, std::set<storm::expressions::Variable> 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<DdType::CUDD> andExists(Dd<DdType::CUDD> const& other, std::set<storm::expressions::Variable> 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<DdType::CUDD> greater(double value) const;
-
- /*!
- * Computes a DD that represents the function in which all assignments with a function value larger or equal
- * to the given value are mapped to one and all others to zero.
- *
- * @param value The value used for the comparison.
- * @return The resulting DD.
- */
- Dd<DdType::CUDD> greaterOrEqual(double value) const;
-
- /*!
- * Computes a DD that represents the function in which all assignments with a function value unequal to zero
- * are mapped to one and all others to zero.
- *
- * @return The resulting DD.
- */
- Dd<DdType::CUDD> notZero() const;
-
- /*!
- * 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<DdType::CUDD> constrain(Dd<DdType::CUDD> 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<DdType::CUDD> restrict(Dd<DdType::CUDD> 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<DdType::CUDD> getSupport() const;
+ virtual Bdd<DdType::CUDD> 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<storm::expressions::Variable, int_fast64_t> const& metaVariableToValueMap = std::map<storm::expressions::Variable, int_fast64_t>(), 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<storm::expressions::Variable, int_fast64_t> const& metaVariableToValueMap = std::map<storm::expressions::Variable, int_fast64_t>()) 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<typename ValueType>
- std::vector<ValueType> 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<typename ValueType>
- std::vector<ValueType> toVector(storm::dd::Odd<DdType::CUDD> 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<double> 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<double> toMatrix(storm::dd::Odd<DdType::CUDD> const& rowOdd, storm::dd::Odd<DdType::CUDD> 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<double> toMatrix(std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, storm::dd::Odd<DdType::CUDD> const& rowOdd, storm::dd::Odd<DdType::CUDD> 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<double> toMatrix(std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::set<storm::expressions::Variable> const& groupMetaVariables, storm::dd::Odd<DdType::CUDD> const& rowOdd, storm::dd::Odd<DdType::CUDD> 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<storm::expressions::Variable> 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<storm::expressions::Variable>& 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<DdManager<DdType::CUDD> 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<DdType::CUDD> 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<DdType::CUDD> 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<DdType::CUDD>& 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<DdType::CUDD> toBdd() const;
-
- /*!
- * Converts a BDD to an equivalent MTBDD.
- *
- * @return The corresponding MTBDD.
- */
- Dd<DdType::CUDD> 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<storm::expressions::Variable>& 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<storm::expressions::Variable> 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<storm::expressions::Variable> const& variables);
+ void removeMetaVariables(std::set<storm::expressions::Variable> 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<storm::expressions::Variable> 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<DdManager<DdType::CUDD> const> ddManager, ADD cuddDd, std::set<storm::expressions::Variable> const& containedMetaVariables = std::set<storm::expressions::Variable>());
-
- /*!
- * 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<DdManager<DdType::CUDD> const> ddManager, BDD cuddDd, std::set<storm::expressions::Variable> const& containedMetaVariables = std::set<storm::expressions::Variable>());
-
- /*!
- * 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<uint_fast64_t>& rowIndications, std::vector<storm::storage::MatrixEntry<uint_fast64_t, double>>& columnsAndValues, std::vector<uint_fast64_t> const& rowGroupOffsets, Odd<DdType::CUDD> const& rowOdd, Odd<DdType::CUDD> const& columnOdd, uint_fast64_t currentRowLevel, uint_fast64_t currentColumnLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, uint_fast64_t currentColumnOffset, std::vector<uint_fast64_t> const& ddRowVariableIndices, std::vector<uint_fast64_t> 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<Dd<DdType::CUDD>>& groups, std::vector<uint_fast64_t> const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::set<storm::expressions::Variable> const& remainingMetaVariables) const;
+ Dd(std::shared_ptr<DdManager<DdType::CUDD> const> ddManager, std::set<storm::expressions::Variable> const& containedMetaVariables = std::set<storm::expressions::Variable>());
- /*!
- * 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<typename ValueType>
- void addToVectorRec(DdNode const* dd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd<DdType::CUDD> const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<ValueType>& 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<uint_fast64_t> getSortedVariableIndices() const;
+ private:
// A pointer to the manager responsible for this DD.
std::shared_ptr<DdManager<DdType::CUDD> const> ddManager;
- // The ADD created by CUDD.
- boost::variant<BDD, ADD> cuddDd;
-
// The meta variables that appear in this DD.
std::set<storm::expressions::Variable> containedMetaVariables;
};