diff --git a/src/storage/PairHash.h b/src/storage/PairHash.h new file mode 100644 index 000000000..dc7b7e7f2 --- /dev/null +++ b/src/storage/PairHash.h @@ -0,0 +1,17 @@ +#ifndef STORM_STORAGE_PAIRHASH_H_ +#define STORM_STORAGE_PAIRHASH_H_ + +namespace std { + template <> + struct hash> + { + std::size_t operator()(std::pair const& key) const { + std::size_t seed = 0; + boost::hash_combine(seed, key.first); + boost::hash_combine(seed, key.second); + return seed; + } + }; +} + +#endif /* STORM_STORAGE_PAIRHASH_H_ */ diff --git a/src/storage/dd/CuddBdd.cpp b/src/storage/dd/CuddBdd.cpp index 98d50132a..fc673e0f2 100644 --- a/src/storage/dd/CuddBdd.cpp +++ b/src/storage/dd/CuddBdd.cpp @@ -7,6 +7,9 @@ #include "src/storage/dd/CuddOdd.h" #include "src/storage/dd/CuddDdManager.h" +#include "src/storage/expressions/ExpressionManager.h" +#include "src/storage/expressions/Expression.h" + #include "src/storage/BitVector.h" #include "src/logic/ComparisonType.h" @@ -372,23 +375,71 @@ namespace storm { // Create (and maintain) a mapping from the DD nodes to a counter that says the how-many-th node (within the // nodes of equal index) the node was. - std::unordered_map nodeToCounterMap; - this->toExpressionRec(this->getCuddDdNode(), this->getDdManager()->getCuddManager(), manager, result.first, result.second, nodeToCounterMap); + std::unordered_map nodeToCounterMap; + std::vector nextCounterForIndex(this->getDdManager()->getNumberOfDdVariables(), 0); + bool negated = Cudd_Regular(this->getCuddDdNode()) != this->getCuddDdNode(); + + // Translate from the top node downwards. + storm::expressions::Variable topVariable = this->toExpressionRec(Cudd_Regular(this->getCuddDdNode()), this->getDdManager()->getCuddManager(), manager, result.first, result.second, nodeToCounterMap, nextCounterForIndex, indexToExpressionMap); + + // Create the final expression. + if (negated) { + result.first.push_back(!topVariable); + } else { + result.first.push_back(topVariable); + } return result; } - void Bdd::toExpressionRec(DdNode const* f, Cudd const& ddManager, storm::expressions::ExpressionManager& manager, std::vector& expressions, std::unordered_map, storm::expressions::Variable>& countIndexToVariablePair, std::unordered_map& nodeToCounterMap) const { - DdNode const* F = Cudd_Regular(f); + storm::expressions::Variable Bdd::toExpressionRec(DdNode const* dd, Cudd const& ddManager, storm::expressions::ExpressionManager& manager, std::vector& expressions, std::unordered_map, storm::expressions::Variable>& countIndexToVariablePair, std::unordered_map& nodeToCounterMap, std::vector& nextCounterForIndex, std::unordered_map const& indexToExpressionMap) const { + STORM_LOG_ASSERT(dd == Cudd_Regular(dd), "Expected non-negated BDD node."); + + // First, try to look up the current node. + auto nodeCounterIt = nodeToCounterMap.find(dd); + if (nodeCounterIt != nodeToCounterMap.end()) { + // If we have found the node, this means we can look up the counter-index pair and get the corresponding variable. + auto variableIt = countIndexToVariablePair.find(std::make_pair(nodeCounterIt->second, dd->index)); + STORM_LOG_ASSERT(variableIt != countIndexToVariablePair.end(), "Unable to find node."); + return variableIt->second; + } + + // If the node was not yet encountered, we create a variable and associate it with the appropriate expression. + storm::expressions::Variable newVariable = manager.declareFreshBooleanVariable(); + + // Since we want to reuse the variable whenever possible, we insert the appropriate entries in the hash table. + if (!Cudd_IsConstant(dd)) { + // If we are dealing with a non-terminal node, we count it as a new node with this index. + nodeToCounterMap[dd] = nextCounterForIndex[dd->index]; + countIndexToVariablePair[std::make_pair(nextCounterForIndex[dd->index], dd->index)] = newVariable; + ++nextCounterForIndex[dd->index]; + } else { + // If it's a terminal node, it is the one leaf and there's no need to keep track of a counter for this level. + nodeToCounterMap[dd] = 0; + countIndexToVariablePair[std::make_pair(0, dd->index)] = newVariable; + } - // Terminal cases. - if (F == Cudd_ReadOne(ddManager.getManager())) { + // In the terminal case, we can only have a one since we are considering non-negated nodes only. + if (dd == Cudd_ReadOne(ddManager.getManager())) { + // Push the expression that enforces that the new variable is true. + expressions.push_back(storm::expressions::implies(manager.boolean(true), newVariable)); + } else { + // In the non-terminal case, we recursively translate the children nodes and then construct and appropriate ite-expression. + DdNode const* t = Cudd_T(dd); + DdNode const* e = Cudd_E(dd); + DdNode const* T = Cudd_Regular(t); + DdNode const* E = Cudd_Regular(e); + storm::expressions::Variable thenVariable = toExpressionRec(T, ddManager, manager, expressions, countIndexToVariablePair, nodeToCounterMap, nextCounterForIndex, indexToExpressionMap); + storm::expressions::Variable elseVariable = toExpressionRec(E, ddManager, manager, expressions, countIndexToVariablePair, nodeToCounterMap, nextCounterForIndex, indexToExpressionMap); + // Create the appropriate expression. + auto expressionIt = indexToExpressionMap.find(dd->index); + STORM_LOG_ASSERT(expressionIt != indexToExpressionMap.end(), "Unable to find expression for variable index."); + expressions.push_back(storm::expressions::iff(newVariable, storm::expressions::ite(expressionIt->second, t == T ? thenVariable : !thenVariable, e == E ? elseVariable : !elseVariable))); } - // Non-terminal cases. - // (1) Check if we have seen the node before. - auto nodeIt = nodeToCounterMap.find(); + // Return the variable for this node. + return newVariable; } void Bdd::toVectorRec(DdNode const* dd, Cudd const& manager, storm::storage::BitVector& result, Odd const& rowOdd, bool complement, uint_fast64_t currentRowLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, std::vector const& ddRowVariableIndices) const { diff --git a/src/storage/dd/CuddBdd.h b/src/storage/dd/CuddBdd.h index a8e434958..91019d79f 100644 --- a/src/storage/dd/CuddBdd.h +++ b/src/storage/dd/CuddBdd.h @@ -6,6 +6,7 @@ #include "src/storage/dd/Bdd.h" #include "src/storage/dd/CuddDd.h" +#include "src/storage/PairHash.h" #include "src/utility/OsDetection.h" // Include the C++-interface of CUDD. @@ -382,7 +383,7 @@ namespace storm { */ void toVectorRec(DdNode const* dd, Cudd const& manager, storm::storage::BitVector& result, Odd const& rowOdd, bool complement, uint_fast64_t currentRowLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, std::vector const& ddRowVariableIndices) const; - void toExpressionRec(DdNode const* dd, Cudd const& ddManager, storm::expressions::ExpressionManager& manager, std::vector& expressions, std::unordered_map, storm::expressions::Variable>& countIndexToVariablePair, std::unordered_map& nodeToCounterMap) const; + storm::expressions::Variable toExpressionRec(DdNode const* dd, Cudd const& ddManager, storm::expressions::ExpressionManager& manager, std::vector& expressions, std::unordered_map, storm::expressions::Variable>& countIndexToVariablePair, std::unordered_map& nodeToCounterMap, std::vector& nextCounterForIndex, std::unordered_map const& indexToExpressionMap) const; // The BDD created by CUDD. BDD cuddBdd; diff --git a/src/storage/dd/CuddDdManager.cpp b/src/storage/dd/CuddDdManager.cpp index 622ecbb44..c782033ae 100644 --- a/src/storage/dd/CuddDdManager.cpp +++ b/src/storage/dd/CuddDdManager.cpp @@ -16,7 +16,7 @@ namespace storm { namespace dd { - DdManager::DdManager() : cuddManager(), metaVariableMap(), reorderingTechnique(CUDD_REORDER_NONE), manager(new storm::expressions::ExpressionManager()) { + DdManager::DdManager() : cuddManager(), metaVariableMap(), reorderingTechnique(CUDD_REORDER_NONE), manager(new storm::expressions::ExpressionManager()), numberOfDdVariables(0) { this->cuddManager.SetMaxMemory(static_cast(storm::settings::cuddSettings().getMaximalMemory() * 1024ul * 1024ul)); this->cuddManager.SetEpsilon(storm::settings::cuddSettings().getConstantPrecision()); @@ -160,6 +160,7 @@ namespace storm { variablesPrime.emplace_back(Bdd(this->shared_from_this(), cuddManager.bddVar(), {primed})); } } + numberOfDdVariables += numberOfBits; // Now group the non-primed and primed variable. for (uint_fast64_t i = 0; i < numberOfBits; ++i) { @@ -191,6 +192,7 @@ namespace storm { ++level.get(); } } + numberOfDdVariables += 2; storm::expressions::Variable unprimed = manager->declareBooleanVariable(name); storm::expressions::Variable primed = manager->declareBooleanVariable(name + "'"); @@ -235,6 +237,10 @@ namespace storm { return this->metaVariableMap.size(); } + std::size_t DdManager::getNumberOfDdVariables() const { + return numberOfDdVariables; + } + bool DdManager::hasMetaVariable(std::string const& metaVariableName) const { return manager->hasVariable(metaVariableName); } diff --git a/src/storage/dd/CuddDdManager.h b/src/storage/dd/CuddDdManager.h index 411a64b55..fe267c423 100644 --- a/src/storage/dd/CuddDdManager.h +++ b/src/storage/dd/CuddDdManager.h @@ -145,6 +145,13 @@ namespace storm { */ std::size_t getNumberOfMetaVariables() const; + /*! + * Retrieves the number of DD variables that are contained in this manager. + * + * @return The number of DD variables contained in this manager. + */ + std::size_t getNumberOfDdVariables() const; + /*! * Retrieves whether the given meta variable name is already in use. * @@ -250,6 +257,9 @@ namespace storm { // The manager responsible for the variables. std::shared_ptr manager; + + // Keep track of all DD variables of this manager. + uint_fast64_t numberOfDdVariables; }; } } diff --git a/test/functional/storage/CuddDdTest.cpp b/test/functional/storage/CuddDdTest.cpp index 33a67b197..b6130d297 100644 --- a/test/functional/storage/CuddDdTest.cpp +++ b/test/functional/storage/CuddDdTest.cpp @@ -5,6 +5,8 @@ #include "src/storage/dd/CuddAdd.h" #include "src/storage/dd/CuddOdd.h" #include "src/storage/dd/DdMetaVariable.h" +#include "src/storage/expressions/ExpressionManager.h" +#include "src/storage/expressions/Expression.h" #include "src/settings/SettingsManager.h" #include "src/storage/SparseMatrix.h" @@ -406,4 +408,28 @@ TEST(CuddDd, BddOddTest) { EXPECT_EQ(9ul, matrix.getRowGroupCount()); EXPECT_EQ(9ul, matrix.getColumnCount()); EXPECT_EQ(106ul, matrix.getNonzeroEntryCount()); +} + +TEST(CuddDd, BddToExpressionTest) { + std::shared_ptr> ddManager(new storm::dd::DdManager()); + std::pair a = ddManager->addMetaVariable("a"); + std::pair b = ddManager->addMetaVariable("b"); + + storm::dd::Bdd bdd = ddManager->getBddOne(); + bdd &= ddManager->getEncoding(a.first, 1); + bdd |= ddManager->getEncoding(b.first, 0); + + std::shared_ptr manager = std::make_shared(); + storm::expressions::Variable c = manager->declareBooleanVariable("c"); + storm::expressions::Variable d = manager->declareBooleanVariable("d"); + + std::unordered_map indexToExpressionMap; + indexToExpressionMap[0] = c; + indexToExpressionMap[2] = d; + auto result = bdd.toExpression(*manager, indexToExpressionMap); + + for (auto const& expression : result.first) { + std::cout << expression << std::endl; + } + } \ No newline at end of file