patrick
/
anthem
1
0
Fork 0
Code Issues 15 Releases 21 Activity

Improved output of negated literals and added unit test.

This commit is contained in:
Patrick Lühne 2016-11-24 16:04:53 +01:00
parent b675946927
commit fc89a65ce7
Signed by: patrick
GPG Key ID: 05F3611E97A70ABF
3 changed files with 14 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
include/anthem/Body.h
View File

@ -87,12 +87,10 @@ struct TermPrintVisitor
<< argument;
}
outputStream << " " << Clingo::AST::BinaryOperator::And << " ";
if (literal.sign == Clingo::AST::Sign::Negation)
outputStream << Clingo::AST::Sign::Negation << " ";
outputStream << output::Function(function.name) << "(";
outputStream
<< " " << Clingo::AST::BinaryOperator::And << " "
<< literal.sign
<< output::Function(function.name) << "(";
for (auto i = function.arguments.cbegin(); i != function.arguments.cend(); i++)
{

4
include/anthem/Head.h
View File

@ -222,8 +222,8 @@ struct HeadLiteralPrintSubstitutedVisitor
{
if (literal.sign == Clingo::AST::Sign::DoubleNegation)
throwErrorAtLocation(literal.location, "double-negated literals currently unsupported", context);
else if (literal.sign == Clingo::AST::Sign::Negation)
context.logger.outputStream() << Clingo::AST::Sign::Negation << " ";
context.logger.outputStream() << literal.sign;
literal.data.accept(LiteralPrintSubstitutedVisitor(), literal, context);
}

8
tests/TestTranslation.cpp
View File

@ -120,4 +120,12 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]")
REQUIRE(output.str() == "V1 in X and V2 in (1,) and exists X1, X2 (X1 in X and X2 in (2,) and q(X1, X2)) -> p(V1, V2)\n");
}
SECTION("single negation")
{
input << "not p(X, 1) :- not q(X, 2).";
anthem::translate("input", input, context);
REQUIRE(output.str() == "V1 in X and V2 in 1 and exists X1, X2 (X1 in X and X2 in 2 and not q(X1, X2)) -> not p(V1, V2)\n");
}
}