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

Implemented prenex normalization.

Browse Source
This commit is contained in:
Patrick Lühne 2016-09-07 00:34:26 +02:00
parent 2e52357dd2
commit e0ed145716
10 changed files with 203 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
include/plasp/pddl/Expression.h
View File

@ -120,11 +120,15 @@ class Expression
ExpressionPointer normalized();
virtual ExpressionPointer reduced();
virtual ExpressionPointer negationNormalized();
virtual ExpressionPointer prenex();
virtual ExpressionPointer simplified();
ExpressionPointer negated();
virtual void print(std::ostream &ostream) const = 0;
protected:
static ExpressionPointer prenex(ExpressionPointer parent, ExpressionPointer &child);
private:
friend void intrusive_ptr_add_ref(Expression *expression);
friend void intrusive_ptr_release(Expression *expression);

2
include/plasp/pddl/expressions/At.h
View File

@ -39,6 +39,8 @@ class At: public ExpressionCRTP<At>
ExpressionPointer reduced() override;
ExpressionPointer negationNormalized() override;
ExpressionPointer prenex() override;
ExpressionPointer simplified() override;
void print(std::ostream &ostream) const override;

22
include/plasp/pddl/expressions/Binary.h
View File

@ -4,6 +4,9 @@
#include <plasp/pddl/Context.h>
#include <plasp/pddl/Expression.h>
#include <plasp/pddl/expressions/Exists.h>
#include <plasp/pddl/expressions/ForAll.h>
namespace plasp
{
namespace pddl
@ -31,6 +34,7 @@ class Binary: public ExpressionCRTP<Derived>
ExpressionPointer reduced() override;
ExpressionPointer negationNormalized() override;
ExpressionPointer prenex() override;
void print(std::ostream &ostream) const override;
@ -117,6 +121,24 @@ inline ExpressionPointer Binary<Derived>::negationNormalized()
////////////////////////////////////////////////////////////////////////////////////////////////////
template<class Derived>
inline ExpressionPointer Binary<Derived>::prenex()
{
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;
}
////////////////////////////////////////////////////////////////////////////////////////////////////
template<class Derived>
inline void Binary<Derived>::print(std::ostream &ostream) const
{

24
include/plasp/pddl/expressions/NAry.h
View File

@ -4,6 +4,9 @@
#include <plasp/pddl/Context.h>
#include <plasp/pddl/Expression.h>
#include <plasp/pddl/expressions/Exists.h>
#include <plasp/pddl/expressions/ForAll.h>
namespace plasp
{
namespace pddl
@ -33,6 +36,7 @@ class NAry: public ExpressionCRTP<Derived>
ExpressionPointer reduced() override;
ExpressionPointer negationNormalized() override;
ExpressionPointer prenex() override;
ExpressionPointer simplified() override;
void print(std::ostream &ostream) const override;
@ -148,6 +152,26 @@ inline ExpressionPointer NAry<Derived>::negationNormalized()
////////////////////////////////////////////////////////////////////////////////////////////////////
template<class Derived>
inline ExpressionPointer NAry<Derived>::prenex()
{
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];
BOOST_ASSERT(argument);
result = Expression::prenex(result, argument);
}
return result;
}
////////////////////////////////////////////////////////////////////////////////////////////////////
template<class Derived>
inline ExpressionPointer NAry<Derived>::simplified()
{

2
include/plasp/pddl/expressions/Not.h
View File

@ -34,6 +34,8 @@ class Not: public ExpressionCRTP<Not>
ExpressionPointer reduced() override;
ExpressionPointer negationNormalized() override;
ExpressionPointer prenex() override;
ExpressionPointer simplified() override;
void print(std::ostream &ostream) const override;

24
include/plasp/pddl/expressions/Quantified.h
View File

@ -36,6 +36,7 @@ class Quantified: public ExpressionCRTP<Derived>
ExpressionPointer reduced() override;
ExpressionPointer negationNormalized() override;
ExpressionPointer prenex() override;
ExpressionPointer simplified() override;
void print(std::ostream &ostream) const override;
@ -121,7 +122,9 @@ const Variables &Quantified<Derived>::variables() const
template<class Derived>
inline ExpressionPointer Quantified<Derived>::reduced()
{
m_argument = m_argument->reduced();
BOOST_ASSERT(m_argument);
m_argument = m_argument->prenex();
return this;
}
@ -131,7 +134,22 @@ inline ExpressionPointer Quantified<Derived>::reduced()
template<class Derived>
inline ExpressionPointer Quantified<Derived>::negationNormalized()
{
m_argument = m_argument->negationNormalized();
BOOST_ASSERT(m_argument);
m_argument = m_argument->prenex();
return this;
}
////////////////////////////////////////////////////////////////////////////////////////////////////
template<class Derived>
inline ExpressionPointer Quantified<Derived>::prenex()
{
BOOST_ASSERT(m_argument);
// Quantifiers may not move before other quantifiers, their order matters
m_argument = m_argument->prenex();
return this;
}
@ -141,6 +159,8 @@ inline ExpressionPointer Quantified<Derived>::negationNormalized()
template<class Derived>
inline ExpressionPointer Quantified<Derived>::simplified()
{
BOOST_ASSERT(m_argument);
m_argument = m_argument->simplified();
// Associate same-type children, such as (forall (?x) (forall (?y) (...)))

53
src/plasp/pddl/Expression.cpp
View File

@ -28,7 +28,7 @@ namespace pddl
ExpressionPointer Expression::normalized()
{
return reduced()->negationNormalized()->simplified();
return reduced()->negationNormalized()->prenex()->simplified();
}
////////////////////////////////////////////////////////////////////////////////////////////////////
@ -47,6 +47,57 @@ ExpressionPointer Expression::negationNormalized()
////////////////////////////////////////////////////////////////////////////////////////////////////
ExpressionPointer Expression::prenex()
{
return this;
}
////////////////////////////////////////////////////////////////////////////////////////////////////
ExpressionPointer Expression::prenex(ExpressionPointer parent, ExpressionPointer &child)
{
BOOST_ASSERT(child);
child = child->prenex();
if (child->expressionType() == Expression::Type::Exists)
{
auto quantifiedExpression = expressions::ExistsPointer(dynamic_cast<expressions::Exists *>(child.get()));
// Move argument up
child = quantifiedExpression->argument();
// Recursively build prenex form on new child
parent = Expression::prenex(parent, child);
// Move quantifier up
quantifiedExpression->setArgument(parent);
// Make parent point to the quantifier that has been moved up
return quantifiedExpression;
}
else if (child->expressionType() == Expression::Type::ForAll)
{
auto quantifiedExpression = expressions::ForAllPointer(dynamic_cast<expressions::ForAll *>(child.get()));
// Move argument up
child = quantifiedExpression->argument();
// Recursively build prenex form on new child
parent = Expression::prenex(parent, child);
// Move quantifier up
quantifiedExpression->setArgument(parent);
// Make parent point to the quantifier that has been moved up
return quantifiedExpression;
}
return parent;
}
////////////////////////////////////////////////////////////////////////////////////////////////////
ExpressionPointer Expression::simplified()
{
return this;

20
src/plasp/pddl/expressions/At.cpp
View File

@ -54,6 +54,26 @@ ExpressionPointer At::negationNormalized()
////////////////////////////////////////////////////////////////////////////////////////////////////
ExpressionPointer At::prenex()
{
BOOST_ASSERT(m_argument);
return Expression::prenex(this, m_argument);
}
////////////////////////////////////////////////////////////////////////////////////////////////////
ExpressionPointer At::simplified()
{
BOOST_ASSERT(m_argument);
m_argument = m_argument->simplified();
return this;
}
////////////////////////////////////////////////////////////////////////////////////////////////////
void At::print(std::ostream &ostream) const
{
ostream << "(at " << m_timePoint << " ";

20
src/plasp/pddl/expressions/Not.cpp
View File

@ -128,6 +128,26 @@ ExpressionPointer Not::negationNormalized()
////////////////////////////////////////////////////////////////////////////////////////////////////
ExpressionPointer Not::prenex()
{
BOOST_ASSERT(m_argument);
return Expression::prenex(this, m_argument);
}
////////////////////////////////////////////////////////////////////////////////////////////////////
ExpressionPointer Not::simplified()
{
BOOST_ASSERT(m_argument);
m_argument = m_argument->simplified();
return this;
}
////////////////////////////////////////////////////////////////////////////////////////////////////
void Not::print(std::ostream &ostream) const
{
ostream << "(not ";

41
tests/TestPDDLNormalization.cpp
View File

@ -173,13 +173,11 @@ TEST(PDDLNormalizationTests, SimplifyNestedForAll)
auto f1 = expressions::ForAllPointer(new expressions::ForAll);
auto f2 = expressions::ForAllPointer(new expressions::ForAll);
auto d = expressions::DummyPointer(new expressions::Dummy("a"));
f1->variables() = {v1, v2, v3};
f2->variables() = {v4, v5, v6};
f1->setArgument(f2);
f2->setArgument(d);
f2->setArgument(new expressions::Dummy("a"));
std::stringstream output;
f1->normalized()->print(output);
@ -201,16 +199,47 @@ TEST(PDDLNormalizationTests, SimplifyNestedExists)
auto e1 = expressions::ExistsPointer(new expressions::Exists);
auto e2 = expressions::ExistsPointer(new expressions::Exists);
auto d = expressions::DummyPointer(new expressions::Dummy("a"));
e1->variables() = {v1, v2, v3};
e2->variables() = {v4, v5, v6};
e1->setArgument(e2);
e2->setArgument(d);
e2->setArgument(new expressions::Dummy("a"));
std::stringstream output;
e1->normalized()->print(output);
ASSERT_EQ(output.str(), "(exists (?x ?y ?z ?u ?v ?w) (a))");
}
////////////////////////////////////////////////////////////////////////////////////////////////////
TEST(PDDLNormalizationTests, Prenex)
{
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"));
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();
std::stringstream output;
normalized->print(output);
ASSERT_EQ(output.str(), "(forall (?x) (exists (?z) (forall (?y) (and (a) (or (b) (c))))))");
}