Started implementing translation for derived predicates.

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;

include/plasp/pddl/Expression.h

@@ -2,6 +2,7 @@
 #define __PLASP__PDDL__EXPRESSION_H
 
 #include <iosfwd>
+#include <set>
 
 #include <boost/intrusive_ptr.hpp>
 
@@ -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();
+		// Transform such that only existential (and no universal) quantifiers are used
-		virtual ExpressionPointer prenex(Expression::Type lastQuantifierType = Expression::Type::Exists);
+		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<expressions::VariablePointer> &parameters);
+
 		virtual void print(std::ostream &ostream) const = 0;
 
 	protected:

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;

include/plasp/pddl/expressions/And.h

@@ -24,7 +24,6 @@ class And: public NAry<And>
 		static const std::string Identifier;
 
 	public:
-		ExpressionPointer disjunctionNormalized() override;
 		ExpressionPointer decomposed(DerivedPredicates &derivedPredicates) override;
 };
 

include/plasp/pddl/expressions/At.h

@@ -40,10 +40,10 @@ class At: public ExpressionCRTP<At>
 		ExpressionPointer argument() const;
 
 		ExpressionPointer reduced() override;
-		ExpressionPointer negationNormalized() override;
+		ExpressionPointer existentiallyQuantified() override;
-		ExpressionPointer prenex(Expression::Type lastExpressionType) override;
 		ExpressionPointer simplified() override;
-		ExpressionPointer disjunctionNormalized() override;
+
+		void collectParameters(std::set<VariablePointer> &parameters) override;
 
 		void print(std::ostream &ostream) const override;
 

include/plasp/pddl/expressions/Binary.h

@@ -32,13 +32,14 @@ class Binary: public ExpressionCRTP<Derived>
 		ExpressionPointer copy() override;
 
 		void setArgument(size_t i, ExpressionPointer argument);
+		std::array<ExpressionPointer, 2> &arguments();
 		const std::array<ExpressionPointer, 2> &arguments() const;
 
 		ExpressionPointer reduced() override;
-		ExpressionPointer negationNormalized() override;
+		ExpressionPointer existentiallyQuantified() override;
-		ExpressionPointer prenex(Expression::Type lastExpressionType) override;
 		ExpressionPointer simplified() override;
-		ExpressionPointer disjunctionNormalized() override;
+
+		void collectParameters(std::set<VariablePointer> &parameters) override;
 
 		void print(std::ostream &ostream) const override;
 
@@ -100,6 +101,14 @@ void Binary<Derived>::setArgument(size_t i, ExpressionPointer expression)
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
+template<class Derived>
+std::array<ExpressionPointer, 2> &Binary<Derived>::arguments()
+{
+	return m_arguments;
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
 template<class Derived>
 const std::array<ExpressionPointer, 2> &Binary<Derived>::arguments() const
 {
@@ -111,11 +120,11 @@ const std::array<ExpressionPointer, 2> &Binary<Derived>::arguments() const
 template<class Derived>
 inline ExpressionPointer Binary<Derived>::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<Derived>::reduced()
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
 template<class Derived>
-inline ExpressionPointer Binary<Derived>::negationNormalized()
+inline ExpressionPointer Binary<Derived>::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<Derived>::negationNormalized()
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-template<class Derived>
-inline ExpressionPointer Binary<Derived>::prenex(Expression::Type)
-{
-	// TODO: implement by refactoring binary expressions
-	return this;
-}
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
 template<class Derived>
 inline ExpressionPointer Binary<Derived>::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<Derived>::simplified()
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
 template<class Derived>
-inline ExpressionPointer Binary<Derived>::disjunctionNormalized()
+inline void Binary<Derived>::collectParameters(std::set<VariablePointer> &parameters)
 {
-	for (size_t i = 0; i < m_arguments.size(); i++)
+	for (const auto &argument : m_arguments)
-	{
+		argument->collectParameters(parameters);
-		BOOST_ASSERT(m_arguments[i]);
-
-		m_arguments[i] = m_arguments[i]->disjunctionNormalized();
-	}
-
-	return this;
 }
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////

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 <set>
+
 #include <plasp/pddl/Expression.h>
 
 namespace plasp
@@ -24,19 +26,22 @@ class DerivedPredicate: public ExpressionCRTP<DerivedPredicate>
 		// TODO: consider implementing parsing functions for compatibility with older PDDL versions
 
 	public:
-		explicit DerivedPredicate(size_t id);
+		void setPreconditions(std::vector<Expressions> &&preconditions);
+		const std::vector<Expressions> &preconditions() const;
 
-		size_t id() const;
+		const std::set<VariablePointer> &parameters() const;
 
-		void setArgument(ExpressionPointer argument);
+		void collectParameters(std::set<VariablePointer> &parameters) override;
-		ExpressionPointer argument() const;
 
 		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<Expressions> m_preconditions;
+
+		std::set<VariablePointer> m_parameters;
 };
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////

include/plasp/pddl/expressions/Exists.h

@@ -22,9 +22,6 @@ class Exists: public QuantifiedCRTP<Exists>
 		static const Expression::Type ExpressionType = Expression::Type::Exists;
 
 		static const std::string Identifier;
-
-	public:
-		ExpressionPointer decomposed(DerivedPredicates &derivedPredicates) override;
 };
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////

