diff --git a/src/storage/dd/CuddDd.cpp b/src/storage/dd/CuddDd.cpp index be51d5a98..873107d27 100644 --- a/src/storage/dd/CuddDd.cpp +++ b/src/storage/dd/CuddDd.cpp @@ -1,3 +1,5 @@ +#include + #include "src/storage/dd/CuddDd.h" #include "src/storage/dd/CuddDdManager.h" @@ -5,7 +7,7 @@ namespace storm { namespace dd { - Dd::Dd(std::shared_ptr> ddManager, ADD cuddAdd, std::set const& containedMetaVariableNames) noexcept : ddManager(ddManager), cuddAdd(cuddAdd), containedMetaVariableNames(containedMetaVariableNames) { + Dd::Dd(std::shared_ptr> ddManager, ADD cuddAdd, std::set const& containedMetaVariableNames) : ddManager(ddManager), cuddAdd(cuddAdd), containedMetaVariableNames(containedMetaVariableNames) { // Intentionally left empty. } diff --git a/src/storage/dd/CuddDd.h b/src/storage/dd/CuddDd.h index 0aa71889e..74a1a6c7f 100644 --- a/src/storage/dd/CuddDd.h +++ b/src/storage/dd/CuddDd.h @@ -6,6 +6,7 @@ #include #include "src/storage/dd/Dd.h" +#include "utility\OsDetection.h" // Include the C++-interface of CUDD. #include "cuddObj.hh" @@ -24,9 +25,11 @@ namespace storm { // Instantiate all copy/move constructors/assignments with the default implementation. Dd() = default; Dd(Dd const& other) = default; - Dd(Dd&& other) = default; - Dd& operator=(Dd const& other) = default; - Dd& operator=(Dd&& other) = default; + Dd& operator=(Dd const& other) = default; + #ifndef WINDOWS + Dd(Dd&& other) = default; + Dd& operator=(Dd&& other) = default; + #endif /*! * Retrieves whether the two DDs represent the same function. @@ -387,7 +390,7 @@ namespace storm { * @param cuddAdd The CUDD ADD to store. * @param */ - Dd(std::shared_ptr> ddManager, ADD cuddAdd, std::set const& containedMetaVariableNames) noexcept; + Dd(std::shared_ptr> ddManager, ADD cuddAdd, std::set const& containedMetaVariableNames); // A pointer to the manager responsible for this DD. std::shared_ptr> ddManager; diff --git a/src/storage/dd/CuddDdManager.cpp b/src/storage/dd/CuddDdManager.cpp index e6ca9e8e7..931b968d9 100644 --- a/src/storage/dd/CuddDdManager.cpp +++ b/src/storage/dd/CuddDdManager.cpp @@ -5,7 +5,7 @@ namespace storm { namespace dd { - DdManager::DdManager() noexcept : metaVariableMap(), cuddManager() { + DdManager::DdManager() : metaVariableMap(), cuddManager() { // Intentionally left empty. } diff --git a/src/storage/dd/CuddDdManager.h b/src/storage/dd/CuddDdManager.h index 76da42bd5..25feb01cf 100644 --- a/src/storage/dd/CuddDdManager.h +++ b/src/storage/dd/CuddDdManager.h @@ -6,6 +6,7 @@ #include "src/storage/dd/DdManager.h" #include "src/storage/dd/DdMetaVariable.h" #include "src/storage/dd/CuddDd.h" +#include "utility\OsDetection.h" // Include the C++-interface of CUDD. #include "cuddObj.hh" @@ -21,13 +22,17 @@ namespace storm { /*! * Creates an empty manager without any meta variables. */ - DdManager() noexcept; + DdManager(); // Explictly forbid copying a DdManager, but allow moving it. DdManager(DdManager const& other) = delete; - DdManager(DdManager&& other) = default; - DdManager& operator=(DdManager const& other) = delete; - DdManager& operator=(DdManager&& other) = default; + DdManager& operator=(DdManager const& other) = delete; + #ifndef WINDOWS + DdManager(DdManager&& other) = default; + DdManager& operator=(DdManager&& other) = default; + #endif + + /*! * Retrieves a DD representing the constant one function. diff --git a/src/storage/dd/DdMetaVariable.cpp b/src/storage/dd/DdMetaVariable.cpp index 72e7baba5..7671289fc 100644 --- a/src/storage/dd/DdMetaVariable.cpp +++ b/src/storage/dd/DdMetaVariable.cpp @@ -4,7 +4,7 @@ namespace storm { namespace dd { template - DdMetaVariable::DdMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high, std::vector> const& ddVariables, std::shared_ptr> manager) noexcept : name(name), low(low), high(high), ddVariables(ddVariables), cube(manager->getOne()), manager(manager) { + DdMetaVariable::DdMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high, std::vector> const& ddVariables, std::shared_ptr> manager) : name(name), low(low), high(high), ddVariables(ddVariables), cube(manager->getOne()), manager(manager) { // Create the cube of all variables of this meta variable. for (auto const& ddVariable : this->ddVariables) { this->cube *= ddVariable; diff --git a/src/storage/dd/DdMetaVariable.h b/src/storage/dd/DdMetaVariable.h index c5e7c00cf..2212cf265 100644 --- a/src/storage/dd/DdMetaVariable.h +++ b/src/storage/dd/DdMetaVariable.h @@ -6,6 +6,7 @@ #include #include +#include "utility\OsDetection.h" #include "src/storage/dd/CuddDd.h" namespace storm { @@ -29,13 +30,17 @@ namespace storm { * @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) noexcept; + DdMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high, std::vector> const& ddVariables, std::shared_ptr> manager); // Explictly generate all default versions of copy/move constructors/assignments. DdMetaVariable(DdMetaVariable const& other) = default; - DdMetaVariable(DdMetaVariable&& other) = default; - DdMetaVariable& operator=(DdMetaVariable const& other) = default; - DdMetaVariable& operator=(DdMetaVariable&& 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.