From 4350ea72d75dcb91622275833e1515cdd61a1271 Mon Sep 17 00:00:00 2001
From: Sebastian Junges <sebastian.junges@gmail.com>
Date: Tue, 9 Jun 2020 14:30:43 -0700
Subject: [PATCH] Simplifying expressions with iff and implies a bit more

---
 .../expressions/BinaryBooleanFunctionExpression.cpp | 13 +++++++++++++
 1 file changed, 13 insertions(+)

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