include/plasp/pddl/expressions/ForAll.h

@@ -24,7 +24,7 @@ class ForAll: public QuantifiedCRTP<ForAll>
 		static const std::string Identifier;
 
 	public:
-		ExpressionPointer decomposed(DerivedPredicates &derivedPredicates) override;
+		ExpressionPointer existentiallyQuantified() override;
 };
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////

include/plasp/pddl/expressions/NAry.h

@@ -37,10 +37,10 @@ class NAry: public ExpressionCRTP<Derived>
 		const Expressions &arguments() const;
 
 		ExpressionPointer reduced() override;
-		ExpressionPointer negationNormalized() override;
+		ExpressionPointer existentiallyQuantified() override;
-		ExpressionPointer prenex(Expression::Type lastExpressionType) override;
 		ExpressionPointer simplified() override;
-		ExpressionPointer disjunctionNormalized() override;
+
+		void collectParameters(std::set<VariablePointer> &parameters) override;
 
 		void print(std::ostream &ostream) const override;
 
@@ -143,11 +143,11 @@ Expressions &NAry<Derived>::arguments()
 template<class Derived>
 inline ExpressionPointer NAry<Derived>::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<Derived>::reduced()
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
 template<class Derived>
-inline ExpressionPointer NAry<Derived>::negationNormalized()
+inline ExpressionPointer NAry<Derived>::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<Derived>::negationNormalized()
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-template<class Derived>
-inline ExpressionPointer NAry<Derived>::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<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;
-}
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
 template<class Derived>
 inline ExpressionPointer NAry<Derived>::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<Derived &>(*argument);
-		auto &nAryExpression = dynamic_cast<Derived &>(*child);
 
 		BOOST_ASSERT(!nAryExpression.arguments().empty());
 
@@ -292,16 +208,10 @@ inline ExpressionPointer NAry<Derived>::simplified()
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
 template<class Derived>
-inline ExpressionPointer NAry<Derived>::disjunctionNormalized()
+inline void NAry<Derived>::collectParameters(std::set<VariablePointer> &parameters)
 {
-	for (size_t i = 0; i < m_arguments.size(); i++)
+	for (const auto &argument : m_arguments)
-	{
+		argument->collectParameters(parameters);
-		BOOST_ASSERT(m_arguments[i]);
-
-		m_arguments[i] = m_arguments[i]->disjunctionNormalized();
-	}
-
-	return this;
 }
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
@@ -311,12 +221,11 @@ inline void NAry<Derived>::print(std::ostream &ostream) const
 {
 	ostream << "(" << Derived::Identifier;
 
-	std::for_each(m_arguments.begin(), m_arguments.end(),
+	for (const auto &argument : m_arguments)
-		[&](auto &argument)
+	{
-		{
+		ostream << " ";
-			ostream << " ";
+		argument->print(ostream);
-			argument->print(ostream);
+	}
-		});
 
 	ostream << ")";
 }

include/plasp/pddl/expressions/Not.h

@@ -35,12 +35,12 @@ class Not: public ExpressionCRTP<Not>
 		ExpressionPointer argument() const;
 
 		ExpressionPointer reduced() override;
