From 5722c1258c99a5a35fd26974ea44f1626580afff Mon Sep 17 00:00:00 2001
From: Sebastian Junges <sebastian.junges@gmail.com>
Date: Mon, 20 Jul 2020 17:14:24 -0700
Subject: [PATCH] pipe all rf-variable creations through a single object file
---
.../transformer/ApplyFiniteSchedulerToPomdp.cpp | 2 +-
src/storm/adapters/RationalFunctionAdapter.cpp | 7 +++++++
src/storm/adapters/RationalFunctionAdapter.h | 2 ++
src/storm/builder/DdPrismModelBuilder.cpp | 2 +-
.../storage/expressions/ToRationalFunctionVisitor.cpp | 2 +-
5 files changed, 12 insertions(+), 3 deletions(-)
create mode 100644 src/storm/adapters/RationalFunctionAdapter.cpp
diff --git a/src/storm-pomdp/transformer/ApplyFiniteSchedulerToPomdp.cpp b/src/storm-pomdp/transformer/ApplyFiniteSchedulerToPomdp.cpp
index a125289bf..00e443efe 100644
--- a/src/storm-pomdp/transformer/ApplyFiniteSchedulerToPomdp.cpp
+++ b/src/storm-pomdp/transformer/ApplyFiniteSchedulerToPomdp.cpp
@@ -60,7 +60,7 @@ namespace storm {
storm::RationalFunction lastWeight = storm::utility::one<storm::RationalFunction>();
for (uint64_t a = 0; a < pomdp.getNumberOfChoices(state) - 1; ++a) {
std::string varName = "p" + std::to_string(observation) + "_" + std::to_string(a);
- storm::RationalFunction var = ratFuncConstructor.translate(carl::freshRealVariable(varName));
+ storm::RationalFunction var = ratFuncConstructor.translate(storm::createRFVariable(varName));
if (applicationMode == PomdpFscApplicationMode::SIMPLE_LINEAR) {
weights.push_back(collected * var);
collected *= storm::utility::one<storm::RationalFunction>() - var;
diff --git a/src/storm/adapters/RationalFunctionAdapter.cpp b/src/storm/adapters/RationalFunctionAdapter.cpp
new file mode 100644
index 000000000..7218c4454
--- /dev/null
+++ b/src/storm/adapters/RationalFunctionAdapter.cpp
@@ -0,0 +1,7 @@
+#include "storm/adapters/RationalFunctionAdapter.h"
+
+namespace storm {
+ RationalFunctionVariable createRFVariable(std::string const& name) {
+ return carl::freshRealVariable(name);
+ }
+}
\ No newline at end of file
diff --git a/src/storm/adapters/RationalFunctionAdapter.h b/src/storm/adapters/RationalFunctionAdapter.h
index 9ecf8b579..0387aae63 100644
--- a/src/storm/adapters/RationalFunctionAdapter.h
+++ b/src/storm/adapters/RationalFunctionAdapter.h
@@ -41,6 +41,8 @@ namespace carl {
namespace storm {
typedef carl::Variable RationalFunctionVariable;
+ RationalFunctionVariable createRFVariable(std::string const& name);
+
#if defined(STORM_HAVE_CLN) && defined(STORM_USE_CLN_RF)
typedef cln::cl_RA RationalFunctionCoefficient;
#elif defined(STORM_HAVE_GMP) && !defined(STORM_USE_CLN_RF)
diff --git a/src/storm/builder/DdPrismModelBuilder.cpp b/src/storm/builder/DdPrismModelBuilder.cpp
index 9e907a857..b08e9295d 100644
--- a/src/storm/builder/DdPrismModelBuilder.cpp
+++ b/src/storm/builder/DdPrismModelBuilder.cpp
@@ -56,7 +56,7 @@ namespace storm {
void create(storm::prism::Program const& program, storm::adapters::AddExpressionAdapter<Type, storm::RationalFunction>& rowExpressionAdapter) {
for (auto const& constant : program.getConstants()) {
if (!constant.isDefined()) {
- storm::RationalFunctionVariable carlVariable = carl::freshRealVariable(constant.getExpressionVariable().getName());
+ storm::RationalFunctionVariable carlVariable = storm::createRFVariable(constant.getExpressionVariable().getName());
parameters.insert(carlVariable);
auto rf = convertVariableToPolynomial(carlVariable);
rowExpressionAdapter.setValue(constant.getExpressionVariable(), rf);
diff --git a/src/storm/storage/expressions/ToRationalFunctionVisitor.cpp b/src/storm/storage/expressions/ToRationalFunctionVisitor.cpp
index 21ee060ea..21aeddce8 100644
--- a/src/storm/storage/expressions/ToRationalFunctionVisitor.cpp
+++ b/src/storm/storage/expressions/ToRationalFunctionVisitor.cpp
@@ -82,7 +82,7 @@ namespace storm {
if (variablePair != variableToVariableMap.end()) {
return convertVariableToPolynomial(variablePair->second);
} else {
- storm::RationalFunctionVariable carlVariable = carl::freshRealVariable(expression.getVariableName());
+ storm::RationalFunctionVariable carlVariable = storm::createRFVariable(expression.getVariableName());
variableToVariableMap.emplace(expression.getVariable(), carlVariable);
return convertVariableToPolynomial(carlVariable);
}