fixed some issues in CUDD (fixes provided by Fabio Somenzi)

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

@@ -1343,7 +1343,7 @@ cuddHashTableResize(
 	    while (item != NULL) {
 		next = item->next;
 		key = item->key;
-		posn = ddLCHash2(key[0], key[0], shift);
+		posn = ddLCHash1(key[0], shift);
 		item->next = buckets[posn];
 		buckets[posn] = item;
 		item = next;

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

@@ -1,3 +1,4 @@
+
 /**
   @file
 
@@ -1314,36 +1315,36 @@ Cudd_bddClosestCube(
   DdNode *g,
   int *distance)
 {
-    DdNode *res, *acube;
-    CUDD_VALUE_TYPE rdist;
+    DdNode *res, *acube = NULL;
+    CUDD_VALUE_TYPE rdist = DD_PLUS_INF_VAL;
+    CUDD_VALUE_TYPE epsilon = Cudd_ReadEpsilon(dd);
 
-    /* Compute the cube and distance as a single ADD. */
     do {
+        /* Compute the cube and distance as a single ADD. */
+        Cudd_SetEpsilon(dd,(CUDD_VALUE_TYPE)0.0);
 	dd->reordered = 0;
 	res = cuddBddClosestCube(dd,f,g,CUDD_CONST_INDEX + 1.0);
-    } while (dd->reordered == 1);
-    if (res == NULL) {
-        if (dd->errorCode == CUDD_TIMEOUT_EXPIRED && dd->timeoutHandler) {
-            dd->timeoutHandler(dd, dd->tohArg);
+        Cudd_SetEpsilon(dd,epsilon);
+        if (dd->reordered == 0) {
+            if (res == NULL) {
+                if (dd->errorCode == CUDD_TIMEOUT_EXPIRED && dd->timeoutHandler) {
+                    dd->timeoutHandler(dd, dd->tohArg);
+                }
+                return(NULL);
+            }
+            cuddRef(res);
+            /* Unpack distance and cube. */
+            acube = separateCube(dd, res, &rdist);
+            Cudd_RecursiveDeref(dd, res);
         }
-        return(NULL);
-    }
-    cuddRef(res);
-
-    /* Unpack distance and cube. */
-    do {
-	dd->reordered = 0;
-	acube = separateCube(dd, res, &rdist);
     } while (dd->reordered == 1);
     if (acube == NULL) {
-	Cudd_RecursiveDeref(dd, res);
         if (dd->errorCode == CUDD_TIMEOUT_EXPIRED && dd->timeoutHandler) {
             dd->timeoutHandler(dd, dd->tohArg);
         }
-	return(NULL);
+        return(NULL);
     }
     cuddRef(acube);
-    Cudd_RecursiveDeref(dd, res);
 
     /* Convert cube from ADD to BDD. */
     do {

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

@@ -592,10 +592,7 @@ Cudd_SharingSize(
 //     * to deal with functions that depend on more than 1023, but less
 //     * than 2044 variables and don't have too many minterms.
 //     */
-//    printf("vars: %i, min_exp: %.400f, %i\n", nvars, DBL_MIN_EXP, DBL_MIN_EXP);
-//    printf("1: %f, 2: %i \n", (double)(nvars + DBL_MIN_EXP), (nvars + DBL_MIN_EXP));
 //    max = pow(2.0,(double)(nvars + DBL_MIN_EXP));
-//    printf("max: %f, DD_PLUS_INF_VAL: %.50f\n", max, DD_PLUS_INF_VAL);
 //    if (max >= DD_PLUS_INF_VAL) {
 //        return((double)CUDD_OUT_OF_MEM);
 //    }
@@ -615,10 +612,8 @@ Cudd_SharingSize(
 //        /* Minterm count is too large to be scaled back. */
 //        return(DD_PLUS_INF_VAL);
 //    } else {
-//        printf("in third case: %.400f\n", res);
 //        /* Undo the scaling. */
 //        res *= pow(2.0,(double)-DBL_MIN_EXP);
-//        printf("after rescaling: %f\n", res);
 //        return(res);
 //    }
 //

src/storm/settings/modules/CuddSettings.cpp

@@ -20,7 +20,7 @@ namespace storm {
             const std::string CuddSettings::reorderOptionName = "reorder";
             
             CuddSettings::CuddSettings() : ModuleSettings(moduleName) {
-                this->addOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, true, "Sets the precision used by Cudd.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision up to which to constants are considered to be different.").setDefaultValueDouble(1e-15).addValidatorDouble(ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(0.0, 1.0)).build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, true, "Sets the precision used by Cudd.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision up to which to constants are considered to be different.").setDefaultValueDouble(1e-15).addValidatorDouble(ArgumentValidatorFactory::createDoubleRangeValidatorIncluding(0.0, 1.0)).build()).build());
                 
                 this->addOption(storm::settings::OptionBuilder(moduleName, maximalMemoryOptionName, true, "Sets the upper bound of memory available to Cudd in MB.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("value", "The memory available to Cudd (0 means unlimited).").setDefaultValueUnsignedInteger(4096).build()).build());