Browse Source

constants in header

Former-commit-id: 281e490873
tempestpy_adaptions
sjunges 9 years ago
parent
commit
5faebdff86
  1. 2
      CMakeLists.txt
  2. 2
      src/builder/ExplicitDFTModelBuilder.cpp
  3. 520
      src/utility/constants.cpp
  4. 195
      src/utility/constants.h
  5. 2
      src/utility/storm.h
  6. 7
      src/utility/vector.h

2
CMakeLists.txt

@ -364,7 +364,7 @@ find_package(CLN QUIET)
set(STORM_USE_CLN_NUMBERS OFF) set(STORM_USE_CLN_NUMBERS OFF)
if(CLN_FOUND) if(CLN_FOUND)
set(STORM_HAVE_CLN ON) set(STORM_HAVE_CLN ON)
set(STORM_USE_CLN_NUMBERS ON)
set(STORM_USE_CLN_NUMBERS OFF)
message(STATUS "StoRM - Linking with CLN ${CLN_VERSION_STRING}") message(STATUS "StoRM - Linking with CLN ${CLN_VERSION_STRING}")
include_directories("${CLN_INCLUDE_DIR}") include_directories("${CLN_INCLUDE_DIR}")
list(APPEND STORM_LINK_LIBRARIES ${CLN_LIBRARIES}) list(APPEND STORM_LINK_LIBRARIES ${CLN_LIBRARIES})

2
src/builder/ExplicitDFTModelBuilder.cpp

@ -2,7 +2,7 @@
#include <src/models/sparse/MarkovAutomaton.h> #include <src/models/sparse/MarkovAutomaton.h>
#include <src/models/sparse/Ctmc.h> #include <src/models/sparse/Ctmc.h>
#include <src/utility/constants.h> #include <src/utility/constants.h>
#include <src/utility/vector.h>
#include "src/utility/vector.h"
#include <src/exceptions/UnexpectedException.h> #include <src/exceptions/UnexpectedException.h>
#include <map> #include <map>

520
src/utility/constants.cpp

