Version bump for release 0.1.8 RC 3

Remove unnecessary parentheses
The unary modulus operation does not require extra parentheses to be printed in cases like “|X + Y|”. This adds a new option to the printing routine to omit parentheses in cases where the parent expression already defines a parenthesis-like scope (currently only with unary operations).
2018-04-12 01:06:28 +02:00 · 2018-04-12 00:59:03 +02:00 · 2018-04-12 00:38:48 +02:00 · 2018-04-11 23:21:56 +02:00 · 2018-04-11 21:50:15 +02:00 · 2018-04-11 21:42:08 +02:00
41 changed files with 1657 additions and 352 deletions
--- a/.ci/Dockerfile-arch-latest
+++ b/.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
--- a/.ci/Dockerfile-ubuntu-18.04
+++ b/.ci/Dockerfile-ubuntu-18.04
@@ -0,0 +1,10 @@
+FROM ubuntu:18.04
+
+ARG toolchain
+
+RUN apt-get update
+RUN apt-get install -y bison 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
--- a/.ci/ci.sh
+++ b/.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
--- a/.gitmodules
+++ b/.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
--- a/.travis.yml
+++ b/.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}"
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,10 +1,26 @@
 # Change Log

-## (unreleased)
+## 0.1.8 RC 3 (2018-04-12)
+
+### Features
+
+* more and advanced simplification rules
+* adds support for exponentiation (power) and modulus (absolute value)
+* new examples: prime numbers, permutation generator, and graph coloring (extended)
+
+## 0.1.7 (2018-04-08)
+
+### 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 +28,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 +36,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
--- a/CMakeLists.txt
+++ b/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)

--- a/LICENSE.md
+++ b/LICENSE.md
@@ -1,6 +1,6 @@
 # The MIT License (MIT)

-Copyright © 2016–2017 Patrick Lühne
+Copyright © 2016–2018 Patrick Lühne

 Permission is hereby granted, free of charge, to any person obtaining a copy
 of this software and associated documentation files (the "Software"), to deal
--- a/README.md
+++ b/README.md
@@ -9,15 +9,16 @@
 ## Usage

 ```bash
-$ anthem [--simplify] file...
+$ anthem [--complete] [--simplify] file...
 ```

-With the option `--simplify`, output formulas are simplified by applying several basic transformation rules.
+`--complete` instructs `anthem` to perform Clark’s completion on the translated formulas.
+With the option `--simplify`, the output formulas are simplified by applying several basic transformation rules.

 ## 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
--- a/app/CMakeLists.txt
+++ b/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
 )

--- a/app/main.cpp
+++ b/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.8-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 (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);
 	}
--- a/examples/graph-coloring.lp
+++ b/examples/graph-coloring.lp
@@ -1,12 +1,10 @@
-colored(V, red) :- vertex(V), not colored(V, green), not colored(V, blue).
-colored(V, green) :- vertex(V), not colored(V, red), not colored(V, blue).
-colored(V, blue) :- vertex(V), not colored(V, red), not colored(V, green).
+#external color(1).
+#external edge(2).
+#external vertex(1).
+#show color/2.

-:- edge(V1, V2), colored(V1, C), colored(V2, C).
-
-vertex(a).
-vertex(b).
-vertex(c).
-
-edge(a, b).
-edge(a, c).
+{color(V, C)} :- vertex(V), color(C).
+covered(V) :- color(V, _).
+:- vertex(V), not covered(V).
+:- color(V1, C), color(V2, C), edge(V1, V2).
+:- color(V, C1), color(V, C2), C1 != C2.
--- a/examples/permutations.lp
+++ b/examples/permutations.lp
@@ -0,0 +1,12 @@
+{p(1..n, 1..n)}.
+
+:- p(X, Y1), p(X, Y2), Y1 != Y2.
+:- p(X1, Y), p(X2, Y), X1 != X2.
+
+q1(X) :- p(X, _).
+q2(Y) :- p(_, Y).
+
+:- not q1(X), X = 1..n.
+:- not q2(Y), Y = 1..n.
+
+#show p/2.
--- a/examples/prime.lp
+++ b/examples/prime.lp
@@ -0,0 +1,4 @@
+#show prime/1.
+
+composite(I * J) :- I = 2..n, J = 2..n.
+prime(N) :- N = 2..n, not composite(N).
--- a/examples/schur-numbers.lp
+++ b/examples/schur-numbers.lp
@@ -3,3 +3,5 @@ covered(I) :- in(I, S).

 :- I = 1..n, not covered(I).
 :- in(I, S), in(J, S), in(I + J, S).
+
+#show in/2.
--- a/include/anthem/AST.h
+++ b/include/anthem/AST.h
@@ -32,7 +32,8 @@ struct BinaryOperation
 		Minus,
 		Multiplication,
 		Division,
-		Modulo
+		Modulo,
+		Power
 	};

 	explicit BinaryOperation(Operator operator_, Term &&left, Term &&right)
@@ -292,6 +293,30 @@ struct String

 ////////////////////////////////////////////////////////////////////////////////////////////////////

+struct UnaryOperation
+{
+	enum class Operator
+	{
+		Absolute
+	};
+
+	explicit UnaryOperation(Operator operator_, Term &&argument)
+	:	operator_{operator_},
+		argument{std::move(argument)}
+	{
+	}
+
+	UnaryOperation(const UnaryOperation &other) = delete;
+	UnaryOperation &operator=(const UnaryOperation &other) = delete;
+	UnaryOperation(UnaryOperation &&other) noexcept = default;
+	UnaryOperation &operator=(UnaryOperation &&other) noexcept = default;
+
+	Operator operator_;
+	Term argument;
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
 struct Variable
 {
 	explicit Variable(VariableDeclaration *declaration)
--- a/include/anthem/ASTForward.h
+++ b/include/anthem/ASTForward.h
@@ -37,6 +37,7 @@ struct Or;
 struct Predicate;
 struct SpecialInteger;
 struct String;
+struct UnaryOperation;
 struct Variable;
 struct VariableDeclaration;
 using VariableDeclarationPointer = std::unique_ptr<VariableDeclaration>;
@@ -68,6 +69,7 @@ using Term = Clingo::Variant<
 	Interval,
 	SpecialInteger,
 	String,
+	UnaryOperation,
 	Variable>;

 ////////////////////////////////////////////////////////////////////////////////////////////////////
--- a/include/anthem/ASTUtils.h
+++ b/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
--- a/include/anthem/ASTVisitors.h
+++ b/include/anthem/ASTVisitors.h
@@ -165,6 +165,14 @@ struct RecursiveTermVisitor
 		return T::accept(string, term, std::forward<Arguments>(arguments)...);
 	}

+	template <class... Arguments>
+	ReturnType visit(UnaryOperation &unaryOperation, Term &term, Arguments &&... arguments)
+	{
+		unaryOperation.argument.accept(*this, unaryOperation.argument, std::forward<Arguments>(arguments)...);
+
+		return T::accept(unaryOperation, term, std::forward<Arguments>(arguments)...);
+	}
+
 	template <class... Arguments>
 	ReturnType visit(Variable &variable, Term &term, Arguments &&... arguments)
 	{
--- a/include/anthem/Body.h
+++ b/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;
 	}
 };

--- a/include/anthem/Context.h
+++ b/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;
 };
