From 34496a715850694632833631b5c9fc7bde2dc954 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Patrick=20L=C3=BChne?= Date: Thu, 8 Sep 2016 02:40:51 +0200 Subject: [PATCH] Finished implementing the prenex normal form with maximal groups of same-type quantifiers. --- include/plasp/pddl/Expression.h | 7 +- include/plasp/pddl/expressions/At.h | 2 +- include/plasp/pddl/expressions/Binary.h | 17 +--- include/plasp/pddl/expressions/Exists.h | 2 +- include/plasp/pddl/expressions/ForAll.h | 2 +- include/plasp/pddl/expressions/NAry.h | 84 ++++++++++++++++--- include/plasp/pddl/expressions/Not.h | 2 +- include/plasp/pddl/expressions/Quantified.h | 92 +++++++++++---------- src/plasp/pddl/Expression.cpp | 12 +-- src/plasp/pddl/expressions/At.cpp | 6 +- src/plasp/pddl/expressions/Not.cpp | 6 +- tests/TestPDDLNormalization.cpp | 61 +++++++++++++- 12 files changed, 207 insertions(+), 86 deletions(-) diff --git a/include/plasp/pddl/Expression.h b/include/plasp/pddl/Expression.h index ebc9798..52d0919 100644 --- a/include/plasp/pddl/Expression.h +++ b/include/plasp/pddl/Expression.h @@ -73,6 +73,9 @@ class PrimitiveType; using PrimitiveTypePointer = boost::intrusive_ptr; using PrimitiveTypes = std::vector; +class Quantified; +using QuantifiedPointer = boost::intrusive_ptr; + template class Reference; template @@ -120,14 +123,14 @@ class Expression ExpressionPointer normalized(); virtual ExpressionPointer reduced(); virtual ExpressionPointer negationNormalized(); - virtual ExpressionPointer prenex(); + virtual ExpressionPointer prenex(Expression::Type lastQuantifierType = Expression::Type::Exists); virtual ExpressionPointer simplified(); ExpressionPointer negated(); virtual void print(std::ostream &ostream) const = 0; protected: - static ExpressionPointer prenex(ExpressionPointer parent, ExpressionPointer &child); + static ExpressionPointer moveUpQuantifiers(ExpressionPointer parent, ExpressionPointer &child); private: friend void intrusive_ptr_add_ref(Expression *expression); diff --git a/include/plasp/pddl/expressions/At.h b/include/plasp/pddl/expressions/At.h index 8357257..3996f1c 100644 --- a/include/plasp/pddl/expressions/At.h +++ b/include/plasp/pddl/expressions/At.h @@ -39,7 +39,7 @@ class At: public ExpressionCRTP ExpressionPointer reduced() override; ExpressionPointer negationNormalized() override; - ExpressionPointer prenex() override; + ExpressionPointer prenex(Expression::Type lastExpressionType) override; ExpressionPointer simplified() 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 50c83f1..5483518 100644 --- a/include/plasp/pddl/expressions/Binary.h +++ b/include/plasp/pddl/expressions/Binary.h @@ -34,7 +34,7 @@ class Binary: public ExpressionCRTP ExpressionPointer reduced() override; ExpressionPointer negationNormalized() override; - ExpressionPointer prenex() override; + ExpressionPointer prenex(Expression::Type lastExpressionType) override; void print(std::ostream &ostream) const override; @@ -122,19 +122,10 @@ inline ExpressionPointer Binary::negationNormalized() //////////////////////////////////////////////////////////////////////////////////////////////////// template -inline ExpressionPointer Binary::prenex() +inline ExpressionPointer Binary::prenex(Expression::Type) { - ExpressionPointer result = this; - - for (size_t i = 0; i < m_arguments.size(); i++) - { - // Iterate in backward order to wrap quantifiers in forward order - auto &argument = m_arguments[m_arguments.size() - i - 1]; - - result = Expression::prenex(result, argument); - } - - return result; + // TODO: implement by refactoring binary expressions + return this; } //////////////////////////////////////////////////////////////////////////////////////////////////// diff --git a/include/plasp/pddl/expressions/Exists.h b/include/plasp/pddl/expressions/Exists.h index d795176..815b34f 100644 --- a/include/plasp/pddl/expressions/Exists.h +++ b/include/plasp/pddl/expressions/Exists.h @@ -16,7 +16,7 @@ namespace expressions // //////////////////////////////////////////////////////////////////////////////////////////////////// -class Exists: public Quantified +class Exists: public QuantifiedCRTP { public: static const Expression::Type ExpressionType = Expression::Type::Exists; diff --git a/include/plasp/pddl/expressions/ForAll.h b/include/plasp/pddl/expressions/ForAll.h index ee9ea00..2c33be4 100644 --- a/include/plasp/pddl/expressions/ForAll.h +++ b/include/plasp/pddl/expressions/ForAll.h @@ -16,7 +16,7 @@ namespace expressions // //////////////////////////////////////////////////////////////////////////////////////////////////// -class ForAll: public Quantified +class ForAll: public QuantifiedCRTP { public: static const Expression::Type ExpressionType = Expression::Type::ForAll; diff --git a/include/plasp/pddl/expressions/NAry.h b/include/plasp/pddl/expressions/NAry.h index 9ba8889..2c289e1 100644 --- a/include/plasp/pddl/expressions/NAry.h +++ b/include/plasp/pddl/expressions/NAry.h @@ -36,7 +36,7 @@ class NAry: public ExpressionCRTP ExpressionPointer reduced() override; ExpressionPointer negationNormalized() override; - ExpressionPointer prenex() override; + ExpressionPointer prenex(Expression::Type lastExpressionType) override; ExpressionPointer simplified() override; void print(std::ostream &ostream) const override; @@ -153,21 +153,85 @@ inline ExpressionPointer NAry::negationNormalized() //////////////////////////////////////////////////////////////////////////////////////////////////// template -inline ExpressionPointer NAry::prenex() +inline ExpressionPointer NAry::prenex(Expression::Type lastExpressionType) { - ExpressionPointer result = this; - + // First, move all childrens’ quantifiers to the front for (size_t i = 0; i < m_arguments.size(); i++) { - // Iterate in backward order to wrap quantifiers in forward order - auto &argument = m_arguments[m_arguments.size() - i - 1]; + BOOST_ASSERT(m_arguments[i]); - BOOST_ASSERT(argument); - - result = Expression::prenex(result, argument); + m_arguments[i] = m_arguments[i]->prenex(lastExpressionType); } - return result; + // 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; } //////////////////////////////////////////////////////////////////////////////////////////////////// diff --git a/include/plasp/pddl/expressions/Not.h b/include/plasp/pddl/expressions/Not.h index 7485822..3ef2827 100644 --- a/include/plasp/pddl/expressions/Not.h +++ b/include/plasp/pddl/expressions/Not.h @@ -34,7 +34,7 @@ class Not: public ExpressionCRTP ExpressionPointer reduced() override; ExpressionPointer negationNormalized() override; - ExpressionPointer prenex() override; + ExpressionPointer prenex(Expression::Type lastExpressionType) override; ExpressionPointer simplified() override; void print(std::ostream &ostream) const override; diff --git a/include/plasp/pddl/expressions/Quantified.h b/include/plasp/pddl/expressions/Quantified.h index 895b5c8..761744b 100644 --- a/include/plasp/pddl/expressions/Quantified.h +++ b/include/plasp/pddl/expressions/Quantified.h @@ -19,14 +19,8 @@ namespace expressions // //////////////////////////////////////////////////////////////////////////////////////////////////// -template -class Quantified: public ExpressionCRTP +class Quantified: public Expression { - public: - template - static boost::intrusive_ptr parse(Context &context, - ExpressionContext &expressionContext, ExpressionParser parseExpression); - public: void setArgument(ExpressionPointer argument); ExpressionPointer argument() const; @@ -34,13 +28,6 @@ class Quantified: public ExpressionCRTP Variables &variables(); const Variables &variables() const; - ExpressionPointer reduced() override; - ExpressionPointer negationNormalized() override; - ExpressionPointer prenex() override; - ExpressionPointer simplified() override; - - void print(std::ostream &ostream) const override; - protected: Variables m_variables; ExpressionPointer m_argument; @@ -48,9 +35,33 @@ class Quantified: public ExpressionCRTP //////////////////////////////////////////////////////////////////////////////////////////////////// +template +class QuantifiedCRTP: public Quantified +{ + public: + template + static boost::intrusive_ptr parse(Context &context, + ExpressionContext &expressionContext, ExpressionParser parseExpression); + + public: + Type expressionType() const override final + { + return Derived::ExpressionType; + } + + ExpressionPointer reduced() override; + ExpressionPointer negationNormalized() override; + ExpressionPointer prenex(Expression::Type lastExpressionType) override; + ExpressionPointer simplified() override; + + void print(std::ostream &ostream) const override; +}; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + template template -boost::intrusive_ptr Quantified::parse(Context &context, +boost::intrusive_ptr QuantifiedCRTP::parse(Context &context, ExpressionContext &expressionContext, ExpressionParser parseExpression) { auto &parser = context.parser; @@ -75,7 +86,7 @@ boost::intrusive_ptr Quantified::parse(Context &context, expressionContext.variables.push(&expression->m_variables); // Parse argument of the expression - expression->Quantified::setArgument(parseExpression(context, expressionContext)); + expression->Quantified::setArgument(parseExpression(context, expressionContext)); // Clean up variable stack expressionContext.variables.pop(); @@ -87,24 +98,28 @@ boost::intrusive_ptr Quantified::parse(Context &context, //////////////////////////////////////////////////////////////////////////////////////////////////// -template -void Quantified::setArgument(ExpressionPointer expression) +inline void Quantified::setArgument(ExpressionPointer expression) { m_argument = expression; } //////////////////////////////////////////////////////////////////////////////////////////////////// -template -ExpressionPointer Quantified::argument() const +inline ExpressionPointer Quantified::argument() const { return m_argument; } //////////////////////////////////////////////////////////////////////////////////////////////////// -template -Variables &Quantified::variables() +inline Variables &Quantified::variables() +{ + return m_variables; +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +inline const Variables &Quantified::variables() const { return m_variables; } @@ -112,19 +127,24 @@ Variables &Quantified::variables() //////////////////////////////////////////////////////////////////////////////////////////////////// template -const Variables &Quantified::variables() const +inline ExpressionPointer QuantifiedCRTP::reduced() { - return m_variables; + BOOST_ASSERT(m_argument); + + m_argument = m_argument->reduced(); + + // Child quantifiers may not move before this quantifier, the order matters + return this; } //////////////////////////////////////////////////////////////////////////////////////////////////// template -inline ExpressionPointer Quantified::reduced() +inline ExpressionPointer QuantifiedCRTP::negationNormalized() { BOOST_ASSERT(m_argument); - m_argument = m_argument->prenex(); + m_argument = m_argument->negationNormalized(); return this; } @@ -132,32 +152,20 @@ inline ExpressionPointer Quantified::reduced() //////////////////////////////////////////////////////////////////////////////////////////////////// template -inline ExpressionPointer Quantified::negationNormalized() +inline ExpressionPointer QuantifiedCRTP::prenex(Expression::Type) { BOOST_ASSERT(m_argument); - m_argument = m_argument->prenex(); - - return this; -} - -//////////////////////////////////////////////////////////////////////////////////////////////////// - -template -inline ExpressionPointer Quantified::prenex() -{ - BOOST_ASSERT(m_argument); + m_argument = m_argument->prenex(Derived::ExpressionType); // Quantifiers may not move before other quantifiers, their order matters - m_argument = m_argument->prenex(); - return this; } //////////////////////////////////////////////////////////////////////////////////////////////////// template -inline ExpressionPointer Quantified::simplified() +inline ExpressionPointer QuantifiedCRTP::simplified() { BOOST_ASSERT(m_argument); @@ -183,7 +191,7 @@ inline ExpressionPointer Quantified::simplified() //////////////////////////////////////////////////////////////////////////////////////////////////// template -inline void Quantified::print(std::ostream &ostream) const +inline void QuantifiedCRTP::print(std::ostream &ostream) const { ostream << "(" << Derived::Identifier << " ("; diff --git a/src/plasp/pddl/Expression.cpp b/src/plasp/pddl/Expression.cpp index 72b2aca..2ffc8e5 100644 --- a/src/plasp/pddl/Expression.cpp +++ b/src/plasp/pddl/Expression.cpp @@ -47,19 +47,17 @@ ExpressionPointer Expression::negationNormalized() //////////////////////////////////////////////////////////////////////////////////////////////////// -ExpressionPointer Expression::prenex() +ExpressionPointer Expression::prenex(Expression::Type) { return this; } //////////////////////////////////////////////////////////////////////////////////////////////////// -ExpressionPointer Expression::prenex(ExpressionPointer parent, ExpressionPointer &child) +ExpressionPointer Expression::moveUpQuantifiers(ExpressionPointer parent, ExpressionPointer &child) { BOOST_ASSERT(child); - child = child->prenex(); - if (child->expressionType() == Expression::Type::Exists) { auto quantifiedExpression = expressions::ExistsPointer(dynamic_cast(child.get())); @@ -67,9 +65,6 @@ ExpressionPointer Expression::prenex(ExpressionPointer parent, ExpressionPointer // Move argument up child = quantifiedExpression->argument(); - // Recursively build prenex form on new child - parent = Expression::prenex(parent, child); - // Move quantifier up quantifiedExpression->setArgument(parent); @@ -83,9 +78,6 @@ ExpressionPointer Expression::prenex(ExpressionPointer parent, ExpressionPointer // Move argument up child = quantifiedExpression->argument(); - // Recursively build prenex form on new child - parent = Expression::prenex(parent, child); - // Move quantifier up quantifiedExpression->setArgument(parent); diff --git a/src/plasp/pddl/expressions/At.cpp b/src/plasp/pddl/expressions/At.cpp index 21390db..ec92601 100644 --- a/src/plasp/pddl/expressions/At.cpp +++ b/src/plasp/pddl/expressions/At.cpp @@ -54,11 +54,13 @@ ExpressionPointer At::negationNormalized() //////////////////////////////////////////////////////////////////////////////////////////////////// -ExpressionPointer At::prenex() +ExpressionPointer At::prenex(Expression::Type lastExpressionType) { BOOST_ASSERT(m_argument); - return Expression::prenex(this, m_argument); + m_argument = m_argument->prenex(lastExpressionType); + + return Expression::moveUpQuantifiers(this, m_argument); } //////////////////////////////////////////////////////////////////////////////////////////////////// diff --git a/src/plasp/pddl/expressions/Not.cpp b/src/plasp/pddl/expressions/Not.cpp index a9753d9..a002a73 100644 --- a/src/plasp/pddl/expressions/Not.cpp +++ b/src/plasp/pddl/expressions/Not.cpp @@ -128,11 +128,13 @@ ExpressionPointer Not::negationNormalized() //////////////////////////////////////////////////////////////////////////////////////////////////// -ExpressionPointer Not::prenex() +ExpressionPointer Not::prenex(Expression::Type lastExpressionType) { BOOST_ASSERT(m_argument); - return Expression::prenex(this, m_argument); + m_argument = m_argument->prenex(lastExpressionType); + + return Expression::moveUpQuantifiers(this, m_argument); } //////////////////////////////////////////////////////////////////////////////////////////////////// diff --git a/tests/TestPDDLNormalization.cpp b/tests/TestPDDLNormalization.cpp index 38057c2..7c28b08 100644 --- a/tests/TestPDDLNormalization.cpp +++ b/tests/TestPDDLNormalization.cpp @@ -238,8 +238,67 @@ TEST(PDDLNormalizationTests, Prenex) auto normalized = a->reduced()->negationNormalized()->prenex(); + { + std::stringstream output; + normalized->print(output); + + ASSERT_EQ(output.str(), "(forall (?x) (forall (?y) (exists (?z) (and (a) (or (b) (c))))))"); + } + + normalized = normalized->simplified(); + + { + std::stringstream output; + normalized->print(output); + + ASSERT_EQ(output.str(), "(forall (?x ?y) (exists (?z) (and (a) (or (b) (c)))))"); + } +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +TEST(PDDLNormalizationTests, PrenexGroupSameType) +{ + 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); - ASSERT_EQ(output.str(), "(forall (?x) (exists (?z) (forall (?y) (and (a) (or (b) (c))))))"); + ASSERT_EQ(output.str(), "(forall (?v1 ?v2 ?v6 ?v7) (exists (?v3 ?v8) (forall (?v4 ?v9) (exists (?v5) (and (a) (b))))))"); }