Version bump for release 0.1.7 RC 2

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: false
-language: c++
-addons:
-  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
+sudo: required
+
+services:
+  - docker
+
 matrix:
   include:
-    - env: COMPILER_NAME=g++ _CXX=g++-5 _CC=gcc-5
+    - env: distribution=arch-latest toolchain=gcc
       os: linux
       language: cpp
-      addons:
-        apt:
-          sources:
-            - *default_sources
-          packages:
-            - *default_packages
-            - g++-5
-    - env: COMPILER_NAME=g++ _CXX=g++-6 _CC=gcc-6
+    - env: distribution=arch-latest toolchain=clang
       os: linux
       language: cpp
-      addons:
-        apt:
-          sources:
-            - *default_sources
-          packages:
-            - *default_packages
-            - g++-6
+    - env: distribution=ubuntu-18.04 toolchain=gcc
+      os: linux
+      language: cpp
+    - env: distribution=ubuntu-18.04 toolchain=clang
+      os: linux
+      language: cpp
+
+before_install:
+  - docker build --build-arg toolchain=${toolchain} -t ${distribution} - < .ci/Dockerfile-${distribution}
+
 script:
-  - if [[ "${TRAVIS_OS_NAME}" == "linux" ]]; then
-      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
+  - docker run --mount source=$(pwd),target=/app,type=bind -w /app ${distribution} /bin/bash -c ".ci/ci.sh ${toolchain}"

CHANGELOG.md

@@ -1,10 +1,18 @@
 # Change Log
 
-## (unreleased)
+## 0.1.7 RC 2 (2018-04-06)
+
+### 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.
-After installing the dependencies, `anthem` is built with a C++14 compiler (GCC ≥ 6.1 or clang ≥ 3.8).
+`anthem` requires [CMake](https://cmake.org/) for building.
+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");
-	description.add_options()
-		("help,h", "Display this help message")
-		("version,v", "Display version information")
-		("input,i", po::value<std::vector<std::string>>(), "Input files")
-		("simplify,s", po::bool_switch(&context.performSimplification), "Simplify the output")
-		("complete,c", po::bool_switch(&context.performCompletion), "Perform completion")
-		("color", po::value<std::string>()->default_value("auto"), "Colorize output (always, never, auto)")
-		("parentheses", po::value<std::string>()->default_value("normal"), "Parenthesis style (normal, full)")
-		("log-priority,p", po::value<std::string>()->default_value("warning"), "Log messages starting from this priority (debug, info, warning, error)");
+	options.add_options()
+		("h,help", "Display this help message")
+		("v,version", "Display version information")
+		("i,input", "Input files", cxxopts::value<std::vector<std::string>>())
+		("s,simplify", "Simplify the output")
+		("c,complete", "Perform completion")
+		("color", "Colorize output (always, never, auto)", cxxopts::value<std::string>()->default_value("auto"))
+		("parentheses", "Parenthesis style (normal, full)", cxxopts::value<std::string>()->default_value("normal"))
+		("p,log-priority", "Log messages starting from this priority (debug, info, warning, error)", cxxopts::value<std::string>()->default_value("info"));
 
-	po::positional_options_description positionalOptionsDescription;
-	positionalOptionsDescription.add("input", -1);
-
-	po::variables_map variablesMap;
+	options.parse_positional("input");
+	options.positional_help("[<input file...>]");
 
 	const auto printHelp =
 		[&]()
 		{
-			std::cout
-				<< "Usage: anthem [options] file..." << std::endl
-				<< "Translate ASP programs to the language of first-order theorem provers." << std::endl << std::endl
-				<< description;
+			std::cout << options.help();
 		};
 
+	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)
-			.options(description)
-			.positional(positionalOptionsDescription)
-			.run(),
-			variablesMap);
-		po::notify(variablesMap);
+		const auto parseResult = options.parse(argc, argv);
+
+		help = (parseResult.count("help") > 0);
+		version = (parseResult.count("version") > 0);
+
+		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.2" << 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 (parenthesisStyle == "normal")
+	if (parenthesisStyleString == "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"))
-		{
-			const auto &inputFiles = variablesMap["input"].as<std::vector<std::string>>();
+		if (!inputFiles.empty())
 			anthem::translate(inputFiles, context);
-		}
 		else
 			anthem::translate("std::cin", std::cin, context);
 	}

include/anthem/ASTUtils.h

@@ -1,7 +1,7 @@
 #ifndef __ANTHEM__AST_UTILS_H
 #define __ANTHEM__AST_UTILS_H
 
-#include <experimental/optional>
+#include <optional>
 
 #include <anthem/AST.h>
 #include <anthem/ASTVisitors.h>
@@ -28,7 +28,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:

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>
@@ -30,7 +30,8 @@ struct Context
 	bool performSimplification = false;
 	bool performCompletion = false;
 
-	std::experimental::optional<std::vector<ast::PredicateSignature>> visiblePredicateSignatures;
+	std::optional<std::vector<ast::PredicateSignature>> visiblePredicateSignatures;
+	std::optional<std::vector<ast::PredicateSignature>> 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

@@ -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 &)
 	{

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;
 }
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////

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