diff --git a/resources/3rdparty/sylvan/src/sylvan_mtbdd.c b/resources/3rdparty/sylvan/src/sylvan_mtbdd.c index f044e143d..f553f9e7e 100644 --- a/resources/3rdparty/sylvan/src/sylvan_mtbdd.c +++ b/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 THEN ELSE . * 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" + diff --git a/resources/3rdparty/sylvan/src/sylvan_mtbdd.h b/resources/3rdparty/sylvan/src/sylvan_mtbdd.h index e461432b0..731b5be0f 100644 --- a/resources/3rdparty/sylvan/src/sylvan_mtbdd.h +++ b/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); diff --git a/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.c b/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.c index 93b71af57..37fd53cf5 100644 --- a/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.c +++ b/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) { diff --git a/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.h b/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.h index 63bc61c90..781f36800 100644 --- a/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.h +++ b/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 diff --git a/resources/3rdparty/sylvan/src/sylvan_obj.cpp b/resources/3rdparty/sylvan/src/sylvan_obj.cpp index 60d95dcb2..07a232626 100644 --- a/resources/3rdparty/sylvan/src/sylvan_obj.cpp +++ b/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" + diff --git a/resources/3rdparty/sylvan/src/sylvan_obj.hpp b/resources/3rdparty/sylvan/src/sylvan_obj.hpp index e59c30d06..4ae849dad 100644 --- a/resources/3rdparty/sylvan/src/sylvan_obj.hpp +++ b/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 + * @brief Creates a Mtbdd leaf representing the int64 value */ - static Mtbdd uint64Terminal(uint64_t value); + static Mtbdd int64Terminal(int64_t value); /** * @brief Creates a Mtbdd leaf representing the floating-point value @@ -545,7 +546,7 @@ public: * @brief Creates a Mtbdd leaf representing the fraction value / * 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 holding 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(); }; } diff --git a/resources/3rdparty/sylvan/src/sylvan_obj_bdd_storm.hpp b/resources/3rdparty/sylvan/src/sylvan_obj_bdd_storm.hpp index 3c453ae9f..3a81a05f8 100644 --- a/resources/3rdparty/sylvan/src/sylvan_obj_bdd_storm.hpp +++ b/resources/3rdparty/sylvan/src/sylvan_obj_bdd_storm.hpp @@ -1,2 +1,2 @@ Mtbdd toDoubleMtbdd() const; - Mtbdd toUint64Mtbdd() const; + Mtbdd toInt64Mtbdd() const; diff --git a/resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp b/resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp index 8f060069e..789a385d8 100644 --- a/resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp +++ b/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 diff --git a/src/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp b/src/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp index 08018e6fc..b93d0dcc3 100644 --- a/src/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp +++ b/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(new SymbolicQuantitativeCheckResult(model.getReachableStates(), infinityStates.template toAdd() * model.getManager().getConstant(storm::utility::infinity()) + maybeStates.template toAdd() * model.getManager().getConstant(storm::utility::one()))); + return std::unique_ptr(new SymbolicQuantitativeCheckResult(model.getReachableStates(), infinityStates.template toAdd().ite(model.getManager().getConstant(storm::utility::infinity()), model.getManager().template getAddZero()) + maybeStates.template toAdd() * model.getManager().template getAddOne())); } 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(new storm::modelchecker::HybridQuantitativeCheckResult(model.getReachableStates(), model.getReachableStates() && !maybeStates, infinityStates.template toAdd() * model.getManager().getConstant(storm::utility::infinity()), maybeStates, odd, x)); + return std::unique_ptr(new storm::modelchecker::HybridQuantitativeCheckResult(model.getReachableStates(), model.getReachableStates() && !maybeStates, infinityStates.template toAdd().ite(model.getManager().getConstant(storm::utility::infinity()), model.getManager().template getAddZero()), maybeStates, odd, x)); } else { - return std::unique_ptr(new storm::modelchecker::SymbolicQuantitativeCheckResult(model.getReachableStates(), infinityStates.template toAdd() * model.getManager().getConstant(storm::utility::infinity()))); + return std::unique_ptr(new storm::modelchecker::SymbolicQuantitativeCheckResult(model.getReachableStates(), infinityStates.template toAdd().ite(model.getManager().getConstant(storm::utility::infinity()), model.getManager().template getAddZero()))); } } } diff --git a/src/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp b/src/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp index bc5a1c1c2..5fd89271a 100644 --- a/src/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp +++ b/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(new SymbolicQuantitativeCheckResult(model.getReachableStates(), infinityStates.template toAdd() * model.getManager().getConstant(storm::utility::infinity()) + maybeStates.template toAdd() * model.getManager().getConstant(storm::utility::one()))); + return std::unique_ptr(new SymbolicQuantitativeCheckResult(model.getReachableStates(), infinityStates.template toAdd().ite(model.getManager().getConstant(storm::utility::infinity()), model.getManager().template getAddZero()) + maybeStates.template toAdd() * model.getManager().getConstant(storm::utility::one()))); } 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(new storm::modelchecker::HybridQuantitativeCheckResult(model.getReachableStates(), model.getReachableStates() && !maybeStates, infinityStates.template toAdd() * model.getManager().getConstant(storm::utility::infinity()), maybeStates, odd, x)); + return std::unique_ptr(new storm::modelchecker::HybridQuantitativeCheckResult(model.getReachableStates(), model.getReachableStates() && !maybeStates, infinityStates.template toAdd().ite(model.getManager().getConstant(storm::utility::infinity()), model.getManager().template getAddZero()), maybeStates, odd, x)); } else { - return std::unique_ptr(new storm::modelchecker::SymbolicQuantitativeCheckResult(model.getReachableStates(), infinityStates.template toAdd() * model.getManager().getConstant(storm::utility::infinity()))); + return std::unique_ptr(new storm::modelchecker::SymbolicQuantitativeCheckResult(model.getReachableStates(), infinityStates.template toAdd().ite(model.getManager().getConstant(storm::utility::infinity()), model.getManager().template getAddZero()))); } } } diff --git a/src/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp b/src/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp index e870174ce..9d6af2b71 100644 --- a/src/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp +++ b/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() * model.getManager().getConstant(storm::utility::infinity()) + maybeStates.template toAdd() * model.getManager().getConstant(storm::utility::one()); + return infinityStates.template toAdd().ite(model.getManager().getConstant(storm::utility::infinity()), model.getManager().template getAddZero()) + maybeStates.template toAdd() * model.getManager().getConstant(storm::utility::one()); } 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> solver = linearEquationSolverFactory.create(submatrix, maybeStates, model.getRowVariables(), model.getColumnVariables(), model.getRowColumnMetaVariablePairs()); storm::dd::Add result = solver->solveEquationSystem(model.getManager().getConstant(0.5) * maybeStatesAdd, subvector); - return infinityStates.template toAdd() * model.getManager().getConstant(storm::utility::infinity()) + result; + return infinityStates.template toAdd().ite(model.getManager().getConstant(storm::utility::infinity()), result); } else { - return infinityStates.template toAdd() * model.getManager().getConstant(storm::utility::infinity()); + return infinityStates.template toAdd().ite(model.getManager().getConstant(storm::utility::infinity()), model.getManager().getConstant(storm::utility::zero())); } } } diff --git a/src/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp b/src/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp index 9f78545e4..d2ed0f764 100644 --- a/src/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp +++ b/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(new SymbolicQuantitativeCheckResult(model.getReachableStates(), infinityStates.template toAdd() * model.getManager().getConstant(storm::utility::infinity()) + maybeStates.template toAdd() * model.getManager().getConstant(storm::utility::one()))); + return std::unique_ptr(new SymbolicQuantitativeCheckResult(model.getReachableStates(), infinityStates.template toAdd().ite(model.getManager().getConstant(storm::utility::infinity()), model.getManager().template getAddZero()) + maybeStates.template toAdd() * model.getManager().getConstant(storm::utility::one()))); } 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> solver = linearEquationSolverFactory.create(submatrix, maybeStates, model.getIllegalMask() && maybeStates, model.getRowVariables(), model.getColumnVariables(), model.getNondeterminismVariables(), model.getRowColumnMetaVariablePairs()); storm::dd::Add result = solver->solveEquationSystem(minimize, model.getManager().template getAddZero(), subvector); - return std::unique_ptr(new storm::modelchecker::SymbolicQuantitativeCheckResult(model.getReachableStates(), infinityStates.template toAdd() * model.getManager().getConstant(storm::utility::infinity()) + result)); + return std::unique_ptr(new storm::modelchecker::SymbolicQuantitativeCheckResult(model.getReachableStates(), infinityStates.template toAdd().ite(model.getManager().getConstant(storm::utility::infinity()), result))); } else { - return std::unique_ptr(new storm::modelchecker::SymbolicQuantitativeCheckResult(model.getReachableStates(), infinityStates.template toAdd() * model.getManager().getConstant(storm::utility::infinity()))); + return std::unique_ptr(new storm::modelchecker::SymbolicQuantitativeCheckResult(model.getReachableStates(), infinityStates.template toAdd().ite(model.getManager().getConstant(storm::utility::infinity()), model.getManager().template getAddZero()))); } } } diff --git a/src/solver/SymbolicLinearEquationSolver.cpp b/src/solver/SymbolicLinearEquationSolver.cpp index 35f4f9a56..4b795f1ce 100644 --- a/src/solver/SymbolicLinearEquationSolver.cpp +++ b/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; } diff --git a/src/solver/SymbolicMinMaxLinearEquationSolver.cpp b/src/solver/SymbolicMinMaxLinearEquationSolver.cpp index 2821fad19..c33863ab7 100644 --- a/src/solver/SymbolicMinMaxLinearEquationSolver.cpp +++ b/src/solver/SymbolicMinMaxLinearEquationSolver.cpp @@ -14,12 +14,12 @@ namespace storm { namespace solver { template - SymbolicMinMaxLinearEquationSolver::SymbolicMinMaxLinearEquationSolver(storm::dd::Add const& A, storm::dd::Bdd const& allRows, storm::dd::Bdd const& illegalMask, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::set const& choiceVariables, std::vector> const& rowColumnMetaVariablePairs, double precision, uint_fast64_t maximalNumberOfIterations, bool relative) : A(A), allRows(allRows), illegalMaskAdd(illegalMask.template toAdd() * A.getDdManager().getConstant(storm::utility::infinity())), rowMetaVariables(rowMetaVariables), columnMetaVariables(columnMetaVariables), choiceVariables(choiceVariables), rowColumnMetaVariablePairs(rowColumnMetaVariablePairs), precision(precision), maximalNumberOfIterations(maximalNumberOfIterations), relative(relative) { + SymbolicMinMaxLinearEquationSolver::SymbolicMinMaxLinearEquationSolver(storm::dd::Add const& A, storm::dd::Bdd const& allRows, storm::dd::Bdd const& illegalMask, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::set const& choiceVariables, std::vector> const& rowColumnMetaVariablePairs, double precision, uint_fast64_t maximalNumberOfIterations, bool relative) : A(A), allRows(allRows), illegalMaskAdd(illegalMask.template toAdd().ite(A.getDdManager().getConstant(storm::utility::infinity()), A.getDdManager().template getAddZero())), rowMetaVariables(rowMetaVariables), columnMetaVariables(columnMetaVariables), choiceVariables(choiceVariables), rowColumnMetaVariablePairs(rowColumnMetaVariablePairs), precision(precision), maximalNumberOfIterations(maximalNumberOfIterations), relative(relative) { // Intentionally left empty. } template - SymbolicMinMaxLinearEquationSolver::SymbolicMinMaxLinearEquationSolver(storm::dd::Add const& A, storm::dd::Bdd const& allRows, storm::dd::Bdd const& illegalMask, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::set const& choiceVariables, std::vector> const& rowColumnMetaVariablePairs) : A(A), allRows(allRows), illegalMaskAdd(illegalMask.template toAdd() * A.getDdManager().getConstant(storm::utility::infinity())), rowMetaVariables(rowMetaVariables), columnMetaVariables(columnMetaVariables), choiceVariables(choiceVariables), rowColumnMetaVariablePairs(rowColumnMetaVariablePairs) { + SymbolicMinMaxLinearEquationSolver::SymbolicMinMaxLinearEquationSolver(storm::dd::Add const& A, storm::dd::Bdd const& allRows, storm::dd::Bdd const& illegalMask, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::set const& choiceVariables, std::vector> const& rowColumnMetaVariablePairs) : A(A), allRows(allRows), illegalMaskAdd(illegalMask.template toAdd().ite(A.getDdManager().getConstant(storm::utility::infinity()), A.getDdManager().template getAddZero())), rowMetaVariables(rowMetaVariables), columnMetaVariables(columnMetaVariables), choiceVariables(choiceVariables), rowColumnMetaVariablePairs(rowColumnMetaVariablePairs) { // Get the settings object to customize solving. storm::settings::modules::NativeEquationSolverSettings const& settings = storm::settings::nativeEquationSolverSettings(); diff --git a/src/storage/dd/sylvan/InternalSylvanAdd.cpp b/src/storage/dd/sylvan/InternalSylvanAdd.cpp index 824a9dd43..30fa65a59 100644 --- a/src/storage/dd/sylvan/InternalSylvanAdd.cpp +++ b/src/storage/dd/sylvan/InternalSylvanAdd.cpp @@ -355,12 +355,12 @@ namespace storm { template void InternalAdd::composeWithExplicitVector(storm::dd::Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector, std::function 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 void InternalAdd::composeWithExplicitVector(storm::dd::Odd const& odd, std::vector const& ddVariableIndices, std::vector const& offsets, std::vector& targetVector, std::function 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 @@ -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 std::vector> InternalAdd::splitIntoGroups(std::vector const& ddGroupVariableIndices) const { std::vector> 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 std::vector, InternalAdd>> InternalAdd::splitIntoGroups(InternalAdd vector, std::vector const& ddGroupVariableIndices) const { std::vector, InternalAdd>> 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(ddManager, sylvan::Mtbdd(negated ? mtbdd_negate(dd) : dd))); + groups.push_back(InternalAdd(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(ddManager, sylvan::Mtbdd(negated1 ? mtbdd_negate(dd1) : dd1 )), InternalAdd(ddManager, sylvan::Mtbdd(negated2 ? mtbdd_negate(dd2) : dd2)))); + groups.push_back(std::make_pair(InternalAdd(ddManager, negated1 ? sylvan::Mtbdd(dd1).Negate() : sylvan::Mtbdd(dd1)), InternalAdd(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 void InternalAdd::toMatrixComponents(std::vector const& rowGroupIndices, std::vector& rowIndications, std::vector>& columnsAndValues, Odd const& rowOdd, Odd const& columnOdd, std::vector const& ddRowVariableIndices, std::vector 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 @@ -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 MTBDD InternalAdd::getLeaf(uint_fast64_t value) { - return mtbdd_uint64(value); + return mtbdd_int64(value); } template ValueType InternalAdd::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::value) { @@ -618,7 +618,7 @@ namespace storm { return negated ? -mtbdd_getdouble(n) : mtbdd_getdouble(n); } else if (std::is_same::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."); } diff --git a/src/storage/dd/sylvan/InternalSylvanBdd.cpp b/src/storage/dd/sylvan/InternalSylvanBdd.cpp index 70f90d9b7..57e2635fa 100644 --- a/src/storage/dd/sylvan/InternalSylvanBdd.cpp +++ b/src/storage/dd/sylvan/InternalSylvanBdd.cpp @@ -231,7 +231,7 @@ namespace storm { if (std::is_same::value) { return InternalAdd(ddManager, this->sylvanBdd.toDoubleMtbdd()); } else if (std::is_same::value) { - return InternalAdd(ddManager, this->sylvanBdd.toUint64Mtbdd()); + return InternalAdd(ddManager, this->sylvanBdd.toInt64Mtbdd()); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Illegal ADD type."); } diff --git a/src/storage/dd/sylvan/InternalSylvanDdManager.cpp b/src/storage/dd/sylvan/InternalSylvanDdManager.cpp index 9aaaa6585..ff544c712 100644 --- a/src/storage/dd/sylvan/InternalSylvanDdManager.cpp +++ b/src/storage/dd/sylvan/InternalSylvanDdManager.cpp @@ -52,7 +52,7 @@ namespace storm { template<> InternalAdd InternalDdManager::getAddOne() const { - return InternalAdd(this, sylvan::Mtbdd::uint64Terminal(storm::utility::one())); + return InternalAdd(this, sylvan::Mtbdd::int64Terminal(storm::utility::one())); } InternalBdd InternalDdManager::getBddZero() const { @@ -66,7 +66,7 @@ namespace storm { template<> InternalAdd InternalDdManager::getAddZero() const { - return InternalAdd(this, sylvan::Mtbdd::uint64Terminal(storm::utility::zero())); + return InternalAdd(this, sylvan::Mtbdd::int64Terminal(storm::utility::zero())); } template<> @@ -76,7 +76,7 @@ namespace storm { template<> InternalAdd InternalDdManager::getConstant(uint_fast64_t const& value) const { - return InternalAdd(this, sylvan::Mtbdd::uint64Terminal(value)); + return InternalAdd(this, sylvan::Mtbdd::int64Terminal(value)); } std::pair, InternalBdd> InternalDdManager::createNewDdVariablePair() {