Merging the rewriting

Former-commit-id: 44107239d3

examples/dft/seq1.dft

@@ -1,5 +1,5 @@
 toplevel "A";
 "A" and "B" "C";
-"X" seq "B" "C";
+"X" seq "B" "C"
 "B" lambda=0.5 dorm=0.3;
 "C" lambda=0.5 dorm=0.3;

examples/dft/seq2.dft

@@ -0,0 +1,6 @@
+toplevel "A";
+"A" and "B" "C" "D";
+"X" seq "B" "C" "D";
+"B" lambda=0.5 dorm=0.3;
+"C" lambda=0.5 dorm=0.3;
+"D" lambda=0.5 dorm=0.3;

examples/dft/seq3.dft

@@ -0,0 +1,6 @@
+toplevel "A";
+"A" and "C" "D";
+"X" seq "B" "C" "D";
+"B" lambda=0.5 dorm=0.3;
+"C" lambda=0.5 dorm=0.3;
+"D" lambda=0.5 dorm=0.3;

examples/dft/seq3.txt

@@ -0,0 +1,6 @@
+toplevel "A";
+"A" and "C" "D";
+"X" seq "B" "C" "D";
+"B" lambda=0.5 dorm=0.3;
+"C" lambda=0.5 dorm=0.3;
+"D" lambda=0.5 dorm=0.3;

examples/dft/seq4.dft

@@ -0,0 +1,6 @@
+toplevel "A";
+"A" or "C" "D";
+"X" seq "B" "C" "D";
+"B" lambda=0.5 dorm=0.3;
+"C" lambda=0.5 dorm=0.3;
+"D" lambda=0.5 dorm=0.3;

examples/dft/seq5.dft

@@ -0,0 +1,7 @@
+toplevel "A";
+"A" and "T1" "B3";
+"T1" or "B1" "B2";
+"X" seq "B1" "B2" "B3";
+"B1" lambda=0.5 dorm=0.3;
+"B2" lambda=0.5 dorm=0.3;
+"B3" lambda=0.5 dorm=0.3;

examples/dft/seq6.dft

@@ -0,0 +1,8 @@
+toplevel "A";
+"A" and "T1" "T2";
+"T1" pand "B1" "B2"; 
+"T2" pand "B3" "B4;
+"B1" lambda=0.7 dorm=0.3;
+"B2" lambda=0.5 dorm=0.3;
+"B3" lambda=0.5 dorm=0.3;
+"B4" lambda=0.7 dorm=0.3;

src/storage/dft/DFT.cpp

@@ -232,12 +232,21 @@ namespace storm {
         
         template<typename ValueType>
         DFT<ValueType> DFT<ValueType>::optimize() const {
-            std::vector<std::vector<size_t>> rewriteIds = findModulesRewrite();
-            if (rewriteIds.empty()) {
+            std::vector<size_t> modIdea = findModularisationRewrite();
+            std::cout << "Modularisation idea: " << std::endl;
+    
+            for( auto const& i  : modIdea ) {
+                std::cout << i << ", ";
+            }
+
+            if (modIdea.empty()) {
                 // No rewrite needed
                 return *this;
             }
             
+            std::vector<std::vector<size_t>> rewriteIds;
+            rewriteIds.push_back(modIdea);
+            
             DFTBuilder<ValueType> builder;
             
             // Accumulate elements which must be rewritten
@@ -517,6 +526,41 @@ namespace storm {
             }
             return DFTIndependentSymmetries(res);
         }
+        
+        template<typename ValueType>
+        std::vector<size_t> DFT<ValueType>::findModularisationRewrite() const {
+           for(auto const& e : mElements) {
+               if(e->isGate() && (e->type() == DFTElementType::AND || e->type() == DFTElementType::OR) ) {
+                   // suitable parent gate! - Lets check the independent submodules of the children
+                   auto const& children = std::static_pointer_cast<DFTGate<ValueType>>(e)->children();
+                   for(auto const& child : children) {
+                       //std::cout << "check idea for: " << child->id() << std::endl;;
+                       auto ISD = std::static_pointer_cast<DFTGate<ValueType>>(child)->independentSubDft(true);
+                       // In the ISD, check for other children:
+                       //std::cout << "** subdft = ";
+                       for(auto const& isdelemid : ISD) {
+                           std::cout << isdelemid << " ";
+                       }
+                       std::cout << std::endl;
+                       
+                       std::vector<size_t> rewrite = {e->id(), child->id()};
+                       for(size_t isdElemId : ISD) {
+                           if(isdElemId == child->id()) continue;
+                           if(std::find_if(children.begin(), children.end(), [&isdElemId](std::shared_ptr<DFTElement<ValueType>> const& e) { return e->id() == isdElemId; } ) != children.end()) {
+                               //std::cout << "** found child in subdft: " <<  isdElemId << std::endl;
+                               rewrite.push_back(isdElemId);
+                           }
+                       }
+                       if(rewrite.size() > 2) {
+                           return rewrite;
+                       }
+                       
+                   }    
+               }
+           } 
+           return {};
+        }
+    
 
         template<typename ValueType>
         std::pair<std::vector<size_t>, std::vector<size_t>> DFT<ValueType>::getSortedParentAndOutDepIds(size_t index) const {
@@ -530,14 +574,6 @@ namespace storm {
             return res;
         }
         
-        template<typename ValueType>
-        std::vector<std::vector<size_t>> DFT<ValueType>::findModulesRewrite() const {
-            std::vector<std::vector<size_t>> modulesRewrite;
-            // TODO write
-            return modulesRewrite;
-        }
-        
-
         // Explicitly instantiate the class.
         template class DFT<double>;
 

src/storage/dft/DFT.h

@@ -243,8 +243,8 @@ namespace storm {
 
             std::vector<size_t> immediateFailureCauses(size_t index) const;
             
-            std::vector<std::vector<size_t>> findModulesRewrite() const;
-            
+            std::vector<size_t> findModularisationRewrite() const;
+        
         private:
             std::pair<std::vector<size_t>, std::vector<size_t>> getSortedParentAndOutDepIds(size_t index) const;