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)