If requested, the DD iterator can now skip meta variables which are 'don't cares' for the function value.

Former-commit-id: 061cb5f0fa

src/storage/dd/CuddDd.cpp

@@ -473,15 +473,15 @@ namespace storm {
             return this->ddManager;
         }
         
-        DdForwardIterator<DdType::CUDD> Dd<DdType::CUDD>::begin() const {
+        DdForwardIterator<DdType::CUDD> Dd<DdType::CUDD>::begin(bool enumerateDontCareMetaVariables) const {
             int* cube;
             double value;
             DdGen* generator = this->getCuddAdd().FirstCube(&cube, &value);
-            return DdForwardIterator<DdType::CUDD>(this->getDdManager(), generator, cube, value, Cudd_IsGenEmpty(generator), &this->getContainedMetaVariableNames());
+            return DdForwardIterator<DdType::CUDD>(this->getDdManager(), generator, cube, value, Cudd_IsGenEmpty(generator), &this->getContainedMetaVariableNames(), enumerateDontCareMetaVariables);
         }
         
-        DdForwardIterator<DdType::CUDD> Dd<DdType::CUDD>::end() const {
-            return DdForwardIterator<DdType::CUDD>(this->getDdManager(), nullptr, nullptr, 0, true, nullptr);
+        DdForwardIterator<DdType::CUDD> Dd<DdType::CUDD>::end(bool enumerateDontCareMetaVariables) const {
+            return DdForwardIterator<DdType::CUDD>(this->getDdManager(), nullptr, nullptr, 0, true, nullptr, enumerateDontCareMetaVariables);
         }
         
         std::ostream & operator<<(std::ostream& out, const Dd<DdType::CUDD>& dd) {

src/storage/dd/CuddDd.h

@@ -440,16 +440,20 @@ namespace storm {
             /*!
              * Retrieves an iterator that points to the first meta variable assignment with a non-zero function value.
              *
+             * @param enumerateDontCareMetaVariables If set to true, all meta variable assignments are enumerated, even
+             * if a meta variable does not at all influence the the function value.
              * @return An iterator that points to the first meta variable assignment with a non-zero function value.
              */
-            DdForwardIterator<DdType::CUDD> begin() const;
+            DdForwardIterator<DdType::CUDD> begin(bool enumerateDontCareMetaVariables = true) const;
             
             /*!
              * Retrieves an iterator that points past the end of the container.
              *
+             * @param enumerateDontCareMetaVariables If set to true, all meta variable assignments are enumerated, even
+             * if a meta variable does not at all influence the the function value.
              * @return An iterator that points past the end of the container.
              */
-            DdForwardIterator<DdType::CUDD> end() const;
+            DdForwardIterator<DdType::CUDD> end(bool enumerateDontCareMetaVariables = true) const;
             
             friend std::ostream & operator<<(std::ostream& out, const Dd<DdType::CUDD>& dd);
         private:

src/storage/dd/CuddDdForwardIterator.cpp

@@ -5,11 +5,11 @@
 
 namespace storm {
     namespace dd {
-        DdForwardIterator<DdType::CUDD>::DdForwardIterator() : ddManager(), generator(), cube(), value(), isAtEnd(), metaVariables(), cubeCounter(), relevantDontCareDdVariables(), currentValuation() {
+        DdForwardIterator<DdType::CUDD>::DdForwardIterator() : ddManager(), generator(), cube(), value(), isAtEnd(), metaVariables(), enumerateDontCareMetaVariables(), cubeCounter(), relevantDontCareDdVariables(), currentValuation() {
             // Intentionally left empty.
         }
         
-        DdForwardIterator<DdType::CUDD>::DdForwardIterator(std::shared_ptr<DdManager<DdType::CUDD>> ddManager, DdGen* generator, int* cube, double value, bool isAtEnd, std::set<std::string> const* metaVariables) : ddManager(ddManager), generator(generator), cube(cube), value(value), isAtEnd(isAtEnd), metaVariables(metaVariables), cubeCounter(), relevantDontCareDdVariables(), currentValuation() {
+        DdForwardIterator<DdType::CUDD>::DdForwardIterator(std::shared_ptr<DdManager<DdType::CUDD>> ddManager, DdGen* generator, int* cube, double value, bool isAtEnd, std::set<std::string> const* metaVariables, bool enumerateDontCareMetaVariables) : ddManager(ddManager), generator(generator), cube(cube), value(value), isAtEnd(isAtEnd), metaVariables(metaVariables), enumerateDontCareMetaVariables(enumerateDontCareMetaVariables), cubeCounter(), relevantDontCareDdVariables(), currentValuation() {
             // If the given generator is not yet at its end, we need to create the current valuation from the cube from
             // scratch.
             if (!this->isAtEnd) {
@@ -113,29 +113,60 @@ namespace storm {
             // don't cares. In the latter case, we add them to a special list, so we can iterate over their concrete
             // valuations later.
             for (auto const& metaVariableName : *this->metaVariables) {
+                bool metaVariableAppearsInCube = false;
+                std::vector<std::tuple<ADD, std::string, uint_fast64_t>> localRelenvantDontCareDdVariables;
                 auto const& metaVariable = this->ddManager->getMetaVariable(metaVariableName);
                 if (metaVariable.getType() == DdMetaVariable<DdType::CUDD>::MetaVariableType::Bool) {
                     if (this->cube[metaVariable.getDdVariables()[0].getCuddAdd().NodeReadIndex()] == 0) {
-                        currentValuation.setBooleanValue(metaVariableName, false);
+                        metaVariableAppearsInCube = true;
+                        if (!currentValuation.containsBooleanIdentifier(metaVariableName)) {
+                            currentValuation.addBooleanIdentifier(metaVariableName, false);
+                        } else {
+                            currentValuation.setBooleanValue(metaVariableName, false);
+                        }
                     } else if (this->cube[metaVariable.getDdVariables()[0].getCuddAdd().NodeReadIndex()] == 1) {
-                        currentValuation.setBooleanValue(metaVariableName, true);
+                        metaVariableAppearsInCube = true;
+                        if (!currentValuation.containsBooleanIdentifier(metaVariableName)) {
+                            currentValuation.addBooleanIdentifier(metaVariableName, true);
+                        } else {
+                            currentValuation.setBooleanValue(metaVariableName, true);
+                        }
                     } else {
-                        relevantDontCareDdVariables.push_back(std::make_tuple(metaVariable.getDdVariables()[0].getCuddAdd(), metaVariableName, 0));
+                        localRelenvantDontCareDdVariables.push_back(std::make_tuple(metaVariable.getDdVariables()[0].getCuddAdd(), metaVariableName, 0));
                     }
                 } else {
                     int_fast64_t intValue = 0;
                     for (uint_fast64_t bitIndex = 0; bitIndex < metaVariable.getNumberOfDdVariables(); ++bitIndex) {
                         if (cube[metaVariable.getDdVariables()[bitIndex].getCuddAdd().NodeReadIndex()] == 0) {
                             // Leave bit unset.
+                            metaVariableAppearsInCube = true;
                         } else if (cube[metaVariable.getDdVariables()[bitIndex].getCuddAdd().NodeReadIndex()] == 1) {
                             intValue |= 1ull << (metaVariable.getNumberOfDdVariables() - bitIndex - 1);
+                            metaVariableAppearsInCube = true;
                         } else {
                             // Temporarily leave bit unset so we can iterate trough the other option later.
                             // Add the bit to the relevant don't care bits.
-                            this->relevantDontCareDdVariables.push_back(std::make_tuple(metaVariable.getDdVariables()[bitIndex].getCuddAdd(), metaVariableName, metaVariable.getNumberOfDdVariables() - bitIndex - 1));
+                            localRelenvantDontCareDdVariables.push_back(std::make_tuple(metaVariable.getDdVariables()[bitIndex].getCuddAdd(), metaVariableName, metaVariable.getNumberOfDdVariables() - bitIndex - 1));
+                        }
+                    }
+                    if (this->enumerateDontCareMetaVariables || metaVariableAppearsInCube) {
+                        if (!currentValuation.containsIntegerIdentifier(metaVariableName)) {
+                            currentValuation.addIntegerIdentifier(metaVariableName);
                         }
+                        currentValuation.setIntegerValue(metaVariableName, intValue + metaVariable.getLow());
                     }
-                    currentValuation.setIntegerValue(metaVariableName, intValue + metaVariable.getLow());
+                }
+                
+                // If all meta variables are to be enumerated or the meta variable appeared in the cube, we register the
+                // missing bits to later enumerate all possible valuations.
+                if (this->enumerateDontCareMetaVariables || metaVariableAppearsInCube) {
+                    relevantDontCareDdVariables.insert(relevantDontCareDdVariables.end(), localRelenvantDontCareDdVariables.begin(), localRelenvantDontCareDdVariables.end());
+                }
+                
+                // If the meta variable does not appear in the cube and we're not supposed to enumerate such meta variables
+                // we remove the meta variable from the valuation.
+                if (!this->enumerateDontCareMetaVariables && !metaVariableAppearsInCube) {
+                    currentValuation.removeIdentifier(metaVariableName);
                 }
             }
             

src/storage/dd/CuddDdForwardIterator.h

@@ -82,8 +82,10 @@ namespace storm {
              * @param isAtEnd A flag that indicates whether the iterator is at its end and may not be moved forward any
              * more.
              * @param metaVariables The meta variables that appear in the DD.
+             * @param enumerateDontCareMetaVariables If set to true, all meta variable assignments are enumerated, even
+             * if a meta variable does not at all influence the the function value.
              */
-            DdForwardIterator(std::shared_ptr<DdManager<DdType::CUDD>> ddManager, DdGen* generator, int* cube, double value, bool isAtEnd, std::set<std::string> const* metaVariables = nullptr);
+            DdForwardIterator(std::shared_ptr<DdManager<DdType::CUDD>> ddManager, DdGen* generator, int* cube, double value, bool isAtEnd, std::set<std::string> const* metaVariables = nullptr, bool enumerateDontCareMetaVariables = true);
             
             /*!
              * Recreates the internal information when a new cube needs to be treated.
@@ -114,6 +116,10 @@ namespace storm {
             // The set of meta variables appearing in the DD.
             std::set<std::string> const* metaVariables;
             
+            // A flag that indicates whether the iterator is supposed to enumerate meta variable valuations even if
+            // they don't influence the function value.
+            bool enumerateDontCareMetaVariables;
+            
             // A number that represents how many assignments of the current cube have already been returned previously.
             // This is needed, because cubes may represent many assignments (if they have don't care variables).
             uint_fast64_t cubeCounter;

src/storage/expressions/SimpleValuation.cpp

@@ -86,9 +86,14 @@ namespace storm {
         }
         
         std::ostream& operator<<(std::ostream& stream, SimpleValuation const& valuation) {
-            stream << "valuation { ";
+            stream << "{ ";
+            uint_fast64_t elementIndex = 0;
             for (auto const& nameValuePair : valuation.identifierToValueMap) {
-                stream << nameValuePair.first << ": " << nameValuePair.second << std::endl;
+                stream << nameValuePair.first << " -> " << nameValuePair.second << " ";
+                ++elementIndex;
+                if (elementIndex < valuation.identifierToValueMap.size()) {
+                    stream << ", ";
+                }
             }
             stream << "}";
             

test/functional/storage/CuddDdTest.cpp

@@ -307,4 +307,26 @@ TEST(CuddDd, ForwardIteratorTest) {
         ++numberOfValuations;
     }
     EXPECT_EQ(9, numberOfValuations);
+
+    dd = manager->getRange("x");
+    dd = dd.ite(manager->getOne(), manager->getOne());
+    ASSERT_NO_THROW(it = dd.begin());
+    ASSERT_NO_THROW(ite = dd.end());
+    numberOfValuations = 0;
+    while (it != ite) {
+        ASSERT_NO_THROW(valuationValuePair = *it);
+        ASSERT_NO_THROW(++it);
+        ++numberOfValuations;
+    }
+    EXPECT_EQ(16, numberOfValuations);
+    
+    ASSERT_NO_THROW(it = dd.begin(false));
+    ASSERT_NO_THROW(ite = dd.end());
+    numberOfValuations = 0;
+    while (it != ite) {
+        ASSERT_NO_THROW(valuationValuePair = *it);
+        ASSERT_NO_THROW(++it);
+        ++numberOfValuations;
+    }
+    EXPECT_EQ(1, numberOfValuations);
 }