diff --git a/src/storage/dd/Add.h b/src/storage/dd/Add.h index 68fda1a8f..fe66826ac 100644 --- a/src/storage/dd/Add.h +++ b/src/storage/dd/Add.h @@ -4,11 +4,29 @@ #include "src/storage/dd/Dd.h" #include "src/storage/dd/DdType.h" +#include "src/storage/dd/cudd/InternalCuddAdd.h" + namespace storm { namespace dd { - template + template class Add { + friend class DdManager; + + // Instantiate all copy/move constructors/assignments with the default implementation. + Add() = default; + Add(Add const& other) = default; + Add& operator=(Add const& other) = default; + Add(Add&& other) = default; + Add& operator=(Add&& other) = default; + private: + /*! + * We provide a conversion operator from the BDD to its internal type to ease calling the internal functions. + */ + operator InternalAdd(); + operator InternalAdd const() const; + // The internal ADD that depends on the chosen library. + InternalAdd internalAdd; }; } } diff --git a/src/storage/dd/Bdd.cpp b/src/storage/dd/Bdd.cpp index 5d7201a25..a03655ffc 100644 --- a/src/storage/dd/Bdd.cpp +++ b/src/storage/dd/Bdd.cpp @@ -144,13 +144,28 @@ namespace storm { template Bdd Bdd::swapVariables(std::vector> const& metaVariablePairs) const { std::set newContainedMetaVariables; - std::vector const>, std::reference_wrapper const>>> fromTo; + std::vector> from; + std::vector> to; for (auto const& metaVariablePair : metaVariablePairs) { - std::reference_wrapper const> variable1 = this->getDdManager()->getMetaVariable(metaVariablePair.first); - std::reference_wrapper const> variable2 = this->getDdManager()->getMetaVariable(metaVariablePair.second); - fromTo.push_back(std::make_pair(variable1, variable2)); + DdMetaVariable const& variable1 = this->getDdManager()->getMetaVariable(metaVariablePair.first); + DdMetaVariable const& variable2 = this->getDdManager()->getMetaVariable(metaVariablePair.second); + + // Keep track of the contained meta variables in the DD. + if (this->containsMetaVariable(metaVariablePair.first)) { + newContainedMetaVariables.insert(metaVariablePair.second); + } + if (this->containsMetaVariable(metaVariablePair.second)) { + newContainedMetaVariables.insert(metaVariablePair.first); + } + + for (auto const& ddVariable : variable1.getDdVariables()) { + from.push_back(ddVariable); + } + for (auto const& ddVariable : variable2.getDdVariables()) { + to.push_back(ddVariable); + } } - return Bdd(internalBdd.swapVariables(fromTo)); + return Bdd(this->getDdManager(), internalBdd.swapVariables(from, to), newContainedMetaVariables); } template diff --git a/src/storage/dd/DdManager.cpp b/src/storage/dd/DdManager.cpp index 0f59cb9f3..5580a93e5 100644 --- a/src/storage/dd/DdManager.cpp +++ b/src/storage/dd/DdManager.cpp @@ -265,7 +265,7 @@ namespace storm { } template - std::vector DdManager::getSortedVariableIndices(std::set const& metaVariables) { + std::vector DdManager::getSortedVariableIndices(std::set const& metaVariables) const { std::vector ddVariableIndices; for (auto const& metaVariable : metaVariableMap) { for (auto const& ddVariable : metaVariable.second.getDdVariables()) { diff --git a/src/storage/dd/DdManager.h b/src/storage/dd/DdManager.h index deb6f1430..0b1cf11cd 100644 --- a/src/storage/dd/DdManager.h +++ b/src/storage/dd/DdManager.h @@ -19,6 +19,8 @@ namespace storm { template class DdManager : public std::enable_shared_from_this> { public: + friend class Bdd; + /*! * Creates an empty manager without any meta variables. */ @@ -177,7 +179,7 @@ namespace storm { * @param metaVariable The set of meta variables for which to retrieve the index list. * @return The sorted list of variable indices. */ - std::vector getSortedVariableIndices(std::set const& metaVariables); + std::vector getSortedVariableIndices(std::set const& metaVariables) const; /*! * Retrieves the internal DD manager. diff --git a/src/storage/dd/DdMetaVariable.h b/src/storage/dd/DdMetaVariable.h index 8d8044335..2e92c34c7 100644 --- a/src/storage/dd/DdMetaVariable.h +++ b/src/storage/dd/DdMetaVariable.h @@ -11,6 +11,9 @@ namespace storm { template class DdManager; + template + class Add; + // An enumeration for all legal types of meta variables. enum class MetaVariableType { Bool, Int }; @@ -19,6 +22,8 @@ namespace storm { class DdMetaVariable { public: friend class DdManager; + friend class Bdd; + friend class Add; /*! * Retrieves the name of the meta variable. diff --git a/src/storage/dd/Odd.cpp b/src/storage/dd/Odd.cpp index e69de29bb..23e855253 100644 --- a/src/storage/dd/Odd.cpp +++ b/src/storage/dd/Odd.cpp @@ -0,0 +1 @@ +#include "src/storage/dd/Odd.h" \ No newline at end of file diff --git a/src/storage/dd/Odd.h b/src/storage/dd/Odd.h index 21e5fcc90..a4c0a62a3 100644 --- a/src/storage/dd/Odd.h +++ b/src/storage/dd/Odd.h @@ -6,9 +6,7 @@ namespace storm { namespace dd { template - class Odd { - - }; + class Odd; } } diff --git a/src/storage/dd/cudd/CuddDdManager.cpp b/src/storage/dd/cudd/CuddDdManager.cpp deleted file mode 100644 index 8a3fc35f7..000000000 --- a/src/storage/dd/cudd/CuddDdManager.cpp +++ /dev/null @@ -1,52 +0,0 @@ -#include -#include -#include - -#include "src/storage/dd/cudd/CuddDdManager.h" -#include "src/utility/macros.h" -#include "src/storage/expressions/Variable.h" -#include "src/exceptions/InvalidArgumentException.h" -#include "src/settings/SettingsManager.h" -#include "src/settings/modules/CuddSettings.h" -#include "src/storage/expressions/ExpressionManager.h" -#include "src/storage/dd/cudd/CuddAdd.h" -#include "CuddBdd.h" - - -namespace storm { - namespace dd { - - - - - - - - - - - - - - void DdManager::allowDynamicReordering(bool value) { - if (value) { - this->getCuddManager().AutodynEnable(this->reorderingTechnique); - } else { - this->getCuddManager().AutodynDisable(); - } - } - - bool DdManager::isDynamicReorderingAllowed() const { - Cudd_ReorderingType type; - return this->getCuddManager().ReorderingStatus(&type); - } - - void DdManager::triggerReordering() { - this->getCuddManager().ReduceHeap(this->reorderingTechnique, 0); - } - - std::shared_ptr const> DdManager::asSharedPointer() const { - return this->shared_from_this(); - } - } -} \ No newline at end of file diff --git a/src/storage/dd/cudd/CuddDdManager.h b/src/storage/dd/cudd/CuddDdManager.h deleted file mode 100644 index a3028f769..000000000 --- a/src/storage/dd/cudd/CuddDdManager.h +++ /dev/null @@ -1,217 +0,0 @@ -#ifndef STORM_STORAGE_DD_CUDDDDMANAGER_H_ -#define STORM_STORAGE_DD_CUDDDDMANAGER_H_ - -#include -#include - -#include "src/storage/dd/DdManager.h" -#include "src/storage/dd/cudd/CuddDdMetaVariable.h" -#include "src/utility/OsDetection.h" - -// Include the C++-interface of CUDD. -#include "cuddObj.hh" - -namespace storm { - namespace expressions { - class Variable; - } -} - -namespace storm { - namespace dd { - template<> - class DdManager : public std::enable_shared_from_this> { - public: - friend class Bdd; - friend class Add; - friend class Odd; - friend class DdForwardIterator; - - /*! - * 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; -#ifndef WINDOWS - DdManager(DdManager&& other) = default; - DdManager& operator=(DdManager&& other) = default; -#endif - - /*! - * 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. - */ - 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. - */ - 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. - */ - Add getConstant(double 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. - */ - 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; - - /*! - * Retrieves the manager as a shared pointer. - * - * @return A shared pointer to the manager. - */ - std::shared_ptr const> asSharedPointer() 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; - }; - } -} - -#endif /* STORM_STORAGE_DD_CUDDDDMANAGER_H_ */ \ No newline at end of file diff --git a/src/storage/dd/cudd/CuddDdMetaVariable.cpp b/src/storage/dd/cudd/CuddDdMetaVariable.cpp deleted file mode 100644 index df02d0255..000000000 --- a/src/storage/dd/cudd/CuddDdMetaVariable.cpp +++ /dev/null @@ -1,52 +0,0 @@ -#include "src/storage/dd/cudd/CuddDdMetaVariable.h" -#include "src/storage/dd/cudd/CuddDdManager.h" - -namespace storm { - namespace dd { - DdMetaVariable::DdMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high, std::vector> const& ddVariables, std::shared_ptr> manager) : name(name), type(MetaVariableType::Int), low(low), high(high), ddVariables(ddVariables), cube(manager->getBddOne()), manager(manager) { - // Create the cube of all variables of this meta variable. - for (auto const& ddVariable : this->ddVariables) { - this->cube &= ddVariable; - } - } - - DdMetaVariable::DdMetaVariable(std::string const& name, std::vector> const& ddVariables, std::shared_ptr> manager) : name(name), type(MetaVariableType::Bool), low(0), high(1), ddVariables(ddVariables), cube(manager->getBddOne()), manager(manager) { - // Create the cube of all variables of this meta variable. - for (auto const& ddVariable : this->ddVariables) { - this->cube &= ddVariable; - } - } - - std::string const& DdMetaVariable::getName() const { - return this->name; - } - - DdMetaVariable::MetaVariableType DdMetaVariable::getType() const { - return this->type; - } - - int_fast64_t DdMetaVariable::getLow() const { - return this->low; - } - - int_fast64_t DdMetaVariable::getHigh() const { - return this->high; - } - - std::size_t DdMetaVariable::getNumberOfDdVariables() const { - return this->ddVariables.size(); - } - - std::shared_ptr> DdMetaVariable::getDdManager() const { - return this->manager; - } - - std::vector> const& DdMetaVariable::getDdVariables() const { - return this->ddVariables; - } - - Bdd const& DdMetaVariable::getCube() const { - return this->cube; - } - } -} \ No newline at end of file diff --git a/src/storage/dd/cudd/CuddDdMetaVariable.h b/src/storage/dd/cudd/CuddDdMetaVariable.h deleted file mode 100644 index 8f7f08542..000000000 --- a/src/storage/dd/cudd/CuddDdMetaVariable.h +++ /dev/null @@ -1,144 +0,0 @@ -#ifndef STORM_STORAGE_DD_DDMETAVARIABLE_H_ -#define STORM_STORAGE_DD_DDMETAVARIABLE_H_ - -#include -#include -#include -#include - -#include "utility/OsDetection.h" -#include "src/storage/dd/cudd/CuddBdd.h" -#include "src/storage/dd/DdMetaVariable.h" -#include "src/storage/dd/cudd/CuddDdForwardIterator.h" - - -namespace storm { - namespace dd { - // Forward-declare some classes. - template class DdManager; - template class Odd; - template class Add; - - template<> - class DdMetaVariable { - public: - // Declare the DdManager class as friend so it can access the internals of a meta variable. - friend class DdManager; - friend class Dd; - friend class Bdd; - friend class Add; - friend class Odd; - friend class DdForwardIterator; - - // An enumeration for all legal types of meta variables. - enum class MetaVariableType { Bool, Int }; - - /*! - * 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, std::shared_ptr> manager); - - /*! - * 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, std::shared_ptr> manager); - - // Explictly generate all default versions of copy/move constructors/assignments. - DdMetaVariable(DdMetaVariable const& other) = default; - DdMetaVariable& operator=(DdMetaVariable const& other) = default; -#ifndef WINDOWS - DdMetaVariable(DdMetaVariable&& other) = default; - DdMetaVariable& operator=(DdMetaVariable&& other) = default; -#endif - - /*! - * 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 manager that is responsible for this meta variable. - * - * A pointer to the manager that is responsible for this meta variable. - */ - std::shared_ptr> getDdManager() 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; - - private: - /*! - * 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; - - /*! - * 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; - - // 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; - - // A pointer to the manager responsible for this meta variable. - std::shared_ptr> manager; - }; - } -} - -#endif /* STORM_STORAGE_DD_DDMETAVARIABLE_H_ */ \ No newline at end of file diff --git a/src/storage/dd/cudd/InternalCuddAdd.h b/src/storage/dd/cudd/InternalCuddAdd.h index e69de29bb..fa754584a 100644 --- a/src/storage/dd/cudd/InternalCuddAdd.h +++ b/src/storage/dd/cudd/InternalCuddAdd.h @@ -0,0 +1,60 @@ +#ifndef STORM_STORAGE_DD_CUDD_INTERNALCUDDADD_H_ +#define STORM_STORAGE_DD_CUDD_INTERNALCUDDADD_H_ + +#include + +#include "src/storage/dd/DdType.h" +#include "src/storage/dd/InternalAdd.h" + +// Include the C++-interface of CUDD. +#include "cuddObj.hh" + +namespace storm { + namespace storage { + template class SparseMatrix; + class BitVector; + template class MatrixEntry; + } + + namespace dd { + // Forward-declare some classes. + template class DdManager; + template class Odd; + template class Bdd; + + template + class InternalAdd : public Dd { + public: + /*! + * Creates an ADD that encapsulates the given CUDD ADD. + * + * @param ddManager The manager responsible for this DD. + * @param cuddAdd The CUDD ADD to store. + * @param containedMetaVariables The meta variables that appear in the DD. + */ + Add(InternalDdManager const* ddManager, ADD cuddAdd); + + + private: + /*! + * Retrieves the CUDD ADD object associated with this ADD. + * + * @return The CUDD ADD object associated with this ADD. + */ + ADD getCuddAdd() const; + + /*! + * Retrieves the raw DD node of CUDD associated with this ADD. + * + * @return The DD node of CUDD associated with this ADD. + */ + DdNode* getCuddDdNode() const; + + InternalDdManager const* ddManager; + + ADD cuddBdd; + } + } +} + +#endif /* STORM_STORAGE_DD_CUDD_INTERNALCUDDADD_H_ */ \ No newline at end of file diff --git a/src/storage/dd/cudd/InternalCuddBdd.cpp b/src/storage/dd/cudd/InternalCuddBdd.cpp index f5d032a37..9320ef406 100644 --- a/src/storage/dd/cudd/InternalCuddBdd.cpp +++ b/src/storage/dd/cudd/InternalCuddBdd.cpp @@ -91,23 +91,13 @@ namespace storm { 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& from, std::vector> const& to) const { std::vector fromBdd; std::vector toBdd; - for (auto const& metaVariablePair : fromTo) { - DdMetaVariable const& variable1 = metaVariablePair.first.get(); - DdMetaVariable const& variable2 = metaVariablePair.second.get(); - - // Add the variables to swap to the corresponding vectors. - for (auto const& ddVariable : variable1.getDdVariables()) { - fromBdd.push_back(ddVariable.getCuddBdd()); - } - for (auto const& ddVariable : variable2.getDdVariables()) { - toBdd.push_back(ddVariable.getCuddBdd()); - } + for (auto it1 = from.begin(), ite1 = from.end(), it2 = to.begin(); it1 != ite1; ++it1, ++it2) { + fromBdd.push_back(it1->getCuddBdd()); + toBdd.push_back(it2->getCuddBdd()); } - - // Finally, call CUDD to swap the variables. return InternalBdd(ddManager, this->getCuddBdd().SwapVariables(fromBdd, toBdd)); } diff --git a/src/storage/dd/cudd/InternalCuddBdd.h b/src/storage/dd/cudd/InternalCuddBdd.h index a24a561ff..04e3aabf0 100644 --- a/src/storage/dd/cudd/InternalCuddBdd.h +++ b/src/storage/dd/cudd/InternalCuddBdd.h @@ -7,8 +7,6 @@ #include "src/storage/dd/InternalBdd.h" #include "src/storage/dd/InternalAdd.h" -#include "src/storage/dd/DdMetaVariable.h" - // Include the C++-interface of CUDD. #include "cuddObj.hh" @@ -182,7 +180,7 @@ namespace storm { * @param metaVariablePairs A vector of meta variable pairs that are to be swapped for one another. * @return The resulting BDD. */ - InternalBdd swapVariables(std::vector const>, std::reference_wrapper const>>> const& fromTo) const; + InternalBdd swapVariables(std::vector> const& from, std::vector> const& to) const; /*! * Computes the logical and of the current and the given BDD and existentially abstracts from the given set