update to latest version of sylvan and accompanying changes (mostly because 0 * inf = nan in IEEE754)

Former-commit-id: 828e13307f

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

@@ -71,13 +71,20 @@ mtbdd_getvalue(MTBDD leaf)
     return mtbddnode_getvalue(GETNODE(leaf));
 }
 
+// for leaf type 0 (integer)
+int64_t
+mtbdd_getint64(MTBDD leaf)
+{
+    uint64_t value = mtbdd_getvalue(leaf);
+    return *(int64_t*)&value;
+}
+
+// for leaf type 1 (double)
 double
 mtbdd_getdouble(MTBDD leaf)
 {
     uint64_t value = mtbdd_getvalue(leaf);
-    double dv = *(double*)&value;
-    if (mtbdd_isnegated(leaf)) return -dv;
-    else return dv;
+    return *(double*)&value;
 }
 
 /**
@@ -469,31 +476,26 @@ gcd(uint32_t u, uint32_t v)
  */
 
 MTBDD
-mtbdd_uint64(uint64_t value)
+mtbdd_int64(int64_t value)
 {
-    return mtbdd_makeleaf(0, value);
+    return mtbdd_makeleaf(0, *(uint64_t*)&value);
 }
 
 MTBDD
 mtbdd_double(double value)
 {
-    if (value < 0.0) {
-        value = -value;
-        return mtbdd_negate(mtbdd_makeleaf(1, *(uint64_t*)&value));
-    } else {
-        return mtbdd_makeleaf(1, *(uint64_t*)&value);
-    }
+    return mtbdd_makeleaf(1, *(uint64_t*)&value);
 }
 
 MTBDD
-mtbdd_fraction(uint64_t nom, uint64_t denom)
+mtbdd_fraction(int64_t nom, uint64_t denom)
 {
     if (nom == 0) return mtbdd_makeleaf(2, 1);
-    uint32_t c = gcd(nom, denom);
+    uint32_t c = gcd(nom < 0 ? -nom : nom, denom);
     nom /= c;
     denom /= c;
-    if (nom > 0xffffffff || denom > 0xffffffff) fprintf(stderr, "mtbdd_fraction: fraction overflow\n");
-    return mtbdd_makeleaf(2, ((uint64_t)nom)<<32|denom);
+    if (nom > 2147483647 || nom < -2147483647 || denom > 4294967295) fprintf(stderr, "mtbdd_fraction: fraction overflow\n");
+    return mtbdd_makeleaf(2, (nom<<32)|denom);
 }
 
 /**
@@ -819,21 +821,17 @@ TASK_2(MTBDD, mtbdd_uop_times_uint, MTBDD, a, size_t, k)
 
     if (mtbddnode_isleaf(na)) {
         if (mtbddnode_gettype(na) == 0) {
-            uint64_t v = mtbddnode_getvalue(na);
-            v *= k;
-            if (mtbdd_isnegated(a)) return mtbdd_negate(mtbdd_uint64(v));
-            else return mtbdd_uint64(v);
+            int64_t v = mtbdd_getint64(a);
+            return mtbdd_int64(v*k);
         } else if (mtbddnode_gettype(na) == 1) {
             double d = mtbdd_getdouble(a);
             return mtbdd_double(d*k);
         } else if (mtbddnode_gettype(na) == 2) {
-            if (k>0xffffffff) fprintf(stderr, "mtbdd_uop_times_uint: k is too big for fraction multiplication\n");
             uint64_t v = mtbddnode_getvalue(na);
-            uint64_t n = v>>32;
+            int64_t n = (int32_t)(v>>32);
             uint32_t d = v;
             uint32_t c = gcd(d, (uint32_t)k);
-            if (mtbdd_isnegated(a)) return mtbdd_negate(mtbdd_fraction(n*(k/c), d/c));
-            else return mtbdd_fraction(n*(k/c), d/c);
+            return mtbdd_fraction(n*(k/c), d/c);
         }
     }
 
@@ -850,20 +848,14 @@ TASK_2(MTBDD, mtbdd_uop_pow_uint, MTBDD, a, size_t, k)
 
     if (mtbddnode_isleaf(na)) {
         if (mtbddnode_gettype(na) == 0) {
-            uint64_t v = mtbddnode_getvalue(na);
-            v = (uint64_t)pow(v, k);
-            if (mtbdd_isnegated(a) && (k & 1)) return mtbdd_negate(mtbdd_uint64(v));
-            else return mtbdd_uint64(v);
+            int64_t v = mtbdd_getint64(a);
+            return mtbdd_int64(pow(v, k));
         } else if (mtbddnode_gettype(na) == 1) {
             double d = mtbdd_getdouble(a);
             return mtbdd_double(pow(d, k));
         } else if (mtbddnode_gettype(na) == 2) {
             uint64_t v = mtbddnode_getvalue(na);
-            uint64_t n = v>>32;
-            uint32_t d = v;
-            n = (uint64_t)pow(n, k);
-            if (mtbdd_isnegated(a)) return mtbdd_negate(mtbdd_fraction(n, d));
-            else return mtbdd_fraction(n, d);
+            return mtbdd_fraction(pow((int32_t)(v>>32), k), (uint32_t)v);
         }
     }
 
@@ -1003,77 +995,15 @@ TASK_IMPL_2(MTBDD, mtbdd_op_plus, MTBDD*, pa, MTBDD*, pb)
         uint64_t val_a = mtbddnode_getvalue(na);
         uint64_t val_b = mtbddnode_getvalue(nb);
         if (mtbddnode_gettype(na) == 0 && mtbddnode_gettype(nb) == 0) {
-            // both uint64_t
-            if (val_a == 0) return b;
-            else if (val_b == 0) return a;
-            else {
-                int nega = mtbdd_isnegated(a);
-                int negb = mtbdd_isnegated(b);
-                if (nega) {
-                    if (negb) {
-                        // -a + -b = -(a+b)
-                        return mtbdd_negate(mtbdd_uint64(val_a + val_b));
-                    } else {
-                        // b - a
-                        if (val_b >= val_a) {
-                            return mtbdd_uint64(val_b - val_a);
-                        } else {
-                            return mtbdd_negate(mtbdd_uint64(val_a - val_b));
-                        }
-                    }
-                } else {
-                    if (negb) {
-                        // a - b
-                        if (val_a >= val_b) {
-                            return mtbdd_uint64(val_a - val_b);
-                        } else {
-                            return mtbdd_negate(mtbdd_uint64(val_b - val_a));
-                        }
-                    } else {
-                        // a + b
-                        return mtbdd_uint64(val_a + val_b);
-                    }
-                }
-            }
+            // both integer
+            return mtbdd_int64(*(int64_t*)(&val_a) + *(int64_t*)(&val_b));
         } else if (mtbddnode_gettype(na) == 1 && mtbddnode_gettype(nb) == 1) {
             // both double
-            double vval_a = *(double*)&val_a;
-            double vval_b = *(double*)&val_b;
-            if (vval_a == 0.0) return b;
-            else if (vval_b == 0.0) return a;
-            else {
-                int nega = mtbdd_isnegated(a);
-                int negb = mtbdd_isnegated(b);
-                if (nega) {
-                    if (negb) {
-                        // -a + -b = -(a+b)
-                        return mtbdd_negate(mtbdd_double(vval_a + vval_b));
-                    } else {
-                        // b - a
-                        if (val_b >= val_a) {
-                            return mtbdd_double(vval_b - vval_a);
-                        } else {
-                            return mtbdd_negate(mtbdd_double(vval_a - vval_b));
-                        }
-                    }
-                } else {
-                    if (negb) {
-                        // a - b
-                        if (val_a >= val_b) {
-                            return mtbdd_double(vval_a - vval_b);
-                        } else {
-                            return mtbdd_negate(mtbdd_double(vval_b - vval_a));
-                        }
-                    } else {
-                        // a + b
-                        return mtbdd_double(vval_a + vval_b);
-                    }
-                }
-            }
+            return mtbdd_double(*(double*)(&val_a) + *(double*)(&val_b));
         } else if (mtbddnode_gettype(na) == 2 && mtbddnode_gettype(nb) == 2) {
             // both fraction
-            uint64_t nom_a = val_a>>32;
-            uint64_t nom_b = val_b>>32;
+            int64_t nom_a = (int32_t)(val_a>>32);
+            int64_t nom_b = (int32_t)(val_b>>32);
             uint64_t denom_a = val_a&0xffffffff;
             uint64_t denom_b = val_b&0xffffffff;
             // common cases
@@ -1084,18 +1014,8 @@ TASK_IMPL_2(MTBDD, mtbdd_op_plus, MTBDD*, pa, MTBDD*, pb)
             nom_a *= denom_b/c;
             nom_b *= denom_a/c;
             denom_a *= denom_b/c;
-            // add and/or subtract
-            int nega = mtbdd_isnegated(a);
-            int negb = mtbdd_isnegated(b);
-            if (nega) {
-                if (negb) return mtbdd_negate(mtbdd_fraction(nom_a+nom_b, denom_a));
-                else if (nom_b>=nom_a) return mtbdd_fraction(nom_b-nom_a, denom_a);
-                else return mtbdd_negate(mtbdd_fraction(nom_a-nom_b, denom_a));
-            } else {
-                if (!negb) return mtbdd_fraction(nom_a+nom_b, denom_a);
-                else if (nom_a>=nom_b) return mtbdd_fraction(nom_a-nom_b, denom_a);
-                else return mtbdd_negate(mtbdd_fraction(nom_b-nom_a, denom_a));
-            }
+            // add
+            return mtbdd_fraction(nom_a + nom_b, denom_a);
         }
     }
 
@@ -1107,6 +1027,50 @@ TASK_IMPL_2(MTBDD, mtbdd_op_plus, MTBDD*, pa, MTBDD*, pb)
     return mtbdd_invalid;
 }
 
+/**
+ * Binary operation Minus (for MTBDDs of same type)
+ * Only for MTBDDs where either all leaves are Boolean, or Integer, or Double.
+ * For Integer/Double MTBDDs, mtbdd_false is interpreted as "0" or "0.0".
+ */
+TASK_IMPL_2(MTBDD, mtbdd_op_minus, MTBDD*, pa, MTBDD*, pb)
+{
+    MTBDD a = *pa, b = *pb;
+    if (a == mtbdd_false) return mtbdd_negate(b);
+    if (b == mtbdd_false) return a;
+
+    mtbddnode_t na = GETNODE(a);
+    mtbddnode_t nb = GETNODE(b);
+
+    if (mtbddnode_isleaf(na) && mtbddnode_isleaf(nb)) {
+        uint64_t val_a = mtbddnode_getvalue(na);
+        uint64_t val_b = mtbddnode_getvalue(nb);
+        if (mtbddnode_gettype(na) == 0 && mtbddnode_gettype(nb) == 0) {
+            // both integer
+            return mtbdd_int64(*(int64_t*)(&val_a) - *(int64_t*)(&val_b));
+        } else if (mtbddnode_gettype(na) == 1 && mtbddnode_gettype(nb) == 1) {
+            // both double
+            return mtbdd_double(*(double*)(&val_a) - *(double*)(&val_b));
+        } else if (mtbddnode_gettype(na) == 2 && mtbddnode_gettype(nb) == 2) {
+            // both fraction
+            int64_t nom_a = (int32_t)(val_a>>32);
+            int64_t nom_b = (int32_t)(val_b>>32);
+            uint64_t denom_a = val_a&0xffffffff;
+            uint64_t denom_b = val_b&0xffffffff;
+            // common cases
+            if (nom_b == 0) return a;
+            // equalize denominators
+            uint32_t c = gcd(denom_a, denom_b);
+            nom_a *= denom_b/c;
+            nom_b *= denom_a/c;
+            denom_a *= denom_b/c;
+            // subtract
+            return mtbdd_fraction(nom_a - nom_b, denom_a);
+        }
+    }
+
+    return mtbdd_invalid;
+}
+
 /**
  * Binary operation Times (for MTBDDs of same type)
  * Only for MTBDDs where either all leaves are Boolean, or Integer, or Double.
@@ -1129,57 +1093,25 @@ TASK_IMPL_2(MTBDD, mtbdd_op_times, MTBDD*, pa, MTBDD*, pb)
         uint64_t val_a = mtbddnode_getvalue(na);
         uint64_t val_b = mtbddnode_getvalue(nb);
         if (mtbddnode_gettype(na) == 0 && mtbddnode_gettype(nb) == 0) {
-            // both uint64_t
-            if (val_a == 0) return a;
-            else if (val_b == 0) return b;
-            else {
-                MTBDD result;
-                if (val_a == 1) result = mtbdd_regular(b);
-                else if (val_b == 1) result = mtbdd_regular(a);
-                else result = mtbdd_uint64(val_a*val_b);
-                int nega = mtbdd_isnegated(a);
-                int negb = mtbdd_isnegated(b);
-                if (nega ^ negb) return mtbdd_negate(result);
-                else return result;
-            }
+            // both integer
+            return mtbdd_int64(*(int64_t*)(&val_a) * *(int64_t*)(&val_b));
         } else if (mtbddnode_gettype(na) == 1 && mtbddnode_gettype(nb) == 1) {
             // both double
-            double vval_a = *(double*)&val_a;
-            double vval_b = *(double*)&val_b;
-            if (vval_a == 0.0) return a;
-            else if (vval_b == 0.0) return b;
-            else {
-                MTBDD result;
-                if (vval_a == 1.0) result = mtbdd_regular(b);
-                else if (vval_b == 1.0) result = mtbdd_regular(a);
-                else result = mtbdd_double(vval_a*vval_b);
-                int nega = mtbdd_isnegated(a);
-                int negb = mtbdd_isnegated(b);
-                if (nega ^ negb) {
-                    return mtbdd_negate(result);
-                } else {
-                    return result;
-                }
-            }
+            return mtbdd_double(*(double*)(&val_a) * *(double*)(&val_b));
         } else if (mtbddnode_gettype(na) == 2 && mtbddnode_gettype(nb) == 2) {
             // both fraction
-            uint64_t nom_a = val_a>>32;
-            uint64_t nom_b = val_b>>32;
+            int64_t nom_a = (int32_t)(val_a>>32);
+            int64_t nom_b = (int32_t)(val_b>>32);
             uint64_t denom_a = val_a&0xffffffff;
             uint64_t denom_b = val_b&0xffffffff;
             // multiply!
-            uint32_t c = gcd(nom_b, denom_a);
-            uint32_t d = gcd(nom_a, denom_b);
+            uint32_t c = gcd(nom_b < 0 ? -nom_b : nom_b, denom_a);
+            uint32_t d = gcd(nom_a < 0 ? -nom_a : nom_a, denom_b);
             nom_a /= d;
             denom_a /= c;
             nom_a *= (nom_b/c);
             denom_a *= (denom_b/d);
-            // compute result
-            int nega = mtbdd_isnegated(a);
-            int negb = mtbdd_isnegated(b);
-            MTBDD result = mtbdd_fraction(nom_a, denom_a);
-            if (nega ^ negb) return mtbdd_negate(result);
-            else return result;
+            return mtbdd_fraction(nom_a, denom_a);
         }
     }
 
@@ -1215,50 +1147,27 @@ TASK_IMPL_2(MTBDD, mtbdd_op_min, MTBDD*, pa, MTBDD*, pb)
         uint64_t val_a = mtbddnode_getvalue(na);
         uint64_t val_b = mtbddnode_getvalue(nb);
         if (mtbddnode_gettype(na) == 0 && mtbddnode_gettype(nb) == 0) {
-            // both uint64_t
-            int nega = mtbdd_isnegated(a);
-            int negb = mtbdd_isnegated(b);
-            if (nega) {
-                if (negb) return val_a > val_b ? a : b;
-                else return a;
-            } else {
-                if (negb) return b;
-                else return val_a < val_b ? a : b;
-            }
+            // both integer
+            int64_t va = *(int64_t*)(&val_a);
+            int64_t vb = *(int64_t*)(&val_b);
+            return va < vb ? a : b;
         } else if (mtbddnode_gettype(na) == 1 && mtbddnode_gettype(nb) == 1) {
             // both double
-            double vval_a = *(double*)&val_a;
-            double vval_b = *(double*)&val_b;
-            int nega = mtbdd_isnegated(a);
-            int negb = mtbdd_isnegated(b);
-            if (nega) {
-                if (negb) return vval_a > vval_b ? a : b;
-                else return a;
-            } else {
-                if (negb) return b;
-                else return vval_a < vval_b ? a : b;
-            }
+            double va = *(double*)&val_a;
+            double vb = *(double*)&val_b;
+            return va < vb ? a : b;
         } else if (mtbddnode_gettype(na) == 2 && mtbddnode_gettype(nb) == 2) {
             // both fraction
-            uint64_t nom_a = val_a>>32;
-            uint64_t nom_b = val_b>>32;
+            int64_t nom_a = (int32_t)(val_a>>32);
+            int64_t nom_b = (int32_t)(val_b>>32);
             uint64_t denom_a = val_a&0xffffffff;
             uint64_t denom_b = val_b&0xffffffff;
             // equalize denominators
             uint32_t c = gcd(denom_a, denom_b);
             nom_a *= denom_b/c;
             nom_b *= denom_a/c;
-            denom_a *= denom_b/c;
             // compute lowest
-            int nega = mtbdd_isnegated(a);
-            int negb = mtbdd_isnegated(b);
-            if (nega) {
-                if (negb) return nom_a > nom_b ? a : b;
-                else return a;
-            } else {
-                if (negb) return b;
-                else return nom_a < nom_b ? a : b;
-            }
+            return nom_a < nom_b ? a : b;
         }
     }
 
@@ -1292,50 +1201,27 @@ TASK_IMPL_2(MTBDD, mtbdd_op_max, MTBDD*, pa, MTBDD*, pb)
         uint64_t val_a = mtbddnode_getvalue(na);
         uint64_t val_b = mtbddnode_getvalue(nb);
         if (mtbddnode_gettype(na) == 0 && mtbddnode_gettype(nb) == 0) {
-            // both uint64_t
-            int nega = mtbdd_isnegated(a);
-            int negb = mtbdd_isnegated(b);
-            if (nega) {
-                if (negb) return val_a < val_b ? a : b;
-                else return b;
-            } else {
-                if (negb) return a;
-                else return val_a > val_b ? a : b;
-            }
+            // both integer
+            int64_t va = *(int64_t*)(&val_a);
+            int64_t vb = *(int64_t*)(&val_b);
+            return va > vb ? a : b;
         } else if (mtbddnode_gettype(na) == 1 && mtbddnode_gettype(nb) == 1) {
             // both double
             double vval_a = *(double*)&val_a;
             double vval_b = *(double*)&val_b;
-            int nega = mtbdd_isnegated(a);
-            int negb = mtbdd_isnegated(b);
-            if (nega) {
-                if (negb) return vval_a < vval_b ? a : b;
-                else return b;
-            } else {
-                if (negb) return a;
-                else return vval_a > vval_b ? a : b;
-            }
+            return vval_a > vval_b ? a : b;
         } else if (mtbddnode_gettype(na) == 2 && mtbddnode_gettype(nb) == 2) {
             // both fraction
-            uint64_t nom_a = val_a>>32;
-            uint64_t nom_b = val_b>>32;
+            int64_t nom_a = (int32_t)(val_a>>32);
+            int64_t nom_b = (int32_t)(val_b>>32);
             uint64_t denom_a = val_a&0xffffffff;
             uint64_t denom_b = val_b&0xffffffff;
             // equalize denominators
             uint32_t c = gcd(denom_a, denom_b);
             nom_a *= denom_b/c;
             nom_b *= denom_a/c;
-            denom_a *= denom_b/c;
             // compute highest
-            int nega = mtbdd_isnegated(a);
-            int negb = mtbdd_isnegated(b);
-            if (nega) {
-                if (negb) return nom_a < nom_b ? a : b;
-                else return b;
-            } else {
-                if (negb) return a;
-                else return nom_a > nom_b ? a : b;
-            }
+            return nom_a > nom_b ? a : b;
         }
     }
 
@@ -1347,6 +1233,31 @@ TASK_IMPL_2(MTBDD, mtbdd_op_max, MTBDD*, pa, MTBDD*, pb)
     return mtbdd_invalid;
 }
 
+TASK_IMPL_2(MTBDD, mtbdd_op_negate, MTBDD, a, size_t, k)
+{
+    // if a is false, then it is a partial function. Keep partial!
+    if (a == mtbdd_false) return mtbdd_false;
+
+    // a != constant
+    mtbddnode_t na = GETNODE(a);
+
+    if (mtbddnode_isleaf(na)) {
+        if (mtbddnode_gettype(na) == 0) {
+            int64_t v = mtbdd_getint64(a);
+            return mtbdd_int64(-v);
+        } else if (mtbddnode_gettype(na) == 1) {
+            double d = mtbdd_getdouble(a);
+            return mtbdd_double(-d);
+        } else if (mtbddnode_gettype(na) == 2) {
+            uint64_t v = mtbddnode_getvalue(na);
+            return mtbdd_fraction(-(int32_t)(v>>32), (uint32_t)v);
+        }
+    }
+
+    return mtbdd_invalid;
+    (void)k; // unused variable
+}
+
 /**
  * Compute IF <f> THEN <g> ELSE <h>.
  * <f> must be a Boolean MTBDD (or standard BDD).
@@ -1417,11 +1328,11 @@ TASK_IMPL_2(MTBDD, mtbdd_op_threshold_double, MTBDD, a, size_t, svalue)
 
     if (mtbddnode_isleaf(na)) {
         double value = *(double*)&svalue;
-        if (mtbddnode_gettype(na) == 1) return mtbdd_getdouble(a) >= value ? mtbdd_true : mtbdd_false;
-        if (mtbddnode_gettype(na) == 2) {
+        if (mtbddnode_gettype(na) == 1) {
+            return mtbdd_getdouble(a) >= value ? mtbdd_true : mtbdd_false;
+        } else if (mtbddnode_gettype(na) == 2) {
             double d = (double)mtbdd_getnumer(a);
             d /= mtbdd_getdenom(a);
-            if (mtbdd_isnegated(a)) d = -d;
             return d >= value ? mtbdd_true : mtbdd_false;
         }
     }
@@ -1443,11 +1354,11 @@ TASK_IMPL_2(MTBDD, mtbdd_op_strict_threshold_double, MTBDD, a, size_t, svalue)
 
     if (mtbddnode_isleaf(na)) {
         double value = *(double*)&svalue;
-        if (mtbddnode_gettype(na) == 1) return mtbdd_getdouble(a) > value ? mtbdd_true : mtbdd_false;
-        if (mtbddnode_gettype(na) == 2) {
+        if (mtbddnode_gettype(na) == 1) {
+            return mtbdd_getdouble(a) > value ? mtbdd_true : mtbdd_false;
+        } else if (mtbddnode_gettype(na) == 2) {
             double d = (double)mtbdd_getnumer(a);
             d /= mtbdd_getdenom(a);
-            if (mtbdd_isnegated(a)) d = -d;
             return d > value ? mtbdd_true : mtbdd_false;
         }
     }
@@ -1486,9 +1397,7 @@ TASK_4(MTBDD, mtbdd_equal_norm_d2, MTBDD, a, MTBDD, b, size_t, svalue, int*, sho
     if (la && lb) {
         // assume Double MTBDD
         double va = mtbdd_getdouble(a);
-        if (mtbdd_isnegated(a)) va = -va;
         double vb = mtbdd_getdouble(b);
-        if (mtbdd_isnegated(b)) vb = -vb;
         va -= vb;
         if (va < 0) va = -va;
         return (va < *(double*)&svalue) ? mtbdd_true : mtbdd_false;
@@ -1532,7 +1441,7 @@ TASK_4(MTBDD, mtbdd_equal_norm_d2, MTBDD, a, MTBDD, b, size_t, svalue, int*, sho
 
 TASK_IMPL_3(MTBDD, mtbdd_equal_norm_d, MTBDD, a, MTBDD, b, double, d)
 {
-    /* the implementation checks shortcircuit in every task and if the wo
+    /* the implementation checks shortcircuit in every task and if the two
        MTBDDs are not equal module epsilon, then the computation tree quickly aborts */
     int shortcircuit = 0;
     return CALL(mtbdd_equal_norm_d2, a, b, *(size_t*)&d, &shortcircuit);
