translation from expressions involving the power operator to rational functions/rational numbers is now possible

Former-commit-id: e0ce43ab35

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.");
             }

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);