more work on translating BDDs to expressions

Former-commit-id: 0f361f76f5

src/storage/PairHash.h

@@ -0,0 +1,17 @@
+#ifndef STORM_STORAGE_PAIRHASH_H_
+#define STORM_STORAGE_PAIRHASH_H_
+
+namespace std {
+    template <>
+    struct hash<std::pair<uint_fast64_t, uint_fast64_t>>
+    {
+        std::size_t operator()(std::pair<uint_fast64_t, uint_fast64_t> 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_ */

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<DdNode*, uint_fast64_t> nodeToCounterMap;
-            this->toExpressionRec(this->getCuddDdNode(), this->getDdManager()->getCuddManager(), manager, result.first, result.second, nodeToCounterMap);
+            std::unordered_map<DdNode const*, uint_fast64_t> nodeToCounterMap;
+            std::vector<uint_fast64_t> 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<DdType::CUDD>::toExpressionRec(DdNode const* f, Cudd const& ddManager, storm::expressions::ExpressionManager& manager, std::vector<storm::expressions::Expression>& expressions, std::unordered_map<std::pair<uint_fast64_t, uint_fast64_t>, storm::expressions::Variable>& countIndexToVariablePair, std::unordered_map<DdNode*, uint_fast64_t>& nodeToCounterMap) const {
-            DdNode const* F = Cudd_Regular(f);
+        storm::expressions::Variable Bdd<DdType::CUDD>::toExpressionRec(DdNode const* dd, Cudd const& ddManager, storm::expressions::ExpressionManager& manager, std::vector<storm::expressions::Expression>& expressions, std::unordered_map<std::pair<uint_fast64_t, uint_fast64_t>, storm::expressions::Variable>& countIndexToVariablePair, std::unordered_map<DdNode const*, uint_fast64_t>& nodeToCounterMap, std::vector<uint_fast64_t>& nextCounterForIndex, std::unordered_map<uint_fast64_t, storm::expressions::Expression> const& indexToExpressionMap) const {
+            STORM_LOG_ASSERT(dd == Cudd_Regular(dd), "Expected non-negated BDD node.");
             
-            // Terminal cases.
-            if (F == Cudd_ReadOne(ddManager.getManager())) {
+            // 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;
             }
             
-            // Non-terminal cases.
-            // (1) Check if we have seen the node before.
-            auto nodeIt = nodeToCounterMap.find();
+            // 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)));
+            }
+            
+            // Return the variable for this node.
+            return newVariable;
         }
         
         void Bdd<DdType::CUDD>::toVectorRec(DdNode const* dd, Cudd const& manager, storm::storage::BitVector& result, Odd<DdType::CUDD> const& rowOdd, bool complement, uint_fast64_t currentRowLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, std::vector<uint_fast64_t> const& ddRowVariableIndices) const {

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<DdType::CUDD> const& rowOdd, bool complement, uint_fast64_t currentRowLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, std::vector<uint_fast64_t> const& ddRowVariableIndices) const;
             
-            void toExpressionRec(DdNode const* dd, Cudd const& ddManager, storm::expressions::ExpressionManager& manager, std::vector<storm::expressions::Expression>& expressions, std::unordered_map<std::pair<uint_fast64_t, uint_fast64_t>, storm::expressions::Variable>& countIndexToVariablePair, std::unordered_map<DdNode*, uint_fast64_t>& nodeToCounterMap) const;
+            storm::expressions::Variable toExpressionRec(DdNode const* dd, Cudd const& ddManager, storm::expressions::ExpressionManager& manager, std::vector<storm::expressions::Expression>& expressions, std::unordered_map<std::pair<uint_fast64_t, uint_fast64_t>, storm::expressions::Variable>& countIndexToVariablePair, std::unordered_map<DdNode const*, uint_fast64_t>& nodeToCounterMap, std::vector<uint_fast64_t>& nextCounterForIndex, std::unordered_map<uint_fast64_t, storm::expressions::Expression> const& indexToExpressionMap) const;
             
             // The BDD created by CUDD.
             BDD cuddBdd;

src/storage/dd/CuddDdManager.cpp

@@ -16,7 +16,7 @@
 
 namespace storm {
     namespace dd {
-        DdManager<DdType::CUDD>::DdManager() : cuddManager(), metaVariableMap(), reorderingTechnique(CUDD_REORDER_NONE), manager(new storm::expressions::ExpressionManager()) {
+        DdManager<DdType::CUDD>::DdManager() : cuddManager(), metaVariableMap(), reorderingTechnique(CUDD_REORDER_NONE), manager(new storm::expressions::ExpressionManager()), numberOfDdVariables(0) {
             this->cuddManager.SetMaxMemory(static_cast<unsigned long>(storm::settings::cuddSettings().getMaximalMemory() * 1024ul * 1024ul));
             this->cuddManager.SetEpsilon(storm::settings::cuddSettings().getConstantPrecision());
             
@@ -160,6 +160,7 @@ namespace storm {
                     variablesPrime.emplace_back(Bdd<DdType::CUDD>(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<DdType::CUDD>::getNumberOfDdVariables() const {
+            return numberOfDdVariables;
+        }
+        
         bool DdManager<DdType::CUDD>::hasMetaVariable(std::string const& metaVariableName) const {
             return manager->hasVariable(metaVariableName);
         }

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<storm::expressions::ExpressionManager> manager;
+            
+            // Keep track of all DD variables of this manager.
+            uint_fast64_t numberOfDdVariables;
         };
     }
 }

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"
@@ -407,3 +409,27 @@ TEST(CuddDd, BddOddTest) {
     EXPECT_EQ(9ul, matrix.getColumnCount());
     EXPECT_EQ(106ul, matrix.getNonzeroEntryCount());
 }
+
+TEST(CuddDd, BddToExpressionTest) {
+    std::shared_ptr<storm::dd::DdManager<storm::dd::DdType::CUDD>> ddManager(new storm::dd::DdManager<storm::dd::DdType::CUDD>());
+    std::pair<storm::expressions::Variable, storm::expressions::Variable> a = ddManager->addMetaVariable("a");
+    std::pair<storm::expressions::Variable, storm::expressions::Variable> b = ddManager->addMetaVariable("b");
+    
+    storm::dd::Bdd<storm::dd::DdType::CUDD> bdd = ddManager->getBddOne();
+    bdd &= ddManager->getEncoding(a.first, 1);
+    bdd |= ddManager->getEncoding(b.first, 0);
+    
+    std::shared_ptr<storm::expressions::ExpressionManager> manager = std::make_shared<storm::expressions::ExpressionManager>();
+    storm::expressions::Variable c = manager->declareBooleanVariable("c");
+    storm::expressions::Variable d = manager->declareBooleanVariable("d");
+    
+    std::unordered_map<uint_fast64_t, storm::expressions::Expression> indexToExpressionMap;
+    indexToExpressionMap[0] = c;
+    indexToExpressionMap[2] = d;
+    auto result = bdd.toExpression(*manager, indexToExpressionMap);
+    
+    for (auto const& expression : result.first) {
+        std::cout << expression << std::endl;
+    }
+    
+}