From 3e096e39aa58a801b208ac3964612f2541fe7310 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 in order 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 input program: --- include/anthem/Context.h | 1 + include/anthem/StatementVisitor.h | 37 ++++++++++++++++++++++ src/anthem/Completion.cpp | 38 +++++++++++++++++++++++ src/anthem/HiddenPredicateElimination.cpp | 24 ++++++++++---- src/anthem/Translation.cpp | 3 ++ 5 files changed, 97 insertions(+), 6 deletions(-) diff --git a/include/anthem/Context.h b/include/anthem/Context.h index 33ec6ac..88ac927 100644 --- a/include/anthem/Context.h +++ b/include/anthem/Context.h @@ -31,6 +31,7 @@ struct Context bool performCompletion = false; 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..0c41897 100644 --- a/include/anthem/StatementVisitor.h +++ b/include/anthem/StatementVisitor.h @@ -184,6 +184,43 @@ 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 auto &arity = arityArgument.data.get().number(); + + if (!context.externalPredicateSignatures) + context.externalPredicateSignatures.emplace(); + + context.externalPredicateSignatures->emplace_back(std::string(predicate.name), arity); + } + template void visit(const T &, const Clingo::AST::Statement &statement, std::vector &, Context &) { diff --git a/src/anthem/Completion.cpp b/src/anthem/Completion.cpp index c8c435e..4c8c557 100644 --- a/src/anthem/Completion.cpp +++ b/src/anthem/Completion.cpp @@ -180,9 +180,47 @@ std::vector complete(std::vector &&scopedFormu std::vector completedFormulas; + // Warn about incorrect #external declarations + if (context.externalPredicateSignatures) + for (const auto &externalPredicateSignature : *context.externalPredicateSignatures) + { + // TODO: avoid code duplication + const auto matchesPredicateSignature = + [&](const auto &otherPredicateSignature) + { + return ast::matches(externalPredicateSignature, otherPredicateSignature); + }; + + const auto matchingPredicateSignature = + std::find_if(predicateSignatures.cbegin(), predicateSignatures.cend(), matchesPredicateSignature); + + if (matchingPredicateSignature == predicateSignatures.cend()) + context.logger.log(output::Priority::Warning) << "#external declaration of “" << externalPredicateSignature.name << "/" << externalPredicateSignature.arity <<"” does not match any known predicate"; + } + // Complete predicates for (const auto &predicateSignature : predicateSignatures) + { + // Don’t complete predicates that are declared #external + if (context.externalPredicateSignatures) + { + const auto matchesPredicateSignature = + [&](const auto &otherPredicateSignature) + { + return ast::matches(predicateSignature, otherPredicateSignature); + }; + + const auto &externalPredicateSignatures = context.externalPredicateSignatures.value(); + + const auto matchingExternalPredicateSignature = + std::find_if(externalPredicateSignatures.cbegin(), externalPredicateSignatures.cend(), matchesPredicateSignature); + + if (matchingExternalPredicateSignature != externalPredicateSignatures.cend()) + continue; + } + completedFormulas.emplace_back(completePredicate(predicateSignature, scopedFormulas)); + } // Complete integrity constraints for (auto &scopedFormula : scopedFormulas) diff --git a/src/anthem/HiddenPredicateElimination.cpp b/src/anthem/HiddenPredicateElimination.cpp index 31ed6c4..ee46f16 100644 --- a/src/anthem/HiddenPredicateElimination.cpp +++ b/src/anthem/HiddenPredicateElimination.cpp @@ -217,19 +217,31 @@ void eliminateHiddenPredicates(const std::vector &predi { 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); }; - const auto matchingPredicateSignature = - std::find_if(visiblePredicateSignatures.cbegin(), visiblePredicateSignatures.cend(), matchesVisiblePredicateSignature); + const auto matchingVisiblePredicateSignature = + std::find_if(visiblePredicateSignatures.cbegin(), visiblePredicateSignatures.cend(), matchesPredicateSignature); // If the predicate ought to be visible, don’t eliminate it - if (matchingPredicateSignature != visiblePredicateSignatures.cend()) + if (matchingVisiblePredicateSignature != visiblePredicateSignatures.cend()) 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 << "”"; const auto &completedPredicateDefinition = completedFormulas[i]; diff --git a/src/anthem/Translation.cpp b/src/anthem/Translation.cpp index f819e37..1b73d85 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);