fixed bug in cudd minAbstractRepresentative, adapted tests, passing now

Former-commit-id: 7f45376343

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

@@ -1106,7 +1106,7 @@ cuddAddMinAbstractRepresentativeRecur(
         cuddRef(res1Inf);
         Cudd_IterDerefBdd(manager,res1);
         
-        res2Inf = cuddBddIteRecur(manager, Cudd_Not(tmp), res2, logicalZero);
+        res2Inf = cuddBddIteRecur(manager, tmp, logicalZero, res2);
         Cudd_IterDerefBdd(manager,tmp);
         if (res2Inf == NULL) {
             Cudd_IterDerefBdd(manager,res2);
@@ -1144,8 +1144,8 @@ cuddAddMinAbstractRepresentativeRecur(
         }
         cuddRef(res2);
         
-        int compl = (res1 == res2) ? 1 : Cudd_IsComplement(res2);
-        res = (res1 == res2) ? cuddUniqueInter(manager, (int) f->index, one, Cudd_Not(res1)) : cuddUniqueInter(manager, (int) f->index, Cudd_Regular(res2), Cudd_Not(res1));
+        int compl = (res1 == res2) ? 0 : Cudd_IsComplement(res2);
+        res = (res1 == res2) ? res1 : cuddUniqueInter(manager, (int) f->index, Cudd_Regular(res2), compl ? Cudd_Not(res1) : res1);
         if (res == NULL) {
             Cudd_IterDerefBdd(manager,res1);
             Cudd_IterDerefBdd(manager,res2);
@@ -1296,7 +1296,7 @@ cuddAddMaxAbstractRepresentativeRecur(
         Cudd_IterDerefBdd(manager,res1);
         
         cuddRef(zero);
-        res2Inf = cuddBddIteRecur(manager, Cudd_Not(tmp), res2, logicalZero);
+        res2Inf = cuddBddIteRecur(manager, tmp, logicalZero, res2);
         if (res2Inf == NULL) {
             Cudd_IterDerefBdd(manager,res2);
             Cudd_IterDerefBdd(manager,res1Inf);
@@ -1335,8 +1335,8 @@ cuddAddMaxAbstractRepresentativeRecur(
         }
         cuddRef(res2);
         
-        int compl = (res1 == res2) ? 1 : Cudd_IsComplement(res2);
-        res = (res1 == res2) ? cuddUniqueInter(manager, (int) f->index, one, Cudd_Not(res1)) : cuddUniqueInter(manager, (int) f->index, Cudd_Regular(res2), compl ? Cudd_Not(res1) : res1);
+        int compl = (res1 == res2) ? 0 : Cudd_IsComplement(res2);
+        res = (res1 == res2) ? res1 : cuddUniqueInter(manager, (int) f->index, Cudd_Regular(res2), compl ? Cudd_Not(res1) : res1);
         if (res == NULL) {
             Cudd_IterDerefBdd(manager,res1);
             Cudd_IterDerefBdd(manager,res2);

test/functional/storage/CuddDdTest.cpp

@@ -196,27 +196,23 @@ TEST(CuddDd, AddMinExistAbstractRepresentative) {
         + ((bddX0 && (bddY1 && bddZ0)).template toAdd<double>() * manager->template getConstant<double>(0.5))
         + ((bddX0 && (bddY0 && bddZ1)).template toAdd<double>() * manager->template getConstant<double>(1.0))
         + ((bddX0 && (bddY0 && bddZ0)).template toAdd<double>() * manager->template getConstant<double>(0.0));
-	complexAdd.exportToDot("test_CUDD_complexAdd.dot");
 	
 	// Abstract from FALSE
-	std::cout << "Before FALSE" << std::endl;
 	storm::dd::Bdd<storm::dd::DdType::CUDD> representative_false_x = addZero.minAbstractRepresentative({x.first});
 	EXPECT_EQ(0ul, representative_false_x.getNonZeroCount());
     EXPECT_EQ(1ul, representative_false_x.getLeafCount());
     EXPECT_EQ(2ul, representative_false_x.getNodeCount());
 	EXPECT_TRUE(representative_false_x == bddX0);
-	representative_false_x.exportToDot("test_CUDD_representative_false_x.dot");
-	bddX0.exportToDot("test_CUDD_bddX0.dot");
+//	representative_false_x.exportToDot("test_CUDD_representative_false_x.dot");
+//	bddX0.exportToDot("test_CUDD_bddX0.dot");
 
 	// Abstract from TRUE
-	std::cout << "Before TRUE" << std::endl;
 	storm::dd::Bdd<storm::dd::DdType::CUDD> representative_true_x = addOne.minAbstractRepresentative({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);
 	
-	std::cout << "Before TRUE xyz" << std::endl;
 	storm::dd::Bdd<storm::dd::DdType::CUDD> representative_true_xyz = addOne.minAbstractRepresentative({x.first, y.first, z.first});
 	EXPECT_EQ(0ul, representative_true_xyz.getNonZeroCount());
     EXPECT_EQ(1ul, representative_true_xyz.getLeafCount());
@@ -224,7 +220,6 @@ TEST(CuddDd, AddMinExistAbstractRepresentative) {
 	EXPECT_TRUE(representative_true_xyz == ((bddX0 && bddY0) && bddZ0));
 	
 	// Abstract x
-	std::cout << "Before x" << std::endl;
 	storm::dd::Bdd<storm::dd::DdType::CUDD> representative_complex_x = complexAdd.minAbstractRepresentative({x.first});
 	storm::dd::Bdd<storm::dd::DdType::CUDD> comparison_complex_x = (
 	     ((bddX0 && (bddY0 && bddZ0)))
@@ -236,11 +231,10 @@ TEST(CuddDd, AddMinExistAbstractRepresentative) {
     EXPECT_EQ(1ul, representative_complex_x.getLeafCount());
     EXPECT_EQ(3ul, representative_complex_x.getNodeCount());
 	EXPECT_TRUE(representative_complex_x == comparison_complex_x);
-	representative_complex_x.template toAdd<double>().exportToDot("test_CUDD_representative_complex_x.dot");
-	comparison_complex_x.template toAdd<double>().exportToDot("test_CUDD_comparison_complex_x.dot");
+//	representative_complex_x.template toAdd<double>().exportToDot("test_CUDD_representative_complex_x.dot");
+//	comparison_complex_x.template toAdd<double>().exportToDot("test_CUDD_comparison_complex_x.dot");
 	
 	// Abstract y
-	std::cout << "Before y" << std::endl;
 	storm::dd::Bdd<storm::dd::DdType::CUDD> representative_complex_y = complexAdd.minAbstractRepresentative({y.first});
 	storm::dd::Bdd<storm::dd::DdType::CUDD> comparison_complex_y = (
 	     ((bddX0 && (bddY0 && bddZ0)))
@@ -252,11 +246,10 @@ TEST(CuddDd, AddMinExistAbstractRepresentative) {
     EXPECT_EQ(1ul, representative_complex_y.getLeafCount());
     EXPECT_EQ(5ul, representative_complex_y.getNodeCount());
 	EXPECT_TRUE(representative_complex_y == comparison_complex_y);
-	representative_complex_y.template toAdd<double>().exportToDot("test_CUDD_representative_complex_y.dot");
-	comparison_complex_y.template toAdd<double>().exportToDot("test_CUDD_comparison_complex_y.dot");
+//	representative_complex_y.template toAdd<double>().exportToDot("test_CUDD_representative_complex_y.dot");
+//	comparison_complex_y.template toAdd<double>().exportToDot("test_CUDD_comparison_complex_y.dot");
 	
 	// Abstract z
-	std::cout << "Before z" << std::endl;
 	storm::dd::Bdd<storm::dd::DdType::CUDD> representative_complex_z = complexAdd.minAbstractRepresentative({z.first});
 	storm::dd::Bdd<storm::dd::DdType::CUDD> comparison_complex_z = (
 	     ((bddX0 && (bddY0 && bddZ0)))
@@ -264,23 +257,23 @@ TEST(CuddDd, AddMinExistAbstractRepresentative) {
 	  || ((bddX1 && (bddY0 && bddZ0)))
 	  || ((bddX1 && (bddY1 && bddZ1)))
 	);
-	EXPECT_EQ(0ul, representative_complex_z.getNonZeroCount());
+	EXPECT_EQ(4ul, representative_complex_z.getNonZeroCount());
     EXPECT_EQ(1ul, representative_complex_z.getLeafCount());
-    EXPECT_EQ(2ul, representative_complex_z.getNodeCount());
+    EXPECT_EQ(4ul, representative_complex_z.getNodeCount());
 	EXPECT_TRUE(representative_complex_z == comparison_complex_z);
-	representative_complex_z.template toAdd<double>().exportToDot("test_CUDD_representative_complex_z.dot");
-	comparison_complex_z.template toAdd<double>().exportToDot("test_CUDD_comparison_complex_z.dot");
+//    representative_complex_z.exportToDot("test_CUDD_representative_complex_z_bdd.dot");
+//	representative_complex_z.template toAdd<double>().exportToDot("test_CUDD_representative_complex_z.dot");
+//	comparison_complex_z.template toAdd<double>().exportToDot("test_CUDD_comparison_complex_z.dot");
 	
 	// Abstract x, y, z
-	std::cout << "Before x, y, z" << std::endl;
 	storm::dd::Bdd<storm::dd::DdType::CUDD> representative_complex_xyz = complexAdd.minAbstractRepresentative({x.first, y.first, z.first});
 	storm::dd::Bdd<storm::dd::DdType::CUDD> comparison_complex_xyz = (bddX0 && (bddY0 && bddZ0));
 	EXPECT_EQ(1ul, representative_complex_xyz.getNonZeroCount());
     EXPECT_EQ(1ul, representative_complex_xyz.getLeafCount());
     EXPECT_EQ(4ul, representative_complex_xyz.getNodeCount());
 	EXPECT_TRUE(representative_complex_xyz == comparison_complex_xyz);
-	representative_complex_xyz.template toAdd<double>().exportToDot("test_CUDD_representative_complex_xyz.dot");
-	comparison_complex_xyz.template toAdd<double>().exportToDot("test_CUDD_representative_complex_xyz.dot");
+//	representative_complex_xyz.template toAdd<double>().exportToDot("test_CUDD_representative_complex_xyz.dot");
+//	comparison_complex_xyz.template toAdd<double>().exportToDot("test_CUDD_representative_complex_xyz.dot");
 }
 
 TEST(CuddDd, AddGetMetaVariableTest) {