Version bump for release 0.1.7 RC 3

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:

.ci/Dockerfile-arch-latest

@@ -0,0 +1,9 @@
+FROM archimg/base-devel:latest
+
+ARG toolchain
+
+RUN pacman -Sy
+RUN pacman -S --noconfirm cmake git ninja re2c
+RUN if [ "${toolchain}" = "clang" ]; then pacman -S --noconfirm clang; fi
+
+VOLUME /app

.ci/Dockerfile-ubuntu-18.04

@@ -0,0 +1,10 @@
+FROM ubuntu:18.04
+
+ARG toolchain
+
+RUN apt-get update
+RUN apt-get install -y cmake git ninja-build re2c
+RUN if [ "${toolchain}" = "gcc" ]; then apt-get install -y g++; fi
+RUN if [ "${toolchain}" = "clang" ]; then apt-get install -y clang; fi
+
+VOLUME /app

.ci/ci.sh

@@ -0,0 +1,17 @@
+#!/bin/bash
+
+if [ "$1" = "gcc" ]
+then
+	cxx=g++
+	cc=gcc
+elif [ "$1" = "clang" ]
+then
+	cxx=clang++
+	cc=clang
+fi
+
+git submodule update --init --recursive
+mkdir -p build/debug
+cd build/debug
+cmake ../.. -GNinja -DANTHEM_BUILD_TESTS=ON -DCMAKE_CXX_COMPILER=${cxx} -DCMAKE_C_COMPILER=${cc}
+ninja anthem-app && ninja run-tests

.gitmodules

@@ -3,4 +3,7 @@
 	url = https://github.com/potassco/clingo
 [submodule "lib/catch"]
 	path = lib/catch
-	url = https://github.com/philsquared/Catch
+	url = https://github.com/catchorg/Catch2
+[submodule "lib/cxxopts"]
+	path = lib/cxxopts
+	url = https://github.com/jarro2783/cxxopts

.travis.yml

@@ -1,47 +1,25 @@
-# Use container-based distribution
+sudo: required
-sudo: false
+
-language: c++
+services:
-addons:
+  - docker
-  apt:
+
-    sources: &default_sources
-      - ubuntu-toolchain-r-test
-      - boost-latest
-    packages: &default_packages
-      - libboost-program-options1.55-dev
-      - libboost-iostreams1.55-dev
-      - libboost-system1.55-dev
-      - libboost-filesystem1.55-dev
-      - re2c
 matrix:
   include:
-    - env: COMPILER_NAME=g++ _CXX=g++-5 _CC=gcc-5
+    - env: distribution=arch-latest toolchain=gcc
       os: linux
       language: cpp
-      addons:
+    - env: distribution=arch-latest toolchain=clang
-        apt:
-          sources:
-            - *default_sources
-          packages:
-            - *default_packages
-            - g++-5
-    - env: COMPILER_NAME=g++ _CXX=g++-6 _CC=gcc-6
       os: linux
       language: cpp
-      addons:
+    - env: distribution=ubuntu-18.04 toolchain=gcc
-        apt:
+      os: linux
-          sources:
+      language: cpp
-            - *default_sources
+    - env: distribution=ubuntu-18.04 toolchain=clang
-          packages:
+      os: linux
-            - *default_packages
+      language: cpp
-            - g++-6
+
+before_install:
+  - docker build --build-arg toolchain=${toolchain} -t ${distribution} - < .ci/Dockerfile-${distribution}
+
 script:
-  - if [[ "${TRAVIS_OS_NAME}" == "linux" ]]; then
+  - docker run --mount source=$(pwd),target=/app,type=bind -w /app ${distribution} /bin/bash -c ".ci/ci.sh ${toolchain}"
-      CMAKE_URL="http://www.cmake.org/files/v3.7/cmake-3.7.0-Linux-x86_64.tar.gz";
-      mkdir cmake-bin && wget --quiet --no-check-certificate -O - ${CMAKE_URL} | tar --strip-components=1 -xz -C cmake-bin;
-      export PATH=${PWD}/cmake-bin/bin:${PATH};
-    fi
-  - git submodule update --init --recursive
-  - mkdir -p build/debug
-  - cd build/debug
-  - cmake ../.. -DCMAKE_BUILD_TYPE=Debug -DCMAKE_CXX_COMPILER=$_CXX -DCMAKE_C_COMPILER=$_CC -DANTHEM_BUILD_TESTS=ON
-  - make -j3 anthem-app && make -j3 run-tests

CHANGELOG.md

@@ -1,10 +1,18 @@
 # Change Log
 
-## (unreleased)
+## 0.1.7 RC 3 (2018-04-07)
+
+### 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)
 
 ## 0.1.6 (2017-06-12)
 
-Features:
+### Features
 
 * unique IDs for all variables (user-defined variables are renamed)
 * support for hiding predicates from completed output by using `#show` statements
