From c184f6a5413d37583c811c8b96834703b99442fe Mon Sep 17 00:00:00 2001 From: PBerger Date: Mon, 22 Aug 2016 20:36:28 +0200 Subject: [PATCH] Worked on Sylvan min/max ADD abstract w. representative. More tests for existsRepr. Former-commit-id: 08c5d6e9bb6d15cb8c60f826d7748d7670d7bfb0 --- .../3rdparty/sylvan/src/sylvan_bdd_storm.c | 34 ++- resources/3rdparty/sylvan/src/sylvan_mtbdd.h | 2 +- .../3rdparty/sylvan/src/sylvan_mtbdd_storm.c | 225 +++++++++++++++++- .../3rdparty/sylvan/src/sylvan_mtbdd_storm.h | 34 ++- .../sylvan/src/sylvan_obj_mtbdd_storm.hpp | 10 + .../3rdparty/sylvan/src/sylvan_obj_storm.cpp | 13 + test/functional/storage/CuddDdTest.cpp | 132 +++++++++- test/functional/storage/SylvanDdTest.cpp | 35 ++- 8 files changed, 469 insertions(+), 16 deletions(-) diff --git a/resources/3rdparty/sylvan/src/sylvan_bdd_storm.c b/resources/3rdparty/sylvan/src/sylvan_bdd_storm.c index 3841049e8..4f0d3f81d 100644 --- a/resources/3rdparty/sylvan/src/sylvan_bdd_storm.c +++ b/resources/3rdparty/sylvan/src/sylvan_bdd_storm.c @@ -16,7 +16,20 @@ TASK_IMPL_3(BDD, sylvan_existsRepresentative, BDD, a, BDD, variables, BDDVAR, pr return sylvan_true; } else { //printf("return in preprocessing...3\n"); - return variables; + BDD _v = sylvan_set_next(variables); + BDD res = CALL(sylvan_existsRepresentative, a, _v, prev_level); + if (res == sylvan_invalid) { + return sylvan_invalid; + } + sylvan_ref(res); + + BDD res1 = sylvan_ite(sylvan_ithvar(bddnode_getvariable(GETNODE(variables))), sylvan_false, res); + if (res1 == sylvan_invalid) { + sylvan_deref(res); + return sylvan_invalid; + } + sylvan_deref(res); + return res1; } } else { return a; @@ -67,7 +80,24 @@ TASK_IMPL_3(BDD, sylvan_existsRepresentative, BDD, a, BDD, variables, BDDVAR, pr return sylvan_invalid; } if (res1 == sylvan_true) { - return sylvan_not(variables); + BDD res = CALL(sylvan_existsRepresentative, a, _v, level); + if (res == sylvan_invalid) { + return sylvan_invalid; + } + sylvan_ref(res); + + BDD res1 = sylvan_ite(sylvan_ithvar(vv), sylvan_false, res); + + if (res1 == sylvan_invalid) { + sylvan_deref(res); + return sylvan_invalid; + } + sylvan_deref(res); + + //printf("return after abstr. var that does not appear in f...\n"); + return res1; + + //return sylvan_not(variables); } sylvan_ref(res1); diff --git a/resources/3rdparty/sylvan/src/sylvan_mtbdd.h b/resources/3rdparty/sylvan/src/sylvan_mtbdd.h index 1a7de3f57..60d484f50 100644 --- a/resources/3rdparty/sylvan/src/sylvan_mtbdd.h +++ b/resources/3rdparty/sylvan/src/sylvan_mtbdd.h @@ -307,7 +307,7 @@ TASK_DECL_3(MTBDD, mtbdd_abstract_op_max, MTBDD, MTBDD, int); * must be a Boolean MTBDD (or standard BDD). */ TASK_DECL_3(MTBDD, mtbdd_ite, MTBDD, MTBDD, MTBDD); -#define mtbdd_ite(f, g, h) CALL(mtbdd_ite, f, g, h); +#define mtbdd_ite(f, g, h) CALL(mtbdd_ite, f, g, h) /** * Multiply and , and abstract variables using summation. diff --git a/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.c b/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.c index 2d0796a40..87e9bb590 100644 --- a/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.c +++ b/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.c @@ -580,4 +580,227 @@ int mtbdd_iszero(MTBDD dd) { int mtbdd_isnonzero(MTBDD dd) { return mtbdd_iszero(dd) ? 0 : 1; -} \ No newline at end of file +} + +MTBDD +mtbdd_ithvar(uint32_t level) { + return mtbdd_makenode(level, mtbdd_false, mtbdd_true); +} + +TASK_IMPL_2(MTBDD, mtbdd_op_complement, 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); + if (v == 0) { + return mtbdd_int64(1); + } else { + return mtbdd_int64(0); + } + } else if (mtbddnode_gettype(na) == 1) { + double d = mtbdd_getdouble(a); + if (d == 0.0) { + return mtbdd_double(1.0); + } else { + return mtbdd_double(0.0); + } + } else if (mtbddnode_gettype(na) == 2) { + printf("ERROR: mtbdd_op_complement type FRACTION.\n"); + assert(0); + } +#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) + else if ((mtbddnode_gettype(na) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID)) { + printf("ERROR: mtbdd_op_complement type SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID.\n"); + assert(0); + } +#endif + } + + return mtbdd_invalid; + (void)k; // unused variable +} + +TASK_IMPL_3(MTBDD, mtbdd_minExistsRepresentative, MTBDD, a, MTBDD, variables, uint32_t, prev_level) { + MTBDD zero = mtbdd_false; + + /* Maybe perform garbage collection */ + sylvan_gc_test(); + + /* Cube is guaranteed to be a cube at this point. */ + if (mtbdd_isleaf(a)) { + if (mtbdd_set_isempty(variables)) { + return a; // FIXME? + } else { + return variables; + } + } + + mtbddnode_t na = GETNODE(a); + uint32_t va = mtbddnode_getvariable(na); + mtbddnode_t nv = GETNODE(variables); + uint32_t vv = mtbddnode_getvariable(nv); + + /* Abstract a variable that does not appear in a. */ + if (va > vv) { + MTBDD _v = mtbdd_set_next(variables); + MTBDD res = CALL(mtbdd_minExistsRepresentative, a, _v, va); + if (res == mtbdd_invalid) { + return mtbdd_invalid; + } + + // Fill in the missing variables to make representative unique. + mtbdd_ref(res); + MTBDD res1 = mtbdd_ite(mtbdd_ithvar(vv), zero, res); + if (res1 == mtbdd_invalid) { + mtbdd_deref(res); + return mtbdd_invalid; + } + mtbdd_deref(res); + return res1; + } + + /* TODO: Caching here. */ + /*if ((res = cuddCacheLookup2(manager, Cudd_addMinAbstractRepresentative, f, cube)) != NULL) { + return(res); + }*/ + + + MTBDD E = mtbdd_getlow(a); + MTBDD T = mtbdd_gethigh(a); + + /* If the two indices are the same, so are their levels. */ + if (va == vv) { + MTBDD _v = mtbdd_set_next(variables); + MTBDD res1 = CALL(mtbdd_minExistsRepresentative, E, _v, va); + if (res1 == mtbdd_invalid) { + return mtbdd_invalid; + } + mtbdd_ref(res1); + + MTBDD res2 = CALL(mtbdd_minExistsRepresentative, T, _v, va); + if (res2 == mtbdd_invalid) { + mtbdd_deref(res1); + return mtbdd_invalid; + } + mtbdd_ref(res2); + + MTBDD left = mtbdd_abstract_min(E, _v); + if (left == mtbdd_invalid) { + mtbdd_deref(res1); + mtbdd_deref(res2); + return mtbdd_invalid; + } + mtbdd_ref(left); + + MTBDD right = mtbdd_abstract_min(T, _v); + if (right == mtbdd_invalid) { + mtbdd_deref(res1); + mtbdd_deref(res2); + mtbdd_deref(left); + return mtbdd_invalid; + } + mtbdd_ref(right); + + MTBDD tmp = mtbdd_less_or_equal_as_bdd(left, right); + if (tmp == mtbdd_invalid) { + mtbdd_deref(res1); + mtbdd_deref(res2); + mtbdd_deref(left); + mtbdd_deref(right); + return mtbdd_invalid; + } + mtbdd_ref(tmp); + + mtbdd_deref(left); + mtbdd_deref(right); + + MTBDD res1Inf = mtbdd_ite(tmp, res1, zero); + if (res1Inf == mtbdd_invalid) { + mtbdd_deref(res1); + mtbdd_deref(res2); + mtbdd_deref(tmp); + return mtbdd_invalid; + } + mtbdd_ref(res1Inf); + mtbdd_deref(res1); + + MTBDD tmp2 = mtbdd_get_complement(tmp); + if (tmp2 == mtbdd_invalid) { + mtbdd_deref(res2); + mtbdd_deref(left); + mtbdd_deref(right); + mtbdd_deref(tmp); + return mtbdd_invalid; + } + mtbdd_ref(tmp2); + mtbdd_deref(tmp); + + MTBDD res2Inf = mtbdd_ite(tmp2, res2, zero); + if (res2Inf == mtbdd_invalid) { + mtbdd_deref(res2); + mtbdd_deref(res1Inf); + mtbdd_deref(tmp2); + return mtbdd_invalid; + } + mtbdd_ref(res2Inf); + mtbdd_deref(res2); + mtbdd_deref(tmp2); + + MTBDD res = (res1Inf == res2Inf) ? mtbdd_ite(mtbdd_ithvar(va), zero, res1Inf) : mtbdd_ite(mtbdd_ithvar(va), res2Inf, res1Inf); + + if (res == mtbdd_invalid) { + mtbdd_deref(res1Inf); + mtbdd_deref(res2Inf); + return mtbdd_invalid; + } + mtbdd_ref(res); + mtbdd_deref(res1Inf); + mtbdd_deref(res2Inf); + + /* TODO: Caching here. */ + //cuddCacheInsert2(manager, Cudd_addMinAbstractRepresentative, f, cube, res); + + mtbdd_deref(res); + return res; + } + else { /* if (cuddI(manager,f->index) < cuddI(manager,cube->index)) */ + MTBDD res1 = CALL(mtbdd_minExistsRepresentative, E, variables, va); + if (res1 == mtbdd_invalid) { + return mtbdd_invalid; + } + mtbdd_ref(res1); + MTBDD res2 = CALL(mtbdd_minExistsRepresentative, T, variables, va); + if (res2 == mtbdd_invalid) { + mtbdd_deref(res1); + return mtbdd_invalid; + } + mtbdd_ref(res2); + + MTBDD res = (res1 == res2) ? mtbdd_ite(mtbdd_ithvar(va), zero, res1) : mtbdd_ite(mtbdd_ithvar(va), res2, res1); + if (res == mtbdd_invalid) { + mtbdd_deref(res1); + mtbdd_deref(res2); + return mtbdd_invalid; + } + mtbdd_deref(res1); + mtbdd_deref(res2); + /* TODO: Caching here. */ + //cuddCacheInsert2(manager, Cudd_addMinAbstractRepresentative, f, cube, res); + return res; + } + + // Prevent unused variable warning + (void)prev_level; +} + +TASK_IMPL_3(MTBDD, mtbdd_maxExistsRepresentative, MTBDD, a, MTBDD, variables, uint32_t, prev_level) { + (void)variables; + (void)prev_level; + return a; +} diff --git a/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.h b/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.h index a35fd8398..d1119438b 100644 --- a/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.h +++ b/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.h @@ -71,14 +71,14 @@ TASK_DECL_1(MTBDD, mtbdd_not_zero, MTBDD) #define mtbdd_not_zero(dd) CALL(mtbdd_not_zero, dd) /** - * Monad that floors all values Double and Fraction values. + * Monad that floors all Double and Fraction values. */ TASK_DECL_2(MTBDD, mtbdd_op_floor, MTBDD, size_t) TASK_DECL_1(MTBDD, mtbdd_floor, MTBDD) #define mtbdd_floor(dd) CALL(mtbdd_floor, dd) /** - * Monad that ceils all values Double and Fraction values. + * Monad that ceils all Double and Fraction values. */ TASK_DECL_2(MTBDD, mtbdd_op_ceil, MTBDD, size_t) TASK_DECL_1(MTBDD, mtbdd_ceil, MTBDD) @@ -109,3 +109,33 @@ int mtbdd_iszero(MTBDD); int mtbdd_isnonzero(MTBDD); #define mtbdd_regular(dd) (dd & ~mtbdd_complement) + +#define mtbdd_set_next(set) (mtbdd_gethigh(set)) +#define mtbdd_set_isempty(set) (set == mtbdd_true) + +/* Create a MTBDD representing just or the negation of */ +MTBDD mtbdd_ithvar(uint32_t var); + +/** + * Unary operation Complement. + * Supported domains: Integer, Real + */ +TASK_DECL_2(MTBDD, mtbdd_op_complement, MTBDD, size_t); + +/** + * Compute the complement of a. + */ +#define mtbdd_get_complement(a) mtbdd_uapply(a, TASK(mtbdd_op_complement), 0) + +/** + * Just like mtbdd_abstract_min, but instead of abstracting the variables in the given cube, picks a unique representative that realizes the minimal function value. + */ +TASK_DECL_3(MTBDD, mtbdd_minExistsRepresentative, MTBDD, MTBDD, uint32_t); +#define mtbdd_minExistsRepresentative(a, vars) (CALL(mtbdd_minExistsRepresentative, a, vars, 0)) + +/** + * Just like mtbdd_abstract_max but instead of abstracting the variables in the given cube, picks a unique representative that realizes the maximal function value. + */ +TASK_DECL_3(MTBDD, mtbdd_maxExistsRepresentative, MTBDD, MTBDD, uint32_t); +#define mtbdd_maxExistsRepresentative(a, vars) (CALL(mtbdd_maxExistsRepresentative, a, vars, 0)) + diff --git a/resources/3rdparty/sylvan/src/sylvan_obj_mtbdd_storm.hpp b/resources/3rdparty/sylvan/src/sylvan_obj_mtbdd_storm.hpp index 92dd1172c..87ab6735e 100644 --- a/resources/3rdparty/sylvan/src/sylvan_obj_mtbdd_storm.hpp +++ b/resources/3rdparty/sylvan/src/sylvan_obj_mtbdd_storm.hpp @@ -32,6 +32,16 @@ Mtbdd AbstractPlusRF(const BddSet &variables) const; #endif + /** + * @brief Computes abstraction by minimum + */ + Mtbdd AbstractMinRepresentative(const BddSet &variables) const; + + /** + * @brief Computes abstraction by maximum + */ + Mtbdd AbstractMaxRepresentative(const BddSet &variables) const; + Bdd NotZero() const; Bdd Equals(const Mtbdd& other) const; diff --git a/resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp b/resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp index e055478f3..7ef934fbe 100644 --- a/resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp +++ b/resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp @@ -188,3 +188,16 @@ Mtbdd::GetShaHash() const { return std::string(buf); } +Mtbdd +Mtbdd::AbstractMinRepresentative(const BddSet &variables) const +{ + LACE_ME; + return mtbdd_minExistsRepresentative(mtbdd, variables.set.bdd); +} + +Mtbdd +Mtbdd::AbstractMaxRepresentative(const BddSet &variables) const +{ + LACE_ME; + return mtbdd_maxExistsRepresentative(mtbdd, variables.set.bdd); +} diff --git a/test/functional/storage/CuddDdTest.cpp b/test/functional/storage/CuddDdTest.cpp index 763fa0a69..b499da1b7 100644 --- a/test/functional/storage/CuddDdTest.cpp +++ b/test/functional/storage/CuddDdTest.cpp @@ -60,16 +60,45 @@ TEST(CuddDd, BddConstants) { TEST(CuddDd, BddExistAbstractRepresentative) { std::shared_ptr> manager(new storm::dd::DdManager()); + + storm::dd::Bdd zero; + ASSERT_NO_THROW(zero = manager->getBddZero()); + storm::dd::Bdd one; + ASSERT_NO_THROW(one = manager->getBddOne()); + 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 bddX0 = manager->getEncoding(x.first, 0); storm::dd::Bdd bddX1 = manager->getEncoding(x.first, 1); storm::dd::Bdd bddY0 = manager->getEncoding(y.first, 0); + storm::dd::Bdd bddY1 = manager->getEncoding(y.first, 1); storm::dd::Bdd bddZ0 = manager->getEncoding(z.first, 0); + storm::dd::Bdd bddZ1 = manager->getEncoding(z.first, 1); + + // Abstract from FALSE + storm::dd::Bdd representative_false_x = zero.existsAbstractRepresentative({x.first}); + EXPECT_EQ(0ul, representative_false_x.getNonZeroCount()); + EXPECT_EQ(1ul, representative_false_x.getLeafCount()); + EXPECT_EQ(1ul, representative_false_x.getNodeCount()); + EXPECT_TRUE(representative_false_x == zero); + + // Abstract from TRUE + storm::dd::Bdd representative_true_x = one.existsAbstractRepresentative({x.first}); + EXPECT_EQ(0ul, representative_true_x.getNonZeroCount()); + EXPECT_EQ(1ul, representative_true_x.getLeafCount()); + EXPECT_EQ(1ul, representative_true_x.getNodeCount()); + EXPECT_TRUE(representative_true_x == bddX0); + + storm::dd::Bdd representative_true_xyz = one.existsAbstractRepresentative({x.first, y.first, z.first}); + EXPECT_EQ(0ul, representative_true_xyz.getNonZeroCount()); + EXPECT_EQ(1ul, representative_true_xyz.getLeafCount()); + EXPECT_EQ(4ul, representative_true_xyz.getNodeCount()); + EXPECT_TRUE(representative_true_xyz == ((bddX0 && bddY0) && bddZ0)); storm::dd::Bdd bddX1Y0Z0 = (bddX1 && bddY0) && bddZ0; EXPECT_EQ(1ul, bddX1Y0Z0.getNonZeroCount()); @@ -100,10 +129,6 @@ TEST(CuddDd, BddExistAbstractRepresentative) { EXPECT_EQ(4ul, representative_xyz.getNodeCount()); EXPECT_TRUE(bddX1Y0Z0 == representative_xyz); - storm::dd::Bdd bddX0 = manager->getEncoding(x.first, 0); - storm::dd::Bdd bddY1 = manager->getEncoding(y.first, 1); - storm::dd::Bdd bddZ1 = manager->getEncoding(z.first, 1); - storm::dd::Bdd bddX0Y0Z0 = (bddX0 && bddY0) && bddZ0; storm::dd::Bdd bddX1Y1Z1 = (bddX1 && bddY1) && bddZ1; @@ -134,6 +159,103 @@ TEST(CuddDd, BddExistAbstractRepresentative) { EXPECT_EQ(4ul, representative_xyz.getNodeCount()); EXPECT_TRUE(bddX0Y0Z0 == representative_xyz); } +/* +TEST(CuddDd, AddMinExistAbstractRepresentative) { + std::shared_ptr> manager(new storm::dd::DdManager()); + + storm::dd::Add zero; + ASSERT_NO_THROW(zero = manager->template getAddZero()); + storm::dd::Add one; + ASSERT_NO_THROW(one = manager->template getAddOne()); + + 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)); + + // Abstract from FALSE + storm::dd::Add representative_false_x = zero.existsAbstractRepresentative({x.first}); + EXPECT_EQ(0ul, representative_false_x.getNonZeroCount()); + EXPECT_EQ(1ul, representative_false_x.getLeafCount()); + EXPECT_EQ(1ul, representative_false_x.getNodeCount()); + EXPECT_TRUE(representative_false_x == zero); + + // Abstract from TRUE + storm::dd::Add representative_true_x = one.existsAbstractRepresentative({x.first}); + EXPECT_EQ(1ul, representative_true_x.getNonZeroCount()); + EXPECT_EQ(1ul, representative_true_x.getLeafCount()); + EXPECT_EQ(1ul, representative_true_x.getNodeCount()); + EXPECT_TRUE(representative_true_x == manager->getEncoding(x.first, 0)); + + storm::dd::Add bddX1 = manager->getEncoding(x.first, 1); + storm::dd::Add bddY0 = manager->getEncoding(y.first, 0); + storm::dd::Add bddZ0 = manager->getEncoding(z.first, 0); + + storm::dd::Add bddX1Y0Z0 = (bddX1 && bddY0) && bddZ0; + EXPECT_EQ(1ul, bddX1Y0Z0.getNonZeroCount()); + EXPECT_EQ(1ul, bddX1Y0Z0.getLeafCount()); + EXPECT_EQ(4ul, bddX1Y0Z0.getNodeCount()); + + storm::dd::Add representative_x = bddX1Y0Z0.existsAbstractRepresentative({x.first}); + EXPECT_EQ(1ul, representative_x.getNonZeroCount()); + EXPECT_EQ(1ul, representative_x.getLeafCount()); + EXPECT_EQ(4ul, representative_x.getNodeCount()); + EXPECT_TRUE(bddX1Y0Z0 == representative_x); + + storm::dd::Add representative_y = bddX1Y0Z0.existsAbstractRepresentative({y.first}); + EXPECT_EQ(1ul, representative_y.getNonZeroCount()); + EXPECT_EQ(1ul, representative_y.getLeafCount()); + EXPECT_EQ(4ul, representative_y.getNodeCount()); + EXPECT_TRUE(bddX1Y0Z0 == representative_y); + + storm::dd::Add representative_z = bddX1Y0Z0.existsAbstractRepresentative({z.first}); + EXPECT_EQ(1ul, representative_z.getNonZeroCount()); + EXPECT_EQ(1ul, representative_z.getLeafCount()); + EXPECT_EQ(4ul, representative_z.getNodeCount()); + EXPECT_TRUE(bddX1Y0Z0 == representative_z); + + storm::dd::Add representative_xyz = bddX1Y0Z0.existsAbstractRepresentative({x.first, y.first, z.first}); + EXPECT_EQ(1ul, representative_xyz.getNonZeroCount()); + EXPECT_EQ(1ul, representative_xyz.getLeafCount()); + EXPECT_EQ(4ul, representative_xyz.getNodeCount()); + EXPECT_TRUE(bddX1Y0Z0 == representative_xyz); + + storm::dd::Add bddX0 = manager->getEncoding(x.first, 0); + storm::dd::Add bddY1 = manager->getEncoding(y.first, 1); + storm::dd::Add bddZ1 = manager->getEncoding(z.first, 1); + + storm::dd::Add bddX0Y0Z0 = (bddX0 && bddY0) && bddZ0; + storm::dd::Add bddX1Y1Z1 = (bddX1 && bddY1) && bddZ1; + + storm::dd::Add bddAllTrueOrAllFalse = bddX0Y0Z0 || bddX1Y1Z1; + //bddAllTrueOrAllFalse.template toAdd().exportToDot("test_cudd_addAllTrueOrAllFalse.dot"); + + representative_x = bddAllTrueOrAllFalse.existsAbstractRepresentative({x.first}); + EXPECT_EQ(2ul, representative_x.getNonZeroCount()); + EXPECT_EQ(1ul, representative_x.getLeafCount()); + EXPECT_EQ(5ul, representative_x.getNodeCount()); + EXPECT_TRUE(bddAllTrueOrAllFalse == representative_x); + + representative_y = bddAllTrueOrAllFalse.existsAbstractRepresentative({y.first}); + EXPECT_EQ(2ul, representative_y.getNonZeroCount()); + EXPECT_EQ(1ul, representative_y.getLeafCount()); + EXPECT_EQ(5ul, representative_y.getNodeCount()); + EXPECT_TRUE(bddAllTrueOrAllFalse == representative_y); + + representative_z = bddAllTrueOrAllFalse.existsAbstractRepresentative({z.first}); + EXPECT_EQ(2ul, representative_z.getNonZeroCount()); + EXPECT_EQ(1ul, representative_z.getLeafCount()); + EXPECT_EQ(5ul, representative_z.getNodeCount()); + EXPECT_TRUE(bddAllTrueOrAllFalse == representative_z); + + representative_xyz = bddAllTrueOrAllFalse.existsAbstractRepresentative({x.first, y.first, z.first}); + EXPECT_EQ(1ul, representative_xyz.getNonZeroCount()); + EXPECT_EQ(1ul, representative_xyz.getLeafCount()); + EXPECT_EQ(4ul, representative_xyz.getNodeCount()); + EXPECT_TRUE(bddX0Y0Z0 == representative_xyz); +}*/ TEST(CuddDd, AddGetMetaVariableTest) { std::shared_ptr> manager(new storm::dd::DdManager()); diff --git a/test/functional/storage/SylvanDdTest.cpp b/test/functional/storage/SylvanDdTest.cpp index 5b0c26b47..8b5c38859 100644 --- a/test/functional/storage/SylvanDdTest.cpp +++ b/test/functional/storage/SylvanDdTest.cpp @@ -63,16 +63,45 @@ TEST(SylvanDd, BddConstants) { TEST(SylvanDd, BddExistAbstractRepresentative) { std::shared_ptr> manager(new storm::dd::DdManager()); + + storm::dd::Bdd zero; + ASSERT_NO_THROW(zero = manager->getBddZero()); + storm::dd::Bdd one; + ASSERT_NO_THROW(one = manager->getBddOne()); + 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 bddX0 = manager->getEncoding(x.first, 0); storm::dd::Bdd bddX1 = manager->getEncoding(x.first, 1); storm::dd::Bdd bddY0 = manager->getEncoding(y.first, 0); + storm::dd::Bdd bddY1 = manager->getEncoding(y.first, 1); storm::dd::Bdd bddZ0 = manager->getEncoding(z.first, 0); + storm::dd::Bdd bddZ1 = manager->getEncoding(z.first, 1); + + // Abstract from FALSE + storm::dd::Bdd representative_false_x = zero.existsAbstractRepresentative({x.first}); + EXPECT_EQ(0ul, representative_false_x.getNonZeroCount()); + EXPECT_EQ(1ul, representative_false_x.getLeafCount()); + EXPECT_EQ(1ul, representative_false_x.getNodeCount()); + EXPECT_TRUE(representative_false_x == zero); + + // Abstract from TRUE + storm::dd::Bdd representative_true_x = one.existsAbstractRepresentative({x.first}); + EXPECT_EQ(0ul, representative_true_x.getNonZeroCount()); + EXPECT_EQ(1ul, representative_true_x.getLeafCount()); + EXPECT_EQ(2ul, representative_true_x.getNodeCount()); + EXPECT_TRUE(representative_true_x == bddX0); + + storm::dd::Bdd representative_true_xyz = one.existsAbstractRepresentative({x.first, y.first, z.first}); + EXPECT_EQ(0ul, representative_true_xyz.getNonZeroCount()); + EXPECT_EQ(1ul, representative_true_xyz.getLeafCount()); + EXPECT_EQ(4ul, representative_true_xyz.getNodeCount()); + EXPECT_TRUE(representative_true_xyz == ((bddX0 && bddY0) && bddZ0)); storm::dd::Bdd bddX1Y0Z0 = (bddX1 && bddY0) && bddZ0; EXPECT_EQ(1ul, bddX1Y0Z0.getNonZeroCount()); @@ -103,10 +132,6 @@ TEST(SylvanDd, BddExistAbstractRepresentative) { EXPECT_EQ(4ul, representative_xyz.getNodeCount()); EXPECT_TRUE(bddX1Y0Z0 == representative_xyz); - storm::dd::Bdd bddX0 = manager->getEncoding(x.first, 0); - storm::dd::Bdd bddY1 = manager->getEncoding(y.first, 1); - storm::dd::Bdd bddZ1 = manager->getEncoding(z.first, 1); - storm::dd::Bdd bddX0Y0Z0 = (bddX0 && bddY0) && bddZ0; storm::dd::Bdd bddX1Y1Z1 = (bddX1 && bddY1) && bddZ1;