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

Correctly implemented hiding predicates with nested arguments.

Browse Source
This commit is contained in:
Patrick Lühne 2017-06-12 02:21:16 +02:00
parent 1d172589f5
commit a4cd133ba7
Signed by: patrick
GPG Key ID: 05F3611E97A70ABF
2 changed files with 21 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
src/anthem/Translation.cpp
View File

@ -58,14 +58,15 @@ void translate(const char *fileName, std::istream &stream, Context &context)
Clingo::parse_program(fileContent.c_str(), translateStatement, logger);
if (context.performSimplification)
for (auto &scopedFormula : scopedFormulas)
simplify(scopedFormula.formula);
ast::PrintContext printContext(context);
if (!context.performCompletion)
{
// Simplify output if specified
if (context.performSimplification)
for (auto &scopedFormula : scopedFormulas)
simplify(scopedFormula.formula);
if (context.visiblePredicateSignatures)
context.logger.log(output::Priority::Warning) << "#show statements are ignored because completion is not enabled";
@ -78,9 +79,10 @@ void translate(const char *fileName, std::istream &stream, Context &context)
return;
}
// Perform completion
auto completedFormulas = complete(std::move(scopedFormulas), context);
// TODO: rethink simplification steps
// Simplify output if specified
if (context.performSimplification)
for (auto &completedFormula : completedFormulas)
simplify(completedFormula);

14
tests/TestHiddenPredicateElimination.cpp
View File

@ -137,4 +137,18 @@ TEST_CASE("[hidden predicate elimination] Hidden predicates are correctly elimin
CHECK(output.str() ==
"forall V1, V2 (a(V1, V2) <-> exists U1 ((V1 = 1 and V2 = 2 and U1 = 3) or (V1 = 2 and V2 = 4 and U1 = 6)))\n");
}
SECTION("nested arguments are correctly handled when hiding predicates")
{
input <<
"a(X) :- b(c(X)).\n"
"b(c(X)) :- c(X).\n"
"c(1..4).\n"
"#show a/1.";
anthem::translate("input", input, context);
// TODO: simplify further
CHECK(output.str() ==
"forall V1 (a(V1) <-> exists U1 (c(V1) = c(U1) and U1 in 1..4))\n");
}
}