Implemented De Morgan normalization for quantified expressions.

This commit is contained in:
Patrick Lühne 2016-09-06 17:43:47 +02:00
parent bd2ef96216
commit ad6b3d60eb

View File

@ -1,6 +1,8 @@
#include <plasp/pddl/expressions/Not.h>
#include <plasp/pddl/expressions/And.h>
#include <plasp/pddl/expressions/Exists.h>
#include <plasp/pddl/expressions/ForAll.h>
#include <plasp/pddl/expressions/Or.h>
namespace plasp
@ -99,6 +101,28 @@ ExpressionPointer Not::negationNormalized()
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;
}