diff --git a/resources/3rdparty/sylvan/src/lace.h b/resources/3rdparty/sylvan/src/lace.h index ce7a5884c..a4f343ca8 100644 --- a/resources/3rdparty/sylvan/src/lace.h +++ b/resources/3rdparty/sylvan/src/lace.h @@ -182,7 +182,7 @@ struct __lace_common_fields_only { TASK_COMMON_FIELDS(_Task) }; #define LACE_COMMON_FIELD_SIZE sizeof(struct __lace_common_fields_only) typedef struct _Task { - TASK_COMMON_FIELDS(_Task); + TASK_COMMON_FIELDS(_Task) char p1[PAD(LACE_COMMON_FIELD_SIZE, P_SZ)]; char d[LACE_TASKSIZE]; char p2[PAD(ROUND(LACE_COMMON_FIELD_SIZE, P_SZ) + LACE_TASKSIZE, LINE_SIZE)]; diff --git a/resources/3rdparty/sylvan/src/sylvan_mtbdd.c b/resources/3rdparty/sylvan/src/sylvan_mtbdd.c index a02a7877e..311bb9a3d 100644 --- a/resources/3rdparty/sylvan/src/sylvan_mtbdd.c +++ b/resources/3rdparty/sylvan/src/sylvan_mtbdd.c @@ -1263,11 +1263,6 @@ TASK_IMPL_2(MTBDD, mtbdd_op_divide, MTBDD*, pa, MTBDD*, pb) } } - if (a < b) { - *pa = b; - *pb = a; - } - return mtbdd_invalid; } @@ -1480,6 +1475,135 @@ TASK_IMPL_2(MTBDD, mtbdd_op_equals, MTBDD*, pa, MTBDD*, pb) return mtbdd_invalid; } +/** + * Binary operation Equals (for MTBDDs of same type) + * Only for MTBDDs where either all leaves are Boolean, or Integer, or Double. + * For Integer/Double MTBDD, if either operand is mtbdd_false (not defined), + * then the result is mtbdd_false (i.e. not defined). + */ +TASK_IMPL_2(MTBDD, mtbdd_op_less, MTBDD*, pa, MTBDD*, pb) +{ + MTBDD a = *pa, b = *pb; + if (a == mtbdd_false && b == mtbdd_false) return mtbdd_true; + if (a == mtbdd_true && b == mtbdd_true) return mtbdd_true; + + 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 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; + } 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) { + // both fraction + uint64_t nom_a = val_a>>32; + 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; + } + } + + return mtbdd_invalid; +} + +/** + * Binary operation Equals (for MTBDDs of same type) + * Only for MTBDDs where either all leaves are Boolean, or Integer, or Double. + * For Integer/Double MTBDD, if either operand is mtbdd_false (not defined), + * then the result is mtbdd_false (i.e. not defined). + */ +TASK_IMPL_2(MTBDD, mtbdd_op_less_or_equal, MTBDD*, pa, MTBDD*, pb) +{ + MTBDD a = *pa, b = *pb; + if (a == mtbdd_false && b == mtbdd_false) return mtbdd_true; + if (a == mtbdd_true && b == mtbdd_true) return mtbdd_true; + + 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 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; + } 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) { + // both fraction + uint64_t nom_a = val_a>>32; + 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 mtbdd_invalid; +} + /** * Compute IF THEN ELSE . * must be a Boolean MTBDD (or standard BDD). @@ -1588,7 +1712,7 @@ TASK_IMPL_2(MTBDD, mtbdd_op_strict_threshold_double, MTBDD, a, size_t, svalue) return mtbdd_invalid; } -TASK_IMPL_1(MTBDD, mtbdd_not_zero, MTBDD, a) +TASK_IMPL_2(MTBDD, mtbdd_op_not_zero, MTBDD, a, size_t, v) { /* We only expect "double" terminals, or false */ if (a == mtbdd_false) return mtbdd_false; @@ -1607,7 +1731,18 @@ TASK_IMPL_1(MTBDD, mtbdd_not_zero, MTBDD, a) } } - return mtbdd_invalid; + // Ugly hack to get rid of the error "unused variable v" (because there is no version of uapply without a parameter). + return v > 0 ? mtbdd_invalid : mtbdd_invalid; +} + +TASK_IMPL_2(MTBDD, mtbdd_op_bool_to_double, MTBDD, a, size_t, v) +{ + /* We only expect "double" terminals, or false */ + if (a == mtbdd_false) return mtbdd_double(0); + if (a == mtbdd_true) return mtbdd_double(1.0); + + // Ugly hack to get rid of the error "unused variable v" (because there is no version of uapply without a parameter). + return v > 0 ? mtbdd_invalid : mtbdd_invalid; } TASK_IMPL_2(MTBDD, mtbdd_threshold_double, MTBDD, dd, double, d) @@ -1620,6 +1755,16 @@ TASK_IMPL_2(MTBDD, mtbdd_strict_threshold_double, MTBDD, dd, double, d) return mtbdd_uapply(dd, TASK(mtbdd_op_strict_threshold_double), *(size_t*)&d); } +TASK_IMPL_1(MTBDD, mtbdd_not_zero, MTBDD, dd) +{ + return mtbdd_uapply(dd, TASK(mtbdd_op_not_zero), 0); +} + +TASK_IMPL_1(MTBDD, mtbdd_bool_to_double, MTBDD, dd) +{ + return mtbdd_uapply(dd, TASK(mtbdd_op_bool_to_double), 0); +} + /** * Compare two Double MTBDDs, returns Boolean True if they are equal within some value epsilon */ diff --git a/resources/3rdparty/sylvan/src/sylvan_mtbdd.h b/resources/3rdparty/sylvan/src/sylvan_mtbdd.h index 8053b76c1..c3fddc9ac 100644 --- a/resources/3rdparty/sylvan/src/sylvan_mtbdd.h +++ b/resources/3rdparty/sylvan/src/sylvan_mtbdd.h @@ -258,6 +258,22 @@ TASK_DECL_3(MTBDD, mtbdd_abstract_op_max, MTBDD, MTBDD, int); */ TASK_DECL_2(MTBDD, mtbdd_op_equals, MTBDD*, MTBDD*); +/** + * Binary operation Less (for MTBDDs of same type) + * Only for MTBDDs where either all leaves are Boolean, or Integer, or Double. + * For Integer/Double MTBDD, if either operand is mtbdd_false (not defined), + * then the result is the other operand. + */ +TASK_DECL_2(MTBDD, mtbdd_op_less, MTBDD*, MTBDD*); + +/** + * Binary operation Less (for MTBDDs of same type) + * Only for MTBDDs where either all leaves are Boolean, or Integer, or Double. + * For Integer/Double MTBDD, if either operand is mtbdd_false (not defined), + * then the result is the other operand. + */ +TASK_DECL_2(MTBDD, mtbdd_op_less_or_equal, MTBDD*, MTBDD*); + /** * Compute a == b */ @@ -292,6 +308,9 @@ TASK_DECL_2(MTBDD, mtbdd_op_equals, MTBDD*, MTBDD*); * Compute max(a, b) */ #define mtbdd_max(a, b) mtbdd_apply(a, b, TASK(mtbdd_op_max)) + +#define mtbdd_less_as_bdd(a, b) mtbdd_apply(a, b, TASK(mtbdd_op_less)) +#define mtbdd_less_or_equal_as_bdd(a, b) mtbdd_apply(a, b, TASK(mtbdd_op_less_or_equal)) /** * Abstract the variables in from by taking the sum of all values @@ -340,8 +359,12 @@ TASK_DECL_2(MTBDD, mtbdd_op_strict_threshold_double, MTBDD, size_t) /** * Monad that converts double to a Boolean MTBDD, translate terminals != 0 to 1 and to 0 otherwise; */ -TASK_DECL_1(MTBDD, mtbdd_not_zero, MTBDD) -#define mtbdd_not_zero(dd) CALL(mtbdd_not_zero, dd) +TASK_DECL_2(MTBDD, mtbdd_op_not_zero, MTBDD, size_t) + +/** + * Monad that converts Boolean to a Double MTBDD, translate terminals true to 1 and to 0 otherwise; + */ +TASK_DECL_2(MTBDD, mtbdd_op_bool_to_double, MTBDD, size_t) /** * Convert double to a Boolean MTBDD, translate terminals >= value to 1 and to 0 otherwise; @@ -355,6 +378,12 @@ TASK_DECL_2(MTBDD, mtbdd_threshold_double, MTBDD, double); TASK_DECL_2(MTBDD, mtbdd_strict_threshold_double, MTBDD, double); #define mtbdd_strict_threshold_double(dd, value) CALL(mtbdd_strict_threshold_double, dd, value) +TASK_DECL_1(MTBDD, mtbdd_not_zero, MTBDD) +#define mtbdd_not_zero(dd) CALL(mtbdd_not_zero, dd) + +TASK_DECL_1(MTBDD, mtbdd_bool_to_double, MTBDD) +#define mtbdd_bool_to_double(dd) CALL(mtbdd_bool_to_double, dd) + /** * For two Double MTBDDs, calculate whether they are equal module some value epsilon * i.e. abs(a-b)<3 diff --git a/resources/3rdparty/sylvan/src/sylvan_obj.cpp b/resources/3rdparty/sylvan/src/sylvan_obj.cpp index 29e6ec714..f62acd795 100644 --- a/resources/3rdparty/sylvan/src/sylvan_obj.cpp +++ b/resources/3rdparty/sylvan/src/sylvan_obj.cpp @@ -443,6 +443,12 @@ Bdd::NodeCount() const return sylvan_nodecount(bdd); } +Mtbdd +Bdd::toDoubleMtbdd() const { + LACE_ME; + return mtbdd_bool_to_double(bdd); +} + Bdd Bdd::bddOne() { @@ -912,6 +918,32 @@ Mtbdd::Equals(const Mtbdd& other) const { return mtbdd_equals(mtbdd, other.mtbdd); } +Bdd +Mtbdd::Less(const Mtbdd& other) const { + LACE_ME; + return mtbdd_less_as_bdd(mtbdd, other.mtbdd); +} + +Bdd +Mtbdd::LessOrEqual(const Mtbdd& other) const { + LACE_ME; + return mtbdd_less_or_equal_as_bdd(mtbdd, other.mtbdd); +} + +double +Mtbdd::getDoubleMax() const { + LACE_ME; + MTBDD maxNode = mtbdd_maximum(mtbdd); + return mtbdd_getdouble(maxNode); +} + +double +Mtbdd::getDoubleMin() const { + LACE_ME; + MTBDD minNode = mtbdd_minimum(mtbdd); + return mtbdd_getdouble(minNode); +} + Mtbdd Mtbdd::Support() const { diff --git a/resources/3rdparty/sylvan/src/sylvan_obj.hpp b/resources/3rdparty/sylvan/src/sylvan_obj.hpp index fd47fa662..bee74053b 100644 --- a/resources/3rdparty/sylvan/src/sylvan_obj.hpp +++ b/resources/3rdparty/sylvan/src/sylvan_obj.hpp @@ -27,6 +27,8 @@ namespace sylvan { class BddMap; +class Mtbdd; + class Bdd { friend class Sylvan; friend class BddMap; @@ -317,6 +319,8 @@ public: */ size_t NodeCount() const; + Mtbdd toDoubleMtbdd() const; + private: BDD bdd; }; @@ -591,7 +595,15 @@ public: Bdd NotZero() const; Bdd Equals(const Mtbdd& other) const; + + Bdd Less(const Mtbdd& other) const; + Bdd LessOrEqual(const Mtbdd& other) const; + + double getDoubleMax() const; + + double getDoubleMin() const; + /** * @brief Computes the support of a Mtbdd. */ diff --git a/src/storage/dd/sylvan/InternalSylvanAdd.cpp b/src/storage/dd/sylvan/InternalSylvanAdd.cpp index 363f1927c..766da0bac 100644 --- a/src/storage/dd/sylvan/InternalSylvanAdd.cpp +++ b/src/storage/dd/sylvan/InternalSylvanAdd.cpp @@ -24,7 +24,7 @@ namespace storm { template InternalAdd InternalAdd::ite(InternalAdd const& thenDd, InternalAdd const& elseDd) const { - return InternalAdd(ddManager, this->sylvanMtbdd.NotZero().Ite(thenDd.sylvanMtbdd, elseDd.sylvanMtbdd)); + return InternalAdd(ddManager, sylvan::Mtbdd(static_cast(this->sylvanMtbdd.NotZero().GetBDD())).Ite(thenDd.sylvanMtbdd, elseDd.sylvanMtbdd)); } template @@ -73,7 +73,7 @@ namespace storm { template InternalBdd InternalAdd::equals(InternalAdd const& other) const { - return InternalAdd(ddManager, this->sylvanMtbdd.Equals(other.sylvanMtbdd)); + return InternalBdd(ddManager, this->sylvanMtbdd.Equals(other.sylvanMtbdd)); } template @@ -83,12 +83,12 @@ namespace storm { template InternalBdd InternalAdd::less(InternalAdd const& other) const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + return InternalBdd(ddManager, this->sylvanMtbdd.Less(other.sylvanMtbdd)); } template InternalBdd InternalAdd::lessOrEqual(InternalAdd const& other) const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + return InternalBdd(ddManager, this->sylvanMtbdd.LessOrEqual(other.sylvanMtbdd)); } template @@ -227,12 +227,12 @@ namespace storm { template ValueType InternalAdd::getMin() const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + return static_cast(this-sylvanMtbdd.getDoubleMin()); } template ValueType InternalAdd::getMax() const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + return static_cast(this-sylvanMtbdd.getDoubleMax()); } template diff --git a/src/storage/dd/sylvan/InternalSylvanBdd.cpp b/src/storage/dd/sylvan/InternalSylvanBdd.cpp index 6fc9cbe90..d6124853a 100644 --- a/src/storage/dd/sylvan/InternalSylvanBdd.cpp +++ b/src/storage/dd/sylvan/InternalSylvanBdd.cpp @@ -147,7 +147,7 @@ namespace storm { template InternalAdd InternalBdd::toAdd() const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + return InternalAdd(ddManager, this->sylvanBdd.toDoubleMtbdd()); } storm::storage::BitVector InternalBdd::toVector(storm::dd::Odd const& rowOdd, std::vector const& ddVariableIndices) const { diff --git a/test/functional/storage/SylvanDdTest.cpp b/test/functional/storage/SylvanDdTest.cpp index 9ec54b2f0..3aa6eb036 100644 --- a/test/functional/storage/SylvanDdTest.cpp +++ b/test/functional/storage/SylvanDdTest.cpp @@ -144,36 +144,36 @@ TEST(SylvanDd, OperatorTest) { bdd = dd1.toBdd() || dd2.toBdd(); EXPECT_TRUE(bdd.isOne()); -// dd1 = manager->template getIdentity(x.first); -// dd2 = manager->template getConstant(5); -// -// dd3 = dd1.equals(dd2); -// EXPECT_EQ(1ul, dd3.getNonZeroCount()); -// -// storm::dd::Add dd4 = dd1.notEquals(dd2); -// EXPECT_TRUE(dd4.toBdd() == !dd3.toBdd()); -// -// dd3 = dd1.less(dd2); -// EXPECT_EQ(11ul, dd3.getNonZeroCount()); -// -// dd3 = dd1.lessOrEqual(dd2); -// EXPECT_EQ(12ul, dd3.getNonZeroCount()); -// -// dd3 = dd1.greater(dd2); -// EXPECT_EQ(4ul, dd3.getNonZeroCount()); -// -// dd3 = dd1.greaterOrEqual(dd2); -// EXPECT_EQ(5ul, dd3.getNonZeroCount()); -// -// dd3 = (manager->getEncoding(x.first, 2).template toAdd()).ite(dd2, dd1); -// dd4 = dd3.less(dd2); -// EXPECT_EQ(10ul, dd4.getNonZeroCount()); -// -// dd4 = dd3.minimum(dd1); -// dd4 *= manager->getEncoding(x.first, 2).template toAdd(); -// dd4 = dd4.sumAbstract({x.first}); -// EXPECT_EQ(2, dd4.getValue()); -// + dd1 = manager->template getIdentity(x.first); + dd2 = manager->template getConstant(5); + + bdd = dd1.equals(dd2); + EXPECT_EQ(1ul, bdd.getNonZeroCount()); + + storm::dd::Bdd bdd2 = dd1.notEquals(dd2); + EXPECT_TRUE(bdd2 == !bdd); + + bdd = dd1.less(dd2); + EXPECT_EQ(11ul, bdd.getNonZeroCount()); + + bdd = dd1.lessOrEqual(dd2); + EXPECT_EQ(12ul, bdd.getNonZeroCount()); + + bdd = dd1.greater(dd2); + EXPECT_EQ(4ul, bdd.getNonZeroCount()); + + bdd = dd1.greaterOrEqual(dd2); + EXPECT_EQ(5ul, bdd.getNonZeroCount()); + + dd3 = (manager->getEncoding(x.first, 2).template toAdd()).ite(dd2, dd1); + bdd = dd3.less(dd2); + EXPECT_EQ(10ul, bdd.getNonZeroCount()); + + storm::dd::Add dd4 = dd3.minimum(dd1); + dd4 *= manager->getEncoding(x.first, 2).template toAdd(); + dd4 = dd4.sumAbstract({x.first}); + EXPECT_EQ(2, dd4.getValue()); +// // dd4 = dd3.maximum(dd1); // dd4 *= manager->getEncoding(x.first, 2).template toAdd(); // dd4 = dd4.sumAbstract({x.first});