moves-rwth · sjunges · Dec 17, 2023
diff --git a/src/storm-pars-cli/solutionFunctions.h b/src/storm-pars-cli/solutionFunctions.h
@@ -41,12 +41,12 @@ void computeSolutionFunctionsWithSparseEngine(std::shared_ptr<storm::models::spa
                 auto dtmc = model->template as<storm::models::sparse::Dtmc<ValueType>>();
                 std::optional<ValueType> rationalFunction = result->asExplicitQuantitativeCheckResult<ValueType>()[*model->getInitialStates().begin()];
                 auto constraintCollector = storm::analysis::ConstraintCollector<ValueType>(*dtmc);
-                storm::api::exportParametricResultToFile<ValueType>(rationalFunction, constraintCollector, parametricSettings.exportResultPath());
+                storm::api::exportParametricResultToFile(rationalFunction, constraintCollector, parametricSettings.exportResultPath());
             } else if (parametricSettings.exportResultToFile() && model->isOfType(storm::models::ModelType::Ctmc)) {
                 auto ctmc = model->template as<storm::models::sparse::Ctmc<ValueType>>();
                 std::optional<ValueType> rationalFunction = result->asExplicitQuantitativeCheckResult<ValueType>()[*model->getInitialStates().begin()];
                 auto constraintCollector = storm::analysis::ConstraintCollector<ValueType>(*ctmc);
-                storm::api::exportParametricResultToFile<ValueType>(rationalFunction, constraintCollector, parametricSettings.exportResultPath());
+                storm::api::exportParametricResultToFile(rationalFunction, constraintCollector, parametricSettings.exportResultPath());
             }
         });
 }
@@ -69,7 +69,7 @@ void computeSolutionFunctionsWithSymbolicEngine(std::shared_ptr<storm::models::s
             if (parametricSettings.exportResultToFile() && model->isOfType(storm::models::ModelType::Dtmc)) {
                 STORM_LOG_WARN("For symbolic engines, we currently do not support collecting graph-preserving constraints.");
                 std::optional<ValueType> rationalFunction = result->asSymbolicQuantitativeCheckResult<DdType, ValueType>().sum();
-                storm::api::exportParametricResultToFile<ValueType>(rationalFunction, storm::NullRef, parametricSettings.exportResultPath());
+                storm::api::exportParametricResultToFile(rationalFunction, storm::NullRef, parametricSettings.exportResultPath());
             }
         });
 }