-		ExpressionPointer negationNormalized() override;
+		ExpressionPointer existentiallyQuantified() override;
-		ExpressionPointer prenex(Expression::Type lastExpressionType) override;
 		ExpressionPointer simplified() override;
-		ExpressionPointer disjunctionNormalized() override;
 		ExpressionPointer decomposed(DerivedPredicates &derivedPredicates) override;
 
+		void collectParameters(std::set<VariablePointer> &parameters) override;
+
 		void print(std::ostream &ostream) const override;
 
 	protected:

include/plasp/pddl/expressions/Predicate.h

@@ -30,6 +30,10 @@ class Predicate: public ExpressionCRTP<Predicate>
 
 		bool isDeclared() const;
 
+		ExpressionPointer decomposed(expressions::DerivedPredicates &derivedPredicates) override;
+
+		void collectParameters(std::set<VariablePointer> &parameters) override;
+
 		void print(std::ostream &ostream) const override;
 
 	private:

include/plasp/pddl/expressions/Quantified.h

@@ -4,6 +4,7 @@
 #include <plasp/pddl/Context.h>
 #include <plasp/pddl/Expression.h>
 #include <plasp/pddl/ExpressionContext.h>
+#include <plasp/pddl/expressions/DerivedPredicate.h>
 #include <plasp/pddl/expressions/Variable.h>
 
 namespace plasp
@@ -52,10 +53,11 @@ class QuantifiedCRTP: public Quantified
 		ExpressionPointer copy() override;
 
 		ExpressionPointer reduced() override;
-		ExpressionPointer negationNormalized() override;
+		ExpressionPointer existentiallyQuantified() override;
-		ExpressionPointer prenex(Expression::Type lastExpressionType) override;
 		ExpressionPointer simplified() override;
-		ExpressionPointer disjunctionNormalized() override;
+		ExpressionPointer decomposed(expressions::DerivedPredicates &derivedPredicates) override;
+
+		void collectParameters(std::set<VariablePointer> &parameters);
 
 		void print(std::ostream &ostream) const override;
 };
@@ -155,30 +157,17 @@ inline ExpressionPointer QuantifiedCRTP<Derived>::reduced()
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
 template<class Derived>