@ -1,168 +1,168 @@
#include "src/utility/constants.h"
#include "src/storage/sparse/StateType.h"
//#include "src/utility/constants.h"
//
//#include "src/storage/sparse/StateType.h"
#include "src/storage/SparseMatrix.h" #include "src/storage/SparseMatrix.h"
#include "src/settings/SettingsManager.h"
#include "src/settings/modules/GeneralSettings.h"
#include "src/adapters/CarlAdapter.h"
//#include "src/settings/SettingsManager.h"
//#include "src/settings/modules/GeneralSettings.h"
//
//#include "src/adapters/CarlAdapter.h"
//
namespace storm { namespace storm {
namespace utility { namespace utility {
template<typename ValueType>
ValueType one() {
return ValueType(1);
}
template<typename ValueType>
ValueType zero() {
return ValueType(0);
}
template<typename ValueType>
ValueType infinity() {
return std::numeric_limits<ValueType>::infinity();
}
template<typename ValueType>
bool isOne(ValueType const& a) {
return a == one<ValueType>();
}
template<typename ValueType>
bool isZero(ValueType const& a) {
return a == zero<ValueType>();
}
template<typename ValueType>
bool isConstant(ValueType const& a) {
return true;
}
template<>
bool isOne(storm::RationalNumber const& a) {
return carl::isOne(a);
}
template<>
bool isZero(storm::RationalNumber const& a) {
return carl::isZero(a);
}
template<>
storm::RationalNumber infinity() {
// FIXME: this should be treated more properly.
return storm::RationalNumber(-1);
}
template<>
bool isOne(storm::RationalFunction const& a) {
return a.isOne();
}
template<>
bool isZero(storm::RationalFunction const& a) {
return a.isZero();
}
template<>
bool isConstant(storm::RationalFunction const& a) {
return a.isConstant();
}
template<>
bool isOne(storm::Polynomial const& a) {
return a.isOne();
}
template<>
bool isZero(storm::Polynomial const& a) {
return a.isZero();
}
template<>
bool isConstant(storm::Polynomial const& a) {
return a.isConstant();
}
template<>
storm::RationalFunction infinity() {
// FIXME: this should be treated more properly.
return storm::RationalFunction(-1.0);
}
template<typename ValueType>
ValueType pow(ValueType const& value, uint_fast64_t exponent) {
return std::pow(value, exponent);
}
template<typename ValueType>
ValueType simplify(ValueType value) {
// 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.
return value;
}
template<>
double convertNumber(double const& number){
return number;
}
template<typename ValueType>
ValueType abs(ValueType const& number) {
return std::fabs(number);
}
template<>
RationalFunction& simplify(RationalFunction& value);
template<>
RationalFunction&& simplify(RationalFunction&& value);
template<>
RationalFunction pow(RationalFunction const& value, uint_fast64_t exponent) {
return carl::pow(value, exponent);
}
template<>
RationalFunction simplify(RationalFunction value) {
value.simplify();
return value;
}
template<>
RationalFunction& simplify(RationalFunction& value) {
value.simplify();
return value;
}
template<>
RationalFunction&& simplify(RationalFunction&& value) {
value.simplify();
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);
}
template<>
RationalFunction convertNumber(double const& number){
return RationalFunction(carl::rationalize<RationalNumber>(number));
}
template<>
storm::RationalNumber abs(storm::RationalNumber const& number) {
return carl::abs(number);
}
// template<typename ValueType>
// ValueType one() {
// return ValueType(1);
// }
//
// template<typename ValueType>
// ValueType zero() {
// return ValueType(0);
// }
//
// template<typename ValueType>
// ValueType infinity() {
// return std::numeric_limits<ValueType>::infinity();
// }
//
// template<typename ValueType>
// bool isOne(ValueType const& a) {
// return a == one<ValueType>();
// }
//
// template<typename ValueType>
// bool isZero(ValueType const& a) {
// return a == zero<ValueType>();
// }
//
// template<typename ValueType>
// bool isConstant(ValueType const& a) {
// return true;
// }
//
// template<>
// bool isOne(storm::RationalNumber const& a) {
// return carl::isOne(a);
// }
//
// template<>
// bool isZero(storm::RationalNumber const& a) {
// return carl::isZero(a);
// }
//
// template<>
// storm::RationalNumber infinity() {
// // FIXME: this should be treated more properly.
// return storm::RationalNumber(-1);
// }
//
// template<>
// bool isOne(storm::RationalFunction const& a) {
// return a.isOne();
// }
//
// template<>
// bool isZero(storm::RationalFunction const& a) {
// return a.isZero();
// }
//
// template<>
// bool isConstant(storm::RationalFunction const& a) {
// return a.isConstant();
// }
//
// template<>
// bool isOne(storm::Polynomial const& a) {
// return a.isOne();
// }
//
// template<>
// bool isZero(storm::Polynomial const& a) {
// return a.isZero();
// }
//
// template<>
// bool isConstant(storm::Polynomial const& a) {
// return a.isConstant();
// }
//
// template<>
// storm::RationalFunction infinity() {
// // FIXME: this should be treated more properly.
// return storm::RationalFunction(-1.0);
// }
//
// template<typename ValueType>
// ValueType pow(ValueType const& value, uint_fast64_t exponent) {
// return std::pow(value, exponent);
// }
//
// template<typename ValueType>
// ValueType simplify(ValueType value) {
// // 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.
// return value;
// }
//
// template<>
// double convertNumber(double const& number){
// return number;
// }
//
// template<typename ValueType>
// ValueType abs(ValueType const& number) {
// return carl::abs(number);
// }
//
// template<>
// RationalFunction& simplify(RationalFunction& value);
//
// template<>
// RationalFunction&& simplify(RationalFunction&& value);
//
// template<>
// RationalFunction pow(RationalFunction const& value, uint_fast64_t exponent) {
// return carl::pow(value, exponent);
// }
//
// template<>
// RationalFunction simplify(RationalFunction value) {
// value.simplify();
// return value;
// }
//
// template<>
// RationalFunction& simplify(RationalFunction& value) {
// value.simplify();
// return value;
// }
//
// template<>
// RationalFunction&& simplify(RationalFunction&& value) {
// value.simplify();
// 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);
// }
//
// template<>
// RationalFunction convertNumber(double const& number){
// return RationalFunction(carl::rationalize<RationalNumber>(number));
// }
////
//// template<>
//// storm::RationalNumber abs(storm::RationalNumber const& number) {
//// return carl::abs(number);
//// }
//
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) {
simplify(matrixEntry.getValue()); simplify(matrixEntry.getValue());
@ -180,127 +180,127 @@ namespace storm {
simplify(matrixEntry.getValue()); simplify(matrixEntry.getValue());
return std::move(matrixEntry); return std::move(matrixEntry);
} }
// Explicit instantiations.
template bool isOne(double const& value);
template bool isZero(double const& value);
template bool isConstant(double const& value);
template double one();
template double zero();
template double infinity();
template double pow(double const& value, uint_fast64_t exponent);
template double simplify(double value);
//
// // Explicit instantiations.
// template bool isOne(double const& value);
// template bool isZero(double const& value);
// template bool isConstant(double const& value);
//
// template double one();
// template double zero();
// template double infinity();
//
// template double pow(double const& value, uint_fast64_t exponent);
//
// template double simplify(double value);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, double> simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, double> matrixEntry); template storm::storage::MatrixEntry<storm::storage::sparse::state_type, double> simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, double> matrixEntry);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, double>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, double>& matrixEntry); template storm::storage::MatrixEntry<storm::storage::sparse::state_type, double>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, double>& matrixEntry);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, double>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, double>&& matrixEntry); template storm::storage::MatrixEntry<storm::storage::sparse::state_type, double>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, double>&& matrixEntry);
template double abs(double const& number);
template bool isOne(float const& value);
template bool isZero(float const& value);
template bool isConstant(float const& value);
template float one();
template float zero();
template float infinity();
template float pow(float const& value, uint_fast64_t exponent);
template float simplify(float value);
//
// template double abs(double const& number);
//
// template bool isOne(float const& value);
// template bool isZero(float const& value);
// template bool isConstant(float const& value);
//
// template float one();
// template float zero();
// template float infinity();
//
// template float pow(float const& value, uint_fast64_t exponent);
//
// template float simplify(float value);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, float> simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, float> matrixEntry); template storm::storage::MatrixEntry<storm::storage::sparse::state_type, float> simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, float> matrixEntry);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, float>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, float>& matrixEntry); template storm::storage::MatrixEntry<storm::storage::sparse::state_type, float>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, float>& matrixEntry);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, float>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, float>&& matrixEntry); template storm::storage::MatrixEntry<storm::storage::sparse::state_type, float>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, float>&& matrixEntry);
template bool isOne(int const& value);
template bool isZero(int const& value);
template bool isConstant(int const& value);
template int one();
template int zero();
template int infinity();
template int pow(int const& value, uint_fast64_t exponent);
template int simplify(int value);
// template bool isOne(int const& value);
// template bool isZero(int const& value);
// template bool isConstant(int const& value);
//
// template int one();
// template int zero();
// template int infinity();
//
// template int pow(int const& value, uint_fast64_t exponent);
//
// template int simplify(int value);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, int> simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, int> matrixEntry); template storm::storage::MatrixEntry<storm::storage::sparse::state_type, int> simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, int> matrixEntry);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, int>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, int>& matrixEntry); template storm::storage::MatrixEntry<storm::storage::sparse::state_type, int>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, int>& matrixEntry);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, int>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, int>&& matrixEntry); template storm::storage::MatrixEntry<storm::storage::sparse::state_type, int>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, int>&& matrixEntry);
template bool isOne(storm::storage::sparse::state_type const& value);
template bool isZero(storm::storage::sparse::state_type const& value);
template bool isConstant(storm::storage::sparse::state_type const& value);
template uint32_t one();
template uint32_t zero();
template uint32_t infinity();
template storm::storage::sparse::state_type one();
template storm::storage::sparse::state_type zero();
template storm::storage::sparse::state_type infinity();
template storm::storage::sparse::state_type pow(storm::storage::sparse::state_type const& value, uint_fast64_t exponent);
template storm::storage::sparse::state_type simplify(storm::storage::sparse::state_type value);
// template bool isOne(storm::storage::sparse::state_type const& value);
// template bool isZero(storm::storage::sparse::state_type const& value);
// template bool isConstant(storm::storage::sparse::state_type const& value);
//
// template uint32_t one();
// template uint32_t zero();
// template uint32_t infinity();
//
// template storm::storage::sparse::state_type one();
// template storm::storage::sparse::state_type zero();
// template storm::storage::sparse::state_type infinity();
//
// template storm::storage::sparse::state_type pow(storm::storage::sparse::state_type const& value, uint_fast64_t exponent);
//
// template storm::storage::sparse::state_type simplify(storm::storage::sparse::state_type value);
//
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::storage::sparse::state_type> simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::storage::sparse::state_type> matrixEntry); template storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::storage::sparse::state_type> simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::storage::sparse::state_type> matrixEntry);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::storage::sparse::state_type>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::storage::sparse::state_type>& matrixEntry); template storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::storage::sparse::state_type>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::storage::sparse::state_type>& matrixEntry);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::storage::sparse::state_type>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::storage::sparse::state_type>&& matrixEntry); template storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::storage::sparse::state_type>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::storage::sparse::state_type>&& matrixEntry);
// Instantiations for rational number.
template bool isOne(storm::RationalNumber const& value);
template bool isZero(storm::RationalNumber const& value);
template bool isConstant(storm::RationalNumber const& value);
template storm::RationalNumber one();
template storm::RationalNumber zero();
template storm::RationalNumber infinity();
template double convertNumber(storm::RationalNumber const& number);
template storm::RationalNumber convertNumber(double const& number);
template storm::RationalNumber abs(storm::RationalNumber const& number);
// template storm::RationalNumber pow(storm::RationalNumber const& value, uint_fast64_t exponent);
template storm::RationalNumber simplify(storm::RationalNumber value);
//
// // Instantiations for rational number.
// template bool isOne(storm::RationalNumber const& value);
// template bool isZero(storm::RationalNumber const& value);
// template bool isConstant(storm::RationalNumber const& value);
//
// template storm::RationalNumber one();
// template storm::RationalNumber zero();
// template storm::RationalNumber infinity();
//
// template double convertNumber(storm::RationalNumber const& number);
// template storm::RationalNumber convertNumber(double const& number);
//
// template storm::RationalNumber abs(storm::RationalNumber const& number);
//
//// template storm::RationalNumber pow(storm::RationalNumber const& value, uint_fast64_t exponent);
//
// template storm::RationalNumber simplify(storm::RationalNumber value);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::RationalNumber> simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::RationalNumber> matrixEntry); template storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::RationalNumber> simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::RationalNumber> matrixEntry);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::RationalNumber>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::RationalNumber>& matrixEntry); template storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::RationalNumber>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::RationalNumber>& matrixEntry);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::RationalNumber>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::RationalNumber>&& matrixEntry); template storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::RationalNumber>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::RationalNumber>&& matrixEntry);
#ifdef STORM_HAVE_CARL #ifdef STORM_HAVE_CARL
template bool isOne(RationalFunction const& value);
template bool isZero(RationalFunction const& value);
template bool isConstant(RationalFunction const& value);
template RationalFunction one();
template RationalFunction zero();
template storm::RationalFunction infinity();
template RationalFunction pow(RationalFunction const& value, uint_fast64_t exponent);
template RationalFunction simplify(RationalFunction value);
template RationalFunction& simplify(RationalFunction& value);
template RationalFunction&& simplify(RationalFunction&& value);
template Polynomial one();
template Polynomial zero();
template bool isOne(Interval const& value);
template bool isZero(Interval const& value);
template bool isConstant(Interval const& value);
template Interval one();
template Interval zero();
// template bool isOne(RationalFunction const& value);
// template bool isZero(RationalFunction const& value);
// template bool isConstant(RationalFunction const& value);
//
// template RationalFunction one();
// template RationalFunction zero();
// template storm::RationalFunction infinity();
//
// template RationalFunction pow(RationalFunction const& value, uint_fast64_t exponent);
// template RationalFunction simplify(RationalFunction value);
// template RationalFunction& simplify(RationalFunction& value);
// template RationalFunction&& simplify(RationalFunction&& value);
//
// template Polynomial one();
// template Polynomial zero();
//
// template bool isOne(Interval const& value);
// template bool isZero(Interval const& value);
// template bool isConstant(Interval const& value);
//
// template Interval one();
// template Interval zero();
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction> simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction> matrixEntry); template storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction> simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction> matrixEntry);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction>& matrixEntry); template storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction>& matrixEntry);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction>&& matrixEntry); template storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction>&& matrixEntry);
#endif #endif
//
} }
} }

