From fd417fb6d63efa4d275a4b700a7a164b3806f983 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Thu, 3 Dec 2015 23:01:37 +0100
Subject: [PATCH] started working on ODD-based functionality for sylvan

Former-commit-id: 6535ee4b47be91b6a27cb92f3fe6c946bc2d19b7
---
 src/storage/dd/sylvan/InternalSylvanBdd.cpp | 61 ++++++++++++++++++++-
 src/storage/dd/sylvan/InternalSylvanBdd.h   | 15 +++++
 2 files changed, 75 insertions(+), 1 deletion(-)

diff --git a/src/storage/dd/sylvan/InternalSylvanBdd.cpp b/src/storage/dd/sylvan/InternalSylvanBdd.cpp
index f7cedfe04..7f8b5f244 100644
--- a/src/storage/dd/sylvan/InternalSylvanBdd.cpp
+++ b/src/storage/dd/sylvan/InternalSylvanBdd.cpp
@@ -19,7 +19,66 @@ namespace storm {
         
         template<typename ValueType>
         InternalBdd<DdType::Sylvan> InternalBdd<DdType::Sylvan>::fromVector(InternalDdManager<DdType::Sylvan> const* ddManager, std::vector<ValueType> const& values, Odd const& odd, std::vector<uint_fast64_t> const& sortedDdVariableIndices, std::function<bool (ValueType const&)> const& filter) {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented.");
+            uint_fast64_t offset = 0;
+            return InternalBdd<DdType::Sylvan>(ddManager, sylvan::Bdd(fromVectorRec(offset, 0, sortedDdVariableIndices.size(), values, odd, sortedDdVariableIndices, filter)));
+        }
+        
+        template<typename ValueType>
+        BDD InternalBdd<DdType::Sylvan>::fromVectorRec(uint_fast64_t& currentOffset, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::vector<ValueType> const& values, Odd const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::function<bool (ValueType const&)> const& filter) {
+            if (currentLevel == maxLevel) {
+                // If we are in a terminal node of the ODD, we need to check whether the then-offset of the ODD is one
+                // (meaning the encoding is a valid one) or zero (meaning the encoding is not valid). Consequently, we
+                // need to copy the next value of the vector iff the then-offset is greater than zero.
+                if (odd.getThenOffset() > 0) {
+                    if (filter(values[currentOffset++])) {
+                        return mtbdd_true;
+                    } else {
+                        return mtbdd_false;
+                    }
+                } else {
+                    return mtbdd_false;
+                }
+            } else {
+                // If the total offset is zero, we can just return the constant zero DD.
+                if (odd.getThenOffset() + odd.getElseOffset() == 0) {
+                    return mtbdd_false;
+                }
+                
+                // Determine the new else-successor.
+                BDD elseSuccessor;
+                if (odd.getElseOffset() > 0) {
+                    elseSuccessor = fromVectorRec(currentOffset, currentLevel + 1, maxLevel, values, odd.getElseSuccessor(), ddVariableIndices, filter);
+                } else {
+                    elseSuccessor = mtbdd_false;
+                }
+                sylvan_ref(elseSuccessor);
+                
+                // Determine the new then-successor.
+                BDD thenSuccessor;
+                if (odd.getThenOffset() > 0) {
+                    thenSuccessor = fromVectorRec(currentOffset, currentLevel + 1, maxLevel, values, odd.getThenSuccessor(), ddVariableIndices, filter);
+                } else {
+                    thenSuccessor = mtbdd_false;
+                }
+                sylvan_ref(thenSuccessor);
+                
+                // Create a node representing ITE(currentVar, thenSuccessor, elseSuccessor);
+                BDD result = sylvan_ithvar(static_cast<BDDVAR>(ddVariableIndices[currentLevel]));
+                sylvan_ref(result);
+                LACE_ME;
+                BDD newResult = sylvan_ite(result, thenSuccessor, elseSuccessor);
+                sylvan_ref(newResult);
+                
+                // Dispose of the intermediate results
+                sylvan_deref(result);
+                sylvan_deref(thenSuccessor);
+                sylvan_deref(elseSuccessor);
+                
+                // Before returning, we remove the protection imposed by the previous call to sylvan_ref.
+                sylvan_deref(newResult);
+                
+                return newResult;
+            }
         }
         
         bool InternalBdd<DdType::Sylvan>::operator==(InternalBdd<DdType::Sylvan> const& other) const {
diff --git a/src/storage/dd/sylvan/InternalSylvanBdd.h b/src/storage/dd/sylvan/InternalSylvanBdd.h
index 9502c2136..ebf60ca68 100644
--- a/src/storage/dd/sylvan/InternalSylvanBdd.h
+++ b/src/storage/dd/sylvan/InternalSylvanBdd.h
@@ -326,6 +326,21 @@ namespace storm {
             void filterExplicitVector(Odd const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<ValueType> const& sourceValues, std::vector<ValueType>& targetValues) const;
             
         private:
+            /*!
+             * Builds a BDD representing the values that make the given filter function evaluate to true.
+             *
+             * @param currentOffset The current offset in the vector.
+             * @param currentLevel The current level in the DD.
+             * @param maxLevel The maximal level in the DD.
+             * @param values The values that are to be checked against the filter function.
+             * @param odd The ODD used for the translation.
+             * @param ddVariableIndices The (sorted) list of DD variable indices to use.
+             * @param filter A function that determines which encodings are to be mapped to true.
+             * @return The resulting (Sylvan) BDD node.
+             */
+            template<typename ValueType>
+            static BDD fromVectorRec(uint_fast64_t& currentOffset, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::vector<ValueType> const& values, Odd const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::function<bool (ValueType const&)> const& filter);
+
             sylvan::Bdd& getSylvanBdd();
             sylvan::Bdd const& getSylvanBdd() const;