-inline ExpressionPointer QuantifiedCRTP<Derived>::negationNormalized()
+inline ExpressionPointer QuantifiedCRTP<Derived>::existentiallyQuantified()
 {
 	BOOST_ASSERT(m_argument);
 
-	m_argument = m_argument->negationNormalized();
+	m_argument = m_argument->existentiallyQuantified();
 
 	return this;
 }
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-template<class Derived>
-inline ExpressionPointer QuantifiedCRTP<Derived>::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<class Derived>
 inline ExpressionPointer QuantifiedCRTP<Derived>::simplified()
 {
@@ -206,13 +195,28 @@ inline ExpressionPointer QuantifiedCRTP<Derived>::simplified()
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
 template<class Derived>
-inline ExpressionPointer QuantifiedCRTP<Derived>::disjunctionNormalized()
+inline ExpressionPointer QuantifiedCRTP<Derived>::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<class Derived>
+inline void QuantifiedCRTP<Derived>::collectParameters(std::set<VariablePointer> &parameters)
+{
+	m_argument->collectParameters(parameters);
+
+	// Remove bound variables
+	for (const auto &variable : m_variables)
+		parameters.erase(variable);
 }
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////

include/plasp/pddl/expressions/Variable.h

@@ -39,6 +39,8 @@ class Variable: public ExpressionCRTP<Variable>
 		void setDirty(bool isDirty = true);
 		bool isDirty() const;
 
+		void collectParameters(std::set<VariablePointer> &parameters) override;
+
 		void print(std::ostream &ostream) const override;
 
 	private:

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

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);
 		});
 }
 

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<expressions::VariablePointer> &)
+{
+	throw output::TranslatorException("expression parameters could not be collected (expression not normalized)");
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
 ExpressionPointer parseEffectBodyExpression(Context &context, ExpressionContext &expressionContext);
 ExpressionPointer parsePredicate(Context &context, ExpressionContext &expressionContext);
 

src/plasp/pddl/TranslatorASP.cpp

@@ -19,6 +19,15 @@ namespace pddl
 //
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
+template<class T>
+void translateVariablesHead(output::ColorStream &outputStream, const T &variables);
+template<class T>
+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 << "<derived>";
+
+				return;
+			}
+
+			// TODO: implement
+			//m_outputStream << output::String(derivedPredicate->name().c_str());
+			m_outputStream << "<derived>";
+			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 translateExpression =
-			const auto translateLiteral =
 				[&](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
+				switch (precondition.expressionType())
-					|| precondition.expressionType() == Expression::Type::Not)
 				{
-					translateLiteral("precondition", precondition);
+					case Expression::Type::And:
-				}
+					{
-				// Assuming a conjunction
+						const auto &andExpression = dynamic_cast<const expressions::And &>(precondition);
-				else
-				{
-					if (precondition.expressionType() != Expression::Type::And)
-						throw output::TranslatorException("only “and” expressions and (negated) predicates supported as action preconditions currently");
 
-					const auto &andExpression = dynamic_cast<const expressions::And &>(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(),
+						break;
-						[&](const auto argument)
+					}
-						{
+					case Expression::Type::Predicate:
-							translateLiteral("precondition", *argument);
+					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<class T>
+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<class T>
+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<const expressions::PrimitiveType &>(*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<const expressions::Predicate &>(literal);
 
-		m_outputStream << output::Keyword("variable") << "(";
+		outputStream << output::Keyword("variable") << "(";
-		this->translatePredicate(predicate);
+		translatePredicate(outputStream, predicate);
-		m_outputStream << "), " << output::Keyword("value") << "(";
+		outputStream << "), " << output::Keyword("value") << "(";
-		this->translatePredicate(predicate);
+		translatePredicate(outputStream, predicate);
-		m_outputStream << ", " << output::Boolean("true") << ")";
+		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<const expressions::Predicate &>(*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<const expressions::DerivedPredicate &>(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<const expressions::Constant &>(**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<const expressions::Variable &>(**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<const expressions::Predicate &>(*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 << ").";
 			});

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<expressions::Or *>(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
+	derivedPredicates.emplace_back(new DerivedPredicate());
-	std::for_each(m_arguments.begin(), m_arguments.end(),
+	auto &derivedPredicate = derivedPredicates.back();
-		[&](auto &argument)
-		{
-			if (argument->expressionType() == Expression::Type::Not)
-			{
-				argument = argument->decomposed(derivedPredicates);
-				return;
-			}
 
-			if (argument->expressionType() != Expression::Type::Predicate)
+	for (auto &argument : m_arguments)
-				return;
+		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;
 }
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////

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<VariablePointer> &parameters)
 {
-	BOOST_ASSERT(m_argument);
+	m_argument->collectParameters(parameters);
-
-	m_argument = m_argument->disjunctionNormalized();
-
-	return this;
 }
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////

src/plasp/pddl/expressions/DerivedPredicate.cpp

@@ -16,39 +16,97 @@ namespace expressions
 //
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-DerivedPredicate::DerivedPredicate(size_t id)
+void DerivedPredicate::setPreconditions(std::vector<Expressions> &&preconditions)
-:	m_id{id}
 {
+	m_preconditions = std::move(preconditions);
 }
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-size_t DerivedPredicate::id() const
+const std::vector<Expressions> &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<VariablePointer> &DerivedPredicate::parameters() const
 {
-	return m_argument;
+	return m_parameters;
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+void DerivedPredicate::collectParameters(std::set<VariablePointer> &parameters)
+{
+	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 <no name> ";
+	ostream << "(:derived <no name>";
-	m_argument->print(ostream);
+
-	ostream << ")";
+	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 << "))";
 }
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////

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;
-}
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
 }
 }
 }

src/plasp/pddl/expressions/ForAll.cpp

@@ -3,7 +3,8 @@
 #include <algorithm>
 #include <iostream>
 
-#include <plasp/pddl/expressions/DerivedPredicate.h>
+#include <plasp/pddl/expressions/Exists.h>
+#include <plasp/pddl/expressions/Not.h>
 
 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()));
+	auto existsExpression = ExistsPointer(new Exists());
-	derivedPredicates.push_back(derivedPredicate);
+	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;
 }
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////

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
+	m_argument = m_argument->existentiallyQuantified();
-	if (m_argument->expressionType() == Expression::Type::Not)
-	{
-		auto &argument = dynamic_cast<Not &>(*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<Not &>(*m_argument);
-
-		return argument.m_argument;
-	}
-
-	// De Morgan for negative conjunctions
-	if (m_argument->expressionType() == Expression::Type::And)
-	{
-		auto &andExpression = dynamic_cast<And &>(*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<Or &>(*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<Exists &>(*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<ForAll &>(*m_argument);
-		auto existsExpression = ExistsPointer(new Exists);
-
-		existsExpression->setArgument(forAllExpression.argument()->negated());
-
-		return existsExpression->negationNormalized();
-	}
 
 	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 &notExpression = dynamic_cast<expressions::Not &>(*m_argument);
+
+		return notExpression.argument();
+	}
+
 	return this;
 }
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-ExpressionPointer Not::disjunctionNormalized()
+void Not::collectParameters(std::set<VariablePointer> &parameters)
 {
-	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;
-}
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
 }
 }
 }

src/plasp/pddl/expressions/Or.cpp

@@ -1,5 +1,7 @@
 #include <plasp/pddl/expressions/Or.h>
 
+#include <plasp/output/TranslatorException.h>
+#include <plasp/pddl/expressions/And.h>
 #include <plasp/pddl/expressions/DerivedPredicate.h>
 
 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
+	derivedPredicates.emplace_back(new DerivedPredicate());
-	std::for_each(m_arguments.begin(), m_arguments.end(),
+	auto &derivedPredicate = derivedPredicates.back();
-		[&](auto &argument)
+
+	std::vector<Expressions> 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<expressions::And &>(*argument);
-		});
 
