From 4b24be7204a9cb5c4096390e7bc9379f11f09b40 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Wed, 23 Sep 2015 19:27:32 +0200
Subject: [PATCH] commit to switch workplace

Former-commit-id: c50e423557b14078feaed04e2921274a5bfc731d
---
 src/storage/dd/CuddBdd.cpp | 24 ++++++++++++++++++++++++
 src/storage/dd/CuddBdd.h   | 14 ++++++++++++++
 2 files changed, 38 insertions(+)

diff --git a/src/storage/dd/CuddBdd.cpp b/src/storage/dd/CuddBdd.cpp
index 476cd0880..98d50132a 100644
--- a/src/storage/dd/CuddBdd.cpp
+++ b/src/storage/dd/CuddBdd.cpp
@@ -367,6 +367,30 @@ namespace storm {
             return result;
         }
         
+        std::pair<std::vector<storm::expressions::Expression>, std::unordered_map<std::pair<uint_fast64_t, uint_fast64_t>, storm::expressions::Variable>> Bdd<DdType::CUDD>::toExpression(storm::expressions::ExpressionManager& manager, std::unordered_map<uint_fast64_t, storm::expressions::Expression> const& indexToExpressionMap) const {
+            std::pair<std::vector<storm::expressions::Expression>, std::unordered_map<std::pair<uint_fast64_t, uint_fast64_t>, storm::expressions::Variable>> result;
+            
+            // 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);
+            
+            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);
+            
+            // Terminal cases.
+            if (F == Cudd_ReadOne(ddManager.getManager())) {
+                
+            }
+            
+            // Non-terminal cases.
+            // (1) Check if we have seen the node before.
+            auto nodeIt = nodeToCounterMap.find();
+        }
+        
         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 {
             // If there are no more values to select, we can directly return.
             if (dd == Cudd_ReadLogicZero(manager.getManager()) && !complement) {
diff --git a/src/storage/dd/CuddBdd.h b/src/storage/dd/CuddBdd.h
index 6ad869428..a8e434958 100644
--- a/src/storage/dd/CuddBdd.h
+++ b/src/storage/dd/CuddBdd.h
@@ -1,6 +1,7 @@
 #ifndef STORM_STORAGE_DD_CUDDBDD_H_
 #define STORM_STORAGE_DD_CUDDBDD_H_
 
+#include <unordered_map>
 #include <boost/functional/hash.hpp>
 
 #include "src/storage/dd/Bdd.h"
@@ -303,6 +304,17 @@ namespace storm {
              */
             storm::storage::BitVector toVector(storm::dd::Odd<DdType::CUDD> const& rowOdd) const;
             
+            /*!
+             * Translates the function the BDD is representing to a set of expressions that characterize the function.
+             *
+             * @param manager The manager that is used to build the expression and, in particular, create new variables in.
+             * @param indexToExpressionMap A mapping from indices (of DD variables) to expressions with which they are
+             * to be replaced.
+             * @return A pair consisting of the created expressions and a mapping from pairs (i, j) to variables such
+             * that the i-th variable of level j is represented by the mapped-to variable.
+             */
+            std::pair<std::vector<storm::expressions::Expression>, std::unordered_map<std::pair<uint_fast64_t, uint_fast64_t>, storm::expressions::Variable>> toExpression(storm::expressions::ExpressionManager& manager, std::unordered_map<uint_fast64_t, storm::expressions::Expression> const& indexToExpressionMap) const;
+            
         private:
             /*!
              * Retrieves the CUDD BDD object associated with this DD.
@@ -370,6 +382,8 @@ 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;
+            
             // The BDD created by CUDD.
             BDD cuddBdd;
         };