From 2d8cc2efcd8d8f1cb269cb3f29207e3fbdaec7d0 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Tue, 6 May 2014 18:14:45 +0200
Subject: [PATCH] Added reordering functionality to DD interface.

Former-commit-id: ffb8ad62f132a26a650a988ba117f27c967fb524
---
 src/storage/dd/CuddDdManager.cpp | 21 +++++++++++++++++++++
 src/storage/dd/CuddDdManager.h   | 26 ++++++++++++++++++++++++++
 src/storage/prism/Program.cpp    |  2 +-
 3 files changed, 48 insertions(+), 1 deletion(-)

diff --git a/src/storage/dd/CuddDdManager.cpp b/src/storage/dd/CuddDdManager.cpp
index 64261d0aa..b3854ee36 100644
--- a/src/storage/dd/CuddDdManager.cpp
+++ b/src/storage/dd/CuddDdManager.cpp
@@ -224,6 +224,10 @@ namespace storm {
         Cudd& DdManager<DdType::CUDD>::getCuddManager() {
             return this->cuddManager;
         }
+
+        Cudd const& DdManager<DdType::CUDD>::getCuddManager() const {
+            return this->cuddManager;
+        }
         
         std::vector<std::string> DdManager<DdType::CUDD>::getDdVariableNames() const {
             // First, we initialize a list DD variables and their names.
@@ -246,5 +250,22 @@ namespace storm {
             
             return result;
         }
+        
+        void DdManager<DdType::CUDD>::allowDynamicReordering(bool value) {
+            if (value) {
+                this->getCuddManager().AutodynEnable(CUDD_REORDER_GROUP_SIFT_CONV);
+            } else {
+                this->getCuddManager().AutodynDisable();
+            }
+        }
+        
+        bool DdManager<DdType::CUDD>::isDynamicReorderingAllowed() const {
+            Cudd_ReorderingType type;
+            return this->getCuddManager().ReorderingStatus(&type);
+        }
+        
+        void DdManager<DdType::CUDD>::triggerReordering() {
+            this->getCuddManager().ReduceHeap(CUDD_REORDER_GROUP_SIFT_CONV, 0);
+        }
     }
 }
\ No newline at end of file
diff --git a/src/storage/dd/CuddDdManager.h b/src/storage/dd/CuddDdManager.h
index 25844598c..6fba4d254 100644
--- a/src/storage/dd/CuddDdManager.h
+++ b/src/storage/dd/CuddDdManager.h
@@ -138,6 +138,25 @@ namespace storm {
              */
             bool hasMetaVariable(std::string const& metaVariableName) const;
             
+            /*!
+             * Sets whether or not dynamic reordering is allowed for the DDs managed by this manager.
+             *
+             * @param value If set to true, dynamic reordering is allowed and forbidden otherwise.
+             */
+            void allowDynamicReordering(bool value);
+            
+            /*!
+             * Retrieves whether dynamic reordering is currently allowed.
+             *
+             * @return True iff dynamic reordering is currently allowed.
+             */
+            bool isDynamicReorderingAllowed() const;
+            
+            /*!
+             * Triggers a reordering of the DDs managed by this manager.
+             */
+            void triggerReordering();
+            
         private:
             /*!
              * Retrieves a list of names of the DD variables in the order of their index.
@@ -153,6 +172,13 @@ namespace storm {
              */
             Cudd& getCuddManager();
             
+            /*!
+             * Retrieves the underlying CUDD manager.
+             *
+             * @return The underlying CUDD manager.
+             */
+            Cudd const& getCuddManager() const;
+            
             // A mapping from variable names to the meta variable information.
             std::unordered_map<std::string, DdMetaVariable<DdType::CUDD>> metaVariableMap;
             
diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp
index 10a1114e6..617a1c52b 100644
--- a/src/storage/prism/Program.cpp
+++ b/src/storage/prism/Program.cpp
@@ -13,7 +13,7 @@ namespace storm {
         Program::Program(ModelType modelType, std::vector<Constant> const& constants, std::vector<BooleanVariable> const& globalBooleanVariables, std::vector<IntegerVariable> const& globalIntegerVariables, std::vector<Formula> const& formulas, std::vector<Module> const& modules, std::vector<RewardModel> const& rewardModels, bool fixInitialConstruct, storm::prism::InitialConstruct const& initialConstruct, std::vector<Label> const& labels, std::string const& filename, uint_fast64_t lineNumber, bool checkValidity) : LocatedInformation(filename, lineNumber), modelType(modelType), constants(constants), constantToIndexMap(), globalBooleanVariables(globalBooleanVariables), globalBooleanVariableToIndexMap(), globalIntegerVariables(globalIntegerVariables), globalIntegerVariableToIndexMap(), formulas(formulas), formulaToIndexMap(), modules(modules), moduleToIndexMap(), rewardModels(rewardModels), rewardModelToIndexMap(), initialConstruct(initialConstruct), labels(labels), labelToIndexMap(), actions(), actionsToModuleIndexMap(), variableToModuleIndexMap() {
             this->createMappings();
             
-            // Create a new initial construct if none was given explicitly.
+            // Create a new initial construct if the corresponding flag was set.
             if (fixInitialConstruct) {
                 if (this->getInitialConstruct().getInitialStatesExpression().isFalse()) {
                     storm::expressions::Expression newInitialExpression = storm::expressions::Expression::createTrue();