--- a/include/anthem/Equality.h
+++ b/include/anthem/Equality.h
@@ -0,0 +1,430 @@
+#ifndef __ANTHEM__EQUALITY_H
+#define __ANTHEM__EQUALITY_H
+
+#include <anthem/AST.h>
+#include <anthem/ASTUtils.h>
+
+namespace anthem
+{
+namespace ast
+{
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+//
+// Equality
+//
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+// TODO: move to separate class
+enum class Tristate
+{
+	True,
+	False,
+	Unknown,
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+Tristate equal(const Formula &lhs, const Formula &rhs);
+Tristate equal(const Term &lhs, const Term &rhs);
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+struct FormulaEqualityVisitor
+{
+	Tristate visit(const And &and_, const Formula &otherFormula)
+	{
+		if (!otherFormula.is<And>())
+			return Tristate::Unknown;
+
+		const auto &otherAnd = otherFormula.get<And>();
+
+		for (const auto &argument : and_.arguments)
+		{
+			const auto match = std::find_if(
+				otherAnd.arguments.cbegin(), otherAnd.arguments.cend(),
+				[&](const auto &otherArgument)
+				{
+					return equal(argument, otherArgument) == Tristate::True;
+				});
+
+			if (match == otherAnd.arguments.cend())
+				return Tristate::Unknown;
+		}
+
+		for (const auto &otherArgument : otherAnd.arguments)
+		{
+			const auto match = std::find_if(
+				and_.arguments.cbegin(), and_.arguments.cend(),
+				[&](const auto &argument)
+				{
+					return equal(otherArgument, argument) == Tristate::True;
+				});
+
+			if (match == and_.arguments.cend())
+				return Tristate::Unknown;
+		}
+
+		return Tristate::True;
+	}
+
+	Tristate visit(const Biconditional &biconditional, const Formula &otherFormula)
+	{
+		if (!otherFormula.is<Biconditional>())
+			return Tristate::Unknown;
+
+		const auto &otherBiconditional = otherFormula.get<Biconditional>();
+
+		if (equal(biconditional.left, otherBiconditional.left) == Tristate::True
+		    && equal(biconditional.right, otherBiconditional.right) == Tristate::True)
+		{
+			return Tristate::True;
+		}
+
+		if (equal(biconditional.left, otherBiconditional.right) == Tristate::True
+		    && equal(biconditional.right, otherBiconditional.left) == Tristate::True)
+		{
+			return Tristate::True;
+		}
+
+		return Tristate::Unknown;
+	}
+
+	Tristate visit(const Boolean &boolean, const Formula &otherFormula)
+	{
+		if (!otherFormula.is<Boolean>())
+			return Tristate::Unknown;
+
+		const auto &otherBoolean = otherFormula.get<Boolean>();
+
+		return (boolean.value == otherBoolean.value)
+			? Tristate::True
+			: Tristate::False;
+	}
+
+	Tristate visit(const Comparison &comparison, const Formula &otherFormula)
+	{
+		if (!otherFormula.is<Comparison>())
+			return Tristate::Unknown;
+
+		const auto &otherComparison = otherFormula.get<Comparison>();
+
+		if (comparison.operator_ != otherComparison.operator_)
+			return Tristate::Unknown;
+
+		if (equal(comparison.left, otherComparison.left) == Tristate::True
+		    && equal(comparison.right, otherComparison.right) == Tristate::True)
+		{
+			return Tristate::True;
+		}
+
+		// Only = and != are commutative operators, all others don’t need to be checked with exchanged arguments
+		if (comparison.operator_ != Comparison::Operator::Equal
+		    && comparison.operator_ != Comparison::Operator::NotEqual)
+		{
+			return Tristate::Unknown;
+		}
+
+		if (equal(comparison.left, otherComparison.right) == Tristate::True
+		    && equal(comparison.right, otherComparison.left) == Tristate::True)
+		{
+			return Tristate::True;
+		}
+
+		return Tristate::Unknown;
+	}
+
+	Tristate visit(const Exists &, const Formula &otherFormula)
+	{
+		if (!otherFormula.is<Exists>())
+			return Tristate::Unknown;
+
+		// TODO: implement stronger check
+		return Tristate::Unknown;
+	}
+
+	Tristate visit(const ForAll &, const Formula &otherFormula)
+	{
+		if (!otherFormula.is<ForAll>())
+			return Tristate::Unknown;
+
+		// TODO: implement stronger check
+		return Tristate::Unknown;
+	}
+
+	Tristate visit(const Implies &implies, const Formula &otherFormula)
+	{
+		if (!otherFormula.is<Implies>())
+			return Tristate::Unknown;
+
+		const auto &otherImplies = otherFormula.get<Implies>();
+
+		if (equal(implies.antecedent, otherImplies.antecedent) == Tristate::True
+		    && equal(implies.consequent, otherImplies.consequent) == Tristate::True)
+		{
+			return Tristate::True;
+		}
+
+		return Tristate::Unknown;
+	}
+
+	Tristate visit(const In &in, const Formula &otherFormula)
+	{
+		if (!otherFormula.is<In>())
+			return Tristate::Unknown;
+
+		const auto &otherIn = otherFormula.get<In>();
+
+		if (equal(in.element, otherIn.element) == Tristate::True
+		    && equal(in.set, otherIn.set) == Tristate::True)
+		{
+			return Tristate::True;
+		}
+
+		return Tristate::Unknown;
+	}
+
+	Tristate visit(const Not &not_, const Formula &otherFormula)
+	{
+		if (!otherFormula.is<Not>())
+			return Tristate::Unknown;
+
+		const auto &otherNot = otherFormula.get<Not>();
+
+		return equal(not_.argument, otherNot.argument);
+	}
+
+	Tristate visit(const Or &or_, const Formula &otherFormula)
+	{
+		if (!otherFormula.is<Or>())
+			return Tristate::Unknown;
+
+		const auto &otherOr = otherFormula.get<Or>();
+
+		for (const auto &argument : or_.arguments)
+		{
+			const auto match = std::find_if(
+				otherOr.arguments.cbegin(), otherOr.arguments.cend(),
+				[&](const auto &otherArgument)
+				{
+					return equal(argument, otherArgument) == Tristate::True;
+				});
+
+			if (match == otherOr.arguments.cend())
+				return Tristate::Unknown;
+		}
+
+		for (const auto &otherArgument : otherOr.arguments)
+		{
+			const auto match = std::find_if(
+				or_.arguments.cbegin(), or_.arguments.cend(),
+				[&](const auto &argument)
+				{
+					return equal(otherArgument, argument) == Tristate::True;
+				});
+
+			if (match == or_.arguments.cend())
+				return Tristate::Unknown;
+		}
+
+		return Tristate::True;
+	}
+
+	Tristate visit(const Predicate &predicate, const Formula &otherFormula)
+	{
+		if (!otherFormula.is<Predicate>())
+			return Tristate::Unknown;
+
+		const auto &otherPredicate = otherFormula.get<Predicate>();
+
+		if (!matches(predicate, otherPredicate))
+			return Tristate::False;
+
+		assert(predicate.arguments.size() == otherPredicate.arguments.size());
+
+		for (size_t i = 0; i < predicate.arguments.size(); i++)
+			if (equal(predicate.arguments[i], otherPredicate.arguments[i]) != Tristate::True)
+				return Tristate::Unknown;
+
+		return Tristate::True;
+	}
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+struct TermEqualityVisitor
+{
+	Tristate visit(const BinaryOperation &binaryOperation, const Term &otherTerm)
+	{
+		if (!otherTerm.is<BinaryOperation>())
+			return Tristate::Unknown;
+
+		const auto &otherBinaryOperation = otherTerm.get<BinaryOperation>();
+
+		if (binaryOperation.operator_ != otherBinaryOperation.operator_)
+			return Tristate::Unknown;
+
+		if (equal(binaryOperation.left, otherBinaryOperation.left) == Tristate::True
+		    && equal(binaryOperation.right, otherBinaryOperation.right) == Tristate::True)
+		{
+			return Tristate::True;
+		}
+
+		// Only + and * are commutative operators, all others don’t need to be checked with exchanged arguments
+		if (binaryOperation.operator_ != BinaryOperation::Operator::Plus
+		    && binaryOperation.operator_ != BinaryOperation::Operator::Multiplication)
+		{
+			return Tristate::Unknown;
+		}
+
+		if (equal(binaryOperation.left, binaryOperation.right) == Tristate::True
+		    && equal(binaryOperation.right, binaryOperation.left) == Tristate::True)
+		{
+			return Tristate::True;
+		}
+
+		return Tristate::Unknown;
+	}
+
+	Tristate visit(const Boolean &boolean, const Term &otherTerm)
+	{
+		if (!otherTerm.is<Boolean>())
+			return Tristate::Unknown;
+
+		const auto &otherBoolean = otherTerm.get<Boolean>();
+
+		return (boolean.value == otherBoolean.value)
+			? Tristate::True
+			: Tristate::False;
+	}
+
+	Tristate visit(const Constant &constant, const Term &otherTerm)
+	{
+		if (!otherTerm.is<Constant>())
+			return Tristate::Unknown;
+
+		const auto &otherConstant = otherTerm.get<Constant>();
+
+		return (constant.name == otherConstant.name)
+			? Tristate::True
+			: Tristate::False;
+	}
+
+	Tristate visit(const Function &function, const Term &otherTerm)
+	{
+		if (!otherTerm.is<Function>())
+			return Tristate::Unknown;
+
+		const auto &otherFunction = otherTerm.get<Function>();
+
+		if (function.name != otherFunction.name)
+			return Tristate::False;
+
+		if (function.arguments.size() != otherFunction.arguments.size())
+			return Tristate::False;
+
+		for (size_t i = 0; i < function.arguments.size(); i++)
+			if (equal(function.arguments[i], otherFunction.arguments[i]) != Tristate::True)
+				return Tristate::Unknown;
+
+		return Tristate::True;
+	}
+
+	Tristate visit(const Integer &integer, const Term &otherTerm)
+	{
+		if (!otherTerm.is<Integer>())
+			return Tristate::Unknown;
+
+		const auto &otherInteger = otherTerm.get<Integer>();
+
+		return (integer.value == otherInteger.value)
+			? Tristate::True
+			: Tristate::False;
+	}
+
+	Tristate visit(const Interval &interval, const Term &otherTerm)
+	{
+		if (!otherTerm.is<Interval>())
+			return Tristate::Unknown;
+
+		const auto &otherInterval = otherTerm.get<Interval>();
+
+		if (equal(interval.from, otherInterval.from) != Tristate::True)
+			return Tristate::Unknown;
+
+		if (equal(interval.to, otherInterval.to) != Tristate::True)
+			return Tristate::Unknown;
+
+		return Tristate::True;
+	}
+
+	Tristate visit(const SpecialInteger &specialInteger, const Term &otherTerm)
+	{
+		if (!otherTerm.is<SpecialInteger>())
+			return Tristate::Unknown;
+
+		const auto &otherSpecialInteger = otherTerm.get<SpecialInteger>();
+
+		return (specialInteger.type == otherSpecialInteger.type)
+			? Tristate::True
+			: Tristate::False;
+	}
+
+	Tristate visit(const String &string, const Term &otherTerm)
+	{
+		if (!otherTerm.is<String>())
+			return Tristate::Unknown;
+
+		const auto &otherString = otherTerm.get<String>();
+
+		return (string.text == otherString.text)
+			? Tristate::True
+			: Tristate::False;
+	}
+
+	Tristate visit(const UnaryOperation &unaryOperation, const Term &otherTerm)
+	{
+		if (!otherTerm.is<UnaryOperation>())
+			return Tristate::Unknown;
+
+		const auto &otherUnaryOperation = otherTerm.get<UnaryOperation>();
+
+		if (unaryOperation.operator_ != otherUnaryOperation.operator_)
+			return Tristate::Unknown;
+
+		return equal(unaryOperation.argument, otherUnaryOperation.argument);
+	}
+
+	Tristate visit(const Variable &variable, const Term &otherTerm)
+	{
+		if (!otherTerm.is<Variable>())
+			return Tristate::Unknown;
+
+		const auto &otherVariable = otherTerm.get<Variable>();
+
+		return (variable.declaration == otherVariable.declaration)
+			? Tristate::True
+			: Tristate::False;
+	}
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+Tristate equal(const Formula &lhs, const Formula &rhs)
+{
+	return lhs.accept(FormulaEqualityVisitor(), rhs);
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+Tristate equal(const Term &lhs, const Term &rhs)
+{
+	return lhs.accept(TermEqualityVisitor(), rhs);
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+}
+}
+
+#endif
--- a/include/anthem/Head.h
+++ b/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;
 	}
 };

--- a/include/anthem/Simplification.h
+++ b/include/anthem/Simplification.h
@@ -12,6 +12,14 @@ namespace anthem
 //
 ////////////////////////////////////////////////////////////////////////////////////////////////////

+enum class SimplificationResult
+{
+	Simplified,
+	Unchanged,
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
 void simplify(ast::Formula &formula);

 ////////////////////////////////////////////////////////////////////////////////////////////////////
--- a/include/anthem/SimplificationVisitors.h
+++ b/include/anthem/SimplificationVisitors.h
@@ -0,0 +1,198 @@
+#ifndef __ANTHEM__SIMPLIFICATION_VISITORS_H
+#define __ANTHEM__SIMPLIFICATION_VISITORS_H
+
+#include <anthem/AST.h>
+#include <anthem/Simplification.h>
+
+namespace anthem
+{
+namespace ast
+{
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+//
+// Simplification Visitor
+//
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+template<class T>
+struct FormulaSimplificationVisitor
+{
+	template <class... Arguments>
+	SimplificationResult visit(And &and_, Formula &formula, Arguments &&... arguments)
+	{
+		for (auto &argument : and_.arguments)
+			if (argument.accept(*this, argument, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
+				return SimplificationResult::Simplified;
+
+		return T::accept(formula, std::forward<Arguments>(arguments)...);
+	}
+
+	template <class... Arguments>
+	SimplificationResult visit(Biconditional &biconditional, Formula &formula, Arguments &&... arguments)
+	{
+		if (biconditional.left.accept(*this, biconditional.left, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
+			return SimplificationResult::Simplified;
+
+		if (biconditional.right.accept(*this, biconditional.right, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
+			return SimplificationResult::Simplified;
+
+		return T::accept(formula, std::forward<Arguments>(arguments)...);
+	}
+
+	template <class... Arguments>
+	SimplificationResult visit(Boolean &, Formula &formula, Arguments &&... arguments)
+	{
+		return T::accept(formula, std::forward<Arguments>(arguments)...);
+	}
+
+	template <class... Arguments>
+	SimplificationResult visit(Comparison &, Formula &formula, Arguments &&... arguments)
+	{
+		return T::accept(formula, std::forward<Arguments>(arguments)...);
+	}
+
+	template <class... Arguments>
+	SimplificationResult visit(Exists &exists, Formula &formula, Arguments &&... arguments)
+	{
+		if (exists.argument.accept(*this, exists.argument, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
+			return SimplificationResult::Simplified;
+
+		return T::accept(formula, std::forward<Arguments>(arguments)...);
+	}
+
+	template <class... Arguments>
+	SimplificationResult visit(ForAll &forAll, Formula &formula, Arguments &&... arguments)
+	{
+		if (forAll.argument.accept(*this, forAll.argument, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
+			return SimplificationResult::Simplified;
+
+		return T::accept(formula, std::forward<Arguments>(arguments)...);
+	}
+
+	template <class... Arguments>
+	SimplificationResult visit(Implies &implies, Formula &formula, Arguments &&... arguments)
+	{
+		if (implies.antecedent.accept(*this, implies.antecedent, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
+			return SimplificationResult::Simplified;
+
+		if (implies.consequent.accept(*this, implies.consequent, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
+			return SimplificationResult::Simplified;
+
+		return T::accept(formula, std::forward<Arguments>(arguments)...);
+	}
+
+	template <class... Arguments>
+	SimplificationResult visit(In &, Formula &formula, Arguments &&... arguments)
+	{
+		return T::accept(formula, std::forward<Arguments>(arguments)...);
+	}
+
+	template <class... Arguments>
+	SimplificationResult visit(Not &not_, Formula &formula, Arguments &&... arguments)
+	{
+		if (not_.argument.accept(*this, not_.argument, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
+			return SimplificationResult::Simplified;
+
+		return T::accept(formula, std::forward<Arguments>(arguments)...);
+	}
+
+	template <class... Arguments>
+	SimplificationResult visit(Or &or_, Formula &formula, Arguments &&... arguments)
+	{
+		for (auto &argument : or_.arguments)
+			if (argument.accept(*this, argument, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
+				return SimplificationResult::Simplified;
+
+		return T::accept(formula, std::forward<Arguments>(arguments)...);
+	}
+
+	template <class... Arguments>
+	SimplificationResult visit(Predicate &, Formula &formula, Arguments &&... arguments)
+	{
+		return T::accept(formula, std::forward<Arguments>(arguments)...);
+	}
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+template<class T, class SimplificationResult = void>
+struct TermSimplificationVisitor
+{
+	template <class... Arguments>
+	SimplificationResult visit(BinaryOperation &binaryOperation, Term &term, Arguments &&... arguments)
+	{
+		if (binaryOperation.left.accept(*this, binaryOperation.left, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
+			return SimplificationResult::Simplified;
+
+		if (binaryOperation.right.accept(*this, binaryOperation.right, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
+			return SimplificationResult::Simplified;
+
+		return T::accept(term, std::forward<Arguments>(arguments)...);
+	}
+
+	template <class... Arguments>
+	SimplificationResult visit(Boolean &, Term &term, Arguments &&... arguments)
+	{
+		return T::accept(term, std::forward<Arguments>(arguments)...);
+	}
+
+	template <class... Arguments>
+	SimplificationResult visit(Constant &, Term &term, Arguments &&... arguments)
+	{
+		return T::accept(term, std::forward<Arguments>(arguments)...);
+	}
+
+	template <class... Arguments>
+	SimplificationResult visit(Function &function, Term &term, Arguments &&... arguments)
+	{
+		for (auto &argument : function.arguments)
+			if (argument.accept(*this, argument, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
+				return SimplificationResult::Simplified;
+
+		return T::accept(term, std::forward<Arguments>(arguments)...);
+	}
+
+	template <class... Arguments>
+	SimplificationResult visit(Integer &, Term &term, Arguments &&... arguments)
+	{
+		return T::accept(term, std::forward<Arguments>(arguments)...);
+	}
+
+	template <class... Arguments>
+	SimplificationResult visit(Interval &interval, Term &term, Arguments &&... arguments)
+	{
+		if (interval.from.accept(*this, interval.from, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
+			return SimplificationResult::Simplified;
+
+		if (interval.to.accept(*this, interval.to, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
+			return SimplificationResult::Simplified;
+
+		return T::accept(term, std::forward<Arguments>(arguments)...);
+	}
+
+	template <class... Arguments>
+	SimplificationResult visit(SpecialInteger &, Term &term, Arguments &&... arguments)
+	{
+		return T::accept(term, std::forward<Arguments>(arguments)...);
+	}
+
+	template <class... Arguments>
+	SimplificationResult visit(String &, Term &term, Arguments &&... arguments)
+	{
+		return T::accept(term, std::forward<Arguments>(arguments)...);
+	}
+
+	template <class... Arguments>
+	SimplificationResult visit(Variable &, Term &term, Arguments &&... arguments)
+	{
+		return T::accept(term, std::forward<Arguments>(arguments)...);
+	}
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+}
+}
+
+#endif
--- 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<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 &)
 	{
--- a/include/anthem/Term.h
+++ b/include/anthem/Term.h
@@ -23,6 +23,12 @@ ast::BinaryOperation::Operator translate(Clingo::AST::BinaryOperator binaryOpera
 {
 	switch (binaryOperator)
 	{
+		case Clingo::AST::BinaryOperator::XOr:
+			throw TranslationException(term.location, "binary operation “xor” currently unsupported");
+		case Clingo::AST::BinaryOperator::Or:
+			throw TranslationException(term.location, "binary operation “or” currently unsupported");
+		case Clingo::AST::BinaryOperator::And:
+			throw TranslationException(term.location, "binary operation “and” currently unsupported");
 		case Clingo::AST::BinaryOperator::Plus:
 			return ast::BinaryOperation::Operator::Plus;
 		case Clingo::AST::BinaryOperator::Minus:
@@ -33,11 +39,28 @@ ast::BinaryOperation::Operator translate(Clingo::AST::BinaryOperator binaryOpera
 			return ast::BinaryOperation::Operator::Division;
 		case Clingo::AST::BinaryOperator::Modulo:
 			return ast::BinaryOperation::Operator::Modulo;
-		default:
-			throw TranslationException(term.location, "“binary operation” terms currently unsupported");
+		case Clingo::AST::BinaryOperator::Power:
+			return ast::BinaryOperation::Operator::Power;
 	}

-	return ast::BinaryOperation::Operator::Plus;
+	throw TranslationException(term.location, "unknown binary operation");
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+ast::UnaryOperation::Operator translate(Clingo::AST::UnaryOperator unaryOperator, const Clingo::AST::Term &term)
+{
+	switch (unaryOperator)
+	{
+		case Clingo::AST::UnaryOperator::Absolute:
+			return ast::UnaryOperation::Operator::Absolute;
+		case Clingo::AST::UnaryOperator::Minus:
+			throw TranslationException(term.location, "binary operation “minus” currently unsupported");
+		case Clingo::AST::UnaryOperator::Negation:
+			throw TranslationException(term.location, "binary operation “negation” currently unsupported");
+	}
+
+	throw TranslationException(term.location, "unknown unary operation");
 }

 ////////////////////////////////////////////////////////////////////////////////////////////////////
@@ -48,7 +71,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 +104,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 +123,7 @@ 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 &)
-	{
-		throw TranslationException(term.location, "“unary operation” terms currently unsupported");
-		return std::experimental::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 +132,15 @@ 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::UnaryOperation &unaryOperation, const Clingo::AST::Term &term, RuleContext &ruleContext, const ast::VariableStack &variableStack)
+	{
+		const auto operator_ = translate(unaryOperation.unary_operator, term);
+		auto argument = translate(unaryOperation.argument, ruleContext, variableStack);
+
+		return ast::Term::make<ast::UnaryOperation>(operator_, std::move(argument));
+	}
+
+	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 +148,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 +162,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;
 	}
 };

--- a/include/anthem/output/AST.h
+++ b/include/anthem/output/AST.h
@@ -41,37 +41,39 @@ struct PrintContext

 ////////////////////////////////////////////////////////////////////////////////////////////////////

-output::ColorStream &print(output::ColorStream &stream, const BinaryOperation::Operator operator_, PrintContext &printContext);
-output::ColorStream &print(output::ColorStream &stream, const BinaryOperation &binaryOperation, PrintContext &printContext);
-output::ColorStream &print(output::ColorStream &stream, const Boolean &boolean, PrintContext &printContext);
-output::ColorStream &print(output::ColorStream &stream, const Comparison &comparison, PrintContext &printContext);
-output::ColorStream &print(output::ColorStream &stream, const Constant &constant, PrintContext &printContext);
-output::ColorStream &print(output::ColorStream &stream, const Function &function, PrintContext &printContext);
-output::ColorStream &print(output::ColorStream &stream, const In &in, PrintContext &printContext);
-output::ColorStream &print(output::ColorStream &stream, const Integer &integer, PrintContext &printContext);
-output::ColorStream &print(output::ColorStream &stream, const Interval &interval, PrintContext &printContext);
-output::ColorStream &print(output::ColorStream &stream, const Predicate &predicate, PrintContext &printContext);
-output::ColorStream &print(output::ColorStream &stream, const SpecialInteger &specialInteger, PrintContext &printContext);
-output::ColorStream &print(output::ColorStream &stream, const String &string, PrintContext &printContext);
-output::ColorStream &print(output::ColorStream &stream, const Variable &variable, PrintContext &printContext);
-output::ColorStream &print(output::ColorStream &stream, const VariableDeclaration &variableDeclaration, PrintContext &printContext);
+output::ColorStream &print(output::ColorStream &stream, const BinaryOperation::Operator operator_, PrintContext &printContext, bool omitParentheses = false);
+output::ColorStream &print(output::ColorStream &stream, const BinaryOperation &binaryOperation, PrintContext &printContext, bool omitParentheses = false);
+output::ColorStream &print(output::ColorStream &stream, const Boolean &boolean, PrintContext &printContext, bool omitParentheses = false);
+output::ColorStream &print(output::ColorStream &stream, const Comparison &comparison, PrintContext &printContext, bool omitParentheses = false);
+output::ColorStream &print(output::ColorStream &stream, Comparison::Operator operator_, PrintContext &printContext, bool omitParentheses = false);
+output::ColorStream &print(output::ColorStream &stream, const Constant &constant, PrintContext &printContext, bool omitParentheses = false);
+output::ColorStream &print(output::ColorStream &stream, const Function &function, PrintContext &printContext, bool omitParentheses = false);
+output::ColorStream &print(output::ColorStream &stream, const In &in, PrintContext &printContext, bool omitParentheses = false);
+output::ColorStream &print(output::ColorStream &stream, const Integer &integer, PrintContext &printContext, bool omitParentheses = false);
+output::ColorStream &print(output::ColorStream &stream, const Interval &interval, PrintContext &printContext, bool omitParentheses = false);
+output::ColorStream &print(output::ColorStream &stream, const Predicate &predicate, PrintContext &printContext, bool omitParentheses = false);
+output::ColorStream &print(output::ColorStream &stream, const SpecialInteger &specialInteger, PrintContext &printContext, bool omitParentheses = false);
+output::ColorStream &print(output::ColorStream &stream, const String &string, PrintContext &printContext, bool omitParentheses = false);
+output::ColorStream &print(output::ColorStream &stream, const UnaryOperation &unaryOperation, PrintContext &printContext, bool omitParentheses = false);
+output::ColorStream &print(output::ColorStream &stream, const Variable &variable, PrintContext &printContext, bool omitParentheses = false);
+output::ColorStream &print(output::ColorStream &stream, const VariableDeclaration &variableDeclaration, PrintContext &printContext, bool omitParentheses = false);

-output::ColorStream &print(output::ColorStream &stream, const And &and_, PrintContext &printContext);
-output::ColorStream &print(output::ColorStream &stream, const Biconditional &biconditional, PrintContext &printContext);
-output::ColorStream &print(output::ColorStream &stream, const Exists &exists, PrintContext &printContext);
-output::ColorStream &print(output::ColorStream &stream, const ForAll &forAll, PrintContext &printContext);
-output::ColorStream &print(output::ColorStream &stream, const Implies &implies, PrintContext &printContext);
-output::ColorStream &print(output::ColorStream &stream, const Not &not_, PrintContext &printContext);
-output::ColorStream &print(output::ColorStream &stream, const Or &or_, PrintContext &printContext);
+output::ColorStream &print(output::ColorStream &stream, const And &and_, PrintContext &printContext, bool omitParentheses = false);
+output::ColorStream &print(output::ColorStream &stream, const Biconditional &biconditional, PrintContext &printContext, bool omitParentheses = false);
+output::ColorStream &print(output::ColorStream &stream, const Exists &exists, PrintContext &printContext, bool omitParentheses = false);
+output::ColorStream &print(output::ColorStream &stream, const ForAll &forAll, PrintContext &printContext, bool omitParentheses = false);
+output::ColorStream &print(output::ColorStream &stream, const Implies &implies, PrintContext &printContext, bool omitParentheses = false);
+output::ColorStream &print(output::ColorStream &stream, const Not &not_, PrintContext &printContext, bool omitParentheses = false);
+output::ColorStream &print(output::ColorStream &stream, const Or &or_, PrintContext &printContext, bool omitParentheses = false);

-output::ColorStream &print(output::ColorStream &stream, const Formula &formula, PrintContext &printContext);
-output::ColorStream &print(output::ColorStream &stream, const Term &term, PrintContext &printContext);
+output::ColorStream &print(output::ColorStream &stream, const Formula &formula, PrintContext &printContext, bool omitParentheses = false);
+output::ColorStream &print(output::ColorStream &stream, const Term &term, PrintContext &printContext, bool omitParentheses = false);

 ////////////////////////////////////////////////////////////////////////////////////////////////////
 // Primitives
 ////////////////////////////////////////////////////////////////////////////////////////////////////

-inline output::ColorStream &print(output::ColorStream &stream, BinaryOperation::Operator operator_, PrintContext &)
+inline output::ColorStream &print(output::ColorStream &stream, BinaryOperation::Operator operator_, PrintContext &, bool)
 {
 	switch (operator_)
 	{
@@ -85,6 +87,8 @@ inline output::ColorStream &print(output::ColorStream &stream, BinaryOperation::
 			return (stream << output::Operator("/"));
 		case BinaryOperation::Operator::Modulo:
 			return (stream << output::Operator("%"));
+		case BinaryOperation::Operator::Power:
+			return (stream << output::Operator("**"));
 	}

 	return stream;
@@ -92,22 +96,26 @@ inline output::ColorStream &print(output::ColorStream &stream, BinaryOperation::

 ////////////////////////////////////////////////////////////////////////////////////////////////////

-inline output::ColorStream &print(output::ColorStream &stream, const BinaryOperation &binaryOperation, PrintContext &printContext)
+inline output::ColorStream &print(output::ColorStream &stream, const BinaryOperation &binaryOperation, PrintContext &printContext, bool omitParentheses)
 {
-	stream << "(";
+	if (!omitParentheses || printContext.context.parenthesisStyle == ParenthesisStyle::Full)
+		stream << "(";
+
 	print(stream, binaryOperation.left, printContext);
 	stream << " ";
 	print(stream, binaryOperation.operator_, printContext);
 	stream << " ";
 	print(stream, binaryOperation.right, printContext);
-	stream << ")";
+
+	if (!omitParentheses || printContext.context.parenthesisStyle == ParenthesisStyle::Full)
+		stream << ")";

 	return stream;
 }

 ////////////////////////////////////////////////////////////////////////////////////////////////////

-inline output::ColorStream &print(output::ColorStream &stream, const Boolean &boolean, PrintContext &)
+inline output::ColorStream &print(output::ColorStream &stream, const Boolean &boolean, PrintContext &, bool)
 {
 	if (boolean.value)
 		return (stream << output::Boolean("#true"));
@@ -117,7 +125,7 @@ inline output::ColorStream &print(output::ColorStream &stream, const Boolean &bo

 ////////////////////////////////////////////////////////////////////////////////////////////////////

-inline output::ColorStream &print(output::ColorStream &stream, Comparison::Operator operator_, PrintContext &)
+inline output::ColorStream &print(output::ColorStream &stream, Comparison::Operator operator_, PrintContext &, bool)
 {
 	switch (operator_)
 	{
@@ -140,7 +148,7 @@ inline output::ColorStream &print(output::ColorStream &stream, Comparison::Opera

 ////////////////////////////////////////////////////////////////////////////////////////////////////

-inline output::ColorStream &print(output::ColorStream &stream, const Comparison &comparison, PrintContext &printContext)
+inline output::ColorStream &print(output::ColorStream &stream, const Comparison &comparison, PrintContext &printContext, bool)
 {
 	if (printContext.context.parenthesisStyle == ParenthesisStyle::Full)
 		stream << "(";
@@ -159,14 +167,14 @@ inline output::ColorStream &print(output::ColorStream &stream, const Comparison

 ////////////////////////////////////////////////////////////////////////////////////////////////////

-inline output::ColorStream &print(output::ColorStream &stream, const Constant &constant, PrintContext &)
+inline output::ColorStream &print(output::ColorStream &stream, const Constant &constant, PrintContext &, bool)
 {
 	return (stream << constant.name);
 }

 ////////////////////////////////////////////////////////////////////////////////////////////////////

-inline output::ColorStream &print(output::ColorStream &stream, const Function &function, PrintContext &printContext)
+inline output::ColorStream &print(output::ColorStream &stream, const Function &function, PrintContext &printContext, bool)
 {
 	stream << function.name;

@@ -193,7 +201,7 @@ inline output::ColorStream &print(output::ColorStream &stream, const Function &f

 ////////////////////////////////////////////////////////////////////////////////////////////////////

-inline output::ColorStream &print(output::ColorStream &stream, const In &in, PrintContext &printContext)
+inline output::ColorStream &print(output::ColorStream &stream, const In &in, PrintContext &printContext, bool)
 {
 	if (printContext.context.parenthesisStyle == ParenthesisStyle::Full)
 		stream << "(";
@@ -210,14 +218,14 @@ inline output::ColorStream &print(output::ColorStream &stream, const In &in, Pri

 ////////////////////////////////////////////////////////////////////////////////////////////////////

-inline output::ColorStream &print(output::ColorStream &stream, const Integer &integer, PrintContext &)
+inline output::ColorStream &print(output::ColorStream &stream, const Integer &integer, PrintContext &, bool)
 {
 	return (stream << output::Number<int>(integer.value));
 }

 ////////////////////////////////////////////////////////////////////////////////////////////////////

-inline output::ColorStream &print(output::ColorStream &stream, const Interval &interval, PrintContext &printContext)
+inline output::ColorStream &print(output::ColorStream &stream, const Interval &interval, PrintContext &printContext, bool)
 {
 	if (printContext.context.parenthesisStyle == ParenthesisStyle::Full)
 		stream << "(";
@@ -234,7 +242,7 @@ inline output::ColorStream &print(output::ColorStream &stream, const Interval &i

 ////////////////////////////////////////////////////////////////////////////////////////////////////

-inline output::ColorStream &print(output::ColorStream &stream, const Predicate &predicate, PrintContext &printContext)
+inline output::ColorStream &print(output::ColorStream &stream, const Predicate &predicate, PrintContext &printContext, bool)
 {
 	stream << predicate.name;

@@ -258,7 +266,7 @@ inline output::ColorStream &print(output::ColorStream &stream, const Predicate &

 ////////////////////////////////////////////////////////////////////////////////////////////////////

-inline output::ColorStream &print(output::ColorStream &stream, const SpecialInteger &specialInteger, PrintContext &)
+inline output::ColorStream &print(output::ColorStream &stream, const SpecialInteger &specialInteger, PrintContext &, bool)
 {
 	switch (specialInteger.type)
 	{
@@ -273,14 +281,37 @@ inline output::ColorStream &print(output::ColorStream &stream, const SpecialInte

 ////////////////////////////////////////////////////////////////////////////////////////////////////

-inline output::ColorStream &print(output::ColorStream &stream, const String &string, PrintContext &)
+inline output::ColorStream &print(output::ColorStream &stream, const String &string, PrintContext &, bool)
 {
 	return (stream << output::String(string.text.c_str()));
 }

 ////////////////////////////////////////////////////////////////////////////////////////////////////

-inline output::ColorStream &print(output::ColorStream &stream, const Variable &variable, PrintContext &printContext)
+inline output::ColorStream &print(output::ColorStream &stream, const UnaryOperation &unaryOperation, PrintContext &printContext, bool)
+{
+	switch (unaryOperation.operator_)
+	{
+		case UnaryOperation::Operator::Absolute:
+			stream << "|";
+			break;
+	}
+
+	print(stream, unaryOperation.argument, printContext, true);
+
+	switch (unaryOperation.operator_)
+	{
+		case UnaryOperation::Operator::Absolute:
+			stream << "|";
+			break;
+	}
+
+	return stream;
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+inline output::ColorStream &print(output::ColorStream &stream, const Variable &variable, PrintContext &printContext, bool)
 {
 	assert(variable.declaration != nullptr);

@@ -289,7 +320,7 @@ inline output::ColorStream &print(output::ColorStream &stream, const Variable &v

 ////////////////////////////////////////////////////////////////////////////////////////////////////

-inline output::ColorStream &print(output::ColorStream &stream, const VariableDeclaration &variableDeclaration, PrintContext &printContext)
+inline output::ColorStream &print(output::ColorStream &stream, const VariableDeclaration &variableDeclaration, PrintContext &printContext, bool)
 {
 	const auto printVariableDeclaration =
 		[&stream, &variableDeclaration](const auto *prefix, auto &variableIDs) -> output::ColorStream &
@@ -325,9 +356,10 @@ inline output::ColorStream &print(output::ColorStream &stream, const VariableDec
 // Expressions
 ////////////////////////////////////////////////////////////////////////////////////////////////////

-inline output::ColorStream &print(output::ColorStream &stream, const And &and_, PrintContext &printContext)
+inline output::ColorStream &print(output::ColorStream &stream, const And &and_, PrintContext &printContext, bool omitParentheses)
 {
-	stream << "(";
+	if (!omitParentheses || printContext.context.parenthesisStyle == ParenthesisStyle::Full)
+		stream << "(";

 	for (auto i = and_.arguments.cbegin(); i != and_.arguments.cend(); i++)
 	{
@@ -337,27 +369,32 @@ inline output::ColorStream &print(output::ColorStream &stream, const And &and_,
 		print(stream, *i, printContext);
 	}

-	stream << ")";
+	if (!omitParentheses || printContext.context.parenthesisStyle == ParenthesisStyle::Full)
+		stream << ")";

 	return stream;
 }

 ////////////////////////////////////////////////////////////////////////////////////////////////////

-inline output::ColorStream &print(output::ColorStream &stream, const Biconditional &biconditional, PrintContext &printContext)
+inline output::ColorStream &print(output::ColorStream &stream, const Biconditional &biconditional, PrintContext &printContext, bool omitParentheses)
 {
-	stream << "(";
+	if (!omitParentheses || printContext.context.parenthesisStyle == ParenthesisStyle::Full)
+		stream << "(";
+
 	print(stream, biconditional.left, printContext);
 	stream << " <-> ";
 	print(stream, biconditional.right, printContext);
-	stream << ")";
+
+	if (!omitParentheses || printContext.context.parenthesisStyle == ParenthesisStyle::Full)
+		stream << ")";

 	return stream;
 }

 ////////////////////////////////////////////////////////////////////////////////////////////////////

-inline output::ColorStream &print(output::ColorStream &stream, const Exists &exists, PrintContext &printContext)
+inline output::ColorStream &print(output::ColorStream &stream, const Exists &exists, PrintContext &printContext, bool)
 {
 	if (printContext.context.parenthesisStyle == ParenthesisStyle::Full)
 		stream << "(";
@@ -383,7 +420,7 @@ inline output::ColorStream &print(output::ColorStream &stream, const Exists &exi

 ////////////////////////////////////////////////////////////////////////////////////////////////////

-inline output::ColorStream &print(output::ColorStream &stream, const ForAll &forAll, PrintContext &printContext)
+inline output::ColorStream &print(output::ColorStream &stream, const ForAll &forAll, PrintContext &printContext, bool)
 {
 	if (printContext.context.parenthesisStyle == ParenthesisStyle::Full)
 		stream << "(";
@@ -409,20 +446,24 @@ inline output::ColorStream &print(output::ColorStream &stream, const ForAll &for

 ////////////////////////////////////////////////////////////////////////////////////////////////////

-inline output::ColorStream &print(output::ColorStream &stream, const Implies &implies, PrintContext &printContext)
+inline output::ColorStream &print(output::ColorStream &stream, const Implies &implies, PrintContext &printContext, bool omitParentheses)
 {
-	stream << "(";
+	if (!omitParentheses || printContext.context.parenthesisStyle == ParenthesisStyle::Full)
+		stream << "(";
+
 	print(stream, implies.antecedent, printContext);
 	stream << " -> ";
 	print(stream, implies.consequent, printContext);
-	stream << ")";
+
+	if (!omitParentheses || printContext.context.parenthesisStyle == ParenthesisStyle::Full)
+		stream << ")";

 	return stream;
 }

 ////////////////////////////////////////////////////////////////////////////////////////////////////

-inline output::ColorStream &print(output::ColorStream &stream, const Not &not_, PrintContext &printContext)
+inline output::ColorStream &print(output::ColorStream &stream, const Not &not_, PrintContext &printContext, bool)
 {
 	if (printContext.context.parenthesisStyle == ParenthesisStyle::Full)
 		stream << "(";
@@ -438,9 +479,10 @@ inline output::ColorStream &print(output::ColorStream &stream, const Not &not_,

 ////////////////////////////////////////////////////////////////////////////////////////////////////

-inline output::ColorStream &print(output::ColorStream &stream, const Or &or_, PrintContext &printContext)
+inline output::ColorStream &print(output::ColorStream &stream, const Or &or_, PrintContext &printContext, bool omitParentheses)
 {
-	stream << "(";
+	if (!omitParentheses || printContext.context.parenthesisStyle == ParenthesisStyle::Full)
+		stream << "(";

 	for (auto i = or_.arguments.cbegin(); i != or_.arguments.cend(); i++)
 	{
@@ -450,7 +492,8 @@ inline output::ColorStream &print(output::ColorStream &stream, const Or &or_, Pr
 		print(stream, *i, printContext);
 	}

-	stream << ")";
+	if (!omitParentheses || printContext.context.parenthesisStyle == ParenthesisStyle::Full)
+		stream << ")";

 	return stream;
 }
@@ -463,24 +506,24 @@ template<class Variant>
 struct VariantPrintVisitor
 {
 	template<class T>
-	output::ColorStream &visit(const T &x, output::ColorStream &stream, PrintContext &printContext)
+	output::ColorStream &visit(const T &x, output::ColorStream &stream, PrintContext &printContext, bool omitParentheses)
 	{
-		return print(stream, x, printContext);
+		return print(stream, x, printContext, omitParentheses);
 	}
 };

 ////////////////////////////////////////////////////////////////////////////////////////////////////

-inline output::ColorStream &print(output::ColorStream &stream, const Formula &formula, PrintContext &printContext)
+inline output::ColorStream &print(output::ColorStream &stream, const Formula &formula, PrintContext &printContext, bool omitParentheses)
 {
-	return formula.accept(VariantPrintVisitor<Formula>(), stream, printContext);
+	return formula.accept(VariantPrintVisitor<Formula>(), stream, printContext, omitParentheses);
 }

 ////////////////////////////////////////////////////////////////////////////////////////////////////

-inline output::ColorStream &print(output::ColorStream &stream, const Term &term, PrintContext &printContext)
+inline output::ColorStream &print(output::ColorStream &stream, const Term &term, PrintContext &printContext, bool omitParentheses)
 {
-	return term.accept(VariantPrintVisitor<Term>(), stream, printContext);
+	return term.accept(VariantPrintVisitor<Term>(), stream, printContext, omitParentheses);
 }

 ////////////////////////////////////////////////////////////////////////////////////////////////////
--- a/lib/catch
+++ b/lib/catch
--- a/lib/clingo
+++ b/lib/clingo
--- a/lib/cxxopts
+++ b/lib/cxxopts
--- a/src/anthem/ASTCopy.cpp
+++ b/src/anthem/ASTCopy.cpp
@@ -159,6 +159,13 @@ String prepareCopy(const String &other)

 ////////////////////////////////////////////////////////////////////////////////////////////////////

+UnaryOperation prepareCopy(const UnaryOperation &other)
+{
+	return UnaryOperation(other.operator_, prepareCopy(other.argument));
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
 Variable prepareCopy(const Variable &other)
 {
 	return Variable(other.declaration);
@@ -320,6 +327,12 @@ struct FixDanglingVariablesInTermVisitor
 	{
 	}

+	template <class... Arguments>
+	void visit(UnaryOperation &unaryOperation, Arguments &&... arguments)
+	{
+		unaryOperation.argument.accept(*this, std::forward<Arguments>(arguments)...);
+	}
+
 	void visit(Variable &variable, ScopedFormula &scopedFormula, VariableStack &variableStack,
 		std::map<VariableDeclaration *, VariableDeclaration *> &replacements)
 	{
--- a/src/anthem/ASTUtils.cpp
+++ b/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;
 }

 ////////////////////////////////////////////////////////////////////////////////////////////////////
@@ -59,7 +59,7 @@ bool VariableStack::contains(const VariableDeclaration &variableDeclaration) con
 		};

 	const auto layerContainsVariableDeclaration =
-		[&variableDeclaration, &variableDeclarationMatches](const auto &layer)
+		[&variableDeclarationMatches](const auto &layer)
 		{
 			return (std::find_if(layer->cbegin(), layer->cend(), variableDeclarationMatches) != layer->cend());
 		};
@@ -178,6 +178,11 @@ struct CollectFreeVariablesVisitor
 	{
 	}

+	void visit(UnaryOperation &unaryOperation, VariableStack &variableStack, std::vector<VariableDeclaration *> &freeVariables)
+	{
+		unaryOperation.argument.accept(*this, variableStack, freeVariables);
+	}
+
 	void visit(Variable &variable, VariableStack &variableStack, std::vector<VariableDeclaration *> &freeVariables)
 	{
 		if (variableStack.contains(*variable.declaration))
@@ -194,7 +199,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 +211,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 +268,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);
 }

 ////////////////////////////////////////////////////////////////////////////////////////////////////
--- a/src/anthem/Completion.cpp
+++ b/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)
--- a/src/anthem/HiddenPredicateElimination.cpp
+++ b/src/anthem/HiddenPredicateElimination.cpp
@@ -194,41 +194,40 @@ void eliminateHiddenPredicates(const std::vector<ast::PredicateSignature> &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 << "”";

--- a/src/anthem/Simplification.cpp
+++ b/src/anthem/Simplification.cpp
@@ -1,9 +1,11 @@
 #include <anthem/Simplification.h>

-#include <experimental/optional>
+#include <optional>

 #include <anthem/ASTCopy.h>
-#include <anthem/ASTVisitors.h>
+#include <anthem/Equality.h>
+#include <anthem/output/AST.h>
+#include <anthem/SimplificationVisitors.h>

 namespace anthem
 {
@@ -27,15 +29,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 +45,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;
 }

 ////////////////////////////////////////////////////////////////////////////////////////////////////
@@ -97,18 +99,65 @@ struct ReplaceVariableInFormulaVisitor : public ast::RecursiveFormulaVisitor<Rep

 ////////////////////////////////////////////////////////////////////////////////////////////////////

-// Simplifies exists statements by using the equivalence “exists X (X = t and F(X))” == “F(t)”
-// The exists statement has to be of the form “exists <variables> <conjunction>”
-void simplify(ast::Exists &exists, ast::Formula &formula)
+template<class SimplificationRule>
+SimplificationResult simplify(ast::Formula &formula)
 {
-	// Simplify formulas like “exists X (X = Y)” to “#true”
-	// TODO: check that this covers all cases
-	if (exists.argument.is<ast::Comparison>())
+	return SimplificationRule::apply(formula);
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+template<class FirstSimplificationRule, class SecondSimplificationRule, class... OtherSimplificationRules>
+SimplificationResult simplify(ast::Formula &formula)
+{
+	if (simplify<FirstSimplificationRule>(formula) == SimplificationResult::Simplified)
+		return SimplificationResult::Simplified;
+
+	return simplify<SecondSimplificationRule, OtherSimplificationRules...>(formula);
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+struct SimplificationRuleExistsWithoutQuantifiedVariables
+{
+	static constexpr const auto Description = "exists () (F) === F";
+
+	static SimplificationResult apply(ast::Formula &formula)
 	{
+		if (!formula.is<ast::Exists>())
+			return SimplificationResult::Unchanged;
+
+		auto &exists = formula.get<ast::Exists>();
+
+		if (!exists.variables.empty())
+			return SimplificationResult::Unchanged;
+
+		formula = std::move(exists.argument);
+
+		return SimplificationResult::Simplified;
+	}
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+struct SimplificationRuleTrivialAssignmentInExists
+{
+	static constexpr const auto Description = "exists X (X = Y) === #true";
+
+	static SimplificationResult apply(ast::Formula &formula)
+	{
+		if (!formula.is<ast::Exists>())
+			return SimplificationResult::Unchanged;
+
+		const auto &exists = formula.get<ast::Exists>();
+
+		if (!exists.argument.is<ast::Comparison>())
+			return SimplificationResult::Unchanged;
+
 		const auto &comparison = exists.argument.get<ast::Comparison>();

 		if (comparison.operator_ != ast::Comparison::Operator::Equal)
-			return;
+			return SimplificationResult::Unchanged;

 		const auto matchingAssignment = std::find_if(exists.variables.cbegin(), exists.variables.cend(),
 			[&](const auto &variableDeclaration)
@@ -117,107 +166,378 @@ void simplify(ast::Exists &exists, ast::Formula &formula)
 					|| matchesVariableDeclaration(comparison.right, *variableDeclaration);
 			});

-		if (matchingAssignment != exists.variables.cend())
-			formula = ast::Formula::make<ast::Boolean>(true);
+		if (matchingAssignment == exists.variables.cend())
+			return SimplificationResult::Unchanged;

-		return;
+		formula = ast::Formula::make<ast::Boolean>(true);
+
+		return SimplificationResult::Simplified;
 	}
+};

-	if (!exists.argument.is<ast::And>())
-		return;
+////////////////////////////////////////////////////////////////////////////////////////////////////

-	auto &conjunction = exists.argument.get<ast::And>();
-	auto &arguments = conjunction.arguments;
+struct SimplificationRuleAssignmentInExists
+{
+	static constexpr const auto Description = "exists X (X = t and F(X)) === exists () (F(t))";

-	// Simplify formulas of type “exists X (X = t and F(X))” to “F(t)”
-	for (auto i = exists.variables.begin(); i != exists.variables.end();)
+	static SimplificationResult apply(ast::Formula &formula)
 	{
-		const auto &variableDeclaration = **i;
+		if (!formula.is<ast::Exists>())
+			return SimplificationResult::Unchanged;

-		bool wasVariableReplaced = false;
+		auto &exists = formula.get<ast::Exists>();

-		// TODO: refactor
-		for (auto j = arguments.begin(); j != arguments.end(); j++)
+		if (!exists.argument.is<ast::And>())
+			return SimplificationResult::Unchanged;
+
+		auto &and_ = exists.argument.get<ast::And>();
+		auto &arguments = and_.arguments;
+
+		auto simplificationResult = SimplificationResult::Unchanged;
+
+		for (auto i = exists.variables.begin(); i != exists.variables.end();)
 		{
-			auto &argument = *j;
-			// Find term that is equivalent to the given variable
-			auto assignedTerm = extractAssignedTerm(argument, variableDeclaration);
+			const auto &variableDeclaration = **i;

-			if (!assignedTerm)
-				continue;
+			bool wasVariableReplaced = false;

-			// Replace all occurrences of the variable with the equivalent term
-			for (auto k = arguments.begin(); k != arguments.end(); k++)
+			// TODO: refactor
+			for (auto j = arguments.begin(); j != arguments.end(); j++)
 			{
-				if (k == j)
+				auto &argument = *j;
+				// Find term that is equivalent to the given variable
+				auto assignedTerm = extractAssignedTerm(argument, variableDeclaration);
+
+				if (!assignedTerm)
 					continue;

-				auto &otherArgument = *k;
-				otherArgument.accept(ReplaceVariableInFormulaVisitor(), otherArgument, variableDeclaration, assignedTerm.value());
+				// Replace all occurrences of the variable with the equivalent term
+				for (auto k = arguments.begin(); k != arguments.end(); k++)
+				{
+					if (k == j)
+						continue;
+
+					auto &otherArgument = *k;
+					otherArgument.accept(ReplaceVariableInFormulaVisitor(), otherArgument, variableDeclaration, assignedTerm.value());
+				}
+
+				arguments.erase(j);
+
+				wasVariableReplaced = true;
+				simplificationResult = SimplificationResult::Simplified;
+
+				break;
 			}

-			arguments.erase(j);
-			wasVariableReplaced = true;
-			break;
+			if (wasVariableReplaced)
+			{
+				i = exists.variables.erase(i);
+				continue;
+			}
+
+			i++;
 		}

-		if (wasVariableReplaced)
-		{
-			i = exists.variables.erase(i);
-			continue;
-		}
-
-		i++;
+		return simplificationResult;
 	}
+};

-	// If there are no arguments left, we had a formula of the form “exists X1, ..., Xn (X1 = Y1 and ... and Xn = Yn)”
-	// Such exists statements are useless and can be safely replaced with “#true”
-	if (arguments.empty())
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+struct SimplificationRuleEmptyConjunction
+{
+	static constexpr const auto Description = "[empty conjunction] === #true";
+
+	static SimplificationResult apply(ast::Formula &formula)
 	{
+		if (!formula.is<ast::And>())
+			return SimplificationResult::Unchanged;
+
+		auto &and_ = formula.get<ast::And>();
+
+		if (!and_.arguments.empty())
+			return SimplificationResult::Unchanged;
+
 		formula = ast::Formula::make<ast::Boolean>(true);
-		return;
+
+		return SimplificationResult::Simplified;
 	}
+};

-	// If the argument now is a conjunction with just one element, directly replace the input formula with the argument
-	if (arguments.size() == 1)
-		exists.argument = std::move(arguments.front());
+////////////////////////////////////////////////////////////////////////////////////////////////////

-	// If there are still remaining variables, simplification is over
-	if (!exists.variables.empty())
-		return;
+struct SimplificationRuleOneElementConjunction
+{
+	static constexpr const auto Description = "[conjunction of only F] === F";

-	assert(!arguments.empty());
+	static SimplificationResult apply(ast::Formula &formula)
+	{
+		if (!formula.is<ast::And>())
+			return SimplificationResult::Unchanged;

-	// If there is more than one element in the conjunction, replace the input formula with the conjunction
-	formula = std::move(exists.argument);
-}
+		auto &and_ = formula.get<ast::And>();
+
+		if (and_.arguments.size() != 1)
+			return SimplificationResult::Unchanged;
+
+		formula = std::move(and_.arguments.front());
+
+		return SimplificationResult::Simplified;
+	}
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+struct SimplificationRuleTrivialExists
+{
+	static constexpr const auto Description = "exists ... ([#true/#false]) === [#true/#false]";
+
+	static SimplificationResult apply(ast::Formula &formula)
+	{
+		if (!formula.is<ast::Exists>())
+			return SimplificationResult::Unchanged;
+
+		auto &exists = formula.get<ast::Exists>();
+
+		if (!exists.argument.is<ast::Boolean>())
+			return SimplificationResult::Unchanged;
+
+		formula = std::move(exists.argument);
+
+		return SimplificationResult::Simplified;
+	}
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+struct SimplificationRuleInWithPrimitiveArguments
+{
+	static constexpr const auto Description = "[primitive A] in [primitive B] === A = B";
+
+	static SimplificationResult apply(ast::Formula &formula)
+	{
+		if (!formula.is<ast::In>())
+			return SimplificationResult::Unchanged;
+
+		auto &in = formula.get<ast::In>();
+
+		assert(ast::isPrimitive(in.element));
+
+		if (!ast::isPrimitive(in.element) || !ast::isPrimitive(in.set))
+			return SimplificationResult::Unchanged;
+
+		formula = ast::Comparison(ast::Comparison::Operator::Equal, std::move(in.element), std::move(in.set));
+
+		return SimplificationResult::Simplified;
+	}
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+struct SimplificationRuleSubsumptionInBiconditionals
+{
+	static constexpr const auto Description = "(F <-> (F and G)) === (F -> G)";
+
+	static SimplificationResult apply(ast::Formula &formula)
+	{
+		if (!formula.is<ast::Biconditional>())
+			return SimplificationResult::Unchanged;
+
+		auto &biconditional = formula.get<ast::Biconditional>();
+
+		const auto leftIsPredicate = biconditional.left.is<ast::Predicate>();
+		const auto rightIsPredicate = biconditional.right.is<ast::Predicate>();
+
+		const auto leftIsAnd = biconditional.left.is<ast::And>();
+		const auto rightIsAnd = biconditional.right.is<ast::And>();
+
+		if (!(leftIsPredicate && rightIsAnd) && !(rightIsPredicate && leftIsAnd))
+			return SimplificationResult::Unchanged;
+
+		auto &predicateSide = (leftIsPredicate ? biconditional.left : biconditional.right);
+		auto &andSide = (leftIsPredicate ? biconditional.right : biconditional.left);
+		auto &and_ = andSide.get<ast::And>();
+
+		const auto matchingPredicate =
+			std::find_if(and_.arguments.cbegin(), and_.arguments.cend(),
+			[&](const auto &argument)
+			{
+				return (ast::equal(predicateSide, argument) == ast::Tristate::True);
+			});
+
+		if (matchingPredicate == and_.arguments.cend())
+			return SimplificationResult::Unchanged;
+
+		and_.arguments.erase(matchingPredicate);
+
+		formula = ast::Formula::make<ast::Implies>(std::move(predicateSide), std::move(andSide));
+
+		return SimplificationResult::Simplified;
+	}
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+struct SimplificationRuleDoubleNegation
+{
+	static constexpr const auto Description = "not not F === F";
+
+	static SimplificationResult apply(ast::Formula &formula)
+	{
+		if (!formula.is<ast::Not>())
+			return SimplificationResult::Unchanged;
+
+		auto &not_ = formula.get<ast::Not>();
+
+		if (!not_.argument.is<ast::Not>())
+			return SimplificationResult::Unchanged;
+
+		auto &notNot = not_.argument.get<ast::Not>();
+
+		formula = std::move(notNot.argument);
+
+		return SimplificationResult::Simplified;
+	}
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+struct SimplificationRuleDeMorganForConjunctions
+{
+	static constexpr const auto Description = "(not (F and G)) === (not F or not G)";
+
+	static SimplificationResult apply(ast::Formula &formula)
+	{
+		if (!formula.is<ast::Not>())
+			return SimplificationResult::Unchanged;
+
+		auto &not_ = formula.get<ast::Not>();
+
+		if (!not_.argument.is<ast::And>())
+			return SimplificationResult::Unchanged;
+
+		auto &and_ = not_.argument.get<ast::And>();
+
+		for (auto &argument : and_.arguments)
+			argument = ast::Formula::make<ast::Not>(std::move(argument));
+
+		formula = ast::Formula::make<ast::Or>(std::move(and_.arguments));
+
+		return SimplificationResult::Simplified;
+	}
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+struct SimplificationRuleImplicationFromDisjunction
+{
+	static constexpr const auto Description = "(not F or G) === (F -> G)";
+
+	static SimplificationResult apply(ast::Formula &formula)
+	{
+		if (!formula.is<ast::Or>())
+			return SimplificationResult::Unchanged;
+
+		auto &or_ = formula.get<ast::Or>();
+
+		if (or_.arguments.size() != 2)
+			return SimplificationResult::Unchanged;
+
+		const auto leftIsNot = or_.arguments[0].is<ast::Not>();
+		const auto rightIsNot = or_.arguments[1].is<ast::Not>();
+
+		if (leftIsNot == rightIsNot)
+			return SimplificationResult::Unchanged;
+
+		auto &negativeSide = leftIsNot ? or_.arguments[0] : or_.arguments[1];
+		auto &positiveSide = leftIsNot ? or_.arguments[1] : or_.arguments[0];
+
+		assert(negativeSide.is<ast::Not>());
+		assert(!positiveSide.is<ast::Not>());
+
+		auto &negativeSideArgument = negativeSide.get<ast::Not>().argument;
+
+		formula = ast::Formula::make<ast::Implies>(std::move(negativeSideArgument), std::move(positiveSide));
+
+		return SimplificationResult::Simplified;
+	}
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+struct SimplificationRuleNegatedComparison
+{
+	static constexpr const auto Description = "(not F [comparison] G) === (F [negated comparison] G)";
+
+	static SimplificationResult apply(ast::Formula &formula)
+	{
+		if (!formula.is<ast::Not>())
+			return SimplificationResult::Unchanged;
+
+		auto &not_ = formula.get<ast::Not>();
+
+		if (!not_.argument.is<ast::Comparison>())
+			return SimplificationResult::Unchanged;
+
+		auto &comparison = not_.argument.get<ast::Comparison>();
+
+		switch (comparison.operator_)
+		{
+			case ast::Comparison::Operator::GreaterThan:
+				comparison.operator_ = ast::Comparison::Operator::LessEqual;
+				break;
+			case ast::Comparison::Operator::LessThan:
+				comparison.operator_ = ast::Comparison::Operator::GreaterEqual;
+				break;
+			case ast::Comparison::Operator::LessEqual:
+				comparison.operator_ = ast::Comparison::Operator::GreaterThan;
+				break;
+			case ast::Comparison::Operator::GreaterEqual:
+				comparison.operator_ = ast::Comparison::Operator::LessThan;
+				break;
+			case ast::Comparison::Operator::NotEqual:
+				comparison.operator_ = ast::Comparison::Operator::Equal;
+				break;
+			case ast::Comparison::Operator::Equal:
+				comparison.operator_ = ast::Comparison::Operator::NotEqual;
+				break;
+		}
+
+		formula = std::move(comparison);
+
+		return SimplificationResult::Simplified;
+	}
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+const auto simplifyWithDefaultRules =
+	simplify
+	<
+		SimplificationRuleDoubleNegation,
+		SimplificationRuleTrivialAssignmentInExists,
+		SimplificationRuleAssignmentInExists,
+		SimplificationRuleEmptyConjunction,
+		SimplificationRuleTrivialExists,
+		SimplificationRuleOneElementConjunction,
+		SimplificationRuleExistsWithoutQuantifiedVariables,
+		SimplificationRuleInWithPrimitiveArguments,
+		SimplificationRuleSubsumptionInBiconditionals,
+		SimplificationRuleDeMorganForConjunctions,
+		SimplificationRuleImplicationFromDisjunction,
+		SimplificationRuleNegatedComparison
+	>;

 ////////////////////////////////////////////////////////////////////////////////////////////////////

 // Performs the different simplification techniques
-struct SimplifyFormulaVisitor : public ast::RecursiveFormulaVisitor<SimplifyFormulaVisitor>
+struct SimplifyFormulaVisitor : public ast::FormulaSimplificationVisitor<SimplifyFormulaVisitor>
 {
-	// Forward exists statements to the dedicated simplification function
-	static void accept(ast::Exists &exists, ast::Formula &formula)
-	{
-		simplify(exists, formula);
-	}
-
-	// Simplify formulas of type “A in B” to “A = B” if A and B are primitive
-	static void accept(ast::In &in, ast::Formula &formula)
-	{
-		assert(ast::isPrimitive(in.element));
-
-		if (!ast::isPrimitive(in.element) || !ast::isPrimitive(in.set))
-			return;
-
-		formula = ast::Comparison(ast::Comparison::Operator::Equal, std::move(in.element), std::move(in.set));
-	}
-
 	// Do nothing for all other types of expressions
-	template<class T>
-	static void accept(T &, ast::Formula &)
+	static SimplificationResult accept(ast::Formula &formula)
 	{
+		return simplifyWithDefaultRules(formula);
 	}
 };

@@ -225,7 +545,7 @@ struct SimplifyFormulaVisitor : public ast::RecursiveFormulaVisitor<SimplifyForm

 void simplify(ast::Formula &formula)
 {
-	formula.accept(SimplifyFormulaVisitor(), formula);
+	while (formula.accept(SimplifyFormulaVisitor(), formula) == SimplificationResult::Simplified);
 }

 ////////////////////////////////////////////////////////////////////////////////////////////////////
--- 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)
--- a/tests/TestCompletion.cpp
+++ b/tests/TestCompletion.cpp
@@ -152,9 +152,9 @@ TEST_CASE("[completion] Rules are completed", "[completion]")

 		CHECK(output.str() ==
 			"forall V1 (covered(V1) <-> exists U1 in(V1, U1))\n"
-			"forall V2, V3 (in(V2, V3) <-> (V2 in 1..n and V3 in 1..r and in(V2, V3)))\n"
-			"forall U2 not (U2 in 1..n and not covered(U2))\n"
-			"forall U3, U4, U5 not (in(U3, U4) and in(U5, U4) and exists X1 (X1 in (U3 + U5) and in(X1, U4)))\n");
+			"forall V2, V3 (in(V2, V3) -> (V2 in 1..n and V3 in 1..r))\n"
+			"forall U2 (U2 in 1..n -> covered(U2))\n"
+			"forall U3, U4, U5 (not in(U3, U4) or not in(U5, U4) or not exists X1 (X1 in (U3 + U5) and in(X1, U4)))\n");
 	}

 	SECTION("binary operations with multiple variables")
@@ -176,4 +176,20 @@ TEST_CASE("[completion] Rules are completed", "[completion]")
 		CHECK(output.str() ==
 			"forall V1, V2, V3 (p(V1, V2, V3) <-> #true)\n");
 	}
+
+	SECTION("negated comparisons")
+	{
+		input << ":- color(V, C1), color(V, C2), C1 != C2.";
+		anthem::translate("input", input, context);
+
+		CHECK(output.str() == "forall V1, V2 not color(V1, V2)\nforall U1, U2, U3 (not color(U1, U2) or not color(U1, U3) or U2 = U3)\n");
+	}
+
+	SECTION("absolute value operation")
+	{
+		input << "adj(X, Y) :- X = 1..n, Y = 1..n, |X - Y| = 1.";
+		anthem::translate("input", input, context);
+
+		CHECK(output.str() == "forall V1, V2 (adj(V1, V2) <-> (V1 in 1..n and V2 in 1..n and |V1 - V2| = 1))\n");
+	}
 }
--- a/tests/TestHiddenPredicateElimination.cpp
+++ b/tests/TestHiddenPredicateElimination.cpp
@@ -103,9 +103,10 @@ TEST_CASE("[hidden predicate elimination] Hidden predicates are correctly elimin
 			"#show a/1.";
 		anthem::translate("input", input, context);

+		// TODO: simplify further
 		CHECK(output.str() ==
 			"forall V1 (a(V1) <-> not d(V1))\n"
-			"forall V2 (d(V2) <-> not not d(V2))\n"
+			"forall V2 (d(V2) <-> d(V2))\n"
 			"forall V3 (e(V3) <-> e(V3))\n");
 	}

@@ -164,12 +165,11 @@ TEST_CASE("[hidden predicate elimination] Hidden predicates are correctly elimin
 			"#show t/0.";
 		anthem::translate("input", input, context);

-		// TODO: simplify further
 		CHECK(output.str() ==
-			"(s <-> (not #false and s))\n"
-			"(t <-> (not #false and t))\n"
-			"not (s and not t)\n"
-			"not (not #false and not #false and #false)\n");
+			"(s -> not #false)\n"
+			"(t -> not #false)\n"
+			"(s -> t)\n"
+			"(#false or #false or not #false)\n");
 	}

 	SECTION("predicate with more than one argument is hidden correctly")
--- a/tests/TestPlaceholders.cpp
+++ b/tests/TestPlaceholders.cpp
@@ -0,0 +1,62 @@
+#include <catch.hpp>
+
+#include <sstream>
+
+#include <anthem/AST.h>
+#include <anthem/Context.h>
+#include <anthem/Translation.h>
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+TEST_CASE("[placeholders] Programs with placeholders are correctly completed", "[placeholders]")
+{
+	std::stringstream input;
+	std::stringstream output;
+	std::stringstream errors;
+
+	anthem::output::Logger logger(output, errors);
+	anthem::Context context(std::move(logger));
+	context.performSimplification = true;
+	context.performCompletion = true;
+
+	SECTION("no placeholders")
+	{
+		input <<
+			"colored(V, red) :- vertex(V), not colored(V, green), not colored(V, blue).";
+		anthem::translate("input", input, context);
+
+		CHECK(output.str() ==
+			"forall V1, V2 (colored(V1, V2) <-> (V2 = red and vertex(V1) and not colored(V1, green) and not colored(V1, blue)))\n"
+			"forall V3 not vertex(V3)\n");
+	}
+
+	SECTION("single placeholder")
+	{
+		input <<
+			"#external vertex(1).\n"
+			"colored(V, red) :- vertex(V), not colored(V, green), not colored(V, blue).";
+		anthem::translate("input", input, context);
+
+		CHECK(output.str() ==
+			"forall V1, V2 (colored(V1, V2) <-> (V2 = red and vertex(V1) and not colored(V1, green) and not colored(V1, blue)))\n");
+	}
+
+	SECTION("complex example: graph coloring")
+	{
+		input <<
+			"#external color(1).\n"
+			"#external edge(2).\n"
+			"#external vertex(1).\n"
+			"#show color/2.\n"
+			"{color(V, C)} :- vertex(V), color(C).\n"
+			"covered(V) :- color(V, _).\n"
+			":- vertex(V), not covered(V).\n"
+			":- color(V1, C), color(V2, C), edge(V1, V2).";
+		anthem::translate("input", input, context);
+
+		CHECK(output.str() ==
+			"forall V1, V2 (color(V1, V2) -> (vertex(V1) and color(V2)))\n"
+			"forall U1 (vertex(U1) -> exists U2 color(U1, U2))\n"
+			"forall U3, U4, U5 (not color(U3, U4) or not color(U5, U4) or not edge(U3, U5))\n");
+	}
+}
--- a/tests/TestTranslation.cpp
+++ b/tests/TestTranslation.cpp
@@ -296,4 +296,12 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]")

 		CHECK(output.str() == "((V1 in U1 and V2 in U2 and exists X1, X2 (X1 in U3 and X2 in U4 and q(X1, X2))) -> p(V1, V2))\n");
 	}
+
+	SECTION("exponentiation operator")
+	{
+		input << "p(N, N ** N) :- N = 1..n.";
+		anthem::translate("input", input, context);
+
+		CHECK(output.str() == "((V1 in U1 and V2 in (U1 ** U1) and exists X1, X2 (X1 in U1 and X2 in 1..n and X1 = X2)) -> p(V1, V2))\n");
+	}
 }
Author	SHA1	Message	Date
Patrick Lühne	ec88d26922	Version bump for release 0.1.8 RC 3	2018-04-12 01:06:28 +02:00
Patrick Lühne	04094eee23	Remove unnecessary parentheses The unary modulus operation does not require extra parentheses to be printed in cases like “\|X + Y\|”. This adds a new option to the printing routine to omit parentheses in cases where the parent expression already defines a parenthesis-like scope (currently only with unary operations).	2018-04-12 00:59:03 +02:00
Patrick Lühne	8c250f5c59	Support modulus operation (absolute value) This adds support for computing the absolute value of a term along with an according unit test.	2018-04-12 00:38:48 +02:00
Patrick Lühne	0608748349	Describe --complete option in readme The readme was missing information on the --complete option. This adds a brief mention of Clark’s completion to the readme.	2018-04-11 23:21:56 +02:00
Patrick Lühne	31d4a20491	Update change log with recent additions This updates the change log with the advanced simplification rules, support for the exponentation operator, and the newly added examples.	2018-04-11 21:50:15 +02:00
Patrick Lühne	a01e78a467	Add example program for prime number detection	2018-04-11 21:42:08 +02:00
Patrick Lühne	797660d6de	Add new simplification rule This adds the rule “(not F [comparison] G) === (F [negated comparison] G)” to the simplification rule tableau.	2018-04-11 21:39:27 +02:00
Patrick Lühne	b63ef21849	Add example program generating permutations	2018-04-11 21:35:29 +02:00
Patrick Lühne	cc3c9b642c	Minor formatting in graph coloring example	2018-04-11 21:35:04 +02:00
Patrick Lühne	40ddee8444	Add new simplification rule This adds the rule “(not F or G) === (F -> G)” to the simplification rule tableau.	2018-04-10 22:34:47 +02:00
Patrick Lühne	6f7b021712	Add new simplification rule This adds the rule “(not (F and G)) === (not F or not G)” to the simplification rule tableau.	2018-04-10 22:34:47 +02:00
Patrick Lühne	23624007ec	Add new simplification rule This adds the rule “not not F === F” to the simplification rule tableau.	2018-04-10 22:34:47 +02:00
Patrick Lühne	6d7b91c391	Add new simplification rule This adds the rule “(F <-> (F and G)) === (F -> G)” to the simplification rule tableau.	2018-04-10 22:34:47 +02:00
Patrick Lühne	b88393655a	Iteratively apply simplification tableau rules With this change, the tableau rules for simplifying formula are applied iteratively until a fixpoint is reached.	2018-04-10 22:34:47 +02:00
Patrick Lühne	c4c3156e77	Move simplification rule to tableau This moves the rule “[primitive A] in [primitive B] === A = B” to the simplification rule tableau.	2018-04-10 22:34:47 +02:00
Patrick Lühne	107dae7287	Move simplification rule to tableau This moves the rule “exists () (F) === F” to the simplification rule tableau.	2018-04-10 22:34:47 +02:00
Patrick Lühne	827d6e40fe	Move simplification rule to tableau This moves the rule “[conjunction of only F] === F” to the simplification rule tableau.	2018-04-10 22:34:47 +02:00
Patrick Lühne	4a85fc4b23	Move simplification rule to tableau This moves the rule “exists ... ([#true/#false]) === [#true/#false]” to the simplification rule tableau along with “[empty conjunction] ===	2018-04-10 22:34:46 +02:00
Patrick Lühne	7e3fc007c8	Move simplification rule to tableau This moves the rule “exists X (X = t and F(X)) === exists () (F(t))” to the simplification rule tableau.	2018-04-10 22:34:46 +02:00
Patrick Lühne	5c5411c0ff	Implement simplification rule tableau This implements a tableau containing simplification rules that can be iteratively applied to input formulas until they remain unchanged. First, this moves the rule “exists X (X = Y) === #true” to the tableau as a reference implementation.	2018-04-10 22:34:46 +02:00
Patrick Lühne	eaabeb0c55	Support exponentiation operator Because of a bug in the Clingo API, the exponentation operator was not properly exposed to anthem. This updates Clingo to a version with a fixed API and adds proper support for exponentation within anthem along with a matching unit test.	2018-04-10 22:29:55 +02:00
Patrick Lühne	7b6729acaa	Add missing dependency to Ubuntu image For some reason, Bison is not implicitly installed along with the other dependencies in the Ubuntu 18.04 image used for continuous integration. This adds Bison explicitly.	2018-04-10 22:29:55 +02:00
Patrick Lühne	92fddd6665	Version bump after release 0.1.7	2018-04-08 21:03:20 +02:00
Patrick Lühne	582b6ade6d	Version bump for release 0.1.7	2018-04-08 20:44:43 +02:00
Patrick Lühne	e64b2e70de	Remove unused captured lambda reference	2018-04-08 20:44:43 +02:00
Patrick Lühne	d7e4af98d7	Update copyright year in license file	2018-04-08 20:35:03 +02:00
Patrick Lühne	a406cb43bd	Update graph coloring example with placeholders This replaces the former graph coloring example with a new formulation that makes use of the newly supported placeholders.	2018-04-08 20:28:57 +02:00
Patrick Lühne	c294a29cb2	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 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 program: #external <predicate name>(<arity>). Multiple unit tests cover cases where placeholders are used or not as well as a more complex graph coloring example.	2018-04-08 20:28:57 +02:00
Patrick Lühne	c91cbaf58b	Update Catch to 2.2.2	2018-04-07 00:22:01 +02:00
Patrick Lühne	2a2fec0eac	Update change log with dependency change This adds the dependency change from Boost (for program options) to cxxopts to the change log.	2018-04-06 23:08:57 +02:00
Patrick Lühne	09e56c3bce	Format change log sections with proper headings This makes the change log sections have proper headings, which were just normal text before.	2018-04-06 22:53:59 +02:00
Patrick Lühne	e2c0d6b705	Update cxxopts to 2.0.0+3+gabe9ebd With cxxopts 2.0.0, positional arguments weren’t recognized when other command-line options were passed before. This has been fixed in the meantime, but there is no release with the bug fix yet. This updates cxxopts to a newer commit to ship anthem with this fix.	2018-04-06 22:44:14 +02:00
Patrick Lühne	e01506f9ff	Drop Boost dependency Boost was only used for program option parsing. To avoid this huge dependency, this commit replaces boost::program_options with cxxopts, a header-only library with the same functionality. cxxopts is added as a submodule, and Boost is removed from the dependencies in the code and Travis configuration.	2018-03-25 17:24:06 +02:00
Patrick Lühne	50ebf3c6de	Install g++ package explicitly on Ubuntu Apparently, g++ is only installed because of the Boost dependency. Make the g++ dependency explicit to avoid future package errors.	2018-03-25 17:23:33 +02:00
Patrick Lühne	fde2af5841	Add clang to Travis configurations This adds the clang compiler to the tested Travis configurations.	2018-03-24 18:53:51 +01:00
Patrick Lühne	22238bb398	Switch to C++17 With C++17, optionals, an experimental language feature, were moved to the “std” namespace. This makes C++17 mandatory and drops the now obsolete “experimental” namespace.	2018-03-24 16:09:52 +01:00
Patrick Lühne	c7d1026a31	Switch Travis to Docker As Travis only provides outdated packages (compilers in particular), this changes the Travis configuration to use Docker images to build and test the code. This also has the benefit that multiple distributions can be tested and not just Ubuntu. For the time being, Arch Linux and Ubuntu 18.04 are added as supported platforms.	2018-03-24 15:51:20 +01:00
Patrick Lühne	6b1cf6735e	Update clingo to 5.2.2	2018-03-21 16:41:08 +01:00
Patrick Lühne	addc65e3c5	Update Catch to 2.2.1	2018-03-21 16:35:54 +01:00