diff --git a/src/storage/dd/CuddDd.cpp b/src/storage/dd/CuddDd.cpp
index fde9d008a..f12c4bfa8 100644
--- a/src/storage/dd/CuddDd.cpp
+++ b/src/storage/dd/CuddDd.cpp
@@ -325,6 +325,24 @@ namespace storm {
Dd<DdType::CUDD> Dd<DdType::CUDD>::notZero() const {
return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddAdd().BddPattern().Add(), this->getContainedMetaVariableNames());
}
+
+ Dd<DdType::CUDD> Dd<DdType::CUDD>::constrain(Dd<DdType::CUDD> const& constraint) const {
+ std::set<std::string> metaVariableNames(this->getContainedMetaVariableNames());
+ metaVariableNames.insert(constraint.getContainedMetaVariableNames().begin(), constraint.getContainedMetaVariableNames().end());
+
+ return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddAdd().Constrain(constraint.getCuddAdd()), metaVariableNames);
+ }
+
+ Dd<DdType::CUDD> Dd<DdType::CUDD>::restrict(Dd<DdType::CUDD> const& constraint) const {
+ std::set<std::string> metaVariableNames(this->getContainedMetaVariableNames());
+ metaVariableNames.insert(constraint.getContainedMetaVariableNames().begin(), constraint.getContainedMetaVariableNames().end());
+
+ return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddAdd().Restrict(constraint.getCuddAdd()), metaVariableNames);
+ }
+
+ Dd<DdType::CUDD> Dd<DdType::CUDD>::getSupport() const {
+ return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddAdd().Support().Add(), this->getContainedMetaVariableNames());
+ }
uint_fast64_t Dd<DdType::CUDD>::getNonZeroCount() const {
std::size_t numberOfDdVariables = 0;
@@ -496,6 +514,19 @@ namespace storm {
return DdForwardIterator<DdType::CUDD>(this->getDdManager(), nullptr, nullptr, 0, true, nullptr, enumerateDontCareMetaVariables);
}
+ storm::expressions::Expression Dd<DdType::CUDD>::toExpression() const {
+ return toExpressionRecur(this->getCuddAdd().getNode(), this->getDdManager()->getDdVariableNames());
+ }
+
+ storm::expressions::Expression Dd<DdType::CUDD>::toExpressionRecur(DdNode const* dd, std::vector<std::string> const& variableNames) {
+ // 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));
+ }
+ }
+
std::ostream & operator<<(std::ostream& out, const Dd<DdType::CUDD>& dd) {
dd.exportToDot();
return out;
diff --git a/src/storage/dd/CuddDd.h b/src/storage/dd/CuddDd.h
index 6d91960ba..bf879fa34 100644
--- a/src/storage/dd/CuddDd.h
+++ b/src/storage/dd/CuddDd.h
@@ -8,6 +8,7 @@
#include "src/storage/dd/Dd.h"
#include "src/storage/dd/CuddDdForwardIterator.h"
+#include "src/storage/expressions/Expression.h"
#include "src/utility/OsDetection.h"
// Include the C++-interface of CUDD.
@@ -317,6 +318,33 @@ namespace storm {
*/
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.
*
@@ -481,6 +509,15 @@ namespace storm {
*/
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 with a suffix ".i"
+ * expressing that the variable is the i-th bit of the meta variable.
+ *
+ * @return The resulting expression.
+ */
+ storm::expressions::Expression toExpression() const;
+
friend std::ostream & operator<<(std::ostream& out, const Dd<DdType::CUDD>& dd);
private:
/*!
@@ -511,6 +548,15 @@ namespace storm {
*/
void removeContainedMetaVariable(std::string const& metaVariableName);
+ /*!
+ * Performs the recursive step of toExpression on the given DD.
+ *
+ * @param dd The dd to translate into an expression.
+ * @param variableNames The names of the variables to use in the expression.
+ * @return The resulting expression.
+ */
+ static storm::expressions::Expression toExpressionRecur(DdNode const* dd, std::vector<std::string> const& variableNames);
+
/*!
* Creates a DD that encapsulates the given CUDD ADD.
*
diff --git a/src/storage/dd/CuddDdManager.h b/src/storage/dd/CuddDdManager.h
index 14ea4d8a3..a570224c3 100644
--- a/src/storage/dd/CuddDdManager.h
+++ b/src/storage/dd/CuddDdManager.h
@@ -138,7 +138,6 @@ namespace storm {
*/
void triggerReordering();
- protected:
/*!
* Retrieves the meta variable with the given name if it exists.
*
diff --git a/test/functional/storage/CuddDdTest.cpp b/test/functional/storage/CuddDdTest.cpp
index f39e4ad48..c84def017 100644
--- a/test/functional/storage/CuddDdTest.cpp
+++ b/test/functional/storage/CuddDdTest.cpp
@@ -308,3 +308,36 @@ TEST(CuddDd, ForwardIteratorTest) {
}
EXPECT_EQ(1, numberOfValuations);
}
+
+TEST(CuddDd, ToExpressionTest) {
+ std::shared_ptr<storm::dd::DdManager<storm::dd::DdType::CUDD>> manager(new storm::dd::DdManager<storm::dd::DdType::CUDD>());
+ manager->addMetaVariable("x", 1, 9);
+
+ storm::dd::Dd<storm::dd::DdType::CUDD> dd;
+ ASSERT_NO_THROW(dd = manager->getIdentity("x"));
+
+ storm::expressions::Expression ddAsExpression;
+ ASSERT_NO_THROW(ddAsExpression = dd.toExpression());
+
+ storm::expressions::SimpleValuation valuation;
+ for (std::size_t bit = 0; bit < manager->getMetaVariable("x").getNumberOfDdVariables(); ++bit) {
+ valuation.addBooleanIdentifier("x." + std::to_string(bit));
+ }
+
+ storm::dd::DdMetaVariable<storm::dd::DdType::CUDD> const& metaVariable = manager->getMetaVariable("x");
+
+ for (auto valuationValuePair : dd) {
+ for (std::size_t i = 0; i < metaVariable.getNumberOfDdVariables(); ++i) {
+ // Check if the i-th bit is set or not and modify the valuation accordingly.
+ if (((valuationValuePair.first.getIntegerValue("x") - metaVariable.getLow()) & (1 << (metaVariable.getNumberOfDdVariables() - i - 1))) != 0) {
+ valuation.setBooleanValue("x." + std::to_string(i), true);
+ } else {
+ valuation.setBooleanValue("x." + std::to_string(i), false);
+ }
+ }
+
+ // At this point, the constructed valuation should make the expression obtained from the DD evaluate to the very
+ // same value as the current value obtained from the DD.
+ EXPECT_EQ(valuationValuePair.second, ddAsExpression.evaluateAsDouble(&valuation));
+ }
+}
\ No newline at end of file