From 42cea9c6880e0ba19d9533a7a15f968ad6919d06 Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Tue, 14 Nov 2017 16:19:38 +0100
Subject: [PATCH] better subenvironments

---
 src/storm/api/counterexamples.cpp             |  2 +-
 src/storm/environment/Environment.cpp         | 14 ++-----
 src/storm/environment/Environment.h           |  9 +----
 src/storm/environment/SubEnvironment.h        | 38 +++++++++++++++++++
 src/storm/environment/environments.h          |  6 ---
 .../solver/MinMaxSolverEnvironment.h          |  2 +
 .../environment/solver/SolverEnvironment.cpp  | 22 ++++-------
 .../environment/solver/SolverEnvironment.h    |  6 ++-
 .../modelchecker/AbstractModelChecker.cpp     |  2 +-
 ...dpRewardBoundedPcaaWeightVectorChecker.cpp |  2 -
 .../prctl/helper/SparseMdpPrctlHelper.cpp     |  2 -
 .../IterativeMinMaxLinearEquationSolver.cpp   |  2 -
 .../solver/LpMinMaxLinearEquationSolver.cpp   |  2 -
 .../solver/MinMaxLinearEquationSolver.cpp     |  2 -
 .../StandardMinMaxLinearEquationSolver.cpp    |  2 -
 .../SymbolicMinMaxLinearEquationSolver.cpp    |  2 -
 .../TopologicalMinMaxLinearEquationSolver.cpp |  2 -
 17 files changed, 60 insertions(+), 57 deletions(-)
 create mode 100644 src/storm/environment/SubEnvironment.h
 delete mode 100644 src/storm/environment/environments.h

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<SolverEnvironment>()) {
+    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<memory>
+#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> solverEnvironment;
-        
-        
+        SubEnvironment<SolverEnvironment> 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<memory>
+
+namespace storm {
+    
+    
+    template<typename EnvironmentType>
+    class SubEnvironment {
+    public:
+        
+        SubEnvironment() : subEnv(std::make_unique<EnvironmentType>()) {
+            // Intentionally left empty
+        }
+        
+        SubEnvironment(SubEnvironment const& other) : subEnv(new EnvironmentType(*other.subEnv)) {
+            // Intentionally left empty
+        }
+        
+        SubEnvironment<EnvironmentType>& operator=(SubEnvironment const& other) {
+            subEnv = std::make_unique<EnvironmentType>(*other.subEnv);
+            return *this;
+        }
+        
+        EnvironmentType const& get() const {
+            return *subEnv;
+        }
+        
+        EnvironmentType& get() {
+            return *subEnv;
+        }
+        
+    private:
+        std::unique_ptr<EnvironmentType> 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<EigenSolverEnvironment>()),
- //       gmmxxSolverEnvironment(std::make_unique<GmmxxSolverEnvironment>()),
-        minMaxSolverEnvironment(std::make_unique<MinMaxSolverEnvironment>()) //,
-//        nativeSolverEnvironment(std::make_unique<NativeSolverEnvironment>()) {
-    { }
-    
-    SolverEnvironment::SolverEnvironment(SolverEnvironment const& other) :
-            minMaxSolverEnvironment(new MinMaxSolverEnvironment(*other.minMaxSolverEnvironment)),
-            forceSoundness(other.forceSoundness) {
-        // Intentionally left empty
+    SolverEnvironment::SolverEnvironment() {
+        forceSoundness = storm::settings::getModule<storm::settings::modules::GeneralSettings>().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<memory>
 
+#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> eigenSolverEnvironment;
 //        std::unique_ptr<GmmxxSolverEnvironment> gmmxxSolverEnvironment;
-        std::unique_ptr<MinMaxSolverEnvironment> minMaxSolverEnvironment;
+        SubEnvironment<MinMaxSolverEnvironment> minMaxSolverEnvironment;
  //       std::unique_ptr<NativeSolverEnvironment> 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"