Avoiding to decompose “not” expressions if they form simple literals.

This commit is contained in:
Patrick Lühne 2017-06-24 16:02:48 +02:00
parent 079e2ac539
commit d5dd8e849f
Signed by: patrick
GPG Key ID: 05F3611E97A70ABF

View File

@ -120,6 +120,10 @@ normalizedAST::Literal normalizeNested(ast::ImplyPointer<ast::Precondition> &, n
normalizedAST::Literal normalizeNested(ast::NotPointer<ast::Precondition> &not_, normalizedAST::DerivedPredicateDeclarations &derivedPredicates) normalizedAST::Literal normalizeNested(ast::NotPointer<ast::Precondition> &not_, normalizedAST::DerivedPredicateDeclarations &derivedPredicates)
{ {
// “not” expressions may be nested one time to form simple literals
if (not_->argument.is<ast::AtomicFormula>())
return std::make_unique<normalizedAST::Not<normalizedAST::AtomicFormula>>(normalize(std::move(not_->argument.get<ast::AtomicFormula>())));
std::vector<normalizedAST::VariableDeclaration *> parameters; std::vector<normalizedAST::VariableDeclaration *> parameters;
VariableStack variableStack; VariableStack variableStack;