diff --git a/include/plasp/pddl/Action.h b/include/plasp/pddl/Action.h index c1ed856..50f820c 100644 --- a/include/plasp/pddl/Action.h +++ b/include/plasp/pddl/Action.h @@ -30,7 +30,7 @@ class Action const Expression *precondition() const; const Expression *effect() const; - void normalize(); + void normalize(expressions::DerivedPredicates &derivedPredicates); private: Action() = default; diff --git a/include/plasp/pddl/Expression.h b/include/plasp/pddl/Expression.h index 85a8c89..79b0c4f 100644 --- a/include/plasp/pddl/Expression.h +++ b/include/plasp/pddl/Expression.h @@ -2,6 +2,7 @@ #define __PLASP__PDDL__EXPRESSION_H #include +#include #include @@ -131,15 +132,21 @@ class Expression virtual ExpressionPointer copy(); + // Transform into a normal form as used for the translation to ASP ExpressionPointer normalized(); + // Reduce the set of used expressions (eliminates implications, for instance) virtual ExpressionPointer reduced(); - virtual ExpressionPointer negationNormalized(); - virtual ExpressionPointer prenex(Expression::Type lastQuantifierType = Expression::Type::Exists); + // Transform such that only existential (and no universal) quantifiers are used + virtual ExpressionPointer existentiallyQuantified(); + // Simplify the expression equivalently virtual ExpressionPointer simplified(); - virtual ExpressionPointer disjunctionNormalized(); + // Decompose expression into derived predicates (eliminate recursively nested expressions) virtual ExpressionPointer decomposed(expressions::DerivedPredicates &derivedPredicates); + // Negate the expression ExpressionPointer negated(); + virtual void collectParameters(std::set ¶meters); + virtual void print(std::ostream &ostream) const = 0; protected: diff --git a/include/plasp/pddl/TranslatorASP.h b/include/plasp/pddl/TranslatorASP.h index aac4843..ef71ac3 100644 --- a/include/plasp/pddl/TranslatorASP.h +++ b/include/plasp/pddl/TranslatorASP.h @@ -27,17 +27,13 @@ class TranslatorASP void translateDomain() const; void translateTypes() const; void translatePredicates() const; + void translateDerivedPredicates() const; void translateActions() const; void translateProblem() const; void translateInitialState() const; void translateGoal() const; - void translateConstants(const std::string &heading, const expressions::Constants &constants) const; - void translateVariablesHead(const expressions::Variables &variables) const; - void translateVariablesBody(const expressions::Variables &variables) const; - void translateLiteral(const Expression &literal) const; - void translatePredicate(const expressions::Predicate &predicate) const; Description &m_description; output::ColorStream &m_outputStream; diff --git a/include/plasp/pddl/expressions/And.h b/include/plasp/pddl/expressions/And.h index 97d885b..748d12e 100644 --- a/include/plasp/pddl/expressions/And.h +++ b/include/plasp/pddl/expressions/And.h @@ -24,7 +24,6 @@ class And: public NAry static const std::string Identifier; public: - ExpressionPointer disjunctionNormalized() override; ExpressionPointer decomposed(DerivedPredicates &derivedPredicates) override; }; diff --git a/include/plasp/pddl/expressions/At.h b/include/plasp/pddl/expressions/At.h index 1983ba8..b53e09e 100644 --- a/include/plasp/pddl/expressions/At.h +++ b/include/plasp/pddl/expressions/At.h @@ -40,10 +40,10 @@ class At: public ExpressionCRTP ExpressionPointer argument() const; ExpressionPointer reduced() override; - ExpressionPointer negationNormalized() override; - ExpressionPointer prenex(Expression::Type lastExpressionType) override; + ExpressionPointer existentiallyQuantified() override; ExpressionPointer simplified() override; - ExpressionPointer disjunctionNormalized() override; + + void collectParameters(std::set ¶meters) override; void print(std::ostream &ostream) const override; diff --git a/include/plasp/pddl/expressions/Binary.h b/include/plasp/pddl/expressions/Binary.h index fc6b8a2..e347f90 100644 --- a/include/plasp/pddl/expressions/Binary.h +++ b/include/plasp/pddl/expressions/Binary.h @@ -32,13 +32,14 @@ class Binary: public ExpressionCRTP ExpressionPointer copy() override; void setArgument(size_t i, ExpressionPointer argument); + std::array &arguments(); const std::array &arguments() const; ExpressionPointer reduced() override; - ExpressionPointer negationNormalized() override; - ExpressionPointer prenex(Expression::Type lastExpressionType) override; + ExpressionPointer existentiallyQuantified() override; ExpressionPointer simplified() override; - ExpressionPointer disjunctionNormalized() override; + + void collectParameters(std::set ¶meters) override; void print(std::ostream &ostream) const override; @@ -100,6 +101,14 @@ void Binary::setArgument(size_t i, ExpressionPointer expression) //////////////////////////////////////////////////////////////////////////////////////////////////// +template +std::array &Binary::arguments() +{ + return m_arguments; +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + template const std::array &Binary::arguments() const { @@ -111,11 +120,11 @@ const std::array &Binary::arguments() const template inline ExpressionPointer Binary::reduced() { - for (size_t i = 0; i < m_arguments.size(); i++) + for (auto &argument : m_arguments) { - BOOST_ASSERT(m_arguments[i]); + BOOST_ASSERT(argument); - m_arguments[i] = m_arguments[i]->reduced(); + argument = argument->reduced(); } return this; @@ -124,13 +133,13 @@ inline ExpressionPointer Binary::reduced() //////////////////////////////////////////////////////////////////////////////////////////////////// template -inline ExpressionPointer Binary::negationNormalized() +inline ExpressionPointer Binary::existentiallyQuantified() { - for (size_t i = 0; i < m_arguments.size(); i++) + for (auto &argument : m_arguments) { - BOOST_ASSERT(m_arguments[i]); + BOOST_ASSERT(argument); - m_arguments[i] = m_arguments[i]->negationNormalized(); + argument = argument->existentiallyQuantified(); } return this; @@ -138,23 +147,14 @@ inline ExpressionPointer Binary::negationNormalized() //////////////////////////////////////////////////////////////////////////////////////////////////// -template -inline ExpressionPointer Binary::prenex(Expression::Type) -{ - // TODO: implement by refactoring binary expressions - return this; -} - -//////////////////////////////////////////////////////////////////////////////////////////////////// - template inline ExpressionPointer Binary::simplified() { - for (size_t i = 0; i < m_arguments.size(); i++) + for (auto &argument : m_arguments) { - BOOST_ASSERT(m_arguments[i]); + BOOST_ASSERT(argument); - m_arguments[i] = m_arguments[i]->simplified(); + argument = argument->simplified(); } return this; @@ -163,16 +163,10 @@ inline ExpressionPointer Binary::simplified() //////////////////////////////////////////////////////////////////////////////////////////////////// template -inline ExpressionPointer Binary::disjunctionNormalized() +inline void Binary::collectParameters(std::set ¶meters) { - for (size_t i = 0; i < m_arguments.size(); i++) - { - BOOST_ASSERT(m_arguments[i]); - - m_arguments[i] = m_arguments[i]->disjunctionNormalized(); - } - - return this; + for (const auto &argument : m_arguments) + argument->collectParameters(parameters); } //////////////////////////////////////////////////////////////////////////////////////////////////// diff --git a/include/plasp/pddl/expressions/DerivedPredicate.h b/include/plasp/pddl/expressions/DerivedPredicate.h index 3bc3765..2ff0c38 100644 --- a/include/plasp/pddl/expressions/DerivedPredicate.h +++ b/include/plasp/pddl/expressions/DerivedPredicate.h @@ -1,6 +1,8 @@ #ifndef __PLASP__PDDL__EXPRESSIONS__DERIVED_PREDICATE_H #define __PLASP__PDDL__EXPRESSIONS__DERIVED_PREDICATE_H +#include + #include namespace plasp @@ -24,19 +26,22 @@ class DerivedPredicate: public ExpressionCRTP // TODO: consider implementing parsing functions for compatibility with older PDDL versions public: - explicit DerivedPredicate(size_t id); + void setPreconditions(std::vector &&preconditions); + const std::vector &preconditions() const; - size_t id() const; + const std::set ¶meters() const; - void setArgument(ExpressionPointer argument); - ExpressionPointer argument() const; + void collectParameters(std::set ¶meters) override; void print(std::ostream &ostream) const override; private: - size_t m_id; + void collectParameters(); - ExpressionPointer m_argument; + // The arguments are interpreted as a disjunction of conjunctions + std::vector m_preconditions; + + std::set m_parameters; }; //////////////////////////////////////////////////////////////////////////////////////////////////// diff --git a/include/plasp/pddl/expressions/Exists.h b/include/plasp/pddl/expressions/Exists.h index 6f05108..815b34f 100644 --- a/include/plasp/pddl/expressions/Exists.h +++ b/include/plasp/pddl/expressions/Exists.h @@ -22,9 +22,6 @@ class Exists: public QuantifiedCRTP static const Expression::Type ExpressionType = Expression::Type::Exists; static const std::string Identifier; - - public: - ExpressionPointer decomposed(DerivedPredicates &derivedPredicates) override; }; //////////////////////////////////////////////////////////////////////////////////////////////////// diff --git a/include/plasp/pddl/expressions/ForAll.h b/include/plasp/pddl/expressions/ForAll.h index 369f601..1d2f47c 100644 --- a/include/plasp/pddl/expressions/ForAll.h +++ b/include/plasp/pddl/expressions/ForAll.h @@ -24,7 +24,7 @@ class ForAll: public QuantifiedCRTP static const std::string Identifier; public: - ExpressionPointer decomposed(DerivedPredicates &derivedPredicates) override; + ExpressionPointer existentiallyQuantified() override; }; //////////////////////////////////////////////////////////////////////////////////////////////////// diff --git a/include/plasp/pddl/expressions/NAry.h b/include/plasp/pddl/expressions/NAry.h index 9c26278..5951042 100644 --- a/include/plasp/pddl/expressions/NAry.h +++ b/include/plasp/pddl/expressions/NAry.h @@ -37,10 +37,10 @@ class NAry: public ExpressionCRTP const Expressions &arguments() const; ExpressionPointer reduced() override; - ExpressionPointer negationNormalized() override; - ExpressionPointer prenex(Expression::Type lastExpressionType) override; + ExpressionPointer existentiallyQuantified() override; ExpressionPointer simplified() override; - ExpressionPointer disjunctionNormalized() override; + + void collectParameters(std::set ¶meters) override; void print(std::ostream &ostream) const override; @@ -143,11 +143,11 @@ Expressions &NAry::arguments() template inline ExpressionPointer NAry::reduced() { - for (size_t i = 0; i < m_arguments.size(); i++) + for (auto &argument : m_arguments) { - BOOST_ASSERT(m_arguments[i]); + BOOST_ASSERT(argument); - m_arguments[i] = m_arguments[i]->reduced(); + argument = argument->reduced(); } return this; @@ -156,13 +156,13 @@ inline ExpressionPointer NAry::reduced() //////////////////////////////////////////////////////////////////////////////////////////////////// template -inline ExpressionPointer NAry::negationNormalized() +inline ExpressionPointer NAry::existentiallyQuantified() { - for (size_t i = 0; i < m_arguments.size(); i++) + for (auto &argument : m_arguments) { - BOOST_ASSERT(m_arguments[i]); + BOOST_ASSERT(argument); - m_arguments[i] = m_arguments[i]->negationNormalized(); + argument = argument->existentiallyQuantified(); } return this; @@ -170,106 +170,22 @@ inline ExpressionPointer NAry::negationNormalized() //////////////////////////////////////////////////////////////////////////////////////////////////// -template -inline ExpressionPointer NAry::prenex(Expression::Type lastExpressionType) -{ - // First, move all childrens’ quantifiers to the front - for (size_t i = 0; i < m_arguments.size(); i++) - { - BOOST_ASSERT(m_arguments[i]); - - m_arguments[i] = m_arguments[i]->prenex(lastExpressionType); - } - - // Next, move all children’s quantifiers up - - const auto isQuantifier = - [](const auto &expression) - { - return expression->expressionType() == Expression::Type::Exists - || expression->expressionType() == Expression::Type::ForAll; - }; - - QuantifiedPointer front = nullptr; - QuantifiedPointer back = nullptr; - - const auto moveUpQuantifiers = - [&](auto &child, const auto expressionType) - { - BOOST_ASSERT(child); - - bool changed = false; - - while (isQuantifier(child) - && child->expressionType() == expressionType) - { - // Decouple quantifier from tree and replace it with its child - auto expression = Expression::moveUpQuantifiers(nullptr, child); - auto quantifier = QuantifiedPointer(dynamic_cast(expression.get())); - - if (!front) - front = quantifier; - else - back->setArgument(quantifier); - - back = quantifier; - - changed = true; - } - - return changed; - }; - - bool changed = true; - const auto otherExpressionType = (lastExpressionType == Expression::Type::Exists) - ? Expression::Type::ForAll : Expression::Type::Exists; - - // Group quantifiers of the same type when moving them up, starting with the parent quantifier’s type - while (changed) - { - changed = false; - - // Group all quantifiers of the same type as the parent quantifier - for (size_t i = 0; i < m_arguments.size(); i++) - changed = moveUpQuantifiers(m_arguments[i], lastExpressionType) || changed; - - // Group all other quantifiers - for (size_t i = 0; i < m_arguments.size(); i++) - changed = moveUpQuantifiers(m_arguments[i], otherExpressionType) || changed; - } - - // If quantifiers were moved up, put this node back into the node hierarchy - if (front) - { - BOOST_ASSERT(back); - - back->setArgument(this); - - return front; - } - - // If no quantifiers were moved up, simply return this node - return this; -} - -//////////////////////////////////////////////////////////////////////////////////////////////////// - template inline ExpressionPointer NAry::simplified() { // Associate same-type children, such as (a && (b && c)) == (a && b && c) for (size_t i = 0; i < m_arguments.size();) { - m_arguments[i] = m_arguments[i]->simplified(); + auto &argument = m_arguments[i]; + argument = argument->simplified(); - if (m_arguments[i]->expressionType() != Derived::ExpressionType) + if (argument->expressionType() != Derived::ExpressionType) { i++; continue; } - auto child = m_arguments[i]; - auto &nAryExpression = dynamic_cast(*child); + auto &nAryExpression = dynamic_cast(*argument); BOOST_ASSERT(!nAryExpression.arguments().empty()); @@ -292,16 +208,10 @@ inline ExpressionPointer NAry::simplified() //////////////////////////////////////////////////////////////////////////////////////////////////// template -inline ExpressionPointer NAry::disjunctionNormalized() +inline void NAry::collectParameters(std::set ¶meters) { - for (size_t i = 0; i < m_arguments.size(); i++) - { - BOOST_ASSERT(m_arguments[i]); - - m_arguments[i] = m_arguments[i]->disjunctionNormalized(); - } - - return this; + for (const auto &argument : m_arguments) + argument->collectParameters(parameters); } //////////////////////////////////////////////////////////////////////////////////////////////////// @@ -311,12 +221,11 @@ inline void NAry::print(std::ostream &ostream) const { ostream << "(" << Derived::Identifier; - std::for_each(m_arguments.begin(), m_arguments.end(), - [&](auto &argument) - { - ostream << " "; - argument->print(ostream); - }); + for (const auto &argument : m_arguments) + { + ostream << " "; + argument->print(ostream); + } ostream << ")"; } diff --git a/include/plasp/pddl/expressions/Not.h b/include/plasp/pddl/expressions/Not.h index 600bd65..d59ae19 100644 --- a/include/plasp/pddl/expressions/Not.h +++ b/include/plasp/pddl/expressions/Not.h @@ -35,12 +35,12 @@ class Not: public ExpressionCRTP ExpressionPointer argument() const; ExpressionPointer reduced() override; - ExpressionPointer negationNormalized() override; - ExpressionPointer prenex(Expression::Type lastExpressionType) override; + ExpressionPointer existentiallyQuantified() override; ExpressionPointer simplified() override; - ExpressionPointer disjunctionNormalized() override; ExpressionPointer decomposed(DerivedPredicates &derivedPredicates) override; + void collectParameters(std::set ¶meters) override; + void print(std::ostream &ostream) const override; protected: diff --git a/include/plasp/pddl/expressions/Predicate.h b/include/plasp/pddl/expressions/Predicate.h index 3dd81c3..e2eba12 100644 --- a/include/plasp/pddl/expressions/Predicate.h +++ b/include/plasp/pddl/expressions/Predicate.h @@ -30,6 +30,10 @@ class Predicate: public ExpressionCRTP bool isDeclared() const; + ExpressionPointer decomposed(expressions::DerivedPredicates &derivedPredicates) override; + + void collectParameters(std::set ¶meters) override; + void print(std::ostream &ostream) const override; private: diff --git a/include/plasp/pddl/expressions/Quantified.h b/include/plasp/pddl/expressions/Quantified.h index 192e420..3ba2bd9 100644 --- a/include/plasp/pddl/expressions/Quantified.h +++ b/include/plasp/pddl/expressions/Quantified.h @@ -4,6 +4,7 @@ #include #include #include +#include #include namespace plasp @@ -52,10 +53,11 @@ class QuantifiedCRTP: public Quantified ExpressionPointer copy() override; ExpressionPointer reduced() override; - ExpressionPointer negationNormalized() override; - ExpressionPointer prenex(Expression::Type lastExpressionType) override; + ExpressionPointer existentiallyQuantified() override; ExpressionPointer simplified() override; - ExpressionPointer disjunctionNormalized() override; + ExpressionPointer decomposed(expressions::DerivedPredicates &derivedPredicates) override; + + void collectParameters(std::set ¶meters); void print(std::ostream &ostream) const override; }; @@ -155,30 +157,17 @@ inline ExpressionPointer QuantifiedCRTP::reduced() //////////////////////////////////////////////////////////////////////////////////////////////////// template -inline ExpressionPointer QuantifiedCRTP::negationNormalized() +inline ExpressionPointer QuantifiedCRTP::existentiallyQuantified() { BOOST_ASSERT(m_argument); - m_argument = m_argument->negationNormalized(); + m_argument = m_argument->existentiallyQuantified(); return this; } //////////////////////////////////////////////////////////////////////////////////////////////////// -template -inline ExpressionPointer QuantifiedCRTP::prenex(Expression::Type) -{ - BOOST_ASSERT(m_argument); - - m_argument = m_argument->prenex(Derived::ExpressionType); - - // Quantifiers may not move before other quantifiers, their order matters - return this; -} - -//////////////////////////////////////////////////////////////////////////////////////////////////// - template inline ExpressionPointer QuantifiedCRTP::simplified() { @@ -206,13 +195,28 @@ inline ExpressionPointer QuantifiedCRTP::simplified() //////////////////////////////////////////////////////////////////////////////////////////////////// template -inline ExpressionPointer QuantifiedCRTP::disjunctionNormalized() +inline ExpressionPointer QuantifiedCRTP::decomposed(expressions::DerivedPredicates &derivedPredicates) { - BOOST_ASSERT(m_argument); + derivedPredicates.emplace_back(new DerivedPredicate()); + auto &derivedPredicate = derivedPredicates.back(); - m_argument = m_argument->disjunctionNormalized(); + m_argument = m_argument->decomposed(derivedPredicates); - return this; + derivedPredicate->setPreconditions({{this}}); + + return derivedPredicate; +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +template +inline void QuantifiedCRTP::collectParameters(std::set ¶meters) +{ + m_argument->collectParameters(parameters); + + // Remove bound variables + for (const auto &variable : m_variables) + parameters.erase(variable); } //////////////////////////////////////////////////////////////////////////////////////////////////// diff --git a/include/plasp/pddl/expressions/Variable.h b/include/plasp/pddl/expressions/Variable.h index 7b6d890..4c76abe 100644 --- a/include/plasp/pddl/expressions/Variable.h +++ b/include/plasp/pddl/expressions/Variable.h @@ -39,6 +39,8 @@ class Variable: public ExpressionCRTP void setDirty(bool isDirty = true); bool isDirty() const; + void collectParameters(std::set ¶meters) override; + void print(std::ostream &ostream) const override; private: diff --git a/src/plasp/pddl/Action.cpp b/src/plasp/pddl/Action.cpp index 657b68a..8e29923 100644 --- a/src/plasp/pddl/Action.cpp +++ b/src/plasp/pddl/Action.cpp @@ -88,10 +88,10 @@ const Expression *Action::effect() const //////////////////////////////////////////////////////////////////////////////////////////////////// -void Action::normalize() +void Action::normalize(expressions::DerivedPredicates &derivedPredicates) { // Normalize preconditions and effects - m_precondition = m_precondition->normalized(); + m_precondition = m_precondition->normalized()->decomposed(derivedPredicates); m_effect = m_effect->normalized(); // Normalize parameter names diff --git a/src/plasp/pddl/Domain.cpp b/src/plasp/pddl/Domain.cpp index 07f0cfe..216f3ce 100644 --- a/src/plasp/pddl/Domain.cpp +++ b/src/plasp/pddl/Domain.cpp @@ -438,9 +438,9 @@ void Domain::normalize() }); std::for_each(m_actions.begin(), m_actions.end(), - [](auto &action) + [&](auto &action) { - action->normalize(); + action->normalize(m_derivedPredicates); }); } diff --git a/src/plasp/pddl/Expression.cpp b/src/plasp/pddl/Expression.cpp index 70f811e..50073f5 100644 --- a/src/plasp/pddl/Expression.cpp +++ b/src/plasp/pddl/Expression.cpp @@ -37,7 +37,7 @@ ExpressionPointer Expression::copy() ExpressionPointer Expression::normalized() { - return reduced()->negationNormalized()->prenex()->simplified()->disjunctionNormalized()->simplified(); + return reduced()->simplified()->existentiallyQuantified()->simplified(); } //////////////////////////////////////////////////////////////////////////////////////////////////// @@ -49,17 +49,11 @@ ExpressionPointer Expression::reduced() //////////////////////////////////////////////////////////////////////////////////////////////////// -ExpressionPointer Expression::negationNormalized() +ExpressionPointer Expression::existentiallyQuantified() { return this; } -//////////////////////////////////////////////////////////////////////////////////////////////////// - -ExpressionPointer Expression::prenex(Expression::Type) -{ - return this; -} //////////////////////////////////////////////////////////////////////////////////////////////////// @@ -106,16 +100,9 @@ ExpressionPointer Expression::simplified() //////////////////////////////////////////////////////////////////////////////////////////////////// -ExpressionPointer Expression::disjunctionNormalized() -{ - return this; -} - -//////////////////////////////////////////////////////////////////////////////////////////////////// - [[ noreturn ]] ExpressionPointer Expression::decomposed(expressions::DerivedPredicates &) { - throw output::TranslatorException("Expression is not in first-order negation normal form and cannot be decomposed"); + throw output::TranslatorException("expression cannot be decomposed (not normalized)"); } //////////////////////////////////////////////////////////////////////////////////////////////////// @@ -137,6 +124,14 @@ ExpressionPointer Expression::negated() //////////////////////////////////////////////////////////////////////////////////////////////////// +// TODO: implement better (visitor pattern?) +void Expression::collectParameters(std::set &) +{ + throw output::TranslatorException("expression parameters could not be collected (expression not normalized)"); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + ExpressionPointer parseEffectBodyExpression(Context &context, ExpressionContext &expressionContext); ExpressionPointer parsePredicate(Context &context, ExpressionContext &expressionContext); diff --git a/src/plasp/pddl/TranslatorASP.cpp b/src/plasp/pddl/TranslatorASP.cpp index 8f11828..dc49af0 100644 --- a/src/plasp/pddl/TranslatorASP.cpp +++ b/src/plasp/pddl/TranslatorASP.cpp @@ -19,6 +19,15 @@ namespace pddl // //////////////////////////////////////////////////////////////////////////////////////////////////// +template +void translateVariablesHead(output::ColorStream &outputStream, const T &variables); +template +void translateVariablesBody(output::ColorStream &outputStream, const T &variables); +void translateLiteral(output::ColorStream &outputStream, const Expression &literal); +void translatePredicate(output::ColorStream &outputStream, const expressions::Predicate &predicate); + +//////////////////////////////////////////////////////////////////////////////////////////////////// + TranslatorASP::TranslatorASP(Description &description, output::ColorStream &outputStream) : m_description(description), m_outputStream(outputStream) @@ -65,6 +74,13 @@ void TranslatorASP::translateDomain() const translatePredicates(); } + // Derived predicates + if (!domain.derivedPredicates().empty()) + { + m_outputStream << std::endl; + translateDerivedPredicates(); + } + // Actions if (!domain.actions().empty()) { @@ -146,7 +162,7 @@ void TranslatorASP::translatePredicates() const } m_outputStream << "(" << output::String(predicate->name().c_str()); - this->translateVariablesHead(predicate->arguments()); + translateVariablesHead(m_outputStream, predicate->arguments()); m_outputStream << ")"; }; @@ -162,7 +178,65 @@ void TranslatorASP::translatePredicates() const m_outputStream << "))"; - this->translateVariablesBody(predicate->arguments()); + translateVariablesBody(m_outputStream, predicate->arguments()); + + m_outputStream << "."; + }); + + m_outputStream + << std::endl << std::endl + << output::Function("boolean") << "(" << output::Boolean("true") << ")." << std::endl + << output::Function("boolean") << "(" << output::Boolean("false") << ")." << std::endl + << std::endl + << output::Function("contains") << "(" + << output::Keyword("variable") << "(" << output::Variable("X") << "), " + << output::Keyword("value") << "(" << output::Variable("X") << ", " << output::Variable("B") << ")) :- " + << output::Function("variable") << "(" << output::Keyword("variable") << "(" << output::Variable("X") << ")), " + << output::Function("boolean") << "(" << output::Variable("B") << ")." + << std::endl; +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +void TranslatorASP::translateDerivedPredicates() const +{ + m_outputStream << output::Heading2("derived predicates"); + + const auto &derivedPredicates = m_description.domain().derivedPredicates(); + + const auto printDerivedPredicateName = + [&](const auto &derivedPredicate) + { + if (derivedPredicate->parameters().empty()) + { + // TODO: implement + //m_outputStream << output::String(derivedPredicate->name().c_str()); + m_outputStream << ""; + + return; + } + + // TODO: implement + //m_outputStream << output::String(derivedPredicate->name().c_str()); + m_outputStream << ""; + translateVariablesHead(m_outputStream, derivedPredicate->parameters()); + m_outputStream << ")"; + }; + + std::for_each(derivedPredicates.cbegin(), derivedPredicates.cend(), + [&](const auto &predicate) + { + m_outputStream + << std::endl + << output::Function("variable") << "(" + << output::Keyword("variable") << "("; + + printDerivedPredicateName(predicate); + + m_outputStream << "))"; + + // TODO: implement + //translateVariablesBody(m_outputStream, predicate->arguments()); m_outputStream << "."; }); @@ -201,15 +275,14 @@ void TranslatorASP::translateActions() const } m_outputStream << "(" << output::String(action.name().c_str()); - this->translateVariablesHead(action.parameters()); + translateVariablesHead(m_outputStream, action.parameters()); m_outputStream << "))"; }; std::for_each(actions.cbegin(), actions.cend(), [&](const auto &action) { - // TODO: rename - const auto translateLiteral = + const auto translateExpression = [&](const auto &ruleHead, const auto &literal, bool enumerateEffects = false) { m_outputStream << std::endl << output::Function(ruleHead) << "("; @@ -222,7 +295,7 @@ void TranslatorASP::translateActions() const m_outputStream << ", "; - this->translateLiteral(literal); + translateLiteral(m_outputStream, literal); m_outputStream << ") :- " << output::Function("action") << "("; @@ -238,7 +311,7 @@ void TranslatorASP::translateActions() const printActionName(*action); m_outputStream << ")"; - this->translateVariablesBody(action->parameters()); + translateVariablesBody(m_outputStream, action->parameters()); m_outputStream << "."; @@ -247,24 +320,29 @@ void TranslatorASP::translateActions() const { const auto &precondition = *action->precondition(); - if (precondition.expressionType() == Expression::Type::Predicate - || precondition.expressionType() == Expression::Type::Not) + switch (precondition.expressionType()) { - translateLiteral("precondition", precondition); - } - // Assuming a conjunction - else - { - if (precondition.expressionType() != Expression::Type::And) - throw output::TranslatorException("only “and” expressions and (negated) predicates supported as action preconditions currently"); + case Expression::Type::And: + { + const auto &andExpression = dynamic_cast(precondition); - const auto &andExpression = dynamic_cast(precondition); + std::for_each(andExpression.arguments().cbegin(), andExpression.arguments().cend(), + [&](const auto argument) + { + translateExpression("precondition", *argument); + }); - std::for_each(andExpression.arguments().cbegin(), andExpression.arguments().cend(), - [&](const auto argument) - { - translateLiteral("precondition", *argument); - }); + break; + } + case Expression::Type::Predicate: + case Expression::Type::Not: + case Expression::Type::DerivedPredicate: + { + translateExpression("precondition", precondition); + break; + } + default: + throw output::TranslatorException("only “and” expressions and (negated) predicates supported as action preconditions currently (" + std::to_string((int)precondition.expressionType()) + ")"); } } @@ -276,7 +354,7 @@ void TranslatorASP::translateActions() const if (effect.expressionType() == Expression::Type::Predicate || effect.expressionType() == Expression::Type::Not) { - translateLiteral("postcondition", effect, true); + translateExpression("postcondition", effect, true); } // Assuming a conjunction else @@ -289,7 +367,7 @@ void TranslatorASP::translateActions() const std::for_each(andExpression.arguments().cbegin(), andExpression.arguments().cend(), [&](const auto argument) { - translateLiteral("postcondition", *argument, true); + translateExpression("postcondition", *argument, true); }); } } @@ -332,7 +410,8 @@ void TranslatorASP::translateConstants(const std::string &heading, const express //////////////////////////////////////////////////////////////////////////////////////////////////// -void TranslatorASP::translateVariablesHead(const expressions::Variables &variables) const +template +void translateVariablesHead(output::ColorStream &outputStream, const T &variables) { if (variables.empty()) return; @@ -341,25 +420,26 @@ void TranslatorASP::translateVariablesHead(const expressions::Variables &variabl { const auto &variable = **i; - m_outputStream << ", " << output::Variable(variable.name().c_str()); + outputStream << ", " << output::Variable(variable.name().c_str()); } } //////////////////////////////////////////////////////////////////////////////////////////////////// -void TranslatorASP::translateVariablesBody(const expressions::Variables &variables) const +template +void translateVariablesBody(output::ColorStream &outputStream, const T &variables) { if (variables.empty()) return; - m_outputStream << " :- "; + outputStream << " :- "; for (auto i = variables.cbegin(); i != variables.cend(); i++) { const auto &variable = **i; if (i != variables.cbegin()) - m_outputStream << ", "; + outputStream << ", "; if (variable.type() != nullptr) { @@ -368,13 +448,13 @@ void TranslatorASP::translateVariablesBody(const expressions::Variables &variabl const auto &type = dynamic_cast(*variable.type()); - m_outputStream << output::Function("has") << "(" + outputStream << output::Function("has") << "(" << output::Variable(variable.name().c_str()) << ", " << output::Keyword("type") << "(" << output::String(type.name().c_str()) << "))"; } else { - m_outputStream << output::Function("has") << "(" + outputStream << output::Function("has") << "(" << output::Variable(variable.name().c_str()) << ", " << output::Keyword("type") << "(" << output::String("object") << "))"; } @@ -383,18 +463,18 @@ void TranslatorASP::translateVariablesBody(const expressions::Variables &variabl //////////////////////////////////////////////////////////////////////////////////////////////////// -void TranslatorASP::translateLiteral(const Expression &literal) const +void translateLiteral(output::ColorStream &outputStream, const Expression &literal) { // Translate single predicate if (literal.expressionType() == Expression::Type::Predicate) { const auto &predicate = dynamic_cast(literal); - m_outputStream << output::Keyword("variable") << "("; - this->translatePredicate(predicate); - m_outputStream << "), " << output::Keyword("value") << "("; - this->translatePredicate(predicate); - m_outputStream << ", " << output::Boolean("true") << ")"; + outputStream << output::Keyword("variable") << "("; + translatePredicate(outputStream, predicate); + outputStream << "), " << output::Keyword("value") << "("; + translatePredicate(outputStream, predicate); + outputStream << ", " << output::Boolean("true") << ")"; } // Assuming that "not" expression may only contain a predicate else if (literal.expressionType() == Expression::Type::Not) @@ -406,11 +486,23 @@ void TranslatorASP::translateLiteral(const Expression &literal) const const auto &predicate = dynamic_cast(*notExpression.argument()); - m_outputStream << output::Keyword("variable") << "("; + outputStream << output::Keyword("variable") << "("; + translatePredicate(outputStream, predicate); + outputStream << "), " << output::Keyword("value") << "("; + translatePredicate(outputStream, predicate); + outputStream << ", " << output::Boolean("false") << ")"; + } + else if (literal.expressionType() == Expression::Type::DerivedPredicate) + { + const auto &derivedPredicate = dynamic_cast(literal); + + /*m_outputStream << output::Keyword("variable") << "("; this->translatePredicate(predicate); m_outputStream << "), " << output::Keyword("value") << "("; this->translatePredicate(predicate); - m_outputStream << ", " << output::Boolean("false") << ")"; + m_outputStream << ", " << output::Boolean("true") << ")";*/ + + outputStream << "(derived predicate)"; } else throw output::TranslatorException("only primitive predicates and their negations supported as literals currently"); @@ -418,40 +510,40 @@ void TranslatorASP::translateLiteral(const Expression &literal) const //////////////////////////////////////////////////////////////////////////////////////////////////// -void TranslatorASP::translatePredicate(const expressions::Predicate &predicate) const +void translatePredicate(output::ColorStream &outputStream, const expressions::Predicate &predicate) { const auto &arguments = predicate.arguments(); if (arguments.empty()) { - m_outputStream << output::String(predicate.name().c_str()); + outputStream << output::String(predicate.name().c_str()); return; } - m_outputStream << "(" << output::String(predicate.name().c_str()); + outputStream << "(" << output::String(predicate.name().c_str()); for (auto i = arguments.cbegin(); i != arguments.cend(); i++) { - m_outputStream << ", "; + outputStream << ", "; if ((*i)->expressionType() == Expression::Type::Constant) { const auto &constant = dynamic_cast(**i); - m_outputStream << output::Keyword("constant") << "(" << output::String(constant.name().c_str()) << ")"; + outputStream << output::Keyword("constant") << "(" << output::String(constant.name().c_str()) << ")"; } else if ((*i)->expressionType() == Expression::Type::Variable) { const auto &variable = dynamic_cast(**i); - m_outputStream << output::Variable(variable.name().c_str()); + outputStream << output::Variable(variable.name().c_str()); } else throw output::TranslatorException("only variables and constants supported in predicates currently"); } - m_outputStream << ")"; + outputStream << ")"; } //////////////////////////////////////////////////////////////////////////////////////////////////// @@ -501,9 +593,9 @@ void TranslatorASP::translateInitialState() const const auto &predicate = dynamic_cast(*fact); m_outputStream << output::Keyword("variable") << "("; - this->translatePredicate(predicate); + translatePredicate(m_outputStream, predicate); m_outputStream << "), " << output::Keyword("value") << "("; - this->translatePredicate(predicate); + translatePredicate(m_outputStream, predicate); m_outputStream << ", " << output::Boolean("true") << ")"; } // Assuming that "not" expression may only contain a predicate @@ -548,7 +640,7 @@ void TranslatorASP::translateGoal() const { m_outputStream << std::endl << output::Function("goal") << "("; - translateLiteral(goal); + translateLiteral(m_outputStream, goal); m_outputStream << ")."; } @@ -561,7 +653,7 @@ void TranslatorASP::translateGoal() const { m_outputStream << std::endl << output::Function("goal") << "("; - this->translateLiteral(*argument); + translateLiteral(m_outputStream, *argument); m_outputStream << ")."; }); diff --git a/src/plasp/pddl/expressions/And.cpp b/src/plasp/pddl/expressions/And.cpp index 68cb0df..77cf11d 100644 --- a/src/plasp/pddl/expressions/And.cpp +++ b/src/plasp/pddl/expressions/And.cpp @@ -23,70 +23,18 @@ const std::string And::Identifier = "and"; //////////////////////////////////////////////////////////////////////////////////////////////////// -ExpressionPointer And::disjunctionNormalized() -{ - for (size_t i = 0; i < m_arguments.size(); i++) - { - BOOST_ASSERT(m_arguments[i]); - - m_arguments[i] = m_arguments[i]->disjunctionNormalized(); - } - - const auto match = std::find_if(m_arguments.begin(), m_arguments.end(), - [](const auto &argument) - { - return argument->expressionType() == Expression::Type::Or; - }); - - if (match == m_arguments.end()) - return this; - - auto orExpression = OrPointer(dynamic_cast(match->get())); - const size_t orExpressionIndex = match - m_arguments.begin(); - - // Apply the distributive law - // Copy this and expression for each argument of the or expression - for (size_t i = 0; i < orExpression->arguments().size(); i++) - { - auto newAndExpression = new expressions::And; - newAndExpression->arguments().resize(m_arguments.size()); - - for (size_t j = 0; j < m_arguments.size(); j++) - { - if (j == orExpressionIndex) - newAndExpression->arguments()[j] = orExpression->arguments()[i]->copy(); - else - newAndExpression->arguments()[j] = m_arguments[j]->copy(); - } - - // Replace the respective argument with the new, recursively normalized and expression - orExpression->arguments()[i] = newAndExpression->disjunctionNormalized(); - } - - return orExpression; -} - -//////////////////////////////////////////////////////////////////////////////////////////////////// - ExpressionPointer And::decomposed(DerivedPredicates &derivedPredicates) { - // Check that all children are simple or negated predicates - std::for_each(m_arguments.begin(), m_arguments.end(), - [&](auto &argument) - { - if (argument->expressionType() == Expression::Type::Not) - { - argument = argument->decomposed(derivedPredicates); - return; - } + derivedPredicates.emplace_back(new DerivedPredicate()); + auto &derivedPredicate = derivedPredicates.back(); - if (argument->expressionType() != Expression::Type::Predicate) - return; + for (auto &argument : m_arguments) + argument = argument->decomposed(derivedPredicates); - throw output::TranslatorException("Expression is not in first-order negation normal form and cannot be decomposed"); - }); + // Move this expression’s arguments to the derived predicate + derivedPredicate->setPreconditions({m_arguments}); - return this; + return derivedPredicate; } //////////////////////////////////////////////////////////////////////////////////////////////////// diff --git a/src/plasp/pddl/expressions/At.cpp b/src/plasp/pddl/expressions/At.cpp index 2b9c6a2..c3d1f84 100644 --- a/src/plasp/pddl/expressions/At.cpp +++ b/src/plasp/pddl/expressions/At.cpp @@ -54,28 +54,17 @@ ExpressionPointer At::reduced() //////////////////////////////////////////////////////////////////////////////////////////////////// -ExpressionPointer At::negationNormalized() +ExpressionPointer At::existentiallyQuantified() { BOOST_ASSERT(m_argument); - m_argument = m_argument->negationNormalized(); + m_argument = m_argument->existentiallyQuantified(); return this; } //////////////////////////////////////////////////////////////////////////////////////////////////// -ExpressionPointer At::prenex(Expression::Type lastExpressionType) -{ - BOOST_ASSERT(m_argument); - - m_argument = m_argument->prenex(lastExpressionType); - - return Expression::moveUpQuantifiers(this, m_argument); -} - -//////////////////////////////////////////////////////////////////////////////////////////////////// - ExpressionPointer At::simplified() { BOOST_ASSERT(m_argument); @@ -87,13 +76,9 @@ ExpressionPointer At::simplified() //////////////////////////////////////////////////////////////////////////////////////////////////// -ExpressionPointer At::disjunctionNormalized() +void At::collectParameters(std::set ¶meters) { - BOOST_ASSERT(m_argument); - - m_argument = m_argument->disjunctionNormalized(); - - return this; + m_argument->collectParameters(parameters); } //////////////////////////////////////////////////////////////////////////////////////////////////// diff --git a/src/plasp/pddl/expressions/DerivedPredicate.cpp b/src/plasp/pddl/expressions/DerivedPredicate.cpp index cf0d10b..bd88cb3 100644 --- a/src/plasp/pddl/expressions/DerivedPredicate.cpp +++ b/src/plasp/pddl/expressions/DerivedPredicate.cpp @@ -16,39 +16,97 @@ namespace expressions // //////////////////////////////////////////////////////////////////////////////////////////////////// -DerivedPredicate::DerivedPredicate(size_t id) -: m_id{id} +void DerivedPredicate::setPreconditions(std::vector &&preconditions) { + m_preconditions = std::move(preconditions); } //////////////////////////////////////////////////////////////////////////////////////////////////// -size_t DerivedPredicate::id() const +const std::vector &DerivedPredicate::preconditions() const { - return m_id; + return m_preconditions; } //////////////////////////////////////////////////////////////////////////////////////////////////// -void DerivedPredicate::setArgument(ExpressionPointer argument) +void DerivedPredicate::collectParameters() { - m_argument = argument; + for (const auto &conjunction : m_preconditions) + for (const auto &precondition : conjunction) + precondition->collectParameters(m_parameters); } //////////////////////////////////////////////////////////////////////////////////////////////////// -ExpressionPointer DerivedPredicate::argument() const +const std::set &DerivedPredicate::parameters() const { - return m_argument; + return m_parameters; +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +void DerivedPredicate::collectParameters(std::set ¶meters) +{ + for (auto &conjunction : m_preconditions) + for (auto &precondition : conjunction) + precondition->collectParameters(m_parameters); + + // Copy in order not to interfere with potentially bound variables in parent expressions + parameters = m_parameters; } //////////////////////////////////////////////////////////////////////////////////////////////////// void DerivedPredicate::print(std::ostream &ostream) const { - ostream << "(:derived "; - m_argument->print(ostream); - ostream << ")"; + ostream << "(:derived "; + + BOOST_ASSERT(m_preconditions.size() > 0); + + const auto printConjunction = + [&ostream](const auto &conjunction) + { + if (conjunction.size() == 0) + { + conjunction.front()->print(ostream); + return; + } + + ostream << "(and"; + + for (const auto &precondition : conjunction) + { + ostream << " "; + precondition->print(ostream); + } + + ostream << ")"; + }; + + if (m_preconditions.size() == 1) + { + const auto &conjunction = m_preconditions.front(); + + BOOST_ASSERT(conjunction.size() > 0); + + printConjunction(conjunction); + + ostream << ")"; + + return; + } + + ostream << " (or"; + + for (const auto conjunction : m_preconditions) + { + ostream << " "; + + printConjunction(conjunction); + } + + ostream << "))"; } //////////////////////////////////////////////////////////////////////////////////////////////////// diff --git a/src/plasp/pddl/expressions/Exists.cpp b/src/plasp/pddl/expressions/Exists.cpp index eccd1dc..5169f5e 100644 --- a/src/plasp/pddl/expressions/Exists.cpp +++ b/src/plasp/pddl/expressions/Exists.cpp @@ -20,15 +20,6 @@ const std::string Exists::Identifier = "exists"; //////////////////////////////////////////////////////////////////////////////////////////////////// -ExpressionPointer Exists::decomposed(DerivedPredicates &derivedPredicates) -{ - m_argument = m_argument->decomposed(derivedPredicates); - - return this; -} - -//////////////////////////////////////////////////////////////////////////////////////////////////// - } } } diff --git a/src/plasp/pddl/expressions/ForAll.cpp b/src/plasp/pddl/expressions/ForAll.cpp index 6ce8550..53fa1fc 100644 --- a/src/plasp/pddl/expressions/ForAll.cpp +++ b/src/plasp/pddl/expressions/ForAll.cpp @@ -3,7 +3,8 @@ #include #include -#include +#include +#include namespace plasp { @@ -22,14 +23,16 @@ const std::string ForAll::Identifier = "forall"; //////////////////////////////////////////////////////////////////////////////////////////////////// -ExpressionPointer ForAll::decomposed(DerivedPredicates &derivedPredicates) +ExpressionPointer ForAll::existentiallyQuantified() { - auto derivedPredicate = DerivedPredicatePointer(new DerivedPredicate(derivedPredicates.size())); - derivedPredicates.push_back(derivedPredicate); + auto existsExpression = ExistsPointer(new Exists()); + auto notExpression = NotPointer(new Not()); - derivedPredicate->setArgument(this); + notExpression->setArgument(m_argument->existentiallyQuantified()); + existsExpression->setArgument(notExpression); + existsExpression->variables() = std::move(m_variables); - return derivedPredicate; + return existsExpression; } //////////////////////////////////////////////////////////////////////////////////////////////////// diff --git a/src/plasp/pddl/expressions/Not.cpp b/src/plasp/pddl/expressions/Not.cpp index 41785b6..01e8a98 100644 --- a/src/plasp/pddl/expressions/Not.cpp +++ b/src/plasp/pddl/expressions/Not.cpp @@ -62,113 +62,61 @@ ExpressionPointer Not::reduced() //////////////////////////////////////////////////////////////////////////////////////////////////// -ExpressionPointer Not::negationNormalized() +ExpressionPointer Not::existentiallyQuantified() { BOOST_ASSERT(m_argument); - // Remove immediate double negations - if (m_argument->expressionType() == Expression::Type::Not) - { - auto &argument = dynamic_cast(*m_argument); - - return argument.m_argument->negationNormalized(); - } - - // Normalize argument - m_argument = m_argument->negationNormalized(); - - // Remove double negations occurring after normalizing the argument - if (m_argument->expressionType() == Expression::Type::Not) - { - auto &argument = dynamic_cast(*m_argument); - - return argument.m_argument; - } - - // De Morgan for negative conjunctions - if (m_argument->expressionType() == Expression::Type::And) - { - auto &andExpression = dynamic_cast(*m_argument); - auto orExpression = OrPointer(new Or); - - orExpression->arguments().reserve(andExpression.arguments().size()); - - for (size_t i = 0; i < andExpression.arguments().size(); i++) - orExpression->addArgument(andExpression.arguments()[i]->negated()); - - return orExpression->negationNormalized(); - } - - // De Morgan for negative disjunctions - if (m_argument->expressionType() == Expression::Type::Or) - { - auto &orExpression = dynamic_cast(*m_argument); - auto andExpression = AndPointer(new And); - - andExpression->arguments().reserve(orExpression.arguments().size()); - - for (size_t i = 0; i < orExpression.arguments().size(); i++) - andExpression->addArgument(orExpression.arguments()[i]->negated()); - - return andExpression->negationNormalized(); - } - - // De Morgen for existential quantifiers - if (m_argument->expressionType() == Expression::Type::Exists) - { - auto &existsExpression = dynamic_cast(*m_argument); - auto forAllExpression = ForAllPointer(new ForAll); - - forAllExpression->setArgument(existsExpression.argument()->negated()); - - return forAllExpression->negationNormalized(); - } - - // De Morgen for universal quantifiers - if (m_argument->expressionType() == Expression::Type::ForAll) - { - auto &forAllExpression = dynamic_cast(*m_argument); - auto existsExpression = ExistsPointer(new Exists); - - existsExpression->setArgument(forAllExpression.argument()->negated()); - - return existsExpression->negationNormalized(); - } + m_argument = m_argument->existentiallyQuantified(); return this; } //////////////////////////////////////////////////////////////////////////////////////////////////// -ExpressionPointer Not::prenex(Expression::Type lastExpressionType) -{ - BOOST_ASSERT(m_argument); - - m_argument = m_argument->prenex(lastExpressionType); - - return Expression::moveUpQuantifiers(this, m_argument); -} - -//////////////////////////////////////////////////////////////////////////////////////////////////// - ExpressionPointer Not::simplified() { BOOST_ASSERT(m_argument); m_argument = m_argument->simplified(); + // Remove double negations + if (m_argument->expressionType() == Expression::Type::Not) + { + const auto ¬Expression = dynamic_cast(*m_argument); + + return notExpression.argument(); + } + return this; } //////////////////////////////////////////////////////////////////////////////////////////////////// -ExpressionPointer Not::disjunctionNormalized() +void Not::collectParameters(std::set ¶meters) { - BOOST_ASSERT(m_argument); + m_argument->collectParameters(parameters); +} - m_argument = m_argument->disjunctionNormalized(); +//////////////////////////////////////////////////////////////////////////////////////////////////// - return this; +ExpressionPointer Not::decomposed(DerivedPredicates &derivedPredicates) +{ + m_argument = m_argument->decomposed(derivedPredicates); + + // Predicates and derived predicates can be directly negated + if (m_argument->expressionType() == Expression::Type::Predicate + || m_argument->expressionType() == Expression::Type::DerivedPredicate) + { + return this; + } + + derivedPredicates.emplace_back(new DerivedPredicate()); + auto &derivedPredicate = derivedPredicates.back(); + + // Move this expression’s arguments to the derived predicate + derivedPredicate->setPreconditions({{this}}); + + return derivedPredicate; } //////////////////////////////////////////////////////////////////////////////////////////////////// @@ -184,19 +132,6 @@ void Not::print(std::ostream &ostream) const //////////////////////////////////////////////////////////////////////////////////////////////////// -ExpressionPointer Not::decomposed(DerivedPredicates &) -{ - if (m_argument->expressionType() != Expression::Type::Not - && m_argument->expressionType() != Expression::Type::Predicate) - { - throw output::TranslatorException("Expression is not in first-order negation normal form and cannot be decomposed"); - } - - return this; -} - -//////////////////////////////////////////////////////////////////////////////////////////////////// - } } } diff --git a/src/plasp/pddl/expressions/Or.cpp b/src/plasp/pddl/expressions/Or.cpp index f7c0293..25d8713 100644 --- a/src/plasp/pddl/expressions/Or.cpp +++ b/src/plasp/pddl/expressions/Or.cpp @@ -1,5 +1,7 @@ #include +#include +#include #include namespace plasp @@ -21,17 +23,38 @@ const std::string Or::Identifier = "or"; ExpressionPointer Or::decomposed(DerivedPredicates &derivedPredicates) { - // Check that all children are simple or negated predicates - std::for_each(m_arguments.begin(), m_arguments.end(), - [&](auto &argument) + derivedPredicates.emplace_back(new DerivedPredicate()); + auto &derivedPredicate = derivedPredicates.back(); + + std::vector preconditions; + + for (auto &argument : m_arguments) + { + Expressions conjunction; + + // “and” expressions can directly be inlined into the derived predicate + if (argument->expressionType() == Expression::Type::And) { - argument = argument->decomposed(derivedPredicates); - }); + const auto &andExpression = dynamic_cast(*argument); - auto derivedPredicate = DerivedPredicatePointer(new DerivedPredicate(derivedPredicates.size())); - derivedPredicates.push_back(derivedPredicate); + conjunction = std::move(andExpression.arguments()); - derivedPredicate->setArgument(this); + for (auto &argument : conjunction) + argument = argument->decomposed(derivedPredicates); + + break; + } + else + { + conjunction.emplace_back(argument->decomposed(derivedPredicates)); + break; + } + + // Move this expression’s arguments to the derived predicate + preconditions.emplace_back(std::move(conjunction)); + } + + derivedPredicate->setPreconditions(std::move(preconditions)); return derivedPredicate; } diff --git a/src/plasp/pddl/expressions/Predicate.cpp b/src/plasp/pddl/expressions/Predicate.cpp index 80f34a1..33aee63 100644 --- a/src/plasp/pddl/expressions/Predicate.cpp +++ b/src/plasp/pddl/expressions/Predicate.cpp @@ -156,6 +156,22 @@ bool Predicate::isDeclared() const //////////////////////////////////////////////////////////////////////////////////////////////////// +ExpressionPointer Predicate::decomposed(expressions::DerivedPredicates &) +{ + // Predicates cannot be further decomposed + return this; +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +void Predicate::collectParameters(std::set ¶meters) +{ + for (const auto &argument : m_arguments) + argument->collectParameters(parameters); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + const std::string &Predicate::name() const { return m_name; diff --git a/src/plasp/pddl/expressions/Variable.cpp b/src/plasp/pddl/expressions/Variable.cpp index 7c4e3a9..1df7636 100644 --- a/src/plasp/pddl/expressions/Variable.cpp +++ b/src/plasp/pddl/expressions/Variable.cpp @@ -143,33 +143,6 @@ void Variable::parseTypedDeclarations(Context &context, ExpressionContext &expre //////////////////////////////////////////////////////////////////////////////////////////////////// -/* -VariablePointer Variable::parseAndFind(Context &context, const ExpressionContext &expressionContext) -{ - auto &parser = context.parser; - - parser.skipWhiteSpace(); - - parser.expect("?"); - - const auto variableName = parser.parseIdentifier(); - - const auto &variables = expressionContext.parameters; - - const auto match = std::find_if(variables.cbegin(), variables.cend(), - [&](const auto &variable) - { - return variable->name() == variableName; - }); - - if (match == variables.cend()) - throw input::ParserException(parser.location(), "parameter “" + variableName + "” used but never declared"); - - return match->get(); -}*/ - -//////////////////////////////////////////////////////////////////////////////////////////////////// - void Variable::setName(std::string name) { m_name = name; @@ -212,6 +185,13 @@ bool Variable::isDirty() const //////////////////////////////////////////////////////////////////////////////////////////////////// +void Variable::collectParameters(std::set ¶meters) +{ + parameters.emplace(this); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + void Variable::print(std::ostream &ostream) const { ostream << "?" << m_name; diff --git a/tests/TestPDDLNormalization.cpp b/tests/TestPDDLNormalization.cpp index 33d9f26..43c6c7b 100644 --- a/tests/TestPDDLNormalization.cpp +++ b/tests/TestPDDLNormalization.cpp @@ -79,7 +79,7 @@ TEST_CASE("[PDDL normalization] Implications are correctly replaced", "[PDDL nor i->setArgument(1, new expressions::Dummy("b")); std::stringstream output; - i->normalized()->print(output); + i->reduced()->print(output); CHECK(output.str() == "(or (not (a)) (b))"); } @@ -95,68 +95,35 @@ TEST_CASE("[PDDL normalization] Double negations are correctly replaced", "[PDDL n1->setArgument(n2); std::stringstream output; - n1->normalized()->print(output); + n1->simplified()->print(output); CHECK(output.str() == "(a)"); } //////////////////////////////////////////////////////////////////////////////////////////////////// -TEST_CASE("[PDDL normalization] De Morgan’s rule is correctly applied to negative conjunctions", "[PDDL normalization]") -{ - auto a = expressions::AndPointer(new expressions::And); - a->addArgument(new expressions::Dummy("a")); - a->addArgument(new expressions::Dummy("b")); - a->addArgument(new expressions::Dummy("c")); - - auto n = expressions::NotPointer(new expressions::Not); - n->setArgument(a); - - std::stringstream output; - n->normalized()->print(output); - - CHECK(output.str() == "(or (not (a)) (not (b)) (not (c)))"); -} - -//////////////////////////////////////////////////////////////////////////////////////////////////// - -TEST_CASE("[PDDL normalization] De Morgan’s rule is correctly applied to negative disjunctions", "[PDDL normalization]") -{ - auto a = expressions::OrPointer(new expressions::Or); - a->addArgument(new expressions::Dummy("a")); - a->addArgument(new expressions::Dummy("b")); - a->addArgument(new expressions::Dummy("c")); - - auto n = expressions::NotPointer(new expressions::Not); - n->setArgument(a); - - std::stringstream output; - n->normalized()->print(output); - - CHECK(output.str() == "(and (not (a)) (not (b)) (not (c)))"); -} - -//////////////////////////////////////////////////////////////////////////////////////////////////// - -TEST_CASE("[PDDL normalization] Expressions inside double negations are also normalized", "[PDDL normalization]") +TEST_CASE("[PDDL normalization] Expressions inside double negations are also simplified", "[PDDL normalization]") { auto n1 = expressions::NotPointer(new expressions::Not); auto n2 = expressions::NotPointer(new expressions::Not); - auto n3 = expressions::NotPointer(new expressions::Not); - auto a = expressions::AndPointer(new expressions::And); + auto a1 = expressions::AndPointer(new expressions::And); + auto a2 = expressions::AndPointer(new expressions::And); - a->addArgument(new expressions::Dummy("a")); - a->addArgument(new expressions::Dummy("b")); - a->addArgument(new expressions::Dummy("c")); + a2->addArgument(new expressions::Dummy("d")); + a2->addArgument(new expressions::Dummy("e")); - n3->setArgument(a); - n2->setArgument(n3); + a1->addArgument(new expressions::Dummy("a")); + a1->addArgument(new expressions::Dummy("b")); + a1->addArgument(new expressions::Dummy("c")); + a1->addArgument(a2); + + n2->setArgument(a1); n1->setArgument(n2); std::stringstream output; - n1->normalized()->print(output); + n1->simplified()->print(output); - CHECK(output.str() == "(or (not (a)) (not (b)) (not (c)))"); + CHECK(output.str() == "(and (a) (b) (c) (d) (e))"); } //////////////////////////////////////////////////////////////////////////////////////////////////// @@ -180,7 +147,7 @@ TEST_CASE("[PDDL normalization] Nested “for all” expressions are correctly s f2->setArgument(new expressions::Dummy("a")); std::stringstream output; - f1->normalized()->print(output); + f1->simplified()->print(output); CHECK(output.str() == "(forall (?x ?y ?z ?u ?v ?w) (a))"); } @@ -206,149 +173,36 @@ TEST_CASE("[PDDL normalization] Nested “exists” expressions are correctly si e2->setArgument(new expressions::Dummy("a")); std::stringstream output; - e1->normalized()->print(output); + e1->simplified()->print(output); CHECK(output.str() == "(exists (?x ?y ?z ?u ?v ?w) (a))"); } //////////////////////////////////////////////////////////////////////////////////////////////////// -TEST_CASE("[PDDL normalization] Prenex normal form is correctly established", "[PDDL normalization]") +TEST_CASE("[PDDL normalization] “for all” expressions are correctly replaced by “exists” expressions during normalization", "[PDDL normalization]") { - auto a = expressions::AndPointer(new expressions::And); - auto f1 = expressions::ForAllPointer(new expressions::ForAll); - auto o = expressions::OrPointer(new expressions::Or); - auto e = expressions::ExistsPointer(new expressions::Exists); - auto f2 = expressions::ForAllPointer(new expressions::ForAll); - auto v1 = expressions::VariablePointer(new expressions::Variable("x")); auto v2 = expressions::VariablePointer(new expressions::Variable("y")); auto v3 = expressions::VariablePointer(new expressions::Variable("z")); + auto v4 = expressions::VariablePointer(new expressions::Variable("u")); + auto v5 = expressions::VariablePointer(new expressions::Variable("v")); + auto v6 = expressions::VariablePointer(new expressions::Variable("w")); - a->addArgument(new expressions::Dummy("a")); - a->addArgument(f1); - f1->variables() = {v1}; - f1->setArgument(o); - o->addArgument(e); - e->variables() = {v3}; - e->setArgument(new expressions::Dummy("b")); - o->addArgument(f2); - f2->variables() = {v2}; - f2->setArgument(new expressions::Dummy("c")); - - auto normalized = a->reduced()->negationNormalized()->prenex(); - - SECTION("normalized") - { - std::stringstream output; - normalized->print(output); - - CHECK(output.str() == "(forall (?x) (forall (?y) (exists (?z) (and (a) (or (b) (c))))))"); - } - - SECTION("simplified") - { - normalized = normalized->simplified(); - - std::stringstream output; - normalized->print(output); - - CHECK(output.str() == "(forall (?x ?y) (exists (?z) (and (a) (or (b) (c)))))"); - } -} - -//////////////////////////////////////////////////////////////////////////////////////////////////// - -TEST_CASE("[PDDL normalization] Same-type first-order expressions are correctly grouped in prenex normal form", "[PDDL normalization]") -{ auto f1 = expressions::ForAllPointer(new expressions::ForAll); - auto f2 = expressions::ForAllPointer(new expressions::ForAll); - auto f3 = expressions::ForAllPointer(new expressions::ForAll); - auto f4 = expressions::ForAllPointer(new expressions::ForAll); - auto f5 = expressions::ForAllPointer(new expressions::ForAll); - auto f6 = expressions::ForAllPointer(new expressions::ForAll); - auto e1 = expressions::ExistsPointer(new expressions::Exists); - auto e2 = expressions::ExistsPointer(new expressions::Exists); - auto e3 = expressions::ExistsPointer(new expressions::Exists); - auto a = expressions::AndPointer(new expressions::And); - - f1->variables() = {new expressions::Variable("v1")}; - f1->setArgument(a); - - // forall exists forall exists - a->addArgument(f2); - f2->variables() = {new expressions::Variable("v2")}; - f2->setArgument(e1); - e1->variables() = {new expressions::Variable("v3")}; - e1->setArgument(f3); - f3->variables() = {new expressions::Variable("v4")}; - f3->setArgument(e2); - e2->variables() = {new expressions::Variable("v5")}; - e2->setArgument(new expressions::Dummy("a")); - - // forall forall exists forall - a->addArgument(f4); - f4->variables() = {new expressions::Variable("v6")}; - f4->setArgument(f5); - f5->variables() = {new expressions::Variable("v7")}; - f5->setArgument(e3); - e3->variables() = {new expressions::Variable("v8")}; - e3->setArgument(f6); - f6->variables() = {new expressions::Variable("v9")}; - f6->setArgument(new expressions::Dummy("b")); - - auto normalized = f1->normalized(); - - std::stringstream output; - normalized->print(output); - - CHECK(output.str() == "(forall (?v1 ?v2 ?v6 ?v7) (exists (?v3 ?v8) (forall (?v4 ?v9) (exists (?v5) (and (a) (b))))))"); -} - -//////////////////////////////////////////////////////////////////////////////////////////////////// - -TEST_CASE("[PDDL normalization] Disjunctive normal form is correctly established", "[PDDL normalization]") -{ - auto f = expressions::ForAllPointer(new expressions::ForAll); auto e = expressions::ExistsPointer(new expressions::Exists); - auto a = expressions::AndPointer(new expressions::And); - auto o1 = expressions::OrPointer(new expressions::Or); - auto o2 = expressions::OrPointer(new expressions::Or); - auto o3 = expressions::OrPointer(new expressions::Or); + auto f2 = expressions::ForAllPointer(new expressions::ForAll); - f->variables() = {new expressions::Variable("v1")}; - f->setArgument(e); + f1->variables() = {v1, v2}; + e->variables() = {v3, v4}; + f2->variables() = {v5, v6}; - e->variables() = {new expressions::Variable("v2")}; - e->setArgument(o1); - - o1->addArgument(a); - o1->addArgument(new expressions::Dummy("h")); - - a->addArgument(new expressions::Dummy("a")); - a->addArgument(new expressions::Dummy("b")); - a->addArgument(o2); - a->addArgument(o3); - - o2->addArgument(new expressions::Dummy("c")); - o2->addArgument(new expressions::Dummy("d")); - o2->addArgument(new expressions::Dummy("e")); - - o3->addArgument(new expressions::Dummy("f")); - o3->addArgument(new expressions::Dummy("g")); - - auto normalized = f->normalized(); + f1->setArgument(e); + e->setArgument(f2); + f2->setArgument(new expressions::Dummy("a")); std::stringstream output; - normalized->print(output); + f1->normalized()->print(output); - CHECK(output.str() == "(forall (?v1) (exists (?v2) (or " - "(and (a) (b) (c) (f)) " - "(h) " - "(and (a) (b) (d) (f)) " - "(and (a) (b) (e) (f)) " - "(and (a) (b) (c) (g)) " - "(and (a) (b) (d) (g)) " - "(and (a) (b) (e) (g))" - ")))"); + CHECK(output.str() == "(exists (?x ?y) (not (exists (?z ?u ?v ?w) (not (a)))))"); }