diff --git a/resources/3rdparty/sylvan/src/sylvan_bdd.c b/resources/3rdparty/sylvan/src/sylvan_bdd.c index 74936a62d..6b6b3f74f 100644 --- a/resources/3rdparty/sylvan/src/sylvan_bdd.c +++ b/resources/3rdparty/sylvan/src/sylvan_bdd.c @@ -2818,3 +2818,5 @@ TASK_IMPL_1(int, sylvan_test_isbdd, BDD, bdd) if (!SYNC(sylvan_test_isbdd_rec)) result = 0; return result; } + +#include "sylvan_bdd_storm.c" diff --git a/resources/3rdparty/sylvan/src/sylvan_bdd_storm.c b/resources/3rdparty/sylvan/src/sylvan_bdd_storm.c new file mode 100644 index 000000000..c3226c947 --- /dev/null +++ b/resources/3rdparty/sylvan/src/sylvan_bdd_storm.c @@ -0,0 +1,152 @@ +/* */ + +/** + * Calculates \exists variables . a + */ +TASK_IMPL_3(BDD, sylvan_existsRepresentative, BDD, a, BDD, variables, BDDVAR, prev_level) +{ + int aIsNegated = (a & sylvan_complement) == ((uint64_t)0) ? 0 : 1; + + BDD aRegular = (aIsNegated) ? sylvan_not(a) : a; + + if (aRegular == sylvan_false) { + if (aIsNegated) { + //printf("return in preprocessing...1\n"); + return a; + } + + if (sylvan_set_isempty(variables)) { + //printf("return in preprocessing...2\n"); + return sylvan_true; + } else { + //printf("return in preprocessing...3\n"); + return variables; + } + } else if (sylvan_set_isempty(variables)) { + //printf("return in preprocessing...4\n"); + return a; + } + /* From now on, f and cube are non-constant. */ + bddnode_t na = GETNODE(a); + BDDVAR level = bddnode_getvariable(na); + + bddnode_t nv = GETNODE(variables); + BDDVAR vv = bddnode_getvariable(nv); + + //printf("a level %i and cube level %i\n", level, vv); + + /* Abstract a variable that does not appear in f. */ + if (level > vv) { + BDD _v = sylvan_set_next(variables); + BDD res = CALL(sylvan_existsRepresentative, a, _v, level); + if (res == sylvan_invalid) { + return sylvan_invalid; + } + bdd_refs_push(res); + + BDD res1 = sylvan_makenode(vv, sylvan_false, res); + + if (res1 == sylvan_invalid) { + bdd_refs_pop(1); + return sylvan_invalid; + } + bdd_refs_pop(1); + + //printf("return after abstr. var that does not appear in f...\n"); + return res1; + } + + /* Compute the cofactors of a. */ + BDD aLow = node_low(a, na); // ELSE + BDD aHigh = node_high(a, na); // THEN + + /* If the two indices are the same, so are their levels. */ + if (level == vv) { + BDD _v = sylvan_set_next(variables); + BDD res1 = CALL(sylvan_existsRepresentative, aLow, _v, level); + if (res1 == sylvan_invalid) { + return sylvan_invalid; + } + if (res1 == sylvan_true) { + return sylvan_true; + } + bdd_refs_push(res1); + + BDD res2 = CALL(sylvan_existsRepresentative, aHigh, _v, level); + if (res2 == sylvan_invalid) { + bdd_refs_pop(1); + return sylvan_invalid; + } + bdd_refs_push(res2); + + BDD left = CALL(sylvan_exists, aLow, _v, 0); + if (left == sylvan_invalid) { + bdd_refs_pop(2); + return sylvan_invalid; + } + + bdd_refs_push(left); + + BDD res1Inf = sylvan_ite(left, res1, sylvan_false); + if (res1Inf == sylvan_invalid) { + bdd_refs_pop(3); + return sylvan_invalid; + } + bdd_refs_push(res1Inf); + + //Cudd_IterDerefBdd(manager,res1); + + BDD res2Inf = sylvan_ite(left, sylvan_false, res2); + if (res2Inf == sylvan_invalid) { + bdd_refs_pop(4); + return sylvan_invalid; + } + bdd_refs_push(res2Inf); + + //Cudd_IterDerefBdd(manager,res2); + //Cudd_IterDerefBdd(manager,left); + + assert(res1Inf != res2Inf); + BDD res = sylvan_makenode(level, res2Inf, res1Inf); + + if (res == sylvan_invalid) { + bdd_refs_pop(5); + return sylvan_invalid; + } + + // cuddCacheInsert2(manager, Cudd_bddExistAbstractRepresentative, f, cube, res); + // TODO: CACHING HERE + + //printf("return properly computed result...\n"); + bdd_refs_pop(5); + return res; + } else { /* if (level == vv) */ + BDD res1 = CALL(sylvan_existsRepresentative, aLow, variables, level); + if (res1 == sylvan_invalid){ + return sylvan_invalid; + } + bdd_refs_push(res1); + + BDD res2 = CALL(sylvan_existsRepresentative, aHigh, variables, level); + if (res2 == sylvan_invalid) { + bdd_refs_pop(1); + return sylvan_invalid; + } + bdd_refs_push(res2); + + /* ITE takes care of possible complementation of res1 and of the + ** case in which res1 == res2. */ + BDD res = sylvan_makenode(level, res2, res1); + if (res == sylvan_invalid) { + bdd_refs_pop(2); + return sylvan_invalid; + } + + bdd_refs_pop(2); + //printf("return of last case...\n"); + return res; + } + + // Prevent unused variable warning + (void)prev_level; +} diff --git a/resources/3rdparty/sylvan/src/sylvan_bdd_storm.h b/resources/3rdparty/sylvan/src/sylvan_bdd_storm.h index 5806fba5d..f28259a84 100644 --- a/resources/3rdparty/sylvan/src/sylvan_bdd_storm.h +++ b/resources/3rdparty/sylvan/src/sylvan_bdd_storm.h @@ -1,3 +1,6 @@ #define bdd_isnegated(dd) ((dd & sylvan_complement) ? 1 : 0) #define bdd_regular(dd) (dd & ~sylvan_complement) -#define bdd_isterminal(dd) (dd == sylvan_false || dd == sylvan_true) \ No newline at end of file +#define bdd_isterminal(dd) (dd == sylvan_false || dd == sylvan_true) + +TASK_DECL_3(BDD, sylvan_existsRepresentative, BDD, BDD, BDDVAR); +#define sylvan_existsRepresentative(a, vars) (CALL(sylvan_existsRepresentative, a, vars, 0)) diff --git a/resources/3rdparty/sylvan/src/sylvan_obj_bdd_storm.hpp b/resources/3rdparty/sylvan/src/sylvan_obj_bdd_storm.hpp index 172bcf5c6..afcc027e6 100644 --- a/resources/3rdparty/sylvan/src/sylvan_obj_bdd_storm.hpp +++ b/resources/3rdparty/sylvan/src/sylvan_obj_bdd_storm.hpp @@ -4,3 +4,4 @@ Mtbdd toStormRationalFunctionMtbdd() const; #endif Mtbdd Ite(Mtbdd const& thenDd, Mtbdd const& elseDd) const; + Bdd ExistAbstractRepresentative(const BddSet& cube) const; diff --git a/resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp b/resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp index d84f49281..e055478f3 100644 --- a/resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp +++ b/resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp @@ -1,3 +1,9 @@ +Bdd +Bdd::ExistAbstractRepresentative(const BddSet& cube) const { + LACE_ME; + return sylvan_existsRepresentative(bdd, cube.set.bdd); +} + Mtbdd Bdd::toDoubleMtbdd() const { LACE_ME; diff --git a/src/storage/dd/sylvan/InternalSylvanBdd.cpp b/src/storage/dd/sylvan/InternalSylvanBdd.cpp index ac4e1180e..c173a1e51 100644 --- a/src/storage/dd/sylvan/InternalSylvanBdd.cpp +++ b/src/storage/dd/sylvan/InternalSylvanBdd.cpp @@ -161,7 +161,7 @@ namespace storm { } InternalBdd InternalBdd::existsAbstractRepresentative(InternalBdd const& cube) const { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "This operation is currently not supported by sylvan."); + return InternalBdd(ddManager, this->sylvanBdd.ExistAbstractRepresentative(cube.sylvanBdd)); } InternalBdd InternalBdd::universalAbstract(InternalBdd const& cube) const { diff --git a/test/functional/storage/CuddDdTest.cpp b/test/functional/storage/CuddDdTest.cpp index 695d247e2..b05edcaf7 100644 --- a/test/functional/storage/CuddDdTest.cpp +++ b/test/functional/storage/CuddDdTest.cpp @@ -11,7 +11,7 @@ #include "src/storage/SparseMatrix.h" -TEST(CuddDd, Constants) { +TEST(CuddDd, AddConstants) { std::shared_ptr> manager(new storm::dd::DdManager()); storm::dd::Add zero; ASSERT_NO_THROW(zero = manager->template getAddZero()); @@ -41,6 +41,55 @@ TEST(CuddDd, Constants) { EXPECT_EQ(2, two.getMax()); } +TEST(CuddDd, BddConstants) { + std::shared_ptr> manager(new storm::dd::DdManager()); + storm::dd::Bdd zero; + ASSERT_NO_THROW(zero = manager->getBddZero()); + + EXPECT_EQ(0ul, zero.getNonZeroCount()); + EXPECT_EQ(1ul, zero.getLeafCount()); + EXPECT_EQ(1ul, zero.getNodeCount()); + + storm::dd::Bdd one; + ASSERT_NO_THROW(one = manager->getBddOne()); + + EXPECT_EQ(0ul, one.getNonZeroCount()); + EXPECT_EQ(1ul, one.getLeafCount()); + EXPECT_EQ(1ul, one.getNodeCount()); +} + +TEST(CuddDd, BddExistAbstractRepresentative) { + std::shared_ptr> manager(new storm::dd::DdManager()); + std::pair x; + std::pair y; + std::pair z; + ASSERT_NO_THROW(x = manager->addMetaVariable("x", 0, 1)); + ASSERT_NO_THROW(y = manager->addMetaVariable("y", 0, 1)); + ASSERT_NO_THROW(z = manager->addMetaVariable("z", 0, 1)); + + storm::dd::Bdd bddX = manager->getEncoding(x.first, 1); + //bddX.exportToDot("/opt/masterThesis/storm/build/test_bdd_x.dot"); + storm::dd::Bdd bddY = manager->getEncoding(y.first, 0); + //bddY.exportToDot("/opt/masterThesis/storm/build/test_bdd_y.dot"); + storm::dd::Bdd bddZ = manager->getEncoding(z.first, 0); + //bddZ.exportToDot("/opt/masterThesis/storm/build/test_bdd_z.dot"); + + storm::dd::Bdd bddX1Y0Z0 = (bddX && bddY) && bddZ; + //bddX1Y0Z0.exportToDot("/opt/masterThesis/storm/build/test_bddX1Y0Z0.dot"); + + EXPECT_EQ(1ul, bddX1Y0Z0.getNonZeroCount()); + EXPECT_EQ(1ul, bddX1Y0Z0.getLeafCount()); + EXPECT_EQ(4ul, bddX1Y0Z0.getNodeCount()); + + storm::dd::Bdd representative_x = bddX1Y0Z0.existsAbstractRepresentative({x.first}); + //representative_x.exportToDot("/opt/masterThesis/storm/build/test_representative_x.dot"); + storm::dd::Bdd representative_y = bddX1Y0Z0.existsAbstractRepresentative({y.first}); + //representative_y.exportToDot("/opt/masterThesis/storm/build/test_representative_y.dot"); + storm::dd::Bdd representative_z = bddX1Y0Z0.existsAbstractRepresentative({z.first}); + //representative_z.exportToDot("/opt/masterThesis/storm/build/test_representative_z.dot"); +} + + TEST(CuddDd, AddGetMetaVariableTest) { std::shared_ptr> manager(new storm::dd::DdManager()); ASSERT_NO_THROW(manager->addMetaVariable("x", 1, 9)); diff --git a/test/functional/storage/SylvanDdTest.cpp b/test/functional/storage/SylvanDdTest.cpp index 133643744..6695d34f7 100644 --- a/test/functional/storage/SylvanDdTest.cpp +++ b/test/functional/storage/SylvanDdTest.cpp @@ -44,6 +44,54 @@ TEST(SylvanDd, Constants) { EXPECT_EQ(2, two.getMax()); } +TEST(SylvanDd, BddConstants) { + std::shared_ptr> manager(new storm::dd::DdManager()); + storm::dd::Bdd zero; + ASSERT_NO_THROW(zero = manager->getBddZero()); + + EXPECT_EQ(0ul, zero.getNonZeroCount()); + EXPECT_EQ(1ul, zero.getLeafCount()); + EXPECT_EQ(1ul, zero.getNodeCount()); + + storm::dd::Bdd one; + ASSERT_NO_THROW(one = manager->getBddOne()); + + EXPECT_EQ(0ul, one.getNonZeroCount()); + EXPECT_EQ(1ul, one.getLeafCount()); + EXPECT_EQ(1ul, one.getNodeCount()); +} + +TEST(SylvanDd, BddExistAbstractRepresentative) { + std::shared_ptr> manager(new storm::dd::DdManager()); + std::pair x; + std::pair y; + std::pair z; + ASSERT_NO_THROW(x = manager->addMetaVariable("x", 0, 1)); + ASSERT_NO_THROW(y = manager->addMetaVariable("y", 0, 1)); + ASSERT_NO_THROW(z = manager->addMetaVariable("z", 0, 1)); + + storm::dd::Bdd bddX = manager->getEncoding(x.first, 1); + //bddX.exportToDot("/opt/masterThesis/storm/build/tests_bdd_x.dot"); + storm::dd::Bdd bddY = manager->getEncoding(y.first, 0); + //bddY.exportToDot("/opt/masterThesis/storm/build/tests_bdd_y.dot"); + storm::dd::Bdd bddZ = manager->getEncoding(z.first, 0); + //bddZ.exportToDot("/opt/masterThesis/storm/build/tests_bdd_z.dot"); + + storm::dd::Bdd bddX1Y0Z0 = (bddX && bddY) && bddZ; + //bddX1Y0Z0.exportToDot("/opt/masterThesis/storm/build/tests_bddX1Y0Z0.dot"); + + EXPECT_EQ(1ul, bddX1Y0Z0.getNonZeroCount()); + EXPECT_EQ(1ul, bddX1Y0Z0.getLeafCount()); + EXPECT_EQ(4ul, bddX1Y0Z0.getNodeCount()); + + storm::dd::Bdd representative_x = bddX1Y0Z0.existsAbstractRepresentative({x.first}); + //representative_x.exportToDot("/opt/masterThesis/storm/build/tests_representative_x.dot"); + storm::dd::Bdd representative_y = bddX1Y0Z0.existsAbstractRepresentative({y.first}); + //representative_y.exportToDot("/opt/masterThesis/storm/build/tests_representative_y.dot"); + storm::dd::Bdd representative_z = bddX1Y0Z0.existsAbstractRepresentative({z.first}); + //representative_z.exportToDot("/opt/masterThesis/storm/build/tests_representative_z.dot"); +} + TEST(SylvanDd, AddGetMetaVariableTest) { std::shared_ptr> manager(new storm::dd::DdManager()); ASSERT_NO_THROW(manager->addMetaVariable("x", 1, 9));