@@ -1540,6 +1449,7 @@ TASK_IMPL_3(MTBDD, mtbdd_equal_norm_d, MTBDD, a, MTBDD, b, double, d)
 
 /**
  * Compare two Double MTBDDs, returns Boolean True if they are equal within some value epsilon
+ * This version computes the relative difference vs the value in a.
  */
 TASK_4(MTBDD, mtbdd_equal_norm_rel_d2, MTBDD, a, MTBDD, b, size_t, svalue, int*, shortcircuit)
 {
@@ -1559,11 +1469,10 @@ TASK_4(MTBDD, mtbdd_equal_norm_rel_d2, MTBDD, a, MTBDD, b, size_t, svalue, int*,
     if (la && lb) {
         // assume Double MTBDD
         double va = mtbdd_getdouble(a);
-        if (mtbdd_isnegated(a)) va = -va;
         double vb = mtbdd_getdouble(b);
-        if (mtbdd_isnegated(b)) vb = -vb;
         if (va == 0) return mtbdd_false;
-        va = fabs((va - vb) / va);
+        va = (va - vb) / va;
+        if (va < 0) va = -va;
         return (va < *(double*)&svalue) ? mtbdd_true : mtbdd_false;
     }
 
@@ -1599,7 +1508,7 @@ TASK_4(MTBDD, mtbdd_equal_norm_rel_d2, MTBDD, a, MTBDD, b, size_t, svalue, int*,
 
 TASK_IMPL_3(MTBDD, mtbdd_equal_norm_rel_d, MTBDD, a, MTBDD, b, double, d)
 {
-    /* the implementation checks shortcircuit in every task and if the wo
+    /* the implementation checks shortcircuit in every task and if the two
        MTBDDs are not equal module epsilon, then the computation tree quickly aborts */
     int shortcircuit = 0;
     return CALL(mtbdd_equal_norm_rel_d2, a, b, *(size_t*)&d, &shortcircuit);
@@ -1634,43 +1543,28 @@ TASK_3(MTBDD, mtbdd_leq_rec, MTBDD, a, MTBDD, b, int*, shortcircuit)
     int lb = mtbddnode_isleaf(nb);
 
     if (la && lb) {
-        int nega = mtbdd_isnegated(a);
-        int negb = mtbdd_isnegated(b);
-
         uint64_t va = mtbddnode_getvalue(na);
         uint64_t vb = mtbddnode_getvalue(nb);
 
         if (mtbddnode_gettype(na) == 0 && mtbddnode_gettype(nb) == 0) {
-            // type 0 = int64
-            if (va == 0 && vb == 0) result = mtbdd_true;
-            else if (nega && !negb) result = mtbdd_true;
-            else if (nega && negb && va > vb) result = mtbdd_true;
-            else if (!nega && !negb && va < vb) result = mtbdd_true;
-            else result = mtbdd_false;
+            // type 0 = integer
+            result = *(int64_t*)(&va) <= *(int64_t*)(&vb) ? mtbdd_true : mtbdd_false;
         } else if (mtbddnode_gettype(na) == 1 && mtbddnode_gettype(nb) == 1) {
             // type 1 = double
             double vva = *(double*)&va;
             double vvb = *(double*)&vb;
-            if (vva == 0.0 && vvb == 0.0) result = mtbdd_true;
-            else if (nega && !negb) result = mtbdd_true;
-            else if (nega && negb && vva > vvb) result = mtbdd_true;
-            else if (!nega && !negb && vva < vvb) result = mtbdd_true;
-            else result = mtbdd_false;
+            result = vva <= vvb ? mtbdd_true : mtbdd_false;
         } else if (mtbddnode_gettype(na) == 2 && mtbddnode_gettype(nb) == 2) {
             // type 2 = fraction
-            uint64_t nom_a = va>>32;
-            uint64_t nom_b = vb>>32;
+            int64_t nom_a = (int32_t)(va>>32);
+            int64_t nom_b = (int32_t)(vb>>32);
             uint64_t da = va&0xffffffff;
             uint64_t db = vb&0xffffffff;
             // equalize denominators
             uint32_t c = gcd(da, db);
             nom_a *= db/c;
             nom_b *= da/c;
-            if (nom_a == 0 && nom_b == 0) result = mtbdd_true;
-            else if (nega && !negb) result = mtbdd_true;
-            else if (nega && negb && nom_a > nom_b) result = mtbdd_true;
-            else if (!nega && !negb && nom_a < nom_b) result = mtbdd_true;
-            else result = mtbdd_false;
+            result = nom_a <= nom_b ? mtbdd_true : mtbdd_false;
         }
     } else {
         /* Get top variable */
@@ -1699,7 +1593,7 @@ TASK_3(MTBDD, mtbdd_leq_rec, MTBDD, a, MTBDD, b, int*, shortcircuit)
 
 TASK_IMPL_2(MTBDD, mtbdd_leq, MTBDD, a, MTBDD, b)
 {
-    /* the implementation checks shortcircuit in every task and if the wo
+    /* the implementation checks shortcircuit in every task and if the two
        MTBDDs are not equal module epsilon, then the computation tree quickly aborts */
     int shortcircuit = 0;
     return CALL(mtbdd_leq_rec, a, b, &shortcircuit);
@@ -1734,43 +1628,28 @@ TASK_3(MTBDD, mtbdd_less_rec, MTBDD, a, MTBDD, b, int*, shortcircuit)
     int lb = mtbddnode_isleaf(nb);
 
     if (la && lb) {
-        int nega = mtbdd_isnegated(a);
-        int negb = mtbdd_isnegated(b);
-
         uint64_t va = mtbddnode_getvalue(na);
         uint64_t vb = mtbddnode_getvalue(nb);
 
         if (mtbddnode_gettype(na) == 0 && mtbddnode_gettype(nb) == 0) {
-            // type 0 = int64
-            if (va == 0 && vb == 0) result = mtbdd_false;
-            else if (nega && !negb) result = mtbdd_true;
-            else if (nega && negb && va > vb) result = mtbdd_true;
-            else if (!nega && !negb && va < vb) result = mtbdd_true;
-            else result = mtbdd_false;
+            // type 0 = integer
+            result = *(int64_t*)(&va) < *(int64_t*)(&vb) ? mtbdd_true : mtbdd_false;
         } else if (mtbddnode_gettype(na) == 1 && mtbddnode_gettype(nb) == 1) {
             // type 1 = double
             double vva = *(double*)&va;
             double vvb = *(double*)&vb;
-            if (vva == 0.0 && vvb == 0.0) result = mtbdd_false;
-            else if (nega && !negb) result = mtbdd_true;
-            else if (nega && negb && vva > vvb) result = mtbdd_true;
-            else if (!nega && !negb && vva < vvb) result = mtbdd_true;
-            else result = mtbdd_false;
+            result = vva < vvb ? mtbdd_true : mtbdd_false;
         } else if (mtbddnode_gettype(na) == 2 && mtbddnode_gettype(nb) == 2) {
             // type 2 = fraction
-            uint64_t nom_a = va>>32;
-            uint64_t nom_b = vb>>32;
+            int64_t nom_a = (int32_t)(va>>32);
+            int64_t nom_b = (int32_t)(vb>>32);
             uint64_t da = va&0xffffffff;
             uint64_t db = vb&0xffffffff;
             // equalize denominators
             uint32_t c = gcd(da, db);
             nom_a *= db/c;
             nom_b *= da/c;
-            if (nom_a == 0 && nom_b == 0) result = mtbdd_false;
-            else if (nega && !negb) result = mtbdd_true;
-            else if (nega && negb && nom_a > nom_b) result = mtbdd_true;
-            else if (!nega && !negb && nom_a < nom_b) result = mtbdd_true;
-            else result = mtbdd_false;
+            result = nom_a < nom_b ? mtbdd_true : mtbdd_false;
         }
     } else {
         /* Get top variable */
@@ -1799,7 +1678,7 @@ TASK_3(MTBDD, mtbdd_less_rec, MTBDD, a, MTBDD, b, int*, shortcircuit)
 
 TASK_IMPL_2(MTBDD, mtbdd_less, MTBDD, a, MTBDD, b)
 {
-    /* the implementation checks shortcircuit in every task and if the wo
+    /* the implementation checks shortcircuit in every task and if the two
        MTBDDs are not equal module epsilon, then the computation tree quickly aborts */
     int shortcircuit = 0;
     return CALL(mtbdd_less_rec, a, b, &shortcircuit);
@@ -1834,43 +1713,28 @@ TASK_3(MTBDD, mtbdd_geq_rec, MTBDD, a, MTBDD, b, int*, shortcircuit)
     int lb = mtbddnode_isleaf(nb);
 
     if (la && lb) {
-        int nega = mtbdd_isnegated(a);
-        int negb = mtbdd_isnegated(b);
-
         uint64_t va = mtbddnode_getvalue(na);
         uint64_t vb = mtbddnode_getvalue(nb);
 
         if (mtbddnode_gettype(na) == 0 && mtbddnode_gettype(nb) == 0) {
-            // type 0 = int64
-            if (va == 0 && vb == 0) result = mtbdd_true;
-            else if (nega && !negb) result = mtbdd_false;
-            else if (nega && negb && va > vb) result = mtbdd_false;
-            else if (!nega && !negb && va < vb) result = mtbdd_false;
-            else result = mtbdd_true;
+            // type 0 = integer
+            result = *(int64_t*)(&va) >= *(int64_t*)(&vb) ? mtbdd_true : mtbdd_false;
         } else if (mtbddnode_gettype(na) == 1 && mtbddnode_gettype(nb) == 1) {
             // type 1 = double
             double vva = *(double*)&va;
             double vvb = *(double*)&vb;
-            if (vva == 0.0 && vvb == 0.0) result = mtbdd_true;
-            else if (nega && !negb) result = mtbdd_false;
-            else if (nega && negb && vva > vvb) result = mtbdd_false;
-            else if (!nega && !negb && vva < vvb) result = mtbdd_false;
-            else result = mtbdd_true;
+            result = vva >= vvb ? mtbdd_true : mtbdd_false;
         } else if (mtbddnode_gettype(na) == 2 && mtbddnode_gettype(nb) == 2) {
             // type 2 = fraction
-            uint64_t nom_a = va>>32;
-            uint64_t nom_b = vb>>32;
+            int64_t nom_a = (int32_t)(va>>32);
+            int64_t nom_b = (int32_t)(vb>>32);
             uint64_t da = va&0xffffffff;
             uint64_t db = vb&0xffffffff;
             // equalize denominators
             uint32_t c = gcd(da, db);
             nom_a *= db/c;
             nom_b *= da/c;
-            if (nom_a == 0 && nom_b == 0) result = mtbdd_true;
-            else if (nega && !negb) result = mtbdd_false;
-            else if (nega && negb && nom_a > nom_b) result = mtbdd_false;
-            else if (!nega && !negb && nom_a < nom_b) result = mtbdd_false;
-            else result = mtbdd_true;
+            result = nom_a >= nom_b ? mtbdd_true : mtbdd_false;
         }
     } else {
         /* Get top variable */
@@ -1899,7 +1763,7 @@ TASK_3(MTBDD, mtbdd_geq_rec, MTBDD, a, MTBDD, b, int*, shortcircuit)
 
 TASK_IMPL_2(MTBDD, mtbdd_geq, MTBDD, a, MTBDD, b)
 {
-    /* the implementation checks shortcircuit in every task and if the wo
+    /* the implementation checks shortcircuit in every task and if the two
        MTBDDs are not equal module epsilon, then the computation tree quickly aborts */
     int shortcircuit = 0;
     return CALL(mtbdd_geq_rec, a, b, &shortcircuit);
@@ -1934,43 +1798,28 @@ TASK_3(MTBDD, mtbdd_greater_rec, MTBDD, a, MTBDD, b, int*, shortcircuit)
     int lb = mtbddnode_isleaf(nb);
 
     if (la && lb) {
-        int nega = mtbdd_isnegated(a);
-        int negb = mtbdd_isnegated(b);
-
         uint64_t va = mtbddnode_getvalue(na);
         uint64_t vb = mtbddnode_getvalue(nb);
 
         if (mtbddnode_gettype(na) == 0 && mtbddnode_gettype(nb) == 0) {
-            // type 0 = int64
-            if (va == 0 && vb == 0) result = mtbdd_false;
-            else if (nega && !negb) result = mtbdd_false;
-            else if (nega && negb && va > vb) result = mtbdd_false;
-            else if (!nega && !negb && va < vb) result = mtbdd_false;
-            else result = mtbdd_true;
+            // type 0 = integer
+            result = *(int64_t*)(&va) > *(int64_t*)(&vb) ? mtbdd_true : mtbdd_false;
         } else if (mtbddnode_gettype(na) == 1 && mtbddnode_gettype(nb) == 1) {
             // type 1 = double
             double vva = *(double*)&va;
             double vvb = *(double*)&vb;
-            if (vva == 0.0 && vvb == 0.0) result = mtbdd_false;
-            else if (nega && !negb) result = mtbdd_false;
-            else if (nega && negb && vva > vvb) result = mtbdd_false;
-            else if (!nega && !negb && vva < vvb) result = mtbdd_false;
-            else result = mtbdd_true;
+            result = vva > vvb ? mtbdd_true : mtbdd_false;
         } else if (mtbddnode_gettype(na) == 2 && mtbddnode_gettype(nb) == 2) {
             // type 2 = fraction
-            uint64_t nom_a = va>>32;
-            uint64_t nom_b = vb>>32;
+            int64_t nom_a = (int32_t)(va>>32);
+            int64_t nom_b = (int32_t)(vb>>32);
             uint64_t da = va&0xffffffff;
             uint64_t db = vb&0xffffffff;
             // equalize denominators
             uint32_t c = gcd(da, db);
             nom_a *= db/c;
             nom_b *= da/c;
-            if (nom_a == 0 && nom_b == 0) result = mtbdd_false;
-            else if (nega && !negb) result = mtbdd_false;
-            else if (nega && negb && nom_a > nom_b) result = mtbdd_false;
-            else if (!nega && !negb && nom_a < nom_b) result = mtbdd_false;
-            else result = mtbdd_true;
+            result = nom_a > nom_b ? mtbdd_true : mtbdd_false;
         }
     } else {
         /* Get top variable */
@@ -1999,7 +1848,7 @@ TASK_3(MTBDD, mtbdd_greater_rec, MTBDD, a, MTBDD, b, int*, shortcircuit)
 
 TASK_IMPL_2(MTBDD, mtbdd_greater, MTBDD, a, MTBDD, b)
 {
-    /* the implementation checks shortcircuit in every task and if the wo
+    /* the implementation checks shortcircuit in every task and if the two
        MTBDDs are not equal module epsilon, then the computation tree quickly aborts */
     int shortcircuit = 0;
     return CALL(mtbdd_greater_rec, a, b, &shortcircuit);
@@ -2173,48 +2022,24 @@ TASK_IMPL_1(MTBDD, mtbdd_minimum, MTBDD, a)
     MTBDD low = SYNC(mtbdd_minimum);
 
     /* Determine lowest */
-    int negl = mtbdd_isnegated(low);
-    int negh = mtbdd_isnegated(high);
-    if (negl && !negh) result = low;
-    else if (negh && !negl) result = high;
-    else {
-        mtbddnode_t nl = GETNODE(low);
-        mtbddnode_t nh = GETNODE(high);
-        uint64_t val_l = mtbddnode_getvalue(nl);
-        uint64_t val_h = mtbddnode_getvalue(nh);
-
-        if (mtbddnode_gettype(nl) == 0 && mtbddnode_gettype(nh) == 0) {
-            // type 0 = int64
-            if (negl) {
-                result = val_l < val_h ? high : low; // negative numbers!
-            } else {
-                result = val_l < val_h ? low : high;
-            }
-        } else if (mtbddnode_gettype(nl) == 1 && mtbddnode_gettype(nh) == 1) {
-            // type 1 = double
-            double vval_l = *(double*)&val_l;
-            double vval_h = *(double*)&val_h;
-            if (negl) {
-                result = vval_l < vval_h ? high : low; // negative numbers!
-            } else {
-                result = vval_l < vval_h ? low : high;
-            }
-        } else if (mtbddnode_gettype(nl) == 2 && mtbddnode_gettype(nh) == 2) {
-            // type 2 = fraction
-            uint64_t nom_l = val_l>>32;
-            uint64_t nom_h = val_h>>32;
-            uint64_t denom_l = val_l&0xffffffff;
-            uint64_t denom_h = val_h&0xffffffff;
-            // equalize denominators
-            uint32_t c = gcd(denom_l, denom_h);
-            nom_l *= denom_h/c;
-            nom_h *= denom_l/c;
-            if (negl) {
-                result = nom_l < nom_h ? high : low; // negative numbers!
-            } else {
-                result = nom_l < nom_h ? low : high;
-            }
-        }
+    mtbddnode_t nl = GETNODE(low);
+    mtbddnode_t nh = GETNODE(high);
+
+    if (mtbddnode_gettype(nl) == 0 && mtbddnode_gettype(nh) == 0) {
+        result = mtbdd_getint64(low) < mtbdd_getint64(high) ? low : high;
+    } else if (mtbddnode_gettype(nl) == 1 && mtbddnode_gettype(nh) == 1) {
+        result = mtbdd_getdouble(low) < mtbdd_getdouble(high) ? low : high;
+    } else if (mtbddnode_gettype(nl) == 2 && mtbddnode_gettype(nh) == 2) {
+        // type 2 = fraction
+        int64_t nom_l = mtbdd_getnumer(low);
+        int64_t nom_h = mtbdd_getnumer(high);
+        uint64_t denom_l = mtbdd_getdenom(low);
+        uint64_t denom_h = mtbdd_getdenom(high);
+        // equalize denominators
+        uint32_t c = gcd(denom_l, denom_h);
+        nom_l *= denom_h/c;
+        nom_h *= denom_l/c;
+        result = nom_l < nom_h ? low : high;
     }
 
     /* Store in cache */
@@ -2245,48 +2070,24 @@ TASK_IMPL_1(MTBDD, mtbdd_maximum, MTBDD, a)
     MTBDD low = SYNC(mtbdd_maximum);
 
     /* Determine highest */
-    int negl = mtbdd_isnegated(low);
-    int negh = mtbdd_isnegated(high);
-    if (negl && !negh) result = high;
-    else if (negh && !negl) result = low;
-    else {
-        mtbddnode_t nl = GETNODE(low);
-        mtbddnode_t nh = GETNODE(high);
-        uint64_t val_l = mtbddnode_getvalue(nl);
-        uint64_t val_h = mtbddnode_getvalue(nh);
-
-        if (mtbddnode_gettype(nl) == 0 && mtbddnode_gettype(nh) == 0) {
-            // type 0 = int64
-            if (negl) {
-                result = val_l < val_h ? low : high; // negative numbers!
-            } else {
-                result = val_l < val_h ? high : low;
-            }
-        } else if (mtbddnode_gettype(nl) == 1 && mtbddnode_gettype(nh) == 1) {
-            // type 1 = double
-            double vval_l = *(double*)&val_l;
-            double vval_h = *(double*)&val_h;
-            if (negl) {
-                result = vval_l < vval_h ? low : high; // negative numbers!
-            } else {
-                result = vval_l < vval_h ? high : low;
-            }
-        } else if (mtbddnode_gettype(nl) == 2 && mtbddnode_gettype(nh) == 2) {
-            // type 2 = fraction
-            uint64_t nom_l = val_l>>32;
-            uint64_t nom_h = val_h>>32;
-            uint64_t denom_l = val_l&0xffffffff;
-            uint64_t denom_h = val_h&0xffffffff;
-            // equalize denominators
-            uint32_t c = gcd(denom_l, denom_h);
-            nom_l *= denom_h/c;
-            nom_h *= denom_l/c;
-            if (negl) {
-                result = nom_l < nom_h ? low : high; // negative numbers!
-            } else {
-                result = nom_l < nom_h ? high : low;
-            }
-        }
+    mtbddnode_t nl = GETNODE(low);
+    mtbddnode_t nh = GETNODE(high);
+
+    if (mtbddnode_gettype(nl) == 0 && mtbddnode_gettype(nh) == 0) {
+        result = mtbdd_getint64(low) > mtbdd_getint64(high) ? low : high;
+    } else if (mtbddnode_gettype(nl) == 1 && mtbddnode_gettype(nh) == 1) {
+        result = mtbdd_getdouble(low) > mtbdd_getdouble(high) ? low : high;
+    } else if (mtbddnode_gettype(nl) == 2 && mtbddnode_gettype(nh) == 2) {
+        // type 2 = fraction
+        int64_t nom_l = mtbdd_getnumer(low);
+        int64_t nom_h = mtbdd_getnumer(high);
+        uint64_t denom_l = mtbdd_getdenom(low);
+        uint64_t denom_h = mtbdd_getdenom(high);
+        // equalize denominators
+        uint32_t c = gcd(denom_l, denom_h);
+        nom_l *= denom_h/c;
+        nom_h *= denom_l/c;
+        result = nom_l > nom_h ? low : high;
     }
 
     /* Store in cache */
@@ -2560,7 +2361,7 @@ mtbdd_fprintdot_rec(FILE *out, MTBDD mtbdd, print_terminal_label_cb cb)
     } else if (mtbddnode_isleaf(n)) {
         uint32_t type = mtbddnode_gettype(n);
         uint64_t value = mtbddnode_getvalue(n);
-        fprintf(out, "%" PRIu64 " [shape=box, style=filled, label=\"", mtbdd_regular(mtbdd));
+        fprintf(out, "%" PRIu64 " [shape=box, style=filled, label=\"", MTBDD_STRIPMARK(mtbdd));
         switch (type) {
         case 0:
             fprintf(out, "%" PRIu64, value);
@@ -2578,16 +2379,16 @@ mtbdd_fprintdot_rec(FILE *out, MTBDD mtbdd, print_terminal_label_cb cb)
         fprintf(out, "\"];\n");
     } else {
         fprintf(out, "%" PRIu64 " [label=\"%" PRIu32 "\"];\n",
-                mtbdd_regular(mtbdd), mtbddnode_getvariable(n));
+                MTBDD_STRIPMARK(mtbdd), mtbddnode_getvariable(n));
 
-        mtbdd_fprintdot_rec(out, mtbdd_regular(mtbddnode_getlow(n)), cb);
-        mtbdd_fprintdot_rec(out, mtbdd_regular(mtbddnode_gethigh(n)), cb);
+        mtbdd_fprintdot_rec(out, mtbddnode_getlow(n), cb);
+        mtbdd_fprintdot_rec(out, mtbddnode_gethigh(n), cb);
 
-        fprintf(out, "%" PRIu64 " -> %" PRIu64 " [style=dashed dir=both arrowtail=%s];\n",
-                mtbdd, mtbdd_regular(mtbddnode_getlow(n)), mtbdd_isnegated(mtbddnode_getlow(n)) ? "dot" : "none");
+        fprintf(out, "%" PRIu64 " -> %" PRIu64 " [style=dashed];\n",
+                MTBDD_STRIPMARK(mtbdd), mtbddnode_getlow(n));
         fprintf(out, "%" PRIu64 " -> %" PRIu64 " [style=solid dir=both arrowtail=%s];\n",
-                mtbdd, mtbdd_regular(mtbddnode_gethigh(n)),
-                mtbdd_isnegated(mtbddnode_gethigh(n)) ? "dot" : "none");
+                MTBDD_STRIPMARK(mtbdd), MTBDD_STRIPMARK(mtbddnode_gethigh(n)),
+                mtbddnode_getcomp(n) ? "dot" : "none");
     }
 }
 
@@ -2600,9 +2401,9 @@ mtbdd_fprintdot(FILE *out, MTBDD mtbdd, print_terminal_label_cb cb)
     fprintf(out, "edge [dir = forward];\n");
     fprintf(out, "root [style=invis];\n");
     fprintf(out, "root -> %" PRIu64 " [style=solid dir=both arrowtail=%s];\n",
-            mtbdd_regular(mtbdd), mtbdd_isnegated(mtbdd) ? "dot" : "none");
+            MTBDD_STRIPMARK(mtbdd), MTBDD_HASMARK(mtbdd) ? "dot" : "none");
 
-    mtbdd_fprintdot_rec(out, mtbdd_regular(mtbdd), cb);
+    mtbdd_fprintdot_rec(out, mtbdd, cb);
     mtbdd_unmark_rec(mtbdd);
 
     fprintf(out, "}\n");
@@ -2739,3 +2540,4 @@ mtbdd_map_removeall(MTBDDMAP map, MTBDD variables)
 }
 
 #include "sylvan_mtbdd_storm.c"
+

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

@@ -20,15 +20,12 @@
  *
  * Three domains are supported by default: Boolean, Integer and Real.
  * Boolean MTBDDs are identical to BDDs (as supported by the bdd subpackage).
- * Integer MTBDDs are encoded using "uint64_t" terminals.
+ * Integer MTBDDs are encoded using "int64_t" terminals.
  * Real MTBDDs are encoded using "double" terminals.
- * Negative integers/reals are encoded using the complement edge.
  *
  * Labels of Boolean variables of MTBDD nodes are 24-bit integers.
  *
- * Custom terminals are supported. For notification when nodes are deleted in gc,
- * set a callback using sylvan_set_ondead and for each custom terminal node, call
- * the function mtbdd_notify_ondead.
+ * Custom terminals are supported.
  *
  * Terminal type "0" is the Integer type, type "1" is the Real type.
  * Type "2" is the Fraction type, consisting of two 32-bit integers (numerator and denominator)
@@ -100,26 +97,26 @@ MTBDD mtbdd_getlow(MTBDD node);
 MTBDD mtbdd_gethigh(MTBDD node);
 
 /**
- * Compute the negation of the MTBDD
- * For Boolean MTBDDs, this means "not X", for integer and reals, this means "-X".
+ * Compute the complement of the MTBDD.
+ * For Boolean MTBDDs, this means "not X".
  */
-#define mtbdd_isnegated(dd) ((dd & mtbdd_complement) ? 1 : 0)
-#define mtbdd_negate(dd) (dd ^ mtbdd_complement)
+#define mtbdd_hascomp(dd) ((dd & mtbdd_complement) ? 1 : 0)
+#define mtbdd_comp(dd) (dd ^ mtbdd_complement)
 #define mtbdd_not(dd) (dd ^ mtbdd_complement)
 
 /**
- * Create terminals representing uint64_t (type 0), double (type 1), or fraction (type 2) values
+ * Create terminals representing int64_t (type 0), double (type 1), or fraction (type 2) values
  */
-MTBDD mtbdd_uint64(uint64_t value);
+MTBDD mtbdd_int64(int64_t value);
 MTBDD mtbdd_double(double value);
-MTBDD mtbdd_fraction(uint64_t numer, uint64_t denom);
+MTBDD mtbdd_fraction(int64_t numer, uint64_t denom);
 
 /**
- * Get the value of a terminal (for Integer and Real terminals, types 0 and 1)
+ * Get the value of a terminal (for Integer, Real and Fraction terminals, types 0, 1 and 2)
  */
-#define mtbdd_getuint64(terminal) mtbdd_getvalue(terminal)
+int64_t mtbdd_getint64(MTBDD terminal);
 double mtbdd_getdouble(MTBDD terminal);
-#define mtbdd_getnumer(terminal) ((uint32_t)(mtbdd_getvalue(terminal)>>32))
+#define mtbdd_getnumer(terminal) ((int32_t)(mtbdd_getvalue(terminal)>>32))
 #define mtbdd_getdenom(terminal) ((uint32_t)(mtbdd_getvalue(terminal)&0xffffffff))
 
 /**
@@ -207,6 +204,12 @@ LACE_TYPEDEF_CB(MTBDD, mtbdd_abstract_op, MTBDD, MTBDD, int);
 TASK_DECL_3(MTBDD, mtbdd_abstract, MTBDD, MTBDD, mtbdd_abstract_op);
 #define mtbdd_abstract(a, v, op) CALL(mtbdd_abstract, a, v, op)
 
+/**
+ * Unary operation Negate.
+ * Supported domains: Integer, Real, Fraction
+ */
+TASK_DECL_2(MTBDD, mtbdd_op_negate, MTBDD, size_t);
+
 /**
  * Binary operation Plus (for MTBDDs of same type)
  * Only for MTBDDs where either all leaves are Boolean, or Integer, or Double.
@@ -215,6 +218,14 @@ TASK_DECL_3(MTBDD, mtbdd_abstract, MTBDD, MTBDD, mtbdd_abstract_op);
 TASK_DECL_2(MTBDD, mtbdd_op_plus, MTBDD*, MTBDD*);
 TASK_DECL_3(MTBDD, mtbdd_abstract_op_plus, MTBDD, MTBDD, int);
 
+/**
+ * Binary operation Minus (for MTBDDs of same type)
+ * Only for MTBDDs where either all leaves are Boolean, or Integer, or Double.
+ * For Integer/Double MTBDDs, mtbdd_false is interpreted as "0" or "0.0".
+ */
+TASK_DECL_2(MTBDD, mtbdd_op_minus, MTBDD*, MTBDD*);
+TASK_DECL_3(MTBDD, mtbdd_abstract_op_minus, MTBDD, MTBDD, int);
+
 /**
  * Binary operation Times (for MTBDDs of same type)
  * Only for MTBDDs where either all leaves are Boolean, or Integer, or Double.
@@ -242,6 +253,11 @@ TASK_DECL_3(MTBDD, mtbdd_abstract_op_min, MTBDD, MTBDD, int);
 TASK_DECL_2(MTBDD, mtbdd_op_max, MTBDD*, MTBDD*);
 TASK_DECL_3(MTBDD, mtbdd_abstract_op_max, MTBDD, MTBDD, int);
 
+/**
+ * Compute -a
+ */
+#define mtbdd_negate(a) mtbdd_uapply(a, TASK(mtbdd_op_negate), 0)
+
 /**
  * Compute a + b
  */
@@ -250,7 +266,7 @@ TASK_DECL_3(MTBDD, mtbdd_abstract_op_max, MTBDD, MTBDD, int);
 /**
  * Compute a - b
  */
-#define mtbdd_minus(a, b) mtbdd_plus(a, mtbdd_negate(b))
+#define mtbdd_minus(a, b) mtbdd_apply(a, b, TASK(mtbdd_op_minus))
 
 /**
  * Compute a * b
@@ -325,13 +341,14 @@ TASK_DECL_2(MTBDD, mtbdd_strict_threshold_double, MTBDD, double);
 
 /**
  * For two Double MTBDDs, calculate whether they are equal module some value epsilon
- * i.e. abs(a-b)<3
+ * i.e. abs(a-b) < e
  */
 TASK_DECL_3(MTBDD, mtbdd_equal_norm_d, MTBDD, MTBDD, double);
 #define mtbdd_equal_norm_d(a, b, epsilon) CALL(mtbdd_equal_norm_d, a, b, epsilon)
 
 /**
  * For two Double MTBDDs, calculate whether they are equal modulo some value epsilon
+ * This version computes the relative difference vs the value in a.
  * i.e. abs((a-b)/a) < e
  */
 TASK_DECL_3(MTBDD, mtbdd_equal_norm_rel_d, MTBDD, MTBDD, double);

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

@@ -18,18 +18,17 @@ TASK_IMPL_2(MTBDD, mtbdd_op_divide, MTBDD*, pa, MTBDD*, pb)
         uint64_t val_a = mtbddnode_getvalue(na);
         uint64_t val_b = mtbddnode_getvalue(nb);
         if (mtbddnode_gettype(na) == 0 && mtbddnode_gettype(nb) == 0) {
-            // both uint64_t
-            if (val_a == 0) return a;
-            else if (val_b == 0) return b;
+            int64_t va = *(int64_t*)(&val_a);
+            int64_t vb = *(int64_t*)(&val_b);
+
+            if (va == 0) return a;
+            else if (vb == 0) return b;
             else {
                 MTBDD result;
-                if (val_a == 1) result = b;
-                else if (val_b == 1) result = a;
-                else result = mtbdd_uint64(val_a*val_b);
-                int nega = mtbdd_isnegated(a);
-                int negb = mtbdd_isnegated(b);
-                if (nega ^ negb) return mtbdd_negate(result);
-                else return result;
+                if (va == 1) result = b;
+                else if (vb == 1) result = a;
+                else result = mtbdd_int64(va*vb);
+                return result;
             }
         } else if (mtbddnode_gettype(na) == 1 && mtbddnode_gettype(nb) == 1) {
             // both double
@@ -40,12 +39,8 @@ TASK_IMPL_2(MTBDD, mtbdd_op_divide, MTBDD*, pa, MTBDD*, pb)
             else {
                 MTBDD result;
                 if (vval_a == 0.0 || vval_b == 1.0) result = a;
-                
-                int nega = mtbdd_isnegated(a);
-                int negb = mtbdd_isnegated(b);
                 result = mtbdd_double(vval_a / vval_b);
-                if (nega ^ negb) return mtbdd_negate(result);
-                else return result;
+                return result;
             }
         }
         else if (mtbddnode_gettype(na) == 2 && mtbddnode_gettype(nb) == 2) {
@@ -62,11 +57,8 @@ TASK_IMPL_2(MTBDD, mtbdd_op_divide, MTBDD*, pa, MTBDD*, pb)
             nom_a *= (denom_b/c);
             denom_a *= (nom_b/d);
             // compute result
-            int nega = mtbdd_isnegated(a);
-            int negb = mtbdd_isnegated(b);
             MTBDD result = mtbdd_fraction(nom_a, denom_a);
-            if (nega ^ negb) return mtbdd_negate(result);
-            else return result;
+            return result;
         }
     }
     
@@ -92,18 +84,15 @@ TASK_IMPL_2(MTBDD, mtbdd_op_equals, MTBDD*, pa, MTBDD*, pb)
         uint64_t val_a = mtbddnode_getvalue(na);
         uint64_t val_b = mtbddnode_getvalue(nb);
         if (mtbddnode_gettype(na) == 0 && mtbddnode_gettype(nb) == 0) {
-            // both uint64_t
-            int nega = mtbdd_isnegated(a);
-            int negb = mtbdd_isnegated(b);
-            if (val_a == val_b && !(nega ^ negb)) return mtbdd_true;
+            int64_t va = *(int64_t*)(&val_a);
+            int64_t vb = *(int64_t*)(&val_b);
+            if (va == vb) return mtbdd_true;
             return mtbdd_false;
         } else if (mtbddnode_gettype(na) == 1 && mtbddnode_gettype(nb) == 1) {
             // both double
             double vval_a = *(double*)&val_a;
             double vval_b = *(double*)&val_b;
-            int nega = mtbdd_isnegated(a);
-            int negb = mtbdd_isnegated(b);
-            if (vval_a == vval_b && !(nega ^ negb)) return mtbdd_true;
+            if (vval_a == vval_b) return mtbdd_true;
             return mtbdd_false;
         } else if (mtbddnode_gettype(na) == 2 && mtbddnode_gettype(nb) == 2) {
             // both fraction
@@ -111,9 +100,7 @@ TASK_IMPL_2(MTBDD, mtbdd_op_equals, MTBDD*, pa, MTBDD*, pb)
             uint64_t nom_b = val_b>>32;
             uint64_t denom_a = val_a&0xffffffff;
             uint64_t denom_b = val_b&0xffffffff;
-            int nega = mtbdd_isnegated(a);
-            int negb = mtbdd_isnegated(b);
-            if (nom_a == nom_b && denom_a == denom_b && !(nega ^ negb)) return mtbdd_true;
+            if (nom_a == nom_b && denom_a == denom_b) return mtbdd_true;
             return mtbdd_false;
         }
     }
@@ -145,21 +132,14 @@ TASK_IMPL_2(MTBDD, mtbdd_op_less, MTBDD*, pa, MTBDD*, pb)
         uint64_t val_a = mtbddnode_getvalue(na);
         uint64_t val_b = mtbddnode_getvalue(nb);
         if (mtbddnode_gettype(na) == 0 && mtbddnode_gettype(nb) == 0) {
-            // both uint64_t
-            int nega = mtbdd_isnegated(a);
-            int negb = mtbdd_isnegated(b);
-            if (nega && !negb) return mtbdd_true;
-            if (!nega && negb) return mtbdd_false;
-            if (nega && negb && val_a < val_b) return mtbdd_false;
-            return mtbdd_true;
+            int64_t va = *(int64_t*)(&val_a);
+            int64_t vb = *(int64_t*)(&val_b);
+            if (va < vb) return mtbdd_true;
+            return mtbdd_false;
         } else if (mtbddnode_gettype(na) == 1 && mtbddnode_gettype(nb) == 1) {
             // both double
             double vval_a = *(double*)&val_a;
             double vval_b = *(double*)&val_b;
-            int nega = mtbdd_isnegated(a);
-            if (nega) vval_a = -vval_a;
-            int negb = mtbdd_isnegated(b);
-            if (negb) vval_b = -vval_b;
             if (vval_a < vval_b) return mtbdd_true;
             return mtbdd_false;
         } else if (mtbddnode_gettype(na) == 2 && mtbddnode_gettype(nb) == 2) {
@@ -168,10 +148,6 @@ TASK_IMPL_2(MTBDD, mtbdd_op_less, MTBDD*, pa, MTBDD*, pb)
             uint64_t nom_b = val_b>>32;
             uint64_t denom_a = val_a&0xffffffff;
             uint64_t denom_b = val_b&0xffffffff;
-            int nega = mtbdd_isnegated(a);
-            int negb = mtbdd_isnegated(b);
-            if (nega && !negb) return mtbdd_true;
-            if (!nega && negb) return mtbdd_false;
             return nom_a * denom_b < nom_b * denom_a ? mtbdd_true : mtbdd_false;
         }
     }
@@ -198,31 +174,13 @@ TASK_IMPL_2(MTBDD, mtbdd_op_less_or_equal, MTBDD*, pa, MTBDD*, pb)
         uint64_t val_a = mtbddnode_getvalue(na);
         uint64_t val_b = mtbddnode_getvalue(nb);
         if (mtbddnode_gettype(na) == 0 && mtbddnode_gettype(nb) == 0) {
-            // both uint64_t
-            int nega = mtbdd_isnegated(a);
-            int negb = mtbdd_isnegated(b);
-            if (nega && !negb) {
-                if (val_a != 0) return mtbdd_true;
-                if (val_b != 0) return mtbdd_true;
-                return mtbdd_false;
-            }
-            if (!nega && negb) {
-                if (val_b != 0) return mtbdd_false;
-                if (val_a != 0) return mtbdd_false;
-                return mtbdd_true;
-            }
-            if (nega && negb) {
-                return val_a >= val_b ? mtbdd_true : mtbdd_false;
-            }
-            return val_a <= val_b ? mtbdd_true : mtbdd_false;
+            int64_t va = *(int64_t*)(&val_a);
+            int64_t vb = *(int64_t*)(&val_b);
+            return va <= vb ? mtbdd_true : mtbdd_false;
         } else if (mtbddnode_gettype(na) == 1 && mtbddnode_gettype(nb) == 1) {
             // both double
             double vval_a = *(double*)&val_a;
             double vval_b = *(double*)&val_b;
-            int nega = mtbdd_isnegated(a);
-            if (nega) vval_a = -vval_a;
-            int negb = mtbdd_isnegated(b);
-            if (negb) vval_b = -vval_b;
             if (vval_a <= vval_b) return mtbdd_true;
             return mtbdd_false;
         } else if (mtbddnode_gettype(na) == 2 && mtbddnode_gettype(nb) == 2) {
@@ -231,24 +189,9 @@ TASK_IMPL_2(MTBDD, mtbdd_op_less_or_equal, MTBDD*, pa, MTBDD*, pb)
             uint64_t nom_b = val_b>>32;
             uint64_t denom_a = val_a&0xffffffff;
             uint64_t denom_b = val_b&0xffffffff;
-            int nega = mtbdd_isnegated(a);
-            int negb = mtbdd_isnegated(b);
             nom_a *= denom_b;
             nom_b *= denom_a;
-            if (nega && !negb) {
-                if (nom_a != 0) return mtbdd_true;
-                if (nom_b != 0) return mtbdd_true;
-                return mtbdd_false;
-            }
-            if (!nega && negb) {
-                if (nom_a != 0) return mtbdd_false;
-                if (nom_b != 0) return mtbdd_false;
-                return mtbdd_true;
-            }
-            if (nega && negb) {
-                return nom_a >= nom_b ? mtbdd_true : mtbdd_false;
-            }
-            return val_a <= val_b ? mtbdd_true : mtbdd_false;
+            return nom_a <= nom_b ? mtbdd_true : mtbdd_false;
         }
     }
     
@@ -277,10 +220,6 @@ TASK_IMPL_2(MTBDD, mtbdd_op_pow, MTBDD*, pa, MTBDD*, pb)
             // both double
             double vval_a = *(double*)&val_a;
             double vval_b = *(double*)&val_b;
-            int nega = mtbdd_isnegated(a);
-            if (nega) vval_a = -vval_a;
-            int negb = mtbdd_isnegated(b);
-            if (negb) vval_b = -vval_b;
             return mtbdd_double(pow(vval_a, vval_b));
         } else if (mtbddnode_gettype(na) == 2 && mtbddnode_gettype(nb) == 2) {
             assert(0);
@@ -312,10 +251,6 @@ TASK_IMPL_2(MTBDD, mtbdd_op_mod, MTBDD*, pa, MTBDD*, pb)
             // both double
             double vval_a = *(double*)&val_a;
             double vval_b = *(double*)&val_b;
-            int nega = mtbdd_isnegated(a);
-            if (nega) vval_a = -vval_a;
-            int negb = mtbdd_isnegated(b);
-            if (negb) vval_b = -vval_b;
             return mtbdd_double(fmod(vval_a, vval_b));
         } else if (mtbddnode_gettype(na) == 2 && mtbddnode_gettype(nb) == 2) {
             assert(0);
@@ -347,10 +282,6 @@ TASK_IMPL_2(MTBDD, mtbdd_op_logxy, MTBDD*, pa, MTBDD*, pb)
             // both double
             double vval_a = *(double*)&val_a;
             double vval_b = *(double*)&val_b;
-            int nega = mtbdd_isnegated(a);
-            if (nega) vval_a = -vval_a;
-            int negb = mtbdd_isnegated(b);
-            if (negb) vval_b = -vval_b;
             return mtbdd_double(log(vval_a) / log(vval_b));
         } else if (mtbddnode_gettype(na) == 2 && mtbddnode_gettype(nb) == 2) {
             assert(0);
@@ -371,7 +302,7 @@ TASK_IMPL_2(MTBDD, mtbdd_op_not_zero, MTBDD, a, size_t, v)
     
     if (mtbddnode_isleaf(na)) {
         if (mtbddnode_gettype(na) == 0) {
-            return mtbdd_getuint64(a) != 0 ? mtbdd_true : mtbdd_false;
+            return mtbdd_getint64(a) != 0 ? mtbdd_true : mtbdd_false;
         } else if (mtbddnode_gettype(na) == 1) {
             return mtbdd_getdouble(a) != 0.0 ? mtbdd_true : mtbdd_false;
         } else if (mtbddnode_gettype(na) == 2) {
@@ -404,10 +335,10 @@ TASK_IMPL_2(MTBDD, mtbdd_op_floor, MTBDD, a, size_t, v)
             return a;
         } else if (mtbddnode_gettype(na) == 1) {
             MTBDD result = mtbdd_double(floor(mtbdd_getdouble(a)));
-            return mtbdd_isnegated(a) ? mtbdd_negate(result) : result;
+            return result;
         } else if (mtbddnode_gettype(na) == 2) {
             MTBDD result = mtbdd_fraction(mtbdd_getnumer(a) / mtbdd_getdenom(a), 1);
-            return mtbdd_isnegated(a) ? mtbdd_negate(result) : result;
+            return result;
         }
     }
     
@@ -436,10 +367,10 @@ TASK_IMPL_2(MTBDD, mtbdd_op_ceil, MTBDD, a, size_t, v)
             return a;
         } else if (mtbddnode_gettype(na) == 1) {
             MTBDD result = mtbdd_double(ceil(mtbdd_getdouble(a)));
-            return mtbdd_isnegated(a) ? mtbdd_negate(result) : result;
+            return result;
         } else if (mtbddnode_gettype(na) == 2) {
             MTBDD result = mtbdd_fraction(mtbdd_getnumer(a) / mtbdd_getdenom(a) + 1, 1);
-            return mtbdd_isnegated(a) ? mtbdd_negate(result) : result;
+            return result;
         }
     }
 
@@ -471,11 +402,11 @@ TASK_IMPL_1(MTBDD, mtbdd_bool_to_double, MTBDD, dd)
     return mtbdd_uapply(dd, TASK(mtbdd_op_bool_to_double), 0);
 }
 
-TASK_IMPL_2(MTBDD, mtbdd_op_bool_to_uint64, MTBDD, a, size_t, v)
+TASK_IMPL_2(MTBDD, mtbdd_op_bool_to_int64, MTBDD, a, size_t, v)
 {
     /* We only expect "double" terminals, or false */
-    if (a == mtbdd_false) return mtbdd_uint64(0);
-    if (a == mtbdd_true) return mtbdd_uint64(1);
+    if (a == mtbdd_false) return mtbdd_int64(0);
+    if (a == mtbdd_true) return mtbdd_int64(1);
     
     // Ugly hack to get rid of the error "unused variable v" (because there is no version of uapply without a parameter).
     (void)v;
@@ -483,9 +414,9 @@ TASK_IMPL_2(MTBDD, mtbdd_op_bool_to_uint64, MTBDD, a, size_t, v)
     return mtbdd_invalid;
 }
 
-TASK_IMPL_1(MTBDD, mtbdd_bool_to_uint64, MTBDD, dd)
+TASK_IMPL_1(MTBDD, mtbdd_bool_to_int64, MTBDD, dd)
 {
-    return mtbdd_uapply(dd, TASK(mtbdd_op_bool_to_uint64), 0);
+    return mtbdd_uapply(dd, TASK(mtbdd_op_bool_to_int64), 0);
 }
 
 /**
@@ -500,7 +431,7 @@ TASK_IMPL_2(double, mtbdd_non_zero_count, MTBDD, dd, size_t, nvars)
     
     if (mtbdd_isleaf(dd)) {
         if (mtbddnode_gettype(na) == 0) {
-            return mtbdd_getuint64(dd) != 0 ? powl(2.0L, nvars) : 0.0;
+            return mtbdd_getint64(dd) != 0 ? powl(2.0L, nvars) : 0.0;
         } else if (mtbddnode_gettype(na) == 1) {
             return mtbdd_getdouble(dd) != 0 ? powl(2.0L, nvars) : 0.0;
         } else if (mtbddnode_gettype(na) == 2) {
@@ -532,7 +463,7 @@ TASK_IMPL_2(double, mtbdd_non_zero_count, MTBDD, dd, size_t, nvars)
 
 int mtbdd_iszero(MTBDD dd) {
     if (mtbdd_gettype(dd) == 0) {
-        return mtbdd_getuint64(dd) == 0;
+        return mtbdd_getint64(dd) == 0;
     } else if (mtbdd_gettype(dd) == 1) {
         return mtbdd_getdouble(dd) == 0;
     } else if (mtbdd_gettype(dd) == 2) {

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

@@ -92,9 +92,9 @@ TASK_DECL_1(MTBDD, mtbdd_bool_to_double, MTBDD)
 /**
  * Monad that converts Boolean to a uint MTBDD, translate terminals true to 1 and to 0 otherwise;
  */
-TASK_DECL_2(MTBDD, mtbdd_op_bool_to_uint64, MTBDD, size_t)
-TASK_DECL_1(MTBDD, mtbdd_bool_to_uint64, MTBDD)
-#define mtbdd_bool_to_uint64(dd) CALL(mtbdd_bool_to_uint64, dd)
+TASK_DECL_2(MTBDD, mtbdd_op_bool_to_int64, MTBDD, size_t)
+TASK_DECL_1(MTBDD, mtbdd_bool_to_int64, MTBDD)
+#define mtbdd_bool_to_int64(dd) CALL(mtbdd_bool_to_int64, dd)
 
 /**
  * Count the number of assignments (minterms) leading to a non-zero

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

@@ -593,9 +593,9 @@ BddMap::isEmpty() const
  */
 
 Mtbdd
-Mtbdd::uint64Terminal(uint64_t value)
+Mtbdd::int64Terminal(int64_t value)
 {
-    return mtbdd_uint64(value);
+    return mtbdd_int64(value);
 }
 
 Mtbdd
@@ -605,7 +605,7 @@ Mtbdd::doubleTerminal(double value)
 }
 
 Mtbdd
-Mtbdd::fractionTerminal(uint64_t nominator, uint64_t denominator)
+Mtbdd::fractionTerminal(int64_t nominator, uint64_t denominator)
 {
     return mtbdd_fraction(nominator, denominator);
 }
@@ -694,6 +694,7 @@ Mtbdd::Else() const
 Mtbdd
 Mtbdd::Negate() const
 {
+    LACE_ME;
     return mtbdd_negate(mtbdd);
 }
 
@@ -853,14 +854,14 @@ Mtbdd
 Mtbdd::operator-(const Mtbdd& other) const
 {
     LACE_ME;
-    return mtbdd_plus(mtbdd, mtbdd_negate(other.mtbdd));
+    return mtbdd_minus(mtbdd, other.mtbdd);
 }
 
 Mtbdd
 Mtbdd::operator-=(const Mtbdd& other)
 {
     LACE_ME;
-    mtbdd = mtbdd_plus(mtbdd, mtbdd_negate(other.mtbdd));
+    mtbdd = mtbdd_minus(mtbdd, other.mtbdd);
     return *this;
 }
 
@@ -1035,11 +1036,5 @@ Sylvan::quitPackage()
     sylvan_quit();
 }
 
