From eb1619153e6e8a9ac9168d18ae805c2cb9fd62c1 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 12 Nov 2015 17:01:55 +0100 Subject: [PATCH] same same Former-commit-id: 8a5597ca6ffc7e236b23df684bc454af7d09ad29 --- src/storage/dd/Bdd.cpp | 2 +- src/storage/dd/Bdd.h | 1 + src/storage/dd/DdManager.cpp | 281 +++++++++++++++++- src/storage/dd/DdManager.h | 212 ++++++++++++- src/storage/dd/DdMetaVariable.cpp | 62 ++++ src/storage/dd/DdMetaVariable.h | 102 ++++++- src/storage/dd/InternalDdManager.h | 14 + src/storage/dd/cudd/CuddDdManager.cpp | 242 +-------------- src/storage/dd/cudd/CuddDdManager.h | 20 -- src/storage/dd/cudd/InternalCuddAdd.cpp | 0 src/storage/dd/cudd/InternalCuddAdd.h | 0 src/storage/dd/cudd/InternalCuddBdd.cpp | 62 ++-- src/storage/dd/cudd/InternalCuddBdd.h | 10 +- src/storage/dd/cudd/InternalCuddDdManager.cpp | 88 ++++++ src/storage/dd/cudd/InternalCuddDdManager.h | 119 ++++++++ 15 files changed, 901 insertions(+), 314 deletions(-) create mode 100644 src/storage/dd/DdMetaVariable.cpp create mode 100644 src/storage/dd/InternalDdManager.h create mode 100644 src/storage/dd/cudd/InternalCuddAdd.cpp create mode 100644 src/storage/dd/cudd/InternalCuddAdd.h create mode 100644 src/storage/dd/cudd/InternalCuddDdManager.cpp create mode 100644 src/storage/dd/cudd/InternalCuddDdManager.h diff --git a/src/storage/dd/Bdd.cpp b/src/storage/dd/Bdd.cpp index 5ea3bc376..5d7201a25 100644 --- a/src/storage/dd/Bdd.cpp +++ b/src/storage/dd/Bdd.cpp @@ -37,7 +37,7 @@ namespace storm { template template Bdd Bdd::fromVector(std::shared_ptr const> ddManager, std::vector const& values, Odd const& odd, std::set const& metaVariables, std::function const& filter) { - return Bdd(ddManager, InternalBdd::fromVector(ddManager, values, odd, metaVariables, filter), metaVariables); + return Bdd(ddManager, InternalBdd::fromVector(ddManager, values, odd, ddManager->getSortedVariableIndices(metaVariables), filter), metaVariables); } template diff --git a/src/storage/dd/Bdd.h b/src/storage/dd/Bdd.h index ad9c55c08..d83dbfd0a 100644 --- a/src/storage/dd/Bdd.h +++ b/src/storage/dd/Bdd.h @@ -14,6 +14,7 @@ namespace storm { template class Bdd : public Dd { public: + friend class DdManager; // Instantiate all copy/move constructors/assignments with the default implementation. Bdd() = default; diff --git a/src/storage/dd/DdManager.cpp b/src/storage/dd/DdManager.cpp index e9a21873c..0f59cb9f3 100644 --- a/src/storage/dd/DdManager.cpp +++ b/src/storage/dd/DdManager.cpp @@ -1,13 +1,274 @@ +#include "src/storage/dd/DdManager.h" +#include "src/storage/expressions/ExpressionManager.h" + +#include "src/utility/macros.h" +#include "src/exceptions/InvalidArgumentException.h" namespace storm { namespace dd { template - std::vector Dd::getSortedVariableIndices(DdManager const& manager, std::set const& metaVariables) { + DdManager::DdManager() : metaVariableMap(), manager(new storm::expressions::ExpressionManager()), internalDdManager() { + // Intentionally left empty. + } + + template + Bdd DdManager::getBddOne() const { + return Bdd(this->shared_from_this(), internalDdManager.getBddOne()); + } + + template + template + Add DdManager::getAddOne() const { + return Add(this->shared_from_this(), internalDdManager.template getAddOne()); + } + + template + Bdd DdManager::getBddZero() const { + return Bdd(this->shared_from_this(), internalDdManager.getBddZero()); + } + + template + template + Add DdManager::getAddZero() const { + return Add(this->shared_from_this(), internalDdManager.template getAddZero()); + } + + template + template + Add DdManager::getConstant(ValueType const& value) const { + return Add(this->shared_from_this(), internalDdManager.constant(value)); + } + + template + Bdd DdManager::getEncoding(storm::expressions::Variable const& variable, int_fast64_t value) const { + DdMetaVariable const& metaVariable = this->getMetaVariable(variable); + + STORM_LOG_THROW(value >= metaVariable.getLow() && value <= metaVariable.getHigh(), storm::exceptions::InvalidArgumentException, "Illegal value " << value << " for meta variable '" << variable.getName() << "'."); + + // Now compute the encoding relative to the low value of the meta variable. + value -= metaVariable.getLow(); + + std::vector> const& ddVariables = metaVariable.getDdVariables(); + + Bdd result; + if (value & (1ull << (ddVariables.size() - 1))) { + result = ddVariables[0]; + } else { + result = !ddVariables[0]; + } + + for (std::size_t i = 1; i < ddVariables.size(); ++i) { + if (value & (1ull << (ddVariables.size() - i - 1))) { + result &= ddVariables[i]; + } else { + result &= !ddVariables[i]; + } + } + + return result; + } + + template + Bdd DdManager::getRange(storm::expressions::Variable const& variable) const { + storm::dd::DdMetaVariable const& metaVariable = this->getMetaVariable(variable); + + Bdd result = this->getBddZero(); + + for (int_fast64_t value = metaVariable.getLow(); value <= metaVariable.getHigh(); ++value) { + result |= this->getEncoding(variable, value); + } + + return result; + } + + template + template + Add DdManager::getIdentity(storm::expressions::Variable const& variable) const { + storm::dd::DdMetaVariable const& metaVariable = this->getMetaVariable(variable); + + Add result = this->getAddZero(); + for (int_fast64_t value = metaVariable.getLow(); value <= metaVariable.getHigh(); ++value) { + result += this->getEncoding(variable, value).toAdd() * this->getConstant(value); + } + return result; + } + + template + std::pair DdManager::addMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high) { + // Check whether the variable name is legal. + STORM_LOG_THROW(name != "" && name.back() != '\'', storm::exceptions::InvalidArgumentException, "Illegal name of meta variable: '" << name << "'."); + + // Check whether a meta variable already exists. + STORM_LOG_THROW(!this->hasMetaVariable(name), storm::exceptions::InvalidArgumentException, "A meta variable '" << name << "' already exists."); + + // Check that the range is legal. + STORM_LOG_THROW(high != low, storm::exceptions::InvalidArgumentException, "Range of meta variable must be at least 2 elements."); + + std::size_t numberOfBits = static_cast(std::ceil(std::log2(high - low + 1))); + + storm::expressions::Variable unprimed = manager->declareBitVectorVariable(name, numberOfBits); + storm::expressions::Variable primed = manager->declareBitVectorVariable(name + "'", numberOfBits); + + std::vector> variables; + std::vector> variablesPrime; + for (std::size_t i = 0; i < numberOfBits; ++i) { + auto ddVariablePair = internalDdManager.createNewDdVariablePair(); + variables.emplace_back(Bdd(this->shared_from_this(), ddVariablePair.first, {unprimed})); + variables.emplace_back(Bdd(this->shared_from_this(), ddVariablePair.second, {unprimed})); + } + + metaVariableMap.emplace(unprimed, DdMetaVariable(name, low, high, variables, this->shared_from_this())); + metaVariableMap.emplace(primed, DdMetaVariable(name + "'", low, high, variablesPrime, this->shared_from_this())); + + return std::make_pair(unprimed, primed); + } + + template + std::pair DdManager::addMetaVariable(std::string const& name) { + // Check whether the variable name is legal. + STORM_LOG_THROW(name != "" && name.back() != '\'', storm::exceptions::InvalidArgumentException, "Illegal name of meta variable: '" << name << "'."); + + // Check whether a meta variable already exists. + STORM_LOG_THROW(!this->hasMetaVariable(name), storm::exceptions::InvalidArgumentException, "A meta variable '" << name << "' already exists."); + + storm::expressions::Variable unprimed = manager->declareBooleanVariable(name); + storm::expressions::Variable primed = manager->declareBooleanVariable(name + "'"); + + std::vector> variables; + std::vector> variablesPrime; + auto ddVariablePair = internalDdManager.createNewDdVariablePair(); + variables.emplace_back(Bdd(this->shared_from_this(), ddVariablePair.first, {unprimed})); + variablesPrime.emplace_back(Bdd(this->shared_from_this(), ddVariablePair.second, {primed})); + + metaVariableMap.emplace(unprimed, DdMetaVariable(name, variables, this->shared_from_this())); + metaVariableMap.emplace(primed, DdMetaVariable(name + "'", variablesPrime, this->shared_from_this())); + + return std::make_pair(unprimed, primed); + } + + template + DdMetaVariable const& DdManager::getMetaVariable(storm::expressions::Variable const& variable) const { + auto const& variablePair = metaVariableMap.find(variable); + + // Check whether the meta variable exists. + STORM_LOG_THROW(variablePair != metaVariableMap.end(), storm::exceptions::InvalidArgumentException, "Unknown meta variable name '" << variable.getName() << "'."); + + return variablePair->second; + } + + template + std::set DdManager::getAllMetaVariableNames() const { + std::set result; + for (auto const& variablePair : metaVariableMap) { + result.insert(variablePair.first.getName()); + } + return result; + } + + template + std::size_t DdManager::getNumberOfMetaVariables() const { + return this->metaVariableMap.size(); + } + + template + bool DdManager::hasMetaVariable(std::string const& metaVariableName) const { + return manager->hasVariable(metaVariableName); + } + + template + storm::expressions::ExpressionManager const& DdManager::getExpressionManager() const { + return *manager; + } + + template + storm::expressions::ExpressionManager& DdManager::getExpressionManager() { + return *manager; + } + + template + std::vector DdManager::getDdVariableNames() const { + // First, we initialize a list DD variables and their names. + std::vector> variablePairs; + for (auto const& variablePair : this->metaVariableMap) { + DdMetaVariable const& metaVariable = variablePair.second; + // If the meta variable is of type bool, we don't need to suffix it with the bit number. + if (metaVariable.getType() == MetaVariableType::Bool) { + variablePairs.emplace_back(metaVariable.getDdVariables().front().getIndex(), variablePair.first.getName()); + } else { + // For integer-valued meta variables, we, however, have to add the suffix. + for (uint_fast64_t variableIndex = 0; variableIndex < metaVariable.getNumberOfDdVariables(); ++variableIndex) { + variablePairs.emplace_back(metaVariable.getDdVariables()[variableIndex].getIndex(), variablePair.first.getName() + '.' + std::to_string(variableIndex)); + } + } + } + + // Then, we sort this list according to the indices of the ADDs. + std::sort(variablePairs.begin(), variablePairs.end(), [](std::pair const& a, std::pair const& b) { return a.first < b.first; }); + + // Now, we project the sorted vector to its second component. + std::vector result; + for (auto const& element : variablePairs) { + result.push_back(element.second); + } + + return result; + } + + template + std::vector DdManager::getDdVariables() const { + // First, we initialize a list DD variables and their names. + std::vector> variablePairs; + for (auto const& variablePair : this->metaVariableMap) { + DdMetaVariable const& metaVariable = variablePair.second; + // If the meta variable is of type bool, we don't need to suffix it with the bit number. + if (metaVariable.getType() == MetaVariableType::Bool) { + variablePairs.emplace_back(metaVariable.getDdVariables().front().getIndex(), variablePair.first); + } else { + // For integer-valued meta variables, we, however, have to add the suffix. + for (uint_fast64_t variableIndex = 0; variableIndex < metaVariable.getNumberOfDdVariables(); ++variableIndex) { + variablePairs.emplace_back(metaVariable.getDdVariables()[variableIndex].getIndex(), variablePair.first); + } + } + } + + // Then, we sort this list according to the indices of the ADDs. + std::sort(variablePairs.begin(), variablePairs.end(), [](std::pair const& a, std::pair const& b) { return a.first < b.first; }); + + // Now, we project the sorted vector to its second component. + std::vector result; + for (auto const& element : variablePairs) { + result.push_back(element.second); + } + + return result; + } + + template + void DdManager::allowDynamicReordering(bool value) { + internalDdManager.allowDynamicReordering(value); + } + + template + bool DdManager::isDynamicReorderingAllowed() const { + return internalDdManager.isDynamicReorderingAllowed(); + } + + template + void DdManager::triggerReordering() { + internalDdManager.triggerReordering(); + } + + template + std::shared_ptr const> DdManager::asSharedPointer() const { + return this->shared_from_this(); + } + + template + std::vector DdManager::getSortedVariableIndices(std::set const& metaVariables) { std::vector ddVariableIndices; - for (auto const& metaVariableName : metaVariables) { - auto const& metaVariable = manager.getMetaVariable(metaVariableName); - for (auto const& ddVariable : metaVariable.getDdVariables()) { + for (auto const& metaVariable : metaVariableMap) { + for (auto const& ddVariable : metaVariable.second.getDdVariables()) { ddVariableIndices.push_back(ddVariable.getIndex()); } } @@ -16,5 +277,17 @@ namespace storm { std::sort(ddVariableIndices.begin(), ddVariableIndices.end()); return ddVariableIndices; } + + template + InternalDdManager& DdManager::getInternalDdManager() { + return internalDdManager; + } + + template + InternalDdManager const& DdManager::getInternalDdManager() const { + return internalDdManager; + } + + template class DdManager; } } \ No newline at end of file diff --git a/src/storage/dd/DdManager.h b/src/storage/dd/DdManager.h index 11d378e46..deb6f1430 100644 --- a/src/storage/dd/DdManager.h +++ b/src/storage/dd/DdManager.h @@ -1,20 +1,174 @@ #ifndef STORM_STORAGE_DD_DDMANAGER_H_ #define STORM_STORAGE_DD_DDMANAGER_H_ +#include +#include + #include "src/storage/dd/DdType.h" #include "src/storage/dd/DdMetaVariable.h" +#include "src/storage/dd/Bdd.h" +#include "src/storage/dd/Add.h" + #include "src/storage/expressions/Variable.h" +#include "src/storage/dd/cudd/InternalCuddDdManager.h" + namespace storm { namespace dd { // Declare DdManager class so we can then specialize it for the different DD types. template - class DdManager { + class DdManager : public std::enable_shared_from_this> { public: + /*! + * Creates an empty manager without any meta variables. + */ + DdManager(); + + // Explictly forbid copying a DdManager, but allow moving it. + DdManager(DdManager const& other) = delete; + DdManager& operator=(DdManager const& other) = delete; + DdManager(DdManager&& other) = default; + DdManager& operator=(DdManager&& other) = default; + + /*! + * Retrieves a BDD representing the constant one function. + * + * @return A BDD representing the constant one function. + */ Bdd getBddOne() const; + + /*! + * Retrieves an ADD representing the constant one function. + * + * @return An ADD representing the constant one function. + */ + template + Add getAddOne() const; + + /*! + * Retrieves a BDD representing the constant zero function. + * + * @return A BDD representing the constant zero function. + */ Bdd getBddZero() const; + + /*! + * Retrieves an ADD representing the constant zero function. + * + * @return An ADD representing the constant zero function. + */ + template + Add getAddZero() const; + + /*! + * Retrieves an ADD representing the constant function with the given value. + * + * @return An ADD representing the constant function with the given value. + */ + template + Add getConstant(ValueType const& value) const; + + /*! + * Retrieves the BDD representing the function that maps all inputs which have the given meta variable equal + * to the given value one. + * + * @param variable The expression variable associated with the meta variable. + * @param value The value the meta variable is supposed to have. + * @return The DD representing the function that maps all inputs which have the given meta variable equal + * to the given value one. + */ + Bdd getEncoding(storm::expressions::Variable const& variable, int_fast64_t value) const; + + /*! + * Retrieves the BDD representing the range of the meta variable, i.e., a function that maps all legal values + * of the range of the meta variable to one. + * + * @param variable The expression variable associated with the meta variable. + * @return The range of the meta variable. + */ + Bdd getRange(storm::expressions::Variable const& variable) const; + + /*! + * Retrieves the ADD representing the identity of the meta variable, i.e., a function that maps all legal + * values of the range of the meta variable to themselves. + * + * @param variable The expression variable associated with the meta variable. + * @return The identity of the meta variable. + */ + template + Add getIdentity(storm::expressions::Variable const& variable) const; + + /*! + * Adds an integer meta variable with the given range. + * + * @param variableName The name of the new variable. + * @param low The lowest value of the range of the variable. + * @param high The highest value of the range of the variable. + */ + std::pair addMetaVariable(std::string const& variableName, int_fast64_t low, int_fast64_t high); + + /*! + * Adds a boolean meta variable. + * + * @param variableName The name of the new variable. + */ + std::pair addMetaVariable(std::string const& variableName); + + /*! + * Retrieves the names of all meta variables that have been added to the manager. + * + * @return The set of all meta variable names of the manager. + */ + std::set getAllMetaVariableNames() const; + + /*! + * Retrieves the number of meta variables that are contained in this manager. + * + * @return The number of meta variables contained in this manager. + */ + std::size_t getNumberOfMetaVariables() const; + + /*! + * Retrieves whether the given meta variable name is already in use. + * + * @param variableName The name of the variable. + * @return True if the given meta variable name is managed by this manager. + */ + bool hasMetaVariable(std::string const& variableName) const; + + /*! + * Sets whether or not dynamic reordering is allowed for the DDs managed by this manager. + * + * @param value If set to true, dynamic reordering is allowed and forbidden otherwise. + */ + void allowDynamicReordering(bool value); + + /*! + * Retrieves whether dynamic reordering is currently allowed. + * + * @return True iff dynamic reordering is currently allowed. + */ + bool isDynamicReorderingAllowed() const; + + /*! + * Triggers a reordering of the DDs managed by this manager. + */ + void triggerReordering(); + + /*! + * Retrieves the meta variable with the given name if it exists. + * + * @param variable The expression variable associated with the meta variable. + * @return The corresponding meta variable. + */ DdMetaVariable const& getMetaVariable(storm::expressions::Variable const& variable) const; - std::vector getDdVariableNames() const; + + /*! + * Retrieves the manager as a shared pointer. + * + * @return A shared pointer to the manager. + */ + std::shared_ptr const> asSharedPointer() const; /*! * Retrieves the (sorted) list of the variable indices of the DD variables given by the meta variable set. @@ -23,7 +177,59 @@ namespace storm { * @param metaVariable The set of meta variables for which to retrieve the index list. * @return The sorted list of variable indices. */ - static std::vector getSortedVariableIndices(std::set const& metaVariables); + std::vector getSortedVariableIndices(std::set const& metaVariables); + + /*! + * Retrieves the internal DD manager. + * + * @return The internal DD manager. + */ + InternalDdManager& getInternalDdManager(); + + /*! + * Retrieves the internal DD manager. + * + * @return The internal DD manager. + */ + InternalDdManager const& getInternalDdManager() const; + + private: + /*! + * Retrieves a list of names of the DD variables in the order of their index. + * + * @return A list of DD variable names. + */ + std::vector getDdVariableNames() const; + + /*! + * Retrieves a list of expression variables in the order of their index. + * + * @return A list of DD variables. + */ + std::vector getDdVariables() const; + + /*! + * Retrieves the underlying expression manager. + * + * @return The underlying expression manager. + */ + storm::expressions::ExpressionManager const& getExpressionManager() const; + + /*! + * Retrieves the underlying expression manager. + * + * @return The underlying expression manager. + */ + storm::expressions::ExpressionManager& getExpressionManager(); + + // A mapping from variables to the meta variable information. + std::unordered_map> metaVariableMap; + + // The manager responsible for the variables. + std::shared_ptr manager; + + // The DD manager that is customized according to the selected library type. + InternalDdManager internalDdManager; }; } } diff --git a/src/storage/dd/DdMetaVariable.cpp b/src/storage/dd/DdMetaVariable.cpp new file mode 100644 index 000000000..00ef6452a --- /dev/null +++ b/src/storage/dd/DdMetaVariable.cpp @@ -0,0 +1,62 @@ +#include "src/storage/dd/DdMetaVariable.h" + +namespace storm { + namespace dd { + template + DdMetaVariable::DdMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high, std::vector> const& ddVariables) : name(name), type(MetaVariableType::Int), low(low), high(high), ddVariables(ddVariables) { + this->createCube(); + } + + template + DdMetaVariable::DdMetaVariable(std::string const& name, std::vector> const& ddVariables) : name(name), type(MetaVariableType::Bool), low(0), high(1), ddVariables(ddVariables) { + this->createCube(); + } + + template + std::string const& DdMetaVariable::getName() const { + return this->name; + } + + template + MetaVariableType DdMetaVariable::getType() const { + return this->type; + } + + template + int_fast64_t DdMetaVariable::getLow() const { + return this->low; + } + + template + int_fast64_t DdMetaVariable::getHigh() const { + return this->high; + } + + template + std::size_t DdMetaVariable::getNumberOfDdVariables() const { + return this->ddVariables.size(); + } + + template + std::vector> const& DdMetaVariable::getDdVariables() const { + return this->ddVariables; + } + + template + Bdd const& DdMetaVariable::getCube() const { + return this->cube; + } + + template + void DdMetaVariable::createCube() { + auto it = this->ddVariables.begin(); + this->cube = *it; + ++it; + for (auto ite = this->ddVariables.end(); it != ite; ++it) { + this->cube &= *it; + } + } + + template class DdMetaVariable; + } +} \ No newline at end of file diff --git a/src/storage/dd/DdMetaVariable.h b/src/storage/dd/DdMetaVariable.h index 1cc920237..8d8044335 100644 --- a/src/storage/dd/DdMetaVariable.h +++ b/src/storage/dd/DdMetaVariable.h @@ -4,15 +4,113 @@ #include #include "src/storage/dd/DdType.h" +#include "src/storage/dd/Bdd.h" namespace storm { namespace dd { + template + class DdManager; + + // An enumeration for all legal types of meta variables. + enum class MetaVariableType { Bool, Int }; + // Declare DdMetaVariable class so we can then specialize it for the different DD types. template class DdMetaVariable { public: - Bdd getCube() const; - uint_fast64_t getNumberOfDdVariables() const; + friend class DdManager; + + /*! + * Retrieves the name of the meta variable. + * + * @return The name of the variable. + */ + std::string const& getName() const; + + /*! + * Retrieves the type of the meta variable. + * + * @return The type of the meta variable. + */ + MetaVariableType getType() const; + + /*! + * Retrieves the lowest value of the range of the variable. + * + * @return The lowest value of the range of the variable. + */ + int_fast64_t getLow() const; + + /*! + * Retrieves the highest value of the range of the variable. + * + * @return The highest value of the range of the variable. + */ + int_fast64_t getHigh() const; + + /*! + * Retrieves the number of DD variables for this meta variable. + * + * @return The number of DD variables for this meta variable. + */ + std::size_t getNumberOfDdVariables() const; + + /*! + * Retrieves the cube of all variables that encode this meta variable. + * + * @return The cube of all variables that encode this meta variable. + */ + Bdd const& getCube() const; + + private: + /*! + * Creates an integer meta variable with the given name and range bounds. + * + * @param name The name of the meta variable. + * @param low The lowest value of the range of the variable. + * @param high The highest value of the range of the variable. + * @param ddVariables The vector of variables used to encode this variable. + * @param manager A pointer to the manager that is responsible for this meta variable. + */ + DdMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high, std::vector> const& ddVariables); + + /*! + * Creates a boolean meta variable with the given name. + * @param name The name of the meta variable. + * @param ddVariables The vector of variables used to encode this variable. + * @param manager A pointer to the manager that is responsible for this meta variable. + */ + DdMetaVariable(std::string const& name, std::vector> const& ddVariables); + + /*! + * Retrieves the variables used to encode the meta variable. + * + * @return A vector of variables used to encode the meta variable. + */ + std::vector> const& getDdVariables() const; + + /*! + * Creates the cube for this meta variable from the DD variables. + */ + void createCube(); + + // The name of the meta variable. + std::string name; + + // The type of the variable. + MetaVariableType type; + + // The lowest value of the range of the variable. + int_fast64_t low; + + // The highest value of the range of the variable. + int_fast64_t high; + + // The vector of variables that are used to encode the meta variable. + std::vector> ddVariables; + + // The cube consisting of all variables that encode the meta variable. + Bdd cube; }; } } diff --git a/src/storage/dd/InternalDdManager.h b/src/storage/dd/InternalDdManager.h new file mode 100644 index 000000000..50b209708 --- /dev/null +++ b/src/storage/dd/InternalDdManager.h @@ -0,0 +1,14 @@ +#ifndef STORM_STORAGE_DD_INTERNALDDMANAGER_H_ +#define STORM_STORAGE_DD_INTERNALDDMANAGER_H_ + +#include "src/storage/dd/DdType.h" + +namespace storm { + namespace dd { + template + class InternalDdManager; + } +} + + +#endif /* STORM_STORAGE_DD_INTERNALDDMANAGER_H_ */ \ No newline at end of file diff --git a/src/storage/dd/cudd/CuddDdManager.cpp b/src/storage/dd/cudd/CuddDdManager.cpp index 68e50a164..8a3fc35f7 100644 --- a/src/storage/dd/cudd/CuddDdManager.cpp +++ b/src/storage/dd/cudd/CuddDdManager.cpp @@ -15,258 +15,18 @@ namespace storm { namespace dd { - DdManager::DdManager() : metaVariableMap(), cuddManager(), reorderingTechnique(CUDD_REORDER_NONE), manager(new storm::expressions::ExpressionManager()) { - this->cuddManager.SetMaxMemory(static_cast(storm::settings::cuddSettings().getMaximalMemory() * 1024ul * 1024ul)); - this->cuddManager.SetEpsilon(storm::settings::cuddSettings().getConstantPrecision()); - - // Now set the selected reordering technique. - storm::settings::modules::CuddSettings::ReorderingTechnique reorderingTechniqueAsSetting = storm::settings::cuddSettings().getReorderingTechnique(); - switch (reorderingTechniqueAsSetting) { - case storm::settings::modules::CuddSettings::ReorderingTechnique::None: this->reorderingTechnique = CUDD_REORDER_NONE; break; - case storm::settings::modules::CuddSettings::ReorderingTechnique::Random: this->reorderingTechnique = CUDD_REORDER_RANDOM; break; - case storm::settings::modules::CuddSettings::ReorderingTechnique::RandomPivot: this->reorderingTechnique = CUDD_REORDER_RANDOM_PIVOT; break; - case storm::settings::modules::CuddSettings::ReorderingTechnique::Sift: this->reorderingTechnique = CUDD_REORDER_SIFT; break; - case storm::settings::modules::CuddSettings::ReorderingTechnique::SiftConv: this->reorderingTechnique = CUDD_REORDER_SIFT_CONVERGE; break; - case storm::settings::modules::CuddSettings::ReorderingTechnique::SymmetricSift: this->reorderingTechnique = CUDD_REORDER_SYMM_SIFT; break; - case storm::settings::modules::CuddSettings::ReorderingTechnique::SymmetricSiftConv: this->reorderingTechnique = CUDD_REORDER_SYMM_SIFT_CONV; break; - case storm::settings::modules::CuddSettings::ReorderingTechnique::GroupSift: this->reorderingTechnique = CUDD_REORDER_GROUP_SIFT; break; - case storm::settings::modules::CuddSettings::ReorderingTechnique::GroupSiftConv: this->reorderingTechnique = CUDD_REORDER_GROUP_SIFT_CONV; break; - case storm::settings::modules::CuddSettings::ReorderingTechnique::Win2: this->reorderingTechnique = CUDD_REORDER_WINDOW2; break; - case storm::settings::modules::CuddSettings::ReorderingTechnique::Win2Conv: this->reorderingTechnique = CUDD_REORDER_WINDOW2_CONV; break; - case storm::settings::modules::CuddSettings::ReorderingTechnique::Win3: this->reorderingTechnique = CUDD_REORDER_WINDOW3; break; - case storm::settings::modules::CuddSettings::ReorderingTechnique::Win3Conv: this->reorderingTechnique = CUDD_REORDER_WINDOW3_CONV; break; - case storm::settings::modules::CuddSettings::ReorderingTechnique::Win4: this->reorderingTechnique = CUDD_REORDER_WINDOW4; break; - case storm::settings::modules::CuddSettings::ReorderingTechnique::Win4Conv: this->reorderingTechnique = CUDD_REORDER_WINDOW4_CONV; break; - case storm::settings::modules::CuddSettings::ReorderingTechnique::Annealing: this->reorderingTechnique = CUDD_REORDER_ANNEALING; break; - case storm::settings::modules::CuddSettings::ReorderingTechnique::Genetic: this->reorderingTechnique = CUDD_REORDER_GENETIC; break; - case storm::settings::modules::CuddSettings::ReorderingTechnique::Exact: this->reorderingTechnique = CUDD_REORDER_EXACT; break; - } - } - - Bdd DdManager::getBddOne() const { - return Bdd(this->shared_from_this(), cuddManager.bddOne()); - } - Add DdManager::getAddOne() const { - return Add(this->shared_from_this(), cuddManager.addOne()); - } - - Bdd DdManager::getBddZero() const { - return Bdd(this->shared_from_this(), cuddManager.bddZero()); - } - - Add DdManager::getAddZero() const { - return Add(this->shared_from_this(), cuddManager.addZero()); - } - - - Add DdManager::getConstant(double value) const { - return Add(this->shared_from_this(), cuddManager.constant(value)); - } - - Bdd DdManager::getEncoding(storm::expressions::Variable const& variable, int_fast64_t value) const { - DdMetaVariable const& metaVariable = this->getMetaVariable(variable); - - STORM_LOG_THROW(value >= metaVariable.getLow() && value <= metaVariable.getHigh(), storm::exceptions::InvalidArgumentException, "Illegal value " << value << " for meta variable '" << variable.getName() << "'."); - - // Now compute the encoding relative to the low value of the meta variable. - value -= metaVariable.getLow(); - - std::vector> const& ddVariables = metaVariable.getDdVariables(); - Bdd result; - if (value & (1ull << (ddVariables.size() - 1))) { - result = ddVariables[0]; - } else { - result = !ddVariables[0]; - } - - for (std::size_t i = 1; i < ddVariables.size(); ++i) { - if (value & (1ull << (ddVariables.size() - i - 1))) { - result &= ddVariables[i]; - } else { - result &= !ddVariables[i]; - } - } - - return result; - } - Bdd DdManager::getRange(storm::expressions::Variable const& variable) const { - storm::dd::DdMetaVariable const& metaVariable = this->getMetaVariable(variable); - - Bdd result = this->getBddZero(); - - for (int_fast64_t value = metaVariable.getLow(); value <= metaVariable.getHigh(); ++value) { - result |= this->getEncoding(variable, value); - } - - return result; - } - Add DdManager::getIdentity(storm::expressions::Variable const& variable) const { - storm::dd::DdMetaVariable const& metaVariable = this->getMetaVariable(variable); - - Add result = this->getAddZero(); - for (int_fast64_t value = metaVariable.getLow(); value <= metaVariable.getHigh(); ++value) { - result += this->getEncoding(variable, value).toAdd() * this->getConstant(value); - } - return result; - } - - std::pair DdManager::addMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high) { - // Check whether the variable name is legal. - STORM_LOG_THROW(name != "" && name.back() != '\'', storm::exceptions::InvalidArgumentException, "Illegal name of meta variable: '" << name << "'."); - - // Check whether a meta variable already exists. - STORM_LOG_THROW(!this->hasMetaVariable(name), storm::exceptions::InvalidArgumentException, "A meta variable '" << name << "' already exists."); - // Check that the range is legal. - STORM_LOG_THROW(high != low, storm::exceptions::InvalidArgumentException, "Range of meta variable must be at least 2 elements."); - - std::size_t numberOfBits = static_cast(std::ceil(std::log2(high - low + 1))); - - storm::expressions::Variable unprimed = manager->declareBitVectorVariable(name, numberOfBits); - storm::expressions::Variable primed = manager->declareBitVectorVariable(name + "'", numberOfBits); - - std::vector> variables; - std::vector> variablesPrime; - for (std::size_t i = 0; i < numberOfBits; ++i) { - variables.emplace_back(Bdd(this->shared_from_this(), cuddManager.bddVar(), {unprimed})); - variablesPrime.emplace_back(Bdd(this->shared_from_this(), cuddManager.bddVar(), {primed})); - } - - // Now group the non-primed and primed variable. - for (uint_fast64_t i = 0; i < numberOfBits; ++i) { - this->getCuddManager().MakeTreeNode(variables[i].getIndex(), 2, MTR_FIXED); - } - - metaVariableMap.emplace(unprimed, DdMetaVariable(name, low, high, variables, this->shared_from_this())); - metaVariableMap.emplace(primed, DdMetaVariable(name + "'", low, high, variablesPrime, this->shared_from_this())); - - return std::make_pair(unprimed, primed); - } - std::pair DdManager::addMetaVariable(std::string const& name) { - // Check whether the variable name is legal. - STORM_LOG_THROW(name != "" && name.back() != '\'', storm::exceptions::InvalidArgumentException, "Illegal name of meta variable: '" << name << "'."); - - // Check whether a meta variable already exists. - STORM_LOG_THROW(!this->hasMetaVariable(name), storm::exceptions::InvalidArgumentException, "A meta variable '" << name << "' already exists."); - - storm::expressions::Variable unprimed = manager->declareBooleanVariable(name); - storm::expressions::Variable primed = manager->declareBooleanVariable(name + "'"); - std::vector> variables; - std::vector> variablesPrime; - variables.emplace_back(Bdd(this->shared_from_this(), cuddManager.bddVar(), {unprimed})); - variablesPrime.emplace_back(Bdd(this->shared_from_this(), cuddManager.bddVar(), {primed})); - - // Now group the non-primed and primed variable. - this->getCuddManager().MakeTreeNode(variables.front().getIndex(), 2, MTR_FIXED); - - metaVariableMap.emplace(unprimed, DdMetaVariable(name, variables, this->shared_from_this())); - metaVariableMap.emplace(primed, DdMetaVariable(name + "'", variablesPrime, this->shared_from_this())); - - return std::make_pair(unprimed, primed); - } - - DdMetaVariable const& DdManager::getMetaVariable(storm::expressions::Variable const& variable) const { - auto const& variablePair = metaVariableMap.find(variable); - - // Check whether the meta variable exists. - STORM_LOG_THROW(variablePair != metaVariableMap.end(), storm::exceptions::InvalidArgumentException, "Unknown meta variable name '" << variable.getName() << "'."); - - return variablePair->second; - } - - std::set DdManager::getAllMetaVariableNames() const { - std::set result; - for (auto const& variablePair : metaVariableMap) { - result.insert(variablePair.first.getName()); - } - return result; - } - - std::size_t DdManager::getNumberOfMetaVariables() const { - return this->metaVariableMap.size(); - } - bool DdManager::hasMetaVariable(std::string const& metaVariableName) const { - return manager->hasVariable(metaVariableName); - } - Cudd& DdManager::getCuddManager() { - return this->cuddManager; - } - Cudd const& DdManager::getCuddManager() const { - return this->cuddManager; - } - storm::expressions::ExpressionManager const& DdManager::getExpressionManager() const { - return *manager; - } - - storm::expressions::ExpressionManager& DdManager::getExpressionManager() { - return *manager; - } - - std::vector DdManager::getDdVariableNames() const { - // First, we initialize a list DD variables and their names. - std::vector> variablePairs; - for (auto const& variablePair : this->metaVariableMap) { - DdMetaVariable const& metaVariable = variablePair.second; - // If the meta variable is of type bool, we don't need to suffix it with the bit number. - if (metaVariable.getType() == DdMetaVariable::MetaVariableType::Bool) { - variablePairs.emplace_back(metaVariable.getDdVariables().front().getIndex(), variablePair.first.getName()); - } else { - // For integer-valued meta variables, we, however, have to add the suffix. - for (uint_fast64_t variableIndex = 0; variableIndex < metaVariable.getNumberOfDdVariables(); ++variableIndex) { - variablePairs.emplace_back(metaVariable.getDdVariables()[variableIndex].getIndex(), variablePair.first.getName() + '.' + std::to_string(variableIndex)); - } - } - } - - // Then, we sort this list according to the indices of the ADDs. - std::sort(variablePairs.begin(), variablePairs.end(), [](std::pair const& a, std::pair const& b) { return a.first < b.first; }); - - // Now, we project the sorted vector to its second component. - std::vector result; - for (auto const& element : variablePairs) { - result.push_back(element.second); - } - - return result; - } - - std::vector DdManager::getDdVariables() const { - // First, we initialize a list DD variables and their names. - std::vector> variablePairs; - for (auto const& variablePair : this->metaVariableMap) { - DdMetaVariable const& metaVariable = variablePair.second; - // If the meta variable is of type bool, we don't need to suffix it with the bit number. - if (metaVariable.getType() == DdMetaVariable::MetaVariableType::Bool) { - variablePairs.emplace_back(metaVariable.getDdVariables().front().getIndex(), variablePair.first); - } else { - // For integer-valued meta variables, we, however, have to add the suffix. - for (uint_fast64_t variableIndex = 0; variableIndex < metaVariable.getNumberOfDdVariables(); ++variableIndex) { - variablePairs.emplace_back(metaVariable.getDdVariables()[variableIndex].getIndex(), variablePair.first); - } - } - } - - // Then, we sort this list according to the indices of the ADDs. - std::sort(variablePairs.begin(), variablePairs.end(), [](std::pair const& a, std::pair const& b) { return a.first < b.first; }); - - // Now, we project the sorted vector to its second component. - std::vector result; - for (auto const& element : variablePairs) { - result.push_back(element.second); - } - - return result; - } + void DdManager::allowDynamicReordering(bool value) { if (value) { diff --git a/src/storage/dd/cudd/CuddDdManager.h b/src/storage/dd/cudd/CuddDdManager.h index 707bc7206..a3028f769 100644 --- a/src/storage/dd/cudd/CuddDdManager.h +++ b/src/storage/dd/cudd/CuddDdManager.h @@ -191,20 +191,6 @@ namespace storm { */ std::vector getDdVariables() const; - /*! - * Retrieves the underlying CUDD manager. - * - * @return The underlying CUDD manager. - */ - Cudd& getCuddManager(); - - /*! - * Retrieves the underlying CUDD manager. - * - * @return The underlying CUDD manager. - */ - Cudd const& getCuddManager() const; - /*! * Retrieves the underlying expression manager. * @@ -221,12 +207,6 @@ namespace storm { // A mapping from variables to the meta variable information. std::unordered_map> metaVariableMap; - - // The manager responsible for the DDs created/modified with this DdManager. - Cudd cuddManager; - - // The technique that is used for dynamic reordering. - Cudd_ReorderingType reorderingTechnique; // The manager responsible for the variables. std::shared_ptr manager; diff --git a/src/storage/dd/cudd/InternalCuddAdd.cpp b/src/storage/dd/cudd/InternalCuddAdd.cpp new file mode 100644 index 000000000..e69de29bb diff --git a/src/storage/dd/cudd/InternalCuddAdd.h b/src/storage/dd/cudd/InternalCuddAdd.h new file mode 100644 index 000000000..e69de29bb diff --git a/src/storage/dd/cudd/InternalCuddBdd.cpp b/src/storage/dd/cudd/InternalCuddBdd.cpp index 8ac0bac48..f5d032a37 100644 --- a/src/storage/dd/cudd/InternalCuddBdd.cpp +++ b/src/storage/dd/cudd/InternalCuddBdd.cpp @@ -1,16 +1,17 @@ #include "src/storage/dd/cudd/InternalCuddBdd.h" +#include "src/storage/dd/cudd/InternalCuddDdManager.h" + namespace storm { namespace dd { - InternalBdd::InternalBdd(std::shared_ptr const> ddManager, BDD cuddBdd) : ddManager(ddManager), cuddBdd(cuddBdd) { + InternalBdd::InternalBdd(InternalDdManager const* ddManager, BDD cuddBdd) : ddManager(ddManager), cuddBdd(cuddBdd) { // Intentionally left empty. } template - InternalBdd InternalBdd::fromVector(std::shared_ptr const> ddManager, std::vector const& values, Odd const& odd, std::set const& metaVariables, std::function const& filter) { - std::vector ddVariableIndices = ddManager->getSortedVariableIndices(metaVariables); + InternalBdd InternalBdd::fromVector(InternalDdManager const* ddManager, std::vector const& values, Odd const& odd, std::vector const& sortedDdVariableIndices, std::function const& filter) { uint_fast64_t offset = 0; - return BDD(ddManager->getCuddManager(), fromVectorRec(ddManager->getCuddManager().getManager(), offset, 0, ddVariableIndices.size(), values, odd, ddVariableIndices, filter)); + return InternalBdd(ddManager, BDD(ddManager->getCuddManager(), fromVectorRec(ddManager->getCuddManager().getManager(), offset, 0, sortedDdVariableIndices.size(), values, odd, sortedDdVariableIndices, filter))); } bool InternalBdd::operator==(InternalBdd const& other) const { @@ -22,7 +23,7 @@ namespace storm { } InternalBdd InternalBdd::ite(InternalBdd const& thenDd, InternalBdd const& elseDd) const { - return InternalBdd(this->getCuddBdd().Ite(thenDd.getCuddBdd(), elseDd.getCuddBdd())); + return InternalBdd(ddManager, this->getCuddBdd().Ite(thenDd.getCuddBdd(), elseDd.getCuddBdd())); } InternalBdd InternalBdd::operator||(InternalBdd const& other) const { @@ -48,15 +49,15 @@ namespace storm { } InternalBdd InternalBdd::iff(InternalBdd const& other) const { - return InternalBdd(this->getCuddBdd().Xnor(other.getCuddBdd())); + return InternalBdd(ddManager, this->getCuddBdd().Xnor(other.getCuddBdd())); } InternalBdd InternalBdd::exclusiveOr(InternalBdd const& other) const { - return InternalBdd(this->getCuddBdd().Xor(other.getCuddBdd())); + return InternalBdd(ddManager, this->getCuddBdd().Xor(other.getCuddBdd())); } InternalBdd InternalBdd::implies(InternalBdd const& other) const { - return InternalBdd(this->getCuddBdd().Ite(other.getCuddBdd(), this->getDdManager()->getBddOne().getCuddBdd()), metaVariables); + return InternalBdd(ddManager, this->getCuddBdd().Ite(other.getCuddBdd(), ddManager->getBddOne().getCuddBdd())); } InternalBdd InternalBdd::operator!() const { @@ -70,27 +71,27 @@ namespace storm { return *this; } - InternalBdd InternalBdd::existsAbstract(InternalBdd const& cube) const { - return InternalBdd(this->getDdManager(), this->getCuddBdd().ExistAbstract(cube.getCuddBdd()), newMetaVariables); + InternalBdd InternalBdd::existsAbstract(InternalBdd const& cube) const { + return InternalBdd(ddManager, this->getCuddBdd().ExistAbstract(cube.getCuddBdd())); } - InternalBdd InternalBdd::universalAbstract(InternalBdd const& cube) const { - return InternalBdd(this->getDdManager(), this->getCuddBdd().UnivAbstract(cube.getCuddBdd()), newMetaVariables); + InternalBdd InternalBdd::universalAbstract(InternalBdd const& cube) const { + return InternalBdd(ddManager, this->getCuddBdd().UnivAbstract(cube.getCuddBdd())); } - InternalBdd InternalBdd::andExists(InternalBdd const& other, InternalBdd const& cube) const { - return InternalBdd(this->getDdManager(), this->getCuddBdd().AndAbstract(other.getCuddBdd(), cube.getCuddBdd()), containedMetaVariables); + InternalBdd InternalBdd::andExists(InternalBdd const& other, InternalBdd const& cube) const { + return InternalBdd(ddManager, this->getCuddBdd().AndAbstract(other.getCuddBdd(), cube.getCuddBdd())); } InternalBdd InternalBdd::constrain(InternalBdd const& constraint) const { - return InternalBdd(this->getDdManager(), this->getCuddBdd().Constrain(constraint.getCuddBdd()), metaVariables); + return InternalBdd(ddManager, this->getCuddBdd().Constrain(constraint.getCuddBdd())); } InternalBdd InternalBdd::restrict(InternalBdd const& constraint) const { - return InternalBdd(this->getDdManager(), this->getCuddBdd().Restrict(constraint.getCuddBdd()), metaVariables); + return InternalBdd(ddManager, this->getCuddBdd().Restrict(constraint.getCuddBdd())); } - InternalBdd InternalBdd::swapVariables(std::vector const>, std::reference_wrapper const>>> const& fromTo) const { + InternalBdd InternalBdd::swapVariables(std::vector const>, std::reference_wrapper const>>> const& fromTo) const { std::vector fromBdd; std::vector toBdd; for (auto const& metaVariablePair : fromTo) { @@ -107,11 +108,11 @@ namespace storm { } // Finally, call CUDD to swap the variables. - return InternalBdd(this->getDdManager(), this->getCuddBdd().SwapVariables(fromBdd, toBdd), newContainedMetaVariables); + return InternalBdd(ddManager, this->getCuddBdd().SwapVariables(fromBdd, toBdd)); } InternalBdd InternalBdd::getSupport() const { - return InternalBdd(this->getDdManager(), this->getCuddBdd().Support(), this->getContainedMetaVariables()); + return InternalBdd(ddManager, this->getCuddBdd().Support()); } uint_fast64_t InternalBdd::getNonZeroCount(uint_fast64_t numberOfDdVariables) const { @@ -155,7 +156,7 @@ namespace storm { // Open the file, dump the DD and close it again. FILE* filePointer = fopen(filename.c_str() , "w"); std::vector cuddBddVector = { this->getCuddBdd() }; - this->getDdManager()->getCuddManager().DumpDot(cuddBddVector, &ddVariableNames[0], &ddNames[0], filePointer); + ddManager->getCuddManager().DumpDot(cuddBddVector, &ddVariableNames[0], &ddNames[0], filePointer); fclose(filePointer); // Finally, delete the names. @@ -176,27 +177,10 @@ namespace storm { } template - Add InternalBdd::toAdd() const { - return Add(this->getCuddBdd().Add()); + InternalAdd InternalBdd::toAdd() const { + return InternalAdd(ddManager, this->getCuddBdd().Add()); } - - - - - - - - - - - - - - - - - template DdNode* InternalBdd::fromVectorRec(::DdManager* manager, uint_fast64_t& currentOffset, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::vector const& values, Odd const& odd, std::vector const& ddVariableIndices, std::function const& filter) { if (currentLevel == maxLevel) { diff --git a/src/storage/dd/cudd/InternalCuddBdd.h b/src/storage/dd/cudd/InternalCuddBdd.h index f34481cc7..a24a561ff 100644 --- a/src/storage/dd/cudd/InternalCuddBdd.h +++ b/src/storage/dd/cudd/InternalCuddBdd.h @@ -7,7 +7,6 @@ #include "src/storage/dd/InternalBdd.h" #include "src/storage/dd/InternalAdd.h" -#include "src/storage/dd/DdManager.h" #include "src/storage/dd/DdMetaVariable.h" // Include the C++-interface of CUDD. @@ -27,6 +26,9 @@ namespace storm { } namespace dd { + template + class InternalDdManager; + template class Odd; @@ -40,7 +42,7 @@ namespace storm { * @param cuddBdd The CUDD BDD to store. * @param containedMetaVariables The meta variables that appear in the DD. */ - InternalBdd(std::shared_ptr const> ddManager, BDD cuddBdd); + InternalBdd(InternalDdManager const* ddManager, BDD cuddBdd); // Instantiate all copy/move constructors/assignments with the default implementation. InternalBdd() = default; @@ -60,7 +62,7 @@ namespace storm { * @return The resulting BDD. */ template - static InternalBdd fromVector(std::shared_ptr const> ddManager, std::vector const& values, Odd const& odd, std::set const& metaVariables, std::function const& filter); + static InternalBdd fromVector(InternalDdManager const* ddManager, std::vector const& values, Odd const& odd, std::vector const& sortedDdVariableIndices, std::function const& filter); /*! * Retrieves whether the two BDDs represent the same function. @@ -330,7 +332,7 @@ namespace storm { */ DdNode* getCuddDdNode() const; - std::shared_ptr const> ddManager; + InternalDdManager const* ddManager; BDD cuddBdd; }; diff --git a/src/storage/dd/cudd/InternalCuddDdManager.cpp b/src/storage/dd/cudd/InternalCuddDdManager.cpp new file mode 100644 index 000000000..a543cc24b --- /dev/null +++ b/src/storage/dd/cudd/InternalCuddDdManager.cpp @@ -0,0 +1,88 @@ +#include "src/storage/dd/cudd/InternalCuddDdManager.h" + +#include "src/settings/SettingsManager.h" +#include "src/settings/modules/CuddSettings.h" + +namespace storm { + namespace dd { + + InternalDdManager::InternalDdManager() : cuddManager(), reorderingTechnique(CUDD_REORDER_NONE) { + this->cuddManager.SetMaxMemory(static_cast(storm::settings::cuddSettings().getMaximalMemory() * 1024ul * 1024ul)); + this->cuddManager.SetEpsilon(storm::settings::cuddSettings().getConstantPrecision()); + + // Now set the selected reordering technique. + storm::settings::modules::CuddSettings::ReorderingTechnique reorderingTechniqueAsSetting = storm::settings::cuddSettings().getReorderingTechnique(); + switch (reorderingTechniqueAsSetting) { + case storm::settings::modules::CuddSettings::ReorderingTechnique::None: this->reorderingTechnique = CUDD_REORDER_NONE; break; + case storm::settings::modules::CuddSettings::ReorderingTechnique::Random: this->reorderingTechnique = CUDD_REORDER_RANDOM; break; + case storm::settings::modules::CuddSettings::ReorderingTechnique::RandomPivot: this->reorderingTechnique = CUDD_REORDER_RANDOM_PIVOT; break; + case storm::settings::modules::CuddSettings::ReorderingTechnique::Sift: this->reorderingTechnique = CUDD_REORDER_SIFT; break; + case storm::settings::modules::CuddSettings::ReorderingTechnique::SiftConv: this->reorderingTechnique = CUDD_REORDER_SIFT_CONVERGE; break; + case storm::settings::modules::CuddSettings::ReorderingTechnique::SymmetricSift: this->reorderingTechnique = CUDD_REORDER_SYMM_SIFT; break; + case storm::settings::modules::CuddSettings::ReorderingTechnique::SymmetricSiftConv: this->reorderingTechnique = CUDD_REORDER_SYMM_SIFT_CONV; break; + case storm::settings::modules::CuddSettings::ReorderingTechnique::GroupSift: this->reorderingTechnique = CUDD_REORDER_GROUP_SIFT; break; + case storm::settings::modules::CuddSettings::ReorderingTechnique::GroupSiftConv: this->reorderingTechnique = CUDD_REORDER_GROUP_SIFT_CONV; break; + case storm::settings::modules::CuddSettings::ReorderingTechnique::Win2: this->reorderingTechnique = CUDD_REORDER_WINDOW2; break; + case storm::settings::modules::CuddSettings::ReorderingTechnique::Win2Conv: this->reorderingTechnique = CUDD_REORDER_WINDOW2_CONV; break; + case storm::settings::modules::CuddSettings::ReorderingTechnique::Win3: this->reorderingTechnique = CUDD_REORDER_WINDOW3; break; + case storm::settings::modules::CuddSettings::ReorderingTechnique::Win3Conv: this->reorderingTechnique = CUDD_REORDER_WINDOW3_CONV; break; + case storm::settings::modules::CuddSettings::ReorderingTechnique::Win4: this->reorderingTechnique = CUDD_REORDER_WINDOW4; break; + case storm::settings::modules::CuddSettings::ReorderingTechnique::Win4Conv: this->reorderingTechnique = CUDD_REORDER_WINDOW4_CONV; break; + case storm::settings::modules::CuddSettings::ReorderingTechnique::Annealing: this->reorderingTechnique = CUDD_REORDER_ANNEALING; break; + case storm::settings::modules::CuddSettings::ReorderingTechnique::Genetic: this->reorderingTechnique = CUDD_REORDER_GENETIC; break; + case storm::settings::modules::CuddSettings::ReorderingTechnique::Exact: this->reorderingTechnique = CUDD_REORDER_EXACT; break; + } + } + + InternalBdd InternalDdManager::getBddOne() const { + return InternalBdd(this, cuddManager.bddOne()); + } + + template + InternalAdd InternalDdManager::getAddOne() const { + return InternalAdd(this, cuddManager.addOne()); + } + + InternalBdd InternalDdManager::getBddZero() const { + return InternalBdd(this, cuddManager.bddZero()); + } + + template + InternalAdd InternalDdManager::getAddZero() const { + return InternalAdd(this, cuddManager.addZero()); + } + + template + InternalAdd InternalDdManager::getConstant(ValueType const& value) const { + return InternalAdd(this, cuddManager.constant(value)); + } + + std::pair, InternalBdd> InternalDdManager::createNewDdVariablePair() { + std::pair, InternalBdd> result; + result.first = InternalBdd(this, cuddManager.bddVar()); + result.second = InternalBdd(this, cuddManager.bddVar()); + + // Connect the two variables so they are not 'torn apart' during dynamic reordering. + cuddManager.MakeTreeNode(result.first.getIndex(), 2, MTR_FIXED); + + return result; + } + + void InternalDdManager::allowDynamicReordering(bool value) { + if (value) { + this->getCuddManager().AutodynEnable(this->reorderingTechnique); + } else { + this->getCuddManager().AutodynDisable(); + } + } + + bool InternalDdManager::isDynamicReorderingAllowed() const { + Cudd_ReorderingType type; + return this->getCuddManager().ReorderingStatus(&type); + } + + void InternalDdManager::triggerReordering() { + this->getCuddManager().ReduceHeap(this->reorderingTechnique, 0); + } + } +} \ No newline at end of file diff --git a/src/storage/dd/cudd/InternalCuddDdManager.h b/src/storage/dd/cudd/InternalCuddDdManager.h new file mode 100644 index 000000000..a83b03bc2 --- /dev/null +++ b/src/storage/dd/cudd/InternalCuddDdManager.h @@ -0,0 +1,119 @@ +#ifndef STORM_STORAGE_DD_INTERNALCUDDDDMANAGER_H_ +#define STORM_STORAGE_DD_INTERNALCUDDDDMANAGER_H_ + +#include "src/storage/dd/DdType.h" +#include "src/storage/dd/InternalDdManager.h" + +#include "src/storage/dd/cudd/InternalCuddBdd.h" +#include "src/storage/dd/cudd/InternalCuddAdd.h" + +#include "cuddObj.hh" + +namespace storm { + namespace dd { + template + class InternalAdd; + + template + class InternalBdd; + + template<> + class InternalDdManager { + public: + friend class InternalAdd; + friend class InternalBdd; + + /*! + * Creates a new internal manager for CUDD DDs. + */ + InternalDdManager(); + + /*! + * Retrieves a BDD representing the constant one function. + * + * @return A BDD representing the constant one function. + */ + InternalBdd getBddOne() const; + + /*! + * Retrieves an ADD representing the constant one function. + * + * @return An ADD representing the constant one function. + */ + template + InternalAdd getAddOne() const; + + /*! + * Retrieves a BDD representing the constant zero function. + * + * @return A BDD representing the constant zero function. + */ + InternalBdd getBddZero() const; + + /*! + * Retrieves an ADD representing the constant zero function. + * + * @return An ADD representing the constant zero function. + */ + template + InternalAdd getAddZero() const; + + /*! + * Retrieves an ADD representing the constant function with the given value. + * + * @return An ADD representing the constant function with the given value. + */ + template + InternalAdd getConstant(ValueType const& value) const; + + /*! + * Creates a new pair of DD variables and returns the two cubes as a result. + * + * @return The two cubes belonging to the DD variables. + */ + std::pair, InternalBdd> createNewDdVariablePair(); + + /*! + * Sets whether or not dynamic reordering is allowed for the DDs managed by this manager. + * + * @param value If set to true, dynamic reordering is allowed and forbidden otherwise. + */ + void allowDynamicReordering(bool value); + + /*! + * Retrieves whether dynamic reordering is currently allowed. + * + * @return True iff dynamic reordering is currently allowed. + */ + bool isDynamicReorderingAllowed() const; + + /*! + * Triggers a reordering of the DDs managed by this manager. + */ + void triggerReordering(); + + private: + /*! + * Retrieves the underlying CUDD manager. + * + * @return The underlying CUDD manager. + */ + Cudd& getCuddManager(); + + /*! + * Retrieves the underlying CUDD manager. + * + * @return The underlying CUDD manager. + */ + Cudd const& getCuddManager() const; + + // The manager responsible for the DDs created/modified with this DdManager. + Cudd cuddManager; + + // The technique that is used for dynamic reordering. + Cudd_ReorderingType reorderingTechnique; + }; + } +} + +#endif /* STORM_STORAGE_DD_INTERNALCUDDDDMANAGER_H_ */ \ No newline at end of file