sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Use typedefs of RationalFunctionAdapter

tempestpy_adaptions
Matthias Volk 5 years ago
parent
30565e4d0c
commit
fba3223f63
6 changed files with 24 additions and 24 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 12
      src/storm/builder/DdJaniModelBuilder.cpp
  2. 12
      src/storm/builder/DdPrismModelBuilder.cpp
  3. 10
      src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp
  4. 2
      src/storm/builder/jit/ExplicitJitJaniModelBuilder.h
  5. 4
      src/storm/storage/expressions/ToRationalFunctionVisitor.cpp
  6. 8
      src/storm/storage/expressions/ToRationalFunctionVisitor.h

12
src/storm/builder/DdJaniModelBuilder.cpp
View File

@ -156,14 +156,14 @@ namespace storm {
template <storm::dd::DdType Type>
class ParameterCreator<Type, storm::RationalFunction> {
public:
ParameterCreator() : cache(std::make_shared<carl::Cache<carl::PolynomialFactorizationPair<RawPolynomial>>>()) {
ParameterCreator() : cache(std::make_shared<storm::RawPolynomialCache>()) {
// Intentionally left empty.
}
void create(storm::jani::Model const& model, storm::adapters::AddExpressionAdapter<Type, storm::RationalFunction>& rowExpressionAdapter) {
for (auto const& constant : model.getConstants()) {
if (!constant.isDefined()) {
carl::Variable carlVariable = carl::freshRealVariable(constant.getExpressionVariable().getName());
storm::RationalFunctionVariable carlVariable = carl::freshRealVariable(constant.getExpressionVariable().getName());
parameters.insert(carlVariable);
auto rf = convertVariableToPolynomial(carlVariable);
rowExpressionAdapter.setValue(constant.getExpressionVariable(), rf);
@ -172,12 +172,12 @@ namespace storm {
}
template<typename RationalFunctionType = storm::RationalFunction, typename TP = typename RationalFunctionType::PolyType, carl::EnableIf<carl::needs_cache<TP>> = carl::dummy>
RationalFunctionType convertVariableToPolynomial(carl::Variable const& variable) {
RationalFunctionType convertVariableToPolynomial(storm::RationalFunctionVariable const& variable) {
return RationalFunctionType(typename RationalFunctionType::PolyType(typename RationalFunctionType::PolyType::PolyType(variable), cache));
}
template<typename RationalFunctionType = storm::RationalFunction, typename TP = typename RationalFunctionType::PolyType, carl::DisableIf<carl::needs_cache<TP>> = carl::dummy>
RationalFunctionType convertVariableToPolynomial(carl::Variable const& variable) {
RationalFunctionType convertVariableToPolynomial(storm::RationalFunctionVariable const& variable) {
return RationalFunctionType(variable);
}
@ -187,10 +187,10 @@ namespace storm {
private:
// A mapping from our variables to carl's.
std::unordered_map<storm::expressions::Variable, carl::Variable> variableToVariableMap;
std::unordered_map<storm::expressions::Variable, storm::RationalFunctionVariable> variableToVariableMap;
// The cache that is used in case the underlying type needs a cache.
std::shared_ptr<carl::Cache<carl::PolynomialFactorizationPair<RawPolynomial>>> cache;
std::shared_ptr<storm::RawPolynomialCache> cache;
// All created parameters.
std::set<storm::RationalFunctionVariable> parameters;

12
src/storm/builder/DdPrismModelBuilder.cpp
View File

@ -49,14 +49,14 @@ namespace storm {
template <storm::dd::DdType Type>
class ParameterCreator<Type, storm::RationalFunction> {
public:
ParameterCreator() : cache(std::make_shared<carl::Cache<carl::PolynomialFactorizationPair<RawPolynomial>>>()) {
ParameterCreator() : cache(std::make_shared<storm::RawPolynomialCache>()) {
// Intentionally left empty.
}
void create(storm::prism::Program const& program, storm::adapters::AddExpressionAdapter<Type, storm::RationalFunction>& rowExpressionAdapter) {
for (auto const& constant : program.getConstants()) {
if (!constant.isDefined()) {
carl::Variable carlVariable = carl::freshRealVariable(constant.getExpressionVariable().getName());
storm::RationalFunctionVariable carlVariable = carl::freshRealVariable(constant.getExpressionVariable().getName());
parameters.insert(carlVariable);
auto rf = convertVariableToPolynomial(carlVariable);
rowExpressionAdapter.setValue(constant.getExpressionVariable(), rf);
@ -65,12 +65,12 @@ namespace storm {
}
template<typename RationalFunctionType = storm::RationalFunction, typename TP = typename RationalFunctionType::PolyType, carl::EnableIf<carl::needs_cache<TP>> = carl::dummy>
RationalFunctionType convertVariableToPolynomial(carl::Variable const& variable) {
RationalFunctionType convertVariableToPolynomial(storm::RationalFunctionVariable const& variable) {
return RationalFunctionType(typename RationalFunctionType::PolyType(typename RationalFunctionType::PolyType::PolyType(variable), cache));
}
template<typename RationalFunctionType = storm::RationalFunction, typename TP = typename RationalFunctionType::PolyType, carl::DisableIf<carl::needs_cache<TP>> = carl::dummy>
RationalFunctionType convertVariableToPolynomial(carl::Variable const& variable) {
RationalFunctionType convertVariableToPolynomial(storm::RationalFunctionVariable const& variable) {
return RationalFunctionType(variable);
}
@ -80,10 +80,10 @@ namespace storm {
private:
// A mapping from our variables to carl's.
std::unordered_map<storm::expressions::Variable, carl::Variable> variableToVariableMap;
std::unordered_map<storm::expressions::Variable, storm::RationalFunctionVariable> variableToVariableMap;
// The cache that is used in case the underlying type needs a cache.
std::shared_ptr<carl::Cache<carl::PolynomialFactorizationPair<RawPolynomial>>> cache;
std::shared_ptr<storm::RawPolynomialCache> cache;
// All created parameters.
std::set<storm::RationalFunctionVariable> parameters;

10
src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp
View File

@ -2522,22 +2522,22 @@ namespace storm {
}
template<typename RationalFunctionType, typename TP = typename RationalFunctionType::PolyType, carl::EnableIf<carl::needs_cache<TP>> = carl::dummy>
RationalFunctionType convertVariableToPolynomial(carl::Variable const& variable, std::shared_ptr<carl::Cache<carl::PolynomialFactorizationPair<RawPolynomial>>> cache) {
RationalFunctionType convertVariableToPolynomial(storm::RationalFunctionVariable const& variable, std::shared_ptr<storm::RawPolynomialCache> cache) {
return RationalFunctionType(typename RationalFunctionType::PolyType(typename RationalFunctionType::PolyType::PolyType(variable), cache));
}
template<typename RationalFunctionType, typename TP = typename RationalFunctionType::PolyType, carl::DisableIf<carl::needs_cache<TP>> = carl::dummy>
RationalFunctionType convertVariableToPolynomial(carl::Variable const& variable, std::shared_ptr<carl::Cache<carl::PolynomialFactorizationPair<RawPolynomial>>>) {
RationalFunctionType convertVariableToPolynomial(storm::RationalFunctionVariable const& variable, std::shared_ptr<storm::RawPolynomialCache>) {
return RationalFunctionType(variable);
}
template<typename ValueType>
std::vector<storm::RationalFunction> getParameters(storm::jani::Model const&, std::shared_ptr<carl::Cache<carl::PolynomialFactorizationPair<RawPolynomial>>>) {
std::vector<storm::RationalFunction> getParameters(storm::jani::Model const&, std::shared_ptr<storm::RawPolynomialCache>) {
STORM_LOG_THROW(false, storm::exceptions::InvalidStateException, "This function must not be called for this type.");
}
template<>
std::vector<storm::RationalFunction> getParameters<storm::RationalFunction>(storm::jani::Model const& model, std::shared_ptr<carl::Cache<carl::PolynomialFactorizationPair<RawPolynomial>>> cache) {
std::vector<storm::RationalFunction> getParameters<storm::RationalFunction>(storm::jani::Model const& model, std::shared_ptr<storm::RawPolynomialCache> cache) {
std::vector<storm::RationalFunction> parameters;
for (auto const& constant : model.getConstants()) {
if (!constant.isDefined() && constant.isRealConstant()) {
@ -2557,7 +2557,7 @@ namespace storm {
typedef boost::function<InitializeParametersFunctionType> ImportInitializeParametersFunctionType;
// Create the carl cache if we are building a parametric model.
cache = std::make_shared<carl::Cache<carl::PolynomialFactorizationPair<RawPolynomial>>>();
cache = std::make_shared<storm::RawPolynomialCache>();
ImportInitializeParametersFunctionType initializeParametersFunction = boost::dll::import_alias<InitializeParametersFunctionType>(dynamicLibraryPath, "initialize_parameters");
std::vector<storm::RationalFunction> parameters = getParameters<ValueType>(this->model, cache);

2
src/storm/builder/jit/ExplicitJitJaniModelBuilder.h
View File

@ -202,7 +202,7 @@ namespace storm {
std::string gmpIncludeDirectory;
/// A cache that is used by carl.
std::shared_ptr<carl::Cache<carl::PolynomialFactorizationPair<RawPolynomial>>> cache;
std::shared_ptr<storm::RawPolynomialCache> cache;
};
}

4
src/storm/storage/expressions/ToRationalFunctionVisitor.cpp
View File

@ -11,7 +11,7 @@ namespace storm {
#ifdef STORM_HAVE_CARL
template<typename RationalFunctionType>
ToRationalFunctionVisitor<RationalFunctionType>::ToRationalFunctionVisitor(ExpressionEvaluatorBase<RationalFunctionType> const& evaluator) : ExpressionVisitor(), cache(new carl::Cache<carl::PolynomialFactorizationPair<RawPolynomial>>()), evaluator(evaluator) {
ToRationalFunctionVisitor<RationalFunctionType>::ToRationalFunctionVisitor(ExpressionEvaluatorBase<RationalFunctionType> const& evaluator) : ExpressionVisitor(), cache(new storm::RawPolynomialCache()), evaluator(evaluator) {
// Intentionally left empty.
}
@ -82,7 +82,7 @@ namespace storm {
if (variablePair != variableToVariableMap.end()) {
return convertVariableToPolynomial(variablePair->second);
} else {
carl::Variable carlVariable = carl::freshRealVariable(expression.getVariableName());
storm::RationalFunctionVariable carlVariable = carl::freshRealVariable(expression.getVariableName());
variableToVariableMap.emplace(expression.getVariable(), carlVariable);
return convertVariableToPolynomial(carlVariable);
}

8
src/storm/storage/expressions/ToRationalFunctionVisitor.h
View File

@ -37,20 +37,20 @@ namespace storm {
private:
template<typename TP = typename RationalFunctionType::PolyType, carl::EnableIf<carl::needs_cache<TP>> = carl::dummy>
RationalFunctionType convertVariableToPolynomial(carl::Variable const& variable) {
RationalFunctionType convertVariableToPolynomial(storm::RationalFunctionVariable const& variable) {
return RationalFunctionType(typename RationalFunctionType::PolyType(typename RationalFunctionType::PolyType::PolyType(variable), cache));
}
template<typename TP = typename RationalFunctionType::PolyType, carl::DisableIf<carl::needs_cache<TP>> = carl::dummy>
RationalFunctionType convertVariableToPolynomial(carl::Variable const& variable) {
RationalFunctionType convertVariableToPolynomial(storm::RationalFunctionVariable const& variable) {
return RationalFunctionType(variable);
}
// A mapping from our variables to carl's.
std::unordered_map<storm::expressions::Variable, carl::Variable> variableToVariableMap;
std::unordered_map<storm::expressions::Variable, storm::RationalFunctionVariable> variableToVariableMap;
// The cache that is used in case the underlying type needs a cache.
std::shared_ptr<carl::Cache<carl::PolynomialFactorizationPair<RawPolynomial>>> cache;
std::shared_ptr<storm::RawPolynomialCache> cache;
// A mapping from variables to their values.
std::unordered_map<storm::expressions::Variable, RationalFunctionType> valueMapping;

Write Preview
Loading…
Cancel
Save