Add support for ITE expression in the likelihood part of commands (exact, parametric engine)

Support the conversion to rational numbers / rational functions for ITE expressions. Example:

 ... ->  (s<4 ? p : q):(s'=...)

where s is a state variable and p, q are constants or parameters.

src/storm/storage/expressions/ExpressionEvaluator.cpp

@@ -33,7 +33,7 @@ namespace storm {
         }
 
 #ifdef STORM_HAVE_CARL
-        ExpressionEvaluator<RationalNumber>::ExpressionEvaluator(storm::expressions::ExpressionManager const& manager) : ExprtkExpressionEvaluatorBase<RationalNumber>(manager) {
+        ExpressionEvaluator<RationalNumber>::ExpressionEvaluator(storm::expressions::ExpressionManager const& manager) : ExprtkExpressionEvaluatorBase<RationalNumber>(manager), rationalNumberVisitor(*this) {
             // Intentionally left empty.
         }
 
@@ -57,7 +57,7 @@ namespace storm {
             return this->rationalNumberVisitor.toRationalNumber(expression);
         }
         
-        ExpressionEvaluator<RationalFunction>::ExpressionEvaluator(storm::expressions::ExpressionManager const& manager) : ExprtkExpressionEvaluatorBase<RationalFunction>(manager) {
+        ExpressionEvaluator<RationalFunction>::ExpressionEvaluator(storm::expressions::ExpressionManager const& manager) : ExprtkExpressionEvaluatorBase<RationalFunction>(manager), rationalFunctionVisitor(*this) {
             // Intentionally left empty.
         }
         

src/storm/storage/expressions/ToRationalFunctionVisitor.cpp

@@ -11,7 +11,7 @@ namespace storm {
 
 #ifdef STORM_HAVE_CARL
         template<typename RationalFunctionType>
-        ToRationalFunctionVisitor<RationalFunctionType>::ToRationalFunctionVisitor() : ExpressionVisitor(), cache(new carl::Cache<carl::PolynomialFactorizationPair<RawPolynomial>>()) {
+        ToRationalFunctionVisitor<RationalFunctionType>::ToRationalFunctionVisitor(ExpressionEvaluatorBase<RationalFunctionType> const& evaluator) : ExpressionVisitor(), cache(new carl::Cache<carl::PolynomialFactorizationPair<RawPolynomial>>()), evaluator(evaluator) {
             // Intentionally left empty.
         }
         
@@ -21,8 +21,13 @@ namespace storm {
         }
         
         template<typename RationalFunctionType>
-        boost::any ToRationalFunctionVisitor<RationalFunctionType>::visit(IfThenElseExpression const&, boost::any const&) {
-            STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational function.");
+        boost::any ToRationalFunctionVisitor<RationalFunctionType>::visit(IfThenElseExpression const& expression, boost::any const& data) {
+            bool conditionValue = evaluator.asBool(expression.getCondition());
+            if (conditionValue) {
+                return expression.getThenExpression()->accept(*this, data);
+            } else {
+                return expression.getElseExpression()->accept(*this, data);
+            }
         }
         
         template<typename RationalFunctionType>

src/storm/storage/expressions/ToRationalFunctionVisitor.h

@@ -8,6 +8,7 @@
 #include "storm/storage/expressions/Expression.h"
 #include "storm/storage/expressions/Expressions.h"
 #include "storm/storage/expressions/ExpressionVisitor.h"
+#include "storm/storage/expressions/ExpressionEvaluatorBase.h"
 #include "storm/storage/expressions/Variable.h"
 
 namespace storm {
@@ -17,7 +18,7 @@ namespace storm {
         template<typename RationalFunctionType>
         class ToRationalFunctionVisitor : public ExpressionVisitor {
         public:
-            ToRationalFunctionVisitor();
+            ToRationalFunctionVisitor(ExpressionEvaluatorBase<RationalFunctionType> const& evaluator);
             
             RationalFunctionType toRationalFunction(Expression const& expression);
             
@@ -53,6 +54,9 @@ namespace storm {
             
             // A mapping from variables to their values.
             std::unordered_map<storm::expressions::Variable, RationalFunctionType> valueMapping;
+
+            // A reference to an expression evaluator (mainly for resolving the boolean condition in IfThenElse expressions)
+            ExpressionEvaluatorBase<RationalFunctionType> const& evaluator;
         };
 #endif
     }

src/storm/storage/expressions/ToRationalNumberVisitor.cpp

@@ -8,7 +8,7 @@
 namespace storm {
     namespace expressions {
         template<typename RationalNumberType>
-        ToRationalNumberVisitor<RationalNumberType>::ToRationalNumberVisitor() : ExpressionVisitor() {
+        ToRationalNumberVisitor<RationalNumberType>::ToRationalNumberVisitor(ExpressionEvaluatorBase<RationalNumberType> const& evaluator) : ExpressionVisitor(), evaluator(evaluator) {
             // Intentionally left empty.
         }
         
@@ -18,8 +18,13 @@ namespace storm {
         }
         
         template<typename RationalNumberType>
-        boost::any ToRationalNumberVisitor<RationalNumberType>::visit(IfThenElseExpression const&, boost::any const&) {
-            STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational number.");
+        boost::any ToRationalNumberVisitor<RationalNumberType>::visit(IfThenElseExpression const& expression, boost::any const& data) {
+            bool conditionValue = evaluator.asBool(expression.getCondition());
+            if (conditionValue) {
+                return expression.getThenExpression()->accept(*this, data);
+            } else {
+                return expression.getElseExpression()->accept(*this, data);
+            }
         }
         
         template<typename RationalNumberType>

src/storm/storage/expressions/ToRationalNumberVisitor.h

@@ -7,6 +7,7 @@
 #include "storm/storage/expressions/Expression.h"
 #include "storm/storage/expressions/Expressions.h"
 #include "storm/storage/expressions/ExpressionVisitor.h"
+#include "storm/storage/expressions/ExpressionEvaluatorBase.h"
 #include "storm/storage/expressions/Variable.h"
 
 namespace storm {
@@ -15,7 +16,7 @@ namespace storm {
         template<typename RationalNumberType>
         class ToRationalNumberVisitor : public ExpressionVisitor {
         public:
-            ToRationalNumberVisitor();
+            ToRationalNumberVisitor(ExpressionEvaluatorBase<RationalNumberType> const& evaluator);
             
             RationalNumberType toRationalNumber(Expression const& expression);
             
@@ -34,6 +35,9 @@ namespace storm {
             
         private:
             std::unordered_map<storm::expressions::Variable, RationalNumberType> valueMapping;
+
+            // A reference to an expression evaluator (mainly for resolving the boolean condition in IfThenElse expressions)
+            ExpressionEvaluatorBase<RationalNumberType> const& evaluator;
         };
     }
 }