From ad6b3d60ebd4c95482e912ffb18a7019126dd08b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Patrick=20L=C3=BChne?= <patrick-github@luehne.de>
Date: Tue, 6 Sep 2016 17:43:47 +0200
Subject: [PATCH] Implemented De Morgan normalization for quantified
 expressions.

---
 src/plasp/pddl/expressions/Not.cpp | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)

diff --git a/src/plasp/pddl/expressions/Not.cpp b/src/plasp/pddl/expressions/Not.cpp
index ded0f77..b406fcf 100644
--- a/src/plasp/pddl/expressions/Not.cpp
+++ b/src/plasp/pddl/expressions/Not.cpp
@@ -1,6 +1,8 @@
 #include <plasp/pddl/expressions/Not.h>
 
 #include <plasp/pddl/expressions/And.h>
+#include <plasp/pddl/expressions/Exists.h>
+#include <plasp/pddl/expressions/ForAll.h>
 #include <plasp/pddl/expressions/Or.h>
 
 namespace plasp
@@ -99,6 +101,28 @@ ExpressionPointer Not::negationNormalized()
 		return andExpression->negationNormalized();
 	}
 
+	// De Morgen for existential quantifiers
+	if (m_argument->expressionType() == Expression::Type::Exists)
+	{
+		auto &existsExpression = dynamic_cast<Exists &>(*m_argument);
+		auto forAllExpression = ForAllPointer(new ForAll);
+
+		forAllExpression->setArgument(existsExpression.argument()->negated());
+
+		return forAllExpression->negationNormalized();
+	}
+
+	// De Morgen for universal quantifiers
+	if (m_argument->expressionType() == Expression::Type::ForAll)
+	{
+		auto &forAllExpression = dynamic_cast<ForAll &>(*m_argument);
+		auto existsExpression = ExistsPointer(new Exists);
+
+		existsExpression->setArgument(forAllExpression.argument()->negated());
+
+		return existsExpression->negationNormalized();
+	}
+
 	return this;
 }