195
src/utility/constants.h

@ -11,6 +11,11 @@
#include <limits> #include <limits>
#include <cstdint> #include <cstdint>
#include "src/storage/sparse/StateType.h"
#include "src/settings/SettingsManager.h"
#include "src/settings/modules/GeneralSettings.h"
#include "src/adapters/CarlAdapter.h"
namespace storm { namespace storm {
@ -20,42 +25,182 @@ namespace storm {
} }
namespace utility { namespace utility {
template<typename ValueType> template<typename ValueType>
ValueType one();
ValueType one() {
return ValueType(1);
}
template<typename ValueType> template<typename ValueType>
ValueType zero();
ValueType zero() {
return ValueType(0);
}
template<typename ValueType> template<typename ValueType>
ValueType infinity();
ValueType infinity() {
return std::numeric_limits<ValueType>::infinity();
}
template<typename ValueType> template<typename ValueType>
bool isOne(ValueType const& a);
bool isOne(ValueType const& a) {
return a == one<ValueType>();
}
template<typename ValueType> template<typename ValueType>
bool isZero(ValueType const& a);
bool isZero(ValueType const& a) {
return a == zero<ValueType>();
}
template<typename ValueType> template<typename ValueType>
bool isConstant(ValueType const& a);
bool isConstant(ValueType const& a) {
return true;
}
template<>
bool isOne(storm::RationalNumber const& a) {
return carl::isOne(a);
}
template<>
bool isZero(storm::RationalNumber const& a) {
return carl::isZero(a);
}
template<>
storm::RationalNumber infinity() {
// FIXME: this should be treated more properly.
return storm::RationalNumber(-1);
}
template<>
bool isOne(storm::RationalFunction const& a) {
return a.isOne();
}
template<>
bool isZero(storm::RationalFunction const& a) {
return a.isZero();
}
template<>
bool isConstant(storm::RationalFunction const& a) {
return a.isConstant();
}
template<>
bool isOne(storm::Polynomial const& a) {
return a.isOne();
}
template<>
bool isZero(storm::Polynomial const& a) {
return a.isZero();
}
template<>
bool isConstant(storm::Polynomial const& a) {
return a.isConstant();
}
template<>
storm::RationalFunction infinity() {
// FIXME: this should be treated more properly.
return storm::RationalFunction(-1.0);
}
template<typename ValueType> template<typename ValueType>
ValueType pow(ValueType const& value, uint_fast64_t exponent);
ValueType pow(ValueType const& value, uint_fast64_t exponent) {
return std::pow(value, exponent);
}
template<typename ValueType> template<typename ValueType>
ValueType simplify(ValueType value);
template<typename IndexType, typename ValueType>
storm::storage::MatrixEntry<IndexType, ValueType>& simplify(storm::storage::MatrixEntry<IndexType, ValueType>& matrixEntry);
ValueType simplify(ValueType value) {
// 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.
return value;
}
template<typename IndexType, typename ValueType>
storm::storage::MatrixEntry<IndexType, ValueType>&& simplify(storm::storage::MatrixEntry<IndexType, ValueType>&& matrixEntry);
template<typename TargetType, typename SourceType>
template<typename SourceType, typename TargetType>
TargetType convertNumber(SourceType const& number); TargetType convertNumber(SourceType const& number);
template<>
double convertNumber(double const& number){
return number;
}
template<typename ValueType> template<typename ValueType>
ValueType abs(ValueType const& number);
ValueType abs(ValueType const& number) {
return carl::abs(number);
}
template<>
RationalFunction& simplify(RationalFunction& value);
template<>
RationalFunction&& simplify(RationalFunction&& value);
template<>
RationalFunction pow(RationalFunction const& value, uint_fast64_t exponent) {
return carl::pow(value, exponent);
}
template<>
RationalFunction simplify(RationalFunction value) {
value.simplify();
return value;
}
template<>
RationalFunction& simplify(RationalFunction& value) {
value.simplify();
return value;
}
template<>
RationalFunction&& simplify(RationalFunction&& value) {
value.simplify();
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);
}
template<>
RationalFunction convertNumber(double const& number){
return RationalFunction(carl::rationalize<RationalNumber>(number));
}
//
// template<>
// storm::RationalNumber abs(storm::RationalNumber const& number) {
// return carl::abs(number);
// }
template<typename IndexType, typename ValueType>
storm::storage::MatrixEntry<IndexType, ValueType> simplify(storm::storage::MatrixEntry<IndexType, ValueType> matrixEntry) {
simplify(matrixEntry.getValue());
return matrixEntry;
}
template<typename IndexType, typename ValueType>
storm::storage::MatrixEntry<IndexType, ValueType>& simplify(storm::storage::MatrixEntry<IndexType, ValueType>& matrixEntry) {
simplify(matrixEntry.getValue());
return matrixEntry;
}
template<typename IndexType, typename ValueType>
storm::storage::MatrixEntry<IndexType, ValueType>&& simplify(storm::storage::MatrixEntry<IndexType, ValueType>&& matrixEntry) {
simplify(matrixEntry.getValue());
return std::move(matrixEntry);
}
} }
} }

