Support conversion in function parametric::evaluate

src/storm-dft/transformations/DftInstantiator.h

@@ -48,7 +48,7 @@ class DftInstantiator {
     template<typename PT = ParametricType>
     typename std::enable_if<!std::is_same<PT, ConstantType>::value, ConstantType>::type instantiate_helper(
         ParametricType const& function, storm::utility::parametric::Valuation<ParametricType> const& valuation) {
-        return storm::utility::convertNumber<ConstantType>(storm::utility::parametric::evaluate(function, valuation));
+        return storm::utility::parametric::evaluate<ConstantType>(function, valuation);
     }
 
     /*!

src/storm-pars/derivative/SparseDerivativeInstantiationModelChecker.cpp

@@ -63,10 +63,10 @@ std::unique_ptr<modelchecker::ExplicitQuantitativeCheckResult<ConstantType>> Spa
 
     // Write results into the placeholders
     for (auto& functionResult : this->functionsUnderived) {
-        functionResult.second = storm::utility::convertNumber<ConstantType>(storm::utility::parametric::evaluate(functionResult.first, valuation));
+        functionResult.second = storm::utility::parametric::evaluate<ConstantType>(functionResult.first, valuation);
     }
     for (auto& functionResult : this->functionsDerived.at(parameter)) {
-        functionResult.second = storm::utility::convertNumber<ConstantType>(storm::utility::parametric::evaluate(functionResult.first, valuation));
+        functionResult.second = storm::utility::parametric::evaluate<ConstantType>(functionResult.first, valuation);
     }
 
     auto deltaConstrainedMatrixInstantiated = deltaConstrainedMatricesInstantiated->at(parameter);
@@ -81,7 +81,7 @@ std::unique_ptr<modelchecker::ExplicitQuantitativeCheckResult<ConstantType>> Spa
 
     std::vector<ConstantType> instantiatedDerivedOutputVec(derivedOutputVecs->at(parameter).size());
     for (uint_fast64_t i = 0; i < derivedOutputVecs->at(parameter).size(); i++) {
-        instantiatedDerivedOutputVec[i] = utility::convertNumber<ConstantType>(derivedOutputVecs->at(parameter)[i].evaluate(valuation));
+        instantiatedDerivedOutputVec[i] = storm::utility::parametric::evaluate<ConstantType>(derivedOutputVecs->at(parameter)[i], valuation);
     }
 
     instantiationWatch.stop();

src/storm-pars/transformer/ParameterLifter.cpp

@@ -355,9 +355,9 @@ void ParameterLifter<ParametricType, ConstantType>::FunctionValuationCollector::
         ConstantType& placeholder = collectedFunctionValuationPlaceholder.second;
         auto concreteValuations = abstrValuation.getConcreteValuations(region);
         auto concreteValuationIt = concreteValuations.begin();
-        placeholder = storm::utility::convertNumber<ConstantType>(storm::utility::parametric::evaluate(function, *concreteValuationIt));
+        placeholder = storm::utility::parametric::evaluate<ConstantType>(function, *concreteValuationIt);
         for (++concreteValuationIt; concreteValuationIt != concreteValuations.end(); ++concreteValuationIt) {
-            ConstantType currentResult = storm::utility::convertNumber<ConstantType>(storm::utility::parametric::evaluate(function, *concreteValuationIt));
+            ConstantType currentResult = storm::utility::parametric::evaluate<ConstantType>(function, *concreteValuationIt);
             if (storm::solver::minimize(dirForUnspecifiedParameters)) {
                 placeholder = std::min(placeholder, currentResult);
             } else {

src/storm-pars/utility/ModelInstantiator.h

@@ -125,7 +125,7 @@ class ModelInstantiator {
     typename std::enable_if<!std::is_same<PMT, ConstantSparseModelType>::value>::type instantiate_helper(
         storm::utility::parametric::Valuation<ParametricType> const& valuation) {
         for (auto& functionResult : this->functions) {
-            functionResult.second = storm::utility::convertNumber<ConstantType>(storm::utility::parametric::evaluate(functionResult.first, valuation));
+            functionResult.second = storm::utility::parametric::evaluate<ConstantType>(functionResult.first, valuation);
         }
     }
 

src/storm-pars/utility/parametric.cpp

@@ -4,20 +4,12 @@
 #include "storm/adapters/RationalFunctionAdapter.h"
 #include "storm/exceptions/IllegalArgumentException.h"
 #include "storm/exceptions/NotImplementedException.h"
-#include "storm/utility/constants.h"
 #include "storm/utility/macros.h"
 
 namespace storm {
 namespace utility {
 namespace parametric {
 
-#ifdef STORM_HAVE_CARL
-template<>
-typename CoefficientType<storm::RationalFunction>::type evaluate<storm::RationalFunction>(storm::RationalFunction const& function,
-                                                                                          Valuation<storm::RationalFunction> const& valuation) {
-    return function.evaluate(valuation);
-}
-
 template<>
 typename storm::RationalFunction substitute<storm::RationalFunction>(storm::RationalFunction const& function,
                                                                      Valuation<storm::RationalFunction> const& valuation) {
@@ -48,7 +40,6 @@ bool isMultiLinearPolynomial<storm::RationalFunction>(storm::RationalFunction co
     }
     return true;
 }
-#endif
 }  // namespace parametric
 }  // namespace utility
 }  // namespace storm

src/storm-pars/utility/parametric.h

@@ -1,7 +1,7 @@
-#ifndef STORM_UTILITY_PARAMETRIC_H
-#define STORM_UTILITY_PARAMETRIC_H
+#pragma once
 
 #include "storm/adapters/RationalFunctionForward.h"
+#include "storm/utility/constants.h"
 
 #include <map>
 #include <set>
@@ -26,7 +26,6 @@ struct CoefficientType {
     typedef void type;
 };
 
-#ifdef STORM_HAVE_CARL
 template<>
 struct VariableType<storm::RationalFunction> {
     typedef storm::RationalFunctionVariable type;
@@ -35,16 +34,21 @@ template<>
 struct CoefficientType<storm::RationalFunction> {
     typedef storm::RationalFunctionCoefficient type;
 };
-#endif
 
 template<typename FunctionType>
 using Valuation = std::map<typename VariableType<FunctionType>::type, typename CoefficientType<FunctionType>::type>;
 
 /*!
- * Evaluates the given function wrt. the given valuation
+ * Evaluates the given function wrt. the given valuation and returns the required type.
  */
-template<typename FunctionType>
-typename CoefficientType<FunctionType>::type evaluate(FunctionType const& function, Valuation<FunctionType> const& valuation);
+template<typename ReturnType, typename FunctionType>
+ReturnType evaluate(FunctionType const& function, Valuation<FunctionType> const& valuation) {
+    if constexpr (std::is_same<ReturnType, typename CoefficientType<FunctionType>::type>::value) {
+        return function.evaluate(valuation);
+    } else {
+        return storm::utility::convertNumber<ReturnType>(function.evaluate(valuation));
+    }
+}
 
 /*!
  * Evaluates the given function wrt. the given valuation
@@ -71,8 +75,5 @@ template<typename FunctionType>
 bool isMultiLinearPolynomial(FunctionType const& function);
 
 }  // namespace parametric
-
 }  // namespace utility
 }  // namespace storm
-
-#endif /* STORM_UTILITY_PARAMETRIC_H */

src/test/storm-pars/derivative/SparseDerivativeInstantiationModelCheckerTest.cpp

@@ -2,6 +2,11 @@
 #include "storm-config.h"
 #include "test/storm_gtest.h"
 
+#include "storm-pars/analysis/OrderExtender.h"
+#include "storm-pars/api/storm-pars.h"
+#include "storm-pars/derivative/SparseDerivativeInstantiationModelChecker.h"
+#include "storm-pars/transformer/SparseParametricDtmcSimplifier.h"
+#include "storm-parsers/api/storm-parsers.h"
 #include "storm/adapters/RationalFunctionAdapter.h"
 #include "storm/api/builder.h"
 #include "storm/api/storm.h"
@@ -17,13 +22,6 @@
 #include "storm/storage/expressions/BinaryRelationExpression.h"
 #include "storm/storage/expressions/ExpressionManager.h"
 
-#include "storm-parsers/api/storm-parsers.h"
-
-#include "storm-pars/analysis/OrderExtender.h"
-#include "storm-pars/api/storm-pars.h"
-#include "storm-pars/derivative/SparseDerivativeInstantiationModelChecker.h"
-#include "storm-pars/transformer/SparseParametricDtmcSimplifier.h"
-
 namespace {
 class RationalGmmxxEnvironment {
    public:
@@ -143,9 +141,7 @@ void SparseDerivativeInstantiationModelCheckerTest<TestType>::testModel(std::sha
         for (auto const& entry : instantiation) {
             auto parameter = entry.first;
             auto derivativeWrtParameter = derivatives[parameter];
-            typename TestType::ConstantType evaluatedDerivative =
-                storm::utility::convertNumber<typename TestType::ConstantType>(derivativeWrtParameter.evaluate(instantiation));
-            resultMap[parameter] = evaluatedDerivative;
+            resultMap[parameter] = storm::utility::parametric::evaluate<typename TestType::ConstantType>(derivativeWrtParameter, instantiation);
         }
         testCases[instantiation] = resultMap;
     }

src/test/storm-pars/modelchecker/SymbolicParametricDtmcPrctlModelCheckerTest.cpp

@@ -1,9 +1,11 @@
 #include "storm-config.h"
 #include "test/storm_gtest.h"
 
+#include "storm-pars/utility/parametric.h"
 #include "storm-parsers/parser/FormulaParser.h"
 #include "storm-parsers/parser/PrismParser.h"
 #include "storm/builder/DdPrismModelBuilder.h"
+#include "storm/environment/solver/SolverEnvironment.h"
 #include "storm/logic/Formulas.h"
 #include "storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h"
 #include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h"
@@ -15,8 +17,6 @@
 #include "storm/storage/SymbolicModelDescription.h"
 #include "storm/utility/solver.h"
 
-#include "storm/environment/solver/SolverEnvironment.h"
-
 TEST(SymbolicDtmcPrctlModelCheckerTest, Die_RationalFunction_Sylvan) {
     storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/pdtmc/parametric_die.pm");
     storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
@@ -51,7 +51,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Die_RationalFunction_Sylvan) {
     storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, storm::RationalFunction>& quantitativeResult1 =
         result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, storm::RationalFunction>();
 
-    EXPECT_EQ(storm::utility::convertNumber<storm::RationalFunctionCoefficient>(quantitativeResult1.sum().evaluate(instantiation)),
+    EXPECT_EQ(storm::utility::parametric::evaluate<storm::RationalFunctionCoefficient>(quantitativeResult1.sum(), instantiation),
               storm::utility::convertNumber<storm::RationalFunctionCoefficient>(std::string("1/6")));
 
     formula = formulaParser.parseSingleFormulaFromString("P=? [F \"two\"]");
@@ -61,7 +61,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Die_RationalFunction_Sylvan) {
     storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, storm::RationalFunction>& quantitativeResult2 =
         result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, storm::RationalFunction>();
 
-    EXPECT_EQ(storm::utility::convertNumber<storm::RationalFunctionCoefficient>(quantitativeResult2.sum().evaluate(instantiation)),
+    EXPECT_EQ(storm::utility::parametric::evaluate<storm::RationalFunctionCoefficient>(quantitativeResult2.sum(), instantiation),
               storm::utility::convertNumber<storm::RationalFunctionCoefficient>(std::string("1/6")));
 
     formula = formulaParser.parseSingleFormulaFromString("P=? [F \"three\"]");
@@ -71,7 +71,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Die_RationalFunction_Sylvan) {
     storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, storm::RationalFunction>& quantitativeResult3 =
         result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, storm::RationalFunction>();
 
-    EXPECT_EQ(storm::utility::convertNumber<storm::RationalFunctionCoefficient>(quantitativeResult3.sum().evaluate(instantiation)),
+    EXPECT_EQ(storm::utility::parametric::evaluate<storm::RationalFunctionCoefficient>(quantitativeResult3.sum(), instantiation),
               storm::utility::convertNumber<storm::RationalFunctionCoefficient>(std::string("1/6")));
 
     formula = formulaParser.parseSingleFormulaFromString("R=? [F \"done\"]");
@@ -81,6 +81,6 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Die_RationalFunction_Sylvan) {
     storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, storm::RationalFunction>& quantitativeResult4 =
         result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, storm::RationalFunction>();
 
-    EXPECT_EQ(storm::utility::convertNumber<storm::RationalFunctionCoefficient>(quantitativeResult4.sum().evaluate(instantiation)),
+    EXPECT_EQ(storm::utility::parametric::evaluate<storm::RationalFunctionCoefficient>(quantitativeResult4.sum(), instantiation),
               storm::utility::convertNumber<storm::RationalFunctionCoefficient>(std::string("11/3")));
 }