patrick/plasp
Archived
1
0
Fork 0
Code Issues 12 Releases 8 Activity

Implemented normalization of preconditions.

Browse Source
This commit is contained in:
Patrick Lühne 2017-06-24 14:29:13 +02:00
parent 9d1a8f4c0f
commit d7e0beabdf
Signed by: patrick
GPG Key ID: 05F3611E97A70ABF
7 changed files with 419 additions and 145 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

81
lib/pddlparse/include/pddlparse/NormalizedAST.h
View File

@ -20,48 +20,6 @@ namespace normalizedAST
//
////////////////////////////////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////////////////////////////////
// Compounds
////////////////////////////////////////////////////////////////////////////////////////////////////
struct DerivedPredicate
{
using Arguments = Terms;
explicit DerivedPredicate(Arguments &&arguments, DerivedPredicateDeclaration *declaration)
: arguments{std::move(arguments)},
declaration{declaration}
{
}
DerivedPredicate(const DerivedPredicate &other) = delete;
DerivedPredicate &operator=(const DerivedPredicate &&other) = delete;
DerivedPredicate(DerivedPredicate &&other) = default;
DerivedPredicate &operator=(DerivedPredicate &&other) = default;
Arguments arguments;
DerivedPredicateDeclaration *declaration;
};
////////////////////////////////////////////////////////////////////////////////////////////////////
struct DerivedPredicateDeclaration
{
explicit DerivedPredicateDeclaration(std::string &&name, VariableDeclarations &&parameters)
: name{std::move(name)},
parameters{std::move(parameters)}
{
}
DerivedPredicateDeclaration(const DerivedPredicateDeclaration &other) = delete;
DerivedPredicateDeclaration &operator=(const DerivedPredicateDeclaration &&other) = delete;
DerivedPredicateDeclaration(DerivedPredicateDeclaration &&other) = default;
DerivedPredicateDeclaration &operator=(DerivedPredicateDeclaration &&other) = default;
std::string name;
VariableDeclarations parameters;
};
////////////////////////////////////////////////////////////////////////////////////////////////////
// PDDL Structure
////////////////////////////////////////////////////////////////////////////////////////////////////
@ -103,6 +61,45 @@ struct Domain
////////////////////////////////////////////////////////////////////////////////////////////////////
struct DerivedPredicate
{
using Arguments = Terms;
explicit DerivedPredicate(Arguments &&arguments, DerivedPredicateDeclaration *declaration)
: arguments{std::move(arguments)},
declaration{declaration}
{
}
DerivedPredicate(const DerivedPredicate &other) = delete;
DerivedPredicate &operator=(const DerivedPredicate &&other) = delete;
DerivedPredicate(DerivedPredicate &&other) = default;
DerivedPredicate &operator=(DerivedPredicate &&other) = default;
Arguments arguments;
DerivedPredicateDeclaration *declaration;
};
////////////////////////////////////////////////////////////////////////////////////////////////////
struct DerivedPredicateDeclaration
{
explicit DerivedPredicateDeclaration() = default;
DerivedPredicateDeclaration(const DerivedPredicateDeclaration &other) = delete;
DerivedPredicateDeclaration &operator=(const DerivedPredicateDeclaration &&other) = delete;
DerivedPredicateDeclaration(DerivedPredicateDeclaration &&other) = default;
DerivedPredicateDeclaration &operator=(DerivedPredicateDeclaration &&other) = default;
std::string name;
std::vector<VariableDeclaration *> parameters;
VariableDeclarations existentialParameters;
std::experimental::optional<DerivedPredicatePrecondition> precondition;
};
////////////////////////////////////////////////////////////////////////////////////////////////////
struct InitialState
{
InitialState() = default;

21
lib/pddlparse/include/pddlparse/NormalizedASTForward.h
View File

@ -71,6 +71,8 @@ using ast::ForAll;
using ast::ForAllPointer;
using ast::Not;
using ast::NotPointer;
using ast::Or;
using ast::OrPointer;
using ast::When;
using ast::WhenPointer;
@ -148,6 +150,25 @@ using Preconditions = std::vector<Precondition>;
////////////////////////////////////////////////////////////////////////////////////////////////////
class DerivedPredicatePrecondition;
namespace detail
{
using DerivedPredicatePreconditionT = Variant<
Literal,
AndPointer<Literal>,
OrPointer<Literal>>;
}
class DerivedPredicatePrecondition : public detail::DerivedPredicatePreconditionT
{
using detail::DerivedPredicatePreconditionT::DerivedPredicatePreconditionT;
};
using DerivedPredicatePreconditions = std::vector<DerivedPredicatePrecondition>;
////////////////////////////////////////////////////////////////////////////////////////////////////
class ConditionalEffect;
namespace detail

81
lib/pddlparse/include/pddlparse/NormalizedASTOutput.h
View File

@ -59,16 +59,71 @@ inline colorlog::ColorStream &print(colorlog::ColorStream &stream, const Derived
inline colorlog::ColorStream &print(colorlog::ColorStream &stream, const DerivedPredicateDeclaration &derivedPredicateDeclaration, pddl::detail::PrintContext &printContext)
{
// TODO: implement correctly
stream << "(" << colorlog::Keyword(":derived-predicate") << " " << pddl::detail::Identifier(derivedPredicateDeclaration.name);
stream << "(" << pddl::detail::Identifier(derivedPredicateDeclaration.name);
printContext.indentationLevel++;
for (const auto &parameter : derivedPredicateDeclaration.parameters)
if (!derivedPredicateDeclaration.parameters.empty())
{
stream << " ";
print(stream, *parameter, printContext);
pddl::detail::printIndentedNewline(stream, printContext);
stream << colorlog::Keyword(":parameters");
printContext.indentationLevel++;
pddl::detail::printIndentedNewline(stream, printContext);
stream << "(";
for (const auto &parameter : derivedPredicateDeclaration.parameters)
{
if (&parameter != &derivedPredicateDeclaration.parameters.front())
pddl::detail::printIndentedNewline(stream, printContext);
print(stream, *parameter, printContext);
}
stream << ")";
printContext.indentationLevel--;
}
if (!derivedPredicateDeclaration.existentialParameters.empty())
{
pddl::detail::printIndentedNewline(stream, printContext);
stream << colorlog::Keyword(":exists");
printContext.indentationLevel++;
pddl::detail::printIndentedNewline(stream, printContext);
stream << "(";
for (const auto &parameter : derivedPredicateDeclaration.existentialParameters)
{
if (parameter.get() != derivedPredicateDeclaration.existentialParameters.front().get())
pddl::detail::printIndentedNewline(stream, printContext);
print(stream, *parameter, printContext);
}
stream << ")";
printContext.indentationLevel--;
}
if (derivedPredicateDeclaration.precondition)
{
pddl::detail::printIndentedNewline(stream, printContext);
stream << colorlog::Keyword(":precondition");
printContext.indentationLevel++;
pddl::detail::printIndentedNewline(stream, printContext);
print(stream, derivedPredicateDeclaration.precondition.value(), printContext);
printContext.indentationLevel--;
}
printContext.indentationLevel--;
return (stream << ")");
}
@ -180,16 +235,8 @@ inline colorlog::ColorStream &print(colorlog::ColorStream &stream, const Domain
if (!domain.derivedPredicates.empty())
{
printIndentedNewline(stream, printContext);
stream << "(" << colorlog::Keyword(":derived-predicates");
printContext.indentationLevel++;
printIndentedNewline(stream, printContext);
print(stream, domain.derivedPredicates, printContext);
stream << ")";
printContext.indentationLevel--;
}
if (!domain.actions.empty())
@ -234,16 +281,8 @@ inline colorlog::ColorStream &print(colorlog::ColorStream &stream, const Problem
if (!problem.derivedPredicates.empty())
{
printIndentedNewline(stream, printContext);
stream << "(" << colorlog::Keyword(":derived-predicates");
printContext.indentationLevel++;
printIndentedNewline(stream, printContext);
print(stream, problem.derivedPredicates, printContext);
stream << ")";
printContext.indentationLevel--;
}
if (!problem.objects.empty())

1
lib/pddlparse/include/pddlparse/detail/VariableStack.h
View File

@ -24,6 +24,7 @@ class VariableStack
void pop();
std::experimental::optional<ast::VariableDeclaration *> findVariableDeclaration(const std::string &variableName);
bool contains(const ast::VariableDeclaration &variableDeclaration) const;
private:
std::vector<Layer> m_layers;

128
lib/pddlparse/include/pddlparse/detail/normalization/CollectFreeVariables.h Normal file
View File

@ -0,0 +1,128 @@
#ifndef __PDDL_PARSE__DETAIL__NORMALIZATION__COLLECT_FREE_VARIABLES_H
#define __PDDL_PARSE__DETAIL__NORMALIZATION__COLLECT_FREE_VARIABLES_H
#include <pddlparse/ASTForward.h>
#include <pddlparse/Context.h>
#include <pddlparse/Exception.h>
#include <pddlparse/NormalizedASTForward.h>
#include <pddlparse/detail/VariableStack.h>
namespace pddl
{
namespace detail
{
////////////////////////////////////////////////////////////////////////////////////////////////////
//
// Collect Free Variables
//
////////////////////////////////////////////////////////////////////////////////////////////////////
template<class Variant>
void collectFreeVariables(const Variant &variant, std::vector<normalizedAST::VariableDeclaration *> &freeVariables, VariableStack &variableStack)
{
variant.match([&](const auto &x){collectFreeVariables(x, freeVariables, variableStack);});
}
////////////////////////////////////////////////////////////////////////////////////////////////////
void collectFreeVariables(const ast::ConstantPointer &, std::vector<normalizedAST::VariableDeclaration *> &, VariableStack &)
{
}
////////////////////////////////////////////////////////////////////////////////////////////////////
void collectFreeVariables(const ast::VariablePointer &variable, std::vector<normalizedAST::VariableDeclaration *> &freeVariables, VariableStack &variableStack)
{
if (variableStack.contains(*variable->declaration))
return;
const auto matchingFreeVariable = std::find(freeVariables.cbegin(), freeVariables.cend(), variable->declaration);
if (matchingFreeVariable != freeVariables.cend())
return;
freeVariables.emplace_back(variable->declaration);
}
////////////////////////////////////////////////////////////////////////////////////////////////////
void collectFreeVariables(const ast::PredicatePointer &predicate, std::vector<normalizedAST::VariableDeclaration *> &freeVariables, VariableStack &variableStack)
{
for (const auto &argument : predicate->arguments)
collectFreeVariables(argument, freeVariables, variableStack);
}
////////////////////////////////////////////////////////////////////////////////////////////////////
template<class Argument>
void collectFreeVariables(const ast::AndPointer<Argument> &and_, std::vector<normalizedAST::VariableDeclaration *> &freeVariables, VariableStack &variableStack)
{
for (const auto &argument : and_->arguments)
collectFreeVariables(argument, freeVariables, variableStack);
}
////////////////////////////////////////////////////////////////////////////////////////////////////
template<class Argument>
void collectFreeVariables(const ast::ExistsPointer<Argument> &exists, std::vector<normalizedAST::VariableDeclaration *> &freeVariables, VariableStack &variableStack)
{
variableStack.push(&exists->parameters);
collectFreeVariables(exists->argument, freeVariables, variableStack);
variableStack.pop();
}
////////////////////////////////////////////////////////////////////////////////////////////////////
template<class Argument>
void collectFreeVariables(const ast::ForAllPointer<Argument> &forAll, std::vector<normalizedAST::VariableDeclaration *> &freeVariables, VariableStack &variableStack)
{
variableStack.push(&forAll->parameters);
collectFreeVariables(forAll->argument, freeVariables, variableStack);
variableStack.pop();
}
////////////////////////////////////////////////////////////////////////////////////////////////////
template<class Argument>
void collectFreeVariables(const ast::ImplyPointer<Argument> &imply, std::vector<normalizedAST::VariableDeclaration *> &freeVariables, VariableStack &variableStack)
{
collectFreeVariables(imply->argumentLeft, freeVariables, variableStack);
collectFreeVariables(imply->argumentRight, freeVariables, variableStack);
}
////////////////////////////////////////////////////////////////////////////////////////////////////
template<class Argument>
void collectFreeVariables(const ast::NotPointer<Argument> &not_, std::vector<normalizedAST::VariableDeclaration *> &freeVariables, VariableStack &variableStack)
{
collectFreeVariables(not_->argument, freeVariables, variableStack);
}
////////////////////////////////////////////////////////////////////////////////////////////////////
template<class Argument>
void collectFreeVariables(const ast::OrPointer<Argument> &or_, std::vector<normalizedAST::VariableDeclaration *> &freeVariables, VariableStack &variableStack)
{
for (const auto &argument : or_->arguments)
collectFreeVariables(argument, freeVariables, variableStack);
}
////////////////////////////////////////////////////////////////////////////////////////////////////
void collectFreeVariables(const ast::UnsupportedPointer &unsupported, std::vector<normalizedAST::VariableDeclaration *> &, VariableStack &)
{
throw NormalizationException("cannot collect free variables of unsupported “" + unsupported->type + "” expression");
}
////////////////////////////////////////////////////////////////////////////////////////////////////
}
}
#endif

22
lib/pddlparse/src/pddlparse/detail/VariableStack.cpp
View File

@ -51,5 +51,27 @@ std::experimental::optional<ast::VariableDeclaration *> VariableStack::findVaria
////////////////////////////////////////////////////////////////////////////////////////////////////
bool VariableStack::contains(const ast::VariableDeclaration &variableDeclaration) const
{
const auto variableDeclarationMatches =
[&](const auto &other)
{
return &variableDeclaration == other.get();
};
for (auto i = m_layers.rbegin(); i != m_layers.rend(); i++)
{
auto &layer = **i;
const auto matchingVariableDeclaration = std::find_if(layer.begin(), layer.end(), variableDeclarationMatches);
if (matchingVariableDeclaration != layer.end())
return true;
}
return false;
}
////////////////////////////////////////////////////////////////////////////////////////////////////
}
}

230
lib/pddlparse/src/pddlparse/detail/normalization/Precondition.cpp
View File

@ -4,6 +4,7 @@
#include <pddlparse/Exception.h>
#include <pddlparse/NormalizedAST.h>
#include <pddlparse/detail/normalization/AtomicFormula.h>
#include <pddlparse/detail/normalization/CollectFreeVariables.h>
namespace pddl
{
@ -16,69 +17,173 @@ namespace detail
//
////////////////////////////////////////////////////////////////////////////////////////////////////
normalizedAST::DerivedPredicatePointer addDerivedPredicate(normalizedAST::DerivedPredicateDeclarations &derivedPredicates, const std::string &type)
////////////////////////////////////////////////////////////////////////////////////////////////////
// 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> &not_, 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> &&not_, normalizedAST::DerivedPredicateDeclarations &derivedPredicates);
normalizedAST::AndPointer<normalizedAST::Literal> normalize(ast::AndPointer<ast::Precondition> &&and_, normalizedAST::DerivedPredicateDeclarations &derivedPredicates);
////////////////////////////////////////////////////////////////////////////////////////////////////
normalizedAST::DerivedPredicatePointer addDerivedPredicate(const std::vector<normalizedAST::VariableDeclaration *> &parameters, normalizedAST::DerivedPredicateDeclarations &derivedPredicates)
{
auto name = "derived-" + type + "-" + std::to_string(derivedPredicates.size() + 1);
auto name = "derived-predicate-" + std::to_string(derivedPredicates.size() + 1);
derivedPredicates.emplace_back(std::make_unique<normalizedAST::DerivedPredicateDeclaration>(std::move(name), normalizedAST::VariableDeclarations()));
normalizedAST::DerivedPredicate::Arguments arguments;
arguments.reserve(parameters.size());
return std::make_unique<normalizedAST::DerivedPredicate>(normalizedAST::DerivedPredicate::Arguments(), derivedPredicates.back().get());
for (const auto &parameter : parameters)
arguments.emplace_back(std::make_unique<normalizedAST::Variable>(parameter));
derivedPredicates.emplace_back(std::make_unique<normalizedAST::DerivedPredicateDeclaration>());
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);
}
////////////////////////////////////////////////////////////////////////////////////////////////////
normalizedAST::DerivedPredicatePointer normalizeNested(ast::AndPointer<ast::Precondition> &, normalizedAST::DerivedPredicateDeclarations &derivedPredicates)
normalizedAST::Literal normalizeNested(ast::AndPointer<ast::Precondition> &and_, normalizedAST::DerivedPredicateDeclarations &derivedPredicates)
{
// TODO: handle arguments recursively
return addDerivedPredicate(derivedPredicates, "and");
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);
}
////////////////////////////////////////////////////////////////////////////////////////////////////
normalizedAST::DerivedPredicatePointer normalizeNested(ast::AtomicFormula &, normalizedAST::DerivedPredicateDeclarations &)
normalizedAST::Literal normalizeNested(ast::ExistsPointer<ast::Precondition> &exists, normalizedAST::DerivedPredicateDeclarations &derivedPredicates)
{
// TODO: add explanation
throw std::logic_error("atomic formulas should have been handled earlier");
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);
}
////////////////////////////////////////////////////////////////////////////////////////////////////
normalizedAST::DerivedPredicatePointer normalizeNested(ast::ExistsPointer<ast::Precondition> &, normalizedAST::DerivedPredicateDeclarations &derivedPredicates)
normalizedAST::Literal normalizeNested(ast::ForAllPointer<ast::Precondition> &, normalizedAST::DerivedPredicateDeclarations &)
{
// TODO: handle arguments recursively
return addDerivedPredicate(derivedPredicates, "exists");
// “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");
}
////////////////////////////////////////////////////////////////////////////////////////////////////
normalizedAST::DerivedPredicatePointer normalizeNested(ast::ForAllPointer<ast::Precondition> &, normalizedAST::DerivedPredicateDeclarations &derivedPredicates)
normalizedAST::Literal normalizeNested(ast::ImplyPointer<ast::Precondition> &, normalizedAST::DerivedPredicateDeclarations &)
{
// TODO: handle arguments recursively
return addDerivedPredicate(derivedPredicates, "forall");
// “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");
}
////////////////////////////////////////////////////////////////////////////////////////////////////
normalizedAST::DerivedPredicatePointer normalizeNested(ast::ImplyPointer<ast::Precondition> &, normalizedAST::DerivedPredicateDeclarations &derivedPredicates)
normalizedAST::Literal normalizeNested(ast::NotPointer<ast::Precondition> &not_, normalizedAST::DerivedPredicateDeclarations &derivedPredicates)
{
// TODO: handle arguments recursively
return addDerivedPredicate(derivedPredicates, "imply");
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);
}
////////////////////////////////////////////////////////////////////////////////////////////////////
normalizedAST::DerivedPredicatePointer normalizeNested(ast::NotPointer<ast::Precondition> &, normalizedAST::DerivedPredicateDeclarations &derivedPredicates)
normalizedAST::Literal normalizeNested(ast::OrPointer<ast::Precondition> &or_, normalizedAST::DerivedPredicateDeclarations &derivedPredicates)
{
// TODO: handle arguments recursively
return addDerivedPredicate(derivedPredicates, "not");
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::DerivedPredicatePointer normalizeNested(ast::OrPointer<ast::Precondition> &, normalizedAST::DerivedPredicateDeclarations &derivedPredicates)
normalizedAST::Literal normalizeNested(ast::UnsupportedPointer &unsupported, normalizedAST::DerivedPredicateDeclarations &)
{
// TODO: handle arguments recursively
return addDerivedPredicate(derivedPredicates, "or");
throw NormalizationException("“" + unsupported->type + "” expressions in preconditions can’t be normalized currently");
}
////////////////////////////////////////////////////////////////////////////////////////////////////
normalizedAST::Literal normalizeNested(ast::AtomicFormula &atomicFormula, normalizedAST::DerivedPredicateDeclarations &)
{
return normalize(std::move(atomicFormula));
}
////////////////////////////////////////////////////////////////////////////////////////////////////
@ -90,6 +195,13 @@ normalizedAST::PredicatePointer normalize(ast::UnsupportedPointer &&unsupported,
////////////////////////////////////////////////////////////////////////////////////////////////////
normalizedAST::AtomicFormula normalize(ast::AtomicFormula &&atomicFormula, normalizedAST::DerivedPredicateDeclarations &)
{
return normalize(std::move(atomicFormula));
}
////////////////////////////////////////////////////////////////////////////////////////////////////
// Normalize top-level negations
normalizedAST::NotPointer<normalizedAST::AtomicFormula> normalize(ast::NotPointer<ast::Precondition> &&not_, normalizedAST::DerivedPredicateDeclarations &derivedPredicates)
{
@ -97,19 +209,17 @@ normalizedAST::NotPointer<normalizedAST::AtomicFormula> normalize(ast::NotPointe
if (not_->argument.is<ast::AtomicFormula>())
return std::make_unique<normalizedAST::Not<normalizedAST::AtomicFormula>>(normalize(std::move(not_->argument.get<ast::AtomicFormula>())));
const auto handleNested =
auto normalizedArgument = not_->argument.match(
[&](auto &nested) -> normalizedAST::AtomicFormula
{
return normalizeNested(nested, derivedPredicates);
};
auto normalizedLiteral = normalizeNested(nested, derivedPredicates);
const auto handleUnsupported =
[&](ast::UnsupportedPointer &unsupported) -> normalizedAST::AtomicFormula
{
throw NormalizationException("“" + unsupported->type + "” expressions in preconditions can’t be normalized currently");
};
// 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");
auto normalizedArgument = not_->argument.match(handleNested, handleUnsupported);
return std::move(normalizedLiteral.template get<normalizedAST::AtomicFormula>());
});
return std::make_unique<normalizedAST::Not<normalizedAST::AtomicFormula>>(std::move(normalizedArgument));
}
@ -161,55 +271,11 @@ normalizedAST::AndPointer<normalizedAST::Literal> normalize(ast::AndPointer<ast:
normalizedAST::Precondition normalize(ast::Precondition &&precondition, normalizedAST::DerivedPredicateDeclarations &derivedPredicates)
{
/*
reduce
AtomicFormula,
AndPointer<Precondition>,
NotPointer<Precondition>,
UnsupportedPointer>;
ExistsPointer<Precondition>,
ForAllPointer<Precondition>,
ImplyPointer<Precondition>,
OrPointer<Precondition>,
to
Literal,
AndPointer<Literal>>;
*/
const auto handleAtomicFormula =
[&](ast::AtomicFormula &atomicFormula) -> normalizedAST::Precondition
return precondition.match(
[&](auto &x) -> normalizedAST::Precondition
{
return normalize(std::move(atomicFormula));
};
const auto handleNot =
[&](ast::NotPointer<ast::Precondition> &not_) -> normalizedAST::Precondition
{
return normalize(std::move(not_), derivedPredicates);
};
const auto handleAnd =
[&](ast::AndPointer<ast::Precondition> &and_) -> normalizedAST::Precondition
{
return normalize(std::move(and_), derivedPredicates);
};
const auto handleNested =
[&](auto &nested) -> normalizedAST::Precondition
{
return normalizeNested(nested, derivedPredicates);
};
const auto handleUnsupported =
[&](ast::UnsupportedPointer &unsupported) -> normalizedAST::Precondition
{
throw NormalizationException("“" + unsupported->type + "” expressions in preconditions can’t be normalized currently");
};
return precondition.match(handleAtomicFormula, handleNot, handleAnd, handleUnsupported, handleNested);
return normalize(std::move(x), derivedPredicates);
});
}
////////////////////////////////////////////////////////////////////////////////////////////////////