From c294a29cb2899e3af2de3cee5c644a9b33fc6803 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Patrick=20L=C3=BChne?= Date: Thu, 5 Apr 2018 23:22:25 +0200 Subject: [PATCH] Support placeholders with #external declarations MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This adds support for declaring predicates as placeholders through the “#external” directive in the input language of clingo. Placeholders are not subject to completion. This prevents predicates that represent instance-specific facts from being assumed as universally false by default negation when translating an encoding. This stretches clingo’s usual syntax a bit to make the implementation lightweight. In order to declare a predicate with a specific arity as a placeholder, the following statement needs to be added to the program: #external (). Multiple unit tests cover cases where placeholders are used or not as well as a more complex graph coloring example. --- CHANGELOG.md | 4 ++ include/anthem/ASTUtils.h | 3 +- include/anthem/Context.h | 11 +++- include/anthem/StatementVisitor.h | 41 ++++++++++++++- src/anthem/ASTUtils.cpp | 33 ++++++++++-- src/anthem/Completion.cpp | 2 +- src/anthem/HiddenPredicateElimination.cpp | 45 ++++++++-------- src/anthem/Translation.cpp | 23 +++++++++ tests/TestPlaceholders.cpp | 62 +++++++++++++++++++++++ 9 files changed, 192 insertions(+), 32 deletions(-) create mode 100644 tests/TestPlaceholders.cpp diff --git a/CHANGELOG.md b/CHANGELOG.md index 2bd13ff..79b8600 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -2,6 +2,10 @@ ## (unreleased) +### Features + +* support for declaring placeholders with the `#external` directive + ### Internal * drops Boost dependency in favor of the header-only command-line option library [cxxopts](https://github.com/jarro2783/cxxopts) diff --git a/include/anthem/ASTUtils.h b/include/anthem/ASTUtils.h index a0afb56..dfb2470 100644 --- a/include/anthem/ASTUtils.h +++ b/include/anthem/ASTUtils.h @@ -5,6 +5,7 @@ #include #include +#include namespace anthem { @@ -40,7 +41,7 @@ class VariableStack bool matches(const Predicate &lhs, const Predicate &rhs); bool matches(const Predicate &predicate, const PredicateSignature &signature); bool matches(const PredicateSignature &lhs, const PredicateSignature &rhs); -void collectPredicateSignatures(const Formula &formula, std::vector &predicateSignatures); +void collectPredicateSignatures(const Formula &formula, std::vector &predicateSignatures, Context &context); //////////////////////////////////////////////////////////////////////////////////////////////////// // Replacing Variables diff --git a/include/anthem/Context.h b/include/anthem/Context.h index 33ec6ac..bfaa196 100644 --- a/include/anthem/Context.h +++ b/include/anthem/Context.h @@ -16,6 +16,14 @@ namespace anthem // //////////////////////////////////////////////////////////////////////////////////////////////////// +struct PredicateSignatureMeta +{ + ast::PredicateSignature predicateSignature; + bool used{false}; +}; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + struct Context { Context() = default; @@ -30,7 +38,8 @@ struct Context bool performSimplification = false; bool performCompletion = false; - std::optional> visiblePredicateSignatures; + std::optional> visiblePredicateSignatures; + std::optional> externalPredicateSignatures; ast::ParenthesisStyle parenthesisStyle = ast::ParenthesisStyle::Normal; }; diff --git a/include/anthem/StatementVisitor.h b/include/anthem/StatementVisitor.h index 5671eb3..28e38e9 100644 --- a/include/anthem/StatementVisitor.h +++ b/include/anthem/StatementVisitor.h @@ -176,7 +176,8 @@ struct StatementVisitor context.logger.log(output::Priority::Debug, statement.location) << "showing “" << signature.name() << "/" << signature.arity() << "”"; - context.visiblePredicateSignatures.value().emplace_back(std::string(signature.name()), signature.arity()); + auto predicateSignature = ast::PredicateSignature{std::string(signature.name()), signature.arity()}; + context.visiblePredicateSignatures.value().emplace_back(PredicateSignatureMeta{std::move(predicateSignature)}); } void visit(const Clingo::AST::ShowTerm &, const Clingo::AST::Statement &statement, std::vector &, Context &) @@ -184,6 +185,44 @@ struct StatementVisitor throw LogicException(statement.location, "only #show statements for atoms (not terms) are supported currently"); } + void visit(const Clingo::AST::External &external, const Clingo::AST::Statement &statement, std::vector &, Context &context) + { + const auto fail = + [&]() + { + throw LogicException(statement.location, "only #external declarations of the form “#external ().” supported"); + }; + + if (!external.body.empty()) + fail(); + + if (!external.atom.data.is()) + fail(); + + const auto &predicate = external.atom.data.get(); + + if (predicate.arguments.size() != 1) + fail(); + + const auto &arityArgument = predicate.arguments.front(); + + if (!arityArgument.data.is()) + fail(); + + const auto &aritySymbol = arityArgument.data.get(); + + if (aritySymbol.type() != Clingo::SymbolType::Number) + fail(); + + const size_t arity = arityArgument.data.get().number(); + + if (!context.externalPredicateSignatures) + context.externalPredicateSignatures.emplace(); + + auto predicateSignature = ast::PredicateSignature{std::string(predicate.name), arity}; + context.externalPredicateSignatures->emplace_back(PredicateSignatureMeta{std::move(predicateSignature)}); + } + template void visit(const T &, const Clingo::AST::Statement &statement, std::vector &, Context &) { diff --git a/src/anthem/ASTUtils.cpp b/src/anthem/ASTUtils.cpp index db98911..3ff91c9 100644 --- a/src/anthem/ASTUtils.cpp +++ b/src/anthem/ASTUtils.cpp @@ -194,7 +194,7 @@ struct CollectFreeVariablesVisitor struct CollectPredicateSignaturesVisitor : public RecursiveFormulaVisitor { - static void accept(const Predicate &predicate, const Formula &, std::vector &predicateSignatures) + static void accept(const Predicate &predicate, const Formula &, std::vector &predicateSignatures, Context &context) { const auto predicateSignatureMatches = [&predicate](const auto &predicateSignature) @@ -206,12 +206,35 @@ struct CollectPredicateSignaturesVisitor : public RecursiveFormulaVisitorused = true; + return; + } + } + + predicateSignatures.emplace_back(std::move(predicateSignature)); } // Ignore all other types of expressions template - static void accept(const T &, const Formula &, std::vector &) + static void accept(const T &, const Formula &, std::vector &, const Context &) { } }; @@ -240,10 +263,10 @@ bool matches(const PredicateSignature &lhs, const PredicateSignature &rhs) //////////////////////////////////////////////////////////////////////////////////////////////////// // TODO: remove const_cast -void collectPredicateSignatures(const Formula &formula, std::vector &predicateSignatures) +void collectPredicateSignatures(const Formula &formula, std::vector &predicateSignatures, Context &context) { auto &formulaMutable = const_cast(formula); - formulaMutable.accept(CollectPredicateSignaturesVisitor(), formulaMutable, predicateSignatures); + formulaMutable.accept(CollectPredicateSignaturesVisitor(), formulaMutable, predicateSignatures, context); } //////////////////////////////////////////////////////////////////////////////////////////////////// diff --git a/src/anthem/Completion.cpp b/src/anthem/Completion.cpp index c8c435e..93280bc 100644 --- a/src/anthem/Completion.cpp +++ b/src/anthem/Completion.cpp @@ -165,7 +165,7 @@ std::vector complete(std::vector &&scopedFormu // Get a list of all predicates for (const auto &scopedFormula : scopedFormulas) - ast::collectPredicateSignatures(scopedFormula.formula, predicateSignatures); + ast::collectPredicateSignatures(scopedFormula.formula, predicateSignatures, context); std::sort(predicateSignatures.begin(), predicateSignatures.end(), [](const auto &lhs, const auto &rhs) diff --git a/src/anthem/HiddenPredicateElimination.cpp b/src/anthem/HiddenPredicateElimination.cpp index 31ed6c4..014deb1 100644 --- a/src/anthem/HiddenPredicateElimination.cpp +++ b/src/anthem/HiddenPredicateElimination.cpp @@ -194,41 +194,40 @@ void eliminateHiddenPredicates(const std::vector &predi return; } - const auto &visiblePredicateSignatures = context.visiblePredicateSignatures.value(); - - // Check for undeclared predicates that are requested to be shown - for (const auto &visiblePredicateSignature : visiblePredicateSignatures) - { - const auto matchesPredicateSignature = - [&](const auto &predicateSignature) - { - return ast::matches(predicateSignature, visiblePredicateSignature); - }; - - const auto matchingPredicateSignature = - std::find_if(predicateSignatures.cbegin(), predicateSignatures.cend(), matchesPredicateSignature); - - if (matchingPredicateSignature == predicateSignatures.cend()) - context.logger.log(output::Priority::Warning) << "cannot show undeclared predicate “" << visiblePredicateSignature.name << "/" << visiblePredicateSignature.arity <<"”"; - } + auto &visiblePredicateSignatures = context.visiblePredicateSignatures.value(); // Replace all occurrences of hidden predicates for (size_t i = 0; i < predicateSignatures.size(); i++) { auto &predicateSignature = predicateSignatures[i]; - const auto matchesVisiblePredicateSignature = - [&](const auto &visiblePredicateSignature) + const auto matchesPredicateSignature = + [&](const auto &otherPredicateSignature) { - return ast::matches(predicateSignature, visiblePredicateSignature); + return ast::matches(predicateSignature, otherPredicateSignature.predicateSignature); }; - const auto matchingPredicateSignature = - std::find_if(visiblePredicateSignatures.cbegin(), visiblePredicateSignatures.cend(), matchesVisiblePredicateSignature); + const auto matchingVisiblePredicateSignature = + std::find_if(visiblePredicateSignatures.begin(), visiblePredicateSignatures.end(), matchesPredicateSignature); // If the predicate ought to be visible, don’t eliminate it - if (matchingPredicateSignature != visiblePredicateSignatures.cend()) + if (matchingVisiblePredicateSignature != visiblePredicateSignatures.end()) + { + matchingVisiblePredicateSignature->used = true; continue; + } + + // Check that the predicate is not declared #external + if (context.externalPredicateSignatures) + { + const auto &externalPredicateSignatures = context.externalPredicateSignatures.value(); + + const auto matchingExternalPredicateSignature = + std::find_if(externalPredicateSignatures.cbegin(), externalPredicateSignatures.cend(), matchesPredicateSignature); + + if (matchingExternalPredicateSignature != externalPredicateSignatures.cend()) + continue; + } context.logger.log(output::Priority::Debug) << "eliminating “" << predicateSignature.name << "/" << predicateSignature.arity << "”"; diff --git a/src/anthem/Translation.cpp b/src/anthem/Translation.cpp index f819e37..cf521f1 100644 --- a/src/anthem/Translation.cpp +++ b/src/anthem/Translation.cpp @@ -70,6 +70,9 @@ void translate(const char *fileName, std::istream &stream, Context &context) if (context.visiblePredicateSignatures) context.logger.log(output::Priority::Warning) << "#show statements are ignored because completion is not enabled"; + if (context.externalPredicateSignatures) + context.logger.log(output::Priority::Warning) << "#external statements are ignored because completion is not enabled"; + for (const auto &scopedFormula : scopedFormulas) { ast::print(context.logger.outputStream(), scopedFormula.formula, printContext); @@ -82,6 +85,26 @@ void translate(const char *fileName, std::istream &stream, Context &context) // Perform completion auto completedFormulas = complete(std::move(scopedFormulas), context); + // Check for #show statements with undeclared predicates + if (context.visiblePredicateSignatures) + for (const auto &predicateSignature : context.visiblePredicateSignatures.value()) + if (!predicateSignature.used) + context.logger.log(output::Priority::Warning) + << "#show declaration of “" + << predicateSignature.predicateSignature.name + << "/" << predicateSignature.predicateSignature.arity + << "” does not match any eligible predicate"; + + // Check for #external statements with undeclared predicates + if (context.externalPredicateSignatures) + for (const auto &predicateSignature : context.externalPredicateSignatures.value()) + if (!predicateSignature.used) + context.logger.log(output::Priority::Warning) + << "#external declaration of “" + << predicateSignature.predicateSignature.name + << "/" << predicateSignature.predicateSignature.arity + << "” does not match any eligible predicate"; + // Simplify output if specified if (context.performSimplification) for (auto &completedFormula : completedFormulas) diff --git a/tests/TestPlaceholders.cpp b/tests/TestPlaceholders.cpp new file mode 100644 index 0000000..3cc4652 --- /dev/null +++ b/tests/TestPlaceholders.cpp @@ -0,0 +1,62 @@ +#include + +#include + +#include +#include +#include + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +TEST_CASE("[placeholders] Programs with placeholders are correctly completed", "[placeholders]") +{ + std::stringstream input; + std::stringstream output; + std::stringstream errors; + + anthem::output::Logger logger(output, errors); + anthem::Context context(std::move(logger)); + context.performSimplification = true; + context.performCompletion = true; + + SECTION("no placeholders") + { + input << + "colored(V, red) :- vertex(V), not colored(V, green), not colored(V, blue)."; + anthem::translate("input", input, context); + + CHECK(output.str() == + "forall V1, V2 (colored(V1, V2) <-> (V2 = red and vertex(V1) and not colored(V1, green) and not colored(V1, blue)))\n" + "forall V3 not vertex(V3)\n"); + } + + SECTION("single placeholder") + { + input << + "#external vertex(1).\n" + "colored(V, red) :- vertex(V), not colored(V, green), not colored(V, blue)."; + anthem::translate("input", input, context); + + CHECK(output.str() == + "forall V1, V2 (colored(V1, V2) <-> (V2 = red and vertex(V1) and not colored(V1, green) and not colored(V1, blue)))\n"); + } + + SECTION("complex example: graph coloring") + { + input << + "#external color(1).\n" + "#external edge(2).\n" + "#external vertex(1).\n" + "#show color/2.\n" + "{color(V, C)} :- vertex(V), color(C).\n" + "covered(V) :- color(V, _).\n" + ":- vertex(V), not covered(V).\n" + ":- color(V1, C), color(V2, C), edge(V1, V2)."; + anthem::translate("input", input, context); + + CHECK(output.str() == + "forall V1, V2 (color(V1, V2) <-> (vertex(V1) and color(V2) and color(V1, V2)))\n" + "forall U1 not (vertex(U1) and not exists U2 color(U1, U2))\n" + "forall U3, U4, U5 not (color(U3, U4) and color(U5, U4) and edge(U3, U5))\n"); + } +}