Implemented negation normalization (NFF).

This commit is contained in:
Patrick Lühne 2017-06-24 17:19:35 +02:00
parent 939c2c735c
commit 994801525a
Signed by: patrick
GPG Key ID: 05F3611E97A70ABF
2 changed files with 141 additions and 0 deletions

View File

@ -14,6 +14,7 @@
#include <pddlparse/Normalize.h> #include <pddlparse/Normalize.h>
#include <pddlparse/NormalizedASTOutput.h> #include <pddlparse/NormalizedASTOutput.h>
#include <pddlparse/Parse.h> #include <pddlparse/Parse.h>
#include <pddlparse/detail/normalization/Reduction.h>
#include <plasp/LanguageDetection.h> #include <plasp/LanguageDetection.h>
#include <plasp/TranslatorException.h> #include <plasp/TranslatorException.h>

View File

@ -17,6 +17,15 @@ namespace detail
// //
//////////////////////////////////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////////////////////////////////
// Forward declarations
////////////////////////////////////////////////////////////////////////////////////////////////////
void eliminateImply(ast::Precondition &precondition);
void negationNormalize(ast::Precondition &precondition);
////////////////////////////////////////////////////////////////////////////////////////////////////
const auto handleUnsupported = const auto handleUnsupported =
[](ast::UnsupportedPointer &unsupported) [](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) void reduce(ast::Precondition &precondition)
{ {
// Replace “imply” statements with disjunctions // Replace “imply” statements with disjunctions
eliminateImply(precondition); eliminateImply(precondition);
// Negation-normalize the precondition
negationNormalize(precondition);
} }
//////////////////////////////////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////////////////////////////////