2
src/utility/storm.h

@ -243,7 +243,7 @@ namespace storm {
case storm::settings::modules::CoreSettings::Engine::Sparse: { case storm::settings::modules::CoreSettings::Engine::Sparse: {
std::shared_ptr<storm::models::sparse::Model<ValueType>> sparseModel = model->template as<storm::models::sparse::Model<ValueType>>(); std::shared_ptr<storm::models::sparse::Model<ValueType>> sparseModel = model->template as<storm::models::sparse::Model<ValueType>>();
STORM_LOG_THROW(sparseModel != nullptr, storm::exceptions::InvalidArgumentException, "Sparse engine requires a sparse input model"); STORM_LOG_THROW(sparseModel != nullptr, storm::exceptions::InvalidArgumentException, "Sparse engine requires a sparse input model");
return verifySparseModel(sparseModel, formula, onlyInitialStatesRelevant);
return (sparseModel, formula, onlyInitialStatesRelevant);
} }
case storm::settings::modules::CoreSettings::Engine::Hybrid: { case storm::settings::modules::CoreSettings::Engine::Hybrid: {
std::shared_ptr<storm::models::symbolic::Model<DdType>> ddModel = model->template as<storm::models::symbolic::Model<DdType>>(); std::shared_ptr<storm::models::symbolic::Model<DdType>> ddModel = model->template as<storm::models::symbolic::Model<DdType>>();

7
src/utility/vector.h

@ -12,7 +12,6 @@
#include <functional> #include <functional>
#include "src/storage/BitVector.h" #include "src/storage/BitVector.h"
#include "src/utility/constants.h"
#include "src/utility/macros.h" #include "src/utility/macros.h"
#include "src/solver/OptimizationDirection.h" #include "src/solver/OptimizationDirection.h"
@ -588,7 +587,7 @@ namespace storm {
* @return True iff the elements are considered equal. * @return True iff the elements are considered equal.
*/ */
template<class T> template<class T>
bool equalModuloPrecision(T const& val1, T const& val2, T precision, bool relativeError = true) {
bool equalModuloPrecision(T const& val1, T const& val2, T const& precision, bool relativeError = true) {
if (relativeError) { if (relativeError) {
if (val2 == 0) { if (val2 == 0) {
return (storm::utility::abs(val1) <= precision); return (storm::utility::abs(val1) <= precision);
@ -612,7 +611,7 @@ namespace storm {
* @param relativeError If set, the difference between the vectors is computed relative to the value or in absolute terms. * @param relativeError If set, the difference between the vectors is computed relative to the value or in absolute terms.
*/ */
template<class T> template<class T>
bool equalModuloPrecision(std::vector<T> const& vectorLeft, std::vector<T> const& vectorRight, T precision, bool relativeError) {
bool equalModuloPrecision(std::vector<T> const& vectorLeft, std::vector<T> const& vectorRight, T const& precision, bool relativeError) {
STORM_LOG_ASSERT(vectorLeft.size() == vectorRight.size(), "Lengths of vectors does not match."); STORM_LOG_ASSERT(vectorLeft.size() == vectorRight.size(), "Lengths of vectors does not match.");
for (uint_fast64_t i = 0; i < vectorLeft.size(); ++i) { for (uint_fast64_t i = 0; i < vectorLeft.size(); ++i) {
@ -636,7 +635,7 @@ namespace storm {
* @param relativeError If set, the difference between the vectors is computed relative to the value or in absolute terms. * @param relativeError If set, the difference between the vectors is computed relative to the value or in absolute terms.
*/ */
template<class T> template<class T>
bool equalModuloPrecision(std::vector<T> const& vectorLeft, std::vector<T> const& vectorRight, std::vector<uint_fast64_t> const& positions, T precision, bool relativeError) {
bool equalModuloPrecision(std::vector<T> const& vectorLeft, std::vector<T> const& vectorRight, std::vector<uint_fast64_t> const& positions, T const& precision, bool relativeError) {
STORM_LOG_ASSERT(vectorLeft.size() == vectorRight.size(), "Lengths of vectors does not match."); STORM_LOG_ASSERT(vectorLeft.size() == vectorRight.size(), "Lengths of vectors does not match.");
for (uint_fast64_t position : positions) { for (uint_fast64_t position : positions) {

Loading…
Cancel
Save