Worked on Sylvan min/max ADD abstract w. representative.

More tests for existsRepr.


Former-commit-id: 08c5d6e9bb

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);
         

resources/3rdparty/sylvan/src/sylvan_mtbdd.h

@@ -307,7 +307,7 @@ TASK_DECL_3(MTBDD, mtbdd_abstract_op_max, MTBDD, MTBDD, int);
  * <f> 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 <a> and <b>, and abstract variables <vars> using summation.

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;
-}
+}
+
+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;	
+}

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 <var> or the negation of <var> */
+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))
+

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;

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);
+}

test/functional/storage/CuddDdTest.cpp

@@ -60,16 +60,45 @@ TEST(CuddDd, BddConstants) {
 
 TEST(CuddDd, BddExistAbstractRepresentative) {
 	std::shared_ptr<storm::dd::DdManager<storm::dd::DdType::CUDD>> manager(new storm::dd::DdManager<storm::dd::DdType::CUDD>());
+	
+	storm::dd::Bdd<storm::dd::DdType::CUDD> zero;
+    ASSERT_NO_THROW(zero = manager->getBddZero());
+	storm::dd::Bdd<storm::dd::DdType::CUDD> one;
+    ASSERT_NO_THROW(one = manager->getBddOne());
+	
 	std::pair<storm::expressions::Variable, storm::expressions::Variable> x;
 	std::pair<storm::expressions::Variable, storm::expressions::Variable> y;
 	std::pair<storm::expressions::Variable, storm::expressions::Variable> 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<storm::dd::DdType::CUDD> bddX0 = manager->getEncoding(x.first, 0);
 	storm::dd::Bdd<storm::dd::DdType::CUDD> bddX1 = manager->getEncoding(x.first, 1);
 	storm::dd::Bdd<storm::dd::DdType::CUDD> bddY0 = manager->getEncoding(y.first, 0);
+	storm::dd::Bdd<storm::dd::DdType::CUDD> bddY1 = manager->getEncoding(y.first, 1);
 	storm::dd::Bdd<storm::dd::DdType::CUDD> bddZ0 = manager->getEncoding(z.first, 0);
+	storm::dd::Bdd<storm::dd::DdType::CUDD> bddZ1 = manager->getEncoding(z.first, 1);
+
+	// Abstract from FALSE
+	storm::dd::Bdd<storm::dd::DdType::CUDD> 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<storm::dd::DdType::CUDD> 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<storm::dd::DdType::CUDD> 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<storm::dd::DdType::CUDD> 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<storm::dd::DdType::CUDD> bddX0 = manager->getEncoding(x.first, 0);
-	storm::dd::Bdd<storm::dd::DdType::CUDD> bddY1 = manager->getEncoding(y.first, 1);
-	storm::dd::Bdd<storm::dd::DdType::CUDD> bddZ1 = manager->getEncoding(z.first, 1);
-
 	storm::dd::Bdd<storm::dd::DdType::CUDD> bddX0Y0Z0 = (bddX0 && bddY0) && bddZ0;
 	storm::dd::Bdd<storm::dd::DdType::CUDD> 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<storm::dd::DdManager<storm::dd::DdType::CUDD>> manager(new storm::dd::DdManager<storm::dd::DdType::CUDD>());
+	
+	storm::dd::Add<storm::dd::DdType::CUDD, double> zero;
+    ASSERT_NO_THROW(zero = manager->template getAddZero<double>());
+	storm::dd::Add<storm::dd::DdType::CUDD, double> one;
+    ASSERT_NO_THROW(one = manager->template getAddOne<double>());
+	
+	std::pair<storm::expressions::Variable, storm::expressions::Variable> x;
+	std::pair<storm::expressions::Variable, storm::expressions::Variable> y;
+	std::pair<storm::expressions::Variable, storm::expressions::Variable> 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<storm::dd::DdType::CUDD, double> 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<storm::dd::DdType::CUDD, double> 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<storm::dd::DdType::CUDD, double> bddX1 = manager->getEncoding(x.first, 1);
+	storm::dd::Add<storm::dd::DdType::CUDD, double> bddY0 = manager->getEncoding(y.first, 0);
+	storm::dd::Add<storm::dd::DdType::CUDD, double> bddZ0 = manager->getEncoding(z.first, 0);
+
+	storm::dd::Add<storm::dd::DdType::CUDD, double> bddX1Y0Z0 = (bddX1 && bddY0) && bddZ0;
+	EXPECT_EQ(1ul, bddX1Y0Z0.getNonZeroCount());
+	EXPECT_EQ(1ul, bddX1Y0Z0.getLeafCount());
+	EXPECT_EQ(4ul, bddX1Y0Z0.getNodeCount());
+
+	storm::dd::Add<storm::dd::DdType::CUDD, double> 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<storm::dd::DdType::CUDD, double> 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<storm::dd::DdType::CUDD, double> 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<storm::dd::DdType::CUDD, double> 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<storm::dd::DdType::CUDD, double> bddX0 = manager->getEncoding(x.first, 0);
+	storm::dd::Add<storm::dd::DdType::CUDD, double> bddY1 = manager->getEncoding(y.first, 1);
+	storm::dd::Add<storm::dd::DdType::CUDD, double> bddZ1 = manager->getEncoding(z.first, 1);
+
+	storm::dd::Add<storm::dd::DdType::CUDD, double> bddX0Y0Z0 = (bddX0 && bddY0) && bddZ0;
+	storm::dd::Add<storm::dd::DdType::CUDD, double> bddX1Y1Z1 = (bddX1 && bddY1) && bddZ1;
+
+	storm::dd::Add<storm::dd::DdType::CUDD, double> bddAllTrueOrAllFalse = bddX0Y0Z0 || bddX1Y1Z1;
+	//bddAllTrueOrAllFalse.template toAdd<double>().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<storm::dd::DdManager<storm::dd::DdType::CUDD>> manager(new storm::dd::DdManager<storm::dd::DdType::CUDD>());

test/functional/storage/SylvanDdTest.cpp

@@ -63,16 +63,45 @@ TEST(SylvanDd, BddConstants) {
 
 TEST(SylvanDd, BddExistAbstractRepresentative) {
 	std::shared_ptr<storm::dd::DdManager<storm::dd::DdType::Sylvan>> manager(new storm::dd::DdManager<storm::dd::DdType::Sylvan>());
+	
+	storm::dd::Bdd<storm::dd::DdType::Sylvan> zero;
+    ASSERT_NO_THROW(zero = manager->getBddZero());
+	storm::dd::Bdd<storm::dd::DdType::Sylvan> one;
+    ASSERT_NO_THROW(one = manager->getBddOne());
+	
 	std::pair<storm::expressions::Variable, storm::expressions::Variable> x;
 	std::pair<storm::expressions::Variable, storm::expressions::Variable> y;
 	std::pair<storm::expressions::Variable, storm::expressions::Variable> 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<storm::dd::DdType::Sylvan> bddX0 = manager->getEncoding(x.first, 0);
 	storm::dd::Bdd<storm::dd::DdType::Sylvan> bddX1 = manager->getEncoding(x.first, 1);
 	storm::dd::Bdd<storm::dd::DdType::Sylvan> bddY0 = manager->getEncoding(y.first, 0);
+	storm::dd::Bdd<storm::dd::DdType::Sylvan> bddY1 = manager->getEncoding(y.first, 1);
 	storm::dd::Bdd<storm::dd::DdType::Sylvan> bddZ0 = manager->getEncoding(z.first, 0);
+	storm::dd::Bdd<storm::dd::DdType::Sylvan> bddZ1 = manager->getEncoding(z.first, 1);
+	
+	// Abstract from FALSE
+	storm::dd::Bdd<storm::dd::DdType::Sylvan> 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<storm::dd::DdType::Sylvan> 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<storm::dd::DdType::Sylvan> 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<storm::dd::DdType::Sylvan> 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<storm::dd::DdType::Sylvan> bddX0 = manager->getEncoding(x.first, 0);
-	storm::dd::Bdd<storm::dd::DdType::Sylvan> bddY1 = manager->getEncoding(y.first, 1);
-	storm::dd::Bdd<storm::dd::DdType::Sylvan> bddZ1 = manager->getEncoding(z.first, 1);
-
 	storm::dd::Bdd<storm::dd::DdType::Sylvan> bddX0Y0Z0 = (bddX0 && bddY0) && bddZ0;
 	storm::dd::Bdd<storm::dd::DdType::Sylvan> bddX1Y1Z1 = (bddX1 && bddY1) && bddZ1;