From bda9a797e88367e1164560584902266fce09a221 Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 28 Jul 2017 22:04:43 +0200 Subject: [PATCH] fixed some issues in CUDD (fixes provided by Fabio Somenzi) --- .../3rdparty/cudd-3.0.0/cudd/cuddLCache.c | 2 +- .../3rdparty/cudd-3.0.0/cudd/cuddPriority.c | 37 ++++++++++--------- resources/3rdparty/cudd-3.0.0/cudd/cuddUtil.c | 5 --- src/storm/settings/modules/CuddSettings.cpp | 2 +- 4 files changed, 21 insertions(+), 25 deletions(-) diff --git a/resources/3rdparty/cudd-3.0.0/cudd/cuddLCache.c b/resources/3rdparty/cudd-3.0.0/cudd/cuddLCache.c index b439187bf..7983e6428 100644 --- a/resources/3rdparty/cudd-3.0.0/cudd/cuddLCache.c +++ b/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; diff --git a/resources/3rdparty/cudd-3.0.0/cudd/cuddPriority.c b/resources/3rdparty/cudd-3.0.0/cudd/cuddPriority.c index dfb530f14..78c0633cd 100644 --- a/resources/3rdparty/cudd-3.0.0/cudd/cuddPriority.c +++ b/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 { diff --git a/resources/3rdparty/cudd-3.0.0/cudd/cuddUtil.c b/resources/3rdparty/cudd-3.0.0/cudd/cuddUtil.c index 0271fa2bc..45cb503a2 100644 --- a/resources/3rdparty/cudd-3.0.0/cudd/cuddUtil.c +++ b/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); // } // diff --git a/src/storm/settings/modules/CuddSettings.cpp b/src/storm/settings/modules/CuddSettings.cpp index e680276bf..a10ec1bbc 100644 --- a/src/storm/settings/modules/CuddSettings.cpp +++ b/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());