From 69c5ba604e388caef9644063e09a5c0a1063c2c5 Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@web.de>
Date: Wed, 9 Mar 2016 13:29:26 +0100
Subject: [PATCH] Helper functions for parametric stuff

Former-commit-id: 288e4de3da6b1deb13fd4e758dbc2b557f375ab1
---
 src/utility/constants.cpp  | 19 ++++++++++++--
 src/utility/constants.h    |  3 +++
 src/utility/parametric.cpp | 39 +++++++++++++++++++++++++++
 src/utility/parametric.h   | 54 ++++++++++++++++++++++++++++++++++++++
 4 files changed, 113 insertions(+), 2 deletions(-)
 create mode 100644 src/utility/parametric.cpp
 create mode 100644 src/utility/parametric.h

diff --git a/src/utility/constants.cpp b/src/utility/constants.cpp
index 900482a72..2aa10d23a 100644
--- a/src/utility/constants.cpp
+++ b/src/utility/constants.cpp
@@ -39,6 +39,7 @@ namespace storm {
         bool isConstant(ValueType const& a) {
             return true;
         }
+
         
 #ifdef STORM_HAVE_CARL
         template<>
@@ -85,11 +86,11 @@ namespace storm {
 
 		template<typename ValueType>
 		ValueType simplify(ValueType value) {
-            // In the general case, we don't to anything here, but merely return the value. If something else is
+            // In the general case, we don't do anything here, but merely return the value. If something else is
             // supposed to happen here, the templated function can be specialized for this particular type.
 			return value;
 		}
-
+        
 #ifdef STORM_HAVE_CARL
         template<>
         RationalFunction& simplify(RationalFunction& value);
@@ -119,6 +120,17 @@ namespace storm {
             value.simplify();
             return std::move(value);
         }
+        
+        template<>
+        double convertNumber(RationalNumber const& number){
+            return carl::toDouble(number);
+        }
+        
+        template<>
+        RationalNumber convertNumber(double const& number){
+            return carl::rationalize<RationalNumber>(number);
+        }
+
 #endif
         
         template<typename IndexType, typename ValueType>
@@ -221,6 +233,9 @@ namespace storm {
         template RationalFunction& simplify(RationalFunction& value);
         template RationalFunction&& simplify(RationalFunction&& value);
         
+        template double convertNumber(RationalNumber const& number);
+        template RationalNumber convertNumber(double const& number);
+        
         template bool isOne(Interval const& value);
         template bool isZero(Interval const& value);
         template bool isConstant(Interval const& value);
diff --git a/src/utility/constants.h b/src/utility/constants.h
index 8f6d8149e..80222b74f 100644
--- a/src/utility/constants.h
+++ b/src/utility/constants.h
@@ -50,6 +50,9 @@ namespace storm {
 
         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);
     }
 }
 
diff --git a/src/utility/parametric.cpp b/src/utility/parametric.cpp
new file mode 100644
index 000000000..c45882c42
--- /dev/null
+++ b/src/utility/parametric.cpp
@@ -0,0 +1,39 @@
+/* 
+ * File:   parametric.cpp
+ * Author: Tim Quatmann
+ * 
+ * Created by Tim Quatmann on 08/03/16.
+ */
+
+#include <string>
+
+#include "src/utility/parametric.h"
+#include "src/utility/constants.h"
+#include "src/utility/macros.h"
+#include "src/settings/SettingsManager.h"
+#include "src/exceptions/IllegalArgumentException.h"
+#include "src/exceptions/NotImplementedException.h"
+
+#ifdef STORM_HAVE_CARL
+#include<carl/numbers/numbers.h>
+#include<carl/core/VariablePool.h>
+#endif
+
+namespace storm {
+    namespace utility{
+        namespace parametric {
+            
+#ifdef STORM_HAVE_CARL
+            template<>
+            typename CoefficientType<storm::RationalFunction>::type evaluate<storm::RationalFunction>(storm::RationalFunction const& function, std::map<typename VariableType<storm::RationalFunction>::type, typename CoefficientType<storm::RationalFunction>::type> const& valuation){
+                return function.evaluate(valuation);
+            }
+            
+            template<>
+            typename CoefficientType<storm::RationalFunction>::type getConstantPart<storm::RationalFunction>(storm::RationalFunction const& function){
+                return function.constantPart();
+            }
+#endif
+        }
+    }
+}
diff --git a/src/utility/parametric.h b/src/utility/parametric.h
new file mode 100644
index 000000000..2ebf1e18c
--- /dev/null
+++ b/src/utility/parametric.h
@@ -0,0 +1,54 @@
+//
+//  parametric.h
+//
+//  Created by Tim Quatmann on 08/03/16.
+//
+//
+
+#ifndef STORM_UTILITY_PARAMETRIC_H
+#define STORM_UTILITY_PARAMETRIC_H
+
+#include "src/adapters/CarlAdapter.h"
+
+
+namespace storm {
+    namespace utility {
+        namespace parametric {
+            
+            /*!
+             * Access the type of variables from a given function type
+             */
+            template<typename FunctionType>
+            struct VariableType { typedef void type; };
+            /*!
+             * Acess the type of coefficients from a given function type
+             */
+            template<typename FunctionType>
+            struct CoefficientType { typedef void type; };
+            
+#ifdef STORM_HAVE_CARL
+            template<>
+            struct VariableType<storm::RationalFunction> { typedef storm::Variable type; };
+            template<>
+            struct CoefficientType<storm::RationalFunction> { typedef storm::RationalNumber type; };
+#endif
+            
+            /*!
+             * Evaluates the given function wrt. the given valuation
+             */
+            template<typename FunctionType>
+            typename CoefficientType<FunctionType>::type evaluate(FunctionType const& function, std::map<typename VariableType<FunctionType>::type, typename CoefficientType<FunctionType>::type> const& valuation);
+            
+            /*!
+             * Retrieves the constant part of the given function.
+             */
+            template<typename FunctionType>
+            typename CoefficientType<FunctionType>::type getConstantPart(FunctionType const& function);
+
+        }
+        
+    }
+}
+
+
+#endif /* STORM_UTILITY_PARAMETRIC_H */