From 671797738aea3e58313f51075f3629047ecba38c Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 27 Jun 2014 17:28:20 +0200 Subject: [PATCH] Now the parameter that is set for dynamic reordering actually gets passed to CUDD. Former-commit-id: 46676dc9d1c6e9a0bcbe8a411a7580634d981c09 --- src/storage/dd/CuddDdManager.cpp | 56 +++++++++++++++++++++++++++++--- src/storage/dd/CuddDdManager.h | 3 ++ 2 files changed, 55 insertions(+), 4 deletions(-) diff --git a/src/storage/dd/CuddDdManager.cpp b/src/storage/dd/CuddDdManager.cpp index 3f0a2abed..f265a9f6a 100644 --- a/src/storage/dd/CuddDdManager.cpp +++ b/src/storage/dd/CuddDdManager.cpp @@ -16,25 +16,73 @@ bool CuddOptionsRegistered = storm::settings::Settings::registerNewModule([] (st // Set up option for reordering. std::vector reorderingTechniques; reorderingTechniques.push_back("none"); + reorderingTechniques.push_back("random"); + reorderingTechniques.push_back("randompivot"); reorderingTechniques.push_back("sift"); + reorderingTechniques.push_back("siftconv"); reorderingTechniques.push_back("ssift"); + reorderingTechniques.push_back("ssiftconv"); reorderingTechniques.push_back("gsift"); + reorderingTechniques.push_back("gsiftconv"); reorderingTechniques.push_back("win2"); + reorderingTechniques.push_back("win2conv"); reorderingTechniques.push_back("win3"); + reorderingTechniques.push_back("win3conv"); reorderingTechniques.push_back("win4"); + reorderingTechniques.push_back("win4conv"); reorderingTechniques.push_back("annealing"); reorderingTechniques.push_back("genetic"); reorderingTechniques.push_back("exact"); - instance->addOption(storm::settings::OptionBuilder("Cudd", "reorder", "", "Sets the reordering technique used by Cudd.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("method", "Sets which technique is used by Cudd's reordering routines. Must be in {\"none\", \"sift\", \"ssift\", \"gsift\", \"win2\", \"win3\", \"win4\", \"annealing\", \"genetic\", \"exact\"}.").setDefaultValueString("gsift").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(reorderingTechniques)).build()).build()); + instance->addOption(storm::settings::OptionBuilder("Cudd", "reorder", "", "Sets the reordering technique used by Cudd.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("method", "Sets which technique is used by Cudd's reordering routines. Must be in {\"none\", \"random\", \"randompivot\", \"sift\", \"siftconv\", \"ssift\", \"ssiftconv\", \"gsift\", \"gsiftconv\", \"win2\", \"win2conv\", \"win3\", \"win3conv\", \"win4\", \"win4conv\", \"annealing\", \"genetic\", \"exact\"}.").setDefaultValueString("gsift").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(reorderingTechniques)).build()).build()); return true; }); namespace storm { namespace dd { - DdManager::DdManager() : metaVariableMap(), cuddManager() { + DdManager::DdManager() : metaVariableMap(), cuddManager(), reorderingTechnique(CUDD_REORDER_NONE) { this->cuddManager.SetMaxMemory(static_cast(storm::settings::Settings::getInstance()->getOptionByLongName("cuddmaxmem").getArgument(0).getValueAsUnsignedInteger() * 1024ul * 1024ul)); this->cuddManager.SetEpsilon(storm::settings::Settings::getInstance()->getOptionByLongName("cuddprec").getArgument(0).getValueAsDouble()); + + // Now set the selected reordering technique. + std::string const& reorderingTechnique = storm::settings::Settings::getInstance()->getOptionByLongName("reorder").getArgument(0).getValueAsString(); + if (reorderingTechnique == "none") { + this->reorderingTechnique = CUDD_REORDER_NONE; + } else if (reorderingTechnique == "random") { + this->reorderingTechnique = CUDD_REORDER_RANDOM; + } else if (reorderingTechnique == "randompivot") { + this->reorderingTechnique = CUDD_REORDER_RANDOM_PIVOT; + } else if (reorderingTechnique == "sift") { + this->reorderingTechnique = CUDD_REORDER_SIFT; + } else if (reorderingTechnique == "siftconv") { + this->reorderingTechnique = CUDD_REORDER_SIFT_CONVERGE; + } else if (reorderingTechnique == "ssift") { + this->reorderingTechnique = CUDD_REORDER_SYMM_SIFT; + } else if (reorderingTechnique == "ssiftconv") { + this->reorderingTechnique = CUDD_REORDER_SYMM_SIFT_CONV; + } else if (reorderingTechnique == "gsift") { + this->reorderingTechnique = CUDD_REORDER_GROUP_SIFT; + } else if (reorderingTechnique == "gsiftconv") { + this->reorderingTechnique = CUDD_REORDER_GROUP_SIFT_CONV; + } else if (reorderingTechnique == "win2") { + this->reorderingTechnique = CUDD_REORDER_WINDOW2; + } else if (reorderingTechnique == "win2conv") { + this->reorderingTechnique = CUDD_REORDER_WINDOW2_CONV; + } else if (reorderingTechnique == "win3") { + this->reorderingTechnique = CUDD_REORDER_WINDOW3; + } else if (reorderingTechnique == "win3conv") { + this->reorderingTechnique = CUDD_REORDER_WINDOW3_CONV; + } else if (reorderingTechnique == "win4") { + this->reorderingTechnique = CUDD_REORDER_WINDOW4; + } else if (reorderingTechnique == "win4conv") { + this->reorderingTechnique = CUDD_REORDER_WINDOW4_CONV; + } else if (reorderingTechnique == "annealing") { + this->reorderingTechnique = CUDD_REORDER_ANNEALING; + } else if (reorderingTechnique == "genetic") { + this->reorderingTechnique = CUDD_REORDER_GENETIC; + } else if (reorderingTechnique == "exact") { + this->reorderingTechnique = CUDD_REORDER_EXACT; + } } Dd DdManager::getOne() { @@ -208,7 +256,7 @@ namespace storm { void DdManager::allowDynamicReordering(bool value) { if (value) { - this->getCuddManager().AutodynEnable(CUDD_REORDER_GROUP_SIFT_CONV); + this->getCuddManager().AutodynEnable(this->reorderingTechnique); } else { this->getCuddManager().AutodynDisable(); } @@ -220,7 +268,7 @@ namespace storm { } void DdManager::triggerReordering() { - this->getCuddManager().ReduceHeap(CUDD_REORDER_GROUP_SIFT_CONV, 0); + this->getCuddManager().ReduceHeap(this->reorderingTechnique, 0); } } } \ No newline at end of file diff --git a/src/storage/dd/CuddDdManager.h b/src/storage/dd/CuddDdManager.h index 75c6a23de..682fb4c8b 100644 --- a/src/storage/dd/CuddDdManager.h +++ b/src/storage/dd/CuddDdManager.h @@ -174,6 +174,9 @@ namespace storm { // The manager responsible for the DDs created/modified with this DdManager. Cudd cuddManager; + + // The technique that is used for dynamic reordering. + Cudd_ReorderingType reorderingTechnique; }; } }