Simplifying expressions with iff and implies a bit more

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<BaseExpression>(new BooleanLiteralExpression(this->getManager(), false));
                         }
+                        if (firstOperandSimplified->isTrue()) {
+                            return secondOperandSimplified;
+                        }
+                        if (secondOperandSimplified->isTrue()) {
+                            return firstOperandSimplified;
+                        }
+                        if (firstOperandSimplified->isFalse()) {
+                            return std::shared_ptr<BaseExpression>(new UnaryBooleanFunctionExpression(this->getManager(), this->getType(), secondOperandSimplified, UnaryBooleanFunctionExpression::OperatorType::Not));
+                        }
+                        if (secondOperandSimplified->isFalse()) {
+                            return std::shared_ptr<BaseExpression>(new UnaryBooleanFunctionExpression(this->getManager(), this->getType(), firstOperandSimplified, UnaryBooleanFunctionExpression::OperatorType::Not));
+                        }
                         break;
                 }
             }