Fixed CUDD and Sylvan existsRepresentative.

Former-commit-id: e3ec69ab37

resources/3rdparty/cudd-3.0.0/cudd/cuddBddAbs.c

@@ -542,12 +542,27 @@ cuddBddExistAbstractRepresentativeRecur(
         if (cube == one) {
 //            printf("return in preprocessing...\n");
             return one;
-        }
+        } else {
+			res = cuddBddExistAbstractRepresentativeRecur(manager, f, cuddT(cube));
+			if (res == NULL) {
+				return(NULL);
+			}
+			cuddRef(res);
+			
+			res1 = cuddBddIteRecur(manager, manager->vars[cube->index], zero, res);
+			if (res1 == NULL) {
+				Cudd_IterDerefBdd(manager,res);
+				Cudd_IterDerefBdd(manager,zero);
+				return(NULL);
+			}
+			cuddDeref(res);
+			return(res1);
+		}
     } else if (cube == one) {
 //        printf("return in preprocessing...\n");
         return f;
     }
-    /* From now on, cube is non-constant, but f might be constant. */
+    /* From now on, cube and f are non-constant. */
     
 //    printf("F perm %i and cube perm %i\n", manager->perm[F->index], manager->perm[cube->index]);
     

resources/3rdparty/sylvan/src/sylvan_bdd_storm.c

@@ -80,24 +80,7 @@ TASK_IMPL_3(BDD, sylvan_existsRepresentative, BDD, a, BDD, variables, BDDVAR, pr
             return sylvan_invalid;
         }
         if (res1 == sylvan_true) {
-			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);
+			return sylvan_not(variables);
         }
         sylvan_ref(res1);
         

test/functional/storage/CuddDdTest.cpp

@@ -91,7 +91,7 @@ TEST(CuddDd, BddExistAbstractRepresentative) {
 	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_EQ(2ul, 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});