-	auto derivedPredicate = DerivedPredicatePointer(new DerivedPredicate(derivedPredicates.size()));
+			conjunction = std::move(andExpression.arguments());
-	derivedPredicates.push_back(derivedPredicate);
 
-	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;
 }

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<VariablePointer> &parameters)
+{
+	for (const auto &argument : m_arguments)
+		argument->collectParameters(parameters);
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
 const std::string &Predicate::name() const
 {
 	return m_name;

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<std::string>("?");
-
-	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<VariablePointer> &parameters)
+{
+	parameters.emplace(this);
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
 void Variable::print(std::ostream &ostream) const
 {
 	ostream << "?" << m_name;

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]")
+TEST_CASE("[PDDL normalization] Expressions inside double negations are also simplified", "[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]")
 {
 	auto n1 = expressions::NotPointer(new expressions::Not);
 	auto n2 = expressions::NotPointer(new expressions::Not);
-	auto n3 = expressions::NotPointer(new expressions::Not);
+	auto a1 = expressions::AndPointer(new expressions::And);
-	auto a = expressions::AndPointer(new expressions::And);
+	auto a2 = expressions::AndPointer(new expressions::And);
 
-	a->addArgument(new expressions::Dummy("a"));
+	a2->addArgument(new expressions::Dummy("d"));
-	a->addArgument(new expressions::Dummy("b"));
+	a2->addArgument(new expressions::Dummy("e"));
-	a->addArgument(new expressions::Dummy("c"));
 
-	n3->setArgument(a);
+	a1->addArgument(new expressions::Dummy("a"));
-	n2->setArgument(n3);
+	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 f2 = expressions::ForAllPointer(new expressions::ForAll);
-	auto o1 = expressions::OrPointer(new expressions::Or);
-	auto o2 = expressions::OrPointer(new expressions::Or);
-	auto o3 = expressions::OrPointer(new expressions::Or);
 
-	f->variables() = {new expressions::Variable("v1")};
+	f1->variables() = {v1, v2};
-	f->setArgument(e);
+	e->variables() = {v3, v4};
+	f2->variables() = {v5, v6};
 
-	e->variables() = {new expressions::Variable("v2")};
+	f1->setArgument(e);
-	e->setArgument(o1);
+	e->setArgument(f2);
-
+	f2->setArgument(new expressions::Dummy("a"));
-	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();
 
 	std::stringstream output;
-	normalized->print(output);
+	f1->normalized()->print(output);
 
-	CHECK(output.str() == "(forall (?v1) (exists (?v2) (or "
+	CHECK(output.str() == "(exists (?x ?y) (not (exists (?z ?u ?v ?w) (not (a)))))");
-		"(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))"
-		")))");
 }