diff --git a/src/storage/dd/CuddDd.cpp b/src/storage/dd/CuddDd.cpp
index d3ad10493..23f148da0 100644
--- a/src/storage/dd/CuddDd.cpp
+++ b/src/storage/dd/CuddDd.cpp
@@ -1,8 +1,9 @@
#include "src/storage/dd/CuddDd.h"
+#include "src/storage/dd/CuddDdManager.h"
namespace storm {
namespace dd {
- Dd(std::shared_ptr<DdManager<CUDD>> ddManager, ADD cuddAdd, std::unordered_set<std::string> const& containedMetaVariableNames) noexcept : ddManager(ddManager), cuddAdd(cuddAdd), containedMetaVariableNames(containedMetaVariableNames) {
+ Dd<CUDD>::Dd(std::shared_ptr<DdManager<CUDD>> ddManager, ADD cuddAdd, std::unordered_set<std::string> const& containedMetaVariableNames) noexcept : ddManager(ddManager), cuddAdd(cuddAdd), containedMetaVariableNames(containedMetaVariableNames) {
// Intentionally left empty.
}
@@ -13,10 +14,10 @@ namespace storm {
}
Dd<CUDD>& Dd<CUDD>::operator+=(Dd<CUDD> const& other) {
- cuddAdd += other;
+ cuddAdd += other.getCuddAdd();
// Join the variable sets of the two participating DDs.
- std::copy(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().containedMetaVariableNames.end(), std::inserter(this->containedMetaVariableNames, this->containedMetaVariableNames.end()));
+ std::copy(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end(), std::inserter(this->containedMetaVariableNames, this->containedMetaVariableNames.end()));
return *this;
}
@@ -28,10 +29,10 @@ namespace storm {
}
Dd<CUDD>& Dd<CUDD>::operator*=(Dd<CUDD> const& other) {
- cuddAdd *= other;
+ cuddAdd *= other.getCuddAdd();
// Join the variable sets of the two participating DDs.
- std::copy(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().containedMetaVariableNames.end(), std::inserter(this->containedMetaVariableNames, this->containedMetaVariableNames.end()));
+ std::copy(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end(), std::inserter(this->containedMetaVariableNames, this->containedMetaVariableNames.end()));
return *this;
}
@@ -43,10 +44,10 @@ namespace storm {
}
Dd<CUDD>& Dd<CUDD>::operator-=(Dd<CUDD> const& other) {
- cuddAdd -= other;
+ cuddAdd -= other.getCuddAdd();
// Join the variable sets of the two participating DDs.
- std::copy(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().containedMetaVariableNames.end(), std::inserter(this->containedMetaVariableNames, this->containedMetaVariableNames.end()));
+ std::copy(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end(), std::inserter(this->containedMetaVariableNames, this->containedMetaVariableNames.end()));
return *this;
}
@@ -58,10 +59,10 @@ namespace storm {
}
Dd<CUDD>& Dd<CUDD>::operator/=(Dd<CUDD> const& other) {
- cuddAdd.Divide(other);
+ cuddAdd.Divide(other.getCuddAdd());
// Join the variable sets of the two participating DDs.
- std::copy(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().containedMetaVariableNames.end(), std::inserter(this->containedMetaVariableNames, this->containedMetaVariableNames.end()));
+ std::copy(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end(), std::inserter(this->containedMetaVariableNames, this->containedMetaVariableNames.end()));
return *this;
}
@@ -77,12 +78,137 @@ namespace storm {
return *this;
}
+ Dd<CUDD> Dd<CUDD>::equals(Dd<CUDD> const& other) const {
+ Dd<CUDD> result(*this);
+ result.getCuddAdd().Equals(other.getCuddAdd());
+ return result;
+ }
+
+ Dd<CUDD> Dd<CUDD>::notEquals(Dd<CUDD> const& other) const {
+ Dd<CUDD> result(*this);
+ result.getCuddAdd().NotEquals(other.getCuddAdd());
+ return result;
+ }
+
+ Dd<CUDD> Dd<CUDD>::less(Dd<CUDD> const& other) const {
+ Dd<CUDD> result(*this);
+ result.getCuddAdd().LessThan(other.getCuddAdd());
+ return result;
+ }
+
+ Dd<CUDD> Dd<CUDD>::lessOrEqual(Dd<CUDD> const& other) const {
+ Dd<CUDD> result(*this);
+ result.getCuddAdd().LessThanOrEqual(other.getCuddAdd());
+ return result;
+ }
+
+ Dd<CUDD> Dd<CUDD>::greater(Dd<CUDD> const& other) const {
+ Dd<CUDD> result(*this);
+ result.getCuddAdd().GreaterThan(other.getCuddAdd());
+ return result;
+ }
+
+ Dd<CUDD> Dd<CUDD>::greaterOrEqual(Dd<CUDD> const& other) const {
+ Dd<CUDD> result(*this);
+ result.getCuddAdd().GreaterThanOrEqual(other.getCuddAdd());
+ return result;
+ }
+
+ void Dd<CUDD>::existsAbstract(std::unordered_set<std::string> const& metaVariableNames) {
+ Dd<CUDD> cubeDd(this->getDdManager()->getOne());
+
+ for (auto const& metaVariableName : metaVariableNames) {
+ DdMetaVariable<CUDD> const& metaVariable = this->getDdManager()->getMetaVariable(metaVariableName);
+ cubeDd *= metaVariable.getCube();
+ }
+
+ this->getCuddAdd().OrAbstract(cubeDd.getCuddAdd());
+ }
+
+ void Dd<CUDD>::sumAbstract(std::unordered_set<std::string> const& metaVariableNames) {
+ Dd<CUDD> cubeDd(this->getDdManager()->getOne());
+
+ for (auto const& metaVariableName : metaVariableNames) {
+ DdMetaVariable<CUDD> const& metaVariable = this->getDdManager()->getMetaVariable(metaVariableName);
+ cubeDd *= metaVariable.getCube();
+ }
+
+ this->getCuddAdd().ExistAbstract(cubeDd.getCuddAdd());
+ }
+
+ void Dd<CUDD>::minAbstract(std::unordered_set<std::string> const& metaVariableNames) {
+ Dd<CUDD> cubeDd(this->getDdManager()->getOne());
+
+ for (auto const& metaVariableName : metaVariableNames) {
+ DdMetaVariable<CUDD> const& metaVariable = this->getDdManager()->getMetaVariable(metaVariableName);
+ cubeDd *= metaVariable.getCube();
+ }
+
+ this->getCuddAdd().Minimum(cubeDd.getCuddAdd());
+ }
+
+ void Dd<CUDD>::maxAbstract(std::unordered_set<std::string> const& metaVariableNames) {
+ Dd<CUDD> cubeDd(this->getDdManager()->getOne());
+
+ for (auto const& metaVariableName : metaVariableNames) {
+ DdMetaVariable<CUDD> const& metaVariable = this->getDdManager()->getMetaVariable(metaVariableName);
+ cubeDd *= metaVariable.getCube();
+ }
+
+ this->getCuddAdd().Maximum(cubeDd.getCuddAdd());
+ }
+
+ void Dd<CUDD>::setValue(std::string const& metaVariableName, int_fast64_t variableValue, double targetValue) {
+ std::unordered_map<std::string, int_fast64_t> metaVariableNameToValueMap;
+ metaVariableNameToValueMap.emplace(metaVariableName, variableValue);
+ this->setValue(metaVariableNameToValueMap, targetValue);
+ }
+
+ void Dd<CUDD>::setValue(std::string const& metaVariableName1, int_fast64_t variableValue1, std::string const& metaVariableName2, int_fast64_t variableValue2, double targetValue) {
+ std::unordered_map<std::string, int_fast64_t> metaVariableNameToValueMap;
+ metaVariableNameToValueMap.emplace(metaVariableName1, variableValue1);
+ metaVariableNameToValueMap.emplace(metaVariableName2, variableValue2);
+ this->setValue(metaVariableNameToValueMap, targetValue);
+ }
+
+ void Dd<CUDD>::setValue(std::unordered_map<std::string, int_fast64_t> const& metaVariableNameToValueMap, double targetValue) {
+ // TODO: Fill this
+ }
+
+ bool Dd<CUDD>::containsMetaVariable(std::string const& metaVariableName) const {
+ auto const& metaVariable = containedMetaVariableNames.find(metaVariableName);
+ return metaVariable != containedMetaVariableNames.end();
+ }
+
+ bool Dd<CUDD>::containsMetaVariables(std::unordered_set<std::string> metaVariableNames) const {
+ for (auto const& metaVariableName : metaVariableNames) {
+ auto const& metaVariable = containedMetaVariableNames.find(metaVariableName);
+
+ if (metaVariable == containedMetaVariableNames.end()) {
+ return false;
+ }
+ }
+ return true;
+ }
+
+ std::unordered_set<std::string> const& Dd<CUDD>::getContainedMetaVariableNames() const {
+ return containedMetaVariableNames;
+ }
+
void Dd<CUDD>::exportToDot(std::string const& filename) const {
FILE* filePointer = fopen(filename.c_str() , "w");
this->getDdManager()->getCuddManager().DumpDot({this->cuddAdd}, nullptr, nullptr, filePointer);
fclose(filePointer);
}
+ ADD Dd<CUDD>::getCuddAdd() {
+ return this->cuddAdd;
+ }
+
+ ADD const& Dd<CUDD>::getCuddAdd() const {
+ return this->cuddAdd;
+ }
+
std::shared_ptr<DdManager<CUDD>> Dd<CUDD>::getDdManager() const {
return this->ddManager;
}
diff --git a/src/storage/dd/CuddDd.h b/src/storage/dd/CuddDd.h
index eff759bd3..b0a3e33eb 100644
--- a/src/storage/dd/CuddDd.h
+++ b/src/storage/dd/CuddDd.h
@@ -1,14 +1,18 @@
#ifndef STORM_STORAGE_DD_CUDDDD_H_
#define STORM_STORAGE_DD_CUDDDD_H_
+#include <unordered_set>
+#include <unordered_map>
+
#include "src/storage/dd/Dd.h"
-#include "src/storage/dd/CuddDdManager.h"
// Include the C++-interface of CUDD.
#include "cuddObj.hh"
namespace storm {
namespace dd {
+ // Forward-declare the DdManager class.
+ template<DdType Type> class DdManager;
template<>
class Dd<CUDD> {
@@ -264,6 +268,20 @@ namespace storm {
std::shared_ptr<DdManager<CUDD>> getDdManager() const;
private:
+ /*!
+ * Retrieves the CUDD ADD object associated with this DD.
+ *
+ * @return The CUDD ADD object assoicated with this DD.
+ */
+ ADD getCuddAdd();
+
+ /*!
+ * Retrieves the CUDD ADD object associated with this DD.
+ *
+ * @return The CUDD ADD object assoicated with this DD.
+ */
+ ADD const& getCuddAdd() const;
+
/*!
* Creates a DD that encapsulates the given CUDD ADD.
*
diff --git a/src/storage/dd/CuddDdManager.cpp b/src/storage/dd/CuddDdManager.cpp
index 580c6c9a6..40c11fbaa 100644
--- a/src/storage/dd/CuddDdManager.cpp
+++ b/src/storage/dd/CuddDdManager.cpp
@@ -24,10 +24,10 @@ namespace storm {
std::vector<Dd<CUDD>> variables;
for (std::size_t i = 0; i < numberOfBits; ++i) {
- variables.emplace_back(cuddManager.addVar());
+ variables.emplace_back(Dd<CUDD>(this->shared_from_this(), cuddManager.addVar(), {name}));
}
- metaVariableMap.emplace(name, low, high, variables, this->shared_from_this());
+ metaVariableMap.emplace(name, DdMetaVariable<CUDD>(name, low, high, variables, this->shared_from_this()));
}
void DdManager<CUDD>::addMetaVariablesInterleaved(std::vector<std::string> const& names, int_fast64_t low, int_fast64_t high) {
@@ -40,13 +40,13 @@ namespace storm {
std::vector<std::vector<Dd<CUDD>>> variables;
for (uint_fast64_t bit = 0; bit < numberOfBits; ++bit) {
for (uint_fast64_t i = 0; i < names.size(); ++i) {
- variables[i].emplace_back(cuddManager.addVar());
+ variables[i].emplace_back(Dd<CUDD>(this->shared_from_this(), cuddManager.addVar(), {names[i]}));
}
}
// Now add the meta variables.
for (uint_fast64_t i = 0; i < names.size(); ++i) {
- metaVariableMap.emplace(names[i], low, high, variables[i], this->shared_from_this());
+ metaVariableMap.emplace(names[i], DdMetaVariable<CUDD>(names[i], low, high, variables[i], this->shared_from_this()));
}
}
diff --git a/src/storage/dd/CuddDdManager.h b/src/storage/dd/CuddDdManager.h
index 72f2aea0c..ede42104d 100644
--- a/src/storage/dd/CuddDdManager.h
+++ b/src/storage/dd/CuddDdManager.h
@@ -16,7 +16,6 @@ namespace storm {
template<>
class DdManager<CUDD> : std::enable_shared_from_this<DdManager<CUDD>> {
// To break the cylic dependencies, we need to forward-declare the other DD-related classes.
- friend class DdMetaVariable<CUDD>;
friend class Dd<CUDD>;
/*!
diff --git a/src/storage/dd/DdMetaVariable.cpp b/src/storage/dd/DdMetaVariable.cpp
index c2795562b..d5cae858c 100644
--- a/src/storage/dd/DdMetaVariable.cpp
+++ b/src/storage/dd/DdMetaVariable.cpp
@@ -1,4 +1,5 @@
#include "src/storage/dd/DdMetaVariable.h"
+#include "src/storage/dd/CuddDdManager.h"
namespace storm {
namespace dd {
diff --git a/src/storage/dd/DdMetaVariable.h b/src/storage/dd/DdMetaVariable.h
index f784fda2c..6bf5f6c3c 100644
--- a/src/storage/dd/DdMetaVariable.h
+++ b/src/storage/dd/DdMetaVariable.h
@@ -6,16 +6,19 @@
#include <cstdint>
#include <string>
-#include "src/storage/dd/CuddDdManager.h"
#include "src/storage/dd/CuddDd.h"
namespace storm {
namespace dd {
+ // Forward-declare the DdManager class.
+ template<DdType Type> class DdManager;
template <DdType Type>
class DdMetaVariable {
+ public:
// Declare the DdManager class as friend so it can access the internals of a meta variable.
friend class DdManager<Type>;
+ friend class Dd<Type>;
/*!
* Creates a meta variable with the given name, range bounds.