Browse Source

Helper functions for parametric stuff

Former-commit-id: 288e4de3da
tempestpy_adaptions
TimQu 9 years ago
parent
commit
69c5ba604e
  1. 19
      src/utility/constants.cpp
  2. 3
      src/utility/constants.h
  3. 39
      src/utility/parametric.cpp
  4. 54
      src/utility/parametric.h

19
src/utility/constants.cpp

@ -39,6 +39,7 @@ namespace storm {
bool isConstant(ValueType const& a) { bool isConstant(ValueType const& a) {
return true; return true;
} }
#ifdef STORM_HAVE_CARL #ifdef STORM_HAVE_CARL
template<> template<>
@ -85,11 +86,11 @@ namespace storm {
template<typename ValueType> template<typename ValueType>
ValueType simplify(ValueType value) { ValueType simplify(ValueType value) {
// In the general case, we don't to anything here, but merely return the value. If something else is
// In the general case, we don't do anything here, but merely return the value. If something else is
// supposed to happen here, the templated function can be specialized for this particular type. // supposed to happen here, the templated function can be specialized for this particular type.
return value; return value;
} }
#ifdef STORM_HAVE_CARL #ifdef STORM_HAVE_CARL
template<> template<>
RationalFunction& simplify(RationalFunction& value); RationalFunction& simplify(RationalFunction& value);
@ -119,6 +120,17 @@ namespace storm {
value.simplify(); value.simplify();
return std::move(value); return std::move(value);
} }
template<>
double convertNumber(RationalNumber const& number){
return carl::toDouble(number);
}
template<>
RationalNumber convertNumber(double const& number){
return carl::rationalize<RationalNumber>(number);
}
#endif #endif
template<typename IndexType, typename ValueType> template<typename IndexType, typename ValueType>
@ -221,6 +233,9 @@ namespace storm {
template RationalFunction& simplify(RationalFunction& value); template RationalFunction& simplify(RationalFunction& value);
template RationalFunction&& simplify(RationalFunction&& value); template RationalFunction&& simplify(RationalFunction&& value);
template double convertNumber(RationalNumber const& number);
template RationalNumber convertNumber(double const& number);
template bool isOne(Interval const& value); template bool isOne(Interval const& value);
template bool isZero(Interval const& value); template bool isZero(Interval const& value);
template bool isConstant(Interval const& value); template bool isConstant(Interval const& value);

3
src/utility/constants.h

@ -50,6 +50,9 @@ namespace storm {
template<typename IndexType, typename ValueType> template<typename IndexType, typename ValueType>
storm::storage::MatrixEntry<IndexType, ValueType>&& simplify(storm::storage::MatrixEntry<IndexType, ValueType>&& matrixEntry); storm::storage::MatrixEntry<IndexType, ValueType>&& simplify(storm::storage::MatrixEntry<IndexType, ValueType>&& matrixEntry);
template<typename TargetType, typename SourceType>
TargetType convertNumber(SourceType const& number);
} }
} }

39
src/utility/parametric.cpp

@ -0,0 +1,39 @@
/*
* File: parametric.cpp
* Author: Tim Quatmann
*
* Created by Tim Quatmann on 08/03/16.
*/
#include <string>
#include "src/utility/parametric.h"
#include "src/utility/constants.h"
#include "src/utility/macros.h"
#include "src/settings/SettingsManager.h"
#include "src/exceptions/IllegalArgumentException.h"
#include "src/exceptions/NotImplementedException.h"
#ifdef STORM_HAVE_CARL
#include<carl/numbers/numbers.h>
#include<carl/core/VariablePool.h>
#endif
namespace storm {
namespace utility{
namespace parametric {
#ifdef STORM_HAVE_CARL
template<>
typename CoefficientType<storm::RationalFunction>::type evaluate<storm::RationalFunction>(storm::RationalFunction const& function, std::map<typename VariableType<storm::RationalFunction>::type, typename CoefficientType<storm::RationalFunction>::type> const& valuation){
return function.evaluate(valuation);
}
template<>
typename CoefficientType<storm::RationalFunction>::type getConstantPart<storm::RationalFunction>(storm::RationalFunction const& function){
return function.constantPart();
}
#endif
}
}
}

54
src/utility/parametric.h

@ -0,0 +1,54 @@
//
// parametric.h
//
// Created by Tim Quatmann on 08/03/16.
//
//
#ifndef STORM_UTILITY_PARAMETRIC_H
#define STORM_UTILITY_PARAMETRIC_H
#include "src/adapters/CarlAdapter.h"
namespace storm {
namespace utility {
namespace parametric {
/*!
* Access the type of variables from a given function type
*/
template<typename FunctionType>
struct VariableType { typedef void type; };
/*!
* Acess the type of coefficients from a given function type
*/
template<typename FunctionType>
struct CoefficientType { typedef void type; };
#ifdef STORM_HAVE_CARL
template<>
struct VariableType<storm::RationalFunction> { typedef storm::Variable type; };
template<>
struct CoefficientType<storm::RationalFunction> { typedef storm::RationalNumber type; };
#endif
/*!
* Evaluates the given function wrt. the given valuation
*/
template<typename FunctionType>
typename CoefficientType<FunctionType>::type evaluate(FunctionType const& function, std::map<typename VariableType<FunctionType>::type, typename CoefficientType<FunctionType>::type> const& valuation);
/*!
* Retrieves the constant part of the given function.
*/
template<typename FunctionType>
typename CoefficientType<FunctionType>::type getConstantPart(FunctionType const& function);
}
}
}
#endif /* STORM_UTILITY_PARAMETRIC_H */
Loading…
Cancel
Save