From f342ce3287f8b2aacb6fd9149fe24a548b1a2ca3 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Mon, 15 Aug 2016 20:29:50 +0200
Subject: [PATCH] translation from expressions involving the power operator to
 rational functions/rational numbers is now possible

Former-commit-id: e0ce43ab35f88de46426b967c91b584e5adbe955
---
 src/storage/expressions/ToRationalFunctionVisitor.cpp |  6 ++++++
 src/utility/constants.cpp                             | 11 ++++++++++-
 2 files changed, 16 insertions(+), 1 deletion(-)

diff --git a/src/storage/expressions/ToRationalFunctionVisitor.cpp b/src/storage/expressions/ToRationalFunctionVisitor.cpp
index 60fecc08c..a219066e4 100644
--- a/src/storage/expressions/ToRationalFunctionVisitor.cpp
+++ b/src/storage/expressions/ToRationalFunctionVisitor.cpp
@@ -34,6 +34,7 @@ namespace storm {
         boost::any ToRationalFunctionVisitor<RationalFunctionType>::visit(BinaryNumericalFunctionExpression const& expression) {
             RationalFunctionType firstOperandAsRationalFunction = boost::any_cast<RationalFunctionType>(expression.getFirstOperand()->accept(*this));
             RationalFunctionType secondOperandAsRationalFunction = boost::any_cast<RationalFunctionType>(expression.getSecondOperand()->accept(*this));
+            uint_fast64_t exponentAsInteger = 0;
             switch(expression.getOperatorType()) {
                 case BinaryNumericalFunctionExpression::OperatorType::Plus:
                     return firstOperandAsRationalFunction + secondOperandAsRationalFunction;
@@ -47,6 +48,11 @@ namespace storm {
                 case BinaryNumericalFunctionExpression::OperatorType::Divide:
                     return firstOperandAsRationalFunction / secondOperandAsRationalFunction;
                     break;
+                case BinaryNumericalFunctionExpression::OperatorType::Power:
+                    STORM_LOG_THROW(storm::utility::isInteger(secondOperandAsRationalFunction), storm::exceptions::InvalidArgumentException, "Exponent of power operator must be a positive integer.");
+                    exponentAsInteger = storm::utility::convertNumber<uint_fast64_t>(secondOperandAsRationalFunction);
+                    return storm::utility::pow(firstOperandAsRationalFunction, exponentAsInteger);
+                    break;
                 default:
                     STORM_LOG_ASSERT(false, "Illegal operator type.");
             }
diff --git a/src/utility/constants.cpp b/src/utility/constants.cpp
index 2630ed285..6d954722a 100644
--- a/src/utility/constants.cpp
+++ b/src/utility/constants.cpp
@@ -115,6 +115,10 @@ namespace storm {
             return carl::isInteger(number);
         }
 
+        template<>
+        bool isInteger(storm::RationalFunction const& func) {
+            return storm::utility::isConstant(func) && storm::utility::isOne(func.denominator());
+        }
 #endif
         
         template<typename ValueType>
@@ -203,7 +207,12 @@ namespace storm {
         RationalFunction convertNumber(RationalNumber const& number) {
             return RationalFunction(number);
         }
-        
+
+        template<>
+        uint_fast64_t convertNumber(RationalFunction const& func) {
+            return carl::toInt<unsigned long>(func.nominatorAsNumber());
+        }
+
         template<>
         RationalNumber abs(storm::RationalNumber const& number) {
             return carl::abs(number);