@@ -12,7 +20,7 @@ Features:
 * command-line option `--parentheses` to fully parenthesize the output
 * adds multiple example instances for experimenting
 
-Bug Fixes:
+### Bug Fixes
 
 * adds missing error message when attempting to read inaccessible file
 * removes unnecessary parentheses after simplification
@@ -20,52 +28,52 @@ Bug Fixes:
 
 ## 0.1.5 (2017-05-04)
 
-Bug Fixes:
+### Bug Fixes
 
 * fixes lost signs with negated 0-ary predicates
 
 ## 0.1.4 (2017-04-12)
 
-Features:
+### Features
 
 * completion of input programs (optional)
 * command-line option `--complete` to turn on completion
 
 ## 0.1.3 (2017-03-30)
 
-Features:
+### Features
 
 * support for anonymous variables
 
-Bug Fixes:
+### Bug Fixes
 
 * fixes incorrectly simplified rules with comparisons
 * fixes misleading error message concerning negated, unsupported body literals
 
 ## 0.1.2 (2017-03-23)
 
-Features:
+### Features
 
 * simplification of output formulas (optional)
 * command-line option `--simplify` to turn on simplification
 
-Bug Fixes:
+### Bug Fixes
 
 * fixes incorrectly translated choice rules with multiple elements in the head aggregate
 
-Internal:
+### Internal
 
 * explicit syntax tree representation for first-order formulas
 
 ## 0.1.1 (2017-03-06)
 
-Features:
+### Features
 
 * support for choice rules (without guards)
 
 ## 0.1.0 (2016-11-24)
 
-Features:
+### Features
 
 * initial support for translating rules in *Essential Gringo* (excluding aggregates) to first-order logic formulas
 * command-line option `--color` to autodetect, enable, or disable color output

CMakeLists.txt

@@ -7,7 +7,7 @@ option(ANTHEM_BUILD_STATIC "Build static binaries" OFF)
 set(CMAKE_CXX_FLAGS "-Wall -Wextra -Wpedantic ${CMAKE_CXX_FLAGS}")
 set(CMAKE_CXX_FLAGS_DEBUG "-g ${CMAKE_CXX_FLAGS_DEBUG}")
 
-set(CMAKE_CXX_STANDARD 14)
+set(CMAKE_CXX_STANDARD 17)
 set(CMAKE_CXX_STANDARD_REQUIRED ON)
 set(CMAKE_CXX_EXTENSIONS OFF)
 

README.md

@@ -16,8 +16,8 @@ With the option `--simplify`, output formulas are simplified by applying several
 
 ## Building
 
