fixed bug in sylvan

Former-commit-id: 3f3a3df83d

resources/3rdparty/sylvan/src/sylvan_mtbdd.c

@@ -1434,8 +1434,8 @@ TASK_4(MTBDD, mtbdd_equal_norm_d2, MTBDD, a, MTBDD, b, size_t, svalue, int*, sho
     if (result != SYNC(mtbdd_equal_norm_d2)) result = mtbdd_false;
     if (result == mtbdd_false) *shortcircuit = 1;
 
-    /* Store in cache */
-    cache_put3(CACHE_MTBDD_EQUAL_NORM, a, b, svalue, result);
+    /* Store in cache (only if we are not short circuiting) */
+    if (!*shortcircuit) cache_put3(CACHE_MTBDD_EQUAL_NORM, a, b, svalue, result);
     return result;
 }
 
@@ -1470,7 +1470,7 @@ TASK_4(MTBDD, mtbdd_equal_norm_rel_d2, MTBDD, a, MTBDD, b, size_t, svalue, int*,
         // assume Double MTBDD
         double va = mtbdd_getdouble(a);
         double vb = mtbdd_getdouble(b);
-        if (va == 0) return mtbdd_false;
+        if (va == 0.0 || va == -0.0) return mtbdd_false;
         va = (va - vb) / va;
         if (va < 0) va = -va;
         return (va < *(double*)&svalue) ? mtbdd_true : mtbdd_false;
@@ -1501,8 +1501,8 @@ TASK_4(MTBDD, mtbdd_equal_norm_rel_d2, MTBDD, a, MTBDD, b, size_t, svalue, int*,
     if (result != SYNC(mtbdd_equal_norm_rel_d2)) result = mtbdd_false;
     if (result == mtbdd_false) *shortcircuit = 1;
 
-    /* Store in cache */
-    cache_put3(CACHE_MTBDD_EQUAL_NORM_REL, a, b, svalue, result);
+    /* Store in cache (only if we are not short circuiting) */
+    if (!*shortcircuit) cache_put3(CACHE_MTBDD_EQUAL_NORM_REL, a, b, svalue, result);
     return result;
 }
 

resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.c

@@ -1,3 +1,40 @@
+/**
+ * Generate SHA2 structural hashes.
+ * Hashes are independent of location.
+ * Mainly useful for debugging purposes.
+ */
+static void
+mtbdd_sha2_rec(MTBDD mtbdd, SHA256_CTX *ctx)
+{
+    if (mtbdd == sylvan_true || mtbdd == sylvan_false) {
+        SHA256_Update(ctx, (void*)&mtbdd, sizeof(MTBDD));
+        return;
+    }
+    
+    mtbddnode_t node = GETNODE(mtbdd);
+    if (mtbddnode_isleaf(node)) {
+        uint64_t val = mtbddnode_getvalue(node);
+        SHA256_Update(ctx, (void*)&val, sizeof(uint64_t));
+    } else if (mtbddnode_getmark(node) == 0) {
+        mtbddnode_setmark(node, 1);
+        uint32_t level = mtbddnode_getvariable(node);
+        if (MTBDD_STRIPMARK(mtbddnode_gethigh(node))) level |= 0x80000000;
+        SHA256_Update(ctx, (void*)&level, sizeof(uint32_t));
+        mtbdd_sha2_rec(mtbddnode_gethigh(node), ctx);
+        mtbdd_sha2_rec(mtbddnode_getlow(node), ctx);
+    }
+}
+
+void
+mtbdd_getsha(MTBDD mtbdd, char *target)
+{
+    SHA256_CTX ctx;
+    SHA256_Init(&ctx);
+    mtbdd_sha2_rec(mtbdd, &ctx);
+    if (mtbdd != sylvan_true && mtbdd != sylvan_false) mtbdd_unmark_rec(mtbdd);
+    SHA256_End(&ctx, target);
+}
+
 /**
  * Binary operation Times (for MTBDDs of same type)
  * Only for MTBDDs where either all leaves are Integer or Double.

resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.h

@@ -1,3 +1,5 @@
+void mtbdd_getsha(MTBDD mtbdd, char *target); // target must be at least 65 bytes...
+
 /**
  * Binary operation Divide (for MTBDDs of same type)
  * Only for MTBDDs where all leaves are Integer or Double.

resources/3rdparty/sylvan/src/sylvan_obj_mtbdd_storm.hpp

@@ -48,4 +48,4 @@
      */
     void PrintDot(FILE *out) const;
 
-    
+    std::string GetShaHash() const;

resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp

@@ -131,3 +131,11 @@ void
 Mtbdd::PrintDot(FILE *out) const {
     mtbdd_fprintdot(out, mtbdd, NULL);
 }
+
+std::string
+Mtbdd::GetShaHash() const {
+    char buf[65];
+    mtbdd_getsha(mtbdd, buf);
+    return std::string(buf);
+}
+

src/solver/SymbolicMinMaxLinearEquationSolver.cpp

@@ -61,7 +61,7 @@ namespace storm {
                 
                 ++iterations;
             }
-            
+                        
             return xCopy;
         }