From 57a8381f914b2a8103875736c596b6c08da28bc5 Mon Sep 17 00:00:00 2001 From: dehnert Date: Sat, 10 May 2014 15:18:19 +0200 Subject: [PATCH] If requested, the DD iterator can now skip meta variables which are 'don't cares' for the function value. Former-commit-id: 061cb5f0fa0c0f3286906e9b5f01779f176674d1 --- src/storage/dd/CuddDd.cpp | 8 ++-- src/storage/dd/CuddDd.h | 8 +++- src/storage/dd/CuddDdForwardIterator.cpp | 45 +++++++++++++++++---- src/storage/dd/CuddDdForwardIterator.h | 8 +++- src/storage/expressions/SimpleValuation.cpp | 9 ++++- test/functional/storage/CuddDdTest.cpp | 22 ++++++++++ 6 files changed, 84 insertions(+), 16 deletions(-) diff --git a/src/storage/dd/CuddDd.cpp b/src/storage/dd/CuddDd.cpp index 72abb87bf..cdff92894 100644 --- a/src/storage/dd/CuddDd.cpp +++ b/src/storage/dd/CuddDd.cpp @@ -473,15 +473,15 @@ namespace storm { return this->ddManager; } - DdForwardIterator Dd::begin() const { + DdForwardIterator Dd::begin(bool enumerateDontCareMetaVariables) const { int* cube; double value; DdGen* generator = this->getCuddAdd().FirstCube(&cube, &value); - return DdForwardIterator(this->getDdManager(), generator, cube, value, Cudd_IsGenEmpty(generator), &this->getContainedMetaVariableNames()); + return DdForwardIterator(this->getDdManager(), generator, cube, value, Cudd_IsGenEmpty(generator), &this->getContainedMetaVariableNames(), enumerateDontCareMetaVariables); } - DdForwardIterator Dd::end() const { - return DdForwardIterator(this->getDdManager(), nullptr, nullptr, 0, true, nullptr); + DdForwardIterator Dd::end(bool enumerateDontCareMetaVariables) const { + return DdForwardIterator(this->getDdManager(), nullptr, nullptr, 0, true, nullptr, enumerateDontCareMetaVariables); } std::ostream & operator<<(std::ostream& out, const Dd& dd) { diff --git a/src/storage/dd/CuddDd.h b/src/storage/dd/CuddDd.h index f345c28a2..9f638d329 100644 --- a/src/storage/dd/CuddDd.h +++ b/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 begin() const; + DdForwardIterator 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 end() const; + DdForwardIterator end(bool enumerateDontCareMetaVariables = true) const; friend std::ostream & operator<<(std::ostream& out, const Dd& dd); private: diff --git a/src/storage/dd/CuddDdForwardIterator.cpp b/src/storage/dd/CuddDdForwardIterator.cpp index 017845b47..cce5c112c 100644 --- a/src/storage/dd/CuddDdForwardIterator.cpp +++ b/src/storage/dd/CuddDdForwardIterator.cpp @@ -5,11 +5,11 @@ namespace storm { namespace dd { - DdForwardIterator::DdForwardIterator() : ddManager(), generator(), cube(), value(), isAtEnd(), metaVariables(), cubeCounter(), relevantDontCareDdVariables(), currentValuation() { + DdForwardIterator::DdForwardIterator() : ddManager(), generator(), cube(), value(), isAtEnd(), metaVariables(), enumerateDontCareMetaVariables(), cubeCounter(), relevantDontCareDdVariables(), currentValuation() { // Intentionally left empty. } - DdForwardIterator::DdForwardIterator(std::shared_ptr> ddManager, DdGen* generator, int* cube, double value, bool isAtEnd, std::set const* metaVariables) : ddManager(ddManager), generator(generator), cube(cube), value(value), isAtEnd(isAtEnd), metaVariables(metaVariables), cubeCounter(), relevantDontCareDdVariables(), currentValuation() { + DdForwardIterator::DdForwardIterator(std::shared_ptr> ddManager, DdGen* generator, int* cube, double value, bool isAtEnd, std::set 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> localRelenvantDontCareDdVariables; auto const& metaVariable = this->ddManager->getMetaVariable(metaVariableName); if (metaVariable.getType() == DdMetaVariable::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); } } diff --git a/src/storage/dd/CuddDdForwardIterator.h b/src/storage/dd/CuddDdForwardIterator.h index 0515475a4..8b08af929 100644 --- a/src/storage/dd/CuddDdForwardIterator.h +++ b/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, DdGen* generator, int* cube, double value, bool isAtEnd, std::set const* metaVariables = nullptr); + DdForwardIterator(std::shared_ptr> ddManager, DdGen* generator, int* cube, double value, bool isAtEnd, std::set 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 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; diff --git a/src/storage/expressions/SimpleValuation.cpp b/src/storage/expressions/SimpleValuation.cpp index e8fb27611..4a5441e99 100644 --- a/src/storage/expressions/SimpleValuation.cpp +++ b/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 << "}"; diff --git a/test/functional/storage/CuddDdTest.cpp b/test/functional/storage/CuddDdTest.cpp index 91d14f202..ce40c94d1 100644 --- a/test/functional/storage/CuddDdTest.cpp +++ b/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); }