cleaned up constants.cpp to finalize separation of rational functions and rational numbers

resources/3rdparty/sylvan/src/storm_wrapper.cpp

@@ -71,7 +71,7 @@ char* storm_rational_number_to_str(storm_rational_number_ptr val, char *buf, siz
     storm::RationalNumber const& srn_a = *(storm::RationalNumber*)val;
     ss << srn_a;
     std::string s = ss.str();
-    if (s.size() < buflen + 1) {
+    if (s.size() + 1 < buflen) {
         std::memcpy(buf, s.c_str(), s.size() + 1);
         return buf;
     } else {
@@ -286,7 +286,6 @@ void print_storm_rational_number(storm_rational_number_ptr a) {
 #endif
     
     storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a;
-    std::cout << srn_a << std::flush;
 }
 
 void print_storm_rational_number_to_file(storm_rational_number_ptr a, FILE* out) {
@@ -334,7 +333,7 @@ int storm_rational_function_equals(storm_rational_function_ptr a, storm_rational
     return (srf_a == srf_b) ? 1 : 0;
 }
 
-char* storm_rational_function_to_str(storm_rational_function_ptr val, char *buf, size_t buflen) {
+char* storm_rational_function_to_str(storm_rational_function_ptr val, char* buf, size_t buflen) {
 #ifndef RATIONAL_FUNCTION_THREAD_SAFE
     std::lock_guard<std::mutex> lock(rationalFunctionMutex);
 #endif
@@ -343,12 +342,12 @@ char* storm_rational_function_to_str(storm_rational_function_ptr val, char *buf,
     storm::RationalFunction const& srf_a = *(storm::RationalFunction*)val;
     ss << srf_a;
     std::string s = ss.str();
-    if (s.size() < buflen + 1) {
-        std::memcpy(buf, s.c_str(), s.size() + 1);
+    if (s.size() + 1 < buflen) {
+        std::strcpy(buf, s.c_str());
         return buf;
     } else {
         char* result = (char*)malloc(s.size() + 1);
-        std::memcpy(result, s.c_str(), s.size() + 1);
+        std::strcpy(result, s.c_str());
         return result;
     }
 }
@@ -485,7 +484,7 @@ storm_rational_function_ptr storm_rational_function_mod(storm_rational_function_
     storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a;
     storm::RationalFunction const& srf_b = *(storm::RationalFunction const*)b;
     
-    if (!storm::utility::isInteger(srf_a) || !storm::utility::isInteger(srf_b)) {
+    if (!storm::utility::isConstant(srf_a) || !storm::utility::isConstant(srf_b)) {
         throw storm::exceptions::InvalidOperationException() << "Operands of mod must not be non-constant rational functions.";
     }
     throw storm::exceptions::InvalidOperationException() << "Modulo not supported for rational functions.";
@@ -522,11 +521,11 @@ int storm_rational_function_less(storm_rational_function_ptr a, storm_rational_f
     
     storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a;
     storm::RationalFunction const& srf_b = *(storm::RationalFunction const*)b;
-    if (!storm::utility::isInteger(srf_a) || !storm::utility::isInteger(srf_b)) {
+    if (!storm::utility::isConstant(srf_a) || !storm::utility::isConstant(srf_b)) {
         throw storm::exceptions::InvalidOperationException() << "Operands of less must not be non-constant rational functions.";
     }
     
-    if (srf_a.nominatorAsNumber() < srf_b.nominatorAsNumber()) {
+    if (storm::utility::convertNumber<storm::RationalFunctionCoefficient>(srf_a) < storm::utility::convertNumber<storm::RationalFunctionCoefficient>(srf_b)) {
         return 1;
     } else {
         return 0;
@@ -541,11 +540,11 @@ int storm_rational_function_less_or_equal(storm_rational_function_ptr a, storm_r
     
     storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a;
     storm::RationalFunction const& srf_b = *(storm::RationalFunction const*)b;
-    if (!storm::utility::isInteger(srf_a) || !storm::utility::isInteger(srf_b)) {
+    if (!storm::utility::isConstant(srf_a) || !storm::utility::isConstant(srf_b)) {
         throw storm::exceptions::InvalidOperationException() << "Operands of less-or-equal must not be non-constant rational functions.";
     }
     
-    if (srf_a.nominatorAsNumber() <= srf_b.nominatorAsNumber()) {
+    if (storm::utility::convertNumber<storm::RationalFunctionCoefficient>(srf_a) <= storm::utility::convertNumber<storm::RationalFunctionCoefficient>(srf_b)) {
         return 1;
     } else {
         return 0;
@@ -569,10 +568,10 @@ storm_rational_function_ptr storm_rational_function_floor(storm_rational_functio
 #endif
     
     storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a;
-    if (!storm::utility::isInteger(srf_a)) {
+    if (!storm::utility::isConstant(srf_a)) {
         throw storm::exceptions::InvalidOperationException() << "Operand of floor must not be non-constant rational function.";
     }
-    storm::RationalFunction* result_srf = new storm::RationalFunction(carl::floor(srf_a.nominatorAsNumber()));
+    storm::RationalFunction* result_srf = new storm::RationalFunction(carl::floor(storm::utility::convertNumber<storm::RationalFunctionCoefficient>(srf_a)));
     return (storm_rational_function_ptr)result_srf;
 }
 
@@ -582,10 +581,10 @@ storm_rational_function_ptr storm_rational_function_ceil(storm_rational_function
 #endif
     
     storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a;
-    if (!storm::utility::isInteger(srf_a)) {
+    if (!storm::utility::isConstant(srf_a)) {
         throw storm::exceptions::InvalidOperationException() << "Operand of ceil must not be non-constant rational function.";
     }
-    storm::RationalFunction* result_srf = new storm::RationalFunction(carl::ceil(srf_a.nominatorAsNumber()));
+    storm::RationalFunction* result_srf = new storm::RationalFunction(carl::ceil(storm::utility::convertNumber<storm::RationalFunctionCoefficient>(srf_a)));
     return (storm_rational_function_ptr)result_srf;
 }
 

resources/3rdparty/sylvan/src/sylvan_storm_rational_function.c

@@ -38,8 +38,8 @@ static void sylvan_storm_rational_function_destroy(uint64_t val) {
     storm_rational_function_destroy(x);
 }
 
-static char* sylvan_storm_rational_function_to_str(int comp, uint64_t val, char *buf, size_t buflen) {
-    return storm_rational_function_to_str((storm_rational_function_ptr)(size_t)val, *buf, buflen);
+static char* sylvan_storm_rational_function_to_str(int comp, uint64_t val, char* buf, size_t buflen) {
+    return storm_rational_function_to_str((storm_rational_function_ptr)(size_t)val, buf, buflen);
     (void)comp;
 }
 
@@ -66,7 +66,7 @@ MTBDD mtbdd_storm_rational_function(storm_rational_function_ptr val) {
 
 storm_rational_function_ptr mtbdd_getstorm_rational_function_ptr(MTBDD terminal) {
     uint64_t value = mtbdd_getvalue(terminal);
-    return (storm_rational_function_ptr*)value;
+    return (storm_rational_function_ptr)value;
 }
 
 TASK_IMPL_2(MTBDD, mtbdd_op_bool_to_storm_rational_function, MTBDD, a, size_t, v) {

resources/3rdparty/sylvan/src/sylvan_storm_rational_number.c

@@ -38,8 +38,8 @@ static void sylvan_storm_rational_number_destroy(uint64_t val) {
     storm_rational_number_destroy(x);
 }
 
-static char* sylvan_storm_rational_number_to_str(int comp, uint64_t val, char *buf, size_t buflen) {
-    return storm_rational_number_to_str((storm_rational_number_ptr)(size_t)val, *buf, buflen);
+static char* sylvan_storm_rational_number_to_str(int comp, uint64_t val, char* buf, size_t buflen) {
+    return storm_rational_number_to_str((storm_rational_number_ptr)(size_t)val, buf, buflen);
     (void)comp;
 }
 
@@ -66,7 +66,7 @@ MTBDD mtbdd_storm_rational_number(storm_rational_number_ptr val) {
 
 storm_rational_number_ptr mtbdd_getstorm_rational_number_ptr(MTBDD terminal) {
     uint64_t value = mtbdd_getvalue(terminal);
-    return (storm_rational_number_ptr*)value;
+    return (storm_rational_number_ptr)value;
 }
 
 TASK_IMPL_2(MTBDD, mtbdd_op_bool_to_storm_rational_number, MTBDD, a, size_t, v) {

src/storm/adapters/CarlAdapter.h

@@ -41,11 +41,11 @@ namespace carl {
 namespace storm {
     typedef carl::Variable RationalFunctionVariable;
 
-#if defined STORM_HAVE_CLN && defined STORM_USE_CLN_EA
+#if defined(STORM_HAVE_CLN) && defined(STORM_USE_CLN_RF)
     typedef cln::cl_RA RationalFunctionCoefficient;
-#elif defined STORM_HAVE_GMP && !defined STORM_USE_CLN_EA
+#elif defined(STORM_HAVE_GMP) && !defined(STORM_USE_CLN_RF)
     typedef mpq_class RationalFunctionCoefficient;
-#elif defined STORM_USE_CLN_EA
+#elif defined(STORM_USE_CLN_RF)
 #error CLN is to be used, but is not available.
 #else
 #error GMP is to be used, but is not available.

src/storm/adapters/NumberAdapter.h

@@ -2,21 +2,21 @@
 
 #include "storm-config.h"
 
-#if defined STORM_HAVE_CLN
+#if defined(STORM_HAVE_CLN)
 #pragma clang diagnostic push
 #pragma clang diagnostic ignored "-Wmismatched-tags"
 #include <cln/cln.h>
 #pragma clang diagnostic pop
 #endif
 
-#if defined STORM_HAVE_GMP
+#if defined(STORM_HAVE_GMP)
 #include <gmp.h>
 #include <gmpxx.h>
 #endif
 
 #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) && (defined(STORM_USE_CLN_EA) || defined(STORM_USE_CLN_RF))
 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) && (!defined(STORM_USE_CLN_EA) || !defined(STORM_USE_CLN_RF))
 inline size_t hash_value(mpq_class const& q) {
     std::hash<mpq_class> h;
     return h(q);
@@ -33,11 +33,18 @@ inline size_t hash_value(mpq_class const& q) {
 #endif
 
 namespace storm {
-#if defined STORM_HAVE_CLN && defined STORM_USE_CLN_EA
-    typedef cln::cl_RA RationalNumber;
-#elif defined STORM_HAVE_GMP && !defined STORM_USE_CLN_EA
-    typedef mpq_class RationalNumber;
-#elif defined STORM_USE_CLN_EA
+#if defined(STORM_HAVE_CLN)
+    typedef cln::cl_RA ClnRationalNumber;
+#endif
+#if defined(STORM_HAVE_GMP)
+    typedef mpq_class GmpRationalNumber;
+#endif
+    
+#if defined(STORM_HAVE_CLN) && defined(STORM_USE_CLN_EA)
+    typedef ClnRationalNumber RationalNumber;
+#elif defined(STORM_HAVE_GMP) && !defined(STORM_USE_CLN_EA)
+    typedef GmpRationalNumber RationalNumber;
+#elif defined(STORM_USE_CLN_EA)
 #error CLN is to be used, but is not available.
 #else
 #error GMP is to be used, but is not available.

src/storm/builder/DdPrismModelBuilder.cpp

@@ -715,8 +715,6 @@ namespace storm {
                     commandDd += updateResultsIt->updateDd * probabilityDd;
                 }
                 
-                commandDd.exportToDot("command.dot");
-                
                 return ActionDecisionDiagram(guard, guard.template toAdd<ValueType>() * commandDd, globalVariablesInSomeUpdate);
             } else {
                 return ActionDecisionDiagram(*generationInfo.manager);
@@ -1396,8 +1394,6 @@ namespace storm {
             storm::dd::Bdd<Type> statesWithTransition = transitionMatrixBdd.existsAbstract(generationInfo.columnMetaVariables);
             storm::dd::Bdd<Type> deadlockStates = reachableStates && !statesWithTransition;
                         
-            transitionMatrix.exportToDot("trans.dot");
-            
             // If there are deadlocks, either fix them or raise an error.
             if (!deadlockStates.isZero()) {
                 // If we need to fix deadlocks, we do so now.

src/storm/modelchecker/region/ApproximationModel.cpp

@@ -166,7 +166,7 @@ namespace storm {
                                 if(this->maybeStates.get(oldEntry.getColumn())){
                                     STORM_LOG_THROW(eqSysMatrixEntry->getColumn()==newIndices[oldEntry.getColumn()], storm::exceptions::UnexpectedException, "old and new entries do not match");
                                     if(storm::utility::isConstant(oldEntry.getValue())){
-                                        eqSysMatrixEntry->setValue(storm::utility::region::convertNumber<ConstantType>(storm::utility::region::getConstantPart(oldEntry.getValue())));
+                                        eqSysMatrixEntry->setValue(storm::utility::convertNumber<ConstantType>(storm::utility::region::getConstantPart(oldEntry.getValue())));
                                     } else {
                                         auto functionsIt = this->funcSubData.functions.insert(FunctionEntry(FunctionSubstitution(oldEntry.getValue(), this->matrixData.rowSubstitutions[curRow]), dummyNonZeroValue)).first;
                                         this->matrixData.assignment.emplace_back(eqSysMatrixEntry, functionsIt->second);
@@ -181,7 +181,7 @@ namespace storm {
                             }
                             if(!this->computeRewards){
                                 if(storm::utility::isConstant(storm::utility::simplify(targetProbability))){
-                                    *vectorIt = storm::utility::region::convertNumber<ConstantType>(storm::utility::region::getConstantPart(targetProbability));
+                                    *vectorIt = storm::utility::convertNumber<ConstantType>(storm::utility::region::getConstantPart(targetProbability));
                                 } else {
                                     auto functionsIt = this->funcSubData.functions.insert(FunctionEntry(FunctionSubstitution(targetProbability, this->matrixData.rowSubstitutions[curRow]), dummyNonZeroValue)).first;
                                     this->vectorData.assignment.emplace_back(vectorIt, functionsIt->second);
@@ -212,7 +212,7 @@ namespace storm {
                 auto vectorIt = this->vectorData.vector.begin();
                 for(auto oldState : this->maybeStates){
                     if(storm::utility::isConstant(parametricModel.getUniqueRewardModel().getStateRewardVector()[oldState])){
-                        ConstantType reward = storm::utility::region::convertNumber<ConstantType>(storm::utility::region::getConstantPart(parametricModel.getUniqueRewardModel().getStateRewardVector()[oldState]));
+                        ConstantType reward = storm::utility::convertNumber<ConstantType>(storm::utility::region::getConstantPart(parametricModel.getUniqueRewardModel().getStateRewardVector()[oldState]));
                         //Add one of these entries for every row in the row group of oldState
                         for(auto matrixRow=this->matrixData.matrix.getRowGroupIndices()[oldState]; matrixRow<this->matrixData.matrix.getRowGroupIndices()[oldState+1]; ++matrixRow){
                             *vectorIt = reward;
@@ -334,7 +334,7 @@ namespace storm {
                             instantiatedSubs[funcSub.second][vertexSub.first]=vertexSub.second;
                         }
                         //evaluate the function
-                        ConstantType currValue = storm::utility::region::convertNumber<ConstantType>(
+                        ConstantType currValue = storm::utility::convertNumber<ConstantType>(
                                 storm::utility::region::evaluateFunction(
                                     funcSub.first,
                                     instantiatedSubs[funcSub.second]

src/storm/modelchecker/region/ParameterRegion.cpp

@@ -206,11 +206,11 @@ namespace storm {
             std::string ParameterRegion<ParametricType>::toString() const {
                 std::stringstream regionstringstream;
                 for (auto var : this->getVariables()) {
-                    regionstringstream << storm::utility::region::convertNumber<double>(this->getLowerBoundary(var));
+                    regionstringstream << storm::utility::convertNumber<double>(this->getLowerBoundary(var));
                     regionstringstream << "<=";
                     regionstringstream << storm::utility::region::getVariableName(var);
                     regionstringstream << "<=";
-                    regionstringstream << storm::utility::region::convertNumber<double>(this->getUpperBoundary(var));
+                    regionstringstream << storm::utility::convertNumber<double>(this->getUpperBoundary(var));
                     regionstringstream << ",";
                 }
                 std::string regionstring = regionstringstream.str();
@@ -238,8 +238,8 @@ namespace storm {
                     STORM_LOG_THROW(parameter.length()>0, storm::exceptions::InvalidArgumentException, "When parsing the region" << parameterBoundariesString << " I could not find a parameter");
 
                     VariableType var = storm::utility::region::getVariableFromString<VariableType>(parameter);
-                    CoefficientType lb = storm::utility::region::convertNumber<CoefficientType>(parameterBoundariesString.substr(0,positionOfFirstRelation));
-                    CoefficientType ub = storm::utility::region::convertNumber<CoefficientType>(parameterBoundariesString.substr(positionOfSecondRelation+2));
+                    CoefficientType lb = storm::utility::convertNumber<CoefficientType>(parameterBoundariesString.substr(0,positionOfFirstRelation));
+                    CoefficientType ub = storm::utility::convertNumber<CoefficientType>(parameterBoundariesString.substr(positionOfSecondRelation+2));
                     lowerBoundaries.emplace(std::make_pair(var, lb));  
                     upperBoundaries.emplace(std::make_pair(var, ub));
                 }

src/storm/modelchecker/region/SparseDtmcRegionModelChecker.cpp

@@ -296,7 +296,7 @@ namespace storm {
                 }
                 if(isResultConstant){
                     STORM_LOG_WARN("For the given property, the reachability Value is constant, i.e., independent of the region");
-                    constantResult = storm::utility::region::convertNumber<ConstantType>(-1.0);
+                    constantResult = storm::utility::convertNumber<ConstantType>(-1.0);
                 }
             }
 
@@ -392,7 +392,7 @@ namespace storm {
                 }
                 if(isResultConstant){
                     STORM_LOG_WARN("For the given property, the reachability Value is constant, i.e., independent of the region");
-                    constantResult = storm::utility::region::convertNumber<ConstantType>(-1.0);
+                    constantResult = storm::utility::convertNumber<ConstantType>(-1.0);
                 }
             }
 
@@ -597,7 +597,7 @@ namespace storm {
                 storm::expressions::ExpressionManager manager; //this manager will do nothing as we will use carl expressions..
                 this->smtSolver = std::shared_ptr<storm::solver::SmtlibSmtSolver>(new storm::solver::SmtlibSmtSolver(manager, true));
 
-                ParametricType bound= storm::utility::region::convertNumber<ParametricType>(this->getSpecifiedFormulaBound());
+                ParametricType bound= storm::utility::convertNumber<ParametricType>(this->getSpecifiedFormulaBound());
 
                 // To prove that the property is satisfied in the initial state for all parameters,
                 // we ask the solver whether the negation of the property is satisfiable and invert the answer.

src/storm/modelchecker/region/SparseMdpRegionModelChecker.cpp

@@ -248,7 +248,7 @@ namespace storm {
                 }
                 if(isResultConstant){
                     STORM_LOG_WARN("For the given property, the reachability Value is constant, i.e., independent of the region");
-                    constantResult = storm::utility::region::convertNumber<ConstantType>(-1.0); //-1 denotes that the result is constant but not yet computed
+                    constantResult = storm::utility::convertNumber<ConstantType>(-1.0); //-1 denotes that the result is constant but not yet computed
                 }
             }
 

src/storm/modelchecker/region/SparseRegionModelChecker.cpp

@@ -79,7 +79,7 @@ namespace storm {
 
             template<typename ParametricSparseModelType, typename ConstantType>
             ConstantType SparseRegionModelChecker<ParametricSparseModelType, ConstantType>::getSpecifiedFormulaBound() const {
-                return storm::utility::region::convertNumber<ConstantType>(this->getSpecifiedFormula()->getThreshold());
+                return storm::utility::convertNumber<ConstantType>(this->getSpecifiedFormula()->getThreshold());
             }
 
             template<typename ParametricSparseModelType, typename ConstantType>
@@ -177,7 +177,7 @@ namespace storm {
                             (!settings.doSample() && settings.getApproxMode()==storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST)){
                         initializeSamplingModel(*this->getSimpleModel(), this->getSimpleFormula());
                     }
-                } else if (this->isResultConstant() && this->constantResult.get() == storm::utility::region::convertNumber<ConstantType>(-1.0)){
+                } else if (this->isResultConstant() && this->constantResult.get() == storm::utility::convertNumber<ConstantType>(-1.0)){
                     //In this case, the result is constant but has not been computed yet. so do it now!
                     STORM_LOG_DEBUG("The Result is constant and will be computed now.");
                     initializeSamplingModel(*this->getSimpleModel(), this->getSimpleFormula());
@@ -241,7 +241,7 @@ namespace storm {
                 CoefficientType fractionOfUndiscoveredArea = storm::utility::one<CoefficientType>();
                 CoefficientType fractionOfAllSatArea = storm::utility::zero<CoefficientType>();
                 CoefficientType fractionOfAllViolatedArea = storm::utility::zero<CoefficientType>();
-                while(fractionOfUndiscoveredArea > storm::utility::region::convertNumber<CoefficientType>(refinementThreshold)){
+                while(fractionOfUndiscoveredArea > storm::utility::convertNumber<CoefficientType>(refinementThreshold)){
                     STORM_LOG_THROW(indexOfCurrentRegion < regions.size(), storm::exceptions::InvalidStateException, "Threshold for undiscovered area not reached but no unprocessed regions left.");
                     ParameterRegion<ParametricType>& currentRegion = regions[indexOfCurrentRegion];
                     this->checkRegion(currentRegion);
@@ -263,7 +263,7 @@ namespace storm {
                     ++indexOfCurrentRegion;
                 }
                 std::cout << " done! " << std::endl << "Fraction of ALLSAT;ALLVIOLATED;UNDISCOVERED area:" << std::endl;
-                std::cout << "REFINEMENTRESULT;" <<storm::utility::region::convertNumber<double>(fractionOfAllSatArea) << ";" << storm::utility::region::convertNumber<double>(fractionOfAllViolatedArea) << ";" << storm::utility::region::convertNumber<double>(fractionOfUndiscoveredArea) << std::endl;
+                std::cout << "REFINEMENTRESULT;" <<storm::utility::convertNumber<double>(fractionOfAllSatArea) << ";" << storm::utility::convertNumber<double>(fractionOfAllViolatedArea) << ";" << storm::utility::convertNumber<double>(fractionOfUndiscoveredArea) << std::endl;
                 
             }
             
@@ -487,7 +487,7 @@ namespace storm {
             
             template<typename ParametricSparseModelType, typename ConstantType>
             bool SparseRegionModelChecker<ParametricSparseModelType, ConstantType>::valueIsInBoundOfFormula(CoefficientType const& value){
-                return valueIsInBoundOfFormula(storm::utility::region::convertNumber<ConstantType>(value));
+                return valueIsInBoundOfFormula(storm::utility::convertNumber<ConstantType>(value));
             }
 
             template<typename ParametricSparseModelType, typename ConstantType>

src/storm/storage/SparseMatrix.cpp

@@ -1605,16 +1605,29 @@ namespace storm {
         template bool SparseMatrix<int>::isSubmatrixOf(SparseMatrix<storm::storage::sparse::state_type> const& matrix) const;
         
 #ifdef STORM_HAVE_CARL
-        // Rat Number
-        template class MatrixEntry<typename SparseMatrix<RationalNumber>::index_type, RationalNumber>;
-        template std::ostream& operator<<(std::ostream& out, MatrixEntry<uint_fast64_t, RationalNumber> const& entry);
-        template class SparseMatrixBuilder<RationalNumber>;
-        template class SparseMatrix<RationalNumber>;
-        template std::ostream& operator<<(std::ostream& out, SparseMatrix<RationalNumber> const& matrix);
-        template std::vector<storm::RationalNumber> SparseMatrix<RationalNumber>::getPointwiseProductRowSumVector(storm::storage::SparseMatrix<storm::RationalNumber> const& otherMatrix) const;
-        template bool SparseMatrix<storm::RationalNumber>::isSubmatrixOf(SparseMatrix<storm::RationalNumber> const& matrix) const;
-        
-        // Rat Function
+        // Rational Numbers
+        
+#if defined(STORM_HAVE_CLN)
+        template class MatrixEntry<typename SparseMatrix<ClnRationalNumber>::index_type, ClnRationalNumber>;
+        template std::ostream& operator<<(std::ostream& out, MatrixEntry<uint_fast64_t, ClnRationalNumber> const& entry);
+        template class SparseMatrixBuilder<ClnRationalNumber>;
+        template class SparseMatrix<ClnRationalNumber>;
+        template std::ostream& operator<<(std::ostream& out, SparseMatrix<ClnRationalNumber> const& matrix);
+        template std::vector<storm::ClnRationalNumber> SparseMatrix<ClnRationalNumber>::getPointwiseProductRowSumVector(storm::storage::SparseMatrix<storm::ClnRationalNumber> const& otherMatrix) const;
+        template bool SparseMatrix<storm::ClnRationalNumber>::isSubmatrixOf(SparseMatrix<storm::ClnRationalNumber> const& matrix) const;
+#endif
+      
+#if defined(STORM_HAVE_GMP)
+        template class MatrixEntry<typename SparseMatrix<GmpRationalNumber>::index_type, GmpRationalNumber>;
+        template std::ostream& operator<<(std::ostream& out, MatrixEntry<uint_fast64_t, GmpRationalNumber> const& entry);
+        template class SparseMatrixBuilder<GmpRationalNumber>;
+        template class SparseMatrix<GmpRationalNumber>;
+        template std::ostream& operator<<(std::ostream& out, SparseMatrix<GmpRationalNumber> const& matrix);
+        template std::vector<storm::GmpRationalNumber> SparseMatrix<GmpRationalNumber>::getPointwiseProductRowSumVector(storm::storage::SparseMatrix<storm::GmpRationalNumber> const& otherMatrix) const;
+        template bool SparseMatrix<storm::GmpRationalNumber>::isSubmatrixOf(SparseMatrix<storm::GmpRationalNumber> const& matrix) const;
+#endif
+
+        // Rational Function
         template class MatrixEntry<typename SparseMatrix<RationalFunction>::index_type, RationalFunction>;
         template std::ostream& operator<<(std::ostream& out, MatrixEntry<uint_fast64_t, RationalFunction> const& entry);
         template class SparseMatrixBuilder<RationalFunction>;

src/storm/storage/dd/sylvan/SylvanAddIterator.cpp

@@ -11,7 +11,6 @@
 #include <cmath>
 
 #include "storm/adapters/CarlAdapter.h"
-#include "storm-config.h"
 
 namespace storm {
     namespace dd {

src/storm/utility/ConstantsComparator.cpp

@@ -111,10 +111,17 @@ namespace storm {
         template class ConstantsComparator<storm::storage::sparse::state_type>;
 
 #ifdef STORM_HAVE_CARL
+#if defined(STORM_HAVE_CLN)
+        template class ConstantsComparator<ClnRationalNumber>;
+#endif
+        
+#if defined(STORM_HAVE_GMP)
+        template class ConstantsComparator<GmpRationalNumber>;
+#endif
+        
         template class ConstantsComparator<RationalFunction>;
         template class ConstantsComparator<Polynomial>;
         template class ConstantsComparator<Interval>;
-        template class ConstantsComparator<RationalNumber>;
 #endif
     }
 }

src/storm/utility/constants.h

@@ -47,11 +47,20 @@ namespace storm {
         bool isInfinity(ValueType const& a);
 
         template<typename ValueType>
-        ValueType pow(ValueType const& value, uint_fast64_t exponent);
+        bool isInteger(ValueType const& number);
+
+        template<typename TargetType, typename SourceType>
+        TargetType convertNumber(SourceType const& number);
 
         template<typename ValueType>
         ValueType simplify(ValueType value);
 
+        template<typename IndexType, typename ValueType>
+        storm::storage::MatrixEntry<IndexType, ValueType>& simplify(storm::storage::MatrixEntry<IndexType, ValueType>& matrixEntry);
+        
+        template<typename IndexType, typename ValueType>
+        storm::storage::MatrixEntry<IndexType, ValueType>&& simplify(storm::storage::MatrixEntry<IndexType, ValueType>&& matrixEntry);
+
         template<typename ValueType>
         std::pair<ValueType, ValueType> minmax(std::vector<ValueType> const& values);
         
@@ -70,14 +79,8 @@ namespace storm {
         template<typename K, typename ValueType>
         ValueType maximum(std::map<K, ValueType> const& values);
         
-        template<typename IndexType, typename ValueType>
-        storm::storage::MatrixEntry<IndexType, ValueType>& simplify(storm::storage::MatrixEntry<IndexType, ValueType>& matrixEntry);
-
-        template<typename IndexType, typename ValueType>
-        storm::storage::MatrixEntry<IndexType, ValueType>&& simplify(storm::storage::MatrixEntry<IndexType, ValueType>&& matrixEntry);
-
-        template<typename TargetType, typename SourceType>
-        TargetType convertNumber(SourceType const& number);
+        template<typename ValueType>
+        ValueType pow(ValueType const& value, uint_fast64_t exponent);
 
         template<typename ValueType>
         ValueType sqrt(ValueType const& number);
@@ -91,9 +94,6 @@ namespace storm {
         template<typename ValueType>
         ValueType ceil(ValueType const& number);
         
-        template<typename ValueType>
-        bool isInteger(ValueType const& number);
-        
         template<typename ValueType>
         std::string to_string(ValueType const& value);
     }

src/storm/utility/parametric.h

@@ -31,7 +31,7 @@ namespace storm {
             template<>
             struct VariableType<storm::RationalFunction> { typedef storm::RationalFunctionVariable type; };
             template<>
-            struct CoefficientType<storm::RationalFunction> { typedef storm::RationalNumber type; };
+            struct CoefficientType<storm::RationalFunction> { typedef storm::RationalFunctionCoefficient type; };
 #endif
             
             /*!

src/storm/utility/region.cpp

@@ -17,53 +17,7 @@ namespace storm {
     namespace utility{
         namespace region {
             
-            template<>
-            double convertNumber<double, double>(double const& number){
-                return number;
-            }
-            
-            template<>
-            double&& convertNumber<double>(double&& number){
-                return std::move(number);
-           }
-            
-            template<>
-            double convertNumber<double, std::string>(std::string const& number){
-                return std::stod(number);
-            }
-            
 #ifdef STORM_HAVE_CARL
-            template<>
-            storm::RationalNumber convertNumber<storm::RationalNumber, double>(double const& number){
-                return carl::rationalize<storm::RationalNumber>(number);
-            }
-            
-            template<>
-            storm::RationalFunction convertNumber<storm::RationalFunction, double>(double const& number){
-                return storm::RationalFunction(convertNumber<storm::RationalNumber>(number));
-            }
-            
-            template<>
-            double convertNumber<double, storm::RationalNumber>(storm::RationalNumber const& number){
-                return carl::toDouble(number);
-            }
-            
-            template<>
-            storm::RationalNumber convertNumber<storm::RationalNumber, storm::RationalNumber>(storm::RationalNumber const& number){
-                return number;
-            }
-            
-            template<>
-            storm::RationalNumber&& convertNumber<storm::RationalNumber>(storm::RationalNumber&& number){
-                return std::move(number);
-            }
-            
-            template<>
-            storm::RationalNumber convertNumber<storm::RationalNumber, std::string>(std::string const& number){
-                //We parse the number as double and then convert it to a a rational number.
-                return convertNumber<storm::RationalNumber>(convertNumber<double>(number));
-            }
-            
             template<>
             storm::RationalFunctionVariable getVariableFromString<storm::RationalFunctionVariable>(std::string variableString){
                 storm::RationalFunctionVariable const& var = carl::VariablePool::getInstance().findVariableWithName(variableString);
@@ -154,7 +108,7 @@ namespace storm {
             }
             
             template<>
-            void addParameterBoundsToSmtSolver<storm::solver::SmtlibSmtSolver, storm::RationalFunctionVariable, storm::RationalNumber>(std::shared_ptr<storm::solver::SmtlibSmtSolver> solver, storm::RationalFunctionVariable const& variable, storm::logic::ComparisonType relation, storm::RationalNumber const& bound){
+            void addParameterBoundsToSmtSolver<storm::solver::SmtlibSmtSolver, storm::RationalFunctionVariable, storm::RationalFunctionCoefficient>(std::shared_ptr<storm::solver::SmtlibSmtSolver> solver, storm::RationalFunctionVariable const& variable, storm::logic::ComparisonType relation, storm::RationalFunctionCoefficient const& bound){
                 storm::CompareRelation compRel;
                 switch (relation){
                     case storm::logic::ComparisonType::Greater:
@@ -184,7 +138,7 @@ namespace storm {
             }
             
             template<>
-            storm::RationalFunction getNewFunction<storm::RationalFunction, storm::RationalNumber>(storm::RationalNumber initialValue) {
+            storm::RationalFunction getNewFunction<storm::RationalFunction, storm::RationalFunctionCoefficient>(storm::RationalFunctionCoefficient initialValue) {
                 std::shared_ptr<carl::Cache<carl::PolynomialFactorizationPair<storm::RawPolynomial>>> cache(new carl::Cache<carl::PolynomialFactorizationPair<storm::RawPolynomial>>());
                 return storm::RationalFunction(storm::RationalFunction::PolyType(storm::RationalFunction::PolyType::PolyType(initialValue), cache));
             }

src/storm/utility/region.h

@@ -37,20 +37,6 @@ namespace storm {
             using CoefficientType = std::nullptr_t;
 #endif
             
-            /*
-             * Converts a number from one type to a number from the other.
-             * If no exact conversion is possible, the number is rounded up or down, using the given precision or the one from the settings.
-             */
-            template<typename TargetType, typename SourceType>
-            TargetType convertNumber(SourceType const& number);
-            
-            /*
-             * Converts a number from one type to a number from the other.
-             * If no exact conversion is possible, the number is rounded up or down, using the given precision or the one from the settings.
-             */
-            template<typename ValueType>
-            ValueType&& convertNumber(ValueType&& number);
-            
             /*
              * retrieves the variable object from the given string
              * Throws an exception if variable not found

src/storm/utility/storm.h

@@ -523,7 +523,7 @@ namespace storm {
      * @return true iff the specified formula is satisfied (i.e., iff the reachability value is within the bound of the formula)
      */
     inline bool checkSamplingPoint(std::shared_ptr<storm::modelchecker::region::AbstractSparseRegionModelChecker<storm::RationalFunction, double>> regionModelChecker,
-                                   std::map<storm::RationalFunctionVariable, storm::RationalNumber> const& point){
+                                   std::map<storm::RationalFunctionVariable, storm::RationalFunctionCoefficient> const& point){
         return regionModelChecker->valueIsInBoundOfFormula(regionModelChecker->getReachabilityValue(point));
     }
 
@@ -543,8 +543,8 @@ namespace storm {
      * proveAllSat=false, return=false ==> the approximative value IS within the bound of the formula (either the approximation is too bad or there are points in the region that satisfy the property)
      */
     inline bool checkRegionApproximation(std::shared_ptr<storm::modelchecker::region::AbstractSparseRegionModelChecker<storm::RationalFunction, double>> regionModelChecker,
-                                         std::map<storm::RationalFunctionVariable, storm::RationalNumber> const& lowerBoundaries,
-                                         std::map<storm::RationalFunctionVariable, storm::RationalNumber> const& upperBoundaries,
+                                         std::map<storm::RationalFunctionVariable, storm::RationalFunctionCoefficient> const& lowerBoundaries,
+                                         std::map<storm::RationalFunctionVariable, storm::RationalFunctionCoefficient> const& upperBoundaries,
                                          bool proveAllSat){
         storm::modelchecker::region::ParameterRegion<storm::RationalFunction> region(lowerBoundaries, upperBoundaries);
         return regionModelChecker->checkRegionWithApproximation(region, proveAllSat);

src/test/modelchecker/EigenDtmcPrctlModelCheckerTest.cpp

@@ -132,10 +132,10 @@ TEST(EigenDtmcPrctlModelCheckerTest, Die_RationalFunction) {
     ASSERT_EQ(dtmc->getNumberOfStates(), 13ull);
     ASSERT_EQ(dtmc->getNumberOfTransitions(), 20ull);
     
-    std::map<storm::RationalFunctionVariable, storm::RationalNumber> instantiation;
+    std::map<storm::RationalFunctionVariable, storm::RationalFunctionCoefficient> instantiation;
     std::set<storm::RationalFunctionVariable> variables = storm::models::sparse::getProbabilityParameters(*dtmc);
     ASSERT_EQ(variables.size(), 1ull);
-    instantiation.emplace(*variables.begin(), storm::RationalNumber(1) / storm::RationalNumber(2));
+    instantiation.emplace(*variables.begin(), storm::utility::one<storm::RationalFunctionCoefficient>() / storm::utility::convertNumber<storm::RationalFunctionCoefficient>(2));
     
     storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>> checker(*dtmc, std::make_unique<storm::solver::EigenLinearEquationSolverFactory<storm::RationalFunction>>());
     
@@ -144,28 +144,28 @@ TEST(EigenDtmcPrctlModelCheckerTest, Die_RationalFunction) {
     std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
     storm::modelchecker::ExplicitQuantitativeCheckResult<storm::RationalFunction>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<storm::RationalFunction>();
     
-    EXPECT_EQ(storm::RationalNumber(1) / storm::RationalNumber(6), quantitativeResult1[0].evaluate(instantiation));
+    EXPECT_EQ(storm::utility::one<storm::RationalFunctionCoefficient>() / storm::utility::convertNumber<storm::RationalFunctionCoefficient>(6), quantitativeResult1[0].evaluate(instantiation));
     
     formula = formulaParser.parseSingleFormulaFromString("P=? [F \"two\"]");
     
     result = checker.check(*formula);
     storm::modelchecker::ExplicitQuantitativeCheckResult<storm::RationalFunction>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<storm::RationalFunction>();
     
-    EXPECT_EQ(storm::RationalNumber(1) / storm::RationalNumber(6), quantitativeResult2[0].evaluate(instantiation));
+    EXPECT_EQ(storm::utility::one<storm::RationalFunctionCoefficient>() / storm::utility::convertNumber<storm::RationalFunctionCoefficient>(6), quantitativeResult2[0].evaluate(instantiation));
     
     formula = formulaParser.parseSingleFormulaFromString("P=? [F \"three\"]");
     
     result = checker.check(*formula);
     storm::modelchecker::ExplicitQuantitativeCheckResult<storm::RationalFunction>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<storm::RationalFunction>();
     
-    EXPECT_EQ(storm::RationalNumber(1) / storm::RationalNumber(6), quantitativeResult3[0].evaluate(instantiation));
+    EXPECT_EQ(storm::utility::one<storm::RationalFunctionCoefficient>() / storm::utility::convertNumber<storm::RationalFunctionCoefficient>(6), quantitativeResult3[0].evaluate(instantiation));
     
     formula = formulaParser.parseSingleFormulaFromString("R=? [F \"done\"]");
     
     result = checker.check(*formula);
     storm::modelchecker::ExplicitQuantitativeCheckResult<storm::RationalFunction>& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<storm::RationalFunction>();
     
-    EXPECT_EQ(storm::RationalNumber(11) / storm::RationalNumber(3), quantitativeResult4[0].evaluate(instantiation));
+    EXPECT_EQ(storm::utility::convertNumber<storm::RationalFunctionCoefficient>(11) / storm::utility::convertNumber<storm::RationalFunctionCoefficient>(3), quantitativeResult4[0].evaluate(instantiation));
 }
 #endif
 

src/test/modelchecker/SparseDtmcRegionModelCheckerTest.cpp

@@ -40,17 +40,17 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Prob) {
     EXPECT_FALSE(dtmcModelchecker->checkFormulaOnSamplingPoint(allVioRegion.getSomePoint()));
     
     EXPECT_NEAR(0.8369631407, dtmcModelchecker->getReachabilityValue(allSatRegion.getLowerBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
-    EXPECT_NEAR(0.8369631407, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getLowerBoundaries())),  storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+    EXPECT_NEAR(0.8369631407, storm::utility::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getLowerBoundaries())),  storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
     EXPECT_NEAR(0.0476784174, dtmcModelchecker->getReachabilityValue(allSatRegion.getUpperBoundaries()),  storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
-    EXPECT_NEAR(0.0476784174, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getUpperBoundaries())),  storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+    EXPECT_NEAR(0.0476784174, storm::utility::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getUpperBoundaries())),  storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
     EXPECT_NEAR(0.9987948367, dtmcModelchecker->getReachabilityValue(exBothRegion.getLowerBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
-    EXPECT_NEAR(0.9987948367, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(exBothRegion.getLowerBoundaries())),  storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+    EXPECT_NEAR(0.9987948367, storm::utility::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(exBothRegion.getLowerBoundaries())),  storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
     EXPECT_NEAR(0.6020480995, dtmcModelchecker->getReachabilityValue(exBothRegion.getUpperBoundaries()),  storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
-    EXPECT_NEAR(0.6020480995, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(exBothRegion.getUpperBoundaries())),  storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+    EXPECT_NEAR(0.6020480995, storm::utility::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(exBothRegion.getUpperBoundaries())),  storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
     EXPECT_NEAR(1.0000000000, dtmcModelchecker->getReachabilityValue(allVioRegion.getLowerBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
-    EXPECT_NEAR(1.0000000000, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getLowerBoundaries())),  storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+    EXPECT_NEAR(1.0000000000, storm::utility::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getLowerBoundaries())),  storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
     EXPECT_NEAR(0.8429289733, dtmcModelchecker->getReachabilityValue(allVioRegion.getUpperBoundaries()),  storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
-    EXPECT_NEAR(0.8429289733, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getUpperBoundaries())),  storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+    EXPECT_NEAR(0.8429289733, storm::utility::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getUpperBoundaries())),  storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
     
     //test approximative method
     settings = storm::modelchecker::region::SparseRegionModelCheckerSettings(storm::settings::modules::RegionSettings::SampleMode::INSTANTIATE, storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST,  storm::settings::modules::RegionSettings::SmtMode::OFF);
@@ -111,21 +111,21 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Rew) {
     EXPECT_FALSE(dtmcModelchecker->checkFormulaOnSamplingPoint(allVioRegion.getSomePoint()));
     
     EXPECT_NEAR(4.367791292, dtmcModelchecker->getReachabilityValue(allSatRegion.getLowerBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
-    EXPECT_NEAR(4.367791292, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getLowerBoundaries())),  storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+    EXPECT_NEAR(4.367791292, storm::utility::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getLowerBoundaries())),  storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
     EXPECT_NEAR(3.044795147, dtmcModelchecker->getReachabilityValue(allSatRegion.getUpperBoundaries()),  storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
-    EXPECT_NEAR(3.044795147, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getUpperBoundaries())),  storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+    EXPECT_NEAR(3.044795147, storm::utility::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getUpperBoundaries())),  storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
     EXPECT_NEAR(3.182535759, dtmcModelchecker->getReachabilityValue(exBothRegion.getLowerBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
-    EXPECT_NEAR(3.182535759, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(exBothRegion.getLowerBoundaries())),  storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+    EXPECT_NEAR(3.182535759, storm::utility::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(exBothRegion.getLowerBoundaries())),  storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
     EXPECT_NEAR(2.609602197, dtmcModelchecker->getReachabilityValue(exBothRegion.getUpperBoundaries()),  storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
-    EXPECT_NEAR(2.609602197, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(exBothRegion.getUpperBoundaries())),  storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+    EXPECT_NEAR(2.609602197, storm::utility::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(exBothRegion.getUpperBoundaries())),  storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
     EXPECT_NEAR(1.842551039, dtmcModelchecker->getReachabilityValue(exBothHardRegion.getLowerBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
-    EXPECT_NEAR(1.842551039, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(exBothHardRegion.getLowerBoundaries())),  storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+    EXPECT_NEAR(1.842551039, storm::utility::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(exBothHardRegion.getLowerBoundaries())),  storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
     EXPECT_NEAR(2.453500364, dtmcModelchecker->getReachabilityValue(exBothHardRegion.getUpperBoundaries()),  storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
-    EXPECT_NEAR(2.453500364, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(exBothHardRegion.getUpperBoundaries())),  storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+    EXPECT_NEAR(2.453500364, storm::utility::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(exBothHardRegion.getUpperBoundaries())),  storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
     EXPECT_NEAR(0.6721974438, dtmcModelchecker->getReachabilityValue(allVioRegion.getLowerBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
-    EXPECT_NEAR(0.6721974438, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getLowerBoundaries())),  storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+    EXPECT_NEAR(0.6721974438, storm::utility::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getLowerBoundaries())),  storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
     EXPECT_NEAR(1.308324558, dtmcModelchecker->getReachabilityValue(allVioRegion.getUpperBoundaries()),  storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
-    EXPECT_NEAR(1.308324558, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getUpperBoundaries())),  storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+    EXPECT_NEAR(1.308324558, storm::utility::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getUpperBoundaries())),  storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
     
     //test approximative method
     settings = storm::modelchecker::region::SparseRegionModelCheckerSettings(storm::settings::modules::RegionSettings::SampleMode::INSTANTIATE, storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST,  storm::settings::modules::RegionSettings::SmtMode::OFF);
@@ -243,11 +243,11 @@ TEST(SparseDtmcRegionModelCheckerTest, DISABLED_Brp_Rew_4Par) {
     EXPECT_FALSE(dtmcModelchecker->checkFormulaOnSamplingPoint(allVioRegion.getSomePoint()));
     
     EXPECT_NEAR(4.834779705, dtmcModelchecker->getReachabilityValue(allSatRegion.getLowerBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
-    EXPECT_NEAR(4.834779705, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getLowerBoundaries())),  storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+    EXPECT_NEAR(4.834779705, storm::utility::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getLowerBoundaries())),  storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
     EXPECT_NEAR(4.674651623, dtmcModelchecker->getReachabilityValue(exBothRegion.getUpperBoundaries()),  storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
-    EXPECT_NEAR(4.674651623, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(exBothRegion.getUpperBoundaries())),  storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+    EXPECT_NEAR(4.674651623, storm::utility::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(exBothRegion.getUpperBoundaries())),  storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
     EXPECT_NEAR(0.4467496536, dtmcModelchecker->getReachabilityValue(allVioRegion.getLowerBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
-    EXPECT_NEAR(0.4467496536, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getLowerBoundaries())),  storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+    EXPECT_NEAR(0.4467496536, storm::utility::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getLowerBoundaries())),  storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
     
     //test approximative method
     settings = storm::modelchecker::region::SparseRegionModelCheckerSettings(storm::settings::modules::RegionSettings::SampleMode::INSTANTIATE, storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST,  storm::settings::modules::RegionSettings::SmtMode::OFF);
@@ -308,17 +308,17 @@ TEST(SparseDtmcRegionModelCheckerTest, Crowds_Prob) {
     EXPECT_FALSE(dtmcModelchecker->checkFormulaOnSamplingPoint(allVioHardRegion.getSomePoint()));
     
     EXPECT_NEAR(0.1734086422, dtmcModelchecker->getReachabilityValue(allSatRegion.getLowerBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
-    EXPECT_NEAR(0.1734086422, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getLowerBoundaries())),  storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+    EXPECT_NEAR(0.1734086422, storm::utility::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getLowerBoundaries())),  storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
     EXPECT_NEAR(0.47178, dtmcModelchecker->getReachabilityValue(allSatRegion.getUpperBoundaries()),  storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
-    EXPECT_NEAR(0.47178, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getUpperBoundaries())),  storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+    EXPECT_NEAR(0.47178, storm::utility::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getUpperBoundaries())),  storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
     EXPECT_NEAR(0.7085157883, dtmcModelchecker->getReachabilityValue(exBothRegion.getUpperBoundaries()),  storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
-    EXPECT_NEAR(0.7085157883, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(exBothRegion.getUpperBoundaries())),  storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+    EXPECT_NEAR(0.7085157883, storm::utility::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(exBothRegion.getUpperBoundaries())),  storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
     EXPECT_NEAR(0.5095205203, dtmcModelchecker->getReachabilityValue(allVioRegion.getLowerBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
-    EXPECT_NEAR(0.5095205203, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getLowerBoundaries())),  storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+    EXPECT_NEAR(0.5095205203, storm::utility::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getLowerBoundaries())),  storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
     EXPECT_NEAR(0.6819701472, dtmcModelchecker->getReachabilityValue(allVioRegion.getUpperBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
-    EXPECT_NEAR(0.6819701472, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getUpperBoundaries())),  storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+    EXPECT_NEAR(0.6819701472, storm::utility::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getUpperBoundaries())),  storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
     EXPECT_NEAR(0.999895897, dtmcModelchecker->getReachabilityValue(allVioHardRegion.getUpperBoundaries()),  storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
-    EXPECT_NEAR(0.999895897, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allVioHardRegion.getUpperBoundaries())),  storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+    EXPECT_NEAR(0.999895897, storm::utility::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allVioHardRegion.getUpperBoundaries())),  storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
     
     //test approximative method
     settings = storm::modelchecker::region::SparseRegionModelCheckerSettings(storm::settings::modules::RegionSettings::SampleMode::INSTANTIATE, storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST,  storm::settings::modules::RegionSettings::SmtMode::OFF);
@@ -399,13 +399,13 @@ TEST(SparseDtmcRegionModelCheckerTest, Crowds_Prob_1Par) {
     EXPECT_FALSE(dtmcModelchecker->checkFormulaOnSamplingPoint(allVioRegion.getSomePoint()));
     
     EXPECT_NEAR(0.8430128158, dtmcModelchecker->getReachabilityValue(allSatRegion.getUpperBoundaries()),  storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
-    EXPECT_NEAR(0.8430128158, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getUpperBoundaries())),  storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+    EXPECT_NEAR(0.8430128158, storm::utility::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getUpperBoundaries())),  storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
     EXPECT_NEAR(0.7731321947, dtmcModelchecker->getReachabilityValue(exBothRegion.getUpperBoundaries()),  storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
-    EXPECT_NEAR(0.7731321947, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(exBothRegion.getUpperBoundaries())),  storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+    EXPECT_NEAR(0.7731321947, storm::utility::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(exBothRegion.getUpperBoundaries())),  storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
     EXPECT_NEAR(0.4732302663, dtmcModelchecker->getReachabilityValue(allVioRegion.getLowerBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
-    EXPECT_NEAR(0.4732302663, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getLowerBoundaries())),  storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+    EXPECT_NEAR(0.4732302663, storm::utility::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getLowerBoundaries())),  storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
     EXPECT_NEAR(0.7085157883, dtmcModelchecker->getReachabilityValue(allVioRegion.getUpperBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
-    EXPECT_NEAR(0.7085157883, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getUpperBoundaries())),  storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+    EXPECT_NEAR(0.7085157883, storm::utility::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getUpperBoundaries())),  storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
     
     //test approximative method
     settings = storm::modelchecker::region::SparseRegionModelCheckerSettings(storm::settings::modules::RegionSettings::SampleMode::INSTANTIATE, storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST,  storm::settings::modules::RegionSettings::SmtMode::OFF);
@@ -462,9 +462,9 @@ TEST(SparseDtmcRegionModelCheckerTest, Crowds_Prob_Const) {
     EXPECT_TRUE(dtmcModelchecker->checkFormulaOnSamplingPoint(allSatRegion.getSomePoint()));
     
     EXPECT_NEAR(0.6119660237, dtmcModelchecker->getReachabilityValue(allSatRegion.getUpperBoundaries()),  storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
-    EXPECT_NEAR(0.6119660237, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getUpperBoundaries())),  storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+    EXPECT_NEAR(0.6119660237, storm::utility::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getUpperBoundaries())),  storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
     EXPECT_NEAR(0.6119660237, dtmcModelchecker->getReachabilityValue(allSatRegion.getLowerBoundaries()),  storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
-    EXPECT_NEAR(0.6119660237, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getLowerBoundaries())),  storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+    EXPECT_NEAR(0.6119660237, storm::utility::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getLowerBoundaries())),  storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
     
     //test approximative method
     settings = storm::modelchecker::region::SparseRegionModelCheckerSettings(storm::settings::modules::RegionSettings::SampleMode::INSTANTIATE, storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST,  storm::settings::modules::RegionSettings::SmtMode::OFF);

src/test/storage/SylvanDdTest.cpp

@@ -442,8 +442,8 @@ TEST(SylvanDd, RationalFunctionConstants) {
 	carl::StringParser parser;
 	parser.setVariables({"x", "y", "z"});
 	
-	storm::RationalFunction partA = storm::RationalFunction(storm::Polynomial(parser.template parseMultivariatePolynomial<storm::RationalNumber>("2*x+x*y"), cache));
-	storm::RationalFunction partB = storm::RationalFunction(storm::Polynomial(parser.template parseMultivariatePolynomial<storm::RationalNumber>("z"), cache), storm::Polynomial(parser.template parseMultivariatePolynomial<storm::RationalNumber>("2*y"), cache));
+	storm::RationalFunction partA = storm::RationalFunction(storm::Polynomial(parser.template parseMultivariatePolynomial<storm::RationalFunctionCoefficient>("2*x+x*y"), cache));
+	storm::RationalFunction partB = storm::RationalFunction(storm::Polynomial(parser.template parseMultivariatePolynomial<storm::RationalFunctionCoefficient>("z"), cache), storm::Polynomial(parser.template parseMultivariatePolynomial<storm::RationalFunctionCoefficient>("2*y"), cache));
 
 	storm::RationalFunction rationalFunction = storm::RationalFunction(partA + partB);
 	
@@ -472,14 +472,14 @@ TEST(SylvanDd, RationalFunctionToDouble) {
 	storm::dd::Bdd<storm::dd::DdType::Sylvan> bddZ1 = manager->getEncoding(zExpr.first, 1);
 	
 	storm::dd::Add<storm::dd::DdType::Sylvan, storm::RationalFunction> complexAdd = 
-          ((bddX0 && (bddY0 && bddZ0)).template toAdd<storm::RationalFunction>() * manager->template getConstant<storm::RationalFunction>(storm::RationalFunction(storm::RationalNumber(-1))))
-		+ ((bddX0 && (bddY0 && bddZ1)).template toAdd<storm::RationalFunction>() * manager->template getConstant<storm::RationalFunction>(storm::RationalFunction(storm::RationalNumber(0))))
-		+ ((bddX0 && (bddY1 && bddZ0)).template toAdd<storm::RationalFunction>() * manager->template getConstant<storm::RationalFunction>(storm::RationalFunction(storm::RationalNumber(1) / storm::RationalNumber(2))))
-		+ ((bddX0 && (bddY1 && bddZ1)).template toAdd<storm::RationalFunction>() * manager->template getConstant<storm::RationalFunction>(storm::RationalFunction(storm::RationalNumber(1) / storm::RationalNumber(3))))
-		+ ((bddX1 && (bddY0 && bddZ0)).template toAdd<storm::RationalFunction>() * manager->template getConstant<storm::RationalFunction>(storm::RationalFunction(storm::RationalNumber(100000))))
-		+ ((bddX1 && (bddY0 && bddZ1)).template toAdd<storm::RationalFunction>() * manager->template getConstant<storm::RationalFunction>(storm::RationalFunction(storm::RationalNumber(3))))
-		+ ((bddX1 && (bddY1 && bddZ0)).template toAdd<storm::RationalFunction>() * manager->template getConstant<storm::RationalFunction>(storm::RationalFunction(storm::RationalNumber(4))))
-		+ ((bddX1 && (bddY1 && bddZ1)).template toAdd<storm::RationalFunction>() * manager->template getConstant<storm::RationalFunction>(storm::RationalFunction(storm::RationalNumber(0))));
+          ((bddX0 && (bddY0 && bddZ0)).template toAdd<storm::RationalFunction>() * manager->template getConstant<storm::RationalFunction>(storm::RationalFunction(storm::RationalFunctionCoefficient(-1))))
+		+ ((bddX0 && (bddY0 && bddZ1)).template toAdd<storm::RationalFunction>() * manager->template getConstant<storm::RationalFunction>(storm::RationalFunction(storm::RationalFunctionCoefficient(0))))
+		+ ((bddX0 && (bddY1 && bddZ0)).template toAdd<storm::RationalFunction>() * manager->template getConstant<storm::RationalFunction>(storm::RationalFunction(storm::RationalFunctionCoefficient(1) / storm::RationalFunctionCoefficient(2))))
+		+ ((bddX0 && (bddY1 && bddZ1)).template toAdd<storm::RationalFunction>() * manager->template getConstant<storm::RationalFunction>(storm::RationalFunction(storm::RationalFunctionCoefficient(1) / storm::RationalFunctionCoefficient(3))))
+		+ ((bddX1 && (bddY0 && bddZ0)).template toAdd<storm::RationalFunction>() * manager->template getConstant<storm::RationalFunction>(storm::RationalFunction(storm::RationalFunctionCoefficient(100000))))
+		+ ((bddX1 && (bddY0 && bddZ1)).template toAdd<storm::RationalFunction>() * manager->template getConstant<storm::RationalFunction>(storm::RationalFunction(storm::RationalFunctionCoefficient(3))))
+		+ ((bddX1 && (bddY1 && bddZ0)).template toAdd<storm::RationalFunction>() * manager->template getConstant<storm::RationalFunction>(storm::RationalFunction(storm::RationalFunctionCoefficient(4))))
+		+ ((bddX1 && (bddY1 && bddZ1)).template toAdd<storm::RationalFunction>() * manager->template getConstant<storm::RationalFunction>(storm::RationalFunction(storm::RationalFunctionCoefficient(0))));
 	EXPECT_EQ(6ul, complexAdd.getNonZeroCount());
     EXPECT_EQ(7ul, complexAdd.getLeafCount());
     EXPECT_EQ(14ul, complexAdd.getNodeCount());

src/test/utility/ModelInstantiatorTest.cpp

@@ -36,13 +36,13 @@ TEST(ModelInstantiatorTest, BrpProb) {
     EXPECT_FALSE(dtmc->hasRewardModel());
     
     {
-        std::map<storm::RationalFunctionVariable, storm::RationalNumber> valuation;
+        std::map<storm::RationalFunctionVariable, storm::RationalFunctionCoefficient> valuation;
         storm::RationalFunctionVariable const& pL = carl::VariablePool::getInstance().findVariableWithName("pL");
         ASSERT_NE(pL, carl::Variable::NO_VARIABLE);
         storm::RationalFunctionVariable const& pK = carl::VariablePool::getInstance().findVariableWithName("pK");
         ASSERT_NE(pK, carl::Variable::NO_VARIABLE);
-        valuation.insert(std::make_pair(pL,carl::rationalize<storm::RationalNumber>(0.8)));
-        valuation.insert(std::make_pair(pK,carl::rationalize<storm::RationalNumber>(0.9)));
+        valuation.insert(std::make_pair(pL, storm::utility::convertNumber<storm::RationalFunctionCoefficient>(0.8)));
+        valuation.insert(std::make_pair(pK, storm::utility::convertNumber<storm::RationalFunctionCoefficient>(0.9)));
 
         storm::models::sparse::Dtmc<double> const& instantiated(modelInstantiator.instantiate(valuation));
 
@@ -69,13 +69,13 @@ TEST(ModelInstantiatorTest, BrpProb) {
     }
     
     {
-        std::map<storm::RationalFunctionVariable, storm::RationalNumber> valuation;
+        std::map<storm::RationalFunctionVariable, storm::RationalFunctionCoefficient> valuation;
         storm::RationalFunctionVariable const& pL = carl::VariablePool::getInstance().findVariableWithName("pL");
         ASSERT_NE(pL, carl::Variable::NO_VARIABLE);
         storm::RationalFunctionVariable const& pK = carl::VariablePool::getInstance().findVariableWithName("pK");
         ASSERT_NE(pK, carl::Variable::NO_VARIABLE);
-        valuation.insert(std::make_pair(pL,carl::rationalize<storm::RationalNumber>(1.0)));
-        valuation.insert(std::make_pair(pK,carl::rationalize<storm::RationalNumber>(1.0)));
+        valuation.insert(std::make_pair(pL, storm::utility::one<storm::RationalFunctionCoefficient>()));
+        valuation.insert(std::make_pair(pK, storm::utility::one<storm::RationalFunctionCoefficient>()));
 
         storm::models::sparse::Dtmc<double> const& instantiated(modelInstantiator.instantiate(valuation));
 
@@ -102,13 +102,13 @@ TEST(ModelInstantiatorTest, BrpProb) {
     }
     
     {
-        std::map<storm::RationalFunctionVariable, storm::RationalNumber> valuation;
+        std::map<storm::RationalFunctionVariable, storm::RationalFunctionCoefficient> valuation;
         storm::RationalFunctionVariable const& pL = carl::VariablePool::getInstance().findVariableWithName("pL");
         ASSERT_NE(pL, carl::Variable::NO_VARIABLE);
         storm::RationalFunctionVariable const& pK = carl::VariablePool::getInstance().findVariableWithName("pK");
         ASSERT_NE(pK, carl::Variable::NO_VARIABLE);
-        valuation.insert(std::make_pair(pL,carl::rationalize<storm::RationalNumber>(1.0)));
-        valuation.insert(std::make_pair(pK,carl::rationalize<storm::RationalNumber>(0.9)));
+        valuation.insert(std::make_pair(pL, storm::utility::one<storm::RationalFunctionCoefficient>()));
+        valuation.insert(std::make_pair(pK, storm::utility::convertNumber<storm::RationalFunctionCoefficient>(0.9)));
 
         storm::models::sparse::Dtmc<double> const& instantiated(modelInstantiator.instantiate(valuation));
 
@@ -153,7 +153,7 @@ TEST(ModelInstantiatorTest, Brp_Rew) {
     storm::utility::ModelInstantiator<storm::models::sparse::Dtmc<storm::RationalFunction>, storm::models::sparse::Dtmc<double>> modelInstantiator(*dtmc);
     
     {
-        std::map<storm::RationalFunctionVariable, storm::RationalNumber> valuation;
+        std::map<storm::RationalFunctionVariable, storm::RationalFunctionCoefficient> valuation;
         storm::RationalFunctionVariable const& pL = carl::VariablePool::getInstance().findVariableWithName("pL");
         ASSERT_NE(pL, carl::Variable::NO_VARIABLE);
         storm::RationalFunctionVariable const& pK = carl::VariablePool::getInstance().findVariableWithName("pK");
@@ -162,10 +162,10 @@ TEST(ModelInstantiatorTest, Brp_Rew) {
         ASSERT_NE(pK, carl::Variable::NO_VARIABLE);
         storm::RationalFunctionVariable const& TOAck = carl::VariablePool::getInstance().findVariableWithName("TOAck");
         ASSERT_NE(pK, carl::Variable::NO_VARIABLE);
-        valuation.insert(std::make_pair(pL,carl::rationalize<storm::RationalNumber>(0.9)));
-        valuation.insert(std::make_pair(pK,carl::rationalize<storm::RationalNumber>(0.3)));
-        valuation.insert(std::make_pair(TOMsg,carl::rationalize<storm::RationalNumber>(0.3)));
-        valuation.insert(std::make_pair(TOAck,carl::rationalize<storm::RationalNumber>(0.5)));
+        valuation.insert(std::make_pair(pL, storm::utility::convertNumber<storm::RationalFunctionCoefficient>(0.9)));
+        valuation.insert(std::make_pair(pK, storm::utility::convertNumber<storm::RationalFunctionCoefficient>(0.3)));
+        valuation.insert(std::make_pair(TOMsg, storm::utility::convertNumber<storm::RationalFunctionCoefficient>(0.3)));
+        valuation.insert(std::make_pair(TOAck, storm::utility::convertNumber<storm::RationalFunctionCoefficient>(0.5)));
 
         storm::models::sparse::Dtmc<double> const& instantiated(modelInstantiator.instantiate(valuation));
 
@@ -222,13 +222,13 @@ TEST(ModelInstantiatorTest, Consensus) {
 
     storm::utility::ModelInstantiator<storm::models::sparse::Mdp<storm::RationalFunction>, storm::models::sparse::Mdp<double>> modelInstantiator(*mdp);
     
-    std::map<storm::RationalFunctionVariable, storm::RationalNumber> valuation;
+    std::map<storm::RationalFunctionVariable, storm::RationalFunctionCoefficient> valuation;
     storm::RationalFunctionVariable const& p1 = carl::VariablePool::getInstance().findVariableWithName("p1");
     ASSERT_NE(p1, carl::Variable::NO_VARIABLE);
     storm::RationalFunctionVariable const& p2 = carl::VariablePool::getInstance().findVariableWithName("p2");
     ASSERT_NE(p2, carl::Variable::NO_VARIABLE);
-    valuation.insert(std::make_pair(p1,carl::rationalize<storm::RationalNumber>(0.51)));
-    valuation.insert(std::make_pair(p2,carl::rationalize<storm::RationalNumber>(0.49)));
+    valuation.insert(std::make_pair(p1, storm::utility::convertNumber<storm::RationalFunctionCoefficient>(0.51)));
+    valuation.insert(std::make_pair(p2, storm::utility::convertNumber<storm::RationalFunctionCoefficient>(0.49)));
     storm::models::sparse::Mdp<double> const& instantiated(modelInstantiator.instantiate(valuation));
 
     ASSERT_EQ(mdp->getTransitionMatrix().getRowGroupIndices(), instantiated.getTransitionMatrix().getRowGroupIndices());