-void
-Sylvan::triggerGarbageCollection() {
-//    LACE_ME;
-//    sylvan_gc();
-}
-
-
 #include "sylvan_obj_storm.cpp"
+

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

@@ -28,7 +28,7 @@ namespace sylvan {
 class BddSet;
 class BddMap;
 class Mtbdd;
-
+    
 class Bdd {
     friend class Sylvan;
     friend class BddSet;
@@ -429,6 +429,7 @@ public:
         for (size_t i = 0; i < length; i++) {
             set.add(arr[length-i-1]);
         }
+        return set;
     }
 
     /**
@@ -532,9 +533,9 @@ public:
     ~Mtbdd() { mtbdd_unprotect(&mtbdd); }
 
     /**
-     * @brief Creates a Mtbdd leaf representing the uint64 value <value>
+     * @brief Creates a Mtbdd leaf representing the int64 value <value>
      */
-    static Mtbdd uint64Terminal(uint64_t value);
+    static Mtbdd int64Terminal(int64_t value);
 
     /**
      * @brief Creates a Mtbdd leaf representing the floating-point value <value>
@@ -545,7 +546,7 @@ public:
      * @brief Creates a Mtbdd leaf representing the fraction value <nominator>/<denominator>
      * Internally, Sylvan uses 32-bit values and reports overflows to stderr.
      */
-    static Mtbdd fractionTerminal(uint64_t nominator, uint64_t denominator);
+    static Mtbdd fractionTerminal(int64_t nominator, uint64_t denominator);
 
     /**
      * @brief Creates a Mtbdd leaf of type <type> holding value <value>
@@ -643,8 +644,8 @@ public:
     Mtbdd Else() const;
 
     /**
-     * @brief Returns the negation of the MTBDD
-     * For Boolean, this means "not", for floating-point and fractions, this means "negative"
+     * @brief Returns the negation of the MTBDD (every terminal negative)
+     * Do not use this for Boolean MTBDDs, only for Integer/Double/Fraction MTBDDs.
      */
     Mtbdd Negate() const;
 
@@ -773,9 +774,9 @@ public:
      * @brief Gets the number of nodes in this Bdd. Not thread-safe!
      */
     size_t NodeCount() const;
-    
-#include "sylvan_obj_mtbdd_storm.hpp"
 
+#include "sylvan_obj_mtbdd_storm.hpp"
+    
 private:
     MTBDD mtbdd;
 };
