diff --git a/src/storm/storage/expressions/ExpressionEvaluator.cpp b/src/storm/storage/expressions/ExpressionEvaluator.cpp index abea0ce73..3305ec772 100644 --- a/src/storm/storage/expressions/ExpressionEvaluator.cpp +++ b/src/storm/storage/expressions/ExpressionEvaluator.cpp @@ -33,7 +33,7 @@ namespace storm { } #ifdef STORM_HAVE_CARL - ExpressionEvaluator::ExpressionEvaluator(storm::expressions::ExpressionManager const& manager) : ExprtkExpressionEvaluatorBase(manager) { + ExpressionEvaluator::ExpressionEvaluator(storm::expressions::ExpressionManager const& manager) : ExprtkExpressionEvaluatorBase(manager), rationalNumberVisitor(*this) { // Intentionally left empty. } @@ -57,7 +57,7 @@ namespace storm { return this->rationalNumberVisitor.toRationalNumber(expression); } - ExpressionEvaluator::ExpressionEvaluator(storm::expressions::ExpressionManager const& manager) : ExprtkExpressionEvaluatorBase(manager) { + ExpressionEvaluator::ExpressionEvaluator(storm::expressions::ExpressionManager const& manager) : ExprtkExpressionEvaluatorBase(manager), rationalFunctionVisitor(*this) { // Intentionally left empty. } diff --git a/src/storm/storage/expressions/ToRationalFunctionVisitor.cpp b/src/storm/storage/expressions/ToRationalFunctionVisitor.cpp index 9f8ab16ec..6fa620157 100644 --- a/src/storm/storage/expressions/ToRationalFunctionVisitor.cpp +++ b/src/storm/storage/expressions/ToRationalFunctionVisitor.cpp @@ -11,7 +11,7 @@ namespace storm { #ifdef STORM_HAVE_CARL template - ToRationalFunctionVisitor::ToRationalFunctionVisitor() : ExpressionVisitor(), cache(new carl::Cache>()) { + ToRationalFunctionVisitor::ToRationalFunctionVisitor(ExpressionEvaluatorBase const& evaluator) : ExpressionVisitor(), cache(new carl::Cache>()), evaluator(evaluator) { // Intentionally left empty. } @@ -21,8 +21,13 @@ namespace storm { } template - boost::any ToRationalFunctionVisitor::visit(IfThenElseExpression const&, boost::any const&) { - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational function."); + boost::any ToRationalFunctionVisitor::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 diff --git a/src/storm/storage/expressions/ToRationalFunctionVisitor.h b/src/storm/storage/expressions/ToRationalFunctionVisitor.h index 7c7cfacf5..6e90d36ce 100644 --- a/src/storm/storage/expressions/ToRationalFunctionVisitor.h +++ b/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 class ToRationalFunctionVisitor : public ExpressionVisitor { public: - ToRationalFunctionVisitor(); + ToRationalFunctionVisitor(ExpressionEvaluatorBase const& evaluator); RationalFunctionType toRationalFunction(Expression const& expression); @@ -53,6 +54,9 @@ namespace storm { // A mapping from variables to their values. std::unordered_map valueMapping; + + // A reference to an expression evaluator (mainly for resolving the boolean condition in IfThenElse expressions) + ExpressionEvaluatorBase const& evaluator; }; #endif } diff --git a/src/storm/storage/expressions/ToRationalNumberVisitor.cpp b/src/storm/storage/expressions/ToRationalNumberVisitor.cpp index d4ba17c06..26ad15b5a 100644 --- a/src/storm/storage/expressions/ToRationalNumberVisitor.cpp +++ b/src/storm/storage/expressions/ToRationalNumberVisitor.cpp @@ -8,7 +8,7 @@ namespace storm { namespace expressions { template - ToRationalNumberVisitor::ToRationalNumberVisitor() : ExpressionVisitor() { + ToRationalNumberVisitor::ToRationalNumberVisitor(ExpressionEvaluatorBase const& evaluator) : ExpressionVisitor(), evaluator(evaluator) { // Intentionally left empty. } @@ -18,8 +18,13 @@ namespace storm { } template - boost::any ToRationalNumberVisitor::visit(IfThenElseExpression const&, boost::any const&) { - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational number."); + boost::any ToRationalNumberVisitor::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 diff --git a/src/storm/storage/expressions/ToRationalNumberVisitor.h b/src/storm/storage/expressions/ToRationalNumberVisitor.h index 6177fd2ae..89cb9f81f 100644 --- a/src/storm/storage/expressions/ToRationalNumberVisitor.h +++ b/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 class ToRationalNumberVisitor : public ExpressionVisitor { public: - ToRationalNumberVisitor(); + ToRationalNumberVisitor(ExpressionEvaluatorBase const& evaluator); RationalNumberType toRationalNumber(Expression const& expression); @@ -34,6 +35,9 @@ namespace storm { private: std::unordered_map valueMapping; + + // A reference to an expression evaluator (mainly for resolving the boolean condition in IfThenElse expressions) + ExpressionEvaluatorBase const& evaluator; }; } }