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: 4fc816f64b

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;

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.
              *

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.
              *

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));
+    }
+}