Merge branch 'master' into refactor_pla

src/storm/adapters/NumberAdapter.h

@@ -16,7 +16,7 @@
 
 #include <carl/numbers/numbers.h>
 
-#if defined(STORM_HAVE_CLN) && (defined(STORM_USE_CLN_EA) || defined(STORM_USE_CLN_RF))
+#if defined(STORM_HAVE_CLN)
 namespace cln {
     inline size_t hash_value(cl_RA const& n) {
         std::hash<cln::cl_RA> h;
@@ -25,7 +25,7 @@ namespace cln {
 }
 #endif
 
-#if defined(STORM_HAVE_GMP) && (!defined(STORM_USE_CLN_EA) || !defined(STORM_USE_CLN_RF))
+#if defined(STORM_HAVE_GMP)
 inline size_t hash_value(mpq_class const& q) {
     std::hash<mpq_class> h;
     return h(q);

src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp

@@ -66,7 +66,7 @@ namespace storm {
                         submatrix = (model.getRowColumnIdentity() * maybeStatesAdd) - submatrix;
                         
                         // Create the solution vector.
-                        std::vector<ValueType> x(maybeStates.getNonZeroCount(), ValueType(0.5));
+                        std::vector<ValueType> x(maybeStates.getNonZeroCount(), storm::utility::convertNumber<ValueType>(0.5));
                         
                         // Translate the symbolic matrix/vector to their explicit representations and solve the equation system.
                         storm::storage::SparseMatrix<ValueType> explicitSubmatrix = submatrix.toMatrix(odd, odd);
@@ -230,7 +230,7 @@ namespace storm {
                         submatrix = (model.getRowColumnIdentity() * maybeStatesAdd) - submatrix;
                         
                         // Create the solution vector.
-                        std::vector<ValueType> x(maybeStates.getNonZeroCount(), ValueType(0.5));
+                        std::vector<ValueType> x(maybeStates.getNonZeroCount(), storm::utility::convertNumber<ValueType>(0.5));
                         
                         // Translate the symbolic matrix/vector to their explicit representations.
                         storm::storage::SparseMatrix<ValueType> explicitSubmatrix = submatrix.toMatrix(odd, odd);

src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp

@@ -72,7 +72,7 @@ namespace storm {
                         submatrix *= maybeStatesAdd.swapVariables(model.getRowColumnMetaVariablePairs());
                         
                         // Create the solution vector.
-                        std::vector<ValueType> x(maybeStates.getNonZeroCount(), ValueType(0.5));
+                        std::vector<ValueType> x(maybeStates.getNonZeroCount(), storm::utility::zero<ValueType>());
                         
                         // Translate the symbolic matrix/vector to their explicit representations and solve the equation system.
                         std::pair<storm::storage::SparseMatrix<ValueType>, std::vector<ValueType>> explicitRepresentation = submatrix.toMatrixVector(subvector, std::move(rowGroupSizes), model.getNondeterminismVariables(), odd, odd);

src/storm/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp

@@ -33,7 +33,7 @@ namespace storm {
                 // Check whether we need to compute exact probabilities for some states.
                 if (qualitative) {
                     // Set the values for all maybe-states to 0.5 to indicate that their probability values are neither 0 nor 1.
-                    return statesWithProbability01.second.template toAdd<ValueType>() + maybeStates.template toAdd<ValueType>() * model.getManager().getConstant(ValueType(0.5));
+                    return statesWithProbability01.second.template toAdd<ValueType>() + maybeStates.template toAdd<ValueType>() * model.getManager().getConstant(storm::utility::convertNumber<ValueType>(0.5));
                 } else {
                     // If there are maybe states, we need to solve an equation system.
                     if (!maybeStates.isZero()) {

src/storm/utility/constants.cpp

@@ -539,6 +539,11 @@ namespace storm {
         RationalFunction convertNumber(ClnRationalNumber const& number) {
             return RationalFunction(convertNumber<storm::RationalFunctionCoefficient>(number));
         }
+        
+        template<>
+        ClnRationalNumber convertNumber(RationalFunction const& number){
+            return convertNumber<ClnRationalNumber>(number.nominatorAsNumber() / number.denominatorAsNumber());
+        }
 #endif
         
 #if defined(STORM_HAVE_GMP)
@@ -546,16 +551,21 @@ namespace storm {
         RationalFunction convertNumber(GmpRationalNumber const& number) {
             return RationalFunction(convertNumber<storm::RationalFunctionCoefficient>(number));
         }
+        
+        template<>
+        GmpRationalNumber convertNumber(RationalFunction const& number){
+            return convertNumber<GmpRationalNumber>(number.nominatorAsNumber() / number.denominatorAsNumber());
+        }
 #endif
         
         template<>
         uint_fast64_t convertNumber(RationalFunction const& func) {
-            return carl::toInt<unsigned long>(func.nominatorAsNumber());
+            return carl::toInt<unsigned long>(convertNumber<RationalFunctionCoefficient>(func));
         }
         
         template<>
         double convertNumber(RationalFunction const& func) {
-            return carl::toDouble(func.nominatorAsNumber()) / carl::toDouble(func.denominatorAsNumber());
+            return carl::toDouble(convertNumber<RationalFunctionCoefficient>(func));
         }
         
         template<>
@@ -563,11 +573,6 @@ namespace storm {
             return number;
         }
 
-        template<>
-        RationalFunctionCoefficient convertNumber(RationalFunction const& number){
-            return number.nominatorAsNumber() / number.denominatorAsNumber();
-        }
-
         template<>
         RationalFunction convertNumber(storm::storage::sparse::state_type const& number) {
             return RationalFunction(convertNumber<RationalFunctionCoefficient>(number));