From 60b2145461be301510ae96d9da7adff42c00a1eb Mon Sep 17 00:00:00 2001 From: dehnert Date: Sat, 31 May 2014 21:20:56 +0200 Subject: [PATCH] Added function to DD interface that creates a nested if-then-else expression that represents the very same function as the DD. Added a test for this functionality. Added some methods offereded by Cudd to simplify DDs. Former-commit-id: 4fc816f64b4e68cfea8bd59d48fa8663458990a3 --- src/storage/dd/CuddDd.cpp | 31 +++++++++++++++++ src/storage/dd/CuddDd.h | 46 ++++++++++++++++++++++++++ src/storage/dd/CuddDdManager.h | 1 - test/functional/storage/CuddDdTest.cpp | 33 ++++++++++++++++++ 4 files changed, 110 insertions(+), 1 deletion(-) 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 Dd::notZero() const { return Dd(this->getDdManager(), this->getCuddAdd().BddPattern().Add(), this->getContainedMetaVariableNames()); } + + Dd Dd::constrain(Dd const& constraint) const { + std::set metaVariableNames(this->getContainedMetaVariableNames()); + metaVariableNames.insert(constraint.getContainedMetaVariableNames().begin(), constraint.getContainedMetaVariableNames().end()); + + return Dd(this->getDdManager(), this->getCuddAdd().Constrain(constraint.getCuddAdd()), metaVariableNames); + } + + Dd Dd::restrict(Dd const& constraint) const { + std::set metaVariableNames(this->getContainedMetaVariableNames()); + metaVariableNames.insert(constraint.getContainedMetaVariableNames().begin(), constraint.getContainedMetaVariableNames().end()); + + return Dd(this->getDdManager(), this->getCuddAdd().Restrict(constraint.getCuddAdd()), metaVariableNames); + } + + Dd Dd::getSupport() const { + return Dd(this->getDdManager(), this->getCuddAdd().Support().Add(), this->getContainedMetaVariableNames()); + } uint_fast64_t Dd::getNonZeroCount() const { std::size_t numberOfDdVariables = 0; @@ -496,6 +514,19 @@ namespace storm { return DdForwardIterator(this->getDdManager(), nullptr, nullptr, 0, true, nullptr, enumerateDontCareMetaVariables); } + storm::expressions::Expression Dd::toExpression() const { + return toExpressionRecur(this->getCuddAdd().getNode(), this->getDdManager()->getDdVariableNames()); + } + + storm::expressions::Expression Dd::toExpressionRecur(DdNode const* dd, std::vector 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(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& 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 notZero() const; + /*! + * Computes the constraint of the current DD with the given constraint. That is, the function value of the + * resulting DD will be the same as the current ones for all assignments mapping to one in the constraint + * and may be different otherwise. + * + * @param constraint The constraint to use for the operation. + * @return The resulting DD. + */ + Dd constrain(Dd const& constraint) const; + + /*! + * Computes the restriction of the current DD with the given constraint. That is, the function value of the + * resulting DD will be the same as the current ones for all assignments mapping to one in the constraint + * and may be different otherwise. + * + * @param constraint The constraint to use for the operation. + * @return The resulting DD. + */ + Dd restrict(Dd const& constraint) const; + + /*! + * Retrieves the support of the current DD. + * + * @return The support represented as a DD. + */ + Dd getSupport() const; + /*! * Retrieves the number of encodings that are mapped to a non-zero value. * @@ -481,6 +509,15 @@ namespace storm { */ DdForwardIterator end(bool enumerateDontCareMetaVariables = true) const; + /*! + * Converts the DD into a (heavily nested) if-then-else expression that represents the very same function. + * The variable names used in the expression are derived from the meta variable name 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& 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 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> manager(new storm::dd::DdManager()); + manager->addMetaVariable("x", 1, 9); + + storm::dd::Dd 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 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