@@ -847,8 +848,6 @@ public:
      * Warning: if you have any Bdd objects which are not bddZero() or bddOne() after this, your program may crash!
      */
     static void quitPackage();
-    
-    static void triggerGarbageCollection();
 };
 
 }

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

@@ -1,2 +1,2 @@
     Mtbdd toDoubleMtbdd() const;
-    Mtbdd toUint64Mtbdd() const;
+    Mtbdd toInt64Mtbdd() const;

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

@@ -5,9 +5,9 @@ Bdd::toDoubleMtbdd() const {
 }
 
 Mtbdd
-Bdd::toUint64Mtbdd() const {
+Bdd::toInt64Mtbdd() const {
     LACE_ME;
-    return mtbdd_bool_to_uint64(bdd);
+    return mtbdd_bool_to_int64(bdd);
 }
 
 Mtbdd

src/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp

@@ -199,7 +199,7 @@ namespace storm {
                 if (qualitative) {
                     // Set the values for all maybe-states to 1 to indicate that their reward values
                     // are neither 0 nor infinity.
-                    return std::unique_ptr<CheckResult>(new SymbolicQuantitativeCheckResult<DdType>(model.getReachableStates(), infinityStates.template toAdd<ValueType>() * model.getManager().getConstant(storm::utility::infinity<ValueType>()) + maybeStates.template toAdd<ValueType>() * model.getManager().getConstant(storm::utility::one<ValueType>())));
+                    return std::unique_ptr<CheckResult>(new SymbolicQuantitativeCheckResult<DdType>(model.getReachableStates(), infinityStates.template toAdd<ValueType>().ite(model.getManager().getConstant(storm::utility::infinity<ValueType>()), model.getManager().template getAddZero<ValueType>()) + maybeStates.template toAdd<ValueType>() * model.getManager().template getAddOne<ValueType>()));
                 } else {
                     // If there are maybe states, we need to solve an equation system.
                     if (!maybeStates.isZero()) {
@@ -233,9 +233,9 @@ namespace storm {
                         solver->solveEquationSystem(x, b);
                         
                         // Return a hybrid check result that stores the numerical values explicitly.
-                        return std::unique_ptr<CheckResult>(new storm::modelchecker::HybridQuantitativeCheckResult<DdType>(model.getReachableStates(), model.getReachableStates() && !maybeStates, infinityStates.template toAdd<ValueType>() * model.getManager().getConstant(storm::utility::infinity<ValueType>()), maybeStates, odd, x));
+                        return std::unique_ptr<CheckResult>(new storm::modelchecker::HybridQuantitativeCheckResult<DdType>(model.getReachableStates(), model.getReachableStates() && !maybeStates, infinityStates.template toAdd<ValueType>().ite(model.getManager().getConstant(storm::utility::infinity<ValueType>()), model.getManager().template getAddZero<ValueType>()), maybeStates, odd, x));
                     } else {
-                        return std::unique_ptr<CheckResult>(new storm::modelchecker::SymbolicQuantitativeCheckResult<DdType>(model.getReachableStates(), infinityStates.template toAdd<ValueType>() * model.getManager().getConstant(storm::utility::infinity<ValueType>())));
+                        return std::unique_ptr<CheckResult>(new storm::modelchecker::SymbolicQuantitativeCheckResult<DdType>(model.getReachableStates(), infinityStates.template toAdd<ValueType>().ite(model.getManager().getConstant(storm::utility::infinity<ValueType>()), model.getManager().template getAddZero<ValueType>())));
                     }
                 }
             }

src/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp

@@ -218,7 +218,7 @@ namespace storm {
                 if (qualitative) {
                     // Set the values for all maybe-states to 1 to indicate that their reward values
                     // are neither 0 nor infinity.
-                    return std::unique_ptr<CheckResult>(new SymbolicQuantitativeCheckResult<DdType>(model.getReachableStates(), infinityStates.template toAdd<ValueType>() * model.getManager().getConstant(storm::utility::infinity<ValueType>()) + maybeStates.template toAdd<ValueType>() * model.getManager().getConstant(storm::utility::one<ValueType>())));
+                    return std::unique_ptr<CheckResult>(new SymbolicQuantitativeCheckResult<DdType>(model.getReachableStates(), infinityStates.template toAdd<ValueType>().ite(model.getManager().getConstant(storm::utility::infinity<ValueType>()), model.getManager().template getAddZero<ValueType>()) + maybeStates.template toAdd<ValueType>() * model.getManager().getConstant(storm::utility::one<ValueType>())));
                 } else {
                     // If there are maybe states, we need to solve an equation system.
                     if (!maybeStates.isZero()) {
@@ -253,9 +253,9 @@ namespace storm {
                         solver->solveEquationSystem(dir, x, explicitRepresentation.second);
                         
                         // Return a hybrid check result that stores the numerical values explicitly.
-                        return std::unique_ptr<CheckResult>(new storm::modelchecker::HybridQuantitativeCheckResult<DdType>(model.getReachableStates(), model.getReachableStates() && !maybeStates, infinityStates.template toAdd<ValueType>() * model.getManager().getConstant(storm::utility::infinity<ValueType>()), maybeStates, odd, x));
+                        return std::unique_ptr<CheckResult>(new storm::modelchecker::HybridQuantitativeCheckResult<DdType>(model.getReachableStates(), model.getReachableStates() && !maybeStates, infinityStates.template toAdd<ValueType>().ite(model.getManager().getConstant(storm::utility::infinity<ValueType>()), model.getManager().template getAddZero<ValueType>()), maybeStates, odd, x));
                     } else {
-                        return std::unique_ptr<CheckResult>(new storm::modelchecker::SymbolicQuantitativeCheckResult<DdType>(model.getReachableStates(), infinityStates.template toAdd<ValueType>() * model.getManager().getConstant(storm::utility::infinity<ValueType>())));
+                        return std::unique_ptr<CheckResult>(new storm::modelchecker::SymbolicQuantitativeCheckResult<DdType>(model.getReachableStates(), infinityStates.template toAdd<ValueType>().ite(model.getManager().getConstant(storm::utility::infinity<ValueType>()), model.getManager().template getAddZero<ValueType>())));
                     }
                 }
             }

src/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp

@@ -147,7 +147,7 @@ namespace storm {
                 if (qualitative) {
                     // Set the values for all maybe-states to 1 to indicate that their reward values
                     // are neither 0 nor infinity.
-                    return infinityStates.template toAdd<ValueType>() * model.getManager().getConstant(storm::utility::infinity<ValueType>()) + maybeStates.template toAdd<ValueType>() * model.getManager().getConstant(storm::utility::one<ValueType>());
+                    return infinityStates.template toAdd<ValueType>().ite(model.getManager().getConstant(storm::utility::infinity<ValueType>()), model.getManager().template getAddZero<ValueType>()) + maybeStates.template toAdd<ValueType>() * model.getManager().getConstant(storm::utility::one<ValueType>());
                 } else {
                     // If there are maybe states, we need to solve an equation system.
                     if (!maybeStates.isZero()) {
@@ -170,9 +170,9 @@ namespace storm {
                         std::unique_ptr<storm::solver::SymbolicLinearEquationSolver<DdType, ValueType>> solver = linearEquationSolverFactory.create(submatrix, maybeStates, model.getRowVariables(), model.getColumnVariables(), model.getRowColumnMetaVariablePairs());
                         storm::dd::Add<DdType, ValueType> result = solver->solveEquationSystem(model.getManager().getConstant(0.5) * maybeStatesAdd, subvector);
                         
-                        return infinityStates.template toAdd<ValueType>() * model.getManager().getConstant(storm::utility::infinity<ValueType>()) + result;
+                        return infinityStates.template toAdd<ValueType>().ite(model.getManager().getConstant(storm::utility::infinity<ValueType>()), result);
                     } else {
-                        return infinityStates.template toAdd<ValueType>() * model.getManager().getConstant(storm::utility::infinity<ValueType>());
+                        return infinityStates.template toAdd<ValueType>().ite(model.getManager().getConstant(storm::utility::infinity<ValueType>()), model.getManager().getConstant(storm::utility::zero<ValueType>()));
                     }
                 }
             }

src/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp

@@ -171,7 +171,7 @@ namespace storm {
                 if (qualitative) {
                     // Set the values for all maybe-states to 1 to indicate that their reward values
                     // are neither 0 nor infinity.
-                    return std::unique_ptr<CheckResult>(new SymbolicQuantitativeCheckResult<DdType>(model.getReachableStates(), infinityStates.template toAdd<ValueType>() * model.getManager().getConstant(storm::utility::infinity<ValueType>()) + maybeStates.template toAdd<ValueType>() * model.getManager().getConstant(storm::utility::one<ValueType>())));
+                    return std::unique_ptr<CheckResult>(new SymbolicQuantitativeCheckResult<DdType>(model.getReachableStates(), infinityStates.template toAdd<ValueType>().ite(model.getManager().getConstant(storm::utility::infinity<ValueType>()), model.getManager().template getAddZero<ValueType>()) + maybeStates.template toAdd<ValueType>() * model.getManager().getConstant(storm::utility::one<ValueType>())));
                 } else {
                     // If there are maybe states, we need to solve an equation system.
                     if (!maybeStates.isZero()) {
@@ -192,9 +192,9 @@ namespace storm {
                         std::unique_ptr<storm::solver::SymbolicMinMaxLinearEquationSolver<DdType, ValueType>> solver = linearEquationSolverFactory.create(submatrix, maybeStates, model.getIllegalMask() && maybeStates, model.getRowVariables(), model.getColumnVariables(), model.getNondeterminismVariables(), model.getRowColumnMetaVariablePairs());
                         storm::dd::Add<DdType, ValueType> result = solver->solveEquationSystem(minimize, model.getManager().template getAddZero<ValueType>(), subvector);
 
-                        return std::unique_ptr<CheckResult>(new storm::modelchecker::SymbolicQuantitativeCheckResult<DdType>(model.getReachableStates(), infinityStates.template toAdd<ValueType>() * model.getManager().getConstant(storm::utility::infinity<ValueType>()) + result));
+                        return std::unique_ptr<CheckResult>(new storm::modelchecker::SymbolicQuantitativeCheckResult<DdType>(model.getReachableStates(), infinityStates.template toAdd<ValueType>().ite(model.getManager().getConstant(storm::utility::infinity<ValueType>()), result)));
                     } else {
-                        return std::unique_ptr<CheckResult>(new storm::modelchecker::SymbolicQuantitativeCheckResult<DdType>(model.getReachableStates(), infinityStates.template toAdd<ValueType>() * model.getManager().getConstant(storm::utility::infinity<ValueType>())));
+                        return std::unique_ptr<CheckResult>(new storm::modelchecker::SymbolicQuantitativeCheckResult<DdType>(model.getReachableStates(), infinityStates.template toAdd<ValueType>().ite(model.getManager().getConstant(storm::utility::infinity<ValueType>()), model.getManager().template getAddZero<ValueType>())));
                     }
                 }
             }

src/solver/SymbolicLinearEquationSolver.cpp

@@ -62,7 +62,7 @@ namespace storm {
                 // Increase iteration count so we can abort if convergence is too slow.
                 ++iterationCount;
             }
-            
+                        
             return xCopy;
         }
         

src/solver/SymbolicMinMaxLinearEquationSolver.cpp

@@ -14,12 +14,12 @@ namespace storm {
     namespace solver {
         
         template<storm::dd::DdType DdType, typename ValueType>
-        SymbolicMinMaxLinearEquationSolver<DdType, ValueType>::SymbolicMinMaxLinearEquationSolver(storm::dd::Add<DdType, ValueType> const& A, storm::dd::Bdd<DdType> const& allRows, storm::dd::Bdd<DdType> const& illegalMask, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::set<storm::expressions::Variable> const& choiceVariables, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs, double precision, uint_fast64_t maximalNumberOfIterations, bool relative) : A(A), allRows(allRows), illegalMaskAdd(illegalMask.template toAdd<ValueType>() * A.getDdManager().getConstant(storm::utility::infinity<ValueType>())), rowMetaVariables(rowMetaVariables), columnMetaVariables(columnMetaVariables), choiceVariables(choiceVariables), rowColumnMetaVariablePairs(rowColumnMetaVariablePairs), precision(precision), maximalNumberOfIterations(maximalNumberOfIterations), relative(relative) {
+        SymbolicMinMaxLinearEquationSolver<DdType, ValueType>::SymbolicMinMaxLinearEquationSolver(storm::dd::Add<DdType, ValueType> const& A, storm::dd::Bdd<DdType> const& allRows, storm::dd::Bdd<DdType> const& illegalMask, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::set<storm::expressions::Variable> const& choiceVariables, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs, double precision, uint_fast64_t maximalNumberOfIterations, bool relative) : A(A), allRows(allRows), illegalMaskAdd(illegalMask.template toAdd<ValueType>().ite(A.getDdManager().getConstant(storm::utility::infinity<ValueType>()), A.getDdManager().template getAddZero<ValueType>())), rowMetaVariables(rowMetaVariables), columnMetaVariables(columnMetaVariables), choiceVariables(choiceVariables), rowColumnMetaVariablePairs(rowColumnMetaVariablePairs), precision(precision), maximalNumberOfIterations(maximalNumberOfIterations), relative(relative) {
             // Intentionally left empty.
         }
         
         template<storm::dd::DdType DdType, typename ValueType>
-        SymbolicMinMaxLinearEquationSolver<DdType, ValueType>::SymbolicMinMaxLinearEquationSolver(storm::dd::Add<DdType, ValueType> const& A, storm::dd::Bdd<DdType> const& allRows, storm::dd::Bdd<DdType> const& illegalMask, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::set<storm::expressions::Variable> const& choiceVariables, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs) : A(A), allRows(allRows), illegalMaskAdd(illegalMask.template toAdd<ValueType>() * A.getDdManager().getConstant(storm::utility::infinity<ValueType>())), rowMetaVariables(rowMetaVariables), columnMetaVariables(columnMetaVariables), choiceVariables(choiceVariables), rowColumnMetaVariablePairs(rowColumnMetaVariablePairs) {
+        SymbolicMinMaxLinearEquationSolver<DdType, ValueType>::SymbolicMinMaxLinearEquationSolver(storm::dd::Add<DdType, ValueType> const& A, storm::dd::Bdd<DdType> const& allRows, storm::dd::Bdd<DdType> const& illegalMask, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::set<storm::expressions::Variable> const& choiceVariables, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs) : A(A), allRows(allRows), illegalMaskAdd(illegalMask.template toAdd<ValueType>().ite(A.getDdManager().getConstant(storm::utility::infinity<ValueType>()), A.getDdManager().template getAddZero<ValueType>())), rowMetaVariables(rowMetaVariables), columnMetaVariables(columnMetaVariables), choiceVariables(choiceVariables), rowColumnMetaVariablePairs(rowColumnMetaVariablePairs) {
             // Get the settings object to customize solving.
             storm::settings::modules::NativeEquationSolverSettings const& settings = storm::settings::nativeEquationSolverSettings();
             

src/storage/dd/sylvan/InternalSylvanAdd.cpp

@@ -355,12 +355,12 @@ namespace storm {
         
         template<typename ValueType>
         void InternalAdd<DdType::Sylvan, ValueType>::composeWithExplicitVector(storm::dd::Odd const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<ValueType>& targetVector, std::function<ValueType (ValueType const&, ValueType const&)> const& function) const {
-            composeWithExplicitVectorRec(mtbdd_regular(this->getSylvanMtbdd().GetMTBDD()), mtbdd_isnegated(this->getSylvanMtbdd().GetMTBDD()), nullptr, 0, ddVariableIndices.size(), 0, odd, ddVariableIndices, targetVector, function);
+            composeWithExplicitVectorRec(mtbdd_regular(this->getSylvanMtbdd().GetMTBDD()), mtbdd_hascomp(this->getSylvanMtbdd().GetMTBDD()), nullptr, 0, ddVariableIndices.size(), 0, odd, ddVariableIndices, targetVector, function);
         }
         
         template<typename ValueType>
         void InternalAdd<DdType::Sylvan, ValueType>::composeWithExplicitVector(storm::dd::Odd const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<uint_fast64_t> const& offsets, std::vector<ValueType>& targetVector, std::function<ValueType (ValueType const&, ValueType const&)> const& function) const {
-            composeWithExplicitVectorRec(mtbdd_regular(this->getSylvanMtbdd().GetMTBDD()), mtbdd_isnegated(this->getSylvanMtbdd().GetMTBDD()), &offsets, 0, ddVariableIndices.size(), 0, odd, ddVariableIndices, targetVector, function);
+            composeWithExplicitVectorRec(mtbdd_regular(this->getSylvanMtbdd().GetMTBDD()), mtbdd_hascomp(this->getSylvanMtbdd().GetMTBDD()), &offsets, 0, ddVariableIndices.size(), 0, odd, ddVariableIndices, targetVector, function);
         }
         
         template<typename ValueType>
@@ -385,8 +385,8 @@ namespace storm {
                 MTBDD elseNode = mtbdd_getlow(dd);
                 
                 // Determine whether we have to evaluate the successors as if they were complemented.
-                bool elseComplemented = mtbdd_isnegated(elseNode) ^ negated;
-                bool thenComplemented = mtbdd_isnegated(thenNode) ^ negated;
+                bool elseComplemented = mtbdd_hascomp(elseNode) ^ negated;
+                bool thenComplemented = mtbdd_hascomp(thenNode) ^ negated;
                 
                 composeWithExplicitVectorRec(mtbdd_regular(elseNode), elseComplemented, offsets, currentLevel + 1, maxLevel, currentOffset, odd.getElseSuccessor(), ddVariableIndices, targetVector, function);
                 composeWithExplicitVectorRec(mtbdd_regular(thenNode), thenComplemented, offsets, currentLevel + 1, maxLevel, currentOffset + odd.getElseOffset(), odd.getThenSuccessor(), ddVariableIndices, targetVector, function);
@@ -396,14 +396,14 @@ namespace storm {
         template<typename ValueType>
         std::vector<InternalAdd<DdType::Sylvan, ValueType>> InternalAdd<DdType::Sylvan, ValueType>::splitIntoGroups(std::vector<uint_fast64_t> const& ddGroupVariableIndices) const {
             std::vector<InternalAdd<DdType::Sylvan, ValueType>> result;
-            splitIntoGroupsRec(mtbdd_regular(this->getSylvanMtbdd().GetMTBDD()), mtbdd_isnegated(this->getSylvanMtbdd().GetMTBDD()), result, ddGroupVariableIndices, 0, ddGroupVariableIndices.size());
+            splitIntoGroupsRec(mtbdd_regular(this->getSylvanMtbdd().GetMTBDD()), mtbdd_hascomp(this->getSylvanMtbdd().GetMTBDD()), result, ddGroupVariableIndices, 0, ddGroupVariableIndices.size());
             return result;
         }
         
         template<typename ValueType>
         std::vector<std::pair<InternalAdd<DdType::Sylvan, ValueType>, InternalAdd<DdType::Sylvan, ValueType>>> InternalAdd<DdType::Sylvan, ValueType>::splitIntoGroups(InternalAdd<DdType::Sylvan, ValueType> vector, std::vector<uint_fast64_t> const& ddGroupVariableIndices) const {
             std::vector<std::pair<InternalAdd<DdType::Sylvan, ValueType>, InternalAdd<DdType::Sylvan, ValueType>>> result;
-            splitIntoGroupsRec(mtbdd_regular(this->getSylvanMtbdd().GetMTBDD()), mtbdd_isnegated(this->getSylvanMtbdd().GetMTBDD()), mtbdd_regular(vector.getSylvanMtbdd().GetMTBDD()), mtbdd_isnegated(vector.getSylvanMtbdd().GetMTBDD()), result, ddGroupVariableIndices, 0, ddGroupVariableIndices.size());
+            splitIntoGroupsRec(mtbdd_regular(this->getSylvanMtbdd().GetMTBDD()), mtbdd_hascomp(this->getSylvanMtbdd().GetMTBDD()), mtbdd_regular(vector.getSylvanMtbdd().GetMTBDD()), mtbdd_hascomp(vector.getSylvanMtbdd().GetMTBDD()), result, ddGroupVariableIndices, 0, ddGroupVariableIndices.size());
             return result;
         }
         
@@ -415,7 +415,7 @@ namespace storm {
             }
             
             if (currentLevel == maxLevel) {
-                groups.push_back(InternalAdd<DdType::Sylvan, ValueType>(ddManager, sylvan::Mtbdd(negated ? mtbdd_negate(dd) : dd)));
+                groups.push_back(InternalAdd<DdType::Sylvan, ValueType>(ddManager, negated ? sylvan::Mtbdd(dd).Negate() : sylvan::Mtbdd(dd)));
             } else if (mtbdd_isleaf(dd) || ddGroupVariableIndices[currentLevel] < mtbdd_getvar(dd)) {
                 splitIntoGroupsRec(dd, negated, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel);
                 splitIntoGroupsRec(dd, negated, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel);
@@ -425,8 +425,8 @@ namespace storm {
                 MTBDD elseDdNode = mtbdd_getlow(dd);
                 
                 // Determine whether we have to evaluate the successors as if they were complemented.
-                bool elseComplemented = mtbdd_isnegated(elseDdNode) ^ negated;
-                bool thenComplemented = mtbdd_isnegated(thenDdNode) ^ negated;
+                bool elseComplemented = mtbdd_hascomp(elseDdNode) ^ negated;
+                bool thenComplemented = mtbdd_hascomp(thenDdNode) ^ negated;
                 
                 splitIntoGroupsRec(mtbdd_regular(elseDdNode), elseComplemented, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel);
                 splitIntoGroupsRec(mtbdd_regular(thenDdNode), thenComplemented, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel);
@@ -441,7 +441,7 @@ namespace storm {
             }
             
             if (currentLevel == maxLevel) {
-                groups.push_back(std::make_pair(InternalAdd<DdType::Sylvan, ValueType>(ddManager, sylvan::Mtbdd(negated1 ? mtbdd_negate(dd1) : dd1 )), InternalAdd<DdType::Sylvan, ValueType>(ddManager, sylvan::Mtbdd(negated2 ? mtbdd_negate(dd2) : dd2))));
+                groups.push_back(std::make_pair(InternalAdd<DdType::Sylvan, ValueType>(ddManager, negated1 ? sylvan::Mtbdd(dd1).Negate() : sylvan::Mtbdd(dd1)), InternalAdd<DdType::Sylvan, ValueType>(ddManager, negated2 ? sylvan::Mtbdd(dd2).Negate() : sylvan::Mtbdd(dd2))));
             } else if (mtbdd_isleaf(dd1) || ddGroupVariableIndices[currentLevel] < mtbdd_getvar(dd1)) {
                 if (mtbdd_isleaf(dd2) || ddGroupVariableIndices[currentLevel] < mtbdd_getvar(dd2)) {
                     splitIntoGroupsRec(dd1, negated1, dd2, negated2, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel);
@@ -451,8 +451,8 @@ namespace storm {
                     MTBDD dd2ElseNode = mtbdd_getlow(dd2);
                     
                     // Determine whether we have to evaluate the successors as if they were complemented.
-                    bool elseComplemented = mtbdd_isnegated(dd2ElseNode) ^ negated2;
-                    bool thenComplemented = mtbdd_isnegated(dd2ThenNode) ^ negated2;
+                    bool elseComplemented = mtbdd_hascomp(dd2ElseNode) ^ negated2;
+                    bool thenComplemented = mtbdd_hascomp(dd2ThenNode) ^ negated2;
                     
                     splitIntoGroupsRec(dd1, negated1, mtbdd_regular(dd2ThenNode), thenComplemented, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel);
                     splitIntoGroupsRec(dd1, negated1, mtbdd_regular(dd2ElseNode), elseComplemented, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel);
@@ -462,8 +462,8 @@ namespace storm {
                 MTBDD dd1ElseNode = mtbdd_getlow(dd1);
                 
                 // Determine whether we have to evaluate the successors as if they were complemented.
-                bool elseComplemented = mtbdd_isnegated(dd1ElseNode) ^ negated1;
-                bool thenComplemented = mtbdd_isnegated(dd1ThenNode) ^ negated1;
+                bool elseComplemented = mtbdd_hascomp(dd1ElseNode) ^ negated1;
+                bool thenComplemented = mtbdd_hascomp(dd1ThenNode) ^ negated1;
 
                 splitIntoGroupsRec(mtbdd_regular(dd1ThenNode), thenComplemented, dd2, negated2, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel);
                 splitIntoGroupsRec(mtbdd_regular(dd1ElseNode), elseComplemented, dd2, negated2, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel);
@@ -474,10 +474,10 @@ namespace storm {
                 MTBDD dd2ElseNode = mtbdd_getlow(dd2);
                 
                 // Determine whether we have to evaluate the successors as if they were complemented.
-                bool dd1ElseComplemented = mtbdd_isnegated(dd1ElseNode) ^ negated1;
-                bool dd1ThenComplemented = mtbdd_isnegated(dd1ThenNode) ^ negated1;
-                bool dd2ElseComplemented = mtbdd_isnegated(dd2ElseNode) ^ negated2;
-                bool dd2ThenComplemented = mtbdd_isnegated(dd2ThenNode) ^ negated2;
+                bool dd1ElseComplemented = mtbdd_hascomp(dd1ElseNode) ^ negated1;
+                bool dd1ThenComplemented = mtbdd_hascomp(dd1ThenNode) ^ negated1;
+                bool dd2ElseComplemented = mtbdd_hascomp(dd2ElseNode) ^ negated2;
+                bool dd2ThenComplemented = mtbdd_hascomp(dd2ThenNode) ^ negated2;
                 
                 splitIntoGroupsRec(mtbdd_regular(dd1ThenNode), dd1ThenComplemented, mtbdd_regular(dd2ThenNode), dd2ThenComplemented, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel);
                 splitIntoGroupsRec(mtbdd_regular(dd1ElseNode), dd1ElseComplemented, mtbdd_regular(dd2ElseNode), dd2ElseComplemented, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel);
@@ -486,7 +486,7 @@ namespace storm {
         
         template<typename ValueType>
         void InternalAdd<DdType::Sylvan, ValueType>::toMatrixComponents(std::vector<uint_fast64_t> const& rowGroupIndices, std::vector<uint_fast64_t>& rowIndications, std::vector<storm::storage::MatrixEntry<uint_fast64_t, ValueType>>& columnsAndValues, Odd const& rowOdd, Odd const& columnOdd, std::vector<uint_fast64_t> const& ddRowVariableIndices, std::vector<uint_fast64_t> const& ddColumnVariableIndices, bool writeValues) const {
-            return toMatrixComponentsRec(mtbdd_regular(this->getSylvanMtbdd().GetMTBDD()), mtbdd_isnegated(this->getSylvanMtbdd().GetMTBDD()), rowGroupIndices, rowIndications, columnsAndValues, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices, writeValues);
+            return toMatrixComponentsRec(mtbdd_regular(this->getSylvanMtbdd().GetMTBDD()), mtbdd_hascomp(this->getSylvanMtbdd().GetMTBDD()), rowGroupIndices, rowIndications, columnsAndValues, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices, writeValues);
         }
         
         template<typename ValueType>
@@ -532,13 +532,13 @@ namespace storm {
                 }
                 
                 // Visit else-else.
-                toMatrixComponentsRec(mtbdd_regular(elseElse), mtbdd_isnegated(elseElse) ^ negated, rowGroupOffsets, rowIndications, columnsAndValues, rowOdd.getElseSuccessor(), columnOdd.getElseSuccessor(), currentRowLevel + 1, currentColumnLevel + 1, maxLevel, currentRowOffset, currentColumnOffset, ddRowVariableIndices, ddColumnVariableIndices, generateValues);
+                toMatrixComponentsRec(mtbdd_regular(elseElse), mtbdd_hascomp(elseElse) ^ negated, rowGroupOffsets, rowIndications, columnsAndValues, rowOdd.getElseSuccessor(), columnOdd.getElseSuccessor(), currentRowLevel + 1, currentColumnLevel + 1, maxLevel, currentRowOffset, currentColumnOffset, ddRowVariableIndices, ddColumnVariableIndices, generateValues);
                 // Visit else-then.
-                toMatrixComponentsRec(mtbdd_regular(elseThen), mtbdd_isnegated(elseThen) ^ negated, rowGroupOffsets, rowIndications, columnsAndValues, rowOdd.getElseSuccessor(), columnOdd.getThenSuccessor(), currentRowLevel + 1, currentColumnLevel + 1, maxLevel, currentRowOffset, currentColumnOffset + columnOdd.getElseOffset(), ddRowVariableIndices, ddColumnVariableIndices, generateValues);
+                toMatrixComponentsRec(mtbdd_regular(elseThen), mtbdd_hascomp(elseThen) ^ negated, rowGroupOffsets, rowIndications, columnsAndValues, rowOdd.getElseSuccessor(), columnOdd.getThenSuccessor(), currentRowLevel + 1, currentColumnLevel + 1, maxLevel, currentRowOffset, currentColumnOffset + columnOdd.getElseOffset(), ddRowVariableIndices, ddColumnVariableIndices, generateValues);
                 // Visit then-else.
-                toMatrixComponentsRec(mtbdd_regular(thenElse), mtbdd_isnegated(thenElse) ^ negated, rowGroupOffsets, rowIndications, columnsAndValues, rowOdd.getThenSuccessor(), columnOdd.getElseSuccessor(), currentRowLevel + 1, currentColumnLevel + 1, maxLevel, currentRowOffset + rowOdd.getElseOffset(), currentColumnOffset, ddRowVariableIndices, ddColumnVariableIndices, generateValues);
+                toMatrixComponentsRec(mtbdd_regular(thenElse), mtbdd_hascomp(thenElse) ^ negated, rowGroupOffsets, rowIndications, columnsAndValues, rowOdd.getThenSuccessor(), columnOdd.getElseSuccessor(), currentRowLevel + 1, currentColumnLevel + 1, maxLevel, currentRowOffset + rowOdd.getElseOffset(), currentColumnOffset, ddRowVariableIndices, ddColumnVariableIndices, generateValues);
                 // Visit then-then.
-                toMatrixComponentsRec(mtbdd_regular(thenThen), mtbdd_isnegated(thenThen) ^ negated, rowGroupOffsets, rowIndications, columnsAndValues, rowOdd.getThenSuccessor(), columnOdd.getThenSuccessor(), currentRowLevel + 1, currentColumnLevel + 1, maxLevel, currentRowOffset + rowOdd.getElseOffset(), currentColumnOffset + columnOdd.getElseOffset(), ddRowVariableIndices, ddColumnVariableIndices, generateValues);
+                toMatrixComponentsRec(mtbdd_regular(thenThen), mtbdd_hascomp(thenThen) ^ negated, rowGroupOffsets, rowIndications, columnsAndValues, rowOdd.getThenSuccessor(), columnOdd.getThenSuccessor(), currentRowLevel + 1, currentColumnLevel + 1, maxLevel, currentRowOffset + rowOdd.getElseOffset(), currentColumnOffset + columnOdd.getElseOffset(), ddRowVariableIndices, ddColumnVariableIndices, generateValues);
             }
         }
         
@@ -603,14 +603,14 @@ namespace storm {
         
         template<typename ValueType>
         MTBDD InternalAdd<DdType::Sylvan, ValueType>::getLeaf(uint_fast64_t value) {
-            return mtbdd_uint64(value);
+            return mtbdd_int64(value);
         }
         
         template<typename ValueType>
         ValueType InternalAdd<DdType::Sylvan, ValueType>::getValue(MTBDD const& node) {
             STORM_LOG_ASSERT(mtbdd_isleaf(node), "Expected leaf, but got variable " << mtbdd_getvar(node) << ".");
             
-            bool negated = mtbdd_isnegated(node);
+            bool negated = mtbdd_hascomp(node);
             MTBDD n = mtbdd_regular(node);
             
             if (std::is_same<ValueType, double>::value) {
@@ -618,7 +618,7 @@ namespace storm {
                 return negated ? -mtbdd_getdouble(n) : mtbdd_getdouble(n);
             } else if (std::is_same<ValueType, uint_fast64_t>::value) {
                 STORM_LOG_ASSERT(mtbdd_gettype(node) == 0, "Expected an unsigned value.");
-                return negated ? -mtbdd_getuint64(node) : mtbdd_getuint64(node);
+                return negated ? -mtbdd_getint64(node) : mtbdd_getint64(node);
             } else {
                 STORM_LOG_ASSERT(false, "Illegal or unknown type in MTBDD.");
             }

src/storage/dd/sylvan/InternalSylvanBdd.cpp

@@ -231,7 +231,7 @@ namespace storm {
             if (std::is_same<ValueType, double>::value) {
                 return InternalAdd<DdType::Sylvan, ValueType>(ddManager, this->sylvanBdd.toDoubleMtbdd());
             } else if (std::is_same<ValueType, uint_fast64_t>::value) {
-                return InternalAdd<DdType::Sylvan, ValueType>(ddManager, this->sylvanBdd.toUint64Mtbdd());
+                return InternalAdd<DdType::Sylvan, ValueType>(ddManager, this->sylvanBdd.toInt64Mtbdd());
             } else {
                 STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Illegal ADD type.");
             }

src/storage/dd/sylvan/InternalSylvanDdManager.cpp

@@ -52,7 +52,7 @@ namespace storm {
 
         template<>
         InternalAdd<DdType::Sylvan, uint_fast64_t> InternalDdManager<DdType::Sylvan>::getAddOne() const {
-            return InternalAdd<DdType::Sylvan, uint_fast64_t>(this, sylvan::Mtbdd::uint64Terminal(storm::utility::one<uint_fast64_t>()));
+            return InternalAdd<DdType::Sylvan, uint_fast64_t>(this, sylvan::Mtbdd::int64Terminal(storm::utility::one<uint_fast64_t>()));
         }
         
         InternalBdd<DdType::Sylvan> InternalDdManager<DdType::Sylvan>::getBddZero() const {
@@ -66,7 +66,7 @@ namespace storm {
 
         template<>
         InternalAdd<DdType::Sylvan, uint_fast64_t> InternalDdManager<DdType::Sylvan>::getAddZero() const {
-            return InternalAdd<DdType::Sylvan, uint_fast64_t>(this, sylvan::Mtbdd::uint64Terminal(storm::utility::zero<uint_fast64_t>()));
+            return InternalAdd<DdType::Sylvan, uint_fast64_t>(this, sylvan::Mtbdd::int64Terminal(storm::utility::zero<uint_fast64_t>()));
         }
         
         template<>
@@ -76,7 +76,7 @@ namespace storm {
 
         template<>
         InternalAdd<DdType::Sylvan, uint_fast64_t> InternalDdManager<DdType::Sylvan>::getConstant(uint_fast64_t const& value) const {
-            return InternalAdd<DdType::Sylvan, uint_fast64_t>(this, sylvan::Mtbdd::uint64Terminal(value));
+            return InternalAdd<DdType::Sylvan, uint_fast64_t>(this, sylvan::Mtbdd::int64Terminal(value));
         }
         
         std::pair<InternalBdd<DdType::Sylvan>, InternalBdd<DdType::Sylvan>> InternalDdManager<DdType::Sylvan>::createNewDdVariablePair() {