From 68ec4ca0ce46a8cd9d4018412f57d2725bfcbea7 Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Wed, 29 Nov 2017 20:11:15 +0100
Subject: [PATCH] Various fixes for the case STORM_USE_CLN_EA=ON
---
.../solver/IterativeMinMaxLinearEquationSolver.cpp | 2 +-
src/storm/storage/dd/cudd/CuddAddIterator.cpp | 2 +-
src/storm/storage/dd/cudd/InternalCuddAdd.cpp | 12 ++++++------
src/storm/utility/KwekMehlhorn.cpp | 4 ++--
src/storm/utility/constants.cpp | 14 ++++++++++++++
5 files changed, 24 insertions(+), 10 deletions(-)
diff --git a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp
index 371dfab34..fb71fa43f 100644
--- a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp
+++ b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp
@@ -829,7 +829,7 @@ namespace storm {
TemporaryHelper<RationalType, ImpreciseType>::swapSolutions(rationalX, temporaryRational, x, currentX, newX);
} else {
// Increase the precision.
- precision /= 10;
+ precision /= storm::utility::convertNumber<ValueType>(static_cast<uint64_t>(10));
}
}
diff --git a/src/storm/storage/dd/cudd/CuddAddIterator.cpp b/src/storm/storage/dd/cudd/CuddAddIterator.cpp
index 19e148390..d817a79d3 100644
--- a/src/storm/storage/dd/cudd/CuddAddIterator.cpp
+++ b/src/storm/storage/dd/cudd/CuddAddIterator.cpp
@@ -183,7 +183,7 @@ namespace storm {
template<typename ValueType>
std::pair<storm::expressions::SimpleValuation, ValueType> AddIterator<DdType::CUDD, ValueType>::operator*() const {
- return std::make_pair(currentValuation, static_cast<ValueType>(valueAsDouble));
+ return std::make_pair(currentValuation, storm::utility::convertNumber<ValueType>(valueAsDouble));
}
template class AddIterator<DdType::CUDD, double>;
diff --git a/src/storm/storage/dd/cudd/InternalCuddAdd.cpp b/src/storm/storage/dd/cudd/InternalCuddAdd.cpp
index 325f0ad9a..83ace48ae 100644
--- a/src/storm/storage/dd/cudd/InternalCuddAdd.cpp
+++ b/src/storm/storage/dd/cudd/InternalCuddAdd.cpp
@@ -325,18 +325,18 @@ namespace storm {
template<typename ValueType>
ValueType InternalAdd<DdType::CUDD, ValueType>::getMin() const {
cudd::ADD constantMinAdd = this->getCuddAdd().FindMin();
- return static_cast<double>(Cudd_V(constantMinAdd.getNode()));
+ return storm::utility::convertNumber<ValueType>(Cudd_V(constantMinAdd.getNode()));
}
template<typename ValueType>
ValueType InternalAdd<DdType::CUDD, ValueType>::getMax() const {
cudd::ADD constantMaxAdd = this->getCuddAdd().FindMax();
- return static_cast<double>(Cudd_V(constantMaxAdd.getNode()));
+ return storm::utility::convertNumber<ValueType>(Cudd_V(constantMaxAdd.getNode()));
}
template<typename ValueType>
ValueType InternalAdd<DdType::CUDD, ValueType>::getValue() const {
- return static_cast<ValueType>(Cudd_V(this->getCuddAdd().getNode()));
+ return storm::utility::convertNumber<ValueType>(Cudd_V(this->getCuddAdd().getNode()));
}
template<typename ValueType>
@@ -403,7 +403,7 @@ namespace storm {
int* cube;
double value;
DdGen* generator = this->getCuddAdd().FirstCube(&cube, &value);
- return AddIterator<DdType::CUDD, ValueType>(fullDdManager, generator, cube, value, (Cudd_IsGenEmpty(generator) != 0), &metaVariables, enumerateDontCareMetaVariables);
+ return AddIterator<DdType::CUDD, ValueType>(fullDdManager, generator, cube, storm::utility::convertNumber<ValueType>(value), (Cudd_IsGenEmpty(generator) != 0), &metaVariables, enumerateDontCareMetaVariables);
}
template<typename ValueType>
@@ -504,7 +504,7 @@ namespace storm {
// If we are at the maximal level, the value to be set is stored as a constant in the DD.
if (currentLevel == maxLevel) {
ValueType& targetValue = targetVector[offsets != nullptr ? (*offsets)[currentOffset] : currentOffset];
- targetValue = function(targetValue, Cudd_V(dd));
+ targetValue = function(targetValue, storm::utility::convertNumber<ValueType>(Cudd_V(dd)));
} else if (ddVariableIndices[currentLevel] < Cudd_NodeReadIndex(dd)) {
// If we skipped a level, we need to enumerate the explicit entries for the case in which the bit is set
// and for the one in which it is not set.
@@ -590,7 +590,7 @@ namespace storm {
// If we are at the maximal level, the value to be set is stored as a constant in the DD.
if (currentRowLevel + currentColumnLevel == maxLevel) {
if (generateValues) {
- columnsAndValues[rowIndications[rowGroupOffsets[currentRowOffset]]] = storm::storage::MatrixEntry<uint_fast64_t, ValueType>(currentColumnOffset, Cudd_V(dd));
+ columnsAndValues[rowIndications[rowGroupOffsets[currentRowOffset]]] = storm::storage::MatrixEntry<uint_fast64_t, ValueType>(currentColumnOffset, storm::utility::convertNumber<ValueType>(Cudd_V(dd)));
}
++rowIndications[rowGroupOffsets[currentRowOffset]];
} else {
diff --git a/src/storm/utility/KwekMehlhorn.cpp b/src/storm/utility/KwekMehlhorn.cpp
index ec81a3357..070115c72 100644
--- a/src/storm/utility/KwekMehlhorn.cpp
+++ b/src/storm/utility/KwekMehlhorn.cpp
@@ -43,8 +43,8 @@ namespace storm {
}
double powerOfTen = std::pow(10, precision);
- double truncated = storm::utility::trunc<double>(value * powerOfTen);
- return std::make_pair(truncated, powerOfTen);
+ auto truncated = storm::utility::trunc<double>(value * powerOfTen);
+ return std::make_pair(storm::utility::convertNumber<typename NumberTraits<RationalType>::IntegerType>(truncated), storm::utility::convertNumber<typename NumberTraits<RationalType>::IntegerType>(powerOfTen));
}
template<typename RationalType, typename ImpreciseType>
diff --git a/src/storm/utility/constants.cpp b/src/storm/utility/constants.cpp
index 278852f90..cd6556fed 100644
--- a/src/storm/utility/constants.cpp
+++ b/src/storm/utility/constants.cpp
@@ -335,6 +335,15 @@ namespace storm {
return NumberTraits<ClnRationalNumber>::IntegerType(static_cast<unsigned long int>(number));
}
+ template<>
+ typename NumberTraits<ClnRationalNumber>::IntegerType convertNumber(double const& number){
+ if (number < static_cast<double>(std::numeric_limits<uint64_t>::max())) {
+ return NumberTraits<ClnRationalNumber>::IntegerType(static_cast<uint64_t>(number));
+ } else {
+ return carl::round(carl::rationalize<ClnRationalNumber>(number));
+ }
+ }
+
template<>
ClnRationalNumber convertNumber(int_fast64_t const& number) {
STORM_LOG_ASSERT(static_cast<carl::sint>(number) == number, "Rationalizing failed, because the number is too large.");
@@ -518,6 +527,11 @@ namespace storm {
return NumberTraits<GmpRationalNumber>::IntegerType(static_cast<unsigned long int>(number));
}
+ template<>
+ typename NumberTraits<GmpRationalNumber>::IntegerType convertNumber(double const& number){
+ return NumberTraits<GmpRationalNumber>::IntegerType(number);
+ }
+
template<>
GmpRationalNumber convertNumber(int_fast64_t const& number){
STORM_LOG_ASSERT(static_cast<carl::sint>(number) == number, "Rationalizing failed, because the number is too large.");