diff --git a/src/storm/api/counterexamples.cpp b/src/storm/api/counterexamples.cpp index e880c713e..98c2f07bf 100644 --- a/src/storm/api/counterexamples.cpp +++ b/src/storm/api/counterexamples.cpp @@ -1,6 +1,6 @@ #include "storm/api/counterexamples.h" -#include "storm/environment/environments.h" +#include "storm/environment/Environment.h" namespace storm { namespace api { diff --git a/src/storm/environment/Environment.cpp b/src/storm/environment/Environment.cpp index fb4b0ecee..0836de3f7 100644 --- a/src/storm/environment/Environment.cpp +++ b/src/storm/environment/Environment.cpp @@ -1,28 +1,22 @@ #include "storm/environment/Environment.h" +#include "storm/environment/SubEnvironment.h" #include "storm/environment/solver/SolverEnvironment.h" -#include "storm/environment/solver/MinMaxSolverEnvironment.h" - namespace storm { - Environment::Environment() : solverEnvironment(std::make_unique()) { + Environment::Environment() { // Intentionally left empty. } - Environment::Environment(Environment const& other) : - solverEnvironment(new SolverEnvironment(*other.solverEnvironment)) { - // Intentionally left empty. - } - Environment::~Environment() { // Intentionally left empty. } SolverEnvironment& Environment::solver() { - return *solverEnvironment; + return solverEnvironment.get(); } SolverEnvironment const& Environment::solver() const { - return *solverEnvironment; + return solverEnvironment.get(); } } \ No newline at end of file diff --git a/src/storm/environment/Environment.h b/src/storm/environment/Environment.h index f39198fb4..988ca34c6 100644 --- a/src/storm/environment/Environment.h +++ b/src/storm/environment/Environment.h @@ -1,10 +1,9 @@ #pragma once -#include +#include "storm/environment/SubEnvironment.h" namespace storm { - // Forward declare sub-environments class SolverEnvironment; @@ -12,8 +11,6 @@ namespace storm { public: Environment(); - Environment(Environment const& other); - virtual ~Environment(); SolverEnvironment& solver(); @@ -21,9 +18,7 @@ namespace storm { private: - std::unique_ptr solverEnvironment; - - + SubEnvironment solverEnvironment; }; } diff --git a/src/storm/environment/SubEnvironment.h b/src/storm/environment/SubEnvironment.h new file mode 100644 index 000000000..99777f30b --- /dev/null +++ b/src/storm/environment/SubEnvironment.h @@ -0,0 +1,38 @@ +#pragma once + +#include + +namespace storm { + + + template + class SubEnvironment { + public: + + SubEnvironment() : subEnv(std::make_unique()) { + // Intentionally left empty + } + + SubEnvironment(SubEnvironment const& other) : subEnv(new EnvironmentType(*other.subEnv)) { + // Intentionally left empty + } + + SubEnvironment& operator=(SubEnvironment const& other) { + subEnv = std::make_unique(*other.subEnv); + return *this; + } + + EnvironmentType const& get() const { + return *subEnv; + } + + EnvironmentType& get() { + return *subEnv; + } + + private: + std::unique_ptr subEnv; + + }; +} + diff --git a/src/storm/environment/environments.h b/src/storm/environment/environments.h deleted file mode 100644 index 5023df214..000000000 --- a/src/storm/environment/environments.h +++ /dev/null @@ -1,6 +0,0 @@ -#pragma once - -#include "storm/environment/Environment.h" -//#include "storm/environment/solver/SolverEnvironment.h" -//#include "storm/environment/solver/MinMaxSolverEnvironment.h" - diff --git a/src/storm/environment/solver/MinMaxSolverEnvironment.h b/src/storm/environment/solver/MinMaxSolverEnvironment.h index 67921e1cf..6cca14221 100644 --- a/src/storm/environment/solver/MinMaxSolverEnvironment.h +++ b/src/storm/environment/solver/MinMaxSolverEnvironment.h @@ -1,5 +1,7 @@ #pragma once +#include "storm/environment/solver/SolverEnvironment.h" + #include "storm/adapters/RationalNumberAdapter.h" #include "storm/solver/SolverSelectionOptions.h" #include "storm/solver/MultiplicationStyle.h" diff --git a/src/storm/environment/solver/SolverEnvironment.cpp b/src/storm/environment/solver/SolverEnvironment.cpp index 7cba341d8..01f3484b0 100644 --- a/src/storm/environment/solver/SolverEnvironment.cpp +++ b/src/storm/environment/solver/SolverEnvironment.cpp @@ -1,19 +1,13 @@ #include "storm/environment/solver/SolverEnvironment.h" #include "storm/environment/solver/MinMaxSolverEnvironment.h" +#include "storm/settings/SettingsManager.h" +#include "storm/settings/modules/GeneralSettings.h" + namespace storm { - SolverEnvironment::SolverEnvironment() : -// eigenSolverEnvironment(std::make_unique()), - // gmmxxSolverEnvironment(std::make_unique()), - minMaxSolverEnvironment(std::make_unique()) //, -// nativeSolverEnvironment(std::make_unique()) { - { } - - SolverEnvironment::SolverEnvironment(SolverEnvironment const& other) : - minMaxSolverEnvironment(new MinMaxSolverEnvironment(*other.minMaxSolverEnvironment)), - forceSoundness(other.forceSoundness) { - // Intentionally left empty + SolverEnvironment::SolverEnvironment() { + forceSoundness = storm::settings::getModule().isSoundSet(); } SolverEnvironment::~SolverEnvironment() { @@ -21,11 +15,11 @@ namespace storm { } MinMaxSolverEnvironment& SolverEnvironment::minMax() { - return *minMaxSolverEnvironment; + return minMaxSolverEnvironment.get(); } - MinMaxSolverEnvironment const& SolverEnvironment::minMax() const{ - return *minMaxSolverEnvironment; + MinMaxSolverEnvironment const& SolverEnvironment::minMax() const { + return minMaxSolverEnvironment.get(); } bool SolverEnvironment::isForceSoundness() const { diff --git a/src/storm/environment/solver/SolverEnvironment.h b/src/storm/environment/solver/SolverEnvironment.h index af3fb0309..22b47234a 100644 --- a/src/storm/environment/solver/SolverEnvironment.h +++ b/src/storm/environment/solver/SolverEnvironment.h @@ -2,6 +2,9 @@ #include +#include "storm/environment/Environment.h" +#include "storm/environment/SubEnvironment.h" + namespace storm { // Forward declare subenvironments @@ -14,7 +17,6 @@ namespace storm { public: SolverEnvironment(); - SolverEnvironment(SolverEnvironment const& other); ~SolverEnvironment(); // EigenSolverEnvironment& eigen(); @@ -32,7 +34,7 @@ namespace storm { private: // std::unique_ptr eigenSolverEnvironment; // std::unique_ptr gmmxxSolverEnvironment; - std::unique_ptr minMaxSolverEnvironment; + SubEnvironment minMaxSolverEnvironment; // std::unique_ptr nativeSolverEnvironment; bool forceSoundness; diff --git a/src/storm/modelchecker/AbstractModelChecker.cpp b/src/storm/modelchecker/AbstractModelChecker.cpp index 1a4b2be37..40d23d7c5 100644 --- a/src/storm/modelchecker/AbstractModelChecker.cpp +++ b/src/storm/modelchecker/AbstractModelChecker.cpp @@ -9,7 +9,7 @@ #include "storm/exceptions/InvalidArgumentException.h" #include "storm/exceptions/InternalTypeErrorException.h" -#include "storm/environment/environments.h" +#include "storm/environment/Environment.h" #include "storm/models/sparse/Dtmc.h" #include "storm/models/sparse/Ctmc.h" diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp index 9dc4c1925..bde04bf55 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp @@ -10,8 +10,6 @@ #include "storm/solver/MinMaxLinearEquationSolver.h" #include "storm/solver/LinearEquationSolver.h" -#include "storm/environment/Environment.h" -#include "storm/environment/solver/SolverEnvironment.h" #include "storm/environment/solver/MinMaxSolverEnvironment.h" #include "storm/settings/SettingsManager.h" diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index ddf726015..e638a6b15 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -33,8 +33,6 @@ #include "storm/utility/ProgressMeasurement.h" #include "storm/utility/export.h" -#include "storm/environment/Environment.h" -#include "storm/environment/solver/SolverEnvironment.h" #include "storm/environment/solver/MinMaxSolverEnvironment.h" #include "storm/exceptions/InvalidStateException.h" diff --git a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp index 4c4f20bc6..bd75cbc61 100644 --- a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp @@ -2,8 +2,6 @@ #include "storm/utility/ConstantsComparator.h" -#include "storm/environment/Environment.h" -#include "storm/environment/solver/SolverEnvironment.h" #include "storm/environment/solver/MinMaxSolverEnvironment.h" #include "storm/utility/KwekMehlhorn.h" diff --git a/src/storm/solver/LpMinMaxLinearEquationSolver.cpp b/src/storm/solver/LpMinMaxLinearEquationSolver.cpp index c0171aaa0..e7d92fe45 100644 --- a/src/storm/solver/LpMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/LpMinMaxLinearEquationSolver.cpp @@ -1,7 +1,5 @@ #include "storm/solver/LpMinMaxLinearEquationSolver.h" -#include "storm/environment/Environment.h" -#include "storm/environment/solver/SolverEnvironment.h" #include "storm/environment/solver/MinMaxSolverEnvironment.h" #include "storm/utility/vector.h" #include "storm/utility/macros.h" diff --git a/src/storm/solver/MinMaxLinearEquationSolver.cpp b/src/storm/solver/MinMaxLinearEquationSolver.cpp index deb55f3b4..848f78e03 100644 --- a/src/storm/solver/MinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/MinMaxLinearEquationSolver.cpp @@ -7,8 +7,6 @@ #include "storm/solver/TopologicalMinMaxLinearEquationSolver.h" #include "storm/solver/LpMinMaxLinearEquationSolver.h" -#include "storm/environment/Environment.h" -#include "storm/environment/solver/SolverEnvironment.h" #include "storm/environment/solver/MinMaxSolverEnvironment.h" #include "storm/utility/macros.h" diff --git a/src/storm/solver/StandardMinMaxLinearEquationSolver.cpp b/src/storm/solver/StandardMinMaxLinearEquationSolver.cpp index 16158afaa..e3acaa478 100644 --- a/src/storm/solver/StandardMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/StandardMinMaxLinearEquationSolver.cpp @@ -6,8 +6,6 @@ #include "storm/solver/NativeLinearEquationSolver.h" #include "storm/solver/EliminationLinearEquationSolver.h" -#include "storm/environment/Environment.h" -#include "storm/environment/solver/SolverEnvironment.h" #include "storm/environment/solver/MinMaxSolverEnvironment.h" #include "storm/utility/vector.h" diff --git a/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp b/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp index b33a649a0..efdafc610 100644 --- a/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp @@ -7,8 +7,6 @@ #include "storm/utility/constants.h" -#include "storm/environment/Environment.h" -#include "storm/environment/solver/SolverEnvironment.h" #include "storm/environment/solver/MinMaxSolverEnvironment.h" #include "storm/utility/dd.h" diff --git a/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp b/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp index 11eb9e505..11be4637d 100644 --- a/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp @@ -7,8 +7,6 @@ #include "storm/exceptions/InvalidStateException.h" #include "storm/exceptions/InvalidEnvironmentException.h" -#include "storm/environment/Environment.h" -#include "storm/environment/solver/SolverEnvironment.h" #include "storm/environment/solver/MinMaxSolverEnvironment.h" #include "storm/settings/SettingsManager.h"