From d056fabb8b8d5ed1abf8cdf7b316b34a5b16c41e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Patrick=20L=C3=BChne?= Date: Thu, 4 May 2017 15:44:37 +0200 Subject: [PATCH] Fixes lost signs with negated 0-ary predicates. --- CHANGELOG.md | 4 ++++ include/anthem/Body.h | 11 +++++++++-- tests/TestTranslation.cpp | 10 +++++++++- 3 files changed, 22 insertions(+), 3 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 7e15001..30402e0 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -2,6 +2,10 @@ ## (unreleased) +Bug Fixes: + +* fixes lost signs with negated 0-ary predicates + ## 0.1.4 (2017-04-12) Features: diff --git a/include/anthem/Body.h b/include/anthem/Body.h index 0f93d1e..4e5bf4e 100644 --- a/include/anthem/Body.h +++ b/include/anthem/Body.h @@ -58,7 +58,14 @@ struct BodyTermTranslateVisitor throwErrorAtLocation(literal.location, "double-negated literals currently unsupported", context); if (function.arguments.empty()) - return ast::Formula::make(std::string(function.name)); + { + auto predicate = ast::Formula::make(std::string(function.name)); + + if (literal.sign == Clingo::AST::Sign::None) + return std::move(predicate); + else if (literal.sign == Clingo::AST::Sign::Negation) + return ast::Formula::make(std::move(predicate)); + } std::vector variables; variables.reserve(function.arguments.size()); @@ -82,7 +89,7 @@ struct BodyTermTranslateVisitor if (literal.sign == Clingo::AST::Sign::None) conjunction.arguments.emplace_back(std::move(predicate)); - else + else if (literal.sign == Clingo::AST::Sign::Negation) conjunction.arguments.emplace_back(ast::Formula::make(std::move(predicate))); context.auxiliaryBodyVariableID += function.arguments.size(); diff --git a/tests/TestTranslation.cpp b/tests/TestTranslation.cpp index 1cd6fd5..b735d33 100644 --- a/tests/TestTranslation.cpp +++ b/tests/TestTranslation.cpp @@ -188,7 +188,15 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") CHECK(output.str() == "((V1 in M and V2 in N and V3 in O and V4 in P and exists X1, X2 (X1 in M and X2 in N and X1 < X2) and exists X3, X4 (X3 in P and X4 in O and X3 != X4)) -> p(V1, V2, V3, V4))\n"); } - SECTION("single negation") + SECTION("single negation with 0-ary predicates") + { + input << "not p :- not q."; + anthem::translate("input", input, context); + + CHECK(output.str() == "(not q -> not p)\n"); + } + + SECTION("single negation with n-ary predicates") { input << "not p(X, 1) :- not q(X, 2)."; anthem::translate("input", input, context);