2017-06-23 04:18:07 +02:00
|
|
|
|
#include <pddlparse/detail/normalization/Precondition.h>
|
|
|
|
|
|
|
|
|
|
#include <pddlparse/AST.h>
|
|
|
|
|
#include <pddlparse/Exception.h>
|
|
|
|
|
#include <pddlparse/NormalizedAST.h>
|
|
|
|
|
#include <pddlparse/detail/normalization/AtomicFormula.h>
|
2017-06-24 14:29:13 +02:00
|
|
|
|
#include <pddlparse/detail/normalization/CollectFreeVariables.h>
|
2017-06-23 04:18:07 +02:00
|
|
|
|
|
|
|
|
|
namespace pddl
|
|
|
|
|
{
|
|
|
|
|
namespace detail
|
|
|
|
|
{
|
|
|
|
|
|
|
|
|
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
|
|
|
|
//
|
|
|
|
|
// Precondition
|
|
|
|
|
//
|
|
|
|
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
|
|
|
|
|
2017-06-24 14:29:13 +02:00
|
|
|
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
|
|
|
|
// Forward Declarations
|
|
|
|
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
|
|
|
|
|
|
|
|
|
normalizedAST::Literal normalizeNested(ast::AndPointer<ast::Precondition> &and_, normalizedAST::DerivedPredicateDeclarations &derivedPredicates);
|
|
|
|
|
normalizedAST::Literal normalizeNested(ast::ExistsPointer<ast::Precondition> &exists, normalizedAST::DerivedPredicateDeclarations &derivedPredicates);
|
|
|
|
|
normalizedAST::Literal normalizeNested(ast::ForAllPointer<ast::Precondition> &forAll, normalizedAST::DerivedPredicateDeclarations &derivedPredicates);
|
|
|
|
|
normalizedAST::Literal normalizeNested(ast::ImplyPointer<ast::Precondition> &, normalizedAST::DerivedPredicateDeclarations &);
|
|
|
|
|
normalizedAST::Literal normalizeNested(ast::NotPointer<ast::Precondition> ¬_, normalizedAST::DerivedPredicateDeclarations &derivedPredicates);
|
|
|
|
|
normalizedAST::Literal normalizeNested(ast::OrPointer<ast::Precondition> &or_, normalizedAST::DerivedPredicateDeclarations &derivedPredicates);
|
|
|
|
|
normalizedAST::Literal normalizeNested(ast::UnsupportedPointer &unsupported, normalizedAST::DerivedPredicateDeclarations &);
|
|
|
|
|
normalizedAST::Literal normalizeNested(ast::AtomicFormula &, normalizedAST::DerivedPredicateDeclarations &);
|
|
|
|
|
normalizedAST::PredicatePointer normalize(ast::UnsupportedPointer &&unsupported, normalizedAST::DerivedPredicateDeclarations &);
|
|
|
|
|
normalizedAST::AtomicFormula normalize(ast::AtomicFormula &atomicFormula, normalizedAST::DerivedPredicateDeclarations &);
|
|
|
|
|
normalizedAST::NotPointer<normalizedAST::AtomicFormula> normalize(ast::NotPointer<ast::Precondition> &¬_, normalizedAST::DerivedPredicateDeclarations &derivedPredicates);
|
|
|
|
|
normalizedAST::AndPointer<normalizedAST::Literal> normalize(ast::AndPointer<ast::Precondition> &&and_, normalizedAST::DerivedPredicateDeclarations &derivedPredicates);
|
|
|
|
|
|
|
|
|
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
|
|
|
|
|
|
|
|
|
normalizedAST::DerivedPredicatePointer addDerivedPredicate(const std::vector<normalizedAST::VariableDeclaration *> ¶meters, normalizedAST::DerivedPredicateDeclarations &derivedPredicates)
|
2017-06-23 04:18:07 +02:00
|
|
|
|
{
|
2017-06-24 14:29:13 +02:00
|
|
|
|
auto name = "derived-predicate-" + std::to_string(derivedPredicates.size() + 1);
|
|
|
|
|
|
|
|
|
|
normalizedAST::DerivedPredicate::Arguments arguments;
|
|
|
|
|
arguments.reserve(parameters.size());
|
|
|
|
|
|
|
|
|
|
for (const auto ¶meter : parameters)
|
|
|
|
|
arguments.emplace_back(std::make_unique<normalizedAST::Variable>(parameter));
|
2017-06-23 04:18:07 +02:00
|
|
|
|
|
2017-06-24 14:29:13 +02:00
|
|
|
|
derivedPredicates.emplace_back(std::make_unique<normalizedAST::DerivedPredicateDeclaration>());
|
2017-06-23 04:18:07 +02:00
|
|
|
|
|
2017-06-24 14:29:13 +02:00
|
|
|
|
auto *derivedPredicate = derivedPredicates.back().get();
|
|
|
|
|
derivedPredicate->name = std::move(name);
|
|
|
|
|
derivedPredicate->parameters = std::move(parameters);
|
|
|
|
|
|
|
|
|
|
return std::make_unique<normalizedAST::DerivedPredicate>(std::move(arguments), derivedPredicate);
|
2017-06-23 04:18:07 +02:00
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
|
|
|
|
|
2017-06-24 14:29:13 +02:00
|
|
|
|
normalizedAST::Literal normalizeNested(ast::AndPointer<ast::Precondition> &and_, normalizedAST::DerivedPredicateDeclarations &derivedPredicates)
|
2017-06-23 04:18:07 +02:00
|
|
|
|
{
|
2017-06-24 14:29:13 +02:00
|
|
|
|
std::vector<normalizedAST::VariableDeclaration *> parameters;
|
|
|
|
|
VariableStack variableStack;
|
|
|
|
|
|
|
|
|
|
collectFreeVariables(and_, parameters, variableStack);
|
|
|
|
|
|
|
|
|
|
auto derivedPredicate = addDerivedPredicate(parameters, derivedPredicates);
|
|
|
|
|
|
|
|
|
|
normalizedAST::And<normalizedAST::Literal>::Arguments normalizedArguments;
|
|
|
|
|
normalizedArguments.reserve(and_->arguments.size());
|
|
|
|
|
|
|
|
|
|
for (auto &argument : and_->arguments)
|
|
|
|
|
normalizedArguments.emplace_back(argument.match(
|
|
|
|
|
[&](auto &x) -> normalizedAST::Literal
|
|
|
|
|
{
|
|
|
|
|
return normalizeNested(x, derivedPredicates);
|
|
|
|
|
}));
|
|
|
|
|
|
|
|
|
|
derivedPredicate->declaration->precondition = std::make_unique<normalizedAST::And<normalizedAST::Literal>>(std::move(normalizedArguments));
|
|
|
|
|
|
|
|
|
|
// TODO: investigate, could be a compiler bug
|
|
|
|
|
return std::move(derivedPredicate);
|
2017-06-23 04:18:07 +02:00
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
|
|
|
|
|
2017-06-24 14:29:13 +02:00
|
|
|
|
normalizedAST::Literal normalizeNested(ast::ExistsPointer<ast::Precondition> &exists, normalizedAST::DerivedPredicateDeclarations &derivedPredicates)
|
2017-06-23 04:18:07 +02:00
|
|
|
|
{
|
2017-06-24 14:29:13 +02:00
|
|
|
|
std::vector<normalizedAST::VariableDeclaration *> parameters;
|
|
|
|
|
VariableStack variableStack;
|
|
|
|
|
|
|
|
|
|
collectFreeVariables(exists, parameters, variableStack);
|
|
|
|
|
|
|
|
|
|
auto derivedPredicate = addDerivedPredicate(parameters, derivedPredicates);
|
|
|
|
|
|
|
|
|
|
derivedPredicate->declaration->existentialParameters = std::move(exists->parameters);
|
|
|
|
|
derivedPredicate->declaration->precondition = exists->argument.match([&](auto &x){return normalizeNested(x, derivedPredicates);});
|
|
|
|
|
|
|
|
|
|
// TODO: investigate, could be a compiler bug
|
|
|
|
|
return std::move(derivedPredicate);
|
2017-06-23 04:18:07 +02:00
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
|
|
|
|
|
2017-06-24 14:29:13 +02:00
|
|
|
|
normalizedAST::Literal normalizeNested(ast::ForAllPointer<ast::Precondition> &, normalizedAST::DerivedPredicateDeclarations &)
|
2017-06-23 04:18:07 +02:00
|
|
|
|
{
|
2017-06-24 14:29:13 +02:00
|
|
|
|
// “forall” expressions should be reduced to negated “exists” statements at this point
|
|
|
|
|
throw std::logic_error("precondition not in normal form (forall), please report to the bug tracker");
|
2017-06-23 04:18:07 +02:00
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
|
|
|
|
|
2017-06-24 14:29:13 +02:00
|
|
|
|
normalizedAST::Literal normalizeNested(ast::ImplyPointer<ast::Precondition> &, normalizedAST::DerivedPredicateDeclarations &)
|
2017-06-23 04:18:07 +02:00
|
|
|
|
{
|
2017-06-24 14:29:13 +02:00
|
|
|
|
// “imply” expressions should be reduced to disjunctions at this point
|
|
|
|
|
throw std::logic_error("precondition not in normal form (imply), please report to the bug tracker");
|
2017-06-23 04:18:07 +02:00
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
|
|
|
|
|
2017-06-24 14:29:13 +02:00
|
|
|
|
normalizedAST::Literal normalizeNested(ast::NotPointer<ast::Precondition> ¬_, normalizedAST::DerivedPredicateDeclarations &derivedPredicates)
|
2017-06-23 04:18:07 +02:00
|
|
|
|
{
|
2017-06-24 14:29:13 +02:00
|
|
|
|
std::vector<normalizedAST::VariableDeclaration *> parameters;
|
|
|
|
|
VariableStack variableStack;
|
|
|
|
|
|
|
|
|
|
collectFreeVariables(not_, parameters, variableStack);
|
|
|
|
|
|
|
|
|
|
auto derivedPredicate = addDerivedPredicate(parameters, derivedPredicates);
|
|
|
|
|
|
|
|
|
|
auto normalizedArgumentLiteral = not_->argument.match(
|
|
|
|
|
[&](auto &x) -> normalizedAST::Literal
|
|
|
|
|
{
|
|
|
|
|
return normalizeNested(x, derivedPredicates);
|
|
|
|
|
});
|
|
|
|
|
|
|
|
|
|
// Multiple negations should be eliminated at this point
|
|
|
|
|
if (normalizedArgumentLiteral.is<normalizedAST::NotPointer<normalizedAST::AtomicFormula>>())
|
|
|
|
|
throw std::logic_error("precondition not in normal form (multiple negation), please report to the bug tracker");
|
|
|
|
|
|
|
|
|
|
auto &normalizedArgument = normalizedArgumentLiteral.get<normalizedAST::AtomicFormula>();
|
|
|
|
|
|
|
|
|
|
derivedPredicate->declaration->precondition = std::make_unique<normalizedAST::Not<normalizedAST::AtomicFormula>>(std::move(normalizedArgument));
|
|
|
|
|
|
|
|
|
|
// TODO: investigate, could be a compiler bug
|
|
|
|
|
return std::move(derivedPredicate);
|
2017-06-23 04:18:07 +02:00
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
|
|
|
|
|
2017-06-24 14:29:13 +02:00
|
|
|
|
normalizedAST::Literal normalizeNested(ast::OrPointer<ast::Precondition> &or_, normalizedAST::DerivedPredicateDeclarations &derivedPredicates)
|
2017-06-23 04:18:07 +02:00
|
|
|
|
{
|
2017-06-24 14:29:13 +02:00
|
|
|
|
std::vector<normalizedAST::VariableDeclaration *> parameters;
|
|
|
|
|
VariableStack variableStack;
|
|
|
|
|
|
|
|
|
|
collectFreeVariables(or_, parameters, variableStack);
|
|
|
|
|
|
|
|
|
|
auto derivedPredicate = addDerivedPredicate(parameters, derivedPredicates);
|
|
|
|
|
|
|
|
|
|
normalizedAST::Or<normalizedAST::Literal>::Arguments normalizedArguments;
|
|
|
|
|
normalizedArguments.reserve(or_->arguments.size());
|
|
|
|
|
|
|
|
|
|
for (auto &argument : or_->arguments)
|
|
|
|
|
normalizedArguments.emplace_back(argument.match(
|
|
|
|
|
[&](auto &x) -> normalizedAST::Literal
|
|
|
|
|
{
|
|
|
|
|
return normalizeNested(x, derivedPredicates);
|
|
|
|
|
}));
|
|
|
|
|
|
|
|
|
|
derivedPredicate->declaration->precondition = std::make_unique<normalizedAST::Or<normalizedAST::Literal>>(std::move(normalizedArguments));
|
|
|
|
|
|
|
|
|
|
// TODO: investigate, could be a compiler bug
|
|
|
|
|
return std::move(derivedPredicate);
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
|
|
|
|
|
|
|
|
|
normalizedAST::Literal normalizeNested(ast::UnsupportedPointer &unsupported, normalizedAST::DerivedPredicateDeclarations &)
|
|
|
|
|
{
|
|
|
|
|
throw NormalizationException("“" + unsupported->type + "” expressions in preconditions can’t be normalized currently");
|
2017-06-23 04:18:07 +02:00
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
|
|
|
|
|
2017-06-24 14:29:13 +02:00
|
|
|
|
normalizedAST::Literal normalizeNested(ast::AtomicFormula &atomicFormula, normalizedAST::DerivedPredicateDeclarations &)
|
2017-06-23 04:18:07 +02:00
|
|
|
|
{
|
2017-06-24 14:29:13 +02:00
|
|
|
|
return normalize(std::move(atomicFormula));
|
2017-06-23 04:18:07 +02:00
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
|
|
|
|
|
|
|
|
|
normalizedAST::PredicatePointer normalize(ast::UnsupportedPointer &&unsupported, normalizedAST::DerivedPredicateDeclarations &)
|
|
|
|
|
{
|
|
|
|
|
throw NormalizationException("“" + unsupported->type + "” expressions in preconditions can’t be normalized currently");
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
|
|
|
|
|
2017-06-24 14:29:13 +02:00
|
|
|
|
normalizedAST::AtomicFormula normalize(ast::AtomicFormula &&atomicFormula, normalizedAST::DerivedPredicateDeclarations &)
|
|
|
|
|
{
|
|
|
|
|
return normalize(std::move(atomicFormula));
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
|
|
|
|
|
2017-06-23 04:18:07 +02:00
|
|
|
|
// Normalize top-level negations
|
|
|
|
|
normalizedAST::NotPointer<normalizedAST::AtomicFormula> normalize(ast::NotPointer<ast::Precondition> &¬_, normalizedAST::DerivedPredicateDeclarations &derivedPredicates)
|
|
|
|
|
{
|
|
|
|
|
// “not” expressions may be nested one time to form simple literals
|
|
|
|
|
if (not_->argument.is<ast::AtomicFormula>())
|
|
|
|
|
return std::make_unique<normalizedAST::Not<normalizedAST::AtomicFormula>>(normalize(std::move(not_->argument.get<ast::AtomicFormula>())));
|
|
|
|
|
|
2017-06-24 14:29:13 +02:00
|
|
|
|
auto normalizedArgument = not_->argument.match(
|
2017-06-23 04:18:07 +02:00
|
|
|
|
[&](auto &nested) -> normalizedAST::AtomicFormula
|
|
|
|
|
{
|
2017-06-24 14:29:13 +02:00
|
|
|
|
auto normalizedLiteral = normalizeNested(nested, derivedPredicates);
|
2017-06-23 04:18:07 +02:00
|
|
|
|
|
2017-06-24 14:29:13 +02:00
|
|
|
|
// Multiple negations should be eliminated at this point
|
|
|
|
|
if (normalizedLiteral.template is<normalizedAST::NotPointer<normalizedAST::AtomicFormula>>())
|
|
|
|
|
throw std::logic_error("precondition not in normal form (multiple negation), please report to the bug tracker");
|
2017-06-23 04:18:07 +02:00
|
|
|
|
|
2017-06-24 14:29:13 +02:00
|
|
|
|
return std::move(normalizedLiteral.template get<normalizedAST::AtomicFormula>());
|
|
|
|
|
});
|
2017-06-23 04:18:07 +02:00
|
|
|
|
|
|
|
|
|
return std::make_unique<normalizedAST::Not<normalizedAST::AtomicFormula>>(std::move(normalizedArgument));
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
|
|
|
|
|
|
|
|
|
// Normalize top-level conjunctions
|
|
|
|
|
normalizedAST::AndPointer<normalizedAST::Literal> normalize(ast::AndPointer<ast::Precondition> &&and_, normalizedAST::DerivedPredicateDeclarations &derivedPredicates)
|
|
|
|
|
{
|
|
|
|
|
normalizedAST::And<normalizedAST::Literal>::Arguments arguments;
|
|
|
|
|
|
|
|
|
|
arguments.reserve(and_->arguments.size());
|
|
|
|
|
|
|
|
|
|
const auto handleAtomicFormula =
|
|
|
|
|
[&](ast::AtomicFormula &atomicFormula) -> normalizedAST::Literal
|
|
|
|
|
{
|
|
|
|
|
return normalize(std::move(atomicFormula));
|
|
|
|
|
};
|
|
|
|
|
|
|
|
|
|
const auto handleNot =
|
|
|
|
|
[&](ast::NotPointer<ast::Precondition> ¬_) -> normalizedAST::Literal
|
|
|
|
|
{
|
|
|
|
|
return normalize(std::move(not_), derivedPredicates);
|
|
|
|
|
};
|
|
|
|
|
|
|
|
|
|
const auto handleNested =
|
|
|
|
|
[&](auto &nested) -> normalizedAST::Literal
|
|
|
|
|
{
|
|
|
|
|
return normalizeNested(nested, derivedPredicates);
|
|
|
|
|
};
|
|
|
|
|
|
|
|
|
|
const auto handleUnsupported =
|
|
|
|
|
[&](ast::UnsupportedPointer &unsupported) -> normalizedAST::Literal
|
|
|
|
|
{
|
|
|
|
|
throw NormalizationException("“" + unsupported->type + "” expressions in preconditions can’t be normalized currently");
|
|
|
|
|
};
|
|
|
|
|
|
|
|
|
|
for (auto &&argument : and_->arguments)
|
|
|
|
|
{
|
|
|
|
|
auto normalizedArgument = argument.match(handleAtomicFormula, handleNot, handleNested, handleUnsupported);
|
|
|
|
|
|
|
|
|
|
arguments.emplace_back(std::move(normalizedArgument));
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
return std::make_unique<normalizedAST::And<normalizedAST::Literal>>(std::move(arguments));
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
|
|
|
|
|
|
|
|
|
normalizedAST::Precondition normalize(ast::Precondition &&precondition, normalizedAST::DerivedPredicateDeclarations &derivedPredicates)
|
|
|
|
|
{
|
2017-06-24 14:29:13 +02:00
|
|
|
|
return precondition.match(
|
|
|
|
|
[&](auto &x) -> normalizedAST::Precondition
|
2017-06-23 04:18:07 +02:00
|
|
|
|
{
|
2017-06-24 14:29:13 +02:00
|
|
|
|
return normalize(std::move(x), derivedPredicates);
|
|
|
|
|
});
|
2017-06-23 04:18:07 +02:00
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
|
|
|
|
|
|
|
|
|
}
|
|
|
|
|
}
|