Added function to retrieve the minterms of a DD as an expression and added corresponding test.

Former-commit-id: afaf1f02a3

src/storage/dd/CuddDd.cpp

@@ -518,6 +518,16 @@ namespace storm {
             return toExpressionRecur(this->getCuddAdd().getNode(), this->getDdManager()->getDdVariableNames());
         }
         
+        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.
+            Dd<DdType::CUDD> tmp(this->getDdManager(), this->getCuddAdd().BddPattern().Add(), this->getContainedMetaVariableNames());
+            tmp.exportToDot("tmp.dot");
+            
+            
+            return getMintermExpressionRecur(this->getDdManager()->getCuddManager().getManager(), this->getCuddAdd().BddPattern().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)) {
@@ -527,6 +537,30 @@ namespace storm {
             }
         }
         
+        storm::expressions::Expression Dd<DdType::CUDD>::getMintermExpressionRecur(::DdManager* manager, 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)) {
+                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;

src/storage/dd/CuddDd.h

@@ -518,6 +518,16 @@ namespace storm {
              * @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);
         private:
@@ -558,6 +568,16 @@ namespace storm {
              */
             static storm::expressions::Expression toExpressionRecur(DdNode const* dd, std::vector<std::string> const& variableNames);
             
+            /*!
+             * 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 variableNames The names of the variables to use in the expression.
+             * @return The resulting expression.
+             */
+            static storm::expressions::Expression getMintermExpressionRecur(::DdManager* manager, DdNode const* dd, std::vector<std::string> const& variableNames);
+            
             /*!
              * Creates a DD that encapsulates the given CUDD ADD.
              *

test/functional/storage/CuddDdTest.cpp

@@ -340,4 +340,39 @@ TEST(CuddDd, ToExpressionTest) {
         // same value as the current value obtained from the DD.
         EXPECT_EQ(valuationValuePair.second, ddAsExpression.evaluateAsDouble(&valuation));
     }
+    
+    storm::expressions::Expression mintermExpression = dd.getMintermExpression();
+    
+    // Check whether all minterms are covered.
+    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_TRUE(mintermExpression.evaluateAsBool(&valuation));
+    }
+    
+    // Now check no additional minterms are covered.
+    dd = !dd;
+    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_FALSE(mintermExpression.evaluateAsBool(&valuation));
+    }
 }