fixed bug in recent optimization (only CUDD-based implementation was faulty)

src/storm/storage/dd/bisimulation/SignatureRefiner.cpp

@@ -198,7 +198,11 @@ namespace storm {
                             result = thenResult;
                         } else {
                             // Get the node to connect the subresults.
-                            result = cuddUniqueInter(ddman, Cudd_NodeReadIndex(nonBlockVariablesNode) + offset, thenResult, elseResult);
+                            bool complemented = Cudd_IsComplement(thenResult);
+                            result = cuddUniqueInter(ddman, Cudd_NodeReadIndex(nonBlockVariablesNode) + offset, Cudd_Regular(thenResult), complemented ? Cudd_Not(elseResult) : elseResult);
+                            if (complemented) {
+                                result = Cudd_Not(result);
+                            }
                             Cudd_Deref(thenResult);
                             Cudd_Deref(elseResult);
                         }

src/storm/storage/dd/cudd/InternalCuddDdManager.cpp

@@ -58,18 +58,10 @@ namespace storm {
         }
         
         InternalBdd<DdType::CUDD> InternalDdManager<DdType::CUDD>::getBddEncodingLessOrEqualThan(uint64_t bound, InternalBdd<DdType::CUDD> const& cube, uint64_t numberOfDdVariables) const {
-            DdNodePtr node = this->getBddEncodingLessOrEqualThanRec(0, (1ull << numberOfDdVariables) - 1, bound, cube.getCuddDdNode(), numberOfDdVariables);
-            STORM_LOG_ASSERT(node != nullptr, "Wut?");
-            FILE* fp = fopen("range.dot", "w");
-            Cudd_DumpDot(cuddManager.getManager(), 1, &node, nullptr, nullptr, fp);
-            fclose(fp);
-            
-            auto tmp = cudd::BDD(cuddManager, node);
-            return InternalBdd<DdType::CUDD>(this, tmp);
+            return InternalBdd<DdType::CUDD>(this, cudd::BDD(cuddManager, this->getBddEncodingLessOrEqualThanRec(0, (1ull << numberOfDdVariables) - 1, bound, cube.getCuddDdNode(), numberOfDdVariables)));
         }
         
         DdNodePtr InternalDdManager<DdType::CUDD>::getBddEncodingLessOrEqualThanRec(uint64_t minimalValue, uint64_t maximalValue, uint64_t bound, DdNodePtr cube, uint64_t remainingDdVariables) const {
-            std::cout << minimalValue << " / " << maximalValue << " -> " << bound << std::endl;
             if (maximalValue <= bound) {
                 return Cudd_ReadOne(cuddManager.getManager());
             } else if (minimalValue > bound) {
@@ -85,9 +77,11 @@ namespace storm {
             Cudd_Ref(thenResult);
             STORM_LOG_ASSERT(thenResult != elseResult, "Expected different results.");
             
-            std::cout << "creating " << Cudd_NodeReadIndex(cube) << " -> " << thenResult << " / " << elseResult << std::endl;
-            DdNodePtr result = cuddUniqueInter(cuddManager.getManager(), Cudd_NodeReadIndex(cube), thenResult, elseResult);
-            std::cout << "result " << result << std::endl;
+            bool complemented = Cudd_IsComplement(thenResult);
+            DdNodePtr result = cuddUniqueInter(cuddManager.getManager(), Cudd_NodeReadIndex(cube), Cudd_Regular(thenResult), complemented ? Cudd_Not(elseResult) : elseResult);
+            if (complemented) {
+                result = Cudd_Not(result);
+            }
             Cudd_Deref(thenResult);
             Cudd_Deref(elseResult);
             return result;