Browse Source

pipe all rf-variable creations through a single object file

tempestpy_adaptions
Sebastian Junges 4 years ago
parent
commit
5722c1258c
  1. 2
      src/storm-pomdp/transformer/ApplyFiniteSchedulerToPomdp.cpp
  2. 7
      src/storm/adapters/RationalFunctionAdapter.cpp
  3. 2
      src/storm/adapters/RationalFunctionAdapter.h
  4. 2
      src/storm/builder/DdPrismModelBuilder.cpp
  5. 2
      src/storm/storage/expressions/ToRationalFunctionVisitor.cpp

2
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;

7
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);
}
}

2
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)

2
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);

2
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);
}

Loading…
Cancel
Save