Finished implementing the prenex normal form with maximal groups of same-type quantifiers.
This commit is contained in:
parent
e0ed145716
commit
34496a7158
@ -73,6 +73,9 @@ class PrimitiveType;
|
||||
using PrimitiveTypePointer = boost::intrusive_ptr<PrimitiveType>;
|
||||
using PrimitiveTypes = std::vector<PrimitiveTypePointer>;
|
||||
|
||||
class Quantified;
|
||||
using QuantifiedPointer = boost::intrusive_ptr<Quantified>;
|
||||
|
||||
template<class Type>
|
||||
class Reference;
|
||||
template<class Type>
|
||||
@ -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);
|
||||
|
@ -39,7 +39,7 @@ class At: public ExpressionCRTP<At>
|
||||
|
||||
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;
|
||||
|
@ -34,7 +34,7 @@ class Binary: public ExpressionCRTP<Derived>
|
||||
|
||||
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<Derived>::negationNormalized()
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
||||
template<class Derived>
|
||||
inline ExpressionPointer Binary<Derived>::prenex()
|
||||
inline ExpressionPointer Binary<Derived>::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;
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
@ -16,7 +16,7 @@ namespace expressions
|
||||
//
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
||||
class Exists: public Quantified<Exists>
|
||||
class Exists: public QuantifiedCRTP<Exists>
|
||||
{
|
||||
public:
|
||||
static const Expression::Type ExpressionType = Expression::Type::Exists;
|
||||
|
@ -16,7 +16,7 @@ namespace expressions
|
||||
//
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
||||
class ForAll: public Quantified<ForAll>
|
||||
class ForAll: public QuantifiedCRTP<ForAll>
|
||||
{
|
||||
public:
|
||||
static const Expression::Type ExpressionType = Expression::Type::ForAll;
|
||||
|
@ -36,7 +36,7 @@ class NAry: public ExpressionCRTP<Derived>
|
||||
|
||||
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<Derived>::negationNormalized()
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
||||
template<class Derived>
|
||||
inline ExpressionPointer NAry<Derived>::prenex()
|
||||
inline ExpressionPointer NAry<Derived>::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<Quantified *>(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;
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
@ -34,7 +34,7 @@ class Not: public ExpressionCRTP<Not>
|
||||
|
||||
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;
|
||||
|
@ -19,14 +19,8 @@ namespace expressions
|
||||
//
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
||||
template<class Derived>
|
||||
class Quantified: public ExpressionCRTP<Derived>
|
||||
class Quantified: public Expression
|
||||
{
|
||||
public:
|
||||
template<typename ExpressionParser>
|
||||
static boost::intrusive_ptr<Derived> parse(Context &context,
|
||||
ExpressionContext &expressionContext, ExpressionParser parseExpression);
|
||||
|
||||
public:
|
||||
void setArgument(ExpressionPointer argument);
|
||||
ExpressionPointer argument() const;
|
||||
@ -34,13 +28,6 @@ class Quantified: public ExpressionCRTP<Derived>
|
||||
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<Derived>
|
||||
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
||||
template<class Derived>
|
||||
class QuantifiedCRTP: public Quantified
|
||||
{
|
||||
public:
|
||||
template<typename ExpressionParser>
|
||||
static boost::intrusive_ptr<Derived> 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<class Derived>
|
||||
template<typename ExpressionParser>
|
||||
boost::intrusive_ptr<Derived> Quantified<Derived>::parse(Context &context,
|
||||
boost::intrusive_ptr<Derived> QuantifiedCRTP<Derived>::parse(Context &context,
|
||||
ExpressionContext &expressionContext, ExpressionParser parseExpression)
|
||||
{
|
||||
auto &parser = context.parser;
|
||||
@ -75,7 +86,7 @@ boost::intrusive_ptr<Derived> Quantified<Derived>::parse(Context &context,
|
||||
expressionContext.variables.push(&expression->m_variables);
|
||||
|
||||
// Parse argument of the expression
|
||||
expression->Quantified<Derived>::setArgument(parseExpression(context, expressionContext));
|
||||
expression->Quantified::setArgument(parseExpression(context, expressionContext));
|
||||
|
||||
// Clean up variable stack
|
||||
expressionContext.variables.pop();
|
||||
@ -87,24 +98,28 @@ boost::intrusive_ptr<Derived> Quantified<Derived>::parse(Context &context,
|
||||
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
||||
template<class Derived>
|
||||
void Quantified<Derived>::setArgument(ExpressionPointer expression)
|
||||
inline void Quantified::setArgument(ExpressionPointer expression)
|
||||
{
|
||||
m_argument = expression;
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
||||
template<class Derived>
|
||||
ExpressionPointer Quantified<Derived>::argument() const
|
||||
inline ExpressionPointer Quantified::argument() const
|
||||
{
|
||||
return m_argument;
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
||||
template<class Derived>
|
||||
Variables &Quantified<Derived>::variables()
|
||||
inline Variables &Quantified::variables()
|
||||
{
|
||||
return m_variables;
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
||||
inline const Variables &Quantified::variables() const
|
||||
{
|
||||
return m_variables;
|
||||
}
|
||||
@ -112,19 +127,24 @@ Variables &Quantified<Derived>::variables()
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
||||
template<class Derived>
|
||||
const Variables &Quantified<Derived>::variables() const
|
||||
inline ExpressionPointer QuantifiedCRTP<Derived>::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<class Derived>
|
||||
inline ExpressionPointer Quantified<Derived>::reduced()
|
||||
inline ExpressionPointer QuantifiedCRTP<Derived>::negationNormalized()
|
||||
{
|
||||
BOOST_ASSERT(m_argument);
|
||||
|
||||
m_argument = m_argument->prenex();
|
||||
m_argument = m_argument->negationNormalized();
|
||||
|
||||
return this;
|
||||
}
|
||||
@ -132,32 +152,20 @@ inline ExpressionPointer Quantified<Derived>::reduced()
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
||||
template<class Derived>
|
||||
inline ExpressionPointer Quantified<Derived>::negationNormalized()
|
||||
inline ExpressionPointer QuantifiedCRTP<Derived>::prenex(Expression::Type)
|
||||
{
|
||||
BOOST_ASSERT(m_argument);
|
||||
|
||||
m_argument = m_argument->prenex();
|
||||
|
||||
return this;
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
||||
template<class Derived>
|
||||
inline ExpressionPointer Quantified<Derived>::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<class Derived>
|
||||
inline ExpressionPointer Quantified<Derived>::simplified()
|
||||
inline ExpressionPointer QuantifiedCRTP<Derived>::simplified()
|
||||
{
|
||||
BOOST_ASSERT(m_argument);
|
||||
|
||||
@ -183,7 +191,7 @@ inline ExpressionPointer Quantified<Derived>::simplified()
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
||||
template<class Derived>
|
||||
inline void Quantified<Derived>::print(std::ostream &ostream) const
|
||||
inline void QuantifiedCRTP<Derived>::print(std::ostream &ostream) const
|
||||
{
|
||||
ostream << "(" << Derived::Identifier << " (";
|
||||
|
||||
|
@ -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<expressions::Exists *>(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);
|
||||
|
||||
|
@ -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);
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
@ -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);
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
@ -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))))))");
|
||||
}
|
||||
|
Reference in New Issue
Block a user