From 6c1a21c43f57f04d56db34e0cb4ee1a1f7d90fee Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 25 Nov 2015 22:24:03 +0100 Subject: [PATCH] added more functions in sylvan Former-commit-id: f2e0c158a66afcc6d01bc3c87f7549c2ac052c56 --- resources/3rdparty/sylvan/src/sylvan_mtbdd.c | 53 ++++++++++++++++++++ resources/3rdparty/sylvan/src/sylvan_mtbdd.h | 13 +++++ resources/3rdparty/sylvan/src/sylvan_obj.cpp | 6 +++ resources/3rdparty/sylvan/src/sylvan_obj.hpp | 2 + src/storage/dd/sylvan/InternalSylvanAdd.cpp | 10 ++-- test/functional/storage/SylvanDdTest.cpp | 21 ++++---- 6 files changed, 90 insertions(+), 15 deletions(-) diff --git a/resources/3rdparty/sylvan/src/sylvan_mtbdd.c b/resources/3rdparty/sylvan/src/sylvan_mtbdd.c index 26de3cf1b..a02a7877e 100644 --- a/resources/3rdparty/sylvan/src/sylvan_mtbdd.c +++ b/resources/3rdparty/sylvan/src/sylvan_mtbdd.c @@ -1427,6 +1427,59 @@ TASK_IMPL_2(MTBDD, mtbdd_op_max, 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_equals, 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 (val_a == val_b && !(nega ^ negb)) 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; + 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 (nom_a == nom_b && denom_a == denom_b && !(nega ^ negb)) return mtbdd_true; + return mtbdd_false; + } + } + + if (a < b) { + *pa = b; + *pb = a; + } + + return mtbdd_invalid; +} + /** * Compute IF THEN ELSE . * must be a Boolean MTBDD (or standard BDD). diff --git a/resources/3rdparty/sylvan/src/sylvan_mtbdd.h b/resources/3rdparty/sylvan/src/sylvan_mtbdd.h index fb3ec24ac..8053b76c1 100644 --- a/resources/3rdparty/sylvan/src/sylvan_mtbdd.h +++ b/resources/3rdparty/sylvan/src/sylvan_mtbdd.h @@ -250,6 +250,19 @@ 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); +/** + * 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 the other operand. + */ +TASK_DECL_2(MTBDD, mtbdd_op_equals, MTBDD*, MTBDD*); + +/** + * Compute a == b + */ +#define mtbdd_equals(a, b) mtbdd_apply(a, b, TASK(mtbdd_op_equals)) + /** * Compute a + b */ diff --git a/resources/3rdparty/sylvan/src/sylvan_obj.cpp b/resources/3rdparty/sylvan/src/sylvan_obj.cpp index da6f7b66b..29e6ec714 100644 --- a/resources/3rdparty/sylvan/src/sylvan_obj.cpp +++ b/resources/3rdparty/sylvan/src/sylvan_obj.cpp @@ -906,6 +906,12 @@ Mtbdd::NotZero() const return mtbdd_not_zero(mtbdd); } +Bdd +Mtbdd::Equals(const Mtbdd& other) const { + LACE_ME; + return mtbdd_equals(mtbdd, other.mtbdd); +} + Mtbdd Mtbdd::Support() const { diff --git a/resources/3rdparty/sylvan/src/sylvan_obj.hpp b/resources/3rdparty/sylvan/src/sylvan_obj.hpp index 730e86261..fd47fa662 100644 --- a/resources/3rdparty/sylvan/src/sylvan_obj.hpp +++ b/resources/3rdparty/sylvan/src/sylvan_obj.hpp @@ -589,6 +589,8 @@ public: Bdd BddStrictThreshold(double value) const; Bdd NotZero() const; + + Bdd Equals(const Mtbdd& other) 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 ba7d2ec21..363f1927c 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 { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + return InternalAdd(ddManager, this->sylvanMtbdd.NotZero().Ite(thenDd.sylvanMtbdd, elseDd.sylvanMtbdd)); } template @@ -73,12 +73,12 @@ namespace storm { template InternalBdd InternalAdd::equals(InternalAdd const& other) const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + return InternalAdd(ddManager, this->sylvanMtbdd.Equals(other.sylvanMtbdd)); } template InternalBdd InternalAdd::notEquals(InternalAdd const& other) const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + return !this->equals(other); } template @@ -93,12 +93,12 @@ namespace storm { template InternalBdd InternalAdd::greater(InternalAdd const& other) const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + return !this->lessOrEqual(other); } template InternalBdd InternalAdd::greaterOrEqual(InternalAdd const& other) const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + return !this->less(other); } template diff --git a/test/functional/storage/SylvanDdTest.cpp b/test/functional/storage/SylvanDdTest.cpp index cd47c66a7..9ec54b2f0 100644 --- a/test/functional/storage/SylvanDdTest.cpp +++ b/test/functional/storage/SylvanDdTest.cpp @@ -110,10 +110,11 @@ TEST(SylvanDd, OperatorTest) { EXPECT_FALSE(manager->template getAddZero() != manager->template getAddZero()); EXPECT_TRUE(manager->template getAddZero() != manager->template getAddOne()); - + storm::dd::Add dd1 = manager->template getAddOne(); storm::dd::Add dd2 = manager->template getAddOne(); storm::dd::Add dd3 = dd1 + dd2; + storm::dd::Bdd bdd; EXPECT_TRUE(dd3 == manager->template getConstant(2)); dd3 += manager->template getAddZero(); @@ -134,15 +135,15 @@ TEST(SylvanDd, OperatorTest) { dd3 /= manager->template getConstant(2); EXPECT_TRUE(dd3.isOne()); -// dd3 = !dd3; -// EXPECT_TRUE(dd3.isZero()); -// -// dd1 = !dd3; -// EXPECT_TRUE(dd1.isOne()); -// -// dd3 = dd1 || dd2; -// EXPECT_TRUE(dd3.isOne()); -// + bdd = !dd3.toBdd(); + EXPECT_TRUE(bdd.isZero()); + + bdd = !bdd; + EXPECT_TRUE(bdd.isOne()); + + bdd = dd1.toBdd() || dd2.toBdd(); + EXPECT_TRUE(bdd.isOne()); + // dd1 = manager->template getIdentity(x.first); // dd2 = manager->template getConstant(5); //