Support placeholders with #external declarations

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

@@ -31,6 +31,7 @@ struct Context
 	bool performCompletion = false;
 
 	std::optional<std::vector<ast::PredicateSignature>> visiblePredicateSignatures;
+	std::optional<std::vector<ast::PredicateSignature>> externalPredicateSignatures;
 
 	ast::ParenthesisStyle parenthesisStyle = ast::ParenthesisStyle::Normal;
 };

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<ast::ScopedFormula> &, Context &context)
+	{
+		const auto fail =
+			[&]()
+			{
+				throw LogicException(statement.location, "only #external declarations of the form “#external <predicate name>(<arity>).” supported");
+			};
+
+		if (!external.body.empty())
+			fail();
+
+		if (!external.atom.data.is<Clingo::AST::Function>())
+			fail();
+
+		const auto &predicate = external.atom.data.get<Clingo::AST::Function>();
+
+		if (predicate.arguments.size() != 1)
+			fail();
+
+		const auto &arityArgument = predicate.arguments.front();
+
+		if (!arityArgument.data.is<Clingo::Symbol>())
+			fail();
+
+		const auto &aritySymbol = arityArgument.data.get<Clingo::Symbol>();
+
+		if (aritySymbol.type() != Clingo::SymbolType::Number)
+			fail();
+
+		const auto &arity = arityArgument.data.get<Clingo::Symbol>().number();
+
+		if (!context.externalPredicateSignatures)
+			context.externalPredicateSignatures.emplace();
+
+		context.externalPredicateSignatures->emplace_back(std::string(predicate.name), arity);
+	}
+
 	template<class T>
 	void visit(const T &, const Clingo::AST::Statement &statement, std::vector<ast::ScopedFormula> &, Context &)
 	{

src/anthem/Completion.cpp

@@ -180,9 +180,47 @@ std::vector<ast::Formula> complete(std::vector<ast::ScopedFormula> &&scopedFormu
 
 	std::vector<ast::Formula> 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)

src/anthem/HiddenPredicateElimination.cpp

@@ -217,19 +217,31 @@ void eliminateHiddenPredicates(const std::vector<ast::PredicateSignature> &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];

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);