diff --git a/src/storm/storage/expressions/BinaryBooleanFunctionExpression.cpp b/src/storm/storage/expressions/BinaryBooleanFunctionExpression.cpp index 32aed361e..726258f90 100644 --- a/src/storm/storage/expressions/BinaryBooleanFunctionExpression.cpp +++ b/src/storm/storage/expressions/BinaryBooleanFunctionExpression.cpp @@ -4,6 +4,7 @@ #include "storm/storage/expressions/ExpressionVisitor.h" #include "storm/utility/macros.h" #include "storm/exceptions/InvalidTypeException.h" +#include "Expressions.h" namespace storm { namespace expressions { @@ -107,6 +108,18 @@ namespace storm { } else if (firstOperandSimplified->isFalse() && secondOperandSimplified->isTrue()) { return std::shared_ptr(new BooleanLiteralExpression(this->getManager(), false)); } + if (firstOperandSimplified->isTrue()) { + return secondOperandSimplified; + } + if (secondOperandSimplified->isTrue()) { + return firstOperandSimplified; + } + if (firstOperandSimplified->isFalse()) { + return std::shared_ptr(new UnaryBooleanFunctionExpression(this->getManager(), this->getType(), secondOperandSimplified, UnaryBooleanFunctionExpression::OperatorType::Not)); + } + if (secondOperandSimplified->isFalse()) { + return std::shared_ptr(new UnaryBooleanFunctionExpression(this->getManager(), this->getType(), firstOperandSimplified, UnaryBooleanFunctionExpression::OperatorType::Not)); + } break; } }