diff --git a/src/storm-pars/api/export.cpp b/src/storm-pars/api/export.cpp
@@ -0,0 +1,60 @@
+
+#include "storm-pars/api/export.h"
+#include <carl/formula/Formula.h>
+#include "storm/analysis/GraphConditions.h"
+#include "storm/exceptions/NotSupportedException.h"
+#include "storm/io/file.h"
+#include "storm/utility/OptionalRef.h"
+#include "storm/utility/macros.h"
+
+namespace storm::api {
+
+// template<typename ValueType>
+// void exportParametricResultToFile(std::optional<ValueType>, storm::OptionalRef<storm::analysis::ConstraintCollector<ValueType> const> const&,
+//                                   std::string const&) {
+//     STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Cannot export non-parametric result.");
+// }
+
+void exportParametricResultToFile(std::optional<storm::RationalFunction> result,
+                                  storm::OptionalRef<storm::analysis::ConstraintCollector<storm::RationalFunction> const> const& constraintCollector,
+                                  std::string const& path) {
+    std::ofstream filestream;
+    storm::utility::openFile(path, filestream);
+    if (constraintCollector.has_value()) {
+        filestream << "$Parameters: ";
+        auto const& vars = constraintCollector->getVariables();
+        std::copy(vars.begin(), vars.end(), std::ostream_iterator<storm::RationalFunctionVariable>(filestream, "; "));
+        filestream << '\n';
+    } else {
+        if (result) {
+            filestream << "$Parameters: ";
+            auto const& vars = result->gatherVariables();
+            std::copy(vars.begin(), vars.end(), std::ostream_iterator<storm::RationalFunctionVariable>(filestream, "; "));
+            filestream << '\n';
+        }
+    }
+    if (result) {
+        filestream << "$Result: " << result->toString(false, true) << '\n';
+    }
+    if (constraintCollector.has_value()) {
+        filestream << "$Well-formed Constraints: \n";
+        std::vector<std::string> stringConstraints;
+        std::transform(constraintCollector->getWellformedConstraints().begin(), constraintCollector->getWellformedConstraints().end(),
+                       std::back_inserter(stringConstraints),
+                       [](carl::Formula<typename storm::Polynomial::PolyType> const& c) -> std::string { return c.toString(); });
+        std::copy(stringConstraints.begin(), stringConstraints.end(), std::ostream_iterator<std::string>(filestream, "\n"));
+        filestream << "$Graph-preserving Constraints: \n";
+        stringConstraints.clear();
+        std::transform(constraintCollector->getGraphPreservingConstraints().begin(), constraintCollector->getGraphPreservingConstraints().end(),
+                       std::back_inserter(stringConstraints),
+                       [](carl::Formula<typename storm::Polynomial::PolyType> const& c) -> std::string { return c.toString(); });
+        std::copy(stringConstraints.begin(), stringConstraints.end(), std::ostream_iterator<std::string>(filestream, "\n"));
+    }
+    storm::utility::closeFile(filestream);
+}
+
+// template void exportParametricResultToFile<storm::RationalFunction>(std::optional<storm::RationalFunction>,
+// storm::OptionalRef<storm::analysis::ConstraintCollector<storm::RationalFunction> const> const&,
+//                                   std::string const&);
+
+}  // namespace storm::api
diff --git a/src/storm-pars/api/export.h b/src/storm-pars/api/export.h
@@ -1,54 +1,19 @@
-#include "storm/analysis/GraphConditions.h"
+#include <memory>
+#include <vector>
+#include "storm/adapters/RationalFunctionForward.h"
 #include "storm/exceptions/NotSupportedException.h"
 #include "storm/io/file.h"
 #include "storm/utility/OptionalRef.h"
 #include "storm/utility/macros.h"
 
 namespace storm {
-namespace api {
-template<typename ValueType>
-void exportParametricResultToFile(std::optional<ValueType>, storm::OptionalRef<storm::analysis::ConstraintCollector<ValueType> const> const&,
-                                  std::string const&) {
-    STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Cannot export non-parametric result.");
+namespace analysis {
+template<typename V>
+class ConstraintCollector;
 }
 
-template<>
-inline void exportParametricResultToFile(std::optional<storm::RationalFunction> result,
-                                         storm::OptionalRef<storm::analysis::ConstraintCollector<storm::RationalFunction> const> const& constraintCollector,
-                                         std::string const& path) {
-    std::ofstream filestream;
-    storm::utility::openFile(path, filestream);
-    if (constraintCollector.has_value()) {
-        filestream << "$Parameters: ";
-        auto const& vars = constraintCollector->getVariables();
-        std::copy(vars.begin(), vars.end(), std::ostream_iterator<storm::RationalFunctionVariable>(filestream, "; "));
-        filestream << '\n';
-    } else {
-        if (result) {
-            filestream << "$Parameters: ";
-            auto const& vars = result->gatherVariables();
-            std::copy(vars.begin(), vars.end(), std::ostream_iterator<storm::RationalFunctionVariable>(filestream, "; "));
-            filestream << '\n';
-        }
-    }
-    if (result) {
-        filestream << "$Result: " << result->toString(false, true) << '\n';
-    }
-    if (constraintCollector.has_value()) {
-        filestream << "$Well-formed Constraints: \n";
-        std::vector<std::string> stringConstraints;
-        std::transform(constraintCollector->getWellformedConstraints().begin(), constraintCollector->getWellformedConstraints().end(),
-                       std::back_inserter(stringConstraints),
-                       [](carl::Formula<typename storm::Polynomial::PolyType> const& c) -> std::string { return c.toString(); });
-        std::copy(stringConstraints.begin(), stringConstraints.end(), std::ostream_iterator<std::string>(filestream, "\n"));
-        filestream << "$Graph-preserving Constraints: \n";
-        stringConstraints.clear();
-        std::transform(constraintCollector->getGraphPreservingConstraints().begin(), constraintCollector->getGraphPreservingConstraints().end(),
-                       std::back_inserter(stringConstraints),
-                       [](carl::Formula<typename storm::Polynomial::PolyType> const& c) -> std::string { return c.toString(); });
-        std::copy(stringConstraints.begin(), stringConstraints.end(), std::ostream_iterator<std::string>(filestream, "\n"));
-    }
-    storm::utility::closeFile(filestream);
-}
+namespace api {
+void exportParametricResultToFile(std::optional<storm::RationalFunction>,
+                                  storm::OptionalRef<storm::analysis::ConstraintCollector<storm::RationalFunction> const> const&, std::string const&);
 }  // namespace api
 }  // namespace storm
diff --git a/src/storm-pars/derivative/GradientDescentInstantiationSearcher.h b/src/storm-pars/derivative/GradientDescentInstantiationSearcher.h
@@ -1,5 +1,6 @@
 #pragma once
 
+#include <boost/variant.hpp>
 #include <map>
 #include <memory>
 #include "GradientDescentConstraintMethod.h"

diff --git a/src/storm/analysis/GraphConditions.cpp b/src/storm/analysis/GraphConditions.cpp
@@ -1,5 +1,7 @@
 
 #include "GraphConditions.h"
+
+#include <carl/formula/Formula.h>
 #include "storm/exceptions/NotImplementedException.h"
 #include "storm/exceptions/UnexpectedException.h"
 #include "storm/models/sparse/Ctmc.h"
@@ -15,6 +17,9 @@ ConstraintCollector<ValueType>::ConstraintCollector(storm::models::sparse::Model
     process(model);
 }
 
+template<typename ValueType>
+ConstraintCollector<ValueType>::~ConstraintCollector() = default;
+
 template<typename ValueType>
 std::unordered_set<typename ConstraintType<ValueType>::val> const& ConstraintCollector<ValueType>::getWellformedConstraints() const {
     return this->wellformedConstraintSet;

diff --git a/src/storm/analysis/GraphConditions.h b/src/storm/analysis/GraphConditions.h
@@ -1,11 +1,15 @@
 #pragma once
 
-#include <carl/formula/Formula.h>
 #include <type_traits>
 #include <unordered_set>
 #include "storm/adapters/RationalFunctionAdapter.h"
 #include "storm/models/sparse/Dtmc.h"
 
+namespace carl {
+template<typename V>
+class Formula;
+}
+
 namespace storm {
 namespace analysis {
 
@@ -46,6 +50,8 @@ class ConstraintCollector {
      */
     ConstraintCollector(storm::models::sparse::Model<ValueType> const& model);
 
+    ~ConstraintCollector();
+
     /*!
      * Returns the set of wellformed-ness constraints.
      *