diff --git a/src/anthem/Translation.cpp b/src/anthem/Translation.cpp index 9601a83..f819e37 100644 --- a/src/anthem/Translation.cpp +++ b/src/anthem/Translation.cpp @@ -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); diff --git a/tests/TestHiddenPredicateElimination.cpp b/tests/TestHiddenPredicateElimination.cpp index b1b17ed..fa7a6b5 100644 --- a/tests/TestHiddenPredicateElimination.cpp +++ b/tests/TestHiddenPredicateElimination.cpp @@ -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"); + } }