diff --git a/lib/pddlparse/include/pddlparse/NormalizedAST.h b/lib/pddlparse/include/pddlparse/NormalizedAST.h index 0e68ac8..841736b 100644 --- a/lib/pddlparse/include/pddlparse/NormalizedAST.h +++ b/lib/pddlparse/include/pddlparse/NormalizedAST.h @@ -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 &¶meters) - : 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 parameters; + VariableDeclarations existentialParameters; + std::experimental::optional precondition; +}; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + struct InitialState { InitialState() = default; diff --git a/lib/pddlparse/include/pddlparse/NormalizedASTForward.h b/lib/pddlparse/include/pddlparse/NormalizedASTForward.h index 54d50f0..9183677 100644 --- a/lib/pddlparse/include/pddlparse/NormalizedASTForward.h +++ b/lib/pddlparse/include/pddlparse/NormalizedASTForward.h @@ -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; //////////////////////////////////////////////////////////////////////////////////////////////////// +class DerivedPredicatePrecondition; + +namespace detail +{ +using DerivedPredicatePreconditionT = Variant< + Literal, + AndPointer, + OrPointer>; +} + +class DerivedPredicatePrecondition : public detail::DerivedPredicatePreconditionT +{ + using detail::DerivedPredicatePreconditionT::DerivedPredicatePreconditionT; +}; + +using DerivedPredicatePreconditions = std::vector; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + class ConditionalEffect; namespace detail diff --git a/lib/pddlparse/include/pddlparse/NormalizedASTOutput.h b/lib/pddlparse/include/pddlparse/NormalizedASTOutput.h index e7b0625..e7bc646 100644 --- a/lib/pddlparse/include/pddlparse/NormalizedASTOutput.h +++ b/lib/pddlparse/include/pddlparse/NormalizedASTOutput.h @@ -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 ¶meter : 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 ¶meter : derivedPredicateDeclaration.parameters) + { + if (¶meter != &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 ¶meter : 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()) diff --git a/lib/pddlparse/include/pddlparse/detail/VariableStack.h b/lib/pddlparse/include/pddlparse/detail/VariableStack.h index 2bcc46f..7482f6d 100644 --- a/lib/pddlparse/include/pddlparse/detail/VariableStack.h +++ b/lib/pddlparse/include/pddlparse/detail/VariableStack.h @@ -24,6 +24,7 @@ class VariableStack void pop(); std::experimental::optional findVariableDeclaration(const std::string &variableName); + bool contains(const ast::VariableDeclaration &variableDeclaration) const; private: std::vector m_layers; diff --git a/lib/pddlparse/include/pddlparse/detail/normalization/CollectFreeVariables.h b/lib/pddlparse/include/pddlparse/detail/normalization/CollectFreeVariables.h new file mode 100644 index 0000000..046a5f9 --- /dev/null +++ b/lib/pddlparse/include/pddlparse/detail/normalization/CollectFreeVariables.h @@ -0,0 +1,128 @@ +#ifndef __PDDL_PARSE__DETAIL__NORMALIZATION__COLLECT_FREE_VARIABLES_H +#define __PDDL_PARSE__DETAIL__NORMALIZATION__COLLECT_FREE_VARIABLES_H + +#include +#include +#include + +#include +#include + +namespace pddl +{ +namespace detail +{ + +//////////////////////////////////////////////////////////////////////////////////////////////////// +// +// Collect Free Variables +// +//////////////////////////////////////////////////////////////////////////////////////////////////// + +template +void collectFreeVariables(const Variant &variant, std::vector &freeVariables, VariableStack &variableStack) +{ + variant.match([&](const auto &x){collectFreeVariables(x, freeVariables, variableStack);}); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +void collectFreeVariables(const ast::ConstantPointer &, std::vector &, VariableStack &) +{ +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +void collectFreeVariables(const ast::VariablePointer &variable, std::vector &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 &freeVariables, VariableStack &variableStack) +{ + for (const auto &argument : predicate->arguments) + collectFreeVariables(argument, freeVariables, variableStack); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +template +void collectFreeVariables(const ast::AndPointer &and_, std::vector &freeVariables, VariableStack &variableStack) +{ + for (const auto &argument : and_->arguments) + collectFreeVariables(argument, freeVariables, variableStack); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +template +void collectFreeVariables(const ast::ExistsPointer &exists, std::vector &freeVariables, VariableStack &variableStack) +{ + variableStack.push(&exists->parameters); + + collectFreeVariables(exists->argument, freeVariables, variableStack); + + variableStack.pop(); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +template +void collectFreeVariables(const ast::ForAllPointer &forAll, std::vector &freeVariables, VariableStack &variableStack) +{ + variableStack.push(&forAll->parameters); + + collectFreeVariables(forAll->argument, freeVariables, variableStack); + + variableStack.pop(); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +template +void collectFreeVariables(const ast::ImplyPointer &imply, std::vector &freeVariables, VariableStack &variableStack) +{ + collectFreeVariables(imply->argumentLeft, freeVariables, variableStack); + collectFreeVariables(imply->argumentRight, freeVariables, variableStack); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +template +void collectFreeVariables(const ast::NotPointer ¬_, std::vector &freeVariables, VariableStack &variableStack) +{ + collectFreeVariables(not_->argument, freeVariables, variableStack); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +template +void collectFreeVariables(const ast::OrPointer &or_, std::vector &freeVariables, VariableStack &variableStack) +{ + for (const auto &argument : or_->arguments) + collectFreeVariables(argument, freeVariables, variableStack); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +void collectFreeVariables(const ast::UnsupportedPointer &unsupported, std::vector &, VariableStack &) +{ + throw NormalizationException("cannot collect free variables of unsupported “" + unsupported->type + "” expression"); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +} +} + +#endif diff --git a/lib/pddlparse/src/pddlparse/detail/VariableStack.cpp b/lib/pddlparse/src/pddlparse/detail/VariableStack.cpp index 0f4405b..7be8ab9 100644 --- a/lib/pddlparse/src/pddlparse/detail/VariableStack.cpp +++ b/lib/pddlparse/src/pddlparse/detail/VariableStack.cpp @@ -51,5 +51,27 @@ std::experimental::optional 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; +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + } } diff --git a/lib/pddlparse/src/pddlparse/detail/normalization/Precondition.cpp b/lib/pddlparse/src/pddlparse/detail/normalization/Precondition.cpp index e5f82bc..765c40a 100644 --- a/lib/pddlparse/src/pddlparse/detail/normalization/Precondition.cpp +++ b/lib/pddlparse/src/pddlparse/detail/normalization/Precondition.cpp @@ -4,6 +4,7 @@ #include #include #include +#include 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 &and_, normalizedAST::DerivedPredicateDeclarations &derivedPredicates); +normalizedAST::Literal normalizeNested(ast::ExistsPointer &exists, normalizedAST::DerivedPredicateDeclarations &derivedPredicates); +normalizedAST::Literal normalizeNested(ast::ForAllPointer &forAll, normalizedAST::DerivedPredicateDeclarations &derivedPredicates); +normalizedAST::Literal normalizeNested(ast::ImplyPointer &, normalizedAST::DerivedPredicateDeclarations &); +normalizedAST::Literal normalizeNested(ast::NotPointer ¬_, normalizedAST::DerivedPredicateDeclarations &derivedPredicates); +normalizedAST::Literal normalizeNested(ast::OrPointer &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 normalize(ast::NotPointer &¬_, normalizedAST::DerivedPredicateDeclarations &derivedPredicates); +normalizedAST::AndPointer normalize(ast::AndPointer &&and_, normalizedAST::DerivedPredicateDeclarations &derivedPredicates); + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +normalizedAST::DerivedPredicatePointer addDerivedPredicate(const std::vector ¶meters, 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(std::move(name), normalizedAST::VariableDeclarations())); + normalizedAST::DerivedPredicate::Arguments arguments; + arguments.reserve(parameters.size()); - return std::make_unique(normalizedAST::DerivedPredicate::Arguments(), derivedPredicates.back().get()); + for (const auto ¶meter : parameters) + arguments.emplace_back(std::make_unique(parameter)); + + derivedPredicates.emplace_back(std::make_unique()); + + auto *derivedPredicate = derivedPredicates.back().get(); + derivedPredicate->name = std::move(name); + derivedPredicate->parameters = std::move(parameters); + + return std::make_unique(std::move(arguments), derivedPredicate); } //////////////////////////////////////////////////////////////////////////////////////////////////// -normalizedAST::DerivedPredicatePointer normalizeNested(ast::AndPointer &, normalizedAST::DerivedPredicateDeclarations &derivedPredicates) +normalizedAST::Literal normalizeNested(ast::AndPointer &and_, normalizedAST::DerivedPredicateDeclarations &derivedPredicates) { - // TODO: handle arguments recursively - return addDerivedPredicate(derivedPredicates, "and"); + std::vector parameters; + VariableStack variableStack; + + collectFreeVariables(and_, parameters, variableStack); + + auto derivedPredicate = addDerivedPredicate(parameters, derivedPredicates); + + normalizedAST::And::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>(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 &exists, normalizedAST::DerivedPredicateDeclarations &derivedPredicates) { - // TODO: add explanation - throw std::logic_error("atomic formulas should have been handled earlier"); + std::vector 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 &, normalizedAST::DerivedPredicateDeclarations &derivedPredicates) +normalizedAST::Literal normalizeNested(ast::ForAllPointer &, 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 &, normalizedAST::DerivedPredicateDeclarations &derivedPredicates) +normalizedAST::Literal normalizeNested(ast::ImplyPointer &, 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 &, normalizedAST::DerivedPredicateDeclarations &derivedPredicates) +normalizedAST::Literal normalizeNested(ast::NotPointer ¬_, normalizedAST::DerivedPredicateDeclarations &derivedPredicates) { - // TODO: handle arguments recursively - return addDerivedPredicate(derivedPredicates, "imply"); + std::vector 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>()) + throw std::logic_error("precondition not in normal form (multiple negation), please report to the bug tracker"); + + auto &normalizedArgument = normalizedArgumentLiteral.get(); + + derivedPredicate->declaration->precondition = std::make_unique>(std::move(normalizedArgument)); + + // TODO: investigate, could be a compiler bug + return std::move(derivedPredicate); } //////////////////////////////////////////////////////////////////////////////////////////////////// -normalizedAST::DerivedPredicatePointer normalizeNested(ast::NotPointer &, normalizedAST::DerivedPredicateDeclarations &derivedPredicates) +normalizedAST::Literal normalizeNested(ast::OrPointer &or_, normalizedAST::DerivedPredicateDeclarations &derivedPredicates) { - // TODO: handle arguments recursively - return addDerivedPredicate(derivedPredicates, "not"); + std::vector parameters; + VariableStack variableStack; + + collectFreeVariables(or_, parameters, variableStack); + + auto derivedPredicate = addDerivedPredicate(parameters, derivedPredicates); + + normalizedAST::Or::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>(std::move(normalizedArguments)); + + // TODO: investigate, could be a compiler bug + return std::move(derivedPredicate); } //////////////////////////////////////////////////////////////////////////////////////////////////// -normalizedAST::DerivedPredicatePointer normalizeNested(ast::OrPointer &, 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 normalize(ast::NotPointer &¬_, normalizedAST::DerivedPredicateDeclarations &derivedPredicates) { @@ -97,19 +209,17 @@ normalizedAST::NotPointer normalize(ast::NotPointe if (not_->argument.is()) return std::make_unique>(normalize(std::move(not_->argument.get()))); - 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>()) + 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()); + }); return std::make_unique>(std::move(normalizedArgument)); } @@ -161,55 +271,11 @@ normalizedAST::AndPointer normalize(ast::AndPointer, - NotPointer, - UnsupportedPointer>; - - ExistsPointer, - ForAllPointer, - ImplyPointer, - OrPointer, - - to - - Literal, - AndPointer>; - */ - 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 ¬_) -> normalizedAST::Precondition - { - return normalize(std::move(not_), derivedPredicates); - }; - - const auto handleAnd = - [&](ast::AndPointer &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); + }); } ////////////////////////////////////////////////////////////////////////////////////////////////////