From 994801525afeb67f0d443313186cbcd609dde828 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Patrick=20L=C3=BChne?= <patrick-github@luehne.de>
Date: Sat, 24 Jun 2017 17:19:35 +0200
Subject: [PATCH] Implemented negation normalization (NFF).

---
 app/main.cpp                                  |   1 +
 .../detail/normalization/Reduction.cpp        | 140 ++++++++++++++++++
 2 files changed, 141 insertions(+)

diff --git a/app/main.cpp b/app/main.cpp
index 514e149..d350c3a 100644
--- a/app/main.cpp
+++ b/app/main.cpp
@@ -14,6 +14,7 @@
 #include <pddlparse/Normalize.h>
 #include <pddlparse/NormalizedASTOutput.h>
 #include <pddlparse/Parse.h>
+#include <pddlparse/detail/normalization/Reduction.h>
 
 #include <plasp/LanguageDetection.h>
 #include <plasp/TranslatorException.h>
diff --git a/lib/pddlparse/src/pddlparse/detail/normalization/Reduction.cpp b/lib/pddlparse/src/pddlparse/detail/normalization/Reduction.cpp
index 9d29cef..11e6b40 100644
--- a/lib/pddlparse/src/pddlparse/detail/normalization/Reduction.cpp
+++ b/lib/pddlparse/src/pddlparse/detail/normalization/Reduction.cpp
@@ -17,6 +17,15 @@ namespace detail
 //
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
+////////////////////////////////////////////////////////////////////////////////////////////////////
+// Forward declarations
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+void eliminateImply(ast::Precondition &precondition);
+void negationNormalize(ast::Precondition &precondition);
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
 const auto handleUnsupported =
 	[](ast::UnsupportedPointer &unsupported)
 	{
@@ -83,10 +92,141 @@ void eliminateImply(ast::Precondition &precondition)
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
+// Negation-normalize an expression whose parent is a “not” expression
+void negationNormalizeNegated(ast::Precondition &precondition, ast::Precondition &parent)
+{
+	const auto handleAtomicFormula =
+		[](ast::AtomicFormula &)
+		{
+		};
+
+	const auto handleAnd =
+		[&](ast::AndPointer<ast::Precondition> &and_)
+		{
+			ast::Or<ast::Precondition>::Arguments arguments;
+			arguments.reserve(and_->arguments.size());
+
+			// Apply De Morgan
+			for (auto &argument : and_->arguments)
+				arguments.emplace_back(std::make_unique<ast::Not<ast::Precondition>>(std::move(argument)));
+
+			// Finally, negation-normalize each argument
+			for (auto &argument : arguments)
+				negationNormalize(argument);
+
+			// Replace the parent “not” containing this “and” with an “or” over the negated arguments
+			parent = std::make_unique<ast::Or<ast::Precondition>>(std::move(arguments));
+		};
+
+	const auto handleExists =
+		[](ast::ExistsPointer<ast::Precondition> &exists)
+		{
+			negationNormalize(exists->argument);
+		};
+
+	const auto handleForAll =
+		[](ast::ForAllPointer<ast::Precondition> &forAll)
+		{
+			negationNormalize(forAll->argument);
+		};
+
+	const auto handleImply =
+		[](ast::ImplyPointer<ast::Precondition> &)
+		{
+			throw std::logic_error("precondition not ready for negation normalization (imply), please report to the bug tracker");
+		};
+
+	const auto handleNot =
+		[&](ast::NotPointer<ast::Precondition> &not_)
+		{
+			negationNormalize(not_->argument);
+
+			// As the parent contains the argument, the argument needs to be saved before overwriting the parent
+			// TODO: check whether this workaround can be avoided
+			auto argument = std::move(not_->argument);
+			parent = std::move(argument);
+		};
+
+	const auto handleOr =
+		[&](ast::OrPointer<ast::Precondition> &or_)
+		{
+			ast::And<ast::Precondition>::Arguments arguments;
+			arguments.reserve(or_->arguments.size());
+
+			// Apply De Morgan
+			for (auto &argument : or_->arguments)
+				arguments.emplace_back(std::make_unique<ast::Not<ast::Precondition>>(std::move(argument)));
+
+			// Finally, negation-normalize each argument
+			for (auto &argument : arguments)
+				negationNormalize(argument);
+
+			// Replace the parent “not” containing this “or” with an “and” over the negated arguments
+			parent = std::make_unique<ast::And<ast::Precondition>>(std::move(arguments));
+		};
+
+	precondition.match(handleAtomicFormula, handleAnd, handleExists, handleForAll, handleImply, handleNot, handleOr, handleUnsupported);
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+void negationNormalize(ast::Precondition &precondition)
+{
+	const auto handleAtomicFormula =
+		[](ast::AtomicFormula &)
+		{
+		};
+
+	const auto handleAnd =
+		[](ast::AndPointer<ast::Precondition> &and_)
+		{
+			for (auto &argument : and_->arguments)
+				negationNormalize(argument);
+		};
+
+	const auto handleExists =
+		[](ast::ExistsPointer<ast::Precondition> &exists)
+		{
+			negationNormalize(exists->argument);
+		};
+
+	const auto handleForAll =
+		[](ast::ForAllPointer<ast::Precondition> &forAll)
+		{
+			negationNormalize(forAll->argument);
+		};
+
+	const auto handleImply =
+		[](ast::ImplyPointer<ast::Precondition> &)
+		{
+			throw std::logic_error("precondition not ready for negation normalization (imply), please report to the bug tracker");
+		};
+
+	const auto handleNot =
+		[&](ast::NotPointer<ast::Precondition> &not_)
+		{
+			negationNormalizeNegated(not_->argument, precondition);
+		};
+
+	const auto handleOr =
+		[](ast::OrPointer<ast::Precondition> &or_)
+		{
+			for (auto &argument : or_->arguments)
+				negationNormalize(argument);
+		};
+
+	precondition.match(handleAtomicFormula, handleAnd, handleExists, handleForAll, handleImply, handleNot, handleOr, handleUnsupported);
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
 void reduce(ast::Precondition &precondition)
 {
 	// Replace “imply” statements with disjunctions
 	eliminateImply(precondition);
+
+	// Negation-normalize the precondition
+	negationNormalize(precondition);
 }
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////