-`anthem` requires [CMake](https://cmake.org/) and [Boost](http://www.boost.org/) for building.
+`anthem` requires [CMake](https://cmake.org/) for building.
-After installing the dependencies, `anthem` is built with a C++14 compiler (GCC ≥ 6.1 or clang ≥ 3.8).
+After installing the dependencies, `anthem` is built with a C++17 compiler (GCC ≥ 7.3 or clang ≥ 5.0).
 
 ```bash
 $ git clone https://github.com/potassco/anthem.git

app/CMakeLists.txt

@@ -1,7 +1,5 @@
 set(target anthem-app)
 
-find_package(Boost 1.55.0 COMPONENTS program_options system filesystem REQUIRED)
-
 file(GLOB core_sources "*.cpp")
 file(GLOB core_headers "*.h")
 
@@ -11,11 +9,10 @@ set(sources
 )
 
 set(includes
-	${Boost_INCLUDE_DIRS}
+	${PROJECT_SOURCE_DIR}/lib/cxxopts/include
 )
 
 set(libraries
-	${Boost_LIBRARIES}
 	anthem
 )
 

app/main.cpp

@@ -1,6 +1,6 @@
 #include <iostream>
 
-#include <boost/program_options.hpp>
+#include <cxxopts.hpp>
 
 #include <anthem/AST.h>
 #include <anthem/Context.h>
@@ -10,63 +10,70 @@ int main(int argc, char **argv)
 {
 	anthem::Context context;
 
-	namespace po = boost::program_options;
+	cxxopts::Options options("anthem", "Translate ASP programs to the language of first-order theorem provers.");
 
-	po::options_description description("Allowed options");
+	options.add_options()
-	description.add_options()
+		("h,help", "Display this help message")
-		("help,h", "Display this help message")
+		("v,version", "Display version information")
-		("version,v", "Display version information")
+		("i,input", "Input files", cxxopts::value<std::vector<std::string>>())
-		("input,i", po::value<std::vector<std::string>>(), "Input files")
+		("s,simplify", "Simplify the output")
-		("simplify,s", po::bool_switch(&context.performSimplification), "Simplify the output")
+		("c,complete", "Perform completion")
-		("complete,c", po::bool_switch(&context.performCompletion), "Perform completion")
+		("color", "Colorize output (always, never, auto)", cxxopts::value<std::string>()->default_value("auto"))
-		("color", po::value<std::string>()->default_value("auto"), "Colorize output (always, never, auto)")
+		("parentheses", "Parenthesis style (normal, full)", cxxopts::value<std::string>()->default_value("normal"))
-		("parentheses", po::value<std::string>()->default_value("normal"), "Parenthesis style (normal, full)")
+		("p,log-priority", "Log messages starting from this priority (debug, info, warning, error)", cxxopts::value<std::string>()->default_value("info"));
-		("log-priority,p", po::value<std::string>()->default_value("warning"), "Log messages starting from this priority (debug, info, warning, error)");
 
-	po::positional_options_description positionalOptionsDescription;
+	options.parse_positional("input");
-	positionalOptionsDescription.add("input", -1);
+	options.positional_help("[<input file...>]");
-
-	po::variables_map variablesMap;
 
 	const auto printHelp =
 		[&]()
 		{
-			std::cout
+			std::cout << options.help();
-				<< "Usage: anthem [options] file..." << std::endl
-				<< "Translate ASP programs to the language of first-order theorem provers." << std::endl << std::endl
-				<< description;
 		};
 
+	bool help;
+	bool version;
+	std::vector<std::string> inputFiles;
+	std::string colorPolicyString;
+	std::string parenthesisStyleString;
+	std::string logPriorityString;
+
 	try
 	{
-		po::store(po::command_line_parser(argc, argv)
+		const auto parseResult = options.parse(argc, argv);
-			.options(description)
+
-			.positional(positionalOptionsDescription)
+		help = (parseResult.count("help") > 0);
-			.run(),
+		version = (parseResult.count("version") > 0);
-			variablesMap);
+
-		po::notify(variablesMap);
+		if (parseResult.count("input") > 0)
+			inputFiles = parseResult["input"].as<std::vector<std::string>>();
+
+		context.performSimplification = (parseResult.count("simplify") > 0);
+		context.performCompletion = (parseResult.count("complete") > 0);
+		colorPolicyString = parseResult["color"].as<std::string>();
+		parenthesisStyleString = parseResult["parentheses"].as<std::string>();
+		logPriorityString = parseResult["log-priority"].as<std::string>();
 	}
-	catch (const po::error &e)
+	catch (const std::exception &exception)
 	{
-		context.logger.log(anthem::output::Priority::Error) << e.what();
+		context.logger.log(anthem::output::Priority::Error) << exception.what();
+		context.logger.errorStream() << std::endl;
 		printHelp();
 		return EXIT_FAILURE;
 	}
 
-	if (variablesMap.count("help"))
+	if (help)
 	{
 		printHelp();
 		return EXIT_SUCCESS;
 	}
 
-	if (variablesMap.count("version"))
+	if (version)
 	{
-		std::cout << "anthem version 0.1.7-git" << std::endl;
+		std::cout << "anthem version 0.1.7-rc.3" << std::endl;
 		return EXIT_SUCCESS;
 	}
 
-	const auto colorPolicyString = variablesMap["color"].as<std::string>();
-
 	if (colorPolicyString == "auto")
 		context.logger.setColorPolicy(anthem::output::ColorStream::ColorPolicy::Auto);
 	else if (colorPolicyString == "never")
@@ -81,22 +88,18 @@ int main(int argc, char **argv)
 		return EXIT_FAILURE;
 	}
 
-	const auto parenthesisStyle = variablesMap["parentheses"].as<std::string>();
+	if (parenthesisStyleString == "normal")
-
-	if (parenthesisStyle == "normal")
 		context.parenthesisStyle = anthem::ast::ParenthesisStyle::Normal;
-	else if (parenthesisStyle == "full")
+	else if (parenthesisStyleString == "full")
 		context.parenthesisStyle = anthem::ast::ParenthesisStyle::Full;
 	else
 	{
-		context.logger.log(anthem::output::Priority::Error) << "unknown parenthesis style “" << parenthesisStyle << "”";
+		context.logger.log(anthem::output::Priority::Error) << "unknown parenthesis style “" << parenthesisStyleString << "”";
 		context.logger.errorStream() << std::endl;
 		printHelp();
 		return EXIT_FAILURE;
 	}
 
-	const auto logPriorityString = variablesMap["log-priority"].as<std::string>();
-
 	try
 	{
 		const auto logPriority = anthem::output::priorityFromName(logPriorityString.c_str());
@@ -112,11 +115,8 @@ int main(int argc, char **argv)
 
 	try
 	{
-		if (variablesMap.count("input"))
+		if (!inputFiles.empty())
-		{
-			const auto &inputFiles = variablesMap["input"].as<std::vector<std::string>>();
 			anthem::translate(inputFiles, context);
-		}
 		else
 			anthem::translate("std::cin", std::cin, context);
 	}

include/anthem/ASTUtils.h

@@ -1,10 +1,11 @@
 #ifndef __ANTHEM__AST_UTILS_H
 #define __ANTHEM__AST_UTILS_H
 
-#include <experimental/optional>
+#include <optional>
 
 #include <anthem/AST.h>
 #include <anthem/ASTVisitors.h>
+#include <anthem/Context.h>
 
 namespace anthem
 {
@@ -28,7 +29,7 @@ class VariableStack
 		void push(Layer layer);
 		void pop();
 
-		std::experimental::optional<VariableDeclaration *> findUserVariableDeclaration(const char *variableName) const;
+		std::optional<VariableDeclaration *> findUserVariableDeclaration(const char *variableName) const;
 		bool contains(const VariableDeclaration &variableDeclaration) const;
 
 	private:
@@ -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<PredicateSignature> &predicateSignatures);
+void collectPredicateSignatures(const Formula &formula, std::vector<PredicateSignature> &predicateSignatures, Context &context);
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 // Replacing Variables

include/anthem/Body.h

@@ -43,7 +43,7 @@ ast::Comparison::Operator translate(Clingo::AST::ComparisonOperator comparisonOp
 struct BodyTermTranslateVisitor
 {
 	// TODO: refactor
-	std::experimental::optional<ast::Formula> visit(const Clingo::AST::Function &function, const Clingo::AST::Literal &literal, const Clingo::AST::Term &, RuleContext &ruleContext, ast::VariableStack &variableStack)
+	std::optional<ast::Formula> visit(const Clingo::AST::Function &function, const Clingo::AST::Literal &literal, const Clingo::AST::Term &, RuleContext &ruleContext, ast::VariableStack &variableStack)
 	{
 		if (literal.sign == Clingo::AST::Sign::DoubleNegation)
 			throw TranslationException(literal.location, "double-negated literals currently unsupported");
@@ -93,12 +93,12 @@ struct BodyTermTranslateVisitor
 	}
 
 	template<class T>
-	std::experimental::optional<ast::Formula> visit(const T &, const Clingo::AST::Literal &, const Clingo::AST::Term &term, RuleContext &, ast::VariableStack &)
+	std::optional<ast::Formula> visit(const T &, const Clingo::AST::Literal &, const Clingo::AST::Term &term, RuleContext &, ast::VariableStack &)
 	{
 		assert(!term.data.is<Clingo::AST::Function>());
 
 		throw TranslationException(term.location, "term currently unsupported in this context, expected function");
-		return std::experimental::nullopt;
+		return std::nullopt;
 	}
 };
 
@@ -106,18 +106,18 @@ struct BodyTermTranslateVisitor
 
 struct BodyLiteralTranslateVisitor
 {
-	std::experimental::optional<ast::Formula> visit(const Clingo::AST::Boolean &boolean, const Clingo::AST::Literal &, RuleContext &, ast::VariableStack &)
+	std::optional<ast::Formula> visit(const Clingo::AST::Boolean &boolean, const Clingo::AST::Literal &, RuleContext &, ast::VariableStack &)
 	{
 		return ast::Formula::make<ast::Boolean>(boolean.value);
 	}
 
-	std::experimental::optional<ast::Formula> visit(const Clingo::AST::Term &term, const Clingo::AST::Literal &literal, RuleContext &ruleContext, ast::VariableStack &variableStack)
+	std::optional<ast::Formula> visit(const Clingo::AST::Term &term, const Clingo::AST::Literal &literal, RuleContext &ruleContext, ast::VariableStack &variableStack)
 	{
 		return term.data.accept(BodyTermTranslateVisitor(), literal, term, ruleContext, variableStack);
 	}
 
 	// TODO: refactor
-	std::experimental::optional<ast::Formula> visit(const Clingo::AST::Comparison &comparison, const Clingo::AST::Literal &literal, RuleContext &ruleContext, ast::VariableStack &variableStack)
+	std::optional<ast::Formula> visit(const Clingo::AST::Comparison &comparison, const Clingo::AST::Literal &literal, RuleContext &ruleContext, ast::VariableStack &variableStack)
 	{
 		// Comparisons should never have a sign, because these are converted to positive comparisons by clingo
 		if (literal.sign != Clingo::AST::Sign::None)
@@ -140,10 +140,10 @@ struct BodyLiteralTranslateVisitor
 	}
 
 	template<class T>
-	std::experimental::optional<ast::Formula> visit(const T &, const Clingo::AST::Literal &literal, RuleContext &, ast::VariableStack &)
+	std::optional<ast::Formula> visit(const T &, const Clingo::AST::Literal &literal, RuleContext &, ast::VariableStack &)
 	{
 		throw TranslationException(literal.location, "literal currently unsupported in this context, expected function or term");
-		return std::experimental::nullopt;
+		return std::nullopt;
 	}
 };
 
@@ -151,7 +151,7 @@ struct BodyLiteralTranslateVisitor
 
 struct BodyBodyLiteralTranslateVisitor
 {
-	std::experimental::optional<ast::Formula> visit(const Clingo::AST::Literal &literal, const Clingo::AST::BodyLiteral &bodyLiteral, RuleContext &ruleContext, ast::VariableStack &variableStack)
+	std::optional<ast::Formula> visit(const Clingo::AST::Literal &literal, const Clingo::AST::BodyLiteral &bodyLiteral, RuleContext &ruleContext, ast::VariableStack &variableStack)
 	{
 		if (bodyLiteral.sign != Clingo::AST::Sign::None)
 			throw TranslationException(bodyLiteral.location, "only positive body literals supported currently");
@@ -160,10 +160,10 @@ struct BodyBodyLiteralTranslateVisitor
 	}
 
 	template<class T>
-	std::experimental::optional<ast::Formula> visit(const T &, const Clingo::AST::BodyLiteral &bodyLiteral, RuleContext &, ast::VariableStack &)
+	std::optional<ast::Formula> visit(const T &, const Clingo::AST::BodyLiteral &bodyLiteral, RuleContext &, ast::VariableStack &)
 	{
 		throw TranslationException(bodyLiteral.location, "body literal currently unsupported in this context, expected literal");
-		return std::experimental::nullopt;
+		return std::nullopt;
 	}
 };
 

include/anthem/Context.h

@@ -1,7 +1,7 @@
 #ifndef __ANTHEM__CONTEXT_H
 #define __ANTHEM__CONTEXT_H
 
-#include <experimental/optional>
+#include <optional>
 
 #include <anthem/AST.h>
 #include <anthem/output/Logger.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::experimental::optional<std::vector<ast::PredicateSignature>> visiblePredicateSignatures;
+	std::optional<std::vector<PredicateSignatureMeta>> visiblePredicateSignatures;
+	std::optional<std::vector<PredicateSignatureMeta>> externalPredicateSignatures;
 
 	ast::ParenthesisStyle parenthesisStyle = ast::ParenthesisStyle::Normal;
 };

include/anthem/Head.h

@@ -2,7 +2,7 @@
 #define __ANTHEM__HEAD_H
 
 #include <algorithm>
-#include <experimental/optional>
+#include <optional>
 
 #include <anthem/AST.h>
 #include <anthem/Exception.h>
@@ -119,7 +119,7 @@ struct HeadLiteralCollectFunctionTermsVisitor
 struct FunctionTermTranslateVisitor
 {
 	// TODO: check correctness
-	std::experimental::optional<ast::Formula> visit(const Clingo::AST::Function &function, const Clingo::AST::Term &term, RuleContext &ruleContext, size_t &headVariableIndex)
+	std::optional<ast::Formula> visit(const Clingo::AST::Function &function, const Clingo::AST::Term &term, RuleContext &ruleContext, size_t &headVariableIndex)
 	{
 		if (function.external)
 			throw TranslationException(term.location, "external functions currently unsupported");
@@ -134,10 +134,10 @@ struct FunctionTermTranslateVisitor
 	}
 
 	template<class T>
-	std::experimental::optional<ast::Formula> visit(const T &, const Clingo::AST::Term &term, RuleContext &, size_t &)
+	std::optional<ast::Formula> visit(const T &, const Clingo::AST::Term &term, RuleContext &, size_t &)
 	{
 		throw TranslationException(term.location, "term currently unsupported in this context, function expected");
-		return std::experimental::nullopt;
+		return std::nullopt;
 	}
 };
 
@@ -145,21 +145,21 @@ struct FunctionTermTranslateVisitor
 
 struct LiteralTranslateVisitor
 {
-	std::experimental::optional<ast::Formula> visit(const Clingo::AST::Boolean &boolean, const Clingo::AST::Literal &, RuleContext &, size_t &)
+	std::optional<ast::Formula> visit(const Clingo::AST::Boolean &boolean, const Clingo::AST::Literal &, RuleContext &, size_t &)
 	{
 		return ast::Formula::make<ast::Boolean>(boolean.value);
 	}
 
-	std::experimental::optional<ast::Formula> visit(const Clingo::AST::Term &term, const Clingo::AST::Literal &, RuleContext &ruleContext, size_t &headVariableIndex)
+	std::optional<ast::Formula> visit(const Clingo::AST::Term &term, const Clingo::AST::Literal &, RuleContext &ruleContext, size_t &headVariableIndex)
 	{
 		return term.data.accept(FunctionTermTranslateVisitor(), term, ruleContext, headVariableIndex);
 	}
 
 	template<class T>
-	std::experimental::optional<ast::Formula> visit(const T &, const Clingo::AST::Literal &literal, RuleContext &, size_t &)
+	std::optional<ast::Formula> visit(const T &, const Clingo::AST::Literal &literal, RuleContext &, size_t &)
 	{
 		throw TranslationException(literal.location, "only disjunctions of literals allowed as head literals");
-		return std::experimental::nullopt;
+		return std::nullopt;
 	}
 };
 
@@ -167,7 +167,7 @@ struct LiteralTranslateVisitor
 
 struct HeadLiteralTranslateToConsequentVisitor
 {
-	std::experimental::optional<ast::Formula> visit(const Clingo::AST::Literal &literal, const Clingo::AST::HeadLiteral &, RuleContext &ruleContext, size_t &headVariableIndex)
+	std::optional<ast::Formula> visit(const Clingo::AST::Literal &literal, const Clingo::AST::HeadLiteral &, RuleContext &ruleContext, size_t &headVariableIndex)
 	{
 		if (literal.sign == Clingo::AST::Sign::DoubleNegation)
 			throw TranslationException(literal.location, "double-negated head literals currently unsupported");
@@ -178,12 +178,12 @@ struct HeadLiteralTranslateToConsequentVisitor
 			return translatedLiteral;
 
 		if (!translatedLiteral)
-			return std::experimental::nullopt;
+			return std::nullopt;
 
 		return ast::Formula::make<ast::Not>(std::move(translatedLiteral.value()));
 	}
 
-	std::experimental::optional<ast::Formula> visit(const Clingo::AST::Disjunction &disjunction, const Clingo::AST::HeadLiteral &headLiteral, RuleContext &ruleContext, size_t &headVariableIndex)
+	std::optional<ast::Formula> visit(const Clingo::AST::Disjunction &disjunction, const Clingo::AST::HeadLiteral &headLiteral, RuleContext &ruleContext, size_t &headVariableIndex)
 	{
 		std::vector<ast::Formula> arguments;
 		arguments.reserve(disjunction.elements.size());
@@ -204,7 +204,7 @@ struct HeadLiteralTranslateToConsequentVisitor
 		return ast::Formula::make<ast::Or>(std::move(arguments));
 	}
 
-	std::experimental::optional<ast::Formula> visit(const Clingo::AST::Aggregate &aggregate, const Clingo::AST::HeadLiteral &headLiteral, RuleContext &ruleContext, size_t &headVariableIndex)
+	std::optional<ast::Formula> visit(const Clingo::AST::Aggregate &aggregate, const Clingo::AST::HeadLiteral &headLiteral, RuleContext &ruleContext, size_t &headVariableIndex)
 	{
 		if (aggregate.left_guard || aggregate.right_guard)
 			throw TranslationException(headLiteral.location, "aggregates with left or right guards currently unsupported");
@@ -238,10 +238,10 @@ struct HeadLiteralTranslateToConsequentVisitor
 	}
 
 	template<class T>
-	std::experimental::optional<ast::Formula> visit(const T &, const Clingo::AST::HeadLiteral &headLiteral, RuleContext &, size_t &)
+	std::optional<ast::Formula> visit(const T &, const Clingo::AST::HeadLiteral &headLiteral, RuleContext &, size_t &)
 	{
 		throw TranslationException(headLiteral.location, "head literal currently unsupported in this context, expected literal, disjunction, or aggregate");
-		return std::experimental::nullopt;
+		return std::nullopt;
 	}
 };
 

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<ast::ScopedFormula> &, 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<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 size_t arity = arityArgument.data.get<Clingo::Symbol>().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<class T>
 	void visit(const T &, const Clingo::AST::Statement &statement, std::vector<ast::ScopedFormula> &, Context &)
 	{

include/anthem/Term.h

@@ -48,7 +48,7 @@ ast::Term translate(const Clingo::AST::Term &term, RuleContext &ruleContext, con
 
 struct TermTranslateVisitor
 {
-	std::experimental::optional<ast::Term> visit(const Clingo::Symbol &symbol, const Clingo::AST::Term &term, RuleContext &ruleContext, const ast::VariableStack &variableStack)
+	std::optional<ast::Term> visit(const Clingo::Symbol &symbol, const Clingo::AST::Term &term, RuleContext &ruleContext, const ast::VariableStack &variableStack)
 	{
 		switch (symbol.type())
 		{
@@ -81,10 +81,10 @@ struct TermTranslateVisitor
 			}
 		}
 
-		return std::experimental::nullopt;
+		return std::nullopt;
 	}
 
-	std::experimental::optional<ast::Term> visit(const Clingo::AST::Variable &variable, const Clingo::AST::Term &, RuleContext &ruleContext, const ast::VariableStack &variableStack)
+	std::optional<ast::Term> visit(const Clingo::AST::Variable &variable, const Clingo::AST::Term &, RuleContext &ruleContext, const ast::VariableStack &variableStack)
 	{
 		const auto matchingVariableDeclaration = variableStack.findUserVariableDeclaration(variable.name);
 		const auto isAnonymousVariable = (strcmp(variable.name, "_") == 0);
@@ -100,13 +100,13 @@ struct TermTranslateVisitor
 		return ast::Term::make<ast::Variable>(ruleContext.freeVariables.back().get());
 	}
 
-	std::experimental::optional<ast::Term> visit(const Clingo::AST::UnaryOperation &, const Clingo::AST::Term &term, RuleContext &, const ast::VariableStack &)
+	std::optional<ast::Term> visit(const Clingo::AST::UnaryOperation &, const Clingo::AST::Term &term, RuleContext &, const ast::VariableStack &)
 	{
 		throw TranslationException(term.location, "“unary operation” terms currently unsupported");
-		return std::experimental::nullopt;
+		return std::nullopt;
 	}
 
-	std::experimental::optional<ast::Term> visit(const Clingo::AST::BinaryOperation &binaryOperation, const Clingo::AST::Term &term, RuleContext &ruleContext, const ast::VariableStack &variableStack)
+	std::optional<ast::Term> visit(const Clingo::AST::BinaryOperation &binaryOperation, const Clingo::AST::Term &term, RuleContext &ruleContext, const ast::VariableStack &variableStack)
 	{
 		const auto operator_ = translate(binaryOperation.binary_operator, term);
 		auto left = translate(binaryOperation.left, ruleContext, variableStack);
@@ -115,7 +115,7 @@ struct TermTranslateVisitor
 		return ast::Term::make<ast::BinaryOperation>(operator_, std::move(left), std::move(right));
 	}
 
-	std::experimental::optional<ast::Term> visit(const Clingo::AST::Interval &interval, const Clingo::AST::Term &, RuleContext &ruleContext, const ast::VariableStack &variableStack)
+	std::optional<ast::Term> visit(const Clingo::AST::Interval &interval, const Clingo::AST::Term &, RuleContext &ruleContext, const ast::VariableStack &variableStack)
 	{
 		auto left = translate(interval.left, ruleContext, variableStack);
 		auto right = translate(interval.right, ruleContext, variableStack);
@@ -123,7 +123,7 @@ struct TermTranslateVisitor
 		return ast::Term::make<ast::Interval>(std::move(left), std::move(right));
 	}
 
-	std::experimental::optional<ast::Term> visit(const Clingo::AST::Function &function, const Clingo::AST::Term &term, RuleContext &ruleContext, const ast::VariableStack &variableStack)
+	std::optional<ast::Term> visit(const Clingo::AST::Function &function, const Clingo::AST::Term &term, RuleContext &ruleContext, const ast::VariableStack &variableStack)
 	{
 		if (function.external)
 			throw TranslationException(term.location, "external functions currently unsupported");
@@ -137,10 +137,10 @@ struct TermTranslateVisitor
 		return ast::Term::make<ast::Function>(function.name, std::move(arguments));
 	}
 
-	std::experimental::optional<ast::Term> visit(const Clingo::AST::Pool &, const Clingo::AST::Term &term, RuleContext &, const ast::VariableStack &)
+	std::optional<ast::Term> visit(const Clingo::AST::Pool &, const Clingo::AST::Term &term, RuleContext &, const ast::VariableStack &)
 	{
 		throw TranslationException(term.location, "“pool” terms currently unsupported");
-		return std::experimental::nullopt;
+		return std::nullopt;
 	}
 };
 

src/anthem/ASTUtils.cpp

@@ -27,7 +27,7 @@ void VariableStack::pop()
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-std::experimental::optional<VariableDeclaration *> VariableStack::findUserVariableDeclaration(const char *variableName) const
+std::optional<VariableDeclaration *> VariableStack::findUserVariableDeclaration(const char *variableName) const
 {
 	const auto variableDeclarationMatches =
 		[&variableName](const auto &variableDeclaration)
@@ -45,7 +45,7 @@ std::experimental::optional<VariableDeclaration *> VariableStack::findUserVariab
 			return matchingVariableDeclaration->get();
 	}
 
-	return std::experimental::nullopt;
+	return std::nullopt;
 }
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
@@ -194,7 +194,7 @@ struct CollectFreeVariablesVisitor
 
 struct CollectPredicateSignaturesVisitor : public RecursiveFormulaVisitor<CollectPredicateSignaturesVisitor>
 {
-	static void accept(const Predicate &predicate, const Formula &, std::vector<PredicateSignature> &predicateSignatures)
+	static void accept(const Predicate &predicate, const Formula &, std::vector<PredicateSignature> &predicateSignatures, Context &context)
 	{
 		const auto predicateSignatureMatches =
 			[&predicate](const auto &predicateSignature)
@@ -206,12 +206,35 @@ struct CollectPredicateSignaturesVisitor : public RecursiveFormulaVisitor<Collec
 			return;
 
 		// TODO: avoid copies
-		predicateSignatures.emplace_back(std::string(predicate.name), predicate.arity());
+		auto predicateSignature = PredicateSignature(std::string(predicate.name), predicate.arity());
+
+		// Ignore predicates that are declared #external
+		if (context.externalPredicateSignatures)
+		{
+			const auto matchesPredicateSignature =
+				[&](const auto &otherPredicateSignature)
+				{
+					return ast::matches(predicateSignature, otherPredicateSignature.predicateSignature);
+				};
+
+			auto &externalPredicateSignatures = context.externalPredicateSignatures.value();
+
+			const auto matchingExternalPredicateSignature =
+				std::find_if(externalPredicateSignatures.begin(), externalPredicateSignatures.end(), matchesPredicateSignature);
+
+			if (matchingExternalPredicateSignature != externalPredicateSignatures.end())
+			{
+				matchingExternalPredicateSignature->used = true;
+				return;
+			}
+		}
+
+		predicateSignatures.emplace_back(std::move(predicateSignature));
 	}
 
 	// Ignore all other types of expressions
 	template<class T>
-	static void accept(const T &, const Formula &, std::vector<PredicateSignature> &)
+	static void accept(const T &, const Formula &, std::vector<PredicateSignature> &, 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<PredicateSignature> &predicateSignatures)
+void collectPredicateSignatures(const Formula &formula, std::vector<PredicateSignature> &predicateSignatures, Context &context)
 {
 	auto &formulaMutable = const_cast<Formula &>(formula);
-	formulaMutable.accept(CollectPredicateSignaturesVisitor(), formulaMutable, predicateSignatures);
+	formulaMutable.accept(CollectPredicateSignaturesVisitor(), formulaMutable, predicateSignatures, context);
 }
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////

src/anthem/Completion.cpp

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

src/anthem/HiddenPredicateElimination.cpp

@@ -194,41 +194,40 @@ void eliminateHiddenPredicates(const std::vector<ast::PredicateSignature> &predi
 		return;
 	}
 
-	const auto &visiblePredicateSignatures = context.visiblePredicateSignatures.value();
+	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 <<"”";
-	}
 
 	// Replace all occurrences of hidden predicates
 	for (size_t i = 0; i < predicateSignatures.size(); i++)
 	{
 		auto &predicateSignature = predicateSignatures[i];
 
-		const auto matchesVisiblePredicateSignature =
+		const auto matchesPredicateSignature =
-			[&](const auto &visiblePredicateSignature)
+			[&](const auto &otherPredicateSignature)
 			{
-				return ast::matches(predicateSignature, visiblePredicateSignature);
+				return ast::matches(predicateSignature, otherPredicateSignature.predicateSignature);
 			};
 
-		const auto matchingPredicateSignature =
+		const auto matchingVisiblePredicateSignature =
-			std::find_if(visiblePredicateSignatures.cbegin(), visiblePredicateSignatures.cend(), matchesVisiblePredicateSignature);
+			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 << "”";
 

src/anthem/Simplification.cpp

@@ -1,6 +1,6 @@
 #include <anthem/Simplification.h>
 
-#include <experimental/optional>
+#include <optional>
 
 #include <anthem/ASTCopy.h>
 #include <anthem/ASTVisitors.h>
@@ -27,15 +27,15 @@ bool matchesVariableDeclaration(const ast::Term &term, const ast::VariableDeclar
 
 // Extracts the term t if the given formula is of the form “X = t” and X matches the given variable
 // The input formula is no longer usable after this call if a term is returned
-std::experimental::optional<ast::Term> extractAssignedTerm(ast::Formula &formula, const ast::VariableDeclaration &variableDeclaration)
+std::optional<ast::Term> extractAssignedTerm(ast::Formula &formula, const ast::VariableDeclaration &variableDeclaration)
 {
 	if (!formula.is<ast::Comparison>())
-		return std::experimental::nullopt;
+		return std::nullopt;
 
 	auto &comparison = formula.get<ast::Comparison>();
 
 	if (comparison.operator_ != ast::Comparison::Operator::Equal)
-		return std::experimental::nullopt;
+		return std::nullopt;
 
 	if (matchesVariableDeclaration(comparison.left, variableDeclaration))
 		return std::move(comparison.right);
@@ -43,7 +43,7 @@ std::experimental::optional<ast::Term> extractAssignedTerm(ast::Formula &formula
 	if (matchesVariableDeclaration(comparison.right, variableDeclaration))
 		return std::move(comparison.left);
 
-	return std::experimental::nullopt;
+	return std::nullopt;
 }
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////

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)